author  wenzelm 
Mon, 06 Jul 2015 22:57:34 +0200  
changeset 60679  ade12ef2773c 
parent 60580  7e741e22d7fc 
child 61076  bdc1e2f0a86a 
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 

60500  5 
section \<open>Implementation of sets using RBT trees\<close> 
48623
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

6 

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

7 
theory RBT_Set 
51115
7dbd6832a689
consolidation of library theories on product orders
haftmann
parents:
50996
diff
changeset

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

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

10 

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

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

12 
Users should be aware that by including this file all code equations 
58301
de95aeedf49e
fixed situation in 'primrec' whereby the original value of a constructor argument of nested type was not translated correctly to a 'map fst'
blanchet
parents:
57816
diff
changeset

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

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

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

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

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

18 

60500  19 
section \<open>Definition of code datatype constructors\<close> 
48623
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

20 

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" 
56019  22 
where "Set t = {x . RBT.lookup t x = Some ()}" 
48623
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

23 

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 

60500  28 
section \<open>Deletion of already existing code equations\<close> 
48623
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

29 

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 

49948
744934b818c7
moved quite generic material from theory Enum to more appropriate places
haftmann
parents:
49928
diff
changeset

66 
lemma [code, code del]: 
744934b818c7
moved quite generic material from theory Enum to more appropriate places
haftmann
parents:
49928
diff
changeset

67 
"can_select = can_select" .. 
744934b818c7
moved quite generic material from theory Enum to more appropriate places
haftmann
parents:
49928
diff
changeset

68 

48623
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 
"Set.union = Set.union" .. 
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 
"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

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 
"Set.inter = Set.inter" .. 
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 
"card = card" .. 
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 
"the_elem = the_elem" .. 
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 
"Pow = Pow" .. 
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 
"setsum = setsum" .. 
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]: 
58368  91 
"setprod = setprod" .. 
92 

93 
lemma [code, code del]: 

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

94 
"Product_Type.product = Product_Type.product" .. 
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 
"Id_on = Id_on" .. 
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 
"Image = Image" .. 
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 
"trancl = trancl" .. 
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 
"relcomp = relcomp" .. 
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 
"wf = wf" .. 
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 
"Min = Min" .. 
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 
"Inf_fin = Inf_fin" .. 
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]: 
56218
1c3f1f2431f9
elongated INFI and SUPR, to reduced risk of confusing theorems names in the future while still being consistent with INTER and UNION
haftmann
parents:
56212
diff
changeset

118 
"INFIMUM = INFIMUM" .. 
48623
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 
"Max = Max" .. 
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 
"Sup_fin = Sup_fin" .. 
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]: 
56218
1c3f1f2431f9
elongated INFI and SUPR, to reduced risk of confusing theorems names in the future while still being consistent with INTER and UNION
haftmann
parents:
56212
diff
changeset

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

128 

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

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

130 
"(Inf :: 'a set set \<Rightarrow> 'a set) = Inf" .. 
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 
"(Sup :: 'a set set \<Rightarrow> 'a set) = Sup" .. 
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 
lemma [code, code del]: 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

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

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

140 

53955  141 
lemma [code, code del]: 
142 
"List.Bleast = List.Bleast" .. 

143 

60500  144 
section \<open>Lemmas\<close> 
48623
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

145 

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

146 

60500  147 
subsection \<open>Auxiliary lemmas\<close> 
48623
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 [simp]: "x \<noteq> Some () \<longleftrightarrow> x = None" 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

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

151 

56019  152 
lemma Set_set_keys: "Set x = dom (RBT.lookup x)" 
49928  153 
by (auto simp: Set_def) 
154 

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

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

157 

56019  158 
lemma set_keys: "Set t = set(RBT.keys t)" 
49928  159 
by (simp add: Set_set_keys lookup_keys) 
48623
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

160 

60500  161 
subsection \<open>fold and filter\<close> 
48623
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

162 

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

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

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

