src/HOL/Library/RBT_Set.thy
author kuncar
Tue Oct 09 16:57:58 2012 +0200 (2012-10-09)
changeset 49757 73ab6d4a9236
parent 48623 bea613f2543d
child 49758 718f10c8bbfc
permissions -rw-r--r--
rename Set.project to Set.filter - more appropriate name
kuncar@48623
     1
(*  Title:      HOL/Library/RBT_Set.thy
kuncar@48623
     2
    Author:     Ondrej Kuncar
kuncar@48623
     3
*)
kuncar@48623
     4
kuncar@48623
     5
header {* Implementation of sets using RBT trees *}
kuncar@48623
     6
kuncar@48623
     7
theory RBT_Set
kuncar@48623
     8
imports RBT Product_ord
kuncar@48623
     9
begin
kuncar@48623
    10
kuncar@48623
    11
(*
kuncar@48623
    12
  Users should be aware that by including this file all code equations
kuncar@48623
    13
  outside of List.thy using 'a list as an implenentation of sets cannot be
kuncar@48623
    14
  used for code generation. If such equations are not needed, they can be
kuncar@48623
    15
  deleted from the code generator. Otherwise, a user has to provide their 
kuncar@48623
    16
  own equations using RBT trees. 
kuncar@48623
    17
*)
kuncar@48623
    18
kuncar@48623
    19
section {* Definition of code datatype constructors *}
kuncar@48623
    20
kuncar@48623
    21
definition Set :: "('a\<Colon>linorder, unit) rbt \<Rightarrow> 'a set" 
kuncar@48623
    22
  where "Set t = {x . lookup t x = Some ()}"
kuncar@48623
    23
kuncar@48623
    24
definition Coset :: "('a\<Colon>linorder, unit) rbt \<Rightarrow> 'a set" 
kuncar@48623
    25
  where [simp]: "Coset t = - Set t"
kuncar@48623
    26
kuncar@48623
    27
kuncar@48623
    28
section {* Deletion of already existing code equations *}
kuncar@48623
    29
kuncar@48623
    30
lemma [code, code del]:
kuncar@48623
    31
  "Set.empty = Set.empty" ..
kuncar@48623
    32
kuncar@48623
    33
lemma [code, code del]:
kuncar@48623
    34
  "Set.is_empty = Set.is_empty" ..
kuncar@48623
    35
kuncar@48623
    36
lemma [code, code del]:
kuncar@48623
    37
  "uminus_set_inst.uminus_set = uminus_set_inst.uminus_set" ..
kuncar@48623
    38
kuncar@48623
    39
lemma [code, code del]:
kuncar@48623
    40
  "Set.member = Set.member" ..
kuncar@48623
    41
kuncar@48623
    42
lemma [code, code del]:
kuncar@48623
    43
  "Set.insert = Set.insert" ..
kuncar@48623
    44
kuncar@48623
    45
lemma [code, code del]:
kuncar@48623
    46
  "Set.remove = Set.remove" ..
kuncar@48623
    47
kuncar@48623
    48
lemma [code, code del]:
kuncar@48623
    49
  "UNIV = UNIV" ..
kuncar@48623
    50
kuncar@48623
    51
lemma [code, code del]:
kuncar@49757
    52
  "Set.filter = Set.filter" ..
kuncar@48623
    53
kuncar@48623
    54
lemma [code, code del]:
kuncar@48623
    55
  "image = image" ..
kuncar@48623
    56
kuncar@48623
    57
lemma [code, code del]:
kuncar@48623
    58
  "Set.subset_eq = Set.subset_eq" ..
kuncar@48623
    59
kuncar@48623
    60
lemma [code, code del]:
kuncar@48623
    61
  "Ball = Ball" ..
kuncar@48623
    62
kuncar@48623
    63
lemma [code, code del]:
kuncar@48623
    64
  "Bex = Bex" ..
kuncar@48623
    65
kuncar@48623
    66
lemma [code, code del]:
kuncar@48623
    67
  "Set.union = Set.union" ..
kuncar@48623
    68
kuncar@48623
    69
lemma [code, code del]:
kuncar@48623
    70
  "minus_set_inst.minus_set = minus_set_inst.minus_set" ..
kuncar@48623
    71
kuncar@48623
    72
lemma [code, code del]:
kuncar@48623
    73
  "Set.inter = Set.inter" ..
kuncar@48623
    74
kuncar@48623
    75
lemma [code, code del]:
kuncar@48623
    76
  "card = card" ..
kuncar@48623
    77
kuncar@48623
    78
lemma [code, code del]:
kuncar@48623
    79
  "the_elem = the_elem" ..
kuncar@48623
    80
kuncar@48623
    81
lemma [code, code del]:
kuncar@48623
    82
  "Pow = Pow" ..
kuncar@48623
    83
kuncar@48623
    84
lemma [code, code del]:
kuncar@48623
    85
  "setsum = setsum" ..
kuncar@48623
    86
kuncar@48623
    87
lemma [code, code del]:
kuncar@48623
    88
  "Product_Type.product = Product_Type.product"  ..
kuncar@48623
    89
kuncar@48623
    90
lemma [code, code del]:
kuncar@48623
    91
  "Id_on = Id_on" ..
kuncar@48623
    92
kuncar@48623
    93
lemma [code, code del]:
kuncar@48623
    94
  "Image = Image" ..
kuncar@48623
    95
kuncar@48623
    96
lemma [code, code del]:
kuncar@48623
    97
  "trancl = trancl" ..
kuncar@48623
    98
kuncar@48623
    99
lemma [code, code del]:
kuncar@48623
   100
  "relcomp = relcomp" ..
kuncar@48623
   101
kuncar@48623
   102
lemma [code, code del]:
kuncar@48623
   103
  "wf = wf" ..
kuncar@48623
   104
kuncar@48623
   105
lemma [code, code del]:
kuncar@48623
   106
  "Min = Min" ..
kuncar@48623
   107
kuncar@48623
   108
lemma [code, code del]:
kuncar@48623
   109
  "Inf_fin = Inf_fin" ..
kuncar@48623
   110
kuncar@48623
   111
lemma [code, code del]:
kuncar@48623
   112
  "INFI = INFI" ..
kuncar@48623
   113
kuncar@48623
   114
lemma [code, code del]:
kuncar@48623
   115
  "Max = Max" ..
kuncar@48623
   116
kuncar@48623
   117
lemma [code, code del]:
kuncar@48623
   118
  "Sup_fin = Sup_fin" ..
kuncar@48623
   119
kuncar@48623
   120
lemma [code, code del]:
kuncar@48623
   121
  "SUPR = SUPR" ..
kuncar@48623
   122
kuncar@48623
   123
lemma [code, code del]:
kuncar@48623
   124
  "(Inf :: 'a set set \<Rightarrow> 'a set) = Inf" ..
kuncar@48623
   125
kuncar@48623
   126
lemma [code, code del]:
kuncar@48623
   127
  "(Sup :: 'a set set \<Rightarrow> 'a set) = Sup" ..
kuncar@48623
   128
kuncar@48623
   129
lemma [code, code del]:
kuncar@48623
   130
  "sorted_list_of_set = sorted_list_of_set" ..
kuncar@48623
   131
kuncar@48623
   132
lemma [code, code del]: 
kuncar@48623
   133
  "List.map_project = List.map_project" ..
kuncar@48623
   134
kuncar@48623
   135
section {* Lemmas *}
kuncar@48623
   136
kuncar@48623
   137
kuncar@48623
   138
subsection {* Auxiliary lemmas *}
kuncar@48623
   139
kuncar@48623
   140
