src/HOL/Library/List_Cset.thy
author hoelzl
Tue Jul 19 14:37:49 2011 +0200 (2011-07-19)
changeset 43922 c6f35921056e
parent 43307 1a32a953cef1
child 43971 892030194015
permissions -rw-r--r--
add nat => enat coercion
bulwahn@43241
     1
bulwahn@43241
     2
(* Author: Florian Haftmann, TU Muenchen *)
bulwahn@43241
     3
bulwahn@43241
     4
header {* implementation of Cset.sets based on lists *}
bulwahn@43241
     5
bulwahn@43241
     6
theory List_Cset
bulwahn@43241
     7
imports Cset
bulwahn@43241
     8
begin
bulwahn@43241
     9
bulwahn@43241
    10
declare mem_def [simp]
bulwahn@43241
    11
bulwahn@43241
    12
definition set :: "'a list \<Rightarrow> 'a Cset.set" where
bulwahn@43241
    13
  "set xs = Set (List.set xs)"
bulwahn@43241
    14
hide_const (open) set
bulwahn@43241
    15
bulwahn@43241
    16
lemma member_set [simp]:
bulwahn@43241
    17
  "member (List_Cset.set xs) = set xs"
bulwahn@43241
    18
  by (simp add: set_def)
bulwahn@43241
    19
hide_fact (open) member_set
bulwahn@43241
    20
bulwahn@43241
    21
definition coset :: "'a list \<Rightarrow> 'a Cset.set" where
bulwahn@43241
    22
  "coset xs = Set (- set xs)"
bulwahn@43241
    23
hide_const (open) coset
bulwahn@43241
    24
bulwahn@43241
    25
lemma member_coset [simp]:
bulwahn@43241
    26
  "member (List_Cset.coset xs) = - set xs"
bulwahn@43241
    27
  by (simp add: coset_def)
bulwahn@43241
    28
hide_fact (open) member_coset
bulwahn@43241
    29
bulwahn@43241
    30
code_datatype List_Cset.set List_Cset.coset
bulwahn@43241
    31
bulwahn@43241
    32
lemma member_code [code]:
bulwahn@43241
    33
  "member (List_Cset.set xs) = List.member xs"
bulwahn@43241
    34
  "member (List_Cset.coset xs) = Not \<circ> List.member xs"
bulwahn@43241
    35
  by (simp_all add: fun_eq_iff member_def fun_Compl_def bool_Compl_def)
bulwahn@43241
    36
bulwahn@43241
    37
lemma member_image_UNIV [simp]:
bulwahn@43241
    38
  "member ` UNIV = UNIV"
bulwahn@43241
    39
proof -
bulwahn@43241
    40
  have "\<And>A \<Colon> 'a set. \<exists>B \<Colon> 'a Cset.set. A = member B"
bulwahn@43241
    41
  proof
bulwahn@43241
    42
    fix A :: "'a set"
bulwahn@43241
    43
    show "A = member (Set A)" by simp
bulwahn@43241
    44
  qed
bulwahn@43241
    45
  then show ?thesis by (simp add: image_def)
bulwahn@43241
    46
qed
bulwahn@43241
    47
bulwahn@43241
    48
definition (in term_syntax)
bulwahn@43241
    49
  setify :: "'a\<Colon>typerep list \<times> (unit \<Rightarrow> Code_Evaluation.term)
bulwahn@43241
    50
    \<Rightarrow> 'a Cset.set \<times> (unit \<Rightarrow> Code_Evaluation.term)" where
bulwahn@43241
    51
  [code_unfold]: "setify xs = Code_Evaluation.valtermify List_Cset.set {\<cdot>} xs"
bulwahn@43241
    52
bulwahn@43241
    53
notation fcomp (infixl "\<circ>>" 60)
bulwahn@43241
    54
notation scomp (infixl "\<circ>\<rightarrow>" 60)
bulwahn@43241
    55
bulwahn@43241
    56
instantiation Cset.set :: (random) random
bulwahn@43241
    57
begin
bulwahn@43241
    58
bulwahn@43241
    59
