# HG changeset patch # User bulwahn # Date 1311673691 -7200 # Node ID 0e530fe0d33e0730d643f5de52874c2a214b7fc7 # Parent 30f4d346b204c233f726dd9e6f161a3d83423b56# Parent 24a3ddc79a5c76fe5e5f69abc5ea8c57a5472aac merged diff -r 30f4d346b204 -r 0e530fe0d33e src/HOL/Library/Cset.thy --- a/src/HOL/Library/Cset.thy Tue Jul 26 08:07:01 2011 +0200 +++ b/src/HOL/Library/Cset.thy Tue Jul 26 11:48:11 2011 +0200 @@ -86,6 +86,12 @@ subsection {* Basic operations *} +abbreviation empty :: "'a Cset.set" where "empty \ bot" +hide_const (open) empty + +abbreviation UNIV :: "'a Cset.set" where "UNIV \ top" +hide_const (open) UNIV + definition is_empty :: "'a Cset.set \ bool" where [simp]: "is_empty A \ More_Set.is_empty (member A)" @@ -124,9 +130,42 @@ end +subsection {* More operations *} + +text {* conversion from @{typ "'a list"} *} + +definition set :: "'a list \ 'a Cset.set" where + "set xs = Set (List.set xs)" +hide_const (open) set + +text {* conversion from @{typ "'a Predicate.pred"} *} + +definition pred_of_cset :: "'a Cset.set \ 'a Predicate.pred" +where [code del]: "pred_of_cset = Predicate.Pred \ Cset.member" + +definition of_pred :: "'a Predicate.pred \ 'a Cset.set" +where "of_pred = Cset.Set \ Predicate.eval" + +definition of_seq :: "'a Predicate.seq \ 'a Cset.set" +where "of_seq = of_pred \ Predicate.pred_of_seq" + +text {* monad operations *} + +definition single :: "'a \ 'a Cset.set" where + "single a = Set {a}" + +definition bind :: "'a Cset.set \ ('a \ 'b Cset.set) \ 'b Cset.set" + (infixl "\=" 70) + where "A \= f = Set (\x \ member A. member (f x))" subsection {* Simplified simprules *} +lemma empty_simp [simp]: "member Cset.empty = {}" + by(simp) + +lemma UNIV_simp [simp]: "member Cset.UNIV = UNIV" + by simp + lemma is_empty_simp [simp]: "is_empty A \ member A = {}" by (simp add: More_Set.is_empty_def) @@ -142,10 +181,103 @@ by (simp add: More_Set.project_def) declare filter_def [simp del] +lemma member_set [simp]: + "member (Cset.set xs) = set xs" + by (simp add: set_def) +hide_fact (open) member_set set_def + +lemma set_simps [simp]: + "Cset.set [] = Cset.empty" + "Cset.set (x # xs) = insert x (Cset.set xs)" +by(simp_all add: Cset.set_def) + +lemma member_SUPR [simp]: + "member (SUPR A f) = SUPR A (member \ f)" +unfolding SUPR_def by simp + +lemma member_bind [simp]: + "member (P \= f) = member (SUPR (member P) f)" +by (simp add: bind_def Cset.set_eq_iff) + +lemma member_single [simp]: + "member (single a) = {a}" +by(simp add: single_def) + +lemma single_sup_simps [simp]: + shows single_sup: "sup (single a) A = insert a A" + and sup_single: "sup A (single a) = insert a A" +by(auto simp add: Cset.set_eq_iff) + +lemma single_bind [simp]: + "single a \= B = B a" +by(simp add: bind_def single_def) + +lemma bind_bind: + "(A \= B) \= C = A \= (\x. B x \= C)" +by(simp add: bind_def) + +lemma bind_single [simp]: + "A \= single = A" +by(simp add: bind_def single_def) + +lemma bind_const: "A \= (\_. B) = (if Cset.is_empty A then Cset.empty else B)" +by(auto simp add: Cset.set_eq_iff) + +lemma empty_bind [simp]: + "Cset.empty \= f = Cset.empty" +by(simp add: Cset.set_eq_iff) + +lemma member_of_pred [simp]: + "member (of_pred P) = {x. Predicate.eval P x}" +by(simp add: of_pred_def Collect_def) + +lemma member_of_seq [simp]: + "member (of_seq xq) = {x. Predicate.member xq x}" +by(simp add: of_seq_def eval_member) + +lemma eval_pred_of_cset [simp]: + "Predicate.eval (pred_of_cset A) = Cset.member A" +by(simp add: pred_of_cset_def) + +subsection {* Default implementations *} + +lemma set_code [code]: + "Cset.set = foldl (\A x. insert x A) Cset.empty" +proof(rule ext, rule Cset.set_eqI) + fix xs + show "member (Cset.set xs) = member (foldl (\A x. insert x A) Cset.empty xs)" + by(induct xs rule: rev_induct)(simp_all) +qed + +lemma single_code [code]: + "single a = insert a Cset.empty" +by(simp add: Cset.single_def) + +lemma of_pred_code [code]: + "of_pred (Predicate.Seq f) = (case f () of + Predicate.Empty \ Cset.empty + | Predicate.Insert x P \ Cset.insert x (of_pred P) + | Predicate.Join P xq \ sup (of_pred P) (of_seq xq))" +by(auto split: seq.split + simp add: Predicate.Seq_def of_pred_def eval_member Cset.set_eq_iff) + +lemma of_seq_code [code]: + "of_seq Predicate.Empty = Cset.empty" + "of_seq (Predicate.Insert x P) = Cset.insert x (of_pred P)" + "of_seq (Predicate.Join P xq) = sup (of_pred P) (of_seq xq)" +by(auto simp add: of_seq_def of_pred_def Cset.set_eq_iff) + declare mem_def [simp del] +no_notation bind (infixl "\=" 70) hide_const (open) is_empty insert remove map filter forall exists card - Inter Union + Inter Union bind single of_pred of_seq + +hide_fact (open) set_def pred_of_cset_def of_pred_def of_seq_def single_def + bind_def empty_simp UNIV_simp member_set set_simps member_SUPR member_bind + member_single single_sup_simps single_sup sup_single single_bind + bind_bind bind_single bind_const empty_bind member_of_pred member_of_seq + eval_pred_of_cset set_code single_code of_pred_code of_seq_code end diff -r 30f4d346b204 -r 0e530fe0d33e src/HOL/Library/Dlist_Cset.thy --- a/src/HOL/Library/Dlist_Cset.thy Tue Jul 26 08:07:01 2011 +0200 +++ b/src/HOL/Library/Dlist_Cset.thy Tue Jul 26 11:48:11 2011 +0200 @@ -7,7 +7,7 @@ begin definition Set :: "'a dlist \ 'a Cset.set" where - "Set dxs = List_Cset.set (list_of_dlist dxs)" + "Set dxs = Cset.set (list_of_dlist dxs)" definition Coset :: "'a dlist \ 'a Cset.set" where "Coset dxs = List_Cset.coset (list_of_dlist dxs)" @@ -27,6 +27,9 @@ declare forall_set [code del] declare exists_set [code del] declare card_set [code del] +declare List_Cset.single_set [code del] +declare List_Cset.bind_set [code del] +declare List_Cset.pred_of_cset_set [code del] declare inter_project [code del] declare subtract_remove [code del] declare union_insert [code del] @@ -50,7 +53,7 @@ by (simp add: Coset_def member_set not_set_compl) lemma Set_dlist_of_list [code]: - "List_Cset.set xs = Set (dlist_of_list xs)" + "Cset.set xs = Set (dlist_of_list xs)" by (rule Cset.set_eqI) simp lemma Coset_dlist_of_list [code]: @@ -137,4 +140,16 @@ end +declare Cset.single_code[code] + +lemma bind_set [code]: + "Cset.bind (Dlist_Cset.Set xs) f = foldl (\A x. sup A (f x)) Cset.empty (list_of_dlist xs)" +by(simp add: List_Cset.bind_set Dlist_Cset.Set_def) +hide_fact (open) bind_set + +lemma pred_of_cset_set [code]: + "pred_of_cset (Dlist_Cset.Set xs) = foldr sup (map Predicate.single (list_of_dlist xs)) bot" +by(simp add: List_Cset.pred_of_cset_set Dlist_Cset.Set_def) +hide_fact (open) pred_of_cset_set + end diff -r 30f4d346b204 -r 0e530fe0d33e src/HOL/Library/List_Cset.thy --- a/src/HOL/Library/List_Cset.thy Tue Jul 26 08:07:01 2011 +0200 +++ b/src/HOL/Library/List_Cset.thy Tue Jul 26 11:48:11 2011 +0200 @@ -8,15 +8,7 @@ begin declare mem_def [simp] - -definition set :: "'a list \ 'a Cset.set" where - "set xs = Set (List.set xs)" -hide_const (open) set - -lemma member_set [simp]: - "member (List_Cset.set xs) = set xs" - by (simp add: set_def) -hide_fact (open) member_set +declare Cset.set_code [code del] definition coset :: "'a list \ 'a Cset.set" where "coset xs = Set (- set xs)" @@ -27,10 +19,10 @@ by (simp add: coset_def) hide_fact (open) member_coset -code_datatype List_Cset.set List_Cset.coset +code_datatype Cset.set List_Cset.coset lemma member_code [code]: - "member (List_Cset.set xs) = List.member xs" + "member (Cset.set xs) = List.member xs" "member (List_Cset.coset xs) = Not \ List.member xs" by (simp_all add: fun_eq_iff member_def fun_Compl_def bool_Compl_def) @@ -48,7 +40,7 @@ definition (in term_syntax) setify :: "'a\typerep list \ (unit \ Code_Evaluation.term) \ 'a Cset.set \ (unit \ Code_Evaluation.term)" where - [code_unfold]: "setify xs = Code_Evaluation.valtermify List_Cset.set {\} xs" + [code_unfold]: "setify xs = Code_Evaluation.valtermify Cset.set {\} xs" notation fcomp (infixl "\>" 60) notation scomp (infixl "\\" 60) @@ -69,12 +61,12 @@ subsection {* Basic operations *} lemma is_empty_set [code]: - "Cset.is_empty (List_Cset.set xs) \ List.null xs" + "Cset.is_empty (Cset.set xs) \ List.null xs" by (simp add: is_empty_set null_def) hide_fact (open) is_empty_set lemma empty_set [code]: - "bot = List_Cset.set []" + "Cset.empty = Cset.set []" by (simp add: set_def) hide_fact (open) empty_set @@ -84,63 +76,87 @@ hide_fact (open) UNIV_set lemma remove_set [code]: - "Cset.remove x (List_Cset.set xs) = List_Cset.set (removeAll x xs)" + "Cset.remove x (Cset.set xs) = Cset.set (removeAll x xs)" "Cset.remove x (List_Cset.coset xs) = List_Cset.coset (List.insert x xs)" -by (simp_all add: set_def coset_def) +by (simp_all add: Cset.set_def coset_def) (metis List.set_insert More_Set.remove_def remove_set_compl) lemma insert_set [code]: - "Cset.insert x (List_Cset.set xs) = List_Cset.set (List.insert x xs)" + "Cset.insert x (Cset.set xs) = Cset.set (List.insert x xs)" "Cset.insert x (List_Cset.coset xs) = List_Cset.coset (removeAll x xs)" - by (simp_all add: set_def coset_def) + by (simp_all add: Cset.set_def coset_def) lemma map_set [code]: - "Cset.map f (List_Cset.set xs) = List_Cset.set (remdups (List.map f xs))" - by (simp add: set_def) + "Cset.map f (Cset.set xs) = Cset.set (remdups (List.map f xs))" + by (simp add: Cset.set_def) lemma filter_set [code]: - "Cset.filter P (List_Cset.set xs) = List_Cset.set (List.filter P xs)" - by (simp add: set_def project_set) + "Cset.filter P (Cset.set xs) = Cset.set (List.filter P xs)" + by (simp add: Cset.set_def project_set) lemma forall_set [code]: - "Cset.forall P (List_Cset.set xs) \ list_all P xs" - by (simp add: set_def list_all_iff) + "Cset.forall P (Cset.set xs) \ list_all P xs" + by (simp add: Cset.set_def list_all_iff) lemma exists_set [code]: - "Cset.exists P (List_Cset.set xs) \ list_ex P xs" - by (simp add: set_def list_ex_iff) + "Cset.exists P (Cset.set xs) \ list_ex P xs" + by (simp add: Cset.set_def list_ex_iff) lemma card_set [code]: - "Cset.card (List_Cset.set xs) = length (remdups xs)" + "Cset.card (Cset.set xs) = length (remdups xs)" proof - have "Finite_Set.card (set (remdups xs)) = length (remdups xs)" by (rule distinct_card) simp - then show ?thesis by (simp add: set_def) + then show ?thesis by (simp add: Cset.set_def) qed lemma compl_set [simp, code]: - "- List_Cset.set xs = List_Cset.coset xs" - by (simp add: set_def coset_def) + "- Cset.set xs = List_Cset.coset xs" + by (simp add: Cset.set_def coset_def) lemma compl_coset [simp, code]: - "- List_Cset.coset xs = List_Cset.set xs" - by (simp add: set_def coset_def) + "- List_Cset.coset xs = Cset.set xs" + by (simp add: Cset.set_def coset_def) context complete_lattice begin lemma Infimum_inf [code]: - "Infimum (List_Cset.set As) = foldr inf As top" + "Infimum (Cset.set As) = foldr inf As top" "Infimum (List_Cset.coset []) = bot" by (simp_all add: Inf_set_foldr Inf_UNIV) lemma Supremum_sup [code]: - "Supremum (List_Cset.set As) = foldr sup As bot" + "Supremum (Cset.set As) = foldr sup As bot" "Supremum (List_Cset.coset []) = top" by (simp_all add: Sup_set_foldr Sup_UNIV) end +declare single_code [code del] +lemma single_set [code]: + "Cset.single a = Cset.set [a]" +by(simp add: Cset.single_code) +hide_fact (open) single_set + +lemma bind_set [code]: + "Cset.bind (Cset.set xs) f = foldl (\A x. sup A (f x)) (Cset.set []) xs" +proof(rule sym) + show "foldl (\A x. sup A (f x)) (Cset.set []) xs = Cset.bind (Cset.set xs) f" + by(induct xs rule: rev_induct)(auto simp add: Cset.bind_def Cset.set_def) +qed +hide_fact (open) bind_set + +lemma pred_of_cset_set [code]: + "pred_of_cset (Cset.set xs) = foldr sup (map Predicate.single xs) bot" +proof - + have "pred_of_cset (Cset.set xs) = Predicate.Pred (\x. x \ set xs)" + by(auto simp add: Cset.pred_of_cset_def mem_def) + moreover have "foldr sup (map Predicate.single xs) bot = \" + by(induct xs)(auto simp add: bot_pred_def simp del: mem_def intro: pred_eqI, simp) + ultimately show ?thesis by(simp) +qed +hide_fact (open) pred_of_cset_set subsection {* Derived operations *} @@ -171,11 +187,11 @@ subsection {* Functorial operations *} lemma inter_project [code]: - "inf A (List_Cset.set xs) = List_Cset.set (List.filter (Cset.member A) xs)" + "inf A (Cset.set xs) = Cset.set (List.filter (Cset.member A) xs)" "inf A (List_Cset.coset xs) = foldr Cset.remove xs A" proof - - show "inf A (List_Cset.set xs) = List_Cset.set (List.filter (member A) xs)" - by (simp add: inter project_def set_def) + show "inf A (Cset.set xs) = Cset.set (List.filter (member A) xs)" + by (simp add: inter project_def Cset.set_def) have *: "\x::'a. Cset.remove = (\x. Set \ More_Set.remove x \ member)" by (simp add: fun_eq_iff More_Set.remove_def) have "member \ fold (\x. Set \ More_Set.remove x \ member) xs = @@ -193,12 +209,12 @@ qed lemma subtract_remove [code]: - "A - List_Cset.set xs = foldr Cset.remove xs A" - "A - List_Cset.coset xs = List_Cset.set (List.filter (member A) xs)" + "A - Cset.set xs = foldr Cset.remove xs A" + "A - List_Cset.coset xs = Cset.set (List.filter (member A) xs)" by (simp_all only: diff_eq compl_set compl_coset inter_project) lemma union_insert [code]: - "sup (List_Cset.set xs) A = foldr Cset.insert xs A" + "sup (Cset.set xs) A = foldr Cset.insert xs A" "sup (List_Cset.coset xs) A = List_Cset.coset (List.filter (Not \ member A) xs)" proof - have *: "\x::'a. Cset.insert = (\x. Set \ Set.insert x \ member)" @@ -209,11 +225,11 @@ then have "fold Set.insert xs (member A) = member (fold (\x. Set \ Set.insert x \ member) xs A)" by (simp add: fun_eq_iff) - then have "sup (List_Cset.set xs) A = fold Cset.insert xs A" + then have "sup (Cset.set xs) A = fold Cset.insert xs A" by (simp add: union_set *) moreover have "\x y :: 'a. Cset.insert y \ Cset.insert x = Cset.insert x \ Cset.insert y" by (auto simp add: * intro: ext) - ultimately show "sup (List_Cset.set xs) A = foldr Cset.insert xs A" + ultimately show "sup (Cset.set xs) A = foldr Cset.insert xs A" by (simp add: foldr_fold) show "sup (List_Cset.coset xs) A = List_Cset.coset (List.filter (Not \ member A) xs)" by (auto simp add: coset_def)