merged

--- a/src/HOL/Quotient_Examples/Quotient_FSet.thy	Tue Mar 18 14:05:07 2025 +0100
+++ b/src/HOL/Quotient_Examples/Quotient_FSet.thy	Tue Mar 18 18:12:07 2025 +0000
@@ -404,11 +404,9 @@
 
 lemma Cons_rsp2 [quot_respect]:
   shows "((\<approx>) ===> list_all2 (\<approx>) OOO (\<approx>) ===> list_all2 (\<approx>) OOO (\<approx>)) Cons Cons"
-  apply (auto intro!: rel_funI)
-  apply (rule_tac b="x # b" in relcomppI)
-  apply auto
-  apply (rule_tac b="x # ba" in relcomppI)
-  apply auto
+  apply (clarsimp intro!: rel_funI)
+  apply (rule_tac b="x # b" in relcomppI, simp)
+  apply (rule_tac b="x # ba" in relcomppI, auto)
   done
 
 lemma Nil_prs2 [quot_preserve]:
@@ -436,37 +434,44 @@
   using a b by (induct z) (auto elim: reflpE)
 
 lemma append_rsp2_pre0:
-  assumes a:"list_all2 (\<approx>) x x'"
+  assumes "list_all2 (\<approx>) x x'"
   shows "list_all2 (\<approx>) (x @ z) (x' @ z)"
