author | oheimb |
Fri, 20 Dec 1996 10:33:54 +0100 | |
changeset 2458 | 566a0fc5a3e0 |
parent 2444 | 150644698367 |
child 2566 | cbf02fc74332 |
permissions | -rw-r--r-- |
1461 | 1 |
(* Title: HOLCF/cprod3.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 Cprod3.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 Cprod3; |
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 |
(* ------------------------------------------------------------------------ *) |
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
899
diff
changeset
|
12 |
(* continuity of (_,_) , fst, snd *) |
243
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 "Cprod3_lemma1" Cprod3.thy |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
16 |
"is_chain(Y::(nat=>'a)) ==>\ |
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
899
diff
changeset
|
17 |
\ (lub(range(Y)),(x::'b)) =\ |
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
899
diff
changeset
|
18 |
\ (lub(range(%i. fst(Y i,x))),lub(range(%i. snd(Y i,x))))" |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
19 |
(fn prems => |
1461 | 20 |
[ |
21 |
(cut_facts_tac prems 1), |
|
22 |
(res_inst_tac [("f1","Pair")] (arg_cong RS cong) 1), |
|
23 |
(rtac lub_equal 1), |
|
24 |
(atac 1), |
|
25 |
(rtac (monofun_fst RS ch2ch_monofun) 1), |
|
26 |
(rtac ch2ch_fun 1), |
|
27 |
(rtac (monofun_pair1 RS ch2ch_monofun) 1), |
|
28 |
(atac 1), |
|
29 |
(rtac allI 1), |
|
30 |
(Simp_tac 1), |
|
31 |
(rtac sym 1), |
|
32 |
(Simp_tac 1), |
|
33 |
(rtac (lub_const RS thelubI) 1) |
|
34 |
]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
35 |
|
892 | 36 |
qed_goal "contlub_pair1" Cprod3.thy "contlub(Pair)" |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
37 |
(fn prems => |
1461 | 38 |
[ |
39 |
(rtac contlubI 1), |
|
40 |
(strip_tac 1), |
|
41 |
(rtac (expand_fun_eq RS iffD2) 1), |
|
42 |
(strip_tac 1), |
|
2033 | 43 |
(stac (lub_fun RS thelubI) 1), |
1461 | 44 |
(etac (monofun_pair1 RS ch2ch_monofun) 1), |
45 |
(rtac trans 1), |
|
46 |
(rtac (thelub_cprod RS sym) 2), |
|
47 |
(rtac ch2ch_fun 2), |
|
48 |
(etac (monofun_pair1 RS ch2ch_monofun) 2), |
|
49 |
(etac Cprod3_lemma1 1) |
|
50 |
]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
51 |
|
892 | 52 |
qed_goal "Cprod3_lemma2" Cprod3.thy |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
53 |
"is_chain(Y::(nat=>'a)) ==>\ |
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
899
diff
changeset
|
54 |
\ ((x::'b),lub(range Y)) =\ |
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
899
diff
changeset
|
55 |
\ (lub(range(%i. fst(x,Y i))),lub(range(%i. snd(x, Y i))))" |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
56 |
(fn prems => |
1461 | 57 |
[ |
58 |
(cut_facts_tac prems 1), |
|
59 |
(res_inst_tac [("f1","Pair")] (arg_cong RS cong) 1), |
|
60 |
(rtac sym 1), |
|
61 |
(Simp_tac 1), |
|
62 |
(rtac (lub_const RS thelubI) 1), |
|
63 |
(rtac lub_equal 1), |
|
64 |
(atac 1), |
|
65 |
(rtac (monofun_snd RS ch2ch_monofun) 1), |
|
66 |
(rtac (monofun_pair2 RS ch2ch_monofun) 1), |
|
67 |
(atac 1), |
|
68 |
(rtac allI 1), |
|
69 |
(Simp_tac 1) |
|
70 |
]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
71 |
|
892 | 72 |
qed_goal "contlub_pair2" Cprod3.thy "contlub(Pair(x))" |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
73 |
(fn prems => |
1461 | 74 |
[ |
75 |
(rtac contlubI 1), |
|
76 |
(strip_tac 1), |
|
77 |
(rtac trans 1), |
|
78 |
(rtac (thelub_cprod RS sym) 2), |
|
79 |
(etac (monofun_pair2 RS ch2ch_monofun) 2), |
|
80 |
(etac Cprod3_lemma2 1) |
|
81 |
]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
82 |
|
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
899
diff
changeset
|
83 |
qed_goal "cont_pair1" Cprod3.thy "cont(Pair)" |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
84 |
(fn prems => |
1461 | 85 |
[ |
86 |
(rtac monocontlub2cont 1), |
|
87 |
(rtac monofun_pair1 1), |
|
88 |
(rtac contlub_pair1 1) |
|
89 |
]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
90 |
|
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
899
diff
changeset
|
91 |
qed_goal "cont_pair2" Cprod3.thy "cont(Pair(x))" |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
92 |
(fn prems => |
1461 | 93 |
[ |
94 |
(rtac monocontlub2cont 1), |
|
95 |
(rtac monofun_pair2 1), |
|
96 |
(rtac contlub_pair2 1) |
|
97 |
]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
98 |
|
892 | 99 |
qed_goal "contlub_fst" Cprod3.thy "contlub(fst)" |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
100 |
(fn prems => |
1461 | 101 |
[ |
102 |
(rtac contlubI 1), |
|
103 |
(strip_tac 1), |
|
2033 | 104 |
(stac (lub_cprod RS thelubI) 1), |
1461 | 105 |
(atac 1), |
106 |
(Simp_tac 1) |
|
107 |
]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
108 |
|
892 | 109 |
qed_goal "contlub_snd" Cprod3.thy "contlub(snd)" |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
110 |
(fn prems => |
1461 | 111 |
[ |
112 |
(rtac contlubI 1), |
|
113 |
(strip_tac 1), |
|
2033 | 114 |
(stac (lub_cprod RS thelubI) 1), |
1461 | 115 |
(atac 1), |
116 |
(Simp_tac 1) |
|
117 |
]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
118 |
|
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
899
diff
changeset
|
119 |
qed_goal "cont_fst" Cprod3.thy "cont(fst)" |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
120 |
(fn prems => |
1461 | 121 |
[ |
122 |
(rtac monocontlub2cont 1), |
|
123 |
(rtac monofun_fst 1), |
|
124 |
(rtac contlub_fst 1) |
|
125 |
]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
126 |
|
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
899
diff
changeset
|
127 |
qed_goal "cont_snd" Cprod3.thy "cont(snd)" |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
128 |
(fn prems => |
1461 | 129 |
[ |
130 |
(rtac monocontlub2cont 1), |
|
131 |
(rtac monofun_snd 1), |
|
132 |
(rtac contlub_snd 1) |
|
133 |
]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
134 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
135 |
(* |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
136 |
-------------------------------------------------------------------------- |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
137 |
more lemmas for Cprod3.thy |
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 |
*) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
141 |
|
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 |
(* convert all lemmas to the continuous versions *) |
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 |
|
892 | 146 |
qed_goalw "beta_cfun_cprod" Cprod3.thy [cpair_def] |
1461 | 147 |
"(LAM x y.(x,y))`a`b = (a,b)" |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
148 |
(fn prems => |
1461 | 149 |
[ |
2033 | 150 |
(stac beta_cfun 1), |
1461 | 151 |
(cont_tac 1), |
152 |
(rtac cont_pair2 1), |
|
153 |
(rtac cont2cont_CF1L 1), |
|
154 |
(rtac cont_pair1 1), |
|
2033 | 155 |
(stac beta_cfun 1), |
1461 | 156 |
(rtac cont_pair2 1), |
157 |
(rtac refl 1) |
|
158 |
]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
159 |
|
892 | 160 |
qed_goalw "inject_cpair" Cprod3.thy [cpair_def] |
1461 | 161 |
" <a,b>=<aa,ba> ==> a=aa & b=ba" |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
162 |
(fn prems => |
1461 | 163 |
[ |
164 |
(cut_facts_tac prems 1), |
|
165 |
(dtac (beta_cfun_cprod RS subst) 1), |
|
166 |
(dtac (beta_cfun_cprod RS subst) 1), |
|
167 |
(etac Pair_inject 1), |
|
168 |
(fast_tac HOL_cs 1) |
|
169 |
]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
170 |
|
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
899
diff
changeset
|
171 |
qed_goalw "inst_cprod_pcpo2" Cprod3.thy [cpair_def] "UU = <UU,UU>" |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
172 |
(fn prems => |
1461 | 173 |
[ |
174 |
(rtac sym 1), |
|
175 |
(rtac trans 1), |
|
176 |
(rtac beta_cfun_cprod 1), |
|
177 |
(rtac sym 1), |
|
178 |
(rtac inst_cprod_pcpo 1) |
|
179 |
]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
180 |
|
892 | 181 |
qed_goal "defined_cpair_rev" Cprod3.thy |
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
899
diff
changeset
|
182 |
"<a,b> = UU ==> a = UU & b = UU" |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
183 |
(fn prems => |
1461 | 184 |
[ |
185 |
(cut_facts_tac prems 1), |
|
186 |
(dtac (inst_cprod_pcpo2 RS subst) 1), |
|
187 |
(etac inject_cpair 1) |
|
188 |
]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
189 |
|
892 | 190 |
qed_goalw "Exh_Cprod2" Cprod3.thy [cpair_def] |
1461 | 191 |
"? a b. z=<a,b>" |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
192 |
(fn prems => |
1461 | 193 |
[ |
194 |
(rtac PairE 1), |
|
195 |
(rtac exI 1), |
|
196 |
(rtac exI 1), |
|
197 |
(etac (beta_cfun_cprod RS ssubst) 1) |
|
198 |
]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
199 |
|
892 | 200 |
qed_goalw "cprodE" Cprod3.thy [cpair_def] |
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
899
diff
changeset
|
201 |
"[|!!x y. [|p=<x,y> |] ==> Q|] ==> Q" |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
202 |
(fn prems => |
1461 | 203 |
[ |
204 |
(rtac PairE 1), |
|
205 |
(resolve_tac prems 1), |
|
206 |
(etac (beta_cfun_cprod RS ssubst) 1) |
|
207 |
]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
208 |
|
892 | 209 |
qed_goalw "cfst2" Cprod3.thy [cfst_def,cpair_def] |
1461 | 210 |
"cfst`<x,y>=x" |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
211 |
(fn prems => |
1461 | 212 |
[ |
213 |
(cut_facts_tac prems 1), |
|
2033 | 214 |
(stac beta_cfun_cprod 1), |
215 |
(stac beta_cfun 1), |
|
1461 | 216 |
(rtac cont_fst 1), |
217 |
(Simp_tac 1) |
|
218 |
]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
219 |
|
892 | 220 |
qed_goalw "csnd2" Cprod3.thy [csnd_def,cpair_def] |
1461 | 221 |
"csnd`<x,y>=y" |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
222 |
(fn prems => |
1461 | 223 |
[ |
224 |
(cut_facts_tac prems 1), |
|
2033 | 225 |
(stac beta_cfun_cprod 1), |
226 |
(stac beta_cfun 1), |
|
1461 | 227 |
(rtac cont_snd 1), |
228 |
(Simp_tac 1) |
|
229 |
]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
230 |
|
2444 | 231 |
qed_goal "cfst_strict" Cprod3.thy "cfst`UU = UU" (fn _ => [ |
232 |
(simp_tac (HOL_ss addsimps [inst_cprod_pcpo2,cfst2]) 1)]); |
|
233 |
qed_goal "csnd_strict" Cprod3.thy "csnd`UU = UU" (fn _ => [ |
|
234 |
(simp_tac (HOL_ss addsimps [inst_cprod_pcpo2,csnd2]) 1)]); |
|
235 |
||
892 | 236 |
qed_goalw "surjective_pairing_Cprod2" Cprod3.thy |
1461 | 237 |
[cfst_def,csnd_def,cpair_def] "<cfst`p , csnd`p> = p" |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
238 |
(fn prems => |
1461 | 239 |
[ |
2033 | 240 |
(stac beta_cfun_cprod 1), |
241 |
(stac beta_cfun 1), |
|
1461 | 242 |
(rtac cont_snd 1), |
2033 | 243 |
(stac beta_cfun 1), |
1461 | 244 |
(rtac cont_fst 1), |
245 |
(rtac (surjective_pairing RS sym) 1) |
|
246 |
]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
247 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
248 |
|
892 | 249 |
qed_goalw "less_cprod5b" Cprod3.thy [cfst_def,csnd_def,cpair_def] |
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
899
diff
changeset
|
250 |
" (p1 << p2) = (cfst`p1 << cfst`p2 & csnd`p1 << csnd`p2)" |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
251 |
(fn prems => |
1461 | 252 |
[ |
2033 | 253 |
(stac beta_cfun 1), |
1461 | 254 |
(rtac cont_snd 1), |
2033 | 255 |
(stac beta_cfun 1), |
1461 | 256 |
(rtac cont_snd 1), |
2033 | 257 |
(stac beta_cfun 1), |
1461 | 258 |
(rtac cont_fst 1), |
2033 | 259 |
(stac beta_cfun 1), |
1461 | 260 |
(rtac cont_fst 1), |
261 |
(rtac less_cprod3b 1) |
|
262 |
]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
263 |
|
892 | 264 |
qed_goalw "less_cprod5c" Cprod3.thy [cfst_def,csnd_def,cpair_def] |
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
899
diff
changeset
|
265 |
"<xa,ya> << <x,y> ==> xa<<x & ya << y" |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
266 |
(fn prems => |
1461 | 267 |
[ |
268 |
(cut_facts_tac prems 1), |
|
269 |
(rtac less_cprod4c 1), |
|
270 |
(dtac (beta_cfun_cprod RS subst) 1), |
|
271 |
(dtac (beta_cfun_cprod RS subst) 1), |
|
272 |
(atac 1) |
|
273 |
]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
274 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
275 |
|
892 | 276 |
qed_goalw "lub_cprod2" Cprod3.thy [cfst_def,csnd_def,cpair_def] |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
277 |
"[|is_chain(S)|] ==> range(S) <<| \ |
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
899
diff
changeset
|
278 |
\ <(lub(range(%i.cfst`(S i)))) , lub(range(%i.csnd`(S i)))>" |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
279 |
(fn prems => |
1461 | 280 |
[ |
281 |
(cut_facts_tac prems 1), |
|
2033 | 282 |
(stac beta_cfun_cprod 1), |
283 |
(stac (beta_cfun RS ext) 1), |
|
1461 | 284 |
(rtac cont_snd 1), |
2033 | 285 |
(stac (beta_cfun RS ext) 1), |
1461 | 286 |
(rtac cont_fst 1), |
287 |
(rtac lub_cprod 1), |
|
288 |
(atac 1) |
|
289 |
]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
290 |
|
1779 | 291 |
bind_thm ("thelub_cprod2", lub_cprod2 RS thelubI); |
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
899
diff
changeset
|
292 |
(* |
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
899
diff
changeset
|
293 |
is_chain ?S1 ==> |
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
899
diff
changeset
|
294 |
lub (range ?S1) = |
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
899
diff
changeset
|
295 |
<lub (range (%i. cfst`(?S1 i))), lub (range (%i. csnd`(?S1 i)))>" |
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
899
diff
changeset
|
296 |
*) |
892 | 297 |
qed_goalw "csplit2" Cprod3.thy [csplit_def] |
1461 | 298 |
"csplit`f`<x,y> = f`x`y" |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
299 |
(fn prems => |
1461 | 300 |
[ |
2033 | 301 |
(stac beta_cfun 1), |
1461 | 302 |
(cont_tacR 1), |
303 |
(Simp_tac 1), |
|
304 |
(simp_tac (!simpset addsimps [cfst2,csnd2]) 1) |
|
305 |
]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
306 |
|
892 | 307 |
qed_goalw "csplit3" Cprod3.thy [csplit_def] |
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
899
diff
changeset
|
308 |
"csplit`cpair`z=z" |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
309 |
(fn prems => |
1461 | 310 |
[ |
2033 | 311 |
(stac beta_cfun 1), |
1461 | 312 |
(cont_tacR 1), |
313 |
(simp_tac (!simpset addsimps [surjective_pairing_Cprod2]) 1) |
|
314 |
]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
315 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
316 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
317 |
(* install simplifier for Cprod *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
318 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
319 |
|
1267 | 320 |
Addsimps [cfst2,csnd2,csplit2]; |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
321 |
|
1274 | 322 |
val Cprod_rews = [cfst2,csnd2,csplit2]; |