src/HOL/Library/RBT.thy
author wenzelm
Wed, 08 Mar 2017 10:50:59 +0100
changeset 65151 a7394aa4d21c
parent 63219 a5697f7a3322
permissions -rw-r--r--
tuned proofs;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
48622
caaa1a02c650 use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents: 47450
diff changeset
     1
(*  Title:      HOL/Library/RBT.thy
caaa1a02c650 use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents: 47450
diff changeset
     2
    Author:     Lukas Bulwahn and Ondrej Kuncar
caaa1a02c650 use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents: 47450
diff changeset
     3
*)
35617
a6528fb99641 added Table.thy
haftmann
parents:
diff changeset
     4
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 58881
diff changeset
     5
section \<open>Abstract type of RBT trees\<close>
35617
a6528fb99641 added Table.thy
haftmann
parents:
diff changeset
     6
48622
caaa1a02c650 use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents: 47450
diff changeset
     7
theory RBT 
53013
3fbcfa911863 remove unnecessary dependencies on Library/Quotient_*
kuncar
parents: 51375
diff changeset
     8
imports Main RBT_Impl
35617
a6528fb99641 added Table.thy
haftmann
parents:
diff changeset
     9
begin
a6528fb99641 added Table.thy
haftmann
parents:
diff changeset
    10
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 58881
diff changeset
    11
subsection \<open>Type definition\<close>
35617
a6528fb99641 added Table.thy
haftmann
parents:
diff changeset
    12
61260
e6f03fae14d5 explicit indication of overloaded typedefs;
wenzelm
parents: 61076
diff changeset
    13
typedef (overloaded) ('a, 'b) rbt = "{t :: ('a::linorder, 'b) RBT_Impl.rbt. is_rbt t}"
36147
b43b22f63665 theory RBT with abstract type of red-black trees backed by implementation RBT_Impl
haftmann
parents: 36111
diff changeset
    14
  morphisms impl_of RBT
48622
caaa1a02c650 use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents: 47450
diff changeset
    15
proof -
caaa1a02c650 use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents: 47450
diff changeset
    16
  have "RBT_Impl.Empty \<in> ?rbt" by simp
caaa1a02c650 use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents: 47450
diff changeset
    17
  then show ?thesis ..
35617
a6528fb99641 added Table.thy
haftmann
parents:
diff changeset
    18
qed
a6528fb99641 added Table.thy
haftmann
parents:
diff changeset
    19
39380
5a2662c1e44a established emerging canonical names *_eqI and *_eq_iff
haftmann
parents: 39302
diff changeset
    20
lemma rbt_eq_iff:
5a2662c1e44a established emerging canonical names *_eqI and *_eq_iff
haftmann
parents: 39302
diff changeset
    21
  "t1 = t2 \<longleftrightarrow> impl_of t1 = impl_of t2"
5a2662c1e44a established emerging canonical names *_eqI and *_eq_iff
haftmann
parents: 39302
diff changeset
    22
  by (simp add: impl_of_inject)
5a2662c1e44a established emerging canonical names *_eqI and *_eq_iff
haftmann
parents: 39302
diff changeset
    23
5a2662c1e44a established emerging canonical names *_eqI and *_eq_iff
haftmann
parents: 39302
diff changeset
    24
lemma rbt_eqI:
5a2662c1e44a established emerging canonical names *_eqI and *_eq_iff
haftmann
parents: 39302
diff changeset
    25
  "impl_of t1 = impl_of t2 \<Longrightarrow> t1 = t2"
5a2662c1e44a established emerging canonical names *_eqI and *_eq_iff
haftmann
parents: 39302
diff changeset
    26
  by (simp add: rbt_eq_iff)
5a2662c1e44a established emerging canonical names *_eqI and *_eq_iff
haftmann
parents: 39302
diff changeset
    27
36147
b43b22f63665 theory RBT with abstract type of red-black trees backed by implementation RBT_Impl
haftmann
parents: 36111
diff changeset
    28
lemma is_rbt_impl_of [simp, intro]:
b43b22f63665 theory RBT with abstract type of red-black trees backed by implementation RBT_Impl
haftmann
parents: 36111
diff changeset
    29
  "is_rbt (impl_of t)"
