src/HOL/Library/Cset.thy
author bulwahn
Fri Apr 08 16:31:14 2011 +0200 (2011-04-08)
changeset 42316 12635bb655fd
parent 41505 6d19301074cf
child 43241 93b1183e43e5
permissions -rw-r--r--
deactivating other compilations in quickcheck_exhaustive momentarily that only interesting for my benchmarks and experiments
     1 
     2 (* Author: Florian Haftmann, TU Muenchen *)
     3 
     4 header {* A dedicated set type which is executable on its finite part *}
     5 
     6 theory Cset
     7 imports More_Set More_List
     8 begin
     9 
    10 subsection {* Lifting *}
    11 
    12 typedef (open) 'a set = "UNIV :: 'a set set"
    13   morphisms member Set by rule+
    14 hide_type (open) set
    15 
    16 lemma member_Set [simp]:
    17   "member (Set A) = A"
    18   by (rule Set_inverse) rule
    19 
    20 lemma Set_member [simp]:
    21   "Set (member A) = A"
    22   by (fact member_inverse)
    23 
    24 lemma Set_inject [simp]:
    25   "Set A = Set B \<longleftrightarrow> A = B"
    26   by (simp add: Set_inject)
    27 
    28 lemma set_eq_iff:
    29   "A = B \<longleftrightarrow> member A = member B"
    30   by (simp add: member_inject)
    31 hide_fact (open) set_eq_iff
    32 
    33 lemma set_eqI:
    34   "member A = member B \<Longrightarrow> A = B"
    35   by (simp add: Cset.set_eq_iff)
    36 hide_fact (open) set_eqI
    37 
    38 declare mem_def [simp]
    39 
    40 definition set :: "'a list \<Rightarrow> 'a Cset.set" where
    41   "set xs = Set (List.set xs)"
    42 hide_const (open) set
    43 
    44 lemma member_set [simp]:
    45   "member (Cset.set xs) = set xs"
    46   by (simp add: set_def)
    47 hide_fact (open) member_set
    48 
    49 definition coset :: "'a list \<Rightarrow> 'a Cset.set" where
    50   "coset xs = Set (- set xs)"
    51 hide_const (open) coset
    52 
    53 lemma member_coset [simp]:
    54   "member (Cset.coset xs) = - set xs"
    55   by (simp add: coset_def)
    56 hide_fact (open) member_coset
    57 
    58 code_datatype Cset.set Cset.coset
    59 
    60 lemma member_code [code]:
    61   "member (Cset.set xs) = List.member xs"
    62   "member (Cset.coset xs) = Not \<circ> List.member xs"
    63   by (simp_all add: fun_eq_iff member_def fun_Compl_def bool_Compl_def)
    64 
    65 lemma member_image_UNIV [simp]:
    66   "member ` UNIV = UNIV"
    67 proof -
    68   have "\<And>A \<Colon> 'a set. \<exists>B \<Colon> 'a Cset.set. A = member B"
    69   proof
    70     fix A :: "'a set"
    71     show "A = member (Set A)" by simp
    72   qed
    73   then show ?thesis by (simp add: image_def)
    74 qed
    75 
    76 definition (in term_syntax)
    77   setify :: "'a\<Colon>typerep list \<times> (unit \<Rightarrow> Code_Evaluation.term)
    78     \<Rightarrow> 'a Cset.set \<times> (unit \<Rightarrow> Code_Evaluation.term)" where
    79   [code_unfold]: "setify xs = Code_Evaluation.valtermify Cset.set {\<cdot>} xs"
    80 
    81 notation fcomp (infixl "\<circ>>" 60)
    82 notation scomp (infixl "\<circ>\<rightarrow>" 60)
    83 
    84 instantiation Cset.set :: (random) random
    85 begin
    86 
    87 definition
    88   "Quickcheck.random i = Quickcheck.random i \<circ>\<rightarrow> (\<lambda>xs. Pair (setify xs))"
    89 
    90 instance ..
    91 
    92 end
    93 
    94 no_notation fcomp (infixl "\<circ>>" 60)
    95 no_notation scomp (infixl "\<circ>\<rightarrow>" 60)
    96 
    97 
    98 subsection {* Lattice instantiation *}
    99 
   100 instantiation Cset.set :: (type) boolean_algebra
   101 begin
   102 
   103 definition less_eq_set :: "'a Cset.set \<Rightarrow> 'a Cset.set \<Rightarrow> bool" where
   104   [simp]: "A \<le> B \<longleftrightarrow> member A \<subseteq> member B"
   105 
   106 definition less_set :: "'a Cset.set \<Rightarrow> 'a Cset.set \<Rightarrow> bool" where
   107   [simp]: "A < B \<longleftrightarrow> member A \<subset> member B"
   108 
   109 definition inf_set :: "'a Cset.set \<Rightarrow> 'a Cset.set \<Rightarrow> 'a Cset.set" where
   110   [simp]: "inf A B = Set (member A \<inter> member B)"
   111 
   112 definition sup_set :: "'a Cset.set \<Rightarrow> 'a Cset.set \<Rightarrow> 'a Cset.set" where
   113   [simp]: "sup A B = Set (member A \<union> member B)"
   114 
   115 definition bot_set :: "'a Cset.set" where
   116   [simp]: "bot = Set {}"
   117 
   118 definition top_set :: "'a Cset.set" where
   119   [simp]: "top = Set UNIV"
   120 
   121 definition uminus_set :: "'a Cset.set \<Rightarrow> 'a Cset.set" where
   122   [simp]: "- A = Set (- (member A))"
   123 
   124 definition minus_set :: "'a Cset.set \<Rightarrow> 'a Cset.set \<Rightarrow> 'a Cset.set" where
   125   [simp]: "A - B = Set (member A - member B)"
   126 
   127 instance proof
   128 qed (auto intro: Cset.set_eqI)
   129 
   130 end
   131 
   132 instantiation Cset.set :: (type) complete_lattice
   133 begin
   134 
   135 definition Inf_set :: "'a Cset.set set \<Rightarrow> 'a Cset.set" where
   136   [simp]: "Inf_set As = Set (Inf (image member As))"
   137 
   138 definition Sup_set :: "'a Cset.set set \<Rightarrow> 'a Cset.set" where
   139   [simp]: "Sup_set As = Set (Sup (image member As))"
   140 
   141 instance proof
   142 qed (auto simp add: le_fun_def le_bool_def)
   143 
   144 end
   145 
   146 
   147 subsection {* Basic operations *}
   148 
   149 definition is_empty :: "'a Cset.set \<Rightarrow> bool" where
   150   [simp]: "is_empty A \<longleftrightarrow> More_Set.is_empty (member A)"
   151 
   152 lemma is_empty_set [code]:
   153   "is_empty (Cset.set xs) \<longleftrightarrow> List.null xs"
   154   by (simp add: is_empty_set)
   155 hide_fact (open) is_empty_set
   156 
   157 lemma empty_set [code]:
   158   "bot = Cset.set []"
   159   by (simp add: set_def)
   160 hide_fact (open) empty_set
   161 
   162 lemma UNIV_set [code]:
   163   "top = Cset.coset []"
   164   by (simp add: coset_def)
   165 hide_fact (open) UNIV_set
   166 
   167 definition insert :: "'a \<Rightarrow> 'a Cset.set \<Rightarrow> 'a Cset.set" where
   168   [simp]: "insert x A = Set (Set.insert x (member A))"
   169 
   170 lemma insert_set [code]:
   171   "insert x (Cset.set xs) = Cset.set (List.insert x xs)"
   172   "insert x (Cset.coset xs) = Cset.coset (removeAll x xs)"
   173   by (simp_all add: set_def coset_def)
   174 
   175 definition remove :: "'a \<Rightarrow> 'a Cset.set \<Rightarrow> 'a Cset.set" where
   176   [simp]: "remove x A = Set (More_Set.remove x (member A))"
   177 
   178 lemma remove_set [code]:
   179   "remove x (Cset.set xs) = Cset.set (removeAll x xs)"
   180   "remove x (Cset.coset xs) = Cset.coset (List.insert x xs)"
   181   by (simp_all add: set_def coset_def remove_set_compl)
   182     (simp add: More_Set.remove_def)
   183 
   184 definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a Cset.set \<Rightarrow> 'b Cset.set" where
   185   [simp]: "map f A = Set (image f (member A))"
   186 
   187 lemma map_set [code]:
   188   "map f (Cset.set xs) = Cset.set (remdups (List.map f xs))"
   189   by (simp add: set_def)
   190 
   191 enriched_type map: map
   192   by (simp_all add: fun_eq_iff image_compose)
   193 
   194 definition filter :: "('a \<Rightarrow> bool) \<Rightarrow> 'a Cset.set \<Rightarrow> 'a Cset.set" where
   195   [simp]: "filter P A = Set (More_Set.project P (member A))"
   196 
   197 lemma filter_set [code]:
   198   "filter P (Cset.set xs) = Cset.set (List.filter P xs)"
   199   by (simp add: set_def project_set)
   200 
   201 definition forall :: "('a \<Rightarrow> bool) \<Rightarrow> 'a Cset.set \<Rightarrow> bool" where
   202   [simp]: "forall P A \<longleftrightarrow> Ball (member A) P"
   203 
   204 lemma forall_set [code]:
   205   "forall P (Cset.set xs) \<longleftrightarrow> list_all P xs"
   206   by (simp add: set_def list_all_iff)
   207 
   208 definition exists :: "('a \<Rightarrow> bool) \<Rightarrow> 'a Cset.set \<Rightarrow> bool" where
   209   [simp]: "exists P A \<longleftrightarrow> Bex (member A) P"
   210 
   211 lemma exists_set [code]:
   212   "exists P (Cset.set xs) \<longleftrightarrow> list_ex P xs"
   213   by (simp add: set_def list_ex_iff)
   214 
   215 definition card :: "'a Cset.set \<Rightarrow> nat" where
   216   [simp]: "card A = Finite_Set.card (member A)"
   217 
   218 lemma card_set [code]:
   219   "card (Cset.set xs) = length (remdups xs)"
   220 proof -
   221   have "Finite_Set.card (set (remdups xs)) = length (remdups xs)"
   222     by (rule distinct_card) simp
   223   then show ?thesis by (simp add: set_def)
   224 qed
   225 
   226 lemma compl_set [simp, code]:
   227   "- Cset.set xs = Cset.coset xs"
   228   by (simp add: set_def coset_def)
   229 
   230 lemma compl_coset [simp, code]:
   231   "- Cset.coset xs = Cset.set xs"
   232   by (simp add: set_def coset_def)
   233 
   234 
   235 subsection {* Derived operations *}
   236 
   237 lemma subset_eq_forall [code]:
   238   "A \<le> B \<longleftrightarrow> forall (member B) A"
   239   by (simp add: subset_eq)
   240 
   241 lemma subset_subset_eq [code]:
   242   "A < B \<longleftrightarrow> A \<le> B \<and> \<not> B \<le> (A :: 'a Cset.set)"
   243   by (fact less_le_not_le)
   244 
   245 instantiation Cset.set :: (type) equal
   246 begin
   247 
   248 definition [code]:
   249   "HOL.equal A B \<longleftrightarrow> A \<le> B \<and> B \<le> (A :: 'a Cset.set)"
   250 
   251 instance proof
   252 qed (simp add: equal_set_def set_eq [symmetric] Cset.set_eq_iff)
   253 
   254 end
   255 
   256 lemma [code nbe]:
   257   "HOL.equal (A :: 'a Cset.set) A \<longleftrightarrow> True"
   258   by (fact equal_refl)
   259 
   260 
   261 subsection {* Functorial operations *}
   262 
   263 lemma inter_project [code]:
   264   "inf A (Cset.set xs) = Cset.set (List.filter (member A) xs)"
   265   "inf A (Cset.coset xs) = foldr remove xs A"
   266 proof -
   267   show "inf A (Cset.set xs) = Cset.set (List.filter (member A) xs)"
   268     by (simp add: inter project_def set_def)
   269   have *: "\<And>x::'a. remove = (\<lambda>x. Set \<circ> More_Set.remove x \<circ> member)"
   270     by (simp add: fun_eq_iff)
   271   have "member \<circ> fold (\<lambda>x. Set \<circ> More_Set.remove x \<circ> member) xs =
   272     fold More_Set.remove xs \<circ> member"
   273     by (rule fold_commute) (simp add: fun_eq_iff)
   274   then have "fold More_Set.remove xs (member A) = 
   275     member (fold (\<lambda>x. Set \<circ> More_Set.remove x \<circ> member) xs A)"
   276     by (simp add: fun_eq_iff)
   277   then have "inf A (Cset.coset xs) = fold remove xs A"
   278     by (simp add: Diff_eq [symmetric] minus_set *)
   279   moreover have "\<And>x y :: 'a. Cset.remove y \<circ> Cset.remove x = Cset.remove x \<circ> Cset.remove y"
   280     by (auto simp add: More_Set.remove_def * intro: ext)
   281   ultimately show "inf A (Cset.coset xs) = foldr remove xs A"
   282     by (simp add: foldr_fold)
   283 qed
   284 
   285 lemma subtract_remove [code]:
   286   "A - Cset.set xs = foldr remove xs A"
   287   "A - Cset.coset xs = Cset.set (List.filter (member A) xs)"
   288   by (simp_all only: diff_eq compl_set compl_coset inter_project)
   289 
   290 lemma union_insert [code]:
   291   "sup (Cset.set xs) A = foldr insert xs A"
   292   "sup (Cset.coset xs) A = Cset.coset (List.filter (Not \<circ> member A) xs)"
   293 proof -
   294   have *: "\<And>x::'a. insert = (\<lambda>x. Set \<circ> Set.insert x \<circ> member)"
   295     by (simp add: fun_eq_iff)
   296   have "member \<circ> fold (\<lambda>x. Set \<circ> Set.insert x \<circ> member) xs =
   297     fold Set.insert xs \<circ> member"
   298     by (rule fold_commute) (simp add: fun_eq_iff)
   299   then have "fold Set.insert xs (member A) =
   300     member (fold (\<lambda>x. Set \<circ> Set.insert x \<circ> member) xs A)"
   301     by (simp add: fun_eq_iff)
   302   then have "sup (Cset.set xs) A = fold insert xs A"
   303     by (simp add: union_set *)
   304   moreover have "\<And>x y :: 'a. Cset.insert y \<circ> Cset.insert x = Cset.insert x \<circ> Cset.insert y"
   305     by (auto simp add: * intro: ext)
   306   ultimately show "sup (Cset.set xs) A = foldr insert xs A"
   307     by (simp add: foldr_fold)
   308   show "sup (Cset.coset xs) A = Cset.coset (List.filter (Not \<circ> member A) xs)"
   309     by (auto simp add: coset_def)
   310 qed
   311 
   312 context complete_lattice
   313 begin
   314 
   315 definition Infimum :: "'a Cset.set \<Rightarrow> 'a" where
   316   [simp]: "Infimum A = Inf (member A)"
   317 
   318 lemma Infimum_inf [code]:
   319   "Infimum (Cset.set As) = foldr inf As top"
   320   "Infimum (Cset.coset []) = bot"
   321   by (simp_all add: Inf_set_foldr Inf_UNIV)
   322 
   323 definition Supremum :: "'a Cset.set \<Rightarrow> 'a" where
   324   [simp]: "Supremum A = Sup (member A)"
   325 
   326 lemma Supremum_sup [code]:
   327   "Supremum (Cset.set As) = foldr sup As bot"
   328   "Supremum (Cset.coset []) = top"
   329   by (simp_all add: Sup_set_foldr Sup_UNIV)
   330 
   331 end
   332 
   333 
   334 subsection {* Simplified simprules *}
   335 
   336 lemma is_empty_simp [simp]:
   337   "is_empty A \<longleftrightarrow> member A = {}"
   338   by (simp add: More_Set.is_empty_def)
   339 declare is_empty_def [simp del]
   340 
   341 lemma remove_simp [simp]:
   342   "remove x A = Set (member A - {x})"
   343   by (simp add: More_Set.remove_def)
   344 declare remove_def [simp del]
   345 
   346 lemma filter_simp [simp]:
   347   "filter P A = Set {x \<in> member A. P x}"
   348   by (simp add: More_Set.project_def)
   349 declare filter_def [simp del]
   350 
   351 declare mem_def [simp del]
   352 
   353 
   354 hide_const (open) setify is_empty insert remove map filter forall exists card
   355   Inter Union
   356 
   357 end