author  kuncar 
Tue, 09 Oct 2012 16:58:36 +0200  
changeset 49758  718f10c8bbfc 
parent 49757  73ab6d4a9236 
child 49928  e3f0a92de280 
permissions  rwrr 
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 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

5 
header {* Implementation of sets using RBT trees *} 
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 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

8 
imports RBT Product_ord 
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 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

13 
outside of List.thy using 'a list as an implenentation of sets cannot be 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

14 
used for code generation. If such equations are not needed, they can be 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

15 
deleted from the code generator. Otherwise, a user has to provide their 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

16 
own equations using RBT trees. 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

17 
*) 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

18 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

19 
section {* Definition of code datatype constructors *} 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

20 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

21 
definition Set :: "('a\<Colon>linorder, unit) rbt \<Rightarrow> 'a set" 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

22 
where "Set t = {x . lookup t x = Some ()}" 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

23 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

24 
definition Coset :: "('a\<Colon>linorder, unit) rbt \<Rightarrow> 'a set" 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

25 
where [simp]: "Coset t =  Set t" 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

26 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

27 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

28 
section {* Deletion of already existing code equations *} 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

29 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

30 
lemma [code, code del]: 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

31 
"Set.empty = Set.empty" .. 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

32 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

33 
lemma [code, code del]: 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

34 
"Set.is_empty = Set.is_empty" .. 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

35 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

36 
lemma [code, code del]: 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

37 
"uminus_set_inst.uminus_set = uminus_set_inst.uminus_set" .. 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

38 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

39 
lemma [code, code del]: 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

40 
"Set.member = Set.member" .. 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

41 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

42 
lemma [code, code del]: 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

43 
"Set.insert = Set.insert" .. 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

44 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

45 
lemma [code, code del]: 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

46 
"Set.remove = Set.remove" .. 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

47 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

48 
lemma [code, code del]: 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

49 
"UNIV = UNIV" .. 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

50 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

51 
lemma [code, code del]: 
49757
73ab6d4a9236
rename Set.project to Set.filter  more appropriate name
kuncar
parents:
48623
diff
changeset

52 
"Set.filter = Set.filter" .. 
48623
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

53 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

54 
lemma [code, code del]: 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

55 
"image = image" .. 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

56 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

57 
lemma [code, code del]: 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

58 
"Set.subset_eq = Set.subset_eq" .. 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

59 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

60 
lemma [code, code del]: 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

61 
"Ball = Ball" .. 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

62 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

63 
lemma [code, code del]: 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

64 
"Bex = Bex" .. 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

65 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

66 
lemma [code, code del]: 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

67 
"Set.union = Set.union" .. 
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 [code, code del]: 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

70 
"minus_set_inst.minus_set = minus_set_inst.minus_set" .. 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

71 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

72 
lemma [code, code del]: 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

73 
"Set.inter = Set.inter" .. 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

74 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

75 
lemma [code, code del]: 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

76 
"card = card" .. 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

77 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

78 
lemma [code, code del]: 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

79 
"the_elem = the_elem" .. 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

80 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

81 
lemma [code, code del]: 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

82 
"Pow = Pow" .. 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

83 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

84 
lemma [code, code del]: 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

85 
"setsum = setsum" .. 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

86 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

87 
lemma [code, code del]: 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

88 
"Product_Type.product = Product_Type.product" .. 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

89 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

90 
lemma [code, code del]: 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

91 
"Id_on = Id_on" .. 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

92 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

93 
lemma [code, code del]: 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

94 
"Image = Image" .. 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

95 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

96 
lemma [code, code del]: 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

97 
"trancl = trancl" .. 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

98 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

99 
lemma [code, code del]: 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

100 
"relcomp = relcomp" .. 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

101 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

102 
lemma [code, code del]: 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

103 
"wf = wf" .. 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

104 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

105 
lemma [code, code del]: 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

106 
"Min = Min" .. 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

107 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

108 
lemma [code, code del]: 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

109 
"Inf_fin = Inf_fin" .. 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

110 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

111 
lemma [code, code del]: 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

112 
"INFI = INFI" .. 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

113 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

114 
lemma [code, code del]: 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

115 
"Max = Max" .. 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

116 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

117 
lemma [code, code del]: 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

118 
"Sup_fin = Sup_fin" .. 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

119 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

120 
lemma [code, code del]: 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

121 
"SUPR = SUPR" .. 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

122 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

123 
lemma [code, code del]: 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

124 
"(Inf :: 'a set set \<Rightarrow> 'a set) = Inf" .. 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

125 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

126 
lemma [code, code del]: 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

127 
"(Sup :: 'a set set \<Rightarrow> 'a set) = Sup" .. 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

128 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

129 
lemma [code, code del]: 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

130 
"sorted_list_of_set = sorted_list_of_set" .. 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

131 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

132 
lemma [code, code del]: 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

133 
"List.map_project = List.map_project" .. 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

134 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

135 
section {* Lemmas *} 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

136 

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 
subsection {* Auxiliary lemmas *} 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

139 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

140 
lemma [simp]: "x \<noteq> Some () \<longleftrightarrow> x = None" 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

141 
by (auto simp: not_Some_eq[THEN iffD1]) 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

142 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

143 
lemma finite_Set [simp, intro!]: "finite (Set x)" 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

144 
proof  
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

145 
have "Set x = dom (lookup x)" by (auto simp: Set_def) 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

146 
then show ?thesis by simp 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

147 
qed 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

148 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

149 
lemma set_keys: "Set t = set(keys t)" 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

150 
proof  
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

151 
have "\<And>k. ((k, ()) \<in> set (entries t)) = (k \<in> set (keys t))" 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

152 
by (simp add: keys_entries) 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

153 
then show ?thesis by (auto simp: lookup_in_tree Set_def) 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

154 
qed 
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 
subsection {* fold and filter *} 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

157 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

158 
lemma finite_fold_rbt_fold_eq: 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

159 
assumes "comp_fun_commute f" 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

160 
shows "Finite_Set.fold f A (set(entries t)) = fold (curry f) t A" 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

161 
proof  
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

162 
have *: "remdups (entries t) = entries t" 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

163 
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

164 
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

165 
qed 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

166 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

167 
definition fold_keys :: "('a :: linorder \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a, _) rbt \<Rightarrow> 'b \<Rightarrow> 'b" 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

168 
where [code_unfold]:"fold_keys f t A = fold (\<lambda>k _ t. f k t) t A" 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

169 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

170 
lemma fold_keys_def_alt: 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

171 
"fold_keys f t s = List.fold f (keys t) s" 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

172 
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

173 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

174 
lemma finite_fold_fold_keys: 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

175 
assumes "comp_fun_commute f" 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

176 
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

177 
using assms 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

178 
proof  
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

179 
interpret comp_fun_commute f by fact 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

180 
have "set (keys t) = fst ` (set (entries t))" by (auto simp: fst_eq_Domain keys_entries) 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

181 
moreover have "inj_on fst (set (entries t))" using distinct_entries distinct_map by auto 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

182 
ultimately show ?thesis 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

183 
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

184 
comp_comp_fun_commute) 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

185 
qed 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

186 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

187 
definition rbt_filter :: "('a :: linorder \<Rightarrow> bool) \<Rightarrow> ('a, 'b) rbt \<Rightarrow> 'a set" where 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

188 
"rbt_filter P t = fold (\<lambda>k _ A'. if P k then Set.insert k A' else A') t {}" 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

189 

49758
718f10c8bbfc
use Set.filter instead of Finite_Set.filter, which is removed then
kuncar
parents:
49757
diff
changeset

190 
lemma Set_filter_rbt_filter: 
718f10c8bbfc
use Set.filter instead of Finite_Set.filter, which is removed then
kuncar
parents:
49757
diff
changeset

191 
"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

192 
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

193 
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

194 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

195 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

196 
subsection {* foldi and Ball *} 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

197 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

198 
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

199 
by (induction t) auto 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

200 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

201 
lemma rbt_foldi_fold_conj: 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

202 
"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

203 
proof (induction t arbitrary: val) 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

204 
case (Branch c t1) then show ?case 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

205 
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

206 
qed simp 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

207 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

208 
lemma foldi_fold_conj: "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" 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

209 
unfolding fold_keys_def by transfer (rule rbt_foldi_fold_conj) 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

210 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

211 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

212 
subsection {* foldi and Bex *} 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

213 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

214 
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

215 
by (induction t) auto 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

216 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

217 
lemma rbt_foldi_fold_disj: 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

218 
"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

219 
proof (induction t arbitrary: val) 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

220 
case (Branch c t1) then show ?case 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

221 
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

222 
qed simp 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

223 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

224 
lemma foldi_fold_disj: "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" 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

225 
unfolding fold_keys_def by transfer (rule rbt_foldi_fold_disj) 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

226 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

227 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

228 
subsection {* folding over non empty trees and selecting the minimal and maximal element *} 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

229 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

