# HG changeset patch
# User wenzelm
# Date 1632250583 -7200
# Node ID 55007a70bd96c32c79b1e81a5a42e058514cb2dd
# Parent  e5ff77db6f386bb6d8f2189f6e6ebd58f3655e98
clarified antiquotations;

diff -r e5ff77db6f38 -r 55007a70bd96 src/HOL/Tools/Meson/meson.ML
--- a/src/HOL/Tools/Meson/meson.ML	Tue Sep 21 20:56:06 2021 +0200
+++ b/src/HOL/Tools/Meson/meson.ML	Tue Sep 21 20:56:23 2021 +0200
@@ -105,7 +105,7 @@
     \<^try>\<open>
       let val thy = Proof_Context.theory_of ctxt
           val tmA = Thm.concl_of thA
-          val Const(\<^const_name>\<open>Pure.imp\<close>,_) $ tmB $ _ = Thm.prop_of thB
+          val \<^Const_>\<open>Pure.imp for tmB _\<close> = Thm.prop_of thB
           val tenv =
             Pattern.first_order_match thy (tmB, tmA)
                                           (Vartab.empty, Vartab.empty) |> snd
@@ -136,8 +136,8 @@
       | some_eq _ _ = false
     fun add_names quant (Const (quant_s, _) $ Abs (s, _, t')) =
         add_names quant t' #> some_eq quant (quant_of quant_s) ? cons s
-      | add_names quant (\<^const>\<open>Not\<close> $ t) = add_names (flip_quant quant) t
-      | add_names quant (\<^const>\<open>implies\<close> $ t1 $ t2) =
+      | add_names quant \<^Const_>\<open>Not for t\<close> = add_names (flip_quant quant) t
+      | add_names quant \<^Const_>\<open>implies for t1 t2\<close> =
         add_names (flip_quant quant) t1 #> add_names quant t2
       | add_names quant (t1 $ t2) = fold (add_names quant) [t1, t2]
       | add_names _ _ = I
@@ -174,7 +174,7 @@
    workaround is to instantiate "?P := (%c. ... c ... c ... c ...)" manually. *)
 fun quant_resolve_tac ctxt th i st =
   case (Thm.concl_of st, Thm.prop_of th) of
-    (\<^const>\<open>Trueprop\<close> $ (Var _ $ (c as Free _)), \<^const>\<open>Trueprop\<close> $ _) =>
+    (\<^Const_>\<open>Trueprop for \<open>Var _ $ (c as Free _)\<close>\<close>, \<^Const_>\<open>Trueprop for _\<close>) =>
     let
       val cc = Thm.cterm_of ctxt c
       val ct = Thm.dest_arg (Thm.cprop_of th)
@@ -202,21 +202,21 @@
 (*Are any of the logical connectives in "bs" present in the term?*)
 fun has_conns bs =
   let fun has (Const _) = false
-        | has (Const(\<^const_name>\<open>Trueprop\<close>,_) $ p) = has p
-        | has (Const(\<^const_name>\<open>Not\<close>,_) $ p) = has p
-        | has (Const(\<^const_name>\<open>HOL.disj\<close>,_) $ p $ q) = member (op =) bs \<^const_name>\<open>HOL.disj\<close> orelse has p orelse has q
-        | has (Const(\<^const_name>\<open>HOL.conj\<close>,_) $ p $ q) = member (op =) bs \<^const_name>\<open>HOL.conj\<close> orelse has p orelse has q
-        | has (Const(\<^const_name>\<open>All\<close>,_) $ Abs(_,_,p)) = member (op =) bs \<^const_name>\<open>All\<close> orelse has p
-        | has (Const(\<^const_name>\<open>Ex\<close>,_) $ Abs(_,_,p)) = member (op =) bs \<^const_name>\<open>Ex\<close> orelse has p
+        | has \<^Const_>\<open>Trueprop for p\<close> = has p
+        | has \<^Const_>\<open>Not for p\<close> = has p
+        | has \<^Const_>\<open>disj for p q\<close> = member (op =) bs \<^const_name>\<open>disj\<close> orelse has p orelse has q
+        | has \<^Const_>\<open>conj for p q\<close> = member (op =) bs \<^const_name>\<open>conj\<close> orelse has p orelse has q
+        | has \<^Const_>\<open>All _ for \<open>Abs(_,_,p)\<close>\<close> = member (op =) bs \<^const_name>\<open>All\<close> orelse has p
+        | has \<^Const_>\<open>Ex _ for \<open>Abs(_,_,p)\<close>\<close> = member (op =) bs \<^const_name>\<open>Ex\<close> orelse has p
         | has _ = false
   in  has  end;
 
 
 (**** Clause handling ****)
 
-fun literals (Const(\<^const_name>\<open>Trueprop\<close>,_) $ P) = literals P
-  | literals (Const(\<^const_name>\<open>HOL.disj\<close>,_) $ P $ Q) = literals P @ literals Q
-  | literals (Const(\<^const_name>\<open>Not\<close>,_) $ P) = [(false,P)]
+fun literals \<^Const_>\<open>Trueprop for P\<close> = literals P
+  | literals \<^Const_>\<open>disj for P Q\<close> = literals P @ literals Q
+  | literals \<^Const_>\<open>Not for P\<close> = [(false,P)]
   | literals P = [(true,P)];
 
 (*number of literals in a term*)
@@ -225,16 +225,16 @@
 
 (*** Tautology Checking ***)
 
-fun signed_lits_aux (Const (\<^const_name>\<open>HOL.disj\<close>, _) $ P $ Q) (poslits, neglits) =
+fun signed_lits_aux \<^Const_>\<open>disj for P Q\<close> (poslits, neglits) =
       signed_lits_aux Q (signed_lits_aux P (poslits, neglits))
-  | signed_lits_aux (Const(\<^const_name>\<open>Not\<close>,_) $ P) (poslits, neglits) = (poslits, P::neglits)
+  | signed_lits_aux \<^Const_>\<open>Not for P\<close> (poslits, neglits) = (poslits, P::neglits)
   | signed_lits_aux P (poslits, neglits) = (P::poslits, neglits);
 
 fun signed_lits th = signed_lits_aux (HOLogic.dest_Trueprop (Thm.concl_of th)) ([],[]);
 
 (*Literals like X=X are tautologous*)
-fun taut_poslit (Const(\<^const_name>\<open>HOL.eq\<close>,_) $ t $ u) = t aconv u
-  | taut_poslit (Const(\<^const_name>\<open>True\<close>,_)) = true
+fun taut_poslit \<^Const_>\<open>HOL.eq _ for t u\<close> = t aconv u
+  | taut_poslit \<^Const_>\<open>True\<close> = true
   | taut_poslit _ = false;
 
 fun is_taut th =
@@ -261,18 +261,17 @@
 fun refl_clause_aux 0 th = th
   | refl_clause_aux n th =
        case HOLogic.dest_Trueprop (Thm.concl_of th) of
-          (Const (\<^const_name>\<open>HOL.disj\<close>, _) $ (Const (\<^const_name>\<open>HOL.disj\<close>, _) $ _ $ _) $ _) =>
+          \<^Const_>\<open>disj for \<open>\<^Const_>\<open>disj for _ _\<close>\<close> _\<close> =>
             refl_clause_aux n (th RS disj_assoc)    (*isolate an atom as first disjunct*)
-        | (Const (\<^const_name>\<open>HOL.disj\<close>, _) $ (Const(\<^const_name>\<open>Not\<close>,_) $ (Const(\<^const_name>\<open>HOL.eq\<close>,_) $ t $ u)) $ _) =>
+        | \<^Const_>\<open>disj for \<open>\<^Const_>\<open>Not for \<open>\<^Const_>\<open>HOL.eq _ for t u\<close>\<close>\<close>\<close> _\<close> =>
             if eliminable(t,u)
             then refl_clause_aux (n-1) (th RS not_refl_disj_D)  (*Var inequation: delete*)
             else refl_clause_aux (n-1) (th RS disj_comm)  (*not between Vars: ignore*)
-        | (Const (\<^const_name>\<open>HOL.disj\<close>, _) $ _ $ _) => refl_clause_aux n (th RS disj_comm)
+        | \<^Const>\<open>disj for _ _\<close> => refl_clause_aux n (th RS disj_comm)
         | _ => (*not a disjunction*) th;
 
-fun notequal_lits_count (Const (\<^const_name>\<open>HOL.disj\<close>, _) $ P $ Q) =
-      notequal_lits_count P + notequal_lits_count Q
-  | notequal_lits_count (Const(\<^const_name>\<open>Not\<close>,_) $ (Const(\<^const_name>\<open>HOL.eq\<close>,_) $ _ $ _)) = 1
+fun notequal_lits_count \<^Const_>\<open>disj for P Q\<close> = notequal_lits_count P + notequal_lits_count Q
+  | notequal_lits_count \<^Const_>\<open>Not for \<open>\<^Const_>\<open>HOL.eq _ for _ _\<close>\<close>\<close> = 1
   | notequal_lits_count _ = 0;
 
 (*Simplify a clause by applying reflexivity to its negated equality literals*)
@@ -317,26 +316,26 @@
   fun prod x y = if x < bound andalso y < bound then x*y else bound
   
   (*Estimate the number of clauses in order to detect infeasible theorems*)
-  fun signed_nclauses b (Const(\<^const_name>\<open>Trueprop\<close>,_) $ t) = signed_nclauses b t
-    | signed_nclauses b (Const(\<^const_name>\<open>Not\<close>,_) $ t) = signed_nclauses (not b) t
-    | signed_nclauses b (Const(\<^const_name>\<open>HOL.conj\<close>,_) $ t $ u) =
+  fun signed_nclauses b \<^Const_>\<open>Trueprop for t\<close> = signed_nclauses b t
+    | signed_nclauses b \<^Const_>\<open>Not for t\<close> = signed_nclauses (not b) t
+    | signed_nclauses b \<^Const_>\<open>conj for t u\<close> =
         if b then sum (signed_nclauses b t) (signed_nclauses b u)
              else prod (signed_nclauses b t) (signed_nclauses b u)
-    | signed_nclauses b (Const(\<^const_name>\<open>HOL.disj\<close>,_) $ t $ u) =
+    | signed_nclauses b \<^Const_>\<open>disj for t u\<close> =
         if b then prod (signed_nclauses b t) (signed_nclauses b u)
              else sum (signed_nclauses b t) (signed_nclauses b u)
-    | signed_nclauses b (Const(\<^const_name>\<open>HOL.implies\<close>,_) $ t $ u) =
+    | signed_nclauses b \<^Const_>\<open>implies for t u\<close> =
         if b then prod (signed_nclauses (not b) t) (signed_nclauses b u)
              else sum (signed_nclauses (not b) t) (signed_nclauses b u)
-    | signed_nclauses b (Const(\<^const_name>\<open>HOL.eq\<close>, Type ("fun", [T, _])) $ t $ u) =
+    | signed_nclauses b \<^Const_>\<open>HOL.eq \<open>T\<close> for t u\<close> =
         if T = HOLogic.boolT then (*Boolean equality is if-and-only-if*)
             if b then sum (prod (signed_nclauses (not b) t) (signed_nclauses b u))
                           (prod (signed_nclauses (not b) u) (signed_nclauses b t))
                  else sum (prod (signed_nclauses b t) (signed_nclauses b u))
                           (prod (signed_nclauses (not b) t) (signed_nclauses (not b) u))
         else 1
-    | signed_nclauses b (Const(\<^const_name>\<open>Ex\<close>, _) $ Abs (_,_,t)) = signed_nclauses b t
-    | signed_nclauses b (Const(\<^const_name>\<open>All\<close>,_) $ Abs (_,_,t)) = signed_nclauses b t
+    | signed_nclauses b \<^Const_>\<open>Ex _ for \<open>Abs (_,_,t)\<close>\<close> = signed_nclauses b t
+    | signed_nclauses b \<^Const_>\<open>All _ for \<open>Abs (_,_,t)\<close>\<close> = signed_nclauses b t
     | signed_nclauses _ _ = 1; (* literal *)
  in signed_nclauses true t end
 
@@ -351,7 +350,7 @@
   val spec_var =
     Thm.dest_arg (Thm.dest_arg (#2 (Thm.dest_implies (Thm.cprop_of spec))))
     |> Thm.term_of |> dest_Var;
-  fun name_of (Const (\<^const_name>\<open>All\<close>, _) $ Abs(x, _, _)) = x | name_of _ = Name.uu;
+  fun name_of \<^Const_>\<open>All _ for \<open>Abs(x, _, _)\<close>\<close> = x | name_of _ = Name.uu;
 in  
   fun freeze_spec th ctxt =
     let
@@ -379,15 +378,15 @@
         else if not (has_conns [\<^const_name>\<open>All\<close>, \<^const_name>\<open>Ex\<close>, \<^const_name>\<open>HOL.conj\<close>] (Thm.prop_of th))
         then nodups ctxt th :: ths (*no work to do, terminate*)
         else case head_of (HOLogic.dest_Trueprop (Thm.concl_of th)) of
-            Const (\<^const_name>\<open>HOL.conj\<close>, _) => (*conjunction*)
+            \<^Const_>\<open>conj\<close> => (*conjunction*)
                 cnf_aux (th RS conjunct1, cnf_aux (th RS conjunct2, ths))
-          | Const (\<^const_name>\<open>All\<close>, _) => (*universal quantifier*)
+          | \<^Const_>\<open>All _\<close> => (*universal quantifier*)
                 let val (th', ctxt') = freeze_spec th (! ctxt_ref)
                 in  ctxt_ref := ctxt'; cnf_aux (th', ths) end
-          | Const (\<^const_name>\<open>Ex\<close>, _) =>
+          | \<^Const_>\<open>Ex _\<close> =>
               (*existential quantifier: Insert Skolem functions*)
               cnf_aux (apply_skolem_theorem (! ctxt_ref) (th, old_skolem_ths), ths)
-          | Const (\<^const_name>\<open>HOL.disj\<close>, _) =>
+          | \<^Const_>\<open>disj\<close> =>
               (*Disjunction of P, Q: Create new goal of proving ?P | ?Q and solve it using
                 all combinations of converting P, Q to CNF.*)
               (*There is one assumption, which gets bound to prem and then normalized via
@@ -415,8 +414,7 @@
 
 (**** Generation of contrapositives ****)
 
-fun is_left (Const (\<^const_name>\<open>Trueprop\<close>, _) $
-               (Const (\<^const_name>\<open>HOL.disj\<close>, _) $ (Const (\<^const_name>\<open>HOL.disj\<close>, _) $ _ $ _) $ _)) = true
+fun is_left \<^Const_>\<open>Trueprop for \<open>\<^Const_>\<open>disj for \<open>\<^Const_>\<open>disj for _ _\<close>\<close> _\<close>\<close>\<close> = true
   | is_left _ = false;
 
 (*Associate disjuctions to right -- make leftmost disjunct a LITERAL*)
@@ -437,8 +435,8 @@
 
 fun rigid t = not (is_Var (head_of t));
 
-fun ok4horn (Const (\<^const_name>\<open>Trueprop\<close>,_) $ (Const (\<^const_name>\<open>HOL.disj\<close>, _) $ t $ _)) = rigid t
-  | ok4horn (Const (\<^const_name>\<open>Trueprop\<close>,_) $ t) = rigid t
+fun ok4horn \<^Const_>\<open>Trueprop for \<open>\<^Const_>\<open>disj for t _\<close>\<close>\<close> = rigid t
+  | ok4horn \<^Const_>\<open>Trueprop for t\<close> = rigid t
   | ok4horn _ = false;
 
 (*Create a meta-level Horn clause*)
@@ -472,8 +470,7 @@
 
 (***** MESON PROOF PROCEDURE *****)
 
-fun rhyps (Const(\<^const_name>\<open>Pure.imp\<close>,_) $ (Const(\<^const_name>\<open>Trueprop\<close>,_) $ A) $ phi,
-           As) = rhyps(phi, A::As)
+fun rhyps (\<^Const_>\<open>Pure.imp for \<open>\<^Const_>\<open>Trueprop for A\<close>\<close> phi\<close>, As) = rhyps(phi, A::As)
   | rhyps (_, As) = As;
 
 (** Detecting repeated assumptions in a subgoal **)
@@ -517,8 +514,8 @@
 val nnf_rls = [imp_to_disjD, iff_to_disjD, not_conjD, not_disjD,
                not_impD, not_iffD, not_allD, not_exD, not_notD];
 
-fun ok4nnf (Const (\<^const_name>\<open>Trueprop\<close>,_) $ (Const (\<^const_name>\<open>Not\<close>, _) $ t)) = rigid t
-  | ok4nnf (Const (\<^const_name>\<open>Trueprop\<close>,_) $ t) = rigid t
+fun ok4nnf \<^Const_>\<open>Trueprop for \<open>\<^Const_>\<open>Not for t\<close>\<close>\<close> = rigid t
+  | ok4nnf \<^Const_>\<open>Trueprop for t\<close> = rigid t
   | ok4nnf _ = false;
 
 fun make_nnf1 ctxt th =
@@ -610,7 +607,7 @@
           end
       end
   in
-    if T = \<^typ>\<open>bool\<close> then
+    if T = \<^Type>\<open>bool\<close> then
       NONE
     else case pat t u of
       (SOME T, p as _ $ _) => SOME (Abs (Name.uu, T, p))
@@ -623,12 +620,10 @@
 (* Strengthens "f g ~= f h" to "f g ~= f h & (EX x. g x ~= h x)". *)
 fun cong_extensionalize_thm ctxt th =
   (case Thm.concl_of th of
-    \<^const>\<open>Trueprop\<close> $ (\<^const>\<open>Not\<close>
-        $ (Const (\<^const_name>\<open>HOL.eq\<close>, Type (_, [T, _]))
-           $ (t as _ $ _) $ (u as _ $ _))) =>
-    (case get_F_pattern T t u of
-      SOME p => th RS infer_instantiate ctxt [(("F", 0), Thm.cterm_of ctxt p)] ext_cong_neq
-    | NONE => th)
+    \<^Const_>\<open>Trueprop for \<open>\<^Const_>\<open>Not for \<open>\<^Const_>\<open>HOL.eq T for \<open>t as _ $ _\<close> \<open>u as _ $ _\<close>\<close>\<close>\<close>\<close>\<close> =>
+      (case get_F_pattern T t u of
+        SOME p => th RS infer_instantiate ctxt [(("F", 0), Thm.cterm_of ctxt p)] ext_cong_neq
+      | NONE => th)
   | _ => th)
 
 (* Removes the lambdas from an equation of the form "t = (%x1 ... xn. u)". It
@@ -636,9 +631,9 @@
    proof in "Tarski" that relies on the current behavior. *)
 fun abs_extensionalize_conv ctxt ct =
   (case Thm.term_of ct of
-    Const (\<^const_name>\<open>HOL.eq\<close>, _) $ _ $ Abs _ =>
-    ct |> (Conv.rewr_conv @{thm fun_eq_iff [THEN eq_reflection]}
-           then_conv abs_extensionalize_conv ctxt)
+    \<^Const_>\<open>HOL.eq _ for _ \<open>Abs _\<close>\<close> =>
+      ct |> (Conv.rewr_conv @{thm fun_eq_iff [THEN eq_reflection]}
+             then_conv abs_extensionalize_conv ctxt)
   | _ $ _ => Conv.comb_conv (abs_extensionalize_conv ctxt) ct
   | Abs _ => Conv.abs_conv (abs_extensionalize_conv o snd) ctxt ct
   | _ => Conv.all_conv ct)
diff -r e5ff77db6f38 -r 55007a70bd96 src/HOL/Tools/Meson/meson_clausify.ML
--- a/src/HOL/Tools/Meson/meson_clausify.ML	Tue Sep 21 20:56:06 2021 +0200
+++ b/src/HOL/Tools/Meson/meson_clausify.ML	Tue Sep 21 20:56:23 2021 +0200
@@ -41,9 +41,9 @@
    "Sledgehammer_Util".) *)
 fun transform_elim_theorem th =
   (case Thm.concl_of th of    (*conclusion variable*)
-    \<^const>\<open>Trueprop\<close> $ (Var (v as (_, \<^typ>\<open>bool\<close>))) =>
+    \<^Const_>\<open>Trueprop for \<open>Var (v as (_, \<^Type>\<open>bool\<close>))\<close>\<close> =>
       Thm.instantiate (TVars.empty, Vars.make [(v, cfalse)]) th
-  | Var (v as (_, \<^typ>\<open>prop\<close>)) =>
+  | Var (v as (_, \<^Type>\<open>prop\<close>)) =>
       Thm.instantiate (TVars.empty, Vars.make [(v, ctp_false)]) th
   | _ => th)
 
@@ -51,9 +51,8 @@
 (**** SKOLEMIZATION BY INFERENCE (lcp) ****)
 
 fun mk_old_skolem_term_wrapper t =
-  let val T = fastype_of t in
-    Const (\<^const_name>\<open>Meson.skolem\<close>, T --> T) $ t
-  end
+  let val T = fastype_of t
+  in \<^Const>\<open>Meson.skolem T for t\<close> end
 
 fun beta_eta_in_abs_body (Abs (s, T, t')) = Abs (s, T, beta_eta_in_abs_body t')
   | beta_eta_in_abs_body t = Envir.beta_eta_contract t
@@ -61,7 +60,7 @@
 (*Traverse a theorem, accumulating Skolem function definitions.*)
 fun old_skolem_defs th =
   let
-    fun dec_sko (Const (\<^const_name>\<open>Ex\<close>, _) $ (body as Abs (_, T, p))) rhss =
+    fun dec_sko \<^Const_>\<open>Ex _ for \<open>body as Abs (_, T, p)\<close>\<close> rhss =
         (*Existential: declare a Skolem function, then insert into body and continue*)
         let
           val args = Misc_Legacy.term_frees body
@@ -72,20 +71,20 @@
             |> mk_old_skolem_term_wrapper
           val comb = list_comb (rhs, args)
         in dec_sko (subst_bound (comb, p)) (rhs :: rhss) end
-      | dec_sko (Const (\<^const_name>\<open>All\<close>,_) $ Abs (a, T, p)) rhss =
+      | dec_sko \<^Const_>\<open>All _ for \<open>Abs (a, T, p)\<close>\<close> rhss =
         (*Universal quant: insert a free variable into body and continue*)
         let val fname = singleton (Name.variant_list (Misc_Legacy.add_term_names (p, []))) a
         in dec_sko (subst_bound (Free(fname,T), p)) rhss end
-      | dec_sko (\<^const>\<open>conj\<close> $ p $ q) rhss = rhss |> dec_sko p |> dec_sko q
-      | dec_sko (\<^const>\<open>disj\<close> $ p $ q) rhss = rhss |> dec_sko p |> dec_sko q
-      | dec_sko (\<^const>\<open>Trueprop\<close> $ p) rhss = dec_sko p rhss
+      | dec_sko \<^Const_>\<open>conj for p q\<close> rhss = rhss |> dec_sko p |> dec_sko q
+      | dec_sko \<^Const_>\<open>disj for p q\<close> rhss = rhss |> dec_sko p |> dec_sko q
+      | dec_sko \<^Const_>\<open>Trueprop for p\<close> rhss = dec_sko p rhss
       | dec_sko _ rhss = rhss
   in  dec_sko (Thm.prop_of th) []  end;
 
 
 (**** REPLACING ABSTRACTIONS BY COMBINATORS ****)
 
-fun is_quasi_lambda_free (Const (\<^const_name>\<open>Meson.skolem\<close>, _) $ _) = true
+fun is_quasi_lambda_free \<^Const_>\<open>Meson.skolem _ for _\<close> = true
   | is_quasi_lambda_free (t1 $ t2) =
     is_quasi_lambda_free t1 andalso is_quasi_lambda_free t2
   | is_quasi_lambda_free (Abs _) = false