author | nipkow |
Thu, 26 Nov 1998 12:18:08 +0100 | |
changeset 5974 | 6acf3ff0f486 |
parent 4721 | c8a8482a8124 |
child 9248 | e1dee89de037 |
permissions | -rw-r--r-- |
896 | 1 |
(* $Id$ *) |
894 | 2 |
(* Elegant proof for continuity of fixed-point operator *) |
3 |
(* Loeckx & Sieber S.88 *) |
|
4 |
||
5 |
val prems = goalw Fix.thy [Ifix_def] |
|
3842 | 6 |
"Ifix F= lub (range (%i.%G. iterate i G UU)) F"; |
2033 | 7 |
by (stac thelub_fun 1); |
894 | 8 |
by (rtac ch2ch_fun 1); |
9 |
back(); |
|
10 |
by (rtac refl 2); |
|
4721
c8a8482a8124
renamed is_chain to chain, is_tord to tord, replaced chain_finite by chfin
oheimb
parents:
3842
diff
changeset
|
11 |
by (rtac chainI 1); |
894 | 12 |
by (strip_tac 1); |
13 |
by (rtac (less_fun RS iffD2) 1); |
|
14 |
by (strip_tac 1); |
|
15 |
by (rtac (less_fun RS iffD2) 1); |
|
16 |
by (strip_tac 1); |
|
4721
c8a8482a8124
renamed is_chain to chain, is_tord to tord, replaced chain_finite by chfin
oheimb
parents:
3842
diff
changeset
|
17 |
by (rtac (chain_iterate RS chainE RS spec) 1); |
894 | 18 |
val loeckx_sieber = result(); |
19 |
||
20 |
(* |
|
21 |
||
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
896
diff
changeset
|
22 |
Idea: (%i.%G.iterate i G UU) is a chain of continuous functions and |
894 | 23 |
Ifix is the lub of this chain. Hence Ifix is continuous. |
24 |
||
25 |
----- The proof in HOLCF ----------------------- |
|
26 |
||
27 |
Since we already proved the theorem |
|
28 |
||
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
896
diff
changeset
|
29 |
val cont_lubcfun = prove_goal Cfun2.thy |
4721
c8a8482a8124
renamed is_chain to chain, is_tord to tord, replaced chain_finite by chfin
oheimb
parents:
3842
diff
changeset
|
30 |
"chain ?F ==> cont (%x. lub (range (%j. ?F j`x)))" |
894 | 31 |
|
32 |
||
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
896
diff
changeset
|
33 |
it suffices to prove: |
894 | 34 |
|
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
896
diff
changeset
|
35 |
Ifix = (%f.lub (range (%j. (LAM f. iterate j f UU)`f))) |
894 | 36 |
|
37 |
and |
|
38 |
||
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
896
diff
changeset
|
39 |
cont (%f.lub (range (%j. (LAM f. iterate j f UU)`f))) |
894 | 40 |
|
41 |
Note that if we use the term |
|
42 |
||
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
896
diff
changeset
|
43 |
%i.%G.iterate i G UU instead of (%j.(LAM f. iterate j f UU)) |
894 | 44 |
|
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
896
diff
changeset
|
45 |
we cannot use the theorem cont_lubcfun |
894 | 46 |
|
47 |
*) |
|
48 |
||
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
896
diff
changeset
|
49 |
val prems = goal Fix.thy "cont(Ifix)"; |
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
896
diff
changeset
|
50 |
by (res_inst_tac |
3842 | 51 |
[("t","Ifix"),("s","(%f. lub(range(%j.(LAM f. iterate j f UU)`f)))")] |
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
896
diff
changeset
|
52 |
ssubst 1); |
894 | 53 |
by (rtac ext 1); |
1461 | 54 |
by (rewtac Ifix_def ); |
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
896
diff
changeset
|
55 |
by (subgoal_tac |
3842 | 56 |
"range(% i. iterate i f UU) = range(%j.(LAM f. iterate j f UU)`f)" 1); |
894 | 57 |
by (etac arg_cong 1); |
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
896
diff
changeset
|
58 |
by (subgoal_tac |
3842 | 59 |
"(% i. iterate i f UU) = (%j.(LAM f. iterate j f UU)`f)" 1); |
894 | 60 |
by (etac arg_cong 1); |
61 |
by (rtac ext 1); |
|
2033 | 62 |
by (stac beta_cfun 1); |
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
896
diff
changeset
|
63 |
by (rtac cont2cont_CF1L 1); |
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
896
diff
changeset
|
64 |
by (rtac cont_iterate 1); |
894 | 65 |
by (rtac refl 1); |
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
896
diff
changeset
|
66 |
by (rtac cont_lubcfun 1); |
4721
c8a8482a8124
renamed is_chain to chain, is_tord to tord, replaced chain_finite by chfin
oheimb
parents:
3842
diff
changeset
|
67 |
by (rtac chainI 1); |
894 | 68 |
by (strip_tac 1); |
69 |
by (rtac less_cfun2 1); |
|
2033 | 70 |
by (stac beta_cfun 1); |
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
896
diff
changeset
|
71 |
by (rtac cont2cont_CF1L 1); |
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
896
diff
changeset
|
72 |
by (rtac cont_iterate 1); |
2033 | 73 |
by (stac beta_cfun 1); |
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
896
diff
changeset
|
74 |
by (rtac cont2cont_CF1L 1); |
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
896
diff
changeset
|
75 |
by (rtac cont_iterate 1); |
4721
c8a8482a8124
renamed is_chain to chain, is_tord to tord, replaced chain_finite by chfin
oheimb
parents:
3842
diff
changeset
|
76 |
by (rtac (chain_iterate RS chainE RS spec) 1); |
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
896
diff
changeset
|
77 |
val cont_Ifix2 = result(); |
894 | 78 |
|
79 |
(* the proof in little steps *) |
|
80 |
||
81 |
val prems = goal Fix.thy |
|
3842 | 82 |
"(% i. iterate i f UU) = (%j.(LAM f. iterate j f UU)`f)"; |
894 | 83 |
by (rtac ext 1); |
2033 | 84 |
by (stac beta_cfun 1); |
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
896
diff
changeset
|
85 |
by (rtac cont2cont_CF1L 1); |
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
896
diff
changeset
|
86 |
by (rtac cont_iterate 1); |
894 | 87 |
by (rtac refl 1); |
88 |
val fix_lemma1 = result(); |
|
89 |
||
90 |
val prems = goal Fix.thy |
|
3842 | 91 |
" Ifix = (%f. lub(range(%j.(LAM f. iterate j f UU)`f)))"; |
894 | 92 |
by (rtac ext 1); |
1461 | 93 |
by (rewtac Ifix_def ); |
2033 | 94 |
by (stac fix_lemma1 1); |
894 | 95 |
by (rtac refl 1); |
96 |
val fix_lemma2 = result(); |
|
97 |
||
98 |
(* |
|
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
896
diff
changeset
|
99 |
- cont_lubcfun; |
4721
c8a8482a8124
renamed is_chain to chain, is_tord to tord, replaced chain_finite by chfin
oheimb
parents:
3842
diff
changeset
|
100 |
val it = "chain ?F ==> cont (%x. lub (range (%j. ?F j`x)))" : thm |
894 | 101 |
|
102 |
*) |
|
103 |
||
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
896
diff
changeset
|
104 |
val prems = goal Fix.thy "cont Ifix"; |
2033 | 105 |
by (stac fix_lemma2 1); |
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
896
diff
changeset
|
106 |
by (rtac cont_lubcfun 1); |
4721
c8a8482a8124
renamed is_chain to chain, is_tord to tord, replaced chain_finite by chfin
oheimb
parents:
3842
diff
changeset
|
107 |
by (rtac chainI 1); |
894 | 108 |
by (strip_tac 1); |
109 |
by (rtac less_cfun2 1); |
|
2033 | 110 |
by (stac beta_cfun 1); |
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
896
diff
changeset
|
111 |
by (rtac cont2cont_CF1L 1); |
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
896
diff
changeset
|
112 |
by (rtac cont_iterate 1); |
2033 | 113 |
by (stac beta_cfun 1); |
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
896
diff
changeset
|
114 |
by (rtac cont2cont_CF1L 1); |
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
896
diff
changeset
|
115 |
by (rtac cont_iterate 1); |
4721
c8a8482a8124
renamed is_chain to chain, is_tord to tord, replaced chain_finite by chfin
oheimb
parents:
3842
diff
changeset
|
116 |
by (rtac (chain_iterate RS chainE RS spec) 1); |
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
896
diff
changeset
|
117 |
val cont_Ifix2 = result(); |
894 | 118 |