--- 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