166 
proof  
56019  167 
have *: "remdups (RBT.entries t) = RBT.entries t" 
48623
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

168 
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

169 
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

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

171 

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

172 
definition fold_keys :: "('a :: linorder \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a, _) rbt \<Rightarrow> 'b \<Rightarrow> 'b" 
56019  173 
where [code_unfold]:"fold_keys f t A = RBT.fold (\<lambda>k _ t. f k t) t A" 
48623
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

174 

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

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

177 
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

178 

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

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

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

181 
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

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

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

184 
interpret comp_fun_commute f by fact 
56019  185 
have "set (RBT.keys t) = fst ` (set (RBT.entries t))" by (auto simp: fst_eq_Domain keys_entries) 
186 
moreover have "inj_on fst (set (RBT.entries t))" using distinct_entries distinct_map by auto 

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

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

188 
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

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

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

191 

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

192 
definition rbt_filter :: "('a :: linorder \<Rightarrow> bool) \<Rightarrow> ('a, 'b) rbt \<Rightarrow> 'a set" where 
56019  193 
"rbt_filter P t = RBT.fold (\<lambda>k _ A'. if P k then Set.insert k A' else A') t {}" 
48623
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

194 

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

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

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

197 
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

198 
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

199 

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

200 

60500  201 
subsection \<open>foldi and Ball\<close> 
48623
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

202 

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

203 
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

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

205 

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

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

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

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

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

210 
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

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

212 

56019  213 
lemma foldi_fold_conj: "RBT.foldi (\<lambda>s. s = True) (\<lambda>k v s. s \<and> P k) t val = fold_keys (\<lambda>k s. s \<and> P k) t val" 
214 
unfolding fold_keys_def including rbt.lifting by transfer (rule rbt_foldi_fold_conj) 

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

215 

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

216 

60500  217 
subsection \<open>foldi and Bex\<close> 
48623
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

218 

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

219 
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

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

221 

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

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

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

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

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

226 
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

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

228 

56019  229 
lemma foldi_fold_disj: "RBT.foldi (\<lambda>s. s = False) (\<lambda>k v s. s \<or> P k) t val = fold_keys (\<lambda>k s. s \<or> P k) t val" 
230 
unfolding fold_keys_def including rbt.lifting by transfer (rule rbt_foldi_fold_disj) 

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

231 

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

232 

60500  233 
subsection \<open>folding over non empty trees and selecting the minimal and maximal element\<close> 
48623
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

234 

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

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

238 

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

239 
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

240 
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

241 

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

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

243 

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

244 
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

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

246 

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

247 
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

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

249 

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

250 
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

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

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

255 
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

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

257 

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

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

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

260 
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

261 

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

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

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

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

265 

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

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

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

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

269 

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

270 
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

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

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

273 
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

274 
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

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

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

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

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

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

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

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

282 

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

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

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

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

286 
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

287 
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

288 

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

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

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

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

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

293 
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

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

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

296 
case empty 
60580  297 
then show ?case by simp 
48623
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

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

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

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

302 
case (left_non_empty c t1 k v t2 y) 
60580  303 
then consider "y = k"  "y \<in> set (RBT_Impl.keys t1)"  "y \<in> set (RBT_Impl.keys t2)" 
304 
by auto 

305 
then show ?case 

306 
proof cases 

307 
case 1 

308 
with left_non_empty show ?thesis 

309 
by (auto simp add: rbt_min_opt_Branch intro: left_le_key rbt_min_opt_in_set) 

310 
next 

311 
case 2 

312 
with left_non_empty show ?thesis 

313 
by (auto simp add: rbt_min_opt_Branch) 

314 
next 

315 
case y: 3 

316 
have "rbt_min_opt t1 \<le> k" 

317 
using left_non_empty by (simp add: left_le_key rbt_min_opt_in_set) 

318 
moreover have "k \<le> y" 

319 
using left_non_empty y by (simp add: key_le_right) 

320 
ultimately show ?thesis 

321 
using left_non_empty y by (simp add: rbt_min_opt_Branch) 

