# HG changeset patch # User haftmann # Date 1324738391 -3600 # Node ID 2b043ed911acc60b4d910ecf79a63002a610129b # Parent 204f34a99cebd20659f6278e39c385b040e628ea added setup for executable code diff -r 204f34a99ceb -r 2b043ed911ac src/HOL/Library/More_Set.thy --- a/src/HOL/Library/More_Set.thy Sat Dec 24 15:53:11 2011 +0100 +++ b/src/HOL/Library/More_Set.thy Sat Dec 24 15:53:11 2011 +0100 @@ -12,29 +12,35 @@ definition is_empty :: "'a set \ bool" where "is_empty A \ A = {}" +hide_const (open) is_empty + definition remove :: "'a \ 'a set \ 'a set" where "remove x A = A - {x}" +hide_const (open) remove + lemma comp_fun_idem_remove: - "comp_fun_idem remove" + "comp_fun_idem More_Set.remove" proof - - have rem: "remove = (\x A. A - {x})" by (simp add: fun_eq_iff remove_def) + have rem: "More_Set.remove = (\x A. A - {x})" by (simp add: fun_eq_iff remove_def) show ?thesis by (simp only: comp_fun_idem_remove rem) qed lemma minus_fold_remove: assumes "finite A" - shows "B - A = Finite_Set.fold remove B A" + shows "B - A = Finite_Set.fold More_Set.remove B A" proof - - have rem: "remove = (\x A. A - {x})" by (simp add: fun_eq_iff remove_def) + have rem: "More_Set.remove = (\x A. A - {x})" by (simp add: fun_eq_iff remove_def) show ?thesis by (simp only: rem assms minus_fold_remove) qed definition project :: "('a \ bool) \ 'a set \ 'a set" where "project P A = {a \ A. P a}" +hide_const (open) project + lemma bounded_Collect_code [code_unfold_post]: - "{x \ A. P x} = project P A" + "{x \ A. P x} = More_Set.project P A" by (simp add: project_def) definition product :: "'a set \ 'b set \ ('a \ 'b) set" where @@ -50,7 +56,7 @@ subsection {* Basic set operations *} lemma is_empty_set: - "is_empty (set xs) \ List.null xs" + "More_Set.is_empty (set xs) \ List.null xs" by (simp add: is_empty_def null_def) lemma empty_set: @@ -62,7 +68,7 @@ by auto lemma remove_set_compl: - "remove x (- set xs) = - set (List.insert x xs)" + "More_Set.remove x (- set xs) = - set (List.insert x xs)" by (auto simp add: remove_def List.insert_def) lemma image_set: @@ -70,7 +76,7 @@ by simp lemma project_set: - "project P (set xs) = set (filter P xs)" + "More_Set.project P (set xs) = set (filter P xs)" by (auto simp add: project_def) @@ -93,18 +99,18 @@ qed lemma minus_set: - "A - set xs = fold remove xs A" + "A - set xs = fold More_Set.remove xs A" proof - - interpret comp_fun_idem remove + interpret comp_fun_idem More_Set.remove by (fact comp_fun_idem_remove) show ?thesis by (simp add: minus_fold_remove [of _ A] fold_set) qed lemma minus_set_foldr: - "A - set xs = foldr remove xs A" + "A - set xs = foldr More_Set.remove xs A" proof - - have "\x y :: 'a. remove y \ remove x = remove x \ remove y" + have "\x y :: 'a. More_Set.remove y \ More_Set.remove x = More_Set.remove x \ More_Set.remove y" by (auto simp add: remove_def) then show ?thesis by (simp add: minus_set foldr_fold) qed @@ -129,7 +135,7 @@ by (fact eq_iff) lemma inter: - "A \ B = project (\x. x \ A) B" + "A \ B = More_Set.project (\x. x \ A) B" by (auto simp add: project_def) @@ -143,6 +149,9 @@ "Id_on (set xs) = set [(x, x). x \ xs]" by (auto simp add: Id_on_def) +lemma trancl_set_ntrancl: "trancl (set xs) = ntrancl (card (set xs) - 1) (set xs)" + by (simp add: finite_trancl_ntranl) + lemma set_rel_comp: "set xys O set yzs = set ([(fst xy, snd yz). xy \ xys, yz \ yzs, snd xy = fst yz])" by (auto simp add: Bex_def) @@ -151,4 +160,162 @@ "wf (set xs) = acyclic (set xs)" by (simp add: wf_iff_acyclic_if_finite) + +subsection {* Code generator setup *} + +definition coset :: "'a list \ 'a set" where + [simp]: "coset xs = - set xs" + +code_datatype set coset + + +subsection {* Basic operations *} + +lemma [code]: + "x \ set xs \ List.member xs x" + "x \ coset xs \ \ List.member xs x" + by (simp_all add: member_def) + +lemma [code_unfold]: + "A = {} \ More_Set.is_empty A" + by (simp add: is_empty_def) + +declare empty_set [code] + +declare is_empty_set [code] + +lemma UNIV_coset [code]: + "UNIV = coset []" + by simp + +lemma insert_code [code]: + "insert x (set xs) = set (List.insert x xs)" + "insert x (coset xs) = coset (removeAll x xs)" + by simp_all + +lemma remove_code [code]: + "More_Set.remove x (set xs) = set (removeAll x xs)" + "More_Set.remove x (coset xs) = coset (List.insert x xs)" + by (simp_all add: remove_def Compl_insert) + +declare image_set [code] + +declare project_set [code] + +lemma Ball_set [code]: + "Ball (set xs) P \ list_all P xs" + by (simp add: list_all_iff) + +lemma Bex_set [code]: + "Bex (set xs) P \ list_ex P xs" + by (simp add: list_ex_iff) + +lemma card_set [code]: + "card (set xs) = length (remdups xs)" +proof - + have "card (set (remdups xs)) = length (remdups xs)" + by (rule distinct_card) simp + then show ?thesis by simp +qed + + +subsection {* Derived operations *} + +instantiation set :: (equal) equal +begin + +definition + "HOL.equal A B \ A \ B \ B \ A" + +instance proof +qed (auto simp add: equal_set_def) + end + +declare subset_eq [code] + +declare subset [code] + + +subsection {* Functorial operations *} + +lemma inter_code [code]: + "A \ set xs = set (List.filter (\x. x \ A) xs)" + "A \ coset xs = foldr More_Set.remove xs A" + by (simp add: inter project_def) (simp add: Diff_eq [symmetric] minus_set_foldr) + +lemma subtract_code [code]: + "A - set xs = foldr More_Set.remove xs A" + "A - coset xs = set (List.filter (\x. x \ A) xs)" + by (auto simp add: minus_set_foldr) + +lemma union_code [code]: + "set xs \ A = foldr insert xs A" + "coset xs \ A = coset (List.filter (\x. x \ A) xs)" + by (auto simp add: union_set_foldr) + +definition Inf :: "'a::complete_lattice set \ 'a" where + [simp]: "Inf = Complete_Lattices.Inf" + +hide_const (open) Inf + +lemma [code_unfold_post]: + "Inf = More_Set.Inf" + by simp + +definition Sup :: "'a::complete_lattice set \ 'a" where + [simp]: "Sup = Complete_Lattices.Sup" + +hide_const (open) Sup + +lemma [code_unfold_post]: + "Sup = More_Set.Sup" + by simp + +lemma Inf_code [code]: + "More_Set.Inf (set xs) = foldr inf xs top" + "More_Set.Inf (coset []) = bot" + by (simp_all add: Inf_set_foldr) + +lemma Sup_sup [code]: + "More_Set.Sup (set xs) = foldr sup xs bot" + "More_Set.Sup (coset []) = top" + by (simp_all add: Sup_set_foldr) + +lemma INF_code [code]: + "INFI (set xs) f = foldr (inf \ f) xs top" + by (simp add: INF_def Inf_set_foldr image_set foldr_map del: set_map) + +lemma SUP_sup [code]: + "SUPR (set xs) f = foldr (sup \ f) xs bot" + by (simp add: SUP_def Sup_set_foldr image_set foldr_map del: set_map) + +hide_const (open) coset + + +subsection {* Operations on relations *} + +text {* Initially contributed by Tjark Weber. *} + +declare Domain_fst [code] + +declare Range_snd [code] + +declare trans_join [code] + +declare irrefl_distinct [code] + +declare trancl_set_ntrancl [code] + +declare acyclic_irrefl [code] + +declare product_code [code] + +declare Id_on_set [code] + +declare set_rel_comp [code] + +declare wf_set [code] + +end +