author  kleing 
Mon, 21 Jun 2004 10:25:57 +0200  
changeset 14981  e73f8140af78 
parent 12484  7ad150f5fc10 
child 15563  9e125b675253 
permissions  rwrr 
9169  1 
(* Title: HOLCF/Pcpo.ML 
243
c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

2 
ID: $Id$ 
1461  3 
Author: Franz Regensburger 
243
c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

4 

9169  5 
introduction of the classes cpo and pcpo 
243
c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

6 
*) 
c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

7 

2640  8 

9 
(*  *) 

10 
(* derive the old rule minimal *) 

11 
(*  *) 

9169  12 

13 
Goalw [UU_def] "ALL z. UU << z"; 

9969  14 
by (rtac (some_eq_ex RS iffD2) 1); 
9169  15 
by (rtac least 1); 
16 
qed "UU_least"; 

2640  17 

9169  18 
bind_thm("minimal", UU_least RS spec); 
2640  19 

9248
e1dee89de037
massive tidyup: goal > Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset

20 
AddIffs [minimal]; 
e1dee89de037
massive tidyup: goal > Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset

21 

243
c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

22 
(*  *) 
2839  23 
(* in cpo's everthing equal to THE lub has lub properties for every chain *) 
243
c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

24 
(*  *) 
c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

25 

9248
e1dee89de037
massive tidyup: goal > Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset

26 
Goal "[ chain(S); lub(range(S)) = (l::'a::cpo) ] ==> range(S) << l "; 
e1dee89de037
massive tidyup: goal > Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset

27 
by (blast_tac (claset() addDs [cpo] addIs [lubI]) 1); 
9169  28 
qed "thelubE"; 
243
c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

29 

c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

30 
(*  *) 
c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

31 
(* Properties of the lub *) 
c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

32 
(*  *) 
c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

33 

c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

34 

9248
e1dee89de037
massive tidyup: goal > Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset

35 
Goal "chain (S::nat => 'a::cpo) ==> S(x) << lub(range(S))"; 
e1dee89de037
massive tidyup: goal > Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset

36 
by (blast_tac (claset() addDs [cpo] addIs [lubI RS is_ub_lub]) 1); 
e1dee89de037
massive tidyup: goal > Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset

37 
qed "is_ub_thelub"; 
243
c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

38 

9248
e1dee89de037
massive tidyup: goal > Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset

39 
Goal "[ chain (S::nat => 'a::cpo); range(S) < x ] ==> lub(range S) << x"; 
e1dee89de037
massive tidyup: goal > Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset

40 
by (blast_tac (claset() addDs [cpo] addIs [lubI RS is_lub_lub]) 1); 
e1dee89de037
massive tidyup: goal > Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset

41 
qed "is_lub_thelub"; 
e1dee89de037
massive tidyup: goal > Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset

42 

11342  43 
Goal "[ range X <= range Y; chain Y; chain (X::nat=>'a::cpo) ] ==> lub(range X) << lub(range Y)"; 
44 
by (etac is_lub_thelub 1); 

45 
by (rtac ub_rangeI 1); 

46 
by (subgoal_tac "? j. X i = Y j" 1); 

47 
by (Clarsimp_tac 1); 

48 
by (etac is_ub_thelub 1); 

49 
by Auto_tac; 

50 
qed "lub_range_mono"; 

51 

52 
Goal "chain (Y::nat=>'a::cpo) ==> lub(range (%i. Y(i + j))) = lub(range Y)"; 

53 
by (rtac antisym_less 1); 

12484  54 
by (rtac lub_range_mono 1); 
11342  55 
by (Fast_tac 1); 
56 
by (atac 1); 

12484  57 
by (etac chain_shift 1); 
58 
by (rtac is_lub_thelub 1); 

59 
by (assume_tac 1); 

60 
by (rtac ub_rangeI 1); 

61 
by (rtac trans_less 1); 

62 
by (rtac is_ub_thelub 2); 

63 
by (etac chain_shift 2); 

64 
by (etac chain_mono3 1); 

65 
by (rtac le_add1 1); 

11342  66 
qed "lub_range_shift"; 
243
c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

67 

9169  68 
Goal "chain Y ==> max_in_chain i Y = (lub(range(Y)) = ((Y i)::'a::cpo))"; 
69 
by (rtac iffI 1); 

70 
by (fast_tac (HOL_cs addSIs [thelubI,lub_finch1]) 1); 

71 
by (rewtac max_in_chain_def); 

72 
by (safe_tac (HOL_cs addSIs [antisym_less])); 

73 
by (fast_tac (HOL_cs addSEs [chain_mono3]) 1); 

74 
by (dtac sym 1); 

75 
by (force_tac (HOL_cs addSEs [is_ub_thelub], simpset()) 1); 

76 
qed "maxinch_is_thelub"; 

2354  77 

243
c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

78 

c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

79 
(*  *) 
c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

80 
(* the << relation between two chains is preserved by their lubs *) 
c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

81 
(*  *) 
c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

82 

9169  83 
Goal "[chain(C1::(nat=>'a::cpo));chain(C2); ALL k. C1(k) << C2(k)]\ 
84 
\ ==> lub(range(C1)) << lub(range(C2))"; 

85 
by (etac is_lub_thelub 1); 

86 
by (rtac ub_rangeI 1); 

87 
by (rtac trans_less 1); 

88 
by (etac spec 1); 

89 
by (etac is_ub_thelub 1); 

90 
qed "lub_mono"; 

243
c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

91 

c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

92 
(*  *) 
c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

93 
(* the = relation between two chains is preserved by their lubs *) 
c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

94 
(*  *) 
c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

95 

9169  96 
Goal "[ chain(C1::(nat=>'a::cpo));chain(C2);ALL k. C1(k)=C2(k)]\ 
97 
\ ==> lub(range(C1))=lub(range(C2))"; 

98 
by (rtac antisym_less 1); 

99 
by (rtac lub_mono 1); 

100 
by (atac 1); 

101 
by (atac 1); 

102 
by (strip_tac 1); 

103 
by (rtac (antisym_less_inverse RS conjunct1) 1); 

104 
by (etac spec 1); 

105 
by (rtac lub_mono 1); 

106 
by (atac 1); 

107 
by (atac 1); 

108 
by (strip_tac 1); 

109 
by (rtac (antisym_less_inverse RS conjunct2) 1); 

110 
by (etac spec 1); 

111 
qed "lub_equal"; 

243
c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

112 

c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

113 
(*  *) 
c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

114 
(* more results about mono and = of lubs of chains *) 
c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

115 
(*  *) 
c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

116 

9169  117 
Goal "[EX j. ALL i. j<i > X(i::nat)=Y(i);chain(X::nat=>'a::cpo);chain(Y)]\ 
118 
\ ==> lub(range(X))<<lub(range(Y))"; 

119 
by (etac exE 1); 

120 
by (rtac is_lub_thelub 1); 

121 
by (assume_tac 1); 

122 
by (rtac ub_rangeI 1); 

123 
by (strip_tac 1); 

124 
by (case_tac "j<i" 1); 

125 
by (res_inst_tac [("s","Y(i)"),("t","X(i)")] subst 1); 

126 
by (rtac sym 1); 

127 
by (Fast_tac 1); 

128 
by (rtac is_ub_thelub 1); 

129 
by (assume_tac 1); 

130 
by (res_inst_tac [("y","X(Suc(j))")] trans_less 1); 

9248
e1dee89de037
massive tidyup: goal > Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset

131 
by (rtac chain_mono 1); 
9169  132 
by (assume_tac 1); 
133 
by (rtac (not_less_eq RS subst) 1); 

134 
by (atac 1); 

135 
by (res_inst_tac [("s","Y(Suc(j))"),("t","X(Suc(j))")] subst 1); 

136 
by (Asm_simp_tac 1); 

137 
by (etac is_ub_thelub 1); 

138 
qed "lub_mono2"; 

243
c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

139 

9169  140 
Goal "[EX j. ALL i. j<i > X(i)=Y(i); chain(X::nat=>'a::cpo); chain(Y)]\ 
141 
\ ==> lub(range(X))=lub(range(Y))"; 

142 
by (blast_tac (claset() addIs [antisym_less, lub_mono2, sym]) 1); 

143 
qed "lub_equal2"; 

243
c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

144 

9169  145 
Goal "[chain(Y::nat=>'a::cpo);chain(X);\ 
146 
\ALL i. EX j. Y(i)<< X(j)]==> lub(range(Y))<<lub(range(X))"; 