322 
qed 

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

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

324 

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

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

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

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

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

329 
proof  
51489  330 
from assms have "hd (RBT_Impl.keys t) # tl (RBT_Impl.keys t) = RBT_Impl.keys t" by (cases t) simp_all 
331 
with assms show ?thesis 

332 
by (simp add: rbt_min_def rbt_fold1_keys_def rbt_min_opt_is_min 

51540
eea5c4ca4a0e
explicit sublocale dependency for Min/Max yields more appropriate Min/Max prefix for a couple of facts
haftmann
parents:
51489
diff
changeset

333 
Min.set_eq_fold [symmetric] Min_eqI rbt_min_opt_in_set) 
48623
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

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

335 

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

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

337 

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

338 
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

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

340 

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

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

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

343 
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

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

345 

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

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

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

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

349 
shows "List.fold max (tl xs) (hd xs) = List.fold max (tl (rev xs)) (hd (rev xs))" 
51540
eea5c4ca4a0e
explicit sublocale dependency for Min/Max yields more appropriate Min/Max prefix for a couple of facts
haftmann
parents:
51489
diff
changeset

350 
using assms by (simp add: Max.set_eq_fold [symmetric]) 
48623
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

351 

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

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

353 
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

354 
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

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

356 
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

357 
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

358 
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

359 
qed 
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 
fun rbt_max_opt where 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

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

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

364 

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

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

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

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

368 

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

369 
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

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

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

372 
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

373 
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

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

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

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

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

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

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

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

381 

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

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

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

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

385 
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

386 
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

387 

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

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

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

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

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

392 
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

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

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

395 
case empty 
60580  396 
then show ?case by simp 
48623
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

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

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

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

401 
case (right_non_empty c t1 k v t2 y) 
60580  402 
then consider "y = k"  "y \<in> set (RBT_Impl.keys t2)"  "y \<in> set (RBT_Impl.keys t1)" 
403 
by auto 

404 
then show ?case 

405 
proof cases 

406 
case 1 

407 
with right_non_empty show ?thesis 

408 
by (auto simp add: rbt_max_opt_Branch intro: key_le_right rbt_max_opt_in_set) 

409 
next 

410 
case 2 

411 
with right_non_empty show ?thesis 

412 
by (auto simp add: rbt_max_opt_Branch) 

413 
next 

414 
case y: 3 

415 
have "rbt_max_opt t2 \<ge> k" 

416 
using right_non_empty by (simp add: key_le_right rbt_max_opt_in_set) 

417 
moreover have "y \<le> k" 

418 
using right_non_empty y by (simp add: left_le_key) 

419 
ultimately show ?thesis 

420 
using right_non_empty by (simp add: rbt_max_opt_Branch) 

421 
qed 

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

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

423 

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

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

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

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

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

428 
proof  
51489  429 
from assms have "hd (RBT_Impl.keys t) # tl (RBT_Impl.keys t) = RBT_Impl.keys t" by (cases t) simp_all 
430 
with assms show ?thesis 

431 
by (simp add: rbt_max_def rbt_fold1_keys_def rbt_max_opt_is_max 

51540
eea5c4ca4a0e
explicit sublocale dependency for Min/Max yields more appropriate Min/Max prefix for a couple of facts
haftmann
parents:
51489
diff
changeset

432 
Max.set_eq_fold [symmetric] Max_eqI rbt_max_opt_in_set) 
48623
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

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

434 

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

435 

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

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

437 

56019  438 
context includes rbt.lifting begin 
48623
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

439 
lift_definition fold1_keys :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> ('a::linorder, 'b) rbt \<Rightarrow> 'a" 
55565
f663fc1e653b
simplify proofs because of the stronger reflexivity prover
kuncar
parents:
54263
diff
changeset

440 
is rbt_fold1_keys . 
48623
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

441 

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

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

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

445 

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

