author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 46868  6c250adbe101 
child 49834  b27bbb021df1 
permissions  rwrr 
42151  1 
(* Title: HOL/HOLCF/Universal.thy 
27411  2 
Author: Brian Huffman 
3 
*) 

4 

35794  5 
header {* A universal bifinite domain *} 
6 

27411  7 
theory Universal 
41413
64cd30d6b0b8
explicit file specifications  avoid secondary load path;
wenzelm
parents:
41394
diff
changeset

8 
imports Bifinite Completion "~~/src/HOL/Library/Nat_Bijection" 
27411  9 
begin 
10 

39974
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

11 
subsection {* Basis for universal domain *} 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

12 

b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

13 
subsubsection {* Basis datatype *} 
27411  14 

41295  15 
type_synonym ubasis = nat 
27411  16 

17 
definition 

18 
node :: "nat \<Rightarrow> ubasis \<Rightarrow> ubasis set \<Rightarrow> ubasis" 

19 
where 

35701  20 
"node i a S = Suc (prod_encode (i, prod_encode (a, set_encode S)))" 
27411  21 

30505  22 
lemma node_not_0 [simp]: "node i a S \<noteq> 0" 
27411  23 
unfolding node_def by simp 
24 

30505  25 
lemma node_gt_0 [simp]: "0 < node i a S" 
27411  26 
unfolding node_def by simp 
27 

28 
lemma node_inject [simp]: 

30505  29 
"\<lbrakk>finite S; finite T\<rbrakk> 
30 
\<Longrightarrow> node i a S = node j b T \<longleftrightarrow> i = j \<and> a = b \<and> S = T" 

35701  31 
unfolding node_def by (simp add: prod_encode_eq set_encode_eq) 
27411  32 

30505  33 
lemma node_gt0: "i < node i a S" 
27411  34 
unfolding node_def less_Suc_eq_le 
35701  35 
by (rule le_prod_encode_1) 
27411  36 

30505  37 
lemma node_gt1: "a < node i a S" 
27411  38 
unfolding node_def less_Suc_eq_le 
35701  39 
by (rule order_trans [OF le_prod_encode_1 le_prod_encode_2]) 
27411  40 

41 
lemma nat_less_power2: "n < 2^n" 

42 
by (induct n) simp_all 

43 

30505  44 
lemma node_gt2: "\<lbrakk>finite S; b \<in> S\<rbrakk> \<Longrightarrow> b < node i a S" 
35701  45 
unfolding node_def less_Suc_eq_le set_encode_def 
46 
apply (rule order_trans [OF _ le_prod_encode_2]) 

47 
apply (rule order_trans [OF _ le_prod_encode_2]) 

30505  48 
apply (rule order_trans [where y="setsum (op ^ 2) {b}"]) 
27411  49 
apply (simp add: nat_less_power2 [THEN order_less_imp_le]) 
50 
apply (erule setsum_mono2, simp, simp) 

51 
done 

52 

35701  53 
lemma eq_prod_encode_pairI: 
54 
"\<lbrakk>fst (prod_decode x) = a; snd (prod_decode x) = b\<rbrakk> \<Longrightarrow> x = prod_encode (a, b)" 

27411  55 
by (erule subst, erule subst, simp) 
56 

57 
lemma node_cases: 

58 
assumes 1: "x = 0 \<Longrightarrow> P" 

30505  59 
assumes 2: "\<And>i a S. \<lbrakk>finite S; x = node i a S\<rbrakk> \<Longrightarrow> P" 
27411  60 
shows "P" 
61 
apply (cases x) 

62 
apply (erule 1) 

63 
apply (rule 2) 

35701  64 
apply (rule finite_set_decode) 
27411  65 
apply (simp add: node_def) 
35701  66 
apply (rule eq_prod_encode_pairI [OF refl]) 
67 
apply (rule eq_prod_encode_pairI [OF refl refl]) 

27411  68 
done 
69 

70 
lemma node_induct: 

71 
assumes 1: "P 0" 

30505  72 
assumes 2: "\<And>i a S. \<lbrakk>P a; finite S; \<forall>b\<in>S. P b\<rbrakk> \<Longrightarrow> P (node i a S)" 
27411  73 
shows "P x" 
74 
apply (induct x rule: nat_less_induct) 

75 
apply (case_tac n rule: node_cases) 

76 
apply (simp add: 1) 

77 
apply (simp add: 2 node_gt1 node_gt2) 

78 
done 

79 

39974
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

80 
subsubsection {* Basis ordering *} 
27411  81 

82 
inductive 

83 
ubasis_le :: "nat \<Rightarrow> nat \<Rightarrow> bool" 

84 
where 

30505  85 
ubasis_le_refl: "ubasis_le a a" 
27411  86 
 ubasis_le_trans: 
30505  87 
"\<lbrakk>ubasis_le a b; ubasis_le b c\<rbrakk> \<Longrightarrow> ubasis_le a c" 
27411  88 
 ubasis_le_lower: 
30505  89 
"finite S \<Longrightarrow> ubasis_le a (node i a S)" 
27411  90 
 ubasis_le_upper: 
30505  91 
"\<lbrakk>finite S; b \<in> S; ubasis_le a b\<rbrakk> \<Longrightarrow> ubasis_le (node i a S) b" 
27411  92 

93 
lemma ubasis_le_minimal: "ubasis_le 0 x" 

94 
apply (induct x rule: node_induct) 

95 
apply (rule ubasis_le_refl) 

96 
apply (erule ubasis_le_trans) 

97 
apply (erule ubasis_le_lower) 

98 
done 

99 

39974
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

100 
interpretation udom: preorder ubasis_le 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

101 
apply default 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

102 
apply (rule ubasis_le_refl) 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

103 
apply (erule (1) ubasis_le_trans) 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

104 
done 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

105 

27411  106 
subsubsection {* Generic take function *} 
107 

108 
function 

109 
ubasis_until :: "(ubasis \<Rightarrow> bool) \<Rightarrow> ubasis \<Rightarrow> ubasis" 

110 
where 

111 
"ubasis_until P 0 = 0" 

30505  112 
 "finite S \<Longrightarrow> ubasis_until P (node i a S) = 
113 
(if P (node i a S) then node i a S else ubasis_until P a)" 

27411  114 
apply clarify 
115 
apply (rule_tac x=b in node_cases) 

116 
apply simp 

117 
apply simp 

118 
apply fast 

119 
apply simp 

120 
apply simp 

121 
apply simp 

122 
done 

123 

124 
termination ubasis_until 

125 
apply (relation "measure snd") 

126 
apply (rule wf_measure) 

127 
apply (simp add: node_gt1) 

128 
done 

129 

130 
lemma ubasis_until: "P 0 \<Longrightarrow> P (ubasis_until P x)" 

131 
by (induct x rule: node_induct) simp_all 

132 

133 
lemma ubasis_until': "0 < ubasis_until P x \<Longrightarrow> P (ubasis_until P x)" 

134 
by (induct x rule: node_induct) auto 

135 

136 
lemma ubasis_until_same: "P x \<Longrightarrow> ubasis_until P x = x" 

137 
by (induct x rule: node_induct) simp_all 

138 

139 
lemma ubasis_until_idem: 

140 
"P 0 \<Longrightarrow> ubasis_until P (ubasis_until P x) = ubasis_until P x" 

141 
by (rule ubasis_until_same [OF ubasis_until]) 

142 

143 
lemma ubasis_until_0: 

144 
"\<forall>x. x \<noteq> 0 \<longrightarrow> \<not> P x \<Longrightarrow> ubasis_until P x = 0" 

145 
by (induct x rule: node_induct) simp_all 

146 

147 
lemma ubasis_until_less: "ubasis_le (ubasis_until P x) x" 

148 
apply (induct x rule: node_induct) 

149 
apply (simp add: ubasis_le_refl) 

150 
apply (simp add: ubasis_le_refl) 

151 
apply (rule impI) 

152 
apply (erule ubasis_le_trans) 

153 
apply (erule ubasis_le_lower) 

154 
done 

155 

156 
lemma ubasis_until_chain: 

157 
assumes PQ: "\<And>x. P x \<Longrightarrow> Q x" 

158 
shows "ubasis_le (ubasis_until P x) (ubasis_until Q x)" 

159 
apply (induct x rule: node_induct) 

160 
apply (simp add: ubasis_le_refl) 

161 
apply (simp add: ubasis_le_refl) 

162 
apply (simp add: PQ) 

163 
apply clarify 

164 
apply (rule ubasis_le_trans) 

165 
apply (rule ubasis_until_less) 

166 
apply (erule ubasis_le_lower) 

167 
done 

168 

169 
lemma ubasis_until_mono: 

30505  170 
assumes "\<And>i a S b. \<lbrakk>finite S; P (node i a S); b \<in> S; ubasis_le a b\<rbrakk> \<Longrightarrow> P b" 
171 
shows "ubasis_le a b \<Longrightarrow> ubasis_le (ubasis_until P a) (ubasis_until P b)" 

30561  172 
proof (induct set: ubasis_le) 
173 
case (ubasis_le_refl a) show ?case by (rule ubasis_le.ubasis_le_refl) 

174 
next 

175 
case (ubasis_le_trans a b c) thus ?case by  (rule ubasis_le.ubasis_le_trans) 

176 
next 

177 
case (ubasis_le_lower S a i) thus ?case 

178 
apply (clarsimp simp add: ubasis_le_refl) 

179 
apply (rule ubasis_le_trans [OF ubasis_until_less]) 

180 
apply (erule ubasis_le.ubasis_le_lower) 

181 
done 

182 
next 

183 
case (ubasis_le_upper S b a i) thus ?case 

184 
apply clarsimp 

185 
apply (subst ubasis_until_same) 

41529  186 
apply (erule (3) assms) 
30561  187 
apply (erule (2) ubasis_le.ubasis_le_upper) 
188 
done 

189 
qed 

27411  190 

191 
lemma finite_range_ubasis_until: 

192 
"finite {x. P x} \<Longrightarrow> finite (range (ubasis_until P))" 

193 
apply (rule finite_subset [where B="insert 0 {x. P x}"]) 

194 
apply (clarsimp simp add: ubasis_until') 

195 
apply simp 

196 
done 

197 

198 

199 
subsection {* Defining the universal domain by ideal completion *} 

200 

201 
typedef (open) udom = "{S. udom.ideal S}" 

40888
28cd51cff70c
reformulate lemma preorder.ex_ideal, and use it for typedefs
huffman
parents:
40774
diff
changeset

202 
by (rule udom.ex_ideal) 
27411  203 

31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
30729
diff
changeset

204 
instantiation udom :: below 
27411  205 
begin 
206 

207 
definition 

208 
"x \<sqsubseteq> y \<longleftrightarrow> Rep_udom x \<subseteq> Rep_udom y" 

209 

210 
instance .. 

211 
end 

212 

213 
instance udom :: po 

39974
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

214 
using type_definition_udom below_udom_def 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

215 
by (rule udom.typedef_ideal_po) 
27411  216 

217 
instance udom :: cpo 

39974
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

218 
using type_definition_udom below_udom_def 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

219 
by (rule udom.typedef_ideal_cpo) 
27411  220 

221 
definition 

222 
udom_principal :: "nat \<Rightarrow> udom" where 

223 
"udom_principal t = Abs_udom {u. ubasis_le u t}" 

224 

39984  225 
lemma ubasis_countable: "\<exists>f::ubasis \<Rightarrow> nat. inj f" 
226 
by (rule exI, rule inj_on_id) 

27411  227 

30729
461ee3e49ad3
interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents:
30561
diff
changeset

228 
interpretation udom: 
39974
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

229 
ideal_completion ubasis_le udom_principal Rep_udom 
39984  230 
using type_definition_udom below_udom_def 
231 
using udom_principal_def ubasis_countable 

232 
by (rule udom.typedef_ideal_completion) 

27411  233 

234 
text {* Universal domain is pointed *} 

235 

236 
lemma udom_minimal: "udom_principal 0 \<sqsubseteq> x" 

237 
apply (induct x rule: udom.principal_induct) 

238 
apply (simp, simp add: ubasis_le_minimal) 

239 
done 

240 

241 
instance udom :: pcpo 

242 
by intro_classes (fast intro: udom_minimal) 

243 

244 
lemma inst_udom_pcpo: "\<bottom> = udom_principal 0" 

41430
1aa23e9f2c87
change some lemma names containing 'UU' to 'bottom'
huffman
parents:
41413
diff
changeset

245 
by (rule udom_minimal [THEN bottomI, symmetric]) 
27411  246 

39974
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

247 

b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

248 
subsection {* Compact bases of domains *} 
27411  249 

39974
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

250 
typedef (open) 'a compact_basis = "{x::'a::pcpo. compact x}" 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

251 
by auto 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

252 

41370
17b09240893c
declare more simp rules, rewrite proofs in Isarstyle
huffman
parents:
41295
diff
changeset

253 
lemma Rep_compact_basis' [simp]: "compact (Rep_compact_basis a)" 
39974
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

254 
by (rule Rep_compact_basis [unfolded mem_Collect_eq]) 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

255 

41370
17b09240893c
declare more simp rules, rewrite proofs in Isarstyle
huffman
parents:
41295
diff
changeset

256 
lemma Abs_compact_basis_inverse' [simp]: 
17b09240893c
declare more simp rules, rewrite proofs in Isarstyle
huffman
parents:
41295
diff
changeset

257 
"compact x \<Longrightarrow> Rep_compact_basis (Abs_compact_basis x) = x" 
17b09240893c
declare more simp rules, rewrite proofs in Isarstyle
huffman
parents:
41295
diff
changeset

258 
by (rule Abs_compact_basis_inverse [unfolded mem_Collect_eq]) 
17b09240893c
declare more simp rules, rewrite proofs in Isarstyle
huffman
parents:
41295
diff
changeset

259 

39974
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

260 
instantiation compact_basis :: (pcpo) below 
27411  261 
begin 
262 

263 
definition 

39974
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

264 
compact_le_def: 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

265 
"(op \<sqsubseteq>) \<equiv> (\<lambda>x y. Rep_compact_basis x \<sqsubseteq> Rep_compact_basis y)" 
27411  266 

39974
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

267 
instance .. 
27411  268 
end 
269 

39974
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

270 
instance compact_basis :: (pcpo) po 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

271 
using type_definition_compact_basis compact_le_def 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

272 
by (rule typedef_po) 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

273 

b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

274 
definition 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

275 
approximants :: "'a \<Rightarrow> 'a compact_basis set" where 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

276 
"approximants = (\<lambda>x. {a. Rep_compact_basis a \<sqsubseteq> x})" 
27411  277 

39974
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

278 
definition 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

279 
compact_bot :: "'a::pcpo compact_basis" where 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

280 
"compact_bot = Abs_compact_basis \<bottom>" 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

281 

b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

282 
lemma Rep_compact_bot [simp]: "Rep_compact_basis compact_bot = \<bottom>" 
41370
17b09240893c
declare more simp rules, rewrite proofs in Isarstyle
huffman
parents:
41295
diff
changeset

283 
unfolding compact_bot_def by simp 
39974
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

284 

b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

285 
lemma compact_bot_minimal [simp]: "compact_bot \<sqsubseteq> a" 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

286 
unfolding compact_le_def Rep_compact_bot by simp 
27411  287 

288 

35900
aa5dfb03eb1e
remove LaTeX hyperref warnings by avoiding antiquotations within section headings
huffman
parents:
35794
diff
changeset

