src/HOL/Quotient_Examples/Lift_RBT.thy
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 47308 9caab698dbe4
child 47451 ab606e685d52
permissions -rw-r--r--
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions; tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
47308
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47097
diff changeset
     1
(*  Title:      HOL/Quotient_Examples/Lift_RBT.thy
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47097
diff changeset
     2
    Author:     Lukas Bulwahn and Ondrej Kuncar
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47097
diff changeset
     3
*)
45577
33b964e117bd adding another example for lifting definitions
bulwahn
parents:
diff changeset
     4
33b964e117bd adding another example for lifting definitions
bulwahn
parents:
diff changeset
     5
header {* Lifting operations of RBT trees *}
33b964e117bd adding another example for lifting definitions
bulwahn
parents:
diff changeset
     6
33b964e117bd adding another example for lifting definitions
bulwahn
parents:
diff changeset
     7
theory Lift_RBT 
33b964e117bd adding another example for lifting definitions
bulwahn
parents:
diff changeset
     8
imports Main "~~/src/HOL/Library/RBT_Impl"
33b964e117bd adding another example for lifting definitions
bulwahn
parents:
diff changeset
     9
begin
33b964e117bd adding another example for lifting definitions
bulwahn
parents:
diff changeset
    10
33b964e117bd adding another example for lifting definitions
bulwahn
parents:
diff changeset
    11
subsection {* Type definition *}
33b964e117bd adding another example for lifting definitions
bulwahn
parents:
diff changeset
    12
47097
987cb55cac44 fix example files
kuncar
parents: 47093
diff changeset
    13
typedef (open) ('a, 'b) rbt = "{t :: ('a\<Colon>linorder, 'b) RBT_Impl.rbt. is_rbt t}"
987cb55cac44 fix example files
kuncar
parents: 47093
diff changeset
    14
  morphisms impl_of RBT
987cb55cac44 fix example files
kuncar
parents: 47093
diff changeset
    15
proof -
987cb55cac44 fix example files
kuncar
parents: 47093
diff changeset
    16
  have "RBT_Impl.Empty \<in> ?rbt" by simp
987cb55cac44 fix example files
kuncar
parents: 47093
diff changeset
    17
  then show ?thesis ..
987cb55cac44 fix example files
kuncar
parents: 47093
diff changeset
    18
qed
45577
33b964e117bd adding another example for lifting definitions
bulwahn
parents:
diff changeset
    19
33b964e117bd adding another example for lifting definitions
bulwahn
parents:
diff changeset
    20
lemma rbt_eq_iff:
33b964e117bd adding another example for lifting definitions
bulwahn
parents:
diff changeset
    21
  "t1 = t2 \<longleftrightarrow> impl_of t1 = impl_of t2"
33b964e117bd adding another example for lifting definitions
bulwahn
parents:
diff changeset
    22
  by (simp add: impl_of_inject)
33b964e117bd adding another example for lifting definitions
bulwahn
parents:
diff changeset
    23
33b964e117bd adding another example for lifting definitions
bulwahn
parents:
diff changeset
    24
lemma rbt_eqI:
33b964e117bd adding another example for lifting definitions
bulwahn
parents:
diff changeset
    25
  "impl_of t1 = impl_of t2 \<Longrightarrow> t1 = t2"
33b964e117bd adding another example for lifting definitions
bulwahn
parents:
diff changeset
    26
  by (simp add: rbt_eq_iff)
33b964e117bd adding another example for lifting definitions
bulwahn
parents:
diff changeset
    27
33b964e117bd adding another example for lifting definitions
bulwahn
parents:
diff changeset
    28
lemma is_rbt_impl_of [simp, intro]:
33b964e117bd adding another example for lifting definitions
bulwahn
parents:
diff changeset
    29
  "is_rbt (impl_of t)"
33b964e117bd adding another example for lifting definitions
bulwahn
parents:
diff changeset
    30
  using impl_of [of t] by simp