446 
lemma finite_fold1_fold1_keys: 
51489  447 
assumes "semilattice f" 
56019  448 
assumes "\<not> RBT.is_empty t" 
51489  449 
shows "semilattice_set.F f (Set t) = fold1_keys f t" 
48623
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

450 
proof  
60500  451 
from \<open>semilattice f\<close> interpret semilattice_set f by (rule semilattice_set.intro) 
48623
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

452 
show ?thesis using assms 
51489  453 
by (auto simp: fold1_keys_def_alt set_keys fold_def_alt non_empty_keys set_eq_fold [symmetric]) 
48623
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

454 
qed 
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 
(* minimum *) 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

457 

55565
f663fc1e653b
simplify proofs because of the stronger reflexivity prover
kuncar
parents:
54263
diff
changeset

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

459 

55565
f663fc1e653b
simplify proofs because of the stronger reflexivity prover
kuncar
parents:
54263
diff
changeset

460 
lift_definition r_min_opt :: "('a :: linorder, unit) rbt \<Rightarrow> 'a" is rbt_min_opt . 
48623
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

461 

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

462 
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

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

464 

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

465 
lemma r_min_eq_r_min_opt: 
56019  466 
assumes "\<not> (RBT.is_empty t)" 
48623
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

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

468 
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

469 

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

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

471 
fixes t :: "('a :: {linorder, bounded_lattice_top}, unit) rbt" 
56019  472 
assumes "\<not> (RBT.is_empty t)" 
48623
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

473 
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

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

475 
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

476 
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

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

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

479 
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

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

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

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

483 
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

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

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

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

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

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

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

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

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

492 
qed 
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 
(* maximum *) 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

495 

55565
f663fc1e653b
simplify proofs because of the stronger reflexivity prover
kuncar
parents:
54263
diff
changeset

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

497 

55565
f663fc1e653b
simplify proofs because of the stronger reflexivity prover
kuncar
parents:
54263
diff
changeset

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

499 

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

500 
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

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

502 

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

503 
lemma r_max_eq_r_max_opt: 
56019  504 
assumes "\<not> (RBT.is_empty t)" 
48623
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

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

506 
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

507 

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

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

509 
fixes t :: "('a :: {linorder, bounded_lattice_bot}, unit) rbt" 
56019  510 
assumes "\<not> (RBT.is_empty t)" 
48623
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

511 
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

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

513 
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

514 
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

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

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

517 
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

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

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

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

521 
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

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

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

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

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

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

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

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

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

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

531 

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

533 

60500  534 
section \<open>Code equations\<close> 
48623
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 
code_datatype Set Coset 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

537 

57816
d8bbb97689d3
no need for 'set_simps' now that 'datatype_new' generates the desired 'set' property
blanchet
parents:
57514
diff
changeset

538 
declare list.set[code] (* needed? *) 
50996
51ad7b4ac096
restore code equations for List.set in RBT_Set; make Scala happy according to 7.1 in the code generator manual
kuncar
parents:
49948
diff
changeset

539 

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

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

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

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

543 

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

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

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

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

547 

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

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

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

550 
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

551 

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

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

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

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

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

556 

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

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

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

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

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

561 

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

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

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

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

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

566 

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

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

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

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

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

571 

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

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

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

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

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

576 
by (fact comp_fun_idem_insert) 
60500  577 
from finite_fold_fold_keys[OF \<open>comp_fun_commute Set.insert\<close>] 
48623
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

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

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

580 

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

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

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

583 
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

584 

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

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

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

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

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

589 
by (fact comp_fun_idem_remove) 
60500  590 
from finite_fold_fold_keys[OF \<open>comp_fun_commute Set.remove\<close>] 
48623
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

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

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

593 

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

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

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

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

597 
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

598 
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

599 
qed 
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 union_Set_Set [code]: 
56019  602 
"Set t1 \<union> Set t2 = Set (RBT.union t1 t2)" 
48623
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

603 
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

604 

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

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

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

607 
by (simp add: Diff_eq [symmetric] minus_Set) 
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 inter_Coset_Coset [code]: 
56019  610 
"Coset t1 \<inter> Coset t2 = Coset (RBT.union t1 t2)" 
48623
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

