src/HOL/Library/Cset.thy
author bulwahn
Tue Sep 13 09:28:03 2011 +0200 (2011-09-13)
changeset 44913 48240fb48980
parent 44563 01b2732cf4ad
child 45970 b6d0cff57d96
permissions -rw-r--r--
correcting theory name and dependencies
     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 set_of Set by rule+
    14 hide_type (open) set
    15 
    16 lemma set_of_Set [simp]:
    17   "set_of (Set A) = A"
    18   by (rule Set_inverse) rule
    19 
    20 lemma Set_set_of [simp]:
    21   "Set (set_of A) = A"
    22   by (fact set_of_inverse)
    23 
    24 definition member :: "'a Cset.set \<Rightarrow> 'a \<Rightarrow> bool" where
    25   "member A x \<longleftrightarrow> x \<in> set_of A"
    26 
    27 lemma member_set_of:
    28   "set_of = member"
    29   by (rule ext)+ (simp add: member_def mem_def)
    30 
    31 lemma member_Set [simp]:
    32   "member (Set A) x \<longleftrightarrow> x \<in> A"
    33   by (simp add: member_def)
    34 
    35 lemma Set_inject [simp]:
    36   "Set A = Set B \<longleftrightarrow> A = B"
    37   by (simp add: Set_inject)
    38 
    39 lemma set_eq_iff:
    40   "A = B \<longleftrightarrow> member A = member B"
    41   by (auto simp add: fun_eq_iff set_of_inject [symmetric] member_def mem_def)
    42 hide_fact (open) set_eq_iff
    43 
    44 lemma set_eqI:
    45   "member A = member B \<Longrightarrow> A = B"
    46   by (simp add: Cset.set_eq_iff)
    47 hide_fact (open) set_eqI
    48 
    49 subsection {* Lattice instantiation *}
    50 
    51 instantiation Cset.set :: (type) boolean_algebra
    52 begin
    53 
    54 definition less_eq_set :: "'a Cset.set \<Rightarrow> 'a Cset.set \<Rightarrow> bool" where
    55   [simp]: "A \<le> B \<longleftrightarrow> set_of A \<subseteq> set_of B"
    56 
    57 definition less_set :: "'a Cset.set \<Rightarrow> 'a Cset.set \<Rightarrow> bool" where
    58   [simp]: "A < B \<longleftrightarrow> set_of A \<subset> set_of B"
    59 
    60 definition inf_set :: "'a Cset.set \<Rightarrow> 'a Cset.set \<Rightarrow> 'a Cset.set" where
    61   [simp]: "inf A B = Set (set_of A \<inter> set_of B)"
    62 
    63 definition sup_set :: "'a Cset.set \<Rightarrow> 'a Cset.set \<Rightarrow> 'a Cset.set" where
    64   [simp]: "sup A B = Set (set_of A \<union> set_of B)"
    65 
    66 definition bot_set :: "'a Cset.set" where
    67   [simp]: "bot = Set {}"
    68 
    69 definition top_set :: "'a Cset.set" where
    70   [simp]: "top = Set UNIV"
    71 
    72 definition uminus_set :: "'a Cset.set \<Rightarrow> 'a Cset.set" where
    73   [simp]: "- A = Set (- (set_of A))"
    74 
    75 definition minus_set :: "'a Cset.set \<Rightarrow> 'a Cset.set \<Rightarrow> 'a Cset.set" where
    76   [simp]: "A - B = Set (set_of A - set_of B)"
    77 
    78 instance proof
    79 qed (auto intro!: Cset.set_eqI simp add: member_def mem_def)
    80 
    81 end
    82 
    83 instantiation Cset.set :: (type) complete_lattice
    84 begin
    85 
    86 definition Inf_set :: "'a Cset.set set \<Rightarrow> 'a Cset.set" where
    87   [simp]: "Inf_set As = Set (Inf (image set_of As))"
    88 
    89 definition Sup_set :: "'a Cset.set set \<Rightarrow> 'a Cset.set" where
    90   [simp]: "Sup_set As = Set (Sup (image set_of As))"
    91 
    92 instance proof
    93 qed (auto simp add: le_fun_def)
    94 
    95 end
    96 
    97 instance Cset.set :: (type) complete_boolean_algebra proof
    98 qed (unfold INF_def SUP_def, auto)
    99 
   100 
   101 subsection {* Basic operations *}
   102 
   103 abbreviation empty :: "'a Cset.set" where "empty \<equiv> bot"
   104 hide_const (open) empty
   105 
   106 abbreviation UNIV :: "'a Cset.set" where "UNIV \<equiv> top"
   107 hide_const (open) UNIV
   108 
   109 definition is_empty :: "'a Cset.set \<Rightarrow> bool" where
   110   [simp]: "is_empty A \<longleftrightarrow> More_Set.is_empty (set_of A)"
   111 
   112 definition insert :: "'a \<Rightarrow> 'a Cset.set \<Rightarrow> 'a Cset.set" where
   113   [simp]: "insert x A = Set (Set.insert x (set_of A))"
   114 
   115 definition remove :: "'a \<Rightarrow> 'a Cset.set \<Rightarrow> 'a Cset.set" where
   116   [simp]: "remove x A = Set (More_Set.remove x (set_of A))"
   117 
   118 definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a Cset.set \<Rightarrow> 'b Cset.set" where
   119   [simp]: "map f A = Set (image f (set_of A))"
   120 
   121 enriched_type map: map
   122   by (simp_all add: fun_eq_iff image_compose)
   123 
   124 definition filter :: "('a \<Rightarrow> bool) \<Rightarrow> 'a Cset.set \<Rightarrow> 'a Cset.set" where
   125   [simp]: "filter P A = Set (More_Set.project P (set_of A))"
   126 
   127 definition forall :: "('a \<Rightarrow> bool) \<Rightarrow> 'a Cset.set \<Rightarrow> bool" where
   128   [simp]: "forall P A \<longleftrightarrow> Ball (set_of A) P"
   129 
   130 definition exists :: "('a \<Rightarrow> bool) \<Rightarrow> 'a Cset.set \<Rightarrow> bool" where
   131   [simp]: "exists P A \<longleftrightarrow> Bex (set_of A) P"
   132 
   133 definition card :: "'a Cset.set \<Rightarrow> nat" where
   134   [simp]: "card A = Finite_Set.card (set_of A)"
   135   
   136 context complete_lattice
   137 begin
   138 
   139 definition Infimum :: "'a Cset.set \<Rightarrow> 'a" where
   140   [simp]: "Infimum A = Inf (set_of A)"
   141 
   142 definition Supremum :: "'a Cset.set \<Rightarrow> 'a" where
   143   [simp]: "Supremum A = Sup (set_of A)"
   144 
   145 end
   146 
   147 subsection {* More operations *}
   148 
   149 text {* conversion from @{typ "'a list"} *}
   150 
   151 definition set :: "'a list \<Rightarrow> 'a Cset.set" where
   152   "set xs = Set (List.set xs)"
   153 hide_const (open) set
   154 
   155 definition coset :: "'a list \<Rightarrow> 'a Cset.set" where
   156   "coset xs = Set (- List.set xs)"
   157 hide_const (open) coset
   158 
   159 text {* conversion from @{typ "'a Predicate.pred"} *}
   160 
   161 definition pred_of_cset :: "'a Cset.set \<Rightarrow> 'a Predicate.pred" where
   162   [code del]: "pred_of_cset = Predicate.Pred \<circ> Cset.member"
   163 
   164 definition of_pred :: "'a Predicate.pred \<Rightarrow> 'a Cset.set" where
   165   "of_pred = Cset.Set \<circ> Collect \<circ> Predicate.eval"
   166 
   167 definition of_seq :: "'a Predicate.seq \<Rightarrow> 'a Cset.set" where 
   168   "of_seq = of_pred \<circ> Predicate.pred_of_seq"
   169 
   170 text {* monad operations *}
   171 
   172 definition single :: "'a \<Rightarrow> 'a Cset.set" where
   173   "single a = Set {a}"
   174 
   175 definition bind :: "'a Cset.set \<Rightarrow> ('a \<Rightarrow> 'b Cset.set) \<Rightarrow> 'b Cset.set" (infixl "\<guillemotright>=" 70) where
   176   "A \<guillemotright>= f = (SUP x : set_of A. f x)"
   177 
   178 
   179 subsection {* Simplified simprules *}
   180 
   181 lemma empty_simp [simp]: "member Cset.empty = bot"
   182   by (simp add: fun_eq_iff bot_apply)
   183 
   184 lemma UNIV_simp [simp]: "member Cset.UNIV = top"
   185   by (simp add: fun_eq_iff top_apply)
   186 
   187 lemma is_empty_simp [simp]:
   188   "is_empty A \<longleftrightarrow> set_of A = {}"
   189   by (simp add: More_Set.is_empty_def)
   190 declare is_empty_def [simp del]
   191 
   192 lemma remove_simp [simp]:
   193   "remove x A = Set (set_of A - {x})"
   194   by (simp add: More_Set.remove_def)
   195 declare remove_def [simp del]
   196 
   197 lemma filter_simp [simp]:
   198   "filter P A = Set {x \<in> set_of A. P x}"
   199   by (simp add: More_Set.project_def)
   200 declare filter_def [simp del]
   201 
   202 lemma set_of_set [simp]:
   203   "set_of (Cset.set xs) = set xs"
   204   by (simp add: set_def)
   205 hide_fact (open) set_def
   206 
   207 lemma member_set [simp]:
   208   "member (Cset.set xs) = (\<lambda>x. x \<in> set xs)"
   209   by (simp add: fun_eq_iff member_def)
   210 hide_fact (open) member_set
   211 
   212 lemma set_of_coset [simp]:
   213   "set_of (Cset.coset xs) = - set xs"
   214   by (simp add: coset_def)
   215 hide_fact (open) coset_def
   216 
   217 lemma member_coset [simp]:
   218   "member (Cset.coset xs) = (\<lambda>x. x \<in> - set xs)"
   219   by (simp add: fun_eq_iff member_def)
   220 hide_fact (open) member_coset
   221 
   222 lemma set_simps [simp]:
   223   "Cset.set [] = Cset.empty"
   224   "Cset.set (x # xs) = insert x (Cset.set xs)"
   225 by(simp_all add: Cset.set_def)
   226 
   227 lemma member_SUP [simp]:
   228   "member (SUPR A f) = SUPR A (member \<circ> f)"
   229   by (auto simp add: fun_eq_iff SUP_apply member_def, unfold SUP_def, auto)
   230 
   231 lemma member_bind [simp]:
   232   "member (P \<guillemotright>= f) = SUPR (set_of P) (member \<circ> f)"
   233   by (simp add: bind_def Cset.set_eq_iff)
   234 
   235 lemma member_single [simp]:
   236   "member (single a) = (\<lambda>x. x \<in> {a})"
   237   by (simp add: single_def fun_eq_iff)
   238 
   239 lemma single_sup_simps [simp]:
   240   shows single_sup: "sup (single a) A = insert a A"
   241   and sup_single: "sup A (single a) = insert a A"
   242   by (auto simp add: Cset.set_eq_iff single_def)
   243 
   244 lemma single_bind [simp]:
   245   "single a \<guillemotright>= B = B a"
   246   by (simp add: Cset.set_eq_iff SUP_insert single_def)
   247 
   248 lemma bind_bind:
   249   "(A \<guillemotright>= B) \<guillemotright>= C = A \<guillemotright>= (\<lambda>x. B x \<guillemotright>= C)"
   250   by (simp add: bind_def, simp only: SUP_def image_image, simp)
   251  
   252 lemma bind_single [simp]:
   253   "A \<guillemotright>= single = A"
   254   by (simp add: Cset.set_eq_iff SUP_apply fun_eq_iff single_def member_def)
   255 
   256 lemma bind_const: "A \<guillemotright>= (\<lambda>_. B) = (if Cset.is_empty A then Cset.empty else B)"
   257   by (auto simp add: Cset.set_eq_iff fun_eq_iff)
   258 
   259 lemma empty_bind [simp]:
   260   "Cset.empty \<guillemotright>= f = Cset.empty"
   261   by (simp add: Cset.set_eq_iff fun_eq_iff bot_apply)
   262 
   263 lemma member_of_pred [simp]:
   264   "member (of_pred P) = (\<lambda>x. x \<in> {x. Predicate.eval P x})"
   265   by (simp add: of_pred_def fun_eq_iff)
   266 
   267 lemma member_of_seq [simp]:
   268   "member (of_seq xq) = (\<lambda>x. x \<in> {x. Predicate.member xq x})"
   269   by (simp add: of_seq_def eval_member)
   270 
   271 lemma eval_pred_of_cset [simp]: 
   272   "Predicate.eval (pred_of_cset A) = Cset.member A"
   273   by (simp add: pred_of_cset_def)
   274 
   275 subsection {* Default implementations *}
   276 
   277 lemma set_code [code]:
   278   "Cset.set = (\<lambda>xs. fold insert xs Cset.empty)"
   279 proof (rule ext, rule Cset.set_eqI)
   280   fix xs :: "'a list"
   281   show "member (Cset.set xs) = member (fold insert xs Cset.empty)"
   282     by (simp add: fold_commute_apply [symmetric, where ?h = Set and ?g = Set.insert]
   283       fun_eq_iff Cset.set_def union_set [symmetric])
   284 qed
   285 
   286 lemma single_code [code]:
   287   "single a = insert a Cset.empty"
   288   by (simp add: Cset.single_def)
   289 
   290 lemma compl_set [simp]:
   291   "- Cset.set xs = Cset.coset xs"
   292   by (simp add: Cset.set_def Cset.coset_def)
   293 
   294 lemma compl_coset [simp]:
   295   "- Cset.coset xs = Cset.set xs"
   296   by (simp add: Cset.set_def Cset.coset_def)
   297 
   298 lemma inter_project:
   299   "inf A (Cset.set xs) = Cset.set (List.filter (Cset.member A) xs)"
   300   "inf A (Cset.coset xs) = foldr Cset.remove xs A"
   301 proof -
   302   show "inf A (Cset.set xs) = Cset.set (List.filter (member A) xs)"
   303     by (simp add: inter project_def Cset.set_def member_def)
   304   have *: "\<And>x::'a. Cset.remove = (\<lambda>x. Set \<circ> More_Set.remove x \<circ> set_of)"
   305     by (simp add: fun_eq_iff More_Set.remove_def)
   306   have "set_of \<circ> fold (\<lambda>x. Set \<circ> More_Set.remove x \<circ> set_of) xs =
   307     fold More_Set.remove xs \<circ> set_of"
   308     by (rule fold_commute) (simp add: fun_eq_iff)
   309   then have "fold More_Set.remove xs (set_of A) = 
   310     set_of (fold (\<lambda>x. Set \<circ> More_Set.remove x \<circ> set_of) xs A)"
   311     by (simp add: fun_eq_iff)
   312   then have "inf A (Cset.coset xs) = fold Cset.remove xs A"
   313     by (simp add: Diff_eq [symmetric] minus_set *)
   314   moreover have "\<And>x y :: 'a. Cset.remove y \<circ> Cset.remove x = Cset.remove x \<circ> Cset.remove y"
   315     by (auto simp add: More_Set.remove_def *)
   316   ultimately show "inf A (Cset.coset xs) = foldr Cset.remove xs A"
   317     by (simp add: foldr_fold)
   318 qed
   319 
   320 lemma union_insert:
   321   "sup (Cset.set xs) A = foldr Cset.insert xs A"
   322   "sup (Cset.coset xs) A = Cset.coset (List.filter (Not \<circ> member A) xs)"
   323 proof -
   324   have *: "\<And>x::'a. Cset.insert = (\<lambda>x. Set \<circ> Set.insert x \<circ> set_of)"
   325     by (simp add: fun_eq_iff)
   326   have "set_of \<circ> fold (\<lambda>x. Set \<circ> Set.insert x \<circ> set_of) xs =
   327     fold Set.insert xs \<circ> set_of"
   328     by (rule fold_commute) (simp add: fun_eq_iff)
   329   then have "fold Set.insert xs (set_of A) =
   330     set_of (fold (\<lambda>x. Set \<circ> Set.insert x \<circ> set_of) xs A)"
   331     by (simp add: fun_eq_iff)
   332   then have "sup (Cset.set xs) A = fold Cset.insert xs A"
   333     by (simp add: union_set *)
   334   moreover have "\<And>x y :: 'a. Cset.insert y \<circ> Cset.insert x = Cset.insert x \<circ> Cset.insert y"
   335     by (auto simp add: *)
   336   ultimately show "sup (Cset.set xs) A = foldr Cset.insert xs A"
   337     by (simp add: foldr_fold)
   338   show "sup (Cset.coset xs) A = Cset.coset (List.filter (Not \<circ> member A) xs)"
   339     by (auto simp add: Cset.coset_def Cset.member_def)
   340 qed
   341 
   342 lemma subtract_remove:
   343   "A - Cset.set xs = foldr Cset.remove xs A"
   344   "A - Cset.coset xs = Cset.set (List.filter (member A) xs)"
   345   by (simp_all only: diff_eq compl_set compl_coset inter_project)
   346 
   347 context complete_lattice
   348 begin
   349 
   350 lemma Infimum_inf:
   351   "Infimum (Cset.set As) = foldr inf As top"
   352   "Infimum (Cset.coset []) = bot"
   353   by (simp_all add: Inf_set_foldr)
   354 
   355 lemma Supremum_sup:
   356   "Supremum (Cset.set As) = foldr sup As bot"
   357   "Supremum (Cset.coset []) = top"
   358   by (simp_all add: Sup_set_foldr)
   359 
   360 end
   361 
   362 lemma of_pred_code [code]:
   363   "of_pred (Predicate.Seq f) = (case f () of
   364      Predicate.Empty \<Rightarrow> Cset.empty
   365    | Predicate.Insert x P \<Rightarrow> Cset.insert x (of_pred P)
   366    | Predicate.Join P xq \<Rightarrow> sup (of_pred P) (of_seq xq))"
   367   apply (auto split: seq.split simp add: Predicate.Seq_def of_pred_def Cset.set_eq_iff sup_apply eval_member [symmetric] member_def [symmetric] Collect_def mem_def member_set_of)
   368   apply (unfold Set.insert_def Collect_def sup_apply member_set_of)
   369   apply simp_all
   370   done
   371 
   372 lemma of_seq_code [code]:
   373   "of_seq Predicate.Empty = Cset.empty"
   374   "of_seq (Predicate.Insert x P) = Cset.insert x (of_pred P)"
   375   "of_seq (Predicate.Join P xq) = sup (of_pred P) (of_seq xq)"
   376   apply (auto simp add: of_seq_def of_pred_def Cset.set_eq_iff mem_def Collect_def)
   377   apply (unfold Set.insert_def Collect_def sup_apply member_set_of)
   378   apply simp_all
   379   done
   380 
   381 lemma bind_set:
   382   "Cset.bind (Cset.set xs) f = fold (sup \<circ> f) xs (Cset.set [])"
   383   by (simp add: Cset.bind_def SUPR_set_fold)
   384 hide_fact (open) bind_set
   385 
   386 lemma pred_of_cset_set:
   387   "pred_of_cset (Cset.set xs) = foldr sup (List.map Predicate.single xs) bot"
   388 proof -
   389   have "pred_of_cset (Cset.set xs) = Predicate.Pred (\<lambda>x. x \<in> set xs)"
   390     by (simp add: Cset.pred_of_cset_def member_set)
   391   moreover have "foldr sup (List.map Predicate.single xs) bot = \<dots>"
   392     by (induct xs) (auto simp add: bot_pred_def intro: pred_eqI, simp add: mem_def)
   393   ultimately show ?thesis by simp
   394 qed
   395 hide_fact (open) pred_of_cset_set
   396 
   397 no_notation bind (infixl "\<guillemotright>=" 70)
   398 
   399 hide_const (open) is_empty insert remove map filter forall exists card
   400   Inter Union bind single of_pred of_seq
   401 
   402 hide_fact (open) set_def pred_of_cset_def of_pred_def of_seq_def single_def 
   403   bind_def empty_simp UNIV_simp set_simps member_bind 
   404   member_single single_sup_simps single_sup sup_single single_bind
   405   bind_bind bind_single bind_const empty_bind member_of_pred member_of_seq
   406   eval_pred_of_cset set_code single_code of_pred_code of_seq_code
   407 
   408 end