lib/isabelle/Why3_Set.thy

   1 theory Why3_Set
   2 imports
   3   Why3_Setup
   4   Why3_Map
   5   "HOL-Library.FSet"
   6 begin
   7
   8 section \<open> Potentially infinite sets \<close>
   9
  10 definition complement :: "('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool" where
  11   "complement S v = Not (S v)"
  12
  13 definition mapi :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> bool)" where
  14   "mapi f s x = Set.member x (image f (Collect s))"
  15
  16 definition filteri :: " ('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool" where
  17   "filteri f s x = conj (s x) (f x)"
  18
  19 definition product :: "('a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> bool) \<Rightarrow> ('a \<times> 'b \<Rightarrow> bool)" where
  20   "product s1 s2 p = conj (s1 (fst p)) (s2 (snd p))"
  21
  22 why3_open "set/Set.xml"
  23   constants
  24     empty = bot
  25     add = insert
  26     remove = Set.remove
  27     union = sup
  28     inter = inf
  29     diff = minus
  30     complement = complement
  31     pick = Eps
  32     all = top
  33     map = mapi
  34     filter = filteri
  35     product = product
  36
  37 why3_vc diffqtdef by (simp add: mem_def)
  38
  39 why3_vc interqtdef by (simp add: mem_def)
  40
  41 why3_vc is_empty_empty by (simp add: constqtdef mem_def set.Set.is_empty_def)
  42
  43 why3_vc unionqtdef by (simp add: mem_def)
  44
  45 why3_vc add_remove
  46   using assms
  47   by (simp add: fun_upd_idem_iff mem_def)
  48
  49 why3_vc remove_add by auto
  50
  51 why3_vc pick_def
  52   using assms
  53   by (auto simp add: mem_def is_empty_def intro: someI_ex)
  54
  55 why3_vc subset_diff
  56   by (simp add: mem_def diffqtdef subset_def)
  57
  58 why3_vc subset_refl
  59   by (simp add: subset_def)
  60
  61 why3_vc subset_trans
  62   using assms
  63   by (simp add: subset_def)
  64
  65 why3_vc subset_remove
  66   by (simp add: mem_def remove_def subset_def)
  67
  68 why3_vc complementqtdef
  69   by (simp add: mem_def complement_def)
  70
  71 why3_vc extensionality
  72   using assms
  73   by (auto simp add: infix_eqeq_def mem_def)
  74
  75 why3_vc mapqtdef by (simp add: mem_def mapi_def image_iff)
  76
  77 why3_vc mem_map
  78   using assms
  79   by (meson facts.mapqtdef mem_def)
  80
  81 why3_vc mem_singleton
  82   by (metis assms constqtdef fun_upd_other mem_def)
  83
  84 why3_vc empty_is_empty
  85   using assms
  86   by (meson extensionality infix_eqeq_def is_empty_empty set.Set.is_empty_def)
  87
  88 why3_vc subset_inter_1
  89   by (simp add: set.Set.subset_def mem_def)
  90
  91 why3_vc subset_inter_2
  92   by (simp add: set.Set.subset_def mem_def)
  93
  94 why3_vc subset_union_1
  95   by (simp add: set.Set.subset_def mem_def)
  96
  97 why3_vc subset_union_2
  98   by (simp add: set.Set.subset_def mem_def)
  99
 100 why3_vc disjoint_diff_eq
 101   by (smt diffqtdef disjoint_def extensionality infix_eqeq_def mem_def)
 102
 103 why3_vc disjoint_diff_s2
 104   by (simp add: disjoint_def mem_def)
 105
 106 why3_vc disjoint_inter_empty
 107   by (simp add: disjoint_def mem_def set.Set.is_empty_def)
 108
 109 why3_vc filter_def
 110   by (metis filteri_def mem_def)
 111
 112 why3_vc subset_filter
 113   by (simp add: filter_def subset_def)
 114
 115 why3_vc product_def
 116   by (simp add: product_def mem_def)
 117
 118 why3_end
 119
 120
 121 section \<open> Finite sets \<close>
 122
 123 definition fremove :: "'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where
 124   "fremove x A = A - {|x|}"
 125
 126 definition fchoose :: "'a fset \<Rightarrow> 'a" where
 127   "fchoose S = (\<some>x. x |\<in>| S)"
 128
 129 definition is_empty :: "'a fset \<Rightarrow> bool" where
 130   "is_empty S = (S = fempty)"
 131
 132 definition filter :: "'a fset \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'a fset" where
 133   "filter S p = ffilter p S"
 134
 135 why3_open "set/Fset.xml"
 136   constants
 137     mem = fmember
 138     empty = bot
 139     add = finsert
 140     remove = fremove
 141     union = sup
 142     inter = inf
 143     diff = minus
 144     choose = fchoose
 145     all = top
 146     pick = fchoose
 147     filter = filter
 148     map = fimage
 149   types
 150     fset = fset
 151
 152 why3_vc add_def by auto
 153
 154 why3_vc add_remove
 155   using assms
 156   by (auto simp add: fremove_def)
 157
 158 why3_vc remove_add by (simp add: fremove_def)
 159
 160 why3_vc map_def by auto
 161
 162 why3_vc mem_map by (simp add: assms)
 163
 164 why3_vc inter_def by simp
 165
 166 why3_vc union_def by simp
 167
 168 why3_vc remove_def by (auto simp add: fremove_def)
 169
 170 why3_vc diff_def by auto
 171
 172 why3_vc pick_def
 173   using assms
 174   by (auto simp add: fchoose_def is_empty_def intro: someI_ex)
 175
 176 why3_vc subset_diff by (simp add: Fset.subset_def)
 177
 178 why3_vc subset_refl by (simp add: Fset.subset_def)
 179
 180 why3_vc subset_trans
 181   using assms
 182   by (simp add: Fset.subset_def)
 183
 184 why3_vc subset_remove by (auto simp add: Fset.subset_def fremove_def)
 185
 186 why3_vc subset_eq
 187   using assms fcard_seteq
 188   by (metis Fset.subset_def eq_imp_le fsubsetI of_nat_eq_iff)
 189
 190 why3_vc extensionality
 191   using assms
 192   by (simp add:  Fset.infix_eqeq_def fset_eqI)
 193
 194 why3_vc cardinal1
 195 proof (cases s rule: fset_strong_cases)
 196   case 1
 197   with assms
 198   show ?thesis by (simp add: fcard_fempty)
 199 next
 200   case (2 s' x)
 201   show ?thesis
 202   proof (cases s' rule: fset_strong_cases)
 203     case 1
 204     with `s = finsert x s'` assms
 205     show ?thesis by (simp add: fchoose_def)
 206   next
 207     case (2 s'' y)
 208     with `s = finsert x s'` assms
 209     show ?thesis by (auto simp add: fcard_finsert_if fchoose_def
 210       split: if_split_asm)
 211   qed
 212 qed
 213
 214 why3_vc cardinal_add by (auto simp add: fcard_finsert_if finsert_absorb)
 215
 216 why3_vc cardinal_empty by (simp add: is_empty_def)
 217
 218 why3_vc cardinal_nonneg by simp
 219
 220 lemma cardinal_remove_in:
 221   "x |\<in>| s \<longrightarrow> int (fcard (fremove x s)) = int (fcard s) - 1"
 222   by (smt cardinal_add(2) fminus_finsert_absorb fremove_def set_finsert)
 223
 224 lemma cardinal_remove_out:
 225   "x |\<notin>| s \<longrightarrow> int (fcard (fremove x s)) = int (fcard s)"
 226   by (simp add: fremove_def)
 227
 228 why3_vc cardinal_remove by (auto simp add: cardinal_remove_out cardinal_remove_in)
 229
 230 why3_vc cardinal_subset
 231   using assms
 232   by (simp add: Fset.subset_def fcard_mono fsubsetI)
 233
 234 why3_vc filter_def by (simp add: Why3_Set.filter_def)
 235
 236 why3_vc cardinal_map
 237   apply (simp add: fcard_def card_def)
 238   by (metis card_def card_image_le finite_fset)
 239
 240 why3_vc cardinal_diff
 241   by (metis fcard_funion_fsubset fcard_mono fminus_finter2 inf.idem inf_commute inf_sup_ord(1) of_nat_diff)
 242 (*  by (smt fcard_funion_fsubset fcard_mono finter_lower1 fminus_finter2 inf.idem inf_commute int_ops(6) of_nat_mono)*)
 243
 244 why3_vc mem_singleton
 245   using assms by auto
 246
 247 why3_vc subset_filter
 248   by (simp add: Fset.subset_def Why3_Set.filter_def)
 249
 250 why3_vc cardinal_union
 251   by (smt fcard_funion_finter of_nat_add)
 252
 253 why3_vc empty_is_empty
 254   by (meson Fset.is_empty_def assms bot.extremum_uniqueI fsubsetI)
 255
 256 why3_vc is_empty_empty
 257   by (simp add: cardinal_empty)
 258
 259 why3_vc subset_inter_1
 260   by (simp add: Fset.subset_def)
 261
 262 why3_vc subset_inter_2
 263   by (simp add: Fset.subset_def)
 264
 265 why3_vc subset_union_1
 266   by (simp add: Fset.subset_def)
 267
 268 why3_vc subset_union_2
 269   by (simp add: Fset.subset_def)
 270
 271 why3_vc cardinal_filter
 272   using cardinal_subset subset_filter by blast
 273
 274 why3_vc disjoint_diff_eq
 275   by (smt Fset.disjoint_def Fset.facts.diff_def fsubsetI fsubset_antisym)
 276
 277 why3_vc  disjoint_diff_s2
 278   by (simp add: Fset.facts.disjoint_diff_eq)
 279
 280 why3_vc disjoint_inter_empty
 281   by (metis Fset.facts.disjoint_diff_eq Fset.facts.empty_is_empty Fset.facts.is_empty_empty fminus_disjoint fminus_triv)
 282
 283 why3_vc cardinal_inter_disjoint
 284   by (meson Fset.facts.disjoint_inter_empty assms cardinal_empty)
 285
 286 why3_end
 287
 288 end