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