--- a/Nominal/FSet.thy	Mon Apr 19 15:37:33 2010 +0200
+++ b/Nominal/FSet.thy	Mon Apr 19 15:37:54 2010 +0200
@@ -15,9 +15,38 @@
 
 lemma list_eq_equivp:
   shows "equivp list_eq"
-unfolding equivp_reflp_symp_transp 
-unfolding reflp_def symp_def transp_def
-by auto
+  unfolding equivp_reflp_symp_transp 
+  unfolding reflp_def symp_def transp_def
+  by auto
+
+definition
+  memb :: "'a \<Rightarrow> 'a list \<Rightarrow> bool"
+where
+  "memb x xs \<equiv> x \<in> set xs"
+
+definition
+  sub_list :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"
+where
+  "sub_list xs ys \<equiv> (\<forall>x. x \<in> set xs \<longrightarrow> x \<in> set ys)"
+
+lemma sub_list_cons:
+  "sub_list (x # xs) ys = (memb x ys \<and> sub_list xs ys)"
+  by (auto simp add: memb_def sub_list_def)
+
+lemma nil_not_cons:
+  shows "\<not> ([] \<approx> x # xs)"
+  and   "\<not> (x # xs \<approx> [])"
+  by auto
+
+lemma sub_list_rsp1: "\<lbrakk>xs \<approx> ys\<rbrakk> \<Longrightarrow> sub_list xs zs = sub_list ys zs"
+  by (simp add: sub_list_def)
+
+lemma sub_list_rsp2: "\<lbrakk>xs \<approx> ys\<rbrakk> \<Longrightarrow> sub_list zs xs = sub_list zs ys"
+  by (simp add: sub_list_def)
+
+lemma [quot_respect]:
+  "(op \<approx> ===> op \<approx> ===> op =) sub_list sub_list"
+  by (auto simp only: fun_rel_def sub_list_rsp1 sub_list_rsp2)
 
 quotient_type
   'a fset = "'a list" / "list_eq"
@@ -42,11 +71,6 @@
   "{|x, xs|}" == "CONST finsert x {|xs|}"
   "{|x|}"     == "CONST finsert x {||}"
 
-definition
-  memb :: "'a \<Rightarrow> 'a list \<Rightarrow> bool"
-where
-  "memb x xs \<equiv> x \<in> set xs"
-
 quotient_definition
   fin ("_ |\<in>| _" [50, 51] 50)
 where
@@ -71,11 +95,6 @@
 
 section {* Augmenting an fset -- @{const finsert} *}
 
-lemma nil_not_cons:
-  shows "\<not> ([] \<approx> x # xs)"
-  and   "\<not> (x # xs \<approx> [])"
-  by auto
-
 lemma not_memb_nil:
   shows "\<not> memb x []"
   by (simp add: memb_def)
@@ -351,9 +370,8 @@
   apply auto
   apply (drule_tac x="e" in spec)
   apply blast
-  apply (simp add: memb_cons_iff)
-  apply (metis Nitpick.list_size_simp(2) ffold_raw.simps(2)
-    length_Suc_conv memb_absorb nil_not_cons(2))
+  apply (case_tac b)
+  apply simp_all
   apply (subgoal_tac "ffold_raw f z b = f a1 (ffold_raw f z (delete_raw b a1))")
   apply (simp only:)
   apply (rule_tac f="f a1" in arg_cong)
@@ -364,8 +382,9 @@
   apply (erule memb_commute_ffold_raw)
   apply (drule_tac x="a1" in spec)
   apply (simp add: memb_cons_iff)
-  apply (metis Nitpick.list_size_simp(2) ffold_raw.simps(2)
-    length_Suc_conv memb_absorb memb_cons_iff nil_not_cons(2))
+  apply (simp add: memb_cons_iff)
+  apply (case_tac b)
+  apply simp_all
   done
 
 lemma [quot_respect]:
@@ -441,6 +460,79 @@
   shows "(op \<approx> ===> op \<approx> ===> op =) op \<approx> op \<approx>"
   by auto
 