611 
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

612 

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

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

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

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

616 

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

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

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

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

620 

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

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

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

623 
proof  
60679  624 
have "comp_fun_commute (\<lambda>k. Set.insert (f k))" 
625 
by standard auto 

626 
then show ?thesis 

627 
by (auto simp add: image_fold_insert intro!: finite_fold_fold_keys) 

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

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

629 

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

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

632 
proof  
60679  633 
have "comp_fun_commute (\<lambda>k s. s \<and> P k)" 
634 
by standard auto 

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

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

636 
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

637 
qed 
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 
lemma Bex_Set [code]: 
56019  640 
"Bex (Set t) P \<longleftrightarrow> RBT.foldi (\<lambda>s. s = False) (\<lambda>k v s. s \<or> P k) t False" 
48623
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

641 
proof  
60679  642 
have "comp_fun_commute (\<lambda>k s. s \<or> P k)" 
643 
by standard auto 

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

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

645 
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

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

647 

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

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

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

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

651 
by auto 
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 
lemma subset_Coset_empty_Set_empty [code]: 
56019  654 
"Coset t1 \<le> Set t2 \<longleftrightarrow> (case (RBT.impl_of t1, RBT.impl_of t2) of 
48623
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

655 
(rbt.Empty, rbt.Empty) => False  
53745  656 
(_, _) => Code.abort (STR ''non_empty_trees'') (\<lambda>_. Coset t1 \<le> Set t2))" 
48623
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

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

659 
by (subst(asm) RBT_inverse[symmetric]) (auto simp: impl_of_inject) 
56519
c1048f5bbb45
more appropriate name (Lifting.invariant > eq_onp)
kuncar
parents:
56218
diff
changeset

660 
have **: "eq_onp is_rbt rbt.Empty rbt.Empty" unfolding eq_onp_def by simp 
48623
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

661 
show ?thesis 
53745  662 
by (auto simp: Set_def lookup.abs_eq[OF **] dest!: * split: rbt.split) 
48623
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

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

664 

60500  665 
text \<open>A frequent case  avoid intermediate sets\<close> 
48623
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

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

668 
by (simp add: subset_code Ball_Set) 
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 
lemma card_Set [code]: 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

671 
"card (Set t) = fold_keys (\<lambda>_ n. n + 1) t 0" 
51489  672 
by (auto simp add: card.eq_fold intro: finite_fold_fold_keys comp_fun_commute_const) 
48623
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

673 

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

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

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

676 
proof  
60679  677 
have "comp_fun_commute (\<lambda>x. op + (f x))" 
678 
by standard (auto simp: ac_simps) 

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

679 
then show ?thesis 
51489  680 
by (auto simp add: setsum.eq_fold finite_fold_fold_keys o_def) 
48623
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

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

682 

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

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

684 
fixes t :: "('a :: linorder, unit) rbt" 
56019  685 
shows "the_elem (Set t) = (case RBT.impl_of t of 
48623
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

686 
(Branch RBT_Impl.B RBT_Impl.Empty x () RBT_Impl.Empty) \<Rightarrow> x 
53745  687 
 _ \<Rightarrow> Code.abort (STR ''not_a_singleton_tree'') (\<lambda>_. the_elem (Set t)))" 
48623
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

688 
proof  
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 
fix x :: "'a :: linorder" 
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

691 
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

692 
have *:"?t \<in> {t. is_rbt t}" unfolding is_rbt_def by auto 
56519
c1048f5bbb45
more appropriate name (Lifting.invariant > eq_onp)
kuncar
parents:
56218
diff
changeset

693 
then have **:"eq_onp is_rbt ?t ?t" unfolding eq_onp_def by auto 
48623
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

694 

56019  695 
have "RBT.impl_of t = ?t \<Longrightarrow> the_elem (Set t) = x" 
48623
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

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

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

698 
} 
53745  699 
then show ?thesis 
48623
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

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

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