33b964e117bd adding another example for lifting definitions
bulwahn
parents:
diff changeset
    31
33b964e117bd adding another example for lifting definitions
bulwahn
parents:
diff changeset
    32
lemma RBT_impl_of [simp, code abstype]:
33b964e117bd adding another example for lifting definitions
bulwahn
parents:
diff changeset
    33
  "RBT (impl_of t) = t"
33b964e117bd adding another example for lifting definitions
bulwahn
parents:
diff changeset
    34
  by (simp add: impl_of_inverse)
33b964e117bd adding another example for lifting definitions
bulwahn
parents:
diff changeset
    35
33b964e117bd adding another example for lifting definitions
bulwahn
parents:
diff changeset
    36
subsection {* Primitive operations *}
33b964e117bd adding another example for lifting definitions
bulwahn
parents:
diff changeset
    37
47097
987cb55cac44 fix example files
kuncar
parents: 47093
diff changeset
    38
setup_lifting type_definition_rbt
987cb55cac44 fix example files
kuncar
parents: 47093
diff changeset
    39
47308
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47097
diff changeset
    40
lift_definition lookup :: "('a\<Colon>linorder, 'b) rbt \<Rightarrow> 'a \<rightharpoonup> 'b" is "RBT_Impl.lookup" 
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47097
diff changeset
    41
by simp
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47097
diff changeset
    42
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47097
diff changeset
    43
lift_definition empty :: "('a\<Colon>linorder, 'b) rbt" is RBT_Impl.Empty 
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47097
diff changeset
    44
by (simp add: empty_def)
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47097
diff changeset
    45
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47097
diff changeset
    46
lift_definition insert :: "'a\<Colon>linorder \<Rightarrow> 'b \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt" is "RBT_Impl.insert" 
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47097
diff changeset
    47
by simp
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47097
diff changeset
    48
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47097
diff changeset
    49
lift_definition delete :: "'a\<Colon>linorder \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt" is "RBT_Impl.delete" 
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47097
diff changeset
    50
by simp
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47097
diff changeset
    51
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47097
diff changeset
    52
lift_definition entries :: "('a\<Colon>linorder, 'b) rbt \<Rightarrow> ('a \<times> 'b) list" is RBT_Impl.entries
47093
0516a6c1ea59 store the quotient theorem for every quotient
kuncar
parents: 47092
diff changeset
    53
by simp
45577
33b964e117bd adding another example for lifting definitions
bulwahn
parents:
diff changeset
    54
47308
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47097
diff changeset
    55
lift_definition keys :: "('a\<Colon>linorder, 'b) rbt \<Rightarrow> 'a list" is RBT_Impl.keys 
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47097
diff changeset
    56
by simp
45577
33b964e117bd adding another example for lifting definitions
bulwahn
parents:
diff changeset
    57
47308
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47097
diff changeset
    58
lift_definition bulkload :: "('a\<Colon>linorder \<times> 'b) list \<Rightarrow> ('a, 'b) rbt" is "RBT_Impl.bulkload" 
47097
987cb55cac44 fix example files
kuncar
parents: 47093
diff changeset
    59
by simp
45629
ef08425dd2d5 improved example to only use quotient_definitions; added lemmas to serve as possible replacement for the existing RBT theory
bulwahn
parents: 45577
diff changeset
    60
47308
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47097
diff changeset
    61
lift_definition map_entry :: "'a \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> ('a\<Colon>linorder, 'b) rbt \<Rightarrow> ('a, 'b) rbt" is RBT_Impl.map_entry 
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47097
diff changeset
    62
by simp
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47097
diff changeset
    63
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47097
diff changeset
    64
lift_definition map :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a\<Colon>linorder, 'b) rbt \<Rightarrow> ('a, 'b) rbt" is RBT_Impl.map
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47097
diff changeset
    65
by simp
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47097
diff changeset
    66
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47097
diff changeset
    67