+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 # (delete_raw 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_cons_iff)
+  apply (case_tac [!] "a = aa")
+  apply (simp_all add: delete_raw.simps)
+  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 delete_raw.simps(2) list_eq2.intros(1) list_eq2.intros(5) list_eq2.intros(6))
+  apply (auto simp add: list_eq2_refl not_memb_delete_raw_ident)
+  done
+
+lemma memb_delete_list_eq2:
+  assumes a: "memb e r"
+  shows "list_eq2 (e # delete_raw r e) r"
+  using a cons_delete_list_eq2[of e r]
+  by simp
+
+lemma list_eq2_equiv_aux:
+  assumes a: "fcard_raw l = n"
+  and b: "l \<approx> r"
+  shows "list_eq2 l r"
+using a b
+proof (induct n arbitrary: l r)
+  case 0
+  have "fcard_raw l = 0" by fact
+  then have "\<forall>x. \<not> memb x l" using memb_card_not_0[of _ l] by auto
+  then have z: "l = []" using no_memb_nil by auto
+  then have "r = []" sorry
+  then show ?case using z list_eq2_refl by simp
+next
+  case (Suc m)
+  have b: "l \<approx> r" by fact
+  have d: "fcard_raw l = Suc m" by fact
+  have "\<exists>a. memb a l" by (rule fcard_raw_suc_memb[OF d])
+  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 by auto
+  have f: "fcard_raw (delete_raw l a) = m" using fcard_raw_delete[of l a] e d by simp
+  have g: "delete_raw l a \<approx> delete_raw r a" using delete_raw_rsp[OF b] by simp
+  have g': "list_eq2 (delete_raw l a) (delete_raw r a)" by (rule Suc.hyps[OF f g])
+  have h: "list_eq2 (a # delete_raw l a) (a # delete_raw r a)" by (rule list_eq2.intros(5)[OF g'])
+  have i: "list_eq2 l (a # delete_raw l a)" by (rule list_eq2.intros(3)[OF memb_delete_list_eq2[OF e]])
+  have "list_eq2 l (a # delete_raw r a)" 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
+
+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
+  show "l \<approx> r \<Longrightarrow> list_eq2 l r" using list_eq2_equiv_aux by blast
+qed
+
 section {* lifted part *}
 
 lemma not_fin_fnil: "x |\<notin>| {||}"
@@ -531,7 +623,7 @@
   by (lifting fcard_raw_suc_memb)
 
 lemma fin_fcard_not_0: "a |\<in>| A \<Longrightarrow> fcard A \<noteq> 0"
-  by (lifting mem_card_not_0)
+  by (lifting memb_card_not_0)
 
 text {* funion *}
 
@@ -540,6 +632,10 @@
   and   "finsert x S |\<union>| T = finsert x (S |\<union>| T)"
   by (lifting append.simps)
 
+lemma funion_empty[simp]:
+  shows "S |\<union>| {||} = S"
+  by (lifting append_Nil2)
+
 lemma funion_sym:
   shows "S |\<union>| T = T |\<union>| S"
   by (lifting funion_sym_pre)
@@ -548,6 +644,14 @@
   shows "S |\<union>| T |\<union>| U = S |\<union>| (T |\<union>| U)"
   by (lifting append_assoc)
 
+lemma singleton_union_left:
+  "{|a|} |\<union>| S = finsert a S"
+  by simp
+
+lemma singleton_union_right:
+  "S |\<union>| {|a|} = finsert a S"
+  by (subst funion_sym) simp
+
 section {* Induction and Cases rules for finite sets *}
 
 lemma fset_strong_cases:
@@ -670,6 +774,30 @@
   "(S = T) = (\<forall>x. (x |\<in>| S) = (x |\<in>| T))"
   by (lifting list_eq.simps[simplified memb_def[symmetric]])
 
+(* We cannot write it as "assumes .. shows" since Isabelle changes
+   the quantifiers to schematic variables and reintroduces them in
+   a different order *)
+lemma fset_eq_cases:
+ "\<lbrakk>a1 = a2;
+   \<And>a b xs. \<lbrakk>a1 = finsert a (finsert b xs); a2 = finsert b (finsert a xs)\<rbrakk> \<Longrightarrow> P;
+   \<lbrakk>a1 = {||}; a2 = {||}\<rbrakk> \<Longrightarrow> P; \<And>xs ys. \<lbrakk>a1 = ys; a2 = xs; xs = ys\<rbrakk> \<Longrightarrow> P;
+   \<And>a xs. \<lbrakk>a1 = finsert a (finsert a xs); a2 = finsert a xs\<rbrakk> \<Longrightarrow> P;
+   \<And>xs ys a. \<lbrakk>a1 = finsert a xs; a2 = finsert a ys; xs = ys\<rbrakk> \<Longrightarrow> P;
+   \<And>xs1 xs2 xs3. \<lbrakk>a1 = xs1; a2 = xs3; xs1 = xs2; xs2 = xs3\<rbrakk> \<Longrightarrow> P\<rbrakk>
+  \<Longrightarrow> P"
+  by (lifting list_eq2.cases[simplified list_eq2_equiv[symmetric]])
+
+lemma fset_eq_induct:
+  assumes "x1 = x2"
+  and "\<And>a b xs. P (finsert a (finsert b xs)) (finsert b (finsert a xs))"
+  and "P {||} {||}"
+  and "\<And>xs ys. \<lbrakk>xs = ys; P xs ys\<rbrakk> \<Longrightarrow> P ys xs"
+  and "\<And>a xs. P (finsert a (finsert a xs)) (finsert a xs)"
+  and "\<And>xs ys a. \<lbrakk>xs = ys; P xs ys\<rbrakk> \<Longrightarrow> P (finsert a xs) (finsert a ys)"
+  and "\<And>xs1 xs2 xs3. \<lbrakk>xs1 = xs2; P xs1 xs2; xs2 = xs3; P xs2 xs3\<rbrakk> \<Longrightarrow> P xs1 xs3"
+  shows "P x1 x2"
+  using assms
+  by (lifting list_eq2.induct[simplified list_eq2_equiv[symmetric]])
 
 ML {*
 fun dest_fsetT (Type ("FSet.fset", [T])) = T