reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
authorChristian Urban <urbanc@in.tum.de>
Mon Oct 18 14:25:15 2010 +0100 (2010-10-18)
changeset 400309f8dcf6ef563
parent 40029 57e7f651fc70
child 40031 2671cce4d25d
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
src/HOL/Quotient_Examples/FSet.thy
     1.1 --- a/src/HOL/Quotient_Examples/FSet.thy	Sat Oct 16 17:10:23 2010 -0700
     1.2 +++ b/src/HOL/Quotient_Examples/FSet.thy	Mon Oct 18 14:25:15 2010 +0100
     1.3 @@ -2,19 +2,22 @@
     1.4      Author:     Cezary Kaliszyk, TU Munich
     1.5      Author:     Christian Urban, TU Munich
     1.6  
     1.7 -A reasoning infrastructure for the type of finite sets.
     1.8 +    Type of finite sets.
     1.9  *)
    1.10  
    1.11  theory FSet
    1.12  imports Quotient_List
    1.13  begin
    1.14  
    1.15 -text {* Definiton of List relation and the quotient type *}
    1.16 +text {* 
    1.17 +  The type of finite sets is created by a quotient construction
    1.18 +  over lists. The definition of the equivalence:
    1.19 +*}
    1.20  
    1.21  fun
    1.22    list_eq :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" (infix "\<approx>" 50)
    1.23  where
    1.24 -  "list_eq xs ys = (set xs = set ys)"
    1.25 +  "list_eq xs ys \<longleftrightarrow> set xs = set ys"
    1.26  
    1.27  lemma list_eq_equivp:
    1.28    shows "equivp list_eq"
    1.29 @@ -22,222 +25,209 @@
    1.30    unfolding reflp_def symp_def transp_def
    1.31    by auto
    1.32  
    1.33 +text {* Fset type *}
    1.34 +
    1.35  quotient_type
    1.36    'a fset = "'a list" / "list_eq"
    1.37    by (rule list_eq_equivp)
    1.38  
    1.39 -text {* Raw definitions of membership, sublist, cardinality,
    1.40 -  intersection
    1.41 +text {* 
    1.42 +  Definitions for membership, sublist, cardinality, 
    1.43 +  intersection, difference and respectful fold over 
    1.44 +  lists.
    1.45  *}
    1.46  
    1.47 -definition
    1.48 +fun
    1.49    memb :: "'a \<Rightarrow> 'a list \<Rightarrow> bool"
    1.50  where
    1.51 -  "memb x xs \<equiv> x \<in> set xs"
    1.52 +  "memb x xs \<longleftrightarrow> x \<in> set xs"
    1.53  
    1.54 -definition
    1.55 +fun
    1.56    sub_list :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"
    1.57 -where
    1.58 -  "sub_list xs ys \<equiv> set xs \<subseteq> set ys"
    1.59 -
    1.60 -definition
    1.61 -  fcard_raw :: "'a list \<Rightarrow> nat"
    1.62 -where
    1.63 -  "fcard_raw xs = card (set xs)"
    1.64 +where 
    1.65 +  "sub_list xs ys \<longleftrightarrow> set xs \<subseteq> set ys"
    1.66  
    1.67 -primrec
    1.68 -  finter_raw :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
    1.69 +fun
    1.70 +  card_list :: "'a list \<Rightarrow> nat"
    1.71  where
    1.72 -  "finter_raw [] ys = []"
    1.73 -| "finter_raw (x # xs) ys =
    1.74 -    (if x \<in> set ys then x # (finter_raw xs ys) else finter_raw xs ys)"
    1.75 +  "card_list xs = card (set xs)"
    1.76  
    1.77 -primrec
    1.78 -  fminus_raw :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
    1.79 +fun
    1.80 +  inter_list :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
    1.81  where
    1.82 -  "fminus_raw ys [] = ys"
    1.83 -| "fminus_raw ys (x # xs) = fminus_raw (removeAll x ys) xs"
    1.84 +  "inter_list xs ys = [x \<leftarrow> xs. x \<in> set xs \<and> x \<in> set ys]"
    1.85 +
    1.86 +fun
    1.87 +  diff_list :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
    1.88 +where
    1.89 +  "diff_list xs ys = [x \<leftarrow> xs. x \<notin> set ys]"
    1.90  
    1.91  definition
    1.92    rsp_fold
    1.93  where
    1.94 -  "rsp_fold f = (\<forall>u v w. (f u (f v w) = f v (f u w)))"
    1.95 +  "rsp_fold f \<equiv> \<forall>u v w. (f u (f v w) = f v (f u w))"
    1.96  
    1.97  primrec
    1.98 -  ffold_raw :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a list \<Rightarrow> 'b"
    1.99 +  fold_list :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a list \<Rightarrow> 'b"
   1.100  where
   1.101 -  "ffold_raw f z [] = z"
   1.102 -| "ffold_raw f z (a # xs) =
   1.103 +  "fold_list f z [] = z"
   1.104 +| "fold_list f z (a # xs) =
   1.105       (if (rsp_fold f) then
   1.106 -       if a \<in> set xs then ffold_raw f z xs
   1.107 -       else f a (ffold_raw f z xs)
   1.108 +       if a \<in> set xs then fold_list f z xs
   1.109 +       else f a (fold_list f z xs)
   1.110       else z)"
   1.111  
   1.112 -text {* Composition Quotient *}
   1.113 +
   1.114 +
   1.115 +section {* Quotient composition lemmas *}
   1.116  
   1.117 -lemma list_all2_refl1:
   1.118 -  shows "(list_all2 op \<approx>) r r"
   1.119 -  by (rule list_all2_refl) (metis equivp_def fset_equivp)
   1.120 +lemma list_all2_refl':
   1.121 +  assumes q: "equivp R"
   1.122 +  shows "(list_all2 R) r r"
   1.123 +  by (rule list_all2_refl) (metis equivp_def q)
   1.124  
   1.125  lemma compose_list_refl:
   1.126 -  shows "(list_all2 op \<approx> OOO op \<approx>) r r"
   1.127 +  assumes q: "equivp R"
   1.128 +  shows "(list_all2 R OOO op \<approx>) r r"
   1.129  proof
   1.130    have *: "r \<approx> r" by (rule equivp_reflp[OF fset_equivp])
   1.131 -  show "list_all2 op \<approx> r r" by (rule list_all2_refl1)
   1.132 -  with * show "(op \<approx> OO list_all2 op \<approx>) r r" ..
   1.133 +  show "list_all2 R r r" by (rule list_all2_refl'[OF q])
   1.134 +  with * show "(op \<approx> OO list_all2 R) r r" ..
   1.135  qed
   1.136  
   1.137 -lemma Quotient_fset_list:
   1.138 -  shows "Quotient (list_all2 op \<approx>) (map abs_fset) (map rep_fset)"
   1.139 -  by (fact list_quotient[OF Quotient_fset])
   1.140 -
   1.141 -lemma map_rel_cong: "b \<approx> ba \<Longrightarrow> map f b \<approx> map f ba"
   1.142 +lemma map_list_eq_cong: "b \<approx> ba \<Longrightarrow> map f b \<approx> map f ba"
   1.143    unfolding list_eq.simps
   1.144    by (simp only: set_map)
   1.145  
   1.146 +lemma quotient_compose_list_g:
   1.147 +  assumes q: "Quotient R Abs Rep"
   1.148 +  and     e: "equivp R"
   1.149 +  shows  "Quotient ((list_all2 R) OOO (op \<approx>))
   1.150 +    (abs_fset \<circ> (map Abs)) ((map Rep) \<circ> rep_fset)"
   1.151 +  unfolding Quotient_def comp_def
   1.152 +proof (intro conjI allI)
   1.153 +  fix a r s
   1.154 +  show "abs_fset (map Abs (map Rep (rep_fset a))) = a"
   1.155 +    by (simp add: abs_o_rep[OF q] Quotient_abs_rep[OF Quotient_fset] map_id)
   1.156 +  have b: "list_all2 R (map Rep (rep_fset a)) (map Rep (rep_fset a))"
   1.157 +    by (rule list_all2_refl'[OF e])
   1.158 +  have c: "(op \<approx> OO list_all2 R) (map Rep (rep_fset a)) (map Rep (rep_fset a))"
   1.159 +    by (rule, rule equivp_reflp[OF fset_equivp]) (rule b)
   1.160 +  show "(list_all2 R OOO op \<approx>) (map Rep (rep_fset a)) (map Rep (rep_fset a))"
   1.161 +    by (rule, rule list_all2_refl'[OF e]) (rule c)
   1.162 +  show "(list_all2 R OOO op \<approx>) r s = ((list_all2 R OOO op \<approx>) r r \<and>
   1.163 +        (list_all2 R OOO op \<approx>) s s \<and> abs_fset (map Abs r) = abs_fset (map Abs s))"
   1.164 +  proof (intro iffI conjI)
   1.165 +    show "(list_all2 R OOO op \<approx>) r r" by (rule compose_list_refl[OF e])
   1.166 +    show "(list_all2 R OOO op \<approx>) s s" by (rule compose_list_refl[OF e])
   1.167 +  next
   1.168 +    assume a: "(list_all2 R OOO op \<approx>) r s"
   1.169 +    then have b: "map Abs r \<approx> map Abs s"
   1.170 +    proof (elim pred_compE)
   1.171 +      fix b ba
   1.172 +      assume c: "list_all2 R r b"
   1.173 +      assume d: "b \<approx> ba"
   1.174 +      assume e: "list_all2 R ba s"
   1.175 +      have f: "map Abs r = map Abs b"
   1.176 +        using Quotient_rel[OF list_quotient[OF q]] c by blast
   1.177 +      have "map Abs ba = map Abs s"
   1.178 +        using Quotient_rel[OF list_quotient[OF q]] e by blast
   1.179 +      then have g: "map Abs s = map Abs ba" by simp
   1.180 +      then show "map Abs r \<approx> map Abs s" using d f map_list_eq_cong by simp
   1.181 +    qed
   1.182 +    then show "abs_fset (map Abs r) = abs_fset (map Abs s)"
   1.183 +      using Quotient_rel[OF Quotient_fset] by blast
   1.184 +  next
   1.185 +    assume a: "(list_all2 R OOO op \<approx>) r r \<and> (list_all2 R OOO op \<approx>) s s
   1.186 +      \<and> abs_fset (map Abs r) = abs_fset (map Abs s)"
   1.187 +    then have s: "(list_all2 R OOO op \<approx>) s s" by simp
   1.188 +    have d: "map Abs r \<approx> map Abs s"
   1.189 +      by (subst Quotient_rel[OF Quotient_fset]) (simp add: a)
   1.190 +    have b: "map Rep (map Abs r) \<approx> map Rep (map Abs s)"
   1.191 +      by (rule map_list_eq_cong[OF d])
   1.192 +    have y: "list_all2 R (map Rep (map Abs s)) s"
   1.193 +      by (fact rep_abs_rsp_left[OF list_quotient[OF q], OF list_all2_refl'[OF e, of s]])
   1.194 +    have c: "(op \<approx> OO list_all2 R) (map Rep (map Abs r)) s"
   1.195 +      by (rule pred_compI) (rule b, rule y)
   1.196 +    have z: "list_all2 R r (map Rep (map Abs r))"
   1.197 +      by (fact rep_abs_rsp[OF list_quotient[OF q], OF list_all2_refl'[OF e, of r]])
   1.198 +    then show "(list_all2 R OOO op \<approx>) r s"
   1.199 +      using a c pred_compI by simp
   1.200 +  qed
   1.201 +qed
   1.202 +
   1.203  lemma quotient_compose_list[quot_thm]:
   1.204    shows  "Quotient ((list_all2 op \<approx>) OOO (op \<approx>))
   1.205      (abs_fset \<circ> (map abs_fset)) ((map rep_fset) \<circ> rep_fset)"
   1.206 -  unfolding Quotient_def comp_def
   1.207 -proof (intro conjI allI)
   1.208 -  fix a r s
   1.209 -  show "abs_fset (map abs_fset (map rep_fset (rep_fset a))) = a"
   1.210 -    by (simp add: abs_o_rep[OF Quotient_fset] Quotient_abs_rep[OF Quotient_fset] map_id)
   1.211 -  have b: "list_all2 op \<approx> (map rep_fset (rep_fset a)) (map rep_fset (rep_fset a))"
   1.212 -    by (rule list_all2_refl1)
   1.213 -  have c: "(op \<approx> OO list_all2 op \<approx>) (map rep_fset (rep_fset a)) (map rep_fset (rep_fset a))"
   1.214 -    by (rule, rule equivp_reflp[OF fset_equivp]) (rule b)
   1.215 -  show "(list_all2 op \<approx> OOO op \<approx>) (map rep_fset (rep_fset a)) (map rep_fset (rep_fset a))"
   1.216 -    by (rule, rule list_all2_refl1) (rule c)
   1.217 -  show "(list_all2 op \<approx> OOO op \<approx>) r s = ((list_all2 op \<approx> OOO op \<approx>) r r \<and>
   1.218 -        (list_all2 op \<approx> OOO op \<approx>) s s \<and> abs_fset (map abs_fset r) = abs_fset (map abs_fset s))"
   1.219 -  proof (intro iffI conjI)
   1.220 -    show "(list_all2 op \<approx> OOO op \<approx>) r r" by (rule compose_list_refl)
   1.221 -    show "(list_all2 op \<approx> OOO op \<approx>) s s" by (rule compose_list_refl)
   1.222 -  next
   1.223 -    assume a: "(list_all2 op \<approx> OOO op \<approx>) r s"
   1.224 -    then have b: "map abs_fset r \<approx> map abs_fset s"
   1.225 -    proof (elim pred_compE)
   1.226 -      fix b ba
   1.227 -      assume c: "list_all2 op \<approx> r b"
   1.228 -      assume d: "b \<approx> ba"
   1.229 -      assume e: "list_all2 op \<approx> ba s"
   1.230 -      have f: "map abs_fset r = map abs_fset b"
   1.231 -        using Quotient_rel[OF Quotient_fset_list] c by blast
   1.232 -      have "map abs_fset ba = map abs_fset s"
   1.233 -        using Quotient_rel[OF Quotient_fset_list] e by blast
   1.234 -      then have g: "map abs_fset s = map abs_fset ba" by simp
   1.235 -      then show "map abs_fset r \<approx> map abs_fset s" using d f map_rel_cong by simp
   1.236 -    qed
   1.237 -    then show "abs_fset (map abs_fset r) = abs_fset (map abs_fset s)"
   1.238 -      using Quotient_rel[OF Quotient_fset] by blast
   1.239 -  next
   1.240 -    assume a: "(list_all2 op \<approx> OOO op \<approx>) r r \<and> (list_all2 op \<approx> OOO op \<approx>) s s
   1.241 -      \<and> abs_fset (map abs_fset r) = abs_fset (map abs_fset s)"
   1.242 -    then have s: "(list_all2 op \<approx> OOO op \<approx>) s s" by simp
   1.243 -    have d: "map abs_fset r \<approx> map abs_fset s"
   1.244 -      by (subst Quotient_rel[OF Quotient_fset]) (simp add: a)
   1.245 -    have b: "map rep_fset (map abs_fset r) \<approx> map rep_fset (map abs_fset s)"
   1.246 -      by (rule map_rel_cong[OF d])
   1.247 -    have y: "list_all2 op \<approx> (map rep_fset (map abs_fset s)) s"
   1.248 -      by (fact rep_abs_rsp_left[OF Quotient_fset_list, OF list_all2_refl1[of s]])
   1.249 -    have c: "(op \<approx> OO list_all2 op \<approx>) (map rep_fset (map abs_fset r)) s"
   1.250 -      by (rule pred_compI) (rule b, rule y)
   1.251 -    have z: "list_all2 op \<approx> r (map rep_fset (map abs_fset r))"
   1.252 -      by (fact rep_abs_rsp[OF Quotient_fset_list, OF list_all2_refl1[of r]])
   1.253 -    then show "(list_all2 op \<approx> OOO op \<approx>) r s"
   1.254 -      using a c pred_compI by simp
   1.255 -  qed
   1.256 -qed
   1.257 +  by (rule quotient_compose_list_g, rule Quotient_fset, rule list_eq_equivp)
   1.258 +
   1.259  
   1.260  
   1.261 -lemma set_finter_raw[simp]:
   1.262 -  "set (finter_raw xs ys) = set xs \<inter> set ys"
   1.263 -  by (induct xs) (auto simp add: memb_def)
   1.264 +subsection {* Respectfulness lemmas for list operations *}
   1.265  
   1.266 -lemma set_fminus_raw[simp]: 
   1.267 -  "set (fminus_raw xs ys) = (set xs - set ys)"
   1.268 -  by (induct ys arbitrary: xs) (auto)
   1.269 +lemma list_equiv_rsp [quot_respect]:
   1.270 +  shows "(op \<approx> ===> op \<approx> ===> op =) op \<approx> op \<approx>"
   1.271 +  by auto
   1.272  
   1.273 -
   1.274 -text {* Respectfullness *}
   1.275 +lemma append_rsp [quot_respect]:
   1.276 +  shows "(op \<approx> ===> op \<approx> ===> op \<approx>) append append"
   1.277 +  by simp
   1.278  
   1.279 -lemma append_rsp[quot_respect]:
   1.280 -  shows "(op \<approx> ===> op \<approx> ===> op \<approx>) append append"
   1.281 -  by (simp)
   1.282 -
   1.283 -lemma sub_list_rsp[quot_respect]:
   1.284 +lemma sub_list_rsp [quot_respect]:
   1.285    shows "(op \<approx> ===> op \<approx> ===> op =) sub_list sub_list"
   1.286 -  by (auto simp add: sub_list_def)
   1.287 +  by simp
   1.288  
   1.289 -lemma memb_rsp[quot_respect]:
   1.290 +lemma memb_rsp [quot_respect]:
   1.291    shows "(op = ===> op \<approx> ===> op =) memb memb"
   1.292 -  by (auto simp add: memb_def)
   1.293 +  by simp
   1.294  
   1.295 -lemma nil_rsp[quot_respect]:
   1.296 +lemma nil_rsp [quot_respect]:
   1.297    shows "(op \<approx>) Nil Nil"
   1.298    by simp
   1.299  
   1.300 -lemma cons_rsp[quot_respect]:
   1.301 +lemma cons_rsp [quot_respect]:
   1.302    shows "(op = ===> op \<approx> ===> op \<approx>) Cons Cons"
   1.303    by simp
   1.304  
   1.305 -lemma map_rsp[quot_respect]:
   1.306 +lemma map_rsp [quot_respect]:
   1.307    shows "(op = ===> op \<approx> ===> op \<approx>) map map"
   1.308    by auto
   1.309  
   1.310 -lemma set_rsp[quot_respect]:
   1.311 +lemma set_rsp [quot_respect]:
   1.312    "(op \<approx> ===> op =) set set"
   1.313    by auto
   1.314  
   1.315 -lemma list_equiv_rsp[quot_respect]:
   1.316 -  shows "(op \<approx> ===> op \<approx> ===> op =) op \<approx> op \<approx>"
   1.317 -  by auto
   1.318 -
   1.319 -lemma finter_raw_rsp[quot_respect]:
   1.320 -  shows "(op \<approx> ===> op \<approx> ===> op \<approx>) finter_raw finter_raw"
   1.321 +lemma inter_list_rsp [quot_respect]:
   1.322 +  shows "(op \<approx> ===> op \<approx> ===> op \<approx>) inter_list inter_list"
   1.323    by simp
   1.324  
   1.325 -lemma removeAll_rsp[quot_respect]:
   1.326 +lemma removeAll_rsp [quot_respect]:
   1.327    shows "(op = ===> op \<approx> ===> op \<approx>) removeAll removeAll"
   1.328    by simp
   1.329  
   1.330 -lemma fminus_raw_rsp[quot_respect]:
   1.331 -  shows "(op \<approx> ===> op \<approx> ===> op \<approx>) fminus_raw fminus_raw"
   1.332 +lemma diff_list_rsp [quot_respect]:
   1.333 +  shows "(op \<approx> ===> op \<approx> ===> op \<approx>) diff_list diff_list"
   1.334 +  by simp
   1.335 +
   1.336 +lemma card_list_rsp [quot_respect]:
   1.337 +  shows "(op \<approx> ===> op =) card_list card_list"
   1.338 +  by simp
   1.339 +
   1.340 +lemma filter_rsp [quot_respect]:
   1.341 +  shows "(op = ===> op \<approx> ===> op \<approx>) filter filter"
   1.342    by simp
   1.343  
   1.344 -lemma fcard_raw_rsp[quot_respect]:
   1.345 -  shows "(op \<approx> ===> op =) fcard_raw fcard_raw"
   1.346 -  by (simp add: fcard_raw_def)
   1.347 -
   1.348 -
   1.349 -
   1.350 -lemma not_memb_nil:
   1.351 -  shows "\<not> memb x []"
   1.352 -  by (simp add: memb_def)
   1.353 -
   1.354 -lemma memb_cons_iff:
   1.355 -  shows "memb x (y # xs) = (x = y \<or> memb x xs)"
   1.356 -  by (induct xs) (auto simp add: memb_def)
   1.357 +lemma memb_commute_fold_list:
   1.358 +  assumes a: "rsp_fold f"
   1.359 +  and     b: "x \<in> set xs"
   1.360 +  shows "fold_list f y xs = f x (fold_list f y (removeAll x xs))"
   1.361 +  using a b by (induct xs) (auto simp add: rsp_fold_def)
   1.362  
   1.363 -lemma memb_absorb:
   1.364 -  shows "memb x xs \<Longrightarrow> x # xs \<approx> xs"
   1.365 -  by (induct xs) (auto simp add: memb_def)
   1.366 -
   1.367 -lemma none_memb_nil:
   1.368 -  "(\<forall>x. \<not> memb x xs) = (xs \<approx> [])"
   1.369 -  by (simp add: memb_def)
   1.370 -
   1.371 -
   1.372 -lemma memb_commute_ffold_raw:
   1.373 -  "rsp_fold f \<Longrightarrow> h \<in> set b \<Longrightarrow> ffold_raw f z b = f h (ffold_raw f z (removeAll h b))"
   1.374 -  apply (induct b)
   1.375 -  apply (auto simp add: rsp_fold_def)
   1.376 -  done
   1.377 -
   1.378 -lemma ffold_raw_rsp_pre:
   1.379 -  "set a = set b \<Longrightarrow> ffold_raw f z a = ffold_raw f z b"
   1.380 -  apply (induct a arbitrary: b)
   1.381 +lemma fold_list_rsp_pre:
   1.382 +  assumes a: "set xs = set ys"
   1.383 +  shows "fold_list f z xs = fold_list f z ys"
   1.384 +  using a
   1.385 +  apply (induct xs arbitrary: ys)
   1.386    apply (simp)
   1.387    apply (simp (no_asm_use))
   1.388    apply (rule conjI)
   1.389 @@ -245,18 +235,18 @@
   1.390    apply (rule_tac [!] conjI)
   1.391    apply (rule_tac [!] impI)
   1.392    apply (metis insert_absorb)
   1.393 -  apply (metis List.insert_def List.set.simps(2) List.set_insert ffold_raw.simps(2))
   1.394 -  apply (metis Diff_insert_absorb insertI1 memb_commute_ffold_raw set_removeAll)
   1.395 -  apply(drule_tac x="removeAll a1 b" in meta_spec)
   1.396 +  apply (metis List.insert_def List.set.simps(2) List.set_insert fold_list.simps(2))
   1.397 +  apply (metis Diff_insert_absorb insertI1 memb_commute_fold_list set_removeAll)
   1.398 +  apply(drule_tac x="removeAll a ys" in meta_spec)
   1.399    apply(auto)
   1.400    apply(drule meta_mp)
   1.401    apply(blast)
   1.402 -  by (metis List.set.simps(2) emptyE ffold_raw.simps(2) in_listsp_conv_set listsp.simps mem_def)
   1.403 +  by (metis List.set.simps(2) emptyE fold_list.simps(2) in_listsp_conv_set listsp.simps mem_def)
   1.404  
   1.405 -lemma ffold_raw_rsp[quot_respect]:
   1.406 -  shows "(op = ===> op = ===> op \<approx> ===> op =) ffold_raw ffold_raw"
   1.407 +lemma fold_list_rsp [quot_respect]:
   1.408 +  shows "(op = ===> op = ===> op \<approx> ===> op =) fold_list fold_list"
   1.409    unfolding fun_rel_def
   1.410 -  by(auto intro: ffold_raw_rsp_pre)
   1.411 +  by(auto intro: fold_list_rsp_pre)
   1.412  
   1.413  lemma concat_rsp_pre:
   1.414    assumes a: "list_all2 op \<approx> x x'"
   1.415 @@ -273,7 +263,7 @@
   1.416    then show ?thesis using f i by auto
   1.417  qed
   1.418  
   1.419 -lemma concat_rsp[quot_respect]:
   1.420 +lemma concat_rsp [quot_respect]:
   1.421    shows "(list_all2 op \<approx> OOO op \<approx> ===> op \<approx>) concat concat"
   1.422  proof (rule fun_relI, elim pred_compE)
   1.423    fix a b ba bb
   1.424 @@ -298,36 +288,31 @@
   1.425    then show "concat a \<approx> concat b" by auto
   1.426  qed
   1.427  
   1.428 -lemma [quot_respect]:
   1.429 -  shows "((op =) ===> op \<approx> ===> op \<approx>) filter filter"
   1.430 -  by auto
   1.431  
   1.432 -text {* Distributive lattice with bot *}
   1.433  
   1.434 -lemma append_inter_distrib:
   1.435 -  "x @ (finter_raw y z) \<approx> finter_raw (x @ y) (x @ z)"
   1.436 -  apply (induct x)
   1.437 -  apply (auto)
   1.438 -  done
   1.439 +section {* Quotient definitions for fsets *}
   1.440 +
   1.441 +
   1.442 +subsection {* Finite sets are a bounded, distributive lattice with minus *}
   1.443  
   1.444  instantiation fset :: (type) "{bounded_lattice_bot, distrib_lattice, minus}"
   1.445  begin
   1.446  
   1.447  quotient_definition
   1.448 -  "bot :: 'a fset" is "[] :: 'a list"
   1.449 +  "bot :: 'a fset" 
   1.450 +  is "Nil :: 'a list"
   1.451  
   1.452  abbreviation
   1.453 -  fempty  ("{||}")
   1.454 +  empty_fset  ("{||}")
   1.455  where
   1.456    "{||} \<equiv> bot :: 'a fset"
   1.457  
   1.458  quotient_definition
   1.459 -  "less_eq_fset \<Colon> ('a fset \<Rightarrow> 'a fset \<Rightarrow> bool)"
   1.460 -is
   1.461 -  "sub_list \<Colon> ('a list \<Rightarrow> 'a list \<Rightarrow> bool)"
   1.462 +  "less_eq_fset :: ('a fset \<Rightarrow> 'a fset \<Rightarrow> bool)"
   1.463 +  is "sub_list :: ('a list \<Rightarrow> 'a list \<Rightarrow> bool)"
   1.464  
   1.465  abbreviation
   1.466 -  f_subset_eq :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> bool" (infix "|\<subseteq>|" 50)
   1.467 +  subset_fset :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> bool" (infix "|\<subseteq>|" 50)
   1.468  where
   1.469    "xs |\<subseteq>| ys \<equiv> xs \<le> ys"
   1.470  
   1.471 @@ -337,116 +322,108 @@
   1.472    "xs < ys \<equiv> xs \<le> ys \<and> xs \<noteq> (ys::'a fset)"
   1.473  
   1.474  abbreviation
   1.475 -  fsubset :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> bool" (infix "|\<subset>|" 50)
   1.476 +  psubset_fset :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> bool" (infix "|\<subset>|" 50)
   1.477  where
   1.478    "xs |\<subset>| ys \<equiv> xs < ys"
   1.479  
   1.480  quotient_definition
   1.481    "sup :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
   1.482 -is
   1.483 -  "append :: 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
   1.484 +  is "append :: 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
   1.485  
   1.486  abbreviation
   1.487 -  funion (infixl "|\<union>|" 65)
   1.488 +  union_fset (infixl "|\<union>|" 65)
   1.489  where
   1.490 -  "xs |\<union>| ys \<equiv> sup (xs :: 'a fset) ys"
   1.491 +  "xs |\<union>| ys \<equiv> sup xs (ys::'a fset)"
   1.492  
   1.493  quotient_definition
   1.494    "inf :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
   1.495 -is
   1.496 -  "finter_raw :: 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
   1.497 +  is "inter_list :: 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
   1.498  
   1.499  abbreviation
   1.500 -  finter (infixl "|\<inter>|" 65)
   1.501 +  inter_fset (infixl "|\<inter>|" 65)
   1.502  where
   1.503 -  "xs |\<inter>| ys \<equiv> inf (xs :: 'a fset) ys"
   1.504 +  "xs |\<inter>| ys \<equiv> inf xs (ys::'a fset)"
   1.505  
   1.506  quotient_definition
   1.507    "minus :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
   1.508 -is
   1.509 -  "fminus_raw :: 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
   1.510 +  is "diff_list :: 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
   1.511 +
   1.512  
   1.513  instance
   1.514  proof
   1.515    fix x y z :: "'a fset"
   1.516    show "x |\<subset>| y \<longleftrightarrow> x |\<subseteq>| y \<and> \<not> y |\<subseteq>| x"
   1.517      unfolding less_fset_def 
   1.518 -    by (descending) (auto simp add: sub_list_def)
   1.519 -  show "x |\<subseteq>| x"  by (descending) (simp add: sub_list_def)
   1.520 -  show "{||} |\<subseteq>| x" by (descending) (simp add: sub_list_def)
   1.521 -  show "x |\<subseteq>| x |\<union>| y" by (descending) (simp add: sub_list_def)
   1.522 -  show "y |\<subseteq>| x |\<union>| y" by (descending) (simp add: sub_list_def)
   1.523 -  show "x |\<inter>| y |\<subseteq>| x"
   1.524 -    by (descending) (simp add: sub_list_def memb_def[symmetric])
   1.525 -  show "x |\<inter>| y |\<subseteq>| y" 
   1.526 -    by (descending) (simp add: sub_list_def memb_def[symmetric])
   1.527 +    by (descending) (auto)
   1.528 +  show "x |\<subseteq>| x"  by (descending) (simp)
   1.529 +  show "{||} |\<subseteq>| x" by (descending) (simp)
   1.530 +  show "x |\<subseteq>| x |\<union>| y" by (descending) (simp)
   1.531 +  show "y |\<subseteq>| x |\<union>| y" by (descending) (simp)
   1.532 +  show "x |\<inter>| y |\<subseteq>| x" by (descending) (auto)
   1.533 +  show "x |\<inter>| y |\<subseteq>| y" by (descending) (auto)
   1.534    show "x |\<union>| (y |\<inter>| z) = x |\<union>| y |\<inter>| (x |\<union>| z)" 
   1.535 -    by (descending) (rule append_inter_distrib)
   1.536 +    by (descending) (auto)
   1.537  next
   1.538    fix x y z :: "'a fset"
   1.539    assume a: "x |\<subseteq>| y"
   1.540    assume b: "y |\<subseteq>| z"
   1.541 -  show "x |\<subseteq>| z" using a b 
   1.542 -    by (descending) (simp add: sub_list_def)
   1.543 +  show "x |\<subseteq>| z" using a b by (descending) (simp)
   1.544  next
   1.545    fix x y :: "'a fset"
   1.546    assume a: "x |\<subseteq>| y"
   1.547    assume b: "y |\<subseteq>| x"
   1.548 -  show "x = y" using a b 
   1.549 -    by (descending) (unfold sub_list_def list_eq.simps, blast)
   1.550 +  show "x = y" using a b by (descending) (auto)
   1.551  next
   1.552    fix x y z :: "'a fset"
   1.553    assume a: "y |\<subseteq>| x"
   1.554    assume b: "z |\<subseteq>| x"
   1.555 -  show "y |\<union>| z |\<subseteq>| x" using a b 
   1.556 -    by (descending) (simp add: sub_list_def)
   1.557 +  show "y |\<union>| z |\<subseteq>| x" using a b by (descending) (simp)
   1.558  next
   1.559    fix x y z :: "'a fset"
   1.560    assume a: "x |\<subseteq>| y"
   1.561    assume b: "x |\<subseteq>| z"
   1.562 -  show "x |\<subseteq>| y |\<inter>| z" using a b 
   1.563 -    by (descending) (simp add: sub_list_def memb_def[symmetric])
   1.564 +  show "x |\<subseteq>| y |\<inter>| z" using a b by (descending) (auto)
   1.565  qed
   1.566  
   1.567  end
   1.568  
   1.569 -section {* Finsert and Membership *}
   1.570 +
   1.571 +subsection {* Other constants for fsets *}
   1.572  
   1.573  quotient_definition
   1.574 -  "finsert :: 'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
   1.575 -is "Cons"
   1.576 +  "insert_fset :: 'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
   1.577 +  is "Cons"
   1.578  
   1.579  syntax
   1.580 -  "@Finset"     :: "args => 'a fset"  ("{|(_)|}")
   1.581 +  "@Insert_fset"     :: "args => 'a fset"  ("{|(_)|}")
   1.582  
   1.583  translations
   1.584 -  "{|x, xs|}" == "CONST finsert x {|xs|}"
   1.585 -  "{|x|}"     == "CONST finsert x {||}"
   1.586 +  "{|x, xs|}" == "CONST insert_fset x {|xs|}"
   1.587 +  "{|x|}"     == "CONST insert_fset x {||}"
   1.588  
   1.589  quotient_definition
   1.590 -  fin (infix "|\<in>|" 50)
   1.591 +  in_fset (infix "|\<in>|" 50)
   1.592  where
   1.593 -  "fin :: 'a \<Rightarrow> 'a fset \<Rightarrow> bool" is "memb"
   1.594 +  "in_fset :: 'a \<Rightarrow> 'a fset \<Rightarrow> bool" is "memb"
   1.595  
   1.596  abbreviation
   1.597 -  fnotin :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool" (infix "|\<notin>|" 50)
   1.598 +  notin_fset :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool" (infix "|\<notin>|" 50)
   1.599  where
   1.600    "x |\<notin>| S \<equiv> \<not> (x |\<in>| S)"
   1.601  
   1.602 -section {* Other constants on the Quotient Type *}
   1.603 +
   1.604 +subsection {* Other constants on the Quotient Type *}
   1.605  
   1.606  quotient_definition
   1.607 -  "fcard :: 'a fset \<Rightarrow> nat"
   1.608 -is
   1.609 -  fcard_raw
   1.610 +  "card_fset :: 'a fset \<Rightarrow> nat"
   1.611 +  is card_list
   1.612  
   1.613  quotient_definition
   1.614 -  "fmap :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset"
   1.615 -is
   1.616 -  map
   1.617 +  "map_fset :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset"
   1.618 +  is map
   1.619  
   1.620  quotient_definition
   1.621 -  "fdelete :: 'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
   1.622 +  "remove_fset :: 'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
   1.623    is removeAll
   1.624  
   1.625  quotient_definition
   1.626 @@ -454,28 +431,25 @@
   1.627    is "set"
   1.628  
   1.629  quotient_definition
   1.630 -  "ffold :: ('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a fset \<Rightarrow> 'b"
   1.631 -  is "ffold_raw"
   1.632 +  "fold_fset :: ('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a fset \<Rightarrow> 'b"
   1.633 +  is fold_list
   1.634  
   1.635  quotient_definition
   1.636 -  "fconcat :: ('a fset) fset \<Rightarrow> 'a fset"
   1.637 -is
   1.638 -  "concat"
   1.639 +  "concat_fset :: ('a fset) fset \<Rightarrow> 'a fset"
   1.640 +  is concat
   1.641  
   1.642  quotient_definition
   1.643 -  "ffilter :: ('a \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
   1.644 -is
   1.645 -  "filter"
   1.646 +  "filter_fset :: ('a \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
   1.647 +  is filter
   1.648  
   1.649 -text {* Compositional Respectfullness and Preservation *}
   1.650 +
   1.651 +subsection {* Compositional respectfulness and preservation lemmas *}
   1.652  
   1.653 -lemma [quot_respect]: "(list_all2 op \<approx> OOO op \<approx>) [] []"
   1.654 -  by (fact compose_list_refl)
   1.655 +lemma Nil_rsp2 [quot_respect]: 
   1.656 +  shows "(list_all2 op \<approx> OOO op \<approx>) Nil Nil"
   1.657 +  by (rule compose_list_refl, rule list_eq_equivp)
   1.658  
   1.659 -lemma [quot_preserve]: "(abs_fset \<circ> map f) [] = abs_fset []"
   1.660 -  by simp
   1.661 -
   1.662 -lemma [quot_respect]:
   1.663 +lemma Cons_rsp2 [quot_respect]:
   1.664    shows "(op \<approx> ===> list_all2 op \<approx> OOO op \<approx> ===> list_all2 op \<approx> OOO op \<approx>) Cons Cons"
   1.665    apply auto
   1.666    apply (rule_tac b="x # b" in pred_compI)
   1.667 @@ -484,13 +458,18 @@
   1.668    apply auto
   1.669    done
   1.670  
   1.671 -lemma [quot_preserve]:
   1.672 -  "(rep_fset ---> (map rep_fset \<circ> rep_fset) ---> (abs_fset \<circ> map abs_fset)) op # = finsert"
   1.673 +lemma map_prs [quot_preserve]: 
   1.674 +  shows "(abs_fset \<circ> map f) [] = abs_fset []"
   1.675 +  by simp
   1.676 +
   1.677 +lemma insert_fset_rsp [quot_preserve]:
   1.678 +  "(rep_fset ---> (map rep_fset \<circ> rep_fset) ---> (abs_fset \<circ> map abs_fset)) Cons = insert_fset"
   1.679    by (simp add: fun_eq_iff Quotient_abs_rep[OF Quotient_fset]
   1.680 -      abs_o_rep[OF Quotient_fset] map_id finsert_def)
   1.681 +      abs_o_rep[OF Quotient_fset] map_id insert_fset_def)
   1.682  
   1.683 -lemma [quot_preserve]:
   1.684 -  "((map rep_fset \<circ> rep_fset) ---> (map rep_fset \<circ> rep_fset) ---> (abs_fset \<circ> map abs_fset)) op @ = funion"
   1.685 +lemma union_fset_rsp [quot_preserve]:
   1.686 +  "((map rep_fset \<circ> rep_fset) ---> (map rep_fset \<circ> rep_fset) ---> (abs_fset \<circ> map abs_fset)) 
   1.687 +  append = union_fset"
   1.688    by (simp add: fun_eq_iff Quotient_abs_rep[OF Quotient_fset]
   1.689        abs_o_rep[OF Quotient_fset] map_id sup_fset_def)
   1.690  
   1.691 @@ -504,13 +483,13 @@
   1.692    assumes a:"list_all2 op \<approx> x x'"
   1.693    shows "list_all2 op \<approx> (x @ z) (x' @ z)"
   1.694    using a apply (induct x x' rule: list_induct2')
   1.695 -  by simp_all (rule list_all2_refl1)
   1.696 +  by simp_all (rule list_all2_refl'[OF list_eq_equivp])
   1.697  
   1.698  lemma append_rsp2_pre1:
   1.699    assumes a:"list_all2 op \<approx> x x'"
   1.700    shows "list_all2 op \<approx> (z @ x) (z @ x')"
   1.701    using a apply (induct x x' arbitrary: z rule: list_induct2')
   1.702 -  apply (rule list_all2_refl1)
   1.703 +  apply (rule list_all2_refl'[OF list_eq_equivp])
   1.704    apply (simp_all del: list_eq.simps)
   1.705    apply (rule list_all2_app_l)
   1.706    apply (simp_all add: reflp_def)
   1.707 @@ -525,14 +504,14 @@
   1.708    apply (rule a)
   1.709    using b apply (induct z z' rule: list_induct2')
   1.710    apply (simp_all only: append_Nil2)
   1.711 -  apply (rule list_all2_refl1)
   1.712 +  apply (rule list_all2_refl'[OF list_eq_equivp])
   1.713    apply simp_all
   1.714    apply (rule append_rsp2_pre1)
   1.715    apply simp
   1.716    done
   1.717  
   1.718 -lemma [quot_respect]:
   1.719 -  "(list_all2 op \<approx> OOO op \<approx> ===> list_all2 op \<approx> OOO op \<approx> ===> list_all2 op \<approx> OOO op \<approx>) op @ op @"
   1.720 +lemma append_rsp2 [quot_respect]:
   1.721 +  "(list_all2 op \<approx> OOO op \<approx> ===> list_all2 op \<approx> OOO op \<approx> ===> list_all2 op \<approx> OOO op \<approx>) append append"
   1.722  proof (intro fun_relI, elim pred_compE)
   1.723    fix x y z w x' z' y' w' :: "'a list list"
   1.724    assume a:"list_all2 op \<approx> x x'"
   1.725 @@ -550,62 +529,465 @@
   1.726      by (rule pred_compI) (rule a', rule d')
   1.727  qed
   1.728  
   1.729 -text {* Raw theorems. Finsert, memb, singleron, sub_list *}
   1.730 +
   1.731 +
   1.732 +section {* Lifted theorems *}
   1.733 +
   1.734 +subsection {* fset *}
   1.735 +
   1.736 +lemma fset_simps [simp]:
   1.737 +  shows "fset {||} = {}"
   1.738 +  and   "fset (insert_fset x S) = insert x (fset S)"
   1.739 +  by (descending, simp)+
   1.740 +
   1.741 +lemma finite_fset [simp]: 
   1.742 +  shows "finite (fset S)"
   1.743 +  by (descending) (simp)
   1.744 +
   1.745 +lemma fset_cong:
   1.746 +  shows "fset S = fset T \<longleftrightarrow> S = T"
   1.747 +  by (descending) (simp)
   1.748 +
   1.749 +lemma filter_fset [simp]: 
   1.750 +  shows "fset (filter_fset P xs) = P \<inter> fset xs"
   1.751 +  by (descending) (auto simp add: mem_def)
   1.752 +
   1.753 +lemma remove_fset [simp]: 
   1.754 +  shows "fset (remove_fset x xs) = fset xs - {x}"
   1.755 +  by (descending) (simp)
   1.756 +
   1.757 +lemma inter_fset [simp]: 
   1.758 +  shows "fset (xs |\<inter>| ys) = fset xs \<inter> fset ys"
   1.759 +  by (descending) (auto)
   1.760 +
   1.761 +lemma union_fset [simp]: 
   1.762 +  shows "fset (xs |\<union>| ys) = fset xs \<union> fset ys"
   1.763 +  by (lifting set_append)
   1.764 +
   1.765 +lemma minus_fset [simp]: 
   1.766 +  shows "fset (xs - ys) = fset xs - fset ys"
   1.767 +  by (descending) (auto)
   1.768 +
   1.769 +
   1.770 +subsection {* in_fset *}
   1.771 +
   1.772 +lemma in_fset: 
   1.773 +  shows "x |\<in>| S \<longleftrightarrow> x \<in> fset S"
   1.774 +  by (descending) (simp)
   1.775 +
   1.776 +lemma notin_fset: 
   1.777 +  shows "x |\<notin>| S \<longleftrightarrow> x \<notin> fset S"
   1.778 +  by (simp add: in_fset)
   1.779 +
   1.780 +lemma notin_empty_fset: 
   1.781 +  shows "x |\<notin>| {||}"
   1.782 +  by (simp add: in_fset)
   1.783  
   1.784 -lemma nil_not_cons:
   1.785 -  shows "\<not> ([] \<approx> x # xs)"
   1.786 -  and   "\<not> (x # xs \<approx> [])"
   1.787 -  by auto
   1.788 +lemma fset_eq_iff:
   1.789 +  shows "S = T \<longleftrightarrow> (\<forall>x. (x |\<in>| S) = (x |\<in>| T))"
   1.790 +  by (descending) (auto)
   1.791 +
   1.792 +lemma none_in_empty_fset:
   1.793 +  shows "(\<forall>x. x |\<notin>| S) \<longleftrightarrow> S = {||}"
   1.794 +  by (descending) (simp)
   1.795 +
   1.796 +
   1.797 +subsection {* insert_fset *}
   1.798 +
   1.799 +lemma in_insert_fset_iff [simp]:
   1.800 +  shows "x |\<in>| insert_fset y S \<longleftrightarrow> x = y \<or> x |\<in>| S"
   1.801 +  by (descending) (simp)
   1.802 +
   1.803 +lemma
   1.804 +  shows insert_fsetI1: "x |\<in>| insert_fset x S"
   1.805 +  and   insert_fsetI2: "x |\<in>| S \<Longrightarrow> x |\<in>| insert_fset y S"
   1.806 +  by simp_all
   1.807 +
   1.808 +lemma insert_absorb_fset [simp]:
   1.809 +  shows "x |\<in>| S \<Longrightarrow> insert_fset x S = S"
   1.810 +  by (descending) (auto)
   1.811  
   1.812 -lemma no_memb_nil:
   1.813 -  "(\<forall>x. \<not> memb x xs) = (xs = [])"
   1.814 -  by (simp add: memb_def)
   1.815 +lemma empty_not_insert_fset[simp]:
   1.816 +  shows "{||} \<noteq> insert_fset x S"
   1.817 +  and   "insert_fset x S \<noteq> {||}"
   1.818 +  by (descending, simp)+
   1.819 +
   1.820 +lemma insert_fset_left_comm:
   1.821 +  shows "insert_fset x (insert_fset y S) = insert_fset y (insert_fset x S)"
   1.822 +  by (descending) (auto)
   1.823 +
   1.824 +lemma insert_fset_left_idem:
   1.825 +  shows "insert_fset x (insert_fset x S) = insert_fset x S"
   1.826 +  by (descending) (auto)
   1.827 +
   1.828 +lemma singleton_fset_eq[simp]:
   1.829 +  shows "{|x|} = {|y|} \<longleftrightarrow> x = y"
   1.830 +  by (descending) (auto)
   1.831 +
   1.832 +lemma in_fset_mdef:
   1.833 +  shows "x |\<in>| F \<longleftrightarrow> x |\<notin>| (F - {|x|}) \<and> F = insert_fset x (F - {|x|})"
   1.834 +  by (descending) (auto)
   1.835 +
   1.836 +
   1.837 +subsection {* union_fset *}
   1.838 +
   1.839 +lemmas [simp] =
   1.840 +  sup_bot_left[where 'a="'a fset", standard]
   1.841 +  sup_bot_right[where 'a="'a fset", standard]
   1.842 +
   1.843 +lemma union_insert_fset [simp]:
   1.844 +  shows "insert_fset x S |\<union>| T = insert_fset x (S |\<union>| T)"
   1.845 +  by (lifting append.simps(2))
   1.846  
   1.847 -lemma memb_consI1:
   1.848 -  shows "memb x (x # xs)"
   1.849 -  by (simp add: memb_def)
   1.850 +lemma singleton_union_fset_left:
   1.851 +  shows "{|a|} |\<union>| S = insert_fset a S"
   1.852 +  by simp
   1.853 +
   1.854 +lemma singleton_union_fset_right:
   1.855 +  shows "S |\<union>| {|a|} = insert_fset a S"
   1.856 +  by (subst sup.commute) simp
   1.857 +
   1.858 +lemma in_union_fset:
   1.859 +  shows "x |\<in>| S |\<union>| T \<longleftrightarrow> x |\<in>| S \<or> x |\<in>| T"
   1.860 +  by (descending) (simp)
   1.861 +
   1.862 +
   1.863 +subsection {* minus_fset *}
   1.864 +
   1.865 +lemma minus_in_fset: 
   1.866 +  shows "x |\<in>| (xs - ys) \<longleftrightarrow> x |\<in>| xs \<and> x |\<notin>| ys"
   1.867 +  by (descending) (simp)
   1.868 +
   1.869 +lemma minus_insert_fset: 
   1.870 +  shows "insert_fset x xs - ys = (if x |\<in>| ys then xs - ys else insert_fset x (xs - ys))"
   1.871 +  by (descending) (auto)
   1.872 +
   1.873 +lemma minus_insert_in_fset[simp]: 
   1.874 +  shows "x |\<in>| ys \<Longrightarrow> insert_fset x xs - ys = xs - ys"
   1.875 +  by (simp add: minus_insert_fset)
   1.876 +
   1.877 +lemma minus_insert_notin_fset[simp]: 
   1.878 +  shows "x |\<notin>| ys \<Longrightarrow> insert_fset x xs - ys = insert_fset x (xs - ys)"
   1.879 +  by (simp add: minus_insert_fset)
   1.880 +
   1.881 +lemma in_minus_fset: 
   1.882 +  shows "x |\<in>| F - S \<Longrightarrow> x |\<notin>| S"
   1.883 +  unfolding in_fset minus_fset
   1.884 +  by blast
   1.885 +
   1.886 +lemma notin_minus_fset: 
   1.887 +  shows "x |\<in>| S \<Longrightarrow> x |\<notin>| F - S"
   1.888 +  unfolding in_fset minus_fset
   1.889 +  by blast
   1.890 +
   1.891 +
   1.892 +subsection {* remove_fset *}
   1.893 +
   1.894 +lemma in_remove_fset:
   1.895 +  shows "x |\<in>| remove_fset y S \<longleftrightarrow> x |\<in>| S \<and> x \<noteq> y"
   1.896 +  by (descending) (simp)
   1.897 +
   1.898 +lemma notin_remove_fset:
   1.899 +  shows "x |\<notin>| remove_fset x S"
   1.900 +  by (descending) (simp)
   1.901  
   1.902 -lemma memb_consI2:
   1.903 -  shows "memb x xs \<Longrightarrow> memb x (y # xs)"
   1.904 -  by (simp add: memb_def)
   1.905 +lemma notin_remove_ident_fset:
   1.906 +  shows "x |\<notin>| S \<Longrightarrow> remove_fset x S = S"
   1.907 +  by (descending) (simp)
   1.908 +
   1.909 +lemma remove_fset_cases:
   1.910 +  shows "S = {||} \<or> (\<exists>x. x |\<in>| S \<and> S = insert_fset x (remove_fset x S))"
   1.911 +  by (descending) (auto simp add: insert_absorb)
   1.912 +  
   1.913 +
   1.914 +subsection {* inter_fset *}
   1.915 +
   1.916 +lemma inter_empty_fset_l:
   1.917 +  shows "{||} |\<inter>| S = {||}"
   1.918 +  by simp
   1.919 +
   1.920 +lemma inter_empty_fset_r:
   1.921 +  shows "S |\<inter>| {||} = {||}"
   1.922 +  by simp
   1.923 +
   1.924 +lemma inter_insert_fset:
   1.925 +  shows "insert_fset x S |\<inter>| T = (if x |\<in>| T then insert_fset x (S |\<inter>| T) else S |\<inter>| T)"
   1.926 +  by (descending) (auto)
   1.927 +
   1.928 +lemma in_inter_fset:
   1.929 +  shows "x |\<in>| (S |\<inter>| T) \<longleftrightarrow> x |\<in>| S \<and> x |\<in>| T"
   1.930 +  by (descending) (simp)
   1.931 +
   1.932  
   1.933 -lemma singleton_list_eq:
   1.934 -  shows "[x] \<approx> [y] \<longleftrightarrow> x = y"
   1.935 -  by (simp)
   1.936 +subsection {* subset_fset and psubset_fset *}
   1.937 +
   1.938 +lemma subset_fset: 
   1.939 +  shows "xs |\<subseteq>| ys \<longleftrightarrow> fset xs \<subseteq> fset ys"
   1.940 +  by (descending) (simp)
   1.941 +
   1.942 +lemma psubset_fset: 
   1.943 +  shows "xs |\<subset>| ys \<longleftrightarrow> fset xs \<subset> fset ys"
   1.944 +  unfolding less_fset_def 
   1.945 +  by (descending) (auto)
   1.946 +
   1.947 +lemma subset_insert_fset:
   1.948 +  shows "(insert_fset x xs) |\<subseteq>| ys \<longleftrightarrow> x |\<in>| ys \<and> xs |\<subseteq>| ys"
   1.949 +  by (descending) (simp)
   1.950 +
   1.951 +lemma subset_in_fset: 
   1.952 +  shows "xs |\<subseteq>| ys = (\<forall>x. x |\<in>| xs \<longrightarrow> x |\<in>| ys)"
   1.953 +  by (descending) (auto)
   1.954 +
   1.955 +lemma subset_empty_fset:
   1.956 +  shows "xs |\<subseteq>| {||} \<longleftrightarrow> xs = {||}"
   1.957 +  by (descending) (simp)
   1.958 +
   1.959 +lemma not_psubset_empty_fset: 
   1.960 +  shows "\<not> xs |\<subset>| {||}"
   1.961 +  by (metis fset_simps(1) psubset_fset not_psubset_empty)
   1.962 +
   1.963 +
   1.964 +subsection {* map_fset *}
   1.965  
   1.966 -lemma sub_list_cons:
   1.967 -  "sub_list (x # xs) ys = (memb x ys \<and> sub_list xs ys)"
   1.968 -  by (auto simp add: memb_def sub_list_def)
   1.969 +lemma map_fset_simps [simp]:
   1.970 +   shows "map_fset f {||} = {||}"
   1.971 +  and   "map_fset f (insert_fset x S) = insert_fset (f x) (map_fset f S)"
   1.972 +  by (descending, simp)+
   1.973 +
   1.974 +lemma map_fset_image [simp]:
   1.975 +  shows "fset (map_fset f S) = f ` (fset S)"
   1.976 +  by (descending) (simp)
   1.977 +
   1.978 +lemma inj_map_fset_cong:
   1.979 +  shows "inj f \<Longrightarrow> map_fset f S = map_fset f T \<longleftrightarrow> S = T"
   1.980 +  by (descending) (metis inj_vimage_image_eq list_eq.simps set_map)
   1.981 +
   1.982 +lemma map_union_fset: 
   1.983 +  shows "map_fset f (S |\<union>| T) = map_fset f S |\<union>| map_fset f T"
   1.984 +  by (descending) (simp)
   1.985 +
   1.986 +
   1.987 +subsection {* card_fset *}
   1.988 +
   1.989 +lemma card_fset: 
   1.990 +  shows "card_fset xs = card (fset xs)"
   1.991 +  by (descending) (simp)
   1.992 +
   1.993 +lemma card_insert_fset_iff [simp]:
   1.994 +  shows "card_fset (insert_fset x S) = (if x |\<in>| S then card_fset S else Suc (card_fset S))"
   1.995 +  by (descending) (simp add: insert_absorb)
   1.996 +
   1.997 +lemma card_fset_0[simp]:
   1.998 +  shows "card_fset S = 0 \<longleftrightarrow> S = {||}"
   1.999 +  by (descending) (simp)
  1.1000 +
  1.1001 +lemma card_empty_fset[simp]:
  1.1002 +  shows "card_fset {||} = 0"
  1.1003 +  by (simp add: card_fset)
  1.1004 +
  1.1005 +lemma card_fset_1:
  1.1006 +  shows "card_fset S = 1 \<longleftrightarrow> (\<exists>x. S = {|x|})"
  1.1007 +  by (descending) (auto simp add: card_Suc_eq)
  1.1008 +
  1.1009 +lemma card_fset_gt_0:
  1.1010 +  shows "x \<in> fset S \<Longrightarrow> 0 < card_fset S"
  1.1011 +  by (descending) (auto simp add: card_gt_0_iff)
  1.1012 +  
  1.1013 +lemma card_notin_fset:
  1.1014 +  shows "(x |\<notin>| S) = (card_fset (insert_fset x S) = Suc (card_fset S))"
  1.1015 +  by simp
  1.1016  
  1.1017 -lemma fminus_raw_red: 
  1.1018 -  "fminus_raw (x # xs) ys = (if x \<in> set ys then fminus_raw xs ys else x # (fminus_raw xs ys))"
  1.1019 -  by (induct ys arbitrary: xs x) (simp_all)
  1.1020 +lemma card_fset_Suc: 
  1.1021 +  shows "card_fset S = Suc n \<Longrightarrow> \<exists>x T. x |\<notin>| T \<and> S = insert_fset x T \<and> card_fset T = n"
  1.1022 +  apply(descending)
  1.1023 +  apply(auto dest!: card_eq_SucD)
  1.1024 +  by (metis Diff_insert_absorb set_removeAll)
  1.1025 +
  1.1026 +lemma card_remove_fset_iff [simp]:
  1.1027 +  shows "card_fset (remove_fset y S) = (if y |\<in>| S then card_fset S - 1 else card_fset S)"
  1.1028 +  by (descending) (simp)
  1.1029 +
  1.1030 +lemma card_Suc_exists_in_fset: 
  1.1031 +  shows "card_fset S = Suc n \<Longrightarrow> \<exists>a. a |\<in>| S"
  1.1032 +  by (drule card_fset_Suc) (auto)
  1.1033 +
  1.1034 +lemma in_card_fset_not_0: 
  1.1035 +  shows "a |\<in>| A \<Longrightarrow> card_fset A \<noteq> 0"
  1.1036 +  by (descending) (auto)
  1.1037 +
  1.1038 +lemma card_fset_mono: 
  1.1039 +  shows "xs |\<subseteq>| ys \<Longrightarrow> card_fset xs \<le> card_fset ys"
  1.1040 +  unfolding card_fset psubset_fset
  1.1041 +  by (simp add: card_mono subset_fset)
  1.1042 +
  1.1043 +lemma card_subset_fset_eq: 
  1.1044 +  shows "xs |\<subseteq>| ys \<Longrightarrow> card_fset ys \<le> card_fset xs \<Longrightarrow> xs = ys"
  1.1045 +  unfolding card_fset subset_fset
  1.1046 +  by (auto dest: card_seteq[OF finite_fset] simp add: fset_cong)
  1.1047  
  1.1048 -text {* Cardinality of finite sets *}
  1.1049 +lemma psubset_card_fset_mono: 
  1.1050 +  shows "xs |\<subset>| ys \<Longrightarrow> card_fset xs < card_fset ys"
  1.1051 +  unfolding card_fset subset_fset
  1.1052 +  by (metis finite_fset psubset_fset psubset_card_mono)
  1.1053 +
  1.1054 +lemma card_union_inter_fset: 
  1.1055 +  shows "card_fset xs + card_fset ys = card_fset (xs |\<union>| ys) + card_fset (xs |\<inter>| ys)"
  1.1056 +  unfolding card_fset union_fset inter_fset
  1.1057 +  by (rule card_Un_Int[OF finite_fset finite_fset])
  1.1058 +
  1.1059 +lemma card_union_disjoint_fset: 
  1.1060 +  shows "xs |\<inter>| ys = {||} \<Longrightarrow> card_fset (xs |\<union>| ys) = card_fset xs + card_fset ys"
  1.1061 +  unfolding card_fset union_fset 
  1.1062 +  apply (rule card_Un_disjoint[OF finite_fset finite_fset])
  1.1063 +  by (metis inter_fset fset_simps(1))
  1.1064 +
  1.1065 +lemma card_remove_fset_less1: 
  1.1066 +  shows "x |\<in>| xs \<Longrightarrow> card_fset (remove_fset x xs) < card_fset xs"
  1.1067 +  unfolding card_fset in_fset remove_fset 
  1.1068 +  by (rule card_Diff1_less[OF finite_fset])
  1.1069 +
  1.1070 +lemma card_remove_fset_less2: 
  1.1071 +  shows "x |\<in>| xs \<Longrightarrow> y |\<in>| xs \<Longrightarrow> card_fset (remove_fset y (remove_fset x xs)) < card_fset xs"
  1.1072 +  unfolding card_fset remove_fset in_fset
  1.1073 +  by (rule card_Diff2_less[OF finite_fset])
  1.1074 +
  1.1075 +lemma card_remove_fset_le1: 
  1.1076 +  shows "card_fset (remove_fset x xs) \<le> card_fset xs"
  1.1077 +  unfolding remove_fset card_fset
  1.1078 +  by (rule card_Diff1_le[OF finite_fset])
  1.1079  
  1.1080 -lemma fcard_raw_0:
  1.1081 -  shows "fcard_raw xs = 0 \<longleftrightarrow> xs \<approx> []"
  1.1082 -  unfolding fcard_raw_def
  1.1083 -  by (induct xs) (auto)
  1.1084 +lemma card_psubset_fset: 
  1.1085 +  shows "ys |\<subseteq>| xs \<Longrightarrow> card_fset ys < card_fset xs \<Longrightarrow> ys |\<subset>| xs"
  1.1086 +  unfolding card_fset psubset_fset subset_fset
  1.1087 +  by (rule card_psubset[OF finite_fset])
  1.1088 +
  1.1089 +lemma card_map_fset_le: 
  1.1090 +  shows "card_fset (map_fset f xs) \<le> card_fset xs"
  1.1091 +  unfolding card_fset map_fset_image
  1.1092 +  by (rule card_image_le[OF finite_fset])
  1.1093 +
  1.1094 +lemma card_minus_insert_fset[simp]:
  1.1095 +  assumes "a |\<in>| A" and "a |\<notin>| B"
  1.1096 +  shows "card_fset (A - insert_fset a B) = card_fset (A - B) - 1"
  1.1097 +  using assms 
  1.1098 +  unfolding in_fset card_fset minus_fset
  1.1099 +  by (simp add: card_Diff_insert[OF finite_fset])
  1.1100 +
  1.1101 +lemma card_minus_subset_fset:
  1.1102 +  assumes "B |\<subseteq>| A"
  1.1103 +  shows "card_fset (A - B) = card_fset A - card_fset B"
  1.1104 +  using assms 
  1.1105 +  unfolding subset_fset card_fset minus_fset
  1.1106 +  by (rule card_Diff_subset[OF finite_fset])
  1.1107 +
  1.1108 +lemma card_minus_fset:
  1.1109 +  shows "card_fset (A - B) = card_fset A - card_fset (A |\<inter>| B)"
  1.1110 +  unfolding inter_fset card_fset minus_fset
  1.1111 +  by (rule card_Diff_subset_Int) (simp)
  1.1112 +
  1.1113 +
  1.1114 +subsection {* concat_fset *}
  1.1115 +
  1.1116 +lemma concat_empty_fset [simp]:
  1.1117 +  shows "concat_fset {||} = {||}"
  1.1118 +  by (lifting concat.simps(1))
  1.1119 +
  1.1120 +lemma concat_insert_fset [simp]:
  1.1121 +  shows "concat_fset (insert_fset x S) = x |\<union>| concat_fset S"
  1.1122 +  by (lifting concat.simps(2))
  1.1123 +
  1.1124 +lemma concat_inter_fset [simp]:
  1.1125 +  shows "concat_fset (xs |\<union>| ys) = concat_fset xs |\<union>| concat_fset ys"
  1.1126 +  by (lifting concat_append)
  1.1127 +
  1.1128 +
  1.1129 +subsection {* filter_fset *}
  1.1130 +
  1.1131 +lemma subset_filter_fset: 
  1.1132 +  shows "filter_fset P xs |\<subseteq>| filter_fset Q xs = (\<forall> x. x |\<in>| xs \<longrightarrow> P x \<longrightarrow> Q x)"
  1.1133 +  by  (descending) (auto)
  1.1134 +
  1.1135 +lemma eq_filter_fset: 
  1.1136 +  shows "(filter_fset P xs = filter_fset Q xs) = (\<forall>x. x |\<in>| xs \<longrightarrow> P x = Q x)"
  1.1137 +  by (descending) (auto)
  1.1138  
  1.1139 -lemma memb_card_not_0:
  1.1140 -  assumes a: "memb a A"
  1.1141 -  shows "\<not>(fcard_raw A = 0)"
  1.1142 -proof -
  1.1143 -  have "\<not>(\<forall>x. \<not> memb x A)" using a by auto
  1.1144 -  then have "\<not>A \<approx> []" using none_memb_nil[of A] by simp
  1.1145 -  then show ?thesis using fcard_raw_0[of A] by simp
  1.1146 +lemma psubset_filter_fset:
  1.1147 +  shows "(\<And>x. x |\<in>| xs \<Longrightarrow> P x \<Longrightarrow> Q x) \<Longrightarrow> (x |\<in>| xs & \<not> P x & Q x) \<Longrightarrow> 
  1.1148 +    filter_fset P xs |\<subset>| filter_fset Q xs"
  1.1149 +  unfolding less_fset_def by (auto simp add: subset_filter_fset eq_filter_fset)
  1.1150 +
  1.1151 +
  1.1152 +subsection {* fold_fset *}
  1.1153 +
  1.1154 +lemma fold_empty_fset: 
  1.1155 +  shows "fold_fset f z {||} = z"
  1.1156 +  by (descending) (simp)
  1.1157 +
  1.1158 +lemma fold_insert_fset: "fold_fset f z (insert_fset a A) =
  1.1159 +  (if rsp_fold f then if a |\<in>| A then fold_fset f z A else f a (fold_fset f z A) else z)"
  1.1160 +  by (descending) (simp)
  1.1161 +
  1.1162 +lemma in_commute_fold_fset:
  1.1163 +  "\<lbrakk>rsp_fold f; h |\<in>| b\<rbrakk> \<Longrightarrow> fold_fset f z b = f h (fold_fset f z (remove_fset h b))"
  1.1164 +  by (descending) (simp add: memb_commute_fold_list)
  1.1165 +
  1.1166 +
  1.1167 +subsection {* Choice in fsets *}
  1.1168 +
  1.1169 +lemma fset_choice: 
  1.1170 +  assumes a: "\<forall>x. x |\<in>| A \<longrightarrow> (\<exists>y. P x y)"
  1.1171 +  shows "\<exists>f. \<forall>x. x |\<in>| A \<longrightarrow> P x (f x)"
  1.1172 +  using a
  1.1173 +  apply(descending)
  1.1174 +  using finite_set_choice
  1.1175 +  by (auto simp add: Ball_def)
  1.1176 +
  1.1177 +
  1.1178 +section {* Induction and Cases rules for fsets *}
  1.1179 +
  1.1180 +lemma fset_exhaust [case_names empty_fset insert_fset, cases type: fset]:
  1.1181 +  assumes empty_fset_case: "S = {||} \<Longrightarrow> P" 
  1.1182 +  and     insert_fset_case: "\<And>x S'. S = insert_fset x S' \<Longrightarrow> P"
  1.1183 +  shows "P"
  1.1184 +  using assms by (lifting list.exhaust)
  1.1185 +
  1.1186 +lemma fset_induct [case_names empty_fset insert_fset]:
  1.1187 +  assumes empty_fset_case: "P {||}"
  1.1188 +  and     insert_fset_case: "\<And>x S. P S \<Longrightarrow> P (insert_fset x S)"
  1.1189 +  shows "P S"
  1.1190 +  using assms 
  1.1191 +  by (descending) (blast intro: list.induct)
  1.1192 +
  1.1193 +lemma fset_induct_stronger [case_names empty_fset insert_fset, induct type: fset]:
  1.1194 +  assumes empty_fset_case: "P {||}"
  1.1195 +  and     insert_fset_case: "\<And>x S. \<lbrakk>x |\<notin>| S; P S\<rbrakk> \<Longrightarrow> P (insert_fset x S)"
  1.1196 +  shows "P S"
  1.1197 +proof(induct S rule: fset_induct)
  1.1198 +  case empty_fset
  1.1199 +  show "P {||}" using empty_fset_case by simp
  1.1200 +next
  1.1201 +  case (insert_fset x S)
  1.1202 +  have "P S" by fact
  1.1203 +  then show "P (insert_fset x S)" using insert_fset_case 
  1.1204 +    by (cases "x |\<in>| S") (simp_all)
  1.1205  qed
  1.1206  
  1.1207 -text {* fmap *}
  1.1208 -
  1.1209 -lemma map_append:
  1.1210 -  "map f (xs @ ys) \<approx> (map f xs) @ (map f ys)"
  1.1211 -  by simp
  1.1212 -
  1.1213 -lemma memb_append:
  1.1214 -  "memb x (xs @ ys) \<longleftrightarrow> memb x xs \<or> memb x ys"
  1.1215 -  by (induct xs) (simp_all add: not_memb_nil memb_cons_iff)
  1.1216 +lemma fset_card_induct:
  1.1217 +  assumes empty_fset_case: "P {||}"
  1.1218 +  and     card_fset_Suc_case: "\<And>S T. Suc (card_fset S) = (card_fset T) \<Longrightarrow> P S \<Longrightarrow> P T"
  1.1219 +  shows "P S"
  1.1220 +proof (induct S)
  1.1221 +  case empty_fset
  1.1222 +  show "P {||}" by (rule empty_fset_case)
  1.1223 +next
  1.1224 +  case (insert_fset x S)
  1.1225 +  have h: "P S" by fact
  1.1226 +  have "x |\<notin>| S" by fact
  1.1227 +  then have "Suc (card_fset S) = card_fset (insert_fset x S)" 
  1.1228 +    using card_fset_Suc by auto
  1.1229 +  then show "P (insert_fset x S)" 
  1.1230 +    using h card_fset_Suc_case by simp
  1.1231 +qed
  1.1232  
  1.1233  lemma fset_raw_strong_cases:
  1.1234    obtains "xs = []"
  1.1235 @@ -617,7 +999,9 @@
  1.1236    case (Cons a xs)
  1.1237    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
  1.1238    have b: "\<And>x' ys'. \<lbrakk>\<not> memb x' ys'; a # xs \<approx> x' # ys'\<rbrakk> \<Longrightarrow> thesis" by fact
  1.1239 -  have c: "xs = [] \<Longrightarrow> thesis" by (metis no_memb_nil singleton_list_eq b)
  1.1240 +  have c: "xs = [] \<Longrightarrow> thesis" using b 
  1.1241 +    apply(simp)
  1.1242 +    by (metis List.set.simps(1) emptyE empty_subsetI)
  1.1243    have "\<And>x ys. \<lbrakk>\<not> memb x ys; xs \<approx> x # ys\<rbrakk> \<Longrightarrow> thesis"
  1.1244    proof -
  1.1245      fix x :: 'a
  1.1246 @@ -632,64 +1016,63 @@
  1.1247        show thesis using b f g by simp
  1.1248      next
  1.1249        assume h: "x \<noteq> a"
  1.1250 -      then have f: "\<not> memb x (a # ys)" using d unfolding memb_def by auto
  1.1251 +      then have f: "\<not> memb x (a # ys)" using d by auto
  1.1252        have g: "a # xs \<approx> x # (a # ys)" using e h by auto
  1.1253 -      show thesis using b f g by simp
  1.1254 +      show thesis using b f g by (simp del: memb.simps) 
  1.1255      qed
  1.1256    qed
  1.1257    then show thesis using a c by blast
  1.1258  qed
  1.1259  
  1.1260 -section {* deletion *}
  1.1261 +
  1.1262 +lemma fset_strong_cases:
  1.1263 +  obtains "xs = {||}"
  1.1264 +    | x ys where "x |\<notin>| ys" and "xs = insert_fset x ys"
  1.1265 +  by (lifting fset_raw_strong_cases)
  1.1266  
  1.1267  
  1.1268 -lemma fset_raw_removeAll_cases:
  1.1269 -  "xs = [] \<or> (\<exists>x. memb x xs \<and> xs \<approx> x # removeAll x xs)"
  1.1270 -  by (induct xs) (auto simp add: memb_def)
  1.1271 -
  1.1272 -lemma fremoveAll_filter:
  1.1273 -  "removeAll y xs = [x \<leftarrow> xs. x \<noteq> y]"
  1.1274 -  by (induct xs) simp_all
  1.1275 +lemma fset_induct2:
  1.1276 +  "P {||} {||} \<Longrightarrow>
  1.1277 +  (\<And>x xs. x |\<notin>| xs \<Longrightarrow> P (insert_fset x xs) {||}) \<Longrightarrow>
  1.1278 +  (\<And>y ys. y |\<notin>| ys \<Longrightarrow> P {||} (insert_fset y ys)) \<Longrightarrow>
  1.1279 +  (\<And>x xs y ys. \<lbrakk>P xs ys; x |\<notin>| xs; y |\<notin>| ys\<rbrakk> \<Longrightarrow> P (insert_fset x xs) (insert_fset y ys)) \<Longrightarrow>
  1.1280 +  P xsa ysa"
  1.1281 +  apply (induct xsa arbitrary: ysa)
  1.1282 +  apply (induct_tac x rule: fset_induct_stronger)
  1.1283 +  apply simp_all
  1.1284 +  apply (induct_tac xa rule: fset_induct_stronger)
  1.1285 +  apply simp_all
  1.1286 +  done
  1.1287  
  1.1288 -lemma fcard_raw_delete:
  1.1289 -  "fcard_raw (removeAll y xs) = (if memb y xs then fcard_raw xs - 1 else fcard_raw xs)"
  1.1290 -  by (auto simp add: fcard_raw_def memb_def)
  1.1291 +
  1.1292  
  1.1293 -lemma set_cong:
  1.1294 -  shows "(x \<approx> y) = (set x = set y)"
  1.1295 -  by auto
  1.1296 -
  1.1297 -lemma inj_map_eq_iff:
  1.1298 -  "inj f \<Longrightarrow> (map f l \<approx> map f m) = (l \<approx> m)"
  1.1299 -  by (simp add: set_eq_iff[symmetric] inj_image_eq_iff)
  1.1300 -
  1.1301 -text {* alternate formulation with a different decomposition principle
  1.1302 +subsection {* alternate formulation with a different decomposition principle
  1.1303    and a proof of equivalence *}
  1.1304  
  1.1305  inductive
  1.1306 -  list_eq2
  1.1307 +  list_eq2 ("_ \<approx>2 _")
  1.1308  where
  1.1309 -  "list_eq2 (a # b # xs) (b # a # xs)"
  1.1310 -| "list_eq2 [] []"
  1.1311 -| "list_eq2 xs ys \<Longrightarrow> list_eq2 ys xs"
  1.1312 -| "list_eq2 (a # a # xs) (a # xs)"
  1.1313 -| "list_eq2 xs ys \<Longrightarrow> list_eq2 (a # xs) (a # ys)"
  1.1314 -| "\<lbrakk>list_eq2 xs1 xs2; list_eq2 xs2 xs3\<rbrakk> \<Longrightarrow> list_eq2 xs1 xs3"
  1.1315 +  "(a # b # xs) \<approx>2 (b # a # xs)"
  1.1316 +| "[] \<approx>2 []"
  1.1317 +| "xs \<approx>2 ys \<Longrightarrow>  ys \<approx>2 xs"
  1.1318 +| "(a # a # xs) \<approx>2 (a # xs)"
  1.1319 +| "xs \<approx>2 ys \<Longrightarrow>  (a # xs) \<approx>2 (a # ys)"
  1.1320 +| "\<lbrakk>xs1 \<approx>2 xs2;  xs2 \<approx>2 xs3\<rbrakk> \<Longrightarrow> xs1 \<approx>2 xs3"
  1.1321  
  1.1322  lemma list_eq2_refl:
  1.1323 -  shows "list_eq2 xs xs"
  1.1324 +  shows "xs \<approx>2 xs"
  1.1325    by (induct xs) (auto intro: list_eq2.intros)
  1.1326  
  1.1327  lemma cons_delete_list_eq2:
  1.1328 -  shows "list_eq2 (a # (removeAll a A)) (if memb a A then A else a # A)"
  1.1329 +  shows "(a # (removeAll a A)) \<approx>2 (if memb a A then A else a # A)"
  1.1330    apply (induct A)
  1.1331 -  apply (simp add: memb_def list_eq2_refl)
  1.1332 +  apply (simp add: list_eq2_refl)
  1.1333    apply (case_tac "memb a (aa # A)")
  1.1334 -  apply (simp_all only: memb_cons_iff)
  1.1335 +  apply (simp_all)
  1.1336    apply (case_tac [!] "a = aa")
  1.1337    apply (simp_all)
  1.1338    apply (case_tac "memb a A")
  1.1339 -  apply (auto simp add: memb_def)[2]
  1.1340 +  apply (auto)[2]
  1.1341    apply (metis list_eq2.intros(3) list_eq2.intros(4) list_eq2.intros(5) list_eq2.intros(6))
  1.1342    apply (metis list_eq2.intros(1) list_eq2.intros(5) list_eq2.intros(6))
  1.1343    apply (auto simp add: list_eq2_refl memb_def)
  1.1344 @@ -697,7 +1080,7 @@
  1.1345  
  1.1346  lemma memb_delete_list_eq2:
  1.1347    assumes a: "memb e r"
  1.1348 -  shows "list_eq2 (e # removeAll e r) r"
  1.1349 +  shows "(e # removeAll e r) \<approx>2 r"
  1.1350    using a cons_delete_list_eq2[of e r]
  1.1351    by simp
  1.1352  
  1.1353 @@ -708,542 +1091,67 @@
  1.1354  next
  1.1355    {
  1.1356      fix n
  1.1357 -    assume a: "fcard_raw l = n" and b: "l \<approx> r"
  1.1358 -    have "list_eq2 l r"
  1.1359 +    assume a: "card_list l = n" and b: "l \<approx> r"
  1.1360 +    have "l \<approx>2 r"
  1.1361        using a b
  1.1362      proof (induct n arbitrary: l r)
  1.1363        case 0
  1.1364 -      have "fcard_raw l = 0" by fact
  1.1365 -      then have "\<forall>x. \<not> memb x l" using memb_card_not_0[of _ l] by auto
  1.1366 -      then have z: "l = []" using no_memb_nil by auto
  1.1367 +      have "card_list l = 0" by fact
  1.1368 +      then have "\<forall>x. \<not> memb x l" by auto
  1.1369 +      then have z: "l = []" by auto
  1.1370        then have "r = []" using `l \<approx> r` by simp
  1.1371        then show ?case using z list_eq2_refl by simp
  1.1372      next
  1.1373        case (Suc m)
  1.1374        have b: "l \<approx> r" by fact
  1.1375 -      have d: "fcard_raw l = Suc m" by fact
  1.1376 +      have d: "card_list l = Suc m" by fact
  1.1377        then have "\<exists>a. memb a l" 
  1.1378 -	apply(simp add: fcard_raw_def memb_def)
  1.1379 +	apply(simp)
  1.1380  	apply(drule card_eq_SucD)
  1.1381  	apply(blast)
  1.1382  	done
  1.1383        then obtain a where e: "memb a l" by auto
  1.1384        then have e': "memb a r" using list_eq.simps[simplified memb_def[symmetric], of l r] b 
  1.1385 -	unfolding memb_def by auto
  1.1386 -      have f: "fcard_raw (removeAll a l) = m" using fcard_raw_delete[of a l] e d by simp
  1.1387 +	by auto
  1.1388 +      have f: "card_list (removeAll a l) = m" using e d by (simp)
  1.1389        have g: "removeAll a l \<approx> removeAll a r" using removeAll_rsp b by simp
  1.1390 -      have "list_eq2 (removeAll a l) (removeAll a r)" by (rule Suc.hyps[OF f g])
  1.1391 -      then have h: "list_eq2 (a # removeAll a l) (a # removeAll a r)" by (rule list_eq2.intros(5))
  1.1392 -      have i: "list_eq2 l (a # removeAll a l)"
  1.1393 +      have "(removeAll a l) \<approx>2 (removeAll a r)" by (rule Suc.hyps[OF f g])
  1.1394 +      then have h: "(a # removeAll a l) \<approx>2 (a # removeAll a r)" by (rule list_eq2.intros(5))
  1.1395 +      have i: "l \<approx>2 (a # removeAll a l)"	
  1.1396          by (rule list_eq2.intros(3)[OF memb_delete_list_eq2[OF e]])
  1.1397 -      have "list_eq2 l (a # removeAll a r)" by (rule list_eq2.intros(6)[OF i h])
  1.1398 +      have "l \<approx>2 (a # removeAll a r)" by (rule list_eq2.intros(6)[OF i h])
  1.1399        then show ?case using list_eq2.intros(6)[OF _ memb_delete_list_eq2[OF e']] by simp
  1.1400      qed
  1.1401      }
  1.1402 -  then show "l \<approx> r \<Longrightarrow> list_eq2 l r" by blast
  1.1403 -qed
  1.1404 -
  1.1405 -text {* Lifted theorems *}
  1.1406 -
  1.1407 -lemma not_fin_fnil: "x |\<notin>| {||}"
  1.1408 -  by (descending) (simp add: memb_def)
  1.1409 -
  1.1410 -lemma fin_finsert_iff[simp]:
  1.1411 -  "x |\<in>| finsert y S \<longleftrightarrow> x = y \<or> x |\<in>| S"
  1.1412 -  by (descending) (simp add: memb_def)
  1.1413 -
  1.1414 -lemma
  1.1415 -  shows finsertI1: "x |\<in>| finsert x S"
  1.1416 -  and   finsertI2: "x |\<in>| S \<Longrightarrow> x |\<in>| finsert y S"
  1.1417 -  by (lifting memb_consI1 memb_consI2)
  1.1418 -
  1.1419 -lemma finsert_absorb[simp]:
  1.1420 -  shows "x |\<in>| S \<Longrightarrow> finsert x S = S"
  1.1421 -  by (descending) (auto simp add: memb_def)
  1.1422 -
  1.1423 -lemma fempty_not_finsert[simp]:
  1.1424 -  "{||} \<noteq> finsert x S"
  1.1425 -  "finsert x S \<noteq> {||}"
  1.1426 -  by (lifting nil_not_cons)
  1.1427 -
  1.1428 -lemma finsert_left_comm:
  1.1429 -  "finsert x (finsert y S) = finsert y (finsert x S)"
  1.1430 -  by (descending) (auto)
  1.1431 -
  1.1432 -lemma finsert_left_idem:
  1.1433 -  "finsert x (finsert x S) = finsert x S"
  1.1434 -  by (descending) (auto)
  1.1435 -
  1.1436 -lemma fsingleton_eq[simp]:
  1.1437 -  shows "{|x|} = {|y|} \<longleftrightarrow> x = y"
  1.1438 -  by (descending) (auto)
  1.1439 -
  1.1440 -
  1.1441 -text {* fset *}
  1.1442 -
  1.1443 -lemma fset_simps[simp]:
  1.1444 -  "fset {||} = ({} :: 'a set)"
  1.1445 -  "fset (finsert (h :: 'a) t) = insert h (fset t)"
  1.1446 -  by (lifting set.simps)
  1.1447 -
  1.1448 -lemma in_fset:
  1.1449 -  "x \<in> fset S \<equiv> x |\<in>| S"
  1.1450 -  by (lifting memb_def[symmetric])
  1.1451 -
  1.1452 -lemma none_fin_fempty:
  1.1453 -  "(\<forall>x. x |\<notin>| S) \<longleftrightarrow> S = {||}"
  1.1454 -  by (lifting none_memb_nil)
  1.1455 -
  1.1456 -lemma fset_cong:
  1.1457 -  "S = T \<longleftrightarrow> fset S = fset T"
  1.1458 -  by (lifting set_cong)
  1.1459 -
  1.1460 -
  1.1461 -text {* fcard *}
  1.1462 -
  1.1463 -lemma fcard_finsert_if [simp]:
  1.1464 -  shows "fcard (finsert x S) = (if x |\<in>| S then fcard S else Suc (fcard S))"
  1.1465 -  by (descending) (auto simp add: fcard_raw_def memb_def insert_absorb)
  1.1466 -
  1.1467 -lemma fcard_0[simp]:
  1.1468 -  shows "fcard S = 0 \<longleftrightarrow> S = {||}"
  1.1469 -  by (descending) (simp add: fcard_raw_def)
  1.1470 -
  1.1471 -lemma fcard_fempty[simp]:
  1.1472 -  shows "fcard {||} = 0"
  1.1473 -  by (simp add: fcard_0)
  1.1474 -
  1.1475 -lemma fcard_1:
  1.1476 -  shows "fcard S = 1 \<longleftrightarrow> (\<exists>x. S = {|x|})"
  1.1477 -  by (descending) (auto simp add: fcard_raw_def card_Suc_eq)
  1.1478 -
  1.1479 -lemma fcard_gt_0:
  1.1480 -  shows "x \<in> fset S \<Longrightarrow> 0 < fcard S"
  1.1481 -  by (descending) (auto simp add: fcard_raw_def card_gt_0_iff)
  1.1482 -  
  1.1483 -lemma fcard_not_fin:
  1.1484 -  shows "(x |\<notin>| S) = (fcard (finsert x S) = Suc (fcard S))"
  1.1485 -  by (descending) (auto simp add: memb_def fcard_raw_def insert_absorb)
  1.1486 -
  1.1487 -lemma fcard_suc: "fcard S = Suc n \<Longrightarrow> \<exists>x T. x |\<notin>| T \<and> S = finsert x T \<and> fcard T = n"
  1.1488 -  apply descending
  1.1489 -  apply(simp add: fcard_raw_def memb_def)
  1.1490 -  apply(drule card_eq_SucD)
  1.1491 -  apply(auto)
  1.1492 -  apply(rule_tac x="b" in exI)
  1.1493 -  apply(rule_tac x="removeAll b S" in exI)
  1.1494 -  apply(auto)
  1.1495 -  done
  1.1496 -
  1.1497 -lemma fcard_delete:
  1.1498 -  "fcard (fdelete y S) = (if y |\<in>| S then fcard S - 1 else fcard S)"
  1.1499 -  by (lifting fcard_raw_delete)
  1.1500 -
  1.1501 -lemma fcard_suc_memb: 
  1.1502 -  shows "fcard A = Suc n \<Longrightarrow> \<exists>a. a |\<in>| A"
  1.1503 -  apply(descending)
  1.1504 -  apply(simp add: fcard_raw_def memb_def)
  1.1505 -  apply(drule card_eq_SucD)
  1.1506 -  apply(auto)
  1.1507 -  done
  1.1508 -
  1.1509 -lemma fin_fcard_not_0: 
  1.1510 -  shows "a |\<in>| A \<Longrightarrow> fcard A \<noteq> 0"
  1.1511 -  by (descending) (auto simp add: fcard_raw_def memb_def)
  1.1512 -
  1.1513 -
  1.1514 -text {* funion *}
  1.1515 -
  1.1516 -lemmas [simp] =
  1.1517 -  sup_bot_left[where 'a="'a fset", standard]
  1.1518 -  sup_bot_right[where 'a="'a fset", standard]
  1.1519 -
  1.1520 -lemma funion_finsert[simp]:
  1.1521 -  shows "finsert x S |\<union>| T = finsert x (S |\<union>| T)"
  1.1522 -  by (lifting append.simps(2))
  1.1523 -
  1.1524 -lemma singleton_union_left:
  1.1525 -  shows "{|a|} |\<union>| S = finsert a S"
  1.1526 -  by simp
  1.1527 -
  1.1528 -lemma singleton_union_right:
  1.1529 -  shows "S |\<union>| {|a|} = finsert a S"
  1.1530 -  by (subst sup.commute) simp
  1.1531 -
  1.1532 -
  1.1533 -section {* Induction and Cases rules for fsets *}
  1.1534 -
  1.1535 -lemma fset_strong_cases:
  1.1536 -  obtains "xs = {||}"
  1.1537 -    | x ys where "x |\<notin>| ys" and "xs = finsert x ys"
  1.1538 -  by (lifting fset_raw_strong_cases)
  1.1539 -
  1.1540 -lemma fset_exhaust[case_names fempty finsert, cases type: fset]:
  1.1541 -  shows "\<lbrakk>S = {||} \<Longrightarrow> P; \<And>x S'. S = finsert x S' \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
  1.1542 -  by (lifting list.exhaust)
  1.1543 -
  1.1544 -lemma fset_induct_weak[case_names fempty finsert]:
  1.1545 -  shows "\<lbrakk>P {||}; \<And>x S. P S \<Longrightarrow> P (finsert x S)\<rbrakk> \<Longrightarrow> P S"
  1.1546 -  by (lifting list.induct)
  1.1547 -
  1.1548 -lemma fset_induct[case_names fempty finsert, induct type: fset]:
  1.1549 -  assumes prem1: "P {||}"
  1.1550 -  and     prem2: "\<And>x S. \<lbrakk>x |\<notin>| S; P S\<rbrakk> \<Longrightarrow> P (finsert x S)"
  1.1551 -  shows "P S"
  1.1552 -proof(induct S rule: fset_induct_weak)
  1.1553 -  case fempty
  1.1554 -  show "P {||}" by (rule prem1)
  1.1555 -next
  1.1556 -  case (finsert x S)
  1.1557 -  have asm: "P S" by fact
  1.1558 -  show "P (finsert x S)"
  1.1559 -    by (cases "x |\<in>| S") (simp_all add: asm prem2)
  1.1560 +  then show "l \<approx> r \<Longrightarrow> l \<approx>2 r" by blast
  1.1561  qed
  1.1562  
  1.1563 -lemma fset_induct2:
  1.1564 -  "P {||} {||} \<Longrightarrow>
  1.1565 -  (\<And>x xs. x |\<notin>| xs \<Longrightarrow> P (finsert x xs) {||}) \<Longrightarrow>
  1.1566 -  (\<And>y ys. y |\<notin>| ys \<Longrightarrow> P {||} (finsert y ys)) \<Longrightarrow>
  1.1567 -  (\<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>
  1.1568 -  P xsa ysa"
  1.1569 -  apply (induct xsa arbitrary: ysa)
  1.1570 -  apply (induct_tac x rule: fset_induct)
  1.1571 -  apply simp_all
  1.1572 -  apply (induct_tac xa rule: fset_induct)
  1.1573 -  apply simp_all
  1.1574 -  done
  1.1575 -
  1.1576 -lemma fset_fcard_induct:
  1.1577 -  assumes a: "P {||}"
  1.1578 -  and     b: "\<And>xs ys. Suc (fcard xs) = (fcard ys) \<Longrightarrow> P xs \<Longrightarrow> P ys"
  1.1579 -  shows "P zs"
  1.1580 -proof (induct zs)
  1.1581 -  show "P {||}" by (rule a)
  1.1582 -next
  1.1583 -  fix x :: 'a and zs :: "'a fset"
  1.1584 -  assume h: "P zs"
  1.1585 -  assume "x |\<notin>| zs"
  1.1586 -  then have H1: "Suc (fcard zs) = fcard (finsert x zs)" using fcard_suc by auto
  1.1587 -  then show "P (finsert x zs)" using b h by simp
  1.1588 -qed
  1.1589 -
  1.1590 -text {* fmap *}
  1.1591 -
  1.1592 -lemma fmap_simps[simp]:
  1.1593 -  fixes f::"'a \<Rightarrow> 'b"
  1.1594 -  shows "fmap f {||} = {||}"
  1.1595 -  and   "fmap f (finsert x S) = finsert (f x) (fmap f S)"
  1.1596 -  by (lifting map.simps)
  1.1597 -
  1.1598 -lemma fmap_set_image:
  1.1599 -  "fset (fmap f S) = f ` (fset S)"
  1.1600 -  by (induct S) simp_all
  1.1601 -
  1.1602 -lemma inj_fmap_eq_iff:
  1.1603 -  "inj f \<Longrightarrow> fmap f S = fmap f T \<longleftrightarrow> S = T"
  1.1604 -  by (lifting inj_map_eq_iff)
  1.1605 -
  1.1606 -lemma fmap_funion: 
  1.1607 -  shows "fmap f (S |\<union>| T) = fmap f S |\<union>| fmap f T"
  1.1608 -  by (lifting map_append)
  1.1609 -
  1.1610 -lemma fin_funion:
  1.1611 -  shows "x |\<in>| S |\<union>| T \<longleftrightarrow> x |\<in>| S \<or> x |\<in>| T"
  1.1612 -  by (lifting memb_append)
  1.1613 -
  1.1614 -
  1.1615 -section {* fset *}
  1.1616 -
  1.1617 -lemma fin_set: 
  1.1618 -  shows "x |\<in>| xs \<longleftrightarrow> x \<in> fset xs"
  1.1619 -  by (lifting memb_def)
  1.1620 -
  1.1621 -lemma fnotin_set: 
  1.1622 -  shows "x |\<notin>| xs \<longleftrightarrow> x \<notin> fset xs"
  1.1623 -  by (simp add: fin_set)
  1.1624 -
  1.1625 -lemma fcard_set: 
  1.1626 -  shows "fcard xs = card (fset xs)"
  1.1627 -  by (lifting fcard_raw_def)
  1.1628 -
  1.1629 -lemma fsubseteq_set: 
  1.1630 -  shows "xs |\<subseteq>| ys \<longleftrightarrow> fset xs \<subseteq> fset ys"
  1.1631 -  by (lifting sub_list_def)
  1.1632 -
  1.1633 -lemma fsubset_set: 
  1.1634 -  shows "xs |\<subset>| ys \<longleftrightarrow> fset xs \<subset> fset ys"
  1.1635 -  unfolding less_fset_def 
  1.1636 -  by (descending) (auto simp add: sub_list_def)
  1.1637 -
  1.1638 -lemma ffilter_set [simp]: 
  1.1639 -  shows "fset (ffilter P xs) = P \<inter> fset xs"
  1.1640 -  by (descending) (auto simp add: mem_def)
  1.1641 -
  1.1642 -lemma fdelete_set [simp]: 
  1.1643 -  shows "fset (fdelete x xs) = fset xs - {x}"
  1.1644 -  by (lifting set_removeAll)
  1.1645 -
  1.1646 -lemma finter_set [simp]: 
  1.1647 -  shows "fset (xs |\<inter>| ys) = fset xs \<inter> fset ys"
  1.1648 -  by (lifting set_finter_raw)
  1.1649 -
  1.1650 -lemma funion_set [simp]: 
  1.1651 -  shows "fset (xs |\<union>| ys) = fset xs \<union> fset ys"
  1.1652 -  by (lifting set_append)
  1.1653 -
  1.1654 -lemma fminus_set [simp]: 
  1.1655 -  shows "fset (xs - ys) = fset xs - fset ys"
  1.1656 -  by (lifting set_fminus_raw)
  1.1657 -
  1.1658 -lemmas fset_to_set_trans =
  1.1659 -  fin_set fnotin_set fcard_set fsubseteq_set fsubset_set
  1.1660 -  finter_set funion_set ffilter_set fset_simps
  1.1661 -  fset_cong fdelete_set fmap_set_image fminus_set
  1.1662 -
  1.1663 -
  1.1664 -text {* ffold *}
  1.1665 -
  1.1666 -lemma ffold_nil: 
  1.1667 -  shows "ffold f z {||} = z"
  1.1668 -  by (lifting ffold_raw.simps(1)[where 'a="'b" and 'b="'a"])
  1.1669 -
  1.1670 -lemma ffold_finsert: "ffold f z (finsert a A) =
  1.1671 -  (if rsp_fold f then if a |\<in>| A then ffold f z A else f a (ffold f z A) else z)"
  1.1672 -  by (descending) (simp add: memb_def)
  1.1673 -
  1.1674 -lemma fin_commute_ffold:
  1.1675 -  "\<lbrakk>rsp_fold f; h |\<in>| b\<rbrakk> \<Longrightarrow> ffold f z b = f h (ffold f z (fdelete h b))"
  1.1676 -  by (descending) (simp add: memb_def memb_commute_ffold_raw)
  1.1677 -
  1.1678 -
  1.1679 -text {* fdelete *}
  1.1680 -
  1.1681 -lemma fin_fdelete:
  1.1682 -  shows "x |\<in>| fdelete y S \<longleftrightarrow> x |\<in>| S \<and> x \<noteq> y"
  1.1683 -  by (descending) (simp add: memb_def)
  1.1684 -
  1.1685 -lemma fnotin_fdelete:
  1.1686 -  shows "x |\<notin>| fdelete x S"
  1.1687 -  by (descending) (simp add: memb_def)
  1.1688 -
  1.1689 -lemma fnotin_fdelete_ident:
  1.1690 -  shows "x |\<notin>| S \<Longrightarrow> fdelete x S = S"
  1.1691 -  by (descending) (simp add: memb_def)
  1.1692 -
  1.1693 -lemma fset_fdelete_cases:
  1.1694 -  shows "S = {||} \<or> (\<exists>x. x |\<in>| S \<and> S = finsert x (fdelete x S))"
  1.1695 -  by (lifting fset_raw_removeAll_cases)
  1.1696 -
  1.1697 -text {* finite intersection *}
  1.1698 -
  1.1699 -lemma finter_empty_l:
  1.1700 -  shows "{||} |\<inter>| S = {||}"
  1.1701 -  by simp
  1.1702 -
  1.1703 -
  1.1704 -lemma finter_empty_r:
  1.1705 -  shows "S |\<inter>| {||} = {||}"
  1.1706 -  by simp
  1.1707 -
  1.1708 -lemma finter_finsert:
  1.1709 -  shows "finsert x S |\<inter>| T = (if x |\<in>| T then finsert x (S |\<inter>| T) else S |\<inter>| T)"
  1.1710 -  by (descending) (simp add: memb_def)
  1.1711 -
  1.1712 -lemma fin_finter:
  1.1713 -  shows "x |\<in>| (S |\<inter>| T) \<longleftrightarrow> x |\<in>| S \<and> x |\<in>| T"
  1.1714 -  by (descending) (simp add: memb_def)
  1.1715 -
  1.1716 -lemma fsubset_finsert:
  1.1717 -  shows "finsert x xs |\<subseteq>| ys \<longleftrightarrow> x |\<in>| ys \<and> xs |\<subseteq>| ys"
  1.1718 -  by (lifting sub_list_cons)
  1.1719 -
  1.1720 -lemma 
  1.1721 -  shows "xs |\<subseteq>| ys \<equiv> \<forall>x. x |\<in>| xs \<longrightarrow> x |\<in>| ys"
  1.1722 -  by (descending) (auto simp add: sub_list_def memb_def)
  1.1723 -
  1.1724 -lemma fsubset_fin: 
  1.1725 -  shows "xs |\<subseteq>| ys = (\<forall>x. x |\<in>| xs \<longrightarrow> x |\<in>| ys)"
  1.1726 -  by (descending) (auto simp add: sub_list_def memb_def)
  1.1727 -
  1.1728 -lemma fminus_fin: 
  1.1729 -  shows "x |\<in>| xs - ys \<longleftrightarrow> x |\<in>| xs \<and> x |\<notin>| ys"
  1.1730 -  by (descending) (simp add: memb_def)
  1.1731 -
  1.1732 -lemma fminus_red: 
  1.1733 -  shows "finsert x xs - ys = (if x |\<in>| ys then xs - ys else finsert x (xs - ys))"
  1.1734 -  by (descending) (auto simp add: memb_def)
  1.1735 -
  1.1736 -lemma fminus_red_fin [simp]: 
  1.1737 -  shows "x |\<in>| ys \<Longrightarrow> finsert x xs - ys = xs - ys"
  1.1738 -  by (simp add: fminus_red)
  1.1739 -
  1.1740 -lemma fminus_red_fnotin[simp]: 
  1.1741 -  shows "x |\<notin>| ys \<Longrightarrow> finsert x xs - ys = finsert x (xs - ys)"
  1.1742 -  by (simp add: fminus_red)
  1.1743 -
  1.1744 -lemma fset_eq_iff:
  1.1745 -  shows "S = T \<longleftrightarrow> (\<forall>x. (x |\<in>| S) = (x |\<in>| T))"
  1.1746 -  by (descending) (auto simp add: memb_def)
  1.1747  
  1.1748  (* We cannot write it as "assumes .. shows" since Isabelle changes
  1.1749     the quantifiers to schematic variables and reintroduces them in
  1.1750     a different order *)
  1.1751  lemma fset_eq_cases:
  1.1752   "\<lbrakk>a1 = a2;
  1.1753 -   \<And>a b xs. \<lbrakk>a1 = finsert a (finsert b xs); a2 = finsert b (finsert a xs)\<rbrakk> \<Longrightarrow> P;
  1.1754 +   \<And>a b xs. \<lbrakk>a1 = insert_fset a (insert_fset b xs); a2 = insert_fset b (insert_fset a xs)\<rbrakk> \<Longrightarrow> P;
  1.1755     \<lbrakk>a1 = {||}; a2 = {||}\<rbrakk> \<Longrightarrow> P; \<And>xs ys. \<lbrakk>a1 = ys; a2 = xs; xs = ys\<rbrakk> \<Longrightarrow> P;
  1.1756 -   \<And>a xs. \<lbrakk>a1 = finsert a (finsert a xs); a2 = finsert a xs\<rbrakk> \<Longrightarrow> P;
  1.1757 -   \<And>xs ys a. \<lbrakk>a1 = finsert a xs; a2 = finsert a ys; xs = ys\<rbrakk> \<Longrightarrow> P;
  1.1758 +   \<And>a xs. \<lbrakk>a1 = insert_fset a (insert_fset a xs); a2 = insert_fset a xs\<rbrakk> \<Longrightarrow> P;
  1.1759 +   \<And>xs ys a. \<lbrakk>a1 = insert_fset a xs; a2 = insert_fset a ys; xs = ys\<rbrakk> \<Longrightarrow> P;
  1.1760     \<And>xs1 xs2 xs3. \<lbrakk>a1 = xs1; a2 = xs3; xs1 = xs2; xs2 = xs3\<rbrakk> \<Longrightarrow> P\<rbrakk>
  1.1761    \<Longrightarrow> P"
  1.1762    by (lifting list_eq2.cases[simplified list_eq2_equiv[symmetric]])
  1.1763  
  1.1764  lemma fset_eq_induct:
  1.1765    assumes "x1 = x2"
  1.1766 -  and "\<And>a b xs. P (finsert a (finsert b xs)) (finsert b (finsert a xs))"
  1.1767 +  and "\<And>a b xs. P (insert_fset a (insert_fset b xs)) (insert_fset b (insert_fset a xs))"
  1.1768    and "P {||} {||}"
  1.1769    and "\<And>xs ys. \<lbrakk>xs = ys; P xs ys\<rbrakk> \<Longrightarrow> P ys xs"
  1.1770 -  and "\<And>a xs. P (finsert a (finsert a xs)) (finsert a xs)"
  1.1771 -  and "\<And>xs ys a. \<lbrakk>xs = ys; P xs ys\<rbrakk> \<Longrightarrow> P (finsert a xs) (finsert a ys)"
  1.1772 +  and "\<And>a xs. P (insert_fset a (insert_fset a xs)) (insert_fset a xs)"
  1.1773 +  and "\<And>xs ys a. \<lbrakk>xs = ys; P xs ys\<rbrakk> \<Longrightarrow> P (insert_fset a xs) (insert_fset a ys)"
  1.1774    and "\<And>xs1 xs2 xs3. \<lbrakk>xs1 = xs2; P xs1 xs2; xs2 = xs3; P xs2 xs3\<rbrakk> \<Longrightarrow> P xs1 xs3"
  1.1775    shows "P x1 x2"
  1.1776    using assms
  1.1777    by (lifting list_eq2.induct[simplified list_eq2_equiv[symmetric]])
  1.1778  
  1.1779 -section {* fconcat *}
  1.1780 -
  1.1781 -lemma fconcat_empty:
  1.1782 -  shows "fconcat {||} = {||}"
  1.1783 -  by (lifting concat.simps(1))
  1.1784 -
  1.1785 -lemma fconcat_insert:
  1.1786 -  shows "fconcat (finsert x S) = x |\<union>| fconcat S"
  1.1787 -  by (lifting concat.simps(2))
  1.1788 -
  1.1789 -lemma 
  1.1790 -  shows "fconcat (xs |\<union>| ys) = fconcat xs |\<union>| fconcat ys"
  1.1791 -  by (lifting concat_append)
  1.1792 -
  1.1793 -
  1.1794 -section {* ffilter *}
  1.1795 -
  1.1796 -lemma subseteq_filter: 
  1.1797 -  shows "ffilter P xs <= ffilter Q xs = (\<forall> x. x |\<in>| xs \<longrightarrow> P x \<longrightarrow> Q x)"
  1.1798 -  by  (descending) (auto simp add: memb_def sub_list_def)
  1.1799 -
  1.1800 -lemma eq_ffilter: 
  1.1801 -  shows "(ffilter P xs = ffilter Q xs) = (\<forall>x. x |\<in>| xs \<longrightarrow> P x = Q x)"
  1.1802 -  by (descending) (auto simp add: memb_def)
  1.1803 -
  1.1804 -lemma subset_ffilter:
  1.1805 -  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"
  1.1806 -  unfolding less_fset_def by (auto simp add: subseteq_filter eq_ffilter)
  1.1807 -
  1.1808 -
  1.1809 -section {* lemmas transferred from Finite_Set theory *}
  1.1810 -
  1.1811 -text {* finiteness for finite sets holds *}
  1.1812 -lemma finite_fset [simp]: 
  1.1813 -  shows "finite (fset S)"
  1.1814 -  by (induct S) auto
  1.1815 -
  1.1816 -lemma fset_choice: 
  1.1817 -  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)"
  1.1818 -  unfolding fset_to_set_trans
  1.1819 -  by (rule finite_set_choice[simplified Ball_def, OF finite_fset])
  1.1820 -
  1.1821 -lemma fsubseteq_fempty:
  1.1822 -  shows "xs |\<subseteq>| {||} \<longleftrightarrow> xs = {||}"
  1.1823 -  by (metis finter_empty_r le_iff_inf)
  1.1824 -
  1.1825 -lemma not_fsubset_fnil: 
  1.1826 -  shows "\<not> xs |\<subset>| {||}"
  1.1827 -  by (metis fset_simps(1) fsubset_set not_psubset_empty)
  1.1828 -  
  1.1829 -lemma fcard_mono: 
  1.1830 -  shows "xs |\<subseteq>| ys \<Longrightarrow> fcard xs \<le> fcard ys"
  1.1831 -  unfolding fset_to_set_trans
  1.1832 -  by (rule card_mono[OF finite_fset])
  1.1833 -
  1.1834 -lemma fcard_fseteq: 
  1.1835 -  shows "xs |\<subseteq>| ys \<Longrightarrow> fcard ys \<le> fcard xs \<Longrightarrow> xs = ys"
  1.1836 -  unfolding fcard_set fsubseteq_set
  1.1837 -  by (simp add: card_seteq[OF finite_fset] fset_cong)
  1.1838 -
  1.1839 -lemma psubset_fcard_mono: 
  1.1840 -  shows "xs |\<subset>| ys \<Longrightarrow> fcard xs < fcard ys"
  1.1841 -  unfolding fset_to_set_trans
  1.1842 -  by (rule psubset_card_mono[OF finite_fset])
  1.1843 -
  1.1844 -lemma fcard_funion_finter: 
  1.1845 -  shows "fcard xs + fcard ys = fcard (xs |\<union>| ys) + fcard (xs |\<inter>| ys)"
  1.1846 -  unfolding fset_to_set_trans
  1.1847 -  by (rule card_Un_Int[OF finite_fset finite_fset])
  1.1848 -
  1.1849 -lemma fcard_funion_disjoint: 
  1.1850 -  shows "xs |\<inter>| ys = {||} \<Longrightarrow> fcard (xs |\<union>| ys) = fcard xs + fcard ys"
  1.1851 -  unfolding fset_to_set_trans
  1.1852 -  by (rule card_Un_disjoint[OF finite_fset finite_fset])
  1.1853 -
  1.1854 -lemma fcard_delete1_less: 
  1.1855 -  shows "x |\<in>| xs \<Longrightarrow> fcard (fdelete x xs) < fcard xs"
  1.1856 -  unfolding fset_to_set_trans
  1.1857 -  by (rule card_Diff1_less[OF finite_fset])
  1.1858 -
  1.1859 -lemma fcard_delete2_less: 
  1.1860 -  shows "x |\<in>| xs \<Longrightarrow> y |\<in>| xs \<Longrightarrow> fcard (fdelete y (fdelete x xs)) < fcard xs"
  1.1861 -  unfolding fset_to_set_trans
  1.1862 -  by (rule card_Diff2_less[OF finite_fset])
  1.1863 -
  1.1864 -lemma fcard_delete1_le: 
  1.1865 -  shows "fcard (fdelete x xs) \<le> fcard xs"
  1.1866 -  unfolding fset_to_set_trans
  1.1867 -  by (rule card_Diff1_le[OF finite_fset])
  1.1868 -
  1.1869 -lemma fcard_psubset: 
  1.1870 -  shows "ys |\<subseteq>| xs \<Longrightarrow> fcard ys < fcard xs \<Longrightarrow> ys |\<subset>| xs"
  1.1871 -  unfolding fset_to_set_trans
  1.1872 -  by (rule card_psubset[OF finite_fset])
  1.1873 -
  1.1874 -lemma fcard_fmap_le: 
  1.1875 -  shows "fcard (fmap f xs) \<le> fcard xs"
  1.1876 -  unfolding fset_to_set_trans
  1.1877 -  by (rule card_image_le[OF finite_fset])
  1.1878 -
  1.1879 -lemma fin_fminus_fnotin: 
  1.1880 -  shows "x |\<in>| F - S \<Longrightarrow> x |\<notin>| S"
  1.1881 -  unfolding fset_to_set_trans
  1.1882 -  by blast
  1.1883 -
  1.1884 -lemma fin_fnotin_fminus: 
  1.1885 -  shows "x |\<in>| S \<Longrightarrow> x |\<notin>| F - S"
  1.1886 -  unfolding fset_to_set_trans
  1.1887 -  by blast
  1.1888 -
  1.1889 -lemma fin_mdef: 
  1.1890 -  "x |\<in>| F \<longleftrightarrow> x |\<notin>| (F - {|x|}) \<and> F = finsert x (F - {|x|})"
  1.1891 -  unfolding fset_to_set_trans
  1.1892 -  by blast
  1.1893 -
  1.1894 -lemma fcard_fminus_finsert[simp]:
  1.1895 -  assumes "a |\<in>| A" and "a |\<notin>| B"
  1.1896 -  shows "fcard(A - finsert a B) = fcard(A - B) - 1"
  1.1897 -  using assms 
  1.1898 -  unfolding fset_to_set_trans
  1.1899 -  by (rule card_Diff_insert[OF finite_fset])
  1.1900 -
  1.1901 -lemma fcard_fminus_fsubset:
  1.1902 -  assumes "B |\<subseteq>| A"
  1.1903 -  shows "fcard (A - B) = fcard A - fcard B"
  1.1904 -  using assms unfolding fset_to_set_trans
  1.1905 -  by (rule card_Diff_subset[OF finite_fset])
  1.1906 -
  1.1907 -lemma fcard_fminus_subset_finter:
  1.1908 -  shows "fcard (A - B) = fcard A - fcard (A |\<inter>| B)"
  1.1909 -  unfolding fset_to_set_trans
  1.1910 -  by (rule card_Diff_subset_Int) (fold finter_set, rule finite_fset)
  1.1911 -
  1.1912 -
  1.1913  ML {*
  1.1914  fun dest_fsetT (Type (@{type_name fset}, [T])) = T
  1.1915    | dest_fsetT T = raise TYPE ("dest_fsetT: fset type expected", [T], []);
  1.1916 @@ -1251,5 +1159,6 @@
  1.1917  
  1.1918  no_notation
  1.1919    list_eq (infix "\<approx>" 50)
  1.1920 +and list_eq2 (infix "\<approx>2" 50)
  1.1921  
  1.1922  end