author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 42151  4da4fc77664b 
child 54863  82acc20ded73 
permissions  rwrr 
42151  1 
(* Title: HOL/HOLCF/Completion.thy 
27404  2 
Author: Brian Huffman 
3 
*) 

4 

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

5 
header {* Defining algebraic domains by ideal completion *} 
27404  6 

7 
theory Completion 

40502
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
40500
diff
changeset

8 
imports Plain_HOLCF 
27404  9 
begin 
10 

11 
subsection {* Ideals over a preorder *} 

12 

13 
locale preorder = 

14 
fixes r :: "'a::type \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<preceq>" 50) 

15 
assumes r_refl: "x \<preceq> x" 

16 
assumes r_trans: "\<lbrakk>x \<preceq> y; y \<preceq> z\<rbrakk> \<Longrightarrow> x \<preceq> z" 

17 
begin 

18 

19 
definition 

20 
ideal :: "'a set \<Rightarrow> bool" where 

21 
"ideal A = ((\<exists>x. x \<in> A) \<and> (\<forall>x\<in>A. \<forall>y\<in>A. \<exists>z\<in>A. x \<preceq> z \<and> y \<preceq> z) \<and> 

22 
(\<forall>x y. x \<preceq> y \<longrightarrow> y \<in> A \<longrightarrow> x \<in> A))" 

23 

24 
lemma idealI: 

25 
assumes "\<exists>x. x \<in> A" 

26 
assumes "\<And>x y. \<lbrakk>x \<in> A; y \<in> A\<rbrakk> \<Longrightarrow> \<exists>z\<in>A. x \<preceq> z \<and> y \<preceq> z" 

27 
assumes "\<And>x y. \<lbrakk>x \<preceq> y; y \<in> A\<rbrakk> \<Longrightarrow> x \<in> A" 

28 
shows "ideal A" 

41529  29 
unfolding ideal_def using assms by fast 
27404  30 

31 
lemma idealD1: 

32 
"ideal A \<Longrightarrow> \<exists>x. x \<in> A" 

33 
unfolding ideal_def by fast 

34 

35 
lemma idealD2: 

36 
"\<lbrakk>ideal A; x \<in> A; y \<in> A\<rbrakk> \<Longrightarrow> \<exists>z\<in>A. x \<preceq> z \<and> y \<preceq> z" 

37 
unfolding ideal_def by fast 

38 

39 
lemma idealD3: 

40 
"\<lbrakk>ideal A; x \<preceq> y; y \<in> A\<rbrakk> \<Longrightarrow> x \<in> A" 

41 
unfolding ideal_def by fast 

42 

43 
lemma ideal_principal: "ideal {x. x \<preceq> z}" 

44 
apply (rule idealI) 

45 
apply (rule_tac x=z in exI) 

46 
apply (fast intro: r_refl) 

47 
apply (rule_tac x=z in bexI, fast) 

48 
apply (fast intro: r_refl) 

49 
apply (fast intro: r_trans) 

50 
done 

51 

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

52 
lemma ex_ideal: "\<exists>A. A \<in> {A. ideal A}" 
28cd51cff70c
reformulate lemma preorder.ex_ideal, and use it for typedefs
huffman
parents:
40774
diff
changeset

53 
by (fast intro: ideal_principal) 
27404  54 

55 
text {* The set of ideals is a cpo *} 

56 

57 
lemma ideal_UN: 

58 
fixes A :: "nat \<Rightarrow> 'a set" 

59 
assumes ideal_A: "\<And>i. ideal (A i)" 

60 
assumes chain_A: "\<And>i j. i \<le> j \<Longrightarrow> A i \<subseteq> A j" 

61 
shows "ideal (\<Union>i. A i)" 

62 
apply (rule idealI) 

63 
apply (cut_tac idealD1 [OF ideal_A], fast) 

64 
apply (clarify, rename_tac i j) 