lift_definition fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'c) \<Rightarrow> ('a\<Colon>linorder, 'b) rbt \<Rightarrow> 'c \<Rightarrow> 'c"  is RBT_Impl.fold 
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47097
diff changeset
    68
by simp
45629
ef08425dd2d5 improved example to only use quotient_definitions; added lemmas to serve as possible replacement for the existing RBT theory
bulwahn
parents: 45577
diff changeset
    69
47097
987cb55cac44 fix example files
kuncar
parents: 47093
diff changeset
    70
export_code lookup empty insert delete entries keys bulkload map_entry map fold in SML
45629
ef08425dd2d5 improved example to only use quotient_definitions; added lemmas to serve as possible replacement for the existing RBT theory
bulwahn
parents: 45577
diff changeset
    71
ef08425dd2d5 improved example to only use quotient_definitions; added lemmas to serve as possible replacement for the existing RBT theory
bulwahn
parents: 45577
diff changeset
    72
subsection {* Derived operations *}
ef08425dd2d5 improved example to only use quotient_definitions; added lemmas to serve as possible replacement for the existing RBT theory
bulwahn
parents: 45577
diff changeset
    73
ef08425dd2d5 improved example to only use quotient_definitions; added lemmas to serve as possible replacement for the existing RBT theory
bulwahn
parents: 45577
diff changeset
    74
definition is_empty :: "('a\<Colon>linorder, 'b) rbt \<Rightarrow> bool" where
ef08425dd2d5 improved example to only use quotient_definitions; added lemmas to serve as possible replacement for the existing RBT theory
bulwahn
parents: 45577
diff changeset
    75
  [code]: "is_empty t = (case impl_of t of RBT_Impl.Empty \<Rightarrow> True | _ \<Rightarrow> False)"
ef08425dd2d5 improved example to only use quotient_definitions; added lemmas to serve as possible replacement for the existing RBT theory
bulwahn
parents: 45577
diff changeset
    76
ef08425dd2d5 improved example to only use quotient_definitions; added lemmas to serve as possible replacement for the existing RBT theory
bulwahn
parents: 45577
diff changeset
    77
ef08425dd2d5 improved example to only use quotient_definitions; added lemmas to serve as possible replacement for the existing RBT theory
bulwahn
parents: 45577
diff changeset
    78
subsection {* Abstract lookup properties *}
ef08425dd2d5 improved example to only use quotient_definitions; added lemmas to serve as possible replacement for the existing RBT theory
bulwahn
parents: 45577
diff changeset
    79
ef08425dd2d5 improved example to only use quotient_definitions; added lemmas to serve as possible replacement for the existing RBT theory
bulwahn
parents: 45577
diff changeset
    80
(* TODO: obtain the following lemmas by lifting existing theorems. *)
ef08425dd2d5 improved example to only use quotient_definitions; added lemmas to serve as possible replacement for the existing RBT theory
bulwahn
parents: 45577
diff changeset
    81
ef08425dd2d5 improved example to only use quotient_definitions; added lemmas to serve as possible replacement for the existing RBT theory
bulwahn
parents: 45577
diff changeset
    82
lemma lookup_RBT:
ef08425dd2d5 improved example to only use quotient_definitions; added lemmas to serve as possible replacement for the existing RBT theory
bulwahn
parents: 45577
diff changeset
    83
  "is_rbt t \<Longrightarrow> lookup (RBT t) = RBT_Impl.lookup t"
ef08425dd2d5 improved example to only use quotient_definitions; added lemmas to serve as possible replacement for the existing RBT theory
bulwahn
parents: 45577
diff changeset
    84
  by (simp add: lookup_def RBT_inverse)
ef08425dd2d5 improved example to only use quotient_definitions; added lemmas to serve as possible replacement for the existing RBT theory
bulwahn
parents: 45577
diff changeset
    85
