111 *) |
111 *) |
112 |
112 |
113 lemma cpo_cprod: "chain(S::nat=>'a::cpo*'b::cpo)==>EX x. range S<<| x" |
113 lemma cpo_cprod: "chain(S::nat=>'a::cpo*'b::cpo)==>EX x. range S<<| x" |
114 by (rule exI, erule lub_cprod) |
114 by (rule exI, erule lub_cprod) |
115 |
115 |
116 instance "*" :: (cpo,cpo)cpo |
116 instance "*" :: (cpo, cpo) cpo |
117 by intro_classes (rule cpo_cprod) |
117 by intro_classes (rule cpo_cprod) |
118 |
118 |
119 subsection {* Type @{typ "'a * 'b"} is pointed *} |
119 subsection {* Type @{typ "'a * 'b"} is pointed *} |
120 |
120 |
121 lemma minimal_cprod: "(UU,UU)<<p" |
121 lemma minimal_cprod: "(UU,UU)<<p" |
126 lemma least_cprod: "EX x::'a*'b. ALL y. x<<y" |
126 lemma least_cprod: "EX x::'a*'b. ALL y. x<<y" |
127 apply (rule_tac x = " (UU,UU) " in exI) |
127 apply (rule_tac x = " (UU,UU) " in exI) |
128 apply (rule minimal_cprod [THEN allI]) |
128 apply (rule minimal_cprod [THEN allI]) |
129 done |
129 done |
130 |
130 |
131 instance "*" :: (pcpo,pcpo)pcpo |
131 instance "*" :: (pcpo, pcpo) pcpo |
132 by intro_classes (rule least_cprod) |
132 by intro_classes (rule least_cprod) |
133 |
133 |
134 text {* for compatibility with old HOLCF-Version *} |
134 text {* for compatibility with old HOLCF-Version *} |
135 lemma inst_cprod_pcpo: "UU = (UU,UU)" |
135 lemma inst_cprod_pcpo: "UU = (UU,UU)" |
136 apply (simp add: UU_cprod_def[folded UU_def]) |
136 apply (simp add: UU_cprod_def[folded UU_def]) |
209 cpair_def: "cpair == (LAM x y.(x,y))" |
209 cpair_def: "cpair == (LAM x y.(x,y))" |
210 cfst_def: "cfst == (LAM p. fst(p))" |
210 cfst_def: "cfst == (LAM p. fst(p))" |
211 csnd_def: "csnd == (LAM p. snd(p))" |
211 csnd_def: "csnd == (LAM p. snd(p))" |
212 csplit_def: "csplit == (LAM f p. f$(cfst$p)$(csnd$p))" |
212 csplit_def: "csplit == (LAM f p. f$(cfst$p)$(csnd$p))" |
213 |
213 |
214 |
214 subsection {* Syntax *} |
215 |
215 |
216 (* introduce syntax for |
216 text {* syntax for @{text "LAM <x,y,z>.e"} *} |
217 |
|
218 Let <x,y> = e1; z = E2 in E3 |
|
219 |
|
220 and |
|
221 |
|
222 LAM <x,y,z>.e |
|
223 *) |
|
224 |
|
225 constdefs |
|
226 CLet :: "'a -> ('a -> 'b) -> 'b" |
|
227 "CLet == LAM s f. f$s" |
|
228 |
|
229 |
|
230 (* syntax for Let *) |
|
231 |
|
232 nonterminals |
|
233 Cletbinds Cletbind |
|
234 |
|
235 syntax |
|
236 "_Cbind" :: "[pttrn, 'a] => Cletbind" ("(2_ =/ _)" 10) |
|
237 "" :: "Cletbind => Cletbinds" ("_") |
|
238 "_Cbinds" :: "[Cletbind, Cletbinds] => Cletbinds" ("_;/ _") |
|
239 "_CLet" :: "[Cletbinds, 'a] => 'a" ("(Let (_)/ in (_))" 10) |
|
240 |
|
241 translations |
|
242 "_CLet (_Cbinds b bs) e" == "_CLet b (_CLet bs e)" |
|
243 "Let x = a in e" == "CLet$a$(LAM x. e)" |
|
244 |
|
245 |
|
246 (* syntax for LAM <x,y,z>.e *) |
|
247 |
217 |
248 syntax |
218 syntax |
249 "_LAM" :: "[patterns, 'a => 'b] => ('a -> 'b)" ("(3LAM <_>./ _)" [0, 10] 10) |
219 "_LAM" :: "[patterns, 'a => 'b] => ('a -> 'b)" ("(3LAM <_>./ _)" [0, 10] 10) |
250 |
220 |
251 translations |
221 translations |
253 "LAM <x,y>. LAM zs. b" <= "csplit$(LAM x y zs. b)" |
223 "LAM <x,y>. LAM zs. b" <= "csplit$(LAM x y zs. b)" |
254 "LAM <x,y>.b" == "csplit$(LAM x y. b)" |
224 "LAM <x,y>.b" == "csplit$(LAM x y. b)" |
255 |
225 |
256 syntax (xsymbols) |
226 syntax (xsymbols) |
257 "_LAM" :: "[patterns, 'a => 'b] => ('a -> 'b)" ("(3\<Lambda>()<_>./ _)" [0, 10] 10) |
227 "_LAM" :: "[patterns, 'a => 'b] => ('a -> 'b)" ("(3\<Lambda>()<_>./ _)" [0, 10] 10) |
|
228 |
|
229 text {* syntax for Let *} |
|
230 |
|
231 constdefs |
|
232 CLet :: "'a::cpo -> ('a -> 'b::cpo) -> 'b" |
|
233 "CLet == LAM s f. f$s" |
|
234 |
|
235 nonterminals |
|
236 Cletbinds Cletbind |
|
237 |
|
238 syntax |
|
239 "_Cbind" :: "[pttrn, 'a] => Cletbind" ("(2_ =/ _)" 10) |
|
240 "_Cbindp" :: "[patterns, 'a] => Cletbind" ("(2<_> =/ _)" 10) |
|
241 "" :: "Cletbind => Cletbinds" ("_") |
|
242 "_Cbinds" :: "[Cletbind, Cletbinds] => Cletbinds" ("_;/ _") |
|
243 "_CLet" :: "[Cletbinds, 'a] => 'a" ("(Let (_)/ in (_))" 10) |
|
244 |
|
245 translations |
|
246 "_CLet (_Cbinds b bs) e" == "_CLet b (_CLet bs e)" |
|
247 "Let x = a in LAM ys. e" == "CLet$a$(LAM x ys. e)" |
|
248 "Let x = a in e" == "CLet$a$(LAM x. e)" |
|
249 "Let <xs> = a in e" == "CLet$a$(LAM <xs>. e)" |
258 |
250 |
259 subsection {* Convert all lemmas to the continuous versions *} |
251 subsection {* Convert all lemmas to the continuous versions *} |
260 |
252 |
261 lemma beta_cfun_cprod: |
253 lemma beta_cfun_cprod: |
262 "(LAM x y.(x,y))$a$b = (a,b)" |
254 "(LAM x y.(x,y))$a$b = (a,b)" |