b43b22f63665 theory RBT with abstract type of red-black trees backed by implementation RBT_Impl
haftmann
parents: 36111
diff changeset
    30
  using impl_of [of t] by simp
35617
a6528fb99641 added Table.thy
haftmann
parents:
diff changeset
    31
39380
5a2662c1e44a established emerging canonical names *_eqI and *_eq_iff
haftmann
parents: 39302
diff changeset
    32
lemma RBT_impl_of [simp, code abstype]:
36147
b43b22f63665 theory RBT with abstract type of red-black trees backed by implementation RBT_Impl
haftmann
parents: 36111
diff changeset
    33
  "RBT (impl_of t) = t"
b43b22f63665 theory RBT with abstract type of red-black trees backed by implementation RBT_Impl
haftmann
parents: 36111
diff changeset
    34
  by (simp add: impl_of_inverse)
35617
a6528fb99641 added Table.thy
haftmann
parents:
diff changeset
    35
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 58881
diff changeset
    36
subsection \<open>Primitive operations\<close>
35617
a6528fb99641 added Table.thy
haftmann
parents:
diff changeset
    37
48622
caaa1a02c650 use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents: 47450
diff changeset
    38
setup_lifting type_definition_rbt
35617
a6528fb99641 added Table.thy
haftmann
parents:
diff changeset
    39
61076
bdc1e2f0a86a eliminated \<Colon>;
wenzelm
parents: 60500
diff changeset
    40
lift_definition lookup :: "('a::linorder, 'b) rbt \<Rightarrow> 'a \<rightharpoonup> 'b" is "rbt_lookup" .
35617
a6528fb99641 added Table.thy
haftmann
parents:
diff changeset
    41
61076
bdc1e2f0a86a eliminated \<Colon>;
wenzelm
parents: 60500
diff changeset
    42
lift_definition empty :: "('a::linorder, 'b) rbt" is RBT_Impl.Empty 
48622
caaa1a02c650 use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents: 47450
diff changeset
    43
by (simp add: empty_def)
35617
a6528fb99641 added Table.thy
haftmann
parents:
diff changeset
    44
61076
bdc1e2f0a86a eliminated \<Colon>;
wenzelm
parents: 60500
diff changeset
    45
lift_definition insert :: "'a::linorder \<Rightarrow> 'b \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt" is "rbt_insert" 
48622
caaa1a02c650 use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents: 47450
diff changeset
    46
by simp
35617
a6528fb99641 added Table.thy
haftmann
parents:
diff changeset
    47
61076
bdc1e2f0a86a eliminated \<Colon>;
wenzelm
parents: 60500
diff changeset
    48
lift_definition delete :: "'a::linorder \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt" is "rbt_delete" 
48622
caaa1a02c650 use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents: 47450
diff changeset
    49
by simp
35617
a6528fb99641 added Table.thy
haftmann
parents:
diff changeset
    50
61076
bdc1e2f0a86a eliminated \<Colon>;
wenzelm
parents: 60500
diff changeset
    51
lift_definition entries :: "('a::linorder, 'b) rbt \<Rightarrow> ('a \<times> 'b) list" is RBT_Impl.entries .
55565
f663fc1e653b simplify proofs because of the stronger reflexivity prover
kuncar
parents: 55466
diff changeset
    52
61076
bdc1e2f0a86a eliminated \<Colon>;
wenzelm
parents: 60500
diff changeset
    53
lift_definition keys :: "('a::linorder, 'b) rbt \<Rightarrow> 'a list" is RBT_Impl.keys .
35617
a6528fb99641 added Table.thy
haftmann
parents:
diff changeset
    54
61076
bdc1e2f0a86a eliminated \<Colon>;
wenzelm
parents: 60500
diff changeset
    55
lift_definition bulkload :: "('a::linorder \<times> 'b) list \<Rightarrow> ('a, 'b) rbt" is "rbt_bulkload" ..
35617
a6528fb99641 added Table.thy
haftmann
parents:
diff changeset
    56
61076
bdc1e2f0a86a eliminated \<Colon>;
wenzelm
parents: 60500
diff changeset
    57
lift_definition map_entry :: "'a \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> ('a::linorder, 'b) rbt \<Rightarrow> ('a, 'b) rbt" is rbt_map_entry
48622
caaa1a02c650 use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents: 47450
diff changeset
    58
