6 "Ifix F= lub (range (%i.%G. iterate i G UU)) F"; |
6 "Ifix F= lub (range (%i.%G. iterate i G UU)) F"; |
7 by (stac thelub_fun 1); |
7 by (stac thelub_fun 1); |
8 by (rtac ch2ch_fun 1); |
8 by (rtac ch2ch_fun 1); |
9 back(); |
9 back(); |
10 by (rtac refl 2); |
10 by (rtac refl 2); |
11 by (rtac is_chainI 1); |
11 by (rtac chainI 1); |
12 by (strip_tac 1); |
12 by (strip_tac 1); |
13 by (rtac (less_fun RS iffD2) 1); |
13 by (rtac (less_fun RS iffD2) 1); |
14 by (strip_tac 1); |
14 by (strip_tac 1); |
15 by (rtac (less_fun RS iffD2) 1); |
15 by (rtac (less_fun RS iffD2) 1); |
16 by (strip_tac 1); |
16 by (strip_tac 1); |
17 by (rtac (is_chain_iterate RS is_chainE RS spec) 1); |
17 by (rtac (chain_iterate RS chainE RS spec) 1); |
18 val loeckx_sieber = result(); |
18 val loeckx_sieber = result(); |
19 |
19 |
20 (* |
20 (* |
21 |
21 |
22 Idea: (%i.%G.iterate i G UU) is a chain of continuous functions and |
22 Idea: (%i.%G.iterate i G UU) is a chain of continuous functions and |
25 ----- The proof in HOLCF ----------------------- |
25 ----- The proof in HOLCF ----------------------- |
26 |
26 |
27 Since we already proved the theorem |
27 Since we already proved the theorem |
28 |
28 |
29 val cont_lubcfun = prove_goal Cfun2.thy |
29 val cont_lubcfun = prove_goal Cfun2.thy |
30 "is_chain ?F ==> cont (%x. lub (range (%j. ?F j`x)))" |
30 "chain ?F ==> cont (%x. lub (range (%j. ?F j`x)))" |
31 |
31 |
32 |
32 |
33 it suffices to prove: |
33 it suffices to prove: |
34 |
34 |
35 Ifix = (%f.lub (range (%j. (LAM f. iterate j f UU)`f))) |
35 Ifix = (%f.lub (range (%j. (LAM f. iterate j f UU)`f))) |
62 by (stac beta_cfun 1); |
62 by (stac beta_cfun 1); |
63 by (rtac cont2cont_CF1L 1); |
63 by (rtac cont2cont_CF1L 1); |
64 by (rtac cont_iterate 1); |
64 by (rtac cont_iterate 1); |
65 by (rtac refl 1); |
65 by (rtac refl 1); |
66 by (rtac cont_lubcfun 1); |
66 by (rtac cont_lubcfun 1); |
67 by (rtac is_chainI 1); |
67 by (rtac chainI 1); |
68 by (strip_tac 1); |
68 by (strip_tac 1); |
69 by (rtac less_cfun2 1); |
69 by (rtac less_cfun2 1); |
70 by (stac beta_cfun 1); |
70 by (stac beta_cfun 1); |
71 by (rtac cont2cont_CF1L 1); |
71 by (rtac cont2cont_CF1L 1); |
72 by (rtac cont_iterate 1); |
72 by (rtac cont_iterate 1); |
73 by (stac beta_cfun 1); |
73 by (stac beta_cfun 1); |
74 by (rtac cont2cont_CF1L 1); |
74 by (rtac cont2cont_CF1L 1); |
75 by (rtac cont_iterate 1); |
75 by (rtac cont_iterate 1); |
76 by (rtac (is_chain_iterate RS is_chainE RS spec) 1); |
76 by (rtac (chain_iterate RS chainE RS spec) 1); |
77 val cont_Ifix2 = result(); |
77 val cont_Ifix2 = result(); |
78 |
78 |
79 (* the proof in little steps *) |
79 (* the proof in little steps *) |
80 |
80 |
81 val prems = goal Fix.thy |
81 val prems = goal Fix.thy |
95 by (rtac refl 1); |
95 by (rtac refl 1); |
96 val fix_lemma2 = result(); |
96 val fix_lemma2 = result(); |
97 |
97 |
98 (* |
98 (* |
99 - cont_lubcfun; |
99 - cont_lubcfun; |
100 val it = "is_chain ?F ==> cont (%x. lub (range (%j. ?F j`x)))" : thm |
100 val it = "chain ?F ==> cont (%x. lub (range (%j. ?F j`x)))" : thm |
101 |
101 |
102 *) |
102 *) |
103 |
103 |
104 val prems = goal Fix.thy "cont Ifix"; |
104 val prems = goal Fix.thy "cont Ifix"; |
105 by (stac fix_lemma2 1); |
105 by (stac fix_lemma2 1); |
106 by (rtac cont_lubcfun 1); |
106 by (rtac cont_lubcfun 1); |
107 by (rtac is_chainI 1); |
107 by (rtac chainI 1); |
108 by (strip_tac 1); |
108 by (strip_tac 1); |
109 by (rtac less_cfun2 1); |
109 by (rtac less_cfun2 1); |
110 by (stac beta_cfun 1); |
110 by (stac beta_cfun 1); |
111 by (rtac cont2cont_CF1L 1); |
111 by (rtac cont2cont_CF1L 1); |
112 by (rtac cont_iterate 1); |
112 by (rtac cont_iterate 1); |
113 by (stac beta_cfun 1); |
113 by (stac beta_cfun 1); |
114 by (rtac cont2cont_CF1L 1); |
114 by (rtac cont2cont_CF1L 1); |
115 by (rtac cont_iterate 1); |
115 by (rtac cont_iterate 1); |
116 by (rtac (is_chain_iterate RS is_chainE RS spec) 1); |
116 by (rtac (chain_iterate RS chainE RS spec) 1); |
117 val cont_Ifix2 = result(); |
117 val cont_Ifix2 = result(); |
118 |
118 |