38 |
38 |
39 (*Associativity of addition*) |
39 (*Associativity of addition*) |
40 lemma "[| a:N; b:N; c:N |] |
40 lemma "[| a:N; b:N; c:N |] |
41 ==> rec(rec(a, b, %x y. succ(y)), c, %x y. succ(y)) = |
41 ==> rec(rec(a, b, %x y. succ(y)), c, %x y. succ(y)) = |
42 rec(a, rec(b, c, %x y. succ(y)), %x y. succ(y)) : N" |
42 rec(a, rec(b, c, %x y. succ(y)), %x y. succ(y)) : N" |
43 apply (tactic {* NE_tac "a" 1 *}) |
43 apply (tactic {* NE_tac @{context} "a" 1 *}) |
44 apply (tactic "hyp_rew_tac []") |
44 apply (tactic "hyp_rew_tac []") |
45 done |
45 done |
46 |
46 |
47 (*Martin-Lof (1984) page 62: pairing is surjective*) |
47 (*Martin-Lof (1984) page 62: pairing is surjective*) |
48 lemma "p : Sum(A,B) ==> <split(p,%x y. x), split(p,%x y. y)> = p : Sum(A,B)" |
48 lemma "p : Sum(A,B) ==> <split(p,%x y. x), split(p,%x y. y)> = p : Sum(A,B)" |