src/HOL/Library/Cset.thy
author Andreas Lochbihler
Mon Jul 25 16:55:48 2011 +0200 (2011-07-25)
changeset 43971 892030194015
parent 43241 93b1183e43e5
child 44555 da75ffe3d988
permissions -rw-r--r--
added operations to Cset with code equations in backing implementations
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@40672
    13
  morphisms member Set by rule+
haftmann@40672
    14
hide_type (open) set
haftmann@31807
    15
haftmann@40672
    16
lemma member_Set [simp]:
haftmann@40672
    17
  "member (Set A) = A"
haftmann@40672
    18
  by (rule Set_inverse) rule
haftmann@34048
    19
haftmann@40672
    20
lemma Set_member [simp]:
haftmann@40672
    21
  "Set (member A) = A"
haftmann@37699
    22
  by (fact member_inverse)
haftmann@37468
    23
haftmann@40672
    24
lemma Set_inject [simp]:
haftmann@40672
    25
  "Set A = Set B \<longleftrightarrow> A = B"
haftmann@40672
    26
  by (simp add: Set_inject)
haftmann@37468
    27
haftmann@40672
    28
lemma set_eq_iff:
haftmann@39380
    29
  "A = B \<longleftrightarrow> member A = member B"
haftmann@39380
    30
  by (simp add: member_inject)
haftmann@40672
    31
hide_fact (open) set_eq_iff
haftmann@39380
    32
haftmann@40672
    33
lemma set_eqI:
haftmann@37473
    34
  "member A = member B \<Longrightarrow> A = B"
haftmann@40672
    35
  by (simp add: Cset.set_eq_iff)
haftmann@40672
    36
hide_fact (open) set_eqI
haftmann@37473
    37
haftmann@34048
    38
subsection {* Lattice instantiation *}
haftmann@34048
    39
haftmann@40672
    40
instantiation Cset.set :: (type) boolean_algebra
haftmann@34048
    41
begin
haftmann@34048
    42
haftmann@40672
    43
definition less_eq_set :: "'a Cset.set \<Rightarrow> 'a Cset.set \<Rightarrow> bool" where
haftmann@34048
    44
  [simp]: "A \<le> B \<longleftrightarrow> member A \<subseteq> member B"
haftmann@34048
    45
haftmann@40672
    46
definition less_set :: "'a Cset.set \<Rightarrow> 'a Cset.set \<Rightarrow> bool" where
haftmann@34048
    47
  [simp]: "A < B \<longleftrightarrow> member A \<subset> member B"
haftmann@34048
    48
haftmann@40672
    49
definition inf_set :: "'a Cset.set \<Rightarrow> 'a Cset.set \<Rightarrow> 'a Cset.set" where
haftmann@40672
    50
  [simp]: "inf A B = Set (member A \<inter> member B)"
haftmann@34048
    51
haftmann@40672
    52
definition sup_set :: "'a Cset.set \<Rightarrow> 'a Cset.set \<Rightarrow> 'a Cset.set" where
haftmann@40672
    53
  [simp]: "sup A B = Set (member A \<union> member B)"
haftmann@34048
    54
haftmann@40672
    55
definition bot_set :: "'a Cset.set" where
haftmann@40672
    56
  [simp]: "bot = Set {}"
haftmann@34048
    57
haftmann@40672
    58
definition top_set :: "'a Cset.set" where
haftmann@40672
    59
  [simp]: "top = Set UNIV"
haftmann@34048
    60
haftmann@40672
    61
definition uminus_set :: "'a Cset.set \<Rightarrow> 'a Cset.set" where
haftmann@40672
    62
  [simp]: "- A = Set (- (member A))"
haftmann@34048
    63
haftmann@40672
    64
definition minus_set :: "'a Cset.set \<Rightarrow> 'a Cset.set \<Rightarrow> 'a Cset.set" where
haftmann@40672
    65
  [simp]: "A - B = Set (member A - member B)"
haftmann@34048
    66
haftmann@34048
    67
instance proof
haftmann@40672
    68
qed (auto intro: Cset.set_eqI)
haftmann@34048
    69
haftmann@34048
    70
end
haftmann@34048
    71
haftmann@40672
    72
instantiation Cset.set :: (type) complete_lattice
haftmann@34048
    73
begin
haftmann@34048
    74
haftmann@40672
    75
definition Inf_set :: "'a Cset.set set \<Rightarrow> 'a Cset.set" where
haftmann@40672
    76
  [simp]: "Inf_set As = Set (Inf (image member As))"
haftmann@34048
    77
haftmann@40672
    78
definition Sup_set :: "'a Cset.set set \<Rightarrow> 'a Cset.set" where
haftmann@40672
    79
  [simp]: "Sup_set As = Set (Sup (image member As))"
haftmann@34048
    80
haftmann@34048
    81
instance proof
haftmann@34048
    82
qed (auto simp add: le_fun_def le_bool_def)
haftmann@34048
    83
haftmann@34048
    84
end
haftmann@34048
    85
haftmann@37023
    86
haftmann@31807
    87
subsection {* Basic operations *}
haftmann@31807
    88
Andreas@43971
    89
abbreviation empty :: "'a Cset.set" where "empty \<equiv> bot"
Andreas@43971
    90
hide_const (open) empty
Andreas@43971
    91
Andreas@43971
    92
abbreviation UNIV :: "'a Cset.set" where "UNIV \<equiv> top"
Andreas@43971
    93
hide_const (open) UNIV
Andreas@43971
    94
haftmann@40672
    95
definition is_empty :: "'a Cset.set \<Rightarrow> bool" where
haftmann@37024
    96
  [simp]: "is_empty A \<longleftrightarrow> More_Set.is_empty (member A)"
haftmann@31807
    97
haftmann@40672
    98
definition insert :: "'a \<Rightarrow> 'a Cset.set \<Rightarrow> 'a Cset.set" where
haftmann@40672
    99
  [simp]: "insert x A = Set (Set.insert x (member A))"
haftmann@31807
   100
haftmann@40672
   101
definition remove :: "'a \<Rightarrow> 'a Cset.set \<Rightarrow> 'a Cset.set" where
haftmann@40672
   102
  [simp]: "remove x A = Set (More_Set.remove x (member A))"
haftmann@31807
   103
haftmann@40672
   104
definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a Cset.set \<Rightarrow> 'b Cset.set" where
haftmann@40672
   105
  [simp]: "map f A = Set (image f (member A))"
haftmann@31807
   106
haftmann@41505
   107
enriched_type map: map
haftmann@41372
   108
  by (simp_all add: fun_eq_iff image_compose)
haftmann@40604
   109
haftmann@40672
   110
definition filter :: "('a \<Rightarrow> bool) \<Rightarrow> 'a Cset.set \<Rightarrow> 'a Cset.set" where
haftmann@40672
   111
  [simp]: "filter P A = Set (More_Set.project P (member A))"
haftmann@31807
   112
haftmann@40672
   113
definition forall :: "('a \<Rightarrow> bool) \<Rightarrow> 'a Cset.set \<Rightarrow> bool" where
haftmann@31846
   114
  [simp]: "forall P A \<longleftrightarrow> Ball (member A) P"
haftmann@31807
   115
haftmann@40672
   116
definition exists :: "('a \<Rightarrow> bool) \<Rightarrow> 'a Cset.set \<Rightarrow> bool" where
haftmann@31846
   117
  [simp]: "exists P A \<longleftrightarrow> Bex (member A) P"
haftmann@31807
   118
haftmann@40672
   119
definition card :: "'a Cset.set \<Rightarrow> nat" where
haftmann@31849
   120
  [simp]: "card A = Finite_Set.card (member A)"
bulwahn@43241
   121
  
haftmann@34048
   122
context complete_lattice
haftmann@34048
   123
begin
haftmann@31807
   124
haftmann@40672
   125
definition Infimum :: "'a Cset.set \<Rightarrow> 'a" where
haftmann@34048
   126
  [simp]: "Infimum A = Inf (member A)"
haftmann@31807
   127
haftmann@40672
   128
definition Supremum :: "'a Cset.set \<Rightarrow> 'a" where
haftmann@34048
   129
  [simp]: "Supremum A = Sup (member A)"
haftmann@34048
   130
haftmann@34048
   131
end
haftmann@31807
   132
Andreas@43971
   133
subsection {* More operations *}
Andreas@43971
   134
Andreas@43971
   135
text {* conversion from @{typ "'a list"} *}
Andreas@43971
   136
Andreas@43971
   137
definition set :: "'a list \<Rightarrow> 'a Cset.set" where
Andreas@43971
   138
  "set xs = Set (List.set xs)"
Andreas@43971
   139
hide_const (open) set
Andreas@43971
   140
Andreas@43971
   141
text {* conversion from @{typ "'a Predicate.pred"} *}
Andreas@43971
   142
Andreas@43971
   143
definition pred_of_cset :: "'a Cset.set \<Rightarrow> 'a Predicate.pred"
Andreas@43971
   144
where [code del]: "pred_of_cset = Predicate.Pred \<circ> Cset.member"
Andreas@43971
   145
Andreas@43971
   146
definition of_pred :: "'a Predicate.pred \<Rightarrow> 'a Cset.set"
Andreas@43971
   147
where "of_pred = Cset.Set \<circ> Predicate.eval"
Andreas@43971
   148
Andreas@43971
   149
definition of_seq :: "'a Predicate.seq \<Rightarrow> 'a Cset.set"
Andreas@43971
   150
where "of_seq = of_pred \<circ> Predicate.pred_of_seq"
Andreas@43971
   151
Andreas@43971
   152
text {* monad operations *}
Andreas@43971
   153
Andreas@43971
   154
definition single :: "'a \<Rightarrow> 'a Cset.set" where
Andreas@43971
   155
  "single a = Set {a}"
Andreas@43971
   156
Andreas@43971
   157
definition bind :: "'a Cset.set \<Rightarrow> ('a \<Rightarrow> 'b Cset.set) \<Rightarrow> 'b Cset.set"
Andreas@43971
   158
                (infixl "\<guillemotright>=" 70)
Andreas@43971
   159
  where "A \<guillemotright>= f = Set (\<Union>x \<in> member A. member (f x))"
haftmann@31807
   160
haftmann@31846
   161
subsection {* Simplified simprules *}
haftmann@31846
   162
Andreas@43971
   163
lemma empty_simp [simp]: "member Cset.empty = {}"
Andreas@43971
   164
  by(simp)
Andreas@43971
   165
Andreas@43971
   166
lemma UNIV_simp [simp]: "member Cset.UNIV = UNIV"
Andreas@43971
   167
  by simp
Andreas@43971
   168
haftmann@31846
   169
lemma is_empty_simp [simp]:
haftmann@31846
   170
  "is_empty A \<longleftrightarrow> member A = {}"
haftmann@37024
   171
  by (simp add: More_Set.is_empty_def)
haftmann@31846
   172
declare is_empty_def [simp del]
haftmann@31846
   173
haftmann@31846
   174
lemma remove_simp [simp]:
haftmann@40672
   175
  "remove x A = Set (member A - {x})"
haftmann@37024
   176
  by (simp add: More_Set.remove_def)
haftmann@31846
   177
declare remove_def [simp del]
haftmann@31846
   178
haftmann@31847
   179
lemma filter_simp [simp]:
haftmann@40672
   180
  "filter P A = Set {x \<in> member A. P x}"
haftmann@37024
   181
  by (simp add: More_Set.project_def)
haftmann@31847
   182
declare filter_def [simp del]
haftmann@31846
   183
Andreas@43971
   184
lemma member_set [simp]:
Andreas@43971
   185
  "member (Cset.set xs) = set xs"
Andreas@43971
   186
  by (simp add: set_def)
Andreas@43971
   187
hide_fact (open) member_set set_def
Andreas@43971
   188
Andreas@43971
   189
lemma set_simps [simp]:
Andreas@43971
   190
  "Cset.set [] = Cset.empty"
Andreas@43971
   191
  "Cset.set (x # xs) = insert x (Cset.set xs)"
Andreas@43971
   192
by(simp_all add: Cset.set_def)
Andreas@43971
   193
Andreas@43971
   194
lemma member_SUPR [simp]:
Andreas@43971
   195
  "member (SUPR A f) = SUPR A (member \<circ> f)"
Andreas@43971
   196
unfolding SUPR_def by simp
Andreas@43971
   197
Andreas@43971
   198
lemma member_bind [simp]:
Andreas@43971
   199
  "member (P \<guillemotright>= f) = member (SUPR (member P) f)"
Andreas@43971
   200
by (simp add: bind_def Cset.set_eq_iff)
Andreas@43971
   201
Andreas@43971
   202
lemma member_single [simp]:
Andreas@43971
   203
  "member (single a) = {a}"
Andreas@43971
   204
by(simp add: single_def)
Andreas@43971
   205
Andreas@43971
   206
lemma single_sup_simps [simp]:
Andreas@43971
   207
  shows single_sup: "sup (single a) A = insert a A"
Andreas@43971
   208
  and sup_single: "sup A (single a) = insert a A"
Andreas@43971
   209
by(auto simp add: Cset.set_eq_iff)
Andreas@43971
   210
Andreas@43971
   211
lemma single_bind [simp]:
Andreas@43971
   212
  "single a \<guillemotright>= B = B a"
Andreas@43971
   213
by(simp add: bind_def single_def)
Andreas@43971
   214
Andreas@43971
   215
lemma bind_bind:
Andreas@43971
   216
  "(A \<guillemotright>= B) \<guillemotright>= C = A \<guillemotright>= (\<lambda>x. B x \<guillemotright>= C)"
Andreas@43971
   217
by(simp add: bind_def)
Andreas@43971
   218
