FSet: definition changes propagated from Nominal and more use of 'descending' tactic
authorCezary Kaliszyk <kaliszyk@in.tum.de>
Fri Oct 15 21:50:26 2010 +0900 (2010-10-15)
changeset 39996c02078ff8691
parent 39995 849578dd6127
child 39998 b253319c9a95
FSet: definition changes propagated from Nominal and more use of 'descending' tactic
src/HOL/Quotient_Examples/FSet.thy
     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.117    by (simp add: memb_def)
   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.206    by (simp add: memb_def)
   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.684    by (simp add: fin_set)
   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.847    by (simp add: fminus_red)
   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