author Christian Urban Mon Oct 18 14:25:15 2010 +0100 (2010-10-18) changeset 40030 9f8dcf6ef563 parent 40029 57e7f651fc70 child 40031 2671cce4d25d
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
```     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.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
```