ef08425dd2d5 improved example to only use quotient_definitions; added lemmas to serve as possible replacement for the existing RBT theory
bulwahn
parents: 45577
diff changeset
    86
lemma lookup_impl_of:
ef08425dd2d5 improved example to only use quotient_definitions; added lemmas to serve as possible replacement for the existing RBT theory
bulwahn
parents: 45577
diff changeset
    87
  "RBT_Impl.lookup (impl_of t) = lookup t"
ef08425dd2d5 improved example to only use quotient_definitions; added lemmas to serve as possible replacement for the existing RBT theory
bulwahn
parents: 45577
diff changeset
    88
  by (simp add: lookup_def)
ef08425dd2d5 improved example to only use quotient_definitions; added lemmas to serve as possible replacement for the existing RBT theory
bulwahn
parents: 45577
diff changeset
    89
ef08425dd2d5 improved example to only use quotient_definitions; added lemmas to serve as possible replacement for the existing RBT theory
bulwahn
parents: 45577
diff changeset
    90
lemma entries_impl_of:
ef08425dd2d5 improved example to only use quotient_definitions; added lemmas to serve as possible replacement for the existing RBT theory
bulwahn
parents: 45577
diff changeset
    91
  "RBT_Impl.entries (impl_of t) = entries t"
ef08425dd2d5 improved example to only use quotient_definitions; added lemmas to serve as possible replacement for the existing RBT theory
bulwahn
parents: 45577
diff changeset
    92
  by (simp add: entries_def)
ef08425dd2d5 improved example to only use quotient_definitions; added lemmas to serve as possible replacement for the existing RBT theory
bulwahn
parents: 45577
diff changeset
    93
ef08425dd2d5 improved example to only use quotient_definitions; added lemmas to serve as possible replacement for the existing RBT theory
bulwahn
parents: 45577
diff changeset
    94
lemma keys_impl_of:
ef08425dd2d5 improved example to only use quotient_definitions; added lemmas to serve as possible replacement for the existing RBT theory
bulwahn
parents: 45577
diff changeset
    95
  "RBT_Impl.keys (impl_of t) = keys t"
ef08425dd2d5 improved example to only use quotient_definitions; added lemmas to serve as possible replacement for the existing RBT theory
bulwahn
parents: 45577
diff changeset
    96
  by (simp add: keys_def)
ef08425dd2d5 improved example to only use quotient_definitions; added lemmas to serve as possible replacement for the existing RBT theory
bulwahn
parents: 45577
diff changeset
    97
ef08425dd2d5 improved example to only use quotient_definitions; added lemmas to serve as possible replacement for the existing RBT theory
bulwahn
parents: 45577
diff changeset
    98
lemma lookup_empty [simp]:
ef08425dd2d5 improved example to only use quotient_definitions; added lemmas to serve as possible replacement for the existing RBT theory
bulwahn
parents: 45577
diff changeset
    99
  "lookup empty = Map.empty"
ef08425dd2d5 improved example to only use quotient_definitions; added lemmas to serve as possible replacement for the existing RBT theory
bulwahn
parents: 45577
diff changeset
   100
  by (simp add: empty_def lookup_RBT fun_eq_iff)
ef08425dd2d5 improved example to only use quotient_definitions; added lemmas to serve as possible replacement for the existing RBT theory
bulwahn
parents: 45577
diff changeset
   101
ef08425dd2d5 improved example to only use quotient_definitions; added lemmas to serve as possible replacement for the existing RBT theory
bulwahn
parents: 45577
diff changeset
   102
lemma lookup_insert [simp]:
ef08425dd2d5 improved example to only use quotient_definitions; added lemmas to serve as possible replacement for the existing RBT theory
bulwahn
parents: 45577
diff changeset
   103
  "lookup (insert k v t) = (lookup t)(k \<mapsto> v)"
ef08425dd2d5 improved example to only use quotient_definitions; added lemmas to serve as possible replacement for the existing RBT theory
bulwahn
parents: 45577
diff changeset
   104
  by (simp add: insert_def lookup_RBT lookup_insert lookup_impl_of)
