author | paulson |
Fri, 21 Nov 2003 11:15:40 +0100 | |
changeset 14265 | 95b42e69436c |
parent 12484 | 7ad150f5fc10 |
child 14981 | e73f8140af78 |
permissions | -rw-r--r-- |
9245 | 1 |
(* Title: HOLCF/Cfun2 |
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 |
Class Instance ->::(cpo,cpo)po |
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 |
|
2640 | 9 |
(* for compatibility with old HOLCF-Version *) |
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
10 |
Goal "(op <<)=(%f1 f2. Rep_CFun f1 << Rep_CFun f2)"; |
9245 | 11 |
by (fold_goals_tac [less_cfun_def]); |
12 |
by (rtac refl 1); |
|
13 |
qed "inst_cfun_po"; |
|
2640 | 14 |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
15 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
16 |
(* access to less_cfun in class po *) |
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 |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
19 |
Goal "( f1 << f2 ) = (Rep_CFun(f1) << Rep_CFun(f2))"; |
9245 | 20 |
by (simp_tac (simpset() addsimps [inst_cfun_po]) 1); |
21 |
qed "less_cfun"; |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
22 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
23 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
24 |
(* Type 'a ->'b is pointed *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
25 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
26 |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
27 |
Goal "Abs_CFun(% x. UU) << f"; |
9245 | 28 |
by (stac less_cfun 1); |
29 |
by (stac Abs_Cfun_inverse2 1); |
|
30 |
by (rtac cont_const 1); |
|
31 |
by (rtac minimal_fun 1); |
|
32 |
qed "minimal_cfun"; |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
33 |
|
2640 | 34 |
bind_thm ("UU_cfun_def",minimal_cfun RS minimal2UU RS sym); |
35 |
||
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
36 |
Goal "? x::'a->'b::pcpo.!y. x<<y"; |
9245 | 37 |
by (res_inst_tac [("x","Abs_CFun(% x. UU)")] exI 1); |
38 |
by (rtac (minimal_cfun RS allI) 1); |
|
39 |
qed "least_cfun"; |
|
2640 | 40 |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
41 |
(* ------------------------------------------------------------------------ *) |
5291 | 42 |
(* Rep_CFun yields continuous functions in 'a => 'b *) |
43 |
(* this is continuity of Rep_CFun in its 'second' argument *) |
|
44 |
(* cont_Rep_CFun2 ==> monofun_Rep_CFun2 & contlub_Rep_CFun2 *) |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
45 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
46 |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
47 |
Goal "cont(Rep_CFun(fo))"; |
9245 | 48 |
by (res_inst_tac [("P","cont")] CollectD 1); |
49 |
by (fold_goals_tac [CFun_def]); |
|
50 |
by (rtac Rep_Cfun 1); |
|
51 |
qed "cont_Rep_CFun2"; |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
52 |
|
5291 | 53 |
bind_thm ("monofun_Rep_CFun2", cont_Rep_CFun2 RS cont2mono); |
54 |
(* monofun(Rep_CFun(?fo1)) *) |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
55 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
56 |
|
5291 | 57 |
bind_thm ("contlub_Rep_CFun2", cont_Rep_CFun2 RS cont2contlub); |
58 |
(* contlub(Rep_CFun(?fo1)) *) |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
59 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
60 |
(* ------------------------------------------------------------------------ *) |
5291 | 61 |
(* expanded thms cont_Rep_CFun2, contlub_Rep_CFun2 *) |
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
892
diff
changeset
|
62 |
(* looks nice with mixfix syntac *) |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
63 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
64 |
|
5291 | 65 |
bind_thm ("cont_cfun_arg", (cont_Rep_CFun2 RS contE RS spec RS mp)); |
10834 | 66 |
(* chain(?x1) ==> range (%i. ?fo3$(?x1 i)) <<| ?fo3$(lub (range ?x1)) *) |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
67 |
|
5291 | 68 |
bind_thm ("contlub_cfun_arg", (contlub_Rep_CFun2 RS contlubE RS spec RS mp)); |
10834 | 69 |
(* chain(?x1) ==> ?fo4$(lub (range ?x1)) = lub (range (%i. ?fo4$(?x1 i))) *) |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
70 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
71 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
72 |
(* ------------------------------------------------------------------------ *) |
5291 | 73 |
(* Rep_CFun is monotone in its 'first' argument *) |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
74 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
75 |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
76 |
Goalw [monofun] "monofun(Rep_CFun)"; |
9245 | 77 |
by (strip_tac 1); |
78 |
by (etac (less_cfun RS subst) 1); |
|
79 |
qed "monofun_Rep_CFun1"; |
|
243
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 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
82 |
(* ------------------------------------------------------------------------ *) |
5291 | 83 |
(* monotonicity of application Rep_CFun in mixfix syntax [_]_ *) |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
84 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
85 |
|
10834 | 86 |
Goal "f1 << f2 ==> f1$x << f2$x"; |
9245 | 87 |
by (res_inst_tac [("x","x")] spec 1); |
88 |
by (rtac (less_fun RS subst) 1); |
|
89 |
by (etac (monofun_Rep_CFun1 RS monofunE RS spec RS spec RS mp) 1); |
|
90 |
qed "monofun_cfun_fun"; |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
91 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
92 |
|
5291 | 93 |
bind_thm ("monofun_cfun_arg", monofun_Rep_CFun2 RS monofunE RS spec RS spec RS mp); |
10834 | 94 |
(* ?x2 << ?x1 ==> ?fo5$?x2 << ?fo5$?x1 *) |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
95 |
|
11341 | 96 |
Goal "chain Y ==> chain (%i. f\\<cdot>(Y i))"; |
12484 | 97 |
by (rtac chainI 1); |
98 |
by (rtac monofun_cfun_arg 1); |
|
99 |
by (etac chainE 1); |
|
11341 | 100 |
qed "chain_monofun"; |
101 |
||
102 |
||
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
103 |
(* ------------------------------------------------------------------------ *) |
5291 | 104 |
(* monotonicity of Rep_CFun in both arguments in mixfix syntax [_]_ *) |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
105 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
106 |
|
10834 | 107 |
Goal "[|f1<<f2;x1<<x2|] ==> f1$x1 << f2$x2"; |
9245 | 108 |
by (rtac trans_less 1); |
109 |
by (etac monofun_cfun_arg 1); |
|
110 |
by (etac monofun_cfun_fun 1); |
|
111 |
qed "monofun_cfun"; |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
112 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
113 |
|
10834 | 114 |
Goal "f$x = UU ==> f$UU = UU"; |
9245 | 115 |
by (rtac (eq_UU_iff RS iffD2) 1); |
116 |
by (etac subst 1); |
|
117 |
by (rtac (minimal RS monofun_cfun_arg) 1); |
|
118 |
qed "strictI"; |
|
1989 | 119 |
|
120 |
||
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 |
(* ch2ch - rules for the type 'a -> 'b *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
123 |
(* use MF2 lemmas from Cont.ML *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
124 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
125 |
|
10834 | 126 |
Goal "chain(Y) ==> chain(%i. f$(Y i))"; |
9245 | 127 |
by (etac (monofun_Rep_CFun2 RS ch2ch_MF2R) 1); |
128 |
qed "ch2ch_Rep_CFunR"; |
|
243
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 |
|
5291 | 131 |
bind_thm ("ch2ch_Rep_CFunL", monofun_Rep_CFun1 RS ch2ch_MF2L); |
10834 | 132 |
(* chain(?F) ==> chain (%i. ?F i$?x) *) |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
133 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
134 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
135 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
136 |
(* the lub of a chain of continous functions is monotone *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
137 |
(* use MF2 lemmas from Cont.ML *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
138 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
139 |
|
10834 | 140 |
Goal "chain(F) ==> monofun(% x. lub(range(% j.(F j)$x)))"; |
9245 | 141 |
by (rtac lub_MF2_mono 1); |
142 |
by (rtac monofun_Rep_CFun1 1); |
|
143 |
by (rtac (monofun_Rep_CFun2 RS allI) 1); |
|
144 |
by (atac 1); |
|
145 |
qed "lub_cfun_mono"; |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
146 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
147 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
148 |
(* a lemma about the exchange of lubs for type 'a -> 'b *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
149 |
(* use MF2 lemmas from Cont.ML *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
150 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
151 |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
152 |
Goal "[| chain(F); chain(Y) |] ==>\ |
10834 | 153 |
\ lub(range(%j. lub(range(%i. F(j)$(Y i))))) =\ |
154 |
\ lub(range(%i. lub(range(%j. F(j)$(Y i)))))"; |
|
9245 | 155 |
by (rtac ex_lubMF2 1); |
156 |
by (rtac monofun_Rep_CFun1 1); |
|
157 |
by (rtac (monofun_Rep_CFun2 RS allI) 1); |
|
158 |
by (atac 1); |
|
159 |
by (atac 1); |
|
160 |
qed "ex_lubcfun"; |
|
243
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 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
163 |
(* the lub of a chain of cont. functions is continuous *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
164 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
165 |
|
10834 | 166 |
Goal "chain(F) ==> cont(% x. lub(range(% j. F(j)$x)))"; |
9245 | 167 |
by (rtac monocontlub2cont 1); |
168 |
by (etac lub_cfun_mono 1); |
|
169 |
by (rtac contlubI 1); |
|
170 |
by (strip_tac 1); |
|
171 |
by (stac (contlub_cfun_arg RS ext) 1); |
|
172 |
by (atac 1); |
|
173 |
by (etac ex_lubcfun 1); |
|
174 |
by (atac 1); |
|
175 |
qed "cont_lubcfun"; |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
176 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
177 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
178 |
(* type 'a -> 'b is chain complete *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
179 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
180 |
|
10834 | 181 |
Goal "chain(CCF) ==> range(CCF) <<| (LAM x. lub(range(% i. CCF(i)$x)))"; |
9245 | 182 |
by (rtac is_lubI 1); |
183 |
by (rtac ub_rangeI 1); |
|
184 |
by (stac less_cfun 1); |
|
185 |
by (stac Abs_Cfun_inverse2 1); |
|
186 |
by (etac cont_lubcfun 1); |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
187 |
by (rtac (lub_fun RS is_lubD1 RS ub_rangeD) 1); |
9245 | 188 |
by (etac (monofun_Rep_CFun1 RS ch2ch_monofun) 1); |
189 |
by (stac less_cfun 1); |
|
190 |
by (stac Abs_Cfun_inverse2 1); |
|
191 |
by (etac cont_lubcfun 1); |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
192 |
by (rtac (lub_fun RS is_lub_lub) 1); |
9245 | 193 |
by (etac (monofun_Rep_CFun1 RS ch2ch_monofun) 1); |
194 |
by (etac (monofun_Rep_CFun1 RS ub2ub_monofun) 1); |
|
195 |
qed "lub_cfun"; |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
196 |
|
1779 | 197 |
bind_thm ("thelub_cfun", lub_cfun RS thelubI); |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
198 |
(* |
10834 | 199 |
chain(?CCF1) ==> lub (range ?CCF1) = (LAM x. lub (range (%i. ?CCF1 i$x))) |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
200 |
*) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
201 |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
202 |
Goal "chain(CCF::nat=>('a->'b)) ==> ? x. range(CCF) <<| x"; |
9245 | 203 |
by (rtac exI 1); |
204 |
by (etac lub_cfun 1); |
|
205 |
qed "cpo_cfun"; |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
206 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
207 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
208 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
209 |
(* Extensionality in 'a -> 'b *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
210 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
211 |
|
10834 | 212 |
val prems = Goal "(!!x. f$x = g$x) ==> f = g"; |
9245 | 213 |
by (res_inst_tac [("t","f")] (Rep_Cfun_inverse RS subst) 1); |
214 |
by (res_inst_tac [("t","g")] (Rep_Cfun_inverse RS subst) 1); |
|
215 |
by (res_inst_tac [("f","Abs_CFun")] arg_cong 1); |
|
216 |
by (rtac ext 1); |
|
217 |
by (resolve_tac prems 1); |
|
218 |
qed "ext_cfun"; |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
219 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
220 |
(* ------------------------------------------------------------------------ *) |
5291 | 221 |
(* Monotonicity of Abs_CFun *) |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
222 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
223 |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
224 |
Goal "[| cont(f); cont(g); f<<g|] ==> Abs_CFun(f)<<Abs_CFun(g)"; |
9245 | 225 |
by (rtac (less_cfun RS iffD2) 1); |
226 |
by (stac Abs_Cfun_inverse2 1); |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
227 |
by (assume_tac 1); |
9245 | 228 |
by (stac Abs_Cfun_inverse2 1); |
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
229 |
by (assume_tac 1); |
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
230 |
by (assume_tac 1); |
9245 | 231 |
qed "semi_monofun_Abs_CFun"; |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
232 |
|
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 |
(* Extenionality wrt. << in 'a -> 'b *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
235 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
236 |
|
10834 | 237 |
val prems = Goal "(!!x. f$x << g$x) ==> f << g"; |
9245 | 238 |
by (res_inst_tac [("t","f")] (Rep_Cfun_inverse RS subst) 1); |
239 |
by (res_inst_tac [("t","g")] (Rep_Cfun_inverse RS subst) 1); |
|
240 |
by (rtac semi_monofun_Abs_CFun 1); |
|
241 |
by (rtac cont_Rep_CFun2 1); |
|
242 |
by (rtac cont_Rep_CFun2 1); |
|
243 |
by (rtac (less_fun RS iffD2) 1); |
|
244 |
by (rtac allI 1); |
|
245 |
by (resolve_tac prems 1); |
|
246 |
qed "less_cfun2"; |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
247 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
248 |