author | paulson |
Mon, 23 Sep 1996 18:18:18 +0200 | |
changeset 2010 | 0a22b9d63a18 |
parent 1989 | 8e0ff1bfcfea |
child 2033 | 639de962ded4 |
permissions | -rw-r--r-- |
1461 | 1 |
(* Title: HOLCF/cfun2.thy |
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 |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
4 |
Copyright 1993 Technische Universitaet Muenchen |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
5 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
6 |
Lemmas for cfun2.thy |
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 |
open Cfun2; |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
10 |
|
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 |
(* access to less_cfun in class po *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
13 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
14 |
|
892 | 15 |
qed_goal "less_cfun" Cfun2.thy "( f1 << f2 ) = (fapp(f1) << fapp(f2))" |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
16 |
(fn prems => |
1461 | 17 |
[ |
18 |
(rtac (inst_cfun_po RS ssubst) 1), |
|
19 |
(fold_goals_tac [less_cfun_def]), |
|
20 |
(rtac refl 1) |
|
21 |
]); |
|
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 |
|
892 | 27 |
qed_goalw "minimal_cfun" Cfun2.thy [UU_cfun_def] "UU_cfun << f" |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
28 |
(fn prems => |
1461 | 29 |
[ |
30 |
(rtac (less_cfun RS ssubst) 1), |
|
31 |
(rtac (Abs_Cfun_inverse2 RS ssubst) 1), |
|
32 |
(rtac cont_const 1), |
|
33 |
(fold_goals_tac [UU_fun_def]), |
|
34 |
(rtac minimal_fun 1) |
|
35 |
]); |
|
243
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 |
(* fapp yields continuous functions in 'a => 'b *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
39 |
(* this is continuity of fapp in its 'second' argument *) |
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
892
diff
changeset
|
40 |
(* cont_fapp2 ==> monofun_fapp2 & contlub_fapp2 *) |
243
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 |
|
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
892
diff
changeset
|
43 |
qed_goal "cont_fapp2" Cfun2.thy "cont(fapp(fo))" |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
44 |
(fn prems => |
1461 | 45 |
[ |
46 |
(res_inst_tac [("P","cont")] CollectD 1), |
|
47 |
(fold_goals_tac [Cfun_def]), |
|
48 |
(rtac Rep_Cfun 1) |
|
49 |
]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
50 |
|
1779 | 51 |
bind_thm ("monofun_fapp2", cont_fapp2 RS cont2mono); |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
52 |
(* monofun(fapp(?fo1)) *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
53 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
54 |
|
1779 | 55 |
bind_thm ("contlub_fapp2", cont_fapp2 RS cont2contlub); |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
56 |
(* contlub(fapp(?fo1)) *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
57 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
58 |
(* ------------------------------------------------------------------------ *) |
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
892
diff
changeset
|
59 |
(* expanded thms cont_fapp2, contlub_fapp2 *) |
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
892
diff
changeset
|
60 |
(* looks nice with mixfix syntac *) |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
61 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
62 |
|
1779 | 63 |
bind_thm ("cont_cfun_arg", (cont_fapp2 RS contE RS spec RS mp)); |
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
892
diff
changeset
|
64 |
(* is_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
|
65 |
|
1779 | 66 |
bind_thm ("contlub_cfun_arg", (contlub_fapp2 RS contlubE RS spec RS mp)); |
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
892
diff
changeset
|
67 |
(* is_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
|
68 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
69 |
|
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 |
(* fapp is monotone in its 'first' argument *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
72 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
73 |
|
892 | 74 |
qed_goalw "monofun_fapp1" Cfun2.thy [monofun] "monofun(fapp)" |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
75 |
(fn prems => |
1461 | 76 |
[ |
77 |
(strip_tac 1), |
|
78 |
(etac (less_cfun RS subst) 1) |
|
79 |
]); |
|
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 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
83 |
(* monotonicity of application fapp in mixfix syntax [_]_ *) |
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 |
|
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
892
diff
changeset
|
86 |
qed_goal "monofun_cfun_fun" Cfun2.thy "f1 << f2 ==> f1`x << f2`x" |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
87 |
(fn prems => |
1461 | 88 |
[ |
89 |
(cut_facts_tac prems 1), |
|
90 |
(res_inst_tac [("x","x")] spec 1), |
|
91 |
(rtac (less_fun RS subst) 1), |
|
92 |
(etac (monofun_fapp1 RS monofunE RS spec RS spec RS mp) 1) |
|
93 |
]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
94 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
95 |
|
1779 | 96 |
bind_thm ("monofun_cfun_arg", monofun_fapp2 RS monofunE RS spec RS spec RS mp); |
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
892
diff
changeset
|
97 |
(* ?x2 << ?x1 ==> ?fo5`?x2 << ?fo5`?x1 *) |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
98 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
99 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
100 |
(* monotonicity of fapp in both arguments in mixfix syntax [_]_ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
101 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
102 |
|
892 | 103 |
qed_goal "monofun_cfun" Cfun2.thy |
1461 | 104 |
"[|f1<<f2;x1<<x2|] ==> f1`x1 << f2`x2" |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
105 |
(fn prems => |
1461 | 106 |
[ |
107 |
(cut_facts_tac prems 1), |
|
108 |
(rtac trans_less 1), |
|
109 |
(etac monofun_cfun_arg 1), |
|
110 |
(etac monofun_cfun_fun 1) |
|
111 |
]); |
|
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 |
|
1989 | 114 |
qed_goal "strictI" Cfun2.thy "f`x = UU ==> f`UU = UU" (fn prems => [ |
115 |
cut_facts_tac prems 1, |
|
116 |
rtac (eq_UU_iff RS iffD2) 1, |
|
117 |
etac subst 1, |
|
118 |
rtac (minimal RS monofun_cfun_arg) 1]); |
|
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 |
|
892 | 126 |
qed_goal "ch2ch_fappR" Cfun2.thy |
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
892
diff
changeset
|
127 |
"is_chain(Y) ==> is_chain(%i. f`(Y i))" |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
128 |
(fn prems => |
1461 | 129 |
[ |
130 |
(cut_facts_tac prems 1), |
|
131 |
(etac (monofun_fapp2 RS ch2ch_MF2R) 1) |
|
132 |
]); |
|
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 |
|
1779 | 135 |
bind_thm ("ch2ch_fappL", monofun_fapp1 RS ch2ch_MF2L); |
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
892
diff
changeset
|
136 |
(* is_chain(?F) ==> is_chain (%i. ?F i`?x) *) |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
137 |
|
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 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
140 |
(* 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
|
141 |
(* use MF2 lemmas from Cont.ML *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
142 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
143 |
|
892 | 144 |
qed_goal "lub_cfun_mono" Cfun2.thy |
1461 | 145 |
"is_chain(F) ==> monofun(% x.lub(range(% j.(F j)`x)))" |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
146 |
(fn prems => |
1461 | 147 |
[ |
148 |
(cut_facts_tac prems 1), |
|
149 |
(rtac lub_MF2_mono 1), |
|
150 |
(rtac monofun_fapp1 1), |
|
151 |
(rtac (monofun_fapp2 RS allI) 1), |
|
152 |
(atac 1) |
|
153 |
]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
154 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
155 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
156 |
(* 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
|
157 |
(* use MF2 lemmas from Cont.ML *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
158 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
159 |
|
892 | 160 |
qed_goal "ex_lubcfun" Cfun2.thy |
1461 | 161 |
"[| is_chain(F); is_chain(Y) |] ==>\ |
162 |
\ lub(range(%j. lub(range(%i. F(j)`(Y i))))) =\ |
|
163 |
\ lub(range(%i. lub(range(%j. F(j)`(Y i)))))" |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
164 |
(fn prems => |
1461 | 165 |
[ |
166 |
(cut_facts_tac prems 1), |
|
167 |
(rtac ex_lubMF2 1), |
|
168 |
(rtac monofun_fapp1 1), |
|
169 |
(rtac (monofun_fapp2 RS allI) 1), |
|
170 |
(atac 1), |
|
171 |
(atac 1) |
|
172 |
]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
173 |
|
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 |
(* 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
|
176 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
177 |
|
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
892
diff
changeset
|
178 |
qed_goal "cont_lubcfun" Cfun2.thy |
1461 | 179 |
"is_chain(F) ==> cont(% x.lub(range(% j.F(j)`x)))" |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
180 |
(fn prems => |
1461 | 181 |
[ |
182 |
(cut_facts_tac prems 1), |
|
183 |
(rtac monocontlub2cont 1), |
|
184 |
(etac lub_cfun_mono 1), |
|
185 |
(rtac contlubI 1), |
|
186 |
(strip_tac 1), |
|
187 |
(rtac (contlub_cfun_arg RS ext RS ssubst) 1), |
|
188 |
(atac 1), |
|
189 |
(etac ex_lubcfun 1), |
|
190 |
(atac 1) |
|
191 |
]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
192 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
193 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
194 |
(* type 'a -> 'b is chain complete *) |
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 |
|
892 | 197 |
qed_goal "lub_cfun" Cfun2.thy |
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
892
diff
changeset
|
198 |
"is_chain(CCF) ==> range(CCF) <<| (LAM x.lub(range(% i.CCF(i)`x)))" |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
199 |
(fn prems => |
1461 | 200 |
[ |
201 |
(cut_facts_tac prems 1), |
|
202 |
(rtac is_lubI 1), |
|
203 |
(rtac conjI 1), |
|
204 |
(rtac ub_rangeI 1), |
|
205 |
(rtac allI 1), |
|
206 |
(rtac (less_cfun RS ssubst) 1), |
|
207 |
(rtac (Abs_Cfun_inverse2 RS ssubst) 1), |
|
208 |
(etac cont_lubcfun 1), |
|
209 |
(rtac (lub_fun RS is_lubE RS conjunct1 RS ub_rangeE RS spec) 1), |
|
210 |
(etac (monofun_fapp1 RS ch2ch_monofun) 1), |
|
211 |
(strip_tac 1), |
|
212 |
(rtac (less_cfun RS ssubst) 1), |
|
213 |
(rtac (Abs_Cfun_inverse2 RS ssubst) 1), |
|
214 |
(etac cont_lubcfun 1), |
|
215 |
(rtac (lub_fun RS is_lubE RS conjunct2 RS spec RS mp) 1), |
|
216 |
(etac (monofun_fapp1 RS ch2ch_monofun) 1), |
|
217 |
(etac (monofun_fapp1 RS ub2ub_monofun) 1) |
|
218 |
]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
219 |
|
1779 | 220 |
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
|
221 |
(* |
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
892
diff
changeset
|
222 |
is_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
|
223 |
*) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
224 |
|
892 | 225 |
qed_goal "cpo_cfun" Cfun2.thy |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
226 |
"is_chain(CCF::nat=>('a::pcpo->'b::pcpo)) ==> ? x. range(CCF) <<| x" |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
227 |
(fn prems => |
1461 | 228 |
[ |
229 |
(cut_facts_tac prems 1), |
|
230 |
(rtac exI 1), |
|
231 |
(etac lub_cfun 1) |
|
232 |
]); |
|
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 |
|
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 |
(* Extensionality in 'a -> 'b *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
237 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
238 |
|
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
892
diff
changeset
|
239 |
qed_goal "ext_cfun" Cfun1.thy "(!!x. f`x = g`x) ==> f = g" |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
240 |
(fn prems => |
1461 | 241 |
[ |
242 |
(res_inst_tac [("t","f")] (Rep_Cfun_inverse RS subst) 1), |
|
243 |
(res_inst_tac [("t","g")] (Rep_Cfun_inverse RS subst) 1), |
|
244 |
(res_inst_tac [("f","fabs")] arg_cong 1), |
|
245 |
(rtac ext 1), |
|
246 |
(resolve_tac prems 1) |
|
247 |
]); |
|
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 |
(* Monotonicity of fabs *) |
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 |
|
892 | 253 |
qed_goal "semi_monofun_fabs" Cfun2.thy |
1461 | 254 |
"[|cont(f);cont(g);f<<g|]==>fabs(f)<<fabs(g)" |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
255 |
(fn prems => |
1461 | 256 |
[ |
257 |
(rtac (less_cfun RS iffD2) 1), |
|
258 |
(rtac (Abs_Cfun_inverse2 RS ssubst) 1), |
|
259 |
(resolve_tac prems 1), |
|
260 |
(rtac (Abs_Cfun_inverse2 RS ssubst) 1), |
|
261 |
(resolve_tac prems 1), |
|
262 |
(resolve_tac prems 1) |
|
263 |
]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
264 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
265 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
266 |
(* Extenionality wrt. << in 'a -> 'b *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
267 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
268 |
|
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
892
diff
changeset
|
269 |
qed_goal "less_cfun2" Cfun2.thy "(!!x. f`x << g`x) ==> f << g" |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
270 |
(fn prems => |
1461 | 271 |
[ |
272 |
(res_inst_tac [("t","f")] (Rep_Cfun_inverse RS subst) 1), |
|
273 |
(res_inst_tac [("t","g")] (Rep_Cfun_inverse RS subst) 1), |
|
274 |
(rtac semi_monofun_fabs 1), |
|
275 |
(rtac cont_fapp2 1), |
|
276 |
(rtac cont_fapp2 1), |
|
277 |
(rtac (less_fun RS iffD2) 1), |
|
278 |
(rtac allI 1), |
|
279 |
(resolve_tac prems 1) |
|
280 |
]); |
|
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 |