--- a/src/HOLCF/Cprod.thy Mon Mar 14 17:04:10 2005 +0100
+++ b/src/HOLCF/Cprod.thy Mon Mar 14 20:30:43 2005 +0100
@@ -113,7 +113,7 @@
lemma cpo_cprod: "chain(S::nat=>'a::cpo*'b::cpo)==>EX x. range S<<| x"
by (rule exI, erule lub_cprod)
-instance "*" :: (cpo,cpo)cpo
+instance "*" :: (cpo, cpo) cpo
by intro_classes (rule cpo_cprod)
subsection {* Type @{typ "'a * 'b"} is pointed *}
@@ -128,7 +128,7 @@
apply (rule minimal_cprod [THEN allI])
done
-instance "*" :: (pcpo,pcpo)pcpo
+instance "*" :: (pcpo, pcpo) pcpo
by intro_classes (rule least_cprod)
text {* for compatibility with old HOLCF-Version *}
@@ -211,39 +211,9 @@
csnd_def: "csnd == (LAM p. snd(p))"
csplit_def: "csplit == (LAM f p. f$(cfst$p)$(csnd$p))"
-
-
-(* introduce syntax for
-
- Let <x,y> = e1; z = E2 in E3
-
- and
-
- LAM <x,y,z>.e
-*)
-
-constdefs
- CLet :: "'a -> ('a -> 'b) -> 'b"
- "CLet == LAM s f. f$s"
-
+subsection {* Syntax *}
-(* syntax for Let *)
-
-nonterminals
- Cletbinds Cletbind
-
-syntax
- "_Cbind" :: "[pttrn, 'a] => Cletbind" ("(2_ =/ _)" 10)
- "" :: "Cletbind => Cletbinds" ("_")
- "_Cbinds" :: "[Cletbind, Cletbinds] => Cletbinds" ("_;/ _")
- "_CLet" :: "[Cletbinds, 'a] => 'a" ("(Let (_)/ in (_))" 10)
-
-translations
- "_CLet (_Cbinds b bs) e" == "_CLet b (_CLet bs e)"
- "Let x = a in e" == "CLet$a$(LAM x. e)"
-
-
-(* syntax for LAM <x,y,z>.e *)
+text {* syntax for @{text "LAM <x,y,z>.e"} *}
syntax
"_LAM" :: "[patterns, 'a => 'b] => ('a -> 'b)" ("(3LAM <_>./ _)" [0, 10] 10)
@@ -256,6 +226,28 @@
syntax (xsymbols)
"_LAM" :: "[patterns, 'a => 'b] => ('a -> 'b)" ("(3\<Lambda>()<_>./ _)" [0, 10] 10)
+text {* syntax for Let *}
+
+constdefs
+ CLet :: "'a::cpo -> ('a -> 'b::cpo) -> 'b"
+ "CLet == LAM s f. f$s"
+
+nonterminals
+ Cletbinds Cletbind
+
+syntax
+ "_Cbind" :: "[pttrn, 'a] => Cletbind" ("(2_ =/ _)" 10)
+ "_Cbindp" :: "[patterns, 'a] => Cletbind" ("(2<_> =/ _)" 10)
+ "" :: "Cletbind => Cletbinds" ("_")
+ "_Cbinds" :: "[Cletbind, Cletbinds] => Cletbinds" ("_;/ _")
+ "_CLet" :: "[Cletbinds, 'a] => 'a" ("(Let (_)/ in (_))" 10)
+
+translations
+ "_CLet (_Cbinds b bs) e" == "_CLet b (_CLet bs e)"
+ "Let x = a in LAM ys. e" == "CLet$a$(LAM x ys. e)"
+ "Let x = a in e" == "CLet$a$(LAM x. e)"
+ "Let <xs> = a in e" == "CLet$a$(LAM <xs>. e)"
+
subsection {* Convert all lemmas to the continuous versions *}
lemma beta_cfun_cprod: