--- a/src/HOL/Tools/Meson/meson_clausify.ML Sat Apr 13 19:58:28 2019 +0200
+++ b/src/HOL/Tools/Meson/meson_clausify.ML Sat Apr 13 21:43:41 2019 +0200
@@ -94,37 +94,36 @@
| is_quasi_lambda_free (Abs _) = false
| is_quasi_lambda_free _ = true
-(* FIXME: Requires more use of cterm constructors. *)
fun abstract ctxt ct =
let
- val Abs(x,_,body) = Thm.term_of ct
- val Type (\<^type_name>\<open>fun\<close>, [xT,bodyT]) = Thm.typ_of_cterm ct
- val cxT = Thm.ctyp_of ctxt xT
- val cbodyT = Thm.ctyp_of ctxt bodyT
- fun makeK () =
- Thm.instantiate' [SOME cxT, SOME cbodyT] [SOME (Thm.cterm_of ctxt body)] @{thm abs_K}
+ val Abs (_, _, body) = Thm.term_of ct
+ val (x, cbody) = Thm.dest_abs NONE ct
+ val (A, cbodyT) = Thm.dest_ctyp_fun (Thm.ctyp_of_cterm ct)
+ fun makeK () = Thm.instantiate' [SOME A, SOME cbodyT] [SOME cbody] @{thm abs_K}
in
case body of
Const _ => makeK()
| Free _ => makeK()
| Var _ => makeK() (*though Var isn't expected*)
- | Bound 0 => Thm.instantiate' [SOME cxT] [] @{thm abs_I} (*identity: I*)
+ | Bound 0 => Thm.instantiate' [SOME A] [] @{thm abs_I} (*identity: I*)
| rator$rand =>
if Term.is_dependent rator then (*C or S*)
if Term.is_dependent rand then (*S*)
- let val crator = Thm.cterm_of ctxt (Abs (x, xT, rator))
- val crand = Thm.cterm_of ctxt (Abs (x, xT, rand))
- val abs_S' =
- infer_instantiate ctxt [(("f", 0), crator), (("g", 0), crand)] @{thm abs_S}
+ let val crator = Thm.lambda x (Thm.dest_fun cbody)
+ val crand = Thm.lambda x (Thm.dest_arg cbody)
+ val (C, B) = Thm.dest_ctyp_fun (Thm.dest_ctyp_nth 1 (Thm.ctyp_of_cterm crator))
+ val abs_S' = @{thm abs_S}
+ |> instantiate'_normalize [SOME A, SOME B, SOME C] [SOME crator, SOME crand]
val (_,rhs) = Thm.dest_equals (Thm.cprop_of abs_S')
in
Thm.transitive abs_S' (Conv.binop_conv (abstract ctxt) rhs)
end
else (*C*)
- let val crator = Thm.cterm_of ctxt (Abs (x, xT, rator))
- val abs_C' =
- infer_instantiate ctxt [(("f", 0), crator), (("b", 0), Thm.cterm_of ctxt rand)]
- @{thm abs_C}
+ let val crator = Thm.lambda x (Thm.dest_fun cbody)
+ val crand = Thm.dest_arg cbody
+ val (C, B) = Thm.dest_ctyp_fun (Thm.dest_ctyp_nth 1 (Thm.ctyp_of_cterm crator))
+ val abs_C' = @{thm abs_C}
+ |> instantiate'_normalize [SOME A, SOME B, SOME C] [SOME crator, SOME crand]
val (_,rhs) = Thm.dest_equals (Thm.cprop_of abs_C')
in
Thm.transitive abs_C' (Conv.fun_conv (Conv.arg_conv (abstract ctxt)) rhs)
@@ -132,10 +131,11 @@
else if Term.is_dependent rand then (*B or eta*)
if rand = Bound 0 then Thm.eta_conversion ct
else (*B*)
- let val crand = Thm.cterm_of ctxt (Abs (x, xT, rand))
- val crator = Thm.cterm_of ctxt rator
- val abs_B' =
- infer_instantiate ctxt [(("a", 0), crator), (("g", 0), crand)] @{thm abs_B}
+ let val crator = Thm.dest_fun cbody
+ val crand = Thm.lambda x (Thm.dest_arg cbody)
+ val (C, B) = Thm.dest_ctyp_fun (Thm.ctyp_of_cterm crator)
+ val abs_B' = @{thm abs_B}
+ |> instantiate'_normalize [SOME A, SOME B, SOME C] [SOME crator, SOME crand]
val (_,rhs) = Thm.dest_equals (Thm.cprop_of abs_B')
in Thm.transitive abs_B' (Conv.arg_conv (abstract ctxt) rhs) end
else makeK ()
--- a/src/Pure/drule.ML Sat Apr 13 19:58:28 2019 +0200
+++ b/src/Pure/drule.ML Sat Apr 13 21:43:41 2019 +0200
@@ -21,6 +21,7 @@
val implies_intr_list: cterm list -> thm -> thm
val instantiate_normalize: ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list ->
thm -> thm
+ val instantiate'_normalize: ctyp option list -> cterm option list -> thm -> thm
val infer_instantiate_types: Proof.context -> ((indexname * typ) * cterm) list -> thm -> thm
val infer_instantiate: Proof.context -> (indexname * cterm) list -> thm -> thm
val infer_instantiate': Proof.context -> cterm option list -> thm -> thm
@@ -731,6 +732,9 @@
fun instantiate_normalize instpair th =
Thm.adjust_maxidx_thm ~1 (Thm.instantiate instpair th COMP_INCR asm_rl);
+fun instantiate'_normalize Ts ts th =
+ Thm.adjust_maxidx_thm ~1 (Thm.instantiate' Ts ts th COMP_INCR asm_rl);
+
(*instantiation with type-inference for variables*)
fun infer_instantiate_types _ [] th = th
| infer_instantiate_types ctxt args raw_th =