45577
33b964e117bd adding another example for lifting definitions
bulwahn
parents:
diff changeset
   105
45629
ef08425dd2d5 improved example to only use quotient_definitions; added lemmas to serve as possible replacement for the existing RBT theory
bulwahn
parents: 45577
diff changeset
   106
lemma lookup_delete [simp]:
ef08425dd2d5 improved example to only use quotient_definitions; added lemmas to serve as possible replacement for the existing RBT theory
bulwahn
parents: 45577
diff changeset
   107
  "lookup (delete k t) = (lookup t)(k := None)"
ef08425dd2d5 improved example to only use quotient_definitions; added lemmas to serve as possible replacement for the existing RBT theory
bulwahn
parents: 45577
diff changeset
   108
  by (simp add: delete_def lookup_RBT RBT_Impl.lookup_delete lookup_impl_of restrict_complement_singleton_eq)
ef08425dd2d5 improved example to only use quotient_definitions; added lemmas to serve as possible replacement for the existing RBT theory
bulwahn
parents: 45577
diff changeset
   109
ef08425dd2d5 improved example to only use quotient_definitions; added lemmas to serve as possible replacement for the existing RBT theory
bulwahn
parents: 45577
diff changeset
   110
lemma map_of_entries [simp]:
ef08425dd2d5 improved example to only use quotient_definitions; added lemmas to serve as possible replacement for the existing RBT theory
bulwahn
parents: 45577
diff changeset
   111
  "map_of (entries t) = lookup t"
ef08425dd2d5 improved example to only use quotient_definitions; added lemmas to serve as possible replacement for the existing RBT theory
bulwahn
parents: 45577
diff changeset
   112
  by (simp add: entries_def map_of_entries lookup_impl_of)
ef08425dd2d5 improved example to only use quotient_definitions; added lemmas to serve as possible replacement for the existing RBT theory
bulwahn
parents: 45577
diff changeset
   113
ef08425dd2d5 improved example to only use quotient_definitions; added lemmas to serve as possible replacement for the existing RBT theory
bulwahn
parents: 45577
diff changeset
   114
lemma entries_lookup:
ef08425dd2d5 improved example to only use quotient_definitions; added lemmas to serve as possible replacement for the existing RBT theory
bulwahn
parents: 45577
diff changeset
   115
  "entries t1 = entries t2 \<longleftrightarrow> lookup t1 = lookup t2"
ef08425dd2d5 improved example to only use quotient_definitions; added lemmas to serve as possible replacement for the existing RBT theory
bulwahn
parents: 45577
diff changeset
   116
  by (simp add: entries_def lookup_def entries_lookup)
ef08425dd2d5 improved example to only use quotient_definitions; added lemmas to serve as possible replacement for the existing RBT theory
bulwahn
parents: 45577
diff changeset
   117
ef08425dd2d5 improved example to only use quotient_definitions; added lemmas to serve as possible replacement for the existing RBT theory
bulwahn
parents: 45577
diff changeset
   118
lemma lookup_bulkload [simp]:
ef08425dd2d5 improved example to only use quotient_definitions; added lemmas to serve as possible replacement for the existing RBT theory
bulwahn
parents: 45577
diff changeset
   119
  "lookup (bulkload xs) = map_of xs"
ef08425dd2d5 improved example to only use quotient_definitions; added lemmas to serve as possible replacement for the existing RBT theory
bulwahn
parents: 45577
diff changeset
   120
  by (simp add: bulkload_def lookup_RBT RBT_Impl.lookup_bulkload)
ef08425dd2d5 improved example to only use quotient_definitions; added lemmas to serve as possible replacement for the existing RBT theory
bulwahn
parents: 45577
diff changeset
   121
ef08425dd2d5 improved example to only use quotient_definitions; added lemmas to serve as possible replacement for the existing RBT theory
bulwahn
parents: 45577
diff changeset
   122
