1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
|
(* ** DATATYPES ** *)
type farg =
Fint of int
| Fstring of string
| Fterm of term
| Ftype of hol_type
| Fthm of finfo
| Fpair of farg * farg
| Flist of farg list
| Ffn of finfo
and finfo =
string option (* Function's name *)
* farg list;; (* Function's args *)
(* finfo_as_meta_arg *)
let finfo_as_meta_arg (info:finfo) =
match info with
(x_, ((_::_) as args))
-> Ffn (x_, front args)
| _ -> failwith "finfo_as_meta_arg: Unexpected empty rule arg list";;
(* Atomic tests *)
let is_atomic_farg arg =
match arg with
Fthm (_,(_::_)) | Fpair _ -> false
| _ -> true;;
let is_atomic_finfo ((x_,args):finfo) = (is_empty args);;
(* active_info *)
let active_info = (Some "...", []);;
(* The 'xthm' datatype *)
(* This couples a theorem with an 'finfo' representation of its proof. For *)
(* named ML objects, this 'finfo' will simply be the ML name of the theorem. *)
(* For rule applications, it will capture the rule and its arguments. *)
type xthm = thm * finfo;;
type xconv = term -> xthm;;
(* Constructors and destructors *)
let mk_xthm (xth:thm*finfo) : xthm = xth;;
let mk_xthm0 x th = mk_xthm (th, (Some x, []));;
let dest_xthm ((th,x):xthm) : thm * finfo = (th,x);;
let xthm_thm ((th,_):xthm) = th;;
let xthm_proof ((_,prf):xthm) = prf;;
(* ** WRAPPER FUNCTIONS ** *)
(* Theorem wrapper *)
let theorem_wrap (x:string) (th:thm) : xthm =
(th, (Some x, []));;
(* Rule wrappers *)
(* Lots of rule wrappers are required because there are many different type *)
(* shapes for rules. *)
let rule_wrap0 finfo (r:'a->thm) (arg:'a) : xthm =
let th' = r arg in
mk_xthm (th',finfo);;
let conv_wrap x (r:term->thm) (tm:term) : xthm =
rule_wrap0 (Some x, [Fterm tm]) r tm;;
let thm_conv_wrap x (r:thm->term->thm) (thx:xthm) tm : xthm =
let (th,prf) = dest_xthm thx in
rule_wrap0 (Some x, [Fthm prf; Fterm tm]) (r th) tm;;
let thmlist_conv_wrap x (r:thm list->term->thm) thxs (tm:term) : xthm =
let (ths,prfs) = unzip (map dest_xthm thxs) in
rule_wrap0 (Some x, [Flist (map (fun prf -> Fthm prf) prfs); Fterm tm])
(r ths) tm;;
let rule_wrap x (r:thm->thm) (thx:xthm) : xthm =
let (th,prf) = dest_xthm thx in
rule_wrap0 (Some x, [Fthm prf]) r th;;
let drule_wrap x (r:thm->thm->thm) (thx1:xthm) (thx2:xthm) : xthm =
let (th1,prf1) = dest_xthm thx1 in
let (th2,prf2) = dest_xthm thx2 in
rule_wrap0 (Some x, [Fthm prf1; Fthm prf2]) (r th1) th2;;
let prule_wrap x (r:thm*thm->thm) ((thx1:xthm),(thx2:xthm)) : xthm =
let (th1,prf1) = dest_xthm thx1 in
let (th2,prf2) = dest_xthm thx2 in
rule_wrap0 (Some x, [Fpair(Fthm prf1, Fthm prf2)]) r (th1,th2);;
let trule_wrap x (r:thm->thm->thm->thm)
(thx1:xthm) (thx2:xthm) (thx3:xthm) : xthm =
let (th1,prf1) = dest_xthm thx1 in
let (th2,prf2) = dest_xthm thx2 in
let (th3,prf3) = dest_xthm thx3 in
rule_wrap0 (Some x, [Fthm prf1; Fthm prf2; Fthm prf3]) (r th1 th2) th3;;
let term_rule_wrap x (r:term->thm->thm) tm (thx:xthm) : xthm =
let (th,prf) = dest_xthm thx in
rule_wrap0 (Some x, [Fterm tm; Fthm prf]) (r tm) th;;
let termpair_rule_wrap x (r:term*term->thm->thm) (tm1,tm2) (thx:xthm) : xthm =
let (th,prf) = dest_xthm thx in
rule_wrap0 (Some x, [Fpair(Fterm tm1,Fterm tm2); Fthm prf]) (r (tm1,tm2)) th;;
let termthmpair_rule_wrap x (r:term*thm->thm->thm) (tm,thx0) (thx:xthm) : xthm =
let (th0,prf0) = dest_xthm thx0 in
let (th,prf) = dest_xthm thx in
rule_wrap0 (Some x, [Fpair(Fterm tm, Fthm prf0); Fthm prf]) (r (tm,th0)) th;;
let termlist_rule_wrap x (r:term list->thm->thm) tms (thx:xthm) : xthm =
let (th,prf) = dest_xthm thx in
rule_wrap0 (Some x, [Flist (map (fun tm -> Fterm tm) tms); Fthm prf])
(r tms) th;;
let terminst_rule_wrap x (r:(term*term)list->thm->thm) theta (thx:xthm) : xthm =
let (th,prf) = dest_xthm thx in
rule_wrap0 (Some x,
[Flist (map (fun (tm1,tm2) -> Fpair(Fterm tm1, Fterm tm2)) theta);
Fthm prf])
(r theta) th;;
let typeinst_rule_wrap x (r:(hol_type*hol_type)list->thm->thm)
theta (thx:xthm) : xthm =
let (th,prf) = dest_xthm thx in
rule_wrap0 (Some x,
[Flist (map (fun (tm1,tm2) -> Fpair(Ftype tm1, Ftype tm2)) theta);
Fthm prf])
(r theta) th;;
let thmlist_rule_wrap x (r:thm list->thm->thm) thxs (thx:xthm) : xthm =
let (ths,prfs) = unzip (map dest_xthm thxs) in
let (th,prf) = dest_xthm thx in
rule_wrap0 (Some x, [Flist (map (fun prf -> Fthm prf) prfs); Fthm prf])
(r ths) th;;
(* Meta rule wrappers *)
(* This works by ... *)
(* Fails to give a meta argument if it never gets executed. *)
let meta_rule_wrap0 finfo0 (mr:('a->thm)->'b->thm)
(xr:'a->xthm) (arg:'b) : xthm =
let temp = ref ((Some "???", []) : finfo) in
let r arg0 = let thx = xr arg0 in
let (th,finfo) = dest_xthm thx in
((match finfo with
(x_, (_::_ as args))
-> (temp := (x_, front args))
| _ -> ());
th) in
let th' = mr r arg in
let (x_,args0) = finfo0 in
let finfo' = (x_, (Ffn !temp)::args0) in
(th',finfo');;
let conv_conv_wrap x (mc:conv->conv) (c:term->xthm) (tm:term) : xthm =
meta_rule_wrap0 (Some x, [Fterm tm]) mc c tm;;
(* ** INSTALL PRINTERS ** *)
let print_xthm ((th,info):xthm) = print_thm th;;
#install_printer print_xthm;;
|