by simp
35617
a6528fb99641 added Table.thy
haftmann
parents:
diff changeset
    59
61076
bdc1e2f0a86a eliminated \<Colon>;
wenzelm
parents: 60500
diff changeset
    60
lift_definition map :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> ('a::linorder, 'b) rbt \<Rightarrow> ('a, 'c) rbt" is RBT_Impl.map
48622
caaa1a02c650 use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents: 47450
diff changeset
    61
by simp
35617
a6528fb99641 added Table.thy
haftmann
parents:
diff changeset
    62
61076
bdc1e2f0a86a eliminated \<Colon>;
wenzelm
parents: 60500
diff changeset
    63
lift_definition fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'c) \<Rightarrow> ('a::linorder, 'b) rbt \<Rightarrow> 'c \<Rightarrow> 'c"  is RBT_Impl.fold .
35617
a6528fb99641 added Table.thy
haftmann
parents:
diff changeset
    64
61076
bdc1e2f0a86a eliminated \<Colon>;
wenzelm
parents: 60500
diff changeset
    65
lift_definition union :: "('a::linorder, 'b) rbt \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt" is "rbt_union"
48622
caaa1a02c650 use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents: 47450
diff changeset
    66
by (simp add: rbt_union_is_rbt)
35617
a6528fb99641 added Table.thy
haftmann
parents:
diff changeset
    67
48622
caaa1a02c650 use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents: 47450
diff changeset
    68
lift_definition foldi :: "('c \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'c) \<Rightarrow> ('a :: linorder, 'b) rbt \<Rightarrow> 'c \<Rightarrow> 'c"
55565
f663fc1e653b simplify proofs because of the stronger reflexivity prover
kuncar
parents: 55466
diff changeset
    69
  is RBT_Impl.foldi .
63194
0b7bdb75f451 Added code generation for PMFs
eberlm
parents: 61260
diff changeset
    70
  
0b7bdb75f451 Added code generation for PMFs
eberlm
parents: 61260
diff changeset
    71
lift_definition combine_with_key :: "('a \<Rightarrow> 'b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a::linorder, 'b) rbt \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt"
0b7bdb75f451 Added code generation for PMFs
eberlm
parents: 61260
diff changeset
    72
  is RBT_Impl.rbt_union_with_key by (rule is_rbt_rbt_unionwk)
0b7bdb75f451 Added code generation for PMFs
eberlm
parents: 61260
diff changeset
    73
0b7bdb75f451 Added code generation for PMFs
eberlm
parents: 61260
diff changeset
    74
lift_definition combine :: "('b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a::linorder, 'b) rbt \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt"
0b7bdb75f451 Added code generation for PMFs
eberlm
parents: 61260
diff changeset
    75
  is RBT_Impl.rbt_union_with by (rule rbt_unionw_is_rbt)
35617
a6528fb99641 added Table.thy
haftmann
parents:
diff changeset
    76
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 58881
diff changeset
    77
subsection \<open>Derived operations\<close>
35617
a6528fb99641 added Table.thy
haftmann
parents:
diff changeset
    78
61076
bdc1e2f0a86a eliminated \<Colon>;
wenzelm
parents: 60500
diff changeset
    79
definition is_empty :: "('a::linorder, 'b) rbt \<Rightarrow> bool" where
36147
b43b22f63665 theory RBT with abstract type of red-black trees backed by implementation RBT_Impl
haftmann
parents: 36111
diff changeset
    80
  [code]: "is_empty t = (case impl_of t of RBT_Impl.Empty \<Rightarrow> True | _ \<Rightarrow> False)"
35617
a6528fb99641 added Table.thy
haftmann
parents:
diff changeset
    81
63194
0b7bdb75f451 Added code generation for PMFs
eberlm
parents: 61260
diff changeset
    82
