# HG changeset patch
# User paulson
# Date 1737753882 0
# Node ID d6906956ba341322e81074dc1907e16bbbbe19e3
# Parent  82cf33956a172c509d14544e18159766288f8cb5# Parent  6065afce538af119c4f07eb6782dcb7c6de6a910
merged

diff -r 82cf33956a17 -r d6906956ba34 src/HOL/Library/Code_Abstract_Nat.thy
--- a/src/HOL/Library/Code_Abstract_Nat.thy	Fri Jan 24 20:05:01 2025 +0100
+++ b/src/HOL/Library/Code_Abstract_Nat.thy	Fri Jan 24 21:24:42 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
diff -r 82cf33956a17 -r d6906956ba34 src/HOL/Library/Code_Binary_Nat.thy
--- a/src/HOL/Library/Code_Binary_Nat.thy	Fri Jan 24 20:05:01 2025 +0100
+++ b/src/HOL/Library/Code_Binary_Nat.thy	Fri Jan 24 21:24:42 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> _"]]
 
diff -r 82cf33956a17 -r d6906956ba34 src/HOL/Library/Countable_Set_Type.thy
--- a/src/HOL/Library/Countable_Set_Type.thy	Fri Jan 24 20:05:01 2025 +0100
+++ b/src/HOL/Library/Countable_Set_Type.thy	Fri Jan 24 21:24:42 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
diff -r 82cf33956a17 -r d6906956ba34 src/HOL/Library/Infinite_Set.thy
--- a/src/HOL/Library/Infinite_Set.thy	Fri Jan 24 20:05:01 2025 +0100
+++ b/src/HOL/Library/Infinite_Set.thy	Fri Jan 24 21:24:42 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)"
diff -r 82cf33956a17 -r d6906956ba34 src/HOL/Library/Mapping.thy
--- a/src/HOL/Library/Mapping.thy	Fri Jan 24 20:05:01 2025 +0100
+++ b/src/HOL/Library/Mapping.thy	Fri Jan 24 21:24:42 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]: