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