definition
bulwahn@43241
    60
  "Quickcheck.random i = Quickcheck.random i \<circ>\<rightarrow> (\<lambda>xs. Pair (setify xs))"
bulwahn@43241
    61
bulwahn@43241
    62
instance ..
bulwahn@43241
    63
bulwahn@43241
    64
end
bulwahn@43241
    65
bulwahn@43241
    66
no_notation fcomp (infixl "\<circ>>" 60)
bulwahn@43241
    67
no_notation scomp (infixl "\<circ>\<rightarrow>" 60)
bulwahn@43241
    68
bulwahn@43241
    69
subsection {* Basic operations *}
bulwahn@43241
    70
bulwahn@43241
    71
lemma is_empty_set [code]:
bulwahn@43241
    72
  "Cset.is_empty (List_Cset.set xs) \<longleftrightarrow> List.null xs"
bulwahn@43241
    73
  by (simp add: is_empty_set null_def)
bulwahn@43241
    74
hide_fact (open) is_empty_set
bulwahn@43241
    75
bulwahn@43241
    76
lemma empty_set [code]:
bulwahn@43241
    77
  "bot = List_Cset.set []"
bulwahn@43241
    78
  by (simp add: set_def)
bulwahn@43241
    79
hide_fact (open) empty_set
bulwahn@43241
    80
bulwahn@43241
    81
lemma UNIV_set [code]:
bulwahn@43241
    82
  "top = List_Cset.coset []"
bulwahn@43241
    83
  by (simp add: coset_def)
bulwahn@43241
    84
hide_fact (open) UNIV_set
bulwahn@43241
    85
bulwahn@43241
    86
lemma remove_set [code]:
bulwahn@43241
    87
  "Cset.remove x (List_Cset.set xs) = List_Cset.set (removeAll x xs)"
bulwahn@43241
    88
  "Cset.remove x (List_Cset.coset xs) = List_Cset.coset (List.insert x xs)"
bulwahn@43241
    89
by (simp_all add: set_def coset_def)
bulwahn@43241
    90
  (metis List.set_insert More_Set.remove_def remove_set_compl)
bulwahn@43241
    91
bulwahn@43241
    92
lemma insert_set [code]:
bulwahn@43241
    93
  "Cset.insert x (List_Cset.set xs) = List_Cset.set (List.insert x xs)"
bulwahn@43241
    94
  "Cset.insert x (List_Cset.coset xs) = List_Cset.coset (removeAll x xs)"
bulwahn@43241
    95
  by (simp_all add: set_def coset_def)
bulwahn@43241
    96
bulwahn@43241
    97
lemma map_set [code]:
bulwahn@43241
    98
  "Cset.map f (List_Cset.set xs) = List_Cset.set (remdups (List.map f xs))"
bulwahn@43241
    99
  by (simp add: set_def)
bulwahn@43241
   100
  
bulwahn@43241
   101
lemma filter_set [code]:
bulwahn@43241
   102
  "Cset.filter P (List_Cset.set xs) = List_Cset.set (List.filter P xs)"
bulwahn@43241
   103
  by (simp add: set_def project_set)
bulwahn@43241
   104
bulwahn@43241
   105
lemma forall_set [code]:
bulwahn@43241
   106
  "Cset.forall P (List_Cset.set xs) \<longleftrightarrow> list_all P xs"
bulwahn@43241
   107
  by (simp add: set_def list_all_iff)
bulwahn@43241
   108
bulwahn@43241
   109
lemma exists_set [code]:
bulwahn@43241
   110
  "Cset.exists P (List_Cset.set xs) \<longleftrightarrow> list_ex P xs"
bulwahn@43241
   111
  by (simp add: set_def list_ex_iff)
bulwahn@43241
   112
bulwahn@43241
   113
lemma card_set [code]:
bulwahn@43241
   114
  "Cset.card (List_Cset.set xs) = length (remdups xs)"
bulwahn@43241
   115
proof -
bulwahn@43241
   116
  have "Finite_Set.card (set (remdups xs)) = length (remdups xs)"
bulwahn@43241
   117
    by (rule distinct_card) simp
