author | nipkow |
Sun, 22 Dec 2002 10:43:43 +0100 | |
changeset 13763 | f94b569cd610 |
parent 13524 | 604d0f3622d6 |
child 14981 | e73f8140af78 |
permissions | -rw-r--r-- |
2640 | 1 |
(* Title: HOLCF/Fix.ML |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
2 |
ID: $Id$ |
1461 | 3 |
Author: Franz Regensburger |
12030 | 4 |
License: GPL (GNU GENERAL PUBLIC LICENSE) |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
5 |
|
9245 | 6 |
fixed point operator and admissibility |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
7 |
*) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
8 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
9 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
10 |
(* derive inductive properties of iterate from primitive recursion *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
11 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
12 |
|
10834 | 13 |
Goal "iterate (Suc n) F x = iterate n F (F$x)"; |
9245 | 14 |
by (induct_tac "n" 1); |
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
15 |
by Auto_tac; |
9245 | 16 |
qed "iterate_Suc2"; |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
17 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
18 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
19 |
(* the sequence of function itertaions is a chain *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
20 |
(* This property is essential since monotonicity of iterate makes no sense *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
21 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
22 |
|
11346 | 23 |
Goalw [chain_def] "x << F$x ==> chain (%i. iterate i F x)"; |
9245 | 24 |
by (strip_tac 1); |
25 |
by (induct_tac "i" 1); |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
26 |
by Auto_tac; |
9245 | 27 |
by (etac monofun_cfun_arg 1); |
28 |
qed "chain_iterate2"; |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
29 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
30 |
|
11346 | 31 |
Goal "chain (%i. iterate i F UU)"; |
9245 | 32 |
by (rtac chain_iterate2 1); |
33 |
by (rtac minimal 1); |
|
34 |
qed "chain_iterate"; |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
35 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
36 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
37 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
38 |
(* Kleene's fixed point theorems for continuous functions in pointed *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
39 |
(* omega cpo's *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
40 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
41 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
42 |
|
10834 | 43 |
Goalw [Ifix_def] "Ifix F =F$(Ifix F)"; |
9245 | 44 |
by (stac contlub_cfun_arg 1); |
45 |
by (rtac chain_iterate 1); |
|
46 |
by (rtac antisym_less 1); |
|
47 |
by (rtac lub_mono 1); |
|
48 |
by (rtac chain_iterate 1); |
|
49 |
by (rtac ch2ch_Rep_CFunR 1); |
|
50 |
by (rtac chain_iterate 1); |
|
51 |
by (rtac allI 1); |
|
52 |
by (rtac (iterate_Suc RS subst) 1); |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
53 |
by (rtac (chain_iterate RS chainE) 1); |
9245 | 54 |
by (rtac is_lub_thelub 1); |
55 |
by (rtac ch2ch_Rep_CFunR 1); |
|
56 |
by (rtac chain_iterate 1); |
|
57 |
by (rtac ub_rangeI 1); |
|
58 |
by (rtac (iterate_Suc RS subst) 1); |
|
59 |
by (rtac is_ub_thelub 1); |
|
60 |
by (rtac chain_iterate 1); |
|
61 |
qed "Ifix_eq"; |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
62 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
63 |
|
10834 | 64 |
Goalw [Ifix_def] "F$x=x ==> Ifix(F) << x"; |
9245 | 65 |
by (rtac is_lub_thelub 1); |
66 |
by (rtac chain_iterate 1); |
|
67 |
by (rtac ub_rangeI 1); |
|
68 |
by (strip_tac 1); |
|
69 |
by (induct_tac "i" 1); |
|
70 |
by (Asm_simp_tac 1); |
|
71 |
by (Asm_simp_tac 1); |
|
72 |
by (res_inst_tac [("t","x")] subst 1); |
|
73 |
by (atac 1); |
|
74 |
by (etac monofun_cfun_arg 1); |
|
75 |
qed "Ifix_least"; |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
76 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
77 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
78 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
79 |
(* monotonicity and continuity of iterate *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
80 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
81 |
|
9245 | 82 |
Goalw [monofun] "monofun(iterate(i))"; |
83 |
by (strip_tac 1); |
|
84 |
by (induct_tac "i" 1); |
|
85 |
by (Asm_simp_tac 1); |
|
86 |
by (asm_full_simp_tac (simpset() addsimps [less_fun, monofun_cfun]) 1); |
|
87 |
qed "monofun_iterate"; |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
88 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
89 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
90 |
(* the following lemma uses contlub_cfun which itself is based on a *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
91 |
(* diagonalisation lemma for continuous functions with two arguments. *) |
5291 | 92 |
(* In this special case it is the application function Rep_CFun *) |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
93 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
94 |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
95 |
Goalw [contlub] "contlub(iterate(i))"; |
9245 | 96 |
by (strip_tac 1); |
97 |
by (induct_tac "i" 1); |
|
98 |
by (Asm_simp_tac 1); |
|
99 |
by (rtac (lub_const RS thelubI RS sym) 1); |
|
100 |
by (asm_simp_tac (simpset() delsimps [range_composition]) 1); |
|
101 |
by (rtac ext 1); |
|
102 |
by (stac thelub_fun 1); |
|
103 |
by (rtac chainI 1); |
|
104 |
by (rtac (less_fun RS iffD2) 1); |
|
105 |
by (rtac allI 1); |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
106 |
by (rtac (chainE) 1); |
9245 | 107 |
by (rtac (monofun_Rep_CFun1 RS ch2ch_MF2LR) 1); |
108 |
by (rtac allI 1); |
|
109 |
by (rtac monofun_Rep_CFun2 1); |
|
110 |
by (atac 1); |
|
111 |
by (rtac ch2ch_fun 1); |
|
112 |
by (rtac (monofun_iterate RS ch2ch_monofun) 1); |
|
113 |
by (atac 1); |
|
114 |
by (stac thelub_fun 1); |
|
115 |
by (rtac (monofun_iterate RS ch2ch_monofun) 1); |
|
116 |
by (atac 1); |
|
117 |
by (rtac contlub_cfun 1); |
|
118 |
by (atac 1); |
|
119 |
by (etac (monofun_iterate RS ch2ch_monofun RS ch2ch_fun) 1); |
|
120 |
qed "contlub_iterate"; |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
121 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
122 |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
123 |
Goal "cont(iterate(i))"; |
9245 | 124 |
by (rtac monocontlub2cont 1); |
125 |
by (rtac monofun_iterate 1); |
|
126 |
by (rtac contlub_iterate 1); |
|
127 |
qed "cont_iterate"; |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
128 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
129 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
130 |
(* a lemma about continuity of iterate in its third argument *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
131 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
132 |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
133 |
Goal "monofun(iterate n F)"; |
9245 | 134 |
by (rtac monofunI 1); |
135 |
by (strip_tac 1); |
|
136 |
by (induct_tac "n" 1); |
|
137 |
by (Asm_simp_tac 1); |
|
138 |
by (Asm_simp_tac 1); |
|
139 |
by (etac monofun_cfun_arg 1); |
|
140 |
qed "monofun_iterate2"; |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
141 |
|
9245 | 142 |
Goal "contlub(iterate n F)"; |
143 |
by (rtac contlubI 1); |
|
144 |
by (strip_tac 1); |
|
145 |
by (induct_tac "n" 1); |
|
146 |
by (Simp_tac 1); |
|
147 |
by (Simp_tac 1); |
|
148 |
by (res_inst_tac [("t","iterate n F (lub(range(%u. Y u)))"), |
|
149 |
("s","lub(range(%i. iterate n F (Y i)))")] ssubst 1); |
|
150 |
by (atac 1); |
|
151 |
by (rtac contlub_cfun_arg 1); |
|
152 |
by (etac (monofun_iterate2 RS ch2ch_monofun) 1); |
|
153 |
qed "contlub_iterate2"; |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
154 |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
155 |
Goal "cont (iterate n F)"; |
9245 | 156 |
by (rtac monocontlub2cont 1); |
157 |
by (rtac monofun_iterate2 1); |
|
158 |
by (rtac contlub_iterate2 1); |
|
159 |
qed "cont_iterate2"; |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
160 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
161 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
162 |
(* monotonicity and continuity of Ifix *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
163 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
164 |
|
9245 | 165 |
Goalw [monofun,Ifix_def] "monofun(Ifix)"; |
166 |
by (strip_tac 1); |
|
167 |
by (rtac lub_mono 1); |
|
168 |
by (rtac chain_iterate 1); |
|
169 |
by (rtac chain_iterate 1); |
|
170 |
by (rtac allI 1); |
|
171 |
by (rtac (less_fun RS iffD1 RS spec) 1 THEN |
|
172 |
etac (monofun_iterate RS monofunE RS spec RS spec RS mp) 1); |
|
173 |
qed "monofun_Ifix"; |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
174 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
175 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
176 |
(* since iterate is not monotone in its first argument, special lemmas must *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
177 |
(* be derived for lubs in this argument *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
178 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
179 |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
180 |
Goal |
9245 | 181 |
"chain(Y) ==> chain(%i. lub(range(%ia. iterate ia (Y i) UU)))"; |
182 |
by (rtac chainI 1); |
|
183 |
by (strip_tac 1); |
|
184 |
by (rtac lub_mono 1); |
|
185 |
by (rtac chain_iterate 1); |
|
186 |
by (rtac chain_iterate 1); |
|
187 |
by (strip_tac 1); |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
188 |
by (etac (monofun_iterate RS ch2ch_monofun RS ch2ch_fun RS chainE) 1); |
9245 | 189 |
qed "chain_iterate_lub"; |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
190 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
191 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
192 |
(* this exchange lemma is analog to the one for monotone functions *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
193 |
(* observe that monotonicity is not really needed. The propagation of *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
194 |
(* chains is the essential argument which is usually derived from monot. *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
195 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
196 |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
197 |
Goal "chain(Y) ==>iterate n (lub(range Y)) y = lub(range(%i. iterate n (Y i) y))"; |
9245 | 198 |
by (rtac (thelub_fun RS subst) 1); |
199 |
by (etac (monofun_iterate RS ch2ch_monofun) 1); |
|
200 |
by (asm_simp_tac (simpset() addsimps [contlub_iterate RS contlubE]) 1); |
|
201 |
qed "contlub_Ifix_lemma1"; |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
202 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
203 |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
204 |
Goal "chain(Y) ==>\ |
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
892
diff
changeset
|
205 |
\ lub(range(%i. lub(range(%ia. iterate i (Y ia) UU)))) =\ |
9245 | 206 |
\ lub(range(%i. lub(range(%ia. iterate ia (Y i) UU))))"; |
207 |
by (rtac antisym_less 1); |
|
208 |
by (rtac is_lub_thelub 1); |
|
209 |
by (rtac (contlub_Ifix_lemma1 RS ext RS subst) 1); |
|
210 |
by (atac 1); |
|
211 |
by (rtac chain_iterate 1); |
|
212 |
by (rtac ub_rangeI 1); |
|
213 |
by (strip_tac 1); |
|
214 |
by (rtac lub_mono 1); |
|
215 |
by (etac (monofun_iterate RS ch2ch_monofun RS ch2ch_fun) 1); |
|
216 |
by (etac chain_iterate_lub 1); |
|
217 |
by (strip_tac 1); |
|
218 |
by (rtac is_ub_thelub 1); |
|
219 |
by (rtac chain_iterate 1); |
|
220 |
by (rtac is_lub_thelub 1); |
|
221 |
by (etac chain_iterate_lub 1); |
|
222 |
by (rtac ub_rangeI 1); |
|
223 |
by (strip_tac 1); |
|
224 |
by (rtac lub_mono 1); |
|
225 |
by (rtac chain_iterate 1); |
|
226 |
by (rtac (contlub_Ifix_lemma1 RS ext RS subst) 1); |
|
227 |
by (atac 1); |
|
228 |
by (rtac chain_iterate 1); |
|
229 |
by (strip_tac 1); |
|
230 |
by (rtac is_ub_thelub 1); |
|
231 |
by (etac (monofun_iterate RS ch2ch_monofun RS ch2ch_fun) 1); |
|
232 |
qed "ex_lub_iterate"; |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
233 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
234 |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
235 |
Goalw [contlub,Ifix_def] "contlub(Ifix)"; |
9245 | 236 |
by (strip_tac 1); |
237 |
by (stac (contlub_Ifix_lemma1 RS ext) 1); |
|
238 |
by (atac 1); |
|
239 |
by (etac ex_lub_iterate 1); |
|
240 |
qed "contlub_Ifix"; |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
241 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
242 |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
243 |
Goal "cont(Ifix)"; |
9245 | 244 |
by (rtac monocontlub2cont 1); |
245 |
by (rtac monofun_Ifix 1); |
|
246 |
by (rtac contlub_Ifix 1); |
|
247 |
qed "cont_Ifix"; |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
248 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
249 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
250 |
(* propagate properties of Ifix to its continuous counterpart *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
251 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
252 |
|
10834 | 253 |
Goalw [fix_def] "fix$F = F$(fix$F)"; |
9245 | 254 |
by (asm_simp_tac (simpset() addsimps [cont_Ifix]) 1); |
255 |
by (rtac Ifix_eq 1); |
|
256 |
qed "fix_eq"; |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
257 |
|
10834 | 258 |
Goalw [fix_def] "F$x = x ==> fix$F << x"; |
9245 | 259 |
by (asm_simp_tac (simpset() addsimps [cont_Ifix]) 1); |
260 |
by (etac Ifix_least 1); |
|
261 |
qed "fix_least"; |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
262 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
263 |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
264 |
Goal |
10834 | 265 |
"[| F$x = x; !z. F$z = z --> x << z |] ==> x = fix$F"; |
9245 | 266 |
by (rtac antisym_less 1); |
267 |
by (etac allE 1); |
|
268 |
by (etac mp 1); |
|
269 |
by (rtac (fix_eq RS sym) 1); |
|
270 |
by (etac fix_least 1); |
|
271 |
qed "fix_eqI"; |
|
1274 | 272 |
|
273 |
||
10834 | 274 |
Goal "f == fix$F ==> f = F$f"; |
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
275 |
by (asm_simp_tac (simpset() addsimps [fix_eq RS sym]) 1); |
9245 | 276 |
qed "fix_eq2"; |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
277 |
|
10834 | 278 |
Goal "f == fix$F ==> f$x = F$f$x"; |
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
279 |
by (etac (fix_eq2 RS cfun_fun_cong) 1); |
9245 | 280 |
qed "fix_eq3"; |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
281 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
282 |
fun fix_tac3 thm i = ((rtac trans i) THEN (rtac (thm RS fix_eq3) i)); |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
283 |
|
10834 | 284 |
Goal "f = fix$F ==> f = F$f"; |
9245 | 285 |
by (hyp_subst_tac 1); |
286 |
by (rtac fix_eq 1); |
|
287 |
qed "fix_eq4"; |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
288 |
|
10834 | 289 |
Goal "f = fix$F ==> f$x = F$f$x"; |
9245 | 290 |
by (rtac trans 1); |
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
291 |
by (etac (fix_eq4 RS cfun_fun_cong) 1); |
9245 | 292 |
by (rtac refl 1); |
293 |
qed "fix_eq5"; |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
294 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
295 |
fun fix_tac5 thm i = ((rtac trans i) THEN (rtac (thm RS fix_eq5) i)); |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
296 |
|
10834 | 297 |
(* proves the unfolding theorem for function equations f = fix$... *) |
3652 | 298 |
fun fix_prover thy fixeq s = prove_goal thy s (fn prems => [ |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
299 |
(rtac trans 1), |
3652 | 300 |
(rtac (fixeq RS fix_eq4) 1), |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
301 |
(rtac trans 1), |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
302 |
(rtac beta_cfun 1), |
2566 | 303 |
(Simp_tac 1) |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
304 |
]); |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
305 |
|
10834 | 306 |
(* proves the unfolding theorem for function definitions f == fix$... *) |
3652 | 307 |
fun fix_prover2 thy fixdef s = prove_goal thy s (fn prems => [ |
1461 | 308 |
(rtac trans 1), |
309 |
(rtac (fix_eq2) 1), |
|
310 |
(rtac fixdef 1), |
|
311 |
(rtac beta_cfun 1), |
|
2566 | 312 |
(Simp_tac 1) |
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
892
diff
changeset
|
313 |
]); |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
314 |
|
3652 | 315 |
(* proves an application case for a function from its unfolding thm *) |
316 |
fun case_prover thy unfold s = prove_goal thy s (fn prems => [ |
|
317 |
(cut_facts_tac prems 1), |
|
318 |
(rtac trans 1), |
|
319 |
(stac unfold 1), |
|
4477
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4423
diff
changeset
|
320 |
Auto_tac |
3652 | 321 |
]); |
322 |
||
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
323 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
324 |
(* better access to definitions *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
325 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
326 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
327 |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
328 |
Goal "Ifix=(%x. lub(range(%i. iterate i x UU)))"; |
9245 | 329 |
by (rtac ext 1); |
330 |
by (rewtac Ifix_def); |
|
331 |
by (rtac refl 1); |
|
332 |
qed "Ifix_def2"; |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
333 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
334 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
335 |
(* direct connection between fix and iteration without Ifix *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
336 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
337 |
|
10834 | 338 |
Goalw [fix_def] "fix$F = lub(range(%i. iterate i F UU))"; |
9245 | 339 |
by (fold_goals_tac [Ifix_def]); |
340 |
by (asm_simp_tac (simpset() addsimps [cont_Ifix]) 1); |
|
341 |
qed "fix_def2"; |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
342 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
343 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
344 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
345 |
(* Lemmas about admissibility and fixed point induction *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
346 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
347 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
348 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
349 |
(* access to definitions *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
350 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
351 |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
352 |
val prems = Goalw [adm_def] |
11346 | 353 |
"(!!Y. [| chain Y; !i. P (Y i) |] ==> P (lub (range Y))) ==> adm P"; |
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
354 |
by (blast_tac (claset() addIs prems) 1); |
9245 | 355 |
qed "admI"; |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
356 |
|
11346 | 357 |
Goal "!x. P x ==> adm P"; |
358 |
by (rtac admI 1); |
|
359 |
by (etac spec 1); |
|
360 |
qed "triv_admI"; |
|
361 |
||
9245 | 362 |
Goalw [adm_def] "[| adm(P); chain(Y); !i. P(Y(i)) |] ==> P(lub(range(Y)))"; |
363 |
by (Blast_tac 1); |
|
364 |
qed "admD"; |
|
365 |
||
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
366 |
Goalw [admw_def] "admw(P) = (!F.(!n. P(iterate n F UU)) -->\ |
9245 | 367 |
\ P (lub(range(%i. iterate i F UU))))"; |
368 |
by (rtac refl 1); |
|
369 |
qed "admw_def2"; |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
370 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
371 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
372 |
(* an admissible formula is also weak admissible *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
373 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
374 |
|
10230 | 375 |
Goalw [admw_def] "adm(P)==>admw(P)"; |
9245 | 376 |
by (strip_tac 1); |
377 |
by (etac admD 1); |
|
378 |
by (rtac chain_iterate 1); |
|
379 |
by (atac 1); |
|
380 |
qed "adm_impl_admw"; |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
381 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
382 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
383 |
(* fixed point induction *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
384 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
385 |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
386 |
val major::prems = Goal |
10834 | 387 |
"[| adm(P); P(UU); !!x. P(x) ==> P(F$x)|] ==> P(fix$F)"; |
9245 | 388 |
by (stac fix_def2 1); |
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
389 |
by (rtac (major RS admD) 1); |
9245 | 390 |
by (rtac chain_iterate 1); |
391 |
by (rtac allI 1); |
|
392 |
by (induct_tac "i" 1); |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
393 |
by (asm_simp_tac (simpset() addsimps (iterate_0::prems)) 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
394 |
by (asm_simp_tac (simpset() addsimps (iterate_Suc::prems)) 1); |
9245 | 395 |
qed "fix_ind"; |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
396 |
|
10834 | 397 |
val prems = Goal "[| f == fix$F; adm(P); \ |
398 |
\ P(UU); !!x. P(x) ==> P(F$x)|] ==> P f"; |
|
9245 | 399 |
by (cut_facts_tac prems 1); |
400 |
by (asm_simp_tac HOL_ss 1); |
|
401 |
by (etac fix_ind 1); |
|
402 |
by (atac 1); |
|
403 |
by (eresolve_tac prems 1); |
|
404 |
qed "def_fix_ind"; |
|
2568 | 405 |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
406 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
407 |
(* computational induction for weak admissible formulae *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
408 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
409 |
|
10834 | 410 |
Goal "[| admw(P); !n. P(iterate n F UU)|] ==> P(fix$F)"; |
9245 | 411 |
by (stac fix_def2 1); |
412 |
by (rtac (admw_def2 RS iffD1 RS spec RS mp) 1); |
|
413 |
by (atac 1); |
|
414 |
by (rtac allI 1); |
|
415 |
by (etac spec 1); |
|
416 |
qed "wfix_ind"; |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
417 |
|
10834 | 418 |
Goal "[| f == fix$F; admw(P); \ |
9245 | 419 |
\ !n. P(iterate n F UU) |] ==> P f"; |
420 |
by (asm_simp_tac HOL_ss 1); |
|
421 |
by (etac wfix_ind 1); |
|
422 |
by (atac 1); |
|
423 |
qed "def_wfix_ind"; |
|
2568 | 424 |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
425 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
426 |
(* for chain-finite (easy) types every formula is admissible *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
427 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
428 |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
429 |
Goalw [adm_def] |
9245 | 430 |
"!Y. chain(Y::nat=>'a) --> (? n. max_in_chain n Y) ==> adm(P::'a=>bool)"; |
431 |
by (strip_tac 1); |
|
432 |
by (rtac exE 1); |
|
433 |
by (rtac mp 1); |
|
434 |
by (etac spec 1); |
|
435 |
by (atac 1); |
|
436 |
by (stac (lub_finch1 RS thelubI) 1); |
|
437 |
by (atac 1); |
|
438 |
by (atac 1); |
|
439 |
by (etac spec 1); |
|
440 |
qed "adm_max_in_chain"; |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
441 |
|
4720 | 442 |
bind_thm ("adm_chfin" ,chfin RS adm_max_in_chain); |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
443 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
444 |
(* ------------------------------------------------------------------------ *) |
4720 | 445 |
(* some lemmata for functions with flat/chfin domain/range types *) |
2354 | 446 |
(* ------------------------------------------------------------------------ *) |
447 |
||
10834 | 448 |
val _ = goalw thy [adm_def] "adm (%(u::'a::cpo->'b::chfin). P(u$s))"; |
9245 | 449 |
by (strip_tac 1); |
450 |
by (dtac chfin_Rep_CFunR 1); |
|
451 |
by (eres_inst_tac [("x","s")] allE 1); |
|
452 |
by (fast_tac (HOL_cs addss (simpset() addsimps [chfin])) 1); |
|
453 |
qed "adm_chfindom"; |
|
2354 | 454 |
|
3324 | 455 |
(* adm_flat not needed any more, since it is a special case of adm_chfindom *) |
2354 | 456 |
|
1992 | 457 |
(* ------------------------------------------------------------------------ *) |
3326 | 458 |
(* improved admisibility introduction *) |
1992 | 459 |
(* ------------------------------------------------------------------------ *) |
460 |
||
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
461 |
val prems = Goalw [adm_def] |
4720 | 462 |
"(!!Y. [| chain Y; !i. P (Y i); !i. ? j. i < j & Y i ~= Y j & Y i << Y j |]\ |
9245 | 463 |
\ ==> P(lub (range Y))) ==> adm P"; |
464 |
by (strip_tac 1); |
|
465 |
by (etac increasing_chain_adm_lemma 1); |
|
466 |
by (atac 1); |
|
467 |
by (eresolve_tac prems 1); |
|
468 |
by (atac 1); |
|
469 |
by (atac 1); |
|
470 |
qed "admI2"; |
|
1992 | 471 |
|
472 |
||
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
473 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
474 |
(* admissibility of special formulae and propagation *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
475 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
476 |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
477 |
Goalw [adm_def] "[|cont u;cont v|]==> adm(%x. u x << v x)"; |
9245 | 478 |
by (strip_tac 1); |
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
479 |
by (forw_inst_tac [("f","u")] (cont2mono RS ch2ch_monofun) 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
480 |
by (assume_tac 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
481 |
by (forw_inst_tac [("f","v")] (cont2mono RS ch2ch_monofun) 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
482 |
by (assume_tac 1); |
9245 | 483 |
by (etac (cont2contlub RS contlubE RS spec RS mp RS ssubst) 1); |
484 |
by (atac 1); |
|
485 |
by (etac (cont2contlub RS contlubE RS spec RS mp RS ssubst) 1); |
|
486 |
by (atac 1); |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
487 |
by (blast_tac (claset() addIs [lub_mono]) 1); |
9245 | 488 |
qed "adm_less"; |
3460 | 489 |
Addsimps [adm_less]; |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
490 |
|
10230 | 491 |
Goal "[| adm P; adm Q |] ==> adm(%x. P x & Q x)"; |
9245 | 492 |
by (fast_tac (HOL_cs addEs [admD] addIs [admI]) 1); |
493 |
qed "adm_conj"; |
|
3460 | 494 |
Addsimps [adm_conj]; |
495 |
||
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
496 |
Goalw [adm_def] "adm(%x. t)"; |
9245 | 497 |
by (fast_tac HOL_cs 1); |
498 |
qed "adm_not_free"; |
|
3460 | 499 |
Addsimps [adm_not_free]; |
500 |
||
10230 | 501 |
Goalw [adm_def] "cont t ==> adm(%x.~ (t x) << u)"; |
9245 | 502 |
by (strip_tac 1); |
10230 | 503 |
by (rtac contrapos_nn 1); |
9245 | 504 |
by (etac spec 1); |
505 |
by (rtac trans_less 1); |
|
506 |
by (atac 2); |
|
507 |
by (etac (cont2mono RS monofun_fun_arg) 1); |
|
508 |
by (rtac is_ub_thelub 1); |
|
509 |
by (atac 1); |
|
510 |
qed "adm_not_less"; |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
511 |
|
10230 | 512 |
Goal "!y. adm(P y) ==> adm(%x.!y. P y x)"; |
9245 | 513 |
by (fast_tac (HOL_cs addIs [admI] addEs [admD]) 1); |
514 |
qed "adm_all"; |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
515 |
|
1779 | 516 |
bind_thm ("adm_all2", allI RS adm_all); |
625 | 517 |
|
10230 | 518 |
Goal "[|cont t; adm P|] ==> adm(%x. P (t x))"; |
9245 | 519 |
by (rtac admI 1); |
520 |
by (stac (cont2contlub RS contlubE RS spec RS mp) 1); |
|
521 |
by (atac 1); |
|
522 |
by (atac 1); |
|
523 |
by (etac admD 1); |
|
524 |
by (etac (cont2mono RS ch2ch_monofun) 1); |
|
525 |
by (atac 1); |
|
526 |
by (atac 1); |
|
527 |
qed "adm_subst"; |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
528 |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
529 |
Goal "adm(%x.~ UU << t(x))"; |
9245 | 530 |
by (Simp_tac 1); |
531 |
qed "adm_UU_not_less"; |
|
3460 | 532 |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
533 |
|
9245 | 534 |
Goalw [adm_def] "cont(t)==> adm(%x.~ (t x) = UU)"; |
535 |
by (strip_tac 1); |
|
10230 | 536 |
by (rtac contrapos_nn 1); |
9245 | 537 |
by (etac spec 1); |
538 |
by (rtac (chain_UU_I RS spec) 1); |
|
539 |
by (etac (cont2mono RS ch2ch_monofun) 1); |
|
540 |
by (atac 1); |
|
541 |
by (etac (cont2contlub RS contlubE RS spec RS mp RS subst) 1); |
|
542 |
by (atac 1); |
|
543 |
by (atac 1); |
|
544 |
qed "adm_not_UU"; |
|
545 |
||
546 |
Goal "[|cont u ; cont v|]==> adm(%x. u x = v x)"; |
|
547 |
by (asm_simp_tac (simpset() addsimps [po_eq_conv]) 1); |
|
548 |
qed "adm_eq"; |
|
3460 | 549 |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
550 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
551 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
552 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
553 |
(* admissibility for disjunction is hard to prove. It takes 10 Lemmas *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
554 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
555 |
|
1992 | 556 |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
557 |
Goal "!n. P(Y n)|Q(Y n) ==> (? i.!j. R i j --> Q(Y(j))) | (!i.? j. R i j & P(Y(j)))"; |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
558 |
by (Fast_tac 1); |
9245 | 559 |
qed "adm_disj_lemma1"; |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
560 |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
561 |
Goal "[| adm(Q); ? X. chain(X) & (!n. Q(X(n))) &\ |
9245 | 562 |
\ lub(range(Y))=lub(range(X))|] ==> Q(lub(range(Y)))"; |
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
563 |
by (force_tac (claset() addEs [admD], simpset()) 1); |
9245 | 564 |
qed "adm_disj_lemma2"; |
2619 | 565 |
|
11346 | 566 |
Goalw [chain_def]"chain Y ==> chain (%m. if m < Suc i then Y (Suc i) else Y m)"; |
9245 | 567 |
by (Asm_simp_tac 1); |
568 |
by (safe_tac HOL_cs); |
|
569 |
by (subgoal_tac "ia = i" 1); |
|
570 |
by (ALLGOALS Asm_simp_tac); |
|
571 |
qed "adm_disj_lemma3"; |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
572 |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
573 |
Goal "!j. i < j --> Q(Y(j)) ==> !n. Q( if n < Suc i then Y(Suc i) else Y n)"; |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
574 |
by (Asm_simp_tac 1); |
9245 | 575 |
qed "adm_disj_lemma4"; |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
576 |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
577 |
Goal |
4720 | 578 |
"!!Y::nat=>'a::cpo. [| chain(Y); ! j. i < j --> Q(Y(j)) |] ==>\ |
9245 | 579 |
\ lub(range(Y)) = lub(range(%m. if m< Suc(i) then Y(Suc(i)) else Y m))"; |
580 |
by (safe_tac (HOL_cs addSIs [lub_equal2,adm_disj_lemma3])); |
|
581 |
by (atac 2); |
|
582 |
by (res_inst_tac [("x","i")] exI 1); |
|
583 |
by (Asm_simp_tac 1); |
|
584 |
qed "adm_disj_lemma5"; |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
585 |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
586 |
Goal |
4720 | 587 |
"[| chain(Y::nat=>'a::cpo); ? i. ! j. i < j --> Q(Y(j)) |] ==>\ |
9245 | 588 |
\ ? X. chain(X) & (! n. Q(X(n))) & lub(range(Y)) = lub(range(X))"; |
589 |
by (etac exE 1); |
|
590 |
by (res_inst_tac [("x","%m. if m<Suc(i) then Y(Suc(i)) else Y m")] exI 1); |
|
591 |
by (rtac conjI 1); |
|
592 |
by (rtac adm_disj_lemma3 1); |
|
593 |
by (atac 1); |
|
594 |
by (rtac conjI 1); |
|
595 |
by (rtac adm_disj_lemma4 1); |
|
596 |
by (atac 1); |
|
597 |
by (rtac adm_disj_lemma5 1); |
|
598 |
by (atac 1); |
|
599 |
by (atac 1); |
|
600 |
qed "adm_disj_lemma6"; |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
601 |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
602 |
Goal |
4720 | 603 |
"[| chain(Y::nat=>'a::cpo); ! i. ? j. i < j & P(Y(j)) |] ==>\ |
9245 | 604 |
\ chain(%m. Y(Least(%j. m<j & P(Y(j)))))"; |
605 |
by (rtac chainI 1); |
|
606 |
by (rtac chain_mono3 1); |
|
607 |
by (atac 1); |
|
608 |
by (rtac Least_le 1); |
|
609 |
by (rtac conjI 1); |
|
610 |
by (rtac Suc_lessD 1); |
|
611 |
by (etac allE 1); |
|
612 |
by (etac exE 1); |
|
613 |
by (rtac (LeastI RS conjunct1) 1); |
|
614 |
by (atac 1); |
|
615 |
by (etac allE 1); |
|
616 |
by (etac exE 1); |
|
617 |
by (rtac (LeastI RS conjunct2) 1); |
|
618 |
by (atac 1); |
|
619 |
qed "adm_disj_lemma7"; |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
620 |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
621 |
Goal |
9245 | 622 |
"[| ! i. ? j. i < j & P(Y(j)) |] ==> ! m. P(Y(LEAST j::nat. m<j & P(Y(j))))"; |
623 |
by (strip_tac 1); |
|
624 |
by (etac allE 1); |
|
625 |
by (etac exE 1); |
|
626 |
by (etac (LeastI RS conjunct2) 1); |
|
627 |
qed "adm_disj_lemma8"; |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
628 |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
629 |
Goal |
4720 | 630 |
"[| chain(Y::nat=>'a::cpo); ! i. ? j. i < j & P(Y(j)) |] ==>\ |
9245 | 631 |
\ lub(range(Y)) = lub(range(%m. Y(Least(%j. m<j & P(Y(j))))))"; |
632 |
by (rtac antisym_less 1); |
|
633 |
by (rtac lub_mono 1); |
|
634 |
by (atac 1); |
|
635 |
by (rtac adm_disj_lemma7 1); |
|
636 |
by (atac 1); |
|
637 |
by (atac 1); |
|
638 |
by (strip_tac 1); |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
639 |
by (rtac (chain_mono) 1); |
9245 | 640 |
by (atac 1); |
641 |
by (etac allE 1); |
|
642 |
by (etac exE 1); |
|
643 |
by (rtac (LeastI RS conjunct1) 1); |
|
644 |
by (atac 1); |
|
645 |
by (rtac lub_mono3 1); |
|
646 |
by (rtac adm_disj_lemma7 1); |
|
647 |
by (atac 1); |
|
648 |
by (atac 1); |
|
649 |
by (atac 1); |
|
650 |
by (strip_tac 1); |
|
651 |
by (rtac exI 1); |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
652 |
by (rtac (chain_mono) 1); |
9245 | 653 |
by (atac 1); |
654 |
by (rtac lessI 1); |
|
655 |
qed "adm_disj_lemma9"; |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
656 |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
657 |
Goal "[| chain(Y::nat=>'a::cpo); ! i. ? j. i < j & P(Y(j)) |] ==>\ |
9245 | 658 |
\ ? X. chain(X) & (! n. P(X(n))) & lub(range(Y)) = lub(range(X))"; |
659 |
by (res_inst_tac [("x","%m. Y(Least(%j. m<j & P(Y(j))))")] exI 1); |
|
660 |
by (rtac conjI 1); |
|
661 |
by (rtac adm_disj_lemma7 1); |
|
662 |
by (atac 1); |
|
663 |
by (atac 1); |
|
664 |
by (rtac conjI 1); |
|
665 |
by (rtac adm_disj_lemma8 1); |
|
666 |
by (atac 1); |
|
667 |
by (rtac adm_disj_lemma9 1); |
|
668 |
by (atac 1); |
|
669 |
by (atac 1); |
|
670 |
qed "adm_disj_lemma10"; |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
671 |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
672 |
Goal "[| adm(P); chain(Y);? i. ! j. i < j --> P(Y(j))|]==>P(lub(range(Y)))"; |
9245 | 673 |
by (etac adm_disj_lemma2 1); |
674 |
by (etac adm_disj_lemma6 1); |
|
675 |
by (atac 1); |
|
676 |
qed "adm_disj_lemma12"; |
|
430 | 677 |
|
1992 | 678 |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
679 |
Goal |
9245 | 680 |
"[| adm(P); chain(Y); ! i. ? j. i < j & P(Y(j)) |]==>P(lub(range(Y)))"; |
681 |
by (etac adm_disj_lemma2 1); |
|
682 |
by (etac adm_disj_lemma10 1); |
|
683 |
by (atac 1); |
|
684 |
qed "adm_lemma11"; |
|
430 | 685 |
|
10230 | 686 |
Goal "[| adm P; adm Q |] ==> adm(%x. P x | Q x)"; |
9245 | 687 |
by (rtac admI 1); |
688 |
by (rtac (adm_disj_lemma1 RS disjE) 1); |
|
689 |
by (atac 1); |
|
690 |
by (rtac disjI2 1); |
|
691 |
by (etac adm_disj_lemma12 1); |
|
692 |
by (atac 1); |
|
693 |
by (atac 1); |
|
694 |
by (rtac disjI1 1); |
|
695 |
by (etac adm_lemma11 1); |
|
696 |
by (atac 1); |
|
697 |
by (atac 1); |
|
698 |
qed "adm_disj"; |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
699 |
|
10230 | 700 |
Goal "[| adm(%x.~(P x)); adm Q |] ==> adm(%x. P x --> Q x)"; |
9245 | 701 |
by (subgoal_tac "(%x. P x --> Q x) = (%x. ~P x | Q x)" 1); |
702 |
by (etac ssubst 1); |
|
703 |
by (etac adm_disj 1); |
|
704 |
by (atac 1); |
|
705 |
by (Simp_tac 1); |
|
706 |
qed "adm_imp"; |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
707 |
|
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5068
diff
changeset
|
708 |
Goal "[| adm (%x. P x --> Q x); adm (%x. Q x --> P x) |] \ |
3460 | 709 |
\ ==> adm (%x. P x = Q x)"; |
4423 | 710 |
by (subgoal_tac "(%x. P x = Q x) = (%x. (P x --> Q x) & (Q x --> P x))" 1); |
3460 | 711 |
by (Asm_simp_tac 1); |
712 |
by (rtac ext 1); |
|
713 |
by (fast_tac HOL_cs 1); |
|
714 |
qed"adm_iff"; |
|
715 |
||
716 |
||
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
717 |
Goal "[| adm (%x. ~ P x); adm (%x. ~ Q x) |] ==> adm (%x. ~ (P x & Q x))"; |
9245 | 718 |
by (subgoal_tac "(%x. ~ (P x & Q x)) = (%x. ~ P x | ~ Q x)" 1); |
719 |
by (rtac ext 2); |
|
720 |
by (fast_tac HOL_cs 2); |
|
721 |
by (etac ssubst 1); |
|
722 |
by (etac adm_disj 1); |
|
723 |
by (atac 1); |
|
724 |
qed "adm_not_conj"; |
|
1675 | 725 |
|
11346 | 726 |
bind_thms ("adm_lemmas", [adm_not_free,adm_imp,adm_disj,adm_eq,adm_not_UU, |
727 |
adm_UU_not_less,adm_all2,adm_not_less,adm_not_conj,adm_iff]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
728 |
|
2566 | 729 |
Addsimps adm_lemmas; |