65 
apply (drule subsetD [OF chain_A [OF le_maxI1]]) 

66 
apply (drule subsetD [OF chain_A [OF le_maxI2]]) 

67 
apply (drule (1) idealD2 [OF ideal_A]) 

68 
apply blast 

69 
apply clarify 

70 
apply (drule (1) idealD3 [OF ideal_A]) 

71 
apply fast 

72 
done 

73 

74 
lemma typedef_ideal_po: 

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

75 
fixes Abs :: "'a set \<Rightarrow> 'b::below" 
27404  76 
assumes type: "type_definition Rep Abs {S. ideal S}" 
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

77 
assumes below: "\<And>x y. x \<sqsubseteq> y \<longleftrightarrow> Rep x \<subseteq> Rep y" 
27404  78 
shows "OFCLASS('b, po_class)" 
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

79 
apply (intro_classes, unfold below) 
27404  80 
apply (rule subset_refl) 
81 
apply (erule (1) subset_trans) 

82 
apply (rule type_definition.Rep_inject [OF type, THEN iffD1]) 

83 
apply (erule (1) subset_antisym) 

84 
done 

85 

86 
lemma 

87 
fixes Abs :: "'a set \<Rightarrow> 'b::po" 

88 
assumes type: "type_definition Rep Abs {S. ideal S}" 

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

89 
assumes below: "\<And>x y. x \<sqsubseteq> y \<longleftrightarrow> Rep x \<subseteq> Rep y" 
27404  90 
assumes S: "chain S" 
91 
shows typedef_ideal_lub: "range S << Abs (\<Union>i. Rep (S i))" 

40769  92 
and typedef_ideal_rep_lub: "Rep (\<Squnion>i. S i) = (\<Union>i. Rep (S i))" 
27404  93 
proof  
94 
have 1: "ideal (\<Union>i. Rep (S i))" 

95 
apply (rule ideal_UN) 

