src/HOLCF/Cprod.thy
changeset 15609 d12c459e2325
parent 15600 a59f07556a8d
child 16008 861a255cf1e7
equal deleted inserted replaced
15608:f161fa6f8fd5 15609:d12c459e2325
   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)"