--- a/src/HOL/BNF_Wellorder_Constructions.thy Fri Jul 15 09:18:21 2022 +0200
+++ b/src/HOL/BNF_Wellorder_Constructions.thy Fri Jul 22 14:39:56 2022 +0200
@@ -106,12 +106,22 @@
lemma ofilter_Restr_under:
assumes WELL: "Well_order r" and OF: "wo_rel.ofilter r A" and IN: "a \<in> A"
shows "under (Restr r A) a = under r a"
-using assms wo_rel_def
-proof(auto simp add: wo_rel.ofilter_def under_def)
- fix b assume *: "a \<in> A" and "(b,a) \<in> r"
- hence "b \<in> under r a \<and> a \<in> Field r"
- unfolding under_def using Field_def by fastforce
- thus "b \<in> A" using * assms by (auto simp add: wo_rel_def wo_rel.ofilter_def)
+ unfolding wo_rel.ofilter_def under_def
+proof
+ show "{b. (b, a) \<in> Restr r A} \<subseteq> {b. (b, a) \<in> r}"
+ by auto
+next
+ have "under r a \<subseteq> A"
+ proof
+ fix x
+ assume *: "x \<in> under r a"
+ then have "a \<in> Field r"
+ unfolding under_def using Field_def by fastforce
+ then show "x \<in> A" using IN assms *
+ by (auto simp add: wo_rel_def wo_rel.ofilter_def)
+ qed
+ then show "{b. (b, a) \<in> r} \<subseteq> {b. (b, a) \<in> Restr r A}"
+ unfolding under_def using assms by auto
qed
lemma ofilter_embed:
@@ -120,12 +130,13 @@
proof
assume *: "wo_rel.ofilter r A"
show "A \<le> Field r \<and> embed (Restr r A) r id"
- proof(unfold embed_def, auto)
+ unfolding embed_def
+ proof safe
fix a assume "a \<in> A" thus "a \<in> Field r" using assms *
by (auto simp add: wo_rel_def wo_rel.ofilter_def)
next
fix a assume "a \<in> Field (Restr r A)"
- thus "bij_betw id (under (Restr r A) a) (under r a)" using assms *
+ thus "bij_betw id (under (Restr r A) a) (under r (id a))" using assms *
by (simp add: ofilter_Restr_under Field_Restr_ofilter)
qed
next
@@ -160,7 +171,8 @@
by (simp add: Well_order_Restr wo_rel_def)
(* Main proof *)
show ?thesis using WellB assms
- proof(auto simp add: wo_rel.ofilter_def under_def)
+ unfolding wo_rel.ofilter_def under_def ofilter_def
+ proof safe
fix a assume "a \<in> A" and *: "a \<in> B"
hence "a \<in> Field r" using OFA Well by (auto simp add: wo_rel.ofilter_def)
with * show "a \<in> Field ?rB" using Field by auto
@@ -714,7 +726,7 @@
lemma ordLess_iff_ordIso_Restr:
assumes WELL: "Well_order r" and WELL': "Well_order r'"
shows "(r' <o r) = (\<exists>a \<in> Field r. r' =o Restr r (underS r a))"
-proof(auto)
+proof safe
fix a assume *: "a \<in> Field r" and **: "r' =o Restr r (underS r a)"
hence "Restr r (underS r a) <o r" using WELL underS_Restr_ordLess[of r] by blast
thus "r' <o r" using ** ordIso_ordLess_trans by blast
@@ -779,7 +791,7 @@
lemma ordLeq_iff_ordLess_Restr:
assumes WELL: "Well_order r" and WELL': "Well_order r'"
shows "(r \<le>o r') = (\<forall>a \<in> Field r. Restr r (underS r a) <o r')"
-proof(auto)
+proof safe
assume *: "r \<le>o r'"
fix a assume "a \<in> Field r"
hence "Restr r (underS r a) <o r"
@@ -932,7 +944,8 @@
lemma trans_dir_image:
assumes TRANS: "trans r" and INJ: "inj_on f (Field r)"
shows "trans(dir_image r f)"
-proof(unfold trans_def, auto)
+unfolding trans_def
+proof safe
fix a' b' c'
assume "(a',b') \<in> dir_image r f" "(b',c') \<in> dir_image r f"
then obtain a b1 b2 c where 1: "a' = f a \<and> b' = f b1 \<and> b' = f b2 \<and> c' = f c" and
@@ -953,7 +966,8 @@
lemma antisym_dir_image:
assumes AN: "antisym r" and INJ: "inj_on f (Field r)"
shows "antisym(dir_image r f)"
-proof(unfold antisym_def, auto)
+unfolding antisym_def
+proof safe
fix a' b'
assume "(a',b') \<in> dir_image r f" "(b',a') \<in> dir_image r f"
then obtain a1 b1 a2 b2 where 1: "a' = f a1 \<and> a' = f a2 \<and> b' = f b1 \<and> b' = f b2" and
@@ -1096,7 +1110,7 @@
qed
next
show "Field r \<times> Field r \<le> Field (bsqr r)"
- proof(auto)
+ proof safe
fix a1 a2 assume "a1 \<in> Field r" and "a2 \<in> Field r"
hence "((a1,a2),(a1,a2)) \<in> bsqr r" unfolding bsqr_def by blast
thus "(a1,a2) \<in> Field (bsqr r)" unfolding Field_def by auto
@@ -1109,7 +1123,8 @@
lemma bsqr_Trans:
assumes "Well_order r"
shows "trans (bsqr r)"
-proof(unfold trans_def, auto)
+unfolding trans_def
+proof safe
(* Preliminary facts *)
have Well: "wo_rel r" using assms wo_rel_def by auto
hence Trans: "trans r" using wo_rel.TRANS by auto
@@ -1573,12 +1588,11 @@
lemma bij_betw_curr:
"bij_betw (curr A) (Func (A \<times> B) C) (Func A (Func B C))"
-unfolding bij_betw_def inj_on_def image_def
-apply (intro impI conjI ballI)
-apply (erule curr_inj[THEN iffD1], assumption+)
-apply auto
-apply (erule curr_in)
-using curr_surj by blast
+ unfolding bij_betw_def inj_on_def image_def
+ apply (intro impI conjI ballI)
+ apply (erule curr_inj[THEN iffD1], assumption+, safe)
+ using curr_surj curr_in apply blast+
+ done
definition Func_map where
"Func_map B2 f1 f2 g b2 \<equiv> if b2 \<in> B2 then f1 (g (f2 b2)) else undefined"
@@ -1661,7 +1675,7 @@
using j2A2 B1 A2 unfolding j1_def by (fast intro: inv_into_into)+
ultimately show "h \<in> Func_map B2 f1 f2 ` Func A2 A1"
unfolding Func_map_def[abs_def] by auto
- qed(insert B1 Func_map[OF _ _ A2(2)], auto)
+ qed(use B1 Func_map[OF _ _ A2(2)] in auto)
qed
end
--- a/src/HOL/BNF_Wellorder_Relation.thy Fri Jul 15 09:18:21 2022 +0200
+++ b/src/HOL/BNF_Wellorder_Relation.thy Fri Jul 22 14:39:56 2022 +0200
@@ -220,27 +220,26 @@
shows "\<exists>b. isMinim B b"
proof-
from spec[OF WF[unfolded wf_eq_minimal[of "r - Id"]], of B] NE obtain b where
- *: "b \<in> B \<and> (\<forall>b'. b' \<noteq> b \<and> (b',b) \<in> r \<longrightarrow> b' \<notin> B)" by auto
- show ?thesis
- proof(simp add: isMinim_def, rule exI[of _ b], auto)
- show "b \<in> B" using * by simp
- next
- fix b' assume As: "b' \<in> B"
- hence **: "b \<in> Field r \<and> b' \<in> Field r" using As SUB * by auto
- (* *)
- from As * have "b' = b \<or> (b',b) \<notin> r" by auto
- moreover
- {assume "b' = b"
- hence "(b,b') \<in> r"
- using ** REFL by (auto simp add: refl_on_def)
- }
- moreover
- {assume "b' \<noteq> b \<and> (b',b) \<notin> r"
- hence "(b,b') \<in> r"
- using ** TOTAL by (auto simp add: total_on_def)
- }
- ultimately show "(b,b') \<in> r" by blast
+ *: "b \<in> B \<and> (\<forall>b'. b' \<noteq> b \<and> (b',b) \<in> r \<longrightarrow> b' \<notin> B)" by auto
+ have "\<forall>b'. b' \<in> B \<longrightarrow> (b, b') \<in> r"
+ proof
+ fix b'
+ show "b' \<in> B \<longrightarrow> (b, b') \<in> r"
+ proof
+ assume As: "b' \<in> B"
+ hence **: "b \<in> Field r \<and> b' \<in> Field r" using As SUB * by auto
+ from As * have "b' = b \<or> (b',b) \<notin> r" by auto
+ moreover have "b' = b \<Longrightarrow> (b, b') \<in> r"
+ using ** REFL by (auto simp add: refl_on_def)
+ moreover have "b' \<noteq> b \<and> (b',b) \<notin> r \<Longrightarrow> (b,b') \<in> r"
+ using ** TOTAL by (auto simp add: total_on_def)
+ ultimately show "(b,b') \<in> r" by blast
+ qed
qed
+ then have "isMinim B b"
+ unfolding isMinim_def using * by auto
+ then show ?thesis
+ by auto
qed
lemma minim_isMinim:
@@ -395,16 +394,22 @@
lemma under_ofilter:
"ofilter (under a)"
-proof(unfold ofilter_def under_def, auto simp add: Field_def)
- fix aa x
- assume "(aa,a) \<in> r" "(x,aa) \<in> r"
- thus "(x,a) \<in> r"
- using TRANS trans_def[of r] by blast
+proof -
+ have "\<And>aa x. (aa, a) \<in> r \<Longrightarrow> (x, aa) \<in> r \<Longrightarrow> (x, a) \<in> r"
+ proof -
+ fix aa x
+ assume "(aa,a) \<in> r" "(x,aa) \<in> r"
+ then show "(x,a) \<in> r"
+ using TRANS trans_def[of r] by blast
+ qed
+ then show ?thesis unfolding ofilter_def under_def
+ by (auto simp add: Field_def)
qed
lemma underS_ofilter:
"ofilter (underS a)"
-proof(unfold ofilter_def underS_def under_def, auto simp add: Field_def)
+ unfolding ofilter_def underS_def under_def
+proof safe
fix aa assume "(a, aa) \<in> r" "(aa, a) \<in> r" and DIFF: "aa \<noteq> a"
thus False
using ANTISYM antisym_def[of r] by blast
@@ -412,7 +417,13 @@
fix aa x
assume "(aa,a) \<in> r" "aa \<noteq> a" "(x,aa) \<in> r"
thus "(x,a) \<in> r"
- using TRANS trans_def[of r] by blast
+ using TRANS trans_def[of r] by blast
+next
+ fix x
+ assume "x \<noteq> a" and "(x, a) \<in> r"
+ then show "x \<in> Field r"
+ unfolding Field_def
+ by auto
qed
lemma Field_ofilter:
@@ -430,7 +441,7 @@
let ?One = "(\<exists>a\<in>Field r. A = underS a)"
let ?Two = "(A = Field r)"
show "?One \<or> ?Two"
- proof(cases ?Two, simp)
+ proof(cases ?Two)
let ?B = "(Field r) - A"
let ?a = "minim ?B"
assume "A \<noteq> Field r"
@@ -445,7 +456,7 @@
have "A = underS ?a"
proof
show "A \<le> underS ?a"
- proof(unfold underS_def, auto simp add: 4)
+ proof
fix x assume **: "x \<in> A"
hence 11: "x \<in> Field r" using 5 by auto
have 12: "x \<noteq> ?a" using 4 ** by auto
@@ -458,25 +469,32 @@
hence "?a \<in> A" using ** 13 by blast
with 4 have False by simp
}
- thus "(x,?a) \<in> r" by blast
+ then have "(x,?a) \<in> r" by blast
+ thus "x \<in> underS ?a"
+ unfolding underS_def by (auto simp add: 12)
qed
next
show "underS ?a \<le> A"
- proof(unfold underS_def, auto)
+ proof
fix x
- assume **: "x \<noteq> ?a" and ***: "(x,?a) \<in> r"
- hence 11: "x \<in> Field r" using Field_def by fastforce
+ assume **: "x \<in> underS ?a"
+ hence 11: "x \<in> Field r"
+ using Field_def unfolding underS_def by fastforce
{assume "x \<notin> A"
hence "x \<in> ?B" using 11 by auto
hence "(?a,x) \<in> r" using 3 minim_least[of ?B x] by blast
hence False
- using ANTISYM antisym_def[of r] ** *** by auto
+ using ANTISYM antisym_def[of r] ** unfolding underS_def by auto
}
thus "x \<in> A" by blast
qed
qed
ultimately have ?One using 2 by blast
thus ?thesis by simp
+ next
+ assume "A = Field r"
+ then show ?thesis
+ by simp
qed
qed
--- a/src/HOL/Complete_Lattices.thy Fri Jul 15 09:18:21 2022 +0200
+++ b/src/HOL/Complete_Lattices.thy Fri Jul 22 14:39:56 2022 +0200
@@ -988,9 +988,9 @@
by blast
lemma disjnt_inj_on_iff:
- "\<lbrakk>inj_on f (\<Union>\<A>); X \<in> \<A>; Y \<in> \<A>\<rbrakk> \<Longrightarrow> disjnt (f ` X) (f ` Y) \<longleftrightarrow> disjnt X Y"
- apply (auto simp: disjnt_def)
- using inj_on_eq_iff by fastforce
+ "\<lbrakk>inj_on f (\<Union>\<A>); X \<in> \<A>; Y \<in> \<A>\<rbrakk> \<Longrightarrow> disjnt (f ` X) (f ` Y) \<longleftrightarrow> disjnt X Y"
+ unfolding disjnt_def
+ by safe (use inj_on_eq_iff in \<open>fastforce+\<close>)
lemma disjnt_Union1 [simp]: "disjnt (\<Union>\<A>) B \<longleftrightarrow> (\<forall>A \<in> \<A>. disjnt A B)"
by (auto simp: disjnt_def)
--- a/src/HOL/Conditionally_Complete_Lattices.thy Fri Jul 15 09:18:21 2022 +0200
+++ b/src/HOL/Conditionally_Complete_Lattices.thy Fri Jul 22 14:39:56 2022 +0200
@@ -522,31 +522,29 @@
assumes "a < b" and "P a" and "\<not> P b"
shows "\<exists>c. a \<le> c \<and> c \<le> b \<and> (\<forall>x. a \<le> x \<and> x < c \<longrightarrow> P x) \<and>
(\<forall>d. (\<forall>x. a \<le> x \<and> x < d \<longrightarrow> P x) \<longrightarrow> d \<le> c)"
-proof (rule exI [where x = "Sup {d. \<forall>x. a \<le> x \<and> x < d \<longrightarrow> P x}"], auto)
+proof (rule exI [where x = "Sup {d. \<forall>x. a \<le> x \<and> x < d \<longrightarrow> P x}"], safe)
show "a \<le> Sup {d. \<forall>c. a \<le> c \<and> c < d \<longrightarrow> P c}"
by (rule cSup_upper, auto simp: bdd_above_def)
(metis \<open>a < b\<close> \<open>\<not> P b\<close> linear less_le)
next
show "Sup {d. \<forall>c. a \<le> c \<and> c < d \<longrightarrow> P c} \<le> b"
- apply (rule cSup_least)
- apply auto
- apply (metis less_le_not_le)
- apply (metis \<open>a<b\<close> \<open>\<not> P b\<close> linear less_le)
- done
+ by (rule cSup_least)
+ (use \<open>a<b\<close> \<open>\<not> P b\<close> in \<open>auto simp add: less_le_not_le\<close>)
next
fix x
assume x: "a \<le> x" and lt: "x < Sup {d. \<forall>c. a \<le> c \<and> c < d \<longrightarrow> P c}"
show "P x"
- apply (rule less_cSupE [OF lt], auto)
- apply (metis less_le_not_le)
- apply (metis x)
- done
+ by (rule less_cSupE [OF lt]) (use less_le_not_le x in \<open>auto\<close>)
next
fix d
- assume 0: "\<forall>x. a \<le> x \<and> x < d \<longrightarrow> P x"
- thus "d \<le> Sup {d. \<forall>c. a \<le> c \<and> c < d \<longrightarrow> P c}"
- by (rule_tac cSup_upper, auto simp: bdd_above_def)
- (metis \<open>a<b\<close> \<open>\<not> P b\<close> linear less_le)
+ assume 0: "\<forall>x. a \<le> x \<and> x < d \<longrightarrow> P x"
+ then have "d \<in> {d. \<forall>c. a \<le> c \<and> c < d \<longrightarrow> P c}"
+ by auto
+ moreover have "bdd_above {d. \<forall>c. a \<le> c \<and> c < d \<longrightarrow> P c}"
+ unfolding bdd_above_def using \<open>a<b\<close> \<open>\<not> P b\<close> linear
+ by (simp add: less_le) blast
+ ultimately show "d \<le> Sup {d. \<forall>c. a \<le> c \<and> c < d \<longrightarrow> P c}"
+ by (auto simp: cSup_upper)
qed
end
--- a/src/HOL/Divides.thy Fri Jul 15 09:18:21 2022 +0200
+++ b/src/HOL/Divides.thy Fri Jul 22 14:39:56 2022 +0200
@@ -40,7 +40,7 @@
lemma unique_quotient_lemma_neg:
"b * q' + r' \<le> b*q + r \<Longrightarrow> r \<le> 0 \<Longrightarrow> b < r \<Longrightarrow> b < r' \<Longrightarrow> q \<le> (q'::int)"
- by (rule_tac b = "-b" and r = "-r'" and r' = "-r" in unique_quotient_lemma) auto
+ using unique_quotient_lemma[where b = "-b" and r = "-r'" and r'="-r"] by auto
lemma unique_quotient:
"eucl_rel_int a b (q, r) \<Longrightarrow> eucl_rel_int a b (q', r') \<Longrightarrow> q = q'"
@@ -50,11 +50,15 @@
done
lemma unique_remainder:
- "eucl_rel_int a b (q, r) \<Longrightarrow> eucl_rel_int a b (q', r') \<Longrightarrow> r = r'"
-apply (subgoal_tac "q = q'")
- apply (simp add: eucl_rel_int_iff)
-apply (blast intro: unique_quotient)
-done
+ assumes "eucl_rel_int a b (q, r)"
+ and "eucl_rel_int a b (q', r')"
+ shows "r = r'"
+proof -
+ have "q = q'"
+ using assms by (blast intro: unique_quotient)
+ then show "r = r'"
+ using assms by (simp add: eucl_rel_int_iff)
+qed
lemma eucl_rel_int:
"eucl_rel_int k l (k div l, k mod l)"
@@ -445,7 +449,7 @@
shows "i mod k = i \<longleftrightarrow> k = 0 \<or> 0 \<le> i \<and> i < k \<or> i \<le> 0 \<and> k < i"
proof -
have "i mod k = i \<longleftrightarrow> i div k = 0"
- by safe (insert div_mult_mod_eq [of i k], auto)
+ using div_mult_mod_eq [of i k] by safe auto
with zdiv_eq_0_iff
show ?thesis
by simp
@@ -482,17 +486,15 @@
by simp
next
case False
- moreover have \<open>0 < k mod l\<close> \<open>k mod l < 1 + l\<close>
- using \<open>0 < l\<close> le_imp_0_less False apply auto
- using le_less apply fastforce
- using pos_mod_bound [of l k] apply linarith
- done
- with \<open>l > 0\<close> have \<open>(k mod l - 1) mod l = k mod l - 1\<close>
+ moreover have 1: \<open>0 < k mod l\<close>
+ using \<open>0 < l\<close> False le_less by fastforce
+ moreover have 2: \<open>k mod l < 1 + l\<close>
+ using \<open>0 < l\<close> pos_mod_bound[of l k] by linarith
+ from 1 2 \<open>l > 0\<close> have \<open>(k mod l - 1) mod l = k mod l - 1\<close>
by (simp add: zmod_trivial_iff)
ultimately show ?thesis
- apply (simp only: zmod_zminus1_eq_if)
- apply (simp add: mod_eq_0_iff_dvd algebra_simps mod_simps)
- done
+ by (simp only: zmod_zminus1_eq_if)
+ (simp add: mod_eq_0_iff_dvd algebra_simps mod_simps)
qed
qed
@@ -581,9 +583,12 @@
for k l :: int
proof (cases "k = 0 \<or> l = 0")
case False
+ then have *: "k \<noteq> 0" "l \<noteq> 0"
+ by auto
+ then have "0 \<le> k div l \<Longrightarrow> \<not> k < 0 \<Longrightarrow> 0 \<le> l"
+ by (meson neg_imp_zdiv_neg_iff not_le not_less_iff_gr_or_eq)
then show ?thesis
- apply (auto simp add: pos_imp_zdiv_nonneg_iff neg_imp_zdiv_nonneg_iff)
- by (meson neg_imp_zdiv_neg_iff not_le not_less_iff_gr_or_eq)
+ using * by (auto simp add: pos_imp_zdiv_nonneg_iff neg_imp_zdiv_nonneg_iff)
qed auto
lemma mod_int_pos_iff:
@@ -672,7 +677,7 @@
lemma nat_mod_eq_lemma:
assumes "(x::nat) mod n = y mod n" and "y \<le> x"
shows "\<exists>q. x = y + n * q"
- using assms by (rule mod_eq_nat1E) rule
+ using assms by (rule mod_eq_nat1E) (rule exI)
lemma nat_mod_eq_iff: "(x::nat) mod n = y mod n \<longleftrightarrow> (\<exists>q1 q2. x + n * q1 = y + n * q2)"
(is "?lhs = ?rhs")
@@ -681,11 +686,25 @@
{assume xy: "x \<le> y"
from H have th: "y mod n = x mod n" by simp
from nat_mod_eq_lemma[OF th xy] have ?rhs
- apply clarify apply (rule_tac x="q" in exI) by (rule exI[where x="0"], simp)}
+ proof
+ fix q
+ assume "y = x + n * q"
+ then have "x + n * q = y + n * 0"
+ by simp
+ then show "\<exists>q1 q2. x + n * q1 = y + n * q2"
+ by blast
+ qed}
moreover
{assume xy: "y \<le> x"
from nat_mod_eq_lemma[OF H xy] have ?rhs
- apply clarify apply (rule_tac x="0" in exI) by (rule_tac x="q" in exI, simp)}
+ proof
+ fix q
+ assume "x = y + n * q"
+ then have "x + n * 0 = y + n * q"
+ by simp
+ then show "\<exists>q1 q2. x + n * q1 = y + n * q2"
+ by blast
+ qed}
ultimately show ?rhs using linear[of x y] by blast
next
assume ?rhs then obtain q1 q2 where q12: "x + n * q1 = y + n * q2" by blast
@@ -740,7 +759,7 @@
have mod_w: "a mod (2 * b) = a mod b + b * w"
by (simp add: w_def mod_mult2_eq ac_simps)
from assms w_exhaust have "w = 1"
- by (auto simp add: mod_w) (insert mod_less, auto)
+ using mod_less by (auto simp add: mod_w)
with mod_w have mod: "a mod (2 * b) = a mod b + b" by simp
have "2 * (a div (2 * b)) = a div b - w"
by (simp add: w_def div_mult2_eq minus_mod_eq_mult_div ac_simps)
--- a/src/HOL/Equiv_Relations.thy Fri Jul 15 09:18:21 2022 +0200
+++ b/src/HOL/Equiv_Relations.thy Fri Jul 22 14:39:56 2022 +0200
@@ -264,11 +264,10 @@
assume cd: "(c,d) \<in> r1"
then have "c \<in> A1" "d \<in> A1"
using \<open>equiv A1 r1\<close> by (auto elim!: equiv_type [THEN subsetD, THEN SigmaE2])
- with assms show "\<Union> (f c ` r2 `` {a}) = \<Union> (f d ` r2 `` {a})"
- proof (simp add: UN_equiv_class congruent2_implies_congruent)
- show "f c a = f d a"
- using assms cd unfolding congruent2_def equiv_def refl_on_def by blast
- qed
+ moreover have "f c a = f d a"
+ using assms cd unfolding congruent2_def equiv_def refl_on_def by blast
+ ultimately show "\<Union> (f c ` r2 `` {a}) = \<Union> (f d ` r2 `` {a})"
+ using assms by (simp add: UN_equiv_class congruent2_implies_congruent)
qed
lemma UN_equiv_class2:
@@ -368,7 +367,7 @@
assume ?lhs
then show ?rhs
unfolding proj_def quotient_def
- proof clarsimp
+ proof safe
fix y
assume y: "y \<in> A" and "r `` {x} = r `` {y}"
moreover have "y \<in> r `` {y}"
--- a/src/HOL/Euclidean_Division.thy Fri Jul 15 09:18:21 2022 +0200
+++ b/src/HOL/Euclidean_Division.thy Fri Jul 22 14:39:56 2022 +0200
@@ -99,7 +99,8 @@
with size_mult_mono'[OF assms(1), of b]
have eq: "euclidean_size (a * b) = euclidean_size b" by simp
have "a * b dvd b"
- by (rule dvd_euclidean_size_eq_imp_dvd [OF _ eq]) (insert assms, simp_all)
+ by (rule dvd_euclidean_size_eq_imp_dvd [OF _ eq])
+ (use assms in simp_all)
hence "a * b dvd 1 * b" by simp
with \<open>b \<noteq> 0\<close> have "is_unit a" by (subst (asm) dvd_times_right_cancel_iff)
with assms(3) show False by contradiction
@@ -108,7 +109,7 @@
lemma dvd_imp_size_le:
assumes "a dvd b" "b \<noteq> 0"
shows "euclidean_size a \<le> euclidean_size b"
- using assms by (auto elim!: dvdE simp: size_mult_mono)
+ using assms by (auto simp: size_mult_mono)
lemma dvd_proper_imp_size_less:
assumes "a dvd b" "\<not> b dvd a" "b \<noteq> 0"
@@ -139,7 +140,7 @@
lemma coprime_mod_left_iff [simp]:
"coprime (a mod b) b \<longleftrightarrow> coprime a b" if "b \<noteq> 0"
- by (rule; rule coprimeI)
+ by (rule iffI; rule coprimeI)
(use that in \<open>auto dest!: dvd_mod_imp_dvd coprime_common_divisor simp add: dvd_mod_iff\<close>)
lemma coprime_mod_right_iff [simp]:
--- a/src/HOL/Fields.thy Fri Jul 15 09:18:21 2022 +0200
+++ b/src/HOL/Fields.thy Fri Jul 22 14:39:56 2022 +0200
@@ -286,7 +286,7 @@
lemma inverse_nonzero_iff_nonzero [simp]:
"inverse a = 0 \<longleftrightarrow> a = 0"
- by rule (fact inverse_zero_imp_zero, simp)
+ by (rule iffI) (fact inverse_zero_imp_zero, simp)
lemma inverse_minus_eq [simp]:
"inverse (- a) = - inverse a"
@@ -519,7 +519,7 @@
lemma inverse_eq_1_iff [simp]:
"inverse x = 1 \<longleftrightarrow> x = 1"
- by (insert inverse_eq_iff_eq [of x 1], simp)
+ using inverse_eq_iff_eq [of x 1] by simp
lemma divide_eq_0_iff [simp]:
"a / b = 0 \<longleftrightarrow> a = 0 \<or> b = 0"
@@ -647,8 +647,8 @@
lemma negative_imp_inverse_negative:
"a < 0 \<Longrightarrow> inverse a < 0"
- by (insert positive_imp_inverse_positive [of "-a"],
- simp add: nonzero_inverse_minus_eq less_imp_not_eq)
+ using positive_imp_inverse_positive [of "-a"]
+ by (simp add: nonzero_inverse_minus_eq less_imp_not_eq)
lemma inverse_le_imp_le:
assumes invle: "inverse a \<le> inverse b" and apos: "0 < a"
--- a/src/HOL/Finite_Set.thy Fri Jul 15 09:18:21 2022 +0200
+++ b/src/HOL/Finite_Set.thy Fri Jul 22 14:39:56 2022 +0200
@@ -1226,7 +1226,7 @@
subsubsection \<open>Expressing set operations via \<^const>\<open>fold\<close>\<close>
lemma comp_fun_commute_const: "comp_fun_commute (\<lambda>_. f)"
- by standard rule
+ by standard (rule refl)
lemma comp_fun_idem_insert: "comp_fun_idem insert"
by standard auto
@@ -1571,7 +1571,7 @@
global_interpretation card: folding "\<lambda>_. Suc" 0
defines card = "folding_on.F (\<lambda>_. Suc) 0"
- by standard rule
+ by standard (rule refl)
lemma card_insert_disjoint: "finite A \<Longrightarrow> x \<notin> A \<Longrightarrow> card (insert x A) = Suc (card A)"
by (fact card.insert)
@@ -1824,11 +1824,12 @@
from "2.prems"(1,2,5) "2.hyps"(1,2) have cst: "card s \<le> card t"
by simp
from "2.prems"(3) [OF "2.hyps"(1) cst]
- obtain f where "f ` s \<subseteq> t" "inj_on f s"
+ obtain f where *: "f ` s \<subseteq> t" "inj_on f s"
by blast
- with "2.prems"(2) "2.hyps"(2) show ?case
- unfolding inj_on_def
- by (rule_tac x = "\<lambda>z. if z = x then y else f z" in exI) auto
+ let ?g = "(\<lambda>a. if a = x then y else f a)"
+ have "?g ` insert x s \<subseteq> insert y t \<and> inj_on ?g (insert x s)"
+ using * "2.prems"(2) "2.hyps"(2) unfolding inj_on_def by auto
+ then show ?case by (rule exI[where ?x="?g"])
qed
qed
@@ -2415,7 +2416,7 @@
by (simp add: fS)
have "\<lbrakk>x \<noteq> y; x \<in> S; z \<in> S; f x = f y\<rbrakk>
\<Longrightarrow> \<exists>x \<in> S. x \<noteq> y \<and> f z = f x" for z
- by (case_tac "z = y \<longrightarrow> z = x") auto
+ by (cases "z = y \<longrightarrow> z = x") auto
then show "T \<subseteq> f ` (S - {y})"
using h xy x y f by fastforce
qed
--- a/src/HOL/Fun.thy Fri Jul 15 09:18:21 2022 +0200
+++ b/src/HOL/Fun.thy Fri Jul 22 14:39:56 2022 +0200
@@ -377,28 +377,30 @@
lemma bij_betw_comp_iff2:
assumes bij: "bij_betw f' A' A''"
and img: "f ` A \<le> A'"
- shows "bij_betw f A A' \<longleftrightarrow> bij_betw (f' \<circ> f) A A''"
- using assms
-proof (auto simp add: bij_betw_comp_iff)
- assume *: "bij_betw (f' \<circ> f) A A''"
- then show "bij_betw f A A'"
- using img
- proof (auto simp add: bij_betw_def)
- assume "inj_on (f' \<circ> f) A"
- then show "inj_on f A"
- using inj_on_imageI2 by blast
+ shows "bij_betw f A A' \<longleftrightarrow> bij_betw (f' \<circ> f) A A''" (is "?L \<longleftrightarrow> ?R")
+proof
+ assume "?L"
+ then show "?R"
+ using assms by (auto simp add: bij_betw_comp_iff)
next
- fix a'
- assume **: "a' \<in> A'"
- with bij have "f' a' \<in> A''"
- unfolding bij_betw_def by auto
- with * obtain a where 1: "a \<in> A \<and> f' (f a) = f' a'"
- unfolding bij_betw_def by force
- with img have "f a \<in> A'" by auto
- with bij ** 1 have "f a = a'"
- unfolding bij_betw_def inj_on_def by auto
- with 1 show "a' \<in> f ` A" by auto
- qed
+ assume *: "?R"
+ have "inj_on (f' \<circ> f) A \<Longrightarrow> inj_on f A"
+ using inj_on_imageI2 by blast
+ moreover have "A' \<subseteq> f ` A"
+ proof
+ fix a'
+ assume **: "a' \<in> A'"
+ with bij have "f' a' \<in> A''"
+ unfolding bij_betw_def by auto
+ with * obtain a where 1: "a \<in> A \<and> f' (f a) = f' a'"
+ unfolding bij_betw_def by force
+ with img have "f a \<in> A'" by auto
+ with bij ** 1 have "f a = a'"
+ unfolding bij_betw_def inj_on_def by auto
+ with 1 show "a' \<in> f ` A" by auto
+ qed
+ ultimately show "?L"
+ using img * by (auto simp add: bij_betw_def)
qed
lemma bij_betw_inv:
@@ -425,7 +427,7 @@
from g [OF a1] a1 g [OF a2] a2 \<open>?g x = ?g y\<close> show "x = y" by simp
qed
moreover have "?g ` B = A"
- proof (auto simp: image_def)
+ proof safe
fix b
assume "b \<in> B"
with s obtain a where P: "?P b a" by blast
@@ -435,7 +437,9 @@
assume "a \<in> A"
with s obtain b where P: "?P b a" by blast
with s have "b \<in> B" by blast
- with g[OF P] show "\<exists>b\<in>B. a = ?g b" by blast
+ with g[OF P] have "\<exists>b\<in>B. a = ?g b" by blast
+ then show "a \<in> ?g ` B"
+ by auto
qed
ultimately show ?thesis
by (auto simp: bij_betw_def)
@@ -637,7 +641,7 @@
next
assume *: "bij_betw f (A \<union> {b}) (A' \<union> {f b})"
have "f ` A = A'"
- proof auto
+ proof safe
fix a
assume **: "a \<in> A"
then have "f a \<in> A' \<union> {f b}"
@@ -797,7 +801,6 @@
unfolding fun_upd_def
apply safe
apply (erule subst)
- apply (rule_tac [2] ext)
apply auto
done
@@ -903,12 +906,13 @@
"bij_betw f A B \<longleftrightarrow> (\<exists>g. (\<forall>x \<in> A. f x \<in> B \<and> g(f x) = x) \<and> (\<forall>y \<in> B. g y \<in> A \<and> f(g y) = y))"
(is "?lhs = ?rhs")
proof
- assume L: ?lhs
- then show ?rhs
- apply (rule_tac x="the_inv_into A f" in exI)
- apply (auto simp: bij_betw_def f_the_inv_into_f the_inv_into_f_f the_inv_into_into)
- done
-qed (force intro: bij_betw_byWitness)
+ show "?lhs \<Longrightarrow> ?rhs"
+ by (auto simp: bij_betw_def f_the_inv_into_f the_inv_into_f_f the_inv_into_into
+ exI[where ?x="the_inv_into A f"])
+next
+ show "?rhs \<Longrightarrow> ?lhs"
+ by (force intro: bij_betw_byWitness)
+qed
abbreviation the_inv :: "('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'a)"
where "the_inv f \<equiv> the_inv_into UNIV f"
@@ -1048,17 +1052,21 @@
lemma strict_mono_on_leD:
assumes "strict_mono_on A (f :: (_ :: linorder) \<Rightarrow> _ :: preorder)" "x \<in> A" "y \<in> A" "x \<le> y"
shows "f x \<le> f y"
-proof (insert le_less_linear[of y x], elim disjE)
- assume "x < y"
- with assms have "f x < f y" by (rule_tac strict_mono_onD[OF assms(1)]) simp_all
- thus ?thesis by (rule less_imp_le)
-qed (insert assms, simp)
+proof (cases "x = y")
+ case True
+ then show ?thesis by simp
+next
+ case False
+ with assms have "f x < f y"
+ using strict_mono_onD[OF assms(1)] by simp
+ then show ?thesis by (rule less_imp_le)
+qed
lemma strict_mono_on_eqD:
fixes f :: "(_ :: linorder) \<Rightarrow> (_ :: preorder)"
assumes "strict_mono_on A f" "f x = f y" "x \<in> A" "y \<in> A"
shows "y = x"
- using assms by (rule_tac linorder_cases[of x y]) (auto dest: strict_mono_onD)
+ using assms by (cases rule: linorder_cases) (auto dest: strict_mono_onD)
lemma strict_mono_on_imp_mono_on:
"strict_mono_on A (f :: (_ :: linorder) \<Rightarrow> _ :: preorder) \<Longrightarrow> mono_on A f"
--- a/src/HOL/Fun_Def.thy Fri Jul 15 09:18:21 2022 +0200
+++ b/src/HOL/Fun_Def.thy Fri Jul 22 14:39:56 2022 +0200
@@ -40,20 +40,14 @@
assumes ex1: "\<exists>!y. G x y"
assumes elm: "G x (h x)"
shows "h x = f x"
- apply (simp only: f_def)
- apply (rule THE_default1_equality [symmetric])
- apply (rule ex1)
- apply (rule elm)
- done
+ by (auto simp add: f_def ex1 elm THE_default1_equality[symmetric])
lemma fundef_ex1_iff:
assumes f_def: "f \<equiv> (\<lambda>x::'a. THE_default (d x) (\<lambda>y. G x y))"
assumes ex1: "\<exists>!y. G x y"
shows "(G x y) = (f x = y)"
- apply (auto simp:ex1 f_def THE_default1_equality)
- apply (rule THE_defaultI')
- apply (rule ex1)
- done
+ by (auto simp add: ex1 f_def THE_default1_equality THE_defaultI')
+
lemma fundef_default_value:
assumes f_def: "f \<equiv> (\<lambda>x::'a. THE_default (d x) (\<lambda>y. G x y))"
@@ -243,17 +237,33 @@
lemma max_ext_compat:
assumes "R O S \<subseteq> R"
shows "max_ext R O (max_ext S \<union> {({}, {})}) \<subseteq> max_ext R"
- using assms
- apply auto
- apply (elim max_ext.cases)
- apply rule
- apply auto[3]
- apply (drule_tac x=xa in meta_spec)
- apply simp
- apply (erule bexE)
- apply (drule_tac x=xb in meta_spec)
- apply auto
- done
+proof -
+ have "\<And>X Y Z. (X, Y) \<in> max_ext R \<Longrightarrow> (Y, Z) \<in> max_ext S \<Longrightarrow> (X, Z) \<in> max_ext R"
+ proof -
+ fix X Y Z
+ assume "(X,Y)\<in>max_ext R"
+ "(Y, Z)\<in>max_ext S"
+ then have *: "finite X" "finite Y" "finite Z" "Y\<noteq>{}" "Z\<noteq>{}"
+ "(\<And>x. x\<in>X \<Longrightarrow> \<exists>y\<in>Y. (x, y)\<in>R)"
+ "(\<And>y. y\<in>Y \<Longrightarrow> \<exists>z\<in>Z. (y, z)\<in>S)"
+ by (auto elim: max_ext.cases)
+ moreover have "\<And>x. x\<in>X \<Longrightarrow> \<exists>z\<in>Z. (x, z)\<in>R"
+ proof -
+ fix x
+ assume "x\<in>X"
+ then obtain y where 1: "y\<in>Y" "(x, y)\<in>R"
+ using * by auto
+ then obtain z where "z\<in>Z" "(y, z)\<in>S"
+ using * by auto
+ then show "\<exists>z\<in>Z. (x, z)\<in>R"
+ using assms 1 by (auto elim: max_ext.cases)
+ qed
+ ultimately show "(X,Z)\<in>max_ext R"
+ by auto
+ qed
+ then show "max_ext R O (max_ext S \<union> {({}, {})}) \<subseteq> max_ext R"
+ by auto
+qed
lemma max_rpair_set: "reduction_pair (max_strict, max_weak)"
unfolding max_strict_def max_weak_def
@@ -265,15 +275,25 @@
lemma min_ext_compat:
assumes "R O S \<subseteq> R"
- shows "min_ext R O (min_ext S \<union> {({},{})}) \<subseteq> min_ext R"
- using assms
- apply (auto simp: min_ext_def)
- apply (drule_tac x=ya in bspec, assumption)
- apply (erule bexE)
- apply (drule_tac x=xc in bspec)
- apply assumption
- apply auto
- done
+ shows "min_ext R O (min_ext S \<union> {({},{})}) \<subseteq> min_ext R"
+proof -
+ have "\<And>X Y Z z. \<forall>y\<in>Y. \<exists>x\<in>X. (x, y) \<in> R \<Longrightarrow> \<forall>z\<in>Z. \<exists>y\<in>Y. (y, z) \<in> S
+ \<Longrightarrow> z \<in> Z \<Longrightarrow> \<exists>x\<in>X. (x, z) \<in> R"
+ proof -
+ fix X Y Z z
+ assume *: "\<forall>y\<in>Y. \<exists>x\<in>X. (x, y) \<in> R"
+ "\<forall>z\<in>Z. \<exists>y\<in>Y. (y, z) \<in> S"
+ "z\<in>Z"
+ then obtain y' where 1: "y'\<in>Y" "(y', z) \<in> S"
+ by auto
+ then obtain x' where 2: "x'\<in>X" "(x', y') \<in> R"
+ using * by auto
+ show "\<exists>x\<in>X. (x, z) \<in> R"
+ using 1 2 assms by auto
+ qed
+ then show ?thesis
+ using assms by (auto simp: min_ext_def)
+qed
lemma min_rpair_set: "reduction_pair (min_strict, min_weak)"
unfolding min_strict_def min_weak_def
--- a/src/HOL/Groups_Big.thy Fri Jul 15 09:18:21 2022 +0200
+++ b/src/HOL/Groups_Big.thy Fri Jul 22 14:39:56 2022 +0200
@@ -1001,12 +1001,15 @@
case empty
then show ?case by simp
next
- case insert
+ case (insert x F)
then show ?case
- apply (auto simp: insert_Diff_if)
- apply (drule mk_disjoint_insert)
- apply auto
- done
+ proof (cases "a \<in> F")
+ case True
+ then have "\<exists>B. F = insert a B \<and> a \<notin> B"
+ by (auto simp: mk_disjoint_insert)
+ then show ?thesis using insert
+ by (auto simp: insert_Diff_if)
+ qed (auto)
qed
lemma sum_diff_nat:
@@ -1497,7 +1500,7 @@
next
case (insert a A)
then have "f a = 0 \<or> (\<exists>a\<in>A. f a = 0)" by simp
- then have "f a * prod f A = 0" by rule (simp_all add: insert)
+ then have "f a * prod f A = 0" by (rule disjE) (simp_all add: insert)
with insert show ?case by simp
qed
--- a/src/HOL/HOL.thy Fri Jul 15 09:18:21 2022 +0200
+++ b/src/HOL/HOL.thy Fri Jul 22 14:39:56 2022 +0200
@@ -745,13 +745,13 @@
subsubsection \<open>Atomizing elimination rules\<close>
lemma atomize_exL[atomize_elim]: "(\<And>x. P x \<Longrightarrow> Q) \<equiv> ((\<exists>x. P x) \<Longrightarrow> Q)"
- by rule iprover+
+ by (rule equal_intr_rule) iprover+
lemma atomize_conjL[atomize_elim]: "(A \<Longrightarrow> B \<Longrightarrow> C) \<equiv> (A \<and> B \<Longrightarrow> C)"
- by rule iprover+
+ by (rule equal_intr_rule) iprover+
lemma atomize_disjL[atomize_elim]: "((A \<Longrightarrow> C) \<Longrightarrow> (B \<Longrightarrow> C) \<Longrightarrow> C) \<equiv> ((A \<or> B \<Longrightarrow> C) \<Longrightarrow> C)"
- by rule iprover+
+ by (rule equal_intr_rule) iprover+
lemma atomize_elimL[atomize_elim]: "(\<And>B. (A \<Longrightarrow> B) \<Longrightarrow> B) \<equiv> Trueprop A" ..
@@ -1923,7 +1923,7 @@
by (rule ext equal_eq)+
lemma equal_refl: "equal x x \<longleftrightarrow> True"
- unfolding equal by rule+
+ unfolding equal by (rule iffI TrueI refl)+
lemma eq_equal: "(=) \<equiv> equal"
by (rule eq_reflection) (rule ext, rule ext, rule sym, rule equal_eq)
--- a/src/HOL/Int.thy Fri Jul 15 09:18:21 2022 +0200
+++ b/src/HOL/Int.thy Fri Jul 22 14:39:56 2022 +0200
@@ -53,7 +53,7 @@
lift_definition times_int :: "int \<Rightarrow> int \<Rightarrow> int"
is "\<lambda>(x, y) (u, v). (x*u + y*v, x*v + y*u)"
-proof (clarsimp)
+proof (unfold intrel_def, clarify)
fix s t u v w x y z :: nat
assume "s + v = u + t" and "w + z = y + x"
then have "(s + v) * w + (u + t) * x + u * (w + z) + v * (y + x) =
@@ -140,7 +140,7 @@
assumes "k \<ge> (0::int)" shows "\<exists>n. k = int n"
proof -
have "b \<le> a \<Longrightarrow> \<exists>n::nat. a = n + b" for a b
- by (rule_tac x="a - b" in exI) simp
+ using exI[of _ "a - b"] by simp
with assms show ?thesis
by transfer auto
qed
@@ -149,7 +149,7 @@
assumes "k > (0::int)" shows "\<exists>n>0. k = int n"
proof -
have "b < a \<Longrightarrow> \<exists>n::nat. n>0 \<and> a = n + b" for a b
- by (rule_tac x="a - b" in exI) simp
+ using exI[of _ "a - b"] by simp
with assms show ?thesis
by transfer auto
qed
@@ -189,7 +189,14 @@
for w z :: int
proof -
have "\<And>a b c d. a + d < c + b \<Longrightarrow> \<exists>n. c + b = Suc (a + n + d)"
- by (rule_tac x="c+b - Suc(a+d)" in exI) arith
+ proof -
+ fix a b c d :: nat
+ assume "a + d < c + b"
+ then have "c + b = Suc (a + (c + b - Suc (a + d)) + d) "
+ by arith
+ then show "\<exists>n. c + b = Suc (a + n + d)"
+ by (rule exI)
+ qed
then show ?thesis
by transfer auto
qed
@@ -474,14 +481,20 @@
instance int :: no_top
proof
- show "\<And>x::int. \<exists>y. x < y"
- by (rule_tac x="x + 1" in exI) simp
+ fix x::int
+ have "x < x + 1"
+ by simp
+ then show "\<exists>y. x < y"
+ by (rule exI)
qed
instance int :: no_bot
proof
- show "\<And>x::int. \<exists>y. y < x"
- by (rule_tac x="x - 1" in exI) simp
+ fix x::int
+ have "x - 1< x"
+ by simp
+ then show "\<exists>y. y < x"
+ by (rule exI)
qed
@@ -738,7 +751,14 @@
assumes "x < 0" shows "\<exists>n. x = - (int (Suc n))"
proof -
have "\<And>a b. a < b \<Longrightarrow> \<exists>n. Suc (a + n) = b"
- by (rule_tac x="b - Suc a" in exI) arith
+ proof -
+ fix a b:: nat
+ assume "a < b"
+ then have "Suc (a + (b - Suc a)) = b"
+ by arith
+ then show "\<exists>n. Suc (a + n) = b"
+ by (rule exI)
+ qed
with assms show ?thesis
by transfer auto
qed
@@ -1148,9 +1168,9 @@
proof (rule Ints_cases [OF \<open>x \<in> Ints\<close>])
fix z::int
assume "x = of_int z"
- with \<open>x \<noteq> 0\<close>
+ with \<open>x \<noteq> 0\<close>
show "1 \<le> \<bar>x\<bar>"
- apply (auto simp add: abs_if)
+ apply (auto simp: abs_if)
by (metis diff_0 of_int_1 of_int_le_iff of_int_minus zle_diff1_eq)
qed
@@ -1425,7 +1445,7 @@
obtain i where "i \<le> n - m" "k = f (m + i)"
using nat_ivt_aux [of "n - m" "f \<circ> plus m" k] assms by auto
with assms show ?thesis
- by (rule_tac x = "m + i" in exI) auto
+ using exI[of _ "m + i"] by auto
qed
lemma nat0_intermed_int_val:
--- a/src/HOL/Lattices_Big.thy Fri Jul 15 09:18:21 2022 +0200
+++ b/src/HOL/Lattices_Big.thy Fri Jul 22 14:39:56 2022 +0200
@@ -1042,16 +1042,22 @@
lemma ex_has_greatest_nat_lemma:
"P k \<Longrightarrow> \<forall>x. P x \<longrightarrow> (\<exists>y. P y \<and> \<not> f y \<le> f x) \<Longrightarrow> \<exists>y. P y \<and> \<not> f y < f k + n"
for f :: "'a \<Rightarrow> nat"
-by (induct n) (force simp: le_Suc_eq)+
+ by (induct n) (force simp: le_Suc_eq)+
lemma ex_has_greatest_nat:
- "P k \<Longrightarrow> \<forall>y. P y \<longrightarrow> f y < b \<Longrightarrow> \<exists>x. P x \<and> (\<forall>y. P y \<longrightarrow> f y \<le> f x)"
- for f :: "'a \<Rightarrow> nat"
-apply (rule ccontr)
-apply (cut_tac P = P and n = "b - f k" in ex_has_greatest_nat_lemma)
- apply (subgoal_tac [3] "f k \<le> b")
- apply auto
-done
+ assumes "P k"
+ and "\<forall>y. P y \<longrightarrow> (f:: 'a \<Rightarrow> nat) y < b"
+shows "\<exists>x. P x \<and> (\<forall>y. P y \<longrightarrow> f y \<le> f x)"
+proof (rule ccontr)
+ assume "\<nexists>x. P x \<and> (\<forall>y. P y \<longrightarrow> f y \<le> f x)"
+ then have "\<forall>x. P x \<longrightarrow> (\<exists>y. P y \<and> \<not> f y \<le> f x)"
+ by auto
+ then have "\<exists>y. P y \<and> \<not> f y < f k + (b - f k)"
+ using assms ex_has_greatest_nat_lemma[of P k f "b - f k"]
+ by blast
+ then show "False"
+ using assms by auto
+qed
lemma arg_max_nat_lemma:
"\<lbrakk> P k; \<forall>y. P y \<longrightarrow> f y < b \<rbrakk>
--- a/src/HOL/Nat.thy Fri Jul 15 09:18:21 2022 +0200
+++ b/src/HOL/Nat.thy Fri Jul 22 14:39:56 2022 +0200
@@ -77,11 +77,20 @@
free_constructors case_nat for "0 :: nat" | Suc pred
where "pred (0 :: nat) = (0 :: nat)"
- apply atomize_elim
- apply (rename_tac n, induct_tac n rule: nat_induct0, auto)
- apply (simp add: Suc_def Nat_Abs_Nat_inject Nat_Rep_Nat Suc_RepI Suc_Rep_inject' Rep_Nat_inject)
- apply (simp only: Suc_not_Zero)
- done
+proof atomize_elim
+ fix n
+ show "n = 0 \<or> (\<exists>m. n = Suc m)"
+ by (induction n rule: nat_induct0) auto
+next
+ fix n m
+ show "(Suc n = Suc m) = (n = m)"
+ by (simp add: Suc_def Nat_Abs_Nat_inject Nat_Rep_Nat Suc_RepI Suc_Rep_inject' Rep_Nat_inject)
+next
+ fix n
+ show "0 \<noteq> Suc n"
+ by (simp add: Suc_not_Zero)
+qed
+
\<comment> \<open>Avoid name clashes by prefixing the output of \<open>old_rep_datatype\<close> with \<open>old\<close>.\<close>
setup \<open>Sign.mandatory_path "old"\<close>
@@ -1084,8 +1093,9 @@
and "\<And>n. n > 0 \<Longrightarrow> \<not> P n \<Longrightarrow> \<exists>m. m < n \<and> \<not> P m"
shows "P n"
proof (rule infinite_descent)
- show "\<And>n. \<not> P n \<Longrightarrow> \<exists>m<n. \<not> P m"
- using assms by (case_tac "n > 0") auto
+ fix n
+ show "\<not> P n \<Longrightarrow> \<exists>m<n. \<not> P m"
+ using assms by (cases "n > 0") auto
qed
text \<open>
@@ -1124,9 +1134,11 @@
proof -
from assms obtain n where "n = V x" by auto
moreover have "\<And>x. V x = n \<Longrightarrow> P x"
- proof (induct n rule: infinite_descent, auto)
- show "\<exists>m < V x. \<exists>y. V y = m \<and> \<not> P y" if "\<not> P x" for x
+ proof -
+ have "\<exists>m < V x. \<exists>y. V y = m \<and> \<not> P y" if "\<not> P x" for x
using assms and that by auto
+ then show "\<And>x. V x = n \<Longrightarrow> P x"
+ by (induct n rule: infinite_descent, auto)
qed
ultimately show "P x" by auto
qed
--- a/src/HOL/Num.thy Fri Jul 15 09:18:21 2022 +0200
+++ b/src/HOL/Num.thy Fri Jul 22 14:39:56 2022 +0200
@@ -391,20 +391,42 @@
by (induct k) (simp_all add: numeral.simps is_num.intros)
lemma is_num_add_commute: "is_num x \<Longrightarrow> is_num y \<Longrightarrow> x + y = y + x"
- apply (induct x rule: is_num.induct)
- apply (induct y rule: is_num.induct)
- apply simp
- apply (rule_tac a=x in add_left_imp_eq)
- apply (rule_tac a=x in add_right_imp_eq)
- apply (simp add: add.assoc)
- apply (simp add: add.assoc [symmetric])
- apply (simp add: add.assoc)
- apply (rule_tac a=x in add_left_imp_eq)
- apply (rule_tac a=x in add_right_imp_eq)
- apply (simp add: add.assoc)
- apply (simp add: add.assoc)
- apply (simp add: add.assoc [symmetric])
- done
+proof(induction x rule: is_num.induct)
+ case 1
+ then show ?case
+ proof (induction y rule: is_num.induct)
+ case 1
+ then show ?case by simp
+ next
+ case (2 y)
+ then have "y + (1 + - y) + y = y + (- y + 1) + y"
+ by (simp add: add.assoc)
+ then have "y + (1 + - y) = y + (- y + 1)"
+ by simp
+ then show ?case
+ by (rule add_left_imp_eq[of y])
+ next
+ case (3 x y)
+ then have "1 + (x + y) = x + 1 + y"
+ by (simp add: add.assoc [symmetric])
+ then show ?case using 3
+ by (simp add: add.assoc)
+ qed
+next
+ case (2 x)
+ then have "x + (- x + y) + x = x + (y + - x) + x"
+ by (simp add: add.assoc)
+ then have "x + (- x + y) = x + (y + - x)"
+ by simp
+ then show ?case
+ by (rule add_left_imp_eq[of x])
+next
+ case (3 x z)
+ moreover have "x + (y + z) = (x + y) + z"
+ by (simp add: add.assoc[symmetric])
+ ultimately show ?case
+ by (simp add: add.assoc)
+qed
lemma is_num_add_left_commute: "is_num x \<Longrightarrow> is_num y \<Longrightarrow> x + (y + z) = y + (x + z)"
by (simp only: add.assoc [symmetric] is_num_add_commute)
@@ -1508,21 +1530,22 @@
by simp
next
case (Bit0 q)
- then show ?case
- apply (simp only: Num.numeral_Bit0 Num.numeral_add)
- apply (subst num_of_nat_double)
- apply simp_all
- done
+ then have "num_of_nat (numeral (num.Bit0 q)) = num_of_nat (numeral q + numeral q)"
+ by (simp only: Num.numeral_Bit0 Num.numeral_add)
+ also have "\<dots> = num.Bit0 (num_of_nat (numeral q))"
+ by (rule num_of_nat_double) simp
+ finally show ?case
+ using Bit0.IH by simp
next
case (Bit1 q)
- then show ?case
- apply (simp only: Num.numeral_Bit1 Num.numeral_add)
- apply (subst num_of_nat_plus_distrib)
- apply simp
- apply simp
- apply (subst num_of_nat_double)
- apply simp_all
- done
+ then have "num_of_nat (numeral (num.Bit1 q)) = num_of_nat (numeral q + numeral q + 1)"
+ by (simp only: Num.numeral_Bit1 Num.numeral_add)
+ also have "\<dots> = num_of_nat (numeral q + numeral q) + num_of_nat 1"
+ by (rule num_of_nat_plus_distrib) auto
+ also have "\<dots> = num.Bit0 (num_of_nat (numeral q)) + num_of_nat 1"
+ by (subst num_of_nat_double) auto
+ finally show ?case
+ using Bit1.IH by simp
qed
end
--- a/src/HOL/Order_Relation.thy Fri Jul 15 09:18:21 2022 +0200
+++ b/src/HOL/Order_Relation.thy Fri Jul 22 14:39:56 2022 +0200
@@ -133,15 +133,19 @@
assumes "Total r"
and not_Id: "\<not> r \<subseteq> Id"
shows "Field r = Field (r - Id)"
- using mono_Field[of "r - Id" r] Diff_subset[of r Id]
-proof auto
- fix a assume *: "a \<in> Field r"
- from not_Id have "r \<noteq> {}" by fast
- with not_Id obtain b and c where "b \<noteq> c \<and> (b,c) \<in> r" by auto
- then have "b \<noteq> c \<and> {b, c} \<subseteq> Field r" by (auto simp: Field_def)
- with * obtain d where "d \<in> Field r" "d \<noteq> a" by auto
- with * \<open>Total r\<close> have "(a, d) \<in> r \<or> (d, a) \<in> r" by (simp add: total_on_def)
- with \<open>d \<noteq> a\<close> show "a \<in> Field (r - Id)" unfolding Field_def by blast
+proof -
+ have "Field r \<subseteq> Field (r - Id)"
+ proof (rule subsetI)
+ fix a assume *: "a \<in> Field r"
+ from not_Id have "r \<noteq> {}" by fast
+ with not_Id obtain b and c where "b \<noteq> c \<and> (b,c) \<in> r" by auto
+ then have "b \<noteq> c \<and> {b, c} \<subseteq> Field r" by (auto simp: Field_def)
+ with * obtain d where "d \<in> Field r" "d \<noteq> a" by auto
+ with * \<open>Total r\<close> have "(a, d) \<in> r \<or> (d, a) \<in> r" by (simp add: total_on_def)
+ with \<open>d \<noteq> a\<close> show "a \<in> Field (r - Id)" unfolding Field_def by blast
+ qed
+ then show ?thesis
+ using mono_Field[of "r - Id" r] Diff_subset[of r Id] by auto
qed
subsection\<open>Relations given by a predicate and the field\<close>
@@ -323,7 +327,7 @@
and "(a, b) \<in> r"
shows "under r a \<subseteq> under r b"
unfolding under_def
-proof auto
+proof safe
fix x assume "(x, a) \<in> r"
with assms trans_def[of r] show "(x, b) \<in> r" by blast
qed
@@ -334,7 +338,7 @@
and ab: "(a, b) \<in> r"
shows "underS r a \<subseteq> underS r b"
unfolding underS_def
-proof auto
+proof safe
assume *: "b \<noteq> a" and **: "(b, a) \<in> r"
with \<open>antisym r\<close> antisym_def[of r] ab show False
by blast
@@ -440,12 +444,18 @@
then have "(\<forall>b. (\<forall>c. (c, b) \<in> R a \<longrightarrow> chi c) \<longrightarrow> chi b) \<longrightarrow> (\<forall>b. chi b)"
unfolding wf_def by blast
also have "\<forall>b. (\<forall>c. (c, b) \<in> R a \<longrightarrow> chi c) \<longrightarrow> chi b"
- proof (auto simp add: chi_def R_def)
+ proof safe
fix b
- assume "(b, a) \<in> r" and "\<forall>c. (c, b) \<in> r \<and> (c, a) \<in> r \<longrightarrow> phi c"
- then have "\<forall>c. (c, b) \<in> r \<longrightarrow> phi c"
- using assms trans_def[of r] by blast
- with ** show "phi b" by blast
+ assume "\<forall>c. (c, b) \<in> R a \<longrightarrow> chi c"
+ moreover have "(b, a) \<in> r \<Longrightarrow> \<forall>c. (c, b) \<in> r \<and> (c, a) \<in> r \<longrightarrow> phi c \<Longrightarrow> phi b"
+ proof -
+ assume "(b, a) \<in> r" and "\<forall>c. (c, b) \<in> r \<and> (c, a) \<in> r \<longrightarrow> phi c"
+ then have "\<forall>c. (c, b) \<in> r \<longrightarrow> phi c"
+ using assms trans_def[of r] by blast
+ with ** show "phi b" by blast
+ qed
+ ultimately show "chi b"
+ by (auto simp add: chi_def R_def)
qed
finally have "\<forall>b. chi b" .
with ** chi_def show "phi a" by blast
@@ -456,13 +466,18 @@
text\<open>A transitive relation is well-founded if all initial segments are finite.\<close>
corollary wf_finite_segments:
assumes "irrefl r" and "trans r" and "\<And>x. finite {y. (y, x) \<in> r}"
- shows "wf (r)"
-proof (clarsimp simp: trans_wf_iff wf_iff_acyclic_if_finite converse_def assms)
- fix a
- have "trans (r \<inter> ({x. (x, a) \<in> r} \<times> {x. (x, a) \<in> r}))"
- using assms unfolding trans_def Field_def by blast
- then show "acyclic (r \<inter> {x. (x, a) \<in> r} \<times> {x. (x, a) \<in> r})"
- using assms acyclic_def assms irrefl_def by fastforce
+ shows "wf r"
+proof -
+ have "\<And>a. acyclic (r \<inter> {x. (x, a) \<in> r} \<times> {x. (x, a) \<in> r})"
+ proof -
+ fix a
+ have "trans (r \<inter> ({x. (x, a) \<in> r} \<times> {x. (x, a) \<in> r}))"
+ using assms unfolding trans_def Field_def by blast
+ then show "acyclic (r \<inter> {x. (x, a) \<in> r} \<times> {x. (x, a) \<in> r})"
+ using assms acyclic_def assms irrefl_def by fastforce
+ qed
+ then show ?thesis
+ by (clarsimp simp: trans_wf_iff wf_iff_acyclic_if_finite converse_def assms)
qed
text \<open>The next lemma is a variation of \<open>wf_eq_minimal\<close> from Wellfounded,
@@ -472,13 +487,26 @@
proof-
let ?phi = "\<lambda>A. A \<noteq> {} \<longrightarrow> (\<exists>a \<in> A. \<forall>a' \<in> A. (a',a) \<notin> r)"
have "wf r \<longleftrightarrow> (\<forall>A. ?phi A)"
- apply (auto simp: ex_in_conv [THEN sym])
- apply (erule wfE_min)
- apply assumption
- apply blast
- apply (rule wfI_min)
- apply fast
- done
+ proof
+ assume "wf r"
+ show "\<forall>A. ?phi A"
+ proof clarify
+ fix A:: "'a set"
+ assume "A \<noteq> {}"
+ then obtain x where "x \<in> A"
+ by auto
+ show "\<exists>a\<in>A. \<forall>a'\<in>A. (a', a) \<notin> r"
+ apply (rule wfE_min[of r x A])
+ apply fact+
+ by blast
+ qed
+ next
+ assume *: "\<forall>A. ?phi A"
+ then show "wf r"
+ apply (clarsimp simp: ex_in_conv [THEN sym])
+ apply (rule wfI_min)
+ by fast
+ qed
also have "(\<forall>A. ?phi A) \<longleftrightarrow> (\<forall>B \<subseteq> Field r. ?phi B)"
proof
assume "\<forall>A. ?phi A"
--- a/src/HOL/Orderings.thy Fri Jul 15 09:18:21 2022 +0200
+++ b/src/HOL/Orderings.thy Fri Jul 22 14:39:56 2022 +0200
@@ -790,109 +790,109 @@
end
-lemma order_less_subst2: "(a::'a::order) < b ==> f b < (c::'c::order) ==>
- (!!x y. x < y ==> f x < f y) ==> f a < c"
+lemma order_less_subst2: "(a::'a::order) < b \<Longrightarrow> f b < (c::'c::order) \<Longrightarrow>
+ (!!x y. x < y \<Longrightarrow> f x < f y) \<Longrightarrow> f a < c"
proof -
- assume r: "!!x y. x < y ==> f x < f y"
+ assume r: "!!x y. x < y \<Longrightarrow> f x < f y"
assume "a < b" hence "f a < f b" by (rule r)
also assume "f b < c"
finally (less_trans) show ?thesis .
qed
-lemma order_less_subst1: "(a::'a::order) < f b ==> (b::'b::order) < c ==>
- (!!x y. x < y ==> f x < f y) ==> a < f c"
+lemma order_less_subst1: "(a::'a::order) < f b \<Longrightarrow> (b::'b::order) < c \<Longrightarrow>
+ (!!x y. x < y \<Longrightarrow> f x < f y) \<Longrightarrow> a < f c"
proof -
- assume r: "!!x y. x < y ==> f x < f y"
+ assume r: "!!x y. x < y \<Longrightarrow> f x < f y"
assume "a < f b"
also assume "b < c" hence "f b < f c" by (rule r)
finally (less_trans) show ?thesis .
qed
-lemma order_le_less_subst2: "(a::'a::order) <= b ==> f b < (c::'c::order) ==>
- (!!x y. x <= y ==> f x <= f y) ==> f a < c"
+lemma order_le_less_subst2: "(a::'a::order) <= b \<Longrightarrow> f b < (c::'c::order) \<Longrightarrow>
+ (!!x y. x <= y \<Longrightarrow> f x <= f y) \<Longrightarrow> f a < c"
proof -
- assume r: "!!x y. x <= y ==> f x <= f y"
+ assume r: "!!x y. x <= y \<Longrightarrow> f x <= f y"
assume "a <= b" hence "f a <= f b" by (rule r)
also assume "f b < c"
finally (le_less_trans) show ?thesis .
qed
-lemma order_le_less_subst1: "(a::'a::order) <= f b ==> (b::'b::order) < c ==>
- (!!x y. x < y ==> f x < f y) ==> a < f c"
+lemma order_le_less_subst1: "(a::'a::order) <= f b \<Longrightarrow> (b::'b::order) < c \<Longrightarrow>
+ (!!x y. x < y \<Longrightarrow> f x < f y) \<Longrightarrow> a < f c"
proof -
- assume r: "!!x y. x < y ==> f x < f y"
+ assume r: "!!x y. x < y \<Longrightarrow> f x < f y"
assume "a <= f b"
also assume "b < c" hence "f b < f c" by (rule r)
finally (le_less_trans) show ?thesis .
qed
-lemma order_less_le_subst2: "(a::'a::order) < b ==> f b <= (c::'c::order) ==>
- (!!x y. x < y ==> f x < f y) ==> f a < c"
+lemma order_less_le_subst2: "(a::'a::order) < b \<Longrightarrow> f b <= (c::'c::order) \<Longrightarrow>
+ (!!x y. x < y \<Longrightarrow> f x < f y) \<Longrightarrow> f a < c"
proof -
- assume r: "!!x y. x < y ==> f x < f y"
+ assume r: "!!x y. x < y \<Longrightarrow> f x < f y"
assume "a < b" hence "f a < f b" by (rule r)
also assume "f b <= c"
finally (less_le_trans) show ?thesis .
qed
-lemma order_less_le_subst1: "(a::'a::order) < f b ==> (b::'b::order) <= c ==>
- (!!x y. x <= y ==> f x <= f y) ==> a < f c"
+lemma order_less_le_subst1: "(a::'a::order) < f b \<Longrightarrow> (b::'b::order) <= c \<Longrightarrow>
+ (!!x y. x <= y \<Longrightarrow> f x <= f y) \<Longrightarrow> a < f c"
proof -
- assume r: "!!x y. x <= y ==> f x <= f y"
+ assume r: "!!x y. x <= y \<Longrightarrow> f x <= f y"
assume "a < f b"
also assume "b <= c" hence "f b <= f c" by (rule r)
finally (less_le_trans) show ?thesis .
qed
-lemma order_subst1: "(a::'a::order) <= f b ==> (b::'b::order) <= c ==>
- (!!x y. x <= y ==> f x <= f y) ==> a <= f c"
+lemma order_subst1: "(a::'a::order) <= f b \<Longrightarrow> (b::'b::order) <= c \<Longrightarrow>
+ (!!x y. x <= y \<Longrightarrow> f x <= f y) \<Longrightarrow> a <= f c"
proof -
- assume r: "!!x y. x <= y ==> f x <= f y"
+ assume r: "!!x y. x <= y \<Longrightarrow> f x <= f y"
assume "a <= f b"
also assume "b <= c" hence "f b <= f c" by (rule r)
finally (order_trans) show ?thesis .
qed
-lemma order_subst2: "(a::'a::order) <= b ==> f b <= (c::'c::order) ==>
- (!!x y. x <= y ==> f x <= f y) ==> f a <= c"
+lemma order_subst2: "(a::'a::order) <= b \<Longrightarrow> f b <= (c::'c::order) \<Longrightarrow>
+ (!!x y. x <= y \<Longrightarrow> f x <= f y) \<Longrightarrow> f a <= c"
proof -
- assume r: "!!x y. x <= y ==> f x <= f y"
+ assume r: "!!x y. x <= y \<Longrightarrow> f x <= f y"
assume "a <= b" hence "f a <= f b" by (rule r)
also assume "f b <= c"
finally (order_trans) show ?thesis .
qed
-lemma ord_le_eq_subst: "a <= b ==> f b = c ==>
- (!!x y. x <= y ==> f x <= f y) ==> f a <= c"
+lemma ord_le_eq_subst: "a <= b \<Longrightarrow> f b = c \<Longrightarrow>
+ (!!x y. x <= y \<Longrightarrow> f x <= f y) \<Longrightarrow> f a <= c"
proof -
- assume r: "!!x y. x <= y ==> f x <= f y"
+ assume r: "!!x y. x <= y \<Longrightarrow> f x <= f y"
assume "a <= b" hence "f a <= f b" by (rule r)
also assume "f b = c"
finally (ord_le_eq_trans) show ?thesis .
qed
-lemma ord_eq_le_subst: "a = f b ==> b <= c ==>
- (!!x y. x <= y ==> f x <= f y) ==> a <= f c"
+lemma ord_eq_le_subst: "a = f b \<Longrightarrow> b <= c \<Longrightarrow>
+ (!!x y. x <= y \<Longrightarrow> f x <= f y) \<Longrightarrow> a <= f c"
proof -
- assume r: "!!x y. x <= y ==> f x <= f y"
+ assume r: "!!x y. x <= y \<Longrightarrow> f x <= f y"
assume "a = f b"
also assume "b <= c" hence "f b <= f c" by (rule r)
finally (ord_eq_le_trans) show ?thesis .
qed
-lemma ord_less_eq_subst: "a < b ==> f b = c ==>
- (!!x y. x < y ==> f x < f y) ==> f a < c"
+lemma ord_less_eq_subst: "a < b \<Longrightarrow> f b = c \<Longrightarrow>
+ (!!x y. x < y \<Longrightarrow> f x < f y) \<Longrightarrow> f a < c"
proof -
- assume r: "!!x y. x < y ==> f x < f y"
+ assume r: "!!x y. x < y \<Longrightarrow> f x < f y"
assume "a < b" hence "f a < f b" by (rule r)
also assume "f b = c"
finally (ord_less_eq_trans) show ?thesis .
qed
-lemma ord_eq_less_subst: "a = f b ==> b < c ==>
- (!!x y. x < y ==> f x < f y) ==> a < f c"
+lemma ord_eq_less_subst: "a = f b \<Longrightarrow> b < c \<Longrightarrow>
+ (!!x y. x < y \<Longrightarrow> f x < f y) \<Longrightarrow> a < f c"
proof -
- assume r: "!!x y. x < y ==> f x < f y"
+ assume r: "!!x y. x < y \<Longrightarrow> f x < f y"
assume "a = f b"
also assume "b < c" hence "f b < f c" by (rule r)
finally (ord_eq_less_trans) show ?thesis .
@@ -975,7 +975,7 @@
trans
text \<open>These support proving chains of decreasing inequalities
- a >= b >= c ... in Isar proofs.\<close>
+ a \<ge> b \<ge> c ... in Isar proofs.\<close>
lemma xt1 [no_atp]:
"a = b \<Longrightarrow> b > c \<Longrightarrow> a > c"
@@ -997,54 +997,78 @@
by auto
lemma xt2 [no_atp]:
- "(a::'a::order) >= f b ==> b >= c ==> (!!x y. x >= y ==> f x >= f y) ==> a >= f c"
-by (subgoal_tac "f b >= f c", force, force)
+ assumes "(a::'a::order) \<ge> f b"
+ and "b \<ge> c"
+ and "\<And>x y. x \<ge> y \<Longrightarrow> f x \<ge> f y"
+ shows "a \<ge> f c"
+ using assms by force
-lemma xt3 [no_atp]: "(a::'a::order) >= b ==> (f b::'b::order) >= c ==>
- (!!x y. x >= y ==> f x >= f y) ==> f a >= c"
-by (subgoal_tac "f a >= f b", force, force)
+lemma xt3 [no_atp]:
+ assumes "(a::'a::order) \<ge> b"
+ and "(f b::'b::order) \<ge> c"
+ and "\<And>x y. x \<ge> y \<Longrightarrow> f x \<ge> f y"
+ shows "f a \<ge> c"
+ using assms by force
-lemma xt4 [no_atp]: "(a::'a::order) > f b ==> (b::'b::order) >= c ==>
- (!!x y. x >= y ==> f x >= f y) ==> a > f c"
-by (subgoal_tac "f b >= f c", force, force)
+lemma xt4 [no_atp]:
+ assumes "(a::'a::order) > f b"
+ and "(b::'b::order) \<ge> c"
+ and "\<And>x y. x \<ge> y \<Longrightarrow> f x \<ge> f y"
+ shows "a > f c"
+ using assms by force
-lemma xt5 [no_atp]: "(a::'a::order) > b ==> (f b::'b::order) >= c==>
- (!!x y. x > y ==> f x > f y) ==> f a > c"
-by (subgoal_tac "f a > f b", force, force)
+lemma xt5 [no_atp]:
+ assumes "(a::'a::order) > b"
+ and "(f b::'b::order) \<ge> c"
+ and "\<And>x y. x > y \<Longrightarrow> f x > f y"
+ shows "f a > c"
+ using assms by force
-lemma xt6 [no_atp]: "(a::'a::order) >= f b ==> b > c ==>
- (!!x y. x > y ==> f x > f y) ==> a > f c"
-by (subgoal_tac "f b > f c", force, force)
+lemma xt6 [no_atp]:
+ assumes "(a::'a::order) \<ge> f b"
+ and "b > c"
+ and "\<And>x y. x > y \<Longrightarrow> f x > f y"
+ shows "a > f c"
+ using assms by force
-lemma xt7 [no_atp]: "(a::'a::order) >= b ==> (f b::'b::order) > c ==>
- (!!x y. x >= y ==> f x >= f y) ==> f a > c"
-by (subgoal_tac "f a >= f b", force, force)
+lemma xt7 [no_atp]:
+ assumes "(a::'a::order) \<ge> b"
+ and "(f b::'b::order) > c"
+ and "\<And>x y. x \<ge> y \<Longrightarrow> f x \<ge> f y"
+ shows "f a > c"
+ using assms by force
-lemma xt8 [no_atp]: "(a::'a::order) > f b ==> (b::'b::order) > c ==>
- (!!x y. x > y ==> f x > f y) ==> a > f c"
-by (subgoal_tac "f b > f c", force, force)
+lemma xt8 [no_atp]:
+ assumes "(a::'a::order) > f b"
+ and "(b::'b::order) > c"
+ and "\<And>x y. x > y \<Longrightarrow> f x > f y"
+ shows "a > f c"
+ using assms by force
-lemma xt9 [no_atp]: "(a::'a::order) > b ==> (f b::'b::order) > c ==>
- (!!x y. x > y ==> f x > f y) ==> f a > c"
-by (subgoal_tac "f a > f b", force, force)
+lemma xt9 [no_atp]:
+ assumes "(a::'a::order) > b"
+ and "(f b::'b::order) > c"
+ and "\<And>x y. x > y \<Longrightarrow> f x > f y"
+ shows "f a > c"
+ using assms by force
lemmas xtrans = xt1 xt2 xt3 xt4 xt5 xt6 xt7 xt8 xt9
(*
- Since "a >= b" abbreviates "b <= a", the abbreviation "..." stands
+ Since "a \<ge> b" abbreviates "b \<le> a", the abbreviation "..." stands
for the wrong thing in an Isar proof.
The extra transitivity rules can be used as follows:
lemma "(a::'a::order) > z"
proof -
- have "a >= b" (is "_ >= ?rhs")
+ have "a \<ge> b" (is "_ \<ge> ?rhs")
sorry
- also have "?rhs >= c" (is "_ >= ?rhs")
+ also have "?rhs \<ge> c" (is "_ \<ge> ?rhs")
sorry
also (xtrans) have "?rhs = d" (is "_ = ?rhs")
sorry
- also (xtrans) have "?rhs >= e" (is "_ >= ?rhs")
+ also (xtrans) have "?rhs \<ge> e" (is "_ \<ge> ?rhs")
sorry
also (xtrans) have "?rhs > f" (is "_ > ?rhs")
sorry
--- a/src/HOL/Partial_Function.thy Fri Jul 15 09:18:21 2022 +0200
+++ b/src/HOL/Partial_Function.thy Fri Jul 22 14:39:56 2022 +0200
@@ -219,11 +219,18 @@
and step: "\<And>f. P (U f) \<Longrightarrow> P (U (F f))"
shows "P (U f)"
unfolding eq inverse
-apply (rule ccpo.fixp_induct[OF ccpo adm])
-apply (insert mono, auto simp: monotone_def fun_ord_def bot fun_lub_def)[2]
-apply (rule_tac f5="C x" in step)
-apply (simp add: inverse)
-done
+proof (rule ccpo.fixp_induct[OF ccpo adm])
+ show "monotone le_fun le_fun (\<lambda>f. U (F (C f)))"
+ using mono by (auto simp: monotone_def fun_ord_def)
+next
+ show "P (lub_fun {})"
+ by (auto simp: bot fun_lub_def)
+next
+ fix x
+ assume "P x"
+ then show "P (U (F (C x)))"
+ using step[of "C x"] by (simp add: inverse)
+qed
text \<open>Rules for \<^term>\<open>mono_body\<close>:\<close>
--- a/src/HOL/Power.thy Fri Jul 15 09:18:21 2022 +0200
+++ b/src/HOL/Power.thy Fri Jul 22 14:39:56 2022 +0200
@@ -368,7 +368,7 @@
also from \<open>m > n\<close> have "m = n + (m - n)" by simp
also have "x ^ \<dots> = x ^ n * x ^ (m - n)" by (rule power_add)
finally have "x ^ (m - n) dvd 1"
- by (subst (asm) dvd_times_left_cancel_iff) (insert assms, simp_all)
+ using assms by (subst (asm) dvd_times_left_cancel_iff) simp_all
with \<open>m > n\<close> have "is_unit x" by (simp add: is_unit_power_iff)
}
thus "is_unit x \<or> m \<le> n" by force
@@ -490,9 +490,16 @@
\<close>
lemma power_less_imp_less_exp: "1 < a \<Longrightarrow> a ^ m < a ^ n \<Longrightarrow> m < n"
by (simp add: order_less_le [of m n] less_le [of "a^m" "a^n"] power_le_imp_le_exp)
-
-lemma power_strict_mono [rule_format]: "a < b \<Longrightarrow> 0 \<le> a \<Longrightarrow> 0 < n \<longrightarrow> a ^ n < b ^ n"
- by (induct n) (auto simp: mult_strict_mono le_less_trans [of 0 a b])
+
+lemma power_strict_mono: "a < b \<Longrightarrow> 0 \<le> a \<Longrightarrow> 0 < n \<Longrightarrow> a ^ n < b ^ n"
+proof (induct n)
+ case 0
+ then show ?case by simp
+next
+ case (Suc n)
+ then show ?case
+ by (cases "n = 0") (auto simp: mult_strict_mono le_less_trans [of 0 a b])
+qed
lemma power_mono_iff [simp]:
shows "\<lbrakk>a \<ge> 0; b \<ge> 0; n>0\<rbrakk> \<Longrightarrow> a ^ n \<le> b ^ n \<longleftrightarrow> a \<le> b"
@@ -502,35 +509,27 @@
lemma power_Suc_less: "0 < a \<Longrightarrow> a < 1 \<Longrightarrow> a * a ^ n < a ^ n"
by (induct n) (auto simp: mult_strict_left_mono)
-lemma power_strict_decreasing [rule_format]: "n < N \<Longrightarrow> 0 < a \<Longrightarrow> a < 1 \<longrightarrow> a ^ N < a ^ n"
-proof (induct N)
+lemma power_strict_decreasing: "n < N \<Longrightarrow> 0 < a \<Longrightarrow> a < 1 \<Longrightarrow> a ^ N < a ^ n"
+proof (induction N)
+ case 0
+ then show ?case by simp
+ next
+ case (Suc N)
+ then show ?case
+ using mult_strict_mono[of a 1 "a ^ N" "a ^ n"]
+ by (auto simp add: power_Suc_less less_Suc_eq)
+ qed
+
+text \<open>Proof resembles that of \<open>power_strict_decreasing\<close>.\<close>
+lemma power_decreasing: "n \<le> N \<Longrightarrow> 0 \<le> a \<Longrightarrow> a \<le> 1 \<Longrightarrow> a ^ N \<le> a ^ n"
+proof (induction N)
case 0
then show ?case by simp
next
case (Suc N)
then show ?case
- apply (auto simp add: power_Suc_less less_Suc_eq)
- apply (subgoal_tac "a * a^N < 1 * a^n")
- apply simp
- apply (rule mult_strict_mono)
- apply auto
- done
-qed
-
-text \<open>Proof resembles that of \<open>power_strict_decreasing\<close>.\<close>
-lemma power_decreasing: "n \<le> N \<Longrightarrow> 0 \<le> a \<Longrightarrow> a \<le> 1 \<Longrightarrow> a ^ N \<le> a ^ n"
-proof (induct N)
- case 0
- then show ?case by simp
-next
- case (Suc N)
- then show ?case
- apply (auto simp add: le_Suc_eq)
- apply (subgoal_tac "a * a^N \<le> 1 * a^n")
- apply simp
- apply (rule mult_mono)
- apply auto
- done
+ using mult_mono[of a 1 "a^N" "a ^ n"]
+ by (auto simp add: le_Suc_eq)
qed
lemma power_decreasing_iff [simp]: "\<lbrakk>0 < b; b < 1\<rbrakk> \<Longrightarrow> b ^ m \<le> b ^ n \<longleftrightarrow> n \<le> m"
@@ -552,12 +551,8 @@
next
case (Suc N)
then show ?case
- apply (auto simp add: le_Suc_eq)
- apply (subgoal_tac "1 * a^n \<le> a * a^N")
- apply simp
- apply (rule mult_mono)
- apply (auto simp add: order_trans [OF zero_le_one])
- done
+ using mult_mono[of 1 a "a ^ n" "a ^ N"]
+ by (auto simp add: le_Suc_eq order_trans [OF zero_le_one])
qed
text \<open>Lemma for \<open>power_strict_increasing\<close>.\<close>
@@ -571,12 +566,8 @@
next
case (Suc N)
then show ?case
- apply (auto simp add: power_less_power_Suc less_Suc_eq)
- apply (subgoal_tac "1 * a^n < a * a^N")
- apply simp
- apply (rule mult_strict_mono)
- apply (auto simp add: less_trans [OF zero_less_one] less_imp_le)
- done
+ using mult_strict_mono[of 1 a "a^n" "a^N"]
+ by (auto simp add: power_less_power_Suc less_Suc_eq less_trans [OF zero_less_one] less_imp_le)
qed
lemma power_increasing_iff [simp]: "1 < b \<Longrightarrow> b ^ x \<le> b ^ y \<longleftrightarrow> x \<le> y"
--- a/src/HOL/Presburger.thy Fri Jul 15 09:18:21 2022 +0200
+++ b/src/HOL/Presburger.thy Fri Jul 22 14:39:56 2022 +0200
@@ -28,7 +28,36 @@
"\<exists>z.\<forall>(x::'b::{linorder,plus,Rings.dvd})<z. (d dvd x + s) = (d dvd x + s)"
"\<exists>z.\<forall>(x::'b::{linorder,plus,Rings.dvd})<z. (\<not> d dvd x + s) = (\<not> d dvd x + s)"
"\<exists>z.\<forall>x<z. F = F"
- by ((erule exE, erule exE,rule_tac x="min z za" in exI,simp)+, (rule_tac x="t" in exI,fastforce)+) simp_all
+proof safe
+ fix z1 z2
+ assume "\<forall>x<z1. P x = P' x" and "\<forall>x<z2. Q x = Q' x"
+ then have "\<forall>x < min z1 z2. (P x \<and> Q x) = (P' x \<and> Q' x)"
+ by simp
+ then show "\<exists>z. \<forall>x<z. (P x \<and> Q x) = (P' x \<and> Q' x)"
+ by blast
+next
+ fix z1 z2
+ assume "\<forall>x<z1. P x = P' x" and "\<forall>x<z2. Q x = Q' x"
+ then have "\<forall>x < min z1 z2. (P x \<or> Q x) = (P' x \<or> Q' x)"
+ by simp
+ then show "\<exists>z. \<forall>x<z. (P x \<or> Q x) = (P' x \<or> Q' x)"
+ by blast
+next
+ have "\<forall>x<t. x \<le> t"
+ by fastforce
+ then show "\<exists>z. \<forall>x<z. (x \<le> t) = True"
+ by auto
+next
+ have "\<forall>x<t. \<not> t < x"
+ by fastforce
+ then show "\<exists>z. \<forall>x<z. (t < x) = False"
+ by auto
+next
+ have "\<forall>x<t. \<not> t \<le> x"
+ by fastforce
+ then show "\<exists>z. \<forall>x<z. (t \<le> x) = False"
+ by auto
+qed auto
lemma pinf:
"\<lbrakk>\<exists>(z ::'a::linorder).\<forall>x>z. P x = P' x; \<exists>z.\<forall>x>z. Q x = Q' x\<rbrakk>
@@ -44,7 +73,36 @@
"\<exists>z.\<forall>(x::'b::{linorder,plus,Rings.dvd})>z. (d dvd x + s) = (d dvd x + s)"
"\<exists>z.\<forall>(x::'b::{linorder,plus,Rings.dvd})>z. (\<not> d dvd x + s) = (\<not> d dvd x + s)"
"\<exists>z.\<forall>x>z. F = F"
- by ((erule exE, erule exE,rule_tac x="max z za" in exI,simp)+,(rule_tac x="t" in exI,fastforce)+) simp_all
+proof safe
+ fix z1 z2
+ assume "\<forall>x>z1. P x = P' x" and "\<forall>x>z2. Q x = Q' x"
+ then have "\<forall>x > max z1 z2. (P x \<and> Q x) = (P' x \<and> Q' x)"
+ by simp
+ then show "\<exists>z. \<forall>x>z. (P x \<and> Q x) = (P' x \<and> Q' x)"
+ by blast
+next
+ fix z1 z2
+ assume "\<forall>x>z1. P x = P' x" and "\<forall>x>z2. Q x = Q' x"
+ then have "\<forall>x > max z1 z2. (P x \<or> Q x) = (P' x \<or> Q' x)"
+ by simp
+ then show "\<exists>z. \<forall>x>z. (P x \<or> Q x) = (P' x \<or> Q' x)"
+ by blast
+next
+ have "\<forall>x>t. \<not> x < t"
+ by fastforce
+ then show "\<exists>z. \<forall>x>z. x < t = False"
+ by blast
+next
+ have "\<forall>x>t. \<not> x \<le> t"
+ by fastforce
+ then show "\<exists>z. \<forall>x>z. x \<le> t = False"
+ by blast
+next
+ have "\<forall>x>t. t \<le> x"
+ by fastforce
+ then show "\<exists>z. \<forall>x>z. t \<le> x = True"
+ by blast
+qed auto
lemma inf_period:
"\<lbrakk>\<forall>x k. P x = P (x - k*D); \<forall>x k. Q x = Q (x - k*D)\<rbrakk>
@@ -166,8 +224,19 @@
thus "\<forall>x.(\<forall>j\<in>{1 .. D}. \<forall>b\<in>A. x \<noteq> b - j)\<longrightarrow> (x \<le> t) \<longrightarrow> (x + D \<le> t)" by blast
next
assume d: "d dvd D"
- {fix x assume H: "d dvd x + t" with d have "d dvd (x + D) + t"
- by (clarsimp simp add: dvd_def,rule_tac x= "ka + k" in exI,simp add: algebra_simps)}
+ have "\<And>x. d dvd x + t \<Longrightarrow> d dvd x + D + t"
+ proof -
+ fix x
+ assume H: "d dvd x + t"
+ then obtain ka where "x + t = d * ka"
+ unfolding dvd_def by blast
+ moreover from d obtain k where *:"D = d * k"
+ unfolding dvd_def by blast
+ ultimately have "x + d * k + t = d * (ka + k)"
+ by (simp add: algebra_simps)
+ then show "d dvd (x + D) + t"
+ using * unfolding dvd_def by blast
+ qed
thus "\<forall>(x::int).(\<forall>j\<in>{1 .. D}. \<forall>b\<in>A. x \<noteq> b - j)\<longrightarrow> (d dvd x+t) \<longrightarrow> (d dvd (x + D) + t)" by simp
next
assume d: "d dvd D"
@@ -346,20 +415,7 @@
done
theorem unity_coeff_ex: "(\<exists>(x::'a::{semiring_0,Rings.dvd}). P (l * x)) \<equiv> (\<exists>x. l dvd (x + 0) \<and> P x)"
- apply (rule eq_reflection [symmetric])
- apply (rule iffI)
- defer
- apply (erule exE)
- apply (rule_tac x = "l * x" in exI)
- apply (simp add: dvd_def)
- apply (rule_tac x = x in exI, simp)
- apply (erule exE)
- apply (erule conjE)
- apply simp
- apply (erule dvdE)
- apply (rule_tac x = k in exI)
- apply simp
- done
+ unfolding dvd_def by (rule eq_reflection, rule iffI) auto
lemma zdvd_mono:
fixes k m t :: int
--- a/src/HOL/Product_Type.thy Fri Jul 15 09:18:21 2022 +0200
+++ b/src/HOL/Product_Type.thy Fri Jul 22 14:39:56 2022 +0200
@@ -177,7 +177,7 @@
end
lemma [code]: "HOL.equal u v \<longleftrightarrow> True" for u v :: unit
- unfolding equal unit_eq [of u] unit_eq [of v] by rule+
+ unfolding equal unit_eq [of u] unit_eq [of v] by (rule iffI TrueI refl)+
code_printing
type_constructor unit \<rightharpoonup>
@@ -694,7 +694,12 @@
lemma prod_cases3 [cases type]:
obtains (fields) a b c where "y = (a, b, c)"
- by (cases y, case_tac b) blast
+proof (cases y)
+ case (Pair a b)
+ with that show ?thesis
+ by (cases b) blast
+qed
+
lemma prod_induct3 [case_names fields, induct type]:
"(\<And>a b c. P (a, b, c)) \<Longrightarrow> P x"
@@ -702,7 +707,11 @@
lemma prod_cases4 [cases type]:
obtains (fields) a b c d where "y = (a, b, c, d)"
- by (cases y, case_tac c) blast
+proof (cases y)
+ case (fields a b c)
+ with that show ?thesis
+ by (cases c) blast
+qed
lemma prod_induct4 [case_names fields, induct type]:
"(\<And>a b c d. P (a, b, c, d)) \<Longrightarrow> P x"
@@ -710,7 +719,11 @@
lemma prod_cases5 [cases type]:
obtains (fields) a b c d e where "y = (a, b, c, d, e)"
- by (cases y, case_tac d) blast
+proof (cases y)
+ case (fields a b c d)
+ with that show ?thesis
+ by (cases d) blast
+qed
lemma prod_induct5 [case_names fields, induct type]:
"(\<And>a b c d e. P (a, b, c, d, e)) \<Longrightarrow> P x"
@@ -718,7 +731,11 @@
lemma prod_cases6 [cases type]:
obtains (fields) a b c d e f where "y = (a, b, c, d, e, f)"
- by (cases y, case_tac e) blast
+proof (cases y)
+ case (fields a b c d e)
+ with that show ?thesis
+ by (cases e) blast
+qed
lemma prod_induct6 [case_names fields, induct type]:
"(\<And>a b c d e f. P (a, b, c, d, e, f)) \<Longrightarrow> P x"
@@ -726,7 +743,12 @@
lemma prod_cases7 [cases type]:
obtains (fields) a b c d e f g where "y = (a, b, c, d, e, f, g)"
- by (cases y, case_tac f) blast
+proof (cases y)
+ case (fields a b c d e f)
+ with that show ?thesis
+ by (cases f) blast
+qed
+
lemma prod_induct7 [case_names fields, induct type]:
"(\<And>a b c d e f g. P (a, b, c, d, e, f, g)) \<Longrightarrow> P x"
@@ -852,11 +874,12 @@
assumes major: "c \<in> map_prod f g ` R"
and cases: "\<And>x y. c = (f x, g y) \<Longrightarrow> (x, y) \<in> R \<Longrightarrow> P"
shows P
- apply (rule major [THEN imageE])
- apply (case_tac x)
- apply (rule cases)
- apply simp_all
- done
+proof (rule major [THEN imageE])
+ fix x
+ assume "c = map_prod f g x" "x \<in> R"
+ then show P
+ using cases by (cases x) simp
+qed
definition apfst :: "('a \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c \<times> 'b"
where "apfst f = map_prod f id"
--- a/src/HOL/Quotient.thy Fri Jul 15 09:18:21 2022 +0200
+++ b/src/HOL/Quotient.thy Fri Jul 22 14:39:56 2022 +0200
@@ -148,8 +148,8 @@
moreover
have "(R1 ===> R2) ((abs1 ---> rep2) a) ((abs1 ---> rep2) a)" for a
by (rule rel_funI)
- (insert q1 q2 Quotient3_rel_abs [of R1 abs1 rep1] Quotient3_rel_rep [of R2 abs2 rep2],
- simp (no_asm) add: Quotient3_def, simp)
+ (use q1 q2 Quotient3_rel_abs [of R1 abs1 rep1] Quotient3_rel_rep [of R2 abs2 rep2]
+ in \<open>simp (no_asm) add: Quotient3_def, simp\<close>)
moreover
have "(R1 ===> R2) r s = ((R1 ===> R2) r r \<and> (R1 ===> R2) s s \<and>
(rep1 ---> abs2) r = (rep1 ---> abs2) s)" for r s
@@ -322,9 +322,9 @@
lemma babs_rsp:
assumes q: "Quotient3 R1 Abs1 Rep1"
- and a: "(R1 ===> R2) f g"
- shows "(R1 ===> R2) (Babs (Respects R1) f) (Babs (Respects R1) g)"
-proof (clarsimp simp add: Babs_def in_respects rel_fun_def)
+ and a: "(R1 ===> R2) f g"
+ shows "(R1 ===> R2) (Babs (Respects R1) f) (Babs (Respects R1) g)"
+proof
fix x y
assume "R1 x y"
then have "x \<in> Respects R1 \<and> y \<in> Respects R1"
@@ -542,7 +542,7 @@
then have "Abs (Collect (R r)) = Abs (Collect (R s)) \<longleftrightarrow> Collect (R r) = Collect (R s)"
by (metis abs_inverse)
also have "Collect (R r) = Collect (R s) \<longleftrightarrow> (\<lambda>A x. x \<in> A) (Collect (R r)) = (\<lambda>A x. x \<in> A) (Collect (R s))"
- by rule simp_all
+ by (rule iffI) simp_all
finally show "Abs (Collect (R r)) = Abs (Collect (R s)) \<longleftrightarrow> R r = R s" by simp
qed
then show "R r s \<longleftrightarrow> R r r \<and> R s s \<and> (Abs (Collect (R r)) = Abs (Collect (R s)))"
--- a/src/HOL/Relation.thy Fri Jul 15 09:18:21 2022 +0200
+++ b/src/HOL/Relation.thy Fri Jul 22 14:39:56 2022 +0200
@@ -1180,12 +1180,19 @@
by blast
text \<open>Converse inclusion requires some assumptions\<close>
-lemma Image_INT_eq: "single_valued (r\<inverse>) \<Longrightarrow> A \<noteq> {} \<Longrightarrow> r `` (\<Inter>(B ` A)) = (\<Inter>x\<in>A. r `` B x)"
- apply (rule equalityI)
- apply (rule Image_INT_subset)
- apply (auto simp add: single_valued_def)
- apply blast
- done
+lemma Image_INT_eq:
+ assumes "single_valued (r\<inverse>)"
+ and "A \<noteq> {}"
+ shows "r `` (\<Inter>(B ` A)) = (\<Inter>x\<in>A. r `` B x)"
+proof(rule equalityI, rule Image_INT_subset)
+ show "(\<Inter>x\<in>A. r `` B x) \<subseteq> r `` \<Inter> (B ` A)"
+ proof
+ fix x
+ assume "x \<in> (\<Inter>x\<in>A. r `` B x)"
+ then show "x \<in> r `` \<Inter> (B ` A)"
+ using assms unfolding single_valued_def by simp blast
+ qed
+qed
lemma Image_subset_eq: "r``A \<subseteq> B \<longleftrightarrow> A \<subseteq> - ((r\<inverse>) `` (- B))"
by blast
--- a/src/HOL/Rings.thy Fri Jul 15 09:18:21 2022 +0200
+++ b/src/HOL/Rings.thy Fri Jul 22 14:39:56 2022 +0200
@@ -191,7 +191,7 @@
by (auto intro: dvdI)
lemma dvd_mult [simp]: "a dvd (b * c)" if "a dvd c"
- using that by rule (auto intro: mult.left_commute dvdI)
+ using that by (auto intro: mult.left_commute dvdI)
lemma dvd_mult2 [simp]: "a dvd (b * c)" if "a dvd b"
using that dvd_mult [of a b c] by (simp add: ac_simps)
@@ -1175,7 +1175,7 @@
lemma unit_div_eq_0_iff:
assumes "is_unit b"
shows "a div b = 0 \<longleftrightarrow> a = 0"
- by (rule dvd_div_eq_0_iff) (insert assms, auto)
+ using assms by (simp add: dvd_div_eq_0_iff unit_imp_dvd)
lemma div_mult_unit2:
"is_unit c \<Longrightarrow> b dvd a \<Longrightarrow> a div (b * c) = a div b div c"
@@ -1542,7 +1542,7 @@
lemma coprime_normalize_left_iff [simp]:
"coprime (normalize a) b \<longleftrightarrow> coprime a b"
- by (rule; rule coprimeI) (auto intro: coprime_common_divisor)
+ by (rule iffI; rule coprimeI) (auto intro: coprime_common_divisor)
lemma coprime_normalize_right_iff [simp]:
"coprime a (normalize b) \<longleftrightarrow> coprime a b"
@@ -2039,7 +2039,7 @@
lemma mult_strict_mono':
assumes "a < b" and "c < d" and "0 \<le> a" and "0 \<le> c"
shows "a * c < b * d"
- by (rule mult_strict_mono) (insert assms, auto)
+ using assms by (auto simp add: mult_strict_mono)
lemma mult_less_le_imp_less:
assumes "a < b" and "c \<le> d" and "0 \<le> a" and "0 < c"
@@ -2365,7 +2365,7 @@
begin
subclass zero_neq_one
- by standard (insert zero_less_one, blast)
+ by standard
subclass comm_semiring_1
by standard (rule mult_1_left)
@@ -2405,10 +2405,12 @@
subclass linordered_nonzero_semiring
proof
show "a + 1 < b + 1" if "a < b" for a b
- proof (rule ccontr, simp add: not_less)
- assume "b \<le> a"
- with that show False
+ proof (rule ccontr)
+ assume "\<not> a + 1 < b + 1"
+ moreover with that have "a + 1 < b + 1"
by simp
+ ultimately show False
+ by contradiction
qed
qed
--- a/src/HOL/Set_Interval.thy Fri Jul 15 09:18:21 2022 +0200
+++ b/src/HOL/Set_Interval.thy Fri Jul 22 14:39:56 2022 +0200
@@ -464,11 +464,16 @@
lemma (in linorder) atLeastLessThan_subset_iff:
"{a..<b} \<subseteq> {c..<d} \<Longrightarrow> b \<le> a \<or> c\<le>a \<and> b\<le>d"
- apply (auto simp:subset_eq Ball_def not_le)
- apply(frule_tac x=a in spec)
- apply(erule_tac x=d in allE)
- apply auto
- done
+proof (cases "a < b")
+ case True
+ assume assm: "{a..<b} \<subseteq> {c..<d}"
+ then have 1: "c \<le> a \<and> a \<le> d"
+ using True by (auto simp add: subset_eq Ball_def)
+ then have 2: "b \<le> d"
+ using assm by (auto simp add: subset_eq)
+ from 1 2 show ?thesis
+ by simp
+qed (auto)
lemma atLeastLessThan_inj:
fixes a b c d :: "'a::linorder"
@@ -941,7 +946,7 @@
next
fix y assume "y \<le> -x"
have "- (-y) \<in> uminus ` {x..}"
- by (rule imageI) (insert \<open>y \<le> -x\<close>[THEN le_imp_neg_le], simp)
+ by (rule imageI) (use \<open>y \<le> -x\<close>[THEN le_imp_neg_le] in \<open>simp\<close>)
thus "y \<in> uminus ` {x..}" by simp
qed simp_all
@@ -991,9 +996,17 @@
lemma image_diff_atLeastAtMost [simp]:
fixes d::"'a::linordered_idom" shows "((-) d ` {a..b}) = {d-b..d-a}"
- apply auto
- apply (rule_tac x="d-x" in rev_image_eqI, auto)
- done
+proof
+ show "{d - b..d - a} \<subseteq> (-) d ` {a..b}"
+ proof
+ fix x
+ assume "x \<in> {d - b..d - a}"
+ then have "d - x \<in> {a..b}" and "x = d - (d - x)"
+ by auto
+ then show "x \<in> (-) d ` {a..b}"
+ by (rule rev_image_eqI)
+ qed
+qed(auto)
lemma image_diff_atLeastLessThan [simp]:
fixes a b c::"'a::linordered_idom"
@@ -1144,10 +1157,7 @@
lemma image_add_int_atLeastLessThan:
"(\<lambda>x. x + (l::int)) ` {0..<u-l} = {l..<u}"
- apply (auto simp add: image_def)
- apply (rule_tac x = "x - l" in bexI)
- apply auto
- done
+ by safe auto
lemma image_minus_const_atLeastLessThan_nat:
fixes c :: nat
@@ -1218,8 +1228,9 @@
by (blast dest:less_imp_le_nat le_imp_less_Suc)
lemma finite_less_ub:
- "!!f::nat=>nat. (!!n. n \<le> f n) ==> finite {n. f n \<le> u}"
-by (rule_tac B="{..u}" in finite_subset, auto intro: order_trans)
+ "\<And>f::nat\<Rightarrow>nat. (!!n. n \<le> f n) \<Longrightarrow> finite {n. f n \<le> u}"
+ by (rule finite_subset[of _ "{..u}"])
+ (auto intro: order_trans)
lemma bounded_Max_nat:
fixes P :: "nat \<Rightarrow> bool"
@@ -1315,7 +1326,7 @@
lemma UN_finite2_subset:
assumes "\<And>n::nat. (\<Union>i\<in>{0..<n}. A i) \<subseteq> (\<Union>i\<in>{0..<n + k}. B i)"
shows "(\<Union>n. A n) \<subseteq> (\<Union>n. B n)"
-proof (rule UN_finite_subset, rule)
+proof (rule UN_finite_subset, rule subsetI)
fix n and a
from assms have "(\<Union>i\<in>{0..<n}. A i) \<subseteq> (\<Union>i\<in>{0..<n + k}. B i)" .
moreover assume "a \<in> (\<Union>i\<in>{0..<n}. A i)"
@@ -1324,12 +1335,17 @@
qed
lemma UN_finite2_eq:
- "(\<And>n::nat. (\<Union>i\<in>{0..<n}. A i) = (\<Union>i\<in>{0..<n + k}. B i)) \<Longrightarrow>
- (\<Union>n. A n) = (\<Union>n. B n)"
- apply (rule subset_antisym [OF UN_finite_subset UN_finite2_subset])
- apply auto
- apply (force simp add: atLeastLessThan_add_Un [of 0])+
- done
+ assumes "(\<And>n::nat. (\<Union>i\<in>{0..<n}. A i) = (\<Union>i\<in>{0..<n + k}. B i))"
+ shows "(\<Union>n. A n) = (\<Union>n. B n)"
+proof (rule subset_antisym [OF UN_finite_subset UN_finite2_subset])
+ fix n
+ show "\<Union> (A ` {0..<n}) \<subseteq> (\<Union>n. B n)"
+ using assms by auto
+next
+ fix n
+ show "\<Union> (B ` {0..<n}) \<subseteq> \<Union> (A ` {0..<n + k})"
+ using assms by (force simp add: atLeastLessThan_add_Un [of 0])+
+qed
subsubsection \<open>Cardinality\<close>
@@ -1342,11 +1358,21 @@
lemma card_atLeastLessThan [simp]: "card {l..<u} = u - l"
proof -
- have "{l..<u} = (\<lambda>x. x + l) ` {..<u-l}"
- apply (auto simp add: image_def atLeastLessThan_def lessThan_def)
- apply (rule_tac x = "x - l" in exI)
- apply arith
- done
+ have "(\<lambda>x. x + l) ` {..<u - l} \<subseteq> {l..<u}"
+ by auto
+ moreover have "{l..<u} \<subseteq> (\<lambda>x. x + l) ` {..<u-l}"
+ proof
+ fix x
+ assume *: "x \<in> {l..<u}"
+ then have "x - l \<in> {..< u -l}"
+ by auto
+ then have "(x - l) + l \<in> (\<lambda>x. x + l) ` {..< u -l}"
+ by auto
+ then show "x \<in> (\<lambda>x. x + l) ` {..<u - l}"
+ using * by auto
+ qed
+ ultimately have "{l..<u} = (\<lambda>x. x + l) ` {..<u-l}"
+ by auto
then have "card {l..<u} = card {..<u-l}"
by (simp add: card_image inj_on_def)
then show ?thesis
@@ -1430,7 +1456,8 @@
let ?f = "\<lambda>a. SOME b. ?P a b"
have 1: "?f ` A \<subseteq> B" by (auto intro: someI2_ex[OF assms(2)])
have "inj_on ?f A"
- proof (auto simp: inj_on_def)
+ unfolding inj_on_def
+ proof safe
fix a1 a2 assume asms: "a1 \<in> A" "a2 \<in> A" "?f a1 = ?f a2"
have 0: "?f a1 \<in> B" using "1" \<open>a1 \<in> A\<close> by blast
have 1: "r a1 (?f a1)" using someI_ex[OF assms(2)[OF \<open>a1 \<in> A\<close>]] by blast
@@ -1475,13 +1502,24 @@
subsubsection \<open>Finiteness\<close>
-lemma image_atLeastZeroLessThan_int: "0 \<le> u ==>
- {(0::int)..<u} = int ` {..<nat u}"
+lemma image_atLeastZeroLessThan_int:
+ assumes "0 \<le> u"
+ shows "{(0::int)..<u} = int ` {..<nat u}"
unfolding image_def lessThan_def
- apply auto
- apply (rule_tac x = "nat x" in exI)
- apply (auto simp add: zless_nat_eq_int_zless [THEN sym])
- done
+proof
+ show "{0..<u} \<subseteq> {y. \<exists>x\<in>{x. x < nat u}. y = int x}"
+ proof
+ fix x
+ assume "x \<in> {0..<u}"
+ then have "x = int (nat x)" and "nat x < nat u"
+ by (auto simp add: zless_nat_eq_int_zless [THEN sym])
+ then have "\<exists>xa<nat u. x = int xa"
+ using exI[of _ "(nat x)"] by simp
+ then show "x \<in> {y. \<exists>x\<in>{x. x < nat u}. y = int x}"
+ by simp
+ qed
+qed (auto)
+
lemma finite_atLeastZeroLessThan_int: "finite {(0::int)..<u}"
proof (cases "0 \<le> u")
@@ -1695,9 +1733,7 @@
lemma ivl_subset [simp]: "({i..<j} \<subseteq> {m..<n}) = (j \<le> i \<or> m \<le> i \<and> j \<le> (n::'a::linorder))"
using linorder_class.le_less_linear[of i n]
- apply (auto simp: linorder_not_le)
- apply (force intro: leI)+
- done
+ by safe (force intro: leI)+
subsection \<open>Generic big monoid operation over intervals\<close>
@@ -1707,7 +1743,7 @@
lemma inj_on_of_nat [simp]:
"inj_on of_nat N"
- by rule simp
+ by (rule inj_onI) simp
lemma bij_betw_of_nat [simp]:
"bij_betw of_nat N A \<longleftrightarrow> of_nat ` N = A"
@@ -2310,8 +2346,24 @@
(if n < m then 0
else if x = 1 then of_nat((n + 1) - m)
else (x^m - x^Suc n) / (1 - x))"
-using sum_gp_multiplied [of m n x] apply auto
-by (metis eq_iff_diff_eq_0 mult.commute nonzero_divide_eq_eq)
+proof (cases "n < m")
+ case False
+ assume *: "\<not> n < m"
+ then show ?thesis
+ proof (cases "x = 1")
+ case False
+ assume "x \<noteq> 1"
+ then have not_zero: "1 - x \<noteq> 0"
+ by auto
+ have "(1 - x) * (\<Sum>i=m..n. x^i) = x ^ m - x * x ^ n"
+ using sum_gp_multiplied [of m n x] * by auto
+ then have "(\<Sum>i=m..n. x^i) = (x ^ m - x * x ^ n) / (1 - x) "
+ using nonzero_divide_eq_eq mult.commute not_zero
+ by metis
+ then show ?thesis
+ by auto
+ qed (auto)
+qed (auto)
subsubsection\<open>Geometric progressions\<close>
--- a/src/HOL/Transfer.thy Fri Jul 15 09:18:21 2022 +0200
+++ b/src/HOL/Transfer.thy Fri Jul 22 14:39:56 2022 +0200
@@ -532,7 +532,12 @@
lemma rec_nat_transfer [transfer_rule]:
"(A ===> ((=) ===> A ===> A) ===> (=) ===> A) rec_nat rec_nat"
- unfolding rel_fun_def by (clarsimp, rename_tac n, induct_tac n, simp_all)
+ unfolding rel_fun_def
+ apply safe
+ subgoal for _ _ _ _ _ n
+ by (induction n) simp_all
+ done
+
lemma funpow_transfer [transfer_rule]:
"((=) ===> (A ===> A) ===> (A ===> A)) compow compow"
--- a/src/HOL/Transitive_Closure.thy Fri Jul 15 09:18:21 2022 +0200
+++ b/src/HOL/Transitive_Closure.thy Fri Jul 22 14:39:56 2022 +0200
@@ -251,7 +251,7 @@
shows P
proof -
have "x = z \<or> (\<exists>y. r x y \<and> r\<^sup>*\<^sup>* y z)"
- by (rule_tac major [THEN converse_rtranclp_induct]) iprover+
+ by (rule major [THEN converse_rtranclp_induct]) iprover+
then show ?thesis
by (auto intro: cases)
qed
@@ -1007,10 +1007,10 @@
next
case (Suc n)
show ?case
- proof (simp add: relcomp_unfold Suc)
- show "(\<exists>y. (\<exists>f. f 0 = a \<and> f n = y \<and> (\<forall>i<n. (f i,f(Suc i)) \<in> R)) \<and> (y,b) \<in> R) \<longleftrightarrow>
+ proof -
+ have "(\<exists>y. (\<exists>f. f 0 = a \<and> f n = y \<and> (\<forall>i<n. (f i,f(Suc i)) \<in> R)) \<and> (y,b) \<in> R) \<longleftrightarrow>
(\<exists>f. f 0 = a \<and> f(Suc n) = b \<and> (\<forall>i<Suc n. (f i, f (Suc i)) \<in> R))"
- (is "?l = ?r")
+ (is "?l \<longleftrightarrow> ?r")
proof
assume ?l
then obtain c f
@@ -1022,8 +1022,9 @@
assume ?r
then obtain f where 1: "f 0 = a" "b = f (Suc n)" "\<And>i. i < Suc n \<Longrightarrow> (f i, f (Suc i)) \<in> R"
by auto
- show ?l by (rule exI[of _ "f n"], rule conjI, rule exI[of _ f], insert 1, auto)
+ show ?l by (rule exI[of _ "f n"], rule conjI, rule exI[of _ f], auto simp add: 1)
qed
+ then show ?thesis by (simp add: relcomp_unfold Suc)
qed
qed
--- a/src/HOL/Wellfounded.thy Fri Jul 15 09:18:21 2022 +0200
+++ b/src/HOL/Wellfounded.thy Fri Jul 22 14:39:56 2022 +0200
@@ -257,8 +257,10 @@
then obtain z where "z \<in> Q" "(z, y) \<in> r\<^sup>*"
"\<And>z'. (z', z) \<in> r \<longrightarrow> z' \<in> Q \<longrightarrow> (z', y) \<notin> r\<^sup>*"
using R' [of "{z \<in> Q. (z,y) \<in> r\<^sup>*}"] by auto
- with R show ?thesis
- by (rule_tac x="z" in bexI) (blast intro: rtrancl_trans)
+ then have "\<forall>y'. (y', z) \<in> insert (y, x) r \<longrightarrow> y' \<notin> Q"
+ using R by(blast intro: rtrancl_trans)+
+ then show ?thesis
+ by (rule bexI) fact
next
case False
then show ?thesis
@@ -293,7 +295,7 @@
thus ?thesis
using inj unfolding A_def
by (intro bexI[of _ "f a0"]) auto
- qed (insert \<open>b \<in> B\<close>, unfold A_def, auto)
+ qed (use \<open>b \<in> B\<close> in \<open>unfold A_def, auto\<close>)
qed
lemma wf_map_prod_image: "wf r \<Longrightarrow> inj f \<Longrightarrow> wf (map_prod f f ` r)"
@@ -581,11 +583,13 @@
unfolding less_eq rtrancl_eq_or_trancl by auto
lemma wf_pred_nat: "wf pred_nat"
- apply (unfold wf_def pred_nat_def)
- apply clarify
- apply (induct_tac x)
- apply blast+
- done
+ unfolding wf_def
+proof clarify
+ fix P x
+ assume "\<forall>x'. (\<forall>y. (y, x') \<in> pred_nat \<longrightarrow> P y) \<longrightarrow> P x'"
+ then show "P x"
+ unfolding pred_nat_def by (induction x) blast+
+qed
lemma wf_less_than [iff]: "wf less_than"
by (simp add: less_than_def wf_pred_nat [THEN wf_trancl])
@@ -673,10 +677,12 @@
by (blast dest: accp_downwards_aux)
theorem accp_wfPI: "\<forall>x. accp r x \<Longrightarrow> wfP r"
- apply (rule wfPUNIVI)
- apply (rule_tac P = P in accp_induct)
- apply blast+
- done
+proof (rule wfPUNIVI)
+ fix P x
+ assume "\<forall>x. accp r x" "\<forall>x. (\<forall>y. r y x \<longrightarrow> P y) \<longrightarrow> P x"
+ then show "P x"
+ using accp_induct[where P = P] by blast
+qed
theorem accp_wfPD: "wfP r \<Longrightarrow> accp r x"
apply (erule wfP_induct_rule)
@@ -750,15 +756,20 @@
fixes f :: "'a \<Rightarrow> 'b"
assumes "wf r"
shows "wf (inv_image r f)"
-proof (clarsimp simp: inv_image_def wf_eq_minimal)
- fix P and x::'a
- assume "x \<in> P"
- then obtain w where w: "w \<in> {w. \<exists>x::'a. x \<in> P \<and> f x = w}"
- by auto
- have *: "\<And>Q u. u \<in> Q \<Longrightarrow> \<exists>z\<in>Q. \<forall>y. (y, z) \<in> r \<longrightarrow> y \<notin> Q"
- using assms by (auto simp add: wf_eq_minimal)
- show "\<exists>z\<in>P. \<forall>y. (f y, f z) \<in> r \<longrightarrow> y \<notin> P"
- using * [OF w] by auto
+proof -
+ have "\<And>x P. x \<in> P \<Longrightarrow> \<exists>z\<in>P. \<forall>y. (f y, f z) \<in> r \<longrightarrow> y \<notin> P"
+ proof -
+ fix P and x::'a
+ assume "x \<in> P"
+ then obtain w where w: "w \<in> {w. \<exists>x::'a. x \<in> P \<and> f x = w}"
+ by auto
+ have *: "\<And>Q u. u \<in> Q \<Longrightarrow> \<exists>z\<in>Q. \<forall>y. (y, z) \<in> r \<longrightarrow> y \<notin> Q"
+ using assms by (auto simp add: wf_eq_minimal)
+ show "\<exists>z\<in>P. \<forall>y. (f y, f z) \<in> r \<longrightarrow> y \<notin> P"
+ using * [OF w] by auto
+ qed
+ then show ?thesis
+ by (clarsimp simp: inv_image_def wf_eq_minimal)
qed
text \<open>Measure functions into \<^typ>\<open>nat\<close>\<close>
@@ -901,7 +912,7 @@
next
case False
from * finites have N2: "(?N2, M) \<in> max_ext r"
- by (rule_tac max_extI[OF _ _ \<open>M \<noteq> {}\<close>]) auto
+ using max_extI[OF _ _ \<open>M \<noteq> {}\<close>, where ?X = ?N2] by auto
with \<open>M \<in> ?W\<close> show "?N2 \<in> ?W" by (rule acc_downward)
qed
with finites have "?N1 \<union> ?N2 \<in> ?W"
--- a/src/HOL/Wfrec.thy Fri Jul 15 09:18:21 2022 +0200
+++ b/src/HOL/Wfrec.thy Fri Jul 22 14:39:56 2022 +0200
@@ -101,15 +101,20 @@
lemma wf_same_fst:
assumes "\<And>x. P x \<Longrightarrow> wf (R x)"
shows "wf (same_fst P R)"
-proof (clarsimp simp add: wf_def same_fst_def)
- fix Q a b
- assume *: "\<forall>a b. (\<forall>x. P a \<and> (x,b) \<in> R a \<longrightarrow> Q (a,x)) \<longrightarrow> Q (a,b)"
- show "Q(a,b)"
- proof (cases "wf (R a)")
- case True
- then show ?thesis
- by (induction b rule: wf_induct_rule) (use * in blast)
- qed (use * assms in blast)
+proof -
+ have "\<And>a b Q. \<forall>a b. (\<forall>x. P a \<and> (x, b) \<in> R a \<longrightarrow> Q (a, x)) \<longrightarrow> Q (a, b) \<Longrightarrow> Q (a, b)"
+ proof -
+ fix Q a b
+ assume *: "\<forall>a b. (\<forall>x. P a \<and> (x,b) \<in> R a \<longrightarrow> Q (a,x)) \<longrightarrow> Q (a,b)"
+ show "Q(a,b)"
+ proof (cases "wf (R a)")
+ case True
+ then show ?thesis
+ by (induction b rule: wf_induct_rule) (use * in blast)
+ qed (use * assms in blast)
+ qed
+ then show ?thesis
+ by (clarsimp simp add: wf_def same_fst_def)
qed
end