--- a/src/HOL/Tools/ATP/atp_problem_generate.ML Tue Sep 28 22:08:03 2021 +0200
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Tue Sep 28 22:08:51 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 22:08:03 2021 +0200
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Tue Sep 28 22:08:51 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 22:08:03 2021 +0200
+++ b/src/HOL/Tools/ATP/atp_util.ML Tue Sep 28 22:08:51 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/Sledgehammer/sledgehammer_fact.ML Tue Sep 28 22:08:03 2021 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Tue Sep 28 22:08:51 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 22:08:03 2021 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML Tue Sep 28 22:08:51 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 22:08:03 2021 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Tue Sep 28 22:08:51 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)