147 
by (rtac is_lub_thelub 1); 

148 
by (atac 1); 

149 
by (rtac ub_rangeI 1); 

150 
by (strip_tac 1); 

151 
by (etac allE 1); 

152 
by (etac exE 1); 

153 
by (rtac trans_less 1); 

154 
by (rtac is_ub_thelub 2); 

155 
by (atac 2); 

156 
by (atac 1); 

157 
qed "lub_mono3"; 

243
c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

158 

c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

159 
(*  *) 
c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

160 
(* usefull lemmas about UU *) 
c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

161 
(*  *) 
c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

162 

9169  163 
Goal "(x=UU)=(x<<UU)"; 
164 
by (rtac iffI 1); 

165 
by (hyp_subst_tac 1); 

166 
by (rtac refl_less 1); 

167 
by (rtac antisym_less 1); 

168 
by (atac 1); 

169 
by (rtac minimal 1); 

170 
qed "eq_UU_iff"; 

243
c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

171 

9169  172 
Goal "x << UU ==> x = UU"; 
173 
by (stac eq_UU_iff 1); 

174 
by (assume_tac 1); 

175 
qed "UU_I"; 

243
c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

176 

9169  177 
Goal "~(x::'a::po)<<y ==> ~x=y"; 
178 
by Auto_tac; 