702 

60679  703 
lemma Pow_Set [code]: "Pow (Set t) = fold_keys (\<lambda>x A. A \<union> Set.insert x ` A) t {{}}" 
704 
by (simp add: Pow_fold finite_fold_fold_keys[OF comp_fun_commute_Pow_fold]) 

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

705 

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

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

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

708 
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

709 
proof  
60679  710 
have *: "comp_fun_commute (\<lambda>y. Set.insert (x, y))" for x 
711 
by standard auto 

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

712 
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

713 
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

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

715 

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

717 
proof  
60679  718 
have "comp_fun_commute (\<lambda>x. Set.insert (x, x))" 
719 
by standard auto 

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

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

721 
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

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

723 

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

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

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

726 
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

727 

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

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

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

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

731 

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

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

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

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

735 
proof  
60679  736 
interpret comp_fun_idem Set.insert 
737 
by (fact comp_fun_idem_insert) 

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

738 
have *: "\<And>x y. comp_fun_commute (\<lambda>(w, z) A'. if y = w then Set.insert (x, z) A' else A')" 
60679  739 
by standard (auto simp add: fun_eq_iff) 
740 
show ?thesis 

741 
using finite_fold_fold_keys[OF comp_fun_commute_relcomp_fold, of "Set t2" "{}" t1] 

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

742 
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

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

744 

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

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

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

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

748 

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

749 
lemma Min_fin_set_fold [code]: 
53745  750 
"Min (Set t) = 
56019  751 
(if RBT.is_empty t 
53745  752 
then Code.abort (STR ''not_non_empty_tree'') (\<lambda>_. Min (Set t)) 
753 
else r_min_opt t)" 

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

754 
proof  
51489  755 
have *: "semilattice (min :: 'a \<Rightarrow> 'a \<Rightarrow> 'a)" .. 
756 
with finite_fold1_fold1_keys [OF *, folded Min_def] 

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

757 
show ?thesis 
53745  758 
by (simp add: r_min_alt_def r_min_eq_r_min_opt [symmetric]) 
48623
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

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

760 

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

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

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

763 
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

764 

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

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

766 
fixes t :: "('a :: {linorder, complete_lattice}, unit) rbt" 
56019  767 
shows "Inf (Set t) = (if RBT.is_empty t then top else r_min_opt t)" 
48623
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

768 
proof  
60679  769 
have "comp_fun_commute (min :: 'a \<Rightarrow> 'a \<Rightarrow> 'a)" 
770 
by standard (simp add: fun_eq_iff ac_simps) 

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

772 
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

773 
then show ?thesis 
60679  774 
by (auto simp add: Inf_fold_inf inf_min empty_Set[symmetric] 
775 
r_min_eq_r_min_opt[symmetric] r_min_alt_def) 

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

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

777 

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

778 
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

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

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

781 

56212
3253aaf73a01
consolidated theorem names containing INFI and SUPR: have INF and SUP instead uniformly
haftmann
parents:
56019
diff
changeset

782 
lemma INF_Set_fold [code]: 
54263
c4159fe6fa46
move Lubs from HOL to HOLLibrary (replaced by conditionally complete lattices)
hoelzl
parents:
53955
diff
changeset

783 
fixes f :: "_ \<Rightarrow> 'a::complete_lattice" 
56218
1c3f1f2431f9
elongated INFI and SUPR, to reduced risk of confusing theorems names in the future while still being consistent with INTER and UNION
haftmann
parents:
56212
diff
changeset

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

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

786 
have "comp_fun_commute ((inf :: 'a \<Rightarrow> 'a \<Rightarrow> 'a) \<circ> f)" 
60679  787 
by standard (auto simp add: fun_eq_iff ac_simps) 
48623
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

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

789 
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

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

791 

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

792 
lemma Max_fin_set_fold [code]: 
53745  793 
"Max (Set t) = 
56019  794 
(if RBT.is_empty t 
53745  795 
then Code.abort (STR ''not_non_empty_tree'') (\<lambda>_. Max (Set t)) 
796 
else r_max_opt t)" 

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

