author | wenzelm |
Fri, 17 Dec 2010 20:21:35 +0100 | |
changeset 41253 | 42f24340ae53 |
parent 36452 | d37c6eed8117 |
child 41310 | 65631ca437c9 |
permissions | -rw-r--r-- |
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 First-Order 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 |
|
35128 | 21 |
typedecl ('a,'b) "*" (infixl "*" 6) |
22 |
typedecl ('a,'b) "+" (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 |
17248 | 26 |
"*" :: (cpo, cpo) cpo |
27 |
"+" :: (cpo, cpo) cpo |
|
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 |
|
47 |
axioms |
|
0 | 48 |
(** DOMAIN THEORY **) |
49 |
||
17248 | 50 |
eq_def: "x=y == x << y & y << x" |
0 | 51 |
|
17248 | 52 |
less_trans: "[| x << y; y << z |] ==> x << z" |
0 | 53 |
|
17248 | 54 |
less_ext: "(ALL x. f(x) << g(x)) ==> f << g" |
0 | 55 |
|
17248 | 56 |
mono: "[| f << g; x << y |] ==> f(x) << g(y)" |
0 | 57 |
|
17248 | 58 |
minimal: "UU << x" |
0 | 59 |
|
17248 | 60 |
FIX_eq: "f(FIX(f)) = FIX(f)" |
0 | 61 |
|
62 |
(** TR **) |
|
63 |
||
17248 | 64 |
tr_cases: "p=UU | p=TT | p=FF" |
0 | 65 |
|
17248 | 66 |
not_TT_less_FF: "~ TT << FF" |
67 |
not_FF_less_TT: "~ FF << TT" |
|
68 |
not_TT_less_UU: "~ TT << UU" |
|
69 |
not_FF_less_UU: "~ FF << UU" |
|
0 | 70 |
|
17248 | 71 |
COND_UU: "UU => x | y = UU" |
72 |
COND_TT: "TT => x | y = x" |
|
73 |
COND_FF: "FF => x | y = y" |
|
0 | 74 |
|
75 |
(** PAIRS **) |
|
76 |
||
17248 | 77 |
surj_pairing: "<FST(z),SND(z)> = z" |
0 | 78 |
|
17248 | 79 |
FST: "FST(<x,y>) = x" |
80 |
SND: "SND(<x,y>) = y" |
|
0 | 81 |
|
82 |
(*** STRICT SUM ***) |
|
83 |
||
17248 | 84 |
INL_DEF: "~x=UU ==> ~INL(x)=UU" |
85 |
INR_DEF: "~x=UU ==> ~INR(x)=UU" |
|
0 | 86 |
|
17248 | 87 |
INL_STRICT: "INL(UU) = UU" |
88 |
INR_STRICT: "INR(UU) = UU" |
|
0 | 89 |
|
17248 | 90 |
WHEN_UU: "WHEN(f,g,UU) = UU" |
91 |
WHEN_INL: "~x=UU ==> WHEN(f,g,INL(x)) = f(x)" |
|
92 |
WHEN_INR: "~x=UU ==> WHEN(f,g,INR(x)) = g(x)" |
|
0 | 93 |
|
17248 | 94 |
SUM_EXHAUSTION: |
0 | 95 |
"z = UU | (EX x. ~x=UU & z = INL(x)) | (EX y. ~y=UU & z = INR(y))" |
96 |
||
97 |
(** VOID **) |
|
98 |
||
17248 | 99 |
void_cases: "(x::void) = UU" |
0 | 100 |
|
101 |
(** INDUCTION **) |
|
102 |
||
17248 | 103 |
induct: "[| adm(P); P(UU); ALL x. P(x) --> P(f(x)) |] ==> P(FIX(f))" |
0 | 104 |
|
105 |
(** Admissibility / Chain Completeness **) |
|
106 |
(* All rules can be found on pages 199--200 of Larry's LCF book. |
|
107 |
Note that "easiness" of types is not taken into account |
|
108 |
because it cannot be expressed schematically; flatness could be. *) |
|
109 |
||
17248 | 110 |
adm_less: "adm(%x. t(x) << u(x))" |
111 |
adm_not_less: "adm(%x.~ t(x) << u)" |
|
112 |
adm_not_free: "adm(%x. A)" |
|
113 |
adm_subst: "adm(P) ==> adm(%x. P(t(x)))" |
|
114 |
adm_conj: "[| adm(P); adm(Q) |] ==> adm(%x. P(x)&Q(x))" |
|
115 |
adm_disj: "[| adm(P); adm(Q) |] ==> adm(%x. P(x)|Q(x))" |
|
116 |
adm_imp: "[| adm(%x.~P(x)); adm(Q) |] ==> adm(%x. P(x)-->Q(x))" |
|
117 |
adm_all: "(!!y. adm(P(y))) ==> adm(%x. ALL y. P(y,x))" |
|
118 |
||
19757 | 119 |
|
120 |
lemma eq_imp_less1: "x = y ==> x << y" |
|
121 |
by (simp add: eq_def) |
|
122 |
||
123 |
lemma eq_imp_less2: "x = y ==> y << x" |
|
124 |
by (simp add: eq_def) |
|
125 |
||
126 |
lemma less_refl [simp]: "x << x" |
|
127 |
apply (rule eq_imp_less1) |
|
128 |
apply (rule refl) |
|
129 |
done |
|
130 |
||
131 |
lemma less_anti_sym: "[| x << y; y << x |] ==> x=y" |
|
132 |
by (simp add: eq_def) |
|
133 |
||
134 |
lemma ext: "(!!x::'a::cpo. f(x)=(g(x)::'b::cpo)) ==> (%x. f(x))=(%x. g(x))" |
|
135 |
apply (rule less_anti_sym) |
|
136 |
apply (rule less_ext) |
|
137 |
apply simp |
|
138 |
apply simp |
|
139 |
done |
|
140 |
||
141 |
lemma cong: "[| f=g; x=y |] ==> f(x)=g(y)" |
|
142 |
by simp |
|
143 |
||
144 |
lemma less_ap_term: "x << y ==> f(x) << f(y)" |
|
145 |
by (rule less_refl [THEN mono]) |
|
146 |
||
147 |
lemma less_ap_thm: "f << g ==> f(x) << g(x)" |
|
148 |
by (rule less_refl [THEN [2] mono]) |
|
149 |
||
150 |
lemma ap_term: "(x::'a::cpo) = y ==> (f(x)::'b::cpo) = f(y)" |
|
151 |
apply (rule cong [OF refl]) |
|
152 |
apply simp |
|
153 |
done |
|
154 |
||
155 |
lemma ap_thm: "f = g ==> f(x) = g(x)" |
|
156 |
apply (erule cong) |
|
157 |
apply (rule refl) |
|
158 |
done |
|
159 |
||
160 |
||
161 |
lemma UU_abs: "(%x::'a::cpo. UU) = UU" |
|
162 |
apply (rule less_anti_sym) |
|
163 |
prefer 2 |
|
164 |
apply (rule minimal) |
|
165 |
apply (rule less_ext) |
|
166 |
apply (rule allI) |
|
167 |
apply (rule minimal) |
|
168 |
done |
|
169 |
||
170 |
lemma UU_app: "UU(x) = UU" |
|
171 |
by (rule UU_abs [symmetric, THEN ap_thm]) |
|
172 |
||
173 |
lemma less_UU: "x << UU ==> x=UU" |
|
174 |
apply (rule less_anti_sym) |
|
175 |
apply assumption |
|
176 |
apply (rule minimal) |
|
177 |
done |
|
17248 | 178 |
|
19757 | 179 |
lemma tr_induct: "[| P(UU); P(TT); P(FF) |] ==> ALL b. P(b)" |
180 |
apply (rule allI) |
|
181 |
apply (rule mp) |
|
182 |
apply (rule_tac [2] p = b in tr_cases) |
|
183 |
apply blast |
|
184 |
done |
|
185 |
||
186 |
lemma Contrapos: "~ B ==> (A ==> B) ==> ~A" |
|
187 |
by blast |
|
188 |
||
189 |
lemma not_less_imp_not_eq1: "~ x << y \<Longrightarrow> x \<noteq> y" |
|
190 |
apply (erule Contrapos) |
|
191 |
apply simp |
|
192 |
done |
|
193 |
||
194 |
lemma not_less_imp_not_eq2: "~ y << x \<Longrightarrow> x \<noteq> y" |
|
195 |
apply (erule Contrapos) |
|
196 |
apply simp |
|
197 |
done |
|
198 |
||
199 |
lemma not_UU_eq_TT: "UU \<noteq> TT" |
|
200 |
by (rule not_less_imp_not_eq2) (rule not_TT_less_UU) |
|
201 |
lemma not_UU_eq_FF: "UU \<noteq> FF" |
|
202 |
by (rule not_less_imp_not_eq2) (rule not_FF_less_UU) |
|
203 |
lemma not_TT_eq_UU: "TT \<noteq> UU" |
|
204 |
by (rule not_less_imp_not_eq1) (rule not_TT_less_UU) |
|
205 |
lemma not_TT_eq_FF: "TT \<noteq> FF" |
|
206 |
by (rule not_less_imp_not_eq1) (rule not_TT_less_FF) |
|
207 |
lemma not_FF_eq_UU: "FF \<noteq> UU" |
|
208 |
by (rule not_less_imp_not_eq1) (rule not_FF_less_UU) |
|
209 |
lemma not_FF_eq_TT: "FF \<noteq> TT" |
|
210 |
by (rule not_less_imp_not_eq1) (rule not_FF_less_TT) |
|
211 |
||
212 |
||
213 |
lemma COND_cases_iff [rule_format]: |
|
214 |
"ALL b. P(b=>x|y) <-> (b=UU-->P(UU)) & (b=TT-->P(x)) & (b=FF-->P(y))" |
|
215 |
apply (insert not_UU_eq_TT not_UU_eq_FF not_TT_eq_UU |
|
216 |
not_TT_eq_FF not_FF_eq_UU not_FF_eq_TT) |
|
217 |
apply (rule tr_induct) |
|
218 |
apply (simplesubst COND_UU) |
|
219 |
apply blast |
|
220 |
apply (simplesubst COND_TT) |
|
221 |
apply blast |
|
222 |
apply (simplesubst COND_FF) |
|
223 |
apply blast |
|
224 |
done |
|
225 |
||
226 |
lemma COND_cases: |
|
227 |
"[| x = UU --> P(UU); x = TT --> P(xa); x = FF --> P(y) |] ==> P(x => xa | y)" |
|
228 |
apply (rule COND_cases_iff [THEN iffD2]) |
|
229 |
apply blast |
|
230 |
done |
|
231 |
||
232 |
lemmas [simp] = |
|
233 |
minimal |
|
234 |
UU_app |
|
235 |
UU_app [THEN ap_thm] |
|
236 |
UU_app [THEN ap_thm, THEN ap_thm] |
|
237 |
not_TT_less_FF not_FF_less_TT not_TT_less_UU not_FF_less_UU not_UU_eq_TT |
|
238 |
not_UU_eq_FF not_TT_eq_UU not_TT_eq_FF not_FF_eq_UU not_FF_eq_TT |
|
239 |
COND_UU COND_TT COND_FF |
|
240 |
surj_pairing FST SND |
|
17248 | 241 |
|
242 |
||
243 |
subsection {* Ordered pairs and products *} |
|
244 |
||
19757 | 245 |
lemma expand_all_PROD: "(ALL p. P(p)) <-> (ALL x y. P(<x,y>))" |
246 |
apply (rule iffI) |
|
247 |
apply blast |
|
248 |
apply (rule allI) |
|
249 |
apply (rule surj_pairing [THEN subst]) |
|
250 |
apply blast |
|
251 |
done |
|
252 |
||
253 |
lemma PROD_less: "(p::'a*'b) << q <-> FST(p) << FST(q) & SND(p) << SND(q)" |
|
254 |
apply (rule iffI) |
|
255 |
apply (rule conjI) |
|
256 |
apply (erule less_ap_term) |
|
257 |
apply (erule less_ap_term) |
|
258 |
apply (erule conjE) |
|
259 |
apply (rule surj_pairing [of p, THEN subst]) |
|
260 |
apply (rule surj_pairing [of q, THEN subst]) |
|
261 |
apply (rule mono, erule less_ap_term, assumption) |
|
262 |
done |
|
263 |
||
264 |
lemma PROD_eq: "p=q <-> FST(p)=FST(q) & SND(p)=SND(q)" |
|
265 |
apply (rule iffI) |
|
266 |
apply simp |
|
267 |
apply (unfold eq_def) |
|
268 |
apply (simp add: PROD_less) |
|
269 |
done |
|
270 |
||
271 |
lemma PAIR_less [simp]: "<a,b> << <c,d> <-> a<<c & b<<d" |
|
272 |
by (simp add: PROD_less) |
|
273 |
||
274 |
lemma PAIR_eq [simp]: "<a,b> = <c,d> <-> a=c & b=d" |
|
275 |
by (simp add: PROD_eq) |
|
276 |
||
277 |
lemma UU_is_UU_UU [simp]: "<UU,UU> = UU" |
|
278 |
by (rule less_UU) (simp add: PROD_less) |
|
279 |
||
280 |
lemma FST_STRICT [simp]: "FST(UU) = UU" |
|
281 |
apply (rule subst [OF UU_is_UU_UU]) |
|
282 |
apply (simp del: UU_is_UU_UU) |
|
283 |
done |
|
284 |
||
285 |
lemma SND_STRICT [simp]: "SND(UU) = UU" |
|
286 |
apply (rule subst [OF UU_is_UU_UU]) |
|
287 |
apply (simp del: UU_is_UU_UU) |
|
288 |
done |
|
17248 | 289 |
|
290 |
||
291 |
subsection {* Fixedpoint theory *} |
|
292 |
||
19757 | 293 |
lemma adm_eq: "adm(%x. t(x)=(u(x)::'a::cpo))" |
294 |
apply (unfold eq_def) |
|
295 |
apply (rule adm_conj adm_less)+ |
|
296 |
done |
|
297 |
||
298 |
lemma adm_not_not: "adm(P) ==> adm(%x.~~P(x))" |
|
299 |
by simp |
|
300 |
||
301 |
lemma not_eq_TT: "ALL p. ~p=TT <-> (p=FF | p=UU)" |
|
302 |
and not_eq_FF: "ALL p. ~p=FF <-> (p=TT | p=UU)" |
|
303 |
and not_eq_UU: "ALL p. ~p=UU <-> (p=TT | p=FF)" |
|
304 |
by (rule tr_induct, simp_all)+ |
|
305 |
||
306 |
lemma adm_not_eq_tr: "ALL p::tr. adm(%x. ~t(x)=p)" |
|
307 |
apply (rule tr_induct) |
|
308 |
apply (simp_all add: not_eq_TT not_eq_FF not_eq_UU) |
|
309 |
apply (rule adm_disj adm_eq)+ |
|
310 |
done |
|
311 |
||
312 |
lemmas adm_lemmas = |
|
313 |
adm_not_free adm_eq adm_less adm_not_less |
|
314 |
adm_not_eq_tr adm_conj adm_disj adm_imp adm_all |
|
315 |
||
316 |
||
317 |
ML {* |
|
27208
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
22810
diff
changeset
|
318 |
fun induct_tac ctxt v i = |
27239 | 319 |
res_inst_tac ctxt [(("f", 0), v)] @{thm induct} i THEN |
22810 | 320 |
REPEAT (resolve_tac @{thms adm_lemmas} i) |
19757 | 321 |
*} |
322 |
||
323 |
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
|
324 |
apply (tactic {* induct_tac @{context} "f" 1 *}) |
19757 | 325 |
apply (rule minimal) |
326 |
apply (intro strip) |
|
327 |
apply (erule subst) |
|
328 |
apply (erule less_ap_term) |
|
329 |
done |
|
330 |
||
331 |
lemma lfp_is_FIX: |
|
332 |
assumes 1: "f(p) = p" |
|
333 |
and 2: "ALL q. f(q)=q --> p << q" |
|
334 |
shows "p = FIX(f)" |
|
335 |
apply (rule less_anti_sym) |
|
336 |
apply (rule 2 [THEN spec, THEN mp]) |
|
337 |
apply (rule FIX_eq) |
|
338 |
apply (rule least_FIX) |
|
339 |
apply (rule 1) |
|
340 |
done |
|
341 |
||
342 |
||
343 |
lemma FIX_pair: "<FIX(f),FIX(g)> = FIX(%p.<f(FST(p)),g(SND(p))>)" |
|
344 |
apply (rule lfp_is_FIX) |
|
345 |
apply (simp add: FIX_eq [of f] FIX_eq [of g]) |
|
346 |
apply (intro strip) |
|
347 |
apply (simp add: PROD_less) |
|
348 |
apply (rule conjI) |
|
349 |
apply (rule least_FIX) |
|
350 |
apply (erule subst, rule FST [symmetric]) |
|
351 |
apply (rule least_FIX) |
|
352 |
apply (erule subst, rule SND [symmetric]) |
|
353 |
done |
|
354 |
||
355 |
lemma FIX1: "FIX(f) = FST(FIX(%p. <f(FST(p)),g(SND(p))>))" |
|
356 |
by (rule FIX_pair [unfolded PROD_eq FST SND, THEN conjunct1]) |
|
357 |
||
358 |
lemma FIX2: "FIX(g) = SND(FIX(%p. <f(FST(p)),g(SND(p))>))" |
|
359 |
by (rule FIX_pair [unfolded PROD_eq FST SND, THEN conjunct2]) |
|
360 |
||
361 |
lemma induct2: |
|
362 |
assumes 1: "adm(%p. P(FST(p),SND(p)))" |
|
363 |
and 2: "P(UU::'a,UU::'b)" |
|
364 |
and 3: "ALL x y. P(x,y) --> P(f(x),g(y))" |
|
365 |
shows "P(FIX(f),FIX(g))" |
|
366 |
apply (rule FIX1 [THEN ssubst, of _ f g]) |
|
367 |
apply (rule FIX2 [THEN ssubst, of _ f g]) |
|
19758 | 368 |
apply (rule induct [where ?f = "%x. <f(FST(x)),g(SND(x))>"]) |
369 |
apply (rule 1) |
|
19757 | 370 |
apply simp |
371 |
apply (rule 2) |
|
372 |
apply (simp add: expand_all_PROD) |
|
373 |
apply (rule 3) |
|
374 |
done |
|
375 |
||
376 |
ML {* |
|
27208
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
22810
diff
changeset
|
377 |
fun induct2_tac ctxt (f, g) i = |
27239 | 378 |
res_inst_tac ctxt [(("f", 0), f), (("g", 0), g)] @{thm induct2} i THEN |
22810 | 379 |
REPEAT(resolve_tac @{thms adm_lemmas} i) |
19757 | 380 |
*} |
381 |
||
382 |
end |