385 |
385 |
386 subsection \<open>Code setup for sets\<close> |
386 subsection \<open>Code setup for sets\<close> |
387 |
387 |
388 text \<open> |
388 text \<open> |
389 Implement @{term "CARD('a)"} via @{term card_UNIV} and provide |
389 Implement @{term "CARD('a)"} via @{term card_UNIV} and provide |
390 implementations for @{term "finite"}, @{term "card"}, @{term "op \<subseteq>"}, |
390 implementations for @{term "finite"}, @{term "card"}, @{term "(\<subseteq>)"}, |
391 and @{term "op ="}if the calling context already provides @{class finite_UNIV} |
391 and @{term "(=)"}if the calling context already provides @{class finite_UNIV} |
392 and @{class card_UNIV} instances. If we implemented the latter |
392 and @{class card_UNIV} instances. If we implemented the latter |
393 always via @{term card_UNIV}, we would require instances of essentially all |
393 always via @{term card_UNIV}, we would require instances of essentially all |
394 element types, i.e., a lot of instantiation proofs and -- at run time -- |
394 element types, i.e., a lot of instantiation proofs and -- at run time -- |
395 possibly slow dictionary constructions. |
395 possibly slow dictionary constructions. |
396 \<close> |
396 \<close> |
439 "card' (List.coset xs) = of_phantom (card_UNIV :: 'a card_UNIV) - length (remdups xs)" |
439 "card' (List.coset xs) = of_phantom (card_UNIV :: 'a card_UNIV) - length (remdups xs)" |
440 by(simp_all add: List.card_set card_Compl card_UNIV) |
440 by(simp_all add: List.card_set card_Compl card_UNIV) |
441 |
441 |
442 |
442 |
443 qualified definition subset' :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" |
443 qualified definition subset' :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" |
444 where [simp, code del, code_abbrev]: "subset' = op \<subseteq>" |
444 where [simp, code del, code_abbrev]: "subset' = (\<subseteq>)" |
445 |
445 |
446 lemma subset'_code [code]: |
446 lemma subset'_code [code]: |
447 "subset' A (List.coset ys) \<longleftrightarrow> (\<forall>y \<in> set ys. y \<notin> A)" |
447 "subset' A (List.coset ys) \<longleftrightarrow> (\<forall>y \<in> set ys. y \<notin> A)" |
448 "subset' (set ys) B \<longleftrightarrow> (\<forall>y \<in> set ys. y \<in> B)" |
448 "subset' (set ys) B \<longleftrightarrow> (\<forall>y \<in> set ys. y \<in> B)" |
449 "subset' (List.coset xs) (set ys) \<longleftrightarrow> (let n = CARD('a) in n > 0 \<and> card(set (xs @ ys)) = n)" |
449 "subset' (List.coset xs) (set ys) \<longleftrightarrow> (let n = CARD('a) in n > 0 \<and> card(set (xs @ ys)) = n)" |
450 by(auto simp add: Let_def card_gt_0_iff dest: card_eq_UNIV_imp_eq_UNIV intro: arg_cong[where f=card]) |
450 by(auto simp add: Let_def card_gt_0_iff dest: card_eq_UNIV_imp_eq_UNIV intro: arg_cong[where f=card]) |
451 (metis finite_compl finite_set rev_finite_subset) |
451 (metis finite_compl finite_set rev_finite_subset) |
452 |
452 |
453 qualified definition eq_set :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" |
453 qualified definition eq_set :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" |
454 where [simp, code del, code_abbrev]: "eq_set = op =" |
454 where [simp, code del, code_abbrev]: "eq_set = (=)" |
455 |
455 |
456 lemma eq_set_code [code]: |
456 lemma eq_set_code [code]: |
457 fixes ys |
457 fixes ys |
458 defines "rhs \<equiv> |
458 defines "rhs \<equiv> |
459 let n = CARD('a) |
459 let n = CARD('a) |