author | nipkow |
Sun, 22 Dec 2002 10:43:43 +0100 | |
changeset 13763 | f94b569cd610 |
parent 12030 | 46d57d0290a2 |
child 14981 | e73f8140af78 |
permissions | -rw-r--r-- |
9245 | 1 |
(* Title: HOLCF/Cprod3 |
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 |
12030 | 4 |
License: GPL (GNU GENERAL PUBLIC LICENSE) |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
5 |
|
9245 | 6 |
Class instance of * for class pcpo and cpo. |
243
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 |
|
2640 | 9 |
(* for compatibility with old HOLCF-Version *) |
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
10 |
Goal "UU = (UU,UU)"; |
9245 | 11 |
by (simp_tac (HOL_ss addsimps [UU_def,UU_cprod_def]) 1); |
12 |
qed "inst_cprod_pcpo"; |
|
2640 | 13 |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
14 |
(* ------------------------------------------------------------------------ *) |
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
899
diff
changeset
|
15 |
(* continuity of (_,_) , fst, snd *) |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
16 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
17 |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
18 |
Goal |
4721
c8a8482a8124
renamed is_chain to chain, is_tord to tord, replaced chain_finite by chfin
oheimb
parents:
4098
diff
changeset
|
19 |
"chain(Y::(nat=>'a::cpo)) ==>\ |
2840
7e03e61612b0
generalized theorems and class instances for Cprod.
slotosch
parents:
2640
diff
changeset
|
20 |
\ (lub(range(Y)),(x::'b::cpo)) =\ |
9245 | 21 |
\ (lub(range(%i. fst(Y i,x))),lub(range(%i. snd(Y i,x))))"; |
22 |
by (res_inst_tac [("f1","Pair")] (arg_cong RS cong) 1); |
|
23 |
by (rtac lub_equal 1); |
|
24 |
by (atac 1); |
|
25 |
by (rtac (monofun_fst RS ch2ch_monofun) 1); |
|
26 |
by (rtac ch2ch_fun 1); |
|
27 |
by (rtac (monofun_pair1 RS ch2ch_monofun) 1); |
|
28 |
by (atac 1); |
|
29 |
by (rtac allI 1); |
|
30 |
by (Simp_tac 1); |
|
31 |
by (rtac sym 1); |
|
32 |
by (Simp_tac 1); |
|
33 |
by (rtac (lub_const RS thelubI) 1); |
|
34 |
qed "Cprod3_lemma1"; |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
35 |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
36 |
Goal "contlub(Pair)"; |
9245 | 37 |
by (rtac contlubI 1); |
38 |
by (strip_tac 1); |
|
39 |
by (rtac (expand_fun_eq RS iffD2) 1); |
|
40 |
by (strip_tac 1); |
|
41 |
by (stac (lub_fun RS thelubI) 1); |
|
42 |
by (etac (monofun_pair1 RS ch2ch_monofun) 1); |
|
43 |
by (rtac trans 1); |
|
44 |
by (rtac (thelub_cprod RS sym) 2); |
|
45 |
by (rtac ch2ch_fun 2); |
|
46 |
by (etac (monofun_pair1 RS ch2ch_monofun) 2); |
|
47 |
by (etac Cprod3_lemma1 1); |
|
48 |
qed "contlub_pair1"; |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
49 |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
50 |
Goal |
4721
c8a8482a8124
renamed is_chain to chain, is_tord to tord, replaced chain_finite by chfin
oheimb
parents:
4098
diff
changeset
|
51 |
"chain(Y::(nat=>'a::cpo)) ==>\ |
2840
7e03e61612b0
generalized theorems and class instances for Cprod.
slotosch
parents:
2640
diff
changeset
|
52 |
\ ((x::'b::cpo),lub(range Y)) =\ |
9245 | 53 |
\ (lub(range(%i. fst(x,Y i))),lub(range(%i. snd(x, Y i))))"; |
54 |
by (res_inst_tac [("f1","Pair")] (arg_cong RS cong) 1); |
|
55 |
by (rtac sym 1); |
|
56 |
by (Simp_tac 1); |
|
57 |
by (rtac (lub_const RS thelubI) 1); |
|
58 |
by (rtac lub_equal 1); |
|
59 |
by (atac 1); |
|
60 |
by (rtac (monofun_snd RS ch2ch_monofun) 1); |
|
61 |
by (rtac (monofun_pair2 RS ch2ch_monofun) 1); |
|
62 |
by (atac 1); |
|
63 |
by (rtac allI 1); |
|
64 |
by (Simp_tac 1); |
|
65 |
qed "Cprod3_lemma2"; |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
66 |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
67 |
Goal "contlub(Pair(x))"; |
9245 | 68 |
by (rtac contlubI 1); |
69 |
by (strip_tac 1); |
|
70 |
by (rtac trans 1); |
|
71 |
by (rtac (thelub_cprod RS sym) 2); |
|
72 |
by (etac (monofun_pair2 RS ch2ch_monofun) 2); |
|
73 |
by (etac Cprod3_lemma2 1); |
|
74 |
qed "contlub_pair2"; |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
75 |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
76 |
Goal "cont(Pair)"; |
9245 | 77 |
by (rtac monocontlub2cont 1); |
78 |
by (rtac monofun_pair1 1); |
|
79 |
by (rtac contlub_pair1 1); |
|
80 |
qed "cont_pair1"; |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
81 |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
82 |
Goal "cont(Pair(x))"; |
9245 | 83 |
by (rtac monocontlub2cont 1); |
84 |
by (rtac monofun_pair2 1); |
|
85 |
by (rtac contlub_pair2 1); |
|
86 |
qed "cont_pair2"; |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
87 |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
88 |
Goal "contlub(fst)"; |
9245 | 89 |
by (rtac contlubI 1); |
90 |
by (strip_tac 1); |
|
91 |
by (stac (lub_cprod RS thelubI) 1); |
|
92 |
by (atac 1); |
|
93 |
by (Simp_tac 1); |
|
94 |
qed "contlub_fst"; |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
95 |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
96 |
Goal "contlub(snd)"; |
9245 | 97 |
by (rtac contlubI 1); |
98 |
by (strip_tac 1); |
|
99 |
by (stac (lub_cprod RS thelubI) 1); |
|
100 |
by (atac 1); |
|
101 |
by (Simp_tac 1); |
|
102 |
qed "contlub_snd"; |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
103 |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
104 |
Goal "cont(fst)"; |
9245 | 105 |
by (rtac monocontlub2cont 1); |
106 |
by (rtac monofun_fst 1); |
|
107 |
by (rtac contlub_fst 1); |
|
108 |
qed "cont_fst"; |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
109 |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
110 |
Goal "cont(snd)"; |
9245 | 111 |
by (rtac monocontlub2cont 1); |
112 |
by (rtac monofun_snd 1); |
|
113 |
by (rtac contlub_snd 1); |
|
114 |
qed "cont_snd"; |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
115 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
116 |
(* |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
117 |
-------------------------------------------------------------------------- |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
118 |
more lemmas for Cprod3.thy |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
119 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
120 |
-------------------------------------------------------------------------- |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
121 |
*) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
122 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
123 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
124 |
(* convert all lemmas to the continuous versions *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
125 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
126 |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
127 |
Goalw [cpair_def] |
10834 | 128 |
"(LAM x y.(x,y))$a$b = (a,b)"; |
9245 | 129 |
by (stac beta_cfun 1); |
130 |
by (simp_tac (simpset() addsimps [cont_pair1,cont_pair2,cont2cont_CF1L]) 1); |
|
131 |
by (stac beta_cfun 1); |
|
132 |
by (rtac cont_pair2 1); |
|
133 |
by (rtac refl 1); |
|
134 |
qed "beta_cfun_cprod"; |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
135 |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
136 |
Goalw [cpair_def] |
9245 | 137 |
" <a,b>=<aa,ba> ==> a=aa & b=ba"; |
138 |
by (dtac (beta_cfun_cprod RS subst) 1); |
|
139 |
by (dtac (beta_cfun_cprod RS subst) 1); |
|
140 |
by (etac Pair_inject 1); |
|
141 |
by (fast_tac HOL_cs 1); |
|
142 |
qed "inject_cpair"; |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
143 |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
144 |
Goalw [cpair_def] "UU = <UU,UU>"; |
9245 | 145 |
by (rtac sym 1); |
146 |
by (rtac trans 1); |
|
147 |
by (rtac beta_cfun_cprod 1); |
|
148 |
by (rtac sym 1); |
|
149 |
by (rtac inst_cprod_pcpo 1); |
|
150 |
qed "inst_cprod_pcpo2"; |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
151 |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
152 |
Goal |
9245 | 153 |
"<a,b> = UU ==> a = UU & b = UU"; |
154 |
by (dtac (inst_cprod_pcpo2 RS subst) 1); |
|
155 |
by (etac inject_cpair 1); |
|
156 |
qed "defined_cpair_rev"; |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
157 |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
158 |
Goalw [cpair_def] |
9245 | 159 |
"? a b. z=<a,b>"; |
160 |
by (rtac PairE 1); |
|
161 |
by (rtac exI 1); |
|
162 |
by (rtac exI 1); |
|
163 |
by (etac (beta_cfun_cprod RS ssubst) 1); |
|
164 |
qed "Exh_Cprod2"; |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
165 |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
166 |
val prems = Goalw [cpair_def] "[|!!x y. [|p=<x,y> |] ==> Q|] ==> Q"; |
9245 | 167 |
by (rtac PairE 1); |
168 |
by (resolve_tac prems 1); |
|
169 |
by (etac (beta_cfun_cprod RS ssubst) 1); |
|
170 |
qed "cprodE"; |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
171 |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
172 |
Goalw [cfst_def,cpair_def] |
10834 | 173 |
"cfst$<x,y>=x"; |
9245 | 174 |
by (stac beta_cfun_cprod 1); |
175 |
by (stac beta_cfun 1); |
|
176 |
by (rtac cont_fst 1); |
|
177 |
by (Simp_tac 1); |
|
178 |
qed "cfst2"; |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
179 |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
180 |
Goalw [csnd_def,cpair_def] |
10834 | 181 |
"csnd$<x,y>=y"; |
9245 | 182 |
by (stac beta_cfun_cprod 1); |
183 |
by (stac beta_cfun 1); |
|
184 |
by (rtac cont_snd 1); |
|
185 |
by (Simp_tac 1); |
|
186 |
qed "csnd2"; |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
187 |
|
10834 | 188 |
Goal "cfst$UU = UU"; |
9245 | 189 |
by (simp_tac (HOL_ss addsimps [inst_cprod_pcpo2,cfst2]) 1); |
190 |
qed "cfst_strict"; |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
191 |
|
10834 | 192 |
Goal "csnd$UU = UU"; |
9245 | 193 |
by (simp_tac (HOL_ss addsimps [inst_cprod_pcpo2,csnd2]) 1); |
194 |
qed "csnd_strict"; |
|
2444 | 195 |
|
10834 | 196 |
Goalw [cfst_def,csnd_def,cpair_def] "<cfst$p , csnd$p> = p"; |
9245 | 197 |
by (stac beta_cfun_cprod 1); |
198 |
by (stac beta_cfun 1); |
|
199 |
by (rtac cont_snd 1); |
|
200 |
by (stac beta_cfun 1); |
|
201 |
by (rtac cont_fst 1); |
|
202 |
by (rtac (surjective_pairing RS sym) 1); |
|
203 |
qed "surjective_pairing_Cprod2"; |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
204 |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
205 |
Goalw [cfst_def,csnd_def,cpair_def] |
9245 | 206 |
"<xa,ya> << <x,y> ==> xa<<x & ya << y"; |
207 |
by (rtac less_cprod4c 1); |
|
208 |
by (dtac (beta_cfun_cprod RS subst) 1); |
|
209 |
by (dtac (beta_cfun_cprod RS subst) 1); |
|
210 |
by (atac 1); |
|
211 |
qed "less_cprod5c"; |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
212 |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
213 |
Goalw [cfst_def,csnd_def,cpair_def] |
4721
c8a8482a8124
renamed is_chain to chain, is_tord to tord, replaced chain_finite by chfin
oheimb
parents:
4098
diff
changeset
|
214 |
"[|chain(S)|] ==> range(S) <<| \ |
10834 | 215 |
\ <(lub(range(%i. cfst$(S i)))) , lub(range(%i. csnd$(S i)))>"; |
9245 | 216 |
by (stac beta_cfun_cprod 1); |
217 |
by (stac (beta_cfun RS ext) 1); |
|
218 |
by (rtac cont_snd 1); |
|
219 |
by (stac (beta_cfun RS ext) 1); |
|
220 |
by (rtac cont_fst 1); |
|
221 |
by (rtac lub_cprod 1); |
|
222 |
by (atac 1); |
|
223 |
qed "lub_cprod2"; |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
224 |
|
1779 | 225 |
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
|
226 |
(* |
4721
c8a8482a8124
renamed is_chain to chain, is_tord to tord, replaced chain_finite by chfin
oheimb
parents:
4098
diff
changeset
|
227 |
chain ?S1 ==> |
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
899
diff
changeset
|
228 |
lub (range ?S1) = |
10834 | 229 |
<lub (range (%i. cfst$(?S1 i))), lub (range (%i. csnd$(?S1 i)))>" |
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
899
diff
changeset
|
230 |
*) |
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
231 |
Goalw [csplit_def] |
10834 | 232 |
"csplit$f$<x,y> = f$x$y"; |
9245 | 233 |
by (stac beta_cfun 1); |
234 |
by (Simp_tac 1); |
|
235 |
by (simp_tac (simpset() addsimps [cfst2,csnd2]) 1); |
|
236 |
qed "csplit2"; |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
237 |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
238 |
Goalw [csplit_def] |
10834 | 239 |
"csplit$cpair$z=z"; |
9245 | 240 |
by (stac beta_cfun 1); |
241 |
by (Simp_tac 1); |
|
242 |
by (simp_tac (simpset() addsimps [surjective_pairing_Cprod2]) 1); |
|
243 |
qed "csplit3"; |
|
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 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
246 |
(* install simplifier for Cprod *) |
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 |
|
1267 | 249 |
Addsimps [cfst2,csnd2,csplit2]; |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
250 |
|
1274 | 251 |
val Cprod_rews = [cfst2,csnd2,csplit2]; |