797 
proof  
51489  798 
have *: "semilattice (max :: 'a \<Rightarrow> 'a \<Rightarrow> 'a)" .. 
799 
with finite_fold1_fold1_keys [OF *, folded Max_def] 

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

800 
show ?thesis 
53745  801 
by (simp add: r_max_alt_def r_max_eq_r_max_opt [symmetric]) 
48623
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

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

803 

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

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

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

806 
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

807 

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

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

809 
fixes t :: "('a :: {linorder, complete_lattice}, unit) rbt" 
56019  810 
shows "Sup (Set t) = (if RBT.is_empty t then bot else r_max_opt t)" 
48623
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

811 
proof  
60679  812 
have "comp_fun_commute (max :: 'a \<Rightarrow> 'a \<Rightarrow> 'a)" 
813 
by standard (simp add: fun_eq_iff ac_simps) 

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

815 
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

816 
then show ?thesis 
60679  817 
by (auto simp add: Sup_fold_sup sup_max empty_Set[symmetric] 
818 
r_max_eq_r_max_opt[symmetric] r_max_alt_def) 

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

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

820 

60679  821 
definition Sup' :: "'a :: {linorder,complete_lattice} set \<Rightarrow> 'a" 
822 
where [code del]: "Sup' x = Sup x" 

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

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

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

825 

56212
3253aaf73a01
consolidated theorem names containing INFI and SUPR: have INF and SUP instead uniformly
haftmann
parents:
56019
diff
changeset

826 
lemma SUP_Set_fold [code]: 
54263
c4159fe6fa46
move Lubs from HOL to HOLLibrary (replaced by conditionally complete lattices)
hoelzl
parents:
53955
diff
changeset

827 
fixes f :: "_ \<Rightarrow> 'a::complete_lattice" 
56218
1c3f1f2431f9
elongated INFI and SUPR, to reduced risk of confusing theorems names in the future while still being consistent with INTER and UNION
haftmann
parents:
56212
diff
changeset

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

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

830 
have "comp_fun_commute ((sup :: 'a \<Rightarrow> 'a \<Rightarrow> 'a) \<circ> f)" 
60679  831 
by standard (auto simp add: fun_eq_iff ac_simps) 
48623
bea613f2543d
implementation of sets by RBT trees for the code generator
kuncar
parents:
diff
changeset

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

833 
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

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

835 

60679  836 
lemma sorted_list_set[code]: "sorted_list_of_set (Set t) = RBT.keys t" 
837 
by (auto simp add: set_keys intro: sorted_distinct_set_unique) 

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

838 

53955  839 
lemma Bleast_code [code]: 
60679  840 
"Bleast (Set t) P = 
841 
(case filter P (RBT.keys t) of 

842 
x # xs \<Rightarrow> x 

843 
 [] \<Rightarrow> abort_Bleast (Set t) P)" 

56019  844 
proof (cases "filter P (RBT.keys t)") 
60679  845 
case Nil 
846 
thus ?thesis by (simp add: Bleast_def abort_Bleast_def) 

53955  847 
next 
848 
case (Cons x ys) 

849 
have "(LEAST x. x \<in> Set t \<and> P x) = x" 

850 
proof (rule Least_equality) 

60679  851 
show "x \<in> Set t \<and> P x" 
852 
using Cons[symmetric] 

853 
by (auto simp add: set_keys Cons_eq_filter_iff) 

53955  854 
next 
60679  855 
fix y 
856 
assume "y \<in> Set t \<and> P y" 

857 
then show "x \<le> y" 

858 
using Cons[symmetric] 

53955  859 
by(auto simp add: set_keys Cons_eq_filter_iff) 
860 
(metis sorted_Cons sorted_append sorted_keys) 

861 
qed 

862 
thus ?thesis using Cons by (simp add: Bleast_def) 

863 
qed 

864 

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

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

866 

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

867 
end 