Andreas@43971
   219
lemma bind_single [simp]:
Andreas@43971
   220
  "A \<guillemotright>= single = A"
Andreas@43971
   221
by(simp add: bind_def single_def)
Andreas@43971
   222
Andreas@43971
   223
lemma bind_const: "A \<guillemotright>= (\<lambda>_. B) = (if Cset.is_empty A then Cset.empty else B)"
Andreas@43971
   224
by(auto simp add: Cset.set_eq_iff)
Andreas@43971
   225
Andreas@43971
   226
lemma empty_bind [simp]:
Andreas@43971
   227
  "Cset.empty \<guillemotright>= f = Cset.empty"
Andreas@43971
   228
by(simp add: Cset.set_eq_iff)
Andreas@43971
   229
Andreas@43971
   230
lemma member_of_pred [simp]:
Andreas@43971
   231
  "member (of_pred P) = {x. Predicate.eval P x}"
Andreas@43971
   232
by(simp add: of_pred_def Collect_def)
Andreas@43971
   233
Andreas@43971
   234
lemma member_of_seq [simp]:
Andreas@43971
   235
  "member (of_seq xq) = {x. Predicate.member xq x}"
Andreas@43971
   236
by(simp add: of_seq_def eval_member)
Andreas@43971
   237
Andreas@43971
   238
lemma eval_pred_of_cset [simp]: 
Andreas@43971
   239
  "Predicate.eval (pred_of_cset A) = Cset.member A"
Andreas@43971
   240
by(simp add: pred_of_cset_def)
Andreas@43971
   241
Andreas@43971
   242
subsection {* Default implementations *}
Andreas@43971
   243
Andreas@43971
   244
lemma set_code [code]:
Andreas@43971
   245
  "Cset.set = foldl (\<lambda>A x. insert x A) Cset.empty"
Andreas@43971
   246
proof(rule ext, rule Cset.set_eqI)
Andreas@43971
   247
  fix xs
Andreas@43971
   248
  show "member (Cset.set xs) = member (foldl (\<lambda>A x. insert x A) Cset.empty xs)"
Andreas@43971
   249
    by(induct xs rule: rev_induct)(simp_all)
Andreas@43971
   250
qed
Andreas@43971
   251
Andreas@43971
   252
lemma single_code [code]:
Andreas@43971
   253
  "single a = insert a Cset.empty"
Andreas@43971
   254
by(simp add: Cset.single_def)
Andreas@43971
   255
Andreas@43971
   256
lemma of_pred_code [code]:
Andreas@43971
   257
  "of_pred (Predicate.Seq f) = (case f () of
Andreas@43971
   258
     Predicate.Empty \<Rightarrow> Cset.empty
Andreas@43971
   259
   | Predicate.Insert x P \<Rightarrow> Cset.insert x (of_pred P)
Andreas@43971
   260
   | Predicate.Join P xq \<Rightarrow> sup (of_pred P) (of_seq xq))"
Andreas@43971
   261
by(auto split: seq.split 
Andreas@43971
   262
        simp add: Predicate.Seq_def of_pred_def eval_member Cset.set_eq_iff)
Andreas@43971
   263
Andreas@43971
   264
lemma of_seq_code [code]:
Andreas@43971
   265
  "of_seq Predicate.Empty = Cset.empty"
Andreas@43971
   266
  "of_seq (Predicate.Insert x P) = Cset.insert x (of_pred P)"
Andreas@43971
   267
  "of_seq (Predicate.Join P xq) = sup (of_pred P) (of_seq xq)"
Andreas@43971
   268
by(auto simp add: of_seq_def of_pred_def Cset.set_eq_iff)
Andreas@43971
   269
haftmann@31846
   270
declare mem_def [simp del]
haftmann@31846
   271
Andreas@43971
   272
no_notation bind (infixl "\<guillemotright>=" 70)
haftmann@31849
   273
bulwahn@43241
   274
hide_const (open) is_empty insert remove map filter forall exists card
Andreas@43971
   275
  Inter Union bind single of_pred of_seq
Andreas@43971
   276
Andreas@43971
   277
hide_fact (open) set_def pred_of_cset_def of_pred_def of_seq_def single_def 
Andreas@43971
   278
  bind_def empty_simp UNIV_simp member_set set_simps member_SUPR member_bind 
Andreas@43971
   279
  member_single single_sup_simps single_sup sup_single single_bind
Andreas@43971
   280
  bind_bind bind_single bind_const empty_bind member_of_pred member_of_seq
Andreas@43971
   281
  eval_pred_of_cset set_code single_code of_pred_code of_seq_code
haftmann@31849
   282
haftmann@31807
   283
end