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