src/HOL/Quotient_Examples/FSet.thy
 author Cezary Kaliszyk Fri Oct 15 21:50:26 2010 +0900 (2010-10-15) changeset 39996 c02078ff8691 parent 39995 849578dd6127 child 40030 9f8dcf6ef563 permissions -rw-r--r--
FSet: definition changes propagated from Nominal and more use of 'descending' tactic
```     1 (*  Title:      HOL/Quotient_Examples/FSet.thy
```
```     2     Author:     Cezary Kaliszyk, TU Munich
```
```     3     Author:     Christian Urban, TU Munich
```
```     4
```
```     5 A reasoning infrastructure for the type of finite sets.
```
```     6 *)
```
```     7
```
```     8 theory FSet
```
```     9 imports Quotient_List
```
```    10 begin
```
```    11
```
```    12 text {* Definiton of List relation and the quotient type *}
```
```    13
```
```    14 fun
```
```    15   list_eq :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" (infix "\<approx>" 50)
```
```    16 where
```
```    17   "list_eq xs ys = (set xs = set ys)"
```
```    18
```
```    19 lemma list_eq_equivp:
```
```    20   shows "equivp list_eq"
```
```    21   unfolding equivp_reflp_symp_transp
```
```    22   unfolding reflp_def symp_def transp_def
```
```    23   by auto
```
```    24
```
```    25 quotient_type
```
```    26   'a fset = "'a list" / "list_eq"
```
```    27   by (rule list_eq_equivp)
```
```    28
```
```    29 text {* Raw definitions of membership, sublist, cardinality,
```
```    30   intersection
```
```    31 *}
```
```    32
```
```    33 definition
```
```    34   memb :: "'a \<Rightarrow> 'a list \<Rightarrow> bool"
```
```    35 where
```
```    36   "memb x xs \<equiv> x \<in> set xs"
```
```    37
```
```    38 definition
```
```    39   sub_list :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"
```
```    40 where
```
```    41   "sub_list xs ys \<equiv> set xs \<subseteq> set ys"
```
```    42
```
```    43 definition
```
```    44   fcard_raw :: "'a list \<Rightarrow> nat"
```
```    45 where
```
```    46   "fcard_raw xs = card (set xs)"
```
```    47
```
```    48 primrec
```
```    49   finter_raw :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
```
```    50 where
```
```    51   "finter_raw [] ys = []"
```
```    52 | "finter_raw (x # xs) ys =
```
```    53     (if x \<in> set ys then x # (finter_raw xs ys) else finter_raw xs ys)"
```
```    54
```
```    55 primrec
```
```    56   fminus_raw :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
```
```    57 where
```
```    58   "fminus_raw ys [] = ys"
```
```    59 | "fminus_raw ys (x # xs) = fminus_raw (removeAll x ys) xs"
```
```    60
```
```    61 definition
```
```    62   rsp_fold
```
```    63 where
```
```    64   "rsp_fold f = (\<forall>u v w. (f u (f v w) = f v (f u w)))"
```
```    65
```
```    66 primrec
```
```    67   ffold_raw :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a list \<Rightarrow> 'b"
```
```    68 where
```
```    69   "ffold_raw f z [] = z"
```
```    70 | "ffold_raw f z (a # xs) =
```
```    71      (if (rsp_fold f) then
```
```    72        if a \<in> set xs then ffold_raw f z xs
```
```    73        else f a (ffold_raw f z xs)
```
```    74      else z)"
```
```    75
```
```    76 text {* Composition Quotient *}
```
```    77
```
```    78 lemma list_all2_refl1:
```
```    79   shows "(list_all2 op \<approx>) r r"
```
```    80   by (rule list_all2_refl) (metis equivp_def fset_equivp)
```
```    81
```
```    82 lemma compose_list_refl:
```
```    83   shows "(list_all2 op \<approx> OOO op \<approx>) r r"
```
```    84 proof
```
```    85   have *: "r \<approx> r" by (rule equivp_reflp[OF fset_equivp])
```
```    86   show "list_all2 op \<approx> r r" by (rule list_all2_refl1)
```
```    87   with * show "(op \<approx> OO list_all2 op \<approx>) r r" ..
```
```    88 qed
```
```    89
```
```    90 lemma Quotient_fset_list:
```
```    91   shows "Quotient (list_all2 op \<approx>) (map abs_fset) (map rep_fset)"
```
```    92   by (fact list_quotient[OF Quotient_fset])
```
```    93
```
```    94 lemma map_rel_cong: "b \<approx> ba \<Longrightarrow> map f b \<approx> map f ba"
```
```    95   unfolding list_eq.simps
```
```    96   by (simp only: set_map)
```
```    97
```
```    98 lemma quotient_compose_list[quot_thm]:
```
```    99   shows  "Quotient ((list_all2 op \<approx>) OOO (op \<approx>))
```
```   100     (abs_fset \<circ> (map abs_fset)) ((map rep_fset) \<circ> rep_fset)"
```
```   101   unfolding Quotient_def comp_def
```
```   102 proof (intro conjI allI)
```
```   103   fix a r s
```
```   104   show "abs_fset (map abs_fset (map rep_fset (rep_fset a))) = a"
```
```   105     by (simp add: abs_o_rep[OF Quotient_fset] Quotient_abs_rep[OF Quotient_fset] map_id)
```
```   106   have b: "list_all2 op \<approx> (map rep_fset (rep_fset a)) (map rep_fset (rep_fset a))"
```
```   107     by (rule list_all2_refl1)
```
```   108   have c: "(op \<approx> OO list_all2 op \<approx>) (map rep_fset (rep_fset a)) (map rep_fset (rep_fset a))"
```
```   109     by (rule, rule equivp_reflp[OF fset_equivp]) (rule b)
```
```   110   show "(list_all2 op \<approx> OOO op \<approx>) (map rep_fset (rep_fset a)) (map rep_fset (rep_fset a))"
```
```   111     by (rule, rule list_all2_refl1) (rule c)
```
```   112   show "(list_all2 op \<approx> OOO op \<approx>) r s = ((list_all2 op \<approx> OOO op \<approx>) r r \<and>
```
```   113         (list_all2 op \<approx> OOO op \<approx>) s s \<and> abs_fset (map abs_fset r) = abs_fset (map abs_fset s))"
```
```   114   proof (intro iffI conjI)
```
```   115     show "(list_all2 op \<approx> OOO op \<approx>) r r" by (rule compose_list_refl)
```
```   116     show "(list_all2 op \<approx> OOO op \<approx>) s s" by (rule compose_list_refl)
```
```   117   next
```
```   118     assume a: "(list_all2 op \<approx> OOO op \<approx>) r s"
```
```   119     then have b: "map abs_fset r \<approx> map abs_fset s"
```
```   120     proof (elim pred_compE)
```
```   121       fix b ba
```
```   122       assume c: "list_all2 op \<approx> r b"
```
```   123       assume d: "b \<approx> ba"
```
```   124       assume e: "list_all2 op \<approx> ba s"
```
```   125       have f: "map abs_fset r = map abs_fset b"
```
```   126         using Quotient_rel[OF Quotient_fset_list] c by blast
```
```   127       have "map abs_fset ba = map abs_fset s"
```
```   128         using Quotient_rel[OF Quotient_fset_list] e by blast
```
```   129       then have g: "map abs_fset s = map abs_fset ba" by simp
```
```   130       then show "map abs_fset r \<approx> map abs_fset s" using d f map_rel_cong by simp
```
```   131     qed
```
```   132     then show "abs_fset (map abs_fset r) = abs_fset (map abs_fset s)"
```
```   133       using Quotient_rel[OF Quotient_fset] by blast
```
```   134   next
```
```   135     assume a: "(list_all2 op \<approx> OOO op \<approx>) r r \<and> (list_all2 op \<approx> OOO op \<approx>) s s
```
```   136       \<and> abs_fset (map abs_fset r) = abs_fset (map abs_fset s)"
```
```   137     then have s: "(list_all2 op \<approx> OOO op \<approx>) s s" by simp
```
```   138     have d: "map abs_fset r \<approx> map abs_fset s"
```
```   139       by (subst Quotient_rel[OF Quotient_fset]) (simp add: a)
```
```   140     have b: "map rep_fset (map abs_fset r) \<approx> map rep_fset (map abs_fset s)"
```
```   141       by (rule map_rel_cong[OF d])
```
```   142     have y: "list_all2 op \<approx> (map rep_fset (map abs_fset s)) s"
```
```   143       by (fact rep_abs_rsp_left[OF Quotient_fset_list, OF list_all2_refl1[of s]])
```
```   144     have c: "(op \<approx> OO list_all2 op \<approx>) (map rep_fset (map abs_fset r)) s"
```
```   145       by (rule pred_compI) (rule b, rule y)
```
```   146     have z: "list_all2 op \<approx> r (map rep_fset (map abs_fset r))"
```
```   147       by (fact rep_abs_rsp[OF Quotient_fset_list, OF list_all2_refl1[of r]])
```
```   148     then show "(list_all2 op \<approx> OOO op \<approx>) r s"
```
```   149       using a c pred_compI by simp
```
```   150   qed
```
```   151 qed
```
```   152
```
```   153
```
```   154 lemma set_finter_raw[simp]:
```
```   155   "set (finter_raw xs ys) = set xs \<inter> set ys"
```
```   156   by (induct xs) (auto simp add: memb_def)
```
```   157
```
```   158 lemma set_fminus_raw[simp]:
```
```   159   "set (fminus_raw xs ys) = (set xs - set ys)"
```
```   160   by (induct ys arbitrary: xs) (auto)
```
```   161
```
```   162
```
```   163 text {* Respectfullness *}
```
```   164
```
```   165 lemma append_rsp[quot_respect]:
```
```   166   shows "(op \<approx> ===> op \<approx> ===> op \<approx>) append append"
```
```   167   by (simp)
```
```   168
```
```   169 lemma sub_list_rsp[quot_respect]:
```
```   170   shows "(op \<approx> ===> op \<approx> ===> op =) sub_list sub_list"
```
```   171   by (auto simp add: sub_list_def)
```
```   172
```
```   173 lemma memb_rsp[quot_respect]:
```
```   174   shows "(op = ===> op \<approx> ===> op =) memb memb"
```
```   175   by (auto simp add: memb_def)
```
```   176
```
```   177 lemma nil_rsp[quot_respect]:
```
```   178   shows "(op \<approx>) Nil Nil"
```
```   179   by simp
```
```   180
```
```   181 lemma cons_rsp[quot_respect]:
```
```   182   shows "(op = ===> op \<approx> ===> op \<approx>) Cons Cons"
```
```   183   by simp
```
```   184
```
```   185 lemma map_rsp[quot_respect]:
```
```   186   shows "(op = ===> op \<approx> ===> op \<approx>) map map"
```
```   187   by auto
```
```   188
```
```   189 lemma set_rsp[quot_respect]:
```
```   190   "(op \<approx> ===> op =) set set"
```
```   191   by auto
```
```   192
```
```   193 lemma list_equiv_rsp[quot_respect]:
```
```   194   shows "(op \<approx> ===> op \<approx> ===> op =) op \<approx> op \<approx>"
```
```   195   by auto
```
```   196
```
```   197 lemma finter_raw_rsp[quot_respect]:
```
```   198   shows "(op \<approx> ===> op \<approx> ===> op \<approx>) finter_raw finter_raw"
```
```   199   by simp
```
```   200
```
```   201 lemma removeAll_rsp[quot_respect]:
```
```   202   shows "(op = ===> op \<approx> ===> op \<approx>) removeAll removeAll"
```
```   203   by simp
```
```   204
```
```   205 lemma fminus_raw_rsp[quot_respect]:
```
```   206   shows "(op \<approx> ===> op \<approx> ===> op \<approx>) fminus_raw fminus_raw"
```
```   207   by simp
```
```   208
```
```   209 lemma fcard_raw_rsp[quot_respect]:
```
```   210   shows "(op \<approx> ===> op =) fcard_raw fcard_raw"
```
```   211   by (simp add: fcard_raw_def)
```
```   212
```
```   213
```
```   214
```
```   215 lemma not_memb_nil:
```
```   216   shows "\<not> memb x []"
```
```   217   by (simp add: memb_def)
```
```   218
```
```   219 lemma memb_cons_iff:
```
```   220   shows "memb x (y # xs) = (x = y \<or> memb x xs)"
```
```   221   by (induct xs) (auto simp add: memb_def)
```
```   222
```
```   223 lemma memb_absorb:
```
```   224   shows "memb x xs \<Longrightarrow> x # xs \<approx> xs"
```
```   225   by (induct xs) (auto simp add: memb_def)
```
```   226
```
```   227 lemma none_memb_nil:
```
```   228   "(\<forall>x. \<not> memb x xs) = (xs \<approx> [])"
```
```   229   by (simp add: memb_def)
```
```   230
```
```   231
```
```   232 lemma memb_commute_ffold_raw:
```
```   233   "rsp_fold f \<Longrightarrow> h \<in> set b \<Longrightarrow> ffold_raw f z b = f h (ffold_raw f z (removeAll h b))"
```
```   234   apply (induct b)
```
```   235   apply (auto simp add: rsp_fold_def)
```
```   236   done
```
```   237
```
```   238 lemma ffold_raw_rsp_pre:
```
```   239   "set a = set b \<Longrightarrow> ffold_raw f z a = ffold_raw f z b"
```
```   240   apply (induct a arbitrary: b)
```
```   241   apply (simp)
```
```   242   apply (simp (no_asm_use))
```
```   243   apply (rule conjI)
```
```   244   apply (rule_tac [!] impI)
```
```   245   apply (rule_tac [!] conjI)
```
```   246   apply (rule_tac [!] impI)
```
```   247   apply (metis insert_absorb)
```
```   248   apply (metis List.insert_def List.set.simps(2) List.set_insert ffold_raw.simps(2))
```
```   249   apply (metis Diff_insert_absorb insertI1 memb_commute_ffold_raw set_removeAll)
```
```   250   apply(drule_tac x="removeAll a1 b" in meta_spec)
```
```   251   apply(auto)
```
```   252   apply(drule meta_mp)
```
```   253   apply(blast)
```
```   254   by (metis List.set.simps(2) emptyE ffold_raw.simps(2) in_listsp_conv_set listsp.simps mem_def)
```
```   255
```
```   256 lemma ffold_raw_rsp[quot_respect]:
```
```   257   shows "(op = ===> op = ===> op \<approx> ===> op =) ffold_raw ffold_raw"
```
```   258   unfolding fun_rel_def
```
```   259   by(auto intro: ffold_raw_rsp_pre)
```
```   260
```
```   261 lemma concat_rsp_pre:
```
```   262   assumes a: "list_all2 op \<approx> x x'"
```
```   263   and     b: "x' \<approx> y'"
```
```   264   and     c: "list_all2 op \<approx> y' y"
```
```   265   and     d: "\<exists>x\<in>set x. xa \<in> set x"
```
```   266   shows "\<exists>x\<in>set y. xa \<in> set x"
```
```   267 proof -
```
```   268   obtain xb where e: "xb \<in> set x" and f: "xa \<in> set xb" using d by auto
```
```   269   have "\<exists>y. y \<in> set x' \<and> xb \<approx> y" by (rule list_all2_find_element[OF e a])
```
```   270   then obtain ya where h: "ya \<in> set x'" and i: "xb \<approx> ya" by auto
```
```   271   have "ya \<in> set y'" using b h by simp
```
```   272   then have "\<exists>yb. yb \<in> set y \<and> ya \<approx> yb" using c by (rule list_all2_find_element)
```
```   273   then show ?thesis using f i by auto
```
```   274 qed
```
```   275
```
```   276 lemma concat_rsp[quot_respect]:
```
```   277   shows "(list_all2 op \<approx> OOO op \<approx> ===> op \<approx>) concat concat"
```
```   278 proof (rule fun_relI, elim pred_compE)
```
```   279   fix a b ba bb
```
```   280   assume a: "list_all2 op \<approx> a ba"
```
```   281   assume b: "ba \<approx> bb"
```
```   282   assume c: "list_all2 op \<approx> bb b"
```
```   283   have "\<forall>x. (\<exists>xa\<in>set a. x \<in> set xa) = (\<exists>xa\<in>set b. x \<in> set xa)"
```
```   284   proof
```
```   285     fix x
```
```   286     show "(\<exists>xa\<in>set a. x \<in> set xa) = (\<exists>xa\<in>set b. x \<in> set xa)"
```
```   287     proof
```
```   288       assume d: "\<exists>xa\<in>set a. x \<in> set xa"
```
```   289       show "\<exists>xa\<in>set b. x \<in> set xa" by (rule concat_rsp_pre[OF a b c d])
```
```   290     next
```
```   291       assume e: "\<exists>xa\<in>set b. x \<in> set xa"
```
```   292       have a': "list_all2 op \<approx> ba a" by (rule list_all2_symp[OF list_eq_equivp, OF a])
```
```   293       have b': "bb \<approx> ba" by (rule equivp_symp[OF list_eq_equivp, OF b])
```
```   294       have c': "list_all2 op \<approx> b bb" by (rule list_all2_symp[OF list_eq_equivp, OF c])
```
```   295       show "\<exists>xa\<in>set a. x \<in> set xa" by (rule concat_rsp_pre[OF c' b' a' e])
```
```   296     qed
```
```   297   qed
```
```   298   then show "concat a \<approx> concat b" by auto
```
```   299 qed
```
```   300
```
```   301 lemma [quot_respect]:
```
```   302   shows "((op =) ===> op \<approx> ===> op \<approx>) filter filter"
```
```   303   by auto
```
```   304
```
```   305 text {* Distributive lattice with bot *}
```
```   306
```
```   307 lemma append_inter_distrib:
```
```   308   "x @ (finter_raw y z) \<approx> finter_raw (x @ y) (x @ z)"
```
```   309   apply (induct x)
```
```   310   apply (auto)
```
```   311   done
```
```   312
```
```   313 instantiation fset :: (type) "{bounded_lattice_bot, distrib_lattice, minus}"
```
```   314 begin
```
```   315
```
```   316 quotient_definition
```
```   317   "bot :: 'a fset" is "[] :: 'a list"
```
```   318
```
```   319 abbreviation
```
```   320   fempty  ("{||}")
```
```   321 where
```
```   322   "{||} \<equiv> bot :: 'a fset"
```
```   323
```
```   324 quotient_definition
```
```   325   "less_eq_fset \<Colon> ('a fset \<Rightarrow> 'a fset \<Rightarrow> bool)"
```
```   326 is
```
```   327   "sub_list \<Colon> ('a list \<Rightarrow> 'a list \<Rightarrow> bool)"
```
```   328
```
```   329 abbreviation
```
```   330   f_subset_eq :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> bool" (infix "|\<subseteq>|" 50)
```
```   331 where
```
```   332   "xs |\<subseteq>| ys \<equiv> xs \<le> ys"
```
```   333
```
```   334 definition
```
```   335   less_fset :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> bool"
```
```   336 where
```
```   337   "xs < ys \<equiv> xs \<le> ys \<and> xs \<noteq> (ys::'a fset)"
```
```   338
```
```   339 abbreviation
```
```   340   fsubset :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> bool" (infix "|\<subset>|" 50)
```
```   341 where
```
```   342   "xs |\<subset>| ys \<equiv> xs < ys"
```
```   343
```
```   344 quotient_definition
```
```   345   "sup :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
```
```   346 is
```
```   347   "append :: 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
```
```   348
```
```   349 abbreviation
```
```   350   funion (infixl "|\<union>|" 65)
```
```   351 where
```
```   352   "xs |\<union>| ys \<equiv> sup (xs :: 'a fset) ys"
```
```   353
```
```   354 quotient_definition
```
```   355   "inf :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
```
```   356 is
```
```   357   "finter_raw :: 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
```
```   358
```
```   359 abbreviation
```
```   360   finter (infixl "|\<inter>|" 65)
```
```   361 where
```
```   362   "xs |\<inter>| ys \<equiv> inf (xs :: 'a fset) ys"
```
```   363
```
```   364 quotient_definition
```
```   365   "minus :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
```
```   366 is
```
```   367   "fminus_raw :: 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
```
```   368
```
```   369 instance
```
```   370 proof
```
```   371   fix x y z :: "'a fset"
```
```   372   show "x |\<subset>| y \<longleftrightarrow> x |\<subseteq>| y \<and> \<not> y |\<subseteq>| x"
```
```   373     unfolding less_fset_def
```
```   374     by (descending) (auto simp add: sub_list_def)
```
```   375   show "x |\<subseteq>| x"  by (descending) (simp add: sub_list_def)
```
```   376   show "{||} |\<subseteq>| x" by (descending) (simp add: sub_list_def)
```
```   377   show "x |\<subseteq>| x |\<union>| y" by (descending) (simp add: sub_list_def)
```
```   378   show "y |\<subseteq>| x |\<union>| y" by (descending) (simp add: sub_list_def)
```
```   379   show "x |\<inter>| y |\<subseteq>| x"
```
```   380     by (descending) (simp add: sub_list_def memb_def[symmetric])
```
```   381   show "x |\<inter>| y |\<subseteq>| y"
```
```   382     by (descending) (simp add: sub_list_def memb_def[symmetric])
```
```   383   show "x |\<union>| (y |\<inter>| z) = x |\<union>| y |\<inter>| (x |\<union>| z)"
```
```   384     by (descending) (rule append_inter_distrib)
```
```   385 next
```
```   386   fix x y z :: "'a fset"
```
```   387   assume a: "x |\<subseteq>| y"
```
```   388   assume b: "y |\<subseteq>| z"
```
```   389   show "x |\<subseteq>| z" using a b
```
```   390     by (descending) (simp add: sub_list_def)
```
```   391 next
```
```   392   fix x y :: "'a fset"
```
```   393   assume a: "x |\<subseteq>| y"
```
```   394   assume b: "y |\<subseteq>| x"
```
```   395   show "x = y" using a b
```
```   396     by (descending) (unfold sub_list_def list_eq.simps, blast)
```
```   397 next
```
```   398   fix x y z :: "'a fset"
```
```   399   assume a: "y |\<subseteq>| x"
```
```   400   assume b: "z |\<subseteq>| x"
```
```   401   show "y |\<union>| z |\<subseteq>| x" using a b
```
```   402     by (descending) (simp add: sub_list_def)
```
```   403 next
```
```   404   fix x y z :: "'a fset"
```
```   405   assume a: "x |\<subseteq>| y"
```
```   406   assume b: "x |\<subseteq>| z"
```
```   407   show "x |\<subseteq>| y |\<inter>| z" using a b
```
```   408     by (descending) (simp add: sub_list_def memb_def[symmetric])
```
```   409 qed
```
```   410
```
```   411 end
```
```   412
```
```   413 section {* Finsert and Membership *}
```
```   414
```
```   415 quotient_definition
```
```   416   "finsert :: 'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
```
```   417 is "Cons"
```
```   418
```
```   419 syntax
```
```   420   "@Finset"     :: "args => 'a fset"  ("{|(_)|}")
```
```   421
```
```   422 translations
```
```   423   "{|x, xs|}" == "CONST finsert x {|xs|}"
```
```   424   "{|x|}"     == "CONST finsert x {||}"
```
```   425
```
```   426 quotient_definition
```
```   427   fin (infix "|\<in>|" 50)
```
```   428 where
```
```   429   "fin :: 'a \<Rightarrow> 'a fset \<Rightarrow> bool" is "memb"
```
```   430
```
```   431 abbreviation
```
```   432   fnotin :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool" (infix "|\<notin>|" 50)
```
```   433 where
```
```   434   "x |\<notin>| S \<equiv> \<not> (x |\<in>| S)"
```
```   435
```
```   436 section {* Other constants on the Quotient Type *}
```
```   437
```
```   438 quotient_definition
```
```   439   "fcard :: 'a fset \<Rightarrow> nat"
```
```   440 is
```
```   441   fcard_raw
```
```   442
```
```   443 quotient_definition
```
```   444   "fmap :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset"
```
```   445 is
```
```   446   map
```
```   447
```
```   448 quotient_definition
```
```   449   "fdelete :: 'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
```
```   450   is removeAll
```
```   451
```
```   452 quotient_definition
```
```   453   "fset :: 'a fset \<Rightarrow> 'a set"
```
```   454   is "set"
```
```   455
```
```   456 quotient_definition
```
```   457   "ffold :: ('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a fset \<Rightarrow> 'b"
```
```   458   is "ffold_raw"
```
```   459
```
```   460 quotient_definition
```
```   461   "fconcat :: ('a fset) fset \<Rightarrow> 'a fset"
```
```   462 is
```
```   463   "concat"
```
```   464
```
```   465 quotient_definition
```
```   466   "ffilter :: ('a \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
```
```   467 is
```
```   468   "filter"
```
```   469
```
```   470 text {* Compositional Respectfullness and Preservation *}
```
```   471
```
```   472 lemma [quot_respect]: "(list_all2 op \<approx> OOO op \<approx>) [] []"
```
```   473   by (fact compose_list_refl)
```
```   474
```
```   475 lemma [quot_preserve]: "(abs_fset \<circ> map f) [] = abs_fset []"
```
```   476   by simp
```
```   477
```
```   478 lemma [quot_respect]:
```
```   479   shows "(op \<approx> ===> list_all2 op \<approx> OOO op \<approx> ===> list_all2 op \<approx> OOO op \<approx>) Cons Cons"
```
```   480   apply auto
```
```   481   apply (rule_tac b="x # b" in pred_compI)
```
```   482   apply auto
```
```   483   apply (rule_tac b="x # ba" in pred_compI)
```
```   484   apply auto
```
```   485   done
```
```   486
```
```   487 lemma [quot_preserve]:
```
```   488   "(rep_fset ---> (map rep_fset \<circ> rep_fset) ---> (abs_fset \<circ> map abs_fset)) op # = finsert"
```
```   489   by (simp add: fun_eq_iff Quotient_abs_rep[OF Quotient_fset]
```
```   490       abs_o_rep[OF Quotient_fset] map_id finsert_def)
```
```   491
```
```   492 lemma [quot_preserve]:
```
```   493   "((map rep_fset \<circ> rep_fset) ---> (map rep_fset \<circ> rep_fset) ---> (abs_fset \<circ> map abs_fset)) op @ = funion"
```
```   494   by (simp add: fun_eq_iff Quotient_abs_rep[OF Quotient_fset]
```
```   495       abs_o_rep[OF Quotient_fset] map_id sup_fset_def)
```
```   496
```
```   497 lemma list_all2_app_l:
```
```   498   assumes a: "reflp R"
```
```   499   and b: "list_all2 R l r"
```
```   500   shows "list_all2 R (z @ l) (z @ r)"
```
```   501   by (induct z) (simp_all add: b rev_iffD1[OF a meta_eq_to_obj_eq[OF reflp_def]])
```
```   502
```
```   503 lemma append_rsp2_pre0:
```
```   504   assumes a:"list_all2 op \<approx> x x'"
```
```   505   shows "list_all2 op \<approx> (x @ z) (x' @ z)"
```
```   506   using a apply (induct x x' rule: list_induct2')
```
```   507   by simp_all (rule list_all2_refl1)
```
```   508
```
```   509 lemma append_rsp2_pre1:
```
```   510   assumes a:"list_all2 op \<approx> x x'"
```
```   511   shows "list_all2 op \<approx> (z @ x) (z @ x')"
```
```   512   using a apply (induct x x' arbitrary: z rule: list_induct2')
```
```   513   apply (rule list_all2_refl1)
```
```   514   apply (simp_all del: list_eq.simps)
```
```   515   apply (rule list_all2_app_l)
```
```   516   apply (simp_all add: reflp_def)
```
```   517   done
```
```   518
```
```   519 lemma append_rsp2_pre:
```
```   520   assumes a:"list_all2 op \<approx> x x'"
```
```   521   and     b: "list_all2 op \<approx> z z'"
```
```   522   shows "list_all2 op \<approx> (x @ z) (x' @ z')"
```
```   523   apply (rule list_all2_transp[OF fset_equivp])
```
```   524   apply (rule append_rsp2_pre0)
```
```   525   apply (rule a)
```
```   526   using b apply (induct z z' rule: list_induct2')
```
```   527   apply (simp_all only: append_Nil2)
```
```   528   apply (rule list_all2_refl1)
```
```   529   apply simp_all
```
```   530   apply (rule append_rsp2_pre1)
```
```   531   apply simp
```
```   532   done
```
```   533
```
```   534 lemma [quot_respect]:
```
```   535   "(list_all2 op \<approx> OOO op \<approx> ===> list_all2 op \<approx> OOO op \<approx> ===> list_all2 op \<approx> OOO op \<approx>) op @ op @"
```
```   536 proof (intro fun_relI, elim pred_compE)
```
```   537   fix x y z w x' z' y' w' :: "'a list list"
```
```   538   assume a:"list_all2 op \<approx> x x'"
```
```   539   and b:    "x' \<approx> y'"
```
```   540   and c:    "list_all2 op \<approx> y' y"
```
```   541   assume aa: "list_all2 op \<approx> z z'"
```
```   542   and bb:   "z' \<approx> w'"
```
```   543   and cc:   "list_all2 op \<approx> w' w"
```
```   544   have a': "list_all2 op \<approx> (x @ z) (x' @ z')" using a aa append_rsp2_pre by auto
```
```   545   have b': "x' @ z' \<approx> y' @ w'" using b bb by simp
```
```   546   have c': "list_all2 op \<approx> (y' @ w') (y @ w)" using c cc append_rsp2_pre by auto
```
```   547   have d': "(op \<approx> OO list_all2 op \<approx>) (x' @ z') (y @ w)"
```
```   548     by (rule pred_compI) (rule b', rule c')
```
```   549   show "(list_all2 op \<approx> OOO op \<approx>) (x @ z) (y @ w)"
```
```   550     by (rule pred_compI) (rule a', rule d')
```
```   551 qed
```
```   552
```
```   553 text {* Raw theorems. Finsert, memb, singleron, sub_list *}
```
```   554
```
```   555 lemma nil_not_cons:
```
```   556   shows "\<not> ([] \<approx> x # xs)"
```
```   557   and   "\<not> (x # xs \<approx> [])"
```
```   558   by auto
```
```   559
```
```   560 lemma no_memb_nil:
```
```   561   "(\<forall>x. \<not> memb x xs) = (xs = [])"
```
```   562   by (simp add: memb_def)
```
```   563
```
```   564 lemma memb_consI1:
```
```   565   shows "memb x (x # xs)"
```
```   566   by (simp add: memb_def)
```
```   567
```
```   568 lemma memb_consI2:
```
```   569   shows "memb x xs \<Longrightarrow> memb x (y # xs)"
```
```   570   by (simp add: memb_def)
```
```   571
```
```   572 lemma singleton_list_eq:
```
```   573   shows "[x] \<approx> [y] \<longleftrightarrow> x = y"
```
```   574   by (simp)
```
```   575
```
```   576 lemma sub_list_cons:
```
```   577   "sub_list (x # xs) ys = (memb x ys \<and> sub_list xs ys)"
```
```   578   by (auto simp add: memb_def sub_list_def)
```
```   579
```
```   580 lemma fminus_raw_red:
```
```   581   "fminus_raw (x # xs) ys = (if x \<in> set ys then fminus_raw xs ys else x # (fminus_raw xs ys))"
```
```   582   by (induct ys arbitrary: xs x) (simp_all)
```
```   583
```
```   584 text {* Cardinality of finite sets *}
```
```   585
```
```   586 lemma fcard_raw_0:
```
```   587   shows "fcard_raw xs = 0 \<longleftrightarrow> xs \<approx> []"
```
```   588   unfolding fcard_raw_def
```
```   589   by (induct xs) (auto)
```
```   590
```
```   591 lemma memb_card_not_0:
```
```   592   assumes a: "memb a A"
```
```   593   shows "\<not>(fcard_raw A = 0)"
```
```   594 proof -
```
```   595   have "\<not>(\<forall>x. \<not> memb x A)" using a by auto
```
```   596   then have "\<not>A \<approx> []" using none_memb_nil[of A] by simp
```
```   597   then show ?thesis using fcard_raw_0[of A] by simp
```
```   598 qed
```
```   599
```
```   600 text {* fmap *}
```
```   601
```
```   602 lemma map_append:
```
```   603   "map f (xs @ ys) \<approx> (map f xs) @ (map f ys)"
```
```   604   by simp
```
```   605
```
```   606 lemma memb_append:
```
```   607   "memb x (xs @ ys) \<longleftrightarrow> memb x xs \<or> memb x ys"
```
```   608   by (induct xs) (simp_all add: not_memb_nil memb_cons_iff)
```
```   609
```
```   610 lemma fset_raw_strong_cases:
```
```   611   obtains "xs = []"
```
```   612     | x ys where "\<not> memb x ys" and "xs \<approx> x # ys"
```
```   613 proof (induct xs arbitrary: x ys)
```
```   614   case Nil
```
```   615   then show thesis by simp
```
```   616 next
```
```   617   case (Cons a xs)
```
```   618   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
```
```   619   have b: "\<And>x' ys'. \<lbrakk>\<not> memb x' ys'; a # xs \<approx> x' # ys'\<rbrakk> \<Longrightarrow> thesis" by fact
```
```   620   have c: "xs = [] \<Longrightarrow> thesis" by (metis no_memb_nil singleton_list_eq b)
```
```   621   have "\<And>x ys. \<lbrakk>\<not> memb x ys; xs \<approx> x # ys\<rbrakk> \<Longrightarrow> thesis"
```
```   622   proof -
```
```   623     fix x :: 'a
```
```   624     fix ys :: "'a list"
```
```   625     assume d:"\<not> memb x ys"
```
```   626     assume e:"xs \<approx> x # ys"
```
```   627     show thesis
```
```   628     proof (cases "x = a")
```
```   629       assume h: "x = a"
```
```   630       then have f: "\<not> memb a ys" using d by simp
```
```   631       have g: "a # xs \<approx> a # ys" using e h by auto
```
```   632       show thesis using b f g by simp
```
```   633     next
```
```   634       assume h: "x \<noteq> a"
```
```   635       then have f: "\<not> memb x (a # ys)" using d unfolding memb_def by auto
```
```   636       have g: "a # xs \<approx> x # (a # ys)" using e h by auto
```
```   637       show thesis using b f g by simp
```
```   638     qed
```
```   639   qed
```
```   640   then show thesis using a c by blast
```
```   641 qed
```
```   642
```
```   643 section {* deletion *}
```
```   644
```
```   645
```
```   646 lemma fset_raw_removeAll_cases:
```
```   647   "xs = [] \<or> (\<exists>x. memb x xs \<and> xs \<approx> x # removeAll x xs)"
```
```   648   by (induct xs) (auto simp add: memb_def)
```
```   649
```
```   650 lemma fremoveAll_filter:
```
```   651   "removeAll y xs = [x \<leftarrow> xs. x \<noteq> y]"
```
```   652   by (induct xs) simp_all
```
```   653
```
```   654 lemma fcard_raw_delete:
```
```   655   "fcard_raw (removeAll y xs) = (if memb y xs then fcard_raw xs - 1 else fcard_raw xs)"
```
```   656   by (auto simp add: fcard_raw_def memb_def)
```
```   657
```
```   658 lemma set_cong:
```
```   659   shows "(x \<approx> y) = (set x = set y)"
```
```   660   by auto
```
```   661
```
```   662 lemma inj_map_eq_iff:
```
```   663   "inj f \<Longrightarrow> (map f l \<approx> map f m) = (l \<approx> m)"
```
```   664   by (simp add: set_eq_iff[symmetric] inj_image_eq_iff)
```
```   665
```
```   666 text {* alternate formulation with a different decomposition principle
```
```   667   and a proof of equivalence *}
```
```   668
```
```   669 inductive
```
```   670   list_eq2
```
```   671 where
```
```   672   "list_eq2 (a # b # xs) (b # a # xs)"
```
```   673 | "list_eq2 [] []"
```
```   674 | "list_eq2 xs ys \<Longrightarrow> list_eq2 ys xs"
```
```   675 | "list_eq2 (a # a # xs) (a # xs)"
```
```   676 | "list_eq2 xs ys \<Longrightarrow> list_eq2 (a # xs) (a # ys)"
```
```   677 | "\<lbrakk>list_eq2 xs1 xs2; list_eq2 xs2 xs3\<rbrakk> \<Longrightarrow> list_eq2 xs1 xs3"
```
```   678
```
```   679 lemma list_eq2_refl:
```
```   680   shows "list_eq2 xs xs"
```
```   681   by (induct xs) (auto intro: list_eq2.intros)
```
```   682
```
```   683 lemma cons_delete_list_eq2:
```
```   684   shows "list_eq2 (a # (removeAll a A)) (if memb a A then A else a # A)"
```
```   685   apply (induct A)
```
```   686   apply (simp add: memb_def list_eq2_refl)
```
```   687   apply (case_tac "memb a (aa # A)")
```
```   688   apply (simp_all only: memb_cons_iff)
```
```   689   apply (case_tac [!] "a = aa")
```
```   690   apply (simp_all)
```
```   691   apply (case_tac "memb a A")
```
```   692   apply (auto simp add: memb_def)[2]
```
```   693   apply (metis list_eq2.intros(3) list_eq2.intros(4) list_eq2.intros(5) list_eq2.intros(6))
```
```   694   apply (metis list_eq2.intros(1) list_eq2.intros(5) list_eq2.intros(6))
```
```   695   apply (auto simp add: list_eq2_refl memb_def)
```
```   696   done
```
```   697
```
```   698 lemma memb_delete_list_eq2:
```
```   699   assumes a: "memb e r"
```
```   700   shows "list_eq2 (e # removeAll e r) r"
```
```   701   using a cons_delete_list_eq2[of e r]
```
```   702   by simp
```
```   703
```
```   704 lemma list_eq2_equiv:
```
```   705   "(l \<approx> r) \<longleftrightarrow> (list_eq2 l r)"
```
```   706 proof
```
```   707   show "list_eq2 l r \<Longrightarrow> l \<approx> r" by (induct rule: list_eq2.induct) auto
```
```   708 next
```
```   709   {
```
```   710     fix n
```
```   711     assume a: "fcard_raw l = n" and b: "l \<approx> r"
```
```   712     have "list_eq2 l r"
```
```   713       using a b
```
```   714     proof (induct n arbitrary: l r)
```
```   715       case 0
```
```   716       have "fcard_raw l = 0" by fact
```
```   717       then have "\<forall>x. \<not> memb x l" using memb_card_not_0[of _ l] by auto
```
```   718       then have z: "l = []" using no_memb_nil by auto
```
```   719       then have "r = []" using `l \<approx> r` by simp
```
```   720       then show ?case using z list_eq2_refl by simp
```
```   721     next
```
```   722       case (Suc m)
```
```   723       have b: "l \<approx> r" by fact
```
```   724       have d: "fcard_raw l = Suc m" by fact
```
```   725       then have "\<exists>a. memb a l"
```
```   726 	apply(simp add: fcard_raw_def memb_def)
```
```   727 	apply(drule card_eq_SucD)
```
```   728 	apply(blast)
```
```   729 	done
```
```   730       then obtain a where e: "memb a l" by auto
```
```   731       then have e': "memb a r" using list_eq.simps[simplified memb_def[symmetric], of l r] b
```
```   732 	unfolding memb_def by auto
```
```   733       have f: "fcard_raw (removeAll a l) = m" using fcard_raw_delete[of a l] e d by simp
```
```   734       have g: "removeAll a l \<approx> removeAll a r" using removeAll_rsp b by simp
```
```   735       have "list_eq2 (removeAll a l) (removeAll a r)" by (rule Suc.hyps[OF f g])
```
```   736       then have h: "list_eq2 (a # removeAll a l) (a # removeAll a r)" by (rule list_eq2.intros(5))
```
```   737       have i: "list_eq2 l (a # removeAll a l)"
```
```   738         by (rule list_eq2.intros(3)[OF memb_delete_list_eq2[OF e]])
```
```   739       have "list_eq2 l (a # removeAll a r)" by (rule list_eq2.intros(6)[OF i h])
```
```   740       then show ?case using list_eq2.intros(6)[OF _ memb_delete_list_eq2[OF e']] by simp
```
```   741     qed
```
```   742     }
```
```   743   then show "l \<approx> r \<Longrightarrow> list_eq2 l r" by blast
```
```   744 qed
```
```   745
```
```   746 text {* Lifted theorems *}
```
```   747
```
```   748 lemma not_fin_fnil: "x |\<notin>| {||}"
```
```   749   by (descending) (simp add: memb_def)
```
```   750
```
```   751 lemma fin_finsert_iff[simp]:
```
```   752   "x |\<in>| finsert y S \<longleftrightarrow> x = y \<or> x |\<in>| S"
```
```   753   by (descending) (simp add: memb_def)
```
```   754
```
```   755 lemma
```
```   756   shows finsertI1: "x |\<in>| finsert x S"
```
```   757   and   finsertI2: "x |\<in>| S \<Longrightarrow> x |\<in>| finsert y S"
```
```   758   by (lifting memb_consI1 memb_consI2)
```
```   759
```
```   760 lemma finsert_absorb[simp]:
```
```   761   shows "x |\<in>| S \<Longrightarrow> finsert x S = S"
```
```   762   by (descending) (auto simp add: memb_def)
```
```   763
```
```   764 lemma fempty_not_finsert[simp]:
```
```   765   "{||} \<noteq> finsert x S"
```
```   766   "finsert x S \<noteq> {||}"
```
```   767   by (lifting nil_not_cons)
```
```   768
```
```   769 lemma finsert_left_comm:
```
```   770   "finsert x (finsert y S) = finsert y (finsert x S)"
```
```   771   by (descending) (auto)
```
```   772
```
```   773 lemma finsert_left_idem:
```
```   774   "finsert x (finsert x S) = finsert x S"
```
```   775   by (descending) (auto)
```
```   776
```
```   777 lemma fsingleton_eq[simp]:
```
```   778   shows "{|x|} = {|y|} \<longleftrightarrow> x = y"
```
```   779   by (descending) (auto)
```
```   780
```
```   781
```
```   782 text {* fset *}
```
```   783
```
```   784 lemma fset_simps[simp]:
```
```   785   "fset {||} = ({} :: 'a set)"
```
```   786   "fset (finsert (h :: 'a) t) = insert h (fset t)"
```
```   787   by (lifting set.simps)
```
```   788
```
```   789 lemma in_fset:
```
```   790   "x \<in> fset S \<equiv> x |\<in>| S"
```
```   791   by (lifting memb_def[symmetric])
```
```   792
```
```   793 lemma none_fin_fempty:
```
```   794   "(\<forall>x. x |\<notin>| S) \<longleftrightarrow> S = {||}"
```
```   795   by (lifting none_memb_nil)
```
```   796
```
```   797 lemma fset_cong:
```
```   798   "S = T \<longleftrightarrow> fset S = fset T"
```
```   799   by (lifting set_cong)
```
```   800
```
```   801
```
```   802 text {* fcard *}
```
```   803
```
```   804 lemma fcard_finsert_if [simp]:
```
```   805   shows "fcard (finsert x S) = (if x |\<in>| S then fcard S else Suc (fcard S))"
```
```   806   by (descending) (auto simp add: fcard_raw_def memb_def insert_absorb)
```
```   807
```
```   808 lemma fcard_0[simp]:
```
```   809   shows "fcard S = 0 \<longleftrightarrow> S = {||}"
```
```   810   by (descending) (simp add: fcard_raw_def)
```
```   811
```
```   812 lemma fcard_fempty[simp]:
```
```   813   shows "fcard {||} = 0"
```
```   814   by (simp add: fcard_0)
```
```   815
```
```   816 lemma fcard_1:
```
```   817   shows "fcard S = 1 \<longleftrightarrow> (\<exists>x. S = {|x|})"
```
```   818   by (descending) (auto simp add: fcard_raw_def card_Suc_eq)
```
```   819
```
```   820 lemma fcard_gt_0:
```
```   821   shows "x \<in> fset S \<Longrightarrow> 0 < fcard S"
```
```   822   by (descending) (auto simp add: fcard_raw_def card_gt_0_iff)
```
```   823
```
```   824 lemma fcard_not_fin:
```
```   825   shows "(x |\<notin>| S) = (fcard (finsert x S) = Suc (fcard S))"
```
```   826   by (descending) (auto simp add: memb_def fcard_raw_def insert_absorb)
```
```   827
```
```   828 lemma fcard_suc: "fcard S = Suc n \<Longrightarrow> \<exists>x T. x |\<notin>| T \<and> S = finsert x T \<and> fcard T = n"
```
```   829   apply descending
```
```   830   apply(simp add: fcard_raw_def memb_def)
```
```   831   apply(drule card_eq_SucD)
```
```   832   apply(auto)
```
```   833   apply(rule_tac x="b" in exI)
```
```   834   apply(rule_tac x="removeAll b S" in exI)
```
```   835   apply(auto)
```
```   836   done
```
```   837
```
```   838 lemma fcard_delete:
```
```   839   "fcard (fdelete y S) = (if y |\<in>| S then fcard S - 1 else fcard S)"
```
```   840   by (lifting fcard_raw_delete)
```
```   841
```
```   842 lemma fcard_suc_memb:
```
```   843   shows "fcard A = Suc n \<Longrightarrow> \<exists>a. a |\<in>| A"
```
```   844   apply(descending)
```
```   845   apply(simp add: fcard_raw_def memb_def)
```
```   846   apply(drule card_eq_SucD)
```
```   847   apply(auto)
```
```   848   done
```
```   849
```
```   850 lemma fin_fcard_not_0:
```
```   851   shows "a |\<in>| A \<Longrightarrow> fcard A \<noteq> 0"
```
```   852   by (descending) (auto simp add: fcard_raw_def memb_def)
```
```   853
```
```   854
```
```   855 text {* funion *}
```
```   856
```
```   857 lemmas [simp] =
```
```   858   sup_bot_left[where 'a="'a fset", standard]
```
```   859   sup_bot_right[where 'a="'a fset", standard]
```
```   860
```
```   861 lemma funion_finsert[simp]:
```
```   862   shows "finsert x S |\<union>| T = finsert x (S |\<union>| T)"
```
```   863   by (lifting append.simps(2))
```
```   864
```
```   865 lemma singleton_union_left:
```
```   866   shows "{|a|} |\<union>| S = finsert a S"
```
```   867   by simp
```
```   868
```
```   869 lemma singleton_union_right:
```
```   870   shows "S |\<union>| {|a|} = finsert a S"
```
```   871   by (subst sup.commute) simp
```
```   872
```
```   873
```
```   874 section {* Induction and Cases rules for fsets *}
```
```   875
```
```   876 lemma fset_strong_cases:
```
```   877   obtains "xs = {||}"
```
```   878     | x ys where "x |\<notin>| ys" and "xs = finsert x ys"
```
```   879   by (lifting fset_raw_strong_cases)
```
```   880
```
```   881 lemma fset_exhaust[case_names fempty finsert, cases type: fset]:
```
```   882   shows "\<lbrakk>S = {||} \<Longrightarrow> P; \<And>x S'. S = finsert x S' \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
```
```   883   by (lifting list.exhaust)
```
```   884
```
```   885 lemma fset_induct_weak[case_names fempty finsert]:
```
```   886   shows "\<lbrakk>P {||}; \<And>x S. P S \<Longrightarrow> P (finsert x S)\<rbrakk> \<Longrightarrow> P S"
```
```   887   by (lifting list.induct)
```
```   888
```
```   889 lemma fset_induct[case_names fempty finsert, induct type: fset]:
```
```   890   assumes prem1: "P {||}"
```
```   891   and     prem2: "\<And>x S. \<lbrakk>x |\<notin>| S; P S\<rbrakk> \<Longrightarrow> P (finsert x S)"
```
```   892   shows "P S"
```
```   893 proof(induct S rule: fset_induct_weak)
```
```   894   case fempty
```
```   895   show "P {||}" by (rule prem1)
```
```   896 next
```
```   897   case (finsert x S)
```
```   898   have asm: "P S" by fact
```
```   899   show "P (finsert x S)"
```
```   900     by (cases "x |\<in>| S") (simp_all add: asm prem2)
```
```   901 qed
```
```   902
```
```   903 lemma fset_induct2:
```
```   904   "P {||} {||} \<Longrightarrow>
```
```   905   (\<And>x xs. x |\<notin>| xs \<Longrightarrow> P (finsert x xs) {||}) \<Longrightarrow>
```
```   906   (\<And>y ys. y |\<notin>| ys \<Longrightarrow> P {||} (finsert y ys)) \<Longrightarrow>
```
```   907   (\<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>
```
```   908   P xsa ysa"
```
```   909   apply (induct xsa arbitrary: ysa)
```
```   910   apply (induct_tac x rule: fset_induct)
```
```   911   apply simp_all
```
```   912   apply (induct_tac xa rule: fset_induct)
```
```   913   apply simp_all
```
```   914   done
```
```   915
```
```   916 lemma fset_fcard_induct:
```
```   917   assumes a: "P {||}"
```
```   918   and     b: "\<And>xs ys. Suc (fcard xs) = (fcard ys) \<Longrightarrow> P xs \<Longrightarrow> P ys"
```
```   919   shows "P zs"
```
```   920 proof (induct zs)
```
```   921   show "P {||}" by (rule a)
```
```   922 next
```
```   923   fix x :: 'a and zs :: "'a fset"
```
```   924   assume h: "P zs"
```
```   925   assume "x |\<notin>| zs"
```
```   926   then have H1: "Suc (fcard zs) = fcard (finsert x zs)" using fcard_suc by auto
```
```   927   then show "P (finsert x zs)" using b h by simp
```
```   928 qed
```
```   929
```
```   930 text {* fmap *}
```
```   931
```
```   932 lemma fmap_simps[simp]:
```
```   933   fixes f::"'a \<Rightarrow> 'b"
```
```   934   shows "fmap f {||} = {||}"
```
```   935   and   "fmap f (finsert x S) = finsert (f x) (fmap f S)"
```
```   936   by (lifting map.simps)
```
```   937
```
```   938 lemma fmap_set_image:
```
```   939   "fset (fmap f S) = f ` (fset S)"
```
```   940   by (induct S) simp_all
```
```   941
```
```   942 lemma inj_fmap_eq_iff:
```
```   943   "inj f \<Longrightarrow> fmap f S = fmap f T \<longleftrightarrow> S = T"
```
```   944   by (lifting inj_map_eq_iff)
```
```   945
```
```   946 lemma fmap_funion:
```
```   947   shows "fmap f (S |\<union>| T) = fmap f S |\<union>| fmap f T"
```
```   948   by (lifting map_append)
```
```   949
```
```   950 lemma fin_funion:
```
```   951   shows "x |\<in>| S |\<union>| T \<longleftrightarrow> x |\<in>| S \<or> x |\<in>| T"
```
```   952   by (lifting memb_append)
```
```   953
```
```   954
```
```   955 section {* fset *}
```
```   956
```
```   957 lemma fin_set:
```
```   958   shows "x |\<in>| xs \<longleftrightarrow> x \<in> fset xs"
```
```   959   by (lifting memb_def)
```
```   960
```
```   961 lemma fnotin_set:
```
```   962   shows "x |\<notin>| xs \<longleftrightarrow> x \<notin> fset xs"
```
```   963   by (simp add: fin_set)
```
```   964
```
```   965 lemma fcard_set:
```
```   966   shows "fcard xs = card (fset xs)"
```
```   967   by (lifting fcard_raw_def)
```
```   968
```
```   969 lemma fsubseteq_set:
```
```   970   shows "xs |\<subseteq>| ys \<longleftrightarrow> fset xs \<subseteq> fset ys"
```
```   971   by (lifting sub_list_def)
```
```   972
```
```   973 lemma fsubset_set:
```
```   974   shows "xs |\<subset>| ys \<longleftrightarrow> fset xs \<subset> fset ys"
```
```   975   unfolding less_fset_def
```
```   976   by (descending) (auto simp add: sub_list_def)
```
```   977
```
```   978 lemma ffilter_set [simp]:
```
```   979   shows "fset (ffilter P xs) = P \<inter> fset xs"
```
```   980   by (descending) (auto simp add: mem_def)
```
```   981
```
```   982 lemma fdelete_set [simp]:
```
```   983   shows "fset (fdelete x xs) = fset xs - {x}"
```
```   984   by (lifting set_removeAll)
```
```   985
```
```   986 lemma finter_set [simp]:
```
```   987   shows "fset (xs |\<inter>| ys) = fset xs \<inter> fset ys"
```
```   988   by (lifting set_finter_raw)
```
```   989
```
```   990 lemma funion_set [simp]:
```
```   991   shows "fset (xs |\<union>| ys) = fset xs \<union> fset ys"
```
```   992   by (lifting set_append)
```
```   993
```
```   994 lemma fminus_set [simp]:
```
```   995   shows "fset (xs - ys) = fset xs - fset ys"
```
```   996   by (lifting set_fminus_raw)
```
```   997
```
```   998 lemmas fset_to_set_trans =
```
```   999   fin_set fnotin_set fcard_set fsubseteq_set fsubset_set
```
```  1000   finter_set funion_set ffilter_set fset_simps
```
```  1001   fset_cong fdelete_set fmap_set_image fminus_set
```
```  1002
```
```  1003
```
```  1004 text {* ffold *}
```
```  1005
```
```  1006 lemma ffold_nil:
```
```  1007   shows "ffold f z {||} = z"
```
```  1008   by (lifting ffold_raw.simps(1)[where 'a="'b" and 'b="'a"])
```
```  1009
```
```  1010 lemma ffold_finsert: "ffold f z (finsert a A) =
```
```  1011   (if rsp_fold f then if a |\<in>| A then ffold f z A else f a (ffold f z A) else z)"
```
```  1012   by (descending) (simp add: memb_def)
```
```  1013
```
```  1014 lemma fin_commute_ffold:
```
```  1015   "\<lbrakk>rsp_fold f; h |\<in>| b\<rbrakk> \<Longrightarrow> ffold f z b = f h (ffold f z (fdelete h b))"
```
```  1016   by (descending) (simp add: memb_def memb_commute_ffold_raw)
```
```  1017
```
```  1018
```
```  1019 text {* fdelete *}
```
```  1020
```
```  1021 lemma fin_fdelete:
```
```  1022   shows "x |\<in>| fdelete y S \<longleftrightarrow> x |\<in>| S \<and> x \<noteq> y"
```
```  1023   by (descending) (simp add: memb_def)
```
```  1024
```
```  1025 lemma fnotin_fdelete:
```
```  1026   shows "x |\<notin>| fdelete x S"
```
```  1027   by (descending) (simp add: memb_def)
```
```  1028
```
```  1029 lemma fnotin_fdelete_ident:
```
```  1030   shows "x |\<notin>| S \<Longrightarrow> fdelete x S = S"
```
```  1031   by (descending) (simp add: memb_def)
```
```  1032
```
```  1033 lemma fset_fdelete_cases:
```
```  1034   shows "S = {||} \<or> (\<exists>x. x |\<in>| S \<and> S = finsert x (fdelete x S))"
```
```  1035   by (lifting fset_raw_removeAll_cases)
```
```  1036
```
```  1037 text {* finite intersection *}
```
```  1038
```
```  1039 lemma finter_empty_l:
```
```  1040   shows "{||} |\<inter>| S = {||}"
```
```  1041   by simp
```
```  1042
```
```  1043
```
```  1044 lemma finter_empty_r:
```
```  1045   shows "S |\<inter>| {||} = {||}"
```
```  1046   by simp
```
```  1047
```
```  1048 lemma finter_finsert:
```
```  1049   shows "finsert x S |\<inter>| T = (if x |\<in>| T then finsert x (S |\<inter>| T) else S |\<inter>| T)"
```
```  1050   by (descending) (simp add: memb_def)
```
```  1051
```
```  1052 lemma fin_finter:
```
```  1053   shows "x |\<in>| (S |\<inter>| T) \<longleftrightarrow> x |\<in>| S \<and> x |\<in>| T"
```
```  1054   by (descending) (simp add: memb_def)
```
```  1055
```
```  1056 lemma fsubset_finsert:
```
```  1057   shows "finsert x xs |\<subseteq>| ys \<longleftrightarrow> x |\<in>| ys \<and> xs |\<subseteq>| ys"
```
```  1058   by (lifting sub_list_cons)
```
```  1059
```
```  1060 lemma
```
```  1061   shows "xs |\<subseteq>| ys \<equiv> \<forall>x. x |\<in>| xs \<longrightarrow> x |\<in>| ys"
```
```  1062   by (descending) (auto simp add: sub_list_def memb_def)
```
```  1063
```
```  1064 lemma fsubset_fin:
```
```  1065   shows "xs |\<subseteq>| ys = (\<forall>x. x |\<in>| xs \<longrightarrow> x |\<in>| ys)"
```
```  1066   by (descending) (auto simp add: sub_list_def memb_def)
```
```  1067
```
```  1068 lemma fminus_fin:
```
```  1069   shows "x |\<in>| xs - ys \<longleftrightarrow> x |\<in>| xs \<and> x |\<notin>| ys"
```
```  1070   by (descending) (simp add: memb_def)
```
```  1071
```
```  1072 lemma fminus_red:
```
```  1073   shows "finsert x xs - ys = (if x |\<in>| ys then xs - ys else finsert x (xs - ys))"
```
```  1074   by (descending) (auto simp add: memb_def)
```
```  1075
```
```  1076 lemma fminus_red_fin [simp]:
```
```  1077   shows "x |\<in>| ys \<Longrightarrow> finsert x xs - ys = xs - ys"
```
```  1078   by (simp add: fminus_red)
```
```  1079
```
```  1080 lemma fminus_red_fnotin[simp]:
```
```  1081   shows "x |\<notin>| ys \<Longrightarrow> finsert x xs - ys = finsert x (xs - ys)"
```
```  1082   by (simp add: fminus_red)
```
```  1083
```
```  1084 lemma fset_eq_iff:
```
```  1085   shows "S = T \<longleftrightarrow> (\<forall>x. (x |\<in>| S) = (x |\<in>| T))"
```
```  1086   by (descending) (auto simp add: memb_def)
```
```  1087
```
```  1088 (* We cannot write it as "assumes .. shows" since Isabelle changes
```
```  1089    the quantifiers to schematic variables and reintroduces them in
```
```  1090    a different order *)
```
```  1091 lemma fset_eq_cases:
```
```  1092  "\<lbrakk>a1 = a2;
```
```  1093    \<And>a b xs. \<lbrakk>a1 = finsert a (finsert b xs); a2 = finsert b (finsert a xs)\<rbrakk> \<Longrightarrow> P;
```
```  1094    \<lbrakk>a1 = {||}; a2 = {||}\<rbrakk> \<Longrightarrow> P; \<And>xs ys. \<lbrakk>a1 = ys; a2 = xs; xs = ys\<rbrakk> \<Longrightarrow> P;
```
```  1095    \<And>a xs. \<lbrakk>a1 = finsert a (finsert a xs); a2 = finsert a xs\<rbrakk> \<Longrightarrow> P;
```
```  1096    \<And>xs ys a. \<lbrakk>a1 = finsert a xs; a2 = finsert a ys; xs = ys\<rbrakk> \<Longrightarrow> P;
```
```  1097    \<And>xs1 xs2 xs3. \<lbrakk>a1 = xs1; a2 = xs3; xs1 = xs2; xs2 = xs3\<rbrakk> \<Longrightarrow> P\<rbrakk>
```
```  1098   \<Longrightarrow> P"
```
```  1099   by (lifting list_eq2.cases[simplified list_eq2_equiv[symmetric]])
```
```  1100
```
```  1101 lemma fset_eq_induct:
```
```  1102   assumes "x1 = x2"
```
```  1103   and "\<And>a b xs. P (finsert a (finsert b xs)) (finsert b (finsert a xs))"
```
```  1104   and "P {||} {||}"
```
```  1105   and "\<And>xs ys. \<lbrakk>xs = ys; P xs ys\<rbrakk> \<Longrightarrow> P ys xs"
```
```  1106   and "\<And>a xs. P (finsert a (finsert a xs)) (finsert a xs)"
```
```  1107   and "\<And>xs ys a. \<lbrakk>xs = ys; P xs ys\<rbrakk> \<Longrightarrow> P (finsert a xs) (finsert a ys)"
```
```  1108   and "\<And>xs1 xs2 xs3. \<lbrakk>xs1 = xs2; P xs1 xs2; xs2 = xs3; P xs2 xs3\<rbrakk> \<Longrightarrow> P xs1 xs3"
```
```  1109   shows "P x1 x2"
```
```  1110   using assms
```
```  1111   by (lifting list_eq2.induct[simplified list_eq2_equiv[symmetric]])
```
```  1112
```
```  1113 section {* fconcat *}
```
```  1114
```
```  1115 lemma fconcat_empty:
```
```  1116   shows "fconcat {||} = {||}"
```
```  1117   by (lifting concat.simps(1))
```
```  1118
```
```  1119 lemma fconcat_insert:
```
```  1120   shows "fconcat (finsert x S) = x |\<union>| fconcat S"
```
```  1121   by (lifting concat.simps(2))
```
```  1122
```
```  1123 lemma
```
```  1124   shows "fconcat (xs |\<union>| ys) = fconcat xs |\<union>| fconcat ys"
```
```  1125   by (lifting concat_append)
```
```  1126
```
```  1127
```
```  1128 section {* ffilter *}
```
```  1129
```
```  1130 lemma subseteq_filter:
```
```  1131   shows "ffilter P xs <= ffilter Q xs = (\<forall> x. x |\<in>| xs \<longrightarrow> P x \<longrightarrow> Q x)"
```
```  1132   by  (descending) (auto simp add: memb_def sub_list_def)
```
```  1133
```
```  1134 lemma eq_ffilter:
```
```  1135   shows "(ffilter P xs = ffilter Q xs) = (\<forall>x. x |\<in>| xs \<longrightarrow> P x = Q x)"
```
```  1136   by (descending) (auto simp add: memb_def)
```
```  1137
```
```  1138 lemma subset_ffilter:
```
```  1139   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"
```
```  1140   unfolding less_fset_def by (auto simp add: subseteq_filter eq_ffilter)
```
```  1141
```
```  1142
```
```  1143 section {* lemmas transferred from Finite_Set theory *}
```
```  1144
```
```  1145 text {* finiteness for finite sets holds *}
```
```  1146 lemma finite_fset [simp]:
```
```  1147   shows "finite (fset S)"
```
```  1148   by (induct S) auto
```
```  1149
```
```  1150 lemma fset_choice:
```
```  1151   shows "\<forall>x. x |\<in>| A \<longrightarrow> (\<exists>y. P x y) \<Longrightarrow> \<exists>f. \<forall>x. x |\<in>| A \<longrightarrow> P x (f x)"
```
```  1152   unfolding fset_to_set_trans
```
```  1153   by (rule finite_set_choice[simplified Ball_def, OF finite_fset])
```
```  1154
```
```  1155 lemma fsubseteq_fempty:
```
```  1156   shows "xs |\<subseteq>| {||} \<longleftrightarrow> xs = {||}"
```
```  1157   by (metis finter_empty_r le_iff_inf)
```
```  1158
```
```  1159 lemma not_fsubset_fnil:
```
```  1160   shows "\<not> xs |\<subset>| {||}"
```
```  1161   by (metis fset_simps(1) fsubset_set not_psubset_empty)
```
```  1162
```
```  1163 lemma fcard_mono:
```
```  1164   shows "xs |\<subseteq>| ys \<Longrightarrow> fcard xs \<le> fcard ys"
```
```  1165   unfolding fset_to_set_trans
```
```  1166   by (rule card_mono[OF finite_fset])
```
```  1167
```
```  1168 lemma fcard_fseteq:
```
```  1169   shows "xs |\<subseteq>| ys \<Longrightarrow> fcard ys \<le> fcard xs \<Longrightarrow> xs = ys"
```
```  1170   unfolding fcard_set fsubseteq_set
```
```  1171   by (simp add: card_seteq[OF finite_fset] fset_cong)
```
```  1172
```
```  1173 lemma psubset_fcard_mono:
```
```  1174   shows "xs |\<subset>| ys \<Longrightarrow> fcard xs < fcard ys"
```
```  1175   unfolding fset_to_set_trans
```
```  1176   by (rule psubset_card_mono[OF finite_fset])
```
```  1177
```
```  1178 lemma fcard_funion_finter:
```
```  1179   shows "fcard xs + fcard ys = fcard (xs |\<union>| ys) + fcard (xs |\<inter>| ys)"
```
```  1180   unfolding fset_to_set_trans
```
```  1181   by (rule card_Un_Int[OF finite_fset finite_fset])
```
```  1182
```
```  1183 lemma fcard_funion_disjoint:
```
```  1184   shows "xs |\<inter>| ys = {||} \<Longrightarrow> fcard (xs |\<union>| ys) = fcard xs + fcard ys"
```
```  1185   unfolding fset_to_set_trans
```
```  1186   by (rule card_Un_disjoint[OF finite_fset finite_fset])
```
```  1187
```
```  1188 lemma fcard_delete1_less:
```
```  1189   shows "x |\<in>| xs \<Longrightarrow> fcard (fdelete x xs) < fcard xs"
```
```  1190   unfolding fset_to_set_trans
```
```  1191   by (rule card_Diff1_less[OF finite_fset])
```
```  1192
```
```  1193 lemma fcard_delete2_less:
```
```  1194   shows "x |\<in>| xs \<Longrightarrow> y |\<in>| xs \<Longrightarrow> fcard (fdelete y (fdelete x xs)) < fcard xs"
```
```  1195   unfolding fset_to_set_trans
```
```  1196   by (rule card_Diff2_less[OF finite_fset])
```
```  1197
```
```  1198 lemma fcard_delete1_le:
```
```  1199   shows "fcard (fdelete x xs) \<le> fcard xs"
```
```  1200   unfolding fset_to_set_trans
```
```  1201   by (rule card_Diff1_le[OF finite_fset])
```
```  1202
```
```  1203 lemma fcard_psubset:
```
```  1204   shows "ys |\<subseteq>| xs \<Longrightarrow> fcard ys < fcard xs \<Longrightarrow> ys |\<subset>| xs"
```
```  1205   unfolding fset_to_set_trans
```
```  1206   by (rule card_psubset[OF finite_fset])
```
```  1207
```
```  1208 lemma fcard_fmap_le:
```
```  1209   shows "fcard (fmap f xs) \<le> fcard xs"
```
```  1210   unfolding fset_to_set_trans
```
```  1211   by (rule card_image_le[OF finite_fset])
```
```  1212
```
```  1213 lemma fin_fminus_fnotin:
```
```  1214   shows "x |\<in>| F - S \<Longrightarrow> x |\<notin>| S"
```
```  1215   unfolding fset_to_set_trans
```
```  1216   by blast
```
```  1217
```
```  1218 lemma fin_fnotin_fminus:
```
```  1219   shows "x |\<in>| S \<Longrightarrow> x |\<notin>| F - S"
```
```  1220   unfolding fset_to_set_trans
```
```  1221   by blast
```
```  1222
```
```  1223 lemma fin_mdef:
```
```  1224   "x |\<in>| F \<longleftrightarrow> x |\<notin>| (F - {|x|}) \<and> F = finsert x (F - {|x|})"
```
```  1225   unfolding fset_to_set_trans
```
```  1226   by blast
```
```  1227
```
```  1228 lemma fcard_fminus_finsert[simp]:
```
```  1229   assumes "a |\<in>| A" and "a |\<notin>| B"
```
```  1230   shows "fcard(A - finsert a B) = fcard(A - B) - 1"
```
```  1231   using assms
```
```  1232   unfolding fset_to_set_trans
```
```  1233   by (rule card_Diff_insert[OF finite_fset])
```
```  1234
```
```  1235 lemma fcard_fminus_fsubset:
```
```  1236   assumes "B |\<subseteq>| A"
```
```  1237   shows "fcard (A - B) = fcard A - fcard B"
```
```  1238   using assms unfolding fset_to_set_trans
```
```  1239   by (rule card_Diff_subset[OF finite_fset])
```
```  1240
```
```  1241 lemma fcard_fminus_subset_finter:
```
```  1242   shows "fcard (A - B) = fcard A - fcard (A |\<inter>| B)"
```
```  1243   unfolding fset_to_set_trans
```
```  1244   by (rule card_Diff_subset_Int) (fold finter_set, rule finite_fset)
```
```  1245
```
```  1246
```
```  1247 ML {*
```
```  1248 fun dest_fsetT (Type (@{type_name fset}, [T])) = T
```
```  1249   | dest_fsetT T = raise TYPE ("dest_fsetT: fset type expected", [T], []);
```
```  1250 *}
```
```  1251
```
```  1252 no_notation
```
```  1253   list_eq (infix "\<approx>" 50)
```
```  1254
```
```  1255 end
```