src/HOLCF/Cprod.thy
changeset 15577 e16da3068ad6
parent 15576 efb95d0d01f7
child 15593 24d770bbc44a
equal deleted inserted replaced
15576:efb95d0d01f7 15577:e16da3068ad6
     6 Partial ordering for cartesian product of HOL theory prod.thy
     6 Partial ordering for cartesian product of HOL theory prod.thy
     7 *)
     7 *)
     8 
     8 
     9 header {* The cpo of cartesian products *}
     9 header {* The cpo of cartesian products *}
    10 
    10 
    11 theory Cprod = Cfun:
    11 theory Cprod
       
    12 imports Cfun
       
    13 begin
    12 
    14 
    13 defaultsort cpo
    15 defaultsort cpo
    14 
    16 
    15 instance "*"::(sq_ord,sq_ord)sq_ord ..
    17 instance "*"::(sq_ord,sq_ord)sq_ord ..
    16 
    18 
   229   "LAM <x,y,zs>.b"        == "csplit$(LAM x. LAM <y,zs>.b)"
   231   "LAM <x,y,zs>.b"        == "csplit$(LAM x. LAM <y,zs>.b)"
   230   "LAM <x,y>. LAM zs. b"  <= "csplit$(LAM x y zs. b)"
   232   "LAM <x,y>. LAM zs. b"  <= "csplit$(LAM x y zs. b)"
   231   "LAM <x,y>.b"           == "csplit$(LAM x y. b)"
   233   "LAM <x,y>.b"           == "csplit$(LAM x y. b)"
   232 
   234 
   233 syntax (xsymbols)
   235 syntax (xsymbols)
   234   "_LAM"    :: "[patterns, 'a => 'b] => ('a -> 'b)"  ("(3\\<Lambda>()<_>./ _)" [0, 10] 10)
   236   "_LAM"    :: "[patterns, 'a => 'b] => ('a -> 'b)"  ("(3\<Lambda>()<_>./ _)" [0, 10] 10)
   235 
   237 
   236 (* for compatibility with old HOLCF-Version *)
   238 (* for compatibility with old HOLCF-Version *)
   237 lemma inst_cprod_pcpo: "UU = (UU,UU)"
   239 lemma inst_cprod_pcpo: "UU = (UU,UU)"
   238 apply (simp add: UU_cprod_def[folded UU_def])
   240 apply (simp add: UU_cprod_def[folded UU_def])
   239 done
   241 done