# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1287182754 -3600
# Node ID a8f5611dbd6541fbe339db8ef6dcd17b9d7ae935
# Parent  c9deccd1247675bd6f39739e1fbba19fa16e612c
more cleaning

diff -r c9deccd12476 -r a8f5611dbd65 Nominal/FSet.thy
--- a/Nominal/FSet.thy	Fri Oct 15 17:37:44 2010 +0100
+++ b/Nominal/FSet.thy	Fri Oct 15 23:45:54 2010 +0100
@@ -54,13 +54,13 @@
   "rsp_fold f \<equiv> \<forall>u v w. (f u (f v w) = f v (f u w))"
 
 primrec
-  ffold_raw :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a list \<Rightarrow> 'b"
+  ffold_list :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a list \<Rightarrow> 'b"
 where
-  "ffold_raw f z [] = z"
-| "ffold_raw f z (a # xs) =
+  "ffold_list f z [] = z"
+| "ffold_list f z (a # xs) =
      (if (rsp_fold f) then
-       if a \<in> set xs then ffold_raw f z xs
-       else f a (ffold_raw f z xs)
+       if a \<in> set xs then ffold_list f z xs
+       else f a (ffold_list f z xs)
      else z)"
 
 
@@ -196,14 +196,14 @@
   shows "(op = ===> op \<approx> ===> op \<approx>) filter filter"
   by simp
 
-lemma memb_commute_ffold_raw:
-  "rsp_fold f \<Longrightarrow> h \<in> set b \<Longrightarrow> ffold_raw f z b = f h (ffold_raw f z (removeAll h b))"
+lemma memb_commute_ffold_list:
+  "rsp_fold f \<Longrightarrow> h \<in> set b \<Longrightarrow> ffold_list f z b = f h (ffold_list f z (removeAll h b))"
   apply (induct b)
   apply (auto simp add: rsp_fold_def)
   done
 
-lemma ffold_raw_rsp_pre:
-  "set a = set b \<Longrightarrow> ffold_raw f z a = ffold_raw f z b"
+lemma ffold_list_rsp_pre:
+  "set a = set b \<Longrightarrow> ffold_list f z a = ffold_list f z b"
   apply (induct a arbitrary: b)
   apply (simp)
   apply (simp (no_asm_use))
@@ -212,18 +212,18 @@
   apply (rule_tac [!] conjI)
   apply (rule_tac [!] impI)
   apply (metis insert_absorb)
-  apply (metis List.insert_def List.set.simps(2) List.set_insert ffold_raw.simps(2))
-  apply (metis Diff_insert_absorb insertI1 memb_commute_ffold_raw set_removeAll)
+  apply (metis List.insert_def List.set.simps(2) List.set_insert ffold_list.simps(2))
+  apply (metis Diff_insert_absorb insertI1 memb_commute_ffold_list set_removeAll)
   apply(drule_tac x="removeAll a1 b" in meta_spec)
   apply(auto)
   apply(drule meta_mp)
   apply(blast)
-  by (metis List.set.simps(2) emptyE ffold_raw.simps(2) in_listsp_conv_set listsp.simps mem_def)
+  by (metis List.set.simps(2) emptyE ffold_list.simps(2) in_listsp_conv_set listsp.simps mem_def)
 
-lemma ffold_raw_rsp [quot_respect]:
-  shows "(op = ===> op = ===> op \<approx> ===> op =) ffold_raw ffold_raw"
+lemma ffold_list_rsp [quot_respect]:
+  shows "(op = ===> op = ===> op \<approx> ===> op =) ffold_list ffold_list"
   unfolding fun_rel_def
-  by(auto intro: ffold_raw_rsp_pre)
+  by(auto intro: ffold_list_rsp_pre)
 
 lemma concat_rsp_pre:
   assumes a: "list_all2 op \<approx> x x'"
@@ -266,6 +266,10 @@
 qed
 
 
+
+section {* Quotient definitions for fsets *}
+
+
 subsection {* Finite sets are a bounded, distributive lattice with minus *}
 
 instantiation fset :: (type) "{bounded_lattice_bot, distrib_lattice, minus}"
@@ -366,10 +370,6 @@
 
 end
 
-
-section {* Quotient definitions for fsets *}
-
-
 quotient_definition
   "finsert :: 'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
   is "Cons"
