Mercurial Mercurial > repos > isabelle / file revision
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOLCF/Ssum3.thy
author nipkow
Tue, 13 Aug 2002 22:01:53 +0200
changeset 13501 79242cccaddc
parent 12030 46d57d0290a2
child 14981 e73f8140af78
permissions -rw-r--r--
arith_tac should not produce counter example

(*  Title:      HOLCF/ssum3.thy
    ID:         $Id$
    Author:     Franz Regensburger
    License:    GPL (GNU GENERAL PUBLIC LICENSE)

Class instance of  ++ for class pcpo
*)

Ssum3 = Ssum2 +

instance "++" :: (pcpo,pcpo)pcpo (least_ssum,cpo_ssum)

consts  
        sinl    :: "'a -> ('a++'b)" 
        sinr    :: "'b -> ('a++'b)" 
        sscase  :: "('a->'c)->('b->'c)->('a ++ 'b)-> 'c"

defs

sinl_def        "sinl   == (LAM x. Isinl(x))"
sinr_def        "sinr   == (LAM x. Isinr(x))"
sscase_def      "sscase   == (LAM f g s. Iwhen(f)(g)(s))"

translations
"case s of sinl$x => t1 | sinr$y => t2" == "sscase$(LAM x. t1)$(LAM y. t2)$s"

end
isabelle