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.";
```