|
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 val split_eq = result(); |
|
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 val when_eq = result(); |
|
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*) |