src/CTT/ex/equal.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/equal
```
```     2     ID:         \$Id\$
```
```     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
```
```     4     Copyright   1991  University of Cambridge
```
```     5
```
```     6 Equality reasoning by rewriting.
```
```     7 *)
```
```     8
```
```     9 val prems =
```
```    10 goal CTT.thy "p : Sum(A,B) ==> split(p,pair) = p : Sum(A,B)";
```
```    11 by (rtac EqE 1);
```
```    12 by (resolve_tac elim_rls 1  THEN  resolve_tac prems 1);
```
```    13 by (rew_tac prems);
```
```    14 qed "split_eq";
```
```    15
```
```    16 val prems =
```
```    17 goal CTT.thy
```
```    18     "[| A type;  B type;  p : A+B |] ==> when(p,inl,inr) = p : A + B";
```
```    19 by (rtac EqE 1);
```
```    20 by (resolve_tac elim_rls 1  THEN  resolve_tac prems 1);
```
```    21 by (rew_tac prems);
```
```    22 qed "when_eq";
```
```    23
```
```    24
```
```    25 (*in the "rec" formulation of addition, 0+n=n *)
```
```    26 val prems =
```
```    27 goal CTT.thy "p:N ==> rec(p,0, %y z.succ(y)) = p : N";
```
```    28 by (rtac EqE 1);
```
```    29 by (resolve_tac elim_rls 1  THEN  resolve_tac prems 1);
```
```    30 by (rew_tac prems);
```
```    31 result();
```
```    32
```
```    33
```
```    34 (*the harder version, n+0=n: recursive, uses induction hypothesis*)
```
```    35 val prems =
```
```    36 goal CTT.thy "p:N ==> rec(p,0, %y z.succ(z)) = p : N";
```
```    37 by (rtac EqE 1);
```
```    38 by (resolve_tac elim_rls 1  THEN  resolve_tac prems 1);
```
```    39 by (hyp_rew_tac prems);
```
```    40 result();
```
```    41
```
```    42
```
```    43 (*Associativity of addition*)
```
```    44 val prems =
```
```    45 goal CTT.thy
```
```    46    "[| a:N;  b:N;  c:N |] ==> rec(rec(a, b, %x y.succ(y)), c, %x y.succ(y)) = \
```
```    47 \                   rec(a, rec(b, c, %x y.succ(y)), %x y.succ(y)) : N";
```
```    48 by (NE_tac "a" 1);
```
```    49 by (hyp_rew_tac prems);
```
```    50 result();
```
```    51
```
```    52
```
```    53 (*Martin-Lof (1984) page 62: pairing is surjective*)
```
```    54 val prems =
```
```    55 goal CTT.thy
```
```    56     "p : Sum(A,B) ==> <split(p,%x y.x), split(p,%x y.y)> = p : Sum(A,B)";
```
```    57 by (rtac EqE 1);
```
```    58 by (resolve_tac elim_rls 1  THEN  resolve_tac prems 1);
```
```    59 by (DEPTH_SOLVE_1 (rew_tac prems));   (*!!!!!!!*)
```
```    60 result();
```
```    61
```
```    62
```
```    63 val prems =
```
```    64 goal CTT.thy "[| a : A;  b : B |] ==> \
```
```    65 \    (lam u. split(u, %v w.<w,v>)) ` <a,b> = <b,a> : SUM x:B.A";
```
```    66 by (rew_tac prems);
```
```    67 result();
```
```    68
```
```    69
```
```    70 (*a contrived, complicated simplication, requires sum-elimination also*)
```
```    71 val prems =
```
```    72 goal CTT.thy
```
```    73    "(lam f. lam x. f`(f`x)) ` (lam u. split(u, %v w.<w,v>)) =  \
```
```    74 \     lam x. x  :  PROD x:(SUM y:N.N). (SUM y:N.N)";
```
```    75 by (resolve_tac reduction_rls 1);
```
```    76 by (resolve_tac intrL_rls 3);
```
```    77 by (rtac EqE 4);
```
```    78 by (rtac SumE 4  THEN  assume_tac 4);
```
```    79 (*order of unifiers is essential here*)
```
```    80 by (rew_tac prems);
```
```    81 result();
```
```    82
```
```    83 writeln"Reached end of file.";
```
```    84 (*28 August 1988: loaded this file in 34 seconds*)
```
```    85 (*2 September 1988: loaded this file in 48 seconds*)
```