author | paulson |
Mon, 16 Dec 1996 10:50:08 +0100 | |
changeset 2416 | 8ba800a46e14 |
parent 2394 | 91d8abf108be |
child 2445 | 51993fea433f |
permissions | -rw-r--r-- |
1461 | 1 |
(* Title: HOLCF/pcpo.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 |
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 pcpo.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 Pcpo; |
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 |
(* in pcpo's everthing equal to THE lub has lub properties for every chain *) |
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 "thelubE" Pcpo.thy |
1461 | 16 |
"[| is_chain(S);lub(range(S)) = (l::'a::pcpo)|] ==> range(S) <<| l " |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
17 |
(fn prems => |
1461 | 18 |
[ |
19 |
(cut_facts_tac prems 1), |
|
20 |
(hyp_subst_tac 1), |
|
21 |
(rtac lubI 1), |
|
22 |
(etac cpo 1) |
|
23 |
]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
24 |
|
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 |
(* Properties of the lub *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
27 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
28 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
29 |
|
1779 | 30 |
bind_thm ("is_ub_thelub", cpo RS lubI RS is_ub_lub); |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
31 |
(* is_chain(?S1) ==> ?S1(?x) << lub(range(?S1)) *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
32 |
|
1779 | 33 |
bind_thm ("is_lub_thelub", cpo RS lubI RS is_lub_lub); |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
34 |
(* [| is_chain(?S5); range(?S5) <| ?x1 |] ==> lub(range(?S5)) << ?x1 *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
35 |
|
2354 | 36 |
qed_goal "maxinch_is_thelub" Pcpo.thy "is_chain Y ==> \ |
2394 | 37 |
\ max_in_chain i Y = (lub(range(Y)) = ((Y i)::'a::pcpo))" |
2354 | 38 |
(fn prems => |
2416 | 39 |
[ |
40 |
cut_facts_tac prems 1, |
|
41 |
rtac iffI 1, |
|
42 |
fast_tac (HOL_cs addSIs [thelubI,lub_finch1]) 1, |
|
43 |
rewtac max_in_chain_def, |
|
44 |
safe_tac (HOL_cs addSIs [antisym_less]), |
|
45 |
fast_tac (HOL_cs addSEs [chain_mono3]) 1, |
|
46 |
dtac sym 1, |
|
47 |
fast_tac ((HOL_cs addSEs [is_ub_thelub]) addss !simpset) 1 |
|
48 |
]); |
|
2354 | 49 |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
50 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
51 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
52 |
(* the << relation between two chains is preserved by their lubs *) |
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 |
|
892 | 55 |
qed_goal "lub_mono" Pcpo.thy |
1461 | 56 |
"[|is_chain(C1::(nat=>'a::pcpo));is_chain(C2); ! k. C1(k) << C2(k)|]\ |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
57 |
\ ==> lub(range(C1)) << lub(range(C2))" |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
58 |
(fn prems => |
1461 | 59 |
[ |
60 |
(cut_facts_tac prems 1), |
|
61 |
(etac is_lub_thelub 1), |
|
62 |
(rtac ub_rangeI 1), |
|
63 |
(rtac allI 1), |
|
64 |
(rtac trans_less 1), |
|
65 |
(etac spec 1), |
|
66 |
(etac is_ub_thelub 1) |
|
67 |
]); |
|
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 |
(* the = relation between two chains is preserved by their lubs *) |
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 |
|
892 | 73 |
qed_goal "lub_equal" Pcpo.thy |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
74 |
"[| is_chain(C1::(nat=>'a::pcpo));is_chain(C2);!k.C1(k)=C2(k)|]\ |
1461 | 75 |
\ ==> lub(range(C1))=lub(range(C2))" |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
76 |
(fn prems => |
1461 | 77 |
[ |
78 |
(cut_facts_tac prems 1), |
|
79 |
(rtac antisym_less 1), |
|
80 |
(rtac lub_mono 1), |
|
81 |
(atac 1), |
|
82 |
(atac 1), |
|
83 |
(strip_tac 1), |
|
84 |
(rtac (antisym_less_inverse RS conjunct1) 1), |
|
85 |
(etac spec 1), |
|
86 |
(rtac lub_mono 1), |
|
87 |
(atac 1), |
|
88 |
(atac 1), |
|
89 |
(strip_tac 1), |
|
90 |
(rtac (antisym_less_inverse RS conjunct2) 1), |
|
91 |
(etac spec 1) |
|
92 |
]); |
|
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 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
95 |
(* more results about mono and = of lubs of chains *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
96 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
97 |
|
892 | 98 |
qed_goal "lub_mono2" Pcpo.thy |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
99 |
"[|? j.!i. j<i --> X(i::nat)=Y(i);is_chain(X::nat=>'a::pcpo);is_chain(Y)|]\ |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
100 |
\ ==> lub(range(X))<<lub(range(Y))" |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
101 |
(fn prems => |
1461 | 102 |
[ |
103 |
(rtac exE 1), |
|
104 |
(resolve_tac prems 1), |
|
105 |
(rtac is_lub_thelub 1), |
|
106 |
(resolve_tac prems 1), |
|
107 |
(rtac ub_rangeI 1), |
|
108 |
(strip_tac 1), |
|
1675 | 109 |
(case_tac "x<i" 1), |
1461 | 110 |
(res_inst_tac [("s","Y(i)"),("t","X(i)")] subst 1), |
111 |
(rtac sym 1), |
|
112 |
(fast_tac HOL_cs 1), |
|
113 |
(rtac is_ub_thelub 1), |
|
114 |
(resolve_tac prems 1), |
|
115 |
(res_inst_tac [("y","X(Suc(x))")] trans_less 1), |
|
116 |
(rtac (chain_mono RS mp) 1), |
|
117 |
(resolve_tac prems 1), |
|
118 |
(rtac (not_less_eq RS subst) 1), |
|
119 |
(atac 1), |
|
120 |
(res_inst_tac [("s","Y(Suc(x))"),("t","X(Suc(x))")] subst 1), |
|
121 |
(rtac sym 1), |
|
122 |
(Asm_simp_tac 1), |
|
123 |
(rtac is_ub_thelub 1), |
|
124 |
(resolve_tac prems 1) |
|
125 |
]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
126 |
|
892 | 127 |
qed_goal "lub_equal2" Pcpo.thy |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
128 |
"[|? j.!i. j<i --> X(i)=Y(i);is_chain(X::nat=>'a::pcpo);is_chain(Y)|]\ |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
129 |
\ ==> lub(range(X))=lub(range(Y))" |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
130 |
(fn prems => |
1461 | 131 |
[ |
132 |
(rtac antisym_less 1), |
|
133 |
(rtac lub_mono2 1), |
|
134 |
(REPEAT (resolve_tac prems 1)), |
|
135 |
(cut_facts_tac prems 1), |
|
136 |
(rtac lub_mono2 1), |
|
137 |
(safe_tac HOL_cs), |
|
138 |
(step_tac HOL_cs 1), |
|
139 |
(safe_tac HOL_cs), |
|
140 |
(rtac sym 1), |
|
141 |
(fast_tac HOL_cs 1) |
|
142 |
]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
143 |
|
892 | 144 |
qed_goal "lub_mono3" Pcpo.thy "[|is_chain(Y::nat=>'a::pcpo);is_chain(X);\ |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
145 |
\! i. ? j. Y(i)<< X(j)|]==> lub(range(Y))<<lub(range(X))" |
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 is_lub_thelub 1), |
|
150 |
(atac 1), |
|
151 |
(rtac ub_rangeI 1), |
|
152 |
(strip_tac 1), |
|
153 |
(etac allE 1), |
|
154 |
(etac exE 1), |
|
155 |
(rtac trans_less 1), |
|
156 |
(rtac is_ub_thelub 2), |
|
157 |
(atac 2), |
|
158 |
(atac 1) |
|
159 |
]); |
|
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 |
(* usefull lemmas about UU *) |
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 |
|
2275 | 165 |
val eq_UU_sym = prove_goal Pcpo.thy "(UU = x) = (x = UU)" (fn _ => [ |
2416 | 166 |
fast_tac HOL_cs 1]); |
2275 | 167 |
|
892 | 168 |
qed_goal "eq_UU_iff" Pcpo.thy "(x=UU)=(x<<UU)" |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
169 |
(fn prems => |
1461 | 170 |
[ |
171 |
(rtac iffI 1), |
|
172 |
(hyp_subst_tac 1), |
|
173 |
(rtac refl_less 1), |
|
174 |
(rtac antisym_less 1), |
|
175 |
(atac 1), |
|
176 |
(rtac minimal 1) |
|
177 |
]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
178 |
|
892 | 179 |
qed_goal "UU_I" Pcpo.thy "x << UU ==> x = UU" |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
180 |
(fn prems => |
1461 | 181 |
[ |
2033 | 182 |
(stac eq_UU_iff 1), |
1461 | 183 |
(resolve_tac prems 1) |
184 |
]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
185 |
|
892 | 186 |
qed_goal "not_less2not_eq" Pcpo.thy "~x<<y ==> ~x=y" |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
187 |
(fn prems => |
1461 | 188 |
[ |
189 |
(cut_facts_tac prems 1), |
|
190 |
(rtac classical3 1), |
|
191 |
(atac 1), |
|
192 |
(hyp_subst_tac 1), |
|
193 |
(rtac refl_less 1) |
|
194 |
]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
195 |
|
892 | 196 |
qed_goal "chain_UU_I" Pcpo.thy |
1461 | 197 |
"[|is_chain(Y);lub(range(Y))=UU|] ==> ! i.Y(i)=UU" |
1043 | 198 |
(fn prems => |
1461 | 199 |
[ |
200 |
(cut_facts_tac prems 1), |
|
201 |
(rtac allI 1), |
|
202 |
(rtac antisym_less 1), |
|
203 |
(rtac minimal 2), |
|
204 |
(etac subst 1), |
|
205 |
(etac is_ub_thelub 1) |
|
206 |
]); |
|
243
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 |
|
892 | 209 |
qed_goal "chain_UU_I_inverse" Pcpo.thy |
1461 | 210 |
"!i.Y(i::nat)=UU ==> lub(range(Y::(nat=>'a::pcpo)))=UU" |
1043 | 211 |
(fn prems => |
1461 | 212 |
[ |
213 |
(cut_facts_tac prems 1), |
|
214 |
(rtac lub_chain_maxelem 1), |
|
215 |
(rtac exI 1), |
|
216 |
(etac spec 1), |
|
217 |
(rtac allI 1), |
|
218 |
(rtac (antisym_less_inverse RS conjunct1) 1), |
|
219 |
(etac spec 1) |
|
220 |
]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
221 |
|
892 | 222 |
qed_goal "chain_UU_I_inverse2" Pcpo.thy |
1461 | 223 |
"~lub(range(Y::(nat=>'a::pcpo)))=UU ==> ? i.~ Y(i)=UU" |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
224 |
(fn prems => |
1461 | 225 |
[ |
226 |
(cut_facts_tac prems 1), |
|
1675 | 227 |
(rtac (not_all RS iffD1) 1), |
1461 | 228 |
(rtac swap 1), |
229 |
(rtac chain_UU_I_inverse 2), |
|
230 |
(etac notnotD 2), |
|
231 |
(atac 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 |
|
892 | 235 |
qed_goal "notUU_I" Pcpo.thy "[| x<<y; ~x=UU |] ==> ~y=UU" |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
236 |
(fn prems => |
1461 | 237 |
[ |
238 |
(cut_facts_tac prems 1), |
|
239 |
(etac contrapos 1), |
|
240 |
(rtac UU_I 1), |
|
241 |
(hyp_subst_tac 1), |
|
242 |
(atac 1) |
|
243 |
]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
244 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
245 |
|
892 | 246 |
qed_goal "chain_mono2" Pcpo.thy |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
247 |
"[|? j.~Y(j)=UU;is_chain(Y::nat=>'a::pcpo)|]\ |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
248 |
\ ==> ? j.!i.j<i-->~Y(i)=UU" |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
249 |
(fn prems => |
1461 | 250 |
[ |
251 |
(cut_facts_tac prems 1), |
|
252 |
(safe_tac HOL_cs), |
|
253 |
(step_tac HOL_cs 1), |
|
254 |
(strip_tac 1), |
|
255 |
(rtac notUU_I 1), |
|
256 |
(atac 2), |
|
257 |
(etac (chain_mono RS mp) 1), |
|
258 |
(atac 1) |
|
259 |
]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
260 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
261 |
|
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 |
|
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 |
(* uniqueness in void *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
266 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
267 |
|
892 | 268 |
qed_goal "unique_void2" Pcpo.thy "(x::void)=UU" |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
269 |
(fn prems => |
1461 | 270 |
[ |
2033 | 271 |
(stac inst_void_pcpo 1), |
1461 | 272 |
(rtac (Rep_Void_inverse RS subst) 1), |
273 |
(rtac (Rep_Void_inverse RS subst) 1), |
|
274 |
(rtac arg_cong 1), |
|
275 |
(rtac box_equals 1), |
|
276 |
(rtac refl 1), |
|
277 |
(rtac (unique_void RS sym) 1), |
|
278 |
(rtac (unique_void RS sym) 1) |
|
279 |
]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
280 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
281 |