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*)