289 
subsection {* Universality of \emph{udom} *} 
27411  290 

39974
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

291 
text {* We use a locale to parameterize the construction over a chain 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

292 
of approx functions on the type to be embedded. *} 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

293 

46868  294 
locale bifinite_approx_chain = 
295 
approx_chain approx for approx :: "nat \<Rightarrow> 'a::bifinite \<rightarrow> 'a" 

39974
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

296 
begin 
27411  297 

298 
subsubsection {* Choosing a maximal element from a finite set *} 

299 

300 
lemma finite_has_maximal: 

39974
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

301 
fixes A :: "'a compact_basis set" 
27411  302 
shows "\<lbrakk>finite A; A \<noteq> {}\<rbrakk> \<Longrightarrow> \<exists>x\<in>A. \<forall>y\<in>A. x \<sqsubseteq> y \<longrightarrow> x = y" 
303 
proof (induct rule: finite_ne_induct) 

304 
case (singleton x) 

305 
show ?case by simp 

306 
next 

307 
case (insert a A) 

308 
from `\<exists>x\<in>A. \<forall>y\<in>A. x \<sqsubseteq> y \<longrightarrow> x = y` 

309 
obtain x where x: "x \<in> A" 

310 
and x_eq: "\<And>y. \<lbrakk>y \<in> A; x \<sqsubseteq> y\<rbrakk> \<Longrightarrow> x = y" by fast 

311 
show ?case 

312 
proof (intro bexI ballI impI) 

313 
fix y 

314 
assume "y \<in> insert a A" and "(if x \<sqsubseteq> a then a else x) \<sqsubseteq> y" 

315 
thus "(if x \<sqsubseteq> a then a else x) = y" 

316 
apply auto 

31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
30729
diff
changeset

317 
apply (frule (1) below_trans) 
27411  318 
apply (frule (1) x_eq) 
31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
30729
diff
changeset

319 
apply (rule below_antisym, assumption) 
27411  320 
apply simp 
321 
apply (erule (1) x_eq) 

322 
done 

323 
next 

324 
show "(if x \<sqsubseteq> a then a else x) \<in> insert a A" 

325 
by (simp add: x) 

326 
qed 

327 
qed 

328 

329 
definition 

330 
choose :: "'a compact_basis set \<Rightarrow> 'a compact_basis" 

331 
where 

332 
"choose A = (SOME x. x \<in> {x\<in>A. \<forall>y\<in>A. x \<sqsubseteq> y \<longrightarrow> x = y})" 

333 

334 
lemma choose_lemma: 

335 
"\<lbrakk>finite A; A \<noteq> {}\<rbrakk> \<Longrightarrow> choose A \<in> {x\<in>A. \<forall>y\<in>A. x \<sqsubseteq> y \<longrightarrow> x = y}" 

336 
unfolding choose_def 

337 
apply (rule someI_ex) 

338 
apply (frule (1) finite_has_maximal, fast) 

339 
done 

340 

341 
lemma maximal_choose: 

342 
"\<lbrakk>finite A; y \<in> A; choose A \<sqsubseteq> y\<rbrakk> \<Longrightarrow> choose A = y" 

343 
apply (cases "A = {}", simp) 

344 
apply (frule (1) choose_lemma, simp) 

345 
done 

346 

347 
lemma choose_in: "\<lbrakk>finite A; A \<noteq> {}\<rbrakk> \<Longrightarrow> choose A \<in> A" 

348 
by (frule (1) choose_lemma, simp) 

349 

350 
function 

351 
choose_pos :: "'a compact_basis set \<Rightarrow> 'a compact_basis \<Rightarrow> nat" 

352 
where 

353 
"choose_pos A x = 

354 
(if finite A \<and> x \<in> A \<and> x \<noteq> choose A 

355 
then Suc (choose_pos (A  {choose A}) x) else 0)" 

356 
by auto 

357 

358 
termination choose_pos 

359 
apply (relation "measure (card \<circ> fst)", simp) 

360 
apply clarsimp 

361 
apply (rule card_Diff1_less) 

362 
apply assumption 

363 
apply (erule choose_in) 

364 
apply clarsimp 

365 
done 

366 

367 
declare choose_pos.simps [simp del] 

368 

369 
lemma choose_pos_choose: "finite A \<Longrightarrow> choose_pos A (choose A) = 0" 

370 
by (simp add: choose_pos.simps) 

371 

372 
lemma inj_on_choose_pos [OF refl]: 

373 
"\<lbrakk>card A = n; finite A\<rbrakk> \<Longrightarrow> inj_on (choose_pos A) A" 

374 
apply (induct n arbitrary: A) 

375 
apply simp 

376 
apply (case_tac "A = {}", simp) 

377 
apply (frule (1) choose_in) 

378 
apply (rule inj_onI) 

379 
apply (drule_tac x="A  {choose A}" in meta_spec, simp) 

380 
apply (simp add: choose_pos.simps) 

381 
apply (simp split: split_if_asm) 

382 
apply (erule (1) inj_onD, simp, simp) 

383 
done 

384 

385 
lemma choose_pos_bounded [OF refl]: 

386 
"\<lbrakk>card A = n; finite A; x \<in> A\<rbrakk> \<Longrightarrow> choose_pos A x < n" 

387 
apply (induct n arbitrary: A) 

388 
apply simp 

389 
apply (case_tac "A = {}", simp) 

390 
apply (frule (1) choose_in) 

391 
apply (subst choose_pos.simps) 

392 
apply simp 

393 
done 

394 

395 
lemma choose_pos_lessD: 

41182  396 
"\<lbrakk>choose_pos A x < choose_pos A y; finite A; x \<in> A; y \<in> A\<rbrakk> \<Longrightarrow> x \<notsqsubseteq> y" 
27411  397 
apply (induct A x arbitrary: y rule: choose_pos.induct) 
398 
apply simp 

399 
apply (case_tac "x = choose A") 

400 
apply simp 

401 
apply (rule notI) 

402 
apply (frule (2) maximal_choose) 

403 
apply simp 

404 
apply (case_tac "y = choose A") 

405 
apply (simp add: choose_pos_choose) 

406 
apply (drule_tac x=y in meta_spec) 

407 
apply simp 

408 
apply (erule meta_mp) 

409 
apply (simp add: choose_pos.simps) 

410 
done 

411 

39974
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

412 
subsubsection {* Compact basis take function *} 
27411  413 

414 
primrec 

39974
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

415 
cb_take :: "nat \<Rightarrow> 'a compact_basis \<Rightarrow> 'a compact_basis" where 
27411  416 
"cb_take 0 = (\<lambda>x. compact_bot)" 
39974
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

417 
 "cb_take (Suc n) = (\<lambda>a. Abs_compact_basis (approx n\<cdot>(Rep_compact_basis a)))" 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

418 

b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

419 
declare cb_take.simps [simp del] 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

420 

b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

421 
lemma cb_take_zero [simp]: "cb_take 0 a = compact_bot" 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

422 
by (simp only: cb_take.simps) 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

423 

b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

424 
lemma Rep_cb_take: 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

425 
"Rep_compact_basis (cb_take (Suc n) a) = approx n\<cdot>(Rep_compact_basis a)" 
41370
17b09240893c
declare more simp rules, rewrite proofs in Isarstyle
huffman
parents:
41295
diff
changeset

426 
by (simp add: cb_take.simps(2)) 
39974
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

427 

b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

428 
lemmas approx_Rep_compact_basis = Rep_cb_take [symmetric] 
27411  429 

430 
lemma cb_take_covers: "\<exists>n. cb_take n x = x" 

39974
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

431 
apply (subgoal_tac "\<exists>n. cb_take (Suc n) x = x", fast) 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

432 
apply (simp add: Rep_compact_basis_inject [symmetric]) 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

433 
apply (simp add: Rep_cb_take) 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

