--- a/NEWS Tue Sep 28 12:35:43 2021 +0200
+++ b/NEWS Wed Sep 29 09:58:19 2021 +0200
@@ -279,12 +279,20 @@
\<^Type>\<open>c\<close>
\<^Type>\<open>c T \<dots>\<close> \<comment> \<open>same with type arguments\<close>
- \<^Type>_fn\<open>c T \<dots>\<close> \<comment> \<open>fn abstraction, failure via exception TYPE\<close>
+ \<^Type_fn>\<open>c T \<dots>\<close> \<comment> \<open>fn abstraction, failure via exception TYPE\<close>
\<^Const>\<open>c\<close>
\<^Const>\<open>c T \<dots>\<close> \<comment> \<open>same with type arguments\<close>
\<^Const>\<open>c for t \<dots>\<close> \<comment> \<open>same with term arguments\<close>
\<^Const_>\<open>c \<dots>\<close> \<comment> \<open>same for patterns: case, let, fn\<close>
- \<^Const>_fn\<open>c T \<dots>\<close> \<comment> \<open>fn abstraction, failure via exception TERM\<close>
+ \<^Const_fn>\<open>c T \<dots>\<close> \<comment> \<open>fn abstraction, failure via exception TERM\<close>
+
+The type/term arguments refer to nested ML source, which may contain
+antiquotations recursively. The following argument syntax is supported:
+
+ - an underscore (dummy pattern)
+ - an atomic item of "embedded" syntax, e.g. identifier or cartouche
+ - an antiquotation in control-symbol/cartouche form, e.g. \<^Type>\<open>c\<close>
+ as short form of \<open>\<^Type>\<open>c\<close>\<close>.
Examples in HOL:
--- a/src/CCL/Wfd.thy Tue Sep 28 12:35:43 2021 +0200
+++ b/src/CCL/Wfd.thy Wed Sep 29 09:58:19 2021 +0200
@@ -441,7 +441,7 @@
fun is_rigid_prog t =
(case (Logic.strip_assums_concl t) of
- \<^Const_>\<open>Trueprop for \<open>\<^Const_>\<open>mem _ for a _\<close>\<close>\<close> => null (Term.add_vars a [])
+ \<^Const_>\<open>Trueprop for \<^Const_>\<open>mem _ for a _\<close>\<close> => null (Term.add_vars a [])
| _ => false)
in
--- a/src/FOLP/IFOLP.thy Tue Sep 28 12:35:43 2021 +0200
+++ b/src/FOLP/IFOLP.thy Wed Sep 29 09:58:19 2021 +0200
@@ -612,7 +612,7 @@
structure Hypsubst = Hypsubst
(
(*Take apart an equality judgement; otherwise raise Match!*)
- fun dest_eq \<^Const_>\<open>Proof for \<open>\<^Const_>\<open>eq _ for t u\<close>\<close> _\<close> = (t, u);
+ fun dest_eq \<^Const_>\<open>Proof for \<^Const_>\<open>eq _ for t u\<close> _\<close> = (t, u);
val imp_intr = @{thm impI}
--- a/src/HOL/HOL.thy Tue Sep 28 12:35:43 2021 +0200
+++ b/src/HOL/HOL.thy Wed Sep 29 09:58:19 2021 +0200
@@ -888,7 +888,7 @@
structure Blast = Blast
(
structure Classical = Classical
- val Trueprop_const = dest_Const \<^const>\<open>Trueprop\<close>
+ val Trueprop_const = dest_Const \<^Const>\<open>Trueprop\<close>
val equality_name = \<^const_name>\<open>HOL.eq\<close>
val not_name = \<^const_name>\<open>Not\<close>
val notE = @{thm notE}
@@ -1549,7 +1549,7 @@
{lhss = [\<^term>\<open>induct_false \<Longrightarrow> PROP P \<Longrightarrow> PROP Q\<close>],
proc = fn _ => fn _ => fn ct =>
(case Thm.term_of ct of
- _ $ (P as _ $ \<^const>\<open>induct_false\<close>) $ (_ $ Q $ _) =>
+ _ $ (P as _ $ \<^Const_>\<open>induct_false\<close>) $ (_ $ Q $ _) =>
if P <> Q then SOME Drule.swap_prems_eq else NONE
| _ => NONE)},
Simplifier.make_simproc \<^context> "induct_equal_conj_curry"
@@ -1558,11 +1558,11 @@
(case Thm.term_of ct of
_ $ (_ $ P) $ _ =>
let
- fun is_conj (\<^const>\<open>induct_conj\<close> $ P $ Q) =
+ fun is_conj \<^Const_>\<open>induct_conj for P Q\<close> =
is_conj P andalso is_conj Q
- | is_conj (Const (\<^const_name>\<open>induct_equal\<close>, _) $ _ $ _) = true
- | is_conj \<^const>\<open>induct_true\<close> = true
- | is_conj \<^const>\<open>induct_false\<close> = true
+ | is_conj \<^Const_>\<open>induct_equal _ for _ _\<close> = true
+ | is_conj \<^Const_>\<open>induct_true\<close> = true
+ | is_conj \<^Const_>\<open>induct_false\<close> = true
| is_conj _ = false
in if is_conj P then SOME @{thm induct_conj_curry} else NONE end
| _ => NONE)}]
--- a/src/HOL/HOLCF/Tools/holcf_library.ML Tue Sep 28 12:35:43 2021 +0200
+++ b/src/HOL/HOLCF/Tools/holcf_library.ML Wed Sep 29 09:58:19 2021 +0200
@@ -58,7 +58,7 @@
let
val T = Term.range_type (Term.fastype_of t)
val UNIV_const = \<^term>\<open>UNIV :: nat set\<close>
- in \<^Const>\<open>lub T for \<open>\<^Const>\<open>image \<open>\<^Type>\<open>nat\<close>\<close> T for t UNIV_const\<close>\<close>\<close> end
+ in \<^Const>\<open>lub T for \<^Const>\<open>image \<^Type>\<open>nat\<close> T for t UNIV_const\<close>\<close> end
(*** Continuous function space ***)
--- a/src/HOL/Hoare/hoare_tac.ML Tue Sep 28 12:35:43 2021 +0200
+++ b/src/HOL/Hoare/hoare_tac.ML Wed Sep 29 09:58:19 2021 +0200
@@ -49,7 +49,7 @@
Abs (_, T, _) => T
| Const (_, Type (_, [_, Type (_, [T, _])])) $ _ => T);
in
- \<^Const>\<open>case_prod T T2 \<open>\<^Type>\<open>bool\<close>\<close> for \<open>absfree (x, T) z\<close>\<close>
+ \<^Const>\<open>case_prod T T2 \<^Type>\<open>bool\<close> for \<open>absfree (x, T) z\<close>\<close>
end;
(** maps [x1,...,xn] to (x1,...,xn) and types**)
--- a/src/HOL/IMP/Hoare_Total.thy Tue Sep 28 12:35:43 2021 +0200
+++ b/src/HOL/IMP/Hoare_Total.thy Wed Sep 29 09:58:19 2021 +0200
@@ -89,6 +89,32 @@
apply simp
done
+text \<open>Nested loops. This poses a problem for VCGs because the proof of the inner loop needs to
+refer to outer loops. This works here because the invariant is not written down statically but
+created in the context of a proof that has already introduced/fixed outer \<open>n\<close>s that can be
+referred to.\<close>
+
+lemma
+ "\<turnstile>\<^sub>t {\<lambda>_. True}
+ WHILE Less (N 0) (V ''x'')
+ DO (''x'' ::= Plus (V ''x'') (N(-1));;
+ ''y'' ::= V ''x'';;
+ WHILE Less (N 0) (V ''y'') DO ''y'' ::= Plus (V ''y'') (N(-1)))
+ {\<lambda>_. True}"
+apply(rule While_fun'[where f = "\<lambda>s. nat(s ''x'')"])
+ prefer 2 apply simp
+apply(rule_tac P\<^sub>2 = "\<lambda>s. nat(s ''x'') < n" in Seq)
+ apply(rule_tac P\<^sub>2 = "\<lambda>s. nat(s ''x'') < n" in Seq)
+ apply(rule Assign')
+ apply simp
+ apply(rule Assign')
+ apply simp
+(* note that the invariant refers to the outer \<open>n\<close>: *)
+apply(rule While_fun'[where f = "\<lambda>s. nat(s ''y'')"])
+ prefer 2 apply simp
+apply(rule Assign')
+apply simp
+done
text\<open>The soundness theorem:\<close>
--- a/src/HOL/Library/Pattern_Aliases.thy Tue Sep 28 12:35:43 2021 +0200
+++ b/src/HOL/Library/Pattern_Aliases.thy Wed Sep 29 09:58:19 2021 +0200
@@ -97,7 +97,7 @@
fun check_pattern_syntax t =
case strip_all t of
- (vars, \<^const>\<open>Trueprop\<close> $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ lhs $ rhs)) =>
+ (vars, \<^Const>\<open>Trueprop\<close> $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ lhs $ rhs)) =>
let
fun go (Const (\<^const_name>\<open>as\<close>, _) $ pat $ var, rhs) =
let
@@ -126,7 +126,7 @@
fun uncheck_pattern_syntax ctxt t =
case strip_all t of
- (vars, \<^const>\<open>Trueprop\<close> $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ lhs $ rhs)) =>
+ (vars, \<^Const>\<open>Trueprop\<close> $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ lhs $ rhs)) =>
let
(* restricted to going down abstractions; ignores eta-contracted rhs *)
fun go lhs (rhs as Const (\<^const_name>\<open>Let\<close>, _) $ pat $ Abs (name, typ, t)) ctxt frees =
--- a/src/HOL/Library/code_lazy.ML Tue Sep 28 12:35:43 2021 +0200
+++ b/src/HOL/Library/code_lazy.ML Wed Sep 29 09:58:19 2021 +0200
@@ -378,8 +378,8 @@
||>> fold_map (mk_name ("case_" ^ short_type_name ^ "_lazy_") "") ctr_names
val mk_Lazy_delay_eq =
- (#const lazy_ctr_def $ mk_delay (Bound 0), Rep_lazy $ (Bound 0 $ \<^const>\<open>Unity\<close>))
- |> mk_eq |> all_abs [\<^typ>\<open>unit\<close> --> lazy_type]
+ (#const lazy_ctr_def $ mk_delay (Bound 0), Rep_lazy $ (Bound 0 $ \<^Const>\<open>Unity\<close>))
+ |> mk_eq |> all_abs [\<^Type>\<open>unit\<close> --> lazy_type]
val (Lazy_delay_thm, lthy8a) = mk_thm
((Lazy_delay_eq_name, mk_Lazy_delay_eq), [#thm lazy_ctr_def, @{thm force_delay}])
lthy8
--- a/src/HOL/Library/code_test.ML Tue Sep 28 12:35:43 2021 +0200
+++ b/src/HOL/Library/code_test.ML Wed Sep 29 09:58:19 2021 +0200
@@ -179,15 +179,15 @@
lhs :: rhs :: acc)
| add_eval _ = I
-fun mk_term_of [] = \<^term>\<open>None :: (unit \<Rightarrow> yxml_of_term) option\<close>
+fun mk_term_of [] = \<^Const>\<open>None \<^typ>\<open>unit \<Rightarrow> yxml_of_term\<close>\<close>
| mk_term_of ts =
let
val tuple = mk_tuples ts
val T = fastype_of tuple
in
\<^term>\<open>Some :: (unit \<Rightarrow> yxml_of_term) \<Rightarrow> (unit \<Rightarrow> yxml_of_term) option\<close> $
- (absdummy \<^typ>\<open>unit\<close> (\<^const>\<open>yxml_string_of_term\<close> $
- (Const (\<^const_name>\<open>Code_Evaluation.term_of\<close>, T --> \<^typ>\<open>term\<close>) $ tuple)))
+ (absdummy \<^typ>\<open>unit\<close> (\<^Const>\<open>yxml_string_of_term\<close> $
+ (Const (\<^const_name>\<open>Code_Evaluation.term_of\<close>, T --> \<^Type>\<open>term\<close>) $ tuple)))
end
fun test_terms ctxt ts target =
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML Tue Sep 28 12:35:43 2021 +0200
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Wed Sep 29 09:58:19 2021 +0200
@@ -773,17 +773,17 @@
fun is_first_order_lambda_free t =
(case t of
- \<^const>\<open>Not\<close> $ t1 => is_first_order_lambda_free t1
- | Const (\<^const_name>\<open>All\<close>, _) $ Abs (_, _, t') => is_first_order_lambda_free t'
- | Const (\<^const_name>\<open>All\<close>, _) $ t1 => is_first_order_lambda_free t1
- | Const (\<^const_name>\<open>Ex\<close>, _) $ Abs (_, _, t') => is_first_order_lambda_free t'
- | Const (\<^const_name>\<open>Ex\<close>, _) $ t1 => is_first_order_lambda_free t1
- | \<^const>\<open>HOL.conj\<close> $ t1 $ t2 => is_first_order_lambda_free t1 andalso is_first_order_lambda_free t2
- | \<^const>\<open>HOL.disj\<close> $ t1 $ t2 => is_first_order_lambda_free t1 andalso is_first_order_lambda_free t2
- | \<^const>\<open>HOL.implies\<close> $ t1 $ t2 =>
- is_first_order_lambda_free t1 andalso is_first_order_lambda_free t2
- | Const (\<^const_name>\<open>HOL.eq\<close>, Type (_, [\<^typ>\<open>bool\<close>, _])) $ t1 $ t2 =>
- is_first_order_lambda_free t1 andalso is_first_order_lambda_free t2
+ \<^Const_>\<open>Not for t1\<close> => is_first_order_lambda_free t1
+ | \<^Const_>\<open>All _ for \<open>Abs (_, _, t')\<close>\<close> => is_first_order_lambda_free t'
+ | \<^Const_>\<open>All _ for t1\<close> => is_first_order_lambda_free t1
+ | \<^Const_>\<open>Ex _ for \<open>Abs (_, _, t')\<close>\<close> => is_first_order_lambda_free t'
+ | \<^Const_>\<open>Ex _ for t1\<close> => is_first_order_lambda_free t1
+ | \<^Const_>\<open>conj for t1 t2\<close> => is_first_order_lambda_free t1 andalso is_first_order_lambda_free t2
+ | \<^Const_>\<open>disj for t1 t2\<close> => is_first_order_lambda_free t1 andalso is_first_order_lambda_free t2
+ | \<^Const_>\<open>implies for t1 t2\<close> =>
+ is_first_order_lambda_free t1 andalso is_first_order_lambda_free t2
+ | \<^Const_>\<open>HOL.eq \<^Type>\<open>bool\<close> for t1 t2\<close> =>
+ is_first_order_lambda_free t1 andalso is_first_order_lambda_free t2
| _ => not (exists_subterm (fn Abs _ => true | _ => false) t))
fun simple_translate_lambdas eta_matters do_lambdas ctxt type_enc t =
@@ -793,22 +793,22 @@
let
fun trans_first_order Ts t =
(case t of
- \<^const>\<open>Not\<close> $ t1 => \<^const>\<open>Not\<close> $ trans_first_order Ts t1
- | (t0 as Const (\<^const_name>\<open>All\<close>, _)) $ Abs (s, T, t') =>
+ \<^Const_>\<open>Not for t1\<close> => \<^Const>\<open>Not for \<open>trans_first_order Ts t1\<close>\<close>
+ | (t0 as \<^Const_>\<open>All _\<close>) $ Abs (s, T, t') =>
t0 $ Abs (s, T, trans_first_order (T :: Ts) t')
- | (t0 as Const (\<^const_name>\<open>All\<close>, _)) $ t1 =>
+ | (t0 as \<^Const_>\<open>All _\<close>) $ t1 =>
trans_first_order Ts (t0 $ eta_expand Ts t1 1)
- | (t0 as Const (\<^const_name>\<open>Ex\<close>, _)) $ Abs (s, T, t') =>
+ | (t0 as \<^Const_>\<open>Ex _\<close>) $ Abs (s, T, t') =>
t0 $ Abs (s, T, trans_first_order (T :: Ts) t')
- | (t0 as Const (\<^const_name>\<open>Ex\<close>, _)) $ t1 =>
+ | (t0 as \<^Const_>\<open>Ex _\<close>) $ t1 =>
trans_first_order Ts (t0 $ eta_expand Ts t1 1)
- | (t0 as \<^const>\<open>HOL.conj\<close>) $ t1 $ t2 =>
+ | (t0 as \<^Const_>\<open>conj\<close>) $ t1 $ t2 =>
t0 $ trans_first_order Ts t1 $ trans_first_order Ts t2
- | (t0 as \<^const>\<open>HOL.disj\<close>) $ t1 $ t2 =>
+ | (t0 as \<^Const_>\<open>disj\<close>) $ t1 $ t2 =>
t0 $ trans_first_order Ts t1 $ trans_first_order Ts t2
- | (t0 as \<^const>\<open>HOL.implies\<close>) $ t1 $ t2 =>
+ | (t0 as \<^Const_>\<open>implies\<close>) $ t1 $ t2 =>
t0 $ trans_first_order Ts t1 $ trans_first_order Ts t2
- | (t0 as Const (\<^const_name>\<open>HOL.eq\<close>, Type (_, [\<^typ>\<open>bool\<close>, _]))) $ t1 $ t2 =>
+ | (t0 as \<^Const_>\<open>HOL.eq \<^Type>\<open>bool\<close>\<close>) $ t1 $ t2 =>
t0 $ trans_first_order Ts t1 $ trans_first_order Ts t2
| _ =>
if not (exists_subterm (fn Abs _ => true | _ => false) t) then t
@@ -1381,18 +1381,18 @@
do_formula bs pos1 t1 ##>> do_formula bs pos2 t2 #>> uncurry (mk_aconn c)
and do_formula bs pos t =
(case t of
- \<^const>\<open>Trueprop\<close> $ t1 => do_formula bs pos t1
- | \<^const>\<open>Not\<close> $ t1 => do_formula bs (Option.map not pos) t1 #>> mk_anot
- | Const (\<^const_name>\<open>All\<close>, _) $ Abs (s, T, t') => do_quant bs AForall pos s T t'
- | (t0 as Const (\<^const_name>\<open>All\<close>, _)) $ t1 =>
+ \<^Const_>\<open>Trueprop for t1\<close> => do_formula bs pos t1
+ | \<^Const_>\<open>Not for t1\<close> => do_formula bs (Option.map not pos) t1 #>> mk_anot
+ | \<^Const_>\<open>All _ for \<open>Abs (s, T, t')\<close>\<close> => do_quant bs AForall pos s T t'
+ | (t0 as \<^Const_>\<open>All _\<close>) $ t1 =>
do_formula bs pos (t0 $ eta_expand (map (snd o snd) bs) t1 1)
- | Const (\<^const_name>\<open>Ex\<close>, _) $ Abs (s, T, t') => do_quant bs AExists pos s T t'
- | (t0 as Const (\<^const_name>\<open>Ex\<close>, _)) $ t1 =>
+ | \<^Const_>\<open>Ex _ for \<open>Abs (s, T, t')\<close>\<close> => do_quant bs AExists pos s T t'
+ | (t0 as \<^Const_>\<open>Ex _\<close>) $ t1 =>
do_formula bs pos (t0 $ eta_expand (map (snd o snd) bs) t1 1)
- | \<^const>\<open>HOL.conj\<close> $ t1 $ t2 => do_conn bs AAnd pos t1 pos t2
- | \<^const>\<open>HOL.disj\<close> $ t1 $ t2 => do_conn bs AOr pos t1 pos t2
- | \<^const>\<open>HOL.implies\<close> $ t1 $ t2 => do_conn bs AImplies (Option.map not pos) t1 pos t2
- | Const (\<^const_name>\<open>HOL.eq\<close>, Type (_, [\<^typ>\<open>bool\<close>, _])) $ t1 $ t2 =>
+ | \<^Const_>\<open>conj for t1 t2\<close> => do_conn bs AAnd pos t1 pos t2
+ | \<^Const_>\<open>disj for t1 t2\<close> => do_conn bs AOr pos t1 pos t2
+ | \<^Const_>\<open>implies for t1 t2\<close> => do_conn bs AImplies (Option.map not pos) t1 pos t2
+ | \<^Const_>\<open>HOL.eq \<^Type>\<open>bool\<close> for t1 t2\<close> =>
if iff_for_eq then do_conn bs AIff NONE t1 NONE t2 else do_term bs t
| _ => do_term bs t)
in do_formula [] end
@@ -1449,7 +1449,7 @@
|> presimplify_term simp_options ctxt
|> HOLogic.dest_Trueprop
end
- handle TERM _ => \<^const>\<open>True\<close>
+ handle TERM _ => \<^Const>\<open>True\<close>
(* Satallax prefers "=" to "<=>" (for definitions) and Metis (CNF) requires "=" for technical
reasons. *)
@@ -2030,9 +2030,9 @@
end
in List.partition (curry (op =) Definition o #role) #>> reorder [] #> op @ end
-fun s_not_prop (\<^const>\<open>Trueprop\<close> $ t) = \<^const>\<open>Trueprop\<close> $ s_not t
- | s_not_prop (\<^const>\<open>Pure.imp\<close> $ t $ \<^prop>\<open>False\<close>) = t
- | s_not_prop t = \<^const>\<open>Pure.imp\<close> $ t $ \<^prop>\<open>False\<close>
+fun s_not_prop \<^Const_>\<open>Trueprop for t\<close> = \<^Const>\<open>Trueprop for \<open>s_not t\<close>\<close>
+ | s_not_prop \<^Const_>\<open>Pure.imp for t \<^prop>\<open>False\<close>\<close> = t
+ | s_not_prop t = \<^Const>\<open>Pure.imp for t \<^prop>\<open>False\<close>\<close>
fun translate_formulas simp_options ctxt prem_role format type_enc lam_trans presimp hyp_ts concl_t
facts =
--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Tue Sep 28 12:35:43 2021 +0200
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Wed Sep 29 09:58:19 2021 +0200
@@ -127,7 +127,7 @@
| (u, Const (\<^const_name>\<open>True\<close>, _)) => u
| (Const (\<^const_name>\<open>False\<close>, _), v) => s_not v
| (u, Const (\<^const_name>\<open>False\<close>, _)) => s_not u
- | _ => if u aconv v then \<^const>\<open>True\<close> else t $ simplify_bool u $ simplify_bool v)
+ | _ => if u aconv v then \<^Const>\<open>True\<close> else t $ simplify_bool u $ simplify_bool v)
| simplify_bool (t $ u) = simplify_bool t $ simplify_bool u
| simplify_bool (Abs (s, T, t)) = Abs (s, T, simplify_bool t)
| simplify_bool t = t
@@ -351,7 +351,7 @@
error "Isar proof reconstruction failed because the ATP proof contains unparsable \
\material"
else if String.isPrefix native_type_prefix s then
- \<^const>\<open>True\<close> (* ignore TPTP type information (needed?) *)
+ \<^Const>\<open>True\<close> (* ignore TPTP type information (needed?) *)
else if s = tptp_equal then
list_comb (Const (\<^const_name>\<open>HOL.eq\<close>, Type_Infer.anyT \<^sort>\<open>type\<close>),
map (do_term [] NONE) us)
@@ -372,7 +372,7 @@
(nth us (length us - 2))
end
else if s' = type_guard_name then
- \<^const>\<open>True\<close> (* ignore type predicates *)
+ \<^Const>\<open>True\<close> (* ignore type predicates *)
else
let
val new_skolem = String.isPrefix new_skolem_const_prefix s''
@@ -436,7 +436,7 @@
fun term_of_atom ctxt format type_enc textual sym_tab pos (u as ATerm ((s, _), _)) =
if String.isPrefix class_prefix s then
add_type_constraint pos (type_constraint_of_term ctxt u)
- #> pair \<^const>\<open>True\<close>
+ #> pair \<^Const>\<open>True\<close>
else
pair (term_of_atp ctxt format type_enc textual sym_tab (SOME \<^typ>\<open>bool\<close>) u)
@@ -617,8 +617,8 @@
fun repair_waldmeister_endgame proof =
let
- fun repair_tail (name, _, \<^const>\<open>Trueprop\<close> $ t, rule, deps) =
- (name, Negated_Conjecture, \<^const>\<open>Trueprop\<close> $ s_not t, rule, deps)
+ fun repair_tail (name, _, \<^Const>\<open>Trueprop for t\<close>, rule, deps) =
+ (name, Negated_Conjecture, \<^Const>\<open>Trueprop for \<open>s_not t\<close>\<close>, rule, deps)
fun repair_body [] = []
| repair_body ((line as ((num, _), _, _, _, _)) :: lines) =
if num = waldmeister_conjecture_num then map repair_tail (line :: lines)
--- a/src/HOL/Tools/ATP/atp_util.ML Tue Sep 28 12:35:43 2021 +0200
+++ b/src/HOL/Tools/ATP/atp_util.ML Wed Sep 29 09:58:19 2021 +0200
@@ -261,43 +261,39 @@
(* Simple simplifications to ensure that sort annotations don't leave a trail of
spurious "True"s. *)
-fun s_not (Const (\<^const_name>\<open>All\<close>, T) $ Abs (s, T', t')) =
- Const (\<^const_name>\<open>Ex\<close>, T) $ Abs (s, T', s_not t')
- | s_not (Const (\<^const_name>\<open>Ex\<close>, T) $ Abs (s, T', t')) =
- Const (\<^const_name>\<open>All\<close>, T) $ Abs (s, T', s_not t')
- | s_not (\<^const>\<open>HOL.implies\<close> $ t1 $ t2) = \<^const>\<open>HOL.conj\<close> $ t1 $ s_not t2
- | s_not (\<^const>\<open>HOL.conj\<close> $ t1 $ t2) =
- \<^const>\<open>HOL.disj\<close> $ s_not t1 $ s_not t2
- | s_not (\<^const>\<open>HOL.disj\<close> $ t1 $ t2) =
- \<^const>\<open>HOL.conj\<close> $ s_not t1 $ s_not t2
- | s_not (\<^const>\<open>False\<close>) = \<^const>\<open>True\<close>
- | s_not (\<^const>\<open>True\<close>) = \<^const>\<open>False\<close>
- | s_not (\<^const>\<open>Not\<close> $ t) = t
- | s_not t = \<^const>\<open>Not\<close> $ t
+fun s_not \<^Const_>\<open>All T for \<open>Abs (s, T', t')\<close>\<close> = \<^Const>\<open>Ex T for \<open>Abs (s, T', s_not t')\<close>\<close>
+ | s_not \<^Const_>\<open>Ex T for \<open>Abs (s, T', t')\<close>\<close> = \<^Const>\<open>All T for \<open>Abs (s, T', s_not t')\<close>\<close>
+ | s_not \<^Const_>\<open>implies for t1 t2\<close> = \<^Const>\<open>conj for t1 \<open>s_not t2\<close>\<close>
+ | s_not \<^Const_>\<open>conj for t1 t2\<close> = \<^Const>\<open>disj for \<open>s_not t1\<close> \<open>s_not t2\<close>\<close>
+ | s_not \<^Const_>\<open>disj for t1 t2\<close> = \<^Const>\<open>conj for \<open>s_not t1\<close> \<open>s_not t2\<close>\<close>
+ | s_not \<^Const_>\<open>False\<close> = \<^Const>\<open>True\<close>
+ | s_not \<^Const_>\<open>True\<close> = \<^Const>\<open>False\<close>
+ | s_not \<^Const_>\<open>Not for t\<close> = t
+ | s_not t = \<^Const>\<open>Not for t\<close>
-fun s_conj (\<^const>\<open>True\<close>, t2) = t2
- | s_conj (t1, \<^const>\<open>True\<close>) = t1
- | s_conj (\<^const>\<open>False\<close>, _) = \<^const>\<open>False\<close>
- | s_conj (_, \<^const>\<open>False\<close>) = \<^const>\<open>False\<close>
+fun s_conj (\<^Const_>\<open>True\<close>, t2) = t2
+ | s_conj (t1, \<^Const_>\<open>True\<close>) = t1
+ | s_conj (\<^Const_>\<open>False\<close>, _) = \<^Const>\<open>False\<close>
+ | s_conj (_, \<^Const_>\<open>False\<close>) = \<^Const>\<open>False\<close>
| s_conj (t1, t2) = if t1 aconv t2 then t1 else HOLogic.mk_conj (t1, t2)
-fun s_disj (\<^const>\<open>False\<close>, t2) = t2
- | s_disj (t1, \<^const>\<open>False\<close>) = t1
- | s_disj (\<^const>\<open>True\<close>, _) = \<^const>\<open>True\<close>
- | s_disj (_, \<^const>\<open>True\<close>) = \<^const>\<open>True\<close>
+fun s_disj (\<^Const_>\<open>False\<close>, t2) = t2
+ | s_disj (t1, \<^Const_>\<open>False\<close>) = t1
+ | s_disj (\<^Const_>\<open>True\<close>, _) = \<^Const>\<open>True\<close>
+ | s_disj (_, \<^Const_>\<open>True\<close>) = \<^Const>\<open>True\<close>
| s_disj (t1, t2) = if t1 aconv t2 then t1 else HOLogic.mk_disj (t1, t2)
-fun s_imp (\<^const>\<open>True\<close>, t2) = t2
- | s_imp (t1, \<^const>\<open>False\<close>) = s_not t1
- | s_imp (\<^const>\<open>False\<close>, _) = \<^const>\<open>True\<close>
- | s_imp (_, \<^const>\<open>True\<close>) = \<^const>\<open>True\<close>
+fun s_imp (\<^Const_>\<open>True\<close>, t2) = t2
+ | s_imp (t1, \<^Const_>\<open>False\<close>) = s_not t1
+ | s_imp (\<^Const_>\<open>False\<close>, _) = \<^Const>\<open>True\<close>
+ | s_imp (_, \<^Const_>\<open>True\<close>) = \<^Const>\<open>True\<close>
| s_imp p = HOLogic.mk_imp p
-fun s_iff (\<^const>\<open>True\<close>, t2) = t2
- | s_iff (t1, \<^const>\<open>True\<close>) = t1
- | s_iff (\<^const>\<open>False\<close>, t2) = s_not t2
- | s_iff (t1, \<^const>\<open>False\<close>) = s_not t1
- | s_iff (t1, t2) = if t1 aconv t2 then \<^const>\<open>True\<close> else HOLogic.eq_const HOLogic.boolT $ t1 $ t2
+fun s_iff (\<^Const_>\<open>True\<close>, t2) = t2
+ | s_iff (t1, \<^Const_>\<open>True\<close>) = t1
+ | s_iff (\<^Const_>\<open>False\<close>, t2) = s_not t2
+ | s_iff (t1, \<^Const_>\<open>False\<close>) = s_not t1
+ | s_iff (t1, t2) = if t1 aconv t2 then \<^Const>\<open>True\<close> else HOLogic.eq_const HOLogic.boolT $ t1 $ t2
fun close_form t =
fold (fn ((s, i), T) => fn t' =>
@@ -352,18 +348,15 @@
t
fun unextensionalize_def t =
- case t of
- \<^const>\<open>Trueprop\<close> $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ lhs $ rhs) =>
- (case strip_comb lhs of
- (c as Const (_, T), args) =>
- if forall is_Var args andalso not (has_duplicates (op =) args) then
- \<^const>\<open>Trueprop\<close>
- $ (Const (\<^const_name>\<open>HOL.eq\<close>, T --> T --> \<^typ>\<open>bool\<close>)
- $ c $ fold_rev lambda args rhs)
- else
- t
- | _ => t)
- | _ => t
+ (case t of
+ \<^Const_>\<open>Trueprop for \<^Const_>\<open>HOL.eq _ for lhs rhs\<close>\<close> =>
+ (case strip_comb lhs of
+ (c as Const (_, T), args) =>
+ if forall is_Var args andalso not (has_duplicates (op =) args) then
+ \<^Const>\<open>Trueprop for \<^Const>\<open>HOL.eq T for c \<open>fold_rev lambda args rhs\<close>\<close>\<close>
+ else t
+ | _ => t)
+ | _ => t)
(* Converts an elim-rule into an equivalent theorem that does not have the
predicate variable. Leaves other theorems unchanged. We simply instantiate
@@ -371,9 +364,8 @@
"Meson_Clausify".) *)
fun transform_elim_prop t =
case Logic.strip_imp_concl t of
- \<^const>\<open>Trueprop\<close> $ Var (z, \<^typ>\<open>bool\<close>) =>
- subst_Vars [(z, \<^const>\<open>False\<close>)] t
- | Var (z, \<^typ>\<open>prop\<close>) => subst_Vars [(z, \<^prop>\<open>False\<close>)] t
+ \<^Const_>\<open>Trueprop for \<open>Var (z, \<^typ>\<open>bool\<close>)\<close>\<close> => subst_Vars [(z, \<^Const>\<open>False\<close>)] t
+ | Var (z, \<^Type>\<open>prop\<close>) => subst_Vars [(z, \<^prop>\<open>False\<close>)] t
| _ => t
fun specialize_type thy (s, T) t =
--- a/src/HOL/Tools/Argo/argo_real.ML Tue Sep 28 12:35:43 2021 +0200
+++ b/src/HOL/Tools/Argo/argo_real.ML Wed Sep 29 09:58:19 2021 +0200
@@ -12,25 +12,25 @@
fun trans_type _ \<^Type>\<open>real\<close> tcx = SOME (Argo_Expr.Real, tcx)
| trans_type _ _ _ = NONE
-fun trans_term f \<^Const_>\<open>uminus \<open>\<^Type>\<open>real\<close>\<close> for t\<close> tcx =
+fun trans_term f \<^Const_>\<open>uminus \<^Type>\<open>real\<close> for t\<close> tcx =
tcx |> f t |>> Argo_Expr.mk_neg |> SOME
- | trans_term f \<^Const_>\<open>plus \<open>\<^Type>\<open>real\<close>\<close> for t1 t2\<close> tcx =
+ | trans_term f \<^Const_>\<open>plus \<^Type>\<open>real\<close> for t1 t2\<close> tcx =
tcx |> f t1 ||>> f t2 |>> uncurry Argo_Expr.mk_add2 |> SOME
- | trans_term f \<^Const_>\<open>minus \<open>\<^Type>\<open>real\<close>\<close> for t1 t2\<close> tcx =
+ | trans_term f \<^Const_>\<open>minus \<^Type>\<open>real\<close> for t1 t2\<close> tcx =
tcx |> f t1 ||>> f t2 |>> uncurry Argo_Expr.mk_sub |> SOME
- | trans_term f \<^Const_>\<open>times \<open>\<^Type>\<open>real\<close>\<close> for t1 t2\<close> tcx =
+ | trans_term f \<^Const_>\<open>times \<^Type>\<open>real\<close> for t1 t2\<close> tcx =
tcx |> f t1 ||>> f t2 |>> uncurry Argo_Expr.mk_mul |> SOME
- | trans_term f \<^Const_>\<open>divide \<open>\<^Type>\<open>real\<close>\<close> for t1 t2\<close> tcx =
+ | trans_term f \<^Const_>\<open>divide \<^Type>\<open>real\<close> for t1 t2\<close> tcx =
tcx |> f t1 ||>> f t2 |>> uncurry Argo_Expr.mk_div |> SOME
- | trans_term f \<^Const_>\<open>min \<open>\<^Type>\<open>real\<close>\<close> for t1 t2\<close> tcx =
+ | trans_term f \<^Const_>\<open>min \<^Type>\<open>real\<close> for t1 t2\<close> tcx =
tcx |> f t1 ||>> f t2 |>> uncurry Argo_Expr.mk_min |> SOME
- | trans_term f \<^Const_>\<open>max \<open>\<^Type>\<open>real\<close>\<close> for t1 t2\<close> tcx =
+ | trans_term f \<^Const_>\<open>max \<^Type>\<open>real\<close> for t1 t2\<close> tcx =
tcx |> f t1 ||>> f t2 |>> uncurry Argo_Expr.mk_max |> SOME
- | trans_term f \<^Const_>\<open>abs \<open>\<^Type>\<open>real\<close>\<close> for t\<close> tcx =
+ | trans_term f \<^Const_>\<open>abs \<^Type>\<open>real\<close> for t\<close> tcx =
tcx |> f t |>> Argo_Expr.mk_abs |> SOME
- | trans_term f \<^Const_>\<open>less \<open>\<^Type>\<open>real\<close>\<close> for t1 t2\<close> tcx =
+ | trans_term f \<^Const_>\<open>less \<^Type>\<open>real\<close> for t1 t2\<close> tcx =
tcx |> f t1 ||>> f t2 |>> uncurry Argo_Expr.mk_lt |> SOME
- | trans_term f \<^Const_>\<open>less_eq \<open>\<^Type>\<open>real\<close>\<close> for t1 t2\<close> tcx =
+ | trans_term f \<^Const_>\<open>less_eq \<^Type>\<open>real\<close> for t1 t2\<close> tcx =
tcx |> f t1 ||>> f t2 |>> uncurry Argo_Expr.mk_le |> SOME
| trans_term _ t tcx =
(case try HOLogic.dest_number t of
@@ -40,12 +40,12 @@
(* reverse translation *)
-fun mk_plus t1 t2 = \<^Const>\<open>plus \<open>\<^Type>\<open>real\<close>\<close> for t1 t2\<close>
+fun mk_plus t1 t2 = \<^Const>\<open>plus \<^Type>\<open>real\<close> for t1 t2\<close>
fun mk_sum ts = uncurry (fold_rev mk_plus) (split_last ts)
-fun mk_times t1 t2 = \<^Const>\<open>times \<open>\<^Type>\<open>real\<close>\<close> for t1 t2\<close>
-fun mk_divide t1 t2 = \<^Const>\<open>divide \<open>\<^Type>\<open>real\<close>\<close> for t1 t2\<close>
-fun mk_le t1 t2 = \<^Const>\<open>less_eq \<open>\<^Type>\<open>real\<close>\<close> for t1 t2\<close>
-fun mk_lt t1 t2 = \<^Const>\<open>less \<open>\<^Type>\<open>real\<close>\<close> for t1 t2\<close>
+fun mk_times t1 t2 = \<^Const>\<open>times \<^Type>\<open>real\<close> for t1 t2\<close>
+fun mk_divide t1 t2 = \<^Const>\<open>divide \<^Type>\<open>real\<close> for t1 t2\<close>
+fun mk_le t1 t2 = \<^Const>\<open>less_eq \<^Type>\<open>real\<close> for t1 t2\<close>
+fun mk_lt t1 t2 = \<^Const>\<open>less \<^Type>\<open>real\<close> for t1 t2\<close>
fun mk_real_num i = HOLogic.mk_number \<^Type>\<open>real\<close> i
@@ -54,17 +54,17 @@
in if q = 1 then mk_real_num p else mk_divide (mk_real_num p) (mk_real_num q) end
fun term_of _ (Argo_Expr.E (Argo_Expr.Num n, _)) = SOME (mk_number n)
- | term_of f (Argo_Expr.E (Argo_Expr.Neg, [e])) = SOME \<^Const>\<open>uminus \<open>\<^Type>\<open>real\<close>\<close> for \<open>f e\<close>\<close>
+ | term_of f (Argo_Expr.E (Argo_Expr.Neg, [e])) = SOME \<^Const>\<open>uminus \<^Type>\<open>real\<close> for \<open>f e\<close>\<close>
| term_of f (Argo_Expr.E (Argo_Expr.Add, es)) = SOME (mk_sum (map f es))
| term_of f (Argo_Expr.E (Argo_Expr.Sub, [e1, e2])) =
- SOME \<^Const>\<open>minus \<open>\<^Type>\<open>real\<close>\<close> for \<open>f e1\<close> \<open>f e2\<close>\<close>
+ SOME \<^Const>\<open>minus \<^Type>\<open>real\<close> for \<open>f e1\<close> \<open>f e2\<close>\<close>
| term_of f (Argo_Expr.E (Argo_Expr.Mul, [e1, e2])) = SOME (mk_times (f e1) (f e2))
| term_of f (Argo_Expr.E (Argo_Expr.Div, [e1, e2])) = SOME (mk_divide (f e1) (f e2))
| term_of f (Argo_Expr.E (Argo_Expr.Min, [e1, e2])) =
- SOME \<^Const>\<open>min \<open>\<^Type>\<open>real\<close>\<close> for \<open>f e1\<close> \<open>f e2\<close>\<close>
+ SOME \<^Const>\<open>min \<^Type>\<open>real\<close> for \<open>f e1\<close> \<open>f e2\<close>\<close>
| term_of f (Argo_Expr.E (Argo_Expr.Max, [e1, e2])) =
- SOME \<^Const>\<open>max \<open>\<^Type>\<open>real\<close>\<close> for \<open>f e1\<close> \<open>f e2\<close>\<close>
- | term_of f (Argo_Expr.E (Argo_Expr.Abs, [e])) = SOME \<^Const>\<open>abs \<open>\<^Type>\<open>real\<close>\<close> for \<open>f e\<close>\<close>
+ SOME \<^Const>\<open>max \<^Type>\<open>real\<close> for \<open>f e1\<close> \<open>f e2\<close>\<close>
+ | term_of f (Argo_Expr.E (Argo_Expr.Abs, [e])) = SOME \<^Const>\<open>abs \<^Type>\<open>real\<close> for \<open>f e\<close>\<close>
| term_of f (Argo_Expr.E (Argo_Expr.Le, [e1, e2])) = SOME (mk_le (f e1) (f e2))
| term_of f (Argo_Expr.E (Argo_Expr.Lt, [e1, e2])) = SOME (mk_lt (f e1) (f e2))
| term_of _ _ = NONE
@@ -97,10 +97,10 @@
local
-fun is_add2 \<^Const_>\<open>plus \<open>\<^Type>\<open>real\<close>\<close> for _ _\<close> = true
+fun is_add2 \<^Const_>\<open>plus \<^Type>\<open>real\<close> for _ _\<close> = true
| is_add2 _ = false
-fun is_add3 \<^Const_>\<open>plus \<open>\<^Type>\<open>real\<close>\<close> for _ t\<close> = is_add2 t
+fun is_add3 \<^Const_>\<open>plus \<^Type>\<open>real\<close> for _ t\<close> = is_add2 t
| is_add3 _ = false
val flatten_thm = mk_rewr @{lemma "(a::real) + b + c = a + (b + c)" by simp}
--- a/src/HOL/Tools/Argo/argo_tactic.ML Tue Sep 28 12:35:43 2021 +0200
+++ b/src/HOL/Tools/Argo/argo_tactic.ML Wed Sep 29 09:58:19 2021 +0200
@@ -600,7 +600,7 @@
fun unclausify (thm, lits) ls =
(case (Thm.prop_of thm, lits) of
- (\<^Const_>\<open>Trueprop for \<open>\<^Const_>\<open>False\<close>\<close>\<close>, [(_, ct)]) =>
+ (\<^Const_>\<open>Trueprop for \<^Const_>\<open>False\<close>\<close>, [(_, ct)]) =>
let val thm = Thm.implies_intr ct thm
in (discharge thm unclausify_rule1 handle THM _ => discharge thm unclausify_rule2, ls) end
| _ => (thm, Ord_List.union lit_ord lits ls))
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Tue Sep 28 12:35:43 2021 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Wed Sep 29 09:58:19 2021 +0200
@@ -2215,7 +2215,7 @@
let
fun mk_goal c cps gcorec n k disc =
mk_Trueprop_eq (disc $ (gcorec $ c),
- if n = 1 then \<^const>\<open>True\<close>
+ if n = 1 then \<^Const>\<open>True\<close>
else Library.foldr1 HOLogic.mk_conj (seq_conds mk_maybe_not n k cps));
val goalss = @{map 6} (map2 oooo mk_goal) cs cpss gcorecs ns kss discss;
--- a/src/HOL/Tools/BNF/bnf_fp_rec_sugar_transfer.ML Tue Sep 28 12:35:43 2021 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_rec_sugar_transfer.ML Wed Sep 29 09:58:19 2021 +0200
@@ -42,7 +42,7 @@
let
fun instantiate_with_lambda thm =
let
- val prop as \<^const>\<open>Trueprop\<close> $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ (Var (_, fT) $ _) $ _) =
+ val prop as \<^Const_>\<open>Trueprop for \<open>\<^Const_>\<open>HOL.eq _ for \<open>Var (_, fT) $ _\<close> _\<close>\<close>\<close> =
Thm.prop_of thm;
val T = range_type fT;
val j = Term.maxidx_of_term prop + 1;
--- a/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML Tue Sep 28 12:35:43 2021 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML Wed Sep 29 09:58:19 2021 +0200
@@ -385,7 +385,7 @@
val ssig_map_thms = #map_thms ssig_fp_bnf_sugar;
val all_algLam_alg_pointfuls = map (mk_pointful ctxt) all_algLam_algs;
- val \<^const>\<open>Trueprop\<close> $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ lhs $ rhs) = code_goal;
+ val \<^Const_>\<open>Trueprop for \<^Const_>\<open>HOL.eq _ for lhs rhs\<close>\<close> = code_goal;
val (fun_t, args) = strip_comb lhs;
val closed_rhs = fold_rev lambda args rhs;
@@ -447,7 +447,7 @@
val fp_nesting_Ts = map T_of_bnf fp_nesting_bnfs;
- fun is_nullary_disc_def (\<^const>\<open>Trueprop\<close> $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ _
+ fun is_nullary_disc_def (\<^Const>\<open>Trueprop\<close> $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ _
$ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ _ $ _))) = true
| is_nullary_disc_def (Const (\<^const_name>\<open>Pure.eq\<close>, _) $ _
$ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ _ $ _)) = true
@@ -512,7 +512,7 @@
val goal = mk_Trueprop_eq (fun_t, abs_curried_balanced arg_Ts algrho);
fun const_of_transfer thm =
- (case Thm.prop_of thm of \<^const>\<open>Trueprop\<close> $ (_ $ cst $ _) => cst);
+ (case Thm.prop_of thm of \<^Const>\<open>Trueprop\<close> $ (_ $ cst $ _) => cst);
val eq_algrho =
Goal.prove (*no sorry*) ctxt [] [] goal (fn {context = ctxt, prems = _} =>
@@ -590,7 +590,7 @@
fun derive_cong_ctr_intros ctxt cong_ctor_intro =
let
- val \<^const>\<open>Pure.imp\<close> $ _ $ (\<^const>\<open>Trueprop\<close> $ ((Rcong as _ $ _) $ _ $ (ctor $ _))) =
+ val \<^Const_>\<open>Pure.imp\<close> $ _ $ (\<^Const_>\<open>Trueprop\<close> $ ((Rcong as _ $ _) $ _ $ (ctor $ _))) =
Thm.prop_of cong_ctor_intro;
val fpT as Type (fpT_name, fp_argTs) = range_type (fastype_of ctor);
@@ -615,19 +615,19 @@
fun derive_cong_friend_intro ctxt cong_algrho_intro =
let
- val \<^const>\<open>Pure.imp\<close> $ _ $ (\<^const>\<open>Trueprop\<close> $ ((Rcong as _ $ _) $ _
+ val \<^Const_>\<open>Pure.imp\<close> $ _ $ (\<^Const_>\<open>Trueprop\<close> $ ((Rcong as _ $ _) $ _
$ ((algrho as Const (algrho_name, _)) $ _))) =
Thm.prop_of cong_algrho_intro;
val fpT as Type (_, fp_argTs) = range_type (fastype_of algrho);
- fun has_algrho (\<^const>\<open>Trueprop\<close> $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ _ $ rhs)) =
+ fun has_algrho (\<^Const_>\<open>Trueprop\<close> $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ _ $ rhs)) =
fst (dest_Const (head_of (strip_abs_body rhs))) = algrho_name;
val eq_algrho :: _ =
maps (filter (has_algrho o Thm.prop_of) o #eq_algrhos o snd) (all_friend_extras_of ctxt);
- val \<^const>\<open>Trueprop\<close> $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ friend0 $ _) = Thm.prop_of eq_algrho;
+ val \<^Const_>\<open>Trueprop\<close> $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ friend0 $ _) = Thm.prop_of eq_algrho;
val friend = mk_ctr fp_argTs friend0;
val goal = mk_cong_intro_ctr_or_friend_goal ctxt fpT Rcong friend;
@@ -654,8 +654,8 @@
let
val thy = Proof_Context.theory_of ctxt;
- val \<^const>\<open>Pure.imp\<close> $ (\<^const>\<open>Trueprop\<close> $ (_ $ Abs (_, _, _ $
- Abs (_, _, \<^const>\<open>implies\<close> $ _ $ (_ $ (cong0 $ _) $ _ $ _))))) $ _ =
+ val \<^Const_>\<open>Pure.imp\<close> $ (\<^Const_>\<open>Trueprop\<close> $ (_ $ Abs (_, _, _ $
+ Abs (_, _, \<^Const_>\<open>implies\<close> $ _ $ (_ $ (cong0 $ _) $ _ $ _))))) $ _ =
Thm.prop_of dtor_coinduct;
val SOME {X as TVar ((X_s, _), _), fp_res = {dtor_ctors, ...}, pre_bnf,
@@ -820,7 +820,7 @@
|> curry (op ~~) (map (fn disc => disc $ lhs) discs);
fun mk_disc_iff_props props [] = props
- | mk_disc_iff_props _ ((lhs, \<^const>\<open>HOL.True\<close>) :: _) = [lhs]
+ | mk_disc_iff_props _ ((lhs, \<^Const_>\<open>True\<close>) :: _) = [lhs]
| mk_disc_iff_props props ((lhs, rhs) :: views) =
mk_disc_iff_props ((HOLogic.mk_eq (lhs, rhs)) :: props) views;
in
@@ -2242,7 +2242,7 @@
val fun_T =
(case code_goal of
- \<^const>\<open>Trueprop\<close> $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ t $ _) => fastype_of (head_of t)
+ \<^Const_>\<open>Trueprop\<close> $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ t $ _) => fastype_of (head_of t)
| _ => ill_formed_equation_lhs_rhs lthy [code_goal]);
val fun_t = Const (fun_name, fun_T);
--- a/src/HOL/Tools/BNF/bnf_gfp_grec_sugar_util.ML Tue Sep 28 12:35:43 2021 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_grec_sugar_util.ML Wed Sep 29 09:58:19 2021 +0200
@@ -367,7 +367,7 @@
ctrXs_Tss
|> map_index (fn (i, Ts) =>
Abs (Name.uu, mk_tupleT_balanced Ts,
- if i + 1 = k then \<^const>\<open>HOL.True\<close> else \<^const>\<open>HOL.False\<close>))
+ if i + 1 = k then \<^Const>\<open>True\<close> else \<^Const>\<open>False\<close>))
|> mk_case_sumN_balanced
|> map_types substXYT
|> (fn tm => Library.foldl1 HOLogic.mk_comp [tm, rep, snd_const YpreT])
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Tue Sep 28 12:35:43 2021 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Wed Sep 29 09:58:19 2021 +0200
@@ -189,22 +189,22 @@
fun sort_list_duplicates xs = map snd (sort (int_ord o apply2 fst) xs);
-val mk_conjs = try (foldr1 HOLogic.mk_conj) #> the_default \<^const>\<open>True\<close>;
-val mk_disjs = try (foldr1 HOLogic.mk_disj) #> the_default \<^const>\<open>False\<close>;
+val mk_conjs = try (foldr1 HOLogic.mk_conj) #> the_default \<^Const>\<open>True\<close>;
+val mk_disjs = try (foldr1 HOLogic.mk_disj) #> the_default \<^Const>\<open>False\<close>;
val mk_dnf = mk_disjs o map mk_conjs;
-val conjuncts_s = filter_out (curry (op aconv) \<^const>\<open>True\<close>) o HOLogic.conjuncts;
+val conjuncts_s = filter_out (curry (op aconv) \<^Const>\<open>True\<close>) o HOLogic.conjuncts;
-fun s_not \<^const>\<open>True\<close> = \<^const>\<open>False\<close>
- | s_not \<^const>\<open>False\<close> = \<^const>\<open>True\<close>
- | s_not (\<^const>\<open>Not\<close> $ t) = t
- | s_not (\<^const>\<open>conj\<close> $ t $ u) = \<^const>\<open>disj\<close> $ s_not t $ s_not u
- | s_not (\<^const>\<open>disj\<close> $ t $ u) = \<^const>\<open>conj\<close> $ s_not t $ s_not u
- | s_not t = \<^const>\<open>Not\<close> $ t;
+fun s_not \<^Const_>\<open>True\<close> = \<^Const>\<open>False\<close>
+ | s_not \<^Const_>\<open>False\<close> = \<^Const>\<open>True\<close>
+ | s_not \<^Const_>\<open>Not for t\<close> = t
+ | s_not \<^Const_>\<open>conj for t u\<close> = \<^Const>\<open>disj for \<open>s_not t\<close> \<open>s_not u\<close>\<close>
+ | s_not \<^Const_>\<open>disj for t u\<close> = \<^Const>\<open>conj for \<open>s_not t\<close> \<open>s_not u\<close>\<close>
+ | s_not t = \<^Const>\<open>Not for t\<close>;
val s_not_conj = conjuncts_s o s_not o mk_conjs;
-fun propagate_unit_pos u cs = if member (op aconv) cs u then [\<^const>\<open>False\<close>] else cs;
+fun propagate_unit_pos u cs = if member (op aconv) cs u then [\<^Const>\<open>False\<close>] else cs;
fun propagate_unit_neg not_u cs = remove (op aconv) not_u cs;
fun propagate_units css =
@@ -215,17 +215,17 @@
(map (propagate_unit_pos u) (uss @ css'))));
fun s_conjs cs =
- if member (op aconv) cs \<^const>\<open>False\<close> then \<^const>\<open>False\<close>
- else mk_conjs (remove (op aconv) \<^const>\<open>True\<close> cs);
+ if member (op aconv) cs \<^Const>\<open>False\<close> then \<^Const>\<open>False\<close>
+ else mk_conjs (remove (op aconv) \<^Const>\<open>True\<close> cs);
fun s_disjs ds =
- if member (op aconv) ds \<^const>\<open>True\<close> then \<^const>\<open>True\<close>
- else mk_disjs (remove (op aconv) \<^const>\<open>False\<close> ds);
+ if member (op aconv) ds \<^Const>\<open>True\<close> then \<^Const>\<open>True\<close>
+ else mk_disjs (remove (op aconv) \<^Const>\<open>False\<close> ds);
fun s_dnf css0 =
let val css = propagate_units css0 in
if null css then
- [\<^const>\<open>False\<close>]
+ [\<^Const>\<open>False\<close>]
else if exists null css then
[]
else
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML Tue Sep 28 12:35:43 2021 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML Wed Sep 29 09:58:19 2021 +0200
@@ -154,7 +154,7 @@
fun inst_split_eq ctxt split =
(case Thm.prop_of split of
- \<^const>\<open>Trueprop\<close> $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ (Var (_, Type (_, [T, _])) $ _) $ _) =>
+ \<^Const_>\<open>Trueprop for \<^Const_>\<open>HOL.eq _ for \<open>Var (_, Type (_, [T, _])) $ _\<close> _\<close>\<close> =>
let
val s = Name.uu;
val eq = Abs (Name.uu, T, HOLogic.mk_eq (Free (s, T), Bound 0));
--- a/src/HOL/Tools/BNF/bnf_lfp_countable.ML Tue Sep 28 12:35:43 2021 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_countable.ML Wed Sep 29 09:58:19 2021 +0200
@@ -70,13 +70,13 @@
fun encode_sumN n k t =
Balanced_Tree.access {init = t,
- left = fn t => \<^const>\<open>sum_encode\<close> $ (@{const Inl (nat, nat)} $ t),
- right = fn t => \<^const>\<open>sum_encode\<close> $ (@{const Inr (nat, nat)} $ t)}
+ left = fn t => \<^Const>\<open>sum_encode for \<^Const>\<open>Inl \<^Type>\<open>nat\<close> \<^Type>\<open>nat\<close> for t\<close>\<close>,
+ right = fn t => \<^Const>\<open>sum_encode for \<^Const>\<open>Inr \<^Type>\<open>nat\<close> \<^Type>\<open>nat\<close> for t\<close>\<close>}
n k;
-fun encode_tuple [] = \<^term>\<open>0 :: nat\<close>
+fun encode_tuple [] = \<^Const>\<open>zero_class.zero \<^Type>\<open>nat\<close>\<close>
| encode_tuple ts =
- Balanced_Tree.make (fn (t, u) => \<^const>\<open>prod_encode\<close> $ (@{const Pair (nat, nat)} $ u $ t)) ts;
+ Balanced_Tree.make (fn (t, u) => \<^Const>\<open>prod_encode for \<^Const>\<open>Pair \<^Type>\<open>nat\<close> \<^Type>\<open>nat\<close> for u t\<close>\<close>) ts;
fun mk_encode_funs ctxt fpTs ns ctrss0 recs0 =
let
@@ -181,7 +181,7 @@
|> map (Thm.close_derivation \<^here>)
end;
-fun get_countable_goal_type_name (\<^const>\<open>Trueprop\<close> $ (Const (\<^const_name>\<open>Ex\<close>, _)
+fun get_countable_goal_type_name (\<^Const>\<open>Trueprop\<close> $ (Const (\<^const_name>\<open>Ex\<close>, _)
$ Abs (_, Type (_, [Type (s, _), _]), Const (\<^const_name>\<open>inj_on\<close>, _) $ Bound 0
$ Const (\<^const_name>\<open>top\<close>, _)))) = s
| get_countable_goal_type_name _ = error "Wrong goal format for datatype countability tactic";
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Tue Sep 28 12:35:43 2021 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Wed Sep 29 09:58:19 2021 +0200
@@ -303,11 +303,11 @@
fun name_of_disc t =
(case head_of t of
- Abs (_, _, \<^const>\<open>Not\<close> $ (t' $ Bound 0)) =>
+ Abs (_, _, \<^Const_>\<open>Not for \<open>t' $ Bound 0\<close>\<close>) =>
Long_Name.map_base_name (prefix not_prefix) (name_of_disc t')
- | Abs (_, _, Const (\<^const_name>\<open>HOL.eq\<close>, _) $ Bound 0 $ t') =>
+ | Abs (_, _, \<^Const_>\<open>HOL.eq _ for \<open>Bound 0\<close> t'\<close>) =>
Long_Name.map_base_name (prefix is_prefix) (name_of_disc t')
- | Abs (_, _, \<^const>\<open>Not\<close> $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ Bound 0 $ t')) =>
+ | Abs (_, _, \<^Const_>\<open>Not for \<^Const_>\<open>HOL.eq _ for \<open>Bound 0\<close> t'\<close>\<close>) =>
Long_Name.map_base_name (prefix (not_prefix ^ is_prefix)) (name_of_disc t')
| t' => name_of_const "discriminator" (perhaps (try domain_type)) t');
@@ -1037,7 +1037,7 @@
val disc_eq_case_thms =
let
- fun const_of_bool b = if b then \<^const>\<open>True\<close> else \<^const>\<open>False\<close>;
+ fun const_of_bool b = if b then \<^Const>\<open>True\<close> else \<^Const>\<open>False\<close>;
fun mk_case_args n = map_index (fn (k, argTs) =>
fold_rev Term.absdummy argTs (const_of_bool (n = k))) ctr_Tss;
val goals = map_index (fn (n, udisc) =>
--- a/src/HOL/Tools/Lifting/lifting_def_code_dt.ML Tue Sep 28 12:35:43 2021 +0200
+++ b/src/HOL/Tools/Lifting/lifting_def_code_dt.ML Wed Sep 29 09:58:19 2021 +0200
@@ -400,7 +400,7 @@
let val (sel_rhs, wits) = mk_sel_case_args lthy4 ctr_Tss ks arg
in (arg |> #2, wits, list_comb (mk_sel_casex arg, sel_rhs)) end;
fun mk_dis_case_args args k = map (fn (k', arg) => (if k = k'
- then fold_rev Term.lambda arg \<^const>\<open>True\<close> else fold_rev Term.lambda arg \<^const>\<open>False\<close>)) args;
+ then fold_rev Term.lambda arg \<^Const>\<open>True\<close> else fold_rev Term.lambda arg \<^Const>\<open>False\<close>)) args;
val sel_rhs = map (map mk_sel_rhs) sel_argss
val dis_rhs = map (fn k => list_comb (dis_casex, mk_dis_case_args (ks ~~ xss) k)) ks
val dis_qty = qty_isom --> HOLogic.boolT;
--- a/src/HOL/Tools/Meson/meson.ML Tue Sep 28 12:35:43 2021 +0200
+++ b/src/HOL/Tools/Meson/meson.ML Wed Sep 29 09:58:19 2021 +0200
@@ -261,9 +261,9 @@
fun refl_clause_aux 0 th = th
| refl_clause_aux n th =
case HOLogic.dest_Trueprop (Thm.concl_of th) of
- \<^Const_>\<open>disj for \<open>\<^Const_>\<open>disj for _ _\<close>\<close> _\<close> =>
+ \<^Const_>\<open>disj for \<^Const_>\<open>disj for _ _\<close> _\<close> =>
refl_clause_aux n (th RS disj_assoc) (*isolate an atom as first disjunct*)
- | \<^Const_>\<open>disj for \<open>\<^Const_>\<open>Not for \<open>\<^Const_>\<open>HOL.eq _ for t u\<close>\<close>\<close>\<close> _\<close> =>
+ | \<^Const_>\<open>disj for \<^Const_>\<open>Not for \<^Const_>\<open>HOL.eq _ for t u\<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*)
@@ -271,7 +271,7 @@
| _ => (*not a disjunction*) th;
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 \<^Const_>\<open>Not for \<^Const_>\<open>HOL.eq _ for _ _\<close>\<close> = 1
| notequal_lits_count _ = 0;
(*Simplify a clause by applying reflexivity to its negated equality literals*)
@@ -414,7 +414,7 @@
(**** Generation of contrapositives ****)
-fun is_left \<^Const_>\<open>Trueprop for \<open>\<^Const_>\<open>disj for \<open>\<^Const_>\<open>disj for _ _\<close>\<close> _\<close>\<close>\<close> = true
+fun is_left \<^Const_>\<open>Trueprop for \<^Const_>\<open>disj for \<^Const_>\<open>disj for _ _\<close> _\<close>\<close> = true
| is_left _ = false;
(*Associate disjuctions to right -- make leftmost disjunct a LITERAL*)
@@ -435,7 +435,7 @@
fun rigid t = not (is_Var (head_of t));
-fun ok4horn \<^Const_>\<open>Trueprop for \<open>\<^Const_>\<open>disj for t _\<close>\<close>\<close> = rigid t
+fun ok4horn \<^Const_>\<open>Trueprop for \<^Const_>\<open>disj for t _\<close>\<close> = rigid t
| ok4horn \<^Const_>\<open>Trueprop for t\<close> = rigid t
| ok4horn _ = false;
@@ -470,7 +470,7 @@
(***** MESON PROOF PROCEDURE *****)
-fun rhyps (\<^Const_>\<open>Pure.imp for \<open>\<^Const_>\<open>Trueprop for A\<close>\<close> phi\<close>, As) = rhyps(phi, A::As)
+fun rhyps (\<^Const_>\<open>Pure.imp for \<^Const_>\<open>Trueprop for A\<close> phi\<close>, As) = rhyps(phi, A::As)
| rhyps (_, As) = As;
(** Detecting repeated assumptions in a subgoal **)
@@ -514,7 +514,7 @@
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_>\<open>Trueprop for \<open>\<^Const_>\<open>Not for t\<close>\<close>\<close> = rigid t
+fun ok4nnf \<^Const_>\<open>Trueprop for \<^Const_>\<open>Not for t\<close>\<close> = rigid t
| ok4nnf \<^Const_>\<open>Trueprop for t\<close> = rigid t
| ok4nnf _ = false;
@@ -620,7 +620,7 @@
(* 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 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> =>
+ \<^Const_>\<open>Trueprop for \<^Const_>\<open>Not for \<^Const_>\<open>HOL.eq T for \<open>t as _ $ _\<close> \<open>u as _ $ _\<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)
--- a/src/HOL/Tools/Nitpick/nitpick.ML Tue Sep 28 12:35:43 2021 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick.ML Wed Sep 29 09:58:19 2021 +0200
@@ -182,8 +182,7 @@
fun none_true assigns = forall (not_equal (SOME true) o snd) assigns
-fun has_lonely_bool_var (\<^const>\<open>Pure.conjunction\<close>
- $ (\<^const>\<open>Trueprop\<close> $ Free _) $ _) = true
+fun has_lonely_bool_var \<^Const_>\<open>Pure.conjunction for \<^Const_>\<open>Trueprop for \<open>Free _\<close>\<close> _\<close> = true
| has_lonely_bool_var _ = false
val syntactic_sorts =
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Tue Sep 28 12:35:43 2021 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Wed Sep 29 09:58:19 2021 +0200
@@ -331,16 +331,16 @@
else
s
-fun s_conj (t1, \<^const>\<open>True\<close>) = t1
- | s_conj (\<^const>\<open>True\<close>, t2) = t2
+fun s_conj (t1, \<^Const_>\<open>True\<close>) = t1
+ | s_conj (\<^Const_>\<open>True\<close>, t2) = t2
| s_conj (t1, t2) =
- if t1 = \<^const>\<open>False\<close> orelse t2 = \<^const>\<open>False\<close> then \<^const>\<open>False\<close>
+ if t1 = \<^Const>\<open>False\<close> orelse t2 = \<^Const>\<open>False\<close> then \<^Const>\<open>False\<close>
else HOLogic.mk_conj (t1, t2)
-fun s_disj (t1, \<^const>\<open>False\<close>) = t1
- | s_disj (\<^const>\<open>False\<close>, t2) = t2
+fun s_disj (t1, \<^Const_>\<open>False\<close>) = t1
+ | s_disj (\<^Const_>\<open>False\<close>, t2) = t2
| s_disj (t1, t2) =
- if t1 = \<^const>\<open>True\<close> orelse t2 = \<^const>\<open>True\<close> then \<^const>\<open>True\<close>
+ if t1 = \<^Const>\<open>True\<close> orelse t2 = \<^Const>\<open>True\<close> then \<^Const>\<open>True\<close>
else HOLogic.mk_disj (t1, t2)
fun strip_connective conn_t (t as (t0 $ t1 $ t2)) =
@@ -348,13 +348,13 @@
| strip_connective _ t = [t]
fun strip_any_connective (t as (t0 $ _ $ _)) =
- if t0 = \<^const>\<open>HOL.conj\<close> orelse t0 = \<^const>\<open>HOL.disj\<close> then
+ if t0 = \<^Const>\<open>conj\<close> orelse t0 = \<^Const>\<open>disj\<close> then
(strip_connective t0 t, t0)
else
- ([t], \<^const>\<open>Not\<close>)
- | strip_any_connective t = ([t], \<^const>\<open>Not\<close>)
-val conjuncts_of = strip_connective \<^const>\<open>HOL.conj\<close>
-val disjuncts_of = strip_connective \<^const>\<open>HOL.disj\<close>
+ ([t], \<^Const>\<open>Not\<close>)
+ | strip_any_connective t = ([t], \<^Const>\<open>Not\<close>)
+val conjuncts_of = strip_connective \<^Const>\<open>conj\<close>
+val disjuncts_of = strip_connective \<^Const>\<open>disj\<close>
(* When you add constants to these lists, make sure to handle them in
"Nitpick_Nut.nut_from_term", and perhaps in "Nitpick_Mono.consider_term" as
@@ -797,8 +797,8 @@
the (Quotient_Info.lookup_quotients thy s)
val partial =
case Thm.prop_of equiv_thm of
- \<^const>\<open>Trueprop\<close> $ (Const (\<^const_name>\<open>equivp\<close>, _) $ _) => false
- | \<^const>\<open>Trueprop\<close> $ (Const (\<^const_name>\<open>part_equivp\<close>, _) $ _) => true
+ \<^Const_>\<open>Trueprop for \<^Const_>\<open>equivp _ for _\<close>\<close> => false
+ | \<^Const_>\<open>Trueprop for \<^Const_>\<open>part_equivp _ for _\<close>\<close> => true
| _ => raise NOT_SUPPORTED "Ill-formed quotient type equivalence \
\relation theorem"
val Ts' = qtyp |> dest_Type |> snd
@@ -948,7 +948,7 @@
fold (fn (z as ((s, _), T)) => fn t' =>
Logic.all_const T $ Abs (s, T, abstract_over (Var z, t')))
(take (length zs' - length zs) zs')
- fun aux zs (\<^const>\<open>Pure.imp\<close> $ t1 $ t2) =
+ fun aux zs \<^Const>\<open>Pure.imp for t1 t2\<close> =
let val zs' = Term.add_vars t1 zs in
close_up zs zs' (Logic.mk_implies (t1, aux zs' t2))
end
@@ -957,8 +957,8 @@
fun distinctness_formula T =
all_distinct_unordered_pairs_of
- #> map (fn (t1, t2) => \<^const>\<open>Not\<close> $ (HOLogic.eq_const T $ t1 $ t2))
- #> List.foldr (s_conj o swap) \<^const>\<open>True\<close>
+ #> map (fn (t1, t2) => \<^Const>\<open>Not\<close> $ (HOLogic.eq_const T $ t1 $ t2))
+ #> List.foldr (s_conj o swap) \<^Const>\<open>True\<close>
fun zero_const T = Const (\<^const_name>\<open>zero_class.zero\<close>, T)
fun suc_const T = Const (\<^const_name>\<open>Suc\<close>, T --> T)
@@ -986,7 +986,7 @@
SOME {abs_type, rep_type, Abs_name, ...} =>
[(Abs_name, varify_and_instantiate_type ctxt abs_type T rep_type --> T)]
| NONE =>
- if T = \<^typ>\<open>ind\<close> then [dest_Const \<^const>\<open>Zero_Rep\<close>, dest_Const \<^const>\<open>Suc_Rep\<close>]
+ if T = \<^typ>\<open>ind\<close> then [dest_Const \<^Const>\<open>Zero_Rep\<close>, dest_Const \<^Const>\<open>Suc_Rep\<close>]
else [])
| uncached_data_type_constrs _ _ = []
@@ -1145,8 +1145,8 @@
if t1' aconv t2 then \<^prop>\<open>True\<close> else t1 $ t2
| s_betapply _ (t1 as Const (\<^const_name>\<open>HOL.eq\<close>, _) $ t1', t2) =
if t1' aconv t2 then \<^term>\<open>True\<close> else t1 $ t2
- | s_betapply _ (Const (\<^const_name>\<open>If\<close>, _) $ \<^const>\<open>True\<close> $ t1', _) = t1'
- | s_betapply _ (Const (\<^const_name>\<open>If\<close>, _) $ \<^const>\<open>False\<close> $ _, t2) = t2
+ | s_betapply _ (Const (\<^const_name>\<open>If\<close>, _) $ \<^Const_>\<open>True\<close> $ t1', _) = t1'
+ | s_betapply _ (Const (\<^const_name>\<open>If\<close>, _) $ \<^Const_>\<open>False\<close> $ _, t2) = t2
| s_betapply Ts (Const (\<^const_name>\<open>Let\<close>,
Type (_, [bound_T, Type (_, [_, body_T])]))
$ t12 $ Abs (s, T, t13'), t2) =
@@ -1181,18 +1181,18 @@
fun discr_term_for_constr hol_ctxt (x as (s, T)) =
let val dataT = body_type T in
if s = \<^const_name>\<open>Suc\<close> then
- Abs (Name.uu, dataT, \<^const>\<open>Not\<close> $ HOLogic.mk_eq (zero_const dataT, Bound 0))
+ Abs (Name.uu, dataT, \<^Const>\<open>Not\<close> $ HOLogic.mk_eq (zero_const dataT, Bound 0))
else if length (data_type_constrs hol_ctxt dataT) >= 2 then
Const (discr_for_constr x)
else
- Abs (Name.uu, dataT, \<^const>\<open>True\<close>)
+ Abs (Name.uu, dataT, \<^Const>\<open>True\<close>)
end
fun discriminate_value (hol_ctxt as {ctxt, ...}) x t =
case head_of t of
Const x' =>
- if x = x' then \<^const>\<open>True\<close>
- else if is_nonfree_constr ctxt x' then \<^const>\<open>False\<close>
+ if x = x' then \<^Const>\<open>True\<close>
+ else if is_nonfree_constr ctxt x' then \<^Const>\<open>False\<close>
else s_betapply [] (discr_term_for_constr hol_ctxt x, t)
| _ => s_betapply [] (discr_term_for_constr hol_ctxt x, t)
@@ -1379,10 +1379,10 @@
simplification rules (equational specifications). *)
fun term_under_def t =
case t of
- \<^const>\<open>Pure.imp\<close> $ _ $ t2 => term_under_def t2
- | Const (\<^const_name>\<open>Pure.eq\<close>, _) $ t1 $ _ => term_under_def t1
- | \<^const>\<open>Trueprop\<close> $ t1 => term_under_def t1
- | Const (\<^const_name>\<open>HOL.eq\<close>, _) $ t1 $ _ => term_under_def t1
+ \<^Const_>\<open>Pure.imp for _ t2\<close> => term_under_def t2
+ | \<^Const_>\<open>Pure.eq _ for t1 _\<close> => term_under_def t1
+ | \<^Const_>\<open>Trueprop for t1\<close> => term_under_def t1
+ | \<^Const_>\<open>HOL.eq _ for t1 _\<close> => term_under_def t1
| Abs (_, _, t') => term_under_def t'
| t1 $ _ => term_under_def t1
| _ => t
@@ -1405,9 +1405,8 @@
| aux _ _ = NONE
val (lhs, rhs) =
case t of
- Const (\<^const_name>\<open>Pure.eq\<close>, _) $ t1 $ t2 => (t1, t2)
- | \<^const>\<open>Trueprop\<close> $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ t1 $ t2) =>
- (t1, t2)
+ \<^Const_>\<open>Pure.eq _ for t1 t2\<close> => (t1, t2)
+ | \<^Const_>\<open>Trueprop for \<^Const_>\<open>HOL.eq _ for t1 t2\<close>\<close> => (t1, t2)
| _ => raise TERM ("Nitpick_HOL.normalized_rhs_of", [t])
val args = strip_comb lhs |> snd
in fold_rev aux args (SOME rhs) end
@@ -1482,13 +1481,13 @@
fun lhs_of_equation t =
case t of
- Const (\<^const_name>\<open>Pure.all\<close>, _) $ Abs (_, _, t1) => lhs_of_equation t1
- | Const (\<^const_name>\<open>Pure.eq\<close>, _) $ t1 $ _ => SOME t1
- | \<^const>\<open>Pure.imp\<close> $ _ $ t2 => lhs_of_equation t2
- | \<^const>\<open>Trueprop\<close> $ t1 => lhs_of_equation t1
- | Const (\<^const_name>\<open>All\<close>, _) $ Abs (_, _, t1) => lhs_of_equation t1
- | Const (\<^const_name>\<open>HOL.eq\<close>, _) $ t1 $ _ => SOME t1
- | \<^const>\<open>HOL.implies\<close> $ _ $ t2 => lhs_of_equation t2
+ \<^Const_>\<open>Pure.all _ for \<open>Abs (_, _, t1)\<close>\<close> => lhs_of_equation t1
+ | \<^Const_>\<open>Pure.eq _ for t1 _\<close> => SOME t1
+ | \<^Const_>\<open>Pure.imp for _ t2\<close> => lhs_of_equation t2
+ | \<^Const_>\<open>Trueprop for t1\<close> => lhs_of_equation t1
+ | \<^Const_>\<open>All _ for \<open>Abs (_, _, t1)\<close>\<close> => lhs_of_equation t1
+ | \<^Const_>\<open>HOL.eq _ for t1 _\<close> => SOME t1
+ | \<^Const_>\<open>implies for _ t2\<close> => lhs_of_equation t2
| _ => NONE
fun is_constr_pattern _ (Bound _) = true
@@ -1598,19 +1597,19 @@
(incr_boundvars 1 func_t, x),
discriminate_value hol_ctxt x (Bound 0)))
|> AList.group (op aconv)
- |> map (apsnd (List.foldl s_disj \<^const>\<open>False\<close>))
+ |> map (apsnd (List.foldl s_disj \<^Const>\<open>False\<close>))
|> sort (int_ord o apply2 (size_of_term o snd))
|> rev
in
if res_T = bool_T then
- if forall (member (op =) [\<^const>\<open>False\<close>, \<^const>\<open>True\<close>] o fst) cases then
+ if forall (member (op =) [\<^Const>\<open>False\<close>, \<^Const>\<open>True\<close>] o fst) cases then
case cases of
[(body_t, _)] => body_t
- | [_, (\<^const>\<open>True\<close>, head_t2)] => head_t2
- | [_, (\<^const>\<open>False\<close>, head_t2)] => \<^const>\<open>Not\<close> $ head_t2
+ | [_, (\<^Const>\<open>True\<close>, head_t2)] => head_t2
+ | [_, (\<^Const>\<open>False\<close>, head_t2)] => \<^Const>\<open>Not for head_t2\<close>
| _ => raise BAD ("Nitpick_HOL.optimized_case_def", "impossible cases")
else
- \<^const>\<open>True\<close> |> fold_rev (add_constr_case res_T) cases
+ \<^Const>\<open>True\<close> |> fold_rev (add_constr_case res_T) cases
else
fst (hd cases) |> fold_rev (add_constr_case res_T) (tl cases)
end
@@ -1895,13 +1894,12 @@
in
Logic.list_implies (prems,
case concl of
- \<^const>\<open>Trueprop\<close> $ (Const (\<^const_name>\<open>HOL.eq\<close>, Type (_, [T, _]))
- $ t1 $ t2) =>
- \<^const>\<open>Trueprop\<close> $ extensional_equal j T t1 t2
- | \<^const>\<open>Trueprop\<close> $ t' =>
- \<^const>\<open>Trueprop\<close> $ HOLogic.mk_eq (t', \<^const>\<open>True\<close>)
- | Const (\<^const_name>\<open>Pure.eq\<close>, Type (_, [T, _])) $ t1 $ t2 =>
- \<^const>\<open>Trueprop\<close> $ extensional_equal j T t1 t2
+ \<^Const_>\<open>Trueprop for \<^Const_>\<open>HOL.eq T for t1 t2\<close>\<close> =>
+ \<^Const>\<open>Trueprop for \<open>extensional_equal j T t1 t2\<close>\<close>
+ | \<^Const_>\<open>Trueprop for t'\<close> =>
+ \<^Const>\<open>Trueprop for \<open>HOLogic.mk_eq (t', \<^Const>\<open>True\<close>)\<close>\<close>
+ | \<^Const_>\<open>Pure.eq T for t1 t2\<close> =>
+ \<^Const>\<open>Trueprop for \<open>extensional_equal j T t1 t2\<close>\<close>
| _ => (warning ("Ignoring " ^ quote tag ^ " for non-equation " ^
quote (Syntax.string_of_term ctxt t));
raise SAME ()))
@@ -1951,7 +1949,7 @@
end
fun ground_theorem_table thy =
- fold ((fn \<^const>\<open>Trueprop\<close> $ t1 =>
+ fold ((fn \<^Const_>\<open>Trueprop for t1\<close> =>
is_ground_term t1 ? Inttab.map_default (hash_term t1, []) (cons t1)
| _ => I) o Thm.prop_of o snd) (Global_Theory.all_thms_of thy true) Inttab.empty
@@ -2016,13 +2014,13 @@
in
[Logic.mk_equals (normal_fun $ sel_a_t, sel_a_t),
Logic.list_implies
- ([\<^const>\<open>Not\<close> $ (is_unknown_t $ normal_x),
- \<^const>\<open>Not\<close> $ (is_unknown_t $ normal_y),
+ ([\<^Const>\<open>Not\<close> $ (is_unknown_t $ normal_x),
+ \<^Const>\<open>Not\<close> $ (is_unknown_t $ normal_y),
equiv_rel $ x_var $ y_var] |> map HOLogic.mk_Trueprop,
Logic.mk_equals (normal_x, normal_y)),
Logic.list_implies
- ([HOLogic.mk_Trueprop (\<^const>\<open>Not\<close> $ (is_unknown_t $ normal_x)),
- HOLogic.mk_Trueprop (\<^const>\<open>Not\<close> $ HOLogic.mk_eq (normal_x, x_var))],
+ ([HOLogic.mk_Trueprop (\<^Const>\<open>Not\<close> $ (is_unknown_t $ normal_x)),
+ HOLogic.mk_Trueprop (\<^Const>\<open>Not\<close> $ HOLogic.mk_eq (normal_x, x_var))],
HOLogic.mk_Trueprop (equiv_rel $ x_var $ normal_x))]
|> partial ? cons (HOLogic.mk_Trueprop (equiv_rel $ sel_a_t $ sel_a_t))
end
@@ -2031,8 +2029,8 @@
let
val xs = data_type_constrs hol_ctxt T
val pred_T = T --> bool_T
- val iter_T = \<^typ>\<open>bisim_iterator\<close>
- val bisim_max = \<^const>\<open>bisim_iterator_max\<close>
+ val iter_T = \<^Type>\<open>bisim_iterator\<close>
+ val bisim_max = \<^Const>\<open>bisim_iterator_max\<close>
val n_var = Var (("n", 0), iter_T)
val n_var_minus_1 =
Const (\<^const_name>\<open>safe_The\<close>, (iter_T --> bool_T) --> iter_T)
@@ -2214,8 +2212,8 @@
fun repair_rec j (Const (\<^const_name>\<open>Ex\<close>, T1) $ Abs (s2, T2, t2')) =
Const (\<^const_name>\<open>Ex\<close>, T1)
$ Abs (s2, T2, repair_rec (j + 1) t2')
- | repair_rec j (\<^const>\<open>HOL.conj\<close> $ t1 $ t2) =
- \<^const>\<open>HOL.conj\<close> $ repair_rec j t1 $ repair_rec j t2
+ | repair_rec j \<^Const_>\<open>conj for t1 t2\<close> =
+ \<^Const>\<open>conj for \<open>repair_rec j t1\<close> \<open>repair_rec j t2\<close>\<close>
| repair_rec j t =
let val (head, args) = strip_comb t in
if head = Bound j then
@@ -2227,9 +2225,9 @@
val (nonrecs, recs) =
List.partition (curry (op =) 0 o num_occs_of_bound_in_term j)
(disjuncts_of body)
- val base_body = nonrecs |> List.foldl s_disj \<^const>\<open>False\<close>
+ val base_body = nonrecs |> List.foldl s_disj \<^Const>\<open>False\<close>
val step_body = recs |> map (repair_rec j)
- |> List.foldl s_disj \<^const>\<open>False\<close>
+ |> List.foldl s_disj \<^Const>\<open>False\<close>
in
(fold_rev Term.abs (tl xs) (incr_bv (~1, j, base_body))
|> ap_n_split (length arg_Ts) tuple_T bool_T,
@@ -2241,11 +2239,7 @@
in aux end
fun predicatify T t =
- let val set_T = HOLogic.mk_setT T in
- Abs (Name.uu, T,
- Const (\<^const_name>\<open>Set.member\<close>, T --> set_T --> bool_T)
- $ Bound 0 $ incr_boundvars 1 t)
- end
+ Abs (Name.uu, T, \<^Const>\<open>Set.member T for \<open>Bound 0\<close> \<open>incr_boundvars 1 t\<close>\<close>)
fun starred_linear_pred_const (hol_ctxt as {simp_table, ...}) (s, T) def =
let
@@ -2365,7 +2359,7 @@
[inductive_pred_axiom hol_ctxt x]
else case def_of_const thy def_tables x of
SOME def =>
- \<^const>\<open>Trueprop\<close> $ HOLogic.mk_eq (Const x, def)
+ \<^Const>\<open>Trueprop\<close> $ HOLogic.mk_eq (Const x, def)
|> equationalize_term ctxt "" |> the |> single
| NONE => [])
| psimps => psimps)
@@ -2373,7 +2367,7 @@
fun is_equational_fun_surely_complete hol_ctxt x =
case equational_fun_axioms hol_ctxt x of
- [\<^const>\<open>Trueprop\<close> $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ t1 $ _)] =>
+ [\<^Const_>\<open>Trueprop for \<^Const_>\<open>HOL.eq _ for t1 _\<close>\<close>] =>
strip_comb t1 |> snd |> forall is_Var
| _ => false
--- a/src/HOL/Tools/Nitpick/nitpick_model.ML Tue Sep 28 12:35:43 2021 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_model.ML Wed Sep 29 09:58:19 2021 +0200
@@ -333,8 +333,8 @@
else raise TYPE ("Nitpick_Model.format_fun.do_term", [T, T'], [])
in if T1' = T1 andalso T2' = T2 then t else do_fun T1' T2' T1 T2 t end
-fun truth_const_sort_key \<^const>\<open>True\<close> = "0"
- | truth_const_sort_key \<^const>\<open>False\<close> = "2"
+fun truth_const_sort_key \<^Const_>\<open>True\<close> = "0"
+ | truth_const_sort_key \<^Const_>\<open>False\<close> = "2"
| truth_const_sort_key _ = "1"
fun mk_tuple (Type (\<^type_name>\<open>prod\<close>, [T1, T2])) ts =
@@ -411,14 +411,14 @@
empty_const
| aux ((t1, t2) :: zs) =
aux zs
- |> t2 <> \<^const>\<open>False\<close>
+ |> t2 <> \<^Const>\<open>False\<close>
? curry (op $)
(insert_const
- $ (t1 |> t2 <> \<^const>\<open>True\<close>
+ $ (t1 |> t2 <> \<^Const>\<open>True\<close>
? curry (op $)
(Const (maybe_name, T --> T))))
in
- if forall (fn (_, t) => t <> \<^const>\<open>True\<close> andalso t <> \<^const>\<open>False\<close>)
+ if forall (fn (_, t) => t <> \<^Const>\<open>True\<close> andalso t <> \<^Const>\<open>False\<close>)
tps then
Const (unknown, set_T)
else
@@ -516,7 +516,7 @@
| term_for_atom seen \<^typ>\<open>prop\<close> _ j k =
HOLogic.mk_Trueprop (term_for_atom seen bool_T bool_T j k)
| term_for_atom _ \<^typ>\<open>bool\<close> _ j _ =
- if j = 0 then \<^const>\<open>False\<close> else \<^const>\<open>True\<close>
+ if j = 0 then \<^Const>\<open>False\<close> else \<^Const>\<open>True\<close>
| term_for_atom seen T _ j k =
if T = nat_T then
HOLogic.mk_number nat_T j
@@ -524,7 +524,7 @@
HOLogic.mk_number int_T (int_for_atom (k, 0) j)
else if is_fp_iterator_type T then
HOLogic.mk_number nat_T (k - j - 1)
- else if T = \<^typ>\<open>bisim_iterator\<close> then
+ else if T = \<^Type>\<open>bisim_iterator\<close> then
HOLogic.mk_number nat_T j
else case data_type_spec data_types T of
NONE => nth_atom thy atomss pool T j
--- a/src/HOL/Tools/Nitpick/nitpick_mono.ML Tue Sep 28 12:35:43 2021 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML Wed Sep 29 09:58:19 2021 +0200
@@ -829,10 +829,10 @@
" \<turnstile> " ^ Syntax.string_of_term ctxt t ^
" : _?");
case t of
- \<^const>\<open>False\<close> => (bool_M, accum ||> add_comp_frame (A Fls) Leq frame)
+ \<^Const_>\<open>False\<close> => (bool_M, accum ||> add_comp_frame (A Fls) Leq frame)
| Const (\<^const_name>\<open>None\<close>, T) =>
(mtype_for T, accum ||> add_comp_frame (A Fls) Leq frame)
- | \<^const>\<open>True\<close> => (bool_M, accum ||> add_comp_frame (A Tru) Leq frame)
+ | \<^Const_>\<open>True\<close> => (bool_M, accum ||> add_comp_frame (A Tru) Leq frame)
| (t0 as Const (\<^const_name>\<open>HOL.eq\<close>, _)) $ Bound 0 $ t2 =>
(* hack to exploit symmetry of equality when typing "insert" *)
(if t2 = Bound 0 then do_term \<^term>\<open>True\<close>
@@ -850,9 +850,9 @@
| \<^const_name>\<open>Ex\<close> =>
let val set_T = domain_type T in
do_term (Abs (Name.uu, set_T,
- \<^const>\<open>Not\<close> $ (HOLogic.mk_eq
+ \<^Const>\<open>Not\<close> $ (HOLogic.mk_eq
(Abs (Name.uu, domain_type set_T,
- \<^const>\<open>False\<close>),
+ \<^Const>\<open>False\<close>),
Bound 0)))) accum
end
| \<^const_name>\<open>HOL.eq\<close> => do_equals T accum
@@ -971,12 +971,11 @@
val (M', accum) =
do_term t' (accum |>> push_bound (V x) T M)
in (MFun (M, V x, M'), accum |>> pop_bound) end))
- | \<^const>\<open>Not\<close> $ t1 => do_connect imp_spec t1 \<^const>\<open>False\<close> accum
- | \<^const>\<open>conj\<close> $ t1 $ t2 => do_connect conj_spec t1 t2 accum
- | \<^const>\<open>disj\<close> $ t1 $ t2 => do_connect disj_spec t1 t2 accum
- | \<^const>\<open>implies\<close> $ t1 $ t2 => do_connect imp_spec t1 t2 accum
- | Const (\<^const_name>\<open>Let\<close>, _) $ t1 $ t2 =>
- do_term (betapply (t2, t1)) accum
+ | \<^Const_>\<open>Not for t1\<close> => do_connect imp_spec t1 \<^Const>\<open>False\<close> accum
+ | \<^Const_>\<open>conj for t1 t2\<close> => do_connect conj_spec t1 t2 accum
+ | \<^Const_>\<open>disj for t1 t2\<close> => do_connect disj_spec t1 t2 accum
+ | \<^Const_>\<open>implies for t1 t2\<close> => do_connect imp_spec t1 t2 accum
+ | \<^Const_>\<open>Let _ _ for t1 t2\<close> => do_term (betapply (t2, t1)) accum
| t1 $ t2 =>
let
fun is_in t (j, _) = loose_bvar1 (t, length bound_Ts - j - 1)
@@ -1060,7 +1059,7 @@
Const (s as \<^const_name>\<open>Pure.all\<close>, _) $ Abs (_, T1, t1) =>
do_quantifier s T1 t1
| Const (\<^const_name>\<open>Pure.eq\<close>, _) $ t1 $ t2 => do_equals t1 t2
- | \<^const>\<open>Trueprop\<close> $ t1 => do_formula sn t1 accum
+ | \<^Const_>\<open>Trueprop for t1\<close> => do_formula sn t1 accum
| Const (s as \<^const_name>\<open>All\<close>, _) $ Abs (_, T1, t1) =>
do_quantifier s T1 t1
| Const (s as \<^const_name>\<open>Ex\<close>, T0) $ (t1 as Abs (_, T1, t1')) =>
@@ -1068,19 +1067,17 @@
Plus => do_quantifier s T1 t1'
| Minus =>
(* FIXME: Needed? *)
- do_term (\<^const>\<open>Not\<close>
+ do_term (\<^Const>\<open>Not\<close>
$ (HOLogic.eq_const (domain_type T0) $ t1
- $ Abs (Name.uu, T1, \<^const>\<open>False\<close>))) accum)
- | Const (\<^const_name>\<open>HOL.eq\<close>, _) $ t1 $ t2 => do_equals t1 t2
- | Const (\<^const_name>\<open>Let\<close>, _) $ t1 $ t2 =>
- do_formula sn (betapply (t2, t1)) accum
- | \<^const>\<open>Pure.conjunction\<close> $ t1 $ t2 =>
- do_connect meta_conj_spec false t1 t2 accum
- | \<^const>\<open>Pure.imp\<close> $ t1 $ t2 => do_connect meta_imp_spec true t1 t2 accum
- | \<^const>\<open>Not\<close> $ t1 => do_connect imp_spec true t1 \<^const>\<open>False\<close> accum
- | \<^const>\<open>conj\<close> $ t1 $ t2 => do_connect conj_spec false t1 t2 accum
- | \<^const>\<open>disj\<close> $ t1 $ t2 => do_connect disj_spec false t1 t2 accum
- | \<^const>\<open>implies\<close> $ t1 $ t2 => do_connect imp_spec true t1 t2 accum
+ $ Abs (Name.uu, T1, \<^Const>\<open>False\<close>))) accum)
+ | \<^Const_>\<open>HOL.eq _ for t1 t2\<close> => do_equals t1 t2
+ | \<^Const_>\<open>Let _ _ for t1 t2\<close> => do_formula sn (betapply (t2, t1)) accum
+ | \<^Const_>\<open>Pure.conjunction for t1 t2\<close> => do_connect meta_conj_spec false t1 t2 accum
+ | \<^Const_>\<open>Pure.imp for t1 t2\<close> => do_connect meta_imp_spec true t1 t2 accum
+ | \<^Const_>\<open>Not for t1\<close> => do_connect imp_spec true t1 \<^Const>\<open>False\<close> accum
+ | \<^Const_>\<open>conj for t1 t2\<close> => do_connect conj_spec false t1 t2 accum
+ | \<^Const_>\<open>disj for t1 t2\<close> => do_connect disj_spec false t1 t2 accum
+ | \<^Const_>\<open>implies for t1 t2\<close> => do_connect imp_spec true t1 t2 accum
| _ => do_term t accum
end
|> tap (fn (gamma, _) =>
@@ -1122,18 +1119,15 @@
and do_implies t1 t2 = do_term t1 #> do_formula t2
and do_formula t accum =
case t of
- Const (\<^const_name>\<open>Pure.all\<close>, _) $ Abs (_, T1, t1) => do_all T1 t1 accum
- | \<^const>\<open>Trueprop\<close> $ t1 => do_formula t1 accum
- | Const (\<^const_name>\<open>Pure.eq\<close>, _) $ t1 $ t2 =>
- consider_general_equals mdata true t1 t2 accum
- | \<^const>\<open>Pure.imp\<close> $ t1 $ t2 => do_implies t1 t2 accum
- | \<^const>\<open>Pure.conjunction\<close> $ t1 $ t2 =>
- fold (do_formula) [t1, t2] accum
- | Const (\<^const_name>\<open>All\<close>, _) $ Abs (_, T1, t1) => do_all T1 t1 accum
- | Const (\<^const_name>\<open>HOL.eq\<close>, _) $ t1 $ t2 =>
- consider_general_equals mdata true t1 t2 accum
- | \<^const>\<open>conj\<close> $ t1 $ t2 => fold (do_formula) [t1, t2] accum
- | \<^const>\<open>implies\<close> $ t1 $ t2 => do_implies t1 t2 accum
+ \<^Const_>\<open>Pure.all _ for \<open>Abs (_, T1, t1)\<close>\<close> => do_all T1 t1 accum
+ | \<^Const_>\<open>Trueprop for t1\<close> => do_formula t1 accum
+ | \<^Const_>\<open>Pure.eq _ for t1 t2\<close> => consider_general_equals mdata true t1 t2 accum
+ | \<^Const_>\<open>Pure.imp for t1 t2\<close> => do_implies t1 t2 accum
+ | \<^Const_>\<open>Pure.conjunction for t1 t2\<close> => fold (do_formula) [t1, t2] accum
+ | \<^Const_>\<open>All _ for \<open>Abs (_, T1, t1)\<close>\<close> => do_all T1 t1 accum
+ | \<^Const_>\<open>HOL.eq _ for t1 t2\<close> => consider_general_equals mdata true t1 t2 accum
+ | \<^Const_>\<open>conj for t1 t2\<close> => fold (do_formula) [t1, t2] accum
+ | \<^Const_>\<open>implies for t1 t2\<close> => do_implies t1 t2 accum
| _ => raise TERM ("Nitpick_Mono.consider_definitional_axiom.\
\do_formula", [t])
in do_formula t end
--- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML Tue Sep 28 12:35:43 2021 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML Wed Sep 29 09:58:19 2021 +0200
@@ -36,15 +36,12 @@
val may_use_binary_ints =
let
- fun aux def (Const (\<^const_name>\<open>Pure.eq\<close>, _) $ t1 $ t2) =
- aux def t1 andalso aux false t2
- | aux def (\<^const>\<open>Pure.imp\<close> $ t1 $ t2) = aux false t1 andalso aux def t2
- | aux def (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ t1 $ t2) =
- aux def t1 andalso aux false t2
- | aux def (\<^const>\<open>HOL.implies\<close> $ t1 $ t2) = aux false t1 andalso aux def t2
+ fun aux def \<^Const_>\<open>Pure.eq _ for t1 t2\<close> = aux def t1 andalso aux false t2
+ | aux def \<^Const_>\<open>Pure.imp for t1 t2\<close> = aux false t1 andalso aux def t2
+ | aux def \<^Const_>\<open>HOL.eq _ for t1 t2\<close> = aux def t1 andalso aux false t2
+ | aux def \<^Const_>\<open>implies for t1 t2\<close> = aux false t1 andalso aux def t2
| aux def (t1 $ t2) = aux def t1 andalso aux def t2
- | aux def (t as Const (s, _)) =
- (not def orelse t <> \<^const>\<open>Suc\<close>) andalso
+ | aux def (t as Const (s, _)) = (not def orelse t <> \<^Const>\<open>Suc\<close>) andalso
not (member (op =)
[\<^const_name>\<open>Abs_Frac\<close>, \<^const_name>\<open>Rep_Frac\<close>,
\<^const_name>\<open>nat_gcd\<close>, \<^const_name>\<open>nat_lcm\<close>,
@@ -143,7 +140,7 @@
| _ => exists_subterm (curry (op =) (Var z)) t' ? insert (op =) T
fun box_var_in_def new_Ts old_Ts t (z as (_, T)) =
case t of
- \<^const>\<open>Trueprop\<close> $ t1 => box_var_in_def new_Ts old_Ts t1 z
+ \<^Const_>\<open>Trueprop for t1\<close> => box_var_in_def new_Ts old_Ts t1 z
| Const (s0, _) $ t1 $ _ =>
if s0 = \<^const_name>\<open>Pure.eq\<close> orelse s0 = \<^const_name>\<open>HOL.eq\<close> then
let
@@ -190,31 +187,29 @@
do_quantifier new_Ts old_Ts polar s0 T0 s1 T1 t1
| Const (s0 as \<^const_name>\<open>Pure.eq\<close>, T0) $ t1 $ t2 =>
do_equals new_Ts old_Ts s0 T0 t1 t2
- | \<^const>\<open>Pure.imp\<close> $ t1 $ t2 =>
- \<^const>\<open>Pure.imp\<close> $ do_term new_Ts old_Ts (flip_polarity polar) t1
- $ do_term new_Ts old_Ts polar t2
- | \<^const>\<open>Pure.conjunction\<close> $ t1 $ t2 =>
- \<^const>\<open>Pure.conjunction\<close> $ do_term new_Ts old_Ts polar t1
- $ do_term new_Ts old_Ts polar t2
- | \<^const>\<open>Trueprop\<close> $ t1 =>
- \<^const>\<open>Trueprop\<close> $ do_term new_Ts old_Ts polar t1
- | \<^const>\<open>Not\<close> $ t1 =>
- \<^const>\<open>Not\<close> $ do_term new_Ts old_Ts (flip_polarity polar) t1
+ | \<^Const_>\<open>Pure.imp for t1 t2\<close> =>
+ \<^Const>\<open>Pure.imp for \<open>do_term new_Ts old_Ts (flip_polarity polar) t1\<close>
+ \<open>do_term new_Ts old_Ts polar t2\<close>\<close>
+ | \<^Const_>\<open>Pure.conjunction for t1 t2\<close> =>
+ \<^Const>\<open>Pure.conjunction for \<open>do_term new_Ts old_Ts polar t1\<close>
+ \<open>do_term new_Ts old_Ts polar t2\<close>\<close>
+ | \<^Const_>\<open>Trueprop for t1\<close> => \<^Const>\<open>Trueprop for \<open>do_term new_Ts old_Ts polar t1\<close>\<close>
+ | \<^Const_>\<open>Not for t1\<close> => \<^Const>\<open>Not for \<open>do_term new_Ts old_Ts (flip_polarity polar) t1\<close>\<close>
| Const (s0 as \<^const_name>\<open>All\<close>, T0) $ Abs (s1, T1, t1) =>
do_quantifier new_Ts old_Ts polar s0 T0 s1 T1 t1
| Const (s0 as \<^const_name>\<open>Ex\<close>, T0) $ Abs (s1, T1, t1) =>
do_quantifier new_Ts old_Ts polar s0 T0 s1 T1 t1
| Const (s0 as \<^const_name>\<open>HOL.eq\<close>, T0) $ t1 $ t2 =>
do_equals new_Ts old_Ts s0 T0 t1 t2
- | \<^const>\<open>HOL.conj\<close> $ t1 $ t2 =>
- \<^const>\<open>HOL.conj\<close> $ do_term new_Ts old_Ts polar t1
- $ do_term new_Ts old_Ts polar t2
- | \<^const>\<open>HOL.disj\<close> $ t1 $ t2 =>
- \<^const>\<open>HOL.disj\<close> $ do_term new_Ts old_Ts polar t1
- $ do_term new_Ts old_Ts polar t2
- | \<^const>\<open>HOL.implies\<close> $ t1 $ t2 =>
- \<^const>\<open>HOL.implies\<close> $ do_term new_Ts old_Ts (flip_polarity polar) t1
- $ do_term new_Ts old_Ts polar t2
+ | \<^Const_>\<open>conj for t1 t2\<close> =>
+ \<^Const>\<open>conj for \<open>do_term new_Ts old_Ts polar t1\<close>
+ \<open>do_term new_Ts old_Ts polar t2\<close>\<close>
+ | \<^Const_>\<open>disj for t1 t2\<close> =>
+ \<^Const>\<open>disj for \<open>do_term new_Ts old_Ts polar t1\<close>
+ \<open>do_term new_Ts old_Ts polar t2\<close>\<close>
+ | \<^Const_>\<open>implies for t1 t2\<close> =>
+ \<^Const>\<open>implies for \<open>do_term new_Ts old_Ts (flip_polarity polar) t1\<close>
+ \<open>do_term new_Ts old_Ts polar t2\<close>\<close>
| Const (x as (s, T)) =>
if is_descr s then
do_descr s T
@@ -335,11 +330,11 @@
case t of
(t0 as Const (\<^const_name>\<open>Pure.eq\<close>, _)) $ t1 $ t2 =>
do_eq_or_imp Ts true def t0 t1 t2 seen
- | (t0 as \<^const>\<open>Pure.imp\<close>) $ t1 $ t2 =>
+ | (t0 as \<^Const_>\<open>Pure.imp\<close>) $ t1 $ t2 =>
if def then (t, []) else do_eq_or_imp Ts false def t0 t1 t2 seen
| (t0 as Const (\<^const_name>\<open>HOL.eq\<close>, _)) $ t1 $ t2 =>
do_eq_or_imp Ts true def t0 t1 t2 seen
- | (t0 as \<^const>\<open>HOL.implies\<close>) $ t1 $ t2 =>
+ | (t0 as \<^Const_>\<open>implies\<close>) $ t1 $ t2 =>
do_eq_or_imp Ts false def t0 t1 t2 seen
| Abs (s, T, t') =>
let val (t', seen) = do_term (T :: Ts) def t' [] seen in
@@ -402,11 +397,11 @@
| _ => I) t (K 0)
fun aux Ts careful ((t0 as Const (\<^const_name>\<open>Pure.eq\<close>, _)) $ t1 $ t2) =
aux_eq Ts careful true t0 t1 t2
- | aux Ts careful ((t0 as \<^const>\<open>Pure.imp\<close>) $ t1 $ t2) =
+ | aux Ts careful ((t0 as \<^Const_>\<open>Pure.imp\<close>) $ t1 $ t2) =
t0 $ aux Ts false t1 $ aux Ts careful t2
| aux Ts careful ((t0 as Const (\<^const_name>\<open>HOL.eq\<close>, _)) $ t1 $ t2) =
aux_eq Ts careful true t0 t1 t2
- | aux Ts careful ((t0 as \<^const>\<open>HOL.implies\<close>) $ t1 $ t2) =
+ | aux Ts careful ((t0 as \<^Const_>\<open>implies\<close>) $ t1 $ t2) =
t0 $ aux Ts false t1 $ aux Ts careful t2
| aux Ts careful (Abs (s, T, t')) = Abs (s, T, aux (T :: Ts) careful t')
| aux Ts careful (t1 $ t2) = aux Ts careful t1 $ aux Ts careful t2
@@ -417,13 +412,13 @@
raise SAME ()
else if axiom andalso is_Var t2 andalso
num_occs_of_var (dest_Var t2) = 1 then
- \<^const>\<open>True\<close>
+ \<^Const>\<open>True\<close>
else case strip_comb t2 of
(* The first case is not as general as it could be. *)
(Const (\<^const_name>\<open>PairBox\<close>, _),
[Const (\<^const_name>\<open>fst\<close>, _) $ Var z1,
Const (\<^const_name>\<open>snd\<close>, _) $ Var z2]) =>
- if z1 = z2 andalso num_occs_of_var z1 = 2 then \<^const>\<open>True\<close>
+ if z1 = z2 andalso num_occs_of_var z1 = 2 then \<^Const>\<open>True\<close>
else raise SAME ()
| (Const (x as (s, T)), args) =>
let
@@ -454,26 +449,22 @@
(** Destruction of universal and existential equalities **)
-fun curry_assms (\<^const>\<open>Pure.imp\<close> $ (\<^const>\<open>Trueprop\<close>
- $ (\<^const>\<open>HOL.conj\<close> $ t1 $ t2)) $ t3) =
+fun curry_assms \<^Const_>\<open>Pure.imp for \<^Const>\<open>Trueprop for \<^Const_>\<open>conj for t1 t2\<close>\<close> t3\<close> =
curry_assms (Logic.list_implies ([t1, t2] |> map HOLogic.mk_Trueprop, t3))
- | curry_assms (\<^const>\<open>Pure.imp\<close> $ t1 $ t2) =
- \<^const>\<open>Pure.imp\<close> $ curry_assms t1 $ curry_assms t2
+ | curry_assms \<^Const_>\<open>Pure.imp for t1 t2\<close> = \<^Const>\<open>Pure.imp for \<open>curry_assms t1\<close> \<open>curry_assms t2\<close>\<close>
| curry_assms t = t
val destroy_universal_equalities =
let
fun aux prems zs t =
case t of
- \<^const>\<open>Pure.imp\<close> $ t1 $ t2 => aux_implies prems zs t1 t2
+ \<^Const_>\<open>Pure.imp for t1 t2\<close> => aux_implies prems zs t1 t2
| _ => Logic.list_implies (rev prems, t)
and aux_implies prems zs t1 t2 =
case t1 of
- Const (\<^const_name>\<open>Pure.eq\<close>, _) $ Var z $ t' => aux_eq prems zs z t' t1 t2
- | \<^const>\<open>Trueprop\<close> $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ Var z $ t') =>
- aux_eq prems zs z t' t1 t2
- | \<^const>\<open>Trueprop\<close> $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ t' $ Var z) =>
- aux_eq prems zs z t' t1 t2
+ \<^Const_>\<open>Pure.eq _ for \<open>Var z\<close> t'\<close> => aux_eq prems zs z t' t1 t2
+ | \<^Const_>\<open>Trueprop for \<^Const_>\<open>HOL.eq _ for \<open>Var z\<close> t'\<close>\<close> => aux_eq prems zs z t' t1 t2
+ | \<^Const_>\<open>Trueprop for \<^Const_>\<open>HOL.eq _ for t' \<open>Var z\<close>\<close>\<close> => aux_eq prems zs z t' t1 t2
| _ => aux (t1 :: prems) (Term.add_vars t1 zs) t2
and aux_eq prems zs z t' t1 t2 =
if not (member (op =) zs z) andalso
@@ -528,7 +519,7 @@
fun kill [] [] ts = foldr1 s_conj ts
| kill (s :: ss) (T :: Ts) ts =
(case find_bound_assign ctxt (length ss) [] ts of
- SOME (_, []) => \<^const>\<open>True\<close>
+ SOME (_, []) => \<^Const>\<open>True\<close>
| SOME (arg_t, ts) =>
kill ss Ts (map (subst_one_bound (length ss)
(incr_bv (~1, length ss + 1, arg_t))) ts)
@@ -592,27 +583,27 @@
case t of
Const (s0 as \<^const_name>\<open>Pure.all\<close>, T0) $ Abs (s1, T1, t1) =>
do_quantifier s0 T0 s1 T1 t1
- | \<^const>\<open>Pure.imp\<close> $ t1 $ t2 =>
- \<^const>\<open>Pure.imp\<close> $ aux ss Ts js skolemizable (flip_polarity polar) t1
- $ aux ss Ts js skolemizable polar t2
- | \<^const>\<open>Pure.conjunction\<close> $ t1 $ t2 =>
- \<^const>\<open>Pure.conjunction\<close> $ aux ss Ts js skolemizable polar t1
- $ aux ss Ts js skolemizable polar t2
- | \<^const>\<open>Trueprop\<close> $ t1 =>
- \<^const>\<open>Trueprop\<close> $ aux ss Ts js skolemizable polar t1
- | \<^const>\<open>Not\<close> $ t1 =>
- \<^const>\<open>Not\<close> $ aux ss Ts js skolemizable (flip_polarity polar) t1
+ | \<^Const_>\<open>Pure.imp for t1 t2\<close> =>
+ \<^Const>\<open>Pure.imp for \<open>aux ss Ts js skolemizable (flip_polarity polar) t1\<close>
+ \<open>aux ss Ts js skolemizable polar t2\<close>\<close>
+ | \<^Const_>\<open>Pure.conjunction for t1 t2\<close> =>
+ \<^Const>\<open>Pure.conjunction for \<open>aux ss Ts js skolemizable polar t1\<close>
+ \<open>aux ss Ts js skolemizable polar t2\<close>\<close>
+ | \<^Const_>\<open>Trueprop for t1\<close> =>
+ \<^Const>\<open>Trueprop for \<open>aux ss Ts js skolemizable polar t1\<close>\<close>
+ | \<^Const_>\<open>Not for t1\<close> =>
+ \<^Const>\<open>Not for \<open>aux ss Ts js skolemizable (flip_polarity polar) t1\<close>\<close>
| Const (s0 as \<^const_name>\<open>All\<close>, T0) $ Abs (s1, T1, t1) =>
do_quantifier s0 T0 s1 T1 t1
| Const (s0 as \<^const_name>\<open>Ex\<close>, T0) $ Abs (s1, T1, t1) =>
do_quantifier s0 T0 s1 T1 t1
- | \<^const>\<open>HOL.conj\<close> $ t1 $ t2 =>
+ | \<^Const_>\<open>conj for t1 t2\<close> =>
s_conj (apply2 (aux ss Ts js skolemizable polar) (t1, t2))
- | \<^const>\<open>HOL.disj\<close> $ t1 $ t2 =>
+ | \<^Const_>\<open>disj for t1 t2\<close> =>
s_disj (apply2 (aux ss Ts js skolemizable polar) (t1, t2))
- | \<^const>\<open>HOL.implies\<close> $ t1 $ t2 =>
- \<^const>\<open>HOL.implies\<close> $ aux ss Ts js skolemizable (flip_polarity polar) t1
- $ aux ss Ts js skolemizable polar t2
+ | \<^Const_>\<open>implies for t1 t2\<close> =>
+ \<^Const>\<open>implies for \<open>aux ss Ts js skolemizable (flip_polarity polar) t1\<close>
+ \<open>aux ss Ts js skolemizable polar t2\<close>\<close>
| (t0 as Const (\<^const_name>\<open>Let\<close>, _)) $ t1 $ t2 =>
t0 $ t1 $ aux ss Ts js skolemizable polar t2
| Const (x as (s, T)) =>
@@ -622,8 +613,8 @@
let
val gfp = (fixpoint_kind_of_const thy def_tables x = Gfp)
val (pref, connective) =
- if gfp then (lbfp_prefix, \<^const>\<open>HOL.disj\<close>)
- else (ubfp_prefix, \<^const>\<open>HOL.conj\<close>)
+ if gfp then (lbfp_prefix, \<^Const>\<open>disj\<close>)
+ else (ubfp_prefix, \<^Const>\<open>conj\<close>)
fun pos () = unrolled_inductive_pred_const hol_ctxt gfp x
|> aux ss Ts js skolemizable polar
fun neg () = Const (pref ^ s, T)
@@ -653,10 +644,9 @@
(** Function specialization **)
-fun params_in_equation (\<^const>\<open>Pure.imp\<close> $ _ $ t2) = params_in_equation t2
- | params_in_equation (\<^const>\<open>Trueprop\<close> $ t1) = params_in_equation t1
- | params_in_equation (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ t1 $ _) =
- snd (strip_comb t1)
+fun params_in_equation \<^Const_>\<open>Pure.imp for _ t2\<close> = params_in_equation t2
+ | params_in_equation \<^Const_>\<open>Trueprop for t1\<close> = params_in_equation t1
+ | params_in_equation \<^Const_>\<open>HOL.eq _ for t1 _\<close> = snd (strip_comb t1)
| params_in_equation _ = []
fun specialize_fun_axiom x x' fixed_js fixed_args extra_args t =
@@ -865,10 +855,8 @@
if exists_subterm (curry (op aconv) u) def then NONE else SOME u
in
case t of
- Const (\<^const_name>\<open>Pure.eq\<close>, _) $ (u as Free _) $ def => do_equals u def
- | \<^const>\<open>Trueprop\<close>
- $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ (u as Free _) $ def) =>
- do_equals u def
+ \<^Const_>\<open>Pure.eq _ for \<open>u as Free _\<close> def\<close> => do_equals u def
+ | \<^Const_>\<open>Trueprop\<close> $ \<^Const_>\<open>HOL.eq _ for \<open>u as Free _\<close> def\<close> => do_equals u def
| _ => NONE
end
@@ -917,7 +905,7 @@
and add_def_axiom depth = add_axiom fst apfst true depth
and add_nondef_axiom depth = add_axiom snd apsnd false depth
and add_maybe_def_axiom depth t =
- (if head_of t <> \<^const>\<open>Pure.imp\<close> then add_def_axiom
+ (if head_of t <> \<^Const>\<open>Pure.imp\<close> then add_def_axiom
else add_nondef_axiom) depth t
and add_eq_axiom depth t =
(if is_constr_pattern_formula ctxt t then add_def_axiom
@@ -1104,10 +1092,10 @@
case t of
(t0 as Const (\<^const_name>\<open>All\<close>, T0)) $ Abs (s, T1, t1) =>
(case t1 of
- (t10 as \<^const>\<open>HOL.conj\<close>) $ t11 $ t12 =>
+ (t10 as \<^Const_>\<open>conj\<close>) $ t11 $ t12 =>
t10 $ distribute_quantifiers (t0 $ Abs (s, T1, t11))
$ distribute_quantifiers (t0 $ Abs (s, T1, t12))
- | (t10 as \<^const>\<open>Not\<close>) $ t11 =>
+ | (t10 as \<^Const_>\<open>Not\<close>) $ t11 =>
t10 $ distribute_quantifiers (Const (\<^const_name>\<open>Ex\<close>, T0)
$ Abs (s, T1, t11))
| t1 =>
@@ -1117,14 +1105,14 @@
t0 $ Abs (s, T1, distribute_quantifiers t1))
| (t0 as Const (\<^const_name>\<open>Ex\<close>, T0)) $ Abs (s, T1, t1) =>
(case distribute_quantifiers t1 of
- (t10 as \<^const>\<open>HOL.disj\<close>) $ t11 $ t12 =>
+ (t10 as \<^Const_>\<open>disj\<close>) $ t11 $ t12 =>
t10 $ distribute_quantifiers (t0 $ Abs (s, T1, t11))
$ distribute_quantifiers (t0 $ Abs (s, T1, t12))
- | (t10 as \<^const>\<open>HOL.implies\<close>) $ t11 $ t12 =>
+ | (t10 as \<^Const_>\<open>implies\<close>) $ t11 $ t12 =>
t10 $ distribute_quantifiers (Const (\<^const_name>\<open>All\<close>, T0)
$ Abs (s, T1, t11))
$ distribute_quantifiers (t0 $ Abs (s, T1, t12))
- | (t10 as \<^const>\<open>Not\<close>) $ t11 =>
+ | (t10 as \<^Const_>\<open>Not\<close>) $ t11 =>
t10 $ distribute_quantifiers (Const (\<^const_name>\<open>All\<close>, T0)
$ Abs (s, T1, t11))
| t1 =>
--- a/src/HOL/Tools/Nunchaku/nunchaku.ML Tue Sep 28 12:35:43 2021 +0200
+++ b/src/HOL/Tools/Nunchaku/nunchaku.ML Wed Sep 29 09:58:19 2021 +0200
@@ -131,7 +131,7 @@
fun none_true assigns = forall (curry (op <>) (SOME true) o snd) assigns;
-fun has_lonely_bool_var (\<^const>\<open>Pure.conjunction\<close> $ (\<^const>\<open>Trueprop\<close> $ Free _) $ _) = true
+fun has_lonely_bool_var \<^Const_>\<open>Pure.conjunction for \<^Const_>\<open>Trueprop for \<open>Free _\<close>\<close> _\<close> = true
| has_lonely_bool_var _ = false;
val syntactic_sorts =
--- a/src/HOL/Tools/Nunchaku/nunchaku_collect.ML Tue Sep 28 12:35:43 2021 +0200
+++ b/src/HOL/Tools/Nunchaku/nunchaku_collect.ML Wed Sep 29 09:58:19 2021 +0200
@@ -240,7 +240,7 @@
fun mutual_co_datatypes_of ctxt (T_name, Ts) =
(if T_name = \<^type_name>\<open>itself\<close> then
- (BNF_Util.Least_FP, [\<^typ>\<open>'a itself\<close>], [[@{const Pure.type ('a)}]])
+ (BNF_Util.Least_FP, [\<^typ>\<open>'a itself\<close>], [[\<^Const>\<open>Pure.type \<^typ>\<open>'a\<close>\<close>]])
else
let
val (fp, ctr_sugars) =
@@ -269,7 +269,7 @@
val A = Logic.varifyT_global \<^typ>\<open>'a\<close>;
val absT = Type (\<^type_name>\<open>set\<close>, [A]);
val repT = A --> HOLogic.boolT;
- val pred = Abs (Name.uu, repT, \<^const>\<open>True\<close>);
+ val pred = Abs (Name.uu, repT, \<^Const>\<open>True\<close>);
val abs = Const (\<^const_name>\<open>Collect\<close>, repT --> absT);
val rep = Const (\<^const_name>\<open>rmember\<close>, absT --> repT);
in
@@ -518,8 +518,8 @@
fold process_spec specs NONE
end;
-fun lhs_of_equation (Const (\<^const_name>\<open>Pure.eq\<close>, _) $ t $ _) = t
- | lhs_of_equation (\<^const>\<open>Trueprop\<close> $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ t $ _)) = t;
+fun lhs_of_equation \<^Const_>\<open>Pure.eq _ for t _\<close> = t
+ | lhs_of_equation \<^Const_>\<open>Trueprop for \<^Const_>\<open>HOL.eq _ for t _\<close>\<close> = t;
fun specialize_definition_type thy x def0 =
let
@@ -674,10 +674,10 @@
[cmd] :: (group :: groups)
end;
-fun defined_by (Const (\<^const_name>\<open>All\<close>, _) $ t) = defined_by t
+fun defined_by \<^Const_>\<open>All _ for t\<close> = defined_by t
| defined_by (Abs (_, _, t)) = defined_by t
- | defined_by (\<^const>\<open>implies\<close> $ _ $ u) = defined_by u
- | defined_by (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ t $ _) = head_of t
+ | defined_by \<^Const_>\<open>implies for _ u\<close> = defined_by u
+ | defined_by \<^Const_>\<open>HOL.eq _ for t _\<close> = head_of t
| defined_by t = head_of t;
fun partition_props [_] props = SOME [props]
@@ -1002,14 +1002,14 @@
val (poly_axioms, mono_axioms0) = orphan_axioms_of ctxt
|> List.partition has_polymorphism;
- fun implicit_evals_of pol (\<^const>\<open>Not\<close> $ t) = implicit_evals_of (not pol) t
- | implicit_evals_of pol (\<^const>\<open>implies\<close> $ t $ u) =
+ fun implicit_evals_of pol \<^Const_>\<open>Not for t\<close> = implicit_evals_of (not pol) t
+ | implicit_evals_of pol \<^Const_>\<open>implies for t u\<close> =
(case implicit_evals_of pol u of
[] => implicit_evals_of (not pol) t
| ts => ts)
- | implicit_evals_of pol (\<^const>\<open>conj\<close> $ t $ u) =
+ | implicit_evals_of pol \<^Const_>\<open>conj for t u\<close> =
union (op aconv) (implicit_evals_of pol t) (implicit_evals_of pol u)
- | implicit_evals_of pol (\<^const>\<open>disj\<close> $ t $ u) =
+ | implicit_evals_of pol \<^Const_>\<open>disj for t u\<close> =
union (op aconv) (implicit_evals_of pol t) (implicit_evals_of pol u)
| implicit_evals_of false (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ t $ u) =
distinct (op aconv) [t, u]
@@ -1049,7 +1049,7 @@
Syntax.string_of_term ctxt t ^ " : " ^ Syntax.string_of_typ ctxt (fastype_of t);
fun is_triv_wrt (Abs (_, _, body)) = is_triv_wrt body
- | is_triv_wrt \<^const>\<open>True\<close> = true
+ | is_triv_wrt \<^Const>\<open>True\<close> = true
| is_triv_wrt _ = false;
fun str_of_isa_type_spec ctxt {abs_typ, rep_typ, wrt, abs, rep} =
--- a/src/HOL/Tools/Nunchaku/nunchaku_reconstruct.ML Tue Sep 28 12:35:43 2021 +0200
+++ b/src/HOL/Tools/Nunchaku/nunchaku_reconstruct.ML Wed Sep 29 09:58:19 2021 +0200
@@ -166,11 +166,11 @@
else if id = nun_equals then
Const (\<^const_name>\<open>HOL.eq\<close>, typ_of ty)
else if id = nun_false then
- \<^const>\<open>False\<close>
+ \<^Const>\<open>False\<close>
else if id = nun_if then
Const (\<^const_name>\<open>If\<close>, typ_of ty)
else if id = nun_implies then
- \<^term>\<open>implies\<close>
+ \<^Const>\<open>implies\<close>
else if id = nun_not then
HOLogic.Not
else if id = nun_unique then
@@ -178,7 +178,7 @@
else if id = nun_unique_unsafe then
Const (\<^const_name>\<open>The_unsafe\<close>, typ_of ty)
else if id = nun_true then
- \<^const>\<open>True\<close>
+ \<^Const>\<open>True\<close>
else if String.isPrefix nun_dollar_anon_fun_prefix id then
let val j = Int.fromString (unprefix nun_dollar_anon_fun_prefix id) |> the_default ~1 in
Var ((anonymousN ^ nat_subscript (j + 1), 0), typ_of ty)
@@ -225,12 +225,12 @@
end
| term_of _ (NMatch _) = raise Fail "unexpected match";
- fun rewrite_numbers (t as \<^const>\<open>Suc\<close> $ _) =
+ fun rewrite_numbers (t as \<^Const>\<open>Suc\<close> $ _) =
(case try HOLogic.dest_nat t of
- SOME n => HOLogic.mk_number \<^typ>\<open>nat\<close> n
+ SOME n => HOLogic.mk_number \<^Type>\<open>nat\<close> n
| NONE => t)
- | rewrite_numbers (\<^const>\<open>Abs_Integ\<close> $ (@{const Pair (nat, nat)} $ t $ u)) =
- HOLogic.mk_number \<^typ>\<open>int\<close> (HOLogic.dest_nat t - HOLogic.dest_nat u)
+ | rewrite_numbers \<^Const_>\<open>Abs_Integ for \<^Const>\<open>Pair \<^Type>\<open>nat\<close> \<^Type>\<open>nat\<close> for t u\<close>\<close> =
+ HOLogic.mk_number \<^Type>\<open>int\<close> (HOLogic.dest_nat t - HOLogic.dest_nat u)
| rewrite_numbers (t $ u) = rewrite_numbers t $ rewrite_numbers u
| rewrite_numbers (Abs (s, T, t)) = Abs (s, T, rewrite_numbers t)
| rewrite_numbers t = t;
--- a/src/HOL/Tools/Quickcheck/quickcheck_common.ML Tue Sep 28 12:35:43 2021 +0200
+++ b/src/HOL/Tools/Quickcheck/quickcheck_common.ML Wed Sep 29 09:58:19 2021 +0200
@@ -466,8 +466,8 @@
fun make_fun_upds T1 T2 (tps, t) = fold_rev (mk_fun_upd T1 T2) tps t
fun make_set T1 [] = Const (\<^const_abbrev>\<open>Set.empty\<close>, T1 --> \<^typ>\<open>bool\<close>)
- | make_set T1 ((_, \<^const>\<open>False\<close>) :: tps) = make_set T1 tps
- | make_set T1 ((t1, \<^const>\<open>True\<close>) :: tps) =
+ | make_set T1 ((_, \<^Const_>\<open>False\<close>) :: tps) = make_set T1 tps
+ | make_set T1 ((t1, \<^Const_>\<open>True\<close>) :: tps) =
Const (\<^const_name>\<open>insert\<close>, T1 --> (T1 --> \<^typ>\<open>bool\<close>) --> T1 --> \<^typ>\<open>bool\<close>) $
t1 $ (make_set T1 tps)
| make_set T1 ((_, t) :: _) = raise TERM ("make_set", [t])
@@ -476,8 +476,8 @@
| make_coset T tps =
let
val U = T --> \<^typ>\<open>bool\<close>
- fun invert \<^const>\<open>False\<close> = \<^const>\<open>True\<close>
- | invert \<^const>\<open>True\<close> = \<^const>\<open>False\<close>
+ fun invert \<^Const_>\<open>False\<close> = \<^Const>\<open>True\<close>
+ | invert \<^Const_>\<open>True\<close> = \<^Const>\<open>False\<close>
in
Const (\<^const_name>\<open>Groups.minus_class.minus\<close>, U --> U --> U) $
Const (\<^const_abbrev>\<open>UNIV\<close>, U) $ make_set T (map (apsnd invert) tps)
@@ -505,8 +505,8 @@
(case T2 of
\<^typ>\<open>bool\<close> =>
(case t of
- Abs(_, _, \<^const>\<open>False\<close>) => fst #> rev #> make_set T1
- | Abs(_, _, \<^const>\<open>True\<close>) => fst #> rev #> make_coset T1
+ Abs(_, _, \<^Const_>\<open>False\<close>) => fst #> rev #> make_set T1
+ | Abs(_, _, \<^Const_>\<open>True\<close>) => fst #> rev #> make_coset T1
| Abs(_, _, Const (\<^const_name>\<open>undefined\<close>, _)) => fst #> rev #> make_set T1
| _ => raise TERM ("post_process_term", [t]))
| Type (\<^type_name>\<open>option\<close>, _) =>
--- a/src/HOL/Tools/Quickcheck/random_generators.ML Tue Sep 28 12:35:43 2021 +0200
+++ b/src/HOL/Tools/Quickcheck/random_generators.ML Wed Sep 29 09:58:19 2021 +0200
@@ -96,7 +96,7 @@
fun subst_v t' = map_aterms (fn t as Free (w, _) => if v = w then t' else t | t => t);
val t_rhs = lambda t_k proto_t_rhs;
val eqs0 = [subst_v \<^term>\<open>0::natural\<close> eq,
- subst_v (\<^const>\<open>Code_Numeral.Suc\<close> $ t_k) eq];
+ subst_v \<^Const>\<open>Code_Numeral.Suc for t_k\<close> eq];
val eqs1 = map (Pattern.rewrite_term thy rew_ts []) eqs0;
val ((_, (_, eqs2)), lthy') = lthy
|> BNF_LFP_Compat.primrec_simple
--- a/src/HOL/Tools/SMT/conj_disj_perm.ML Tue Sep 28 12:35:43 2021 +0200
+++ b/src/HOL/Tools/SMT/conj_disj_perm.ML Wed Sep 29 09:58:19 2021 +0200
@@ -25,9 +25,9 @@
fun explode_thm thm =
(case HOLogic.dest_Trueprop (Thm.prop_of thm) of
- \<^const>\<open>HOL.conj\<close> $ _ $ _ => explode_conj_thm @{thm conjunct1} @{thm conjunct2} thm
- | \<^const>\<open>HOL.Not\<close> $ (\<^const>\<open>HOL.disj\<close> $ _ $ _) => explode_conj_thm ndisj1_rule ndisj2_rule thm
- | \<^const>\<open>HOL.Not\<close> $ (\<^const>\<open>HOL.Not\<close> $ _) => explode_thm (thm RS @{thm notnotD})
+ \<^Const_>\<open>conj for _ _\<close> => explode_conj_thm @{thm conjunct1} @{thm conjunct2} thm
+ | \<^Const_>\<open>Not for \<^Const_>\<open>disj for _ _\<close>\<close> => explode_conj_thm ndisj1_rule ndisj2_rule thm
+ | \<^Const_>\<open>Not for \<^Const_>\<open>Not for _\<close>\<close> => explode_thm (thm RS @{thm notnotD})
| _ => add_lit thm)
and explode_conj_thm rule1 rule2 thm lits =
@@ -36,7 +36,7 @@
val not_false_rule = @{lemma "\<not>False" by auto}
fun explode thm = explode_thm thm (add_lit not_false_rule (add_lit @{thm TrueI} Termtab.empty))
-fun find_dual_lit lits (\<^const>\<open>HOL.Not\<close> $ t, thm) = Termtab.lookup lits t |> Option.map (pair thm)
+fun find_dual_lit lits (\<^Const_>\<open>Not for t\<close>, thm) = Termtab.lookup lits t |> Option.map (pair thm)
| find_dual_lit _ _ = NONE
fun find_dual_lits lits = Termtab.get_first (find_dual_lit lits) lits
@@ -49,10 +49,10 @@
SOME thm => thm
| NONE => join_term lits t)
-and join_term lits (\<^const>\<open>HOL.conj\<close> $ t $ u) = @{thm conjI} OF (map (join lits) [t, u])
- | join_term lits (\<^const>\<open>HOL.Not\<close> $ (\<^const>\<open>HOL.disj\<close> $ t $ u)) =
+and join_term lits \<^Const_>\<open>conj for t u\<close> = @{thm conjI} OF (map (join lits) [t, u])
+ | join_term lits \<^Const_>\<open>Not for \<^Const_>\<open>HOL.disj for t u\<close>\<close> =
ndisj_rule OF (map (join lits o HOLogic.mk_not) [t, u])
- | join_term lits (\<^const>\<open>HOL.Not\<close> $ (\<^const>\<open>HOL.Not\<close> $ t)) = join lits t RS not_not_rule
+ | join_term lits \<^Const_>\<open>Not for \<^Const>\<open>Not for t\<close>\<close> = join lits t RS not_not_rule
| join_term _ t = raise TERM ("join_term", [t])
fun prove_conj_disj_imp ct cu = with_assumption ct (fn thm => join (explode thm) (Thm.term_of cu))
@@ -68,19 +68,19 @@
fun prove_any_imp ct =
(case Thm.term_of ct of
- \<^const>\<open>HOL.False\<close> => @{thm FalseE}
- | \<^const>\<open>HOL.Not\<close> $ (\<^const>\<open>HOL.Not\<close> $ \<^const>\<open>HOL.False\<close>) => not_not_false_rule
- | \<^const>\<open>HOL.Not\<close> $ \<^const>\<open>HOL.True\<close> => not_true_rule
+ \<^Const_>\<open>False\<close> => @{thm FalseE}
+ | \<^Const_>\<open>Not for \<^Const>\<open>Not for \<^Const>\<open>False\<close>\<close>\<close> => not_not_false_rule
+ | \<^Const_>\<open>Not for \<^Const>\<open>True\<close>\<close> => not_true_rule
| _ => raise CTERM ("prove_any_imp", [ct]))
fun prove_contradiction_imp ct =
with_assumption ct (fn thm =>
let val lits = explode thm
in
- (case Termtab.lookup lits \<^const>\<open>HOL.False\<close> of
+ (case Termtab.lookup lits \<^Const>\<open>False\<close> of
SOME thm' => thm' RS @{thm FalseE}
| NONE =>
- (case Termtab.lookup lits (\<^const>\<open>HOL.Not\<close> $ \<^const>\<open>HOL.True\<close>) of
+ (case Termtab.lookup lits \<^Const>\<open>Not for \<^Const>\<open>True\<close>\<close> of
SOME thm' => thm' RS not_true_rule
| NONE =>
(case find_dual_lits lits of
@@ -99,13 +99,13 @@
datatype kind = True | False | Conj | Disj | Other
-fun choose t _ _ _ \<^const>\<open>HOL.True\<close> = t
- | choose _ f _ _ \<^const>\<open>HOL.False\<close> = f
- | choose _ _ c _ (\<^const>\<open>HOL.conj\<close> $ _ $ _) = c
- | choose _ _ _ d (\<^const>\<open>HOL.disj\<close> $ _ $ _) = d
+fun choose t _ _ _ \<^Const_>\<open>True\<close> = t
+ | choose _ f _ _ \<^Const_>\<open>False\<close> = f
+ | choose _ _ c _ \<^Const_>\<open>conj for _ _\<close> = c
+ | choose _ _ _ d \<^Const_>\<open>disj for _ _\<close> = d
| choose _ _ _ _ _ = Other
-fun kind_of (\<^const>\<open>HOL.Not\<close> $ t) = choose False True Disj Conj t
+fun kind_of \<^Const_>\<open>Not for t\<close> = choose False True Disj Conj t
| kind_of t = choose True False Conj Disj t
fun prove_conj_disj_perm ct cp =
@@ -120,7 +120,7 @@
fun conj_disj_perm_tac ctxt = CSUBGOAL (fn (ct, i) =>
(case Thm.term_of ct of
- \<^const>\<open>HOL.Trueprop\<close> $ (@{const HOL.eq(bool)} $ _ $ _) =>
+ \<^Const_>\<open>Trueprop for \<^Const>\<open>HOL.eq \<^Type>\<open>bool\<close> for _ _\<close>\<close> =>
resolve_tac ctxt [prove_conj_disj_perm ct (Thm.dest_binop (Thm.dest_arg ct))] i
| _ => no_tac))
--- a/src/HOL/Tools/SMT/smt_normalize.ML Tue Sep 28 12:35:43 2021 +0200
+++ b/src/HOL/Tools/SMT/smt_normalize.ML Wed Sep 29 09:58:19 2021 +0200
@@ -31,7 +31,7 @@
(** instantiate elimination rules **)
local
- val (cpfalse, cfalse) = `SMT_Util.mk_cprop (Thm.cterm_of \<^context> \<^const>\<open>False\<close>)
+ val (cpfalse, cfalse) = `SMT_Util.mk_cprop \<^cterm>\<open>False\<close>
fun inst f ct thm =
let val cv = f (Drule.strip_imp_concl (Thm.cprop_of thm))
@@ -40,7 +40,7 @@
fun instantiate_elim thm =
(case Thm.concl_of thm of
- \<^const>\<open>Trueprop\<close> $ Var (_, \<^typ>\<open>bool\<close>) => inst Thm.dest_arg cfalse thm
+ \<^Const_>\<open>Trueprop for \<open>Var (_, \<^Type>\<open>bool\<close>)\<close>\<close> => inst Thm.dest_arg cfalse thm
| Var _ => inst I cpfalse thm
| _ => thm)
@@ -51,9 +51,8 @@
fun norm_def thm =
(case Thm.prop_of thm of
- \<^const>\<open>Trueprop\<close> $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ _ $ Abs _) =>
- norm_def (thm RS @{thm fun_cong})
- | Const (\<^const_name>\<open>Pure.eq\<close>, _) $ _ $ Abs _ => norm_def (HOLogic.mk_obj_eq thm)
+ \<^Const_>\<open>Trueprop for \<^Const>\<open>HOL.eq _ for _ \<open>Abs _\<close>\<close>\<close> => norm_def (thm RS @{thm fun_cong})
+ | \<^Const_>\<open>Pure.eq _ for _ \<open>Abs _\<close>\<close> => norm_def (HOLogic.mk_obj_eq thm)
| _ => thm)
@@ -61,11 +60,11 @@
fun atomize_conv ctxt ct =
(case Thm.term_of ct of
- \<^const>\<open>Pure.imp\<close> $ _ $ _ =>
+ \<^Const_>\<open>Pure.imp for _ _\<close> =>
Conv.binop_conv (atomize_conv ctxt) then_conv Conv.rewr_conv @{thm atomize_imp}
- | Const (\<^const_name>\<open>Pure.eq\<close>, _) $ _ $ _ =>
+ | \<^Const_>\<open>Pure.eq _ for _ _\<close> =>
Conv.binop_conv (atomize_conv ctxt) then_conv Conv.rewr_conv @{thm atomize_eq}
- | Const (\<^const_name>\<open>Pure.all\<close>, _) $ Abs _ =>
+ | \<^Const_>\<open>Pure.all _ for \<open>Abs _\<close>\<close> =>
Conv.binder_conv (atomize_conv o snd) ctxt then_conv Conv.rewr_conv @{thm atomize_all}
| _ => Conv.all_conv) ct
handle CTERM _ => Conv.all_conv ct
@@ -120,9 +119,9 @@
fun proper_quant inside f t =
(case t of
- Const (\<^const_name>\<open>All\<close>, _) $ Abs (_, _, u) => proper_quant true f u
- | Const (\<^const_name>\<open>Ex\<close>, _) $ Abs (_, _, u) => proper_quant true f u
- | \<^const>\<open>trigger\<close> $ p $ u =>
+ \<^Const_>\<open>All _ for \<open>Abs (_, _, u)\<close>\<close> => proper_quant true f u
+ | \<^Const_>\<open>Ex _ for \<open>Abs (_, _, u)\<close>\<close> => proper_quant true f u
+ | \<^Const_>\<open>trigger for p u\<close> =>
(if inside then f p else false) andalso proper_quant false f u
| Abs (_, _, u) => proper_quant false f u
| u1 $ u2 => proper_quant false f u1 andalso proper_quant false f u2
@@ -142,7 +141,7 @@
fun dest_cond_eq ct =
(case Thm.term_of ct of
Const (\<^const_name>\<open>HOL.eq\<close>, _) $ _ $ _ => Thm.dest_binop ct
- | \<^const>\<open>HOL.implies\<close> $ _ $ _ => dest_cond_eq (Thm.dest_arg ct)
+ | \<^Const_>\<open>implies for _ _\<close> => dest_cond_eq (Thm.dest_arg ct)
| _ => raise CTERM ("no equation", [ct]))
fun get_constrs thy (Type (n, _)) = these (BNF_LFP_Compat.get_constrs thy n)
@@ -220,7 +219,7 @@
in insert_trigger_conv (filter_mpats (get_mpats lhs)) ct end
- fun has_trigger (\<^const>\<open>trigger\<close> $ _ $ _) = true
+ fun has_trigger \<^Const_>\<open>trigger for _ _\<close> = true
| has_trigger _ = false
fun try_trigger_conv cv ct =
@@ -331,12 +330,12 @@
local
val simple_nat_ops = [
- @{const HOL.eq (nat)}, @{const less (nat)}, @{const less_eq (nat)},
- \<^const>\<open>Suc\<close>, @{const plus (nat)}, @{const minus (nat)}]
+ \<^Const>\<open>HOL.eq \<^Type>\<open>nat\<close>\<close>, \<^Const>\<open>less \<^Type>\<open>nat\<close>\<close>, \<^Const>\<open>less_eq \<^Type>\<open>nat\<close>\<close>,
+ \<^Const>\<open>Suc\<close>, \<^Const>\<open>plus \<^Type>\<open>nat\<close>\<close>, \<^Const>\<open>minus \<^Type>\<open>nat\<close>\<close>]
val nat_consts = simple_nat_ops @
- [@{const numeral (nat)}, @{const zero_class.zero (nat)}, @{const one_class.one (nat)}] @
- [@{const times (nat)}, @{const divide (nat)}, @{const modulo (nat)}]
+ [\<^Const>\<open>numeral \<^Type>\<open>nat\<close>\<close>, \<^Const>\<open>zero_class.zero \<^Type>\<open>nat\<close>\<close>, \<^Const>\<open>one_class.one \<^Type>\<open>nat\<close>\<close>] @
+ [\<^Const>\<open>times \<^Type>\<open>nat\<close>\<close>, \<^Const>\<open>divide \<^Type>\<open>nat\<close>\<close>, \<^Const>\<open>modulo \<^Type>\<open>nat\<close>\<close>]
val is_nat_const = member (op aconv) nat_consts
@@ -349,10 +348,10 @@
fun int_ops_conv cv ctxt ct =
(case Thm.term_of ct of
- @{const of_nat (int)} $ (Const (\<^const_name>\<open>If\<close>, _) $ _ $ _ $ _) =>
+ \<^Const_>\<open>of_nat \<^Type>\<open>int\<close> for \<open>\<^Const_>\<open>If _ for _ _ _\<close>\<close>\<close> =>
Conv.rewr_conv int_if_thm then_conv
if_conv (cv ctxt) (int_ops_conv cv ctxt)
- | @{const of_nat (int)} $ _ =>
+ | \<^Const>\<open>of_nat \<^Type>\<open>int\<close> for _\<close> =>
(Conv.rewrs_conv int_ops_thms then_conv
Conv.top_sweep_conv (int_ops_conv cv) ctxt) else_conv
Conv.arg_conv (Conv.sub_conv cv ctxt)
@@ -372,7 +371,7 @@
fun add_int_of_nat vs ct cu (q, cts) =
(case Thm.term_of ct of
- @{const of_nat(int)} =>
+ \<^Const>\<open>of_nat \<^Type>\<open>int\<close>\<close> =>
if Term.exists_subterm (member (op aconv) vs) (Thm.term_of cu) then (true, cts)
else (q, insert (op aconvc) cu cts)
| _ => (q, cts))
@@ -490,7 +489,7 @@
val schematic_consts_of =
let
- fun collect (\<^const>\<open>trigger\<close> $ p $ t) = collect_trigger p #> collect t
+ fun collect \<^Const_>\<open>trigger for p t\<close> = collect_trigger p #> collect t
| collect (t $ u) = collect t #> collect u
| collect (Abs (_, _, t)) = collect t
| collect (t as Const (n, _)) =
--- a/src/HOL/Tools/SMT/smt_real.ML Tue Sep 28 12:35:43 2021 +0200
+++ b/src/HOL/Tools/SMT/smt_real.ML Wed Sep 29 09:58:19 2021 +0200
@@ -25,7 +25,7 @@
| is_linear [t, u] = SMT_Util.is_number t orelse SMT_Util.is_number u
| is_linear _ = false
- fun mk_times ts = Term.list_comb (@{const times (real)}, ts)
+ fun mk_times ts = Term.list_comb (\<^Const>\<open>times \<^Type>\<open>real\<close>\<close>, ts)
fun times _ _ ts = if is_linear ts then SOME ("*", 2, ts, mk_times) else NONE
in
@@ -34,17 +34,17 @@
SMT_Builtin.add_builtin_typ SMTLIB_Interface.smtlibC
(\<^typ>\<open>real\<close>, K (SOME ("Real", [])), real_num) #>
fold (SMT_Builtin.add_builtin_fun' SMTLIB_Interface.smtlibC) [
- (@{const less (real)}, "<"),
- (@{const less_eq (real)}, "<="),
- (@{const uminus (real)}, "-"),
- (@{const plus (real)}, "+"),
- (@{const minus (real)}, "-") ] #>
+ (\<^Const>\<open>less \<^Type>\<open>real\<close>\<close>, "<"),
+ (\<^Const>\<open>less_eq \<^Type>\<open>real\<close>\<close>, "<="),
+ (\<^Const>\<open>uminus \<^Type>\<open>real\<close>\<close>, "-"),
+ (\<^Const>\<open>plus \<^Type>\<open>real\<close>\<close>, "+"),
+ (\<^Const>\<open>minus \<^Type>\<open>real\<close>\<close>, "-") ] #>
SMT_Builtin.add_builtin_fun SMTLIB_Interface.smtlibC
- (Term.dest_Const @{const times (real)}, times) #>
+ (Term.dest_Const \<^Const>\<open>times \<^Type>\<open>real\<close>\<close>, times) #>
SMT_Builtin.add_builtin_fun' Z3_Interface.smtlib_z3C
- (@{const times (real)}, "*") #>
+ (\<^Const>\<open>times \<^Type>\<open>real\<close>\<close>, "*") #>
SMT_Builtin.add_builtin_fun' Z3_Interface.smtlib_z3C
- (@{const divide (real)}, "/")
+ (\<^Const>\<open>divide \<^Type>\<open>real\<close>\<close>, "/")
end
@@ -64,14 +64,14 @@
fun mk_nary _ cu [] = cu
| mk_nary ct _ cts = uncurry (fold_rev (Thm.mk_binop ct)) (split_last cts)
- val mk_uminus = Thm.apply (Thm.cterm_of \<^context> @{const uminus (real)})
- val add = Thm.cterm_of \<^context> @{const plus (real)}
+ val mk_uminus = Thm.apply \<^cterm>\<open>uminus :: real \<Rightarrow> _\<close>
+ val add = \<^cterm>\<open>(+) :: real \<Rightarrow> _\<close>
val real0 = Numeral.mk_cnumber \<^ctyp>\<open>real\<close> 0
- val mk_sub = Thm.mk_binop (Thm.cterm_of \<^context> @{const minus (real)})
- val mk_mul = Thm.mk_binop (Thm.cterm_of \<^context> @{const times (real)})
- val mk_div = Thm.mk_binop (Thm.cterm_of \<^context> @{const divide (real)})
- val mk_lt = Thm.mk_binop (Thm.cterm_of \<^context> @{const less (real)})
- val mk_le = Thm.mk_binop (Thm.cterm_of \<^context> @{const less_eq (real)})
+ val mk_sub = Thm.mk_binop \<^cterm>\<open>(-) :: real \<Rightarrow> _\<close>
+ val mk_mul = Thm.mk_binop \<^cterm>\<open>(*) :: real \<Rightarrow> _\<close>
+ val mk_div = Thm.mk_binop \<^cterm>\<open>(/) :: real \<Rightarrow> _\<close>
+ val mk_lt = Thm.mk_binop \<^cterm>\<open>(<) :: real \<Rightarrow> _\<close>
+ val mk_le = Thm.mk_binop \<^cterm>\<open>(\<le>) :: real \<Rightarrow> _\<close>
fun z3_mk_builtin_fun (Z3_Interface.Sym ("-", _)) [ct] = SOME (mk_uminus ct)
| z3_mk_builtin_fun (Z3_Interface.Sym ("+", _)) cts = SOME (mk_nary add real0 cts)
--- a/src/HOL/Tools/SMT/smt_replay_methods.ML Tue Sep 28 12:35:43 2021 +0200
+++ b/src/HOL/Tools/SMT/smt_replay_methods.ML Wed Sep 29 09:58:19 2021 +0200
@@ -218,30 +218,30 @@
fun abstract_ter abs f t t1 t2 t3 =
abstract_sub t (abs t1 ##>> abs t2 ##>> abs t3 #>> (Scan.triple1 #> f))
-fun abstract_lit (\<^const>\<open>HOL.Not\<close> $ t) = abstract_term t #>> HOLogic.mk_not
+fun abstract_lit \<^Const>\<open>Not for t\<close> = abstract_term t #>> HOLogic.mk_not
| abstract_lit t = abstract_term t
-fun abstract_not abs (t as \<^const>\<open>HOL.Not\<close> $ t1) =
+fun abstract_not abs (t as \<^Const_>\<open>Not\<close> $ t1) =
abstract_sub t (abs t1 #>> HOLogic.mk_not)
| abstract_not _ t = abstract_lit t
-fun abstract_conj (t as \<^const>\<open>HOL.conj\<close> $ t1 $ t2) =
+fun abstract_conj (t as \<^Const_>\<open>conj\<close> $ t1 $ t2) =
abstract_bin abstract_conj HOLogic.mk_conj t t1 t2
| abstract_conj t = abstract_lit t
-fun abstract_disj (t as \<^const>\<open>HOL.disj\<close> $ t1 $ t2) =
+fun abstract_disj (t as \<^Const_>\<open>disj\<close> $ t1 $ t2) =
abstract_bin abstract_disj HOLogic.mk_disj t t1 t2
| abstract_disj t = abstract_lit t
-fun abstract_prop (t as (c as @{const If (bool)}) $ t1 $ t2 $ t3) =
+fun abstract_prop (t as (c as \<^Const>\<open>If \<^Type>\<open>bool\<close>\<close>) $ t1 $ t2 $ t3) =
abstract_ter abstract_prop (fn (t1, t2, t3) => c $ t1 $ t2 $ t3) t t1 t2 t3
- | abstract_prop (t as \<^const>\<open>HOL.disj\<close> $ t1 $ t2) =
+ | abstract_prop (t as \<^Const_>\<open>disj\<close> $ t1 $ t2) =
abstract_bin abstract_prop HOLogic.mk_disj t t1 t2
- | abstract_prop (t as \<^const>\<open>HOL.conj\<close> $ t1 $ t2) =
+ | abstract_prop (t as \<^Const_>\<open>conj\<close> $ t1 $ t2) =
abstract_bin abstract_prop HOLogic.mk_conj t t1 t2
- | abstract_prop (t as \<^const>\<open>HOL.implies\<close> $ t1 $ t2) =
+ | abstract_prop (t as \<^Const_>\<open>implies\<close> $ t1 $ t2) =
abstract_bin abstract_prop HOLogic.mk_imp t t1 t2
- | abstract_prop (t as \<^term>\<open>HOL.eq :: bool => _\<close> $ t1 $ t2) =
+ | abstract_prop (t as \<^Const_>\<open>HOL.eq \<^Type>\<open>bool\<close>\<close> $ t1 $ t2) =
abstract_bin abstract_prop HOLogic.mk_eq t t1 t2
| abstract_prop t = abstract_not abstract_prop t
@@ -253,8 +253,8 @@
abstract_sub t (abs t' #>> (fn u' => c $ Abs (s, T, u')))
| abs (t as (c as Const (\<^const_name>\<open>If\<close>, _)) $ t1 $ t2 $ t3) =
abstract_ter abs (fn (t1, t2, t3) => c $ t1 $ t2 $ t3) t t1 t2 t3
- | abs (t as \<^const>\<open>HOL.Not\<close> $ t1) = abstract_sub t (abs t1 #>> HOLogic.mk_not)
- | abs (t as \<^const>\<open>HOL.disj\<close> $ t1 $ t2) =
+ | abs (t as \<^Const_>\<open>Not\<close> $ t1) = abstract_sub t (abs t1 #>> HOLogic.mk_not)
+ | abs (t as \<^Const_>\<open>disj\<close> $ t1 $ t2) =
abstract_sub t (abs t1 ##>> abs t2 #>> HOLogic.mk_disj)
| abs (t as (c as Const (\<^const_name>\<open>uminus_class.uminus\<close>, _)) $ t1) =
abstract_sub t (abs t1 #>> (fn u => c $ u))
@@ -282,10 +282,10 @@
| (NONE, _) => abstract_term t cx))
in abs u end
-fun abstract_unit (t as (\<^const>\<open>HOL.Not\<close> $ (\<^const>\<open>HOL.disj\<close> $ t1 $ t2))) =
+fun abstract_unit (t as \<^Const_>\<open>Not for \<^Const_>\<open>disj for t1 t2\<close>\<close>) =
abstract_sub t (abstract_unit t1 ##>> abstract_unit t2 #>>
HOLogic.mk_not o HOLogic.mk_disj)
- | abstract_unit (t as (\<^const>\<open>HOL.disj\<close> $ t1 $ t2)) =
+ | abstract_unit (t as \<^Const_>\<open>disj for t1 t2\<close>) =
abstract_sub t (abstract_unit t1 ##>> abstract_unit t2 #>>
HOLogic.mk_disj)
| abstract_unit (t as (Const(\<^const_name>\<open>HOL.eq\<close>, _) $ t1 $ t2)) =
@@ -293,49 +293,49 @@
abstract_sub t (abstract_unit t1 ##>> abstract_unit t2 #>>
HOLogic.mk_eq)
else abstract_lit t
- | abstract_unit (t as (\<^const>\<open>HOL.Not\<close> $ (Const(\<^const_name>\<open>HOL.eq\<close>, _) $ t1 $ t2))) =
+ | abstract_unit (t as \<^Const_>\<open>Not for \<^Const_>\<open>HOL.eq _ for t1 t2\<close>\<close>) =
if fastype_of t1 = \<^typ>\<open>bool\<close> then
abstract_sub t (abstract_unit t1 ##>> abstract_unit t2 #>>
HOLogic.mk_eq #>> HOLogic.mk_not)
else abstract_lit t
- | abstract_unit (t as (\<^const>\<open>HOL.Not\<close> $ t1)) =
+ | abstract_unit (t as \<^Const>\<open>Not for t1\<close>) =
abstract_sub t (abstract_unit t1 #>> HOLogic.mk_not)
| abstract_unit t = abstract_lit t
-fun abstract_bool (t as (@{const HOL.disj} $ t1 $ t2)) =
+fun abstract_bool (t as \<^Const_>\<open>disj for t1 t2\<close>) =
abstract_sub t (abstract_bool t1 ##>> abstract_bool t2 #>>
HOLogic.mk_disj)
- | abstract_bool (t as (@{const HOL.conj} $ t1 $ t2)) =
+ | abstract_bool (t as \<^Const_>\<open>conj for t1 t2\<close>) =
abstract_sub t (abstract_bool t1 ##>> abstract_bool t2 #>>
HOLogic.mk_conj)
- | abstract_bool (t as (Const(@{const_name HOL.eq}, _) $ t1 $ t2)) =
+ | abstract_bool (t as \<^Const_>\<open>HOL.eq _ for t1 t2\<close>) =
if fastype_of t1 = @{typ bool} then
abstract_sub t (abstract_bool t1 ##>> abstract_bool t2 #>>
HOLogic.mk_eq)
else abstract_lit t
- | abstract_bool (t as (@{const HOL.Not} $ t1)) =
+ | abstract_bool (t as \<^Const_>\<open>Not for t1\<close>) =
abstract_sub t (abstract_bool t1 #>> HOLogic.mk_not)
- | abstract_bool (t as (@{const HOL.implies} $ t1 $ t2)) =
+ | abstract_bool (t as \<^Const>\<open>implies for t1 t2\<close>) =
abstract_sub t (abstract_bool t1 ##>> abstract_bool t2 #>>
HOLogic.mk_imp)
| abstract_bool t = abstract_lit t
-fun abstract_bool_shallow (t as (@{const HOL.disj} $ t1 $ t2)) =
+fun abstract_bool_shallow (t as \<^Const_>\<open>disj for t1 t2\<close>) =
abstract_sub t (abstract_bool_shallow t1 ##>> abstract_bool_shallow t2 #>>
HOLogic.mk_disj)
- | abstract_bool_shallow (t as (@{const HOL.Not} $ t1)) =
+ | abstract_bool_shallow (t as \<^Const_>\<open>Not for t1\<close>) =
abstract_sub t (abstract_bool_shallow t1 #>> HOLogic.mk_not)
| abstract_bool_shallow t = abstract_term t
-fun abstract_bool_shallow_equivalence (t as (@{const HOL.disj} $ t1 $ t2)) =
+fun abstract_bool_shallow_equivalence (t as \<^Const_>\<open>disj for t1 t2\<close>) =
abstract_sub t (abstract_bool_shallow_equivalence t1 ##>> abstract_bool_shallow_equivalence t2 #>>
HOLogic.mk_disj)
- | abstract_bool_shallow_equivalence (t as (Const(@{const_name HOL.eq}, _) $ t1 $ t2)) =
- if fastype_of t1 = @{typ bool} then
+ | abstract_bool_shallow_equivalence (t as \<^Const_>\<open>HOL.eq _ for t1 t2\<close>) =
+ if fastype_of t1 = \<^Type>\<open>bool\<close> then
abstract_sub t (abstract_lit t1 ##>> abstract_lit t2 #>>
HOLogic.mk_eq)
else abstract_lit t
- | abstract_bool_shallow_equivalence (t as (@{const HOL.Not} $ t1)) =
+ | abstract_bool_shallow_equivalence (t as \<^Const_>\<open>Not for t1\<close>) =
abstract_sub t (abstract_bool_shallow_equivalence t1 #>> HOLogic.mk_not)
| abstract_bool_shallow_equivalence t = abstract_lit t
@@ -347,8 +347,8 @@
abstract_sub t (abs t' #>> (fn u' => c $ Abs (s, T, u')))
| abs (t as (Const (\<^const_name>\<open>If\<close>, _)) $ _ $ _ $ _) =
abstract_sub t (abstract_term t)
- | abs (t as \<^const>\<open>HOL.Not\<close> $ t1) = abstract_sub t (abs t1 #>> HOLogic.mk_not)
- | abs (t as \<^const>\<open>HOL.disj\<close> $ t1 $ t2) =
+ | abs (t as \<^Const>\<open>Not\<close> $ t1) = abstract_sub t (abs t1 #>> HOLogic.mk_not)
+ | abs (t as \<^Const>\<open>disj\<close> $ t1 $ t2) =
abstract_sub t (abs t1 ##>> abs t2 #>> HOLogic.mk_disj)
| abs (t as (c as Const (\<^const_name>\<open>uminus_class.uminus\<close>, _)) $ t1) =
abstract_sub t (abs t1 #>> (fn u => c $ u))
--- a/src/HOL/Tools/SMT/smt_translate.ML Tue Sep 28 12:35:43 2021 +0200
+++ b/src/HOL/Tools/SMT/smt_translate.ML Wed Sep 29 09:58:19 2021 +0200
@@ -306,12 +306,12 @@
| (u as Bound i, ts) => apply 0 u (nth Ts i) (map (traverse Ts) ts)
| (Abs (n, T, u), ts) => traverses Ts (Abs (n, T, traverse (T::Ts) u)) ts
| (u, ts) => traverses Ts u ts)
- and in_trigger Ts ((c as \<^const>\<open>trigger\<close>) $ p $ t) = c $ in_pats Ts p $ traverse Ts t
+ and in_trigger Ts ((c as \<^Const_>\<open>trigger\<close>) $ p $ t) = c $ in_pats Ts p $ traverse Ts t
| in_trigger Ts t = traverse Ts t
and in_pats Ts ps =
in_list \<^typ>\<open>pattern symb_list\<close> (in_list \<^typ>\<open>pattern\<close> (in_pat Ts)) ps
- and in_pat Ts ((p as Const (\<^const_name>\<open>pat\<close>, _)) $ t) = p $ traverse Ts t
- | in_pat Ts ((p as Const (\<^const_name>\<open>nopat\<close>, _)) $ t) = p $ traverse Ts t
+ and in_pat Ts ((p as \<^Const_>\<open>pat _\<close>) $ t) = p $ traverse Ts t
+ | in_pat Ts ((p as \<^Const_>\<open>nopat _\<close>) $ t) = p $ traverse Ts t
| in_pat _ t = raise TERM ("bad pattern", [t])
and traverses Ts t ts = Term.list_comb (t, map (traverse Ts) ts)
in map (traverse []) ts end
@@ -343,9 +343,9 @@
fun in_term pat t =
(case Term.strip_comb t of
- (\<^const>\<open>True\<close>, []) => t
- | (\<^const>\<open>False\<close>, []) => t
- | (u as Const (\<^const_name>\<open>If\<close>, _), [t1, t2, t3]) =>
+ (\<^Const_>\<open>True\<close>, []) => t
+ | (\<^Const_>\<open>False\<close>, []) => t
+ | (u as \<^Const_>\<open>If _\<close>, [t1, t2, t3]) =>
if pat then raise BAD_PATTERN () else u $ in_form t1 $ in_term pat t2 $ in_term pat t3
| (Const (c as (n, _)), ts) =>
if is_builtin_conn_or_pred ctxt c ts orelse is_quant n then
@@ -364,7 +364,7 @@
and in_pats ps =
in_list \<^typ>\<open>pattern symb_list\<close> (SOME o in_list \<^typ>\<open>pattern\<close> (try in_pat)) ps
- and in_trigger ((c as \<^const>\<open>trigger\<close>) $ p $ t) = c $ in_pats p $ in_form t
+ and in_trigger ((c as \<^Const_>\<open>trigger\<close>) $ p $ t) = c $ in_pats p $ in_form t
| in_trigger t = in_form t
and in_form t =
@@ -412,7 +412,7 @@
| (ps, [false]) => cons (SNoPat ps)
| _ => raise TERM ("bad multi-pattern", ts))
-fun dest_trigger (\<^const>\<open>trigger\<close> $ tl $ t) =
+fun dest_trigger \<^Const_>\<open>trigger for tl t\<close> =
(rev (fold (dest_pats o SMT_Util.dest_symb_list) (SMT_Util.dest_symb_list tl) []), t)
| dest_trigger t = ([], t)
@@ -511,7 +511,7 @@
|> (fn T => Const (\<^const_name>\<open>pat\<close>, T) $ lhs)
|> SMT_Util.mk_symb_list \<^typ>\<open>pattern\<close> o single
|> SMT_Util.mk_symb_list \<^typ>\<open>pattern symb_list\<close> o single
- |> (fn t => \<^const>\<open>trigger\<close> $ t $ eq)
+ |> (fn t => \<^Const>\<open>trigger for t eq\<close>)
| mk_trigger t = t
val (ctxt2, (ts3, ll_defs)) =
--- a/src/HOL/Tools/SMT/smt_util.ML Tue Sep 28 12:35:43 2021 +0200
+++ b/src/HOL/Tools/SMT/smt_util.ML Wed Sep 29 09:58:19 2021 +0200
@@ -131,16 +131,16 @@
(* terms *)
-fun dest_conj (\<^const>\<open>HOL.conj\<close> $ t $ u) = (t, u)
+fun dest_conj \<^Const_>\<open>conj for t u\<close> = (t, u)
| dest_conj t = raise TERM ("not a conjunction", [t])
-fun dest_disj (\<^const>\<open>HOL.disj\<close> $ t $ u) = (t, u)
+fun dest_disj \<^Const_>\<open>disj for t u\<close> = (t, u)
| dest_disj t = raise TERM ("not a disjunction", [t])
fun under_quant f t =
(case t of
- Const (\<^const_name>\<open>All\<close>, _) $ Abs (_, _, u) => under_quant f u
- | Const (\<^const_name>\<open>Ex\<close>, _) $ Abs (_, _, u) => under_quant f u
+ \<^Const_>\<open>All _ for \<open>Abs (_, _, u)\<close>\<close> => under_quant f u
+ | \<^Const_>\<open>Ex _ for \<open>Abs (_, _, u)\<close>\<close> => under_quant f u
| _ => f t)
val is_number =
@@ -197,17 +197,17 @@
val dest_all_cbinders = repeat_yield (try o dest_cbinder)
-val mk_cprop = Thm.apply (Thm.cterm_of \<^context> \<^const>\<open>Trueprop\<close>)
+val mk_cprop = Thm.apply \<^cterm>\<open>Trueprop\<close>
fun dest_cprop ct =
(case Thm.term_of ct of
- \<^const>\<open>Trueprop\<close> $ _ => Thm.dest_arg ct
+ \<^Const_>\<open>Trueprop for _\<close> => Thm.dest_arg ct
| _ => raise CTERM ("not a property", [ct]))
val equals = mk_const_pat \<^theory> \<^const_name>\<open>Pure.eq\<close> Thm.dest_ctyp0
fun mk_cequals ct cu = Thm.mk_binop (instT' ct equals) ct cu
-val dest_prop = (fn \<^const>\<open>Trueprop\<close> $ t => t | t => t)
+val dest_prop = fn \<^Const_>\<open>Trueprop for t\<close> => t | t => t
fun term_of ct = dest_prop (Thm.term_of ct)
fun prop_of thm = dest_prop (Thm.prop_of thm)
@@ -237,7 +237,7 @@
fun prop_conv cv ct =
(case Thm.term_of ct of
- \<^const>\<open>Trueprop\<close> $ _ => Conv.arg_conv cv ct
+ \<^Const_>\<open>Trueprop for _\<close> => Conv.arg_conv cv ct
| _ => raise CTERM ("not a property", [ct]))
end;
--- a/src/HOL/Tools/SMT/smtlib_interface.ML Tue Sep 28 12:35:43 2021 +0200
+++ b/src/HOL/Tools/SMT/smtlib_interface.ML Wed Sep 29 09:58:19 2021 +0200
@@ -35,7 +35,7 @@
| is_linear _ = false
fun times _ _ ts =
- let val mk = Term.list_comb o pair @{const times (int)}
+ let val mk = Term.list_comb o pair \<^Const>\<open>times \<^Type>\<open>int\<close>\<close>
in if is_linear ts then SOME ("*", 2, ts, mk) else NONE end
in
@@ -46,21 +46,21 @@
(\<^typ>\<open>bool\<close>, K (SOME ("Bool", [])), K (K NONE)),
(\<^typ>\<open>int\<close>, K (SOME ("Int", [])), int_num)] #>
fold (SMT_Builtin.add_builtin_fun' smtlibC) [
- (\<^const>\<open>True\<close>, "true"),
- (\<^const>\<open>False\<close>, "false"),
- (\<^const>\<open>Not\<close>, "not"),
- (\<^const>\<open>HOL.conj\<close>, "and"),
- (\<^const>\<open>HOL.disj\<close>, "or"),
- (\<^const>\<open>HOL.implies\<close>, "=>"),
- (@{const HOL.eq ('a)}, "="),
- (@{const If ('a)}, "ite"),
- (@{const less (int)}, "<"),
- (@{const less_eq (int)}, "<="),
- (@{const uminus (int)}, "-"),
- (@{const plus (int)}, "+"),
- (@{const minus (int)}, "-")] #>
+ (\<^Const>\<open>True\<close>, "true"),
+ (\<^Const>\<open>False\<close>, "false"),
+ (\<^Const>\<open>Not\<close>, "not"),
+ (\<^Const>\<open>conj\<close>, "and"),
+ (\<^Const>\<open>disj\<close>, "or"),
+ (\<^Const>\<open>implies\<close>, "=>"),
+ (\<^Const>\<open>HOL.eq \<^typ>\<open>'a\<close>\<close>, "="),
+ (\<^Const>\<open>If \<^typ>\<open>'a\<close>\<close>, "ite"),
+ (\<^Const>\<open>less \<^Type>\<open>int\<close>\<close>, "<"),
+ (\<^Const>\<open>less_eq \<^Type>\<open>int\<close>\<close>, "<="),
+ (\<^Const>\<open>uminus \<^Type>\<open>int\<close>\<close>, "-"),
+ (\<^Const>\<open>plus \<^Type>\<open>int\<close>\<close>, "+"),
+ (\<^Const>\<open>minus \<^Type>\<open>int\<close>\<close>, "-")] #>
SMT_Builtin.add_builtin_fun smtlibC
- (Term.dest_Const @{const times (int)}, times)
+ (Term.dest_Const \<^Const>\<open>times \<^Type>\<open>int\<close>\<close>, times)
end
--- a/src/HOL/Tools/SMT/smtlib_proof.ML Tue Sep 28 12:35:43 2021 +0200
+++ b/src/HOL/Tools/SMT/smtlib_proof.ML Wed Sep 29 09:58:19 2021 +0200
@@ -150,8 +150,8 @@
fun mk_less t1 t2 = mk_binary_pred \<^const_name>\<open>ord_class.less\<close> \<^sort>\<open>linorder\<close> t1 t2
fun mk_less_eq t1 t2 = mk_binary_pred \<^const_name>\<open>ord_class.less_eq\<close> \<^sort>\<open>linorder\<close> t1 t2
-fun core_term_parser (SMTLIB.Sym "true", _) = SOME \<^const>\<open>HOL.True\<close>
- | core_term_parser (SMTLIB.Sym "false", _) = SOME \<^const>\<open>HOL.False\<close>
+fun core_term_parser (SMTLIB.Sym "true", _) = SOME \<^Const>\<open>True\<close>
+ | core_term_parser (SMTLIB.Sym "false", _) = SOME \<^Const>\<open>False\<close>
| core_term_parser (SMTLIB.Sym "not", [t]) = SOME (HOLogic.mk_not t)
| core_term_parser (SMTLIB.Sym "and", t :: ts) = SOME (mk_rassoc (curry HOLogic.mk_conj) t ts)
| core_term_parser (SMTLIB.Sym "or", t :: ts) = SOME (mk_rassoc (curry HOLogic.mk_disj) t ts)
--- a/src/HOL/Tools/SMT/verit_proof.ML Tue Sep 28 12:35:43 2021 +0200
+++ b/src/HOL/Tools/SMT/verit_proof.ML Wed Sep 29 09:58:19 2021 +0200
@@ -738,7 +738,7 @@
fun remove_assumption_id assumption_id prems =
filter_out (curry (op =) assumption_id) prems
fun add_assumption assumption concl =
- \<^const>\<open>Pure.imp\<close> $ mk_prop_of_term assumption $ mk_prop_of_term concl
+ \<^Const>\<open>Pure.imp for \<open>mk_prop_of_term assumption\<close> \<open>mk_prop_of_term concl\<close>\<close>
fun inline_assumption assumption assumption_id
(VeriT_Node {id, rule, prems, proof_ctxt, concl}) =
mk_node id rule (remove_assumption_id assumption_id prems) proof_ctxt
--- a/src/HOL/Tools/SMT/z3_interface.ML Tue Sep 28 12:35:43 2021 +0200
+++ b/src/HOL/Tools/SMT/z3_interface.ML Wed Sep 29 09:58:19 2021 +0200
@@ -38,8 +38,8 @@
fp_kinds = [BNF_Util.Least_FP],
serialize = #serialize (SMTLIB_Interface.translate_config SMT_Util.First_Order ctxt)}
- fun is_div_mod @{const divide (int)} = true
- | is_div_mod @{const modulo (int)} = true
+ fun is_div_mod \<^Const_>\<open>divide \<^Type>\<open>int\<close>\<close> = true
+ | is_div_mod \<^Const>\<open>modulo \<^Type>\<open>int\<close>\<close> = true
| is_div_mod _ = false
val have_int_div_mod = exists (Term.exists_subterm is_div_mod o Thm.prop_of)
@@ -50,9 +50,9 @@
else (thms, extra_thms)
val setup_builtins =
- SMT_Builtin.add_builtin_fun' smtlib_z3C (@{const times (int)}, "*") #>
- SMT_Builtin.add_builtin_fun' smtlib_z3C (\<^const>\<open>z3div\<close>, "div") #>
- SMT_Builtin.add_builtin_fun' smtlib_z3C (\<^const>\<open>z3mod\<close>, "mod")
+ SMT_Builtin.add_builtin_fun' smtlib_z3C (\<^Const>\<open>times \<^Type>\<open>int\<close>\<close>, "*") #>
+ SMT_Builtin.add_builtin_fun' smtlib_z3C (\<^Const>\<open>z3div\<close>, "div") #>
+ SMT_Builtin.add_builtin_fun' smtlib_z3C (\<^Const>\<open>z3mod\<close>, "mod")
in
val _ = Theory.setup (Context.theory_map (
@@ -116,13 +116,13 @@
| mk_builtin_num ctxt i T =
chained_mk_builtin_num ctxt (get_mk_builtins ctxt) i T
-val mk_true = Thm.cterm_of \<^context> (\<^const>\<open>Not\<close> $ \<^const>\<open>False\<close>)
-val mk_false = Thm.cterm_of \<^context> \<^const>\<open>False\<close>
-val mk_not = Thm.apply (Thm.cterm_of \<^context> \<^const>\<open>Not\<close>)
-val mk_implies = Thm.mk_binop (Thm.cterm_of \<^context> \<^const>\<open>HOL.implies\<close>)
-val mk_iff = Thm.mk_binop (Thm.cterm_of \<^context> @{const HOL.eq (bool)})
-val conj = Thm.cterm_of \<^context> \<^const>\<open>HOL.conj\<close>
-val disj = Thm.cterm_of \<^context> \<^const>\<open>HOL.disj\<close>
+val mk_true = \<^cterm>\<open>\<not> False\<close>
+val mk_false = \<^cterm>\<open>False\<close>
+val mk_not = Thm.apply \<^cterm>\<open>HOL.Not\<close>
+val mk_implies = Thm.mk_binop \<^cterm>\<open>HOL.implies\<close>
+val mk_iff = Thm.mk_binop \<^cterm>\<open>(=) :: bool \<Rightarrow> _\<close>
+val conj = \<^cterm>\<open>HOL.conj\<close>
+val disj = \<^cterm>\<open>HOL.disj\<close>
fun mk_nary _ cu [] = cu
| mk_nary ct _ cts = uncurry (fold_rev (Thm.mk_binop ct)) (split_last cts)
@@ -143,15 +143,15 @@
let val cTs = Thm.dest_ctyp (Thm.ctyp_of_cterm array)
in Thm.apply (Thm.mk_binop (SMT_Util.instTs cTs update) array index) value end
-val mk_uminus = Thm.apply (Thm.cterm_of \<^context> @{const uminus (int)})
-val add = Thm.cterm_of \<^context> @{const plus (int)}
+val mk_uminus = Thm.apply \<^cterm>\<open>uminus :: int \<Rightarrow> _\<close>
+val add = \<^cterm>\<open>(+) :: int \<Rightarrow> _\<close>
val int0 = Numeral.mk_cnumber \<^ctyp>\<open>int\<close> 0
-val mk_sub = Thm.mk_binop (Thm.cterm_of \<^context> @{const minus (int)})
-val mk_mul = Thm.mk_binop (Thm.cterm_of \<^context> @{const times (int)})
-val mk_div = Thm.mk_binop (Thm.cterm_of \<^context> \<^const>\<open>z3div\<close>)
-val mk_mod = Thm.mk_binop (Thm.cterm_of \<^context> \<^const>\<open>z3mod\<close>)
-val mk_lt = Thm.mk_binop (Thm.cterm_of \<^context> @{const less (int)})
-val mk_le = Thm.mk_binop (Thm.cterm_of \<^context> @{const less_eq (int)})
+val mk_sub = Thm.mk_binop \<^cterm>\<open>(-) :: int \<Rightarrow> _\<close>
+val mk_mul = Thm.mk_binop \<^cterm>\<open>(*) :: int \<Rightarrow> _\<close>
+val mk_div = Thm.mk_binop \<^cterm>\<open>z3div\<close>
+val mk_mod = Thm.mk_binop \<^cterm>\<open>z3mod\<close>
+val mk_lt = Thm.mk_binop \<^cterm>\<open>(<) :: int \<Rightarrow> _\<close>
+val mk_le = Thm.mk_binop \<^cterm>\<open>(\<le>) :: int \<Rightarrow> _\<close>
fun mk_builtin_fun ctxt sym cts =
(case (sym, cts) of
--- a/src/HOL/Tools/SMT/z3_replay_methods.ML Tue Sep 28 12:35:43 2021 +0200
+++ b/src/HOL/Tools/SMT/z3_replay_methods.ML Wed Sep 29 09:58:19 2021 +0200
@@ -315,10 +315,10 @@
(thm COMP_INCR intro_hyp_rule1)
handle THM _ => thm COMP_INCR intro_hyp_rule2
-fun negated_prop (\<^const>\<open>HOL.Not\<close> $ t) = HOLogic.mk_Trueprop t
+fun negated_prop \<^Const_>\<open>Not for t\<close> = HOLogic.mk_Trueprop t
| negated_prop t = HOLogic.mk_Trueprop (HOLogic.mk_not t)
-fun intro_hyps tab (t as \<^const>\<open>HOL.disj\<close> $ t1 $ t2) cx =
+fun intro_hyps tab (t as \<^Const_>\<open>HOL.disj\<close> $ t1 $ t2) cx =
lookup_intro_hyps tab t (fold (intro_hyps tab) [t1, t2]) cx
| intro_hyps tab t cx =
lookup_intro_hyps tab t (fn _ => raise LEMMA ()) cx
@@ -376,7 +376,7 @@
fun def_axiom_disj ctxt t =
(case dest_prop t of
- \<^const>\<open>HOL.disj\<close> $ u1 $ u2 =>
+ \<^Const_>\<open>disj for u1 u2\<close> =>
SMT_Replay_Methods.prove_abstract' ctxt t prop_tac (
SMT_Replay_Methods.abstract_prop u2 ##>> SMT_Replay_Methods.abstract_prop u1 #>>
HOLogic.mk_disj o swap)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Tue Sep 28 12:35:43 2021 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Wed Sep 29 09:58:19 2021 +0200
@@ -78,10 +78,10 @@
fun is_rec_eq lhs = Term.exists_subterm (curry (op =) (head_of lhs))
-fun is_rec_def (\<^const>\<open>Trueprop\<close> $ t) = is_rec_def t
- | is_rec_def (\<^const>\<open>Pure.imp\<close> $ _ $ t2) = is_rec_def t2
- | is_rec_def (Const (\<^const_name>\<open>Pure.eq\<close>, _) $ t1 $ t2) = is_rec_eq t1 t2
- | is_rec_def (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ t1 $ t2) = is_rec_eq t1 t2
+fun is_rec_def \<^Const_>\<open>Trueprop for t\<close> = is_rec_def t
+ | is_rec_def \<^Const_>\<open>Pure.imp for _ t2\<close> = is_rec_def t2
+ | is_rec_def \<^Const_>\<open>Pure.eq _ for t1 t2\<close> = is_rec_eq t1 t2
+ | is_rec_def \<^Const_>\<open>HOL.eq _ for t1 t2\<close> = is_rec_eq t1 t2
| is_rec_def _ = false
fun is_assum assms th = exists (fn ct => Thm.prop_of th aconv Thm.term_of ct) assms
@@ -249,8 +249,8 @@
else
Interesting
- fun interest_of_prop _ (\<^const>\<open>Trueprop\<close> $ t) = interest_of_bool t
- | interest_of_prop Ts (\<^const>\<open>Pure.imp\<close> $ t $ u) =
+ fun interest_of_prop _ \<^Const_>\<open>Trueprop for t\<close> = interest_of_bool t
+ | interest_of_prop Ts \<^Const_>\<open>Pure.imp for t u\<close> =
combine_interests (interest_of_prop Ts t) (interest_of_prop Ts u)
| interest_of_prop Ts (Const (\<^const_name>\<open>Pure.all\<close>, _) $ Abs (_, T, t)) =
if type_has_top_sort T then Deal_Breaker else interest_of_prop (T :: Ts) t
@@ -331,9 +331,9 @@
end
end
-fun normalize_eq (\<^const>\<open>Trueprop\<close> $ (t as (t0 as Const (\<^const_name>\<open>HOL.eq\<close>, _)) $ t1 $ t2)) =
+fun normalize_eq (\<^Const_>\<open>Trueprop\<close> $ (t as (t0 as Const (\<^const_name>\<open>HOL.eq\<close>, _)) $ t1 $ t2)) =
if is_less_equal (Term_Ord.fast_term_ord (t1, t2)) then t else t0 $ t2 $ t1
- | normalize_eq (\<^const>\<open>Trueprop\<close> $ (t as \<^const>\<open>Not\<close>
+ | normalize_eq (\<^Const_>\<open>Trueprop\<close> $ (t as \<^Const_>\<open>Not\<close>
$ ((t0 as Const (\<^const_name>\<open>HOL.eq\<close>, _)) $ t1 $ t2))) =
if is_less_equal (Term_Ord.fast_term_ord (t1, t2)) then t else HOLogic.mk_not (t0 $ t2 $ t1)
| normalize_eq (Const (\<^const_name>\<open>Pure.eq\<close>, Type (_, [T, _])) $ t1 $ t2) =
@@ -376,7 +376,7 @@
fun struct_induct_rule_on th =
(case Logic.strip_horn (Thm.prop_of th) of
- (prems, \<^const>\<open>Trueprop\<close> $ ((p as Var ((p_name, 0), _)) $ (a as Var (_, ind_T)))) =>
+ (prems, \<^Const_>\<open>Trueprop\<close> $ ((p as Var ((p_name, 0), _)) $ (a as Var (_, ind_T)))) =>
if not (is_TVar ind_T) andalso length prems > 1 andalso
exists (exists_subterm (curry (op aconv) p)) prems andalso
not (exists (exists_subterm (curry (op aconv) a)) prems) then
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML Tue Sep 28 12:35:43 2021 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML Wed Sep 29 09:58:19 2021 +0200
@@ -178,18 +178,18 @@
and do_formula t =
(case t of
Const (\<^const_name>\<open>Pure.all\<close>, _) $ Abs (_, _, t') => do_formula t'
- | \<^const>\<open>Pure.imp\<close> $ t1 $ t2 => do_formula t1 #> do_formula t2
+ | \<^Const_>\<open>Pure.imp for t1 t2\<close> => do_formula t1 #> do_formula t2
| Const (\<^const_name>\<open>Pure.eq\<close>, Type (_, [T, _])) $ t1 $ t2 =>
do_term_or_formula false T t1 #> do_term_or_formula true T t2
- | \<^const>\<open>Trueprop\<close> $ t1 => do_formula t1
- | \<^const>\<open>False\<close> => I
- | \<^const>\<open>True\<close> => I
- | \<^const>\<open>Not\<close> $ t1 => do_formula t1
+ | \<^Const_>\<open>Trueprop for t1\<close> => do_formula t1
+ | \<^Const_>\<open>False\<close> => I
+ | \<^Const_>\<open>True\<close> => I
+ | \<^Const_>\<open>Not for t1\<close> => do_formula t1
| Const (\<^const_name>\<open>All\<close>, _) $ Abs (_, _, t') => do_formula t'
| Const (\<^const_name>\<open>Ex\<close>, _) $ Abs (_, _, t') => do_formula t'
- | \<^const>\<open>HOL.conj\<close> $ t1 $ t2 => do_formula t1 #> do_formula t2
- | \<^const>\<open>HOL.disj\<close> $ t1 $ t2 => do_formula t1 #> do_formula t2
- | \<^const>\<open>HOL.implies\<close> $ t1 $ t2 => do_formula t1 #> do_formula t2
+ | \<^Const_>\<open>conj for t1 t2\<close> => do_formula t1 #> do_formula t2
+ | \<^Const_>\<open>disj for t1 t2\<close> => do_formula t1 #> do_formula t2
+ | \<^Const_>\<open>implies for t1 t2\<close> => do_formula t1 #> do_formula t2
| Const (\<^const_name>\<open>HOL.eq\<close>, Type (_, [T, _])) $ t1 $ t2 =>
do_term_or_formula false T t1 #> do_term_or_formula true T t2
| Const (\<^const_name>\<open>If\<close>, Type (_, [_, Type (_, [T, _])])) $ t1 $ t2 $ t3 =>
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Tue Sep 28 12:35:43 2021 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Wed Sep 29 09:58:19 2021 +0200
@@ -76,17 +76,17 @@
fun do_equals t1 t2 = is_bad_equal t1 t2 orelse is_bad_equal t2 t1
fun do_formula pos t =
(case (pos, t) of
- (_, \<^const>\<open>Trueprop\<close> $ t1) => do_formula pos t1
+ (_, \<^Const_>\<open>Trueprop for t1\<close>) => do_formula pos t1
| (true, Const (\<^const_name>\<open>Pure.all\<close>, _) $ Abs (_, _, t')) => do_formula pos t'
| (true, Const (\<^const_name>\<open>All\<close>, _) $ Abs (_, _, t')) => do_formula pos t'
| (false, Const (\<^const_name>\<open>Ex\<close>, _) $ Abs (_, _, t')) => do_formula pos t'
- | (_, \<^const>\<open>Pure.imp\<close> $ t1 $ t2) =>
+ | (_, \<^Const_>\<open>Pure.imp for t1 t2\<close>) =>
do_formula (not pos) t1 andalso (t2 = \<^prop>\<open>False\<close> orelse do_formula pos t2)
- | (_, \<^const>\<open>HOL.implies\<close> $ t1 $ t2) =>
- do_formula (not pos) t1 andalso (t2 = \<^const>\<open>False\<close> orelse do_formula pos t2)
- | (_, \<^const>\<open>Not\<close> $ t1) => do_formula (not pos) t1
- | (true, \<^const>\<open>HOL.disj\<close> $ t1 $ t2) => forall (do_formula pos) [t1, t2]
- | (false, \<^const>\<open>HOL.conj\<close> $ t1 $ t2) => forall (do_formula pos) [t1, t2]
+ | (_, \<^Const_>\<open>implies for t1 t2\<close>) =>
+ do_formula (not pos) t1 andalso (t2 = \<^Const>\<open>False\<close> orelse do_formula pos t2)
+ | (_, \<^Const_>\<open>Not for t1\<close>) => do_formula (not pos) t1
+ | (true, \<^Const_>\<open>disj for t1 t2\<close>) => forall (do_formula pos) [t1, t2]
+ | (false, \<^Const_>\<open>conj for t1 t2\<close>) => forall (do_formula pos) [t1, t2]
| (true, Const (\<^const_name>\<open>HOL.eq\<close>, _) $ t1 $ t2) => do_equals t1 t2
| (true, Const (\<^const_name>\<open>Pure.eq\<close>, _) $ t1 $ t2) => do_equals t1 t2
| _ => false)
--- a/src/HOL/Tools/Transfer/transfer.ML Tue Sep 28 12:35:43 2021 +0200
+++ b/src/HOL/Tools/Transfer/transfer.ML Wed Sep 29 09:58:19 2021 +0200
@@ -550,8 +550,8 @@
Symtab.join (K or3) (tab1, tab2)
end
val tab = go [] p (t, u) Symtab.empty
- fun f (a, (true, false, false)) = SOME (a, \<^const>\<open>implies\<close>)
- | f (a, (false, true, false)) = SOME (a, \<^const>\<open>rev_implies\<close>)
+ fun f (a, (true, false, false)) = SOME (a, \<^Const>\<open>implies\<close>)
+ | f (a, (false, true, false)) = SOME (a, \<^Const>\<open>rev_implies\<close>)
| f (a, (true, true, _)) = SOME (a, HOLogic.eq_const HOLogic.boolT)
| f _ = NONE
in
--- a/src/HOL/Tools/etc/options Tue Sep 28 12:35:43 2021 +0200
+++ b/src/HOL/Tools/etc/options Wed Sep 29 09:58:19 2021 +0200
@@ -26,7 +26,7 @@
section "Miscellaneous Tools"
-public option sledgehammer_provers : string = "cvc4 z3 spass e remote_vampire"
+public option sledgehammer_provers : string = "cvc4 z3 spass e vampire"
-- "provers for Sledgehammer (separated by blanks)"
public option sledgehammer_timeout : int = 30
--- a/src/HOL/Tools/record.ML Tue Sep 28 12:35:43 2021 +0200
+++ b/src/HOL/Tools/record.ML Wed Sep 29 09:58:19 2021 +0200
@@ -1808,8 +1808,8 @@
distinct_discsss = [], exhaust_discs = [], exhaust_sels = [], collapses = [], expands = [],
split_sels = [], split_sel_asms = [], case_eq_ifs = []};
-fun lhs_of_equation (Const (\<^const_name>\<open>Pure.eq\<close>, _) $ t $ _) = t
- | lhs_of_equation (\<^const>\<open>Trueprop\<close> $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ t $ _)) = t;
+fun lhs_of_equation \<^Const_>\<open>Pure.eq _ for t _\<close> = t
+ | lhs_of_equation \<^Const_>\<open>Trueprop for \<^Const_>\<open>HOL.eq _ for t _\<close>\<close> = t;
fun add_spec_rule rule =
let val head = head_of (lhs_of_equation (Thm.prop_of rule))
--- a/src/HOL/Tools/set_comprehension_pointfree.ML Tue Sep 28 12:35:43 2021 +0200
+++ b/src/HOL/Tools/set_comprehension_pointfree.ML Wed Sep 29 09:58:19 2021 +0200
@@ -250,8 +250,8 @@
(map Pattern pats, Un (fm1', fm2'))
end;
-fun mk_formula vs (\<^const>\<open>HOL.conj\<close> $ t1 $ t2) = merge_inter vs (mk_formula vs t1) (mk_formula vs t2)
- | mk_formula vs (\<^const>\<open>HOL.disj\<close> $ t1 $ t2) = merge_union vs (mk_formula vs t1) (mk_formula vs t2)
+fun mk_formula vs \<^Const_>\<open>conj for t1 t2\<close> = merge_inter vs (mk_formula vs t1) (mk_formula vs t2)
+ | mk_formula vs \<^Const_>\<open>disj for t1 t2\<close> = merge_union vs (mk_formula vs t1) (mk_formula vs t2)
| mk_formula vs t = apfst single (mk_atom vs t)
fun strip_Int (Int (fm1, fm2)) = fm1 :: (strip_Int fm2)
--- a/src/HOL/Transitive_Closure.thy Tue Sep 28 12:35:43 2021 +0200
+++ b/src/HOL/Transitive_Closure.thy Wed Sep 29 09:58:19 2021 +0200
@@ -1289,7 +1289,7 @@
fun decomp \<^Const_>\<open>Trueprop for t\<close> =
let
- fun dec \<^Const_>\<open>Set.member _ for \<open>\<^Const_>\<open>Pair _ _ for a b\<close>\<close> rel\<close> =
+ fun dec \<^Const_>\<open>Set.member _ for \<^Const_>\<open>Pair _ _ for a b\<close> rel\<close> =
let
fun decr \<^Const_>\<open>rtrancl _ for r\<close> = (r,"r*")
| decr \<^Const_>\<open>trancl _ for r\<close> = (r,"r+")
--- a/src/HOL/Typerep.thy Tue Sep 28 12:35:43 2021 +0200
+++ b/src/HOL/Typerep.thy Wed Sep 29 09:58:19 2021 +0200
@@ -32,7 +32,7 @@
typed_print_translation \<open>
let
- fun typerep_tr' ctxt (*"typerep"*) \<^Type>\<open>fun \<open>\<^Type>\<open>itself T\<close>\<close> _\<close>
+ fun typerep_tr' ctxt (*"typerep"*) \<^Type>\<open>fun \<^Type>\<open>itself T\<close> _\<close>
(Const (\<^const_syntax>\<open>Pure.type\<close>, _) :: ts) =
Term.list_comb
(Syntax.const \<^syntax_const>\<open>_TYPEREP\<close> $ Syntax_Phases.term_of_typ ctxt T, ts)
--- a/src/Pure/Admin/isabelle_cronjob.scala Tue Sep 28 12:35:43 2021 +0200
+++ b/src/Pure/Admin/isabelle_cronjob.scala Wed Sep 29 09:58:19 2021 +0200
@@ -313,6 +313,14 @@
val remote_builds1: List[List[Remote_Build]] =
{
List(
+ List(Remote_Build("Linux A", "augsburg1",
+ options = "-m32 -B -M1x2,2,4" +
+ " -e ISABELLE_OCAML=ocaml -e ISABELLE_OCAMLC=ocamlc -e ISABELLE_OCAMLFIND=ocamlfind -e ISABELLE_OCAML_SETUP=true" +
+ " -e ISABELLE_GHC_SETUP=true" +
+ " -e ISABELLE_MLTON=mlton" +
+ " -e ISABELLE_SMLNJ=sml" +
+ " -e ISABELLE_SWIPL=swipl",
+ self_update = true, args = "-a -d '~~/src/Benchmarks'")),
List(Remote_Build("Linux B", "lxbroy10", historic = true, history = 90,
options = "-m32 -B -M1x4,2,4,6", args = "-N -g timing")),
List(Remote_Build("macOS 10.13 High Sierra", "lapbroy68",
--- a/src/Pure/General/antiquote.ML Tue Sep 28 12:35:43 2021 +0200
+++ b/src/Pure/General/antiquote.ML Wed Sep 29 09:58:19 2021 +0200
@@ -7,6 +7,8 @@
signature ANTIQUOTE =
sig
type control = {range: Position.range, name: string * Position.T, body: Symbol_Pos.T list}
+ val no_control: control
+ val control_symbols: control -> Symbol_Pos.T list
type antiq = {start: Position.T, stop: Position.T, range: Position.range, body: Symbol_Pos.T list}
datatype 'a antiquote = Text of 'a | Control of control | Antiq of antiq
val is_text: 'a antiquote -> bool
@@ -17,7 +19,8 @@
val split_lines: text_antiquote list -> text_antiquote list list
val antiq_reports: 'a antiquote list -> Position.report list
val update_reports: bool -> Position.T -> string list -> Position.report_text list
- val scan_control: control scanner
+ val err_prefix: string
+ val scan_control: string -> control scanner
val scan_antiq: antiq scanner
val scan_antiquote: text_antiquote scanner
val scan_antiquote_comments: text_antiquote scanner
@@ -31,6 +34,10 @@
(* datatype antiquote *)
type control = {range: Position.range, name: string * Position.T, body: Symbol_Pos.T list};
+val no_control = {range = Position.no_range, name = ("", Position.none), body = []};
+fun control_symbols ({name = (name, pos), body, ...}: control) =
+ (Symbol.encode (Symbol.Control name), pos) :: body;
+
type antiq = {start: Position.T, stop: Position.T, range: Position.range, body: Symbol_Pos.T list};
datatype 'a antiquote = Text of 'a | Control of control | Antiq of antiq;
@@ -112,9 +119,9 @@
open Basic_Symbol_Pos;
-local
+val err_prefix = "Antiquotation lexical error: ";
-val err_prefix = "Antiquotation lexical error: ";
+local
val scan_nl = Scan.one (fn (s, _) => s = "\n") >> single;
val scan_nl_opt = Scan.optional scan_nl [];
@@ -148,9 +155,9 @@
in
-val scan_control =
+fun scan_control err =
Scan.option (Scan.one (Symbol.is_control o Symbol_Pos.symbol)) --
- Symbol_Pos.scan_cartouche err_prefix >>
+ Symbol_Pos.scan_cartouche err >>
(fn (opt_control, body) =>
let
val (name, range) =
@@ -173,10 +180,10 @@
body = body});
val scan_antiquote =
- scan_text >> Text || scan_control >> Control || scan_antiq >> Antiq;
+ scan_text >> Text || scan_control err_prefix >> Control || scan_antiq >> Antiq;
val scan_antiquote_comments =
- scan_text_comments >> Text || scan_control >> Control || scan_antiq >> Antiq;
+ scan_text_comments >> Text || scan_control err_prefix >> Control || scan_antiq >> Antiq;
end;
--- a/src/Pure/General/scan.scala Tue Sep 28 12:35:43 2021 +0200
+++ b/src/Pure/General/scan.scala Wed Sep 29 09:58:19 2021 +0200
@@ -290,6 +290,13 @@
}
+ /* control cartouches */
+
+ val control_symbol: Parser[String] = one(Symbol.is_control)
+
+ val control_cartouche: Parser[String] = control_symbol ~ cartouche ^^ { case a ~ b => a + b }
+
+
/* keyword */
def literal(lexicon: Lexicon): Parser[String] = new Parser[String]
--- a/src/Pure/Isar/parse.ML Tue Sep 28 12:35:43 2021 +0200
+++ b/src/Pure/Isar/parse.ML Wed Sep 29 09:58:19 2021 +0200
@@ -32,6 +32,7 @@
val alt_string: string parser
val verbatim: string parser
val cartouche: string parser
+ val control: Antiquote.control parser
val eof: string parser
val command_name: string -> string parser
val keyword_with: (string -> bool) -> string parser
@@ -195,6 +196,7 @@
val alt_string = kind Token.Alt_String;
val verbatim = kind Token.Verbatim;
val cartouche = kind Token.Cartouche;
+val control = token (kind Token.control_kind) >> (the o Token.get_control);
val eof = kind Token.EOF;
fun command_name x =
--- a/src/Pure/Isar/token.ML Tue Sep 28 12:35:43 2021 +0200
+++ b/src/Pure/Isar/token.ML Wed Sep 29 09:58:19 2021 +0200
@@ -11,9 +11,12 @@
Command | Keyword | Ident | Long_Ident | Sym_Ident | Var | Type_Ident | Type_Var | Nat |
Float | Space |
(*delimited content*)
- String | Alt_String | Verbatim | Cartouche | Comment of Comment.kind option |
+ String | Alt_String | Verbatim | Cartouche |
+ Control of Antiquote.control |
+ Comment of Comment.kind option |
(*special content*)
Error of string | EOF
+ val control_kind: kind
val str_of_kind: kind -> string
type file = {src_path: Path.T, lines: string list, digest: SHA1.digest, pos: Position.T}
type T
@@ -37,6 +40,7 @@
val stopper: T Scan.stopper
val kind_of: T -> kind
val is_kind: kind -> T -> bool
+ val get_control: T -> Antiquote.control option
val is_command: T -> bool
val keyword_with: (string -> bool) -> T -> bool
val is_command_modifier: T -> bool
@@ -118,10 +122,20 @@
Command | Keyword | Ident | Long_Ident | Sym_Ident | Var | Type_Ident | Type_Var | Nat |
Float | Space |
(*delimited content*)
- String | Alt_String | Verbatim | Cartouche | Comment of Comment.kind option |
+ String | Alt_String | Verbatim | Cartouche |
+ Control of Antiquote.control |
+ Comment of Comment.kind option |
(*special content*)
Error of string | EOF;
+val control_kind = Control Antiquote.no_control;
+
+fun equiv_kind kind kind' =
+ (case (kind, kind') of
+ (Control _, Control _) => true
+ | (Error _, Error _) => true
+ | _ => kind = kind');
+
val str_of_kind =
fn Command => "command"
| Keyword => "keyword"
@@ -138,6 +152,7 @@
| Alt_String => "back-quoted string"
| Verbatim => "verbatim text"
| Cartouche => "text cartouche"
+ | Control _ => "control cartouche"
| Comment NONE => "informal comment"
| Comment (SOME _) => "formal comment"
| Error _ => "bad input"
@@ -152,6 +167,7 @@
| Alt_String => true
| Verbatim => true
| Cartouche => true
+ | Control _ => true
| Comment _ => true
| _ => false);
@@ -214,7 +230,10 @@
(* kind of token *)
fun kind_of (Token (_, (k, _), _)) = k;
-fun is_kind k (Token (_, (k', _), _)) = k = k';
+fun is_kind k (Token (_, (k', _), _)) = equiv_kind k k';
+
+fun get_control tok =
+ (case kind_of tok of Control control => SOME control | _ => NONE);
val is_command = is_kind Command;
@@ -304,6 +323,7 @@
| Alt_String => (Markup.alt_string, "")
| Verbatim => (Markup.verbatim, "")
| Cartouche => (Markup.cartouche, "")
+ | Control _ => (Markup.cartouche, "")
| Comment _ => (Markup.comment, "")
| Error msg => (Markup.bad (), msg)
| _ => (Markup.empty, "");
@@ -354,6 +374,7 @@
| Alt_String => Symbol_Pos.quote_string_bq x
| Verbatim => enclose "{*" "*}" x
| Cartouche => cartouche x
+ | Control control => Symbol_Pos.content (Antiquote.control_symbols control)
| Comment NONE => enclose "(*" "*)" x
| EOF => ""
| _ => x);
@@ -646,9 +667,11 @@
(Symbol_Pos.scan_string_qq err_prefix >> token_range String ||
Symbol_Pos.scan_string_bq err_prefix >> token_range Alt_String ||
scan_verbatim >> token_range Verbatim ||
- scan_cartouche >> token_range Cartouche ||
scan_comment >> token_range (Comment NONE) ||
Comment.scan_outer >> (fn (k, ss) => token (Comment (SOME k)) ss) ||
+ scan_cartouche >> token_range Cartouche ||
+ Antiquote.scan_control err_prefix >> (fn control =>
+ token (Control control) (Antiquote.control_symbols control)) ||
scan_space >> token Space ||
(Scan.max token_leq
(Scan.max token_leq
--- a/src/Pure/Isar/token.scala Tue Sep 28 12:35:43 2021 +0200
+++ b/src/Pure/Isar/token.scala Wed Sep 29 09:58:19 2021 +0200
@@ -34,6 +34,7 @@
val ALT_STRING = Value("back-quoted string")
val VERBATIM = Value("verbatim text")
val CARTOUCHE = Value("text cartouche")
+ val CONTROL = Value("control cartouche")
val INFORMAL_COMMENT = Value("informal comment")
val FORMAL_COMMENT = Value("formal comment")
/*special content*/
@@ -53,11 +54,12 @@
val string = quoted("\"") ^^ (x => Token(Token.Kind.STRING, x))
val alt_string = quoted("`") ^^ (x => Token(Token.Kind.ALT_STRING, x))
val verb = verbatim ^^ (x => Token(Token.Kind.VERBATIM, x))
- val cart = cartouche ^^ (x => Token(Token.Kind.CARTOUCHE, x))
val cmt = comment ^^ (x => Token(Token.Kind.INFORMAL_COMMENT, x))
val formal_cmt = comment_cartouche ^^ (x => Token(Token.Kind.FORMAL_COMMENT, x))
+ val cart = cartouche ^^ (x => Token(Token.Kind.CARTOUCHE, x))
+ val ctrl = control_cartouche ^^ (x => Token(Token.Kind.CONTROL, x))
- string | (alt_string | (verb | (cart | (cmt | formal_cmt))))
+ string | (alt_string | (verb | (cmt | (formal_cmt | (cart | ctrl)))))
}
private def other_token(keywords: Keyword.Keywords): Parser[Token] =
--- a/src/Pure/ML/ml_antiquotations1.ML Tue Sep 28 12:35:43 2021 +0200
+++ b/src/Pure/ML/ml_antiquotations1.ML Wed Sep 29 09:58:19 2021 +0200
@@ -234,27 +234,35 @@
| NONE => error ("Bad input" ^ Position.here (Input.pos_of input)))
end;
-fun ml_sources ctxt srcs =
+fun ml_args ctxt args =
let
- val (decls, ctxt') = fold_map (ML_Context.expand_antiquotes o ML_Lex.read_source) srcs ctxt;
+ val (decls, ctxt') = fold_map (ML_Context.expand_antiquotes) args ctxt;
fun decl' ctxt'' = map (fn decl => decl ctxt'') decls;
in (decl', ctxt') end
val parse_name = Parse.input Parse.name;
-val parse_args = Scan.repeat (Parse.input Parse.underscore || Parse.embedded_input);
+
+val parse_arg =
+ Parse.input Parse.underscore >> ML_Lex.read_source ||
+ Parse.embedded_input >> ML_Lex.read_source ||
+ Parse.control >> (ML_Lex.read_symbols o Antiquote.control_symbols);
+
+val parse_args = Scan.repeat parse_arg;
val parse_for_args =
Scan.optional ((Parse.position (Parse.$$$ "for") >> #2) -- Parse.!!! parse_args)
(Position.none, []);
fun parse_body b =
- if b then Parse.$$$ "=>" |-- Parse.!!! Parse.embedded_input >> single
+ if b then Parse.$$$ "=>" |-- Parse.!!! Parse.embedded_input >> (ML_Lex.read_source #> single)
else Scan.succeed [];
-fun is_dummy s = Input.string_of s = "_";
+fun is_dummy [Antiquote.Text tok] = ML_Lex.content_of tok = "_"
+ | is_dummy _ = false;
val ml = ML_Lex.tokenize_no_range;
val ml_range = ML_Lex.tokenize_range;
val ml_dummy = ml "_";
+fun ml_enclose range x = ml "(" @ x @ ml_range range ")";
fun ml_parens x = ml "(" @ x @ ml ")";
fun ml_bracks x = ml "[" @ x @ ml "]";
fun ml_commas xs = flat (separate (ml ", ") xs);
@@ -279,18 +287,20 @@
error ("Type constructor " ^ quote (Proof_Context.markup_type ctxt c) ^
" takes " ^ string_of_int n ^ " argument(s)" ^ Position.here pos);
- val (decls1, ctxt1) = ml_sources ctxt type_args;
- val (decls2, ctxt2) = (ml_sources ctxt1) fn_body;
+ val (decls1, ctxt1) = ml_args ctxt type_args;
+ val (decls2, ctxt2) = ml_args ctxt1 fn_body;
fun decl' ctxt' =
let
val (ml_args_env, ml_args_body) = split_list (decls1 ctxt');
val (ml_fn_env, ml_fn_body) = split_list (decls2 ctxt');
- val ml1 = ml_parens (ml "Term.Type " @ ml_pair (ml_string c, ml_list ml_args_body));
+ val ml1 =
+ ml_enclose range (ml "Term.Type " @ ml_pair (ml_string c, ml_list ml_args_body));
val ml2 =
if function then
- ml "(" @ ml_range range "fn " @ ml1 @ ml "=> " @ flat ml_fn_body @
- ml "| T => " @ ml_range range "raise" @
- ml " Term.TYPE (" @ ml_string ("Type_fn " ^ quote c) @ ml ", [T], []))"
+ ml_enclose range
+ (ml_range range "fn " @ ml1 @ ml "=> " @ flat ml_fn_body @
+ ml "| T => " @ ml_range range "raise" @
+ ml " Term.TYPE (" @ ml_string ("Type_fn " ^ quote c) @ ml ", [T], [])")
else ml1;
in (flat (ml_args_env @ ml_fn_env), ml2) end;
in (decl', ctxt2) end);
@@ -321,11 +331,11 @@
length type_args <> n andalso err (" takes " ^ string_of_int n ^ " type argument(s)");
val _ =
length term_args > m andalso Term.is_Type (Term.body_type T) andalso
- err (" cannot have more than " ^ string_of_int m ^ " type argument(s)");
+ err (" cannot have more than " ^ string_of_int m ^ " argument(s)");
- val (decls1, ctxt1) = ml_sources ctxt type_args;
- val (decls2, ctxt2) = ml_sources ctxt1 term_args;
- val (decls3, ctxt3) = ml_sources ctxt2 fn_body;
+ val (decls1, ctxt1) = ml_args ctxt type_args;
+ val (decls2, ctxt2) = ml_args ctxt1 term_args;
+ val (decls3, ctxt3) = ml_args ctxt2 fn_body;
fun decl' ctxt' =
let
val (ml_args_env1, ml_args_body1) = split_list (decls1 ctxt');
@@ -351,12 +361,13 @@
| ml_app (u :: us) = ml "Term.$ " @ ml_pair (ml_app us, u);
val ml_env = flat (ml_args_env1 @ ml_args_env2 @ ml_fn_env);
- val ml1 = ml_parens (ml_app (rev ml_args_body2));
+ val ml1 = ml_enclose range (ml_app (rev ml_args_body2));
val ml2 =
if function then
- ml "(" @ ml_range range "fn " @ ml1 @ ml "=> " @ flat ml_fn_body @
- ml "| t => " @ ml_range range "raise" @
- ml " Term.TERM (" @ ml_string ("Const_fn " ^ quote c) @ ml ", [t]))"
+ ml_enclose range
+ (ml_range range "fn " @ ml1 @ ml "=> " @ flat ml_fn_body @
+ ml "| t => " @ ml_range range "raise" @
+ ml " Term.TERM (" @ ml_string ("Const_fn " ^ quote c) @ ml ", [t])")
else ml1;
in (ml_env, ml2) end;
in (decl', ctxt3) end);
--- a/src/Pure/ML/ml_lex.ML Tue Sep 28 12:35:43 2021 +0200
+++ b/src/Pure/ML/ml_lex.ML Wed Sep 29 09:58:19 2021 +0200
@@ -36,6 +36,7 @@
token Antiquote.antiquote Symbol_Pos.scanner -> Input.source -> token Antiquote.antiquote list
val read_source: Input.source -> token Antiquote.antiquote list
val read_source_sml: Input.source -> token Antiquote.antiquote list
+ val read_symbols: Symbol_Pos.T list -> token Antiquote.antiquote list
val read_symbols_sml: Symbol_Pos.T list -> token Antiquote.antiquote list
end;
@@ -315,7 +316,7 @@
val scan_ml_antiq =
Comment.scan_inner >> (fn (kind, ss) => Antiquote.Text (token (Comment (SOME kind)) ss)) ||
- Antiquote.scan_control >> Antiquote.Control ||
+ Antiquote.scan_control Antiquote.err_prefix >> Antiquote.Control ||
Antiquote.scan_antiq >> Antiquote.Antiq ||
scan_rat_antiq >> Antiquote.Antiq ||
scan_sml_antiq;
@@ -389,6 +390,7 @@
read_source' {language = Markup.language_SML, symbols = false, opaque_warning = false}
scan_sml_antiq;
+val read_symbols = reader {opaque_warning = true} scan_ml_antiq;
val read_symbols_sml = reader {opaque_warning = false} scan_sml_antiq;
end;
--- a/src/Pure/Thy/document_output.ML Tue Sep 28 12:35:43 2021 +0200
+++ b/src/Pure/Thy/document_output.ML Wed Sep 29 09:58:19 2021 +0200
@@ -156,6 +156,7 @@
| Token.Alt_String => output false "{\\isacharbackquoteopen}" "{\\isacharbackquoteclose}"
| Token.Verbatim => output true "{\\isacharverbatimopen}" "{\\isacharverbatimclose}"
| Token.Cartouche => output false "{\\isacartoucheopen}" "{\\isacartoucheclose}"
+ | Token.Control control => output_body ctxt false "" "" (Antiquote.control_symbols control)
| _ => output false "" "")
end handle ERROR msg => error (msg ^ Position.here (Token.pos_of tok));
--- a/src/Pure/Tools/generated_files.ML Tue Sep 28 12:35:43 2021 +0200
+++ b/src/Pure/Tools/generated_files.ML Wed Sep 29 09:58:19 2021 +0200
@@ -201,7 +201,7 @@
end;
val scan_antiq =
- Antiquote.scan_control >> Antiquote.Control ||
+ Antiquote.scan_control Antiquote.err_prefix >> Antiquote.Control ||
Scan.one (Symbol.not_eof o Symbol_Pos.symbol) >> (Antiquote.Text o Symbol_Pos.symbol);
fun read_source ctxt (file_type: file_type) source =
--- a/src/Tools/Code/code_runtime.ML Tue Sep 28 12:35:43 2021 +0200
+++ b/src/Tools/Code/code_runtime.ML Wed Sep 29 09:58:19 2021 +0200
@@ -653,7 +653,7 @@
fun ml_computation_check_antiq raw_spec ctxt =
let
- val cTs = insert (op =) (dest_Const \<^const>\<open>holds\<close>) (prep_spec ctxt raw_spec);
+ val cTs = insert (op =) (dest_Const \<^Const>\<open>holds\<close>) (prep_spec ctxt raw_spec);
in (print_computation_check ctxt, register_computation cTs \<^typ>\<open>prop\<close> ctxt) end;
end; (*local*)
--- a/src/Tools/jEdit/src/jedit_rendering.scala Tue Sep 28 12:35:43 2021 +0200
+++ b/src/Tools/jEdit/src/jedit_rendering.scala Wed Sep 29 09:58:19 2021 +0200
@@ -72,6 +72,7 @@
Token.Kind.ALT_STRING -> LITERAL2,
Token.Kind.VERBATIM -> COMMENT3,
Token.Kind.CARTOUCHE -> COMMENT3,
+ Token.Kind.CONTROL -> COMMENT3,
Token.Kind.INFORMAL_COMMENT -> COMMENT1,
Token.Kind.FORMAL_COMMENT -> COMMENT1,
Token.Kind.ERROR -> INVALID
--- a/src/ZF/Tools/inductive_package.ML Tue Sep 28 12:35:43 2021 +0200
+++ b/src/ZF/Tools/inductive_package.ML Wed Sep 29 09:58:19 2021 +0200
@@ -298,7 +298,7 @@
(*Used to make induction rules;
ind_alist = [(rec_tm1,pred1),...] associates predicates with rec ops
prem is a premise of an intr rule*)
- fun add_induct_prem ind_alist (prem as \<^Const_>\<open>Trueprop for \<open>\<^Const_>\<open>mem for t X\<close>\<close>\<close>, iprems) =
+ fun add_induct_prem ind_alist (prem as \<^Const_>\<open>Trueprop for \<^Const_>\<open>mem for t X\<close>\<close>, iprems) =
(case AList.lookup (op aconv) ind_alist X of
SOME pred => prem :: \<^make_judgment> (pred $ t) :: iprems
| NONE => (*possibly membership in M(rec_tm), for M monotone*)
@@ -391,7 +391,7 @@
elem_factors ---> \<^Type>\<open>o\<close>)
val qconcl =
fold_rev (FOLogic.mk_all o Term.dest_Free) elem_frees
- \<^Const>\<open>imp for \<open>\<^Const>\<open>mem for elem_tuple rec_tm\<close>\<close> \<open>list_comb (pfree, elem_frees)\<close>\<close>
+ \<^Const>\<open>imp for \<^Const>\<open>mem for elem_tuple rec_tm\<close> \<open>list_comb (pfree, elem_frees)\<close>\<close>
in (CP.ap_split elem_type \<^Type>\<open>o\<close> pfree,
qconcl)
end;
@@ -400,7 +400,7 @@
(*Used to form simultaneous induction lemma*)
fun mk_rec_imp (rec_tm,pred) =
- \<^Const>\<open>imp for \<open>\<^Const>\<open>mem for \<open>Bound 0\<close> rec_tm\<close>\<close> \<open>pred $ Bound 0\<close>\<close>;
+ \<^Const>\<open>imp for \<^Const>\<open>mem for \<open>Bound 0\<close> rec_tm\<close> \<open>pred $ Bound 0\<close>\<close>;
(*To instantiate the main induction rule*)
val induct_concl =
--- a/src/ZF/Tools/typechk.ML Tue Sep 28 12:35:43 2021 +0200
+++ b/src/ZF/Tools/typechk.ML Wed Sep 29 09:58:19 2021 +0200
@@ -76,7 +76,7 @@
if length rls <= maxr then resolve_tac ctxt rls i else no_tac
end);
-fun is_rigid_elem \<^Const_>\<open>Trueprop for \<open>\<^Const_>\<open>mem for a _\<close>\<close>\<close> = not (is_Var (head_of a))
+fun is_rigid_elem \<^Const_>\<open>Trueprop for \<^Const_>\<open>mem for a _\<close>\<close> = not (is_Var (head_of a))
| is_rigid_elem _ = false;
(*Try solving a:A by assumption provided a is rigid!*)
--- a/src/ZF/arith_data.ML Tue Sep 28 12:35:43 2021 +0200
+++ b/src/ZF/arith_data.ML Wed Sep 29 09:58:19 2021 +0200
@@ -48,7 +48,7 @@
(*Use <-> or = depending on the type of t*)
fun mk_eq_iff(t,u) =
if fastype_of t = \<^Type>\<open>i\<close>
- then \<^Const>\<open>IFOL.eq \<open>\<^Type>\<open>i\<close>\<close> for t u\<close>
+ then \<^Const>\<open>IFOL.eq \<^Type>\<open>i\<close> for t u\<close>
else \<^Const>\<open>IFOL.iff for t u\<close>;
(*We remove equality assumptions because they confuse the simplifier and
--- a/src/ZF/ind_syntax.ML Tue Sep 28 12:35:43 2021 +0200
+++ b/src/ZF/ind_syntax.ML Wed Sep 29 09:58:19 2021 +0200
@@ -22,7 +22,7 @@
fun mk_all_imp (A,P) =
let val T = \<^Type>\<open>i\<close> in
\<^Const>\<open>All T for
- \<open>Abs ("v", T, \<^Const>\<open>imp for \<open>\<^Const>\<open>mem for \<open>Bound 0\<close> A\<close>\<close> \<open>Term.betapply (P, Bound 0)\<close>\<close>)\<close>\<close>
+ \<open>Abs ("v", T, \<^Const>\<open>imp for \<^Const>\<open>mem for \<open>Bound 0\<close> A\<close> \<open>Term.betapply (P, Bound 0)\<close>\<close>)\<close>\<close>
end;
fun mk_Collect (a, D, t) = \<^Const>\<open>Collect for D\<close> $ absfree (a, \<^Type>\<open>i\<close>) t;
@@ -37,7 +37,7 @@
(*Return the conclusion of a rule, of the form t:X*)
fun rule_concl rl =
- let val \<^Const_>\<open>Trueprop for \<open>\<^Const_>\<open>mem for t X\<close>\<close>\<close> = Logic.strip_imp_concl rl
+ let val \<^Const_>\<open>Trueprop for \<^Const_>\<open>mem for t X\<close>\<close> = Logic.strip_imp_concl rl
in (t,X) end;
(*As above, but return error message if bad*)