230 
(** concrete **) 
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 
(* 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

233 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

234 
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

235 
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

236 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

237 
(* minimum *) 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

238 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

239 
definition rbt_min :: "('a::linorder, unit) RBT_Impl.rbt \<Rightarrow> 'a" 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

240 
where "rbt_min t = rbt_fold1_keys min t" 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

241 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

242 
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

243 
by (auto simp: rbt_greater_prop less_imp_le) 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

244 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

245 
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

246 
by (auto simp: rbt_less_prop less_imp_le) 
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 fold_min_triv: 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

249 
fixes k :: "_ :: linorder" 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

250 
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

251 
by (induct xs) (auto simp add: min_def) 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

252 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

253 
lemma rbt_min_simps: 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

254 
"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

255 
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

256 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

257 
fun rbt_min_opt where 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

258 
"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

259 
"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

260 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

261 
lemma rbt_min_opt_Branch: 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

262 
"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

263 
by (cases t1) 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_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

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> 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

269 
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

270 
shows "P t" 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

271 
using assms 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

272 
apply (induction t) 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

273 
apply simp 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

274 
apply (case_tac "t1 = rbt.Empty") 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

275 
apply simp_all 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

276 
done 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

277 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

278 
lemma rbt_min_opt_in_set: 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

279 
fixes t :: "('a :: linorder, unit) RBT_Impl.rbt" 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

280 
assumes "t \<noteq> rbt.Empty" 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

281 
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

282 
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

283 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

284 
lemma rbt_min_opt_is_min: 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

285 
fixes t :: "('a :: linorder, unit) RBT_Impl.rbt" 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

286 
assumes "rbt_sorted t" 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

287 
assumes "t \<noteq> rbt.Empty" 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

288 
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

289 
using assms 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

290 
proof (induction t rule: rbt_min_opt_induct) 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

291 
case empty 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

292 
then show ?case by simp 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

293 
next 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

294 
case left_empty 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

295 
then show ?case by (auto intro: key_le_right simp del: rbt_sorted.simps) 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

296 
next 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

297 
case (left_non_empty c t1 k v t2 y) 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

298 
then have "y = k \<or> y \<in> set (RBT_Impl.keys t1) \<or> y \<in> set (RBT_Impl.keys t2)" by auto 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

299 
with left_non_empty show ?case 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

300 
proof(elim disjE) 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

301 
case goal1 then show ?case 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

302 
by (auto simp add: rbt_min_opt_Branch intro: left_le_key rbt_min_opt_in_set) 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

303 
next 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

304 
case goal2 with left_non_empty show ?case by (auto simp add: rbt_min_opt_Branch) 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

305 
next 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

306 
case goal3 show ?case 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

307 
proof  
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

308 
from goal3 have "rbt_min_opt t1 \<le> k" by (simp add: left_le_key rbt_min_opt_in_set) 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

309 
moreover from goal3 have "k \<le> y" by (simp add: key_le_right) 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

310 
ultimately show ?thesis using goal3 by (simp add: rbt_min_opt_Branch) 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

311 
qed 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

312 
qed 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

313 
qed 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

314 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

315 
lemma rbt_min_eq_rbt_min_opt: 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

316 
assumes "t \<noteq> RBT_Impl.Empty" 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

317 
assumes "is_rbt t" 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

318 
shows "rbt_min t = rbt_min_opt t" 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

319 
proof  
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

320 
interpret ab_semigroup_idem_mult "(min :: 'a \<Rightarrow> 'a \<Rightarrow> 'a)" using ab_semigroup_idem_mult_min 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

321 
unfolding class.ab_semigroup_idem_mult_def by blast 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

322 
show ?thesis 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

323 
by (simp add: Min_eqI rbt_min_opt_is_min rbt_min_opt_in_set assms Min_def[symmetric] 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

324 
non_empty_rbt_keys fold1_set_fold[symmetric] rbt_min_def rbt_fold1_keys_def) 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

325 
qed 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

326 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

327 
(* maximum *) 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

328 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

329 
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

330 
where "rbt_max t = rbt_fold1_keys max t" 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

331 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

332 
lemma fold_max_triv: 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

333 
fixes k :: "_ :: linorder" 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

334 
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

335 
by (induct xs) (auto simp add: max_def) 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

336 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

337 
lemma fold_max_rev_eq: 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

338 
fixes xs :: "('a :: linorder) list" 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

339 
assumes "xs \<noteq> []" 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

340 
shows "List.fold max (tl xs) (hd xs) = List.fold max (tl (rev xs)) (hd (rev xs))" 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

341 
proof  
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

342 
interpret ab_semigroup_idem_mult "(max :: 'a \<Rightarrow> 'a \<Rightarrow> 'a)" using ab_semigroup_idem_mult_max 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

343 
unfolding class.ab_semigroup_idem_mult_def by blast 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

344 
show ?thesis 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

345 
using assms by (auto simp add: fold1_set_fold[symmetric]) 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

346 
qed 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

347 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

348 
lemma rbt_max_simps: 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

349 
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

350 
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

351 
proof  
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

352 
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

353 
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

354 
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

355 
qed 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

356 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

357 
fun rbt_max_opt where 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

358 
"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

359 
"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

360 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

361 
lemma rbt_max_opt_Branch: 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

362 
"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

363 
by (cases t2) auto 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

364 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

365 
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

366 
fixes t :: "('a :: linorder, unit) RBT_Impl.rbt" 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

367 
assumes "P rbt.Empty" 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

368 
assumes "\<And>color t1 a b t2. P t1 \<Longrightarrow> P t2 \<Longrightarrow> t2 = rbt.Empty \<Longrightarrow> P (Branch color t1 a b t2)" 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

369 
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

370 
shows "P t" 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

371 
using assms 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

372 
apply (induction t) 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

373 
apply simp 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

374 
apply (case_tac "t2 = rbt.Empty") 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

375 
apply simp_all 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

376 
done 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

377 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

378 
lemma rbt_max_opt_in_set: 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

379 
fixes t :: "('a :: linorder, unit) RBT_Impl.rbt" 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

380 
assumes "t \<noteq> rbt.Empty" 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

381 
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

382 
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

383 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

384 
lemma rbt_max_opt_is_max: 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

385 
fixes t :: "('a :: linorder, unit) RBT_Impl.rbt" 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

386 
assumes "rbt_sorted t" 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

387 
assumes "t \<noteq> rbt.Empty" 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

388 
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

389 
using assms 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

390 
proof (induction t rule: rbt_max_opt_induct) 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

391 
case empty 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

392 
then show ?case by simp 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

393 
next 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

394 
case right_empty 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

395 
then show ?case by (auto intro: left_le_key simp del: rbt_sorted.simps) 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

396 
next 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

397 
case (right_non_empty c t1 k v t2 y) 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

398 
then have "y = k \<or> y \<in> set (RBT_Impl.keys t2) \<or> y \<in> set (RBT_Impl.keys t1)" by auto 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

399 
with right_non_empty show ?case 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

400 
proof(elim disjE) 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

401 
case goal1 then show ?case 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

402 
by (auto simp add: rbt_max_opt_Branch intro: key_le_right rbt_max_opt_in_set) 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

403 
next 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

404 
case goal2 with right_non_empty show ?case by (auto simp add: rbt_max_opt_Branch) 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

405 
next 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

406 
case goal3 show ?case 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

407 
proof  
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

408 
from goal3 have "rbt_max_opt t2 \<ge> k" by (simp add: key_le_right rbt_max_opt_in_set) 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

409 
moreover from goal3 have "y \<le> k" by (simp add: left_le_key) 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

410 
ultimately show ?thesis using goal3 by (simp add: rbt_max_opt_Branch) 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

411 
qed 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

412 
qed 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

413 
qed 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

414 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

415 
lemma rbt_max_eq_rbt_max_opt: 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

416 
assumes "t \<noteq> RBT_Impl.Empty" 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

417 
assumes "is_rbt t" 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

418 
shows "rbt_max t = rbt_max_opt t" 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

419 
proof  
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

420 
interpret ab_semigroup_idem_mult "(max :: 'a \<Rightarrow> 'a \<Rightarrow> 'a)" using ab_semigroup_idem_mult_max 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

421 
unfolding class.ab_semigroup_idem_mult_def by blast 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

422 
show ?thesis 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

423 
by (simp add: Max_eqI rbt_max_opt_is_max rbt_max_opt_in_set assms Max_def[symmetric] 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

424 
non_empty_rbt_keys fold1_set_fold[symmetric] rbt_max_def rbt_fold1_keys_def) 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

425 
qed 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

426 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

427 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

428 
(** abstract **) 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

429 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

430 
lift_definition fold1_keys :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> ('a::linorder, 'b) rbt \<Rightarrow> 'a" 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

431 
is rbt_fold1_keys by simp 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

432 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

433 
lemma fold1_keys_def_alt: 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

434 
"fold1_keys f t = List.fold f (tl(keys t)) (hd(keys t))" 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

435 
by transfer (simp add: rbt_fold1_keys_def) 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

436 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

437 
lemma finite_fold1_fold1_keys: 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

438 
assumes "class.ab_semigroup_mult f" 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

439 
assumes "\<not> (is_empty t)" 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

440 
shows "Finite_Set.fold1 f (Set t) = fold1_keys f t" 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

441 
proof  
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

442 
interpret ab_semigroup_mult f by fact 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

443 
show ?thesis using assms 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

444 
by (auto simp: fold1_keys_def_alt set_keys fold_def_alt fold1_distinct_set_fold non_empty_keys) 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

445 
qed 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

446 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

447 
(* minimum *) 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

448 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

449 
lift_definition r_min :: "('a :: linorder, unit) rbt \<Rightarrow> 'a" is rbt_min by simp 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

450 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

451 
lift_definition r_min_opt :: "('a :: linorder, unit) rbt \<Rightarrow> 'a" is rbt_min_opt by simp 
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 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

454 
by transfer (simp add: rbt_min_def) 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

455 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

456 
lemma r_min_eq_r_min_opt: 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

457 
assumes "\<not> (is_empty t)" 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

458 
shows "r_min t = r_min_opt t" 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

459 
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

460 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

461 
lemma fold_keys_min_top_eq: 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

462 
fixes t :: "('a :: {linorder, bounded_lattice_top}, unit) rbt" 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

463 
assumes "\<not> (is_empty t)" 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

464 
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

465 
proof  
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

466 
have *: "\<And>t. RBT_Impl.keys t \<noteq> [] \<Longrightarrow> List.fold min (RBT_Impl.keys t) top = 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

467 
List.fold min (hd(RBT_Impl.keys t) # tl(RBT_Impl.keys t)) top" 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

468 
by (simp add: hd_Cons_tl[symmetric]) 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

469 
{ fix x :: "_ :: {linorder, bounded_lattice_top}" and xs 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

470 
have "List.fold min (x#xs) top = List.fold min xs x" 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

471 
by (simp add: inf_min[symmetric]) 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

472 
} note ** = this 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

473 
show ?thesis using assms 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

474 
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

475 
apply transfer 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

476 
apply (case_tac t) 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

477 
apply simp 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

478 
apply (subst *) 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

479 
apply simp 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

480 
apply (subst **) 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

481 
apply simp 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

482 
done 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

483 
qed 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

484 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

485 
(* maximum *) 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

486 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

487 
lift_definition r_max :: "('a :: linorder, unit) rbt \<Rightarrow> 'a" is rbt_max by simp 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

488 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

489 
lift_definition r_max_opt :: "('a :: linorder, unit) rbt \<Rightarrow> 'a" is rbt_max_opt by simp 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

490 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

491 
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

492 
by transfer (simp add: rbt_max_def) 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

493 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

494 
lemma r_max_eq_r_max_opt: 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

495 
assumes "\<not> (is_empty t)" 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

496 
shows "r_max t = r_max_opt t" 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

497 
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

498 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

499 
lemma fold_keys_max_bot_eq: 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

500 
fixes t :: "('a :: {linorder, bounded_lattice_bot}, unit) rbt" 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

501 
assumes "\<not> (is_empty t)" 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

502 
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

503 
proof  
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

504 
have *: "\<And>t. RBT_Impl.keys t \<noteq> [] \<Longrightarrow> List.fold max (RBT_Impl.keys t) bot = 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

505 
List.fold max (hd(RBT_Impl.keys t) # tl(RBT_Impl.keys t)) bot" 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

506 
by (simp add: hd_Cons_tl[symmetric]) 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

507 
{ fix x :: "_ :: {linorder, bounded_lattice_bot}" and xs 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

508 
have "List.fold max (x#xs) bot = List.fold max xs x" 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

509 
by (simp add: sup_max[symmetric]) 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

510 
} note ** = this 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

511 
show ?thesis using assms 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

512 
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

513 
apply transfer 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

514 
apply (case_tac t) 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

515 
apply simp 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

516 
apply (subst *) 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

517 
apply simp 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

518 
apply (subst **) 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

519 
apply simp 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

520 
done 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

521 
qed 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

522 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

523 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

524 
section {* Code equations *} 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

525 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

526 
code_datatype Set Coset 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

527 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

528 
lemma empty_Set [code]: 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

529 
"Set.empty = Set RBT.empty" 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

530 
by (auto simp: Set_def) 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

531 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

532 
lemma UNIV_Coset [code]: 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

533 
"UNIV = Coset RBT.empty" 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

534 
by (auto simp: Set_def) 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

535 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

536 
lemma is_empty_Set [code]: 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

537 
"Set.is_empty (Set t) = RBT.is_empty t" 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

538 
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

539 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

540 
lemma compl_code [code]: 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

541 
" Set xs = Coset xs" 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

542 
" Coset xs = Set xs" 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

543 
by (simp_all add: Set_def) 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

544 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

545 
lemma member_code [code]: 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

546 
"x \<in> (Set t) = (RBT.lookup t x = Some ())" 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

547 
"x \<in> (Coset t) = (RBT.lookup t x = None)" 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

548 
by (simp_all add: Set_def) 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

549 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

550 
lemma insert_code [code]: 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

551 
"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

552 
"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

553 
by (auto simp: Set_def) 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

554 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

555 
lemma remove_code [code]: 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

556 
"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

557 
"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

558 
by (auto simp: Set_def) 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

559 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

560 
lemma union_Set [code]: 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

561 
"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

562 
proof  
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

563 
interpret comp_fun_idem Set.insert 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

564 
by (fact comp_fun_idem_insert) 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

565 
from finite_fold_fold_keys[OF `comp_fun_commute Set.insert`] 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

566 
show ?thesis by (auto simp add: union_fold_insert) 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

567 
qed 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

568 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

569 
lemma inter_Set [code]: 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

570 
"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

571 
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

572 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

573 
lemma minus_Set [code]: 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

574 
"A  Set t = fold_keys Set.remove t A" 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

575 
proof  
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

576 
interpret comp_fun_idem Set.remove 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

577 
by (fact comp_fun_idem_remove) 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

578 
from finite_fold_fold_keys[OF `comp_fun_commute Set.remove`] 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

579 
show ?thesis by (auto simp add: minus_fold_remove) 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

580 
qed 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

581 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

582 
lemma union_Coset [code]: 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

583 
"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

584 
proof  
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

585 
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

586 
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

587 
qed 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

588 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

589 
lemma union_Set_Set [code]: 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

590 
"Set t1 \<union> Set t2 = Set (union t1 t2)" 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

591 
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

592 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

593 
lemma inter_Coset [code]: 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

594 
"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

595 
by (simp add: Diff_eq [symmetric] minus_Set) 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

596 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

597 
lemma inter_Coset_Coset [code]: 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

598 
"Coset t1 \<inter> Coset t2 = Coset (union t1 t2)" 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

599 
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

600 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

601 
lemma minus_Coset [code]: 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

602 
"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

603 
by (simp add: inter_Set[simplified Int_commute]) 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

604 

49757
73ab6d4a9236
rename Set.project to Set.filter  more appropriate name
kuncar
parents:
48623
diff
changeset

605 
lemma filter_Set [code]: 
73ab6d4a9236
rename Set.project to Set.filter  more appropriate name
kuncar
parents:
48623
diff
changeset

606 
"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

607 
by (auto simp add: Set_filter_rbt_filter) 
48623
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

608 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

609 
lemma image_Set [code]: 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

610 
"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

611 
proof  
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

612 
have "comp_fun_commute (\<lambda>k. Set.insert (f k))" by default auto 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

613 
then show ?thesis by (auto simp add: image_fold_insert intro!: finite_fold_fold_keys) 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

614 
qed 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

615 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

616 
lemma Ball_Set [code]: 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

617 
"Ball (Set t) P \<longleftrightarrow> foldi (\<lambda>s. s = True) (\<lambda>k v s. s \<and> P k) t True" 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

618 
proof  
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

619 
have "comp_fun_commute (\<lambda>k s. s \<and> P k)" by default auto 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

620 
then show ?thesis 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

621 
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

622 
qed 
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 Bex_Set [code]: 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

625 
"Bex (Set t) P \<longleftrightarrow> foldi (\<lambda>s. s = False) (\<lambda>k v s. s \<or> P k) t False" 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

626 
proof  
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

627 
have "comp_fun_commute (\<lambda>k s. s \<or> P k)" by default auto 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

628 
then show ?thesis 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

629 
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

630 
qed 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

631 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

632 
lemma subset_code [code]: 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

633 
"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

634 
"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

635 
by auto 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

636 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

637 
definition non_empty_trees where [code del]: "non_empty_trees t1 t2 \<longleftrightarrow> Coset t1 \<le> Set t2" 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

638 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

639 
code_abort non_empty_trees 
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 subset_Coset_empty_Set_empty [code]: 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

642 
"Coset t1 \<le> Set t2 \<longleftrightarrow> (case (impl_of t1, impl_of t2) of 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

643 
(rbt.Empty, rbt.Empty) => False  
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

644 
(_, _) => non_empty_trees t1 t2)" 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

645 
proof  
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

646 
have *: "\<And>t. impl_of t = rbt.Empty \<Longrightarrow> t = RBT rbt.Empty" 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

647 
by (subst(asm) RBT_inverse[symmetric]) (auto simp: impl_of_inject) 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

648 
have **: "Lifting.invariant is_rbt rbt.Empty rbt.Empty" unfolding Lifting.invariant_def by simp 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

649 
show ?thesis 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

650 
by (auto simp: Set_def lookup.abs_eq[OF **] dest!: * split: rbt.split simp: non_empty_trees_def) 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

651 
qed 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

652 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

653 
text {* A frequent case â€“ avoid intermediate sets *} 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

654 
lemma [code_unfold]: 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

655 
"Set t1 \<subseteq> Set t2 \<longleftrightarrow> foldi (\<lambda>s. s = True) (\<lambda>k v s. s \<and> k \<in> Set t2) t1 True" 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

656 
by (simp add: subset_code Ball_Set) 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

657 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

658 
lemma card_Set [code]: 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

659 
"card (Set t) = fold_keys (\<lambda>_ n. n + 1) t 0" 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

660 
by (auto simp add: card_def fold_image_def intro!: finite_fold_fold_keys) (default, simp) 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

661 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

662 
lemma setsum_Set [code]: 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

663 
"setsum f (Set xs) = fold_keys (plus o f) xs 0" 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

664 
proof  
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

665 
have "comp_fun_commute (\<lambda>x. op + (f x))" by default (auto simp: add_ac) 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

666 
then show ?thesis 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

667 
by (auto simp add: setsum_def fold_image_def finite_fold_fold_keys o_def) 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

668 
qed 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

669 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

670 
definition not_a_singleton_tree where [code del]: "not_a_singleton_tree x y = x y" 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

671 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

672 
code_abort not_a_singleton_tree 
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 the_elem_set [code]: 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

675 
fixes t :: "('a :: linorder, unit) rbt" 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

676 
shows "the_elem (Set t) = (case impl_of t of 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

677 
(Branch RBT_Impl.B RBT_Impl.Empty x () RBT_Impl.Empty) \<Rightarrow> x 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

678 
 _ \<Rightarrow> not_a_singleton_tree the_elem (Set t))" 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

679 
proof  
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

680 
{ 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

681 
fix x :: "'a :: linorder" 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

682 
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

683 
have *:"?t \<in> {t. is_rbt t}" unfolding is_rbt_def by auto 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

684 
then have **:"Lifting.invariant is_rbt ?t ?t" unfolding Lifting.invariant_def by auto 
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 
have "impl_of t = ?t \<Longrightarrow> the_elem (Set t) = x" 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

687 
by (subst(asm) RBT_inverse[symmetric, OF *]) 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

688 
(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

689 
} 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

690 
then show ?thesis unfolding not_a_singleton_tree_def 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

691 
by(auto split: rbt.split unit.split color.split) 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

692 
qed 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

693 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

694 
lemma Pow_Set [code]: 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

695 
"Pow (Set t) = fold_keys (\<lambda>x A. A \<union> Set.insert x ` A) t {{}}" 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

696 
by (simp add: Pow_fold finite_fold_fold_keys[OF comp_fun_commute_Pow_fold]) 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

697 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

698 
lemma product_Set [code]: 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

699 
"Product_Type.product (Set t1) (Set t2) = 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

700 
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

701 
proof  
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

702 
have *:"\<And>x. comp_fun_commute (\<lambda>y. Set.insert (x, y))" by default auto 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

703 
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

704 
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

705 
qed 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

706 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

707 
lemma Id_on_Set [code]: 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

708 
"Id_on (Set t) = fold_keys (\<lambda>x. Set.insert (x, x)) t {}" 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

709 
proof  
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

710 
have "comp_fun_commute (\<lambda>x. Set.insert (x, x))" by default auto 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

711 
then show ?thesis 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

712 
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

713 
qed 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

714 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

715 
lemma Image_Set [code]: 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

716 
"(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

717 
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

718 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

719 
lemma trancl_set_ntrancl [code]: 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

720 
"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

721 
by (simp add: finite_trancl_ntranl) 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

722 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

723 
lemma relcomp_Set[code]: 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

724 
"(Set t1) O (Set t2) = fold_keys 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

725 
(\<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

726 
proof  
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

727 
interpret comp_fun_idem Set.insert by (fact comp_fun_idem_insert) 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

728 
have *: "\<And>x y. comp_fun_commute (\<lambda>(w, z) A'. if y = w then Set.insert (x, z) A' else A')" 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

729 
by default (auto simp add: fun_eq_iff) 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

730 
show ?thesis using finite_fold_fold_keys[OF comp_fun_commute_relcomp_fold, of "Set t2" "{}" t1] 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

731 
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

732 
qed 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

733 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

734 
lemma wf_set [code]: 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

735 
"wf (Set t) = acyclic (Set t)" 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

736 
by (simp add: wf_iff_acyclic_if_finite) 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

737 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

738 
definition not_non_empty_tree where [code del]: "not_non_empty_tree x y = x y" 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

739 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

740 
code_abort not_non_empty_tree 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

741 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

742 
lemma Min_fin_set_fold [code]: 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

743 
"Min (Set t) = (if is_empty t then not_non_empty_tree Min (Set t) else r_min_opt t)" 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

744 
proof  
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

745 
have *:"(class.ab_semigroup_mult (min :: 'a \<Rightarrow> 'a \<Rightarrow> 'a))" using ab_semigroup_idem_mult_min 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

746 
unfolding class.ab_semigroup_idem_mult_def by blast 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

747 
show ?thesis 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

748 
by (auto simp add: Min_def not_non_empty_tree_def finite_fold1_fold1_keys[OF *] r_min_alt_def 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

749 
r_min_eq_r_min_opt[symmetric]) 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

750 
qed 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

751 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

752 
lemma Inf_fin_set_fold [code]: 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

753 
"Inf_fin (Set t) = Min (Set t)" 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

754 
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

755 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

756 
lemma Inf_Set_fold: 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

757 
fixes t :: "('a :: {linorder, complete_lattice}, unit) rbt" 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

758 
shows "Inf (Set t) = (if is_empty t then top else r_min_opt t)" 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

759 
proof  
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

760 
have "comp_fun_commute (min :: 'a \<Rightarrow> 'a \<Rightarrow> 'a)" by default (simp add: fun_eq_iff ac_simps) 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

761 
then have "t \<noteq> empty \<Longrightarrow> Finite_Set.fold min top (Set t) = fold1_keys min t" 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

762 
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

763 
then show ?thesis 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

764 
by (auto simp add: Inf_fold_inf inf_min empty_Set[symmetric] r_min_eq_r_min_opt[symmetric] r_min_alt_def) 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

765 
qed 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

766 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

767 
definition Inf' :: "'a :: {linorder, complete_lattice} set \<Rightarrow> 'a" where [code del]: "Inf' x = Inf x" 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

768 
declare Inf'_def[symmetric, code_unfold] 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

769 
declare Inf_Set_fold[folded Inf'_def, code] 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

770 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

771 
lemma INFI_Set_fold [code]: 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

772 
"INFI (Set t) f = fold_keys (inf \<circ> f) t top" 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

773 
proof  
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

774 
have "comp_fun_commute ((inf :: 'a \<Rightarrow> 'a \<Rightarrow> 'a) \<circ> f)" 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

775 
by default (auto simp add: fun_eq_iff ac_simps) 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

776 
then show ?thesis 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

777 
by (auto simp: INF_fold_inf finite_fold_fold_keys) 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

778 
qed 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

779 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

780 
lemma Max_fin_set_fold [code]: 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

781 
"Max (Set t) = (if is_empty t then not_non_empty_tree Max (Set t) else r_max_opt t)" 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

782 
proof  
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

783 
have *:"(class.ab_semigroup_mult (max :: 'a \<Rightarrow> 'a \<Rightarrow> 'a))" using ab_semigroup_idem_mult_max 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

784 
unfolding class.ab_semigroup_idem_mult_def by blast 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

785 
show ?thesis 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

786 
by (auto simp add: Max_def not_non_empty_tree_def finite_fold1_fold1_keys[OF *] r_max_alt_def 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

787 
r_max_eq_r_max_opt[symmetric]) 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

788 
qed 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

789 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

790 
lemma Sup_fin_set_fold [code]: 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

791 
"Sup_fin (Set t) = Max (Set t)" 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

792 
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

793 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

794 
lemma Sup_Set_fold: 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

795 
fixes t :: "('a :: {linorder, complete_lattice}, unit) rbt" 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

796 
shows "Sup (Set t) = (if is_empty t then bot else r_max_opt t)" 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

797 
proof  
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

798 
have "comp_fun_commute (max :: 'a \<Rightarrow> 'a \<Rightarrow> 'a)" by default (simp add: fun_eq_iff ac_simps) 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

799 
then have "t \<noteq> empty \<Longrightarrow> Finite_Set.fold max bot (Set t) = fold1_keys max t" 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

800 
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

801 
then show ?thesis 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

802 
by (auto simp add: Sup_fold_sup sup_max empty_Set[symmetric] r_max_eq_r_max_opt[symmetric] r_max_alt_def) 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

803 
qed 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

804 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

805 
definition Sup' :: "'a :: {linorder, complete_lattice} set \<Rightarrow> 'a" where [code del]: "Sup' x = Sup x" 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

806 
declare Sup'_def[symmetric, code_unfold] 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

807 
declare Sup_Set_fold[folded Sup'_def, code] 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

808 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

809 
lemma SUPR_Set_fold [code]: 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

810 
"SUPR (Set t) f = fold_keys (sup \<circ> f) t bot" 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

811 
proof  
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

812 
have "comp_fun_commute ((sup :: 'a \<Rightarrow> 'a \<Rightarrow> 'a) \<circ> f)" 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

813 
by default (auto simp add: fun_eq_iff ac_simps) 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

814 
then show ?thesis 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

815 
by (auto simp: SUP_fold_sup finite_fold_fold_keys) 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

816 
qed 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

817 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

818 
lemma sorted_list_set[code]: 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

819 
"sorted_list_of_set (Set t) = keys t" 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

820 
by (auto simp add: set_keys intro: sorted_distinct_set_unique) 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

821 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

822 
hide_const (open) RBT_Set.Set RBT_Set.Coset 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

823 

bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

824 
end 