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