434 
apply (rule compact_eq_approx) 
41370
17b09240893c
declare more simp rules, rewrite proofs in Isarstyle
huffman
parents:
41295
diff
changeset

435 
apply (rule Rep_compact_basis') 
27411  436 
done 
437 

438 
lemma cb_take_less: "cb_take n x \<sqsubseteq> x" 

39974
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

439 
unfolding compact_le_def 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

440 
by (cases n, simp, simp add: Rep_cb_take approx_below) 
27411  441 

442 
lemma cb_take_idem: "cb_take n (cb_take n x) = cb_take n x" 

39974
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

443 
unfolding Rep_compact_basis_inject [symmetric] 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

444 
by (cases n, simp, simp add: Rep_cb_take approx_idem) 
27411  445 

446 
lemma cb_take_mono: "x \<sqsubseteq> y \<Longrightarrow> cb_take n x \<sqsubseteq> cb_take n y" 

39974
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

447 
unfolding compact_le_def 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

448 
by (cases n, simp, simp add: Rep_cb_take monofun_cfun_arg) 
27411  449 

450 
lemma cb_take_chain_le: "m \<le> n \<Longrightarrow> cb_take m x \<sqsubseteq> cb_take n x" 

39974
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

451 
unfolding compact_le_def 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

452 
apply (cases m, simp, cases n, simp) 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

453 
apply (simp add: Rep_cb_take, rule chain_mono, simp, simp) 
27411  454 
done 
455 

456 
lemma finite_range_cb_take: "finite (range (cb_take n))" 

457 
apply (cases n) 

39974
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

458 
apply (subgoal_tac "range (cb_take 0) = {compact_bot}", simp, force) 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

459 
apply (rule finite_imageD [where f="Rep_compact_basis"]) 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

460 
apply (rule finite_subset [where B="range (\<lambda>x. approx (n  1)\<cdot>x)"]) 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

461 
apply (clarsimp simp add: Rep_cb_take) 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

462 
apply (rule finite_range_approx) 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

463 
apply (rule inj_onI, simp add: Rep_compact_basis_inject) 
27411  464 
done 
465 

39974
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

466 
subsubsection {* Rank of basis elements *} 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

467 

27411  468 
definition 
469 
rank :: "'a compact_basis \<Rightarrow> nat" 

470 
where 

471 
"rank x = (LEAST n. cb_take n x = x)" 

472 

473 
lemma compact_approx_rank: "cb_take (rank x) x = x" 

474 
unfolding rank_def 

475 
apply (rule LeastI_ex) 

476 
apply (rule cb_take_covers) 

477 
done 

478 

479 
lemma rank_leD: "rank x \<le> n \<Longrightarrow> cb_take n x = x" 

31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
30729
diff
changeset

480 
apply (rule below_antisym [OF cb_take_less]) 
27411  481 
apply (subst compact_approx_rank [symmetric]) 
482 
apply (erule cb_take_chain_le) 

483 
done 

484 

485 
lemma rank_leI: "cb_take n x = x \<Longrightarrow> rank x \<le> n" 

486 
unfolding rank_def by (rule Least_le) 

487 

488 
lemma rank_le_iff: "rank x \<le> n \<longleftrightarrow> cb_take n x = x" 

489 
by (rule iffI [OF rank_leD rank_leI]) 

490 

30505  491 
lemma rank_compact_bot [simp]: "rank compact_bot = 0" 
492 
using rank_leI [of 0 compact_bot] by simp 

493 

494 
lemma rank_eq_0_iff [simp]: "rank x = 0 \<longleftrightarrow> x = compact_bot" 

495 
using rank_le_iff [of x 0] by auto 

496 

27411  497 
definition 
498 
rank_le :: "'a compact_basis \<Rightarrow> 'a compact_basis set" 

499 
where 

500 
"rank_le x = {y. rank y \<le> rank x}" 

501 

502 
definition 

503 
rank_lt :: "'a compact_basis \<Rightarrow> 'a compact_basis set" 

504 
where 

505 
"rank_lt x = {y. rank y < rank x}" 

506 

507 
definition 

508 
rank_eq :: "'a compact_basis \<Rightarrow> 'a compact_basis set" 

509 
where 

510 
"rank_eq x = {y. rank y = rank x}" 

511 

512 
lemma rank_eq_cong: "rank x = rank y \<Longrightarrow> rank_eq x = rank_eq y" 

513 
unfolding rank_eq_def by simp 

514 

515 
lemma rank_lt_cong: "rank x = rank y \<Longrightarrow> rank_lt x = rank_lt y" 

516 
unfolding rank_lt_def by simp 

517 

518 
lemma rank_eq_subset: "rank_eq x \<subseteq> rank_le x" 

519 
unfolding rank_eq_def rank_le_def by auto 

520 

521 
lemma rank_lt_subset: "rank_lt x \<subseteq> rank_le x" 

522 
unfolding rank_lt_def rank_le_def by auto 

523 

524 
lemma finite_rank_le: "finite (rank_le x)" 

525 
unfolding rank_le_def 

526 
apply (rule finite_subset [where B="range (cb_take (rank x))"]) 

527 
apply clarify 

528 
apply (rule range_eqI) 

529 
apply (erule rank_leD [symmetric]) 

530 
apply (rule finite_range_cb_take) 

531 
done 

532 

533 
lemma finite_rank_eq: "finite (rank_eq x)" 

534 
by (rule finite_subset [OF rank_eq_subset finite_rank_le]) 

535 

536 
lemma finite_rank_lt: "finite (rank_lt x)" 

537 
by (rule finite_subset [OF rank_lt_subset finite_rank_le]) 

538 

539 
lemma rank_lt_Int_rank_eq: "rank_lt x \<inter> rank_eq x = {}" 

540 
unfolding rank_lt_def rank_eq_def rank_le_def by auto 

541 

542 
lemma rank_lt_Un_rank_eq: "rank_lt x \<union> rank_eq x = rank_le x" 

543 
unfolding rank_lt_def rank_eq_def rank_le_def by auto 

544 

30505  545 
subsubsection {* Sequencing basis elements *} 
27411  546 

547 
definition 

30505  548 
place :: "'a compact_basis \<Rightarrow> nat" 
27411  549 
where 
30505  550 
"place x = card (rank_lt x) + choose_pos (rank_eq x) x" 
27411  551 

30505  552 
lemma place_bounded: "place x < card (rank_le x)" 
553 
unfolding place_def 

27411  554 
apply (rule ord_less_eq_trans) 
555 
apply (rule add_strict_left_mono) 

556 
apply (rule choose_pos_bounded) 

557 
apply (rule finite_rank_eq) 

558 
apply (simp add: rank_eq_def) 

559 
apply (subst card_Un_disjoint [symmetric]) 

560 
apply (rule finite_rank_lt) 

561 
apply (rule finite_rank_eq) 

562 
apply (rule rank_lt_Int_rank_eq) 

563 
apply (simp add: rank_lt_Un_rank_eq) 

564 
done 

565 

30505  566 
lemma place_ge: "card (rank_lt x) \<le> place x" 
567 
unfolding place_def by simp 

27411  568 

30505  569 
lemma place_rank_mono: 
27411  570 
fixes x y :: "'a compact_basis" 
30505  571 
shows "rank x < rank y \<Longrightarrow> place x < place y" 
572 
apply (rule less_le_trans [OF place_bounded]) 

573 
apply (rule order_trans [OF _ place_ge]) 

27411  574 
apply (rule card_mono) 
575 
apply (rule finite_rank_lt) 

576 
apply (simp add: rank_le_def rank_lt_def subset_eq) 

577 
done 

578 

30505  579 
lemma place_eqD: "place x = place y \<Longrightarrow> x = y" 
27411  580 
apply (rule linorder_cases [where x="rank x" and y="rank y"]) 
30505  581 
apply (drule place_rank_mono, simp) 
582 
apply (simp add: place_def) 

27411  583 
apply (rule inj_on_choose_pos [where A="rank_eq x", THEN inj_onD]) 
584 
apply (rule finite_rank_eq) 

585 
apply (simp cong: rank_lt_cong rank_eq_cong) 

586 
apply (simp add: rank_eq_def) 

587 
apply (simp add: rank_eq_def) 

30505  588 
apply (drule place_rank_mono, simp) 
27411  589 
done 
590 

30505  591 
lemma inj_place: "inj place" 
592 
by (rule inj_onI, erule place_eqD) 

27411  593 

594 
subsubsection {* Embedding and projection on basis elements *} 

595 

30505  596 
definition 
597 
sub :: "'a compact_basis \<Rightarrow> 'a compact_basis" 

598 
where 

599 
"sub x = (case rank x of 0 \<Rightarrow> compact_bot  Suc k \<Rightarrow> cb_take k x)" 

600 

601 
lemma rank_sub_less: "x \<noteq> compact_bot \<Longrightarrow> rank (sub x) < rank x" 

602 
unfolding sub_def 

603 
apply (cases "rank x", simp) 

604 
apply (simp add: less_Suc_eq_le) 

605 
apply (rule rank_leI) 

606 
apply (rule cb_take_idem) 

607 
done 

608 

609 
lemma place_sub_less: "x \<noteq> compact_bot \<Longrightarrow> place (sub x) < place x" 

610 
apply (rule place_rank_mono) 

611 
apply (erule rank_sub_less) 

612 
done 

613 

614 
lemma sub_below: "sub x \<sqsubseteq> x" 

615 
unfolding sub_def by (cases "rank x", simp_all add: cb_take_less) 

616 

617 
lemma rank_less_imp_below_sub: "\<lbrakk>x \<sqsubseteq> y; rank x < rank y\<rbrakk> \<Longrightarrow> x \<sqsubseteq> sub y" 

618 
unfolding sub_def 

619 
apply (cases "rank y", simp) 

620 
apply (simp add: less_Suc_eq_le) 

621 
apply (subgoal_tac "cb_take nat x \<sqsubseteq> cb_take nat y") 

622 
apply (simp add: rank_leD) 

623 
apply (erule cb_take_mono) 

624 
done 

625 

27411  626 
function 
627 
basis_emb :: "'a compact_basis \<Rightarrow> ubasis" 

628 
where 

629 
"basis_emb x = (if x = compact_bot then 0 else 

30505  630 
node (place x) (basis_emb (sub x)) 
631 
(basis_emb ` {y. place y < place x \<and> x \<sqsubseteq> y}))" 

27411  632 
by auto 
633 

634 
termination basis_emb 

30505  635 
apply (relation "measure place", simp) 
636 
apply (simp add: place_sub_less) 

27411  637 
apply simp 
638 
done 

639 

640 
declare basis_emb.simps [simp del] 

641 

642 
lemma basis_emb_compact_bot [simp]: "basis_emb compact_bot = 0" 

643 
by (simp add: basis_emb.simps) 

644 

30505  645 
lemma fin1: "finite {y. place y < place x \<and> x \<sqsubseteq> y}" 
27411  646 
apply (subst Collect_conj_eq) 
647 
apply (rule finite_Int) 

648 
apply (rule disjI1) 

30505  649 
apply (subgoal_tac "finite (place ` {n. n < place x})", simp) 
650 
apply (rule finite_vimageI [OF _ inj_place]) 

27411  651 
apply (simp add: lessThan_def [symmetric]) 
652 
done 

653 

30505  654 
lemma fin2: "finite (basis_emb ` {y. place y < place x \<and> x \<sqsubseteq> y})" 
27411  655 
by (rule finite_imageI [OF fin1]) 
656 

30505  657 
lemma rank_place_mono: 
658 
"\<lbrakk>place x < place y; x \<sqsubseteq> y\<rbrakk> \<Longrightarrow> rank x < rank y" 

659 
apply (rule linorder_cases, assumption) 

660 
apply (simp add: place_def cong: rank_lt_cong rank_eq_cong) 

661 
apply (drule choose_pos_lessD) 

662 
apply (rule finite_rank_eq) 

663 
apply (simp add: rank_eq_def) 

664 
apply (simp add: rank_eq_def) 

665 
apply simp 

666 
apply (drule place_rank_mono, simp) 

667 
done 

668 

669 
lemma basis_emb_mono: 

670 
"x \<sqsubseteq> y \<Longrightarrow> ubasis_le (basis_emb x) (basis_emb y)" 

34915  671 
proof (induct "max (place x) (place y)" arbitrary: x y rule: less_induct) 
672 
case less 

30505  673 
show ?case proof (rule linorder_cases) 
674 
assume "place x < place y" 

675 
then have "rank x < rank y" 

676 
using `x \<sqsubseteq> y` by (rule rank_place_mono) 

677 
with `place x < place y` show ?case 

678 
apply (case_tac "y = compact_bot", simp) 

679 
apply (simp add: basis_emb.simps [of y]) 

680 
apply (rule ubasis_le_trans [OF _ ubasis_le_lower [OF fin2]]) 

34915  681 
apply (rule less) 
30505  682 
apply (simp add: less_max_iff_disj) 
683 
apply (erule place_sub_less) 

684 
apply (erule rank_less_imp_below_sub [OF `x \<sqsubseteq> y`]) 

27411  685 
done 
30505  686 
next 
687 
assume "place x = place y" 

688 
hence "x = y" by (rule place_eqD) 

689 
thus ?case by (simp add: ubasis_le_refl) 

690 
next 

691 
assume "place x > place y" 

692 
with `x \<sqsubseteq> y` show ?case 

693 
apply (case_tac "x = compact_bot", simp add: ubasis_le_minimal) 

694 
apply (simp add: basis_emb.simps [of x]) 

695 
apply (rule ubasis_le_upper [OF fin2], simp) 

34915  696 
apply (rule less) 
30505  697 
apply (simp add: less_max_iff_disj) 
698 
apply (erule place_sub_less) 

31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
30729
diff
changeset

699 
apply (erule rev_below_trans) 
30505  700 
apply (rule sub_below) 
701 
done 

27411  702 
qed 
703 
qed 

704 

705 
lemma inj_basis_emb: "inj basis_emb" 

706 
apply (rule inj_onI) 

707 
apply (case_tac "x = compact_bot") 

708 
apply (case_tac [!] "y = compact_bot") 

709 
apply simp 

710 
apply (simp add: basis_emb.simps) 

711 
apply (simp add: basis_emb.simps) 

712 
apply (simp add: basis_emb.simps) 

30505  713 
apply (simp add: fin2 inj_eq [OF inj_place]) 
27411  714 
done 
715 

716 
definition 

30505  717 
basis_prj :: "ubasis \<Rightarrow> 'a compact_basis" 
27411  718 
where 
719 
"basis_prj x = inv basis_emb 

30505  720 
(ubasis_until (\<lambda>x. x \<in> range (basis_emb :: 'a compact_basis \<Rightarrow> ubasis)) x)" 
27411  721 

722 
lemma basis_prj_basis_emb: "\<And>x. basis_prj (basis_emb x) = x" 

723 
unfolding basis_prj_def 

724 
apply (subst ubasis_until_same) 

725 
apply (rule rangeI) 

726 
apply (rule inv_f_f) 

727 
apply (rule inj_basis_emb) 

728 
done 

729 

730 
lemma basis_prj_node: 

30505  731 
"\<lbrakk>finite S; node i a S \<notin> range (basis_emb :: 'a compact_basis \<Rightarrow> nat)\<rbrakk> 
732 
\<Longrightarrow> basis_prj (node i a S) = (basis_prj a :: 'a compact_basis)" 

27411  733 
unfolding basis_prj_def by simp 
734 

735 
lemma basis_prj_0: "basis_prj 0 = compact_bot" 

736 
apply (subst basis_emb_compact_bot [symmetric]) 

737 
apply (rule basis_prj_basis_emb) 

738 
done 

739 

30505  740 
lemma node_eq_basis_emb_iff: 
741 
"finite S \<Longrightarrow> node i a S = basis_emb x \<longleftrightarrow> 

742 
x \<noteq> compact_bot \<and> i = place x \<and> a = basis_emb (sub x) \<and> 

743 
S = basis_emb ` {y. place y < place x \<and> x \<sqsubseteq> y}" 

744 
apply (cases "x = compact_bot", simp) 

745 
apply (simp add: basis_emb.simps [of x]) 

746 
apply (simp add: fin2) 

27411  747 
done 
748 

30505  749 
lemma basis_prj_mono: "ubasis_le a b \<Longrightarrow> basis_prj a \<sqsubseteq> basis_prj b" 
750 
proof (induct a b rule: ubasis_le.induct) 

31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
30729
diff
changeset

751 
case (ubasis_le_refl a) show ?case by (rule below_refl) 
30505  752 
next 
31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
30729
diff
changeset

753 
case (ubasis_le_trans a b c) thus ?case by  (rule below_trans) 
30505  754 
next 
755 
case (ubasis_le_lower S a i) thus ?case 

30561  756 
apply (cases "node i a S \<in> range (basis_emb :: 'a compact_basis \<Rightarrow> nat)") 
30505  757 
apply (erule rangeE, rename_tac x) 
758 
apply (simp add: basis_prj_basis_emb) 

759 
apply (simp add: node_eq_basis_emb_iff) 

760 
apply (simp add: basis_prj_basis_emb) 

761 
apply (rule sub_below) 

762 
apply (simp add: basis_prj_node) 

763 
done 

764 
next 

765 
case (ubasis_le_upper S b a i) thus ?case 

30561  766 
apply (cases "node i a S \<in> range (basis_emb :: 'a compact_basis \<Rightarrow> nat)") 
30505  767 
apply (erule rangeE, rename_tac x) 
768 
apply (simp add: basis_prj_basis_emb) 

769 
apply (clarsimp simp add: node_eq_basis_emb_iff) 

770 
apply (simp add: basis_prj_basis_emb) 

771 
apply (simp add: basis_prj_node) 

772 
done 

773 
qed 

774 

27411  775 
lemma basis_emb_prj_less: "ubasis_le (basis_emb (basis_prj x)) x" 
776 
unfolding basis_prj_def 

33071
362f59fe5092
renamed f_inv_onto_f to f_inv_into_f (cf. 764547b68538);
wenzelm
parents:
32997
diff
changeset

777 
apply (subst f_inv_into_f [where f=basis_emb]) 
27411  778 
apply (rule ubasis_until) 
779 
apply (rule range_eqI [where x=compact_bot]) 

780 
apply simp 

781 
apply (rule ubasis_until_less) 

782 
done 

783 

41286
3d7685a4a5ff
reintroduce 'bifinite' class, now with existentiallyquantified approx function (cf. b525988432e9)
huffman
parents:
41182
diff
changeset

784 
lemma ideal_completion: 
3d7685a4a5ff
reintroduce 'bifinite' class, now with existentiallyquantified approx function (cf. b525988432e9)
huffman
parents:
41182
diff
changeset

785 
"ideal_completion below Rep_compact_basis (approximants :: 'a \<Rightarrow> _)" 
39974
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

786 
proof 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

787 
fix w :: "'a" 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

788 
show "below.ideal (approximants w)" 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

789 
proof (rule below.idealI) 
41370
17b09240893c
declare more simp rules, rewrite proofs in Isarstyle
huffman
parents:
41295
diff
changeset

790 
have "Abs_compact_basis (approx 0\<cdot>w) \<in> approximants w" 
17b09240893c
declare more simp rules, rewrite proofs in Isarstyle
huffman
parents:
41295
diff
changeset

791 
by (simp add: approximants_def approx_below) 
17b09240893c
declare more simp rules, rewrite proofs in Isarstyle
huffman
parents:
41295
diff
changeset

792 
thus "\<exists>x. x \<in> approximants w" .. 
39974
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

793 
next 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

794 
fix x y :: "'a compact_basis" 
41370
17b09240893c
declare more simp rules, rewrite proofs in Isarstyle
huffman
parents:
41295
diff
changeset

795 
assume x: "x \<in> approximants w" and y: "y \<in> approximants w" 
17b09240893c
declare more simp rules, rewrite proofs in Isarstyle
huffman
parents:
41295
diff
changeset

796 
obtain i where i: "approx i\<cdot>(Rep_compact_basis x) = Rep_compact_basis x" 
17b09240893c
declare more simp rules, rewrite proofs in Isarstyle
huffman
parents:
41295
diff
changeset

797 
using compact_eq_approx Rep_compact_basis' by fast 
17b09240893c
declare more simp rules, rewrite proofs in Isarstyle
huffman
parents:
41295
diff
changeset

798 
obtain j where j: "approx j\<cdot>(Rep_compact_basis y) = Rep_compact_basis y" 
17b09240893c
declare more simp rules, rewrite proofs in Isarstyle
huffman
parents:
41295
diff
changeset

799 
using compact_eq_approx Rep_compact_basis' by fast 
17b09240893c
declare more simp rules, rewrite proofs in Isarstyle
huffman
parents:
41295
diff
changeset

800 
let ?z = "Abs_compact_basis (approx (max i j)\<cdot>w)" 
17b09240893c
declare more simp rules, rewrite proofs in Isarstyle
huffman
parents:
41295
diff
changeset

801 
have "?z \<in> approximants w" 
17b09240893c
declare more simp rules, rewrite proofs in Isarstyle
huffman
parents:
41295
diff
changeset

802 
by (simp add: approximants_def approx_below) 
17b09240893c
declare more simp rules, rewrite proofs in Isarstyle
huffman
parents:
41295
diff
changeset

803 
moreover from x y have "x \<sqsubseteq> ?z \<and> y \<sqsubseteq> ?z" 
17b09240893c
declare more simp rules, rewrite proofs in Isarstyle
huffman
parents:
41295
diff
changeset

804 
by (simp add: approximants_def compact_le_def) 
17b09240893c
declare more simp rules, rewrite proofs in Isarstyle
huffman
parents:
41295
diff
changeset

805 
(metis i j monofun_cfun chain_mono chain_approx le_maxI1 le_maxI2) 
17b09240893c
declare more simp rules, rewrite proofs in Isarstyle
huffman
parents:
41295
diff
changeset

806 
ultimately show "\<exists>z \<in> approximants w. x \<sqsubseteq> z \<and> y \<sqsubseteq> z" .. 
39974
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

807 
next 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

808 
fix x y :: "'a compact_basis" 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

809 
assume "x \<sqsubseteq> y" "y \<in> approximants w" thus "x \<in> approximants w" 
41370
17b09240893c
declare more simp rules, rewrite proofs in Isarstyle
huffman
parents:
41295
diff
changeset

810 
unfolding approximants_def compact_le_def 
17b09240893c
declare more simp rules, rewrite proofs in Isarstyle
huffman
parents:
41295
diff
changeset

811 
by (auto elim: below_trans) 
39974
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

812 
qed 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

813 
next 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

814 
fix Y :: "nat \<Rightarrow> 'a" 
41370
17b09240893c
declare more simp rules, rewrite proofs in Isarstyle
huffman
parents:
41295
diff
changeset

815 
assume "chain Y" 
17b09240893c
declare more simp rules, rewrite proofs in Isarstyle
huffman
parents:
41295
diff
changeset

816 
thus "approximants (\<Squnion>i. Y i) = (\<Union>i. approximants (Y i))" 
39974
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

817 
unfolding approximants_def 
41370
17b09240893c
declare more simp rules, rewrite proofs in Isarstyle
huffman
parents:
41295
diff
changeset

818 
by (auto simp add: compact_below_lub_iff) 
39974
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

819 
next 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

820 
fix a :: "'a compact_basis" 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

821 
show "approximants (Rep_compact_basis a) = {b. b \<sqsubseteq> a}" 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

822 
unfolding approximants_def compact_le_def .. 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

823 
next 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

824 
fix x y :: "'a" 
41370
17b09240893c
declare more simp rules, rewrite proofs in Isarstyle
huffman
parents:
41295
diff
changeset

825 
assume "approximants x \<subseteq> approximants y" 
17b09240893c
declare more simp rules, rewrite proofs in Isarstyle
huffman
parents:
41295
diff
changeset

826 
hence "\<forall>z. compact z \<longrightarrow> z \<sqsubseteq> x \<longrightarrow> z \<sqsubseteq> y" 
17b09240893c
declare more simp rules, rewrite proofs in Isarstyle
huffman
parents:
41295
diff
changeset

827 
by (simp add: approximants_def subset_eq) 
17b09240893c
declare more simp rules, rewrite proofs in Isarstyle
huffman
parents:
41295
diff
changeset

828 
(metis Abs_compact_basis_inverse') 
17b09240893c
declare more simp rules, rewrite proofs in Isarstyle
huffman
parents:
41295
diff
changeset

829 
hence "(\<Squnion>i. approx i\<cdot>x) \<sqsubseteq> y" 
17b09240893c
declare more simp rules, rewrite proofs in Isarstyle
huffman
parents:
41295
diff
changeset

830 
by (simp add: lub_below approx_below) 
17b09240893c
declare more simp rules, rewrite proofs in Isarstyle
huffman
parents:
41295
diff
changeset

831 
thus "x \<sqsubseteq> y" 
17b09240893c
declare more simp rules, rewrite proofs in Isarstyle
huffman
parents:
41295
diff
changeset

832 
by (simp add: lub_distribs) 
39974
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

833 
next 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

834 
show "\<exists>f::'a compact_basis \<Rightarrow> nat. inj f" 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

835 
by (rule exI, rule inj_place) 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

836 
qed 
27411  837 

41286
3d7685a4a5ff
reintroduce 'bifinite' class, now with existentiallyquantified approx function (cf. b525988432e9)
huffman
parents:
41182
diff
changeset

838 
end 
3d7685a4a5ff
reintroduce 'bifinite' class, now with existentiallyquantified approx function (cf. b525988432e9)
huffman
parents:
41182
diff
changeset

839 

3d7685a4a5ff
reintroduce 'bifinite' class, now with existentiallyquantified approx function (cf. b525988432e9)
huffman
parents:
41182
diff
changeset

840 
interpretation compact_basis!: 
3d7685a4a5ff
reintroduce 'bifinite' class, now with existentiallyquantified approx function (cf. b525988432e9)
huffman
parents:
41182
diff
changeset

841 
ideal_completion below Rep_compact_basis 
3d7685a4a5ff
reintroduce 'bifinite' class, now with existentiallyquantified approx function (cf. b525988432e9)
huffman
parents:
41182
diff
changeset

842 
"approximants :: 'a::bifinite \<Rightarrow> 'a compact_basis set" 
3d7685a4a5ff
reintroduce 'bifinite' class, now with existentiallyquantified approx function (cf. b525988432e9)
huffman
parents:
41182
diff
changeset

843 
proof  
3d7685a4a5ff
reintroduce 'bifinite' class, now with existentiallyquantified approx function (cf. b525988432e9)
huffman
parents:
41182
diff
changeset

844 
obtain a :: "nat \<Rightarrow> 'a \<rightarrow> 'a" where "approx_chain a" 
3d7685a4a5ff
reintroduce 'bifinite' class, now with existentiallyquantified approx function (cf. b525988432e9)
huffman
parents:
41182
diff
changeset

845 
using bifinite .. 
3d7685a4a5ff
reintroduce 'bifinite' class, now with existentiallyquantified approx function (cf. b525988432e9)
huffman
parents:
41182
diff
changeset

846 
hence "bifinite_approx_chain a" 
3d7685a4a5ff
reintroduce 'bifinite' class, now with existentiallyquantified approx function (cf. b525988432e9)
huffman
parents:
41182
diff
changeset

847 
unfolding bifinite_approx_chain_def . 
3d7685a4a5ff
reintroduce 'bifinite' class, now with existentiallyquantified approx function (cf. b525988432e9)
huffman
parents:
41182
diff
changeset

848 
thus "ideal_completion below Rep_compact_basis (approximants :: 'a \<Rightarrow> _)" 
3d7685a4a5ff
reintroduce 'bifinite' class, now with existentiallyquantified approx function (cf. b525988432e9)
huffman
parents:
41182
diff
changeset

849 
by (rule bifinite_approx_chain.ideal_completion) 
3d7685a4a5ff
reintroduce 'bifinite' class, now with existentiallyquantified approx function (cf. b525988432e9)
huffman
parents:
41182
diff
changeset

850 
qed 
3d7685a4a5ff
reintroduce 'bifinite' class, now with existentiallyquantified approx function (cf. b525988432e9)
huffman
parents:
41182
diff
changeset

851 

35900
aa5dfb03eb1e
remove LaTeX hyperref warnings by avoiding antiquotations within section headings
huffman
parents:
35794
diff
changeset

852 
subsubsection {* EPpair from any bifinite domain into \emph{udom} *} 
27411  853 

41286
3d7685a4a5ff
reintroduce 'bifinite' class, now with existentiallyquantified approx function (cf. b525988432e9)
huffman
parents:
41182
diff
changeset

854 
context bifinite_approx_chain begin 
39974
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

855 

27411  856 
definition 
39974
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

857 
udom_emb :: "'a \<rightarrow> udom" 
27411  858 
where 
41394
51c866d1b53b
rename function ideal_completion.basis_fun to ideal_completion.extension
huffman
parents:
41370
diff
changeset

859 
"udom_emb = compact_basis.extension (\<lambda>x. udom_principal (basis_emb x))" 
27411  860 

861 
definition 

39974
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

862 
udom_prj :: "udom \<rightarrow> 'a" 
27411  863 
where 
41394
51c866d1b53b
rename function ideal_completion.basis_fun to ideal_completion.extension
huffman
parents:
41370
diff
changeset

864 
"udom_prj = udom.extension (\<lambda>x. Rep_compact_basis (basis_prj x))" 
27411  865 

866 
lemma udom_emb_principal: 

867 
"udom_emb\<cdot>(Rep_compact_basis x) = udom_principal (basis_emb x)" 

868 
unfolding udom_emb_def 

41394
51c866d1b53b
rename function ideal_completion.basis_fun to ideal_completion.extension
huffman
parents:
41370
diff
changeset

869 
apply (rule compact_basis.extension_principal) 
27411  870 
apply (rule udom.principal_mono) 
871 
apply (erule basis_emb_mono) 

872 
done 

873 

874 
lemma udom_prj_principal: 

875 
"udom_prj\<cdot>(udom_principal x) = Rep_compact_basis (basis_prj x)" 

876 
unfolding udom_prj_def 

41394
51c866d1b53b
rename function ideal_completion.basis_fun to ideal_completion.extension
huffman
parents:
41370
diff
changeset

877 
apply (rule udom.extension_principal) 
27411  878 
apply (rule compact_basis.principal_mono) 
879 
apply (erule basis_prj_mono) 

880 
done 

881 

882 
lemma ep_pair_udom: "ep_pair udom_emb udom_prj" 

883 
apply default 

884 
apply (rule compact_basis.principal_induct, simp) 

885 
apply (simp add: udom_emb_principal udom_prj_principal) 

886 
apply (simp add: basis_prj_basis_emb) 

887 
apply (rule udom.principal_induct, simp) 

888 
apply (simp add: udom_emb_principal udom_prj_principal) 

889 
apply (rule basis_emb_prj_less) 

890 
done 

891 

892 
end 

39974
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

893 

41286
3d7685a4a5ff
reintroduce 'bifinite' class, now with existentiallyquantified approx function (cf. b525988432e9)
huffman
parents:
41182
diff
changeset

894 
abbreviation "udom_emb \<equiv> bifinite_approx_chain.udom_emb" 
3d7685a4a5ff
reintroduce 'bifinite' class, now with existentiallyquantified approx function (cf. b525988432e9)
huffman
parents:
41182
diff
changeset

895 
abbreviation "udom_prj \<equiv> bifinite_approx_chain.udom_prj" 
39974
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

896 

41286
3d7685a4a5ff
reintroduce 'bifinite' class, now with existentiallyquantified approx function (cf. b525988432e9)
huffman
parents:
41182
diff
changeset

897 
lemmas ep_pair_udom = 
3d7685a4a5ff
reintroduce 'bifinite' class, now with existentiallyquantified approx function (cf. b525988432e9)
huffman
parents:
41182
diff
changeset

898 
bifinite_approx_chain.ep_pair_udom [unfolded bifinite_approx_chain_def] 
39974
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

899 

b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

900 
subsection {* Chain of approx functions for type \emph{udom} *} 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

901 

b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

902 
definition 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

903 
udom_approx :: "nat \<Rightarrow> udom \<rightarrow> udom" 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

904 
where 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

905 
"udom_approx i = 
41394
51c866d1b53b
rename function ideal_completion.basis_fun to ideal_completion.extension
huffman
parents:
41370
diff
changeset

906 
udom.extension (\<lambda>x. udom_principal (ubasis_until (\<lambda>y. y \<le> i) x))" 
39974
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

907 

b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

908 
lemma udom_approx_mono: 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

909 
"ubasis_le a b \<Longrightarrow> 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

910 
udom_principal (ubasis_until (\<lambda>y. y \<le> i) a) \<sqsubseteq> 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

911 
udom_principal (ubasis_until (\<lambda>y. y \<le> i) b)" 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

912 
apply (rule udom.principal_mono) 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

913 
apply (rule ubasis_until_mono) 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

914 
apply (frule (2) order_less_le_trans [OF node_gt2]) 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

915 
apply (erule order_less_imp_le) 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

916 
apply assumption 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

917 
done 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

918 

b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

919 
lemma adm_mem_finite: "\<lbrakk>cont f; finite S\<rbrakk> \<Longrightarrow> adm (\<lambda>x. f x \<in> S)" 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

920 
by (erule adm_subst, induct set: finite, simp_all) 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

921 

b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

922 
lemma udom_approx_principal: 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

923 
"udom_approx i\<cdot>(udom_principal x) = 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

924 
udom_principal (ubasis_until (\<lambda>y. y \<le> i) x)" 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

925 
unfolding udom_approx_def 
41394
51c866d1b53b
rename function ideal_completion.basis_fun to ideal_completion.extension
huffman
parents:
41370
diff
changeset

926 
apply (rule udom.extension_principal) 
39974
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

927 
apply (erule udom_approx_mono) 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

928 
done 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

929 

b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

930 
lemma finite_deflation_udom_approx: "finite_deflation (udom_approx i)" 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

931 
proof 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

932 
fix x show "udom_approx i\<cdot>(udom_approx i\<cdot>x) = udom_approx i\<cdot>x" 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

933 
by (induct x rule: udom.principal_induct, simp) 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

934 
(simp add: udom_approx_principal ubasis_until_idem) 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

935 
next 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

936 
fix x show "udom_approx i\<cdot>x \<sqsubseteq> x" 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

937 
by (induct x rule: udom.principal_induct, simp) 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

938 
(simp add: udom_approx_principal ubasis_until_less) 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

939 
next 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

940 
have *: "finite (range (\<lambda>x. udom_principal (ubasis_until (\<lambda>y. y \<le> i) x)))" 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

941 
apply (subst range_composition [where f=udom_principal]) 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

942 
apply (simp add: finite_range_ubasis_until) 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

943 
done 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

944 
show "finite {x. udom_approx i\<cdot>x = x}" 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

945 
apply (rule finite_range_imp_finite_fixes) 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

946 
apply (rule rev_finite_subset [OF *]) 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

947 
apply (clarsimp, rename_tac x) 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

948 
apply (induct_tac x rule: udom.principal_induct) 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

949 
apply (simp add: adm_mem_finite *) 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

950 
apply (simp add: udom_approx_principal) 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

951 
done 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

952 
qed 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

953 

b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

954 
interpretation udom_approx: finite_deflation "udom_approx i" 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

955 
by (rule finite_deflation_udom_approx) 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

956 

b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

957 
lemma chain_udom_approx [simp]: "chain (\<lambda>i. udom_approx i)" 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

958 
unfolding udom_approx_def 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

959 
apply (rule chainI) 
41394
51c866d1b53b
rename function ideal_completion.basis_fun to ideal_completion.extension
huffman
parents:
41370
diff
changeset

960 
apply (rule udom.extension_mono) 
39974
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

961 
apply (erule udom_approx_mono) 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

962 
apply (erule udom_approx_mono) 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

963 
apply (rule udom.principal_mono) 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

964 
apply (rule ubasis_until_chain, simp) 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

965 
done 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

966 

b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

967 
lemma lub_udom_approx [simp]: "(\<Squnion>i. udom_approx i) = ID" 
40002
c5b5f7a3a3b1
new theorem names: fun_below_iff, fun_belowI, cfun_eq_iff, cfun_eqI, cfun_below_iff, cfun_belowI
huffman
parents:
39984
diff
changeset

968 
apply (rule cfun_eqI, simp add: contlub_cfun_fun) 
39974
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

969 
apply (rule below_antisym) 
40500
ee9c8d36318e
add lemmas lub_below, below_lub; simplify some proofs; remove some unused lemmas
huffman
parents:
40002
diff
changeset

970 
apply (rule lub_below) 
39974
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

971 
apply (simp) 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

972 
apply (rule udom_approx.below) 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

973 
apply (rule_tac x=x in udom.principal_induct) 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

974 
apply (simp add: lub_distribs) 
40500
ee9c8d36318e
add lemmas lub_below, below_lub; simplify some proofs; remove some unused lemmas
huffman
parents:
40002
diff
changeset

975 
apply (rule_tac i=a in below_lub) 
39974
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

976 
apply simp 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

977 
apply (simp add: udom_approx_principal) 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

978 
apply (simp add: ubasis_until_same ubasis_le_refl) 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

979 
done 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

980 

41286
3d7685a4a5ff
reintroduce 'bifinite' class, now with existentiallyquantified approx function (cf. b525988432e9)
huffman
parents:
41182
diff
changeset

981 
lemma udom_approx [simp]: "approx_chain udom_approx" 
39974
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

982 
proof 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

983 
show "chain (\<lambda>i. udom_approx i)" 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

984 
by (rule chain_udom_approx) 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

985 
show "(\<Squnion>i. udom_approx i) = ID" 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

986 
by (rule lub_udom_approx) 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

987 
qed 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

988 

41286
3d7685a4a5ff
reintroduce 'bifinite' class, now with existentiallyquantified approx function (cf. b525988432e9)
huffman
parents:
41182
diff
changeset

989 
instance udom :: bifinite 
3d7685a4a5ff
reintroduce 'bifinite' class, now with existentiallyquantified approx function (cf. b525988432e9)
huffman
parents:
41182
diff
changeset

990 
by default (fast intro: udom_approx) 
3d7685a4a5ff
reintroduce 'bifinite' class, now with existentiallyquantified approx function (cf. b525988432e9)
huffman
parents:
41182
diff
changeset

991 

39974
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

992 
hide_const (open) node 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

993 

b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
36452
diff
changeset

994 
end 