--- a/src/HOL/Decision_Procs/Cooper.thy Sun Mar 16 09:11:17 2025 +0100
+++ b/src/HOL/Decision_Procs/Cooper.thy Sun Mar 16 12:03:47 2025 +0000
@@ -713,11 +713,7 @@
case 2
with one_dvd[of "Inum bs a"] uminus_dvd_conv[where d="1" and t="Inum bs a"]
show ?thesis
- apply (cases "i = 0")
- apply (simp_all add: Let_def)
- apply (cases "i > 0")
- apply simp_all
- done
+ by (cases i rule: linorder_cases) (auto simp: Let_def)
next
case i: 3
consider v where "?sa = C v" | "\<not> (\<exists>v. ?sa = C v)" by blast
@@ -748,11 +744,7 @@
case 2
with one_dvd[of "Inum bs a"] uminus_dvd_conv[where d="1" and t="Inum bs a"]
show ?thesis
- apply (cases "i = 0")
- apply (simp_all add: Let_def)
- apply (cases "i > 0")
- apply simp_all
- done
+ by (cases i rule: linorder_cases) (auto simp: Let_def)
next
case i: 3
consider v where "?sa = C v" | "\<not> (\<exists>v. ?sa = C v)" by blast
@@ -814,10 +806,8 @@
qed (auto simp add: disj_def imp_def iff_def conj_def not_bn)
lemma simpfm_qf: "qfree p \<Longrightarrow> qfree (simpfm p)"
- apply (induct p rule: simpfm.induct)
- apply (auto simp add: disj_qf imp_qf iff_qf conj_qf not_qf Let_def)
- apply (case_tac "simpnum a", auto)+
- done
+proof (induct p rule: simpfm.induct)
+qed (auto simp add: disj_qf imp_qf iff_qf conj_qf not_qf Let_def split: Cooper.num.splits)
subsection \<open>Generic quantifier elimination\<close>
@@ -1076,11 +1066,7 @@
by auto
let ?N = "\<lambda>t. Inum (i # bs) t"
from 5 Ia nb show ?case
- apply (auto simp add: Let_def split_def algebra_simps)
- apply (cases "?r")
- apply auto
- subgoal for nat a b by (cases nat) auto
- done
+ by (cases "?r") (auto split: prod.splits dest: less_imp_Suc_add)
next
case (6 a)
let ?c = "fst (zsplit0 a)"
@@ -1092,11 +1078,7 @@
by auto
let ?N = "\<lambda>t. Inum (i # bs) t"
from 6 Ia nb show ?case
- apply (auto simp add: Let_def split_def algebra_simps)
- apply (cases "?r")
- apply auto
- subgoal for nat a b by (cases nat) auto
- done
+ by (cases "?r") (auto simp: Let_def split_def algebra_simps dest: less_imp_Suc_add)
next
case (7 a)
let ?c = "fst (zsplit0 a)"
@@ -1108,11 +1090,7 @@
by auto
let ?N = "\<lambda>t. Inum (i # bs) t"
from 7 Ia nb show ?case
- apply (auto simp add: Let_def split_def algebra_simps)
- apply (cases "?r")
- apply auto
- subgoal for nat a b by (cases nat) auto
- done
+ by (cases "?r") (auto simp add: Let_def split_def algebra_simps dest: less_imp_Suc_add)
next
case (8 a)
let ?c = "fst (zsplit0 a)"
@@ -1124,11 +1102,7 @@
by auto
let ?N = "\<lambda>t. Inum (i # bs) t"
from 8 Ia nb show ?case
- apply (auto simp add: Let_def split_def algebra_simps)
- apply (cases "?r")
- apply auto
- subgoal for nat a b by (cases nat) auto
- done
+ by (cases "?r") (auto simp add: Let_def split_def algebra_simps dest: less_imp_Suc_add)
next
case (9 a)
let ?c = "fst (zsplit0 a)"
@@ -1140,11 +1114,7 @@
by auto
let ?N = "\<lambda>t. Inum (i # bs) t"
from 9 Ia nb show ?case
- apply (auto simp add: Let_def split_def algebra_simps)
- apply (cases "?r")
- apply auto
- subgoal for nat a b by (cases nat) auto
- done
+ by (cases "?r") (auto simp add: Let_def split_def algebra_simps dest: less_imp_Suc_add)
next
case (10 a)
let ?c = "fst (zsplit0 a)"
@@ -1156,11 +1126,7 @@
by auto
let ?N = "\<lambda>t. Inum (i # bs) t"
from 10 Ia nb show ?case
- apply (auto simp add: Let_def split_def algebra_simps)
- apply (cases "?r")
- apply auto
- subgoal for nat a b by (cases nat) auto
- done
+ by (cases "?r") (auto simp add: Let_def split_def algebra_simps dest: less_imp_Suc_add)
next
case (11 j a)
let ?c = "fst (zsplit0 a)"
@@ -1183,11 +1149,7 @@
next
case 2
with zsplit0_I[OF spl, where x="i" and bs="bs"] show ?thesis
- apply (auto simp add: Let_def split_def algebra_simps)
- apply (cases "?r")
- apply auto
- subgoal for nat a b by (cases nat) auto
- done
+ by (cases "?r") (auto simp add: Let_def split_def algebra_simps dest: less_imp_Suc_add)
next
case 3
then have l: "?L (?l (Dvd j a))"
@@ -1223,11 +1185,7 @@
next
case 2
with zsplit0_I[OF spl, where x="i" and bs="bs"] show ?thesis
- apply (auto simp add: Let_def split_def algebra_simps)
- apply (cases "?r")
- apply auto
- subgoal for nat a b by (cases nat) auto
- done
+ by (cases "?r") (auto simp add: Let_def split_def algebra_simps dest: less_imp_Suc_add)
next
case 3
then have l: "?L (?l (Dvd j a))"
@@ -1403,15 +1361,11 @@
proof (induct p rule: minusinf.induct)
case (1 p q)
then show ?case
- apply auto
- subgoal for z z' by (rule exI [where x = "min z z'"]) simp
- done
+ by (fastforce simp: intro: exI [where x = "min _ _"])
next
case (2 p q)
then show ?case
- apply auto
- subgoal for z z' by (rule exI [where x = "min z z'"]) simp
- done
+ by (fastforce simp: intro: exI [where x = "min _ _"])
next
case (3 c e)
then have c1: "c = 1" and nb: "numbound0 e"
@@ -2002,12 +1956,12 @@
have vb: "?v \<in> set (\<beta> (Eq (CN 0 c e)))"
by simp
from p have "x= - ?e"
- by (simp add: c1) with 3(5)
- show ?case
- using dp apply simp
- apply (erule ballE[where x="1"])
- apply (simp_all add:algebra_simps numbound0_I[OF bn,where b="x"and b'="a"and bs="bs"])
- done
+ by (simp add: c1)
+ moreover have "x \<noteq> - 1 - Inum (a # bs) e + 1"
+ using dp 3 by force
+ ultimately have False
+ using bn decrnum by fastforce
+ then show ?case ..
next
case (4 c e)
then
@@ -2085,6 +2039,7 @@
show "?P (x - d)" by (rule \<beta>[OF lp u d dp nb2 px])
qed
+(*a duplicate in MIR.thy*)
lemma cpmi_eq:
fixes P P1 :: "int \<Rightarrow> bool"
assumes "0 < D"
@@ -2092,24 +2047,22 @@
and "\<forall>x. \<not> (\<exists>j \<in> {1..D}. \<exists>b \<in> B. P (b + j)) \<longrightarrow> P x \<longrightarrow> P (x - D)"
and "\<forall>x k. P1 x = P1 (x - k * D)"
shows "(\<exists>x. P x) \<longleftrightarrow> (\<exists>j \<in> {1..D}. P1 j) \<or> (\<exists>j \<in> {1..D}. \<exists>b \<in> B. P (b + j))"
- apply (insert assms)
- apply (rule iffI)
- prefer 2
- apply (drule minusinfinity)
- apply assumption+
- apply fastforce
- apply clarsimp
- apply (subgoal_tac "\<And>k. 0 \<le> k \<Longrightarrow> \<forall>x. P x \<longrightarrow> P (x - k * D)")
- apply (frule_tac x = x and z=z in decr_lemma)
- apply (subgoal_tac "P1 (x - (\<bar>x - z\<bar> + 1) * D)")
- prefer 2
- apply (subgoal_tac "0 \<le> \<bar>x - z\<bar> + 1")
- prefer 2 apply arith
- apply fastforce
- apply (drule (1) periodic_finite_ex)
- apply blast
- apply (blast dest: decr_mult_lemma)
- done
+ (is "_ = ?R")
+proof
+ assume L: "\<exists>x. P x"
+ show "(\<exists>j\<in>{1..D}. P1 j) \<or> (\<exists>j\<in>{1..D}. \<exists>b\<in>B. P (b + j))"
+ proof clarsimp
+ assume \<section>: "\<forall>j\<in>{1..D}. \<forall>b\<in>B. \<not> P (b + j)"
+ then have "\<And>k. 0\<le>k \<Longrightarrow> \<forall>x. P x \<longrightarrow> P (x - k*D)"
+ by (simp add: assms decr_mult_lemma)
+ with L \<section> assms show "\<exists>j\<in>{1..D}. P1 j"
+ using periodic_finite_ex [OF \<open>D>0\<close>, of P1]
+ by (metis abs_1 abs_add_abs abs_ge_zero decr_lemma)
+ qed
+next
+ assume ?R then show "\<exists>x. P x"
+ using decr_lemma assms by blast
+qed
theorem cp_thm:
assumes lp: "iszlfm p"
@@ -2141,22 +2094,7 @@
lemma mirror_ex:
assumes "iszlfm p"
shows "(\<exists>x. Ifm bbs (x#bs) (mirror p)) \<longleftrightarrow> (\<exists>x. Ifm bbs (x#bs) p)"
- (is "(\<exists>x. ?I x ?mp) = (\<exists>x. ?I x p)")
-proof auto
- fix x
- assume "?I x ?mp"
- then have "?I (- x) p"
- using mirror[OF assms] by blast
- then show "\<exists>x. ?I x p"
- by blast
-next
- fix x
- assume "?I x p"
- then have "?I (- x) ?mp"
- using mirror[OF assms, where x="- x", symmetric] by auto
- then show "\<exists>x. ?I x ?mp"
- by blast
-qed
+ by (metis assms minus_equation_iff mirror)
lemma cp_thm':
assumes "iszlfm p"
--- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy Sun Mar 16 09:11:17 2025 +0100
+++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy Sun Mar 16 12:03:47 2025 +0000
@@ -29,27 +29,34 @@
(\<exists>x. (\<forall>y \<in> (insert l L). y < x) \<and> (\<forall>y \<in> U. x < y))"
by auto
-lemma gather_start [no_atp]: "(\<exists>x. P x) \<equiv> (\<exists>x. (\<forall>y \<in> {}. y < x) \<and> (\<forall>y\<in> {}. x < y) \<and> P x)"
+lemma gather_start [no_atp]: "(\<exists>x. P x) \<longleftrightarrow> (\<exists>x. (\<forall>y \<in> {}. y < x) \<and> (\<forall>y\<in> {}. x < y) \<and> P x)"
by simp
text\<open>Theorems for \<open>\<exists>z. \<forall>x. x < z \<longrightarrow> (P x \<longleftrightarrow> P\<^sub>-\<^sub>\<infinity>)\<close>\<close>
-lemma minf_lt[no_atp]: "\<exists>z . \<forall>x. x < z \<longrightarrow> (x < t \<longleftrightarrow> True)" by auto
-lemma minf_gt[no_atp]: "\<exists>z . \<forall>x. x < z \<longrightarrow> (t < x \<longleftrightarrow> False)"
+lemma minf_lt[no_atp]: "\<exists>z. \<forall>x. x < z \<longrightarrow> (x < t \<longleftrightarrow> True)"
+ by auto
+lemma minf_gt[no_atp]: "\<exists>z. \<forall>x. x < z \<longrightarrow> (t < x \<longleftrightarrow> False)"
by (simp add: not_less) (rule exI[where x="t"], auto simp add: less_le)
-lemma minf_le[no_atp]: "\<exists>z. \<forall>x. x < z \<longrightarrow> (x \<le> t \<longleftrightarrow> True)" by (auto simp add: less_le)
+lemma minf_le[no_atp]: "\<exists>z. \<forall>x. x < z \<longrightarrow> (x \<le> t \<longleftrightarrow> True)"
+ by (auto simp add: less_le)
lemma minf_ge[no_atp]: "\<exists>z. \<forall>x. x < z \<longrightarrow> (t \<le> x \<longleftrightarrow> False)"
by (auto simp add: less_le not_less not_le)
-lemma minf_eq[no_atp]: "\<exists>z. \<forall>x. x < z \<longrightarrow> (x = t \<longleftrightarrow> False)" by auto
-lemma minf_neq[no_atp]: "\<exists>z. \<forall>x. x < z \<longrightarrow> (x \<noteq> t \<longleftrightarrow> True)" by auto
-lemma minf_P[no_atp]: "\<exists>z. \<forall>x. x < z \<longrightarrow> (P \<longleftrightarrow> P)" by blast
+lemma minf_eq[no_atp]: "\<exists>z. \<forall>x. x < z \<longrightarrow> (x = t \<longleftrightarrow> False)"
+ by auto
+lemma minf_neq[no_atp]: "\<exists>z. \<forall>x. x < z \<longrightarrow> (x \<noteq> t \<longleftrightarrow> True)"
+ by auto
+lemma minf_P[no_atp]: "\<exists>z. \<forall>x. x < z \<longrightarrow> (P \<longleftrightarrow> P)"
+ by blast
text\<open>Theorems for \<open>\<exists>z. \<forall>x. x < z \<longrightarrow> (P x \<longleftrightarrow> P\<^sub>+\<^sub>\<infinity>)\<close>\<close>
-lemma pinf_gt[no_atp]: "\<exists>z. \<forall>x. z < x \<longrightarrow> (t < x \<longleftrightarrow> True)" by auto
+lemma pinf_gt[no_atp]: "\<exists>z. \<forall>x. z < x \<longrightarrow> (t < x \<longleftrightarrow> True)"
+ by auto
lemma pinf_lt[no_atp]: "\<exists>z. \<forall>x. z < x \<longrightarrow> (x < t \<longleftrightarrow> False)"
by (simp add: not_less) (rule exI[where x="t"], auto simp add: less_le)
-lemma pinf_ge[no_atp]: "\<exists>z. \<forall>x. z < x \<longrightarrow> (t \<le> x \<longleftrightarrow> True)" by (auto simp add: less_le)
+lemma pinf_ge[no_atp]: "\<exists>z. \<forall>x. z < x \<longrightarrow> (t \<le> x \<longleftrightarrow> True)"
+ by (auto simp add: less_le)
lemma pinf_le[no_atp]: "\<exists>z. \<forall>x. z < x \<longrightarrow> (x \<le> t \<longleftrightarrow> False)"
by (auto simp add: less_le not_less not_le)
lemma pinf_eq[no_atp]: "\<exists>z. \<forall>x. z < x \<longrightarrow> (x = t \<longleftrightarrow> False)" by auto
@@ -86,104 +93,22 @@
lemma lin_dense_lt[no_atp]:
"t \<in> U \<Longrightarrow>
\<forall>x l u. (\<forall>t. l < t \<and> t < u \<longrightarrow> t \<notin> U) \<and> l < x \<and> x < u \<and> x < t \<longrightarrow> (\<forall>y. l < y \<and> y < u \<longrightarrow> y < t)"
-proof clarsimp
- fix x l u y
- assume tU: "t \<in> U"
- and noU: "\<forall>t. l < t \<and> t < u \<longrightarrow> t \<notin> U"
- and lx: "l < x"
- and xu: "x < u"
- and px: "x < t"
- and ly: "l < y"
- and yu: "y < u"
- from tU noU ly yu have tny: "t \<noteq> y" by auto
- have False if H: "t < y"
- proof -
- from less_trans[OF lx px] less_trans[OF H yu] have "l < t \<and> t < u"
- by simp
- with tU noU show ?thesis
- by auto
- qed
- then have "\<not> t < y"
- by auto
- then have "y \<le> t"
- by (simp add: not_less)
- then show "y < t"
- using tny by (simp add: less_le)
-qed
+ by (metis antisym_conv3 order.strict_trans)
lemma lin_dense_gt[no_atp]:
"t \<in> U \<Longrightarrow>
\<forall>x l u. (\<forall>t. l < t \<and> t < u \<longrightarrow> t \<notin> U) \<and> l < x \<and> x < u \<and> t < x \<longrightarrow> (\<forall>y. l < y \<and> y < u \<longrightarrow> t < y)"
-proof clarsimp
- fix x l u y
- assume tU: "t \<in> U"
- and noU: "\<forall>t. l < t \<and> t < u \<longrightarrow> t \<notin> U"
- and lx: "l < x"
- and xu: "x < u"
- and px: "t < x"
- and ly: "l < y"
- and yu: "y < u"
- from tU noU ly yu have tny: "t \<noteq> y" by auto
- have False if H: "y < t"
- proof -
- from less_trans[OF ly H] less_trans[OF px xu] have "l < t \<and> t < u"
- by simp
- with tU noU show ?thesis
- by auto
- qed
- then have "\<not> y < t"
- by auto
- then have "t \<le> y"
- by (auto simp add: not_less)
- then show "t < y"
- using tny by (simp add: less_le)
-qed
+ by (metis antisym_conv3 order.strict_trans)
lemma lin_dense_le[no_atp]:
"t \<in> U \<Longrightarrow>
\<forall>x l u. (\<forall>t. l < t \<and> t < u \<longrightarrow> t \<notin> U) \<and> l < x \<and> x < u \<and> x \<le> t \<longrightarrow> (\<forall>y. l < y \<and> y < u \<longrightarrow> y \<le> t)"
-proof clarsimp
- fix x l u y
- assume tU: "t \<in> U"
- and noU: "\<forall>t. l < t \<and> t < u \<longrightarrow> t \<notin> U"
- and lx: "l < x"
- and xu: "x < u"
- and px: "x \<le> t"
- and ly: "l < y"
- and yu: "y < u"
- from tU noU ly yu have tny: "t \<noteq> y" by auto
- have False if H: "t < y"
- proof -
- from less_le_trans[OF lx px] less_trans[OF H yu]
- have "l < t \<and> t < u" by simp
- with tU noU show ?thesis by auto
- qed
- then have "\<not> t < y" by auto
- then show "y \<le> t" by (simp add: not_less)
-qed
+ by (metis local.less_le_trans local.less_trans local.not_less)
lemma lin_dense_ge[no_atp]:
"t \<in> U \<Longrightarrow>
\<forall>x l u. (\<forall>t. l < t \<and> t < u \<longrightarrow> t \<notin> U) \<and> l < x \<and> x < u \<and> t \<le> x \<longrightarrow> (\<forall>y. l < y \<and> y < u \<longrightarrow> t \<le> y)"
-proof clarsimp
- fix x l u y
- assume tU: "t \<in> U"
- and noU: "\<forall>t. l < t \<and> t < u \<longrightarrow> t \<notin> U"
- and lx: "l < x"
- and xu: "x < u"
- and px: "t \<le> x"
- and ly: "l < y"
- and yu: "y < u"
- from tU noU ly yu have tny: "t \<noteq> y" by auto
- have False if H: "y < t"
- proof -
- from less_trans[OF ly H] le_less_trans[OF px xu]
- have "l < t \<and> t < u" by simp
- with tU noU show ?thesis by auto
- qed
- then have "\<not> y < t" by auto
- then show "t \<le> y" by (simp add: not_less)
-qed
+ by (metis local.le_less_trans local.nle_le not_le)
lemma lin_dense_eq[no_atp]:
"t \<in> U \<Longrightarrow>
@@ -207,6 +132,7 @@
\<forall>x l u. (\<forall>t. l < t \<and> t < u \<longrightarrow> t \<notin> U) \<and> l < x \<and> x < u \<and> (P1 x \<and> P2 x)
\<longrightarrow> (\<forall>y. l < y \<and> y < u \<longrightarrow> (P1 y \<and> P2 y))"
by blast
+
lemma lin_dense_disj[no_atp]:
"\<lbrakk>\<forall>x l u. (\<forall>t. l < t \<and> t < u \<longrightarrow> t \<notin> U) \<and> l < x \<and> x < u \<and> P1 x
\<longrightarrow> (\<forall>y. l < y \<and> y < u \<longrightarrow> P1 y) ;
@@ -264,26 +190,7 @@
then have binS: "?b \<in> S"
using xMS by blast
have noy: "\<forall>y. ?a < y \<and> y < ?b \<longrightarrow> y \<notin> S"
- proof clarsimp
- fix y
- assume ay: "?a < y" and yb: "y < ?b" and yS: "y \<in> S"
- from yS have "y \<in> ?Mx \<or> y \<in> ?xM"
- by (auto simp add: linear)
- then show False
- proof
- assume "y \<in> ?Mx"
- then have "y \<le> ?a"
- using Mxne fMx by auto
- with ay show ?thesis
- by (simp add: not_le[symmetric])
- next
- assume "y \<in> ?xM"
- then have "?b \<le> y"
- using xMne fxM by auto
- with yb show ?thesis
- by (simp add: not_le[symmetric])
- qed
- qed
+ using Mxne fMx fxM local.linear xMne by auto
from ainS binS noy ax xb px show ?thesis
by blast
qed
@@ -298,17 +205,8 @@
and lS: "\<forall>x\<in> S. l \<le> x"
and Su: "\<forall>x\<in> S. x \<le> u"
shows "(\<exists>s\<in> S. P s) \<or> (\<exists>a \<in> S. \<exists>b \<in> S. (\<forall>y. a < y \<and> y < b \<longrightarrow> y \<notin> S) \<and> a < x \<and> x < b \<and> P x)"
-proof -
- from finite_set_intervals[where P="P", OF px lx xu linS uinS fS lS Su]
- obtain a and b where as: "a \<in> S" and bs: "b \<in> S"
- and noS: "\<forall>y. a < y \<and> y < b \<longrightarrow> y \<notin> S"
- and axb: "a \<le> x \<and> x \<le> b \<and> P x"
- by auto
- from axb have "x = a \<or> x = b \<or> (a < x \<and> x < b)"
- by (auto simp add: le_less)
- then show ?thesis
- using px as bs noS by blast
-qed
+ using finite_set_intervals[where P="P", OF px lx xu linS uinS fS lS Su]
+ by (metis local.neq_le_trans)
end
@@ -326,17 +224,13 @@
and neU: "U \<noteq> {}"
and fL: "finite L"
and fU: "finite U"
- shows "(\<exists>x. (\<forall>y \<in> L. y < x) \<and> (\<forall>y \<in> U. x < y)) \<equiv> (\<forall>l \<in> L. \<forall>u \<in> U. l < u)"
-proof (simp only: atomize_eq, rule iffI)
+ shows "(\<exists>x. (\<forall>y \<in> L. y < x) \<and> (\<forall>y \<in> U. x < y)) = (\<forall>l \<in> L. \<forall>u \<in> U. l < u)"
+proof
assume H: "\<exists>x. (\<forall>y\<in>L. y < x) \<and> (\<forall>y\<in>U. x < y)"
then obtain x where xL: "\<forall>y\<in>L. y < x" and xU: "\<forall>y\<in>U. x < y"
by blast
have "l < u" if l: "l \<in> L" and u: "u \<in> U" for l u
- proof -
- have "l < x" using xL l by blast
- also have "x < u" using xU u by blast
- finally show ?thesis .
- qed
+ using local.dual_order.strict_trans that(1) u xL xU by blast
then show "\<forall>l\<in>L. \<forall>u\<in>U. l < u" by blast
next
assume H: "\<forall>l\<in>L. \<forall>u\<in>U. l < u"
@@ -361,30 +255,21 @@
lemma dlo_qe_noub[no_atp]:
assumes ne: "L \<noteq> {}"
and fL: "finite L"
- shows "(\<exists>x. (\<forall>y \<in> L. y < x) \<and> (\<forall>y \<in> {}. x < y)) \<equiv> True"
-proof (simp add: atomize_eq)
- from gt_ex[of "Max L"] obtain M where M: "Max L < M"
- by blast
- from ne fL have "\<forall>x \<in> L. x \<le> Max L"
- by simp
- with M have "\<forall>x\<in>L. x < M"
- by (auto intro: le_less_trans)
- then show "\<exists>x. \<forall>y\<in>L. y < x"
- by blast
-qed
+ shows "(\<exists>x. (\<forall>y \<in> L. y < x) \<and> (\<forall>y \<in> {}. x < y)) = True"
+ using fL local.Max_less_iff local.gt_ex by fastforce
lemma dlo_qe_nolb[no_atp]:
assumes ne: "U \<noteq> {}"
and fU: "finite U"
- shows "(\<exists>x. (\<forall>y \<in> {}. y < x) \<and> (\<forall>y \<in> U. x < y)) \<equiv> True"
-proof (simp add: atomize_eq)
+ shows "(\<exists>x. (\<forall>y \<in> {}. y < x) \<and> (\<forall>y \<in> U. x < y)) = True"
+proof -
from lt_ex[of "Min U"] obtain M where M: "M < Min U"
by blast
from ne fU have "\<forall>x \<in> U. Min U \<le> x"
by simp
with M have "\<forall>x\<in>U. M < x"
by (auto intro: less_le_trans)
- then show "\<exists>x. \<forall>y\<in>U. x < y"
+ then show ?thesis
by blast
qed
@@ -396,6 +281,7 @@
lemma axiom[no_atp]: "class.unbounded_dense_linorder (\<le>) (<)"
by (rule unbounded_dense_linorder_axioms)
+
lemma atoms[no_atp]:
shows "TERM (less :: 'a \<Rightarrow> _)"
and "TERM (less_eq :: 'a \<Rightarrow> _)"
@@ -457,52 +343,19 @@
assumes ex1: "\<exists>z1. \<forall>x. z1 \<sqsubset> x \<longrightarrow> (P1 x \<longleftrightarrow> P1')"
and ex2: "\<exists>z2. \<forall>x. z2 \<sqsubset> x \<longrightarrow> (P2 x \<longleftrightarrow> P2')"
shows "\<exists>z. \<forall>x. z \<sqsubset> x \<longrightarrow> ((P1 x \<and> P2 x) \<longleftrightarrow> (P1' \<and> P2'))"
-proof -
- from ex1 ex2 obtain z1 and z2
- where z1: "\<forall>x. z1 \<sqsubset> x \<longrightarrow> (P1 x \<longleftrightarrow> P1')"
- and z2: "\<forall>x. z2 \<sqsubset> x \<longrightarrow> (P2 x \<longleftrightarrow> P2')"
- by blast
- from gt_ex obtain z where z:"ord.max less_eq z1 z2 \<sqsubset> z"
- by blast
- from z have zz1: "z1 \<sqsubset> z" and zz2: "z2 \<sqsubset> z"
- by simp_all
- have "(P1 x \<and> P2 x) \<longleftrightarrow> (P1' \<and> P2')" if H: "z \<sqsubset> x" for x
- using less_trans[OF zz1 H] less_trans[OF zz2 H] z1 zz1 z2 zz2 by auto
- then show ?thesis
- by blast
-qed
+ by (metis ex1 ex2 local.max_less_iff_conj)
lemma pinf_disj[no_atp]:
assumes ex1: "\<exists>z1. \<forall>x. z1 \<sqsubset> x \<longrightarrow> (P1 x \<longleftrightarrow> P1')"
and ex2: "\<exists>z2. \<forall>x. z2 \<sqsubset> x \<longrightarrow> (P2 x \<longleftrightarrow> P2')"
shows "\<exists>z. \<forall>x. z \<sqsubset> x \<longrightarrow> ((P1 x \<or> P2 x) \<longleftrightarrow> (P1' \<or> P2'))"
-proof-
- from ex1 ex2 obtain z1 and z2
- where z1: "\<forall>x. z1 \<sqsubset> x \<longrightarrow> (P1 x \<longleftrightarrow> P1')"
- and z2: "\<forall>x. z2 \<sqsubset> x \<longrightarrow> (P2 x \<longleftrightarrow> P2')"
- by blast
- from gt_ex obtain z where z: "ord.max less_eq z1 z2 \<sqsubset> z"
- by blast
- from z have zz1: "z1 \<sqsubset> z" and zz2: "z2 \<sqsubset> z"
- by simp_all
- have "(P1 x \<or> P2 x) \<longleftrightarrow> (P1' \<or> P2')" if H: "z \<sqsubset> x" for x
- using less_trans[OF zz1 H] less_trans[OF zz2 H] z1 zz1 z2 zz2 by auto
- then show ?thesis
- by blast
-qed
+ by (metis ex1 ex2 local.max.strict_boundedE)
lemma pinf_ex[no_atp]:
assumes ex: "\<exists>z. \<forall>x. z \<sqsubset> x \<longrightarrow> (P x \<longleftrightarrow> P1)"
and p1: P1
shows "\<exists>x. P x"
-proof -
- from ex obtain z where z: "\<forall>x. z \<sqsubset> x \<longrightarrow> (P x \<longleftrightarrow> P1)"
- by blast
- from gt_ex obtain x where x: "z \<sqsubset> x"
- by blast
- from z x p1 show ?thesis
- by blast
-qed
+ using ex local.gt_ex p1 by auto
end
@@ -521,52 +374,19 @@
assumes ex1: "\<exists>z1. \<forall>x. x \<sqsubset> z1 \<longrightarrow> (P1 x \<longleftrightarrow> P1')"
and ex2: "\<exists>z2. \<forall>x. x \<sqsubset> z2 \<longrightarrow> (P2 x \<longleftrightarrow> P2')"
shows "\<exists>z. \<forall>x. x \<sqsubset> z \<longrightarrow> ((P1 x \<and> P2 x) \<longleftrightarrow> (P1' \<and> P2'))"
-proof -
- from ex1 ex2 obtain z1 and z2
- where z1: "\<forall>x. x \<sqsubset> z1 \<longrightarrow> (P1 x \<longleftrightarrow> P1')"
- and z2: "\<forall>x. x \<sqsubset> z2 \<longrightarrow> (P2 x \<longleftrightarrow> P2')"
- by blast
- from lt_ex obtain z where z: "z \<sqsubset> ord.min less_eq z1 z2"
- by blast
- from z have zz1: "z \<sqsubset> z1" and zz2: "z \<sqsubset> z2"
- by simp_all
- have "(P1 x \<and> P2 x) \<longleftrightarrow> (P1' \<and> P2')" if H: "x \<sqsubset> z" for x
- using less_trans[OF H zz1] less_trans[OF H zz2] z1 zz1 z2 zz2 by auto
- then show ?thesis
- by blast
-qed
+ by (metis ex1 ex2 local.min_less_iff_conj)
lemma minf_disj[no_atp]:
assumes ex1: "\<exists>z1. \<forall>x. x \<sqsubset> z1 \<longrightarrow> (P1 x \<longleftrightarrow> P1')"
and ex2: "\<exists>z2. \<forall>x. x \<sqsubset> z2 \<longrightarrow> (P2 x \<longleftrightarrow> P2')"
shows "\<exists>z. \<forall>x. x \<sqsubset> z \<longrightarrow> ((P1 x \<or> P2 x) \<longleftrightarrow> (P1' \<or> P2'))"
-proof -
- from ex1 ex2 obtain z1 and z2
- where z1: "\<forall>x. x \<sqsubset> z1 \<longrightarrow> (P1 x \<longleftrightarrow> P1')"
- and z2: "\<forall>x. x \<sqsubset> z2 \<longrightarrow> (P2 x \<longleftrightarrow> P2')"
- by blast
- from lt_ex obtain z where z: "z \<sqsubset> ord.min less_eq z1 z2"
- by blast
- from z have zz1: "z \<sqsubset> z1" and zz2: "z \<sqsubset> z2"
- by simp_all
- have "(P1 x \<or> P2 x) \<longleftrightarrow> (P1' \<or> P2')" if H: "x \<sqsubset> z" for x
- using less_trans[OF H zz1] less_trans[OF H zz2] z1 zz1 z2 zz2 by auto
- then show ?thesis
- by blast
-qed
+ by (metis ex1 ex2 local.min_less_iff_conj)
lemma minf_ex[no_atp]:
assumes ex: "\<exists>z. \<forall>x. x \<sqsubset> z \<longrightarrow> (P x \<longleftrightarrow> P1)"
and p1: P1
shows "\<exists>x. P x"
-proof -
- from ex obtain z where z: "\<forall>x. x \<sqsubset> z \<longrightarrow> (P x \<longleftrightarrow> P1)"
- by blast
- from lt_ex obtain x where x: "x \<sqsubset> z"
- by blast
- from z x p1 show ?thesis
- by blast
-qed
+ using ex local.lt_ex p1 by auto
end
@@ -600,9 +420,8 @@
proof -
from ex obtain x where px: "P x"
by blast
- from px nmi npi nmpiU have "\<exists>u\<in> U. \<exists>u' \<in> U. u \<sqsubseteq> x \<and> x \<sqsubseteq> u'"
- by auto
- then obtain u and u' where uU: "u\<in> U" and uU': "u' \<in> U" and ux: "u \<sqsubseteq> x" and xu': "x \<sqsubseteq> u'"
+ from px nmi npi nmpiU
+ obtain u u' where uU: "u\<in> U" and uU': "u' \<in> U" and ux: "u \<sqsubseteq> x" and xu': "x \<sqsubseteq> u'"
by auto
from uU have Une: "U \<noteq> {}"
by auto
@@ -628,21 +447,16 @@
by blast
then show ?thesis
proof cases
- case u: 1
- have "between u u = u" by (simp add: between_same)
- with u have "P (between u u)" by simp
- with u show ?thesis by blast
+ case 1 then show ?thesis
+ by (metis between_same)
next
case 2
- note t1M = \<open>t1 \<in> U\<close> and t2M = \<open>t2\<in> U\<close>
- and noM = \<open>\<forall>y. t1 \<sqsubset> y \<and> y \<sqsubset> t2 \<longrightarrow> y \<notin> U\<close>
- and t1x = \<open>t1 \<sqsubset> x\<close> and xt2 = \<open>x \<sqsubset> t2\<close>
- and px = \<open>P x\<close>
- from less_trans[OF t1x xt2] have t1t2: "t1 \<sqsubset> t2" .
+ then have t1t2: "t1 \<sqsubset> t2"
+ by order
let ?u = "between t1 t2"
from between_less t1t2 have t1lu: "t1 \<sqsubset> ?u" and ut2: "?u \<sqsubset> t2" by auto
- from lin_dense noM t1x xt2 px t1lu ut2 have "P ?u" by blast
- with t1M t2M show ?thesis by blast
+ then show ?thesis
+ using "2" lin_dense px by blast
qed
qed
@@ -653,43 +467,26 @@
and nmibnd: "\<forall>x. \<not> MP \<and> P x \<longrightarrow> (\<exists>u\<in> U. u \<sqsubseteq> x)"
and npibnd: "\<forall>x. \<not>PP \<and> P x \<longrightarrow> (\<exists>u\<in> U. x \<sqsubseteq> u)"
and mi: "\<exists>z. \<forall>x. x \<sqsubset> z \<longrightarrow> (P x = MP)" and pi: "\<exists>z. \<forall>x. z \<sqsubset> x \<longrightarrow> (P x = PP)"
- shows "(\<exists>x. P x) \<equiv> (MP \<or> PP \<or> (\<exists>u \<in> U. \<exists>u'\<in> U. P (between u u')))"
- (is "_ \<equiv> (_ \<or> _ \<or> ?F)" is "?E \<equiv> ?D")
-proof -
- have "?E \<longleftrightarrow> ?D"
- proof
- show ?D if px: ?E
- proof -
- consider "MP \<or> PP" | "\<not> MP" "\<not> PP" by blast
- then show ?thesis
- proof cases
- case 1
- then show ?thesis by blast
- next
- case 2
- from npmibnd[OF nmibnd npibnd]
- have nmpiU: "\<forall>x. \<not> MP \<and> \<not>PP \<and> P x \<longrightarrow> (\<exists>u\<in> U. \<exists>u' \<in> U. u \<sqsubseteq> x \<and> x \<sqsubseteq> u')" .
- from rinf_U[OF fU lin_dense nmpiU \<open>\<not> MP\<close> \<open>\<not> PP\<close> px] show ?thesis
- by blast
- qed
- qed
- show ?E if ?D
- proof -
- from that consider MP | PP | ?F by blast
- then show ?thesis
- proof cases
- case 1
- from minf_ex[OF mi this] show ?thesis .
- next
- case 2
- from pinf_ex[OF pi this] show ?thesis .
- next
- case 3
- then show ?thesis by blast
- qed
+ shows "(\<exists>x. P x) = (MP \<or> PP \<or> (\<exists>u \<in> U. \<exists>u'\<in> U. P (between u u')))"
+ (is"?E = ?D")
+proof
+ show ?D if px: ?E
+ proof -
+ consider "MP \<or> PP" | "\<not> MP" "\<not> PP" by blast
+ then show ?thesis
+ proof cases
+ case 1
+ then show ?thesis by blast
+ next
+ case 2
+ from npmibnd[OF nmibnd npibnd]
+ have nmpiU: "\<forall>x. \<not> MP \<and> \<not>PP \<and> P x \<longrightarrow> (\<exists>u\<in> U. \<exists>u' \<in> U. u \<sqsubseteq> x \<and> x \<sqsubseteq> u')" .
+ from rinf_U[OF fU lin_dense nmpiU \<open>\<not> MP\<close> \<open>\<not> PP\<close> px] show ?thesis
+ by blast
qed
qed
- then show "?E \<equiv> ?D" by simp
+ show ?E if ?D
+ using local.gt_ex local.lt_ex mi pi that by blast
qed
lemmas minf_thms[no_atp] = minf_conj minf_disj minf_eq minf_neq minf_lt minf_le minf_gt minf_ge minf_P
@@ -758,135 +555,81 @@
lemma neg_prod_lt:
fixes c :: "'a::linordered_field"
assumes "c < 0"
- shows "c * x < 0 \<equiv> x > 0"
-proof -
- have "c * x < 0 \<longleftrightarrow> 0 / c < x"
- by (simp only: neg_divide_less_eq[OF \<open>c < 0\<close>] algebra_simps)
- also have "\<dots> \<longleftrightarrow> 0 < x" by simp
- finally show "PROP ?thesis" by simp
-qed
+ shows "c * x < 0 \<longleftrightarrow> x > 0"
+ by (metis assms mult_less_0_iff mult_neg_neg zero_less_mult_pos)
lemma pos_prod_lt:
fixes c :: "'a::linordered_field"
assumes "c > 0"
- shows "c * x < 0 \<equiv> x < 0"
-proof -
- have "c * x < 0 \<longleftrightarrow> 0 /c > x"
- by (simp only: pos_less_divide_eq[OF \<open>c > 0\<close>] algebra_simps)
- also have "\<dots> \<longleftrightarrow> 0 > x" by simp
- finally show "PROP ?thesis" by simp
-qed
+ shows "c * x < 0 \<longleftrightarrow> x < 0"
+ by (meson assms mult_less_0_iff order_less_imp_not_less)
lemma neg_prod_sum_lt:
fixes c :: "'a::linordered_field"
assumes "c < 0"
- shows "c * x + t < 0 \<equiv> x > (- 1 / c) * t"
-proof -
- have "c * x + t < 0 \<longleftrightarrow> c * x < - t"
- by (subst less_iff_diff_less_0 [of "c * x" "- t"]) simp
- also have "\<dots> \<longleftrightarrow> - t / c < x"
- by (simp only: neg_divide_less_eq[OF \<open>c < 0\<close>] algebra_simps)
- also have "\<dots> \<longleftrightarrow> (- 1 / c) * t < x" by simp
- finally show "PROP ?thesis" by simp
-qed
+ shows "c * x + t < 0 \<longleftrightarrow> x > (- 1 / c) * t"
+ using assms by (auto simp add: mult.commute divide_simps)
lemma pos_prod_sum_lt:
fixes c :: "'a::linordered_field"
assumes "c > 0"
- shows "c * x + t < 0 \<equiv> x < (- 1 / c) * t"
-proof -
- have "c * x + t < 0 \<longleftrightarrow> c * x < - t"
- by (subst less_iff_diff_less_0 [of "c * x" "- t"]) simp
- also have "\<dots> \<longleftrightarrow> - t / c > x"
- by (simp only: pos_less_divide_eq[OF \<open>c > 0\<close>] algebra_simps)
- also have "\<dots> \<longleftrightarrow> (- 1 / c) * t > x" by simp
- finally show "PROP ?thesis" by simp
-qed
+ shows "c * x + t < 0 \<longleftrightarrow> x < (- 1 / c) * t"
+ using assms by (auto simp add: mult.commute divide_simps)
lemma sum_lt:
fixes x :: "'a::ordered_ab_group_add"
- shows "x + t < 0 \<equiv> x < - t"
+ shows "x + t < 0 \<longleftrightarrow> x < - t"
using less_diff_eq[where a= x and b=t and c=0] by simp
lemma neg_prod_le:
fixes c :: "'a::linordered_field"
assumes "c < 0"
- shows "c * x \<le> 0 \<equiv> x \<ge> 0"
-proof -
- have "c * x \<le> 0 \<longleftrightarrow> 0 / c \<le> x"
- by (simp only: neg_divide_le_eq[OF \<open>c < 0\<close>] algebra_simps)
- also have "\<dots> \<longleftrightarrow> 0 \<le> x" by simp
- finally show "PROP ?thesis" by simp
-qed
+ shows "c * x \<le> 0 \<longleftrightarrow> x \<ge> 0"
+ using assms linorder_not_less mult_le_0_iff by auto
lemma pos_prod_le:
fixes c :: "'a::linordered_field"
assumes "c > 0"
- shows "c * x \<le> 0 \<equiv> x \<le> 0"
-proof -
- have "c * x \<le> 0 \<longleftrightarrow> 0 / c \<ge> x"
- by (simp only: pos_le_divide_eq[OF \<open>c > 0\<close>] algebra_simps)
- also have "\<dots> \<longleftrightarrow> 0 \<ge> x" by simp
- finally show "PROP ?thesis" by simp
-qed
+ shows "c * x \<le> 0 \<longleftrightarrow> x \<le> 0"
+ using assms linorder_not_less mult_le_0_iff by auto
lemma neg_prod_sum_le:
fixes c :: "'a::linordered_field"
assumes "c < 0"
- shows "c * x + t \<le> 0 \<equiv> x \<ge> (- 1 / c) * t"
-proof -
- have "c * x + t \<le> 0 \<longleftrightarrow> c * x \<le> -t"
- by (subst le_iff_diff_le_0 [of "c*x" "-t"]) simp
- also have "\<dots> \<longleftrightarrow> - t / c \<le> x"
- by (simp only: neg_divide_le_eq[OF \<open>c < 0\<close>] algebra_simps)
- also have "\<dots> \<longleftrightarrow> (- 1 / c) * t \<le> x" by simp
- finally show "PROP ?thesis" by simp
-qed
+ shows "c * x + t \<le> 0 \<longleftrightarrow> x \<ge> (- 1 / c) * t"
+ using assms by (auto simp add: mult.commute divide_simps)
lemma pos_prod_sum_le:
fixes c :: "'a::linordered_field"
assumes "c > 0"
- shows "c * x + t \<le> 0 \<equiv> x \<le> (- 1 / c) * t"
-proof -
- have "c * x + t \<le> 0 \<longleftrightarrow> c * x \<le> - t"
- by (subst le_iff_diff_le_0 [of "c*x" "-t"]) simp
- also have "\<dots> \<longleftrightarrow> - t / c \<ge> x"
- by (simp only: pos_le_divide_eq[OF \<open>c > 0\<close>] algebra_simps)
- also have "\<dots> \<longleftrightarrow> (- 1 / c) * t \<ge> x" by simp
- finally show "PROP ?thesis" by simp
-qed
+ shows "c * x + t \<le> 0 \<longleftrightarrow> x \<le> (- 1 / c) * t"
+ using assms by (auto simp add: mult.commute divide_simps)
lemma sum_le:
fixes x :: "'a::ordered_ab_group_add"
- shows "x + t \<le> 0 \<equiv> x \<le> - t"
+ shows "x + t \<le> 0 \<longleftrightarrow> x \<le> - t"
using le_diff_eq[where a= x and b=t and c=0] by simp
lemma nz_prod_eq:
fixes c :: "'a::linordered_field"
assumes "c \<noteq> 0"
- shows "c * x = 0 \<equiv> x = 0"
+ shows "c * x = 0 \<longleftrightarrow> x = 0"
using assms by simp
lemma nz_prod_sum_eq:
fixes c :: "'a::linordered_field"
assumes "c \<noteq> 0"
- shows "c * x + t = 0 \<equiv> x = (- 1/c) * t"
-proof -
- have "c * x + t = 0 \<longleftrightarrow> c * x = - t"
- by (subst eq_iff_diff_eq_0 [of "c*x" "-t"]) simp
- also have "\<dots> \<longleftrightarrow> x = - t / c"
- by (simp only: nonzero_eq_divide_eq[OF \<open>c \<noteq> 0\<close>] algebra_simps)
- finally show "PROP ?thesis" by simp
-qed
+ shows "c * x + t = 0 \<longleftrightarrow> x = (- 1/c) * t"
+ using assms by (auto simp add: mult.commute divide_simps)
lemma sum_eq:
fixes x :: "'a::ordered_ab_group_add"
- shows "x + t = 0 \<equiv> x = - t"
+ shows "x + t = 0 \<longleftrightarrow> x = - t"
using eq_diff_eq[where a= x and b=t and c=0] by simp
interpretation class_dense_linordered_field: constr_dense_linorder
"(\<le>)" "(<)" "\<lambda>x y. 1/2 * ((x::'a::linordered_field) + y)"
- by unfold_locales (dlo, dlo, auto)
+ by unfold_locales (auto simp add: gt_ex lt_ex)
declaration \<open>
let
@@ -935,14 +678,14 @@
else Thm.apply (Thm.apply clt cz) c))
val cth = Thm.equal_elim (Thm.symmetric cthp) TrueI
val th = Thm.implies_elim (Thm.instantiate' [SOME (Thm.ctyp_of_cterm x)] (map SOME [c,x,t])
- (if neg then @{thm neg_prod_sum_lt} else @{thm pos_prod_sum_lt})) cth
+ (mk_meta_eq(if neg then @{thm neg_prod_sum_lt} else @{thm pos_prod_sum_lt}))) cth
val rth = Conv.fconv_rule (Conv.arg_conv (Conv.binop_conv
(Semiring_Normalizer.semiring_normalize_ord_conv ctxt (earlier_ord vs)))) th
in rth end
| ("x+t",[t]) =>
let
val T = Thm.ctyp_of_cterm x
- val th = Thm.instantiate' [SOME T] [SOME x, SOME t] @{thm "sum_lt"}
+ val th =Thm.instantiate' [SOME T] [SOME x, SOME t] (mk_meta_eq @{thm "sum_lt"})
val rth = Conv.fconv_rule (Conv.arg_conv (Conv.binop_conv
(Semiring_Normalizer.semiring_normalize_ord_conv ctxt (earlier_ord vs)))) th
in rth end
@@ -958,7 +701,7 @@
else Thm.apply (Thm.apply clt cz) c))
val cth = Thm.equal_elim (Thm.symmetric cthp) TrueI
val th = Thm.implies_elim (Thm.instantiate' [SOME (Thm.ctyp_of_cterm x)] (map SOME [c,x])
- (if neg then @{thm neg_prod_lt} else @{thm pos_prod_lt})) cth
+ (mk_meta_eq(if neg then @{thm neg_prod_lt} else @{thm pos_prod_lt}))) cth
val rth = th
in rth end
| _ => Thm.reflexive ct)
@@ -980,14 +723,14 @@
else Thm.apply (Thm.apply clt cz) c))
val cth = Thm.equal_elim (Thm.symmetric cthp) TrueI
val th = Thm.implies_elim (Thm.instantiate' [SOME cT] (map SOME [c,x,t])
- (if neg then @{thm neg_prod_sum_le} else @{thm pos_prod_sum_le})) cth
+ (mk_meta_eq(if neg then @{thm neg_prod_sum_le} else @{thm pos_prod_sum_le}))) cth
val rth = Conv.fconv_rule (Conv.arg_conv (Conv.binop_conv
(Semiring_Normalizer.semiring_normalize_ord_conv ctxt (earlier_ord vs)))) th
in rth end
| ("x+t",[t]) =>
let
val T = Thm.ctyp_of_cterm x
- val th = Thm.instantiate' [SOME T] [SOME x, SOME t] @{thm "sum_le"}
+ val th = Thm.instantiate' [SOME T] [SOME x, SOME t] (mk_meta_eq @{thm "sum_le"})
val rth = Conv.fconv_rule (Conv.arg_conv (Conv.binop_conv
(Semiring_Normalizer.semiring_normalize_ord_conv ctxt (earlier_ord vs)))) th
in rth end
@@ -1005,7 +748,7 @@
else Thm.apply (Thm.apply clt cz) c))
val cth = Thm.equal_elim (Thm.symmetric cthp) TrueI
val th = Thm.implies_elim (Thm.instantiate' [SOME (Thm.ctyp_of_cterm x)] (map SOME [c,x])
- (if neg then @{thm neg_prod_le} else @{thm pos_prod_le})) cth
+ (mk_meta_eq(if neg then @{thm neg_prod_le} else @{thm pos_prod_le}))) cth
val rth = th
in rth end
| _ => Thm.reflexive ct)
@@ -1023,14 +766,14 @@
(Thm.apply \<^cterm>\<open>Not\<close> (Thm.apply (Thm.apply ceq c) cz)))
val cth = Thm.equal_elim (Thm.symmetric cthp) TrueI
val th = Thm.implies_elim
- (Thm.instantiate' [SOME T] (map SOME [c,x,t]) @{thm nz_prod_sum_eq}) cth
+ (Thm.instantiate' [SOME T] (map SOME [c,x,t]) (mk_meta_eq @{thm nz_prod_sum_eq})) cth
val rth = Conv.fconv_rule (Conv.arg_conv (Conv.binop_conv
(Semiring_Normalizer.semiring_normalize_ord_conv ctxt (earlier_ord vs)))) th
in rth end
| ("x+t",[t]) =>
let
val T = Thm.ctyp_of_cterm x
- val th = Thm.instantiate' [SOME T] [SOME x, SOME t] @{thm "sum_eq"}
+ val th = Thm.instantiate' [SOME T] [SOME x, SOME t] (mk_meta_eq @{thm "sum_eq"})
val rth = Conv.fconv_rule (Conv.arg_conv (Conv.binop_conv
(Semiring_Normalizer.semiring_normalize_ord_conv ctxt (earlier_ord vs)))) th
in rth end
@@ -1045,7 +788,7 @@
(Thm.apply \<^cterm>\<open>Not\<close> (Thm.apply (Thm.apply ceq c) cz)))
val cth = Thm.equal_elim (Thm.symmetric cthp) TrueI
val rth = Thm.implies_elim
- (Thm.instantiate' [SOME T] (map SOME [c,x]) @{thm nz_prod_eq}) cth
+ (Thm.instantiate' [SOME T] (map SOME [c,x]) (mk_meta_eq @{thm nz_prod_eq})) cth
in rth end
| _ => Thm.reflexive ct);
--- a/src/HOL/Decision_Procs/ferrante_rackoff.ML Sun Mar 16 09:11:17 2025 +0100
+++ b/src/HOL/Decision_Procs/ferrante_rackoff.ML Sun Mar 16 12:03:47 2025 +0000
@@ -161,7 +161,7 @@
val qe_th = Drule.implies_elim_list
((fconv_rule (Thm.beta_conversion true))
(Thm.instantiate' [] (map SOME [cU, qx, get_p1 minf_th, get_p1 pinf_th])
- qe))
+ (mk_meta_eq qe)))
[fU, ld_th, nmi_th, npi_th, minf_th, pinf_th]
val bex_conv =
Simplifier.rewrite (put_simpset HOL_basic_ss ctxt addsimps @{thms simp_thms bex_simps(1-5)})