179 
qed "not_less2not_eq"; 

180 

181 
Goal "[chain(Y);lub(range(Y))=UU] ==> ALL i. Y(i)=UU"; 

182 
by (rtac allI 1); 

183 
by (rtac antisym_less 1); 

184 
by (rtac minimal 2); 

185 
by (etac subst 1); 

186 
by (etac is_ub_thelub 1); 

187 
qed "chain_UU_I"; 

243
c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

188 

c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

189 

9169  190 
Goal "ALL i. Y(i::nat)=UU ==> lub(range(Y::(nat=>'a::pcpo)))=UU"; 
191 
by (rtac lub_chain_maxelem 1); 

192 
by (etac spec 1); 

193 
by (rtac allI 1); 

194 
by (rtac (antisym_less_inverse RS conjunct1) 1); 

195 
by (etac spec 1); 

196 
qed "chain_UU_I_inverse"; 

243
c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

197 

9169  198 
Goal "~lub(range(Y::(nat=>'a::pcpo)))=UU ==> EX i.~ Y(i)=UU"; 
199 
by (blast_tac (claset() addIs [chain_UU_I_inverse]) 1); 

200 
qed "chain_UU_I_inverse2"; 

243
c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

201 

9169  202 
Goal "[ x<<y; ~x=UU ] ==> ~y=UU"; 
203 
by (blast_tac (claset() addIs [UU_I]) 1); 

204 
qed "notUU_I"; 

205 

206 
Goal 

207 
"[EX j. ~Y(j)=UU;chain(Y::nat=>'a::pcpo)] ==> EX j. ALL i. j<i>~Y(i)=UU"; 

9248
e1dee89de037
massive tidyup: goal > Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset

208 
by (blast_tac (claset() addDs [notUU_I, chain_mono]) 1); 
9169  209 
qed "chain_mono2"; 
3326  210 

211 
(**************************************) 

212 
(* some properties for chfin and flat *) 

213 
(**************************************) 

214 

215 
(*  *) 

4721
c8a8482a8124
renamed is_chain to chain, is_tord to tord, replaced chain_finite by chfin
oheimb
parents:
4098
diff
changeset

