--- a/src/HOL/Quotient_Examples/Quotient_FSet.thy Tue Oct 08 15:44:52 2024 +0200
+++ b/src/HOL/Quotient_Examples/Quotient_FSet.thy Tue Oct 08 16:13:02 2024 +0200
@@ -1043,7 +1043,7 @@
and a proof of equivalence\<close>
inductive
- list_eq2 :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" (\<open>_ \<approx>2 _\<close>)
+ list_eq2 :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" (infix \<open>\<approx>2\<close> 50)
where
"(a # b # xs) \<approx>2 (b # a # xs)"
| "[] \<approx>2 []"
@@ -1077,45 +1077,35 @@
using a cons_delete_list_eq2[of e r]
by simp
-lemma list_eq2_equiv:
- "(l \<approx> r) \<longleftrightarrow> (list_eq2 l r)"
+lemma list_eq2_equiv: "l \<approx> r \<longleftrightarrow> l \<approx>2 r"
proof
- show "list_eq2 l r \<Longrightarrow> l \<approx> r" by (induct rule: list_eq2.induct) auto
-next
- {
- fix n
- assume a: "card_list l = n" and b: "l \<approx> r"
- have "l \<approx>2 r"
- using a b
- proof (induct n arbitrary: l r)
- case 0
- have "card_list l = 0" by fact
- then have "\<forall>x. \<not> List.member l x" by auto
- then have z: "l = []" by auto
- then have "r = []" using \<open>l \<approx> r\<close> by simp
- then show ?case using z list_eq2_refl by simp
- next
- case (Suc m)
- have b: "l \<approx> r" by fact
- have d: "card_list l = Suc m" by fact
- then have "\<exists>a. List.member l a"
- apply(simp)
- apply(drule card_eq_SucD)
- apply(blast)
- done
- then obtain a where e: "List.member l a" by auto
- then have e': "List.member r a" using list_eq_def [simplified List.member_def [symmetric], of l r] b
- by auto
- have f: "card_list (removeAll a l) = m" using e d by (simp)
- have g: "removeAll a l \<approx> removeAll a r" using remove_fset.rsp b by simp
- have "(removeAll a l) \<approx>2 (removeAll a r)" by (rule Suc.hyps[OF f g])
- then have h: "(a # removeAll a l) \<approx>2 (a # removeAll a r)" by (rule list_eq2.intros(5))
- have i: "l \<approx>2 (a # removeAll a l)"
- by (rule list_eq2.intros(3)[OF member_delete_list_eq2[OF e]])
- have "l \<approx>2 (a # removeAll a r)" by (rule list_eq2.intros(6)[OF i h])
- then show ?case using list_eq2.intros(6)[OF _ member_delete_list_eq2[OF e']] by simp
- qed
- }
+ show "l \<approx>2 r \<Longrightarrow> l \<approx> r"
+ by (induct rule: list_eq2.induct) auto
+ have "card_list l = n \<Longrightarrow> l \<approx> r \<Longrightarrow> l \<approx>2 r" for n
+ proof (induct n arbitrary: l r)
+ case 0
+ have "card_list l = 0" by fact
+ then have "\<forall>x. \<not> List.member l x" by auto
+ then have z: "l = []" by auto
+ then have "r = []" using \<open>l \<approx> r\<close> by simp
+ then show ?case using z list_eq2_refl by simp
+ next
+ case (Suc m)
+ have b: "l \<approx> r" by fact
+ have d: "card_list l = Suc m" by fact
+ then have "\<exists>a. List.member l a" by (auto dest: card_eq_SucD)
+ then obtain a where e: "List.member l a" by auto
+ then have e': "List.member r a" using list_eq_def [simplified List.member_def [symmetric], of l r] b
+ by auto
+ have f: "card_list (removeAll a l) = m" using e d by (simp)
+ have g: "removeAll a l \<approx> removeAll a r" using remove_fset.rsp b by simp
+ have "(removeAll a l) \<approx>2 (removeAll a r)" by (rule Suc.hyps[OF f g])
+ then have h: "(a # removeAll a l) \<approx>2 (a # removeAll a r)" by (rule list_eq2.intros(5))
+ have i: "l \<approx>2 (a # removeAll a l)"
+ by (rule list_eq2.intros(3)[OF member_delete_list_eq2[OF e]])
+ have "l \<approx>2 (a # removeAll a r)" by (rule list_eq2.intros(6)[OF i h])
+ then show ?case using list_eq2.intros(6)[OF _ member_delete_list_eq2[OF e']] by simp
+ qed
then show "l \<approx> r \<Longrightarrow> l \<approx>2 r" by blast
qed
@@ -1145,13 +1135,6 @@
using assms
by (lifting list_eq2.induct[simplified list_eq2_equiv[symmetric]])
-ML \<open>
-fun dest_fsetT \<^Type>\<open>fset T\<close> = T
- | dest_fsetT T = raise TYPE ("dest_fsetT: fset type expected", [T], []);
-\<close>
-
-no_notation
- list_eq (infix \<open>\<approx>\<close> 50) and
- list_eq2 (infix \<open>\<approx>2\<close> 50)
+no_notation list_eq (infix \<open>\<approx>\<close> 50) and list_eq2 (infix \<open>\<approx>2\<close> 50)
end