author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 46125  00cd193a48dc 
child 58249  180f1b3508ed 
permissions  rwrr 
42151  1 
(* Title: HOL/HOLCF/Up.thy 
40502
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
40327
diff
changeset

2 
Author: Franz Regensburger 
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
40327
diff
changeset

3 
Author: Brian Huffman 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

4 
*) 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

5 

efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

6 
header {* The type of lifted values *} 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

7 

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

9 
imports Cfun 
15577  10 
begin 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

11 

36452  12 
default_sort cpo 
15599
10cedbd5289e
instance u :: (cpo) pcpo  argument type no longer needs to be pointed
huffman
parents:
15593
diff
changeset

13 

15593
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

14 
subsection {* Definition of new type for lifting *} 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

15 

16753  16 
datatype 'a u = Ibottom  Iup 'a 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

17 

35427  18 
type_notation (xsymbols) 
19 
u ("(_\<^sub>\<bottom>)" [1000] 999) 

18290  20 

34941  21 
primrec Ifup :: "('a \<rightarrow> 'b::pcpo) \<Rightarrow> 'a u \<Rightarrow> 'b" where 
22 
"Ifup f Ibottom = \<bottom>" 

23 
 "Ifup f (Iup x) = f\<cdot>x" 

15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

24 

18290  25 
subsection {* Ordering on lifted cpo *} 
15593
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

26 

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

27 
instantiation u :: (cpo) below 
25787  28 
begin 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

29 

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

31 
below_up_def: 
16753  32 
"(op \<sqsubseteq>) \<equiv> (\<lambda>x y. case x of Ibottom \<Rightarrow> True  Iup a \<Rightarrow> 
33 
(case y of Ibottom \<Rightarrow> False  Iup b \<Rightarrow> a \<sqsubseteq> b))" 

15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

34 

25787  35 
instance .. 
36 
end 

37 

16753  38 
lemma minimal_up [iff]: "Ibottom \<sqsubseteq> z" 
31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
29530
diff
changeset

39 
by (simp add: below_up_def) 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

40 

41182  41 
lemma not_Iup_below [iff]: "Iup x \<notsqsubseteq> Ibottom" 
31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
29530
diff
changeset

42 
by (simp add: below_up_def) 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

43 

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

44 
lemma Iup_below [iff]: "(Iup x \<sqsubseteq> Iup y) = (x \<sqsubseteq> y)" 
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
29530
diff
changeset

45 
by (simp add: below_up_def) 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

46 

18290  47 
subsection {* Lifted cpo is a partial order *} 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

48 

15599
10cedbd5289e
instance u :: (cpo) pcpo  argument type no longer needs to be pointed
huffman
parents:
15593
diff
changeset

49 
instance u :: (cpo) po 
25787  50 
proof 
51 
fix x :: "'a u" 

52 
show "x \<sqsubseteq> x" 

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

53 
unfolding below_up_def by (simp split: u.split) 
25787  54 
next 
55 
fix x y :: "'a u" 

56 
assume "x \<sqsubseteq> y" "y \<sqsubseteq> x" thus "x = y" 

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

57 
unfolding below_up_def 
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
29530
diff
changeset

58 
by (auto split: u.split_asm intro: below_antisym) 
25787  59 
next 
60 
fix x y z :: "'a u" 

61 
assume "x \<sqsubseteq> y" "y \<sqsubseteq> z" thus "x \<sqsubseteq> z" 

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

62 
unfolding below_up_def 
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
29530
diff
changeset

63 
by (auto split: u.split_asm intro: below_trans) 
25787  64 
qed 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

65 

18290  66 
subsection {* Lifted cpo is a cpo *} 
15593
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

67 

16319
1ff2965cc2e7
major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents:
16215
diff
changeset

68 
lemma is_lub_Iup: 
1ff2965cc2e7
major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents:
16215
diff
changeset

69 
"range S << x \<Longrightarrow> range (\<lambda>i. Iup (S i)) << Iup x" 
40084  70 
unfolding is_lub_def is_ub_def ball_simps 
71 
by (auto simp add: below_up_def split: u.split) 

15599
10cedbd5289e
instance u :: (cpo) pcpo  argument type no longer needs to be pointed
huffman
parents:
15593
diff
changeset

72 

17838  73 
lemma up_chain_lemma: 
40084  74 
assumes Y: "chain Y" obtains "\<forall>i. Y i = Ibottom" 
75 
 A k where "\<forall>i. Iup (A i) = Y (i + k)" and "chain A" and "range Y << Iup (\<Squnion>i. A i)" 

76 
proof (cases "\<exists>k. Y k \<noteq> Ibottom") 