(* TODO: Is deleting more efficient than re-building the tree? 
0b7bdb75f451 Added code generation for PMFs
eberlm
parents: 61260
diff changeset
    83
   (Probably more difficult to prove though *)
0b7bdb75f451 Added code generation for PMFs
eberlm
parents: 61260
diff changeset
    84
definition filter :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a::linorder, 'b) rbt \<Rightarrow> ('a, 'b) rbt" where
0b7bdb75f451 Added code generation for PMFs
eberlm
parents: 61260
diff changeset
    85
  [code]: "filter P t = fold (\<lambda>k v t. if P k v then insert k v t else t) t empty" 
35617
a6528fb99641 added Table.thy
haftmann
parents:
diff changeset
    86
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 58881
diff changeset
    87
subsection \<open>Abstract lookup properties\<close>
35617
a6528fb99641 added Table.thy
haftmann
parents:
diff changeset
    88
36147
b43b22f63665 theory RBT with abstract type of red-black trees backed by implementation RBT_Impl
haftmann
parents: 36111
diff changeset
    89
lemma lookup_RBT:
47450
2ada2be850cb move RBT implementation into type class contexts
Andreas Lochbihler
parents: 46565
diff changeset
    90
  "is_rbt t \<Longrightarrow> lookup (RBT t) = rbt_lookup t"
36147
b43b22f63665 theory RBT with abstract type of red-black trees backed by implementation RBT_Impl
haftmann
parents: 36111
diff changeset
    91
  by (simp add: lookup_def RBT_inverse)
35617
a6528fb99641 added Table.thy
haftmann
parents:
diff changeset
    92
36147
b43b22f63665 theory RBT with abstract type of red-black trees backed by implementation RBT_Impl
haftmann
parents: 36111
diff changeset
    93
lemma lookup_impl_of:
47450
2ada2be850cb move RBT implementation into type class contexts
Andreas Lochbihler
parents: 46565
diff changeset
    94
  "rbt_lookup (impl_of t) = lookup t"
48622
caaa1a02c650 use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents: 47450
diff changeset
    95
  by transfer (rule refl)
35617
a6528fb99641 added Table.thy
haftmann
parents:
diff changeset
    96
36147
b43b22f63665 theory RBT with abstract type of red-black trees backed by implementation RBT_Impl
haftmann
parents: 36111
diff changeset
    97
lemma entries_impl_of:
b43b22f63665 theory RBT with abstract type of red-black trees backed by implementation RBT_Impl
haftmann
parents: 36111
diff changeset
    98
  "RBT_Impl.entries (impl_of t) = entries t"
48622
caaa1a02c650 use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents: 47450
diff changeset
    99
  by transfer (rule refl)
35617
a6528fb99641 added Table.thy
haftmann
parents:
diff changeset
   100
36147
b43b22f63665 theory RBT with abstract type of red-black trees backed by implementation RBT_Impl
haftmann
parents: 36111
diff changeset
   101
lemma keys_impl_of:
b43b22f63665 theory RBT with abstract type of red-black trees backed by implementation RBT_Impl
haftmann
parents: 36111
diff changeset
   102
  "RBT_Impl.keys (impl_of t) = keys t"
48622
caaa1a02c650 use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents: 47450
diff changeset
   103
  by transfer (rule refl)
36111
5844017e31f8 implementation of mappings by rbts
haftmann
parents: 35617
diff changeset
   104
49927
cde0a46b4224 new theorem
kuncar
parents: 49834
diff changeset
   105
lemma lookup_keys: 
cde0a46b4224 new theorem
kuncar
parents: 49834
diff changeset
   106
  "dom (lookup t) = set (keys t)" 
cde0a46b4224 new theorem
kuncar
parents: 49834
diff changeset
   107
  by transfer (simp add: rbt_lookup_keys)
cde0a46b4224 new theorem
kuncar
parents: 49834
diff changeset
   108
35617
a6528fb99641 added Table.thy
haftmann
parents:
diff changeset
   109
lemma lookup_empty [simp]:
a6528fb99641 added Table.thy
haftmann
parents:
diff changeset
   110
  "lookup empty = Map.empty"
39302
d7728f65b353 renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
nipkow
parents: 39198
diff changeset
   111
  by (simp add: empty_def lookup_RBT fun_eq_iff)
35617
a6528fb99641 added Table.thy
haftmann
parents:
diff changeset
   112
36147
b43b22f63665 theory RBT with abstract type of red-black trees backed by implementation RBT_Impl
haftmann
parents: 36111
diff changeset
   113
lemma lookup_insert [simp]:
b43b22f63665 theory RBT with abstract type of red-black trees backed by implementation RBT_Impl
haftmann
parents: 36111
diff changeset
   114
  "lookup (insert k v t) = (lookup t)(k \<mapsto> v)"
48622
caaa1a02c650 use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents: 47450
diff changeset
   115
  by transfer (rule rbt_lookup_rbt_insert)
35617
a6528fb99641 added Table.thy
haftmann
parents:
diff changeset
   116
a6528fb99641 added Table.thy
haftmann
parents:
diff changeset
   117
lemma lookup_delete [simp]:
a6528fb99641 added Table.thy
haftmann
parents:
diff changeset
   118
  "lookup (delete k t) = (lookup t)(k := None)"
48622
caaa1a02c650 use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents: 47450
diff changeset
   119
  by transfer (simp add: rbt_lookup_rbt_delete restrict_complement_singleton_eq)
35617
a6528fb99641 added Table.thy
haftmann
parents:
diff changeset
   120
a6528fb99641 added Table.thy
haftmann
parents:
diff changeset
   121
lemma map_of_entries [simp]:
a6528fb99641 added Table.thy
haftmann
parents:
diff changeset
   122
  "map_of (entries t) = lookup t"
48622
caaa1a02c650 use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents: 47450
diff changeset
   123
  by transfer (simp add: map_of_entries)
35617
a6528fb99641 added Table.thy
haftmann
parents:
diff changeset
   124
36111
5844017e31f8 implementation of mappings by rbts
haftmann
parents: 35617
diff changeset
   125
lemma entries_lookup:
5844017e31f8 implementation of mappings by rbts
haftmann
parents: 35617
diff changeset
   126
  "entries t1 = entries t2 \<longleftrightarrow> lookup t1 = lookup t2"
48622
caaa1a02c650 use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents: 47450
diff changeset
   127
  by transfer (simp add: entries_rbt_lookup)
36111
5844017e31f8 implementation of mappings by rbts
haftmann
parents: 35617
diff changeset
   128
35617
a6528fb99641 added Table.thy
haftmann
parents:
diff changeset
   129
lemma lookup_bulkload [simp]:
a6528fb99641 added Table.thy
haftmann
parents:
diff changeset
   130
  "lookup (bulkload xs) = map_of xs"
48622
caaa1a02c650 use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents: 47450
diff changeset
   131
  by transfer (rule rbt_lookup_rbt_bulkload)
35617
a6528fb99641 added Table.thy
haftmann
parents:
diff changeset
   132
a6528fb99641 added Table.thy
haftmann
parents:
diff changeset
   133
lemma lookup_map_entry [simp]:
55466
786edc984c98 merged 'Option.map' and 'Option.map_option'
blanchet
parents: 55414
diff changeset
   134
  "lookup (map_entry k f t) = (lookup t)(k := map_option f (lookup t k))"
48622
caaa1a02c650 use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents: 47450
diff changeset
   135
  by transfer (rule rbt_lookup_rbt_map_entry)
35617
a6528fb99641 added Table.thy
haftmann
parents:
diff changeset
   136
a6528fb99641 added Table.thy
haftmann
parents:
diff changeset
   137
lemma lookup_map [simp]:
55466
786edc984c98 merged 'Option.map' and 'Option.map_option'
blanchet
parents: 55414
diff changeset
   138
  "lookup (map f t) k = map_option (f k) (lookup t k)"
48622
caaa1a02c650 use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents: 47450
diff changeset
   139
  by transfer (rule rbt_lookup_map)
35617
a6528fb99641 added Table.thy
haftmann
parents:
diff changeset
   140
63194
0b7bdb75f451 Added code generation for PMFs
eberlm
parents: 61260
diff changeset
   141
lemma lookup_combine_with_key [simp]:
0b7bdb75f451 Added code generation for PMFs
eberlm
parents: 61260
diff changeset
   142
  "lookup (combine_with_key f t1 t2) k = combine_options (f k) (lookup t1 k) (lookup t2 k)"
0b7bdb75f451 Added code generation for PMFs
eberlm
parents: 61260
diff changeset
   143
  by transfer (simp_all add: combine_options_def rbt_lookup_rbt_unionwk)
0b7bdb75f451 Added code generation for PMFs
eberlm
parents: 61260
diff changeset
   144
0b7bdb75f451 Added code generation for PMFs
eberlm
parents: 61260
diff changeset
   145
lemma combine_altdef: "combine f t1 t2 = combine_with_key (\<lambda>_. f) t1 t2"
0b7bdb75f451 Added code generation for PMFs
eberlm
parents: 61260
diff changeset
   146
  by transfer (simp add: rbt_union_with_def)
0b7bdb75f451 Added code generation for PMFs
eberlm
parents: 61260
diff changeset
   147
0b7bdb75f451 Added code generation for PMFs
eberlm
parents: 61260
diff changeset
   148
lemma lookup_combine [simp]:
0b7bdb75f451 Added code generation for PMFs
eberlm
parents: 61260
diff changeset
   149
  "lookup (combine f t1 t2) k = combine_options f (lookup t1 k) (lookup t2 k)"
0b7bdb75f451 Added code generation for PMFs
eberlm
parents: 61260
diff changeset
   150
  by (simp add: combine_altdef)
0b7bdb75f451 Added code generation for PMFs
eberlm
parents: 61260
diff changeset
   151
35617
a6528fb99641 added Table.thy
haftmann
parents:
diff changeset
   152
lemma fold_fold:
55414
eab03e9cee8a renamed '{prod,sum,bool,unit}_case' to 'case_...'
blanchet
parents: 53013
diff changeset
   153
  "fold f t = List.fold (case_prod f) (entries t)"
48622
caaa1a02c650 use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents: 47450
diff changeset
   154
  by transfer (rule RBT_Impl.fold_def)
caaa1a02c650 use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents: 47450
diff changeset
   155
caaa1a02c650 use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents: 47450
diff changeset
   156
lemma impl_of_empty:
caaa1a02c650 use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents: 47450
diff changeset
   157
  "impl_of empty = RBT_Impl.Empty"
caaa1a02c650 use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents: 47450
diff changeset
   158
  by transfer (rule refl)
35617
a6528fb99641 added Table.thy
haftmann
parents:
diff changeset
   159
36111
5844017e31f8 implementation of mappings by rbts
haftmann
parents: 35617
diff changeset
   160
lemma is_empty_empty [simp]:
5844017e31f8 implementation of mappings by rbts
haftmann
parents: 35617
diff changeset
   161
  "is_empty t \<longleftrightarrow> t = empty"
48622
caaa1a02c650 use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents: 47450
diff changeset
   162
  unfolding is_empty_def by transfer (simp split: rbt.split)
36111
5844017e31f8 implementation of mappings by rbts
haftmann
parents: 35617
diff changeset
   163
5844017e31f8 implementation of mappings by rbts
haftmann
parents: 35617
diff changeset
   164
lemma RBT_lookup_empty [simp]: (*FIXME*)
47450
2ada2be850cb move RBT implementation into type class contexts
Andreas Lochbihler
parents: 46565
diff changeset
   165
  "rbt_lookup t = Map.empty \<longleftrightarrow> t = RBT_Impl.Empty"
39302
d7728f65b353 renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
nipkow
parents: 39198
diff changeset
   166
  by (cases t) (auto simp add: fun_eq_iff)
36111
5844017e31f8 implementation of mappings by rbts
haftmann
parents: 35617
diff changeset
   167
5844017e31f8 implementation of mappings by rbts
haftmann
parents: 35617
diff changeset
   168
lemma lookup_empty_empty [simp]:
5844017e31f8 implementation of mappings by rbts
haftmann
parents: 35617
diff changeset
   169
  "lookup t = Map.empty \<longleftrightarrow> t = empty"
48622
caaa1a02c650 use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents: 47450
diff changeset
   170
  by transfer (rule RBT_lookup_empty)
36111
5844017e31f8 implementation of mappings by rbts
haftmann
parents: 35617
diff changeset
   171
5844017e31f8 implementation of mappings by rbts
haftmann
parents: 35617
diff changeset
   172
lemma sorted_keys [iff]:
5844017e31f8 implementation of mappings by rbts
haftmann
parents: 35617
diff changeset
   173
  "sorted (keys t)"
48622
caaa1a02c650 use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents: 47450
diff changeset
   174
  by transfer (simp add: RBT_Impl.keys_def rbt_sorted_entries)
36111
5844017e31f8 implementation of mappings by rbts
haftmann
parents: 35617
diff changeset
   175
5844017e31f8 implementation of mappings by rbts
haftmann
parents: 35617
diff changeset
   176
lemma distinct_keys [iff]:
5844017e31f8 implementation of mappings by rbts
haftmann
parents: 35617
diff changeset
   177
  "distinct (keys t)"
48622
caaa1a02c650 use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents: 47450
diff changeset
   178
  by transfer (simp add: RBT_Impl.keys_def distinct_entries)
caaa1a02c650 use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents: 47450
diff changeset
   179
caaa1a02c650 use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents: 47450
diff changeset
   180
lemma finite_dom_lookup [simp, intro!]: "finite (dom (lookup t))"
caaa1a02c650 use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents: 47450
diff changeset
   181
  by transfer simp
caaa1a02c650 use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents: 47450
diff changeset
   182
caaa1a02c650 use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents: 47450
diff changeset
   183
lemma lookup_union: "lookup (union s t) = lookup s ++ lookup t"
caaa1a02c650 use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents: 47450
diff changeset
   184
  by transfer (simp add: rbt_lookup_rbt_union)
caaa1a02c650 use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents: 47450
diff changeset
   185
caaa1a02c650 use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents: 47450
diff changeset
   186
lemma lookup_in_tree: "(lookup t k = Some v) = ((k, v) \<in> set (entries t))"
caaa1a02c650 use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents: 47450
diff changeset
   187
  by transfer (simp add: rbt_lookup_in_tree)
caaa1a02c650 use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents: 47450
diff changeset
   188
caaa1a02c650 use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents: 47450
diff changeset
   189
lemma keys_entries: "(k \<in> set (keys t)) = (\<exists>v. (k, v) \<in> set (entries t))"
caaa1a02c650 use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents: 47450
diff changeset
   190
  by transfer (simp add: keys_entries)
caaa1a02c650 use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents: 47450
diff changeset
   191
caaa1a02c650 use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents: 47450
diff changeset
   192
lemma fold_def_alt:
55414
eab03e9cee8a renamed '{prod,sum,bool,unit}_case' to 'case_...'
blanchet
parents: 53013
diff changeset
   193
  "fold f t = List.fold (case_prod f) (entries t)"
48622
caaa1a02c650 use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents: 47450
diff changeset
   194
  by transfer (auto simp: RBT_Impl.fold_def)
caaa1a02c650 use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents: 47450
diff changeset
   195
caaa1a02c650 use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents: 47450
diff changeset
   196
lemma distinct_entries: "distinct (List.map fst (entries t))"
caaa1a02c650 use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents: 47450
diff changeset
   197
  by transfer (simp add: distinct_entries)
caaa1a02c650 use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents: 47450
diff changeset
   198
caaa1a02c650 use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents: 47450
diff changeset
   199
lemma non_empty_keys: "t \<noteq> empty \<Longrightarrow> keys t \<noteq> []"
caaa1a02c650 use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents: 47450
diff changeset
   200
  by transfer (simp add: non_empty_rbt_keys)
caaa1a02c650 use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents: 47450
diff changeset
   201
caaa1a02c650 use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents: 47450
diff changeset
   202
lemma keys_def_alt:
caaa1a02c650 use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents: 47450
diff changeset
   203
  "keys t = List.map fst (entries t)"
caaa1a02c650 use lifting/transfer formalization of RBT from Lift_RBT
kuncar
parents: 47450
diff changeset
   204
  by transfer (simp add: RBT_Impl.keys_def)
36111
5844017e31f8 implementation of mappings by rbts
haftmann
parents: 35617
diff changeset
   205
63194
0b7bdb75f451 Added code generation for PMFs
eberlm
parents: 61260
diff changeset
   206
context
0b7bdb75f451 Added code generation for PMFs
eberlm
parents: 61260
diff changeset
   207
begin
0b7bdb75f451 Added code generation for PMFs
eberlm
parents: 61260
diff changeset
   208
0b7bdb75f451 Added code generation for PMFs
eberlm
parents: 61260
diff changeset
   209
private lemma lookup_filter_aux:
0b7bdb75f451 Added code generation for PMFs
eberlm
parents: 61260
diff changeset
   210
  assumes "distinct (List.map fst xs)"
0b7bdb75f451 Added code generation for PMFs
eberlm
parents: 61260
diff changeset
   211
  shows   "lookup (List.fold (\<lambda>(k, v) t. if P k v then insert k v t else t) xs t) k =
0b7bdb75f451 Added code generation for PMFs
eberlm
parents: 61260
diff changeset
   212
             (case map_of xs k of 
0b7bdb75f451 Added code generation for PMFs
eberlm
parents: 61260
diff changeset
   213
                None \<Rightarrow> lookup t k
0b7bdb75f451 Added code generation for PMFs
eberlm
parents: 61260
diff changeset
   214
              | Some v \<Rightarrow> if P k v then Some v else lookup t k)"
0b7bdb75f451 Added code generation for PMFs
eberlm
parents: 61260
diff changeset
   215
  using assms by (induction xs arbitrary: t) (force split: option.splits)+
0b7bdb75f451 Added code generation for PMFs
eberlm
parents: 61260
diff changeset
   216
0b7bdb75f451 Added code generation for PMFs
eberlm
parents: 61260
diff changeset
   217
lemma lookup_filter: 
0b7bdb75f451 Added code generation for PMFs
eberlm
parents: 61260
diff changeset
   218
  "lookup (filter P t) k = 
0b7bdb75f451 Added code generation for PMFs
eberlm
parents: 61260
diff changeset
   219
     (case lookup t k of None \<Rightarrow> None | Some v \<Rightarrow> if P k v then Some v else None)"
0b7bdb75f451 Added code generation for PMFs
eberlm
parents: 61260
diff changeset
   220
  unfolding filter_def using lookup_filter_aux[of "entries t" P empty k]
0b7bdb75f451 Added code generation for PMFs
eberlm
parents: 61260
diff changeset
   221
  by (simp add: fold_fold distinct_entries split: option.splits)
0b7bdb75f451 Added code generation for PMFs
eberlm
parents: 61260
diff changeset
   222
  
0b7bdb75f451 Added code generation for PMFs
eberlm
parents: 61260
diff changeset
   223
end
0b7bdb75f451 Added code generation for PMFs
eberlm
parents: 61260
diff changeset
   224
0b7bdb75f451 Added code generation for PMFs
eberlm
parents: 61260
diff changeset
   225
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 58881
diff changeset
   226
subsection \<open>Quickcheck generators\<close>
45928
874845660119 adding quickcheck generators in some HOL-Library theories
bulwahn
parents: 45694
diff changeset
   227
46565
ad21900e0ee9 subtype preprocessing in Quickcheck;
bulwahn
parents: 46133
diff changeset
   228
quickcheck_generator rbt predicate: is_rbt constructors: empty, insert
36111
5844017e31f8 implementation of mappings by rbts
haftmann
parents: 35617
diff changeset
   229
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 58881
diff changeset
   230
subsection \<open>Hide implementation details\<close>
56019
682bba24e474 hide implementation details
kuncar
parents: 55565
diff changeset
   231
682bba24e474 hide implementation details
kuncar
parents: 55565
diff changeset
   232
lifting_update rbt.lifting
682bba24e474 hide implementation details
kuncar
parents: 55565
diff changeset
   233
lifting_forget rbt.lifting
682bba24e474 hide implementation details
kuncar
parents: 55565
diff changeset
   234
682bba24e474 hide implementation details
kuncar
parents: 55565
diff changeset
   235
hide_const (open) impl_of empty lookup keys entries bulkload delete map fold union insert map_entry foldi 
63219
a5697f7a3322 Hid RBT.filter
Manuel Eberl <eberlm@in.tum.de>
parents: 63194
diff changeset
   236
  is_empty filter
56019
682bba24e474 hide implementation details
kuncar
parents: 55565
diff changeset
   237
hide_fact (open) empty_def lookup_def keys_def entries_def bulkload_def delete_def map_def fold_def 
63219
a5697f7a3322 Hid RBT.filter
Manuel Eberl <eberlm@in.tum.de>
parents: 63194
diff changeset
   238
  union_def insert_def map_entry_def foldi_def is_empty_def filter_def
56019
682bba24e474 hide implementation details
kuncar
parents: 55565
diff changeset
   239
35617
a6528fb99641 added Table.thy
haftmann
parents:
diff changeset
   240
end