src/CCL/Type.thy
changeset 0 a5a9c433f639
child 22 41dc6b189412
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/CCL/Type.thy	Thu Sep 16 12:20:38 1993 +0200
     1.3 @@ -0,0 +1,73 @@
     1.4 +(*  Title:      CCL/types.thy
     1.5 +    ID:         $Id$
     1.6 +    Author:     Martin Coen
     1.7 +    Copyright   1993  University of Cambridge
     1.8 +
     1.9 +Types in CCL are defined as sets of terms.
    1.10 +
    1.11 +*)
    1.12 +
    1.13 +Type = Term +
    1.14 +
    1.15 +consts
    1.16 +
    1.17 +  Subtype       :: "['a set, 'a => o] => 'a set"
    1.18 +  Bool          :: "i set"
    1.19 +  Unit          :: "i set"
    1.20 +  "+"           :: "[i set, i set] => i set"            (infixr 55)
    1.21 +  Pi            :: "[i set, i => i set] => i set"
    1.22 +  Sigma         :: "[i set, i => i set] => i set"
    1.23 +  Nat           :: "i set"
    1.24 +  List          :: "i set => i set"
    1.25 +  Lists         :: "i set => i set"
    1.26 +  ILists        :: "i set => i set"
    1.27 +  TAll          :: "(i set => i set) => i set"          (binder "TALL " 55)
    1.28 +  TEx           :: "(i set => i set) => i set"          (binder "TEX " 55)
    1.29 +  Lift          :: "i set => i set"                     ("(3[_])")
    1.30 +
    1.31 +  SPLIT         :: "[i, [i, i] => i set] => i set"
    1.32 +
    1.33 +  "@Pi"         :: "[idt, i set, i set] => i set"       ("(3PROD _:_./ _)" [] 60)
    1.34 +  "@Sigma"      :: "[idt, i set, i set] => i set"       ("(3SUM _:_./ _)" [] 60)
    1.35 +  "@->"         :: "[i set, i set] => i set"            ("(_ ->/ _)"  [54, 53] 53)
    1.36 +  "@*"          :: "[i set, i set] => i set"            ("(_ */ _)" [56, 55] 55)
    1.37 +  "@Subtype"    :: "[idt, 'a set, o] => 'a set"         ("(1{_: _ ./ _})")
    1.38 +
    1.39 +translations
    1.40 +  "PROD x:A. B" => "Pi(A, %x. B)"
    1.41 +  "SUM x:A. B"  => "Sigma(A, %x. B)"
    1.42 +  "{x: A. B}"   == "Subtype(A, %x. B)"
    1.43 +
    1.44 +rules
    1.45 +
    1.46 +  Subtype_def "{x:A.P(x)} == {x.x:A & P(x)}"
    1.47 +  Unit_def          "Unit == {x.x=one}"
    1.48 +  Bool_def          "Bool == {x.x=true | x=false}"
    1.49 +  Plus_def           "A+B == {x. (EX a:A.x=inl(a)) | (EX b:B.x=inr(b))}"
    1.50 +  Pi_def         "Pi(A,B) == {x.EX b.x=lam x.b(x) & (ALL x:A.b(x):B(x))}"
    1.51 +  Sigma_def   "Sigma(A,B) == {x.EX a:A.EX b:B(a).x=<a,b>}"
    1.52 +  Nat_def            "Nat == lfp(% X.Unit + X)"
    1.53 +  List_def       "List(A) == lfp(% X.Unit + A*X)"
    1.54 +
    1.55 +  Lists_def     "Lists(A) == gfp(% X.Unit + A*X)"
    1.56 +  ILists_def   "ILists(A) == gfp(% X.{} + A*X)"
    1.57 +
    1.58 +  Tall_def   "TALL X.B(X) == Inter({X.EX Y.X=B(Y)})"
    1.59 +  Tex_def     "TEX X.B(X) == Union({X.EX Y.X=B(Y)})"
    1.60 +  Lift_def           "[A] == A Un {bot}"
    1.61 +
    1.62 +  SPLIT_def   "SPLIT(p,B) == Union({A.EX x y.p=<x,y> & A=B(x,y)})"
    1.63 +
    1.64 +end
    1.65 +
    1.66 +
    1.67 +ML
    1.68 +
    1.69 +val parse_translation =
    1.70 +  [("@->", ndependent_tr "Pi"),
    1.71 +   ("@*", ndependent_tr "Sigma")];
    1.72 +
    1.73 +val print_translation =
    1.74 +  [("Pi", dependent_tr' ("@Pi", "@->")),
    1.75 +   ("Sigma", dependent_tr' ("@Sigma", "@*"))];
    1.76 +