77 
case True 

78 
then obtain k where k: "Y k \<noteq> Ibottom" .. 

79 
def A \<equiv> "\<lambda>i. THE a. Iup a = Y (i + k)" 

80 
have Iup_A: "\<forall>i. Iup (A i) = Y (i + k)" 

81 
proof 

82 
fix i :: nat 

83 
from Y le_add2 have "Y k \<sqsubseteq> Y (i + k)" by (rule chain_mono) 

84 
with k have "Y (i + k) \<noteq> Ibottom" by (cases "Y k", auto) 

85 
thus "Iup (A i) = Y (i + k)" 

86 
by (cases "Y (i + k)", simp_all add: A_def) 

87 
qed 

88 
from Y have chain_A: "chain A" 

89 
unfolding chain_def Iup_below [symmetric] 

90 
by (simp add: Iup_A) 

91 
hence "range A << (\<Squnion>i. A i)" 

92 
by (rule cpo_lubI) 

93 
hence "range (\<lambda>i. Iup (A i)) << Iup (\<Squnion>i. A i)" 

94 
by (rule is_lub_Iup) 

95 
hence "range (\<lambda>i. Y (i + k)) << Iup (\<Squnion>i. A i)" 

96 
by (simp only: Iup_A) 

97 
hence "range (\<lambda>i. Y i) << Iup (\<Squnion>i. A i)" 

98 
by (simp only: is_lub_range_shift [OF Y]) 

99 
with Iup_A chain_A show ?thesis .. 

100 
next 

101 
case False 

102 
then have "\<forall>i. Y i = Ibottom" by simp 

103 
then show ?thesis .. 

104 
qed 

15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

105 

15599
10cedbd5289e
instance u :: (cpo) pcpo  argument type no longer needs to be pointed
huffman
parents:
15593
diff
changeset

106 
instance u :: (cpo) cpo 
40084  107 
proof 
108 
fix S :: "nat \<Rightarrow> 'a u" 

109 
assume S: "chain S" 

110 
thus "\<exists>x. range (\<lambda>i. S i) << x" 

111 
proof (rule up_chain_lemma) 

112 
assume "\<forall>i. S i = Ibottom" 

113 
hence "range (\<lambda>i. S i) << Ibottom" 

40771  114 
by (simp add: is_lub_const) 
40084  115 
thus ?thesis .. 
116 
next 

40085  117 
fix A :: "nat \<Rightarrow> 'a" 
118 
assume "range S << Iup (\<Squnion>i. A i)" 

40084  119 
thus ?thesis .. 
120 
qed 

121 
qed 

15593
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

122 

18290  123 
subsection {* Lifted cpo is pointed *} 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

124 

15599
10cedbd5289e
instance u :: (cpo) pcpo  argument type no longer needs to be pointed
huffman
parents:
15593
diff
changeset

125 
instance u :: (cpo) pcpo 
40084  126 
by intro_classes fast 
15593
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

127 

24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

128 
text {* for compatibility with old HOLCFVersion *} 
16753  129 
lemma inst_up_pcpo: "\<bottom> = Ibottom" 
41430
1aa23e9f2c87
change some lemma names containing 'UU' to 'bottom'
huffman
parents:
41182
diff
changeset

130 
by (rule minimal_up [THEN bottomI, symmetric]) 
15593
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

131 

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

132 
subsection {* Continuity of \emph{Iup} and \emph{Ifup} *} 
15593
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

133 

24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

134 
text {* continuity for @{term Iup} *} 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

135 

16319
1ff2965cc2e7
major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents:
16215
diff
changeset

136 
lemma cont_Iup: "cont Iup" 
16215  137 
apply (rule contI) 
15599
10cedbd5289e
instance u :: (cpo) pcpo  argument type no longer needs to be pointed
huffman
parents:
15593
diff
changeset

138 
apply (rule is_lub_Iup) 
26027  139 
apply (erule cpo_lubI) 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

140 
done 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

141 

15593
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

142 
text {* continuity for @{term Ifup} *} 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

143 

16319
1ff2965cc2e7
major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents:
16215
diff
changeset

144 
lemma cont_Ifup1: "cont (\<lambda>f. Ifup f x)" 
16753  145 
by (induct x, simp_all) 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

146 

16319
1ff2965cc2e7
major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents:
16215
diff
changeset

147 
lemma monofun_Ifup2: "monofun (\<lambda>x. Ifup f x)" 
1ff2965cc2e7
major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents:
16215
diff
changeset

148 
apply (rule monofunI) 
16753  149 
apply (case_tac x, simp) 
150 
apply (case_tac y, simp) 

