author | clasohm |
Tue, 30 Jan 1996 13:42:57 +0100 | |
changeset 1461 | 6bcb44e4d6e5 |
parent 1277 | caef3601c0b2 |
child 1675 | 36ba4da350c3 |
permissions | -rw-r--r-- |
1461 | 1 |
(* Title: HOLCF/ssum3.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 ssum3.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 Ssum3; |
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 |
(* continuity for Isinl and Isinr *) |
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 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
15 |
|
892 | 16 |
qed_goal "contlub_Isinl" Ssum3.thy "contlub(Isinl)" |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
17 |
(fn prems => |
1461 | 18 |
[ |
19 |
(rtac contlubI 1), |
|
20 |
(strip_tac 1), |
|
21 |
(rtac trans 1), |
|
22 |
(rtac (thelub_ssum1a RS sym) 2), |
|
23 |
(rtac allI 3), |
|
24 |
(rtac exI 3), |
|
25 |
(rtac refl 3), |
|
26 |
(etac (monofun_Isinl RS ch2ch_monofun) 2), |
|
27 |
(res_inst_tac [("Q","lub(range(Y))=UU")] classical2 1), |
|
28 |
(res_inst_tac [("s","UU"),("t","lub(range(Y))")] ssubst 1), |
|
29 |
(atac 1), |
|
30 |
(res_inst_tac [("f","Isinl")] arg_cong 1), |
|
31 |
(rtac (chain_UU_I_inverse RS sym) 1), |
|
32 |
(rtac allI 1), |
|
33 |
(res_inst_tac [("s","UU"),("t","Y(i)")] ssubst 1), |
|
34 |
(etac (chain_UU_I RS spec ) 1), |
|
35 |
(atac 1), |
|
36 |
(rtac Iwhen1 1), |
|
37 |
(res_inst_tac [("f","Isinl")] arg_cong 1), |
|
38 |
(rtac lub_equal 1), |
|
39 |
(atac 1), |
|
40 |
(rtac (monofun_Iwhen3 RS ch2ch_monofun) 1), |
|
41 |
(etac (monofun_Isinl RS ch2ch_monofun) 1), |
|
42 |
(rtac allI 1), |
|
43 |
(res_inst_tac [("Q","Y(k)=UU")] classical2 1), |
|
44 |
(asm_simp_tac Ssum0_ss 1), |
|
45 |
(asm_simp_tac Ssum0_ss 1) |
|
46 |
]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
47 |
|
892 | 48 |
qed_goal "contlub_Isinr" Ssum3.thy "contlub(Isinr)" |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
49 |
(fn prems => |
1461 | 50 |
[ |
51 |
(rtac contlubI 1), |
|
52 |
(strip_tac 1), |
|
53 |
(rtac trans 1), |
|
54 |
(rtac (thelub_ssum1b RS sym) 2), |
|
55 |
(rtac allI 3), |
|
56 |
(rtac exI 3), |
|
57 |
(rtac refl 3), |
|
58 |
(etac (monofun_Isinr RS ch2ch_monofun) 2), |
|
59 |
(res_inst_tac [("Q","lub(range(Y))=UU")] classical2 1), |
|
60 |
(res_inst_tac [("s","UU"),("t","lub(range(Y))")] ssubst 1), |
|
61 |
(atac 1), |
|
62 |
((rtac arg_cong 1) THEN (rtac (chain_UU_I_inverse RS sym) 1)), |
|
63 |
(rtac allI 1), |
|
64 |
(res_inst_tac [("s","UU"),("t","Y(i)")] ssubst 1), |
|
65 |
(etac (chain_UU_I RS spec ) 1), |
|
66 |
(atac 1), |
|
67 |
(rtac (strict_IsinlIsinr RS subst) 1), |
|
68 |
(rtac Iwhen1 1), |
|
69 |
((rtac arg_cong 1) THEN (rtac lub_equal 1)), |
|
70 |
(atac 1), |
|
71 |
(rtac (monofun_Iwhen3 RS ch2ch_monofun) 1), |
|
72 |
(etac (monofun_Isinr RS ch2ch_monofun) 1), |
|
73 |
(rtac allI 1), |
|
74 |
(res_inst_tac [("Q","Y(k)=UU")] classical2 1), |
|
75 |
(asm_simp_tac Ssum0_ss 1), |
|
76 |
(asm_simp_tac Ssum0_ss 1) |
|
77 |
]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
78 |
|
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
892
diff
changeset
|
79 |
qed_goal "cont_Isinl" Ssum3.thy "cont(Isinl)" |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
80 |
(fn prems => |
1461 | 81 |
[ |
82 |
(rtac monocontlub2cont 1), |
|
83 |
(rtac monofun_Isinl 1), |
|
84 |
(rtac contlub_Isinl 1) |
|
85 |
]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
86 |
|
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
892
diff
changeset
|
87 |
qed_goal "cont_Isinr" Ssum3.thy "cont(Isinr)" |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
88 |
(fn prems => |
1461 | 89 |
[ |
90 |
(rtac monocontlub2cont 1), |
|
91 |
(rtac monofun_Isinr 1), |
|
92 |
(rtac contlub_Isinr 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 |
|
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 |
(* continuity for Iwhen in the firts two arguments *) |
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 |
|
892 | 100 |
qed_goal "contlub_Iwhen1" Ssum3.thy "contlub(Iwhen)" |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
101 |
(fn prems => |
1461 | 102 |
[ |
103 |
(rtac contlubI 1), |
|
104 |
(strip_tac 1), |
|
105 |
(rtac trans 1), |
|
106 |
(rtac (thelub_fun RS sym) 2), |
|
107 |
(etac (monofun_Iwhen1 RS ch2ch_monofun) 2), |
|
108 |
(rtac (expand_fun_eq RS iffD2) 1), |
|
109 |
(strip_tac 1), |
|
110 |
(rtac trans 1), |
|
111 |
(rtac (thelub_fun RS sym) 2), |
|
112 |
(rtac ch2ch_fun 2), |
|
113 |
(etac (monofun_Iwhen1 RS ch2ch_monofun) 2), |
|
114 |
(rtac (expand_fun_eq RS iffD2) 1), |
|
115 |
(strip_tac 1), |
|
116 |
(res_inst_tac [("p","xa")] IssumE 1), |
|
117 |
(asm_simp_tac Ssum0_ss 1), |
|
118 |
(rtac (lub_const RS thelubI RS sym) 1), |
|
119 |
(asm_simp_tac Ssum0_ss 1), |
|
120 |
(etac contlub_cfun_fun 1), |
|
121 |
(asm_simp_tac Ssum0_ss 1), |
|
122 |
(rtac (lub_const RS thelubI RS sym) 1) |
|
123 |
]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
124 |
|
892 | 125 |
qed_goal "contlub_Iwhen2" Ssum3.thy "contlub(Iwhen(f))" |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
126 |
(fn prems => |
1461 | 127 |
[ |
128 |
(rtac contlubI 1), |
|
129 |
(strip_tac 1), |
|
130 |
(rtac trans 1), |
|
131 |
(rtac (thelub_fun RS sym) 2), |
|
132 |
(etac (monofun_Iwhen2 RS ch2ch_monofun) 2), |
|
133 |
(rtac (expand_fun_eq RS iffD2) 1), |
|
134 |
(strip_tac 1), |
|
135 |
(res_inst_tac [("p","x")] IssumE 1), |
|
136 |
(asm_simp_tac Ssum0_ss 1), |
|
137 |
(rtac (lub_const RS thelubI RS sym) 1), |
|
138 |
(asm_simp_tac Ssum0_ss 1), |
|
139 |
(rtac (lub_const RS thelubI RS sym) 1), |
|
140 |
(asm_simp_tac Ssum0_ss 1), |
|
141 |
(etac contlub_cfun_fun 1) |
|
142 |
]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
143 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
144 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
145 |
(* continuity for Iwhen in its third argument *) |
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 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
149 |
(* first 5 ugly lemmas *) |
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 |
|
892 | 152 |
qed_goal "ssum_lemma9" Ssum3.thy |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
153 |
"[| is_chain(Y); lub(range(Y)) = Isinl(x)|] ==> !i.? x.Y(i)=Isinl(x)" |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
154 |
(fn prems => |
1461 | 155 |
[ |
156 |
(cut_facts_tac prems 1), |
|
157 |
(strip_tac 1), |
|
158 |
(res_inst_tac [("p","Y(i)")] IssumE 1), |
|
159 |
(etac exI 1), |
|
160 |
(etac exI 1), |
|
161 |
(res_inst_tac [("P","y=UU")] notE 1), |
|
162 |
(atac 1), |
|
163 |
(rtac (less_ssum3d RS iffD1) 1), |
|
164 |
(etac subst 1), |
|
165 |
(etac subst 1), |
|
166 |
(etac is_ub_thelub 1) |
|
167 |
]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
168 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
169 |
|
892 | 170 |
qed_goal "ssum_lemma10" Ssum3.thy |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
171 |
"[| is_chain(Y); lub(range(Y)) = Isinr(x)|] ==> !i.? x.Y(i)=Isinr(x)" |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
172 |
(fn prems => |
1461 | 173 |
[ |
174 |
(cut_facts_tac prems 1), |
|
175 |
(strip_tac 1), |
|
176 |
(res_inst_tac [("p","Y(i)")] IssumE 1), |
|
177 |
(rtac exI 1), |
|
178 |
(etac trans 1), |
|
179 |
(rtac strict_IsinlIsinr 1), |
|
180 |
(etac exI 2), |
|
181 |
(res_inst_tac [("P","xa=UU")] notE 1), |
|
182 |
(atac 1), |
|
183 |
(rtac (less_ssum3c RS iffD1) 1), |
|
184 |
(etac subst 1), |
|
185 |
(etac subst 1), |
|
186 |
(etac is_ub_thelub 1) |
|
187 |
]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
188 |
|
892 | 189 |
qed_goal "ssum_lemma11" Ssum3.thy |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
190 |
"[| is_chain(Y); lub(range(Y)) = Isinl(UU) |] ==>\ |
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
892
diff
changeset
|
191 |
\ Iwhen f g (lub(range Y)) = lub(range(%i. Iwhen f g (Y i)))" |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
192 |
(fn prems => |
1461 | 193 |
[ |
194 |
(cut_facts_tac prems 1), |
|
195 |
(asm_simp_tac Ssum0_ss 1), |
|
196 |
(rtac (chain_UU_I_inverse RS sym) 1), |
|
197 |
(rtac allI 1), |
|
198 |
(res_inst_tac [("s","Isinl(UU)"),("t","Y(i)")] subst 1), |
|
199 |
(rtac (inst_ssum_pcpo RS subst) 1), |
|
200 |
(rtac (chain_UU_I RS spec RS sym) 1), |
|
201 |
(atac 1), |
|
202 |
(etac (inst_ssum_pcpo RS ssubst) 1), |
|
203 |
(asm_simp_tac Ssum0_ss 1) |
|
204 |
]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
205 |
|
892 | 206 |
qed_goal "ssum_lemma12" Ssum3.thy |
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
892
diff
changeset
|
207 |
"[| is_chain(Y); lub(range(Y)) = Isinl(x); x ~= UU |] ==>\ |
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
892
diff
changeset
|
208 |
\ Iwhen f g (lub(range Y)) = lub(range(%i. Iwhen f g (Y i)))" |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
209 |
(fn prems => |
1461 | 210 |
[ |
211 |
(cut_facts_tac prems 1), |
|
212 |
(asm_simp_tac Ssum0_ss 1), |
|
213 |
(res_inst_tac [("t","x")] subst 1), |
|
214 |
(rtac inject_Isinl 1), |
|
215 |
(rtac trans 1), |
|
216 |
(atac 2), |
|
217 |
(rtac (thelub_ssum1a RS sym) 1), |
|
218 |
(atac 1), |
|
219 |
(etac ssum_lemma9 1), |
|
220 |
(atac 1), |
|
221 |
(rtac trans 1), |
|
222 |
(rtac contlub_cfun_arg 1), |
|
223 |
(rtac (monofun_Iwhen3 RS ch2ch_monofun) 1), |
|
224 |
(atac 1), |
|
225 |
(rtac lub_equal2 1), |
|
226 |
(rtac (chain_mono2 RS exE) 1), |
|
227 |
(atac 2), |
|
228 |
(rtac chain_UU_I_inverse2 1), |
|
229 |
(rtac (inst_ssum_pcpo RS ssubst) 1), |
|
230 |
(etac swap 1), |
|
231 |
(rtac inject_Isinl 1), |
|
232 |
(rtac trans 1), |
|
233 |
(etac sym 1), |
|
234 |
(etac notnotD 1), |
|
235 |
(rtac exI 1), |
|
236 |
(strip_tac 1), |
|
237 |
(rtac (ssum_lemma9 RS spec RS exE) 1), |
|
238 |
(atac 1), |
|
239 |
(atac 1), |
|
240 |
(res_inst_tac [("t","Y(i)")] ssubst 1), |
|
241 |
(atac 1), |
|
242 |
(rtac trans 1), |
|
243 |
(rtac cfun_arg_cong 1), |
|
244 |
(rtac Iwhen2 1), |
|
245 |
(res_inst_tac [("Pa","Y(i)=UU")] swap 1), |
|
246 |
(fast_tac HOL_cs 1), |
|
247 |
(rtac (inst_ssum_pcpo RS ssubst) 1), |
|
248 |
(res_inst_tac [("t","Y(i)")] ssubst 1), |
|
249 |
(atac 1), |
|
250 |
(fast_tac HOL_cs 1), |
|
251 |
(rtac (Iwhen2 RS ssubst) 1), |
|
252 |
(res_inst_tac [("Pa","Y(i)=UU")] swap 1), |
|
253 |
(fast_tac HOL_cs 1), |
|
254 |
(rtac (inst_ssum_pcpo RS ssubst) 1), |
|
255 |
(res_inst_tac [("t","Y(i)")] ssubst 1), |
|
256 |
(atac 1), |
|
257 |
(fast_tac HOL_cs 1), |
|
1277
caef3601c0b2
corrected some errors that occurred after introduction of local simpsets
regensbu
parents:
1274
diff
changeset
|
258 |
(simp_tac (simpset_of "Cfun3") 1), |
1461 | 259 |
(rtac (monofun_fapp2 RS ch2ch_monofun) 1), |
260 |
(etac (monofun_Iwhen3 RS ch2ch_monofun) 1), |
|
261 |
(etac (monofun_Iwhen3 RS ch2ch_monofun) 1) |
|
262 |
]); |
|
243
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 |
|
892 | 265 |
qed_goal "ssum_lemma13" Ssum3.thy |
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
892
diff
changeset
|
266 |
"[| is_chain(Y); lub(range(Y)) = Isinr(x); x ~= UU |] ==>\ |
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
892
diff
changeset
|
267 |
\ Iwhen f g (lub(range Y)) = lub(range(%i. Iwhen f g (Y i)))" |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
268 |
(fn prems => |
1461 | 269 |
[ |
270 |
(cut_facts_tac prems 1), |
|
271 |
(asm_simp_tac Ssum0_ss 1), |
|
272 |
(res_inst_tac [("t","x")] subst 1), |
|
273 |
(rtac inject_Isinr 1), |
|
274 |
(rtac trans 1), |
|
275 |
(atac 2), |
|
276 |
(rtac (thelub_ssum1b RS sym) 1), |
|
277 |
(atac 1), |
|
278 |
(etac ssum_lemma10 1), |
|
279 |
(atac 1), |
|
280 |
(rtac trans 1), |
|
281 |
(rtac contlub_cfun_arg 1), |
|
282 |
(rtac (monofun_Iwhen3 RS ch2ch_monofun) 1), |
|
283 |
(atac 1), |
|
284 |
(rtac lub_equal2 1), |
|
285 |
(rtac (chain_mono2 RS exE) 1), |
|
286 |
(atac 2), |
|
287 |
(rtac chain_UU_I_inverse2 1), |
|
288 |
(rtac (inst_ssum_pcpo RS ssubst) 1), |
|
289 |
(etac swap 1), |
|
290 |
(rtac inject_Isinr 1), |
|
291 |
(rtac trans 1), |
|
292 |
(etac sym 1), |
|
293 |
(rtac (strict_IsinlIsinr RS subst) 1), |
|
294 |
(etac notnotD 1), |
|
295 |
(rtac exI 1), |
|
296 |
(strip_tac 1), |
|
297 |
(rtac (ssum_lemma10 RS spec RS exE) 1), |
|
298 |
(atac 1), |
|
299 |
(atac 1), |
|
300 |
(res_inst_tac [("t","Y(i)")] ssubst 1), |
|
301 |
(atac 1), |
|
302 |
(rtac trans 1), |
|
303 |
(rtac cfun_arg_cong 1), |
|
304 |
(rtac Iwhen3 1), |
|
305 |
(res_inst_tac [("Pa","Y(i)=UU")] swap 1), |
|
306 |
(fast_tac HOL_cs 1), |
|
307 |
(dtac notnotD 1), |
|
308 |
(rtac (inst_ssum_pcpo RS ssubst) 1), |
|
309 |
(rtac (strict_IsinlIsinr RS ssubst) 1), |
|
310 |
(res_inst_tac [("t","Y(i)")] ssubst 1), |
|
311 |
(atac 1), |
|
312 |
(fast_tac HOL_cs 1), |
|
313 |
(rtac (Iwhen3 RS ssubst) 1), |
|
314 |
(res_inst_tac [("Pa","Y(i)=UU")] swap 1), |
|
315 |
(fast_tac HOL_cs 1), |
|
316 |
(dtac notnotD 1), |
|
317 |
(rtac (inst_ssum_pcpo RS ssubst) 1), |
|
318 |
(rtac (strict_IsinlIsinr RS ssubst) 1), |
|
319 |
(res_inst_tac [("t","Y(i)")] ssubst 1), |
|
320 |
(atac 1), |
|
321 |
(fast_tac HOL_cs 1), |
|
1277
caef3601c0b2
corrected some errors that occurred after introduction of local simpsets
regensbu
parents:
1274
diff
changeset
|
322 |
(simp_tac (simpset_of "Cfun3") 1), |
1461 | 323 |
(rtac (monofun_fapp2 RS ch2ch_monofun) 1), |
324 |
(etac (monofun_Iwhen3 RS ch2ch_monofun) 1), |
|
325 |
(etac (monofun_Iwhen3 RS ch2ch_monofun) 1) |
|
326 |
]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
327 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
328 |
|
892 | 329 |
qed_goal "contlub_Iwhen3" Ssum3.thy "contlub(Iwhen(f)(g))" |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
330 |
(fn prems => |
1461 | 331 |
[ |
332 |
(rtac contlubI 1), |
|
333 |
(strip_tac 1), |
|
334 |
(res_inst_tac [("p","lub(range(Y))")] IssumE 1), |
|
335 |
(etac ssum_lemma11 1), |
|
336 |
(atac 1), |
|
337 |
(etac ssum_lemma12 1), |
|
338 |
(atac 1), |
|
339 |
(atac 1), |
|
340 |
(etac ssum_lemma13 1), |
|
341 |
(atac 1), |
|
342 |
(atac 1) |
|
343 |
]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
344 |
|
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
892
diff
changeset
|
345 |
qed_goal "cont_Iwhen1" Ssum3.thy "cont(Iwhen)" |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
346 |
(fn prems => |
1461 | 347 |
[ |
348 |
(rtac monocontlub2cont 1), |
|
349 |
(rtac monofun_Iwhen1 1), |
|
350 |
(rtac contlub_Iwhen1 1) |
|
351 |
]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
352 |
|
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
892
diff
changeset
|
353 |
qed_goal "cont_Iwhen2" Ssum3.thy "cont(Iwhen(f))" |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
354 |
(fn prems => |
1461 | 355 |
[ |
356 |
(rtac monocontlub2cont 1), |
|
357 |
(rtac monofun_Iwhen2 1), |
|
358 |
(rtac contlub_Iwhen2 1) |
|
359 |
]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
360 |
|
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
892
diff
changeset
|
361 |
qed_goal "cont_Iwhen3" Ssum3.thy "cont(Iwhen(f)(g))" |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
362 |
(fn prems => |
1461 | 363 |
[ |
364 |
(rtac monocontlub2cont 1), |
|
365 |
(rtac monofun_Iwhen3 1), |
|
366 |
(rtac contlub_Iwhen3 1) |
|
367 |
]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
368 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
369 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
370 |
(* continuous versions of lemmas for 'a ++ 'b *) |
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 |
|
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
892
diff
changeset
|
373 |
qed_goalw "strict_sinl" Ssum3.thy [sinl_def] "sinl`UU =UU" |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
374 |
(fn prems => |
1461 | 375 |
[ |
376 |
(simp_tac (Ssum0_ss addsimps [cont_Isinl]) 1), |
|
377 |
(rtac (inst_ssum_pcpo RS sym) 1) |
|
378 |
]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
379 |
|
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
892
diff
changeset
|
380 |
qed_goalw "strict_sinr" Ssum3.thy [sinr_def] "sinr`UU=UU" |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
381 |
(fn prems => |
1461 | 382 |
[ |
383 |
(simp_tac (Ssum0_ss addsimps [cont_Isinr]) 1), |
|
384 |
(rtac (inst_ssum_pcpo RS sym) 1) |
|
385 |
]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
386 |
|
892 | 387 |
qed_goalw "noteq_sinlsinr" Ssum3.thy [sinl_def,sinr_def] |
1461 | 388 |
"sinl`a=sinr`b ==> a=UU & b=UU" |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
389 |
(fn prems => |
1461 | 390 |
[ |
391 |
(cut_facts_tac prems 1), |
|
392 |
(rtac noteq_IsinlIsinr 1), |
|
393 |
(etac box_equals 1), |
|
394 |
(asm_simp_tac (Ssum0_ss addsimps [cont_Isinr,cont_Isinl]) 1), |
|
395 |
(asm_simp_tac (Ssum0_ss addsimps [cont_Isinr,cont_Isinl]) 1) |
|
396 |
]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
397 |
|
892 | 398 |
qed_goalw "inject_sinl" Ssum3.thy [sinl_def,sinr_def] |
1461 | 399 |
"sinl`a1=sinl`a2==> a1=a2" |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
400 |
(fn prems => |
1461 | 401 |
[ |
402 |
(cut_facts_tac prems 1), |
|
403 |
(rtac inject_Isinl 1), |
|
404 |
(etac box_equals 1), |
|
405 |
(asm_simp_tac (Ssum0_ss addsimps [cont_Isinr,cont_Isinl]) 1), |
|
406 |
(asm_simp_tac (Ssum0_ss addsimps [cont_Isinr,cont_Isinl]) 1) |
|
407 |
]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
408 |
|
892 | 409 |
qed_goalw "inject_sinr" Ssum3.thy [sinl_def,sinr_def] |
1461 | 410 |
"sinr`a1=sinr`a2==> a1=a2" |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
411 |
(fn prems => |
1461 | 412 |
[ |
413 |
(cut_facts_tac prems 1), |
|
414 |
(rtac inject_Isinr 1), |
|
415 |
(etac box_equals 1), |
|
416 |
(asm_simp_tac (Ssum0_ss addsimps [cont_Isinr,cont_Isinl]) 1), |
|
417 |
(asm_simp_tac (Ssum0_ss addsimps [cont_Isinr,cont_Isinl]) 1) |
|
418 |
]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
419 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
420 |
|
892 | 421 |
qed_goal "defined_sinl" Ssum3.thy |
1461 | 422 |
"x~=UU ==> sinl`x ~= UU" |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
423 |
(fn prems => |
1461 | 424 |
[ |
425 |
(cut_facts_tac prems 1), |
|
426 |
(etac swap 1), |
|
427 |
(rtac inject_sinl 1), |
|
428 |
(rtac (strict_sinl RS ssubst) 1), |
|
429 |
(etac notnotD 1) |
|
430 |
]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
431 |
|
892 | 432 |
qed_goal "defined_sinr" Ssum3.thy |
1461 | 433 |
"x~=UU ==> sinr`x ~= UU" |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
434 |
(fn prems => |
1461 | 435 |
[ |
436 |
(cut_facts_tac prems 1), |
|
437 |
(etac swap 1), |
|
438 |
(rtac inject_sinr 1), |
|
439 |
(rtac (strict_sinr RS ssubst) 1), |
|
440 |
(etac notnotD 1) |
|
441 |
]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
442 |
|
892 | 443 |
qed_goalw "Exh_Ssum1" Ssum3.thy [sinl_def,sinr_def] |
1461 | 444 |
"z=UU | (? a. z=sinl`a & a~=UU) | (? b. z=sinr`b & b~=UU)" |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
445 |
(fn prems => |
1461 | 446 |
[ |
447 |
(asm_simp_tac (Ssum0_ss addsimps [cont_Isinr,cont_Isinl]) 1), |
|
448 |
(rtac (inst_ssum_pcpo RS ssubst) 1), |
|
449 |
(rtac Exh_Ssum 1) |
|
450 |
]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
451 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
452 |
|
892 | 453 |
qed_goalw "ssumE" Ssum3.thy [sinl_def,sinr_def] |
1461 | 454 |
"[|p=UU ==> Q ;\ |
455 |
\ !!x.[|p=sinl`x; x~=UU |] ==> Q;\ |
|
456 |
\ !!y.[|p=sinr`y; y~=UU |] ==> Q|] ==> Q" |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
457 |
(fn prems => |
1461 | 458 |
[ |
459 |
(rtac IssumE 1), |
|
460 |
(resolve_tac prems 1), |
|
461 |
(rtac (inst_ssum_pcpo RS ssubst) 1), |
|
462 |
(atac 1), |
|
463 |
(resolve_tac prems 1), |
|
464 |
(atac 2), |
|
465 |
(asm_simp_tac (Ssum0_ss addsimps [cont_Isinr,cont_Isinl]) 1), |
|
466 |
(resolve_tac prems 1), |
|
467 |
(atac 2), |
|
468 |
(asm_simp_tac (Ssum0_ss addsimps [cont_Isinr,cont_Isinl]) 1) |
|
469 |
]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
470 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
471 |
|
892 | 472 |
qed_goalw "ssumE2" Ssum3.thy [sinl_def,sinr_def] |
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
892
diff
changeset
|
473 |
"[|!!x.[|p=sinl`x|] ==> Q;\ |
1461 | 474 |
\ !!y.[|p=sinr`y|] ==> Q|] ==> Q" |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
475 |
(fn prems => |
1461 | 476 |
[ |
477 |
(rtac IssumE2 1), |
|
478 |
(resolve_tac prems 1), |
|
479 |
(rtac (beta_cfun RS ssubst) 1), |
|
480 |
(rtac cont_Isinl 1), |
|
481 |
(atac 1), |
|
482 |
(resolve_tac prems 1), |
|
483 |
(rtac (beta_cfun RS ssubst) 1), |
|
484 |
(rtac cont_Isinr 1), |
|
485 |
(atac 1) |
|
486 |
]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
487 |
|
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
892
diff
changeset
|
488 |
qed_goalw "sswhen1" Ssum3.thy [sswhen_def,sinl_def,sinr_def] |
1461 | 489 |
"sswhen`f`g`UU = UU" |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
490 |
(fn prems => |
1461 | 491 |
[ |
492 |
(rtac (inst_ssum_pcpo RS ssubst) 1), |
|
493 |
(rtac (beta_cfun RS ssubst) 1), |
|
494 |
(REPEAT (resolve_tac (cont_lemmas @ [cont_Iwhen1,cont_Iwhen2, |
|
495 |
cont_Iwhen3,cont2cont_CF1L]) 1)), |
|
496 |
(rtac (beta_cfun RS ssubst) 1), |
|
497 |
(REPEAT (resolve_tac (cont_lemmas @ [cont_Iwhen1,cont_Iwhen2, |
|
498 |
cont_Iwhen3,cont2cont_CF1L]) 1)), |
|
499 |
(rtac (beta_cfun RS ssubst) 1), |
|
500 |
(REPEAT (resolve_tac (cont_lemmas @ [cont_Iwhen1,cont_Iwhen2, |
|
501 |
cont_Iwhen3,cont2cont_CF1L]) 1)), |
|
502 |
(simp_tac Ssum0_ss 1) |
|
503 |
]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
504 |
|
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
892
diff
changeset
|
505 |
qed_goalw "sswhen2" Ssum3.thy [sswhen_def,sinl_def,sinr_def] |
1461 | 506 |
"x~=UU==> sswhen`f`g`(sinl`x) = f`x" |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
507 |
(fn prems => |
1461 | 508 |
[ |
509 |
(cut_facts_tac prems 1), |
|
510 |
(rtac (beta_cfun RS ssubst) 1), |
|
511 |
(REPEAT (resolve_tac (cont_lemmas @ [cont_Iwhen1,cont_Iwhen2, |
|
512 |
cont_Iwhen3,cont_Isinl,cont_Isinr,cont2cont_CF1L]) 1)), |
|
513 |
(rtac (beta_cfun RS ssubst) 1), |
|
514 |
(REPEAT (resolve_tac (cont_lemmas @ [cont_Iwhen1,cont_Iwhen2, |
|
515 |
cont_Iwhen3,cont_Isinl,cont_Isinr,cont2cont_CF1L]) 1)), |
|
516 |
(rtac (beta_cfun RS ssubst) 1), |
|
517 |
(REPEAT (resolve_tac (cont_lemmas @ [cont_Iwhen1,cont_Iwhen2, |
|
518 |
cont_Iwhen3,cont_Isinl,cont_Isinr,cont2cont_CF1L]) 1)), |
|
519 |
(rtac (beta_cfun RS ssubst) 1), |
|
520 |
(REPEAT (resolve_tac (cont_lemmas @ [cont_Iwhen1,cont_Iwhen2, |
|
521 |
cont_Iwhen3,cont_Isinl,cont_Isinr,cont2cont_CF1L]) 1)), |
|
522 |
(asm_simp_tac Ssum0_ss 1) |
|
523 |
]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
524 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
525 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
526 |
|
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
892
diff
changeset
|
527 |
qed_goalw "sswhen3" Ssum3.thy [sswhen_def,sinl_def,sinr_def] |
1461 | 528 |
"x~=UU==> sswhen`f`g`(sinr`x) = g`x" |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
529 |
(fn prems => |
1461 | 530 |
[ |
531 |
(cut_facts_tac prems 1), |
|
532 |
(rtac (beta_cfun RS ssubst) 1), |
|
533 |
(REPEAT (resolve_tac (cont_lemmas @ [cont_Iwhen1,cont_Iwhen2, |
|
534 |
cont_Iwhen3,cont_Isinl,cont_Isinr,cont2cont_CF1L]) 1)), |
|
535 |
(rtac (beta_cfun RS ssubst) 1), |
|
536 |
(REPEAT (resolve_tac (cont_lemmas @ [cont_Iwhen1,cont_Iwhen2, |
|
537 |
cont_Iwhen3,cont_Isinl,cont_Isinr,cont2cont_CF1L]) 1)), |
|
538 |
(rtac (beta_cfun RS ssubst) 1), |
|
539 |
(REPEAT (resolve_tac (cont_lemmas @ [cont_Iwhen1,cont_Iwhen2, |
|
540 |
cont_Iwhen3,cont_Isinl,cont_Isinr,cont2cont_CF1L]) 1)), |
|
541 |
(rtac (beta_cfun RS ssubst) 1), |
|
542 |
(REPEAT (resolve_tac (cont_lemmas @ [cont_Iwhen1,cont_Iwhen2, |
|
543 |
cont_Iwhen3,cont_Isinl,cont_Isinr,cont2cont_CF1L]) 1)), |
|
544 |
(asm_simp_tac Ssum0_ss 1) |
|
545 |
]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
546 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
547 |
|
892 | 548 |
qed_goalw "less_ssum4a" Ssum3.thy [sinl_def,sinr_def] |
1461 | 549 |
"(sinl`x << sinl`y) = (x << y)" |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
550 |
(fn prems => |
1461 | 551 |
[ |
552 |
(rtac (beta_cfun RS ssubst) 1), |
|
553 |
(REPEAT (resolve_tac (cont_lemmas @ [cont_Iwhen1,cont_Iwhen2, |
|
554 |
cont_Iwhen3,cont_Isinl,cont_Isinr,cont2cont_CF1L]) 1)), |
|
555 |
(rtac (beta_cfun RS ssubst) 1), |
|
556 |
(REPEAT (resolve_tac (cont_lemmas @ [cont_Iwhen1,cont_Iwhen2, |
|
557 |
cont_Iwhen3,cont_Isinl,cont_Isinr,cont2cont_CF1L]) 1)), |
|
558 |
(rtac less_ssum3a 1) |
|
559 |
]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
560 |
|
892 | 561 |
qed_goalw "less_ssum4b" Ssum3.thy [sinl_def,sinr_def] |
1461 | 562 |
"(sinr`x << sinr`y) = (x << y)" |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
563 |
(fn prems => |
1461 | 564 |
[ |
565 |
(rtac (beta_cfun RS ssubst) 1), |
|
566 |
(REPEAT (resolve_tac (cont_lemmas @ [cont_Iwhen1,cont_Iwhen2, |
|
567 |
cont_Iwhen3,cont_Isinl,cont_Isinr,cont2cont_CF1L]) 1)), |
|
568 |
(rtac (beta_cfun RS ssubst) 1), |
|
569 |
(REPEAT (resolve_tac (cont_lemmas @ [cont_Iwhen1,cont_Iwhen2, |
|
570 |
cont_Iwhen3,cont_Isinl,cont_Isinr,cont2cont_CF1L]) 1)), |
|
571 |
(rtac less_ssum3b 1) |
|
572 |
]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
573 |
|
892 | 574 |
qed_goalw "less_ssum4c" Ssum3.thy [sinl_def,sinr_def] |
1461 | 575 |
"(sinl`x << sinr`y) = (x = UU)" |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
576 |
(fn prems => |
1461 | 577 |
[ |
578 |
(rtac (beta_cfun RS ssubst) 1), |
|
579 |
(REPEAT (resolve_tac (cont_lemmas @ [cont_Iwhen1,cont_Iwhen2, |
|
580 |
cont_Iwhen3,cont_Isinl,cont_Isinr,cont2cont_CF1L]) 1)), |
|
581 |
(rtac (beta_cfun RS ssubst) 1), |
|
582 |
(REPEAT (resolve_tac (cont_lemmas @ [cont_Iwhen1,cont_Iwhen2, |
|
583 |
cont_Iwhen3,cont_Isinl,cont_Isinr,cont2cont_CF1L]) 1)), |
|
584 |
(rtac less_ssum3c 1) |
|
585 |
]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
586 |
|
892 | 587 |
qed_goalw "less_ssum4d" Ssum3.thy [sinl_def,sinr_def] |
1461 | 588 |
"(sinr`x << sinl`y) = (x = UU)" |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
589 |
(fn prems => |
1461 | 590 |
[ |
591 |
(rtac (beta_cfun RS ssubst) 1), |
|
592 |
(REPEAT (resolve_tac (cont_lemmas @ [cont_Iwhen1,cont_Iwhen2, |
|
593 |
cont_Iwhen3,cont_Isinl,cont_Isinr,cont2cont_CF1L]) 1)), |
|
594 |
(rtac (beta_cfun RS ssubst) 1), |
|
595 |
(REPEAT (resolve_tac (cont_lemmas @ [cont_Iwhen1,cont_Iwhen2, |
|
596 |
cont_Iwhen3,cont_Isinl,cont_Isinr,cont2cont_CF1L]) 1)), |
|
597 |
(rtac less_ssum3d 1) |
|
598 |
]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
599 |
|
892 | 600 |
qed_goalw "ssum_chainE" Ssum3.thy [sinl_def,sinr_def] |
1461 | 601 |
"is_chain(Y) ==> (!i.? x.(Y i)=sinl`x)|(!i.? y.(Y i)=sinr`y)" |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
602 |
(fn prems => |
1461 | 603 |
[ |
604 |
(cut_facts_tac prems 1), |
|
605 |
(asm_simp_tac (Ssum0_ss addsimps [cont_Isinr,cont_Isinl]) 1), |
|
606 |
(etac ssum_lemma4 1) |
|
607 |
]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
608 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
609 |
|
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
892
diff
changeset
|
610 |
qed_goalw "thelub_ssum2a" Ssum3.thy [sinl_def,sinr_def,sswhen_def] |
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
892
diff
changeset
|
611 |
"[| is_chain(Y); !i.? x. Y(i) = sinl`x |] ==>\ |
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
892
diff
changeset
|
612 |
\ lub(range(Y)) = sinl`(lub(range(%i. sswhen`(LAM x. x)`(LAM y. UU)`(Y i))))" |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
613 |
(fn prems => |
1461 | 614 |
[ |
615 |
(cut_facts_tac prems 1), |
|
616 |
(rtac (beta_cfun RS ssubst) 1), |
|
617 |
(REPEAT (resolve_tac (cont_lemmas @ [cont_Iwhen1,cont_Iwhen2, cont_Iwhen3,cont_Isinl,cont_Isinr,cont2cont_CF1L]) 1)), |
|
618 |
(rtac (beta_cfun RS ssubst) 1), |
|
619 |
(REPEAT (resolve_tac (cont_lemmas @ [cont_Iwhen1,cont_Iwhen2, cont_Iwhen3,cont_Isinl,cont_Isinr,cont2cont_CF1L]) 1)), |
|
620 |
(rtac (beta_cfun RS ssubst) 1), |
|
621 |
(REPEAT (resolve_tac (cont_lemmas @ [cont_Iwhen1,cont_Iwhen2, cont_Iwhen3,cont_Isinl,cont_Isinr,cont2cont_CF1L]) 1)), |
|
622 |
(rtac (beta_cfun RS ext RS ssubst) 1), |
|
623 |
(REPEAT (resolve_tac (cont_lemmas @ [cont_Iwhen1,cont_Iwhen2, cont_Iwhen3,cont_Isinl,cont_Isinr,cont2cont_CF1L]) 1)), |
|
624 |
(rtac thelub_ssum1a 1), |
|
625 |
(atac 1), |
|
626 |
(rtac allI 1), |
|
627 |
(etac allE 1), |
|
628 |
(etac exE 1), |
|
629 |
(rtac exI 1), |
|
630 |
(etac box_equals 1), |
|
631 |
(rtac refl 1), |
|
632 |
(asm_simp_tac (Ssum0_ss addsimps [cont_Isinl]) 1) |
|
633 |
]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
634 |
|
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
892
diff
changeset
|
635 |
qed_goalw "thelub_ssum2b" Ssum3.thy [sinl_def,sinr_def,sswhen_def] |
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
892
diff
changeset
|
636 |
"[| is_chain(Y); !i.? x. Y(i) = sinr`x |] ==>\ |
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
892
diff
changeset
|
637 |
\ lub(range(Y)) = sinr`(lub(range(%i. sswhen`(LAM y. UU)`(LAM x.x)`(Y i))))" |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
638 |
(fn prems => |
1461 | 639 |
[ |
640 |
(cut_facts_tac prems 1), |
|
641 |
(rtac (beta_cfun RS ssubst) 1), |
|
642 |
(REPEAT (resolve_tac (cont_lemmas @ [cont_Iwhen1,cont_Iwhen2, |
|
643 |
cont_Iwhen3,cont_Isinl,cont_Isinr,cont2cont_CF1L]) 1)), |
|
644 |
(rtac (beta_cfun RS ssubst) 1), |
|
645 |
(REPEAT (resolve_tac (cont_lemmas @ [cont_Iwhen1,cont_Iwhen2, |
|
646 |
cont_Iwhen3,cont_Isinl,cont_Isinr,cont2cont_CF1L]) 1)), |
|
647 |
(rtac (beta_cfun RS ssubst) 1), |
|
648 |
(REPEAT (resolve_tac (cont_lemmas @ [cont_Iwhen1,cont_Iwhen2, |
|
649 |
cont_Iwhen3,cont_Isinl,cont_Isinr,cont2cont_CF1L]) 1)), |
|
650 |
(rtac (beta_cfun RS ext RS ssubst) 1), |
|
651 |
(REPEAT (resolve_tac (cont_lemmas @ [cont_Iwhen1,cont_Iwhen2, |
|
652 |
cont_Iwhen3,cont_Isinl,cont_Isinr,cont2cont_CF1L]) 1)), |
|
653 |
(rtac thelub_ssum1b 1), |
|
654 |
(atac 1), |
|
655 |
(rtac allI 1), |
|
656 |
(etac allE 1), |
|
657 |
(etac exE 1), |
|
658 |
(rtac exI 1), |
|
659 |
(etac box_equals 1), |
|
660 |
(rtac refl 1), |
|
661 |
(asm_simp_tac (Ssum0_ss addsimps |
|
662 |
[cont_Isinr,cont_Isinl,cont_Iwhen1,cont_Iwhen2, |
|
663 |
cont_Iwhen3]) 1) |
|
664 |
]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
665 |
|
892 | 666 |
qed_goalw "thelub_ssum2a_rev" Ssum3.thy [sinl_def,sinr_def] |
1461 | 667 |
"[| is_chain(Y); lub(range(Y)) = sinl`x|] ==> !i.? x.Y(i)=sinl`x" |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
668 |
(fn prems => |
1461 | 669 |
[ |
670 |
(cut_facts_tac prems 1), |
|
671 |
(asm_simp_tac (Ssum0_ss addsimps |
|
672 |
[cont_Isinr,cont_Isinl,cont_Iwhen1,cont_Iwhen2, |
|
673 |
cont_Iwhen3]) 1), |
|
674 |
(etac ssum_lemma9 1), |
|
675 |
(asm_simp_tac (Ssum0_ss addsimps |
|
676 |
[cont_Isinr,cont_Isinl,cont_Iwhen1,cont_Iwhen2, |
|
677 |
cont_Iwhen3]) 1) |
|
678 |
]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
679 |
|
892 | 680 |
qed_goalw "thelub_ssum2b_rev" Ssum3.thy [sinl_def,sinr_def] |
1461 | 681 |
"[| is_chain(Y); lub(range(Y)) = sinr`x|] ==> !i.? x.Y(i)=sinr`x" |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
682 |
(fn prems => |
1461 | 683 |
[ |
684 |
(cut_facts_tac prems 1), |
|
685 |
(asm_simp_tac (Ssum0_ss addsimps |
|
686 |
[cont_Isinr,cont_Isinl,cont_Iwhen1,cont_Iwhen2, |
|
687 |
cont_Iwhen3]) 1), |
|
688 |
(etac ssum_lemma10 1), |
|
689 |
(asm_simp_tac (Ssum0_ss addsimps |
|
690 |
[cont_Isinr,cont_Isinl,cont_Iwhen1,cont_Iwhen2, |
|
691 |
cont_Iwhen3]) 1) |
|
692 |
]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
693 |
|
892 | 694 |
qed_goal "thelub_ssum3" Ssum3.thy |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
695 |
"is_chain(Y) ==>\ |
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
892
diff
changeset
|
696 |
\ lub(range(Y)) = sinl`(lub(range(%i. sswhen`(LAM x. x)`(LAM y.UU)`(Y i))))\ |
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
892
diff
changeset
|
697 |
\ | lub(range(Y)) = sinr`(lub(range(%i. sswhen`(LAM y. UU)`(LAM x.x)`(Y i))))" |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
698 |
(fn prems => |
1461 | 699 |
[ |
700 |
(cut_facts_tac prems 1), |
|
701 |
(rtac (ssum_chainE RS disjE) 1), |
|
702 |
(atac 1), |
|
703 |
(rtac disjI1 1), |
|
704 |
(etac thelub_ssum2a 1), |
|
705 |
(atac 1), |
|
706 |
(rtac disjI2 1), |
|
707 |
(etac thelub_ssum2b 1), |
|
708 |
(atac 1) |
|
709 |
]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
710 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
711 |
|
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
892
diff
changeset
|
712 |
qed_goal "sswhen4" Ssum3.thy |
1461 | 713 |
"sswhen`sinl`sinr`z=z" |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
714 |
(fn prems => |
1461 | 715 |
[ |
716 |
(res_inst_tac [("p","z")] ssumE 1), |
|
1277
caef3601c0b2
corrected some errors that occurred after introduction of local simpsets
regensbu
parents:
1274
diff
changeset
|
717 |
(asm_simp_tac ((simpset_of "Cfun3") addsimps [sswhen1,sswhen2,sswhen3]) 1), |
caef3601c0b2
corrected some errors that occurred after introduction of local simpsets
regensbu
parents:
1274
diff
changeset
|
718 |
(asm_simp_tac ((simpset_of "Cfun3") addsimps [sswhen1,sswhen2,sswhen3]) 1), |
caef3601c0b2
corrected some errors that occurred after introduction of local simpsets
regensbu
parents:
1274
diff
changeset
|
719 |
(asm_simp_tac ((simpset_of "Cfun3") addsimps [sswhen1,sswhen2,sswhen3]) 1) |
1461 | 720 |
]); |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
721 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
722 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
723 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
724 |
(* install simplifier for Ssum *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
725 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
726 |
|
1274 | 727 |
val Ssum_rews = [strict_sinl,strict_sinr,defined_sinl,defined_sinr, |
1461 | 728 |
sswhen1,sswhen2,sswhen3]; |
1274 | 729 |
|
730 |
Addsimps [strict_sinl,strict_sinr,defined_sinl,defined_sinr, |
|
1461 | 731 |
sswhen1,sswhen2,sswhen3]; |