src/HOLCF/One.thy
changeset 2640 ee4dfce170a0
parent 2275 dbce3dce821a
child 3717 e28553315355
     1.1 --- a/src/HOLCF/One.thy	Sat Feb 15 18:24:05 1997 +0100
     1.2 +++ b/src/HOLCF/One.thy	Mon Feb 17 10:57:11 1997 +0100
     1.3 @@ -1,47 +1,21 @@
     1.4 -(*  Title:      HOLCF/one.thy
     1.5 +(*  Title:      HOLCF/One.thy
     1.6      ID:         $Id$
     1.7 -    Author:     Franz Regensburger
     1.8 -    Copyright   1993 Technische Universitaet Muenchen
     1.9 -
    1.10 -Introduce atomic type one = (void)u
    1.11 -
    1.12 -The type is axiomatized as the least solution of a domain equation.
    1.13 -The functor term that specifies the domain equation is: 
    1.14 -
    1.15 -  FT = <U,K_{void}>
    1.16 -
    1.17 -For details see chapter 5 of:
    1.18 -
    1.19 -[Franz Regensburger] HOLCF: Eine konservative Erweiterung von HOL um LCF,
    1.20 -                     Dissertation, Technische Universit"at M"unchen, 1994
    1.21 -
    1.22 +    Author:     Oscar Slotosch
    1.23 +    Copyright   1997 Technische Universitaet Muenchen
    1.24  *)
    1.25  
    1.26 -One = ccc1+
    1.27 +One = Lift +
    1.28  
    1.29 -types one 0
    1.30 -arities one :: pcpo
    1.31 +types one = "unit lift"
    1.32  
    1.33  consts
    1.34 -        abs_one         :: "(void)u -> one"
    1.35 -        rep_one         :: "one -> (void)u"
    1.36 -        one             :: "one"
    1.37 -        one_when        :: "'c -> one -> 'c"
    1.38 +	ONE             :: "one"
    1.39 +
    1.40 +translations
    1.41 +	     "one" == (type) "unit lift" 
    1.42  
    1.43  rules
    1.44 -  abs_one_iso   "abs_one`(rep_one`u) = u"
    1.45 -  rep_one_iso   "rep_one`(abs_one`x) = x"
    1.46 -
    1.47 -defs
    1.48 -  one_def       "one == abs_one`(up`UU)"
    1.49 -  one_when_def "one_when == (LAM c u.fup`(LAM x.c)`(rep_one`u))"
    1.50 -
    1.51 -translations
    1.52 -  "case l of one => t1" == "one_when`t1`l"
    1.53 -
    1.54 +  ONE_def     "ONE == Def()"
    1.55  end
    1.56  
    1.57  
    1.58 -
    1.59 -
    1.60 -