216 
(* flat types are chfin *) 
3326  217 
(*  *) 
218 

9248
e1dee89de037
massive tidyup: goal > Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset

219 
(*Used only in an "instance" declaration (Fun1.thy)*) 
9169  220 
Goalw [max_in_chain_def] 
9248
e1dee89de037
massive tidyup: goal > Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset

221 
"ALL Y::nat=>'a::flat. chain Y > (EX n. max_in_chain n Y)"; 
e1dee89de037
massive tidyup: goal > Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset

222 
by (Clarify_tac 1); 
9169  223 
by (case_tac "ALL i. Y(i)=UU" 1); 
224 
by (res_inst_tac [("x","0")] exI 1); 

225 
by (Asm_simp_tac 1); 

226 
by (Asm_full_simp_tac 1); 

227 
by (etac exE 1); 

228 
by (res_inst_tac [("x","i")] exI 1); 

229 
by (strip_tac 1); 

230 
by (etac (le_imp_less_or_eq RS disjE) 1); 

231 
by Safe_tac; 

9248
e1dee89de037
massive tidyup: goal > Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset

232 
by (blast_tac (claset() addDs [chain_mono, ax_flat RS spec RS spec RS mp]) 1); 
9169  233 
qed "flat_imp_chfin"; 
3326  234 

235 
(* flat subclass of chfin > adm_flat not needed *) 

236 

9169  237 
Goal "(a::'a::flat) ~= UU ==> a << b = (a = b)"; 
238 
by (safe_tac (HOL_cs addSIs [refl_less])); 

239 
by (dtac (ax_flat RS spec RS spec RS mp) 1); 

240 
by (fast_tac (HOL_cs addSIs [refl_less,ax_flat RS spec RS spec RS mp]) 1); 

241 
qed "flat_eq"; 

3326  242 

9169  243 
Goal "chain (Y::nat=>'a::chfin) ==> finite_chain Y"; 
244 
by (force_tac (HOL_cs, simpset() addsimps [chfin,finite_chain_def]) 1); 

245 
qed "chfin2finch"; 

3326  246 

247 
(*  *) 

248 
(* lemmata for improved admissibility introdution rule *) 

249 
(*  *) 

250 

9169  251 
val prems = Goal 
252 
"[chain Y; ALL i. P (Y i); \ 

253 
\ (!!Y. [ chain Y; ALL i. P (Y i); ~ finite_chain Y ] ==> P (lub(range Y)))\ 

254 
\ ] ==> P (lub (range Y))"; 

255 
by (cut_facts_tac prems 1); 

256 
by (case_tac "finite_chain Y" 1); 

257 
by (eresolve_tac prems 2); 

258 
by (atac 2); 

259 
by (atac 2); 

260 
by (rewtac finite_chain_def); 

261 
by (safe_tac HOL_cs); 

262 
by (etac (lub_finch1 RS thelubI RS ssubst) 1); 

263 
by (atac 1); 

264 
by (etac spec 1); 

265 
qed "infinite_chain_adm_lemma"; 

3326  266 

9169  267 
val prems = Goal 
268 
"[chain Y; ALL i. P (Y i); \ 

269 
\ (!!Y. [ chain Y; ALL i. P (Y i); \ 

270 
\ ALL i. EX j. i < j & Y i ~= Y j & Y i << Y j]\ 

271 
\ ==> P (lub (range Y))) ] ==> P (lub (range Y))"; 

272 
by (cut_facts_tac prems 1); 

273 
by (etac infinite_chain_adm_lemma 1); 

274 
by (atac 1); 

275 
by (etac thin_rl 1); 

276 
by (rewtac finite_chain_def); 

277 
by (rewtac max_in_chain_def); 

278 
by (fast_tac (HOL_cs addIs prems 

9248
e1dee89de037
massive tidyup: goal > Goal, remove use of prems, etc.
paulson
parents:
9169
diff
changeset

279 
addDs [le_imp_less_or_eq] addEs [chain_mono]) 1); 
9169  280 
qed "increasing_chain_adm_lemma"; 