author | regensbu |
Thu, 29 Jun 1995 16:28:40 +0200 | |
changeset 1168 | 74be52691d62 |
parent 896 | 56b9c2626e81 |
child 1461 | 6bcb44e4d6e5 |
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] |
|
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
896
diff
changeset
|
6 |
"Ifix F= lub (range (%i.%G.iterate i G UU)) F"; |
894 | 7 |
by (rtac (thelub_fun RS ssubst) 1); |
8 |
by (rtac ch2ch_fun 1); |
|
9 |
back(); |
|
10 |
by (rtac refl 2); |
|
11 |
by (rtac is_chainI 1); |
|
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); |
|
17 |
by (rtac (is_chain_iterate RS is_chainE RS spec) 1); |
|
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 |
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
896
diff
changeset
|
30 |
"is_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 |
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
896
diff
changeset
|
51 |
[("t","Ifix"),("s","(%f.lub(range(%j.(LAM f. iterate j f UU)`f)))")] |
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); |
54 |
by (rewrite_goals_tac [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 |
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
896
diff
changeset
|
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 |
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
896
diff
changeset
|
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); |
|
62 |
by (rtac (beta_cfun RS ssubst) 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); |
894 | 67 |
by (rtac is_chainI 1); |
68 |
by (strip_tac 1); |
|
69 |
by (rtac less_cfun2 1); |
|
70 |
by (rtac (beta_cfun RS ssubst) 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); |
894 | 73 |
by (rtac (beta_cfun RS ssubst) 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); |
894 | 76 |
by (rtac (is_chain_iterate RS is_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 |
|
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
896
diff
changeset
|
82 |
"(% i.iterate i f UU) = (%j.(LAM f. iterate j f UU)`f)"; |
894 | 83 |
by (rtac ext 1); |
84 |
by (rtac (beta_cfun RS ssubst) 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 |
|
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
896
diff
changeset
|
91 |
" Ifix = (%f.lub(range(%j.(LAM f.iterate j f UU)`f)))"; |
894 | 92 |
by (rtac ext 1); |
93 |
by (rewrite_goals_tac [Ifix_def] ); |
|
94 |
by (rtac (fix_lemma1 RS ssubst) 1); |
|
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; |
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
896
diff
changeset
|
100 |
val it = "is_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"; |
894 | 105 |
by (rtac ( fix_lemma2 RS ssubst) 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); |
894 | 107 |
by (rtac is_chainI 1); |
108 |
by (strip_tac 1); |
|
109 |
by (rtac less_cfun2 1); |
|
110 |
by (rtac (beta_cfun RS ssubst) 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); |
894 | 113 |
by (rtac (beta_cfun RS ssubst) 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); |
894 | 116 |
by (rtac (is_chain_iterate RS is_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 |