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