bulwahn@43241
   118
  then show ?thesis by (simp add: set_def)
bulwahn@43241
   119
qed
bulwahn@43241
   120
bulwahn@43241
   121
lemma compl_set [simp, code]:
bulwahn@43241
   122
  "- List_Cset.set xs = List_Cset.coset xs"
bulwahn@43241
   123
  by (simp add: set_def coset_def)
bulwahn@43241
   124
bulwahn@43241
   125
lemma compl_coset [simp, code]:
bulwahn@43241
   126
  "- List_Cset.coset xs = List_Cset.set xs"
bulwahn@43241
   127
  by (simp add: set_def coset_def)
bulwahn@43241
   128
bulwahn@43241
   129
context complete_lattice
bulwahn@43241
   130
begin
bulwahn@43241
   131
bulwahn@43241
   132
lemma Infimum_inf [code]:
bulwahn@43241
   133
  "Infimum (List_Cset.set As) = foldr inf As top"
bulwahn@43241
   134
  "Infimum (List_Cset.coset []) = bot"
bulwahn@43241
   135
  by (simp_all add: Inf_set_foldr Inf_UNIV)
bulwahn@43241
   136
bulwahn@43241
   137
lemma Supremum_sup [code]:
bulwahn@43241
   138
  "Supremum (List_Cset.set As) = foldr sup As bot"
bulwahn@43241
   139
  "Supremum (List_Cset.coset []) = top"
bulwahn@43241
   140
  by (simp_all add: Sup_set_foldr Sup_UNIV)
bulwahn@43241
   141
bulwahn@43241
   142
end
bulwahn@43241
   143
bulwahn@43241
   144
bulwahn@43241
   145
subsection {* Derived operations *}
bulwahn@43241
   146
bulwahn@43241
   147
lemma subset_eq_forall [code]:
bulwahn@43241
   148
  "A \<le> B \<longleftrightarrow> Cset.forall (member B) A"
bulwahn@43241
   149
  by (simp add: subset_eq)
bulwahn@43241
   150
bulwahn@43241
   151
lemma subset_subset_eq [code]:
bulwahn@43241
   152
  "A < B \<longleftrightarrow> A \<le> B \<and> \<not> B \<le> (A :: 'a Cset.set)"
bulwahn@43241
   153
  by (fact less_le_not_le)
bulwahn@43241
   154
bulwahn@43241
   155
instantiation Cset.set :: (type) equal
bulwahn@43241
   156
begin
bulwahn@43241
   157
bulwahn@43241
   158
definition [code]:
bulwahn@43241
   159
  "HOL.equal A B \<longleftrightarrow> A \<le> B \<and> B \<le> (A :: 'a Cset.set)"
bulwahn@43241
   160
bulwahn@43241
   161
instance proof
bulwahn@43241
   162
qed (simp add: equal_set_def set_eq [symmetric] Cset.set_eq_iff)
bulwahn@43241
   163
bulwahn@43241
   164
end
bulwahn@43241
   165
bulwahn@43241
   166
lemma [code nbe]:
bulwahn@43241
   167
  "HOL.equal (A :: 'a Cset.set) A \<longleftrightarrow> True"
bulwahn@43241
   168
  by (fact equal_refl)
bulwahn@43241
   169
bulwahn@43241
   170
bulwahn@43241
   171
subsection {* Functorial operations *}
bulwahn@43241
   172
bulwahn@43241
   173
lemma inter_project [code]:
bulwahn@43241
   174
  "inf A (List_Cset.set xs) = List_Cset.set (List.filter (Cset.member A) xs)"
bulwahn@43241
   175
  "inf A (List_Cset.coset xs) = foldr Cset.remove xs A"
bulwahn@43241
   176
proof -
bulwahn@43241
   177
  show "inf A (List_Cset.set xs) = List_Cset.set (List.filter (member A) xs)"
bulwahn@43241
   178
    by (simp add: inter project_def set_def)
bulwahn@43241
   179
  have *: "\<And>x::'a. Cset.remove = (\<lambda>x. Set \<circ> More_Set.remove x \<circ> member)"
