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