57   ffold_raw :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a list \<Rightarrow> 'b"

    57   ffold_list :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a list \<Rightarrow> 'b"

    59   "ffold_raw f z [] = z"

    59   "ffold_list f z [] = z"

    60 | "ffold_raw f z (a # xs) =

    60 | "ffold_list f z (a # xs) =

    62        if a \<in> set xs then ffold_raw f z xs

    62        if a \<in> set xs then ffold_list f z xs

    63        else f a (ffold_raw f z xs)

    63        else f a (ffold_list f z xs)

   199 lemma memb_commute_ffold_raw:

   199 lemma memb_commute_ffold_list:

   200   "rsp_fold f \<Longrightarrow> h \<in> set b \<Longrightarrow> ffold_raw f z b = f h (ffold_raw f z (removeAll h b))"

   200   "rsp_fold f \<Longrightarrow> h \<in> set b \<Longrightarrow> ffold_list f z b = f h (ffold_list f z (removeAll h b))"

   205 lemma ffold_raw_rsp_pre:

   205 lemma ffold_list_rsp_pre:

   206   "set a = set b \<Longrightarrow> ffold_raw f z a = ffold_raw f z b"

   206   "set a = set b \<Longrightarrow> ffold_list f z a = ffold_list f z b"

   215   apply (metis List.insert_def List.set.simps(2) List.set_insert ffold_raw.simps(2))

   215   apply (metis List.insert_def List.set.simps(2) List.set_insert ffold_list.simps(2))

   216   apply (metis Diff_insert_absorb insertI1 memb_commute_ffold_raw set_removeAll)

   216   apply (metis Diff_insert_absorb insertI1 memb_commute_ffold_list set_removeAll)

   221   by (metis List.set.simps(2) emptyE ffold_raw.simps(2) in_listsp_conv_set listsp.simps mem_def)

   221   by (metis List.set.simps(2) emptyE ffold_list.simps(2) in_listsp_conv_set listsp.simps mem_def)

   222 

   222 

   223 lemma ffold_raw_rsp [quot_respect]:

   223 lemma ffold_list_rsp [quot_respect]:

   224   shows "(op = ===> op = ===> op \<approx> ===> op =) ffold_raw ffold_raw"

   224   shows "(op = ===> op = ===> op \<approx> ===> op =) ffold_list ffold_list"

   226   by(auto intro: ffold_raw_rsp_pre)

   226   by(auto intro: ffold_list_rsp_pre)

   414   is ffold_raw

   414   is ffold_list

   425 subsection {* Compositional Respectfulness and Preservation *}

   425 section {* Compositional respectfulness and preservation lemmas *}

   426 

   426 

   427 lemma [quot_respect]: "(list_all2 op \<approx> OOO op \<approx>) [] []"

   427 lemma Nil_rsp2 [quot_respect]: 

   428   shows "(list_all2 op \<approx> OOO op \<approx>) Nil Nil"

   430 lemma  [quot_preserve]: "(abs_fset \<circ> map f) [] = abs_fset []"

   431 lemma Cons_rsp2 [quot_respect]:

   431   by simp

   432 

   433 lemma [quot_respect]:

   442 lemma [quot_preserve]:

   440 lemma map_prs [quot_preserve]: 

   441   shows "(abs_fset \<circ> map f) [] = abs_fset []"

   442   by simp

   443 

   444 lemma finsert_rsp [quot_preserve]:

   447 lemma [quot_preserve]:

   449 lemma funion_rsp [quot_preserve]:

   490   "(list_all2 op \<approx> OOO op \<approx> ===> list_all2 op \<approx> OOO op \<approx> ===> list_all2 op \<approx> OOO op \<approx>) op @ op @"

   492   "(list_all2 op \<approx> OOO op \<approx> ===> list_all2 op \<approx> OOO op \<approx> ===> list_all2 op \<approx> OOO op \<approx>) append append"

   510 section {* Cases *}

   512 section {* Lifted theorems *}

   511 

   513 

   514 

   515 subsection {* fin *}

   516 

   517 lemma not_fin_fnil: 

   518   shows "x |\<notin>| {||}"

   519   by (descending) (simp add: memb_def)

   520 

   521 lemma fin_set: 

   522   shows "x |\<in>| S \<longleftrightarrow> x \<in> fset S"

   523   by (descending) (simp add: memb_def)

   524 

   525 lemma fnotin_set: 

   526   shows "x |\<notin>| S \<longleftrightarrow> x \<notin> fset S"

   527   by (descending) (simp add: memb_def)

   528 

   529 lemma fset_eq_iff:

   530   shows "S = T \<longleftrightarrow> (\<forall>x. (x |\<in>| S) = (x |\<in>| T))"

   531   by (descending) (auto simp add: memb_def)

   532 

   533 lemma none_fin_fempty:

   534   shows "(\<forall>x. x |\<notin>| S) \<longleftrightarrow> S = {||}"

   535   by (descending) (simp add: memb_def)

   536 

   537 

   538 subsection {* finsert *}

   539 

   540 lemma fin_finsert_iff[simp]:

   541   shows "x |\<in>| finsert y S \<longleftrightarrow> x = y \<or> x |\<in>| S"

   542   by (descending) (simp add: memb_def)

   543 

   544 lemma

   545   shows finsertI1: "x |\<in>| finsert x S"

   546   and   finsertI2: "x |\<in>| S \<Longrightarrow> x |\<in>| finsert y S"

   547   by (descending, simp add: memb_def)+

   548 

   549 lemma finsert_absorb[simp]:

   550   shows "x |\<in>| S \<Longrightarrow> finsert x S = S"

   551   by (descending) (auto simp add: memb_def)

   552 

   553 lemma fempty_not_finsert[simp]:

   554   shows "{||} \<noteq> finsert x S"

   555   and   "finsert x S \<noteq> {||}"

   556   by (descending, simp)+

   557 

   558 lemma finsert_left_comm:

   559   shows "finsert x (finsert y S) = finsert y (finsert x S)"

   560   by (descending) (auto)

   561 

   562 lemma finsert_left_idem:

   563   shows "finsert x (finsert x S) = finsert x S"

   564   by (descending) (auto)

   565 

   566 lemma fsingleton_eq[simp]:

   567   shows "{|x|} = {|y|} \<longleftrightarrow> x = y"

   568   by (descending) (auto)

   569 

   570 

   571 (* FIXME: is this in any case a useful lemma *)

   572 lemma fin_mdef:

   573   shows "x |\<in>| F \<longleftrightarrow> x |\<notin>| (F - {|x|}) \<and> F = finsert x (F - {|x|})"

   574   by (descending) (auto simp add: memb_def diff_list_def)

   575 

   576 

   577 subsection {* fset *}

   578 

   579 lemma fset_simps[simp]:

   580   "fset {||} = ({} :: 'a set)"

   581   "fset (finsert (x :: 'a) S) = insert x (fset S)"

   582   by (lifting set.simps)

   583 

   584 lemma finite_fset [simp]: 

   585   shows "finite (fset S)"

   586   by (descending) (simp)

   587 

   588 lemma fset_cong:

   589   shows "fset S = fset T \<longleftrightarrow> S = T"

   590   by (descending) (simp)

   591 

   592 lemma ffilter_set [simp]: 

   593   shows "fset (ffilter P xs) = P \<inter> fset xs"

   594   by (descending) (auto simp add: mem_def)

   595 

   596 lemma fdelete_set [simp]: 

   597   shows "fset (fdelete x xs) = fset xs - {x}"

   598   by (descending) (simp)

   599 

   600 lemma finter_set [simp]: 

   601   shows "fset (xs |\<inter>| ys) = fset xs \<inter> fset ys"

   602   by (descending) (auto simp add: inter_list_def)

   603 

   604 lemma funion_set [simp]: 

   605   shows "fset (xs |\<union>| ys) = fset xs \<union> fset ys"

   606   by (lifting set_append)

   607 

   608 lemma fminus_set [simp]: 

   609   shows "fset (xs - ys) = fset xs - fset ys"

   610   by (descending) (auto simp add: diff_list_def)

   611 

   612 

   613 subsection {* funion *}

   614 

   615 lemmas [simp] =

   616   sup_bot_left[where 'a="'a fset", standard]

   617   sup_bot_right[where 'a="'a fset", standard]

   618 

   619 lemma funion_finsert[simp]:

   620   shows "finsert x S |\<union>| T = finsert x (S |\<union>| T)"

   621   by (lifting append.simps(2))

   622 

   623 lemma singleton_funion_left:

   624   shows "{|a|} |\<union>| S = finsert a S"

   625   by simp

   626 

   627 lemma singleton_funion_right:

   628   shows "S |\<union>| {|a|} = finsert a S"

   629   by (subst sup.commute) simp

   630 

   631 lemma fin_funion:

   632   shows "x |\<in>| S |\<union>| T \<longleftrightarrow> x |\<in>| S \<or> x |\<in>| T"

   633   by (descending) (simp add: memb_def)

   634 

   635 

   636 subsection {* fminus *}

   637 

   638 lemma fminus_fin: 

   639   shows "x |\<in>| (xs - ys) \<longleftrightarrow> x |\<in>| xs \<and> x |\<notin>| ys"

   640   by (descending) (simp add: diff_list_def memb_def)

   641 

   642 lemma fminus_red: 

   643   shows "finsert x xs - ys = (if x |\<in>| ys then xs - ys else finsert x (xs - ys))"

   644   by (descending) (auto simp add: diff_list_def memb_def)

   645 

   646 lemma fminus_red_fin[simp]: 

   647   shows "x |\<in>| ys \<Longrightarrow> finsert x xs - ys = xs - ys"

   648   by (simp add: fminus_red)

   649 

   650 lemma fminus_red_fnotin[simp]: 

   651   shows "x |\<notin>| ys \<Longrightarrow> finsert x xs - ys = finsert x (xs - ys)"

   652   by (simp add: fminus_red)

   653 

   654 lemma fin_fminus_fnotin: 

   655   shows "x |\<in>| F - S \<Longrightarrow> x |\<notin>| S"

   656   unfolding fin_set fminus_set

   657   by blast

   658 

   659 lemma fin_fnotin_fminus: 

   660   shows "x |\<in>| S \<Longrightarrow> x |\<notin>| F - S"

   661   unfolding fin_set fminus_set

   662   by blast

   663 

   664 

   665 section {* fdelete *}

   666 

   667 lemma fin_fdelete:

   668   shows "x |\<in>| fdelete y S \<longleftrightarrow> x |\<in>| S \<and> x \<noteq> y"

   669   by (descending) (simp add: memb_def)

   670 

   671 lemma fnotin_fdelete:

   672   shows "x |\<notin>| fdelete x S"

   673   by (descending) (simp add: memb_def)

   674 

   675 lemma fnotin_fdelete_ident:

   676   shows "x |\<notin>| S \<Longrightarrow> fdelete x S = S"

   677   by (descending) (simp add: memb_def)

   678 

   679 lemma fset_fdelete_cases:

   680   shows "S = {||} \<or> (\<exists>x. x |\<in>| S \<and> S = finsert x (fdelete x S))"

   681   by (descending) (auto simp add: memb_def insert_absorb)

   682   

   683 

   684 section {* finter *}

   685 

   686 lemma finter_empty_l:

   687   shows "{||} |\<inter>| S = {||}"

   688   by simp

   689 

   690 lemma finter_empty_r:

   691   shows "S |\<inter>| {||} = {||}"

   692   by simp

   693 

   694 lemma finter_finsert:

   695   shows "finsert x S |\<inter>| T = (if x |\<in>| T then finsert x (S |\<inter>| T) else S |\<inter>| T)"

   696   by (descending) (auto simp add: inter_list_def memb_def)

   697 

   698 lemma fin_finter:

   699   shows "x |\<in>| (S |\<inter>| T) \<longleftrightarrow> x |\<in>| S \<and> x |\<in>| T"

   700   by (descending) (simp add: inter_list_def memb_def)

   701 

   702 

   703 subsection {* fsubset *}

   704 

   705 lemma fsubseteq_set: 

   706   shows "xs |\<subseteq>| ys \<longleftrightarrow> fset xs \<subseteq> fset ys"

   707   by (descending) (simp add: sub_list_def)

   708 

   709 lemma fsubset_set: 

   710   shows "xs |\<subset>| ys \<longleftrightarrow> fset xs \<subset> fset ys"

   711   unfolding less_fset_def 

   712   by (descending) (auto simp add: sub_list_def)

   713 

   714 lemma fsubseteq_finsert:

   715   shows "(finsert x xs) |\<subseteq>| ys \<longleftrightarrow> x |\<in>| ys \<and> xs |\<subseteq>| ys"

   716   by (descending) (simp add: sub_list_def memb_def)

   717 

   718 lemma fsubset_fin: 

   719   shows "xs |\<subseteq>| ys = (\<forall>x. x |\<in>| xs \<longrightarrow> x |\<in>| ys)"

   720   by (descending) (auto simp add: sub_list_def memb_def)

   721 

   722 lemma fsubseteq_fempty:

   723   shows "xs |\<subseteq>| {||} \<longleftrightarrow> xs = {||}"

   724   by (descending) (simp add: sub_list_def)

   725 

   726 lemma not_fsubset_fnil: 

   727   shows "\<not> xs |\<subset>| {||}"

   728   by (metis fset_simps(1) fsubset_set not_psubset_empty)

   729 

   730 

   731 section {* fmap *}

   732 

   733 lemma fmap_simps [simp]:

   734    shows "fmap f {||} = {||}"

   735   and   "fmap f (finsert x S) = finsert (f x) (fmap f S)"

   736   by (descending, simp)+

   737 

   738 lemma fmap_set_image [simp]:

   739   shows "fset (fmap f S) = f ` (fset S)"

   740   by (descending) (simp)

   741 

   742 lemma inj_fmap_eq_iff:

   743   shows "inj f \<Longrightarrow> fmap f S = fmap f T \<longleftrightarrow> S = T"

   744   by (descending) (metis inj_vimage_image_eq list_eq.simps set_map)

   745 

   746 lemma fmap_funion: 

   747   shows "fmap f (S |\<union>| T) = fmap f S |\<union>| fmap f T"

   748   by (descending) (simp)

   749 

   750 

   751 subsection {* fcard *}

   752 

   753 lemma fcard_set: 

   754   shows "fcard xs = card (fset xs)"

   755   by (lifting card_list_def)

   756 

   757 lemma fcard_finsert_if [simp]:

   758   shows "fcard (finsert x S) = (if x |\<in>| S then fcard S else Suc (fcard S))"

   759   by (descending) (auto simp add: card_list_def memb_def insert_absorb)

   760 

   761 lemma fcard_0[simp]:

   762   shows "fcard S = 0 \<longleftrightarrow> S = {||}"

   763   by (descending) (simp add: card_list_def)

   764 

   765 lemma fcard_fempty[simp]:

   766   shows "fcard {||} = 0"

   767   by (simp add: fcard_0)

   768 

   769 lemma fcard_1:

   770   shows "fcard S = 1 \<longleftrightarrow> (\<exists>x. S = {|x|})"

   771   by (descending) (auto simp add: card_list_def card_Suc_eq)

   772 

   773 lemma fcard_gt_0:

   774   shows "x \<in> fset S \<Longrightarrow> 0 < fcard S"

   775   by (descending) (auto simp add: card_list_def card_gt_0_iff)

   776   

   777 lemma fcard_not_fin:

   778   shows "(x |\<notin>| S) = (fcard (finsert x S) = Suc (fcard S))"

   779   by (descending) (auto simp add: memb_def card_list_def insert_absorb)

   780 

   781 lemma fcard_suc: 

   782   shows "fcard S = Suc n \<Longrightarrow> \<exists>x T. x |\<notin>| T \<and> S = finsert x T \<and> fcard T = n"

   783   apply(descending)

   784   apply(auto simp add: card_list_def memb_def)

   785   apply(drule card_eq_SucD)

   786   apply(auto)

   787   apply(rule_tac x="b" in exI)

   788   apply(rule_tac x="removeAll b S" in exI)

   789   apply(auto)

   790   done

   791 

   792 lemma fcard_delete:

   793   shows "fcard (fdelete y S) = (if y |\<in>| S then fcard S - 1 else fcard S)"

   794   by (descending) (simp add: card_list_def memb_def)

   795 

   796 lemma fcard_suc_memb: 

   797   shows "fcard A = Suc n \<Longrightarrow> \<exists>a. a |\<in>| A"

   798   apply(descending)

   799   apply(simp add: card_list_def memb_def)

   800   apply(drule card_eq_SucD)

   801   apply(auto)

   802   done

   803 

   804 lemma fin_fcard_not_0: 

   805   shows "a |\<in>| A \<Longrightarrow> fcard A \<noteq> 0"

   806   by (descending) (auto simp add: card_list_def memb_def)

   807 

   808 lemma fcard_mono: 

   809   shows "xs |\<subseteq>| ys \<Longrightarrow> fcard xs \<le> fcard ys"

   810   unfolding fcard_set fsubseteq_set

   811   by (simp add: card_mono[OF finite_fset])

   812 

   813 lemma fcard_fsubset_eq: 

   814   shows "xs |\<subseteq>| ys \<Longrightarrow> fcard ys \<le> fcard xs \<Longrightarrow> xs = ys"

   815   unfolding fcard_set fsubseteq_set

   816   by (auto dest: card_seteq[OF finite_fset] simp add: fset_cong)

   817 

   818 lemma psubset_fcard_mono: 

   819   shows "xs |\<subset>| ys \<Longrightarrow> fcard xs < fcard ys"

   820   unfolding fcard_set fsubset_set

   821   by (rule psubset_card_mono[OF finite_fset])

   822 

   823 lemma fcard_funion_finter: 

   824   shows "fcard xs + fcard ys = fcard (xs |\<union>| ys) + fcard (xs |\<inter>| ys)"

   825   unfolding fcard_set funion_set finter_set

   826   by (rule card_Un_Int[OF finite_fset finite_fset])

   827 

   828 lemma fcard_funion_disjoint: 

   829   shows "xs |\<inter>| ys = {||} \<Longrightarrow> fcard (xs |\<union>| ys) = fcard xs + fcard ys"

   830   unfolding fcard_set funion_set 

   831   apply (rule card_Un_disjoint[OF finite_fset finite_fset])

   832   by (metis finter_set fset_simps(1))

   833 

   834 lemma fcard_delete1_less: 

   835   shows "x |\<in>| xs \<Longrightarrow> fcard (fdelete x xs) < fcard xs"

   836   unfolding fcard_set fin_set fdelete_set 

   837   by (rule card_Diff1_less[OF finite_fset])

   838 

   839 lemma fcard_delete2_less: 

   840   shows "x |\<in>| xs \<Longrightarrow> y |\<in>| xs \<Longrightarrow> fcard (fdelete y (fdelete x xs)) < fcard xs"

   841   unfolding fcard_set fdelete_set fin_set

   842   by (rule card_Diff2_less[OF finite_fset])

   843 

   844 lemma fcard_delete1_le: 

   845   shows "fcard (fdelete x xs) \<le> fcard xs"

   846   unfolding fdelete_set fcard_set

   847   by (rule card_Diff1_le[OF finite_fset])

   848 

   849 lemma fcard_psubset: 

   850   shows "ys |\<subseteq>| xs \<Longrightarrow> fcard ys < fcard xs \<Longrightarrow> ys |\<subset>| xs"

   851   unfolding fcard_set fsubseteq_set fsubset_set

   852   by (rule card_psubset[OF finite_fset])

   853 

   854 lemma fcard_fmap_le: 

   855   shows "fcard (fmap f xs) \<le> fcard xs"

   856   unfolding fcard_set fmap_set_image

   857   by (rule card_image_le[OF finite_fset])

   858 

   859 lemma fcard_fminus_finsert[simp]:

   860   assumes "a |\<in>| A" and "a |\<notin>| B"

   861   shows "fcard (A - finsert a B) = fcard (A - B) - 1"

   862   using assms 

   863   unfolding fin_set fcard_set fminus_set

   864   by (simp add: card_Diff_insert[OF finite_fset])

   865 

   866 lemma fcard_fminus_fsubset:

   867   assumes "B |\<subseteq>| A"

   868   shows "fcard (A - B) = fcard A - fcard B"

   869   using assms 

   870   unfolding fsubseteq_set fcard_set fminus_set

   871   by (rule card_Diff_subset[OF finite_fset])

   872 

   873 lemma fcard_fminus_subset_finter:

   874   shows "fcard (A - B) = fcard A - fcard (A |\<inter>| B)"

   875   unfolding finter_set fcard_set fminus_set

   876   by (rule card_Diff_subset_Int) (simp)

   877 

   878 

   879 section {* fconcat *}

   880 

   881 lemma fconcat_fempty:

   882   shows "fconcat {||} = {||}"

   883   by (lifting concat.simps(1))

   884 

   885 lemma fconcat_finsert:

   886   shows "fconcat (finsert x S) = x |\<union>| fconcat S"

   887   by (lifting concat.simps(2))

   888 

   889 lemma fconcat_finter:

   890   shows "fconcat (xs |\<union>| ys) = fconcat xs |\<union>| fconcat ys"

   891   by (lifting concat_append)

   892 

   893 

   894 section {* ffilter *}

   895 

   896 lemma subseteq_filter: 

   897   shows "ffilter P xs <= ffilter Q xs = (\<forall> x. x |\<in>| xs \<longrightarrow> P x \<longrightarrow> Q x)"

   898   by  (descending) (auto simp add: memb_def sub_list_def)

   899 

   900 lemma eq_ffilter: 

   901   shows "(ffilter P xs = ffilter Q xs) = (\<forall>x. x |\<in>| xs \<longrightarrow> P x = Q x)"

   902   by (descending) (auto simp add: memb_def)

   903 

   904 lemma subset_ffilter:

   905   shows "(\<And>x. x |\<in>| xs \<Longrightarrow> P x \<Longrightarrow> Q x) \<Longrightarrow> (x |\<in>| xs & \<not> P x & Q x) \<Longrightarrow> ffilter P xs < ffilter Q xs"

   906   unfolding less_fset_def by (auto simp add: subseteq_filter eq_ffilter)

   907 

   908 

   909 subsection {* ffold *}

   910 

   911 lemma ffold_nil: 

   912   shows "ffold f z {||} = z"

   913   by (descending) (simp)

   914 

   915 lemma ffold_finsert: "ffold f z (finsert a A) =

   916   (if rsp_fold f then if a |\<in>| A then ffold f z A else f a (ffold f z A) else z)"

   917   by (descending) (simp add: memb_def)

   918 

   919 lemma fin_commute_ffold:

   920   "\<lbrakk>rsp_fold f; h |\<in>| b\<rbrakk> \<Longrightarrow> ffold f z b = f h (ffold f z (fdelete h b))"

   921   by (descending) (simp add: memb_def memb_commute_ffold_list)

   922 

   923 

   924 subsection {* Choice in fsets *}

   925 

   926 lemma fset_choice: 

   927   assumes a: "\<forall>x. x |\<in>| A \<longrightarrow> (\<exists>y. P x y)"

   928   shows "\<exists>f. \<forall>x. x |\<in>| A \<longrightarrow> P x (f x)"

   929   using a

   930   apply(descending)

   931   using finite_set_choice

   932   by (auto simp add: memb_def Ball_def)

   933 

   934 

   935 section {* Induction and Cases rules for fsets *}

   936 

   937 lemma fset_exhaust [case_names fempty finsert, cases type: fset]:

   938   assumes fempty_case: "S = {||} \<Longrightarrow> P" 

   939   and     finsert_case: "\<And>x S'. S = finsert x S' \<Longrightarrow> P"

   940   shows "P"

   941   using assms by (lifting list.exhaust)

   942 

   943 lemma fset_induct [case_names fempty finsert]:

   944   assumes fempty_case: "P {||}"

   945   and     finsert_case: "\<And>x S. P S \<Longrightarrow> P (finsert x S)"

   946   shows "P S"

   947   using assms 

   948   by (descending) (blast intro: list.induct)

   949 

   950 lemma fset_induct_stronger [case_names fempty finsert, induct type: fset]:

   951   assumes fempty_case: "P {||}"

   952   and     finsert_case: "\<And>x S. \<lbrakk>x |\<notin>| S; P S\<rbrakk> \<Longrightarrow> P (finsert x S)"

   953   shows "P S"

   954 proof(induct S rule: fset_induct)

   955   case fempty

   956   show "P {||}" using fempty_case by simp

   957 next

   958   case (finsert x S)

   959   have "P S" by fact

   960   then show "P (finsert x S)" using finsert_case 

   961     by (cases "x |\<in>| S") (simp_all)

   962 qed

   963 

   964 lemma fcard_induct:

   965   assumes fempty_case: "P {||}"

   966   and     fcard_Suc_case: "\<And>S T. Suc (fcard S) = (fcard T) \<Longrightarrow> P S \<Longrightarrow> P T"

   967   shows "P S"

   968 proof (induct S)

   969   case fempty

   970   show "P {||}" by (rule fempty_case)

   971 next

   972   case (finsert x S)

   973   have h: "P S" by fact

   974   have "x |\<notin>| S" by fact

   975   then have "Suc (fcard S) = fcard (finsert x S)" 

   976     using fcard_suc by auto

   977   then show "P (finsert x S)" 

   978     using h fcard_Suc_case by simp

   979 qed

   548 text {* alternate formulation with a different decomposition principle

  1016 lemma fset_strong_cases:

  1017   obtains "xs = {||}"

  1018     | x ys where "x |\<notin>| ys" and "xs = finsert x ys"

  1019   by (lifting fset_raw_strong_cases)

  1020 

  1021 

  1022 lemma fset_induct2:

  1023   "P {||} {||} \<Longrightarrow>

  1024   (\<And>x xs. x |\<notin>| xs \<Longrightarrow> P (finsert x xs) {||}) \<Longrightarrow>

  1025   (\<And>y ys. y |\<notin>| ys \<Longrightarrow> P {||} (finsert y ys)) \<Longrightarrow>

  1026   (\<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>

  1027   P xsa ysa"

  1028   apply (induct xsa arbitrary: ysa)

  1029   apply (induct_tac x rule: fset_induct_stronger)

  1030   apply simp_all

  1031   apply (induct_tac xa rule: fset_induct_stronger)

  1032   apply simp_all

  1033   done

  1034 

  1035 

  1036 

  1037 subsection {* alternate formulation with a different decomposition principle

   552   list_eq2

  1041   list_eq2 ("_ \<approx>2 _")

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

  1043   "(a # b # xs) \<approx>2 (b # a # xs)"

   555 | "list_eq2 [] []"

  1044 | "[] \<approx>2 []"

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

  1045 | "xs \<approx>2 ys \<Longrightarrow>  ys \<approx>2 xs"

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

  1046 | "(a # a # xs) \<approx>2 (a # xs)"

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

  1047 | "xs \<approx>2 ys \<Longrightarrow>  (a # xs) \<approx>2 (a # ys)"

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

  1048 | "\<lbrakk>xs1 \<approx>2 xs2;  xs2 \<approx>2 xs3\<rbrakk> \<Longrightarrow> xs1 \<approx>2 xs3"

   562   shows "list_eq2 xs xs"

  1051   shows "xs \<approx>2 xs"

   566   shows "list_eq2 (a # (removeAll a A)) (if memb a A then A else a # A)"

  1076   shows "(a # (removeAll a A)) \<approx>2 (if memb a A then A else a # A)"

   582   shows "list_eq2 (e # removeAll e r) r"

  1092   shows "(e # removeAll e r) \<approx>2 r"

   594     have "list_eq2 l r"

  1131     have "l \<approx>2 r"

   619       have i: "list_eq2 l (a # removeAll a l)"

  1156       have i: "list_eq2 l (a # removeAll a l)"