author | Cezary Kaliszyk <kaliszyk@in.tum.de> |
Fri, 19 Aug 2011 17:05:10 +0900 | |
changeset 45164 | 83c4f8ba0aa3 |
parent 44797 | 3264fbfd87d6 |
permissions | -rw-r--r-- |
krauss@44664 | 1 |
(* Title: HOL/Quotient_Examples/List_Cset.thy |
krauss@44664 | 2 |
Author: Florian Haftmann, Alexander Krauss, TU Muenchen |
krauss@44664 | 3 |
*) |
krauss@44664 | 4 |
|
krauss@44664 | 5 |
header {* Implementation of type Cset.set based on lists. Code equations obtained via quotient lifting. *} |
krauss@44664 | 6 |
|
krauss@44664 | 7 |
theory List_Cset |
krauss@44664 | 8 |
imports Cset |
krauss@44664 | 9 |
begin |
krauss@44664 | 10 |
|
krauss@44664 | 11 |
lemma [quot_respect]: "((op = ===> set_eq ===> set_eq) ===> op = ===> set_eq ===> set_eq) |
krauss@44664 | 12 |
foldr foldr" |
krauss@44664 | 13 |
by (simp add: fun_rel_eq) |
krauss@44664 | 14 |
|
krauss@44664 | 15 |
lemma [quot_preserve]: "((id ---> abs_set ---> rep_set) ---> id ---> rep_set ---> abs_set) foldr = foldr" |
krauss@44664 | 16 |
apply (rule ext)+ |
krauss@44664 | 17 |
by (induct_tac xa) (auto simp: Quotient_abs_rep[OF Quotient_set]) |
krauss@44664 | 18 |
|
krauss@44664 | 19 |
|
krauss@44664 | 20 |
subsection {* Relationship to lists *} |
krauss@44664 | 21 |
|
krauss@44664 | 22 |
(*FIXME: maybe define on sets first and then lift -> more canonical*) |
krauss@44664 | 23 |
definition coset :: "'a list \<Rightarrow> 'a Cset.set" where |
krauss@44664 | 24 |
"coset xs = Cset.uminus (Cset.set xs)" |
krauss@44664 | 25 |
|
krauss@44664 | 26 |
code_datatype Cset.set List_Cset.coset |
krauss@44664 | 27 |
|
krauss@44664 | 28 |
lemma member_code [code]: |
krauss@44664 | 29 |
"member x (Cset.set xs) \<longleftrightarrow> List.member xs x" |
krauss@44664 | 30 |
"member x (coset xs) \<longleftrightarrow> \<not> List.member xs x" |
krauss@44664 | 31 |
unfolding coset_def |
krauss@44664 | 32 |
apply (lifting in_set_member) |
krauss@44664 | 33 |
by descending (simp add: in_set_member) |
krauss@44664 | 34 |
|
krauss@44664 | 35 |
definition (in term_syntax) |
krauss@44664 | 36 |
setify :: "'a\<Colon>typerep list \<times> (unit \<Rightarrow> Code_Evaluation.term) |
krauss@44664 | 37 |
\<Rightarrow> 'a Cset.set \<times> (unit \<Rightarrow> Code_Evaluation.term)" where |
krauss@44664 | 38 |
[code_unfold]: "setify xs = Code_Evaluation.valtermify Cset.set {\<cdot>} xs" |
krauss@44664 | 39 |
|
krauss@44664 | 40 |
notation fcomp (infixl "\<circ>>" 60) |
krauss@44664 | 41 |
notation scomp (infixl "\<circ>\<rightarrow>" 60) |
krauss@44664 | 42 |
|
krauss@44664 | 43 |
instantiation Cset.set :: (random) random |
krauss@44664 | 44 |
begin |
krauss@44664 | 45 |
|
krauss@44664 | 46 |
definition |
krauss@44664 | 47 |
"Quickcheck.random i = Quickcheck.random i \<circ>\<rightarrow> (\<lambda>xs. Pair (setify xs))" |
krauss@44664 | 48 |
|
krauss@44664 | 49 |
instance .. |
krauss@44664 | 50 |
|
krauss@44664 | 51 |
end |
krauss@44664 | 52 |
|
krauss@44664 | 53 |
no_notation fcomp (infixl "\<circ>>" 60) |
krauss@44664 | 54 |
no_notation scomp (infixl "\<circ>\<rightarrow>" 60) |
krauss@44664 | 55 |
|
krauss@44664 | 56 |
subsection {* Basic operations *} |
krauss@44664 | 57 |
|
krauss@44664 | 58 |
lemma is_empty_set [code]: |
krauss@44664 | 59 |
"Cset.is_empty (Cset.set xs) \<longleftrightarrow> List.null xs" |
krauss@44664 | 60 |
by (lifting is_empty_set) |
krauss@44664 | 61 |
hide_fact (open) is_empty_set |
krauss@44664 | 62 |
|
krauss@44664 | 63 |
lemma empty_set [code]: |
krauss@44664 | 64 |
"Cset.empty = Cset.set []" |
krauss@44664 | 65 |
by (lifting set.simps(1)[symmetric]) |
krauss@44664 | 66 |
hide_fact (open) empty_set |
krauss@44664 | 67 |
|
krauss@44664 | 68 |
lemma UNIV_set [code]: |
krauss@44664 | 69 |
"Cset.UNIV = coset []" |
krauss@44664 | 70 |
unfolding coset_def by descending simp |
krauss@44664 | 71 |
hide_fact (open) UNIV_set |
krauss@44664 | 72 |
|
krauss@44664 | 73 |
lemma remove_set [code]: |
krauss@44664 | 74 |
"Cset.remove x (Cset.set xs) = Cset.set (removeAll x xs)" |
krauss@44664 | 75 |
"Cset.remove x (coset xs) = coset (List.insert x xs)" |
krauss@44664 | 76 |
unfolding coset_def |
krauss@44664 | 77 |
apply descending |
krauss@44664 | 78 |
apply (simp add: More_Set.remove_def) |
krauss@44664 | 79 |
apply descending |
krauss@44664 | 80 |
by (simp add: remove_set_compl) |
krauss@44664 | 81 |
|
krauss@44664 | 82 |
lemma insert_set [code]: |
krauss@44664 | 83 |
"Cset.insert x (Cset.set xs) = Cset.set (List.insert x xs)" |
krauss@44664 | 84 |
"Cset.insert x (coset xs) = coset (removeAll x xs)" |
krauss@44664 | 85 |
unfolding coset_def |
krauss@44664 | 86 |
apply (lifting set_insert[symmetric]) |
krauss@44664 | 87 |
by descending simp |
krauss@44664 | 88 |
|
krauss@44664 | 89 |
lemma map_set [code]: |
krauss@44664 | 90 |
"Cset.map f (Cset.set xs) = Cset.set (remdups (List.map f xs))" |
krauss@44664 | 91 |
by descending simp |
kaliszyk@45164 | 92 |
|
krauss@44664 | 93 |
lemma filter_set [code]: |
krauss@44664 | 94 |
"Cset.filter P (Cset.set xs) = Cset.set (List.filter P xs)" |
krauss@44664 | 95 |
by descending (simp add: project_set) |
krauss@44664 | 96 |
|
krauss@44664 | 97 |
lemma forall_set [code]: |
krauss@44664 | 98 |
"Cset.forall (Cset.set xs) P \<longleftrightarrow> list_all P xs" |
krauss@44664 | 99 |
(* FIXME: why does (lifting Ball_set_list_all) fail? *) |
krauss@44664 | 100 |
by descending (fact Ball_set_list_all) |
krauss@44664 | 101 |
|
krauss@44664 | 102 |
lemma exists_set [code]: |
krauss@44664 | 103 |
"Cset.exists (Cset.set xs) P \<longleftrightarrow> list_ex P xs" |
krauss@44664 | 104 |
by descending (fact Bex_set_list_ex) |
krauss@44664 | 105 |
|
krauss@44664 | 106 |
lemma card_set [code]: |
krauss@44664 | 107 |
"Cset.card (Cset.set xs) = length (remdups xs)" |
krauss@44664 | 108 |
by (lifting length_remdups_card_conv[symmetric]) |
krauss@44664 | 109 |
|
krauss@44664 | 110 |
lemma compl_set [simp, code]: |
krauss@44664 | 111 |
"Cset.uminus (Cset.set xs) = coset xs" |
krauss@44664 | 112 |
unfolding coset_def by descending simp |
krauss@44664 | 113 |
|
krauss@44664 | 114 |
lemma compl_coset [simp, code]: |
krauss@44664 | 115 |
"Cset.uminus (coset xs) = Cset.set xs" |
krauss@44664 | 116 |
unfolding coset_def by descending simp |
krauss@44664 | 117 |
|
kaliszyk@45164 | 118 |
lemma Inf_inf [code]: |
kaliszyk@45164 | 119 |
"Cset.Inf (Cset.set (xs\<Colon>'a\<Colon>complete_lattice list)) = foldr inf xs top" |
kaliszyk@45164 | 120 |
"Cset.Inf (coset ([]\<Colon>'a\<Colon>complete_lattice list)) = bot" |
kaliszyk@45164 | 121 |
unfolding List_Cset.UNIV_set[symmetric] |
kaliszyk@45164 | 122 |
by (lifting Inf_set_foldr Inf_UNIV) |
krauss@44664 | 123 |
|
kaliszyk@45164 | 124 |
lemma Sup_sup [code]: |
kaliszyk@45164 | 125 |
"Cset.Sup (Cset.set (xs\<Colon>'a\<Colon>complete_lattice list)) = foldr sup xs bot" |
kaliszyk@45164 | 126 |
"Cset.Sup (coset ([]\<Colon>'a\<Colon>complete_lattice list)) = top" |
kaliszyk@45164 | 127 |
unfolding List_Cset.UNIV_set[symmetric] |
kaliszyk@45164 | 128 |
by (lifting Sup_set_foldr Sup_UNIV) |
krauss@44664 | 129 |
|
krauss@44664 | 130 |
subsection {* Derived operations *} |
krauss@44664 | 131 |
|
krauss@44664 | 132 |
lemma subset_eq_forall [code]: |
krauss@44664 | 133 |
"Cset.subset A B \<longleftrightarrow> Cset.forall A (\<lambda>x. member x B)" |
krauss@44664 | 134 |
by descending blast |
krauss@44664 | 135 |
|
krauss@44664 | 136 |
lemma subset_subset_eq [code]: |
krauss@44664 | 137 |
"Cset.psubset A B \<longleftrightarrow> Cset.subset A B \<and> \<not> Cset.subset B A" |
krauss@44664 | 138 |
by descending blast |
krauss@44664 | 139 |
|
krauss@44664 | 140 |
instantiation Cset.set :: (type) equal |
krauss@44664 | 141 |
begin |
krauss@44664 | 142 |
|
krauss@44664 | 143 |
definition [code]: |
krauss@44664 | 144 |
"HOL.equal A B \<longleftrightarrow> Cset.subset A B \<and> Cset.subset B A" |
krauss@44664 | 145 |
|
krauss@44664 | 146 |
instance |
krauss@44664 | 147 |
apply intro_classes |
krauss@44664 | 148 |
unfolding equal_set_def |
krauss@44664 | 149 |
by descending auto |
krauss@44664 | 150 |
|
krauss@44664 | 151 |
end |
krauss@44664 | 152 |
|
krauss@44664 | 153 |
lemma [code nbe]: |
krauss@44664 | 154 |
"HOL.equal (A :: 'a Cset.set) A \<longleftrightarrow> True" |
krauss@44664 | 155 |
by (fact equal_refl) |
krauss@44664 | 156 |
|
krauss@44664 | 157 |
|
krauss@44664 | 158 |
subsection {* Functorial operations *} |
krauss@44664 | 159 |
|
krauss@44664 | 160 |
lemma inter_project [code]: |
krauss@44664 | 161 |
"Cset.inter A (Cset.set xs) = Cset.set (List.filter (\<lambda>x. Cset.member x A) xs)" |
krauss@44664 | 162 |
"Cset.inter A (coset xs) = foldr Cset.remove xs A" |
krauss@44664 | 163 |
apply descending |
krauss@44664 | 164 |
apply auto |
krauss@44664 | 165 |
unfolding coset_def |
krauss@44664 | 166 |
apply descending |
krauss@44664 | 167 |
apply simp |
krauss@44664 | 168 |
by (metis diff_eq minus_set_foldr) |
krauss@44664 | 169 |
|
krauss@44664 | 170 |
lemma subtract_remove [code]: |
krauss@44664 | 171 |
"Cset.minus A (Cset.set xs) = foldr Cset.remove xs A" |
krauss@44664 | 172 |
"Cset.minus A (coset xs) = Cset.set (List.filter (\<lambda>x. member x A) xs)" |
krauss@44664 | 173 |
unfolding coset_def |
krauss@44664 | 174 |
apply (lifting minus_set_foldr) |
krauss@44664 | 175 |
by descending auto |
krauss@44664 | 176 |
|
krauss@44664 | 177 |
lemma union_insert [code]: |
krauss@44664 | 178 |
"Cset.union (Cset.set xs) A = foldr Cset.insert xs A" |
krauss@44664 | 179 |
"Cset.union (coset xs) A = coset (List.filter (\<lambda>x. \<not> member x A) xs)" |
krauss@44664 | 180 |
unfolding coset_def |
krauss@44664 | 181 |
apply (lifting union_set_foldr) |
krauss@44664 | 182 |
by descending auto |
krauss@44664 | 183 |
|
krauss@44797 | 184 |
lemma UNION_code [code]: |
krauss@44797 | 185 |
"Cset.UNION (Cset.set []) f = Cset.set []" |
krauss@44797 | 186 |
"Cset.UNION (Cset.set (x#xs)) f = |
krauss@44797 | 187 |
Cset.union (f x) (Cset.UNION (Cset.set xs) f)" |
krauss@44797 | 188 |
by (descending, simp)+ |
krauss@44797 | 189 |
|
krauss@44797 | 190 |
|
kaliszyk@45164 | 191 |
end |