author  wenzelm 
Mon, 19 Mar 2012 21:49:52 +0100  
changeset 47025  b2b8ae61d6ad 
parent 41310  65631ca437c9 
child 48475  02dd825f5a4e 
permissions  rwrr 
19757  1 
(* Title: LCF/LCF.thy 
1474  2 
Author: Tobias Nipkow 
0  3 
Copyright 1992 University of Cambridge 
4 
*) 

5 

17248  6 
header {* LCF on top of FirstOrder Logic *} 
0  7 

17248  8 
theory LCF 
9 
imports FOL 

10 
begin 

0  11 

17248  12 
text {* This theory is based on Lawrence Paulson's book Logic and Computation. *} 
0  13 

17248  14 
subsection {* Natural Deduction Rules for LCF *} 
15 

16 
classes cpo < "term" 

36452  17 
default_sort cpo 
17248  18 

19 
typedecl tr 

20 
typedecl void 

41310  21 
typedecl ('a,'b) prod (infixl "*" 6) 
22 
typedecl ('a,'b) sum (infixl "+" 5) 

0  23 

283  24 
arities 
27208
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
22810
diff
changeset

25 
"fun" :: (cpo, cpo) cpo 
41310  26 
prod :: (cpo, cpo) cpo 
27 
sum :: (cpo, cpo) cpo 

17248  28 
tr :: cpo 
29 
void :: cpo 

0  30 

31 
consts 

1474  32 
UU :: "'a" 
17248  33 
TT :: "tr" 
34 
FF :: "tr" 

1474  35 
FIX :: "('a => 'a) => 'a" 
36 
FST :: "'a*'b => 'a" 

37 
SND :: "'a*'b => 'b" 

0  38 
INL :: "'a => 'a+'b" 
39 
INR :: "'b => 'a+'b" 

40 
WHEN :: "['a=>'c, 'b=>'c, 'a+'b] => 'c" 

1474  41 
adm :: "('a => o) => o" 
42 
VOID :: "void" ("'(')") 

43 
PAIR :: "['a,'b] => 'a*'b" ("(1<_,/_>)" [0,0] 100) 

44 
COND :: "[tr,'a,'a] => 'a" ("(_ =>/ (_ / _))" [60,60,60] 60) 

22810  45 
less :: "['a,'a] => o" (infixl "<<" 50) 
17248  46 

47025  47 
axiomatization where 
0  48 
(** DOMAIN THEORY **) 
49 

47025  50 
eq_def: "x=y == x << y & y << x" and 
0  51 

47025  52 
less_trans: "[ x << y; y << z ] ==> x << z" and 
0  53 

47025  54 
less_ext: "(ALL x. f(x) << g(x)) ==> f << g" and 
0  55 

47025  56 
mono: "[ f << g; x << y ] ==> f(x) << g(y)" and 
57 

58 
minimal: "UU << x" and 

0  59 

47025  60 
FIX_eq: "\<And>f. f(FIX(f)) = FIX(f)" 
0  61 

47025  62 
axiomatization where 
0  63 
(** TR **) 
64 

47025  65 
tr_cases: "p=UU  p=TT  p=FF" and 
0  66 

47025  67 
not_TT_less_FF: "~ TT << FF" and 
68 
not_FF_less_TT: "~ FF << TT" and 

69 
not_TT_less_UU: "~ TT << UU" and 

70 
not_FF_less_UU: "~ FF << UU" and 

0  71 

47025  72 
COND_UU: "UU => x  y = UU" and 
73 
COND_TT: "TT => x  y = x" and 

17248  74 
COND_FF: "FF => x  y = y" 
0  75 

47025  76 
axiomatization where 
0  77 
(** PAIRS **) 
78 

47025  79 
surj_pairing: "<FST(z),SND(z)> = z" and 
0  80 

47025  81 
FST: "FST(<x,y>) = x" and 
17248  82 
SND: "SND(<x,y>) = y" 
0  83 

47025  84 
axiomatization where 
0  85 
(*** STRICT SUM ***) 
86 

47025  87 
INL_DEF: "~x=UU ==> ~INL(x)=UU" and 
88 
INR_DEF: "~x=UU ==> ~INR(x)=UU" and 

0  89 

47025  90 
INL_STRICT: "INL(UU) = UU" and 
91 
INR_STRICT: "INR(UU) = UU" and 

0  92 

47025  93 
WHEN_UU: "WHEN(f,g,UU) = UU" and 
94 
WHEN_INL: "~x=UU ==> WHEN(f,g,INL(x)) = f(x)" and 

95 
WHEN_INR: "~x=UU ==> WHEN(f,g,INR(x)) = g(x)" and 

0  96 

17248  97 
SUM_EXHAUSTION: 
0  98 
"z = UU  (EX x. ~x=UU & z = INL(x))  (EX y. ~y=UU & z = INR(y))" 
99 

47025  100 
axiomatization where 
0  101 
(** VOID **) 
102 

17248  103 
void_cases: "(x::void) = UU" 
0  104 

105 
(** INDUCTION **) 

106 

47025  107 
axiomatization where 
17248  108 
induct: "[ adm(P); P(UU); ALL x. P(x) > P(f(x)) ] ==> P(FIX(f))" 
0  109 

47025  110 
axiomatization where 
0  111 
(** Admissibility / Chain Completeness **) 
112 
(* All rules can be found on pages 199200 of Larry's LCF book. 

113 
Note that "easiness" of types is not taken into account 

114 
because it cannot be expressed schematically; flatness could be. *) 

115 

47025  116 
adm_less: "\<And>t u. adm(%x. t(x) << u(x))" and 
117 
adm_not_less: "\<And>t u. adm(%x.~ t(x) << u)" and 

118 
adm_not_free: "\<And>A. adm(%x. A)" and 

119 
adm_subst: "\<And>P t. adm(P) ==> adm(%x. P(t(x)))" and 

120 
adm_conj: "\<And>P Q. [ adm(P); adm(Q) ] ==> adm(%x. P(x)&Q(x))" and 

121 
adm_disj: "\<And>P Q. [ adm(P); adm(Q) ] ==> adm(%x. P(x)Q(x))" and 

122 
adm_imp: "\<And>P Q. [ adm(%x.~P(x)); adm(Q) ] ==> adm(%x. P(x)>Q(x))" and 

123 
adm_all: "\<And>P. (!!y. adm(P(y))) ==> adm(%x. ALL y. P(y,x))" 

17248  124 

19757  125 

126 
lemma eq_imp_less1: "x = y ==> x << y" 

127 
by (simp add: eq_def) 

128 

129 
lemma eq_imp_less2: "x = y ==> y << x" 

130 
by (simp add: eq_def) 

131 

132 
lemma less_refl [simp]: "x << x" 

133 
apply (rule eq_imp_less1) 

134 
apply (rule refl) 

135 
done 

136 

137 
lemma less_anti_sym: "[ x << y; y << x ] ==> x=y" 

138 
by (simp add: eq_def) 

139 

140 
lemma ext: "(!!x::'a::cpo. f(x)=(g(x)::'b::cpo)) ==> (%x. f(x))=(%x. g(x))" 

141 
apply (rule less_anti_sym) 

142 
apply (rule less_ext) 

143 
apply simp 

144 
apply simp 

145 
done 

146 

147 
lemma cong: "[ f=g; x=y ] ==> f(x)=g(y)" 

148 
by simp 

149 

150 
lemma less_ap_term: "x << y ==> f(x) << f(y)" 

151 
by (rule less_refl [THEN mono]) 

152 

153 
lemma less_ap_thm: "f << g ==> f(x) << g(x)" 

154 
by (rule less_refl [THEN [2] mono]) 

155 

156 
lemma ap_term: "(x::'a::cpo) = y ==> (f(x)::'b::cpo) = f(y)" 

157 
apply (rule cong [OF refl]) 

158 
apply simp 

159 
done 

160 

161 
lemma ap_thm: "f = g ==> f(x) = g(x)" 

162 
apply (erule cong) 

163 
apply (rule refl) 

164 
done 

165 

166 

167 
lemma UU_abs: "(%x::'a::cpo. UU) = UU" 

168 
apply (rule less_anti_sym) 

169 
prefer 2 

170 
apply (rule minimal) 

171 
apply (rule less_ext) 

172 
apply (rule allI) 

173 
apply (rule minimal) 

174 
done 

175 

176 
lemma UU_app: "UU(x) = UU" 

177 
by (rule UU_abs [symmetric, THEN ap_thm]) 

178 

179 
lemma less_UU: "x << UU ==> x=UU" 

180 
apply (rule less_anti_sym) 

181 
apply assumption 

182 
apply (rule minimal) 

183 
done 

17248  184 

19757  185 
lemma tr_induct: "[ P(UU); P(TT); P(FF) ] ==> ALL b. P(b)" 
186 
apply (rule allI) 

187 
apply (rule mp) 

188 
apply (rule_tac [2] p = b in tr_cases) 

189 
apply blast 

190 
done 

191 

192 
lemma Contrapos: "~ B ==> (A ==> B) ==> ~A" 

193 
by blast 

194 

195 
lemma not_less_imp_not_eq1: "~ x << y \<Longrightarrow> x \<noteq> y" 

196 
apply (erule Contrapos) 

197 
apply simp 

198 
done 

199 

200 
lemma not_less_imp_not_eq2: "~ y << x \<Longrightarrow> x \<noteq> y" 

201 
apply (erule Contrapos) 

202 
apply simp 

203 
done 

204 

205 
lemma not_UU_eq_TT: "UU \<noteq> TT" 

206 
by (rule not_less_imp_not_eq2) (rule not_TT_less_UU) 

207 
lemma not_UU_eq_FF: "UU \<noteq> FF" 

208 
by (rule not_less_imp_not_eq2) (rule not_FF_less_UU) 

209 
lemma not_TT_eq_UU: "TT \<noteq> UU" 

210 
by (rule not_less_imp_not_eq1) (rule not_TT_less_UU) 

211 
lemma not_TT_eq_FF: "TT \<noteq> FF" 

212 
by (rule not_less_imp_not_eq1) (rule not_TT_less_FF) 

213 
lemma not_FF_eq_UU: "FF \<noteq> UU" 

214 
by (rule not_less_imp_not_eq1) (rule not_FF_less_UU) 

215 
lemma not_FF_eq_TT: "FF \<noteq> TT" 

216 
by (rule not_less_imp_not_eq1) (rule not_FF_less_TT) 

217 

218 

219 
lemma COND_cases_iff [rule_format]: 

220 
"ALL b. P(b=>xy) <> (b=UU>P(UU)) & (b=TT>P(x)) & (b=FF>P(y))" 

221 
apply (insert not_UU_eq_TT not_UU_eq_FF not_TT_eq_UU 

222 
not_TT_eq_FF not_FF_eq_UU not_FF_eq_TT) 

223 
apply (rule tr_induct) 

224 
apply (simplesubst COND_UU) 

225 
apply blast 

226 
apply (simplesubst COND_TT) 

227 
apply blast 

228 
apply (simplesubst COND_FF) 

229 
apply blast 

230 
done 

231 

232 
lemma COND_cases: 

233 
"[ x = UU > P(UU); x = TT > P(xa); x = FF > P(y) ] ==> P(x => xa  y)" 

234 
apply (rule COND_cases_iff [THEN iffD2]) 

235 
apply blast 

236 
done 

237 

238 
lemmas [simp] = 

239 
minimal 

240 
UU_app 

241 
UU_app [THEN ap_thm] 

242 
UU_app [THEN ap_thm, THEN ap_thm] 

243 
not_TT_less_FF not_FF_less_TT not_TT_less_UU not_FF_less_UU not_UU_eq_TT 

244 
not_UU_eq_FF not_TT_eq_UU not_TT_eq_FF not_FF_eq_UU not_FF_eq_TT 

245 
COND_UU COND_TT COND_FF 

246 
surj_pairing FST SND 

17248  247 

248 

249 
subsection {* Ordered pairs and products *} 

250 

19757  251 
lemma expand_all_PROD: "(ALL p. P(p)) <> (ALL x y. P(<x,y>))" 
252 
apply (rule iffI) 

253 
apply blast 

254 
apply (rule allI) 

255 
apply (rule surj_pairing [THEN subst]) 

256 
apply blast 

257 
done 

258 

259 
lemma PROD_less: "(p::'a*'b) << q <> FST(p) << FST(q) & SND(p) << SND(q)" 

260 
apply (rule iffI) 

261 
apply (rule conjI) 

262 
apply (erule less_ap_term) 

263 
apply (erule less_ap_term) 

264 
apply (erule conjE) 

265 
apply (rule surj_pairing [of p, THEN subst]) 

266 
apply (rule surj_pairing [of q, THEN subst]) 

267 
apply (rule mono, erule less_ap_term, assumption) 

268 
done 

269 

270 
lemma PROD_eq: "p=q <> FST(p)=FST(q) & SND(p)=SND(q)" 

271 
apply (rule iffI) 

272 
apply simp 

273 
apply (unfold eq_def) 

274 
apply (simp add: PROD_less) 

275 
done 

276 

277 
lemma PAIR_less [simp]: "<a,b> << <c,d> <> a<<c & b<<d" 

278 
by (simp add: PROD_less) 

279 

280 
lemma PAIR_eq [simp]: "<a,b> = <c,d> <> a=c & b=d" 

281 
by (simp add: PROD_eq) 

282 

283 
lemma UU_is_UU_UU [simp]: "<UU,UU> = UU" 

284 
by (rule less_UU) (simp add: PROD_less) 

285 

286 
lemma FST_STRICT [simp]: "FST(UU) = UU" 

287 
apply (rule subst [OF UU_is_UU_UU]) 

288 
apply (simp del: UU_is_UU_UU) 

289 
done 

290 

291 
lemma SND_STRICT [simp]: "SND(UU) = UU" 

292 
apply (rule subst [OF UU_is_UU_UU]) 

293 
apply (simp del: UU_is_UU_UU) 

294 
done 

17248  295 

296 

297 
subsection {* Fixedpoint theory *} 

298 

19757  299 
lemma adm_eq: "adm(%x. t(x)=(u(x)::'a::cpo))" 
300 
apply (unfold eq_def) 

301 
apply (rule adm_conj adm_less)+ 

302 
done 

303 

304 
lemma adm_not_not: "adm(P) ==> adm(%x.~~P(x))" 

305 
by simp 

306 

307 
lemma not_eq_TT: "ALL p. ~p=TT <> (p=FF  p=UU)" 

308 
and not_eq_FF: "ALL p. ~p=FF <> (p=TT  p=UU)" 

309 
and not_eq_UU: "ALL p. ~p=UU <> (p=TT  p=FF)" 

310 
by (rule tr_induct, simp_all)+ 

311 

312 
lemma adm_not_eq_tr: "ALL p::tr. adm(%x. ~t(x)=p)" 

313 
apply (rule tr_induct) 

314 
apply (simp_all add: not_eq_TT not_eq_FF not_eq_UU) 

315 
apply (rule adm_disj adm_eq)+ 

316 
done 

317 

318 
lemmas adm_lemmas = 

319 
adm_not_free adm_eq adm_less adm_not_less 

320 
adm_not_eq_tr adm_conj adm_disj adm_imp adm_all 

321 

322 

323 
ML {* 

27208
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
22810
diff
changeset

324 
fun induct_tac ctxt v i = 
27239  325 
res_inst_tac ctxt [(("f", 0), v)] @{thm induct} i THEN 
22810  326 
REPEAT (resolve_tac @{thms adm_lemmas} i) 
19757  327 
*} 
328 

329 
lemma least_FIX: "f(p) = p ==> FIX(f) << p" 

27208
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
22810
diff
changeset

330 
apply (tactic {* induct_tac @{context} "f" 1 *}) 
19757  331 
apply (rule minimal) 
332 
apply (intro strip) 

333 
apply (erule subst) 

334 
apply (erule less_ap_term) 

335 
done 

336 

337 
lemma lfp_is_FIX: 

338 
assumes 1: "f(p) = p" 

339 
and 2: "ALL q. f(q)=q > p << q" 

340 
shows "p = FIX(f)" 

341 
apply (rule less_anti_sym) 

342 
apply (rule 2 [THEN spec, THEN mp]) 

343 
apply (rule FIX_eq) 

344 
apply (rule least_FIX) 

345 
apply (rule 1) 

346 
done 

347 

348 

349 
lemma FIX_pair: "<FIX(f),FIX(g)> = FIX(%p.<f(FST(p)),g(SND(p))>)" 

350 
apply (rule lfp_is_FIX) 

351 
apply (simp add: FIX_eq [of f] FIX_eq [of g]) 

352 
apply (intro strip) 

353 
apply (simp add: PROD_less) 

354 
apply (rule conjI) 

355 
apply (rule least_FIX) 

356 
apply (erule subst, rule FST [symmetric]) 

357 
apply (rule least_FIX) 

358 
apply (erule subst, rule SND [symmetric]) 

359 
done 

360 

361 
lemma FIX1: "FIX(f) = FST(FIX(%p. <f(FST(p)),g(SND(p))>))" 

362 
by (rule FIX_pair [unfolded PROD_eq FST SND, THEN conjunct1]) 

363 

364 
lemma FIX2: "FIX(g) = SND(FIX(%p. <f(FST(p)),g(SND(p))>))" 

365 
by (rule FIX_pair [unfolded PROD_eq FST SND, THEN conjunct2]) 

366 

367 
lemma induct2: 

368 
assumes 1: "adm(%p. P(FST(p),SND(p)))" 

369 
and 2: "P(UU::'a,UU::'b)" 

370 
and 3: "ALL x y. P(x,y) > P(f(x),g(y))" 

371 
shows "P(FIX(f),FIX(g))" 

372 
apply (rule FIX1 [THEN ssubst, of _ f g]) 

373 
apply (rule FIX2 [THEN ssubst, of _ f g]) 

19758  374 
apply (rule induct [where ?f = "%x. <f(FST(x)),g(SND(x))>"]) 
375 
apply (rule 1) 

19757  376 
apply simp 
377 
apply (rule 2) 

378 
apply (simp add: expand_all_PROD) 

379 
apply (rule 3) 

380 
done 

381 

382 
ML {* 

27208
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
22810
diff
changeset

383 
fun induct2_tac ctxt (f, g) i = 
27239  384 
res_inst_tac ctxt [(("f", 0), f), (("g", 0), g)] @{thm induct2} i THEN 
22810  385 
REPEAT(resolve_tac @{thms adm_lemmas} i) 
19757  386 
*} 
387 

388 
end 