lemma lookup_map_entry [simp]:
ef08425dd2d5 improved example to only use quotient_definitions; added lemmas to serve as possible replacement for the existing RBT theory
bulwahn
parents: 45577
diff changeset
   123
  "lookup (map_entry k f t) = (lookup t)(k := Option.map f (lookup t k))"
ef08425dd2d5 improved example to only use quotient_definitions; added lemmas to serve as possible replacement for the existing RBT theory
bulwahn
parents: 45577
diff changeset
   124
  by (simp add: map_entry_def lookup_RBT RBT_Impl.lookup_map_entry lookup_impl_of)
ef08425dd2d5 improved example to only use quotient_definitions; added lemmas to serve as possible replacement for the existing RBT theory
bulwahn
parents: 45577
diff changeset
   125
ef08425dd2d5 improved example to only use quotient_definitions; added lemmas to serve as possible replacement for the existing RBT theory
bulwahn
parents: 45577
diff changeset
   126
lemma lookup_map [simp]:
ef08425dd2d5 improved example to only use quotient_definitions; added lemmas to serve as possible replacement for the existing RBT theory
bulwahn
parents: 45577
diff changeset
   127
  "lookup (map f t) k = Option.map (f k) (lookup t k)"
ef08425dd2d5 improved example to only use quotient_definitions; added lemmas to serve as possible replacement for the existing RBT theory
bulwahn
parents: 45577
diff changeset
   128
  by (simp add: map_def lookup_RBT RBT_Impl.lookup_map lookup_impl_of)
ef08425dd2d5 improved example to only use quotient_definitions; added lemmas to serve as possible replacement for the existing RBT theory
bulwahn
parents: 45577
diff changeset
   129
ef08425dd2d5 improved example to only use quotient_definitions; added lemmas to serve as possible replacement for the existing RBT theory
bulwahn
parents: 45577
diff changeset
   130
lemma fold_fold:
46133
d9fe85d3d2cd incorporated canonical fold combinator on lists into body of List theory; refactored passages on List.fold(l/r)
haftmann
parents: 45629
diff changeset
   131
  "fold f t = List.fold (prod_case f) (entries t)"
45629
ef08425dd2d5 improved example to only use quotient_definitions; added lemmas to serve as possible replacement for the existing RBT theory
bulwahn
parents: 45577
diff changeset
   132
  by (simp add: fold_def fun_eq_iff RBT_Impl.fold_def entries_impl_of)
ef08425dd2d5 improved example to only use quotient_definitions; added lemmas to serve as possible replacement for the existing RBT theory
bulwahn
parents: 45577
diff changeset
   133
47097
987cb55cac44 fix example files
kuncar
parents: 47093
diff changeset
   134
lemma impl_of_empty:
987cb55cac44 fix example files
kuncar
parents: 47093
diff changeset
   135
  "impl_of empty = RBT_Impl.Empty"
987cb55cac44 fix example files
kuncar
parents: 47093
diff changeset
   136
  by (simp add: empty_def RBT_inverse)
987cb55cac44 fix example files
kuncar
parents: 47093
diff changeset
   137
45629
ef08425dd2d5 improved example to only use quotient_definitions; added lemmas to serve as possible replacement for the existing RBT theory
bulwahn
parents: 45577
diff changeset
   138
lemma is_empty_empty [simp]:
ef08425dd2d5 improved example to only use quotient_definitions; added lemmas to serve as possible replacement for the existing RBT theory
bulwahn
parents: 45577
diff changeset
   139
  "is_empty t \<longleftrightarrow> t = empty"
ef08425dd2d5 improved example to only use quotient_definitions; added lemmas to serve as possible replacement for the existing RBT theory
bulwahn
parents: 45577
diff changeset
   140
  by (simp add: rbt_eq_iff is_empty_def impl_of_empty split: rbt.split)
