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