src/HOLCF/Cprod.thy
changeset 15609 d12c459e2325
parent 15600 a59f07556a8d
child 16008 861a255cf1e7
     1.1 --- a/src/HOLCF/Cprod.thy	Mon Mar 14 17:04:10 2005 +0100
     1.2 +++ b/src/HOLCF/Cprod.thy	Mon Mar 14 20:30:43 2005 +0100
     1.3 @@ -113,7 +113,7 @@
     1.4  lemma cpo_cprod: "chain(S::nat=>'a::cpo*'b::cpo)==>EX x. range S<<| x"
     1.5  by (rule exI, erule lub_cprod)
     1.6  
     1.7 -instance "*" :: (cpo,cpo)cpo
     1.8 +instance "*" :: (cpo, cpo) cpo
     1.9  by intro_classes (rule cpo_cprod)
    1.10  
    1.11  subsection {* Type @{typ "'a * 'b"} is pointed *}
    1.12 @@ -128,7 +128,7 @@
    1.13  apply (rule minimal_cprod [THEN allI])
    1.14  done
    1.15  
    1.16 -instance "*" :: (pcpo,pcpo)pcpo
    1.17 +instance "*" :: (pcpo, pcpo) pcpo
    1.18  by intro_classes (rule least_cprod)
    1.19  
    1.20  text {* for compatibility with old HOLCF-Version *}
    1.21 @@ -211,39 +211,9 @@
    1.22  csnd_def:        "csnd   == (LAM p. snd(p))"      
    1.23  csplit_def:      "csplit == (LAM f p. f$(cfst$p)$(csnd$p))"
    1.24  
    1.25 -
    1.26 -
    1.27 -(* introduce syntax for
    1.28 -
    1.29 -   Let <x,y> = e1; z = E2 in E3
    1.30 -
    1.31 -   and
    1.32 -
    1.33 -   LAM <x,y,z>.e
    1.34 -*)
    1.35 -
    1.36 -constdefs
    1.37 -  CLet           :: "'a -> ('a -> 'b) -> 'b"
    1.38 -  "CLet == LAM s f. f$s"
    1.39 -
    1.40 +subsection {* Syntax *}
    1.41  
    1.42 -(* syntax for Let *)
    1.43 -
    1.44 -nonterminals
    1.45 -  Cletbinds  Cletbind
    1.46 -
    1.47 -syntax
    1.48 -  "_Cbind"  :: "[pttrn, 'a] => Cletbind"             ("(2_ =/ _)" 10)
    1.49 -  ""        :: "Cletbind => Cletbinds"               ("_")
    1.50 -  "_Cbinds" :: "[Cletbind, Cletbinds] => Cletbinds"  ("_;/ _")
    1.51 -  "_CLet"   :: "[Cletbinds, 'a] => 'a"               ("(Let (_)/ in (_))" 10)
    1.52 -
    1.53 -translations
    1.54 -  "_CLet (_Cbinds b bs) e"  == "_CLet b (_CLet bs e)"
    1.55 -  "Let x = a in e"          == "CLet$a$(LAM x. e)"
    1.56 -
    1.57 -
    1.58 -(* syntax for LAM <x,y,z>.e *)
    1.59 +text {* syntax for @{text "LAM <x,y,z>.e"} *}
    1.60  
    1.61  syntax
    1.62    "_LAM"    :: "[patterns, 'a => 'b] => ('a -> 'b)"  ("(3LAM <_>./ _)" [0, 10] 10)
    1.63 @@ -256,6 +226,28 @@
    1.64  syntax (xsymbols)
    1.65    "_LAM"    :: "[patterns, 'a => 'b] => ('a -> 'b)"  ("(3\<Lambda>()<_>./ _)" [0, 10] 10)
    1.66  
    1.67 +text {* syntax for Let *}
    1.68 +
    1.69 +constdefs
    1.70 +  CLet           :: "'a::cpo -> ('a -> 'b::cpo) -> 'b"
    1.71 +  "CLet == LAM s f. f$s"
    1.72 +
    1.73 +nonterminals
    1.74 +  Cletbinds  Cletbind
    1.75 +
    1.76 +syntax
    1.77 +  "_Cbind"  :: "[pttrn, 'a] => Cletbind"             ("(2_ =/ _)" 10)
    1.78 +  "_Cbindp" :: "[patterns, 'a] => Cletbind"          ("(2<_> =/ _)" 10)
    1.79 +  ""        :: "Cletbind => Cletbinds"               ("_")
    1.80 +  "_Cbinds" :: "[Cletbind, Cletbinds] => Cletbinds"  ("_;/ _")
    1.81 +  "_CLet"   :: "[Cletbinds, 'a] => 'a"               ("(Let (_)/ in (_))" 10)
    1.82 +
    1.83 +translations
    1.84 +  "_CLet (_Cbinds b bs) e"  == "_CLet b (_CLet bs e)"
    1.85 +  "Let x = a in LAM ys. e"  == "CLet$a$(LAM x ys. e)"
    1.86 +  "Let x = a in e"          == "CLet$a$(LAM x. e)"
    1.87 +  "Let <xs> = a in e"       == "CLet$a$(LAM <xs>. e)"
    1.88 +
    1.89  subsection {* Convert all lemmas to the continuous versions *}
    1.90  
    1.91  lemma beta_cfun_cprod: