103 val beta_eta_conversion: cterm -> thm |
103 val beta_eta_conversion: cterm -> thm |
104 val eta_long_conversion: cterm -> thm |
104 val eta_long_conversion: cterm -> thm |
105 val forall_conv: int -> (cterm -> thm) -> cterm -> thm |
105 val forall_conv: int -> (cterm -> thm) -> cterm -> thm |
106 val concl_conv: int -> (cterm -> thm) -> cterm -> thm |
106 val concl_conv: int -> (cterm -> thm) -> cterm -> thm |
107 val prems_conv: int -> (int -> cterm -> thm) -> cterm -> thm |
107 val prems_conv: int -> (int -> cterm -> thm) -> cterm -> thm |
|
108 val mk_conjunction: cterm * cterm -> cterm |
108 val conjunction_cong: thm -> thm -> thm |
109 val conjunction_cong: thm -> thm -> thm |
109 val conjunction_conv: int -> (int -> cterm -> thm) -> cterm -> thm |
110 val conjunction_conv: int -> (int -> cterm -> thm) -> cterm -> thm |
110 val goals_conv: (int -> bool) -> (cterm -> thm) -> cterm -> thm |
111 val goals_conv: (int -> bool) -> (cterm -> thm) -> cterm -> thm |
111 val fconv_rule: (cterm -> thm) -> thm -> thm |
112 val fconv_rule: (cterm -> thm) -> thm -> thm |
112 val norm_hhf_eq: thm |
113 val norm_hhf_eq: thm |
141 val conj_intr: thm -> thm -> thm |
142 val conj_intr: thm -> thm -> thm |
142 val conj_intr_list: thm list -> thm |
143 val conj_intr_list: thm list -> thm |
143 val conj_elim: thm -> thm * thm |
144 val conj_elim: thm -> thm * thm |
144 val conj_elim_list: thm -> thm list |
145 val conj_elim_list: thm -> thm list |
145 val conj_elim_precise: int list -> thm -> thm list list |
146 val conj_elim_precise: int list -> thm -> thm list list |
146 val conj_curry: thm -> thm |
147 val conj_uncurry: int -> thm -> thm |
147 val abs_def: thm -> thm |
148 val abs_def: thm -> thm |
148 val read_instantiate_sg': theory -> (indexname * string) list -> thm -> thm |
149 val read_instantiate_sg': theory -> (indexname * string) list -> thm -> thm |
149 val read_instantiate': (indexname * string) list -> thm -> thm |
150 val read_instantiate': (indexname * string) list -> thm -> thm |
150 end; |
151 end; |
151 |
152 |
195 |
196 |
196 fun ctyp_fun f cT = |
197 fun ctyp_fun f cT = |
197 let val {T, thy, ...} = Thm.rep_ctyp cT |
198 let val {T, thy, ...} = Thm.rep_ctyp cT |
198 in Thm.ctyp_of thy (f T) end; |
199 in Thm.ctyp_of thy (f T) end; |
199 |
200 |
|
201 val conjunction = cterm_of ProtoPure.thy Logic.conjunction; |
200 val implies = cterm_of ProtoPure.thy Term.implies; |
202 val implies = cterm_of ProtoPure.thy Term.implies; |
201 |
203 |
202 (*cterm version of mk_implies*) |
204 fun mk_implies (A, B) = Thm.capply (Thm.capply implies A) B; |
203 fun mk_implies(A,B) = Thm.capply (Thm.capply implies A) B; |
205 fun mk_conjunction (A, B) = Thm.capply (Thm.capply conjunction A) B; |
204 |
206 |
205 (*cterm version of list_implies: [A1,...,An], B goes to [|A1;==>;An|]==>B *) |
207 (*cterm version of list_implies: [A1,...,An], B goes to [|A1;==>;An|]==>B *) |
206 fun list_implies([], B) = B |
208 fun list_implies([], B) = B |
207 | list_implies(A::AS, B) = mk_implies (A, list_implies(AS,B)); |
209 | list_implies(A::AS, B) = mk_implies (A, list_implies(AS,B)); |
208 |
210 |
1179 | elims _ _ = []; |
1180 | elims _ _ = []; |
1180 in elims spans o elim (length (filter_out (equal 0) spans)) end; |
1181 in elims spans o elim (length (filter_out (equal 0) spans)) end; |
1181 |
1182 |
1182 end; |
1183 end; |
1183 |
1184 |
1184 fun conj_curry th = |
1185 (* |
|
1186 A1 ==> ... ==> An ==> B |
|
1187 ----------------------- |
|
1188 A1 && ... && An ==> B |
|
1189 *) |
|
1190 fun conj_uncurry n th = |
1185 let |
1191 let |
1186 val {thy, maxidx, ...} = Thm.rep_thm th; |
1192 val {thy, maxidx, ...} = Thm.rep_thm th; |
1187 val n = Thm.nprems_of th; |
1193 val m = if n = ~1 then Thm.nprems_of th else Int.min (n, Thm.nprems_of th); |
1188 in |
1194 in |
1189 if n < 2 then th |
1195 if m < 2 then th |
1190 else |
1196 else |
1191 let |
1197 let |
1192 val cert = Thm.cterm_of thy; |
1198 val cert = Thm.cterm_of thy; |
1193 val As = map (fn i => Free ("A" ^ string_of_int i, propT)) (1 upto n); |
1199 val As = map (fn i => Free ("A" ^ string_of_int i, propT)) (1 upto m); |
1194 val B = Free ("B", propT); |
1200 val B = Free ("B", propT); |
1195 val C = cert (Logic.mk_conjunction_list As); |
1201 val C = cert (Logic.mk_conjunction_list As); |
1196 val D = cert (Logic.list_implies (As, B)); |
1202 val D = cert (Logic.list_implies (As, B)); |
1197 val rule = |
1203 val rule = |
1198 implies_elim_list (Thm.assume D) (conj_elim_list (Thm.assume C)) |
1204 implies_elim_list (Thm.assume D) (conj_elim_list (Thm.assume C)) |