--- a/src/HOL/Bit_Operations.thy Sun Mar 16 15:04:59 2025 +0100
+++ b/src/HOL/Bit_Operations.thy Mon Mar 17 09:00:40 2025 +0100
@@ -338,6 +338,57 @@
\<open>bit (a mod 2) n \<longleftrightarrow> n = 0 \<and> odd a\<close>
by (simp add: mod_2_eq_odd bit_simps)
+lemma stable_index:
+ obtains m where \<open>possible_bit TYPE('a) m\<close>
+ \<open>\<And>n. possible_bit TYPE('a) n \<Longrightarrow> n \<ge> m \<Longrightarrow> bit a n \<longleftrightarrow> bit a m\<close>
+proof -
+ have \<open>\<exists>m. possible_bit TYPE('a) m \<and> (\<forall>n\<ge>m. possible_bit TYPE('a) n \<longrightarrow> bit a n \<longleftrightarrow> bit a m)\<close>
+ proof (induction a rule: bit_induct)
+ case (stable a)
+ show ?case
+ by (rule exI [of _ \<open>0::nat\<close>]) (simp add: stable_imp_bit_iff_odd stable)
+ next
+ case (rec a b)
+ then obtain m where \<open>possible_bit TYPE('a) m\<close>
+ and hyp: \<open>\<And>n. possible_bit TYPE('a) n \<Longrightarrow> n \<ge> m \<Longrightarrow> bit a n \<longleftrightarrow> bit a m\<close>
+ by blast
+ show ?case
+ proof (cases \<open>possible_bit TYPE('a) (Suc m)\<close>)
+ case True
+ moreover have \<open>bit (of_bool b + 2 * a) n \<longleftrightarrow> bit (of_bool b + 2 * a) (Suc m)\<close>
+ if \<open>possible_bit TYPE('a) n\<close> \<open>Suc m \<le> n\<close> for n
+ using hyp [of \<open>n - 1\<close>] possible_bit_less_imp [of n \<open>n - 1\<close>] rec.hyps that
+ by (cases n) (simp_all add: bit_Suc)
+ ultimately show ?thesis
+ by blast
+ next
+ case False
+ have \<open>bit (of_bool b + 2 * a) n \<longleftrightarrow> bit (of_bool b + 2 * a) m\<close>
+ if \<open>possible_bit TYPE('a) n\<close> \<open>m \<le> n\<close> for n
+ proof (cases \<open>m = n\<close>)
+ case True
+ then show ?thesis
+ by simp
+ next
+ case False
+ with \<open>m \<le> n\<close> have \<open>m < n\<close>
+ by simp
+ with \<open>\<not> possible_bit TYPE('a) (Suc m)\<close>
+ have \<open>\<not> possible_bit TYPE('a) n\<close> using possible_bit_less_imp [of n \<open>Suc m\<close>]
+ by auto
+ with \<open>possible_bit TYPE('a) n\<close>
+ show ?thesis
+ by simp
+ qed
+ with \<open>possible_bit TYPE('a) m\<close> show ?thesis
+ by blast
+ qed
+ qed
+ with that show thesis
+ by blast
+qed
+
+
end
lemma nat_bit_induct [case_names zero even odd]:
@@ -1105,6 +1156,20 @@
qed
qed
+lemma impossible_bit_imp_take_bit_eq_self:
+ \<open>take_bit n a = a\<close> if \<open>\<not> possible_bit TYPE('a) n\<close>
+proof -
+ have \<open>drop_bit n a = 0\<close>
+ proof (rule bit_eqI)
+ fix m
+ show \<open>bit (drop_bit n a) m \<longleftrightarrow> bit 0 m\<close>
+ using possible_bit_less_imp [of \<open>n + m\<close> n] that
+ by (auto simp add: bit_simps dest: bit_imp_possible_bit)
+ qed
+ then show ?thesis
+ by (simp add: take_bit_eq_self_iff_drop_bit_eq_0)
+qed
+
lemma drop_bit_exp_eq:
\<open>drop_bit m (2 ^ n) = of_bool (m \<le> n \<and> possible_bit TYPE('a) n) * 2 ^ (n - m)\<close>
by (auto simp: bit_eq_iff bit_simps)
@@ -1486,6 +1551,11 @@
\<open>take_bit m (NOT (mask n)) = 0\<close> if \<open>n \<ge> m\<close>
by (rule bit_eqI) (use that in \<open>simp add: bit_take_bit_iff bit_not_iff bit_mask_iff\<close>)
+lemma mask_eq_minus_one_if_not_possible_bit:
+ \<open>mask n = - 1\<close> if \<open>\<not> possible_bit TYPE('a) n\<close>
+ using that mask_eq_take_bit_minus_one [of n] impossible_bit_imp_take_bit_eq_self [of n \<open>- 1\<close>]
+ by simp
+
lemma unset_bit_eq_and_not:
\<open>unset_bit n a = a AND NOT (push_bit n 1)\<close>
by (rule bit_eqI) (auto simp: bit_simps)
--- a/src/HOL/Decision_Procs/Algebra_Aux.thy Sun Mar 16 15:04:59 2025 +0100
+++ b/src/HOL/Decision_Procs/Algebra_Aux.thy Mon Mar 17 09:00:40 2025 +0100
@@ -259,10 +259,12 @@
by (simp add: cring_class_ops_def)
lemma uminus_class: "\<ominus>\<^bsub>cring_class_ops\<^esub> x = - x"
- apply (simp add: a_inv_def m_inv_def cring_class_ops_def)
- apply (rule the_equality)
- apply (simp_all add: eq_neg_iff_add_eq_0)
- done
+proof -
+ have "(THE y::'a. x + y = 0 \<and> y + x = 0) = - x"
+ by (rule the_equality) (simp_all add: eq_neg_iff_add_eq_0)
+ then show ?thesis
+ by (simp add: a_inv_def m_inv_def cring_class_ops_def)
+qed
lemma minus_class: "x \<ominus>\<^bsub>cring_class_ops\<^esub> y = x - y"
by (simp add: a_minus_def carrier_class plus_class uminus_class)
@@ -482,20 +484,11 @@
lemma field_class: "field (cring_class_ops::'a::field ring)"
apply unfold_locales
apply (simp_all add: cring_class_ops_def)
- apply (auto simp add: Units_def)
- apply (rule_tac x="1 / x" in exI)
- apply simp
- done
+ using field_class.field_inverse by (force simp add: Units_def)
lemma div_class: "(x::'a::field) \<oslash>\<^bsub>cring_class_ops\<^esub> y = x / y"
- apply (simp add: m_div_def m_inv_def class_simps)
- apply (rule impI)
- apply (rule ssubst [OF the_equality, of _ "1 / y"])
- apply simp_all
- apply (drule conjunct2)
- apply (drule_tac f="\<lambda>x. x / y" in arg_cong)
- apply simp
- done
+ by (simp add: carrier_class class_simps cring_class.comm_inv_char
+ field_class.field_divide_inverse m_div_def)
interpretation field_class: field "cring_class_ops::'a::field ring"
rewrites "(\<zero>\<^bsub>cring_class_ops\<^esub>::'a) = 0"
--- a/src/HOL/Decision_Procs/Approximation_Bounds.thy Sun Mar 16 15:04:59 2025 +0100
+++ b/src/HOL/Decision_Procs/Approximation_Bounds.thy Mon Mar 17 09:00:40 2025 +0100
@@ -2648,10 +2648,7 @@
thus ?thesis
unfolding bl_def[symmetric] using \<open>0 < real_of_int m\<close> \<open>0 \<le> bl\<close>
apply (simp add: ln_mult)
- apply (cases "e=0")
- apply (cases "bl = 0", simp_all add: powr_minus ln_inverse ln_powr)
- apply (cases "bl = 0", simp_all add: powr_minus ln_inverse ln_powr field_simps)
- done
+ by argo
next
case False
hence "0 < -e" by auto
@@ -2788,21 +2785,23 @@
using abs_real_le_2_powr_bitlen [of m] \<open>m > 0\<close>
by (simp_all add: bitlen powr_realpow [symmetric] powr_minus powr_add field_simps)
{
- have "float_round_down prec (lb_ln2 prec * ?s) \<le> ln 2 * (e + (bitlen m - 1))"
- (is "real_of_float ?lb2 \<le> _")
- apply (rule float_round_down_le)
- unfolding nat_0 power_0 mult_1_right times_float.rep_eq
- using lb_ln2[of prec]
+ have "real_of_float (lb_ln2 prec) *
+ real_of_float (Float (e + (bitlen m - 1)) 0)
+ \<le> ln 2 * real_of_int (e + (bitlen m - 1))"
proof (rule mult_mono)
from float_gt1_scale[OF \<open>1 \<le> Float m e\<close>]
show "0 \<le> real_of_float (Float (e + (bitlen m - 1)) 0)" by simp
- qed auto
- moreover
+ qed (use lb_ln2[of prec] in auto)
+ then have "float_round_down prec (lb_ln2 prec * ?s) \<le> ln 2 * (e + (bitlen m - 1))"
+ (is "real_of_float ?lb2 \<le> _")
+ by (simp add: Interval_Float.float_round_down_le)
+ moreover
from ln_float_bounds(1)[OF x_bnds]
have "float_round_down prec ((?x - 1) * lb_ln_horner prec (get_even prec) 1 (?x - 1)) \<le> ln ?x" (is "real_of_float ?lb_horner \<le> _")
by (auto intro!: float_round_down_le)
ultimately have "float_plus_down prec ?lb2 ?lb_horner \<le> ln x"
- unfolding Float ln_shifted_float[OF \<open>0 < m\<close>, of e] by (auto intro!: float_plus_down_le)
+ unfolding Float ln_shifted_float[OF \<open>0 < m\<close>, of e]
+ by (auto intro!: float_plus_down_le)
}
moreover
{
--- a/src/HOL/Decision_Procs/Cooper.thy Sun Mar 16 15:04:59 2025 +0100
+++ b/src/HOL/Decision_Procs/Cooper.thy Mon Mar 17 09:00:40 2025 +0100
@@ -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 15:04:59 2025 +0100
+++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy Mon Mar 17 09:00:40 2025 +0100
@@ -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
@@ -918,6 +661,21 @@
else ("Nox",[])
| t => if t aconv Thm.term_of x then ("x",[]) else ("Nox",[]);
+local
+val sum_lt = mk_meta_eq @{thm sum_lt}
+val sum_le = mk_meta_eq @{thm sum_le}
+val sum_eq = mk_meta_eq @{thm sum_eq}
+val neg_prod_sum_lt = mk_meta_eq @{thm neg_prod_sum_lt}
+val pos_prod_sum_lt = mk_meta_eq @{thm pos_prod_sum_lt}
+val neg_prod_sum_le = mk_meta_eq @{thm neg_prod_sum_le}
+val pos_prod_sum_le = mk_meta_eq @{thm pos_prod_sum_le}
+val neg_prod_lt = mk_meta_eq @{thm neg_prod_lt}
+val pos_prod_lt = mk_meta_eq @{thm pos_prod_lt}
+val neg_prod_le = mk_meta_eq @{thm neg_prod_le}
+val pos_prod_le = mk_meta_eq @{thm pos_prod_le}
+val nz_prod_sum_eq = mk_meta_eq @{thm nz_prod_sum_eq}
+val nz_prod_eq = mk_meta_eq @{thm nz_prod_eq}
+in
fun xnormalize_conv ctxt [] ct = Thm.reflexive ct
| xnormalize_conv ctxt (vs as (x::_)) ct =
case Thm.term_of ct of
@@ -935,14 +693,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
+ (if neg then neg_prod_sum_lt else 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] 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 +716,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
+ (if neg then neg_prod_lt else pos_prod_lt)) cth
val rth = th
in rth end
| _ => Thm.reflexive ct)
@@ -980,14 +738,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
+ (if neg then neg_prod_sum_le else 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] 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 +763,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
+ (if neg then neg_prod_le else pos_prod_le)) cth
val rth = th
in rth end
| _ => Thm.reflexive ct)
@@ -1023,14 +781,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]) 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] 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,9 +803,10 @@
(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]) nz_prod_eq) cth
in rth end
| _ => Thm.reflexive ct);
+end
local
val less_iff_diff_less_0 = mk_meta_eq @{thm "less_iff_diff_less_0"}
--- a/src/HOL/Decision_Procs/Ferrack.thy Sun Mar 16 15:04:59 2025 +0100
+++ b/src/HOL/Decision_Procs/Ferrack.thy Mon Mar 17 09:00:40 2025 +0100
@@ -1021,10 +1021,8 @@
qed (auto simp add: disj_def imp_def iff_def conj_def)
lemma simpfm_qf: "qfree p \<Longrightarrow> qfree (simpfm p)"
- apply (induct p rule: simpfm.induct)
- apply (auto simp add: Let_def)
- apply (case_tac "simpnum a", auto)+
- done
+ by (induct p rule: simpfm.induct) (auto simp: Let_def split: num.splits)
+
fun prep :: "fm \<Rightarrow> fm"
where
@@ -1256,17 +1254,11 @@
proof (induct p rule: minusinf.induct)
case (1 p q)
then show ?case
- apply auto
- apply (rule_tac x= "min z za" in exI)
- apply auto
- done
+ by (fastforce simp: intro: exI [where x= "min _ _"])
next
case (2 p q)
then show ?case
- apply auto
- apply (rule_tac x= "min z za" in exI)
- apply auto
- done
+ by (fastforce simp: intro: exI [where x= "min _ _"])
next
case (3 c e)
from 3 have nb: "numbound0 e" by simp
@@ -1386,17 +1378,11 @@
proof (induct p rule: isrlfm.induct)
case (1 p q)
then show ?case
- apply auto
- apply (rule_tac x= "max z za" in exI)
- apply auto
- done
+ by (fastforce simp: intro: exI [where x= "max _ _"])
next
case (2 p q)
then show ?case
- apply auto
- apply (rule_tac x= "max z za" in exI)
- apply auto
- done
+ by (fastforce simp: intro: exI [where x= "max _ _"])
next
case (3 c e)
from 3 have nb: "numbound0 e" by simp
@@ -2195,12 +2181,7 @@
\<in> (\<lambda>((t, n), s, m). (Inum (x # bs) t / real_of_int n + Inum (x # bs) s / real_of_int m) / 2) `
(set U \<times> set U)"
using mnz nnz th
- apply (auto simp add: th add_divide_distrib algebra_simps split_def image_def)
- apply (rule_tac x="(s,m)" in bexI)
- apply simp_all
- apply (rule_tac x="(t,n)" in bexI)
- apply (simp_all add: mult.commute)
- done
+ by (force simp add: th add_divide_distrib algebra_simps split_def image_def)
next
fix t n s m
assume tnU: "(t, n) \<in> set U" and smU: "(s, m) \<in> set U"
@@ -2271,10 +2252,7 @@
from tnU smU UU' have "?g ((t, n), (s, m)) \<in> ?f ` U'"
by blast
then have "\<exists>(t',n') \<in> U'. ?g ((t, n), (s, m)) = ?f (t', n')"
- apply auto
- apply (rule_tac x="(a, b)" in bexI)
- apply auto
- done
+ by fastforce
then obtain t' n' where tnU': "(t',n') \<in> U'" and th: "?g ((t, n), (s, m)) = ?f (t', n')"
by blast
from U' tnU' have tnb': "numbound0 t'" and np': "real_of_int n' > 0"
@@ -2296,10 +2274,7 @@
from tnU' UU' have "?f (t', n') \<in> ?g ` (U \<times> U)"
by blast
then have "\<exists>((t,n),(s,m)) \<in> U \<times> U. ?f (t', n') = ?g ((t, n), (s, m))"
- apply auto
- apply (rule_tac x="(a,b)" in bexI)
- apply auto
- done
+ by force
then obtain t n s m where tnU: "(t, n) \<in> U" and smU: "(s, m) \<in> U" and
th: "?f (t', n') = ?g ((t, n), (s, m))"
by blast
@@ -2361,10 +2336,7 @@
from that have "(t,n) \<in> set ?SS"
by simp
then have "\<exists>(t',n') \<in> set ?S. simp_num_pair (t', n') = (t, n)"
- apply (auto simp add: split_def simp del: map_map)
- apply (rule_tac x="((aa,ba),(ab,bb))" in bexI)
- apply simp_all
- done
+ by (force simp add: split_def simp del: map_map)
then obtain t' n' where tn'S: "(t', n') \<in> set ?S" and tns: "simp_num_pair (t', n') = (t, n)"
by blast
from tn'S Snb have tnb: "numbound0 t'" and np: "n' > 0"
--- a/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy Sun Mar 16 15:04:59 2025 +0100
+++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy Mon Mar 17 09:00:40 2025 +0100
@@ -860,11 +860,17 @@
case (1 c p n)
then have pn: "isnpolyh p n" by simp
from 1(1)[OF pn]
- have th:"Ipoly bs (Add (Mul (head p) (Pw (Bound 0) (degree p))) (behead p)) = Ipoly bs p" .
- then show ?case using "1.hyps"
- apply (simp add: Let_def,cases "behead p = 0\<^sub>p")
- apply (simp_all add: th[symmetric] field_simps)
- done
+ have *: "Ipoly bs (Add (Mul (head p) (Pw (Bound 0) (degree p))) (behead p)) = Ipoly bs p" .
+ show ?case
+ proof (cases "behead p = 0\<^sub>p")
+ case True
+ then show ?thesis
+ using * by auto
+ next
+ case False
+ then show ?thesis
+ by (simp add: field_simps flip: *)
+ qed
qed (auto simp add: Let_def)
lemma behead_isnpolyh:
@@ -1011,7 +1017,7 @@
lemma isnpolyh_Suc_const: "isnpolyh p (Suc n) \<Longrightarrow> isconstant p"
by (simp add: isconstant_polybound0 isnpolyh_polybound0)
-lemma wf_bs_polyadd: "wf_bs bs p \<and> wf_bs bs q \<longrightarrow> wf_bs bs (p +\<^sub>p q)"
+lemma wf_bs_polyadd: "\<lbrakk>wf_bs bs p; wf_bs bs q\<rbrakk> \<Longrightarrow> wf_bs bs (p +\<^sub>p q)"
by (induct p q rule: polyadd.induct) (auto simp add: Let_def wf_bs_def)
lemma wf_bs_polyul: "wf_bs bs p \<Longrightarrow> wf_bs bs q \<Longrightarrow> wf_bs bs (p *\<^sub>p q)"
@@ -1019,7 +1025,7 @@
case (4 c n p c' n' p')
then show ?case
apply (simp add: wf_bs_def)
- by (metis Suc_eq_plus1 max.bounded_iff max_0L maxindex.simps(2) maxindex.simps(8) wf_bs_def wf_bs_polyadd)
+ by (metis "4.prems"(1) max.bounded_iff max_0L maxindex.simps(2,8) wf_bs_def wf_bs_polyadd)
qed (simp_all add: wf_bs_def)
lemma wf_bs_polyneg: "wf_bs bs p \<Longrightarrow> wf_bs bs (~\<^sub>p p)"
@@ -1600,9 +1606,8 @@
show ?ths
proof (cases "s = 0\<^sub>p")
case True
- with np show ?thesis
- apply (clarsimp simp: polydivide_aux.simps)
- by (metis polyadd_0(1) polymul_0(1) zero_normh)
+ with np polyadd_0 polymul_0 zero_normh show ?thesis
+ by (metis degree.simps(2) nakk' polydivide_aux.simps prod.sel order.refl)
next
case sz: False
show ?thesis
@@ -1711,10 +1716,7 @@
by (simp add: h1)
with sp'[symmetric] ns np nxdn polyadd_0(1)[OF polymul_normh[OF np nxdn]]
polyadd_0(2)[OF polymul_normh[OF np nxdn]] show ?thesis
- apply auto
- apply (rule exI[where x="?xdn"])
- apply (auto simp add: polymul_commute[of p])
- done
+ using polymul_commute by auto
qed
then show ?thesis by blast
qed
--- a/src/HOL/Decision_Procs/ferrante_rackoff.ML Sun Mar 16 15:04:59 2025 +0100
+++ b/src/HOL/Decision_Procs/ferrante_rackoff.ML Mon Mar 17 09:00:40 2025 +0100
@@ -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)})