src/CTT/ex/typechk.ML
author paulson
Tue Apr 30 11:08:09 1996 +0200 (1996-04-30)
changeset 1702 4aa538e82f76
parent 1459 d12da312eff4
child 3837 d7f033c74b38
permissions -rw-r--r--
Cosmetic re-ordering of declarations
     1 (*  Title:      CTT/ex/typechk
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1991  University of Cambridge
     5   
     6 Easy examples: type checking and type deduction
     7 *)
     8 
     9 writeln"Single-step proofs: verifying that a type is well-formed";
    10 
    11 goal CTT.thy "?A type";
    12 by (resolve_tac form_rls 1);
    13 result(); 
    14 writeln"getting a second solution";
    15 back();
    16 by (resolve_tac form_rls 1);
    17 by (resolve_tac form_rls 1);
    18 result(); 
    19 
    20 goal CTT.thy "PROD z:?A . N + ?B(z) type";
    21 by (resolve_tac form_rls 1);
    22 by (resolve_tac form_rls 1);
    23 by (resolve_tac form_rls 1);
    24 by (resolve_tac form_rls 1);
    25 by (resolve_tac form_rls 1);
    26 uresult(); 
    27 
    28 
    29 writeln"Multi-step proofs: Type inference";
    30 
    31 goal CTT.thy "PROD w:N. N + N type";
    32 by form_tac;
    33 result(); 
    34 
    35 goal CTT.thy "<0, succ(0)> : ?A";
    36 by (intr_tac[]);
    37 result(); 
    38 
    39 goal CTT.thy "PROD w:N . Eq(?A,w,w) type";
    40 by (typechk_tac[]);
    41 result(); 
    42 
    43 goal CTT.thy "PROD x:N . PROD y:N . Eq(?A,x,y) type";
    44 by (typechk_tac[]);
    45 result(); 
    46 
    47 writeln"typechecking an application of fst";
    48 goal CTT.thy "(lam u. split(u, %v w.v)) ` <0, succ(0)> : ?A";
    49 by (typechk_tac[]);
    50 result(); 
    51 
    52 writeln"typechecking the predecessor function";
    53 goal CTT.thy "lam n. rec(n, 0, %x y.x) : ?A";
    54 by (typechk_tac[]);
    55 result(); 
    56 
    57 writeln"typechecking the addition function";
    58 goal CTT.thy "lam n. lam m. rec(n, m, %x y.succ(y)) : ?A";
    59 by (typechk_tac[]);
    60 result(); 
    61 
    62 (*Proofs involving arbitrary types.
    63   For concreteness, every type variable left over is forced to be N*)
    64 val N_tac = TRYALL (rtac NF);
    65 
    66 goal CTT.thy "lam w. <w,w> : ?A";
    67 by (typechk_tac[]);
    68 by N_tac;
    69 result(); 
    70 
    71 goal CTT.thy "lam x. lam y. x : ?A";
    72 by (typechk_tac[]);
    73 by N_tac;
    74 result(); 
    75 
    76 writeln"typechecking fst (as a function object) ";
    77 goal CTT.thy "lam i. split(i, %j k.j) : ?A";
    78 by (typechk_tac[]);
    79 by N_tac;
    80 result(); 
    81 
    82 writeln"Reached end of file.";