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