src/HOL/Library/RBT_Set.thy
author blanchet
Thu, 07 Aug 2014 12:17:41 +0200
changeset 57816 d8bbb97689d3
parent 57514 bdc2c6b40bf2
child 58301 de95aeedf49e
permissions -rw-r--r--
no need for 'set_simps' now that 'datatype_new' generates the desired 'set' property
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
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
     5
header {* Implementation of sets using RBT trees *}
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
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
    13
  outside of List.thy using 'a list as an implenentation of sets cannot be
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
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
    19
section {* Definition of code datatype constructors *}
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
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
    28
section {* Deletion of already existing code equations *}
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]:
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
    91
  "Product_Type.product = Product_Type.product"  ..
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
    92
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
    93
lemma [code, code del]:
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
    94
  "Id_on = Id_on" ..
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
  "Image = Image" ..
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
  "trancl = trancl" ..
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
  "relcomp = relcomp" ..
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
  "wf = wf" ..
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
  "Min = Min" ..
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
  "Inf_fin = Inf_fin" ..
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]:
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
   115
  "INFIMUM = INFIMUM" ..
48623
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]:
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   118
  "Max = Max" ..
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
  "Sup_fin = Sup_fin" ..
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]:
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
   124
  "SUPREMUM = SUPREMUM" ..
48623
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]:
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   127
  "(Inf :: 'a set set \<Rightarrow> 'a set) = Inf" ..
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
  "(Sup :: 'a set set \<Rightarrow> 'a set) = Sup" ..
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
  "sorted_list_of_set = sorted_list_of_set" ..
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
  "List.map_project = List.map_project" ..
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   137
53955
436649a2ed62 added Bleast code eqns for RBT
nipkow
parents: 53745
diff changeset
   138
lemma [code, code del]: 
436649a2ed62 added Bleast code eqns for RBT
nipkow
parents: 53745
diff changeset
   139
  "List.Bleast = List.Bleast" ..
436649a2ed62 added Bleast code eqns for RBT
nipkow
parents: 53745
diff changeset
   140
48623
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   141
section {* Lemmas *}
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   142
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   143
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   144
subsection {* Auxiliary lemmas *}
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
lemma [simp]: "x \<noteq> Some () \<longleftrightarrow> x = None"
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   147
by (auto simp: not_Some_eq[THEN iffD1])
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   148
56019
682bba24e474 hide implementation details
kuncar
parents: 55584
diff changeset
   149
lemma Set_set_keys: "Set x = dom (RBT.lookup x)" 
49928
e3f0a92de280 tuned proofs
kuncar
parents: 49758
diff changeset
   150
by (auto simp: Set_def)
e3f0a92de280 tuned proofs
kuncar
parents: 49758
diff changeset
   151
48623
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   152
lemma finite_Set [simp, intro!]: "finite (Set x)"
49928
e3f0a92de280 tuned proofs
kuncar
parents: 49758
diff changeset
   153
by (simp add: Set_set_keys)
48623
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   154
56019
682bba24e474 hide implementation details
kuncar
parents: 55584
diff changeset
   155
lemma set_keys: "Set t = set(RBT.keys t)"
49928
e3f0a92de280 tuned proofs
kuncar
parents: 49758
diff changeset
   156
by (simp add: Set_set_keys lookup_keys)
48623
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   157
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   158
subsection {* fold and filter *}
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   159
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   160
lemma finite_fold_rbt_fold_eq:
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   161
  assumes "comp_fun_commute f" 
56019
682bba24e474 hide implementation details
kuncar
parents: 55584
diff changeset
   162
  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
   163
proof -
56019
682bba24e474 hide implementation details
kuncar
parents: 55584
diff changeset
   164
  have *: "remdups (RBT.entries t) = RBT.entries t"
48623
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   165
    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
   166
  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
   167
qed
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   168
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   169
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
   170
  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
   171
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   172
lemma fold_keys_def_alt:
56019
682bba24e474 hide implementation details
kuncar
parents: 55584
diff changeset
   173
  "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
   174
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
   175
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   176
lemma finite_fold_fold_keys:
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   177
  assumes "comp_fun_commute f"
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   178
  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
   179
using assms
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   180
proof -
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   181
  interpret comp_fun_commute f by fact
56019
682bba24e474 hide implementation details
kuncar
parents: 55584
diff changeset
   182
  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
   183
  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
   184
  ultimately show ?thesis 
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   185
    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
   186
      comp_comp_fun_commute)
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   187
qed
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   188
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   189
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
   190
  "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
   191
49758
718f10c8bbfc use Set.filter instead of Finite_Set.filter, which is removed then
kuncar
parents: 49757
diff changeset
   192
lemma Set_filter_rbt_filter:
718f10c8bbfc use Set.filter instead of Finite_Set.filter, which is removed then
kuncar
parents: 49757
diff changeset
   193
  "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
   194
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
   195
  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
   196
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   197
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   198
subsection {* foldi and Ball *}
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
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
   201
by (induction t) auto
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 rbt_foldi_fold_conj: 
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   204
  "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
   205
proof (induction t arbitrary: val) 
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   206
  case (Branch c t1) then show ?case
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   207
    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
   208
qed simp
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   209
56019
682bba24e474 hide implementation details
kuncar
parents: 55584
diff changeset
   210
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
   211
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
   212
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   213
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   214
subsection {* foldi and Bex *}
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
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
   217
by (induction t) auto
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 rbt_foldi_fold_disj: 
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   220
  "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
   221
proof (induction t arbitrary: val) 
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   222
  case (Branch c t1) then show ?case
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   223
    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
   224
qed simp
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   225
56019
682bba24e474 hide implementation details
kuncar
parents: 55584
diff changeset
   226
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
   227
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
   228
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   229
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   230
subsection {* folding over non empty trees and selecting the minimal and maximal element *}
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
(** concrete **)
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   233
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   234
(* 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
   235
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   236
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
   237
  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
   238
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   239
(* minimum *)
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   240
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   241
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
   242
  where "rbt_min t = rbt_fold1_keys min t"
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
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
   245
by  (auto simp: rbt_greater_prop less_imp_le)
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 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
   248
by (auto simp: rbt_less_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 fold_min_triv:
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   251
  fixes k :: "_ :: linorder"
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   252
  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
   253
by (induct xs) (auto simp add: min_def)
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   254
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   255
lemma rbt_min_simps:
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   256
  "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
   257
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
   258
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   259
fun rbt_min_opt where
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   260
  "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
   261
  "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
   262
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   263
lemma rbt_min_opt_Branch:
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   264
  "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
   265
by (cases t1) auto
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   266
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   267
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
   268
  fixes t :: "('a :: linorder, unit) RBT_Impl.rbt"
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   269
  assumes "P rbt.Empty"
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   270
  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
   271
  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
   272
  shows "P t"
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   273
using assms
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   274
  apply (induction t)
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   275
  apply simp
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   276
  apply (case_tac "t1 = rbt.Empty")
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   277
  apply simp_all
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   278
done
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   279
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   280
lemma rbt_min_opt_in_set: 
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   281
  fixes t :: "('a :: linorder, unit) RBT_Impl.rbt"
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   282
  assumes "t \<noteq> rbt.Empty"
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   283
  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
   284
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
   285
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   286
lemma rbt_min_opt_is_min:
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   287
  fixes t :: "('a :: linorder, unit) RBT_Impl.rbt"
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   288
  assumes "rbt_sorted t"
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   289
  assumes "t \<noteq> rbt.Empty"
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   290
  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
   291
using assms 
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   292
proof (induction t rule: rbt_min_opt_induct)
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   293
  case empty
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   294
    then show ?case by simp
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   295
next
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   296
  case left_empty
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   297
    then show ?case by (auto intro: key_le_right simp del: rbt_sorted.simps)
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_non_empty c t1 k v t2 y)
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   300
    then have "y = k \<or> y \<in> set (RBT_Impl.keys t1) \<or> y \<in> set (RBT_Impl.keys t2)" by auto
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   301
    with left_non_empty show ?case 
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   302
    proof(elim disjE)
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   303
      case goal1 then show ?case 
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   304
        by (auto simp add: rbt_min_opt_Branch intro: left_le_key rbt_min_opt_in_set)
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   305
    next
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   306
      case goal2 with left_non_empty show ?case by (auto simp add: rbt_min_opt_Branch)
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   307
    next 
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   308
      case goal3 show ?case
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   309
      proof -
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   310
        from goal3 have "rbt_min_opt t1 \<le> k" by (simp add: left_le_key rbt_min_opt_in_set)
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   311
        moreover from goal3 have "k \<le> y" by (simp add: key_le_right)
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   312
        ultimately show ?thesis using goal3 by (simp add: rbt_min_opt_Branch)
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   313
      qed
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   314
    qed
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   315
qed
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   316
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   317
lemma rbt_min_eq_rbt_min_opt:
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   318
  assumes "t \<noteq> RBT_Impl.Empty"
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   319
  assumes "is_rbt t"
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   320
  shows "rbt_min t = rbt_min_opt t"
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   321
proof -
51489
f738e6dbd844 fundamental revision of big operators on sets
haftmann
parents: 51115
diff changeset
   322
  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
   323
  with assms show ?thesis
f738e6dbd844 fundamental revision of big operators on sets
haftmann
parents: 51115
diff changeset
   324
    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
   325
      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
   326
qed
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   327
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   328
(* maximum *)
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   329
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   330
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
   331
  where "rbt_max t = rbt_fold1_keys max t"
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   332
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   333
lemma fold_max_triv:
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   334
  fixes k :: "_ :: linorder"
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   335
  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
   336
by (induct xs) (auto simp add: max_def)
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
lemma fold_max_rev_eq:
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   339
  fixes xs :: "('a :: linorder) list"
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   340
  assumes "xs \<noteq> []"
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   341
  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
   342
  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
   343
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   344
lemma rbt_max_simps:
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   345
  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
   346
  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
   347
proof -
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   348
  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
   349
    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
   350
  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
   351
qed
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   352
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   353
fun rbt_max_opt where
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   354
  "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
   355
  "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
   356
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   357
lemma rbt_max_opt_Branch:
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   358
  "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
   359
by (cases t2) auto
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
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
   362
  fixes t :: "('a :: linorder, unit) RBT_Impl.rbt"
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   363
  assumes "P rbt.Empty"
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   364
  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
   365
  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
   366
  shows "P t"
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   367
using assms
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   368
  apply (induction t)
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   369
  apply simp
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   370
  apply (case_tac "t2 = rbt.Empty")
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   371
  apply simp_all
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   372
done
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   373
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   374
lemma rbt_max_opt_in_set: 
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   375
  fixes t :: "('a :: linorder, unit) RBT_Impl.rbt"
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   376
  assumes "t \<noteq> rbt.Empty"
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   377
  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
   378
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
   379
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   380
lemma rbt_max_opt_is_max:
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   381
  fixes t :: "('a :: linorder, unit) RBT_Impl.rbt"
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   382
  assumes "rbt_sorted t"
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   383
  assumes "t \<noteq> rbt.Empty"
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   384
  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
   385
using assms 
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   386
proof (induction t rule: rbt_max_opt_induct)
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   387
  case empty
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   388
    then show ?case by simp
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   389
next
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   390
  case right_empty
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   391
    then show ?case by (auto intro: left_le_key simp del: rbt_sorted.simps)
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   392
next
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   393
  case (right_non_empty c t1 k v t2 y)
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   394
    then have "y = k \<or> y \<in> set (RBT_Impl.keys t2) \<or> y \<in> set (RBT_Impl.keys t1)" by auto
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   395
    with right_non_empty show ?case 
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   396
    proof(elim disjE)
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   397
      case goal1 then show ?case 
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   398
        by (auto simp add: rbt_max_opt_Branch intro: key_le_right rbt_max_opt_in_set)
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   399
    next
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   400
      case goal2 with right_non_empty show ?case by (auto simp add: rbt_max_opt_Branch)
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   401
    next 
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   402
      case goal3 show ?case
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   403
      proof -
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   404
        from goal3 have "rbt_max_opt t2 \<ge> k" by (simp add: key_le_right rbt_max_opt_in_set)
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   405
        moreover from goal3 have "y \<le> k" by (simp add: left_le_key)
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   406
        ultimately show ?thesis using goal3 by (simp add: rbt_max_opt_Branch)
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   407
      qed
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   408
    qed
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   409
qed
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   410
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   411
lemma rbt_max_eq_rbt_max_opt:
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   412
  assumes "t \<noteq> RBT_Impl.Empty"
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   413
  assumes "is_rbt t"
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   414
  shows "rbt_max t = rbt_max_opt t"
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   415
proof -
51489
f738e6dbd844 fundamental revision of big operators on sets
haftmann
parents: 51115
diff changeset
   416
  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
   417
  with assms show ?thesis
f738e6dbd844 fundamental revision of big operators on sets
haftmann
parents: 51115
diff changeset
   418
    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
   419
      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
   420
qed
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   421
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   422
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   423
(** abstract **)
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   424
56019
682bba24e474 hide implementation details
kuncar
parents: 55584
diff changeset
   425
context includes rbt.lifting begin
48623
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   426
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
   427
  is rbt_fold1_keys .
48623
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   428
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   429
lemma fold1_keys_def_alt:
56019
682bba24e474 hide implementation details
kuncar
parents: 55584
diff changeset
   430
  "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
   431
  by transfer (simp add: rbt_fold1_keys_def)
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   432
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   433
lemma finite_fold1_fold1_keys:
51489
f738e6dbd844 fundamental revision of big operators on sets
haftmann
parents: 51115
diff changeset
   434
  assumes "semilattice f"
56019
682bba24e474 hide implementation details
kuncar
parents: 55584
diff changeset
   435
  assumes "\<not> RBT.is_empty t"
51489
f738e6dbd844 fundamental revision of big operators on sets
haftmann
parents: 51115
diff changeset
   436
  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
   437
proof -
51489
f738e6dbd844 fundamental revision of big operators on sets
haftmann
parents: 51115
diff changeset
   438
  from `semilattice f` 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
   439
  show ?thesis using assms 
51489
f738e6dbd844 fundamental revision of big operators on sets
haftmann
parents: 51115
diff changeset
   440
    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
   441
qed
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   442
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   443
(* minimum *)
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   444
55565
f663fc1e653b simplify proofs because of the stronger reflexivity prover
kuncar
parents: 54263
diff changeset
   445
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
   446
55565
f663fc1e653b simplify proofs because of the stronger reflexivity prover
kuncar
parents: 54263
diff changeset
   447
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
   448
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   449
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
   450
by transfer (simp add: rbt_min_def)
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   451
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   452
lemma r_min_eq_r_min_opt:
56019
682bba24e474 hide implementation details
kuncar
parents: 55584
diff changeset
   453
  assumes "\<not> (RBT.is_empty t)"
48623
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   454
  shows "r_min t = r_min_opt t"
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   455
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
   456
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   457
lemma fold_keys_min_top_eq:
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   458
  fixes t :: "('a :: {linorder, bounded_lattice_top}, unit) rbt"
56019
682bba24e474 hide implementation details
kuncar
parents: 55584
diff changeset
   459
  assumes "\<not> (RBT.is_empty t)"
48623
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   460
  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
   461
proof -
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   462
  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
   463
    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
   464
    by (simp add: hd_Cons_tl[symmetric])
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   465
  { fix x :: "_ :: {linorder, bounded_lattice_top}" and xs
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   466
    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
   467
    by (simp add: inf_min[symmetric])
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   468
  } note ** = this
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   469
  show ?thesis using assms
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   470
    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
   471
    apply transfer 
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   472
    apply (case_tac t) 
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   473
    apply simp 
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   474
    apply (subst *)
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   475
    apply simp
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   476
    apply (subst **)
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   477
    apply simp
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   478
  done
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   479
qed
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   480
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   481
(* maximum *)
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   482
55565
f663fc1e653b simplify proofs because of the stronger reflexivity prover
kuncar
parents: 54263
diff changeset
   483
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
   484
55565
f663fc1e653b simplify proofs because of the stronger reflexivity prover
kuncar
parents: 54263
diff changeset
   485
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
   486
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   487
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
   488
by transfer (simp add: rbt_max_def)
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   489
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   490
lemma r_max_eq_r_max_opt:
56019
682bba24e474 hide implementation details
kuncar
parents: 55584
diff changeset
   491
  assumes "\<not> (RBT.is_empty t)"
48623
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   492
  shows "r_max t = r_max_opt t"
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   493
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
   494
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   495
lemma fold_keys_max_bot_eq:
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   496
  fixes t :: "('a :: {linorder, bounded_lattice_bot}, unit) rbt"
56019
682bba24e474 hide implementation details
kuncar
parents: 55584
diff changeset
   497
  assumes "\<not> (RBT.is_empty t)"
48623
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   498
  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
   499
proof -
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   500
  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
   501
    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
   502
    by (simp add: hd_Cons_tl[symmetric])
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   503
  { fix x :: "_ :: {linorder, bounded_lattice_bot}" and xs
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   504
    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
   505
    by (simp add: sup_max[symmetric])
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   506
  } note ** = this
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   507
  show ?thesis using assms
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   508
    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
   509
    apply transfer 
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   510
    apply (case_tac t) 
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   511
    apply simp 
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   512
    apply (subst *)
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   513
    apply simp
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   514
    apply (subst **)
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   515
    apply simp
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   516
  done
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   517
qed
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   518
56019
682bba24e474 hide implementation details
kuncar
parents: 55584
diff changeset
   519
end
48623
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   520
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   521
section {* Code equations *}
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   522
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   523
code_datatype Set Coset
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   524
57816
d8bbb97689d3 no need for 'set_simps' now that 'datatype_new' generates the desired 'set' property
blanchet
parents: 57514
diff changeset
   525
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
   526
48623
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   527
lemma empty_Set [code]:
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   528
  "Set.empty = Set RBT.empty"
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   529
by (auto simp: Set_def)
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   530
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   531
lemma UNIV_Coset [code]:
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   532
  "UNIV = Coset RBT.empty"
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   533
by (auto simp: Set_def)
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   534
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   535
lemma is_empty_Set [code]:
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   536
  "Set.is_empty (Set t) = RBT.is_empty t"
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   537
  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
   538
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   539
lemma compl_code [code]:
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   540
  "- Set xs = Coset xs"
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   541
  "- Coset xs = Set xs"
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   542
by (simp_all add: 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 member_code [code]:
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   545
  "x \<in> (Set t) = (RBT.lookup t x = Some ())"
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   546
  "x \<in> (Coset t) = (RBT.lookup t x = None)"
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   547
by (simp_all add: Set_def)
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   548
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   549
lemma insert_code [code]:
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   550
  "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
   551
  "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
   552
by (auto simp: Set_def)
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   553
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   554
lemma remove_code [code]:
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   555
  "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
   556
  "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
   557
by (auto simp: Set_def)
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   558
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   559
lemma union_Set [code]:
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   560
  "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
   561
proof -
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   562
  interpret comp_fun_idem Set.insert
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   563
    by (fact comp_fun_idem_insert)
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   564
  from finite_fold_fold_keys[OF `comp_fun_commute Set.insert`]
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   565
  show ?thesis by (auto simp add: union_fold_insert)
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   566
qed
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   567
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   568
lemma inter_Set [code]:
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   569
  "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
   570
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
   571
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   572
lemma minus_Set [code]:
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   573
  "A - Set t = fold_keys Set.remove 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.remove
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   576
    by (fact comp_fun_idem_remove)
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   577
  from finite_fold_fold_keys[OF `comp_fun_commute Set.remove`]
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   578
  show ?thesis by (auto simp add: minus_fold_remove)
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 union_Coset [code]:
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   582
  "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
   583
proof -
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   584
  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
   585
  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
   586
qed
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   587
 
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   588
lemma union_Set_Set [code]:
56019
682bba24e474 hide implementation details
kuncar
parents: 55584
diff changeset
   589
  "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
   590
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
   591
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   592
lemma inter_Coset [code]:
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   593
  "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
   594
by (simp add: Diff_eq [symmetric] minus_Set)
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   595
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   596
lemma inter_Coset_Coset [code]:
56019
682bba24e474 hide implementation details
kuncar
parents: 55584
diff changeset
   597
  "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
   598
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
   599
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   600
lemma minus_Coset [code]:
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   601
  "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
   602
by (simp add: inter_Set[simplified Int_commute])
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   603
49757
73ab6d4a9236 rename Set.project to Set.filter - more appropriate name
kuncar
parents: 48623
diff changeset
   604
lemma filter_Set [code]:
73ab6d4a9236 rename Set.project to Set.filter - more appropriate name
kuncar
parents: 48623
diff changeset
   605
  "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
   606
by (auto simp add: Set_filter_rbt_filter)
48623
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   607
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   608
lemma image_Set [code]:
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   609
  "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
   610
proof -
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   611
  have "comp_fun_commute (\<lambda>k. Set.insert (f k))" by default auto
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   612
  then show ?thesis by (auto simp add: image_fold_insert intro!: finite_fold_fold_keys)
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   613
qed
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   614
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   615
lemma Ball_Set [code]:
56019
682bba24e474 hide implementation details
kuncar
parents: 55584
diff changeset
   616
  "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
   617
proof -
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   618
  have "comp_fun_commute (\<lambda>k s. s \<and> P k)" by default auto
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   619
  then show ?thesis 
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   620
    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
   621
qed
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   622
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   623
lemma Bex_Set [code]:
56019
682bba24e474 hide implementation details
kuncar
parents: 55584
diff changeset
   624
  "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
   625
proof -
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   626
  have "comp_fun_commute (\<lambda>k s. s \<or> P k)" by default auto
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   627
  then show ?thesis 
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   628
    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
   629
qed
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   630
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   631
lemma subset_code [code]:
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   632
  "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
   633
  "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
   634
by auto
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   635
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   636
lemma subset_Coset_empty_Set_empty [code]:
56019
682bba24e474 hide implementation details
kuncar
parents: 55584
diff changeset
   637
  "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
   638
    (rbt.Empty, rbt.Empty) => False |
53745
788730ab7da4 prefer Code.abort over code_abort
Andreas Lochbihler
parents: 51540
diff changeset
   639
    (_, _) => 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
   640
proof -
56019
682bba24e474 hide implementation details
kuncar
parents: 55584
diff changeset
   641
  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
   642
    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
   643
  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
   644
  show ?thesis  
53745
788730ab7da4 prefer Code.abort over code_abort
Andreas Lochbihler
parents: 51540
diff changeset
   645
    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
   646
qed
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   647
56790
f54097170704 prefer plain ASCII / latex over not-so-universal Unicode;
wenzelm
parents: 56519
diff changeset
   648
text {* A frequent case -- avoid intermediate sets *}
48623
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   649
lemma [code_unfold]:
56019
682bba24e474 hide implementation details
kuncar
parents: 55584
diff changeset
   650
  "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
   651
by (simp add: subset_code Ball_Set)
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 card_Set [code]:
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   654
  "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
   655
  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
   656
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   657
lemma setsum_Set [code]:
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   658
  "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
   659
proof -
57514
bdc2c6b40bf2 prefer ac_simps collections over separate name bindings for add and mult
haftmann
parents: 56790
diff changeset
   660
  have "comp_fun_commute (\<lambda>x. op + (f x))" by default (auto simp: ac_simps)
48623
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   661
  then show ?thesis 
51489
f738e6dbd844 fundamental revision of big operators on sets
haftmann
parents: 51115
diff changeset
   662
    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
   663
qed
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   664
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   665
lemma the_elem_set [code]:
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   666
  fixes t :: "('a :: linorder, unit) rbt"
56019
682bba24e474 hide implementation details
kuncar
parents: 55584
diff changeset
   667
  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
   668
    (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
   669
    | _ \<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
   670
proof -
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   671
  {
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   672
    fix x :: "'a :: linorder"
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   673
    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
   674
    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
   675
    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
   676
56019
682bba24e474 hide implementation details
kuncar
parents: 55584
diff changeset
   677
    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
   678
      by (subst(asm) RBT_inverse[symmetric, OF *])
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   679
        (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
   680
  }
53745
788730ab7da4 prefer Code.abort over code_abort
Andreas Lochbihler
parents: 51540
diff changeset
   681
  then show ?thesis
48623
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   682
    by(auto split: rbt.split unit.split color.split)
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   683
qed
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   684
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   685
lemma Pow_Set [code]:
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   686
  "Pow (Set t) = fold_keys (\<lambda>x A. A \<union> Set.insert x ` A) t {{}}"
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   687
by (simp add: Pow_fold finite_fold_fold_keys[OF comp_fun_commute_Pow_fold])
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   688
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   689
lemma product_Set [code]:
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   690
  "Product_Type.product (Set t1) (Set t2) = 
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   691
    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
   692
proof -
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   693
  have *:"\<And>x. comp_fun_commute (\<lambda>y. Set.insert (x, y))" by default auto
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   694
  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
   695
    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
   696
qed
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   697
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   698
lemma Id_on_Set [code]:
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   699
  "Id_on (Set t) =  fold_keys (\<lambda>x. Set.insert (x, x)) t {}"
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   700
proof -
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   701
  have "comp_fun_commute (\<lambda>x. Set.insert (x, x))" by default auto
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   702
  then show ?thesis
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   703
    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
   704
qed
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 Image_Set [code]:
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   707
  "(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
   708
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
   709
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   710
lemma trancl_set_ntrancl [code]:
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   711
  "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
   712
by (simp add: finite_trancl_ntranl)
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   713
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   714
lemma relcomp_Set[code]:
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   715
  "(Set t1) O (Set t2) = fold_keys 
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   716
    (\<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
   717
proof -
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   718
  interpret comp_fun_idem Set.insert by (fact comp_fun_idem_insert)
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   719
  have *: "\<And>x y. comp_fun_commute (\<lambda>(w, z) A'. if y = w then Set.insert (x, z) A' else A')"
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   720
    by default (auto simp add: fun_eq_iff)
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   721
  show ?thesis using finite_fold_fold_keys[OF comp_fun_commute_relcomp_fold, of "Set t2" "{}" t1]
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   722
    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
   723
qed
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   724
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   725
lemma wf_set [code]:
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   726
  "wf (Set t) = acyclic (Set t)"
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   727
by (simp add: wf_iff_acyclic_if_finite)
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   728
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   729
lemma Min_fin_set_fold [code]:
53745
788730ab7da4 prefer Code.abort over code_abort
Andreas Lochbihler
parents: 51540
diff changeset
   730
  "Min (Set t) = 
56019
682bba24e474 hide implementation details
kuncar
parents: 55584
diff changeset
   731
  (if RBT.is_empty t
53745
788730ab7da4 prefer Code.abort over code_abort
Andreas Lochbihler
parents: 51540
diff changeset
   732
   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
   733
   else r_min_opt t)"
48623
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   734
proof -
51489
f738e6dbd844 fundamental revision of big operators on sets
haftmann
parents: 51115
diff changeset
   735
  have *: "semilattice (min :: 'a \<Rightarrow> 'a \<Rightarrow> 'a)" ..
f738e6dbd844 fundamental revision of big operators on sets
haftmann
parents: 51115
diff changeset
   736
  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
   737
  show ?thesis
53745
788730ab7da4 prefer Code.abort over code_abort
Andreas Lochbihler
parents: 51540
diff changeset
   738
    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
   739
qed
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   740
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   741
lemma Inf_fin_set_fold [code]:
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   742
  "Inf_fin (Set t) = Min (Set t)"
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   743
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
   744
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   745
lemma Inf_Set_fold:
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   746
  fixes t :: "('a :: {linorder, complete_lattice}, unit) rbt"
56019
682bba24e474 hide implementation details
kuncar
parents: 55584
diff changeset
   747
  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
   748
proof -
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   749
  have "comp_fun_commute (min :: 'a \<Rightarrow> 'a \<Rightarrow> 'a)" by default (simp add: fun_eq_iff ac_simps)
56019
682bba24e474 hide implementation details
kuncar
parents: 55584
diff changeset
   750
  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
   751
    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
   752
  then show ?thesis 
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   753
    by (auto simp add: Inf_fold_inf inf_min empty_Set[symmetric] r_min_eq_r_min_opt[symmetric] r_min_alt_def)
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   754
qed
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   755
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   756
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
   757
declare Inf'_def[symmetric, code_unfold]
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   758
declare Inf_Set_fold[folded Inf'_def, code]
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   759
56212
3253aaf73a01 consolidated theorem names containing INFI and SUPR: have INF and SUP instead uniformly
haftmann
parents: 56019
diff changeset
   760
lemma INF_Set_fold [code]:
54263
c4159fe6fa46 move Lubs from HOL to HOL-Library (replaced by conditionally complete lattices)
hoelzl
parents: 53955
diff changeset
   761
  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
   762
  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
   763
proof -
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   764
  have "comp_fun_commute ((inf :: 'a \<Rightarrow> 'a \<Rightarrow> 'a) \<circ> f)" 
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   765
    by default (auto simp add: fun_eq_iff ac_simps)
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   766
  then show ?thesis
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   767
    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
   768
qed
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   769
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   770
lemma Max_fin_set_fold [code]:
53745
788730ab7da4 prefer Code.abort over code_abort
Andreas Lochbihler
parents: 51540
diff changeset
   771
  "Max (Set t) = 
56019
682bba24e474 hide implementation details
kuncar
parents: 55584
diff changeset
   772
  (if RBT.is_empty t
53745
788730ab7da4 prefer Code.abort over code_abort
Andreas Lochbihler
parents: 51540
diff changeset
   773
   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
   774
   else r_max_opt t)"
48623
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   775
proof -
51489
f738e6dbd844 fundamental revision of big operators on sets
haftmann
parents: 51115
diff changeset
   776
  have *: "semilattice (max :: 'a \<Rightarrow> 'a \<Rightarrow> 'a)" ..
f738e6dbd844 fundamental revision of big operators on sets
haftmann
parents: 51115
diff changeset
   777
  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
   778
  show ?thesis
53745
788730ab7da4 prefer Code.abort over code_abort
Andreas Lochbihler
parents: 51540
diff changeset
   779
    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
   780
qed
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   781
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   782
lemma Sup_fin_set_fold [code]:
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   783
  "Sup_fin (Set t) = Max (Set t)"
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   784
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
   785
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   786
lemma Sup_Set_fold:
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   787
  fixes t :: "('a :: {linorder, complete_lattice}, unit) rbt"
56019
682bba24e474 hide implementation details
kuncar
parents: 55584
diff changeset
   788
  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
   789
proof -
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   790
  have "comp_fun_commute (max :: 'a \<Rightarrow> 'a \<Rightarrow> 'a)" by default (simp add: fun_eq_iff ac_simps)
56019
682bba24e474 hide implementation details
kuncar
parents: 55584
diff changeset
   791
  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
   792
    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
   793
  then show ?thesis 
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   794
    by (auto simp add: Sup_fold_sup sup_max empty_Set[symmetric] r_max_eq_r_max_opt[symmetric] r_max_alt_def)
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   795
qed
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   796
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   797
definition Sup' :: "'a :: {linorder, complete_lattice} set \<Rightarrow> 'a" where [code del]: "Sup' x = Sup x"
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   798
declare Sup'_def[symmetric, code_unfold]
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   799
declare Sup_Set_fold[folded Sup'_def, code]
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   800
56212
3253aaf73a01 consolidated theorem names containing INFI and SUPR: have INF and SUP instead uniformly
haftmann
parents: 56019
diff changeset
   801
lemma SUP_Set_fold [code]:
54263
c4159fe6fa46 move Lubs from HOL to HOL-Library (replaced by conditionally complete lattices)
hoelzl
parents: 53955
diff changeset
   802
  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
   803
  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
   804
proof -
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   805
  have "comp_fun_commute ((sup :: 'a \<Rightarrow> 'a \<Rightarrow> 'a) \<circ> f)" 
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   806
    by default (auto simp add: fun_eq_iff ac_simps)
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   807
  then show ?thesis
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   808
    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
   809
qed
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   810
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   811
lemma sorted_list_set[code]:
56019
682bba24e474 hide implementation details
kuncar
parents: 55584
diff changeset
   812
  "sorted_list_of_set (Set t) = RBT.keys t"
48623
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   813
by (auto simp add: set_keys intro: sorted_distinct_set_unique) 
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   814
53955
436649a2ed62 added Bleast code eqns for RBT
nipkow
parents: 53745
diff changeset
   815
lemma Bleast_code [code]:
56019
682bba24e474 hide implementation details
kuncar
parents: 55584
diff changeset
   816
 "Bleast (Set t) P = (case filter P (RBT.keys t) of
53955
436649a2ed62 added Bleast code eqns for RBT
nipkow
parents: 53745
diff changeset
   817
    x#xs \<Rightarrow> x |
436649a2ed62 added Bleast code eqns for RBT
nipkow
parents: 53745
diff changeset
   818
    [] \<Rightarrow> abort_Bleast (Set t) P)"
56019
682bba24e474 hide implementation details
kuncar
parents: 55584
diff changeset
   819
proof (cases "filter P (RBT.keys t)")
53955
436649a2ed62 added Bleast code eqns for RBT
nipkow
parents: 53745
diff changeset
   820
  case Nil thus ?thesis by (simp add: Bleast_def abort_Bleast_def)
436649a2ed62 added Bleast code eqns for RBT
nipkow
parents: 53745
diff changeset
   821
next
436649a2ed62 added Bleast code eqns for RBT
nipkow
parents: 53745
diff changeset
   822
  case (Cons x ys)
436649a2ed62 added Bleast code eqns for RBT
nipkow
parents: 53745
diff changeset
   823
  have "(LEAST x. x \<in> Set t \<and> P x) = x"
436649a2ed62 added Bleast code eqns for RBT
nipkow
parents: 53745
diff changeset
   824
  proof (rule Least_equality)
436649a2ed62 added Bleast code eqns for RBT
nipkow
parents: 53745
diff changeset
   825
    show "x \<in> Set t \<and> P x" using Cons[symmetric]
436649a2ed62 added Bleast code eqns for RBT
nipkow
parents: 53745
diff changeset
   826
      by(auto simp add: set_keys Cons_eq_filter_iff)
436649a2ed62 added Bleast code eqns for RBT
nipkow
parents: 53745
diff changeset
   827
    next
436649a2ed62 added Bleast code eqns for RBT
nipkow
parents: 53745
diff changeset
   828
      fix y assume "y : Set t \<and> P y"
436649a2ed62 added Bleast code eqns for RBT
nipkow
parents: 53745
diff changeset
   829
      then show "x \<le> y" using Cons[symmetric]
436649a2ed62 added Bleast code eqns for RBT
nipkow
parents: 53745
diff changeset
   830
        by(auto simp add: set_keys Cons_eq_filter_iff)
436649a2ed62 added Bleast code eqns for RBT
nipkow
parents: 53745
diff changeset
   831
          (metis sorted_Cons sorted_append sorted_keys)
436649a2ed62 added Bleast code eqns for RBT
nipkow
parents: 53745
diff changeset
   832
  qed
436649a2ed62 added Bleast code eqns for RBT
nipkow
parents: 53745
diff changeset
   833
  thus ?thesis using Cons by (simp add: Bleast_def)
436649a2ed62 added Bleast code eqns for RBT
nipkow
parents: 53745
diff changeset
   834
qed
436649a2ed62 added Bleast code eqns for RBT
nipkow
parents: 53745
diff changeset
   835
48623
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   836
hide_const (open) RBT_Set.Set RBT_Set.Coset
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   837
bea613f2543d implementation of sets by RBT trees for the code generator
kuncar
parents:
diff changeset
   838
end