444 text {* alternate formulation with a different decomposition principle

   445   and a proof of equivalence *}

   446 

   447 inductive

   448   list_eq2

   449 where

   450   "list_eq2 (a # b # xs) (b # a # xs)"

   451 | "list_eq2 [] []"

   452 | "list_eq2 xs ys \<Longrightarrow> list_eq2 ys xs"

   453 | "list_eq2 (a # a # xs) (a # xs)"

   454 | "list_eq2 xs ys \<Longrightarrow> list_eq2 (a # xs) (a # ys)"

   455 | "\<lbrakk>list_eq2 xs1 xs2; list_eq2 xs2 xs3\<rbrakk> \<Longrightarrow> list_eq2 xs1 xs3"

   456 

   457 lemma list_eq2_refl:

   458   shows "list_eq2 xs xs"

   459   by (induct xs) (auto intro: list_eq2.intros)

   460 

   461 lemma cons_delete_list_eq2:

   462   shows "list_eq2 (a # (delete_raw A a)) (if memb a A then A else a # A)"

   463   apply (induct A)

   464   apply (simp add: memb_def list_eq2_refl)

   465   apply (case_tac "memb a (aa # A)")

   466   apply (simp_all only: memb_cons_iff)

   467   apply (case_tac [!] "a = aa")

   468   apply (simp_all add: delete_raw.simps)

   469   apply (case_tac "memb a A")

   470   apply (auto simp add: memb_def)[2]

   471   apply (metis list_eq2.intros(3) list_eq2.intros(4) list_eq2.intros(5) list_eq2.intros(6))

   472   apply (metis delete_raw.simps(2) list_eq2.intros(1) list_eq2.intros(5) list_eq2.intros(6))

   473   apply (auto simp add: list_eq2_refl not_memb_delete_raw_ident)

   474   done

   475 

   476 lemma memb_delete_list_eq2:

   477   assumes a: "memb e r"

   478   shows "list_eq2 (e # delete_raw r e) r"

   479   using a cons_delete_list_eq2[of e r]

   480   by simp

   481 

   482 lemma list_eq2_equiv_aux:

   483   assumes a: "fcard_raw l = n"

   484   and b: "l \<approx> r"

   485   shows "list_eq2 l r"

   486 using a b

   487 proof (induct n arbitrary: l r)

   488   case 0

   489   have "fcard_raw l = 0" by fact

   490   then have "\<forall>x. \<not> memb x l" using mem_card_not_0[of _ l] by auto

   491   then have z: "l = []" using no_memb_nil by auto

   492   then have "r = []" sorry

   493   then show ?case using z list_eq2_refl by simp

   494 next

   495   case (Suc m)

   496   have b: "l \<approx> r" by fact

   497   have d: "fcard_raw l = Suc m" by fact

   498   have "\<exists>a. memb a l" by (rule fcard_raw_suc_memb[OF d])

   499   then obtain a where e: "memb a l" by auto

   500   then have e': "memb a r" using list_eq.simps[simplified memb_def[symmetric], of l r] b by auto

   501   have f: "fcard_raw (delete_raw l a) = m" using fcard_raw_delete[of l a] e d by simp

   502   have g: "delete_raw l a \<approx> delete_raw r a" using delete_raw_rsp[OF b] by simp

   503   have g': "list_eq2 (delete_raw l a) (delete_raw r a)" by (rule Suc.hyps[OF f g])

   504   have h: "list_eq2 (a # delete_raw l a) (a # delete_raw r a)" by (rule list_eq2.intros(5)[OF g'])

   505   have i: "list_eq2 l (a # delete_raw l a)" by (rule list_eq2.intros(3)[OF memb_delete_list_eq2[OF e]])

   506   have "list_eq2 l (a # delete_raw r a)" by (rule list_eq2.intros(6)[OF i h])

   507   then show ?case using list_eq2.intros(6)[OF _ memb_delete_list_eq2[OF e']] by simp

   508 qed

   509 

   510 lemma list_eq2_equiv:

   511   "(l \<approx> r) \<longleftrightarrow> (list_eq2 l r)"

   512 proof

   513   show "list_eq2 l r \<Longrightarrow> l \<approx> r" by (induct rule: list_eq2.induct) auto

   514   show "l \<approx> r \<Longrightarrow> list_eq2 l r" using list_eq2_equiv_aux by blast

   515 qed

   516 

   758 (* We cannot write it as "assumes .. shows" since Isabelle changes

   759    the quantifiers to schematic variables and reintroduces them in

   760    a different order *)

   761 lemma fset_eq_cases:

   762  "\<lbrakk>a1 = a2;

   763    \<And>a b xs. \<lbrakk>a1 = finsert a (finsert b xs); a2 = finsert b (finsert a xs)\<rbrakk> \<Longrightarrow> P;

   764    \<lbrakk>a1 = {||}; a2 = {||}\<rbrakk> \<Longrightarrow> P; \<And>xs ys. \<lbrakk>a1 = ys; a2 = xs; xs = ys\<rbrakk> \<Longrightarrow> P;

   765    \<And>a xs. \<lbrakk>a1 = finsert a (finsert a xs); a2 = finsert a xs\<rbrakk> \<Longrightarrow> P;

   766    \<And>xs ys a. \<lbrakk>a1 = finsert a xs; a2 = finsert a ys; xs = ys\<rbrakk> \<Longrightarrow> P;

   767    \<And>xs1 xs2 xs3. \<lbrakk>a1 = xs1; a2 = xs3; xs1 = xs2; xs2 = xs3\<rbrakk> \<Longrightarrow> P\<rbrakk>

   768   \<Longrightarrow> P"

   769   by (lifting list_eq2.cases[simplified list_eq2_equiv[symmetric]])

   770 

   771 lemma fset_eq_induct:

   772   assumes "x1 = x2"

   773   and "\<And>a b xs. P (finsert a (finsert b xs)) (finsert b (finsert a xs))"

   774   and "P {||} {||}"

   775   and "\<And>xs ys. \<lbrakk>xs = ys; P xs ys\<rbrakk> \<Longrightarrow> P ys xs"

   776   and "\<And>a xs. P (finsert a (finsert a xs)) (finsert a xs)"

   777   and "\<And>xs ys a. \<lbrakk>xs = ys; P xs ys\<rbrakk> \<Longrightarrow> P (finsert a xs) (finsert a ys)"

   778   and "\<And>xs1 xs2 xs3. \<lbrakk>xs1 = xs2; P xs1 xs2; xs2 = xs3; P xs2 xs3\<rbrakk> \<Longrightarrow> P xs1 xs3"

   779   shows "P x1 x2"

   780   using assms

   781   by (lifting list_eq2.induct[simplified list_eq2_equiv[symmetric]])