lemma [simp]: "x \<noteq> Some () \<longleftrightarrow> x = None"
kuncar@48623
   141
by (auto simp: not_Some_eq[THEN iffD1])
kuncar@48623
   142
kuncar@48623
   143
lemma finite_Set [simp, intro!]: "finite (Set x)"
kuncar@48623
   144
proof -
kuncar@48623
   145
  have "Set x = dom (lookup x)" by (auto simp: Set_def)
kuncar@48623
   146
  then show ?thesis by simp
kuncar@48623
   147
qed
kuncar@48623
   148
kuncar@48623
   149
lemma set_keys: "Set t = set(keys t)"
kuncar@48623
   150
proof -
kuncar@48623
   151
 have "\<And>k. ((k, ()) \<in> set (entries t)) = (k \<in> set (keys t))" 
kuncar@48623
   152
    by (simp add: keys_entries)
kuncar@48623
   153
  then show ?thesis by (auto simp: lookup_in_tree Set_def)
kuncar@48623
   154
qed
kuncar@48623
   155
kuncar@48623
   156
subsection {* fold and filter *}
kuncar@48623
   157
kuncar@48623
   158
lemma finite_fold_rbt_fold_eq:
kuncar@48623
   159
  assumes "comp_fun_commute f" 
kuncar@48623
   160
  shows "Finite_Set.fold f A (set(entries t)) = fold (curry f) t A"
kuncar@48623
   161
proof -
kuncar@48623
   162
  have *: "remdups (entries t) = entries t"
kuncar@48623
   163
    using distinct_entries distinct_map by (auto intro: distinct_remdups_id)
kuncar@48623
   164
  show ?thesis using assms by (auto simp: fold_def_alt comp_fun_commute.fold_set_fold_remdups *)
kuncar@48623
   165
qed
kuncar@48623
   166
kuncar@48623
   167
definition fold_keys :: "('a :: linorder \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a, _) rbt \<Rightarrow> 'b \<Rightarrow> 'b" 
kuncar@48623
   168
  where [code_unfold]:"fold_keys f t A = fold (\<lambda>k _ t. f k t) t A"
kuncar@48623
   169
kuncar@48623
   170
lemma fold_keys_def_alt:
kuncar@48623
   171
  "fold_keys f t s = List.fold f (keys t) s"
kuncar@48623
   172
by (auto simp: fold_map o_def split_def fold_def_alt keys_def_alt fold_keys_def)
kuncar@48623
   173
kuncar@48623
   174
lemma finite_fold_fold_keys:
kuncar@48623
   175
  assumes "comp_fun_commute f"
kuncar@48623
   176
  shows "Finite_Set.fold f A (Set t) = fold_keys f t A"
kuncar@48623
   177
using assms
kuncar@48623
   178
proof -
kuncar@48623
   179
  interpret comp_fun_commute f by fact
kuncar@48623
   180
  have "set (keys t) = fst ` (set (entries t))" by (auto simp: fst_eq_Domain keys_entries)
kuncar@48623
   181
  moreover have "inj_on fst (set (entries t))" using distinct_entries distinct_map by auto
kuncar@48623
   182
  ultimately show ?thesis 
kuncar@48623
   183
    by (auto simp add: set_keys fold_keys_def curry_def fold_image finite_fold_rbt_fold_eq 
kuncar@48623
   184
      comp_comp_fun_commute)
kuncar@48623
   185
qed
kuncar@48623
   186
kuncar@48623
   187
definition rbt_filter :: "('a :: linorder \<Rightarrow> bool) \<Rightarrow> ('a, 'b) rbt \<Rightarrow> 'a set" where
kuncar@48623
   188
  "rbt_filter P t = fold (\<lambda>k _ A'. if P k then Set.insert k A' else A') t {}"
kuncar@48623
   189
kuncar@48623
   190
lemma finite_filter_rbt_filter:
kuncar@48623
   191
  "Finite_Set.filter P (Set t) = rbt_filter P t"
kuncar@48623
   192
by (simp add: fold_keys_def Finite_Set.filter_def rbt_filter_def 
kuncar@48623
   193
  finite_fold_fold_keys[OF comp_fun_commute_filter_fold])
kuncar@48623
   194
kuncar@48623
   195
kuncar@48623
   196
subsection {* foldi and Ball *}
kuncar@48623
   197
kuncar@48623
   198
lemma Ball_False: "RBT_Impl.fold (\<lambda>k v s. s \<and> P k) t False = False"
kuncar@48623
   199
by (induction t) auto
kuncar@48623
   200
kuncar@48623
   201
lemma rbt_foldi_fold_conj: 
kuncar@48623
   202
  "RBT_Impl.foldi (\<lambda>s. s = True) (\<lambda>k v s. s \<and> P k) t val = RBT_Impl.fold (\<lambda>k v s. s \<and> P k) t val"
kuncar@48623
   203
proof (induction t arbitrary: val) 
kuncar@48623
   204
  case (Branch c t1) then show ?case
kuncar@48623
   205
    by (cases "RBT_Impl.fold (\<lambda>k v s. s \<and> P k) t1 True") (simp_all add: Ball_False) 
kuncar@48623
   206
qed simp
kuncar@48623
   207
kuncar@48623
   208
lemma foldi_fold_conj: "foldi (\<lambda>s. s = True) (\<lambda>k v s. s \<and> P k) t val = fold_keys (\<lambda>k s. s \<and> P k) t val"
kuncar@48623
   209
unfolding fold_keys_def by transfer (rule rbt_foldi_fold_conj)
kuncar@48623
   210
kuncar@48623
   211
kuncar@48623
   212
subsection {* foldi and Bex *}
kuncar@48623
   213
kuncar@48623
   214
lemma Bex_True: "RBT_Impl.fold (\<lambda>k v s. s \<or> P k) t True = True"
kuncar@48623
   215
by (induction t) auto
kuncar@48623
   216
kuncar@48623
   217
lemma rbt_foldi_fold_disj: 
kuncar@48623
   218
  "RBT_Impl.foldi (\<lambda>s. s = False) (\<lambda>k v s. s \<or> P k) t val = RBT_Impl.fold (\<lambda>k v s. s \<or> P k) t val"
kuncar@48623
   219
proof (induction t arbitrary: val) 
kuncar@48623
   220
  case (Branch c t1) then show ?case
kuncar@48623
   221
    by (cases "RBT_Impl.fold (\<lambda>k v s. s \<or> P k) t1 False") (simp_all add: Bex_True) 
kuncar@48623
   222
qed simp
kuncar@48623
   223
kuncar@48623
   224
lemma foldi_fold_disj: "foldi (\<lambda>s. s = False) (\<lambda>k v s. s \<or> P k) t val = fold_keys (\<lambda>k s. s \<or> P k) t val"
kuncar@48623
   225
unfolding fold_keys_def by transfer (rule rbt_foldi_fold_disj)
kuncar@48623
   226
kuncar@48623
   227
kuncar@48623
   228
subsection {* folding over non empty trees and selecting the minimal and maximal element *}
kuncar@48623
   229
kuncar@48623
   230
(** concrete **)
kuncar@48623
   231
kuncar@48623
   232
