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