# HG changeset patch
# User wenzelm
# Date 1555184621 -7200
# Node ID 62b19f19350af93310fc602b589d673fcc43fd5d
# Parent  5d8833499c4aa1a253e388646c671a904203100f
meson: more cterm operations;

diff -r 5d8833499c4a -r 62b19f19350a src/HOL/Tools/Meson/meson_clausify.ML
--- 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 ()
diff -r 5d8833499c4a -r 62b19f19350a src/Pure/drule.ML
--- 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 =