bulwahn@43241
   180
    by (simp add: fun_eq_iff More_Set.remove_def)
bulwahn@43241
   181
  have "member \<circ> fold (\<lambda>x. Set \<circ> More_Set.remove x \<circ> member) xs =
bulwahn@43241
   182
    fold More_Set.remove xs \<circ> member"
bulwahn@43241
   183
    by (rule fold_commute) (simp add: fun_eq_iff)
bulwahn@43241
   184
  then have "fold More_Set.remove xs (member A) = 
bulwahn@43241
   185
    member (fold (\<lambda>x. Set \<circ> More_Set.remove x \<circ> member) xs A)"
bulwahn@43241
   186
    by (simp add: fun_eq_iff)
bulwahn@43241
   187
  then have "inf A (List_Cset.coset xs) = fold Cset.remove xs A"
bulwahn@43241
   188
    by (simp add: Diff_eq [symmetric] minus_set *)
bulwahn@43241
   189
  moreover have "\<And>x y :: 'a. Cset.remove y \<circ> Cset.remove x = Cset.remove x \<circ> Cset.remove y"
bulwahn@43241
   190
    by (auto simp add: More_Set.remove_def * intro: ext)
bulwahn@43241
   191
  ultimately show "inf A (List_Cset.coset xs) = foldr Cset.remove xs A"
bulwahn@43241
   192
    by (simp add: foldr_fold)
bulwahn@43241
   193
qed
bulwahn@43241
   194
bulwahn@43241
   195
lemma subtract_remove [code]:
bulwahn@43241
   196
  "A - List_Cset.set xs = foldr Cset.remove xs A"
bulwahn@43241
   197
  "A - List_Cset.coset xs = List_Cset.set (List.filter (member A) xs)"
bulwahn@43241
   198
  by (simp_all only: diff_eq compl_set compl_coset inter_project)
bulwahn@43241
   199
bulwahn@43241
   200
lemma union_insert [code]:
bulwahn@43241
   201
  "sup (List_Cset.set xs) A = foldr Cset.insert xs A"
bulwahn@43241
   202
  "sup (List_Cset.coset xs) A = List_Cset.coset (List.filter (Not \<circ> member A) xs)"
bulwahn@43241
   203
proof -
bulwahn@43241
   204
  have *: "\<And>x::'a. Cset.insert = (\<lambda>x. Set \<circ> Set.insert x \<circ> member)"
bulwahn@43241
   205
    by (simp add: fun_eq_iff)
bulwahn@43241
   206
  have "member \<circ> fold (\<lambda>x. Set \<circ> Set.insert x \<circ> member) xs =
bulwahn@43241
   207
    fold Set.insert xs \<circ> member"
bulwahn@43241
   208
    by (rule fold_commute) (simp add: fun_eq_iff)
bulwahn@43241
   209
  then have "fold Set.insert xs (member A) =
bulwahn@43241
   210
    member (fold (\<lambda>x. Set \<circ> Set.insert x \<circ> member) xs A)"
bulwahn@43241
   211
    by (simp add: fun_eq_iff)
bulwahn@43241
   212
  then have "sup (List_Cset.set xs) A = fold Cset.insert xs A"
bulwahn@43241
   213
    by (simp add: union_set *)
bulwahn@43241
   214
  moreover have "\<And>x y :: 'a. Cset.insert y \<circ> Cset.insert x = Cset.insert x \<circ> Cset.insert y"
bulwahn@43241
   215
    by (auto simp add: * intro: ext)
bulwahn@43241
   216
  ultimately show "sup (List_Cset.set xs) A = foldr Cset.insert xs A"
bulwahn@43241
   217
    by (simp add: foldr_fold)
bulwahn@43241
   218
  show "sup (List_Cset.coset xs) A = List_Cset.coset (List.filter (Not \<circ> member A) xs)"
bulwahn@43241
   219
    by (auto simp add: coset_def)
bulwahn@43241
   220
qed
bulwahn@43241
   221
bulwahn@43307
   222
declare mem_def[simp del]
bulwahn@43307
   223
bulwahn@43241
   224
end