16319
1ff2965cc2e7
major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents:
16215
diff
changeset

151 
apply (simp add: monofun_cfun_arg) 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

152 
done 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

153 

16319
1ff2965cc2e7
major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents:
16215
diff
changeset

154 
lemma cont_Ifup2: "cont (\<lambda>x. Ifup f x)" 
40084  155 
proof (rule contI2) 
156 
fix Y assume Y: "chain Y" and Y': "chain (\<lambda>i. Ifup f (Y i))" 

157 
from Y show "Ifup f (\<Squnion>i. Y i) \<sqsubseteq> (\<Squnion>i. Ifup f (Y i))" 

158 
proof (rule up_chain_lemma) 

159 
fix A and k 

160 
assume A: "\<forall>i. Iup (A i) = Y (i + k)" 

161 
assume "chain A" and "range Y << Iup (\<Squnion>i. A i)" 

162 
hence "Ifup f (\<Squnion>i. Y i) = (\<Squnion>i. Ifup f (Iup (A i)))" 

40771  163 
by (simp add: lub_eqI contlub_cfun_arg) 
40084  164 
also have "\<dots> = (\<Squnion>i. Ifup f (Y (i + k)))" 
165 
by (simp add: A) 

166 
also have "\<dots> = (\<Squnion>i. Ifup f (Y i))" 

167 
using Y' by (rule lub_range_shift) 

168 
finally show ?thesis by simp 

169 
qed simp 

170 
qed (rule monofun_Ifup2) 

15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

171 

15593
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

172 
subsection {* Continuous versions of constants *} 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

173 

25131
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
19105
diff
changeset

174 
definition 
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
19105
diff
changeset

175 
up :: "'a \<rightarrow> 'a u" where 
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
19105
diff
changeset

176 
"up = (\<Lambda> x. Iup x)" 
16319
1ff2965cc2e7
major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents:
16215
diff
changeset

177 

25131
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
19105
diff
changeset

178 
definition 
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
19105
diff
changeset

179 
fup :: "('a \<rightarrow> 'b::pcpo) \<rightarrow> 'a u \<rightarrow> 'b" where 
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
19105
diff
changeset

180 
"fup = (\<Lambda> f p. Ifup f p)" 
15593
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

181 

24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

182 
translations 
26046  183 
"case l of XCONST up\<cdot>x \<Rightarrow> t" == "CONST fup\<cdot>(\<Lambda> x. t)\<cdot>l" 
46125
00cd193a48dc
improved case syntax: more careful treatment of position constraints, which enables PIDE markup;
wenzelm
parents:
42151
diff
changeset

184 
"case l of (XCONST up :: 'a)\<cdot>x \<Rightarrow> t" => "CONST fup\<cdot>(\<Lambda> x. t)\<cdot>l" 
26046  185 
"\<Lambda>(XCONST up\<cdot>x). t" == "CONST fup\<cdot>(\<Lambda> x. t)" 
15593
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

186 

24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset

187 
text {* continuous versions of lemmas for @{typ "('a)u"} *} 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

188 

16753  189 
lemma Exh_Up: "z = \<bottom> \<or> (\<exists>x. z = up\<cdot>x)" 
190 
apply (induct z) 

16319
1ff2965cc2e7
major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents:
16215
diff
changeset

191 
apply (simp add: inst_up_pcpo) 
1ff2965cc2e7
major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents:
16215
diff
changeset

192 
apply (simp add: up_def cont_Iup) 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

193 
done 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

194 

16753  195 
lemma up_eq [simp]: "(up\<cdot>x = up\<cdot>y) = (x = y)" 
16319
1ff2965cc2e7
major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents:
16215
diff
changeset

196 
by (simp add: up_def cont_Iup) 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

197 

16753  198 
lemma up_inject: "up\<cdot>x = up\<cdot>y \<Longrightarrow> x = y" 
199 
by simp 

16319
1ff2965cc2e7
major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents:
16215
diff
changeset

200 

17838  201 
lemma up_defined [simp]: "up\<cdot>x \<noteq> \<bottom>" 
16319
1ff2965cc2e7
major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents:
16215
diff
changeset

202 
by (simp add: up_def cont_Iup inst_up_pcpo) 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

203 

41182  204 
lemma not_up_less_UU: "up\<cdot>x \<notsqsubseteq> \<bottom>" 
31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
29530
diff
changeset

205 
by simp (* FIXME: remove? *) 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

206 

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

207 
lemma up_below [simp]: "up\<cdot>x \<sqsubseteq> up\<cdot>y \<longleftrightarrow> x \<sqsubseteq> y" 
16319
1ff2965cc2e7
major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents:
16215
diff
changeset

