author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 47308  9caab698dbe4 
child 47451  ab606e685d52 
permissions  rwrr 
47308  1 
(* Title: HOL/Quotient_Examples/Lift_RBT.thy 
2 
Author: Lukas Bulwahn and Ondrej Kuncar 

3 
*) 

45577  4 

5 
header {* Lifting operations of RBT trees *} 

6 

7 
theory Lift_RBT 

8 
imports Main "~~/src/HOL/Library/RBT_Impl" 

9 
begin 

10 

11 
subsection {* Type definition *} 

12 

47097  13 
typedef (open) ('a, 'b) rbt = "{t :: ('a\<Colon>linorder, 'b) RBT_Impl.rbt. is_rbt t}" 
14 
morphisms impl_of RBT 

15 
proof  

16 
have "RBT_Impl.Empty \<in> ?rbt" by simp 

17 
then show ?thesis .. 

18 
qed 

45577  19 

20 
lemma rbt_eq_iff: 

21 
"t1 = t2 \<longleftrightarrow> impl_of t1 = impl_of t2" 

22 
by (simp add: impl_of_inject) 

23 

24 
lemma rbt_eqI: 

25 
"impl_of t1 = impl_of t2 \<Longrightarrow> t1 = t2" 

26 
by (simp add: rbt_eq_iff) 

27 

28 
lemma is_rbt_impl_of [simp, intro]: 

29 
"is_rbt (impl_of t)" 

30 
using impl_of [of t] by simp 

31 

32 
lemma RBT_impl_of [simp, code abstype]: 

33 
"RBT (impl_of t) = t" 

34 
by (simp add: impl_of_inverse) 

35 

36 
subsection {* Primitive operations *} 

37 

47097  38 
setup_lifting type_definition_rbt 
39 

47308  40 
lift_definition lookup :: "('a\<Colon>linorder, 'b) rbt \<Rightarrow> 'a \<rightharpoonup> 'b" is "RBT_Impl.lookup" 
41 
by simp 

42 

43 
lift_definition empty :: "('a\<Colon>linorder, 'b) rbt" is RBT_Impl.Empty 

44 
by (simp add: empty_def) 

45 

46 
lift_definition insert :: "'a\<Colon>linorder \<Rightarrow> 'b \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt" is "RBT_Impl.insert" 

47 
by simp 

48 

49 
lift_definition delete :: "'a\<Colon>linorder \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt" is "RBT_Impl.delete" 

50 
by simp 

51 

52 
lift_definition entries :: "('a\<Colon>linorder, 'b) rbt \<Rightarrow> ('a \<times> 'b) list" is RBT_Impl.entries 

47093  53 
by simp 
45577  54 

47308  55 
lift_definition keys :: "('a\<Colon>linorder, 'b) rbt \<Rightarrow> 'a list" is RBT_Impl.keys 
56 
by simp 

45577  57 

47308  58 
lift_definition bulkload :: "('a\<Colon>linorder \<times> 'b) list \<Rightarrow> ('a, 'b) rbt" is "RBT_Impl.bulkload" 
47097  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  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 
62 
by simp 

63 

64 
lift_definition map :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a\<Colon>linorder, 'b) rbt \<Rightarrow> ('a, 'b) rbt" is RBT_Impl.map 

65 
by simp 

66 

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 

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  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  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  134 
lemma impl_of_empty: 
135 
"impl_of empty = RBT_Impl.Empty" 

136 
by (simp add: empty_def RBT_inverse) 

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  158 

159 
end 