114 *) |
114 *) |
115 fun make_hyp_def thm ctxt = |
115 fun make_hyp_def thm ctxt = |
116 let |
116 let |
117 val (lhs, rhs) = Thm.dest_binop (Thm.cprem_of thm 1) |
117 val (lhs, rhs) = Thm.dest_binop (Thm.cprem_of thm 1) |
118 val (cf, cvs) = Drule.strip_comb lhs |
118 val (cf, cvs) = Drule.strip_comb lhs |
119 val eq = SMT_Utils.mk_cequals cf (fold_rev Thm.cabs cvs rhs) |
119 val eq = SMT_Utils.mk_cequals cf (fold_rev Thm.lambda cvs rhs) |
120 fun apply cv th = |
120 fun apply cv th = |
121 Thm.combination th (Thm.reflexive cv) |
121 Thm.combination th (Thm.reflexive cv) |
122 |> Conv.fconv_rule (Conv.arg_conv (Thm.beta_conversion false)) |
122 |> Conv.fconv_rule (Conv.arg_conv (Thm.beta_conversion false)) |
123 in |
123 in |
124 yield_singleton Assumption.add_assumes eq ctxt |
124 yield_singleton Assumption.add_assumes eq ctxt |
157 let |
157 let |
158 val (n, ctxt') = yield_singleton Variable.variant_fixes "x" ctxt |
158 val (n, ctxt') = yield_singleton Variable.variant_fixes "x" ctxt |
159 val cv = SMT_Utils.certify ctxt' |
159 val cv = SMT_Utils.certify ctxt' |
160 (Free (n, map SMT_Utils.typ_of cvs' ---> SMT_Utils.typ_of ct)) |
160 (Free (n, map SMT_Utils.typ_of cvs' ---> SMT_Utils.typ_of ct)) |
161 val cu = Drule.list_comb (cv, cvs') |
161 val cu = Drule.list_comb (cv, cvs') |
162 val e = (t, (cv, fold_rev Thm.cabs cvs' ct)) |
162 val e = (t, (cv, fold_rev Thm.lambda cvs' ct)) |
163 val beta_norm' = beta_norm orelse not (null cvs') |
163 val beta_norm' = beta_norm orelse not (null cvs') |
164 in (cu, (ctxt', Termtab.update e tab, idx + 1, beta_norm')) end) |
164 in (cu, (ctxt', Termtab.update e tab, idx + 1, beta_norm')) end) |
165 end |
165 end |
166 |
166 |
167 fun abs_comb f g dcvs ct = |
167 fun abs_comb f g dcvs ct = |
168 let val (cf, cu) = Thm.dest_comb ct |
168 let val (cf, cu) = Thm.dest_comb ct |
169 in f dcvs cf ##>> g dcvs cu #>> uncurry Thm.capply end |
169 in f dcvs cf ##>> g dcvs cu #>> uncurry Thm.apply end |
170 |
170 |
171 fun abs_arg f = abs_comb (K pair) f |
171 fun abs_arg f = abs_comb (K pair) f |
172 |
172 |
173 fun abs_args f dcvs ct = |
173 fun abs_args f dcvs ct = |
174 (case Thm.term_of ct of |
174 (case Thm.term_of ct of |
182 abs_comb (abs_arg f) (abs_list f g) dcvs ct |
182 abs_comb (abs_arg f) (abs_list f g) dcvs ct |
183 | _ => g dcvs ct) |
183 | _ => g dcvs ct) |
184 |
184 |
185 fun abs_abs f (depth, cvs) ct = |
185 fun abs_abs f (depth, cvs) ct = |
186 let val (cv, cu) = Thm.dest_abs NONE ct |
186 let val (cv, cu) = Thm.dest_abs NONE ct |
187 in f (depth, cv :: cvs) cu #>> Thm.cabs cv end |
187 in f (depth, cv :: cvs) cu #>> Thm.lambda cv end |
188 |
188 |
189 val is_atomic = |
189 val is_atomic = |
190 (fn Free _ => true | Var _ => true | Bound _ => true | _ => false) |
190 (fn Free _ => true | Var _ => true | Bound _ => true | _ => false) |
191 |
191 |
192 fun abstract depth (ext_logic, with_theories) = |
192 fun abstract depth (ext_logic, with_theories) = |