src/HOLCF/One.thy
author regensbu
Fri Oct 06 17:25:24 1995 +0100 (1995-10-06)
changeset 1274 ea0668a1c0ba
parent 1168 74be52691d62
child 1479 21eb5e156d91
permissions -rw-r--r--
added 8bit pragmas
added directory ax_ops for sections axioms and ops
added directory domain for sections domain and generated
this is the type definition package of David Oheimb
     1 (*  Title: 	HOLCF/one.thy
     2     ID:         $Id$
     3     Author: 	Franz Regensburger
     4     Copyright   1993 Technische Universitaet Muenchen
     5 
     6 Introduce atomic type one = (void)u
     7 
     8 The type is axiomatized as the least solution of a domain equation.
     9 The functor term that specifies the domain equation is: 
    10 
    11   FT = <U,K_{void}>
    12 
    13 For details see chapter 5 of:
    14 
    15 [Franz Regensburger] HOLCF: Eine konservative Erweiterung von HOL um LCF,
    16                      Dissertation, Technische Universit"at M"unchen, 1994
    17 
    18 *)
    19 
    20 One = ccc1+
    21 
    22 types one 0
    23 arities one :: pcpo
    24 
    25 consts
    26 	abs_one		:: "(void)u -> one"
    27 	rep_one		:: "one -> (void)u"
    28 	one 		:: "one"
    29 	one_when 	:: "'c -> one -> 'c"
    30 
    31 rules
    32   abs_one_iso	"abs_one`(rep_one`u) = u"
    33   rep_one_iso	"rep_one`(abs_one`x) = x"
    34 
    35 defs
    36   one_def	"one == abs_one`(up`UU)"
    37   one_when_def "one_when == (LAM c u.lift`(LAM x.c)`(rep_one`u))"
    38 
    39 translations
    40   "case l of one => t1" == "one_when`t1`l"
    41 
    42 end
    43 
    44 
    45 
    46 
    47