ef08425dd2d5 improved example to only use quotient_definitions; added lemmas to serve as possible replacement for the existing RBT theory
bulwahn
parents: 45577
diff changeset
   141
ef08425dd2d5 improved example to only use quotient_definitions; added lemmas to serve as possible replacement for the existing RBT theory
bulwahn
parents: 45577
diff changeset
   142
lemma RBT_lookup_empty [simp]: (*FIXME*)
ef08425dd2d5 improved example to only use quotient_definitions; added lemmas to serve as possible replacement for the existing RBT theory
bulwahn
parents: 45577
diff changeset
   143
  "RBT_Impl.lookup t = Map.empty \<longleftrightarrow> t = RBT_Impl.Empty"
ef08425dd2d5 improved example to only use quotient_definitions; added lemmas to serve as possible replacement for the existing RBT theory
bulwahn
parents: 45577
diff changeset
   144
  by (cases t) (auto simp add: fun_eq_iff)
ef08425dd2d5 improved example to only use quotient_definitions; added lemmas to serve as possible replacement for the existing RBT theory
bulwahn
parents: 45577
diff changeset
   145
ef08425dd2d5 improved example to only use quotient_definitions; added lemmas to serve as possible replacement for the existing RBT theory
bulwahn
parents: 45577
diff changeset
   146
lemma lookup_empty_empty [simp]:
ef08425dd2d5 improved example to only use quotient_definitions; added lemmas to serve as possible replacement for the existing RBT theory
bulwahn
parents: 45577
diff changeset
   147
  "lookup t = Map.empty \<longleftrightarrow> t = empty"
ef08425dd2d5 improved example to only use quotient_definitions; added lemmas to serve as possible replacement for the existing RBT theory
bulwahn
parents: 45577
diff changeset
   148
  by (cases t) (simp add: empty_def lookup_def RBT_inject RBT_inverse)
ef08425dd2d5 improved example to only use quotient_definitions; added lemmas to serve as possible replacement for the existing RBT theory
bulwahn
parents: 45577
diff changeset
   149
ef08425dd2d5 improved example to only use quotient_definitions; added lemmas to serve as possible replacement for the existing RBT theory
bulwahn
parents: 45577
diff changeset
   150
lemma sorted_keys [iff]:
ef08425dd2d5 improved example to only use quotient_definitions; added lemmas to serve as possible replacement for the existing RBT theory
bulwahn
parents: 45577
diff changeset
   151
  "sorted (keys t)"
ef08425dd2d5 improved example to only use quotient_definitions; added lemmas to serve as possible replacement for the existing RBT theory
bulwahn
parents: 45577
diff changeset
   152
  by (simp add: keys_def RBT_Impl.keys_def sorted_entries)
ef08425dd2d5 improved example to only use quotient_definitions; added lemmas to serve as possible replacement for the existing RBT theory
bulwahn
parents: 45577
diff changeset
   153
ef08425dd2d5 improved example to only use quotient_definitions; added lemmas to serve as possible replacement for the existing RBT theory
bulwahn
parents: 45577
diff changeset
   154
lemma distinct_keys [iff]:
ef08425dd2d5 improved example to only use quotient_definitions; added lemmas to serve as possible replacement for the existing RBT theory
bulwahn
parents: 45577
diff changeset
   155
  "distinct (keys t)"
ef08425dd2d5 improved example to only use quotient_definitions; added lemmas to serve as possible replacement for the existing RBT theory
bulwahn
parents: 45577
diff changeset
   156
  by (simp add: keys_def RBT_Impl.keys_def distinct_entries)
ef08425dd2d5 improved example to only use quotient_definitions; added lemmas to serve as possible replacement for the existing RBT theory
bulwahn
parents: 45577
diff changeset
   157
45577
33b964e117bd adding another example for lifting definitions
bulwahn
parents:
diff changeset
   158
33b964e117bd adding another example for lifting definitions
bulwahn
parents:
diff changeset
   159
end