@@ -411,7 +411,7 @@
 
 quotient_definition
   "ffold :: ('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a fset \<Rightarrow> 'b"
-  is ffold_raw
+  is ffold_list
 
 quotient_definition
   "fconcat :: ('a fset) fset \<Rightarrow> 'a fset"
@@ -422,15 +422,13 @@
   is filter
 
 
-subsection {* Compositional Respectfulness and Preservation *}
+section {* Compositional respectfulness and preservation lemmas *}
 
-lemma [quot_respect]: "(list_all2 op \<approx> OOO op \<approx>) [] []"
+lemma Nil_rsp2 [quot_respect]: 
+  shows "(list_all2 op \<approx> OOO op \<approx>) Nil Nil"
   by (fact compose_list_refl)
 
-lemma  [quot_preserve]: "(abs_fset \<circ> map f) [] = abs_fset []"
-  by simp
-
-lemma [quot_respect]:
+lemma Cons_rsp2 [quot_respect]:
   shows "(op \<approx> ===> list_all2 op \<approx> OOO op \<approx> ===> list_all2 op \<approx> OOO op \<approx>) Cons Cons"
   apply auto
   apply (rule_tac b="x # b" in pred_compI)
@@ -439,12 +437,16 @@
   apply auto
   done
 
-lemma [quot_preserve]:
+lemma map_prs [quot_preserve]: 
+  shows "(abs_fset \<circ> map f) [] = abs_fset []"
+  by simp
+
+lemma finsert_rsp [quot_preserve]:
   "(rep_fset ---> (map rep_fset \<circ> rep_fset) ---> (abs_fset \<circ> map abs_fset)) op # = finsert"
   by (simp add: fun_eq_iff Quotient_abs_rep[OF Quotient_fset]
       abs_o_rep[OF Quotient_fset] map_id finsert_def)
 
-lemma [quot_preserve]:
+lemma funion_rsp [quot_preserve]:
   "((map rep_fset \<circ> rep_fset) ---> (map rep_fset \<circ> rep_fset) ---> (abs_fset \<circ> map abs_fset)) op @ = funion"
   by (simp add: fun_eq_iff Quotient_abs_rep[OF Quotient_fset]
       abs_o_rep[OF Quotient_fset] map_id sup_fset_def)
@@ -487,7 +489,7 @@
   done
 
 lemma [quot_respect]:
-  "(list_all2 op \<approx> OOO op \<approx> ===> list_all2 op \<approx> OOO op \<approx> ===> list_all2 op \<approx> OOO op \<approx>) op @ op @"
+  "(list_all2 op \<approx> OOO op \<approx> ===> list_all2 op \<approx> OOO op \<approx> ===> list_all2 op \<approx> OOO op \<approx>) append append"
 proof (intro fun_relI, elim pred_compE)
   fix x y z w x' z' y' w' :: "'a list list"
   assume a:"list_all2 op \<approx> x x'"
@@ -507,125 +509,6 @@
 
 
 
