--- 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)
--- 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