src/HOL/Quotient_Examples/FSet.thy
 changeset 39996 c02078ff8691 parent 39995 849578dd6127 child 40030 9f8dcf6ef563
```     1.1 --- a/src/HOL/Quotient_Examples/FSet.thy	Fri Oct 15 21:47:45 2010 +0900
1.2 +++ b/src/HOL/Quotient_Examples/FSet.thy	Fri Oct 15 21:50:26 2010 +0900
1.3 @@ -14,7 +14,7 @@
1.4  fun
1.5    list_eq :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" (infix "\<approx>" 50)
1.6  where
1.7 -  "list_eq xs ys = (\<forall>x. x \<in> set xs \<longleftrightarrow> x \<in> set ys)"
1.8 +  "list_eq xs ys = (set xs = set ys)"
1.9
1.10  lemma list_eq_equivp:
1.11    shows "equivp list_eq"
1.12 @@ -38,32 +38,25 @@
1.13  definition
1.14    sub_list :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"
1.15  where
1.16 -  "sub_list xs ys \<equiv> (\<forall>x. x \<in> set xs \<longrightarrow> x \<in> set ys)"
1.17 +  "sub_list xs ys \<equiv> set xs \<subseteq> set ys"
1.18
1.19 -fun
1.20 +definition
1.21    fcard_raw :: "'a list \<Rightarrow> nat"
1.22  where
1.23 -  fcard_raw_nil:  "fcard_raw [] = 0"
1.24 -| fcard_raw_cons: "fcard_raw (x # xs) = (if memb x xs then fcard_raw xs else Suc (fcard_raw xs))"
1.25 +  "fcard_raw xs = card (set xs)"
1.26
1.27  primrec
1.28    finter_raw :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
1.29  where
1.30 -  "finter_raw [] l = []"
1.31 -| "finter_raw (h # t) l =
1.32 -     (if memb h l then h # (finter_raw t l) else finter_raw t l)"
1.33 -
1.34 -primrec
1.35 -  delete_raw :: "'a list \<Rightarrow> 'a \<Rightarrow> 'a list"
1.36 -where
1.37 -  "delete_raw [] x = []"
1.38 -| "delete_raw (a # xs) x = (if (a = x) then delete_raw xs x else a # (delete_raw xs x))"
1.39 +  "finter_raw [] ys = []"
1.40 +| "finter_raw (x # xs) ys =
1.41 +    (if x \<in> set ys then x # (finter_raw xs ys) else finter_raw xs ys)"
1.42
1.43  primrec
1.44    fminus_raw :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
1.45  where
1.46 -  "fminus_raw l [] = l"
1.47 -| "fminus_raw l (h # t) = fminus_raw (delete_raw l h) t"
1.48 +  "fminus_raw ys [] = ys"
1.49 +| "fminus_raw ys (x # xs) = fminus_raw (removeAll x ys) xs"
1.50
1.51  definition
1.52    rsp_fold
1.53 @@ -76,7 +69,7 @@
1.54    "ffold_raw f z [] = z"
1.55  | "ffold_raw f z (a # xs) =
1.56       (if (rsp_fold f) then
1.57 -       if memb a xs then ffold_raw f z xs
1.58 +       if a \<in> set xs then ffold_raw f z xs
1.59         else f a (ffold_raw f z xs)
1.60       else z)"
1.61
1.62 @@ -98,12 +91,9 @@
1.63    shows "Quotient (list_all2 op \<approx>) (map abs_fset) (map rep_fset)"
1.64    by (fact list_quotient[OF Quotient_fset])
1.65
1.66 -lemma set_in_eq: "(\<forall>e. ((e \<in> xs) \<longleftrightarrow> (e \<in> ys))) \<equiv> xs = ys"
1.67 -  by (rule eq_reflection) auto
1.68 -
1.69  lemma map_rel_cong: "b \<approx> ba \<Longrightarrow> map f b \<approx> map f ba"
1.70    unfolding list_eq.simps
1.71 -  by (simp only: set_map set_in_eq)
1.72 +  by (simp only: set_map)
1.73
1.74  lemma quotient_compose_list[quot_thm]:
1.75    shows  "Quotient ((list_all2 op \<approx>) OOO (op \<approx>))
1.76 @@ -160,6 +150,16 @@
1.77    qed
1.78  qed
1.79
1.80 +
1.81 +lemma set_finter_raw[simp]:
1.82 +  "set (finter_raw xs ys) = set xs \<inter> set ys"
1.83 +  by (induct xs) (auto simp add: memb_def)
1.84 +
1.85 +lemma set_fminus_raw[simp]:
1.86 +  "set (fminus_raw xs ys) = (set xs - set ys)"
1.87 +  by (induct ys arbitrary: xs) (auto)
1.88 +
1.89 +
1.90  text {* Respectfullness *}
1.91
1.92  lemma append_rsp[quot_respect]:
1.93 @@ -194,6 +194,24 @@
1.94    shows "(op \<approx> ===> op \<approx> ===> op =) op \<approx> op \<approx>"
1.95    by auto
1.96
1.97 +lemma finter_raw_rsp[quot_respect]:
1.98 +  shows "(op \<approx> ===> op \<approx> ===> op \<approx>) finter_raw finter_raw"
1.99 +  by simp
1.100 +
1.101 +lemma removeAll_rsp[quot_respect]:
1.102 +  shows "(op = ===> op \<approx> ===> op \<approx>) removeAll removeAll"
1.103 +  by simp
1.104 +
1.105 +lemma fminus_raw_rsp[quot_respect]:
1.106 +  shows "(op \<approx> ===> op \<approx> ===> op \<approx>) fminus_raw fminus_raw"
1.107 +  by simp
1.108 +
1.109 +lemma fcard_raw_rsp[quot_respect]:
1.110 +  shows "(op \<approx> ===> op =) fcard_raw fcard_raw"
1.111 +  by (simp add: fcard_raw_def)
1.112 +
1.113 +
1.114 +
1.115  lemma not_memb_nil:
1.116    shows "\<not> memb x []"
1.118 @@ -202,85 +220,6 @@
1.119    shows "memb x (y # xs) = (x = y \<or> memb x xs)"
1.120    by (induct xs) (auto simp add: memb_def)
1.121
1.122 -lemma memb_finter_raw:
1.123 -  "memb x (finter_raw xs ys) \<longleftrightarrow> memb x xs \<and> memb x ys"
1.124 -  by (induct xs) (auto simp add: not_memb_nil memb_cons_iff)
1.125 -
1.126 -lemma [quot_respect]:
1.127 -  "(op \<approx> ===> op \<approx> ===> op \<approx>) finter_raw finter_raw"
1.128 -  by (simp add: memb_def[symmetric] memb_finter_raw)
1.129 -
1.130 -lemma memb_delete_raw:
1.131 -  "memb x (delete_raw xs y) = (memb x xs \<and> x \<noteq> y)"
1.132 -  by (induct xs arbitrary: x y) (auto simp add: memb_def)
1.133 -
1.134 -lemma [quot_respect]:
1.135 -  "(op \<approx> ===> op = ===> op \<approx>) delete_raw delete_raw"
1.136 -  by (simp add: memb_def[symmetric] memb_delete_raw)
1.137 -
1.138 -lemma fminus_raw_memb: "memb x (fminus_raw xs ys) = (memb x xs \<and> \<not> memb x ys)"
1.139 -  by (induct ys arbitrary: xs)
1.140 -     (simp_all add: not_memb_nil memb_delete_raw memb_cons_iff)
1.141 -
1.142 -lemma [quot_respect]:
1.143 -  "(op \<approx> ===> op \<approx> ===> op \<approx>) fminus_raw fminus_raw"
1.144 -  by (simp add: memb_def[symmetric] fminus_raw_memb)
1.145 -
1.146 -lemma fcard_raw_gt_0:
1.147 -  assumes a: "x \<in> set xs"
1.148 -  shows "0 < fcard_raw xs"
1.149 -  using a by (induct xs) (auto simp add: memb_def)
1.150 -
1.151 -lemma fcard_raw_delete_one:
1.152 -  shows "fcard_raw ([x \<leftarrow> xs. x \<noteq> y]) = (if memb y xs then fcard_raw xs - 1 else fcard_raw xs)"
1.153 -  by (induct xs) (auto dest: fcard_raw_gt_0 simp add: memb_def)
1.154 -
1.155 -lemma fcard_raw_rsp_aux:
1.156 -  assumes a: "xs \<approx> ys"
1.157 -  shows "fcard_raw xs = fcard_raw ys"
1.158 -  using a
1.159 -  proof (induct xs arbitrary: ys)
1.160 -    case Nil
1.161 -    show ?case using Nil.prems by simp
1.162 -  next
1.163 -    case (Cons a xs)
1.164 -    have a: "a # xs \<approx> ys" by fact
1.165 -    have b: "\<And>ys. xs \<approx> ys \<Longrightarrow> fcard_raw xs = fcard_raw ys" by fact
1.166 -    show ?case proof (cases "a \<in> set xs")
1.167 -      assume c: "a \<in> set xs"
1.168 -      have "\<forall>x. (x \<in> set xs) = (x \<in> set ys)"
1.169 -      proof (intro allI iffI)
1.170 -        fix x
1.171 -        assume "x \<in> set xs"
1.172 -        then show "x \<in> set ys" using a by auto
1.173 -      next
1.174 -        fix x
1.175 -        assume d: "x \<in> set ys"
1.176 -        have e: "(x \<in> set (a # xs)) = (x \<in> set ys)" using a by simp
1.177 -        show "x \<in> set xs" using c d e unfolding list_eq.simps by simp blast
1.178 -      qed
1.179 -      then show ?thesis using b c by (simp add: memb_def)
1.180 -    next
1.181 -      assume c: "a \<notin> set xs"
1.182 -      have d: "xs \<approx> [x\<leftarrow>ys . x \<noteq> a] \<Longrightarrow> fcard_raw xs = fcard_raw [x\<leftarrow>ys . x \<noteq> a]" using b by simp
1.183 -      have "Suc (fcard_raw xs) = fcard_raw ys"
1.184 -      proof (cases "a \<in> set ys")
1.185 -        assume e: "a \<in> set ys"
1.186 -        have f: "\<forall>x. (x \<in> set xs) = (x \<in> set ys \<and> x \<noteq> a)" using a c
1.187 -          by (auto simp add: fcard_raw_delete_one)
1.188 -        have "fcard_raw ys = Suc (fcard_raw ys - 1)" by (rule Suc_pred'[OF fcard_raw_gt_0]) (rule e)
1.189 -        then show ?thesis using d e f by (simp_all add: fcard_raw_delete_one memb_def)
1.190 -      next
1.191 -        case False then show ?thesis using a c d by auto
1.192 -      qed
1.193 -      then show ?thesis using a c d by (simp add: memb_def)
1.194 -  qed
1.195 -qed
1.196 -
1.197 -lemma fcard_raw_rsp[quot_respect]:
1.198 -  shows "(op \<approx> ===> op =) fcard_raw fcard_raw"
1.199 -  by (simp add: fcard_raw_rsp_aux)
1.200 -
1.201  lemma memb_absorb:
1.202    shows "memb x xs \<Longrightarrow> x # xs \<approx> xs"
1.203    by (induct xs) (auto simp add: memb_def)
1.204 @@ -289,53 +228,35 @@
1.205    "(\<forall>x. \<not> memb x xs) = (xs \<approx> [])"
1.207
1.208 -lemma not_memb_delete_raw_ident:
1.209 -  shows "\<not> memb x xs \<Longrightarrow> delete_raw xs x = xs"
1.210 -  by (induct xs) (auto simp add: memb_def)
1.211
1.212  lemma memb_commute_ffold_raw:
1.213 -  "rsp_fold f \<Longrightarrow> memb h b \<Longrightarrow> ffold_raw f z b = f h (ffold_raw f z (delete_raw b h))"
1.214 +  "rsp_fold f \<Longrightarrow> h \<in> set b \<Longrightarrow> ffold_raw f z b = f h (ffold_raw f z (removeAll h b))"
1.215    apply (induct b)
1.216 -  apply (simp_all add: not_memb_nil)
1.217 -  apply (auto)
1.218 -  apply (simp_all add: memb_delete_raw not_memb_delete_raw_ident rsp_fold_def  memb_cons_iff)
1.219 +  apply (auto simp add: rsp_fold_def)
1.220    done
1.221
1.222  lemma ffold_raw_rsp_pre:
1.223 -  "\<forall>e. memb e a = memb e b \<Longrightarrow> ffold_raw f z a = ffold_raw f z b"
1.224 +  "set a = set b \<Longrightarrow> ffold_raw f z a = ffold_raw f z b"
1.225    apply (induct a arbitrary: b)
1.226 -  apply (simp add: memb_absorb memb_def none_memb_nil)
1.227    apply (simp)
1.228 +  apply (simp (no_asm_use))
1.229    apply (rule conjI)
1.230    apply (rule_tac [!] impI)
1.231    apply (rule_tac [!] conjI)
1.232    apply (rule_tac [!] impI)
1.233 -  apply (subgoal_tac "\<forall>e. memb e a2 = memb e b")
1.234 -  apply (simp)
1.235 -  apply (simp add: memb_cons_iff memb_def)
1.236 -  apply (auto)[1]
1.237 -  apply (drule_tac x="e" in spec)
1.238 -  apply (blast)
1.239 -  apply (case_tac b)
1.240 -  apply (simp_all)
1.241 -  apply (subgoal_tac "ffold_raw f z b = f a1 (ffold_raw f z (delete_raw b a1))")
1.242 -  apply (simp only:)
1.243 -  apply (rule_tac f="f a1" in arg_cong)
1.244 -  apply (subgoal_tac "\<forall>e. memb e a2 = memb e (delete_raw b a1)")
1.245 -  apply (simp)
1.246 -  apply (simp add: memb_delete_raw)
1.247 -  apply (auto simp add: memb_cons_iff)[1]
1.248 -  apply (erule memb_commute_ffold_raw)
1.249 -  apply (drule_tac x="a1" in spec)
1.250 -  apply (simp add: memb_cons_iff)
1.251 -  apply (simp add: memb_cons_iff)
1.252 -  apply (case_tac b)
1.253 -  apply (simp_all)
1.254 -  done
1.255 +  apply (metis insert_absorb)
1.256 +  apply (metis List.insert_def List.set.simps(2) List.set_insert ffold_raw.simps(2))
1.257 +  apply (metis Diff_insert_absorb insertI1 memb_commute_ffold_raw set_removeAll)
1.258 +  apply(drule_tac x="removeAll a1 b" in meta_spec)
1.259 +  apply(auto)
1.260 +  apply(drule meta_mp)
1.261 +  apply(blast)
1.262 +  by (metis List.set.simps(2) emptyE ffold_raw.simps(2) in_listsp_conv_set listsp.simps mem_def)
1.263
1.264  lemma ffold_raw_rsp[quot_respect]:
1.265    shows "(op = ===> op = ===> op \<approx> ===> op =) ffold_raw ffold_raw"
1.266 -  by (simp add: memb_def[symmetric] ffold_raw_rsp_pre)
1.267 +  unfolding fun_rel_def
1.268 +  by(auto intro: ffold_raw_rsp_pre)
1.269
1.270  lemma concat_rsp_pre:
1.271    assumes a: "list_all2 op \<approx> x x'"
1.272 @@ -359,9 +280,11 @@
1.273    assume a: "list_all2 op \<approx> a ba"
1.274    assume b: "ba \<approx> bb"
1.275    assume c: "list_all2 op \<approx> bb b"
1.276 -  have "\<forall>x. (\<exists>xa\<in>set a. x \<in> set xa) = (\<exists>xa\<in>set b. x \<in> set xa)" proof
1.277 +  have "\<forall>x. (\<exists>xa\<in>set a. x \<in> set xa) = (\<exists>xa\<in>set b. x \<in> set xa)"
1.278 +  proof
1.279      fix x
1.280 -    show "(\<exists>xa\<in>set a. x \<in> set xa) = (\<exists>xa\<in>set b. x \<in> set xa)" proof
1.281 +    show "(\<exists>xa\<in>set a. x \<in> set xa) = (\<exists>xa\<in>set b. x \<in> set xa)"
1.282 +    proof
1.283        assume d: "\<exists>xa\<in>set a. x \<in> set xa"
1.284        show "\<exists>xa\<in>set b. x \<in> set xa" by (rule concat_rsp_pre[OF a b c d])
1.285      next
1.286 @@ -372,7 +295,7 @@
1.287        show "\<exists>xa\<in>set a. x \<in> set xa" by (rule concat_rsp_pre[OF c' b' a' e])
1.288      qed
1.289    qed
1.290 -  then show "concat a \<approx> concat b" by simp
1.291 +  then show "concat a \<approx> concat b" by auto
1.292  qed
1.293
1.294  lemma [quot_respect]:
1.295 @@ -384,9 +307,7 @@
1.296  lemma append_inter_distrib:
1.297    "x @ (finter_raw y z) \<approx> finter_raw (x @ y) (x @ z)"
1.298    apply (induct x)
1.299 -  apply (simp_all add: memb_def)
1.300 -  apply (simp add: memb_def[symmetric] memb_finter_raw)
1.301 -  apply (auto simp add: memb_def)
1.302 +  apply (auto)
1.303    done
1.304
1.305  instantiation fset :: (type) "{bounded_lattice_bot, distrib_lattice, minus}"
1.306 @@ -416,7 +337,7 @@
1.307    "xs < ys \<equiv> xs \<le> ys \<and> xs \<noteq> (ys::'a fset)"
1.308
1.309  abbreviation
1.310 -  f_subset :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> bool" (infix "|\<subset>|" 50)
1.311 +  fsubset :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> bool" (infix "|\<subset>|" 50)
1.312  where
1.313    "xs |\<subset>| ys \<equiv> xs < ys"
1.314
1.315 @@ -455,10 +376,10 @@
1.316    show "{||} |\<subseteq>| x" by (descending) (simp add: sub_list_def)
1.317    show "x |\<subseteq>| x |\<union>| y" by (descending) (simp add: sub_list_def)
1.318    show "y |\<subseteq>| x |\<union>| y" by (descending) (simp add: sub_list_def)
1.319 -  show "x |\<inter>| y |\<subseteq>| x"
1.320 -    by (descending) (simp add: sub_list_def memb_def[symmetric] memb_finter_raw)
1.321 +  show "x |\<inter>| y |\<subseteq>| x"
1.322 +    by (descending) (simp add: sub_list_def memb_def[symmetric])
1.323    show "x |\<inter>| y |\<subseteq>| y"
1.324 -    by (descending) (simp add: sub_list_def memb_def[symmetric] memb_finter_raw)
1.325 +    by (descending) (simp add: sub_list_def memb_def[symmetric])
1.326    show "x |\<union>| (y |\<inter>| z) = x |\<union>| y |\<inter>| (x |\<union>| z)"
1.327      by (descending) (rule append_inter_distrib)
1.328  next
1.329 @@ -484,7 +405,7 @@
1.330    assume a: "x |\<subseteq>| y"
1.331    assume b: "x |\<subseteq>| z"
1.332    show "x |\<subseteq>| y |\<inter>| z" using a b
1.333 -    by (descending) (simp add: sub_list_def memb_def[symmetric] memb_finter_raw)
1.334 +    by (descending) (simp add: sub_list_def memb_def[symmetric])
1.335  qed
1.336
1.337  end
1.338 @@ -525,11 +446,11 @@
1.339    map
1.340
1.341  quotient_definition
1.342 -  "fdelete :: 'a fset \<Rightarrow> 'a \<Rightarrow> 'a fset"
1.343 -  is "delete_raw"
1.344 +  "fdelete :: 'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
1.345 +  is removeAll
1.346
1.347  quotient_definition
1.348 -  "fset_to_set :: 'a fset \<Rightarrow> 'a set"
1.349 +  "fset :: 'a fset \<Rightarrow> 'a set"
1.350    is "set"
1.351
1.352  quotient_definition
1.353 @@ -557,7 +478,6 @@
1.354  lemma [quot_respect]:
1.355    shows "(op \<approx> ===> list_all2 op \<approx> OOO op \<approx> ===> list_all2 op \<approx> OOO op \<approx>) Cons Cons"
1.356    apply auto
1.357 -  apply (simp add: set_in_eq)
1.358    apply (rule_tac b="x # b" in pred_compI)
1.359    apply auto
1.360    apply (rule_tac b="x # ba" in pred_compI)
1.361 @@ -651,52 +571,22 @@
1.362
1.363  lemma singleton_list_eq:
1.364    shows "[x] \<approx> [y] \<longleftrightarrow> x = y"
1.365 -  by (simp add: id_simps) auto
1.366 +  by (simp)
1.367
1.368  lemma sub_list_cons:
1.369    "sub_list (x # xs) ys = (memb x ys \<and> sub_list xs ys)"
1.370    by (auto simp add: memb_def sub_list_def)
1.371
1.372 -lemma fminus_raw_red: "fminus_raw (x # xs) ys = (if memb x ys then fminus_raw xs ys else x # (fminus_raw xs ys))"
1.373 -  by (induct ys arbitrary: xs x)
1.374 -     (simp_all add: not_memb_nil memb_delete_raw memb_cons_iff)
1.375 +lemma fminus_raw_red:
1.376 +  "fminus_raw (x # xs) ys = (if x \<in> set ys then fminus_raw xs ys else x # (fminus_raw xs ys))"
1.377 +  by (induct ys arbitrary: xs x) (simp_all)
1.378
1.379  text {* Cardinality of finite sets *}
1.380
1.381  lemma fcard_raw_0:
1.382    shows "fcard_raw xs = 0 \<longleftrightarrow> xs \<approx> []"
1.383 -  by (induct xs) (auto simp add: memb_def)
1.384 -
1.385 -lemma fcard_raw_not_memb:
1.386 -  shows "\<not> memb x xs \<longleftrightarrow> fcard_raw (x # xs) = Suc (fcard_raw xs)"
1.387 -  by auto
1.388 -
1.389 -lemma fcard_raw_suc:
1.390 -  assumes a: "fcard_raw xs = Suc n"
1.391 -  shows "\<exists>x ys. \<not> (memb x ys) \<and> xs \<approx> (x # ys) \<and> fcard_raw ys = n"
1.392 -  using a
1.393 -  by (induct xs) (auto simp add: memb_def split: if_splits)
1.394 -
1.395 -lemma singleton_fcard_1:
1.396 -  shows "set xs = {x} \<Longrightarrow> fcard_raw xs = 1"
1.397 -  by (induct xs) (auto simp add: memb_def subset_insert)
1.398 -
1.399 -lemma fcard_raw_1:
1.400 -  shows "fcard_raw xs = 1 \<longleftrightarrow> (\<exists>x. xs \<approx> [x])"
1.401 -  apply (auto dest!: fcard_raw_suc)
1.402 -  apply (simp add: fcard_raw_0)
1.403 -  apply (rule_tac x="x" in exI)
1.404 -  apply simp
1.405 -  apply (subgoal_tac "set xs = {x}")
1.406 -  apply (drule singleton_fcard_1)
1.407 -  apply auto
1.408 -  done
1.409 -
1.410 -lemma fcard_raw_suc_memb:
1.411 -  assumes a: "fcard_raw A = Suc n"
1.412 -  shows "\<exists>a. memb a A"
1.413 -  using a
1.414 -  by (induct A) (auto simp add: memb_def)
1.415 +  unfolding fcard_raw_def
1.416 +  by (induct xs) (auto)
1.417
1.418  lemma memb_card_not_0:
1.419    assumes a: "memb a A"
1.420 @@ -752,21 +642,18 @@
1.421
1.422  section {* deletion *}
1.423
1.424 -lemma memb_delete_raw_ident:
1.425 -  shows "\<not> memb x (delete_raw xs x)"
1.426 +
1.427 +lemma fset_raw_removeAll_cases:
1.428 +  "xs = [] \<or> (\<exists>x. memb x xs \<and> xs \<approx> x # removeAll x xs)"
1.429    by (induct xs) (auto simp add: memb_def)
1.430
1.431 -lemma fset_raw_delete_raw_cases:
1.432 -  "xs = [] \<or> (\<exists>x. memb x xs \<and> xs \<approx> x # delete_raw xs x)"
1.433 -  by (induct xs) (auto simp add: memb_def)
1.434 -
1.435 -lemma fdelete_raw_filter:
1.436 -  "delete_raw xs y = [x \<leftarrow> xs. x \<noteq> y]"
1.437 +lemma fremoveAll_filter:
1.438 +  "removeAll y xs = [x \<leftarrow> xs. x \<noteq> y]"
1.439    by (induct xs) simp_all
1.440
1.441  lemma fcard_raw_delete:
1.442 -  "fcard_raw (delete_raw xs y) = (if memb y xs then fcard_raw xs - 1 else fcard_raw xs)"
1.443 -  by (simp add: fdelete_raw_filter fcard_raw_delete_one)
1.444 +  "fcard_raw (removeAll y xs) = (if memb y xs then fcard_raw xs - 1 else fcard_raw xs)"
1.445 +  by (auto simp add: fcard_raw_def memb_def)
1.446
1.447  lemma set_cong:
1.448    shows "(x \<approx> y) = (set x = set y)"
1.449 @@ -794,7 +681,7 @@
1.450    by (induct xs) (auto intro: list_eq2.intros)
1.451
1.452  lemma cons_delete_list_eq2:
1.453 -  shows "list_eq2 (a # (delete_raw A a)) (if memb a A then A else a # A)"
1.454 +  shows "list_eq2 (a # (removeAll a A)) (if memb a A then A else a # A)"
1.455    apply (induct A)
1.456    apply (simp add: memb_def list_eq2_refl)
1.457    apply (case_tac "memb a (aa # A)")
1.458 @@ -805,19 +692,15 @@
1.459    apply (auto simp add: memb_def)[2]
1.460    apply (metis list_eq2.intros(3) list_eq2.intros(4) list_eq2.intros(5) list_eq2.intros(6))
1.461    apply (metis list_eq2.intros(1) list_eq2.intros(5) list_eq2.intros(6))
1.462 -  apply (auto simp add: list_eq2_refl not_memb_delete_raw_ident)
1.463 +  apply (auto simp add: list_eq2_refl memb_def)
1.464    done
1.465
1.466  lemma memb_delete_list_eq2:
1.467    assumes a: "memb e r"
1.468 -  shows "list_eq2 (e # delete_raw r e) r"
1.469 +  shows "list_eq2 (e # removeAll e r) r"
1.470    using a cons_delete_list_eq2[of e r]
1.471    by simp
1.472
1.473 -lemma delete_raw_rsp:
1.474 -  "xs \<approx> ys \<Longrightarrow> delete_raw xs x \<approx> delete_raw ys x"
1.475 -  by (simp add: memb_def[symmetric] memb_delete_raw)
1.476 -
1.477  lemma list_eq2_equiv:
1.478    "(l \<approx> r) \<longleftrightarrow> (list_eq2 l r)"
1.479  proof
1.480 @@ -839,58 +722,27 @@
1.481        case (Suc m)
1.482        have b: "l \<approx> r" by fact
1.483        have d: "fcard_raw l = Suc m" by fact
1.484 -      then have "\<exists>a. memb a l" by (rule fcard_raw_suc_memb)
1.485 +      then have "\<exists>a. memb a l"
1.486 +	apply(simp add: fcard_raw_def memb_def)
1.487 +	apply(drule card_eq_SucD)
1.488 +	apply(blast)
1.489 +	done
1.490        then obtain a where e: "memb a l" by auto
1.491 -      then have e': "memb a r" using list_eq.simps[simplified memb_def[symmetric], of l r] b by auto
1.492 -      have f: "fcard_raw (delete_raw l a) = m" using fcard_raw_delete[of l a] e d by simp
1.493 -      have g: "delete_raw l a \<approx> delete_raw r a" using delete_raw_rsp[OF b] by simp
1.494 -      have "list_eq2 (delete_raw l a) (delete_raw r a)" by (rule Suc.hyps[OF f g])
1.495 -      then have h: "list_eq2 (a # delete_raw l a) (a # delete_raw r a)" by (rule list_eq2.intros(5))
1.496 -      have i: "list_eq2 l (a # delete_raw l a)"
1.497 +      then have e': "memb a r" using list_eq.simps[simplified memb_def[symmetric], of l r] b
1.498 +	unfolding memb_def by auto
1.499 +      have f: "fcard_raw (removeAll a l) = m" using fcard_raw_delete[of a l] e d by simp
1.500 +      have g: "removeAll a l \<approx> removeAll a r" using removeAll_rsp b by simp
1.501 +      have "list_eq2 (removeAll a l) (removeAll a r)" by (rule Suc.hyps[OF f g])
1.502 +      then have h: "list_eq2 (a # removeAll a l) (a # removeAll a r)" by (rule list_eq2.intros(5))
1.503 +      have i: "list_eq2 l (a # removeAll a l)"
1.504          by (rule list_eq2.intros(3)[OF memb_delete_list_eq2[OF e]])
1.505 -      have "list_eq2 l (a # delete_raw r a)" by (rule list_eq2.intros(6)[OF i h])
1.506 +      have "list_eq2 l (a # removeAll a r)" by (rule list_eq2.intros(6)[OF i h])
1.507        then show ?case using list_eq2.intros(6)[OF _ memb_delete_list_eq2[OF e']] by simp
1.508      qed
1.509      }
1.510    then show "l \<approx> r \<Longrightarrow> list_eq2 l r" by blast
1.511  qed
1.512
1.513 -text {* Set *}
1.514 -
1.515 -lemma sub_list_set: "sub_list xs ys = (set xs \<subseteq> set ys)"
1.516 -  unfolding sub_list_def by auto
1.517 -
1.518 -lemma sub_list_neq_set: "(sub_list xs ys \<and> \<not> list_eq xs ys) = (set xs \<subset> set ys)"
1.519 -  by (auto simp add: sub_list_set)
1.520 -
1.521 -lemma fcard_raw_set: "fcard_raw xs = card (set xs)"
1.522 -  by (induct xs) (auto simp add: insert_absorb memb_def card_insert_disjoint finite_set)
1.523 -
1.524 -lemma memb_set: "memb x xs = (x \<in> set xs)"
1.525 -  by (simp only: memb_def)
1.526 -
1.527 -lemma filter_set: "set (filter P xs) = P \<inter> (set xs)"
1.528 -  by (induct xs, simp)
1.529 -     (metis Int_insert_right_if0 Int_insert_right_if1 List.set.simps(2) filter.simps(2) mem_def)
1.530 -
1.531 -lemma delete_raw_set: "set (delete_raw xs x) = set xs - {x}"
1.532 -  by (induct xs) auto
1.533 -
1.534 -lemma inter_raw_set: "set (finter_raw xs ys) = set xs \<inter> set ys"
1.535 -  by (induct xs) (simp_all add: memb_def)
1.536 -
1.537 -lemma fminus_raw_set: "set (fminus_raw xs ys) = set xs - set ys"
1.538 -  by (induct ys arbitrary: xs)
1.539 -     (simp_all add: fminus_raw.simps delete_raw_set, blast)
1.540 -
1.541 -text {* Raw theorems of ffilter *}
1.542 -
1.543 -lemma sub_list_filter: "sub_list (filter P xs) (filter Q xs) = (\<forall> x. memb x xs \<longrightarrow> P x \<longrightarrow> Q x)"
1.544 -unfolding sub_list_def memb_def by auto
1.545 -
1.546 -lemma list_eq_filter: "list_eq (filter P xs) (filter Q xs) = (\<forall>x. memb x xs \<longrightarrow> P x = Q x)"
1.547 -unfolding memb_def by auto
1.548 -
1.549  text {* Lifted theorems *}
1.550
1.551  lemma not_fin_fnil: "x |\<notin>| {||}"
1.552 @@ -927,16 +779,15 @@
1.553    by (descending) (auto)
1.554
1.555
1.556 -text {* fset_to_set *}
1.557 +text {* fset *}
1.558
1.559 -lemma fset_to_set_simps [simp]:
1.560 -  fixes h::"'a"
1.561 -  shows "fset_to_set {||} = ({} :: 'a set)"
1.562 -  and "fset_to_set (finsert h t) = insert h (fset_to_set t)"
1.563 +lemma fset_simps[simp]:
1.564 +  "fset {||} = ({} :: 'a set)"
1.565 +  "fset (finsert (h :: 'a) t) = insert h (fset t)"
1.566    by (lifting set.simps)
1.567
1.568 -lemma in_fset_to_set:
1.569 -  "x \<in> fset_to_set S \<equiv> x |\<in>| S"
1.570 +lemma in_fset:
1.571 +  "x \<in> fset S \<equiv> x |\<in>| S"
1.572    by (lifting memb_def[symmetric])
1.573
1.574  lemma none_fin_fempty:
1.575 @@ -944,47 +795,62 @@
1.576    by (lifting none_memb_nil)
1.577
1.578  lemma fset_cong:
1.579 -  "S = T \<longleftrightarrow> fset_to_set S = fset_to_set T"
1.580 +  "S = T \<longleftrightarrow> fset S = fset T"
1.581    by (lifting set_cong)
1.582
1.583 +
1.584  text {* fcard *}
1.585
1.586 -lemma fcard_fempty [simp]:
1.587 -  shows "fcard {||} = 0"
1.588 -  by (descending) (simp)
1.589 -
1.590  lemma fcard_finsert_if [simp]:
1.591    shows "fcard (finsert x S) = (if x |\<in>| S then fcard S else Suc (fcard S))"
1.592 -  by (descending) (simp)
1.593 +  by (descending) (auto simp add: fcard_raw_def memb_def insert_absorb)
1.594
1.595 -lemma fcard_0:
1.596 -  "fcard S = 0 \<longleftrightarrow> S = {||}"
1.597 -  by (lifting fcard_raw_0)
1.598 +lemma fcard_0[simp]:
1.599 +  shows "fcard S = 0 \<longleftrightarrow> S = {||}"
1.600 +  by (descending) (simp add: fcard_raw_def)
1.601 +
1.602 +lemma fcard_fempty[simp]:
1.603 +  shows "fcard {||} = 0"
1.604 +  by (simp add: fcard_0)
1.605
1.606  lemma fcard_1:
1.607    shows "fcard S = 1 \<longleftrightarrow> (\<exists>x. S = {|x|})"
1.608 -  by (lifting fcard_raw_1)
1.609 +  by (descending) (auto simp add: fcard_raw_def card_Suc_eq)
1.610
1.611  lemma fcard_gt_0:
1.612 -  shows "x \<in> fset_to_set S \<Longrightarrow> 0 < fcard S"
1.613 -  by (lifting fcard_raw_gt_0)
1.614 -
1.615 +  shows "x \<in> fset S \<Longrightarrow> 0 < fcard S"
1.616 +  by (descending) (auto simp add: fcard_raw_def card_gt_0_iff)
1.617 +
1.618  lemma fcard_not_fin:
1.619    shows "(x |\<notin>| S) = (fcard (finsert x S) = Suc (fcard S))"
1.620 -  by (lifting fcard_raw_not_memb)
1.621 +  by (descending) (auto simp add: memb_def fcard_raw_def insert_absorb)
1.622
1.623  lemma fcard_suc: "fcard S = Suc n \<Longrightarrow> \<exists>x T. x |\<notin>| T \<and> S = finsert x T \<and> fcard T = n"
1.624 -  by (lifting fcard_raw_suc)
1.625 +  apply descending
1.626 +  apply(simp add: fcard_raw_def memb_def)
1.627 +  apply(drule card_eq_SucD)
1.628 +  apply(auto)
1.629 +  apply(rule_tac x="b" in exI)
1.630 +  apply(rule_tac x="removeAll b S" in exI)
1.631 +  apply(auto)
1.632 +  done
1.633
1.634  lemma fcard_delete:
1.635 -  "fcard (fdelete S y) = (if y |\<in>| S then fcard S - 1 else fcard S)"
1.636 +  "fcard (fdelete y S) = (if y |\<in>| S then fcard S - 1 else fcard S)"
1.637    by (lifting fcard_raw_delete)
1.638
1.639 -lemma fcard_suc_memb: "fcard A = Suc n \<Longrightarrow> \<exists>a. a |\<in>| A"
1.640 -  by (lifting fcard_raw_suc_memb)
1.641 +lemma fcard_suc_memb:
1.642 +  shows "fcard A = Suc n \<Longrightarrow> \<exists>a. a |\<in>| A"
1.643 +  apply(descending)
1.644 +  apply(simp add: fcard_raw_def memb_def)
1.645 +  apply(drule card_eq_SucD)
1.646 +  apply(auto)
1.647 +  done
1.648
1.649 -lemma fin_fcard_not_0: "a |\<in>| A \<Longrightarrow> fcard A \<noteq> 0"
1.650 -  by (lifting memb_card_not_0)
1.651 +lemma fin_fcard_not_0:
1.652 +  shows "a |\<in>| A \<Longrightarrow> fcard A \<noteq> 0"
1.653 +  by (descending) (auto simp add: fcard_raw_def memb_def)
1.654 +
1.655
1.656  text {* funion *}
1.657
1.658 @@ -1070,7 +936,7 @@
1.659    by (lifting map.simps)
1.660
1.661  lemma fmap_set_image:
1.662 -  "fset_to_set (fmap f S) = f ` (fset_to_set S)"
1.663 +  "fset (fmap f S) = f ` (fset S)"
1.664    by (induct S) simp_all
1.665
1.666  lemma inj_fmap_eq_iff:
1.667 @@ -1085,103 +951,107 @@
1.668    shows "x |\<in>| S |\<union>| T \<longleftrightarrow> x |\<in>| S \<or> x |\<in>| T"
1.669    by (lifting memb_append)
1.670
1.671 -text {* to_set *}
1.672 +
1.673 +section {* fset *}
1.674
1.675  lemma fin_set:
1.676 -  shows "x |\<in>| xs \<longleftrightarrow> x \<in> fset_to_set xs"
1.677 -  by (lifting memb_set)
1.678 +  shows "x |\<in>| xs \<longleftrightarrow> x \<in> fset xs"
1.679 +  by (lifting memb_def)
1.680
1.681  lemma fnotin_set:
1.682 -  shows "x |\<notin>| xs \<longleftrightarrow> x \<notin> fset_to_set xs"
1.683 +  shows "x |\<notin>| xs \<longleftrightarrow> x \<notin> fset xs"
1.685
1.686  lemma fcard_set:
1.687 -  shows "fcard xs = card (fset_to_set xs)"
1.688 -  by (lifting fcard_raw_set)
1.689 +  shows "fcard xs = card (fset xs)"
1.690 +  by (lifting fcard_raw_def)
1.691
1.692  lemma fsubseteq_set:
1.693 -  shows "xs |\<subseteq>| ys \<longleftrightarrow> fset_to_set xs \<subseteq> fset_to_set ys"
1.694 -  by (lifting sub_list_set)
1.695 +  shows "xs |\<subseteq>| ys \<longleftrightarrow> fset xs \<subseteq> fset ys"
1.696 +  by (lifting sub_list_def)
1.697
1.698  lemma fsubset_set:
1.699 -  shows "xs |\<subset>| ys \<longleftrightarrow> fset_to_set xs \<subset> fset_to_set ys"
1.700 -  unfolding less_fset_def by (lifting sub_list_neq_set)
1.701 +  shows "xs |\<subset>| ys \<longleftrightarrow> fset xs \<subset> fset ys"
1.702 +  unfolding less_fset_def
1.703 +  by (descending) (auto simp add: sub_list_def)
1.704
1.705 -lemma ffilter_set:
1.706 -  shows "fset_to_set (ffilter P xs) = P \<inter> fset_to_set xs"
1.707 -  by (lifting filter_set)
1.708 +lemma ffilter_set [simp]:
1.709 +  shows "fset (ffilter P xs) = P \<inter> fset xs"
1.710 +  by (descending) (auto simp add: mem_def)
1.711
1.712 -lemma fdelete_set:
1.713 -  shows "fset_to_set (fdelete xs x) = fset_to_set xs - {x}"
1.714 -  by (lifting delete_raw_set)
1.715 +lemma fdelete_set [simp]:
1.716 +  shows "fset (fdelete x xs) = fset xs - {x}"
1.717 +  by (lifting set_removeAll)
1.718
1.719 -lemma finter_set:
1.720 -  shows "fset_to_set (xs |\<inter>| ys) = fset_to_set xs \<inter> fset_to_set ys"
1.721 -  by (lifting inter_raw_set)
1.722 +lemma finter_set [simp]:
1.723 +  shows "fset (xs |\<inter>| ys) = fset xs \<inter> fset ys"
1.724 +  by (lifting set_finter_raw)
1.725
1.726 -lemma funion_set:
1.727 -  shows "fset_to_set (xs |\<union>| ys) = fset_to_set xs \<union> fset_to_set ys"
1.728 +lemma funion_set [simp]:
1.729 +  shows "fset (xs |\<union>| ys) = fset xs \<union> fset ys"
1.730    by (lifting set_append)
1.731
1.732 -lemma fminus_set:
1.733 -  shows "fset_to_set (xs - ys) = fset_to_set xs - fset_to_set ys"
1.734 -  by (lifting fminus_raw_set)
1.735 +lemma fminus_set [simp]:
1.736 +  shows "fset (xs - ys) = fset xs - fset ys"
1.737 +  by (lifting set_fminus_raw)
1.738
1.739  lemmas fset_to_set_trans =
1.740    fin_set fnotin_set fcard_set fsubseteq_set fsubset_set
1.741 -  finter_set funion_set ffilter_set fset_to_set_simps
1.742 +  finter_set funion_set ffilter_set fset_simps
1.743    fset_cong fdelete_set fmap_set_image fminus_set
1.744
1.745
1.746  text {* ffold *}
1.747
1.748 -lemma ffold_nil: "ffold f z {||} = z"
1.749 +lemma ffold_nil:
1.750 +  shows "ffold f z {||} = z"
1.751    by (lifting ffold_raw.simps(1)[where 'a="'b" and 'b="'a"])
1.752
1.753  lemma ffold_finsert: "ffold f z (finsert a A) =
1.754    (if rsp_fold f then if a |\<in>| A then ffold f z A else f a (ffold f z A) else z)"
1.755 -  by (lifting ffold_raw.simps(2)[where 'a="'b" and 'b="'a"])
1.756 +  by (descending) (simp add: memb_def)
1.757
1.758  lemma fin_commute_ffold:
1.759 -  "\<lbrakk>rsp_fold f; h |\<in>| b\<rbrakk> \<Longrightarrow> ffold f z b = f h (ffold f z (fdelete b h))"
1.760 -  by (lifting memb_commute_ffold_raw)
1.761 +  "\<lbrakk>rsp_fold f; h |\<in>| b\<rbrakk> \<Longrightarrow> ffold f z b = f h (ffold f z (fdelete h b))"
1.762 +  by (descending) (simp add: memb_def memb_commute_ffold_raw)
1.763 +
1.764
1.765  text {* fdelete *}
1.766
1.767  lemma fin_fdelete:
1.768 -  shows "x |\<in>| fdelete S y \<longleftrightarrow> x |\<in>| S \<and> x \<noteq> y"
1.769 -  by (lifting memb_delete_raw)
1.770 +  shows "x |\<in>| fdelete y S \<longleftrightarrow> x |\<in>| S \<and> x \<noteq> y"
1.771 +  by (descending) (simp add: memb_def)
1.772
1.773 -lemma fin_fdelete_ident:
1.774 -  shows "x |\<notin>| fdelete S x"
1.775 -  by (lifting memb_delete_raw_ident)
1.776 +lemma fnotin_fdelete:
1.777 +  shows "x |\<notin>| fdelete x S"
1.778 +  by (descending) (simp add: memb_def)
1.779
1.780 -lemma not_memb_fdelete_ident:
1.781 -  shows "x |\<notin>| S \<Longrightarrow> fdelete S x = S"
1.782 -  by (lifting not_memb_delete_raw_ident)
1.783 +lemma fnotin_fdelete_ident:
1.784 +  shows "x |\<notin>| S \<Longrightarrow> fdelete x S = S"
1.785 +  by (descending) (simp add: memb_def)
1.786
1.787  lemma fset_fdelete_cases:
1.788 -  shows "S = {||} \<or> (\<exists>x. x |\<in>| S \<and> S = finsert x (fdelete S x))"
1.789 -  by (lifting fset_raw_delete_raw_cases)
1.790 +  shows "S = {||} \<or> (\<exists>x. x |\<in>| S \<and> S = finsert x (fdelete x S))"
1.791 +  by (lifting fset_raw_removeAll_cases)
1.792
1.793  text {* finite intersection *}
1.794
1.795 -lemma finter_empty_l:
1.796 +lemma finter_empty_l:
1.797    shows "{||} |\<inter>| S = {||}"
1.798    by simp
1.799
1.800
1.801 -lemma finter_empty_r:
1.802 +lemma finter_empty_r:
1.803    shows "S |\<inter>| {||} = {||}"
1.804    by simp
1.805
1.806  lemma finter_finsert:
1.807 -  "finsert x S |\<inter>| T = (if x |\<in>| T then finsert x (S |\<inter>| T) else S |\<inter>| T)"
1.808 -  by (lifting finter_raw.simps(2))
1.809 +  shows "finsert x S |\<inter>| T = (if x |\<in>| T then finsert x (S |\<inter>| T) else S |\<inter>| T)"
1.810 +  by (descending) (simp add: memb_def)
1.811
1.812  lemma fin_finter:
1.813 -  "x |\<in>| (S |\<inter>| T) \<longleftrightarrow> x |\<in>| S \<and> x |\<in>| T"
1.814 -  by (lifting memb_finter_raw)
1.815 +  shows "x |\<in>| (S |\<inter>| T) \<longleftrightarrow> x |\<in>| S \<and> x |\<in>| T"
1.816 +  by (descending) (simp add: memb_def)
1.817
1.818  lemma fsubset_finsert:
1.819    shows "finsert x xs |\<subseteq>| ys \<longleftrightarrow> x |\<in>| ys \<and> xs |\<subseteq>| ys"
1.820 @@ -1189,20 +1059,19 @@
1.821
1.822  lemma
1.823    shows "xs |\<subseteq>| ys \<equiv> \<forall>x. x |\<in>| xs \<longrightarrow> x |\<in>| ys"
1.824 -  by (lifting sub_list_def[simplified memb_def[symmetric]])
1.825 +  by (descending) (auto simp add: sub_list_def memb_def)
1.826
1.827  lemma fsubset_fin:
1.828    shows "xs |\<subseteq>| ys = (\<forall>x. x |\<in>| xs \<longrightarrow> x |\<in>| ys)"
1.829 -by (rule meta_eq_to_obj_eq)
1.830 -   (lifting sub_list_def[simplified memb_def[symmetric]])
1.831 +  by (descending) (auto simp add: sub_list_def memb_def)
1.832
1.833  lemma fminus_fin:
1.834    shows "x |\<in>| xs - ys \<longleftrightarrow> x |\<in>| xs \<and> x |\<notin>| ys"
1.835 -  by (lifting fminus_raw_memb)
1.836 +  by (descending) (simp add: memb_def)
1.837
1.838  lemma fminus_red:
1.839    shows "finsert x xs - ys = (if x |\<in>| ys then xs - ys else finsert x (xs - ys))"
1.840 -  by (lifting fminus_raw_red)
1.841 +  by (descending) (auto simp add: memb_def)
1.842
1.843  lemma fminus_red_fin [simp]:
1.844    shows "x |\<in>| ys \<Longrightarrow> finsert x xs - ys = xs - ys"
1.845 @@ -1212,7 +1081,7 @@
1.846    shows "x |\<notin>| ys \<Longrightarrow> finsert x xs - ys = finsert x (xs - ys)"
1.848
1.849 -lemma expand_fset_eq:
1.850 +lemma fset_eq_iff:
1.851    shows "S = T \<longleftrightarrow> (\<forall>x. (x |\<in>| S) = (x |\<in>| T))"
1.852    by (descending) (auto simp add: memb_def)
1.853
1.854 @@ -1275,7 +1144,7 @@
1.855
1.856  text {* finiteness for finite sets holds *}
1.857  lemma finite_fset [simp]:
1.858 -  shows "finite (fset_to_set S)"
1.859 +  shows "finite (fset S)"
1.860    by (induct S) auto
1.861
1.862  lemma fset_choice:
1.863 @@ -1283,16 +1152,14 @@
1.864    unfolding fset_to_set_trans
1.865    by (rule finite_set_choice[simplified Ball_def, OF finite_fset])
1.866
1.867 -lemma fsubseteq_fnil:
1.868 +lemma fsubseteq_fempty:
1.869    shows "xs |\<subseteq>| {||} \<longleftrightarrow> xs = {||}"
1.870 -  unfolding fset_to_set_trans
1.871 -  by (rule subset_empty)
1.872 +  by (metis finter_empty_r le_iff_inf)
1.873
1.874  lemma not_fsubset_fnil:
1.875    shows "\<not> xs |\<subset>| {||}"
1.876 -  unfolding fset_to_set_trans
1.877 -  by (rule not_psubset_empty)
1.878 -
1.879 +  by (metis fset_simps(1) fsubset_set not_psubset_empty)
1.880 +
1.881  lemma fcard_mono:
1.882    shows "xs |\<subseteq>| ys \<Longrightarrow> fcard xs \<le> fcard ys"
1.883    unfolding fset_to_set_trans
1.884 @@ -1300,8 +1167,8 @@
1.885
1.886  lemma fcard_fseteq:
1.887    shows "xs |\<subseteq>| ys \<Longrightarrow> fcard ys \<le> fcard xs \<Longrightarrow> xs = ys"
1.888 -  unfolding fset_to_set_trans
1.889 -  by (rule card_seteq[OF finite_fset])
1.890 +  unfolding fcard_set fsubseteq_set
1.891 +  by (simp add: card_seteq[OF finite_fset] fset_cong)
1.892
1.893  lemma psubset_fcard_mono:
1.894    shows "xs |\<subset>| ys \<Longrightarrow> fcard xs < fcard ys"
1.895 @@ -1319,17 +1186,17 @@
1.896    by (rule card_Un_disjoint[OF finite_fset finite_fset])
1.897
1.898  lemma fcard_delete1_less:
1.899 -  shows "x |\<in>| xs \<Longrightarrow> fcard (fdelete xs x) < fcard xs"
1.900 +  shows "x |\<in>| xs \<Longrightarrow> fcard (fdelete x xs) < fcard xs"
1.901    unfolding fset_to_set_trans
1.902    by (rule card_Diff1_less[OF finite_fset])
1.903
1.904  lemma fcard_delete2_less:
1.905 -  shows "x |\<in>| xs \<Longrightarrow> y |\<in>| xs \<Longrightarrow> fcard (fdelete (fdelete xs x) y) < fcard xs"
1.906 +  shows "x |\<in>| xs \<Longrightarrow> y |\<in>| xs \<Longrightarrow> fcard (fdelete y (fdelete x xs)) < fcard xs"
1.907    unfolding fset_to_set_trans
1.908    by (rule card_Diff2_less[OF finite_fset])
1.909
1.910  lemma fcard_delete1_le:
1.911 -  shows "fcard (fdelete xs x) \<le> fcard xs"
1.912 +  shows "fcard (fdelete x xs) \<le> fcard xs"
1.913    unfolding fset_to_set_trans
1.914    by (rule card_Diff1_le[OF finite_fset])
1.915
1.916 @@ -1353,14 +1220,16 @@
1.917    unfolding fset_to_set_trans
1.918    by blast
1.919
1.920 -lemma fin_mdef: "x |\<in>| F \<longleftrightarrow> x |\<notin>| (F - {|x|}) \<and> F = finsert x (F - {|x|})"
1.921 +lemma fin_mdef:
1.922 +  "x |\<in>| F \<longleftrightarrow> x |\<notin>| (F - {|x|}) \<and> F = finsert x (F - {|x|})"
1.923    unfolding fset_to_set_trans
1.924    by blast
1.925
1.926  lemma fcard_fminus_finsert[simp]:
1.927    assumes "a |\<in>| A" and "a |\<notin>| B"
1.928    shows "fcard(A - finsert a B) = fcard(A - B) - 1"
1.929 -  using assms unfolding fset_to_set_trans
1.930 +  using assms
1.931 +  unfolding fset_to_set_trans
1.932    by (rule card_Diff_insert[OF finite_fset])
1.933
1.934  lemma fcard_fminus_fsubset:
1.935 @@ -1370,7 +1239,7 @@
1.936    by (rule card_Diff_subset[OF finite_fset])
1.937
1.938  lemma fcard_fminus_subset_finter:
1.939 -  "fcard (A - B) = fcard A - fcard (A |\<inter>| B)"
1.940 +  shows "fcard (A - B) = fcard A - fcard (A |\<inter>| B)"
1.941    unfolding fset_to_set_trans
1.942    by (rule card_Diff_subset_Int) (fold finter_set, rule finite_fset)
1.943
```