-section {* Cases *}
-
-
-lemma fset_raw_strong_cases:
-  obtains "xs = []"
-    | x ys where "\<not> memb x ys" and "xs \<approx> x # ys"
-proof (induct xs arbitrary: x ys)
-  case Nil
-  then show thesis by simp
-next
-  case (Cons a xs)
-  have a: "\<lbrakk>xs = [] \<Longrightarrow> thesis; \<And>x ys. \<lbrakk>\<not> memb x ys; xs \<approx> x # ys\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis" by fact
-  have b: "\<And>x' ys'. \<lbrakk>\<not> memb x' ys'; a # xs \<approx> x' # ys'\<rbrakk> \<Longrightarrow> thesis" by fact
-  have c: "xs = [] \<Longrightarrow> thesis" using b unfolding memb_def
-    by (metis in_set_conv_nth less_zeroE list.size(3) list_eq.simps member_set)
-  have "\<And>x ys. \<lbrakk>\<not> memb x ys; xs \<approx> x # ys\<rbrakk> \<Longrightarrow> thesis"
-  proof -
-    fix x :: 'a
-    fix ys :: "'a list"
-    assume d:"\<not> memb x ys"
-    assume e:"xs \<approx> x # ys"
-    show thesis
-    proof (cases "x = a")
-      assume h: "x = a"
-      then have f: "\<not> memb a ys" 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> memb x (a # ys)" using d unfolding memb_def by auto
-      have g: "a # xs \<approx> x # (a # ys)" using e h by auto
-      show thesis using b f g by simp
-    qed
-  qed
-  then show thesis using a c by blast
-qed
-
-
-text {* alternate formulation with a different decomposition principle
-  and a proof of equivalence *}
-
-inductive
-  list_eq2
-where
-  "list_eq2 (a # b # xs) (b # a # xs)"
-| "list_eq2 [] []"
-| "list_eq2 xs ys \<Longrightarrow> list_eq2 ys xs"
-| "list_eq2 (a # a # xs) (a # xs)"
-| "list_eq2 xs ys \<Longrightarrow> list_eq2 (a # xs) (a # ys)"
-| "\<lbrakk>list_eq2 xs1 xs2; list_eq2 xs2 xs3\<rbrakk> \<Longrightarrow> list_eq2 xs1 xs3"
-
-lemma list_eq2_refl:
-  shows "list_eq2 xs xs"
-  by (induct xs) (auto intro: list_eq2.intros)
-
-lemma cons_delete_list_eq2:
-  shows "list_eq2 (a # (removeAll a A)) (if memb a A then A else a # A)"
-  apply (induct A)
-  apply (simp add: memb_def list_eq2_refl)
-  apply (case_tac "memb a (aa # A)")
-  apply (simp_all only: memb_def)
-  apply (case_tac [!] "a = aa")
-  apply (simp_all)
-  apply (case_tac "memb a A")
-  apply (auto simp add: memb_def)[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 memb_def)
-  done
-
-lemma memb_delete_list_eq2:
-  assumes a: "memb e r"
-  shows "list_eq2 (e # removeAll e r) r"
-  using a cons_delete_list_eq2[of e r]
-  by simp
-
-lemma list_eq2_equiv:
-  "(l \<approx> r) \<longleftrightarrow> (list_eq2 l 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 "list_eq2 l r"
-      using a b
-    proof (induct n arbitrary: l r)
-      case 0
-      have "card_list l = 0" by fact
-      then have "\<forall>x. \<not> memb x l" unfolding card_list_def memb_def by auto
-      then have z: "l = []" unfolding memb_def by auto
-      then have "r = []" using `l \<approx> r` 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. memb a l" 
-	apply(simp add: card_list_def memb_def)
-	apply(drule card_eq_SucD)
-	apply(blast)
-	done
-      then obtain a where e: "memb a l" by auto
-      then have e': "memb a r" using list_eq.simps[simplified memb_def[symmetric], of l r] b 
-	unfolding memb_def by auto
-      have f: "card_list (removeAll a l) = m" using e d by (simp add: card_list_def memb_def)
-      have g: "removeAll a l \<approx> removeAll a r" using removeAll_rsp b by simp
-      have "list_eq2 (removeAll a l) (removeAll a r)" by (rule Suc.hyps[OF f g])
-      then have h: "list_eq2 (a # removeAll a l) (a # removeAll a r)" by (rule list_eq2.intros(5))
-      have i: "list_eq2 l (a # removeAll a l)"
-        by (rule list_eq2.intros(3)[OF memb_delete_list_eq2[OF e]])
-      have "list_eq2 l (a # removeAll a r)" by (rule list_eq2.intros(6)[OF i h])
-      then show ?case using list_eq2.intros(6)[OF _ memb_delete_list_eq2[OF e']] by simp
-    qed
-    }
-  then show "l \<approx> r \<Longrightarrow> list_eq2 l r" by blast
-qed
-
-
 section {* Lifted theorems *}
 
 
@@ -836,18 +719,10 @@
   shows "xs |\<subseteq>| ys = (\<forall>x. x |\<in>| xs \<longrightarrow> x |\<in>| ys)"
   by (descending) (auto simp add: sub_list_def memb_def)
 
-(* FIXME: no type ord *)
-(*
-lemma fsubset_finsert:
-  shows "(finsert x xs) |\<subset>| ys \<longleftrightarrow> x |\<in>| ys \<and> xs |\<subset>| ys"
-  by (descending) (simp add: sub_list_def memb_def)
-*)
-
 lemma fsubseteq_fempty:
   shows "xs |\<subseteq>| {||} \<longleftrightarrow> xs = {||}"
   by (descending) (simp add: sub_list_def)
 
-(* also problem with ord *)
 lemma not_fsubset_fnil: 
   shows "\<not> xs |\<subset>| {||}"
   by (metis fset_simps(1) fsubset_set not_psubset_empty)
@@ -1043,7 +918,7 @@
 
 lemma fin_commute_ffold:
   "\<lbrakk>rsp_fold f; h |\<in>| b\<rbrakk> \<Longrightarrow> ffold f z b = f h (ffold f z (fdelete h b))"
-  by (descending) (simp add: memb_def memb_commute_ffold_raw)
+  by (descending) (simp add: memb_def memb_commute_ffold_list)
 
 
 subsection {* Choice in fsets *}
@@ -1057,38 +932,92 @@
   by (auto simp add: memb_def Ball_def)
 
 
-(* FIXME: is that in any way useful *)  
+section {* Induction and Cases rules for fsets *}
+
+lemma fset_exhaust [case_names fempty finsert, cases type: fset]:
+  assumes fempty_case: "S = {||} \<Longrightarrow> P" 
+  and     finsert_case: "\<And>x S'. S = finsert x S' \<Longrightarrow> P"
+  shows "P"
+  using assms by (lifting list.exhaust)
 
+lemma fset_induct [case_names fempty finsert]:
+  assumes fempty_case: "P {||}"
+  and     finsert_case: "\<And>x S. P S \<Longrightarrow> P (finsert x S)"
+  shows "P S"
+  using assms 
+  by (descending) (blast intro: list.induct)
+
+lemma fset_induct_stronger [case_names fempty finsert, induct type: fset]:
+  assumes fempty_case: "P {||}"
+  and     finsert_case: "\<And>x S. \<lbrakk>x |\<notin>| S; P S\<rbrakk> \<Longrightarrow> P (finsert x S)"
+  shows "P S"
+proof(induct S rule: fset_induct)
+  case fempty
+  show "P {||}" using fempty_case by simp
+next
+  case (finsert x S)
+  have "P S" by fact
+  then show "P (finsert x S)" using finsert_case 
+    by (cases "x |\<in>| S") (simp_all)
+qed
 
+lemma fcard_induct:
+  assumes fempty_case: "P {||}"
+  and     fcard_Suc_case: "\<And>S T. Suc (fcard S) = (fcard T) \<Longrightarrow> P S \<Longrightarrow> P T"
+  shows "P S"
+proof (induct S)
+  case fempty
+  show "P {||}" by (rule fempty_case)
+next
+  case (finsert x S)
+  have h: "P S" by fact
+  have "x |\<notin>| S" by fact
+  then have "Suc (fcard S) = fcard (finsert x S)" 
+    using fcard_suc by auto
+  then show "P (finsert x S)" 
+    using h fcard_Suc_case by simp
+qed
 
-section {* Induction and Cases rules for fsets *}
+lemma fset_raw_strong_cases:
+  obtains "xs = []"
+    | x ys where "\<not> memb x ys" and "xs \<approx> x # ys"
+proof (induct xs arbitrary: x ys)
+  case Nil
+  then show thesis by simp
+next
+  case (Cons a xs)
+  have a: "\<lbrakk>xs = [] \<Longrightarrow> thesis; \<And>x ys. \<lbrakk>\<not> memb x ys; xs \<approx> x # ys\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis" by fact
+  have b: "\<And>x' ys'. \<lbrakk>\<not> memb x' ys'; a # xs \<approx> x' # ys'\<rbrakk> \<Longrightarrow> thesis" by fact
+  have c: "xs = [] \<Longrightarrow> thesis" using b unfolding memb_def
+    by (metis in_set_conv_nth less_zeroE list.size(3) list_eq.simps member_set)
+  have "\<And>x ys. \<lbrakk>\<not> memb x ys; xs \<approx> x # ys\<rbrakk> \<Longrightarrow> thesis"
+  proof -
+    fix x :: 'a
+    fix ys :: "'a list"
+    assume d:"\<not> memb x ys"
+    assume e:"xs \<approx> x # ys"
+    show thesis
+    proof (cases "x = a")
+      assume h: "x = a"
+      then have f: "\<not> memb a ys" 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> memb x (a # ys)" using d unfolding memb_def by auto
+      have g: "a # xs \<approx> x # (a # ys)" using e h by auto
+      show thesis using b f g by simp
+    qed
+  qed
+  then show thesis using a c by blast
+qed
+
 
 lemma fset_strong_cases:
   obtains "xs = {||}"
     | x ys where "x |\<notin>| ys" and "xs = finsert x ys"
   by (lifting fset_raw_strong_cases)
 
-lemma fset_exhaust[case_names fempty finsert, cases type: fset]:
-  shows "\<lbrakk>S = {||} \<Longrightarrow> P; \<And>x S'. S = finsert x S' \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
-  by (lifting list.exhaust)
-
-lemma fset_induct_weak[case_names fempty finsert]:
-  shows "\<lbrakk>P {||}; \<And>x S. P S \<Longrightarrow> P (finsert x S)\<rbrakk> \<Longrightarrow> P S"
-  by (lifting list.induct)
-
-lemma fset_induct[case_names fempty finsert, induct type: fset]:
-  assumes prem1: "P {||}"
-  and     prem2: "\<And>x S. \<lbrakk>x |\<notin>| S; P S\<rbrakk> \<Longrightarrow> P (finsert x S)"
-  shows "P S"
-proof(induct S rule: fset_induct_weak)
-  case fempty
-  show "P {||}" by (rule prem1)
-next
-  case (finsert x S)
-  have asm: "P S" by fact
-  show "P (finsert x S)"
-    by (cases "x |\<in>| S") (simp_all add: asm prem2)
-qed
 
 lemma fset_induct2:
   "P {||} {||} \<Longrightarrow>
@@ -1097,24 +1026,140 @@
   (\<And>x xs y ys. \<lbrakk>P xs ys; x |\<notin>| xs; y |\<notin>| ys\<rbrakk> \<Longrightarrow> P (finsert x xs) (finsert y ys)) \<Longrightarrow>
   P xsa ysa"
   apply (induct xsa arbitrary: ysa)
-  apply (induct_tac x rule: fset_induct)
+  apply (induct_tac x rule: fset_induct_stronger)
   apply simp_all
-  apply (induct_tac xa rule: fset_induct)
+  apply (induct_tac xa rule: fset_induct_stronger)
   apply simp_all
   done
 
-lemma fset_fcard_induct:
-  assumes a: "P {||}"
-  and     b: "\<And>xs ys. Suc (fcard xs) = (fcard ys) \<Longrightarrow> P xs \<Longrightarrow> P ys"
-  shows "P zs"
-proof (induct zs)
-  show "P {||}" by (rule a)
+
+
+subsection {* alternate formulation with a different decomposition principle
+  and a proof of equivalence *}
+
+inductive
+  list_eq2 ("_ \<approx>2 _")
+where
+  "(a # b # xs) \<approx>2 (b # a # xs)"
+| "[] \<approx>2 []"
+| "xs \<approx>2 ys \<Longrightarrow>  ys \<approx>2 xs"
+| "(a # a # xs) \<approx>2 (a # xs)"
+| "xs \<approx>2 ys \<Longrightarrow>  (a # xs) \<approx>2 (a # ys)"
+| "\<lbrakk>xs1 \<approx>2 xs2;  xs2 \<approx>2 xs3\<rbrakk> \<Longrightarrow> xs1 \<approx>2 xs3"
+
+lemma list_eq2_refl:
+  shows "xs \<approx>2 xs"
+  by (induct xs) (auto intro: list_eq2.intros)
+
+lemma list_eq2_set:
+  assumes a: "xs \<approx>2 ys"
+  shows "set xs = set ys"
+using a by (induct) (auto)
+
+lemma list_eq2_card:
+  assumes a: "xs \<approx>2 ys"
+  shows "card_list xs = card_list ys"
+using a 
+apply(induct) 
+apply(auto simp add: card_list_def)
+apply(metis insert_commute)
+apply(metis list_eq2_set)
+done
+
+lemma list_eq2_equiv1:
+  assumes a: "xs \<approx>2 ys"
+  shows "xs \<approx> ys"
+using a by (induct) (auto)
+
+
+lemma cons_delete_list_eq2:
+  shows "(a # (removeAll a A)) \<approx>2 (if memb a A then A else a # A)"
+  apply (induct A)
+  apply (simp add: memb_def list_eq2_refl)
+  apply (case_tac "memb a (aa # A)")
+  apply (simp_all only: memb_def)
+  apply (case_tac [!] "a = aa")
+  apply (simp_all)
+  apply (case_tac "memb a A")
+  apply (auto simp add: memb_def)[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 memb_def)
+  done
+
+lemma memb_delete_list_eq2:
+  assumes a: "memb e r"
+  shows "(e # removeAll e r) \<approx>2 r"
+  using a cons_delete_list_eq2[of e r]
+  by simp
+
+(*
+lemma list_eq2_equiv2:
+  assumes a: "xs \<approx> ys"
+  shows "xs \<approx>2 ys"
+using a
+apply(induct xs arbitrary: ys taking: "card o set" rule: measure_induct)
+apply(simp)
+apply(case_tac x)
+apply(simp)
+apply(auto intro: list_eq2.intros)[1]
+apply(simp)
+apply(case_tac "a \<in> set list")
+apply(simp add: insert_absorb)
+apply(drule_tac x="removeAll a ys" in spec)
+apply(drule mp)
+apply(simp)
+apply(subgoal_tac "0 < card (set ys)")
+apply(simp)
+apply(metis length_pos_if_in_set length_remdups_card_conv set_remdups)
+apply(simp)
+apply(clarify)
+apply(drule_tac x="removeAll a list" in spec)
+apply(drule mp)
+apply(simp)
+oops
+*)
+
+lemma list_eq2_equiv:
+  "(l \<approx> r) \<longleftrightarrow> (list_eq2 l r)"
+proof
+  show "list_eq2 l r \<Longrightarrow> l \<approx> r" by (induct rule: list_eq2.induct) auto
 next
-  fix x :: 'a and zs :: "'a fset"
-  assume h: "P zs"
-  assume "x |\<notin>| zs"
-  then have H1: "Suc (fcard zs) = fcard (finsert x zs)" using fcard_suc by auto
-  then show "P (finsert x zs)" using b h by simp
+  {
+    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> memb x l" unfolding card_list_def memb_def by auto
+      then have z: "l = []" unfolding memb_def by auto
+      then have "r = []" using `l \<approx> r` 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. memb a l" 
+	apply(simp add: card_list_def memb_def)
+	apply(drule card_eq_SucD)
+	apply(blast)
+	done
+      then obtain a where e: "memb a l" by auto
+      then have e': "memb a r" using list_eq.simps[simplified memb_def[symmetric], of l r] b 
+	unfolding memb_def by auto
+      have f: "card_list (removeAll a l) = m" using e d by (simp add: card_list_def memb_def)
+      have g: "removeAll a l \<approx> removeAll a r" using removeAll_rsp b by simp
+      have "list_eq2 (removeAll a l) (removeAll a r)" by (rule Suc.hyps[OF f g])
+      then have h: "list_eq2 (a # removeAll a l) (a # removeAll a r)" by (rule list_eq2.intros(5))
+      have i: "list_eq2 l (a # removeAll a l)"	
+        by (rule list_eq2.intros(3)[OF memb_delete_list_eq2[OF e]])
+      have "list_eq2 l (a # removeAll a r)" by (rule list_eq2.intros(6)[OF i h])
+      then show ?case using list_eq2.intros(6)[OF _ memb_delete_list_eq2[OF e']] by simp
+    qed
+    }
+  then show "l \<approx> r \<Longrightarrow> list_eq2 l r" by blast
 qed
 
 
@@ -1144,14 +1189,6 @@
   by (lifting list_eq2.induct[simplified list_eq2_equiv[symmetric]])
 
 
-
-section {* lemmas transferred from Finite_Set theory *}
-
-text {* finiteness for finite sets holds *}
-
-
-
-
 lemma list_all2_refl:
   assumes q: "equivp R"
   shows "(list_all2 R) r r"
@@ -1231,5 +1268,6 @@
 
 no_notation
   list_eq (infix "\<approx>" 50)
+and list_eq2 (infix "\<approx>2" 50)
 
 end