(* The concrete part is here because it's probably not general enough to be moved to RBT_Impl *)
kuncar@48623
   233
kuncar@48623
   234
definition rbt_fold1_keys :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> ('a::linorder, 'b) RBT_Impl.rbt \<Rightarrow> 'a" 
kuncar@48623
   235
  where "rbt_fold1_keys f t = List.fold f (tl(RBT_Impl.keys t)) (hd(RBT_Impl.keys t))"
kuncar@48623
   236
kuncar@48623
   237
(* minimum *)
kuncar@48623
   238
kuncar@48623
   239
definition rbt_min :: "('a::linorder, unit) RBT_Impl.rbt \<Rightarrow> 'a" 
kuncar@48623
   240
  where "rbt_min t = rbt_fold1_keys min t"
kuncar@48623
   241
kuncar@48623
   242
lemma key_le_right: "rbt_sorted (Branch c lt k v rt) \<Longrightarrow> (\<And>x. x \<in>set (RBT_Impl.keys rt) \<Longrightarrow> k \<le> x)"
kuncar@48623
   243
by  (auto simp: rbt_greater_prop less_imp_le)
kuncar@48623
   244
kuncar@48623
   245
lemma left_le_key: "rbt_sorted (Branch c lt k v rt) \<Longrightarrow> (\<And>x. x \<in>set (RBT_Impl.keys lt) \<Longrightarrow> x \<le> k)"
kuncar@48623
   246
by (auto simp: rbt_less_prop less_imp_le)
kuncar@48623
   247
kuncar@48623
   248
lemma fold_min_triv:
kuncar@48623
   249
  fixes k :: "_ :: linorder"
kuncar@48623
   250
  shows "(\<forall>x\<in>set xs. k \<le> x) \<Longrightarrow> List.fold min xs k = k" 
kuncar@48623
   251
by (induct xs) (auto simp add: min_def)
kuncar@48623
   252
kuncar@48623
   253
lemma rbt_min_simps:
kuncar@48623
   254
  "is_rbt (Branch c RBT_Impl.Empty k v rt) \<Longrightarrow> rbt_min (Branch c RBT_Impl.Empty k v rt) = k"
kuncar@48623
   255
by (auto intro: fold_min_triv dest: key_le_right is_rbt_rbt_sorted simp: rbt_fold1_keys_def rbt_min_def)
kuncar@48623
   256
kuncar@48623
   257
fun rbt_min_opt where
kuncar@48623
   258
  "rbt_min_opt (Branch c RBT_Impl.Empty k v rt) = k" |
kuncar@48623
   259
  "rbt_min_opt (Branch c (Branch lc llc lk lv lrt) k v rt) = rbt_min_opt (Branch lc llc lk lv lrt)"
kuncar@48623
   260
kuncar@48623
   261
lemma rbt_min_opt_Branch:
kuncar@48623
   262
  "t1 \<noteq> rbt.Empty \<Longrightarrow> rbt_min_opt (Branch c t1 k () t2) = rbt_min_opt t1" 
kuncar@48623
   263
by (cases t1) auto
kuncar@48623
   264
kuncar@48623
   265
lemma rbt_min_opt_induct [case_names empty left_empty left_non_empty]:
kuncar@48623
   266
  fixes t :: "('a :: linorder, unit) RBT_Impl.rbt"
kuncar@48623
   267
  assumes "P rbt.Empty"
kuncar@48623
   268
  assumes "\<And>color t1 a b t2. P t1 \<Longrightarrow> P t2 \<Longrightarrow> t1 = rbt.Empty \<Longrightarrow> P (Branch color t1 a b t2)"
kuncar@48623
   269
  assumes "\<And>color t1 a b t2. P t1 \<Longrightarrow> P t2 \<Longrightarrow> t1 \<noteq> rbt.Empty \<Longrightarrow> P (Branch color t1 a b t2)"
kuncar@48623
   270
  shows "P t"
kuncar@48623
   271
using assms
kuncar@48623
   272
  apply (induction t)
kuncar@48623
   273
  apply simp
kuncar@48623
   274
  apply (case_tac "t1 = rbt.Empty")
kuncar@48623
   275
  apply simp_all
kuncar@48623
   276
done
kuncar@48623
   277
kuncar@48623
   278
lemma rbt_min_opt_in_set: 
kuncar@48623
   279
  fixes t :: "('a :: linorder, unit) RBT_Impl.rbt"
kuncar@48623
   280
  assumes "t \<noteq> rbt.Empty"
kuncar@48623
   281
  shows "rbt_min_opt t \<in> set (RBT_Impl.keys t)"
kuncar@48623
   282
using assms by (induction t rule: rbt_min_opt.induct) (auto)
kuncar@48623
   283
kuncar@48623
   284
lemma rbt_min_opt_is_min:
kuncar@48623
   285
  fixes t :: "('a :: linorder, unit) RBT_Impl.rbt"
kuncar@48623
   286
  assumes "rbt_sorted t"
kuncar@48623
   287
  assumes "t \<noteq> rbt.Empty"
kuncar@48623
   288
  shows "\<And>y. y \<in> set (RBT_Impl.keys t) \<Longrightarrow> y \<ge> rbt_min_opt t"
kuncar@48623
   289
using assms 
kuncar@48623
   290
proof (induction t rule: rbt_min_opt_induct)
kuncar@48623
   291
  case empty
kuncar@48623
   292
    then show ?case by simp
kuncar@48623
   293
next
kuncar@48623
   294
  case left_empty
kuncar@48623
   295
    then show ?case by (auto intro: key_le_right simp del: rbt_sorted.simps)
kuncar@48623
   296
next
kuncar@48623
   297
  case (left_non_empty c t1 k v t2 y)
kuncar@48623
   298
    then have "y = k \<or> y \<in> set (RBT_Impl.keys t1) \<or> y \<in> set (RBT_Impl.keys t2)" by auto
kuncar@48623
   299
    with left_non_empty show ?case 
kuncar@48623
   300
    proof(elim disjE)
kuncar@48623
   301
      case goal1 then show ?case 
kuncar@48623
   302
        by (auto simp add: rbt_min_opt_Branch intro: left_le_key rbt_min_opt_in_set)
kuncar@48623
   303
    next
kuncar@48623
   304
      case goal2 with left_non_empty show ?case by (auto simp add: rbt_min_opt_Branch)
kuncar@48623
   305
    next 
kuncar@48623
   306
      case goal3 show ?case
kuncar@48623
   307
      proof -
kuncar@48623
   308
        from goal3 have "rbt_min_opt t1 \<le> k" by (simp add: left_le_key rbt_min_opt_in_set)
kuncar@48623
   309
        moreover from goal3 have "k \<le> y" by (simp add: key_le_right)
kuncar@48623
   310
        ultimately show ?thesis using goal3 by (simp add: rbt_min_opt_Branch)
kuncar@48623
   311
      qed
kuncar@48623
   312
    qed
kuncar@48623
   313
qed
kuncar@48623
   314
kuncar@48623
   315
lemma rbt_min_eq_rbt_min_opt:
kuncar@48623
   316
  assumes "t \<noteq> RBT_Impl.Empty"
kuncar@48623
   317
  assumes "is_rbt t"
kuncar@48623
   318
  shows "rbt_min t = rbt_min_opt t"
kuncar@48623
   319
proof -
kuncar@48623
   320
  interpret ab_semigroup_idem_mult "(min :: 'a \<Rightarrow> 'a \<Rightarrow> 'a)" using ab_semigroup_idem_mult_min
kuncar@48623
   321
    unfolding class.ab_semigroup_idem_mult_def by blast
kuncar@48623
   322
  show ?thesis
kuncar@48623
   323
    by (simp add: Min_eqI rbt_min_opt_is_min rbt_min_opt_in_set assms Min_def[symmetric]
kuncar@48623
   324
      non_empty_rbt_keys fold1_set_fold[symmetric] rbt_min_def rbt_fold1_keys_def)
kuncar@48623
   325
qed
kuncar@48623
   326
kuncar@48623
   327
(* maximum *)
kuncar@48623
   328
kuncar@48623
   329
definition rbt_max :: "('a::linorder, unit) RBT_Impl.rbt \<Rightarrow> 'a" 
kuncar@48623
   330
  where "rbt_max t = rbt_fold1_keys max t"
kuncar@48623
   331
kuncar@48623
   332
lemma fold_max_triv:
kuncar@48623
   333
  fixes k :: "_ :: linorder"
kuncar@48623
   334
  shows "(\<forall>x\<in>set xs. x \<le> k) \<Longrightarrow> List.fold max xs k = k" 
kuncar@48623
   335
by (induct xs) (auto simp add: max_def)
kuncar@48623
   336
kuncar@48623
   337
lemma fold_max_rev_eq:
kuncar@48623
   338
  fixes xs :: "('a :: linorder) list"
kuncar@48623
   339
  assumes "xs \<noteq> []"
kuncar@48623
   340
  shows "List.fold max (tl xs) (hd xs) = List.fold max (tl (rev xs)) (hd (rev xs))" 
kuncar@48623
   341
proof -
kuncar@48623
   342
  interpret ab_semigroup_idem_mult "(max :: 'a \<Rightarrow> 'a \<Rightarrow> 'a)" using ab_semigroup_idem_mult_max
kuncar@48623
   343
    unfolding class.ab_semigroup_idem_mult_def by blast
kuncar@48623
   344
  show ?thesis
kuncar@48623
   345
  using assms by (auto simp add: fold1_set_fold[symmetric])
kuncar@48623
   346
qed
kuncar@48623
   347
kuncar@48623
   348
lemma rbt_max_simps:
kuncar@48623
   349
  assumes "is_rbt (Branch c lt k v RBT_Impl.Empty)" 
kuncar@48623
   350
  shows "rbt_max (Branch c lt k v RBT_Impl.Empty) = k"
kuncar@48623
   351
proof -
kuncar@48623
   352
  have "List.fold max (tl (rev(RBT_Impl.keys lt @ [k]))) (hd (rev(RBT_Impl.keys lt @ [k]))) = k"
kuncar@48623
   353
    using assms by (auto intro!: fold_max_triv dest!: left_le_key is_rbt_rbt_sorted)
kuncar@48623
   354
  then show ?thesis by (auto simp add: rbt_max_def rbt_fold1_keys_def fold_max_rev_eq)
kuncar@48623
   355
qed
kuncar@48623
   356
kuncar@48623
   357
fun rbt_max_opt where
kuncar@48623
   358
  "rbt_max_opt (Branch c lt k v RBT_Impl.Empty) = k" |
kuncar@48623
   359
  "rbt_max_opt (Branch c lt k v (Branch rc rlc rk rv rrt)) = rbt_max_opt (Branch rc rlc rk rv rrt)"
kuncar@48623
   360
kuncar@48623
   361
lemma rbt_max_opt_Branch:
kuncar@48623
   362
  "t2 \<noteq> rbt.Empty \<Longrightarrow> rbt_max_opt (Branch c t1 k () t2) = rbt_max_opt t2" 
kuncar@48623
   363
by (cases t2) auto
kuncar@48623
   364
kuncar@48623
   365
lemma rbt_max_opt_induct [case_names empty right_empty right_non_empty]:
kuncar@48623
   366
  fixes t :: "('a :: linorder, unit) RBT_Impl.rbt"
kuncar@48623
   367
  assumes "P rbt.Empty"
kuncar@48623
   368
  assumes "\<And>color t1 a b t2. P t1 \<Longrightarrow> P t2 \<Longrightarrow> t2 = rbt.Empty \<Longrightarrow> P (Branch color t1 a b t2)"
kuncar@48623
   369
  assumes "\<And>color t1 a b t2. P t1 \<Longrightarrow> P t2 \<Longrightarrow> t2 \<noteq> rbt.Empty \<Longrightarrow> P (Branch color t1 a b t2)"
kuncar@48623
   370
  shows "P t"
kuncar@48623
   371
using assms
kuncar@48623
   372
  apply (induction t)
kuncar@48623
   373
  apply simp
kuncar@48623
   374
  apply (case_tac "t2 = rbt.Empty")
kuncar@48623
   375
  apply simp_all
kuncar@48623
   376
done
kuncar@48623
   377
kuncar@48623
   378
lemma rbt_max_opt_in_set: 
kuncar@48623
   379
  fixes t :: "('a :: linorder, unit) RBT_Impl.rbt"
kuncar@48623
   380
  assumes "t \<noteq> rbt.Empty"
kuncar@48623
   381
  shows "rbt_max_opt t \<in> set (RBT_Impl.keys t)"
kuncar@48623
   382
using assms by (induction t rule: rbt_max_opt.induct) (auto)
kuncar@48623
   383
kuncar@48623
   384
lemma rbt_max_opt_is_max:
kuncar@48623
   385
  fixes t :: "('a :: linorder, unit) RBT_Impl.rbt"
kuncar@48623
   386
  assumes "rbt_sorted t"
kuncar@48623
   387
  assumes "t \<noteq> rbt.Empty"
kuncar@48623
   388
  shows "\<And>y. y \<in> set (RBT_Impl.keys t) \<Longrightarrow> y \<le> rbt_max_opt t"
kuncar@48623
   389
using assms 
kuncar@48623
   390
proof (induction t rule: rbt_max_opt_induct)
kuncar@48623
   391
  case empty
kuncar@48623
   392
    then show ?case by simp
kuncar@48623
   393
next
kuncar@48623
   394
  case right_empty
kuncar@48623
   395
    then show ?case by (auto intro: left_le_key simp del: rbt_sorted.simps)
kuncar@48623
   396
next
kuncar@48623
   397
  case (right_non_empty c t1 k v t2 y)
kuncar@48623
   398
    then have "y = k \<or> y \<in> set (RBT_Impl.keys t2) \<or> y \<in> set (RBT_Impl.keys t1)" by auto
kuncar@48623
   399
    with right_non_empty show ?case 
kuncar@48623
   400
    proof(elim disjE)
kuncar@48623
   401
      case goal1 then show ?case 
kuncar@48623
   402
        by (auto simp add: rbt_max_opt_Branch intro: key_le_right rbt_max_opt_in_set)
kuncar@48623
   403
    next
kuncar@48623
   404
      case goal2 with right_non_empty show ?case by (auto simp add: rbt_max_opt_Branch)
kuncar@48623
   405
    next 
kuncar@48623
   406
      case goal3 show ?case
kuncar@48623
   407
      proof -
kuncar@48623
   408
        from goal3 have "rbt_max_opt t2 \<ge> k" by (simp add: key_le_right rbt_max_opt_in_set)
kuncar@48623
   409
        moreover from goal3 have "y \<le> k" by (simp add: left_le_key)
kuncar@48623
   410
        ultimately show ?thesis using goal3 by (simp add: rbt_max_opt_Branch)
kuncar@48623
   411
      qed
kuncar@48623
   412
    qed
kuncar@48623
   413
qed
kuncar@48623
   414
kuncar@48623
   415
lemma rbt_max_eq_rbt_max_opt:
kuncar@48623
   416
  assumes "t \<noteq> RBT_Impl.Empty"
kuncar@48623
   417
  assumes "is_rbt t"
kuncar@48623
   418
  shows "rbt_max t = rbt_max_opt t"
kuncar@48623
   419
proof -
kuncar@48623
   420
  interpret ab_semigroup_idem_mult "(max :: 'a \<Rightarrow> 'a \<Rightarrow> 'a)" using ab_semigroup_idem_mult_max
kuncar@48623
   421
    unfolding class.ab_semigroup_idem_mult_def by blast
kuncar@48623
   422
  show ?thesis
kuncar@48623
   423
    by (simp add: Max_eqI rbt_max_opt_is_max rbt_max_opt_in_set assms Max_def[symmetric]
kuncar@48623
   424
      non_empty_rbt_keys fold1_set_fold[symmetric] rbt_max_def rbt_fold1_keys_def)
kuncar@48623
   425
qed
kuncar@48623
   426
kuncar@48623
   427
kuncar@48623
   428
(** abstract **)
kuncar@48623
   429
kuncar@48623
   430
lift_definition fold1_keys :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> ('a::linorder, 'b) rbt \<Rightarrow> 'a"
kuncar@48623
   431
  is rbt_fold1_keys by simp
kuncar@48623
   432
kuncar@48623
   433
lemma fold1_keys_def_alt:
kuncar@48623
   434
  "fold1_keys f t = List.fold f (tl(keys t)) (hd(keys t))"
kuncar@48623
   435
  by transfer (simp add: rbt_fold1_keys_def)
kuncar@48623
   436
kuncar@48623
   437
lemma finite_fold1_fold1_keys:
kuncar@48623
   438
  assumes "class.ab_semigroup_mult f"
kuncar@48623
   439
  assumes "\<not> (is_empty t)"
kuncar@48623
   440
  shows "Finite_Set.fold1 f (Set t) = fold1_keys f t"
kuncar@48623
   441
proof -
kuncar@48623
   442
  interpret ab_semigroup_mult f by fact
kuncar@48623
   443
  show ?thesis using assms 
kuncar@48623
   444
    by (auto simp: fold1_keys_def_alt set_keys fold_def_alt fold1_distinct_set_fold non_empty_keys)
kuncar@48623
   445
qed
kuncar@48623
   446
kuncar@48623
   447
(* minimum *)
kuncar@48623
   448
kuncar@48623
   449
lift_definition r_min :: "('a :: linorder, unit) rbt \<Rightarrow> 'a" is rbt_min by simp
kuncar@48623
   450
kuncar@48623
   451
lift_definition r_min_opt :: "('a :: linorder, unit) rbt \<Rightarrow> 'a" is rbt_min_opt by simp
kuncar@48623
   452
kuncar@48623
   453
lemma r_min_alt_def: "r_min t = fold1_keys min t"
kuncar@48623
   454
by transfer (simp add: rbt_min_def)
kuncar@48623
   455
kuncar@48623
   456
lemma r_min_eq_r_min_opt:
kuncar@48623
   457
  assumes "\<not> (is_empty t)"
kuncar@48623
   458
  shows "r_min t = r_min_opt t"
kuncar@48623
   459
using assms unfolding is_empty_empty by transfer (auto intro: rbt_min_eq_rbt_min_opt)
kuncar@48623
   460
kuncar@48623
   461
lemma fold_keys_min_top_eq:
kuncar@48623
   462
  fixes t :: "('a :: {linorder, bounded_lattice_top}, unit) rbt"
kuncar@48623
   463
  assumes "\<not> (is_empty t)"
kuncar@48623
   464
  shows "fold_keys min t top = fold1_keys min t"
kuncar@48623
   465
proof -
kuncar@48623
   466
  have *: "\<And>t. RBT_Impl.keys t \<noteq> [] \<Longrightarrow> List.fold min (RBT_Impl.keys t) top = 
kuncar@48623
   467
    List.fold min (hd(RBT_Impl.keys t) # tl(RBT_Impl.keys t)) top"
kuncar@48623
   468
    by (simp add: hd_Cons_tl[symmetric])
kuncar@48623
   469
  { fix x :: "_ :: {linorder, bounded_lattice_top}" and xs
kuncar@48623
   470
    have "List.fold min (x#xs) top = List.fold min xs x"
kuncar@48623
   471
    by (simp add: inf_min[symmetric])
kuncar@48623
   472
  } note ** = this
kuncar@48623
   473
  show ?thesis using assms
kuncar@48623
   474
    unfolding fold_keys_def_alt fold1_keys_def_alt is_empty_empty
kuncar@48623
   475
    apply transfer 
kuncar@48623
   476
    apply (case_tac t) 
kuncar@48623
   477
    apply simp 
kuncar@48623
   478
    apply (subst *)
kuncar@48623
   479
    apply simp
kuncar@48623
   480
    apply (subst **)
kuncar@48623
   481
    apply simp
kuncar@48623
   482
  done
kuncar@48623
   483
qed
kuncar@48623
   484
kuncar@48623
   485
(* maximum *)
kuncar@48623
   486
kuncar@48623
   487
lift_definition r_max :: "('a :: linorder, unit) rbt \<Rightarrow> 'a" is rbt_max by simp
kuncar@48623
   488
kuncar@48623
   489
lift_definition r_max_opt :: "('a :: linorder, unit) rbt \<Rightarrow> 'a" is rbt_max_opt by simp
kuncar@48623
   490
kuncar@48623
   491
lemma r_max_alt_def: "r_max t = fold1_keys max t"
kuncar@48623
   492
by transfer (simp add: rbt_max_def)
kuncar@48623
   493
kuncar@48623
   494
lemma r_max_eq_r_max_opt:
kuncar@48623
   495
  assumes "\<not> (is_empty t)"
kuncar@48623
   496
  shows "r_max t = r_max_opt t"
kuncar@48623
   497
using assms unfolding is_empty_empty by transfer (auto intro: rbt_max_eq_rbt_max_opt)
kuncar@48623
   498
kuncar@48623
   499
lemma fold_keys_max_bot_eq:
kuncar@48623
   500
  fixes t :: "('a :: {linorder, bounded_lattice_bot}, unit) rbt"
kuncar@48623
   501
  assumes "\<not> (is_empty t)"
kuncar@48623
   502
  shows "fold_keys max t bot = fold1_keys max t"
kuncar@48623
   503
proof -
kuncar@48623
   504
  have *: "\<And>t. RBT_Impl.keys t \<noteq> [] \<Longrightarrow> List.fold max (RBT_Impl.keys t) bot = 
kuncar@48623
   505
    List.fold max (hd(RBT_Impl.keys t) # tl(RBT_Impl.keys t)) bot"
kuncar@48623
   506
    by (simp add: hd_Cons_tl[symmetric])
kuncar@48623
   507
  { fix x :: "_ :: {linorder, bounded_lattice_bot}" and xs
kuncar@48623
   508
    have "List.fold max (x#xs) bot = List.fold max xs x"
kuncar@48623
   509
    by (simp add: sup_max[symmetric])
kuncar@48623
   510
  } note ** = this
kuncar@48623
   511
  show ?thesis using assms
kuncar@48623
   512
    unfolding fold_keys_def_alt fold1_keys_def_alt is_empty_empty
kuncar@48623
   513
    apply transfer 
kuncar@48623
   514
    apply (case_tac t) 
kuncar@48623
   515
    apply simp 
kuncar@48623
   516
    apply (subst *)
kuncar@48623
   517
    apply simp
kuncar@48623
   518
    apply (subst **)
kuncar@48623
   519
    apply simp
kuncar@48623
   520
  done
kuncar@48623
   521
qed
kuncar@48623
   522
kuncar@48623
   523
kuncar@48623
   524
section {* Code equations *}
kuncar@48623
   525
kuncar@48623
   526
code_datatype Set Coset
kuncar@48623
   527
kuncar@48623
   528
lemma empty_Set [code]:
kuncar@48623
   529
  "Set.empty = Set RBT.empty"
kuncar@48623
   530
by (auto simp: Set_def)
kuncar@48623
   531
kuncar@48623
   532
lemma UNIV_Coset [code]:
kuncar@48623
   533
  "UNIV = Coset RBT.empty"
kuncar@48623
   534
by (auto simp: Set_def)
kuncar@48623
   535
kuncar@48623
   536
lemma is_empty_Set [code]:
kuncar@48623
   537
  "Set.is_empty (Set t) = RBT.is_empty t"
kuncar@48623
   538
  unfolding Set.is_empty_def by (auto simp: fun_eq_iff Set_def intro: lookup_empty_empty[THEN iffD1])
kuncar@48623
   539
kuncar@48623
   540
lemma compl_code [code]:
kuncar@48623
   541
  "- Set xs = Coset xs"
kuncar@48623
   542
  "- Coset xs = Set xs"
kuncar@48623
   543
by (simp_all add: Set_def)
kuncar@48623
   544
kuncar@48623
   545
lemma member_code [code]:
kuncar@48623
   546
  "x \<in> (Set t) = (RBT.lookup t x = Some ())"
kuncar@48623
   547
  "x \<in> (Coset t) = (RBT.lookup t x = None)"
kuncar@48623
   548
by (simp_all add: Set_def)
kuncar@48623
   549
kuncar@48623
   550
lemma insert_code [code]:
kuncar@48623
   551
  "Set.insert x (Set t) = Set (RBT.insert x () t)"
kuncar@48623
   552
  "Set.insert x (Coset t) = Coset (RBT.delete x t)"
kuncar@48623
   553
by (auto simp: Set_def)
kuncar@48623
   554
kuncar@48623
   555
lemma remove_code [code]:
kuncar@48623
   556
  "Set.remove x (Set t) = Set (RBT.delete x t)"
kuncar@48623
   557
  "Set.remove x (Coset t) = Coset (RBT.insert x () t)"
kuncar@48623
   558
by (auto simp: Set_def)
kuncar@48623
   559
kuncar@48623
   560
lemma union_Set [code]:
kuncar@48623
   561
  "Set t \<union> A = fold_keys Set.insert t A"
kuncar@48623
   562
proof -
kuncar@48623
   563
  interpret comp_fun_idem Set.insert
kuncar@48623
   564
    by (fact comp_fun_idem_insert)
kuncar@48623
   565
  from finite_fold_fold_keys[OF `comp_fun_commute Set.insert`]
kuncar@48623
   566
  show ?thesis by (auto simp add: union_fold_insert)
kuncar@48623
   567
qed
kuncar@48623
   568
kuncar@48623
   569
lemma inter_Set [code]:
kuncar@48623
   570
  "A \<inter> Set t = rbt_filter (\<lambda>k. k \<in> A) t"
kuncar@48623
   571
by (simp add: inter_filter finite_filter_rbt_filter)
kuncar@48623
   572
kuncar@48623
   573
lemma minus_Set [code]:
kuncar@48623
   574
  "A - Set t = fold_keys Set.remove t A"
kuncar@48623
   575
proof -
kuncar@48623
   576
  interpret comp_fun_idem Set.remove
kuncar@48623
   577
    by (fact comp_fun_idem_remove)
kuncar@48623
   578
  from finite_fold_fold_keys[OF `comp_fun_commute Set.remove`]
kuncar@48623
   579
  show ?thesis by (auto simp add: minus_fold_remove)
kuncar@48623
   580
qed
kuncar@48623
   581
kuncar@48623
   582
lemma union_Coset [code]:
kuncar@48623
   583
  "Coset t \<union> A = - rbt_filter (\<lambda>k. k \<notin> A) t"
kuncar@48623
   584
proof -
kuncar@48623
   585
  have *: "\<And>A B. (-A \<union> B) = -(-B \<inter> A)" by blast
kuncar@48623
   586
  show ?thesis by (simp del: boolean_algebra_class.compl_inf add: * inter_Set)
kuncar@48623
   587
qed
kuncar@48623
   588
 
kuncar@48623
   589
lemma union_Set_Set [code]:
kuncar@48623
   590
  "Set t1 \<union> Set t2 = Set (union t1 t2)"
kuncar@48623
   591
by (auto simp add: lookup_union map_add_Some_iff Set_def)
kuncar@48623
   592
kuncar@48623
   593
lemma inter_Coset [code]:
kuncar@48623
   594
  "A \<inter> Coset t = fold_keys Set.remove t A"
kuncar@48623
   595
by (simp add: Diff_eq [symmetric] minus_Set)
kuncar@48623
   596
kuncar@48623
   597
lemma inter_Coset_Coset [code]:
kuncar@48623
   598
  "Coset t1 \<inter> Coset t2 = Coset (union t1 t2)"
kuncar@48623
   599
by (auto simp add: lookup_union map_add_Some_iff Set_def)
kuncar@48623
   600
kuncar@48623
   601
lemma minus_Coset [code]:
kuncar@48623
   602
  "A - Coset t = rbt_filter (\<lambda>k. k \<in> A) t"
kuncar@48623
   603
by (simp add: inter_Set[simplified Int_commute])
kuncar@48623
   604
kuncar@49757
   605
lemma filter_Set [code]:
kuncar@49757
   606
  "Set.filter P (Set t) = (rbt_filter P t)"
kuncar@48623
   607
by (auto simp add: project_filter finite_filter_rbt_filter)
kuncar@48623
   608
kuncar@48623
   609
lemma image_Set [code]:
kuncar@48623
   610
  "image f (Set t) = fold_keys (\<lambda>k A. Set.insert (f k) A) t {}"
kuncar@48623
   611
proof -
kuncar@48623
   612
  have "comp_fun_commute (\<lambda>k. Set.insert (f k))" by default auto
kuncar@48623
   613
  then show ?thesis by (auto simp add: image_fold_insert intro!: finite_fold_fold_keys)
kuncar@48623
   614
qed
kuncar@48623
   615
kuncar@48623
   616
lemma Ball_Set [code]:
kuncar@48623
   617
  "Ball (Set t) P \<longleftrightarrow> foldi (\<lambda>s. s = True) (\<lambda>k v s. s \<and> P k) t True"
kuncar@48623
   618
proof -
kuncar@48623
   619
  have "comp_fun_commute (\<lambda>k s. s \<and> P k)" by default auto
kuncar@48623
   620
  then show ?thesis 
kuncar@48623
   621
    by (simp add: foldi_fold_conj[symmetric] Ball_fold finite_fold_fold_keys)
kuncar@48623
   622
qed
kuncar@48623
   623
kuncar@48623
   624
lemma Bex_Set [code]:
kuncar@48623
   625
  "Bex (Set t) P \<longleftrightarrow> foldi (\<lambda>s. s = False) (\<lambda>k v s. s \<or> P k) t False"
kuncar@48623
   626
proof -
kuncar@48623
   627
  have "comp_fun_commute (\<lambda>k s. s \<or> P k)" by default auto
kuncar@48623
   628
  then show ?thesis 
kuncar@48623
   629
    by (simp add: foldi_fold_disj[symmetric] Bex_fold finite_fold_fold_keys)
kuncar@48623
   630
qed
kuncar@48623
   631
kuncar@48623
   632
lemma subset_code [code]:
kuncar@48623
   633
  "Set t \<le> B \<longleftrightarrow> (\<forall>x\<in>Set t. x \<in> B)"
kuncar@48623
   634
  "A \<le> Coset t \<longleftrightarrow> (\<forall>y\<in>Set t. y \<notin> A)"
kuncar@48623
   635
by auto
kuncar@48623
   636
kuncar@48623
   637
definition non_empty_trees where [code del]: "non_empty_trees t1 t2 \<longleftrightarrow> Coset t1 \<le> Set t2"
kuncar@48623
   638
kuncar@48623
   639
code_abort non_empty_trees
kuncar@48623
   640
kuncar@48623
   641
lemma subset_Coset_empty_Set_empty [code]:
kuncar@48623
   642
  "Coset t1 \<le> Set t2 \<longleftrightarrow> (case (impl_of t1, impl_of t2) of 
kuncar@48623
   643
    (rbt.Empty, rbt.Empty) => False |
kuncar@48623
   644
    (_, _) => non_empty_trees t1 t2)"
kuncar@48623
   645
proof -
kuncar@48623
   646
  have *: "\<And>t. impl_of t = rbt.Empty \<Longrightarrow> t = RBT rbt.Empty"
kuncar@48623
   647
    by (subst(asm) RBT_inverse[symmetric]) (auto simp: impl_of_inject)
kuncar@48623
   648
  have **: "Lifting.invariant is_rbt rbt.Empty rbt.Empty" unfolding Lifting.invariant_def by simp
kuncar@48623
   649
  show ?thesis  
kuncar@48623
   650
    by (auto simp: Set_def lookup.abs_eq[OF **] dest!: * split: rbt.split simp: non_empty_trees_def)
kuncar@48623
   651
qed
kuncar@48623
   652
kuncar@48623
   653
text {* A frequent case – avoid intermediate sets *}
kuncar@48623
   654
lemma [code_unfold]:
kuncar@48623
   655
  "Set t1 \<subseteq> Set t2 \<longleftrightarrow> foldi (\<lambda>s. s = True) (\<lambda>k v s. s \<and> k \<in> Set t2) t1 True"
kuncar@48623
   656
by (simp add: subset_code Ball_Set)
kuncar@48623
   657
kuncar@48623
   658
lemma card_Set [code]:
kuncar@48623
   659
  "card (Set t) = fold_keys (\<lambda>_ n. n + 1) t 0"
kuncar@48623
   660
by (auto simp add: card_def fold_image_def intro!: finite_fold_fold_keys) (default, simp) 
kuncar@48623
   661
kuncar@48623
   662
lemma setsum_Set [code]:
kuncar@48623
   663
  "setsum f (Set xs) = fold_keys (plus o f) xs 0"
kuncar@48623
   664
proof -
kuncar@48623
   665
  have "comp_fun_commute (\<lambda>x. op + (f x))" by default (auto simp: add_ac)
kuncar@48623
   666
  then show ?thesis 
kuncar@48623
   667
    by (auto simp add: setsum_def fold_image_def finite_fold_fold_keys o_def)
kuncar@48623
   668
qed
kuncar@48623
   669
kuncar@48623
   670
definition not_a_singleton_tree  where [code del]: "not_a_singleton_tree x y = x y"
kuncar@48623
   671
kuncar@48623
   672
code_abort not_a_singleton_tree
kuncar@48623
   673
kuncar@48623
   674
lemma the_elem_set [code]:
kuncar@48623
   675
  fixes t :: "('a :: linorder, unit) rbt"
kuncar@48623
   676
  shows "the_elem (Set t) = (case impl_of t of 
kuncar@48623
   677
    (Branch RBT_Impl.B RBT_Impl.Empty x () RBT_Impl.Empty) \<Rightarrow> x
kuncar@48623
   678
    | _ \<Rightarrow> not_a_singleton_tree the_elem (Set t))"
kuncar@48623
   679
proof -
kuncar@48623
   680
  {
kuncar@48623
   681
    fix x :: "'a :: linorder"
kuncar@48623
   682
    let ?t = "Branch RBT_Impl.B RBT_Impl.Empty x () RBT_Impl.Empty" 
kuncar@48623
   683
    have *:"?t \<in> {t. is_rbt t}" unfolding is_rbt_def by auto
kuncar@48623
   684
    then have **:"Lifting.invariant is_rbt ?t ?t" unfolding Lifting.invariant_def by auto
kuncar@48623
   685
kuncar@48623
   686
    have "impl_of t = ?t \<Longrightarrow> the_elem (Set t) = x" 
kuncar@48623
   687
      by (subst(asm) RBT_inverse[symmetric, OF *])
kuncar@48623
   688
        (auto simp: Set_def the_elem_def lookup.abs_eq[OF **] impl_of_inject)
kuncar@48623
   689
  }
kuncar@48623
   690
  then show ?thesis unfolding not_a_singleton_tree_def
kuncar@48623
   691
    by(auto split: rbt.split unit.split color.split)
kuncar@48623
   692
qed
kuncar@48623
   693
kuncar@48623
   694
lemma Pow_Set [code]:
kuncar@48623
   695
  "Pow (Set t) = fold_keys (\<lambda>x A. A \<union> Set.insert x ` A) t {{}}"
kuncar@48623
   696
by (simp add: Pow_fold finite_fold_fold_keys[OF comp_fun_commute_Pow_fold])
kuncar@48623
   697
kuncar@48623
   698
lemma product_Set [code]:
kuncar@48623
   699
  "Product_Type.product (Set t1) (Set t2) = 
kuncar@48623
   700
    fold_keys (\<lambda>x A. fold_keys (\<lambda>y. Set.insert (x, y)) t2 A) t1 {}"
kuncar@48623
   701
proof -
kuncar@48623
   702
  have *:"\<And>x. comp_fun_commute (\<lambda>y. Set.insert (x, y))" by default auto
kuncar@48623
   703
  show ?thesis using finite_fold_fold_keys[OF comp_fun_commute_product_fold, of "Set t2" "{}" "t1"]  
kuncar@48623
   704
    by (simp add: product_fold Product_Type.product_def finite_fold_fold_keys[OF *])
kuncar@48623
   705
qed
kuncar@48623
   706
kuncar@48623
   707
lemma Id_on_Set [code]:
kuncar@48623
   708
  "Id_on (Set t) =  fold_keys (\<lambda>x. Set.insert (x, x)) t {}"
kuncar@48623
   709
proof -
kuncar@48623
   710
  have "comp_fun_commute (\<lambda>x. Set.insert (x, x))" by default auto
kuncar@48623
   711
  then show ?thesis
kuncar@48623
   712
    by (auto simp add: Id_on_fold intro!: finite_fold_fold_keys)
kuncar@48623
   713
qed
kuncar@48623
   714
kuncar@48623
   715
lemma Image_Set [code]:
kuncar@48623
   716
  "(Set t) `` S = fold_keys (\<lambda>(x,y) A. if x \<in> S then Set.insert y A else A) t {}"
kuncar@48623
   717
by (auto simp add: Image_fold finite_fold_fold_keys[OF comp_fun_commute_Image_fold])
kuncar@48623
   718
kuncar@48623
   719
lemma trancl_set_ntrancl [code]:
kuncar@48623
   720
  "trancl (Set t) = ntrancl (card (Set t) - 1) (Set t)"
kuncar@48623
   721
by (simp add: finite_trancl_ntranl)
kuncar@48623
   722
kuncar@48623
   723
lemma relcomp_Set[code]:
kuncar@48623
   724
  "(Set t1) O (Set t2) = fold_keys 
kuncar@48623
   725
    (\<lambda>(x,y) A. fold_keys (\<lambda>(w,z) A'. if y = w then Set.insert (x,z) A' else A') t2 A) t1 {}"
kuncar@48623
   726
proof -
kuncar@48623
   727
  interpret comp_fun_idem Set.insert by (fact comp_fun_idem_insert)
kuncar@48623
   728
  have *: "\<And>x y. comp_fun_commute (\<lambda>(w, z) A'. if y = w then Set.insert (x, z) A' else A')"
kuncar@48623
   729
    by default (auto simp add: fun_eq_iff)
kuncar@48623
   730
  show ?thesis using finite_fold_fold_keys[OF comp_fun_commute_relcomp_fold, of "Set t2" "{}" t1]
kuncar@48623
   731
    by (simp add: relcomp_fold finite_fold_fold_keys[OF *])
kuncar@48623
   732
qed
kuncar@48623
   733
kuncar@48623
   734
lemma wf_set [code]:
kuncar@48623
   735
  "wf (Set t) = acyclic (Set t)"
kuncar@48623
   736
by (simp add: wf_iff_acyclic_if_finite)
kuncar@48623
   737
kuncar@48623
   738
definition not_non_empty_tree  where [code del]: "not_non_empty_tree x y = x y"
kuncar@48623
   739
kuncar@48623
   740
code_abort not_non_empty_tree
kuncar@48623
   741
kuncar@48623
   742
lemma Min_fin_set_fold [code]:
kuncar@48623
   743
  "Min (Set t) = (if is_empty t then not_non_empty_tree Min (Set t) else r_min_opt t)"
kuncar@48623
   744
proof -
kuncar@48623
   745
  have *:"(class.ab_semigroup_mult (min :: 'a \<Rightarrow> 'a \<Rightarrow> 'a))" using ab_semigroup_idem_mult_min
kuncar@48623
   746
    unfolding class.ab_semigroup_idem_mult_def by blast
kuncar@48623
   747
  show ?thesis
kuncar@48623
   748
    by (auto simp add: Min_def not_non_empty_tree_def finite_fold1_fold1_keys[OF *] r_min_alt_def 
kuncar@48623
   749
      r_min_eq_r_min_opt[symmetric])  
kuncar@48623
   750
qed
kuncar@48623
   751
kuncar@48623
   752
lemma Inf_fin_set_fold [code]:
kuncar@48623
   753
  "Inf_fin (Set t) = Min (Set t)"
kuncar@48623
   754
by (simp add: inf_min Inf_fin_def Min_def)
kuncar@48623
   755
kuncar@48623
   756
lemma Inf_Set_fold:
kuncar@48623
   757
  fixes t :: "('a :: {linorder, complete_lattice}, unit) rbt"
kuncar@48623
   758
  shows "Inf (Set t) = (if is_empty t then top else r_min_opt t)"
kuncar@48623
   759
proof -
kuncar@48623
   760
  have "comp_fun_commute (min :: 'a \<Rightarrow> 'a \<Rightarrow> 'a)" by default (simp add: fun_eq_iff ac_simps)
kuncar@48623
   761
  then have "t \<noteq> empty \<Longrightarrow> Finite_Set.fold min top (Set t) = fold1_keys min t"
kuncar@48623
   762
    by (simp add: finite_fold_fold_keys fold_keys_min_top_eq)
kuncar@48623
   763
  then show ?thesis 
kuncar@48623
   764
    by (auto simp add: Inf_fold_inf inf_min empty_Set[symmetric] r_min_eq_r_min_opt[symmetric] r_min_alt_def)
kuncar@48623
   765
qed
kuncar@48623
   766
kuncar@48623
   767
definition Inf' :: "'a :: {linorder, complete_lattice} set \<Rightarrow> 'a" where [code del]: "Inf' x = Inf x"
kuncar@48623
   768
declare Inf'_def[symmetric, code_unfold]
kuncar@48623
   769
declare Inf_Set_fold[folded Inf'_def, code]
kuncar@48623
   770
kuncar@48623
   771
lemma INFI_Set_fold [code]:
kuncar@48623
   772
  "INFI (Set t) f = fold_keys (inf \<circ> f) t top"
kuncar@48623
   773
proof -
kuncar@48623
   774
  have "comp_fun_commute ((inf :: 'a \<Rightarrow> 'a \<Rightarrow> 'a) \<circ> f)" 
kuncar@48623
   775
    by default (auto simp add: fun_eq_iff ac_simps)
kuncar@48623
   776
  then show ?thesis
kuncar@48623
   777
    by (auto simp: INF_fold_inf finite_fold_fold_keys)
kuncar@48623
   778
qed
kuncar@48623
   779
kuncar@48623
   780
lemma Max_fin_set_fold [code]:
kuncar@48623
   781
  "Max (Set t) = (if is_empty t then not_non_empty_tree Max (Set t) else r_max_opt t)"
kuncar@48623
   782
proof -
kuncar@48623
   783
  have *:"(class.ab_semigroup_mult (max :: 'a \<Rightarrow> 'a \<Rightarrow> 'a))" using ab_semigroup_idem_mult_max
kuncar@48623
   784
    unfolding class.ab_semigroup_idem_mult_def by blast
kuncar@48623
   785
  show ?thesis
kuncar@48623
   786
    by (auto simp add: Max_def not_non_empty_tree_def finite_fold1_fold1_keys[OF *] r_max_alt_def 
kuncar@48623
   787
      r_max_eq_r_max_opt[symmetric])  
kuncar@48623
   788
qed
kuncar@48623
   789
kuncar@48623
   790
lemma Sup_fin_set_fold [code]:
kuncar@48623
   791
  "Sup_fin (Set t) = Max (Set t)"
kuncar@48623
   792
by (simp add: sup_max Sup_fin_def Max_def)
kuncar@48623
   793
kuncar@48623
   794
lemma Sup_Set_fold:
kuncar@48623
   795
  fixes t :: "('a :: {linorder, complete_lattice}, unit) rbt"
kuncar@48623
   796
  shows "Sup (Set t) = (if is_empty t then bot else r_max_opt t)"
kuncar@48623
   797
proof -
kuncar@48623
   798
  have "comp_fun_commute (max :: 'a \<Rightarrow> 'a \<Rightarrow> 'a)" by default (simp add: fun_eq_iff ac_simps)
kuncar@48623
   799
  then have "t \<noteq> empty \<Longrightarrow> Finite_Set.fold max bot (Set t) = fold1_keys max t"
kuncar@48623
   800
    by (simp add: finite_fold_fold_keys fold_keys_max_bot_eq)
kuncar@48623
   801
  then show ?thesis 
kuncar@48623
   802
    by (auto simp add: Sup_fold_sup sup_max empty_Set[symmetric] r_max_eq_r_max_opt[symmetric] r_max_alt_def)
kuncar@48623
   803
qed
kuncar@48623
   804
kuncar@48623
   805
definition Sup' :: "'a :: {linorder, complete_lattice} set \<Rightarrow> 'a" where [code del]: "Sup' x = Sup x"
kuncar@48623
   806
declare Sup'_def[symmetric, code_unfold]
kuncar@48623
   807
declare Sup_Set_fold[folded Sup'_def, code]
kuncar@48623
   808
kuncar@48623
   809
lemma SUPR_Set_fold [code]:
kuncar@48623
   810
  "SUPR (Set t) f = fold_keys (sup \<circ> f) t bot"
kuncar@48623
   811
proof -
kuncar@48623
   812
  have "comp_fun_commute ((sup :: 'a \<Rightarrow> 'a \<Rightarrow> 'a) \<circ> f)" 
kuncar@48623
   813
    by default (auto simp add: fun_eq_iff ac_simps)
kuncar@48623
   814
  then show ?thesis
kuncar@48623
   815
    by (auto simp: SUP_fold_sup finite_fold_fold_keys)
kuncar@48623
   816
qed
kuncar@48623
   817
kuncar@48623
   818
lemma sorted_list_set[code]:
kuncar@48623
   819
  "sorted_list_of_set (Set t) = keys t"
kuncar@48623
   820
by (auto simp add: set_keys intro: sorted_distinct_set_unique) 
kuncar@48623
   821
kuncar@48623
   822
hide_const (open) RBT_Set.Set RBT_Set.Coset
kuncar@48623
   823
kuncar@48623
   824
end