src/CCL/Type.thy
author paulson
Fri Feb 16 17:24:51 1996 +0100 (1996-02-16)
changeset 1511 09354d37a5ab
parent 1474 3f7d67927fe2
child 3837 d7f033c74b38
permissions -rw-r--r--
Elimination of fully-functorial style.
Type tactic changed to a type abbrevation (from a datatype).
Constructor tactic and function apply deleted.
     1 (*  Title:      CCL/types.thy
     2     ID:         $Id$
     3     Author:     Martin Coen
     4     Copyright   1993  University of Cambridge
     5 
     6 Types in CCL are defined as sets of terms.
     7 
     8 *)
     9 
    10 Type = Term +
    11 
    12 consts
    13 
    14   Subtype       :: "['a set, 'a => o] => 'a set"
    15   Bool          :: "i set"
    16   Unit          :: "i set"
    17   "+"           :: "[i set, i set] => i set"         (infixr 55)
    18   Pi            :: "[i set, i => i set] => i set"
    19   Sigma         :: "[i set, i => i set] => i set"
    20   Nat           :: "i set"
    21   List          :: "i set => i set"
    22   Lists         :: "i set => i set"
    23   ILists        :: "i set => i set"
    24   TAll          :: "(i set => i set) => i set"       (binder "TALL " 55)
    25   TEx           :: "(i set => i set) => i set"       (binder "TEX " 55)
    26   Lift          :: "i set => i set"                  ("(3[_])")
    27 
    28   SPLIT         :: "[i, [i, i] => i set] => i set"
    29 
    30   "@Pi"         :: "[idt, i set, i set] => i set"    ("(3PROD _:_./ _)"
    31                                 [0,0,60] 60)
    32 
    33   "@Sigma"      :: "[idt, i set, i set] => i set"    ("(3SUM _:_./ _)"
    34                                 [0,0,60] 60)
    35   
    36   "@->"         :: "[i set, i set] => i set"         ("(_ ->/ _)"  [54, 53] 53)
    37   "@*"          :: "[i set, i set] => i set"         ("(_ */ _)" [56, 55] 55)
    38   "@Subtype"    :: "[idt, 'a set, o] => 'a set"      ("(1{_: _ ./ _})")
    39 
    40 translations
    41   "PROD x:A. B" => "Pi(A, %x. B)"
    42   "A -> B"      => "Pi(A, _K(B))"
    43   "SUM x:A. B"  => "Sigma(A, %x. B)"
    44   "A * B"       => "Sigma(A, _K(B))"
    45   "{x: A. B}"   == "Subtype(A, %x. B)"
    46 
    47 rules
    48 
    49   Subtype_def "{x:A.P(x)} == {x.x:A & P(x)}"
    50   Unit_def          "Unit == {x.x=one}"
    51   Bool_def          "Bool == {x.x=true | x=false}"
    52   Plus_def           "A+B == {x. (EX a:A.x=inl(a)) | (EX b:B.x=inr(b))}"
    53   Pi_def         "Pi(A,B) == {x.EX b.x=lam x.b(x) & (ALL x:A.b(x):B(x))}"
    54   Sigma_def   "Sigma(A,B) == {x.EX a:A.EX b:B(a).x=<a,b>}"
    55   Nat_def            "Nat == lfp(% X.Unit + X)"
    56   List_def       "List(A) == lfp(% X.Unit + A*X)"
    57 
    58   Lists_def     "Lists(A) == gfp(% X.Unit + A*X)"
    59   ILists_def   "ILists(A) == gfp(% X.{} + A*X)"
    60 
    61   Tall_def   "TALL X.B(X) == Inter({X.EX Y.X=B(Y)})"
    62   Tex_def     "TEX X.B(X) == Union({X.EX Y.X=B(Y)})"
    63   Lift_def           "[A] == A Un {bot}"
    64 
    65   SPLIT_def   "SPLIT(p,B) == Union({A.EX x y.p=<x,y> & A=B(x,y)})"
    66 
    67 end
    68 
    69 
    70 ML
    71 
    72 val print_translation =
    73   [("Pi", dependent_tr' ("@Pi", "@->")),
    74    ("Sigma", dependent_tr' ("@Sigma", "@*"))];
    75