96 
apply (rule type_definition.Rep [OF type, unfolded mem_Collect_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

97 
apply (subst below [symmetric]) 
27404  98 
apply (erule chain_mono [OF S]) 
99 
done 

100 
hence 2: "Rep (Abs (\<Union>i. Rep (S i))) = (\<Union>i. Rep (S i))" 

101 
by (simp add: type_definition.Abs_inverse [OF type]) 

102 
show 3: "range S << Abs (\<Union>i. Rep (S i))" 

103 
apply (rule is_lubI) 

104 
apply (rule is_ubI) 

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

105 
apply (simp add: below 2, fast) 
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
30729
diff
changeset

106 
apply (simp add: below 2 is_ub_def, fast) 
27404  107 
done 
108 
hence 4: "(\<Squnion>i. S i) = Abs (\<Union>i. Rep (S i))" 

40771  109 
by (rule lub_eqI) 
27404  110 
show 5: "Rep (\<Squnion>i. S i) = (\<Union>i. Rep (S i))" 
111 
by (simp add: 4 2) 

112 
qed 

113 

114 
lemma typedef_ideal_cpo: 

115 
fixes Abs :: "'a set \<Rightarrow> 'b::po" 

116 
assumes type: "type_definition Rep Abs {S. ideal S}" 

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

117 
assumes below: "\<And>x y. x \<sqsubseteq> y \<longleftrightarrow> Rep x \<subseteq> Rep y" 
27404  118 
shows "OFCLASS('b, cpo_class)" 
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

119 
by (default, rule exI, erule typedef_ideal_lub [OF type below]) 
27404  120 

121 
end 

122 

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

123 
interpretation below: preorder "below :: 'a::po \<Rightarrow> 'a \<Rightarrow> bool" 
27404  124 
apply unfold_locales 
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

125 
apply (rule below_refl) 
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
30729
diff
changeset

126 
apply (erule (1) below_trans) 
27404  127 
done 
128 

28133  129 
subsection {* Lemmas about least upper bounds *} 
27404  130 

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

131 
lemma is_ub_thelub_ex: "\<lbrakk>\<exists>u. S << u; x \<in> S\<rbrakk> \<Longrightarrow> x \<sqsubseteq> lub S" 
40771  132 
apply (erule exE, drule is_lub_lub) 
27404  133 
apply (drule is_lubD1) 
134 
apply (erule (1) is_ubD) 

135 
done 

136 

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

137 
lemma is_lub_thelub_ex: "\<lbrakk>\<exists>u. S << u; S < x\<rbrakk> \<Longrightarrow> lub S \<sqsubseteq> x" 
40771  138 
by (erule exE, drule is_lub_lub, erule is_lubD2) 
27404  139 

28133  140 
subsection {* Locale for ideal completion *} 
141 

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

142 
locale ideal_completion = preorder + 
27404  143 
fixes principal :: "'a::type \<Rightarrow> 'b::cpo" 
144 
fixes rep :: "'b::cpo \<Rightarrow> 'a::type set" 

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

145 
assumes ideal_rep: "\<And>x. ideal (rep x)" 
40769  146 
assumes rep_lub: "\<And>Y. chain Y \<Longrightarrow> rep (\<Squnion>i. Y i) = (\<Union>i. rep (Y i))" 
27404  147 
assumes rep_principal: "\<And>a. rep (principal a) = {b. b \<preceq> a}" 
41033  148 
assumes belowI: "\<And>x y. rep x \<subseteq> rep y \<Longrightarrow> x \<sqsubseteq> y" 
39974
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

149 
assumes countable: "\<exists>f::'a \<Rightarrow> nat. inj f" 
27404  150 
begin 
151 

28133  152 
lemma rep_mono: "x \<sqsubseteq> y \<Longrightarrow> rep x \<subseteq> rep y" 
153 
apply (frule bin_chain) 

40769  154 
apply (drule rep_lub) 
40771  155 
apply (simp only: lub_eqI [OF is_lub_bin_chain]) 
28133  156 
apply (rule subsetI, rule UN_I [where a=0], simp_all) 
157 
done 

158 

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

159 
lemma below_def: "x \<sqsubseteq> y \<longleftrightarrow> rep x \<subseteq> rep y" 
41033  160 
by (rule iffI [OF rep_mono belowI]) 
28133  161 

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

162 
lemma principal_below_iff_mem_rep: "principal a \<sqsubseteq> x \<longleftrightarrow> a \<in> rep x" 
41033  163 
unfolding below_def rep_principal 
164 
by (auto intro: r_refl elim: idealD3 [OF ideal_rep]) 

28133  165 

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

166 
lemma principal_below_iff [simp]: "principal a \<sqsubseteq> principal b \<longleftrightarrow> a \<preceq> b" 
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
30729
diff
changeset

167 
by (simp add: principal_below_iff_mem_rep rep_principal) 
28133  168 

169 
lemma principal_eq_iff: "principal a = principal b \<longleftrightarrow> a \<preceq> b \<and> b \<preceq> a" 

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

170 
unfolding po_eq_conv [where 'a='b] principal_below_iff .. 
28133  171 

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

172 
lemma eq_iff: "x = y \<longleftrightarrow> rep x = rep y" 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

173 
unfolding po_eq_conv below_def by auto 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

174 

28133  175 
lemma principal_mono: "a \<preceq> b \<Longrightarrow> principal a \<sqsubseteq> principal b" 
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

176 
by (simp only: principal_below_iff) 
28133  177 

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

178 
lemma ch2ch_principal [simp]: 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

179 
"\<forall>i. Y i \<preceq> Y (Suc i) \<Longrightarrow> chain (\<lambda>i. principal (Y i))" 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

180 
by (simp add: chainI principal_mono) 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

181 

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

182 
subsubsection {* Principal ideals approximate all elements *} 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

183 

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

184 
lemma compact_principal [simp]: "compact (principal a)" 
40769  185 
by (rule compactI2, simp add: principal_below_iff_mem_rep rep_lub) 
39974
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

186 

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

187 
text {* Construct a chain whose lub is the same as a given ideal *} 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

188 

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

189 
lemma obtain_principal_chain: 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

190 
obtains Y where "\<forall>i. Y i \<preceq> Y (Suc i)" and "x = (\<Squnion>i. principal (Y i))" 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

191 
proof  
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

192 
obtain count :: "'a \<Rightarrow> nat" where inj: "inj count" 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

193 
using countable .. 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

194 
def enum \<equiv> "\<lambda>i. THE a. count a = i" 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

195 
have enum_count [simp]: "\<And>x. enum (count x) = x" 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

196 
unfolding enum_def by (simp add: inj_eq [OF inj]) 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

197 
def a \<equiv> "LEAST i. enum i \<in> rep x" 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

198 
def b \<equiv> "\<lambda>i. LEAST j. enum j \<in> rep x \<and> \<not> enum j \<preceq> enum i" 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

199 
def c \<equiv> "\<lambda>i j. LEAST k. enum k \<in> rep x \<and> enum i \<preceq> enum k \<and> enum j \<preceq> enum k" 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

200 
def P \<equiv> "\<lambda>i. \<exists>j. enum j \<in> rep x \<and> \<not> enum j \<preceq> enum i" 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

201 
def X \<equiv> "nat_rec a (\<lambda>n i. if P i then c i (b i) else i)" 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

202 
have X_0: "X 0 = a" unfolding X_def by simp 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

203 
have X_Suc: "\<And>n. X (Suc n) = (if P (X n) then c (X n) (b (X n)) else X n)" 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

204 
unfolding X_def by simp 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

205 
have a_mem: "enum a \<in> rep x" 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

206 
unfolding a_def 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

207 
apply (rule LeastI_ex) 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

208 
apply (cut_tac ideal_rep [of x]) 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

209 
apply (drule idealD1) 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

210 
apply (clarify, rename_tac a) 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

211 
apply (rule_tac x="count a" in exI, simp) 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

212 
done 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

213 
have b: "\<And>i. P i \<Longrightarrow> enum i \<in> rep x 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

214 
\<Longrightarrow> enum (b i) \<in> rep x \<and> \<not> enum (b i) \<preceq> enum i" 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

215 
unfolding P_def b_def by (erule LeastI2_ex, simp) 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

216 
have c: "\<And>i j. enum i \<in> rep x \<Longrightarrow> enum j \<in> rep x 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

217 
\<Longrightarrow> enum (c i j) \<in> rep x \<and> enum i \<preceq> enum (c i j) \<and> enum j \<preceq> enum (c i j)" 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

218 
unfolding c_def 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

219 
apply (drule (1) idealD2 [OF ideal_rep], clarify) 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

220 
apply (rule_tac a="count z" in LeastI2, simp, simp) 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

221 
done 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

222 
have X_mem: "\<And>n. enum (X n) \<in> rep x" 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

223 
apply (induct_tac n) 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

224 
apply (simp add: X_0 a_mem) 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

225 
apply (clarsimp simp add: X_Suc, rename_tac n) 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

226 
apply (simp add: b c) 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

227 
done 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

228 
have X_chain: "\<And>n. enum (X n) \<preceq> enum (X (Suc n))" 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

229 
apply (clarsimp simp add: X_Suc r_refl) 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

230 
apply (simp add: b c X_mem) 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

231 
done 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

232 
have less_b: "\<And>n i. n < b i \<Longrightarrow> enum n \<in> rep x \<Longrightarrow> enum n \<preceq> enum i" 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

233 
unfolding b_def by (drule not_less_Least, simp) 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

234 
have X_covers: "\<And>n. \<forall>k\<le>n. enum k \<in> rep x \<longrightarrow> enum k \<preceq> enum (X n)" 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

235 
apply (induct_tac n) 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

236 
apply (clarsimp simp add: X_0 a_def) 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

237 
apply (drule_tac k=0 in Least_le, simp add: r_refl) 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

238 
apply (clarsimp, rename_tac n k) 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

239 
apply (erule le_SucE) 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

240 
apply (rule r_trans [OF _ X_chain], simp) 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

241 
apply (case_tac "P (X n)", simp add: X_Suc) 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

242 
apply (rule_tac x="b (X n)" and y="Suc n" in linorder_cases) 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

243 
apply (simp only: less_Suc_eq_le) 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

244 
apply (drule spec, drule (1) mp, simp add: b X_mem) 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

245 
apply (simp add: c X_mem) 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

246 
apply (drule (1) less_b) 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

247 
apply (erule r_trans) 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

248 
apply (simp add: b c X_mem) 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

249 
apply (simp add: X_Suc) 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

250 
apply (simp add: P_def) 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

251 
done 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

252 
have 1: "\<forall>i. enum (X i) \<preceq> enum (X (Suc i))" 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

253 
by (simp add: X_chain) 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

254 
have 2: "x = (\<Squnion>n. principal (enum (X n)))" 
40769  255 
apply (simp add: eq_iff rep_lub 1 rep_principal) 
39974
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

256 
apply (auto, rename_tac a) 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

257 
apply (subgoal_tac "\<exists>i. a = enum i", erule exE) 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

258 
apply (rule_tac x=i in exI, simp add: X_covers) 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

259 
apply (rule_tac x="count a" in exI, simp) 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

260 
apply (erule idealD3 [OF ideal_rep]) 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

261 
apply (rule X_mem) 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

262 
done 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

263 
from 1 2 show ?thesis .. 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

264 
qed 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

265 

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

266 
lemma principal_induct: 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

267 
assumes adm: "adm P" 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

268 
assumes P: "\<And>a. P (principal a)" 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

269 
shows "P x" 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

270 
apply (rule obtain_principal_chain [of x]) 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

271 
apply (simp add: admD [OF adm] P) 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

272 
done 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

273 

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

274 
lemma compact_imp_principal: "compact x \<Longrightarrow> \<exists>a. x = principal a" 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

275 
apply (rule obtain_principal_chain [of x]) 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

276 
apply (drule adm_compact_neq [OF _ cont_id]) 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

277 
apply (subgoal_tac "chain (\<lambda>i. principal (Y i))") 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

278 
apply (drule (2) admD2, fast, simp) 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

279 
done 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

280 

28133  281 
subsection {* Defining functions in terms of basis elements *} 
282 

283 
definition 

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

284 
extension :: "('a::type \<Rightarrow> 'c::cpo) \<Rightarrow> 'b \<rightarrow> 'c" where 
51c866d1b53b
rename function ideal_completion.basis_fun to ideal_completion.extension
huffman
parents:
41182
diff
changeset

285 
"extension = (\<lambda>f. (\<Lambda> x. lub (f ` rep x)))" 
28133  286 

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

287 
lemma extension_lemma: 
27404  288 
fixes f :: "'a::type \<Rightarrow> 'c::cpo" 
289 
assumes f_mono: "\<And>a b. a \<preceq> b \<Longrightarrow> f a \<sqsubseteq> f b" 

290 
shows "\<exists>u. f ` rep x << u" 

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

291 
proof  
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

292 
obtain Y where Y: "\<forall>i. Y i \<preceq> Y (Suc i)" 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

293 
and x: "x = (\<Squnion>i. principal (Y i))" 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

294 
by (rule obtain_principal_chain [of x]) 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

295 
have chain: "chain (\<lambda>i. f (Y i))" 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

296 
by (rule chainI, simp add: f_mono Y) 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

297 
have rep_x: "rep x = (\<Union>n. {a. a \<preceq> Y n})" 
40769  298 
by (simp add: x rep_lub Y rep_principal) 
39974
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

299 
have "f ` rep x << (\<Squnion>n. f (Y n))" 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

300 
apply (rule is_lubI) 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

301 
apply (rule ub_imageI, rename_tac a) 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

302 
apply (clarsimp simp add: rep_x) 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

303 
apply (drule f_mono) 
40500
ee9c8d36318e
add lemmas lub_below, below_lub; simplify some proofs; remove some unused lemmas
huffman
parents:
40002
diff
changeset

304 
apply (erule below_lub [OF chain]) 
ee9c8d36318e
add lemmas lub_below, below_lub; simplify some proofs; remove some unused lemmas
huffman
parents:
40002
diff
changeset

305 
apply (rule lub_below [OF chain]) 
ee9c8d36318e
add lemmas lub_below, below_lub; simplify some proofs; remove some unused lemmas
huffman
parents:
40002
diff
changeset

306 
apply (drule_tac x="Y n" in ub_imageD) 
39974
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

307 
apply (simp add: rep_x, fast intro: r_refl) 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

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

309 
done 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

310 
thus ?thesis .. 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

311 
qed 
27404  312 

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

313 
lemma extension_beta: 
27404  314 
fixes f :: "'a::type \<Rightarrow> 'c::cpo" 
315 
assumes f_mono: "\<And>a b. a \<preceq> b \<Longrightarrow> f a \<sqsubseteq> f b" 

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

316 
shows "extension f\<cdot>x = lub (f ` rep x)" 
51c866d1b53b
rename function ideal_completion.basis_fun to ideal_completion.extension
huffman
parents:
41182
diff
changeset

317 
unfolding extension_def 
27404  318 
proof (rule beta_cfun) 
319 
have lub: "\<And>x. \<exists>u. f ` rep x << u" 

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

320 
using f_mono by (rule extension_lemma) 
27404  321 
show cont: "cont (\<lambda>x. lub (f ` rep x))" 
322 
apply (rule contI2) 

323 
apply (rule monofunI) 

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

324 
apply (rule is_lub_thelub_ex [OF lub ub_imageI]) 
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

325 
apply (rule is_ub_thelub_ex [OF lub imageI]) 
27404  326 
apply (erule (1) subsetD [OF rep_mono]) 
39974
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

327 
apply (rule is_lub_thelub_ex [OF lub ub_imageI]) 
40769  328 
apply (simp add: rep_lub, clarify) 
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

329 
apply (erule rev_below_trans [OF is_ub_thelub]) 
39974
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

330 
apply (erule is_ub_thelub_ex [OF lub imageI]) 
27404  331 
done 
332 
qed 

333 

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

334 
lemma extension_principal: 
27404  335 
fixes f :: "'a::type \<Rightarrow> 'c::cpo" 
336 
assumes f_mono: "\<And>a b. a \<preceq> b \<Longrightarrow> f a \<sqsubseteq> f b" 

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

337 
shows "extension f\<cdot>(principal a) = f a" 
51c866d1b53b
rename function ideal_completion.basis_fun to ideal_completion.extension
huffman
parents:
41182
diff
changeset

338 
apply (subst extension_beta, erule f_mono) 
27404  339 
apply (subst rep_principal) 
41033  340 
apply (rule lub_eqI) 
341 
apply (rule is_lub_maximal) 

342 
apply (rule ub_imageI) 

343 
apply (simp add: f_mono) 

344 
apply (rule imageI) 

345 
apply (simp add: r_refl) 

27404  346 
done 
347 

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

348 
lemma extension_mono: 
27404  349 
assumes f_mono: "\<And>a b. a \<preceq> b \<Longrightarrow> f a \<sqsubseteq> f b" 
350 
assumes g_mono: "\<And>a b. a \<preceq> b \<Longrightarrow> g a \<sqsubseteq> g b" 

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

351 
assumes below: "\<And>a. f a \<sqsubseteq> g a" 
41394
51c866d1b53b
rename function ideal_completion.basis_fun to ideal_completion.extension
huffman
parents:
41182
diff
changeset

352 
shows "extension f \<sqsubseteq> extension g" 
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

353 
apply (rule cfun_belowI) 
41394
51c866d1b53b
rename function ideal_completion.basis_fun to ideal_completion.extension
huffman
parents:
41182
diff
changeset

354 
apply (simp only: extension_beta f_mono g_mono) 
39974
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

355 
apply (rule is_lub_thelub_ex) 
41394
51c866d1b53b
rename function ideal_completion.basis_fun to ideal_completion.extension
huffman
parents:
41182
diff
changeset

356 
apply (rule extension_lemma, erule f_mono) 
27404  357 
apply (rule ub_imageI, rename_tac a) 
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

358 
apply (rule below_trans [OF below]) 
39974
b525988432e9
major reorganization/simplification of HOLCF type classes:
huffman
parents:
39967
diff
changeset

359 
apply (rule is_ub_thelub_ex) 
41394
51c866d1b53b
rename function ideal_completion.basis_fun to ideal_completion.extension
huffman
parents:
41182
diff
changeset

360 
apply (rule extension_lemma, erule g_mono) 
27404  361 
apply (erule imageI) 
362 
done 

363 

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

364 
lemma cont_extension: 
41182  365 
assumes f_mono: "\<And>a b x. a \<preceq> b \<Longrightarrow> f x a \<sqsubseteq> f x b" 
366 
assumes f_cont: "\<And>a. cont (\<lambda>x. f x a)" 

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

367 
shows "cont (\<lambda>x. extension (\<lambda>a. f x a))" 
41182  368 
apply (rule contI2) 
369 
apply (rule monofunI) 

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

370 
apply (rule extension_mono, erule f_mono, erule f_mono) 
41182  371 
apply (erule cont2monofunE [OF f_cont]) 
372 
apply (rule cfun_belowI) 

373 
apply (rule principal_induct, simp) 

374 
apply (simp only: contlub_cfun_fun) 

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

375 
apply (simp only: extension_principal f_mono) 
41182  376 
apply (simp add: cont2contlubE [OF f_cont]) 
377 
done 

378 

27404  379 
end 
380 

39984  381 
lemma (in preorder) typedef_ideal_completion: 
382 
fixes Abs :: "'a set \<Rightarrow> 'b::cpo" 

383 
assumes type: "type_definition Rep Abs {S. ideal S}" 

384 
assumes below: "\<And>x y. x \<sqsubseteq> y \<longleftrightarrow> Rep x \<subseteq> Rep y" 

385 
assumes principal: "\<And>a. principal a = Abs {b. b \<preceq> a}" 

386 
assumes countable: "\<exists>f::'a \<Rightarrow> nat. inj f" 

387 
shows "ideal_completion r principal Rep" 

388 
proof 

389 
interpret type_definition Rep Abs "{S. ideal S}" by fact 

390 
fix a b :: 'a and x y :: 'b and Y :: "nat \<Rightarrow> 'b" 

391 
show "ideal (Rep x)" 

392 
using Rep [of x] by simp 

393 
show "chain Y \<Longrightarrow> Rep (\<Squnion>i. Y i) = (\<Union>i. Rep (Y i))" 

40769  394 
using type below by (rule typedef_ideal_rep_lub) 
39984  395 
show "Rep (principal a) = {b. b \<preceq> a}" 
396 
by (simp add: principal Abs_inverse ideal_principal) 

397 
show "Rep x \<subseteq> Rep y \<Longrightarrow> x \<sqsubseteq> y" 

398 
by (simp only: below) 

399 
show "\<exists>f::'a \<Rightarrow> nat. inj f" 

400 
by (rule countable) 

401 
qed 

402 

27404  403 
end 