2468 by (simp only: finite_set fold1_eq_fold_idem) |
2468 by (simp only: finite_set fold1_eq_fold_idem) |
2469 with xs show ?thesis by (simp add: fold_set_fold mult_commute) |
2469 with xs show ?thesis by (simp add: fold_set_fold mult_commute) |
2470 qed |
2470 qed |
2471 qed |
2471 qed |
2472 |
2472 |
|
2473 lemma union_set_fold: |
|
2474 "set xs \<union> A = fold Set.insert xs A" |
|
2475 proof - |
|
2476 interpret comp_fun_idem Set.insert |
|
2477 by (fact comp_fun_idem_insert) |
|
2478 show ?thesis by (simp add: union_fold_insert fold_set_fold) |
|
2479 qed |
|
2480 |
|
2481 lemma minus_set_fold: |
|
2482 "A - set xs = fold Set.remove xs A" |
|
2483 proof - |
|
2484 interpret comp_fun_idem Set.remove |
|
2485 by (fact comp_fun_idem_remove) |
|
2486 show ?thesis |
|
2487 by (simp add: minus_fold_remove [of _ A] fold_set_fold) |
|
2488 qed |
|
2489 |
2473 lemma (in lattice) Inf_fin_set_fold: |
2490 lemma (in lattice) Inf_fin_set_fold: |
2474 "Inf_fin (set (x # xs)) = fold inf xs x" |
2491 "Inf_fin (set (x # xs)) = fold inf xs x" |
2475 proof - |
2492 proof - |
2476 interpret ab_semigroup_idem_mult "inf :: 'a \<Rightarrow> 'a \<Rightarrow> 'a" |
2493 interpret ab_semigroup_idem_mult "inf :: 'a \<Rightarrow> 'a \<Rightarrow> 'a" |
2477 by (fact ab_semigroup_idem_mult_inf) |
2494 by (fact ab_semigroup_idem_mult_inf) |
2585 text {* Executing operations in terms of @{const foldr} -- tail-recursive! *} |
2602 text {* Executing operations in terms of @{const foldr} -- tail-recursive! *} |
2586 |
2603 |
2587 lemma concat_conv_foldr [code]: |
2604 lemma concat_conv_foldr [code]: |
2588 "concat xss = foldr append xss []" |
2605 "concat xss = foldr append xss []" |
2589 by (simp add: fold_append_concat_rev foldr_def) |
2606 by (simp add: fold_append_concat_rev foldr_def) |
|
2607 |
|
2608 lemma union_set_foldr: |
|
2609 "set xs \<union> A = foldr Set.insert xs A" |
|
2610 proof - |
|
2611 have "\<And>x y :: 'a. insert y \<circ> insert x = insert x \<circ> insert y" |
|
2612 by auto |
|
2613 then show ?thesis by (simp add: union_set_fold foldr_fold) |
|
2614 qed |
|
2615 |
|
2616 lemma minus_set_foldr: |
|
2617 "A - set xs = foldr Set.remove xs A" |
|
2618 proof - |
|
2619 have "\<And>x y :: 'a. Set.remove y \<circ> Set.remove x = Set.remove x \<circ> Set.remove y" |
|
2620 by (auto simp add: remove_def) |
|
2621 then show ?thesis by (simp add: minus_set_fold foldr_fold) |
|
2622 qed |
2590 |
2623 |
2591 lemma (in lattice) Inf_fin_set_foldr [code]: |
2624 lemma (in lattice) Inf_fin_set_foldr [code]: |
2592 "Inf_fin (set (x # xs)) = foldr inf xs x" |
2625 "Inf_fin (set (x # xs)) = foldr inf xs x" |
2593 by (simp add: Inf_fin_set_fold ac_simps foldr_fold fun_eq_iff del: set.simps) |
2626 by (simp add: Inf_fin_set_fold ac_simps foldr_fold fun_eq_iff del: set.simps) |
2594 |
2627 |
5164 subsection {* Code generation *} |
5197 subsection {* Code generation *} |
5165 |
5198 |
5166 subsubsection {* Counterparts for set-related operations *} |
5199 subsubsection {* Counterparts for set-related operations *} |
5167 |
5200 |
5168 definition member :: "'a list \<Rightarrow> 'a \<Rightarrow> bool" where |
5201 definition member :: "'a list \<Rightarrow> 'a \<Rightarrow> bool" where |
5169 [code_abbrev]: "member xs x \<longleftrightarrow> x \<in> set xs" |
5202 "member xs x \<longleftrightarrow> x \<in> set xs" |
5170 |
5203 |
5171 text {* |
5204 text {* |
5172 Use @{text member} only for generating executable code. Otherwise use |
5205 Use @{text member} only for generating executable code. Otherwise use |
5173 @{prop "x \<in> set xs"} instead --- it is much easier to reason about. |
5206 @{prop "x \<in> set xs"} instead --- it is much easier to reason about. |
5174 *} |
5207 *} |
5180 |
5213 |
5181 lemma in_set_member (* FIXME delete candidate *): |
5214 lemma in_set_member (* FIXME delete candidate *): |
5182 "x \<in> set xs \<longleftrightarrow> member xs x" |
5215 "x \<in> set xs \<longleftrightarrow> member xs x" |
5183 by (simp add: member_def) |
5216 by (simp add: member_def) |
5184 |
5217 |
5185 declare INF_def [code_unfold] |
|
5186 declare SUP_def [code_unfold] |
|
5187 |
|
5188 declare set_map [symmetric, code_unfold] |
|
5189 |
|
5190 definition list_all :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool" where |
5218 definition list_all :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool" where |
5191 list_all_iff [code_abbrev]: "list_all P xs \<longleftrightarrow> Ball (set xs) P" |
5219 list_all_iff: "list_all P xs \<longleftrightarrow> Ball (set xs) P" |
5192 |
5220 |
5193 definition list_ex :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool" where |
5221 definition list_ex :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool" where |
5194 list_ex_iff [code_abbrev]: "list_ex P xs \<longleftrightarrow> Bex (set xs) P" |
5222 list_ex_iff: "list_ex P xs \<longleftrightarrow> Bex (set xs) P" |
5195 |
5223 |
5196 definition list_ex1 :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool" where |
5224 definition list_ex1 :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool" where |
5197 list_ex1_iff [code_abbrev]: "list_ex1 P xs \<longleftrightarrow> (\<exists>! x. x \<in> set xs \<and> P x)" |
5225 list_ex1_iff [code_abbrev]: "list_ex1 P xs \<longleftrightarrow> (\<exists>! x. x \<in> set xs \<and> P x)" |
5198 |
5226 |
5199 text {* |
5227 text {* |
5495 (Haskell "all") |
5523 (Haskell "all") |
5496 |
5524 |
5497 code_const list_ex |
5525 code_const list_ex |
5498 (Haskell "any") |
5526 (Haskell "any") |
5499 |
5527 |
|
5528 |
|
5529 subsubsection {* Implementation of sets by lists *} |
|
5530 |
|
5531 text {* Basic operations *} |
|
5532 |
|
5533 lemma is_empty_set [code]: |
|
5534 "Set.is_empty (set xs) \<longleftrightarrow> List.null xs" |
|
5535 by (simp add: Set.is_empty_def null_def) |
|
5536 |
|
5537 lemma empty_set [code]: |
|
5538 "{} = set []" |
|
5539 by simp |
|
5540 |
|
5541 lemma [code]: |
|
5542 "x \<in> set xs \<longleftrightarrow> List.member xs x" |
|
5543 "x \<in> List.coset xs \<longleftrightarrow> \<not> List.member xs x" |
|
5544 by (simp_all add: member_def) |
|
5545 |
|
5546 lemma UNIV_coset [code]: |
|
5547 "UNIV = List.coset []" |
|
5548 by simp |
|
5549 |
|
5550 lemma insert_code [code]: |
|
5551 "insert x (set xs) = set (List.insert x xs)" |
|
5552 "insert x (List.coset xs) = List.coset (removeAll x xs)" |
|
5553 by simp_all |
|
5554 |
|
5555 lemma remove_code [code]: |
|
5556 "Set.remove x (set xs) = set (removeAll x xs)" |
|
5557 "Set.remove x (List.coset xs) = List.coset (List.insert x xs)" |
|
5558 by (simp_all add: remove_def Compl_insert) |
|
5559 |
|
5560 lemma Ball_set [code]: |
|
5561 "Ball (set xs) P \<longleftrightarrow> list_all P xs" |
|
5562 by (simp add: list_all_iff) |
|
5563 |
|
5564 lemma Bex_set [code]: |
|
5565 "Bex (set xs) P \<longleftrightarrow> list_ex P xs" |
|
5566 by (simp add: list_ex_iff) |
|
5567 |
|
5568 lemma card_set [code]: |
|
5569 "card (set xs) = length (remdups xs)" |
|
5570 proof - |
|
5571 have "card (set (remdups xs)) = length (remdups xs)" |
|
5572 by (rule distinct_card) simp |
|
5573 then show ?thesis by simp |
|
5574 qed |
|
5575 |
|
5576 |
|
5577 text {* Operations on relations *} |
|
5578 |
|
5579 lemma product_code [code]: |
|
5580 "Product_Type.product (set xs) (set ys) = set [(x, y). x \<leftarrow> xs, y \<leftarrow> ys]" |
|
5581 by (auto simp add: Product_Type.product_def) |
|
5582 |
|
5583 lemma Id_on_set [code]: |
|
5584 "Id_on (set xs) = set [(x, x). x \<leftarrow> xs]" |
|
5585 by (auto simp add: Id_on_def) |
|
5586 |
|
5587 lemma trancl_set_ntrancl [code]: |
|
5588 "trancl (set xs) = ntrancl (card (set xs) - 1) (set xs)" |
|
5589 by (simp add: finite_trancl_ntranl) |
|
5590 |
|
5591 lemma set_rel_comp [code]: |
|
5592 "set xys O set yzs = set ([(fst xy, snd yz). xy \<leftarrow> xys, yz \<leftarrow> yzs, snd xy = fst yz])" |
|
5593 by (auto simp add: Bex_def) |
|
5594 |
|
5595 lemma wf_set [code]: |
|
5596 "wf (set xs) = acyclic (set xs)" |
|
5597 by (simp add: wf_iff_acyclic_if_finite) |
|
5598 |
5500 end |
5599 end |