author | paulson |
Fri, 31 Jan 1997 17:13:19 +0100 | |
changeset 2572 | 8a47f85e7a03 |
parent 2566 | cbf02fc74332 |
child 2640 | ee4dfce170a0 |
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), |
2566 | 151 |
(simp_tac (!simpset addsimps [cont_pair1,cont_pair2,cont2cont_CF1L]) 1), |
2033 | 152 |
(stac beta_cfun 1), |
1461 | 153 |
(rtac cont_pair2 1), |
154 |
(rtac refl 1) |
|
155 |
]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
156 |
|
892 | 157 |
qed_goalw "inject_cpair" Cprod3.thy [cpair_def] |
1461 | 158 |
" <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
|
159 |
(fn prems => |
1461 | 160 |
[ |
161 |
(cut_facts_tac prems 1), |
|
162 |
(dtac (beta_cfun_cprod RS subst) 1), |
|
163 |
(dtac (beta_cfun_cprod RS subst) 1), |
|
164 |
(etac Pair_inject 1), |
|
165 |
(fast_tac HOL_cs 1) |
|
166 |
]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
167 |
|
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
899
diff
changeset
|
168 |
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
|
169 |
(fn prems => |
1461 | 170 |
[ |
171 |
(rtac sym 1), |
|
172 |
(rtac trans 1), |
|
173 |
(rtac beta_cfun_cprod 1), |
|
174 |
(rtac sym 1), |
|
175 |
(rtac inst_cprod_pcpo 1) |
|
176 |
]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
177 |
|
892 | 178 |
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
|
179 |
"<a,b> = UU ==> a = UU & b = UU" |
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 |
(dtac (inst_cprod_pcpo2 RS subst) 1), |
|
184 |
(etac inject_cpair 1) |
|
185 |
]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
186 |
|
892 | 187 |
qed_goalw "Exh_Cprod2" Cprod3.thy [cpair_def] |
1461 | 188 |
"? a b. z=<a,b>" |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
189 |
(fn prems => |
1461 | 190 |
[ |
191 |
(rtac PairE 1), |
|
192 |
(rtac exI 1), |
|
193 |
(rtac exI 1), |
|
194 |
(etac (beta_cfun_cprod RS ssubst) 1) |
|
195 |
]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
196 |
|
892 | 197 |
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
|
198 |
"[|!!x y. [|p=<x,y> |] ==> Q|] ==> Q" |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
199 |
(fn prems => |
1461 | 200 |
[ |
201 |
(rtac PairE 1), |
|
202 |
(resolve_tac prems 1), |
|
203 |
(etac (beta_cfun_cprod RS ssubst) 1) |
|
204 |
]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
205 |
|
892 | 206 |
qed_goalw "cfst2" Cprod3.thy [cfst_def,cpair_def] |
1461 | 207 |
"cfst`<x,y>=x" |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
208 |
(fn prems => |
1461 | 209 |
[ |
210 |
(cut_facts_tac prems 1), |
|
2033 | 211 |
(stac beta_cfun_cprod 1), |
212 |
(stac beta_cfun 1), |
|
1461 | 213 |
(rtac cont_fst 1), |
214 |
(Simp_tac 1) |
|
215 |
]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
216 |
|
892 | 217 |
qed_goalw "csnd2" Cprod3.thy [csnd_def,cpair_def] |
1461 | 218 |
"csnd`<x,y>=y" |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
219 |
(fn prems => |
1461 | 220 |
[ |
221 |
(cut_facts_tac prems 1), |
|
2033 | 222 |
(stac beta_cfun_cprod 1), |
223 |
(stac beta_cfun 1), |
|
1461 | 224 |
(rtac cont_snd 1), |
225 |
(Simp_tac 1) |
|
226 |
]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
227 |
|
2444 | 228 |
qed_goal "cfst_strict" Cprod3.thy "cfst`UU = UU" (fn _ => [ |
229 |
(simp_tac (HOL_ss addsimps [inst_cprod_pcpo2,cfst2]) 1)]); |
|
230 |
qed_goal "csnd_strict" Cprod3.thy "csnd`UU = UU" (fn _ => [ |
|
231 |
(simp_tac (HOL_ss addsimps [inst_cprod_pcpo2,csnd2]) 1)]); |
|
232 |
||
892 | 233 |
qed_goalw "surjective_pairing_Cprod2" Cprod3.thy |
1461 | 234 |
[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
|
235 |
(fn prems => |
1461 | 236 |
[ |
2033 | 237 |
(stac beta_cfun_cprod 1), |
238 |
(stac beta_cfun 1), |
|
1461 | 239 |
(rtac cont_snd 1), |
2033 | 240 |
(stac beta_cfun 1), |
1461 | 241 |
(rtac cont_fst 1), |
242 |
(rtac (surjective_pairing RS sym) 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_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
|
247 |
" (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
|
248 |
(fn prems => |
1461 | 249 |
[ |
2033 | 250 |
(stac beta_cfun 1), |
1461 | 251 |
(rtac cont_snd 1), |
2033 | 252 |
(stac beta_cfun 1), |
1461 | 253 |
(rtac cont_snd 1), |
2033 | 254 |
(stac beta_cfun 1), |
1461 | 255 |
(rtac cont_fst 1), |
2033 | 256 |
(stac beta_cfun 1), |
1461 | 257 |
(rtac cont_fst 1), |
258 |
(rtac less_cprod3b 1) |
|
259 |
]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
260 |
|
892 | 261 |
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
|
262 |
"<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
|
263 |
(fn prems => |
1461 | 264 |
[ |
265 |
(cut_facts_tac prems 1), |
|
266 |
(rtac less_cprod4c 1), |
|
267 |
(dtac (beta_cfun_cprod RS subst) 1), |
|
268 |
(dtac (beta_cfun_cprod RS subst) 1), |
|
269 |
(atac 1) |
|
270 |
]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
271 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
272 |
|
892 | 273 |
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
|
274 |
"[|is_chain(S)|] ==> range(S) <<| \ |
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
899
diff
changeset
|
275 |
\ <(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
|
276 |
(fn prems => |
1461 | 277 |
[ |
278 |
(cut_facts_tac prems 1), |
|
2033 | 279 |
(stac beta_cfun_cprod 1), |
280 |
(stac (beta_cfun RS ext) 1), |
|
1461 | 281 |
(rtac cont_snd 1), |
2033 | 282 |
(stac (beta_cfun RS ext) 1), |
1461 | 283 |
(rtac cont_fst 1), |
284 |
(rtac lub_cprod 1), |
|
285 |
(atac 1) |
|
286 |
]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
287 |
|
1779 | 288 |
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
|
289 |
(* |
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
899
diff
changeset
|
290 |
is_chain ?S1 ==> |
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
899
diff
changeset
|
291 |
lub (range ?S1) = |
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
899
diff
changeset
|
292 |
<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
|
293 |
*) |
892 | 294 |
qed_goalw "csplit2" Cprod3.thy [csplit_def] |
1461 | 295 |
"csplit`f`<x,y> = f`x`y" |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
296 |
(fn prems => |
1461 | 297 |
[ |
2033 | 298 |
(stac beta_cfun 1), |
1461 | 299 |
(Simp_tac 1), |
300 |
(simp_tac (!simpset addsimps [cfst2,csnd2]) 1) |
|
301 |
]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
302 |
|
892 | 303 |
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
|
304 |
"csplit`cpair`z=z" |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
305 |
(fn prems => |
1461 | 306 |
[ |
2033 | 307 |
(stac beta_cfun 1), |
2566 | 308 |
(Simp_tac 1), |
1461 | 309 |
(simp_tac (!simpset addsimps [surjective_pairing_Cprod2]) 1) |
310 |
]); |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
311 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
312 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
313 |
(* install simplifier for Cprod *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
314 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
315 |
|
1267 | 316 |
Addsimps [cfst2,csnd2,csplit2]; |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
317 |
|
1274 | 318 |
val Cprod_rews = [cfst2,csnd2,csplit2]; |