diff -r 7abd8c1d9f4b -r 59f41804b3f8 Nominal/FSet.thy
--- a/Nominal/FSet.thy	Mon Apr 19 14:08:01 2010 +0200
+++ b/Nominal/FSet.thy	Mon Apr 19 15:08:29 2010 +0200
@@ -441,6 +441,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 mem_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>| {||}"
@@ -682,6 +755,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