208 
by (simp add: up_def cont_Iup) 
1ff2965cc2e7
major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents:
16215
diff
changeset

209 

35783  210 
lemma upE [case_names bottom up, cases type: u]: 
211 
"\<lbrakk>p = \<bottom> \<Longrightarrow> Q; \<And>x. p = up\<cdot>x \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q" 

25788
30cbe0764599
declare upE as cases rule; add new rule up_induct
huffman
parents:
25787
diff
changeset

212 
apply (cases p) 
16319
1ff2965cc2e7
major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents:
16215
diff
changeset

213 
apply (simp add: inst_up_pcpo) 
1ff2965cc2e7
major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents:
16215
diff
changeset

214 
apply (simp add: up_def cont_Iup) 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

215 
done 
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

216 

35783  217 
lemma up_induct [case_names bottom up, induct type: u]: 
218 
"\<lbrakk>P \<bottom>; \<And>x. P (up\<cdot>x)\<rbrakk> \<Longrightarrow> P x" 

25788
30cbe0764599
declare upE as cases rule; add new rule up_induct
huffman
parents:
25787
diff
changeset

219 
by (cases x, simp_all) 
30cbe0764599
declare upE as cases rule; add new rule up_induct
huffman
parents:
25787
diff
changeset

220 

25827
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25789
diff
changeset

221 
text {* lifting preserves chainfiniteness *} 
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25789
diff
changeset

222 

17838  223 
lemma up_chain_cases: 
40084  224 
assumes Y: "chain Y" obtains "\<forall>i. Y i = \<bottom>" 
225 
 A k where "\<forall>i. up\<cdot>(A i) = Y (i + k)" and "chain A" and "(\<Squnion>i. Y i) = up\<cdot>(\<Squnion>i. A i)" 

226 
apply (rule up_chain_lemma [OF Y]) 

40771  227 
apply (simp_all add: inst_up_pcpo up_def cont_Iup lub_eqI) 
40084  228 
done 
17838  229 

25879  230 
lemma compact_up: "compact x \<Longrightarrow> compact (up\<cdot>x)" 
231 
apply (rule compactI2) 

40084  232 
apply (erule up_chain_cases) 
233 
apply simp 

25879  234 
apply (drule (1) compactD2, simp) 
40084  235 
apply (erule exE) 
236 
apply (drule_tac f="up" and x="x" in monofun_cfun_arg) 

237 
apply (simp, erule exI) 

25879  238 
done 
239 

240 
lemma compact_upD: "compact (up\<cdot>x) \<Longrightarrow> compact x" 

241 
unfolding compact_def 

40327  242 
by (drule adm_subst [OF cont_Rep_cfun2 [where f=up]], simp) 
25879  243 

244 
lemma compact_up_iff [simp]: "compact (up\<cdot>x) = compact x" 

245 
by (safe elim!: compact_up compact_upD) 

246 

25827
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25789
diff
changeset

247 
instance u :: (chfin) chfin 
25921  248 
apply intro_classes 
25879  249 
apply (erule compact_imp_max_in_chain) 
25898  250 
apply (rule_tac p="\<Squnion>i. Y i" in upE, simp_all) 
17838  251 
done 
252 

253 
text {* properties of fup *} 

254 

16319
1ff2965cc2e7
major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents:
16215
diff
changeset

255 
lemma fup1 [simp]: "fup\<cdot>f\<cdot>\<bottom> = \<bottom>" 
29530
9905b660612b
change to simpler, more extensible continuity simproc
huffman
parents:
29138
diff
changeset

256 
by (simp add: fup_def cont_Ifup1 cont_Ifup2 inst_up_pcpo cont2cont_LAM) 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

257 

16319
1ff2965cc2e7
major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents:
16215
diff
changeset

258 
lemma fup2 [simp]: "fup\<cdot>f\<cdot>(up\<cdot>x) = f\<cdot>x" 
29530
9905b660612b
change to simpler, more extensible continuity simproc
huffman
parents:
29138
diff
changeset

259 
by (simp add: up_def fup_def cont_Iup cont_Ifup1 cont_Ifup2 cont2cont_LAM) 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

260 

16553  261 
lemma fup3 [simp]: "fup\<cdot>up\<cdot>x = x" 
25788
30cbe0764599
declare upE as cases rule; add new rule up_induct
huffman
parents:
25787
diff
changeset

262 
by (cases x, simp_all) 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
diff
changeset

263 

26962
c8b20f615d6c
use new class package for classes profinite, bifinite; remove approx class
huffman
parents:
26407
diff
changeset

264 
end 