--- a/src/HOL/Library/Code_Abstract_Nat.thy Fri Jan 24 14:35:47 2025 +0100
+++ b/src/HOL/Library/Code_Abstract_Nat.thy Fri Jan 24 17:53:17 2025 +0000
@@ -127,7 +127,6 @@
(case n of 0 \<Rightarrow> None | Suc n \<Rightarrow> (case take_bit_num n m of None \<Rightarrow> None | Some q \<Rightarrow> Some (Num.Bit0 q)))\<close>
\<open>take_bit_num n (Num.Bit1 m) =
(case n of 0 \<Rightarrow> None | Suc n \<Rightarrow> Some (case take_bit_num n m of None \<Rightarrow> Num.One | Some q \<Rightarrow> Num.Bit1 q))\<close>
- apply (cases n; simp)+
- done
+ by (cases n; simp)+
end
--- a/src/HOL/Library/Code_Binary_Nat.thy Fri Jan 24 14:35:47 2025 +0100
+++ b/src/HOL/Library/Code_Binary_Nat.thy Fri Jan 24 17:53:17 2025 +0000
@@ -75,12 +75,9 @@
"sub (Num.Bit1 m) (Num.Bit0 n) = map_option (\<lambda>q. dup q + 1) (sub m n)"
"sub (Num.Bit0 m) (Num.Bit1 n) = (case sub m n of None \<Rightarrow> None
| Some q \<Rightarrow> if q = 0 then None else Some (dup q - 1))"
- apply (auto simp add: nat_of_num_numeral
- Num.dbl_def Num.dbl_inc_def Num.dbl_dec_def
- Let_def le_imp_diff_is_add BitM_plus_one sub_def dup_def)
- apply (simp_all add: sub_non_positive)
- apply (simp_all add: sub_non_negative [symmetric, where ?'a = int])
- done
+ by (auto simp: nat_of_num_numeral Num.dbl_def Num.dbl_inc_def Num.dbl_dec_def
+ Let_def le_imp_diff_is_add BitM_plus_one sub_def dup_def
+ sub_non_positive nat_add_distrib sub_non_negative)
declare [[code drop: "minus :: nat \<Rightarrow> _"]]
--- a/src/HOL/Library/Countable_Set_Type.thy Fri Jan 24 14:35:47 2025 +0100
+++ b/src/HOL/Library/Countable_Set_Type.thy Fri Jan 24 17:53:17 2025 +0000
@@ -414,10 +414,9 @@
by auto
lemma atomize_cBall:
- "(\<And>x. cin x A ==> P x) == Trueprop (cBall A (\<lambda>x. P x))"
-apply (simp only: atomize_all atomize_imp)
-apply (rule equal_intr_rule)
-by (transfer, simp)+
+ "(\<And>x. cin x A \<Longrightarrow> P x) == Trueprop (cBall A (\<lambda>x. P x))"
+ unfolding atomize_all atomize_imp
+ by (rule equal_intr_rule; blast)
subsubsection \<open>\<^const>\<open>cUnion\<close>\<close>
@@ -526,48 +525,43 @@
begin
lemma card_of_countable_sets_range:
-fixes A :: "'a set"
-shows "|{X. X \<subseteq> A \<and> countable X \<and> X \<noteq> {}}| \<le>o |{f::nat \<Rightarrow> 'a. range f \<subseteq> A}|"
-apply(rule card_of_ordLeqI[of from_nat_into]) using inj_on_from_nat_into
-unfolding inj_on_def by auto
+ fixes A :: "'a set"
+ shows "|{X. X \<subseteq> A \<and> countable X \<and> X \<noteq> {}}| \<le>o |{f::nat \<Rightarrow> 'a. range f \<subseteq> A}|"
+proof (intro card_of_ordLeqI[of from_nat_into])
+qed (use inj_on_from_nat_into in \<open>auto simp: inj_on_def\<close>)
lemma card_of_countable_sets_Func:
-"|{X. X \<subseteq> A \<and> countable X \<and> X \<noteq> {}}| \<le>o |A| ^c natLeq"
-using card_of_countable_sets_range card_of_Func_UNIV[THEN ordIso_symmetric]
-unfolding cexp_def Field_natLeq Field_card_of
-by (rule ordLeq_ordIso_trans)
+ "|{X. X \<subseteq> A \<and> countable X \<and> X \<noteq> {}}| \<le>o |A| ^c natLeq"
+ using card_of_countable_sets_range card_of_Func_UNIV[THEN ordIso_symmetric]
+ unfolding cexp_def Field_natLeq Field_card_of
+ by (rule ordLeq_ordIso_trans)
lemma ordLeq_countable_subsets:
-"|A| \<le>o |{X. X \<subseteq> A \<and> countable X}|"
-apply (rule card_of_ordLeqI[of "\<lambda> a. {a}"]) unfolding inj_on_def by auto
+ "|A| \<le>o |{X. X \<subseteq> A \<and> countable X}|"
+proof -
+ have "\<And>a. a \<in> A \<Longrightarrow> {a} \<in> {X. X \<subseteq> A \<and> countable X}"
+ by auto
+ with card_of_ordLeqI[of "\<lambda> a. {a}"] show ?thesis
+ using inj_singleton by blast
+qed
end
lemma finite_countable_subset:
-"finite {X. X \<subseteq> A \<and> countable X} \<longleftrightarrow> finite A"
-apply (rule iffI)
- apply (erule contrapos_pp)
- apply (rule card_of_ordLeq_infinite)
- apply (rule ordLeq_countable_subsets)
- apply assumption
-apply (rule finite_Collect_conjI)
-apply (rule disjI1)
-apply (erule finite_Collect_subsets)
-done
+ "finite {X. X \<subseteq> A \<and> countable X} \<longleftrightarrow> finite A"
+ using card_of_ordLeq_infinite ordLeq_countable_subsets by force
lemma rcset_to_rcset: "countable A \<Longrightarrow> rcset (the_inv rcset A) = A"
including cset.lifting
- apply (rule f_the_inv_into_f[unfolded inj_on_def image_iff])
- apply transfer' apply simp
- apply transfer' apply simp
- done
+ by (meson CollectI f_the_inv_into_f inj_on_inverseI rangeI rcset_induct
+ rcset_inverse)
lemma Collect_Int_Times: "{(x, y). R x y} \<inter> A \<times> B = {(x, y). R x y \<and> x \<in> A \<and> y \<in> B}"
-by auto
+ by auto
lemma rel_cset_aux:
-"(\<forall>t \<in> rcset a. \<exists>u \<in> rcset b. R t u) \<and> (\<forall>t \<in> rcset b. \<exists>u \<in> rcset a. R u t) \<longleftrightarrow>
+ "(\<forall>t \<in> rcset a. \<exists>u \<in> rcset b. R t u) \<and> (\<forall>t \<in> rcset b. \<exists>u \<in> rcset a. R u t) \<longleftrightarrow>
((BNF_Def.Grp {x. rcset x \<subseteq> {(a, b). R a b}} (cimage fst))\<inverse>\<inverse> OO
BNF_Def.Grp {x. rcset x \<subseteq> {(a, b). R a b}} (cimage snd)) a b" (is "?L = ?R")
proof
@@ -626,7 +620,7 @@
fix R
show "rel_cset R = (\<lambda>x y. \<exists>z. rcset z \<subseteq> {(x, y). R x y} \<and>
cimage fst z = x \<and> cimage snd z = y)"
- unfolding rel_cset_alt_def[abs_def] rel_cset_aux[unfolded OO_Grp_alt] by simp
+ unfolding rel_cset_alt_def[abs_def] rel_cset_aux[unfolded OO_Grp_alt] by simp
qed(simp add: bot_cset.rep_eq)
end
--- a/src/HOL/Library/Infinite_Set.thy Fri Jan 24 14:35:47 2025 +0100
+++ b/src/HOL/Library/Infinite_Set.thy Fri Jan 24 17:53:17 2025 +0000
@@ -40,10 +40,7 @@
\<close>
lemma unbounded_k_infinite: "\<forall>m>k. \<exists>n>m. n \<in> S \<Longrightarrow> infinite (S::nat set)"
- apply (clarsimp simp add: finite_nat_set_iff_bounded)
- apply (drule_tac x="Suc (max m k)" in spec)
- using less_Suc_eq apply fastforce
- done
+ by (metis finite_nat_set_iff_bounded gt_ex order_less_not_sym order_less_trans)
lemma nat_not_finite: "finite (UNIV::nat set) \<Longrightarrow> R"
by simp
@@ -306,13 +303,14 @@
next
case (Suc n S)
show ?case
- using enumerate_mono[OF zero_less_Suc \<open>infinite S\<close>, of n] \<open>infinite S\<close>
- apply (subst (1 2) enumerate_Suc')
- apply (subst Suc)
- apply (use \<open>infinite S\<close> in simp)
- apply (intro arg_cong[where f = Least] ext)
- apply (auto simp flip: enumerate_Suc')
- done
+ proof (rule order.antisym)
+ have S: "infinite (S - {wellorder_class.enumerate S 0})"
+ using Suc by auto
+ show "wellorder_class.enumerate S (Suc (Suc n)) \<le> (LEAST s. s \<in> S \<and> wellorder_class.enumerate S (Suc n) < s)"
+ using enumerate_mono[OF zero_less_Suc] \<open>infinite S\<close> S
+ by (smt (verit, best) LeastI_ex Suc.hyps enumerate_0 enumerate_Suc enumerate_in_set
+ enumerate_step insertE insert_Diff linorder_not_less not_less_Least)
+ qed (simp add: Least_le Suc.prems enumerate_in_set)
qed
lemma enumerate_Ex:
@@ -424,10 +422,13 @@
by (metis all_not_in_conv card.empty enumerate.simps(1) not_less0 wellorder_Least_lemma(1))
next
case (Suc n)
+ then have "wellorder_class.enumerate (S - {LEAST n. n \<in> S}) n \<in> S"
+ by (metis Diff_empty Diff_insert0 Suc_lessD Suc_less_eq card.insert_remove
+ finite_Diff insert_Diff insert_Diff_single insert_iff)
+ then
show ?case
using Suc.prems Suc.IH [of "S - {LEAST n. n \<in> S}"]
- apply (simp add: enumerate.simps)
- by (metis Diff_empty Diff_insert0 Suc_lessD card.remove less_Suc_eq)
+ by (simp add: enumerate.simps)
qed
lemma finite_enumerate_step: "\<lbrakk>finite S; Suc n < card S\<rbrakk> \<Longrightarrow> enumerate S n < enumerate S (Suc n)"
--- a/src/HOL/Library/Mapping.thy Fri Jan 24 14:35:47 2025 +0100
+++ b/src/HOL/Library/Mapping.thy Fri Jan 24 17:53:17 2025 +0000
@@ -83,13 +83,7 @@
"(HOL.eq ===> rel_option A)
(\<lambda>k. if k < length xs then Some (xs ! k) else None)
(\<lambda>k. if k < length ys then Some (ys ! k) else None)"
- apply induct
- apply auto
- unfolding rel_fun_def
- apply clarsimp
- apply (case_tac xa)
- apply (auto dest: list_all2_lengthD list_all2_nthD)
- done
+ by induct (auto simp add: list_all2_lengthD list_all2_nthD rel_funI)
qed
lemma map_parametric:
@@ -225,11 +219,11 @@
definition "HOL.equal m1 m2 \<longleftrightarrow> (\<forall>k. lookup m1 k = lookup m2 k)"
instance
- apply standard
+proof
+ show "\<And>x y::('a, 'b) mapping. equal_class.equal x y = (x = y)"
unfolding equal_mapping_def
- apply transfer
- apply auto
- done
+ by transfer auto
+qed
end
@@ -656,10 +650,7 @@
lemma All_mapping_tabulate: "(\<forall>x\<in>set xs. P x (f x)) \<Longrightarrow> All_mapping (Mapping.tabulate xs f) P"
unfolding All_mapping_def
- apply (intro allI)
- apply transfer
- apply (auto split: option.split dest!: map_of_SomeD)
- done
+ by transfer (auto split: option.split dest!: map_of_SomeD)
lemma All_mapping_alist:
"(\<And>k v. (k, v) \<in> set xs \<Longrightarrow> P k v) \<Longrightarrow> All_mapping (Mapping.of_alist xs) P"
@@ -896,7 +887,7 @@
qed
from assms show ?thesis
unfolding ordered_entries_def
- apply (transfer fixing: k v) using "*" by auto
+ by (transfer fixing: k v) (use "*" in auto)
qed
lemma ordered_entries_delete[simp]: