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