-  using a apply (induct x x' rule: list_induct2')
-  by simp_all (rule list_all2_refl'[OF list_eq_equivp])
+  using assms 
+proof (induct x x' rule: list_induct2')
+  case 1
+  then show ?case
+    using list_all2_refl' list_eq_equivp by blast
+qed auto
 
 lemma append_rsp2_pre1:
-  assumes a:"list_all2 (\<approx>) x x'"
+  assumes "list_all2 (\<approx>) x x'"
   shows "list_all2 (\<approx>) (z @ x) (z @ x')"
-  using a apply (induct x x' arbitrary: z rule: list_induct2')
-  apply (rule list_all2_refl'[OF list_eq_equivp])
-  apply (simp_all del: list_eq_def)
-  apply (rule list_all2_app_l)
-  apply (simp_all add: reflpI)
-  done
+  using assms 
+proof (induct x x' arbitrary: z rule: list_induct2')
+  case 1
+  then show ?case
+    using list_all2_refl' list_eq_equivp by blast
+next
+  case (4 x xs y ys)
+  then show ?case
+    using list_all2_app_l list_eq_reflp by blast
+qed auto
 
 lemma append_rsp2_pre:
   assumes "list_all2 (\<approx>) x x'"
     and "list_all2 (\<approx>) z z'"
   shows "list_all2 (\<approx>) (x @ z) (x' @ z')"
-  using assms by (rule list_all2_appendI)
+  using assms list_all2_appendI by blast
 
 lemma compositional_rsp3:
   assumes "(R1 ===> R2 ===> R3) C C" and "(R4 ===> R5 ===> R6) C C"
   shows "(R1 OOO R4 ===> R2 OOO R5 ===> R3 OOO R6) C C"
-  by (auto intro!: rel_funI)
-     (metis (full_types) assms rel_funE relcomppI)
+  using assms
+  by (simp add: OO_def rel_fun_def) metis
 
 lemma append_rsp2 [quot_respect]:
   "(list_all2 (\<approx>) OOO (\<approx>) ===> list_all2 (\<approx>) OOO (\<approx>) ===> list_all2 (\<approx>) OOO (\<approx>)) append append"
-  by (intro compositional_rsp3)
-     (auto intro!: rel_funI simp add: append_rsp2_pre)
+  by (simp add: append_transfer compositional_rsp3 sup_fset.rsp)
 
 lemma map_rsp2 [quot_respect]:
   "(((\<approx>) ===> (\<approx>)) ===> list_all2 (\<approx>) OOO (\<approx>) ===> list_all2 (\<approx>) OOO (\<approx>)) map map"
@@ -766,9 +771,8 @@
 
 lemma card_fset_Suc: 
   shows "card_fset S = Suc n \<Longrightarrow> \<exists>x T. x |\<notin>| T \<and> S = insert_fset x T \<and> card_fset T = n"
-  apply(descending)
-  apply(auto dest!: card_eq_SucD)
-  by (metis Diff_insert_absorb set_removeAll)
+  by (metis Suc_inject card_fset_0 card_notin_fset nat.simps(3) notin_remove_fset
+      remove_fset_cases)
 
 lemma card_remove_fset_iff [simp]:
   shows "card_fset (remove_fset y S) = (if y |\<in>| S then card_fset S - 1 else card_fset S)"
@@ -776,7 +780,7 @@
 
 lemma card_Suc_exists_in_fset: 
   shows "card_fset S = Suc n \<Longrightarrow> \<exists>a. a |\<in>| S"
-  by (drule card_fset_Suc) (auto)
+  using remove_fset_cases by force
 
 lemma in_card_fset_not_0: 
   shows "a |\<in>| A \<Longrightarrow> card_fset A \<noteq> 0"
@@ -804,9 +808,7 @@
 
 lemma card_union_disjoint_fset: 
   shows "xs |\<inter>| ys = {||} \<Longrightarrow> card_fset (xs |\<union>| ys) = card_fset xs + card_fset ys"
-  unfolding card_fset union_fset 
-  apply (rule card_Un_disjoint[OF finite_fset finite_fset])
-  by (metis inter_fset fset_simps(1))
+  by (simp add: card_union_inter_fset)
 
 lemma card_remove_fset_less1: 
   shows "x |\<in>| xs \<Longrightarrow> card_fset (remove_fset x xs) < card_fset xs"
@@ -914,12 +916,9 @@
 subsection \<open>Choice in fsets\<close>
 
 lemma fset_choice: 
-  assumes a: "\<forall>x. x |\<in>| A \<longrightarrow> (\<exists>y. P x y)"
+  assumes "\<forall>x. x |\<in>| A \<longrightarrow> (\<exists>y. P x y)"
   shows "\<exists>f. \<forall>x. x |\<in>| A \<longrightarrow> P x (f x)"
-  using a
-  apply(descending)
-  using finite_set_choice
-  by (auto simp add: Ball_def)
+  using assms by metis
 
 
 section \<open>Induction and Cases rules for fsets\<close>
@@ -969,39 +968,24 @@
 qed
 
 lemma fset_raw_strong_cases:
-  obtains "xs = []"
-    | ys x where "\<not> List.member ys x" and "xs \<approx> x # ys"
+  obtains "xs = []" | ys x where "\<not> List.member ys x" and "xs \<approx> x # ys"
 proof (induct xs)
   case Nil
   then show thesis by simp
 next
   case (Cons a xs)
-  have a: "\<lbrakk>xs = [] \<Longrightarrow> thesis; \<And>x ys. \<lbrakk>\<not> List.member ys x; xs \<approx> x # ys\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis"
-    by (rule Cons(1))
-  have b: "\<And>x' ys'. \<lbrakk>\<not> List.member ys' x'; a # xs \<approx> x' # ys'\<rbrakk> \<Longrightarrow> thesis" by fact
-  have c: "xs = [] \<Longrightarrow> thesis" using b 
-    apply(simp)
-    by (metis list.set(1) emptyE empty_subsetI)
-  have "\<And>x ys. \<lbrakk>\<not> List.member ys x; xs \<approx> x # ys\<rbrakk> \<Longrightarrow> thesis"
-  proof -
-    fix x :: 'a
-    fix ys :: "'a list"
-    assume d:"\<not> List.member ys x"
-    assume e:"xs \<approx> x # ys"
-    show thesis
-    proof (cases "x = a")
-      assume h: "x = a"
-      then have f: "\<not> List.member ys a" using d by simp
-      have g: "a # xs \<approx> a # ys" using e h by auto
-      show thesis using b f g by simp
-    next
-      assume h: "x \<noteq> a"
-      then have f: "\<not> List.member (a # ys) x" using d by auto
-      have g: "a # xs \<approx> x # (a # ys)" using e h by auto
-      show thesis using b f g by (simp del: List.member_def) 
-    qed
+  show ?case
+  proof (cases "xs=[]")
+    case True
+    then show ?thesis
+      using Cons.prems member_rec(2) by fastforce
+  next
+    case False
+    have "\<lbrakk>\<not> List.member ys x; xs \<approx> x # ys\<rbrakk> \<Longrightarrow> thesis" for x ys
+      using Cons.prems by auto
+    then show ?thesis
+      using Cons.hyps False by blast 
   qed
-  then show thesis using a c by blast
 qed
 
 
@@ -1017,12 +1001,15 @@
   (\<And>y ys. y |\<notin>| ys \<Longrightarrow> P {||} (insert_fset y ys)) \<Longrightarrow>
   (\<And>x xs y ys. \<lbrakk>P xs ys; x |\<notin>| xs; y |\<notin>| ys\<rbrakk> \<Longrightarrow> P (insert_fset x xs) (insert_fset y ys)) \<Longrightarrow>
   P xsa ysa"
-  apply (induct xsa arbitrary: ysa)
-  apply (induct_tac x rule: fset_induct_stronger)
-  apply simp_all
-  apply (induct_tac xa rule: fset_induct_stronger)
-  apply simp_all
-  done
+proof (induct xsa arbitrary: ysa)
+  case empty
+  then show ?case
+    by (meson fset_induct_stronger)
+next
+  case (insert x xsa)
+  then show ?case
+    by (metis fset_strong_cases)
+qed
 
 text \<open>Extensionality\<close>
 
@@ -1059,19 +1046,26 @@
   by (induct xs) (auto intro: list_eq2.intros)
 
 lemma cons_delete_list_eq2:
-  shows "(a # (removeAll a A)) \<approx>2 (if List.member A a then A else a # A)"
-  apply (induct A)
-  apply (simp add: list_eq2_refl)
-  apply (case_tac "List.member (aa # A) a")
-  apply (simp_all)
-  apply (case_tac [!] "a = aa")
-  apply (simp_all)
-  apply (case_tac "List.member A a")
-  apply (auto)[2]
-  apply (metis list_eq2.intros(3) list_eq2.intros(4) list_eq2.intros(5) list_eq2.intros(6))
-  apply (metis list_eq2.intros(1) list_eq2.intros(5) list_eq2.intros(6))
-  apply (auto simp add: list_eq2_refl)
-  done
+  shows "(a # (removeAll a xs)) \<approx>2 (if List.member xs a then xs else a # xs)"
+proof (induct xs)
+  case Nil
+  then show ?case
+    by (simp add: list_eq2_refl)
+next
+  case (Cons x xs)
+  show ?case
+  proof (cases "a=x")
+    case True
+    with Cons show ?thesis
+      apply (simp add: split: if_splits)
+      by (metis list_eq2.simps)
+  next
+    case False
+    with Cons show ?thesis
+      apply (simp add: )
+      by (smt (verit, ccfv_SIG) list_eq2.intros)
+  qed
+qed
 
 lemma member_delete_list_eq2:
   assumes a: "List.member r e"

--- a/src/HOL/Quotient_Examples/Quotient_Int.thy	Tue Mar 18 14:05:07 2025 +0100
+++ b/src/HOL/Quotient_Examples/Quotient_Int.thy	Tue Mar 18 18:12:07 2025 +0000
@@ -51,40 +51,21 @@
 where
   "times_int_raw (x, y) (u, v) = (x*u + y*v, x*v + y*u)"
 
-lemma times_int_raw_fst:
-  assumes a: "x \<approx> z"
-  shows "times_int_raw x y \<approx> times_int_raw z y"
-  using a
-  apply(cases x, cases y, cases z)
-  apply(auto simp add: times_int_raw.simps intrel.simps)
-  apply(hypsubst_thin)
-  apply(rename_tac u v w x y z)
-  apply(subgoal_tac "u*w + z*w = y*w + v*w  &  u*x + z*x = y*x + v*x")
-  apply(simp add: ac_simps)
-  apply(simp add: add_mult_distrib [symmetric])
-done
-
-lemma times_int_raw_snd:
-  assumes a: "x \<approx> z"
-  shows "times_int_raw y x \<approx> times_int_raw y z"
-  using a
-  apply(cases x, cases y, cases z)
-  apply(auto simp add: times_int_raw.simps intrel.simps)
-  apply(hypsubst_thin)
-  apply(rename_tac u v w x y z)
-  apply(subgoal_tac "u*w + z*w = y*w + v*w  &  u*x + z*x = y*x + v*x")
-  apply(simp add: ac_simps)
-  apply(simp add: add_mult_distrib [symmetric])
-done
+lemma times_int_raw:
+  assumes "x \<approx> z"
+  shows "times_int_raw x y \<approx> times_int_raw z y \<and> times_int_raw y x \<approx> times_int_raw y z"
+proof (cases x, cases y, cases z)
+  fix a a' b b' c c'
+  assume \<section>: "x = (a, a')" "y = (b, b')" "z = (c, c')"
+  then obtain "a*b + c'*b = c*b + a'*b" "a*b' + c'*b' = c*b' + a'*b'"
+    by (metis add_mult_distrib assms intrel.simps)
+  then show ?thesis
+    by (simp add: \<section> algebra_simps)
+qed
 
 quotient_definition
   "((*)) :: (int \<Rightarrow> int \<Rightarrow> int)" is "times_int_raw"
-  apply(rule equivp_transp[OF int_equivp])
-  apply(rule times_int_raw_fst)
-  apply(assumption)
-  apply(rule times_int_raw_snd)
-  apply(assumption)
-done
+  by (metis Quotient_Int.int.abs_eq_iff times_int_raw)
 
 fun
   le_int_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool"
@@ -143,14 +124,14 @@
      (simp)
 
 lemma add_abs_int:
-  "(abs_int (x,y)) + (abs_int (u,v)) =
-   (abs_int (x + u, y + v))"
-  apply(simp add: plus_int_def id_simps)
-  apply(fold plus_int_raw.simps)
-  apply(rule Quotient3_rel_abs[OF Quotient3_int])
-  apply(rule plus_int_raw_rsp_aux)
-  apply(simp_all add: rep_abs_rsp_left[OF Quotient3_int])
-  done
+  "(abs_int (x,y)) + (abs_int (u,v)) = (abs_int (x + u, y + v))"
+proof -
+  have "abs_int (plus_int_raw (rep_int (abs_int (x, y))) (rep_int (abs_int (u, v)))) 
+     = abs_int (plus_int_raw (x, y) (u, v))"
+  by (meson Quotient3_abs_rep Quotient3_int int.abs_eq_iff plus_int_raw_rsp_aux)
+  then show ?thesis
+    by (simp add: Quotient_Int.plus_int_def)
+qed
 
 definition int_of_nat_raw:
   "int_of_nat_raw m = (m :: nat, 0 :: nat)"
@@ -206,21 +187,24 @@
   fixes i j::int
   and   k::nat
   shows "i < j \<Longrightarrow> 0 < k \<Longrightarrow> of_nat k * i < of_nat k * j"
-  apply(induct "k")
-  apply(simp)
-  apply(case_tac "k = 0")
-  apply(simp_all add: distrib_right add_strict_mono)
-  done
+proof (induction "k")
+  case 0
+  then show ?case by simp
+next
+  case (Suc k)
+  then show ?case 
+    by (cases "k = 0"; simp add: distrib_right add_strict_mono)
+qed
 
 lemma zero_le_imp_eq_int_raw:
-  fixes k::"(nat \<times> nat)"
-  shows "less_int_raw (0, 0) k \<Longrightarrow> (\<exists>n > 0. k \<approx> int_of_nat_raw n)"
-  apply(cases k)
-  apply(simp add:int_of_nat_raw)
-  apply(auto)
-  apply(rule_tac i="b" and j="a" in less_Suc_induct)
-  apply(auto)
-  done
+  assumes "less_int_raw (0, 0) u"
+  shows "(\<exists>n > 0. u \<approx> int_of_nat_raw n)"
+proof -
+  have "\<And>a b::nat. \<lbrakk>b \<le> a; b \<noteq> a\<rbrakk> \<Longrightarrow> \<exists>n>0. a = n + b"
+    by (metis add.comm_neutral add.commute gr0I le_iff_add)
+  with assms show ?thesis
+    by (cases u) (simp add:int_of_nat_raw)
+qed
 
 lemma zero_le_imp_eq_int:
   fixes k::int
@@ -230,10 +214,10 @@
 
 lemma zmult_zless_mono2:
   fixes i j k::int
-  assumes a: "i < j" "0 < k"
+  assumes "i < j" "0 < k"
   shows "k * i < k * j"
-  using a
-  by (drule_tac zero_le_imp_eq_int) (auto simp add: zmult_zless_mono2_lemma)
+  using assms zmult_zless_mono2_lemma [of i j]
+  using Quotient_Int.zero_le_imp_eq_int by blast
 
 text\<open>The integers form an ordered integral domain\<close>