author  wenzelm 
Sun, 27 Jul 2014 15:40:19 +0200  
changeset 57821  f11f3d7589b1 
parent 35762  af3ff2ba4c54 
child 58889  5b7a9633cfa8 
permissions  rwrr 
19761  1 
(* Title: CTT/ex/Equality.thy 
2 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

3 
Copyright 1991 University of Cambridge 

4 
*) 

5 

6 
header "Equality reasoning by rewriting" 

7 

8 
theory Equality 

9 
imports CTT 

10 
begin 

11 

12 
lemma split_eq: "p : Sum(A,B) ==> split(p,pair) = p : Sum(A,B)" 

13 
apply (rule EqE) 

14 
apply (rule elim_rls, assumption) 

15 
apply (tactic "rew_tac []") 

16 
done 

17 

18 
lemma when_eq: "[ A type; B type; p : A+B ] ==> when(p,inl,inr) = p : A + B" 

19 
apply (rule EqE) 

20 
apply (rule elim_rls, assumption) 

21 
apply (tactic "rew_tac []") 

22 
done 

23 

24 
(*in the "rec" formulation of addition, 0+n=n *) 

25 
lemma "p:N ==> rec(p,0, %y z. succ(y)) = p : N" 

26 
apply (rule EqE) 

27 
apply (rule elim_rls, assumption) 

28 
apply (tactic "rew_tac []") 

29 
done 

30 

31 
(*the harder version, n+0=n: recursive, uses induction hypothesis*) 

32 
lemma "p:N ==> rec(p,0, %y z. succ(z)) = p : N" 

33 
apply (rule EqE) 

34 
apply (rule elim_rls, assumption) 

35 
apply (tactic "hyp_rew_tac []") 

36 
done 

37 

38 
(*Associativity of addition*) 

39 
lemma "[ a:N; b:N; c:N ] 

40 
==> rec(rec(a, b, %x y. succ(y)), c, %x y. succ(y)) = 

41 
rec(a, rec(b, c, %x y. succ(y)), %x y. succ(y)) : N" 

27208
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
19761
diff
changeset

42 
apply (tactic {* NE_tac @{context} "a" 1 *}) 
19761  43 
apply (tactic "hyp_rew_tac []") 
44 
done 

45 

46 
(*MartinLof (1984) page 62: pairing is surjective*) 

47 
lemma "p : Sum(A,B) ==> <split(p,%x y. x), split(p,%x y. y)> = p : Sum(A,B)" 

48 
apply (rule EqE) 

49 
apply (rule elim_rls, assumption) 

50 
apply (tactic {* DEPTH_SOLVE_1 (rew_tac []) *}) (*!!!!!!!*) 

51 
done 

52 

53 
lemma "[ a : A; b : B ] ==> 

54 
(lam u. split(u, %v w.<w,v>)) ` <a,b> = <b,a> : SUM x:B. A" 

55 
apply (tactic "rew_tac []") 

56 
done 

57 

58 
(*a contrived, complicated simplication, requires sumelimination also*) 

59 
lemma "(lam f. lam x. f`(f`x)) ` (lam u. split(u, %v w.<w,v>)) = 

60 
lam x. x : PROD x:(SUM y:N. N). (SUM y:N. N)" 

61 
apply (rule reduction_rls) 

62 
apply (rule_tac [3] intrL_rls) 

63 
apply (rule_tac [4] EqE) 

64 
apply (rule_tac [4] SumE, tactic "assume_tac 4") 

65 
(*order of unifiers is essential here*) 

66 
apply (tactic "rew_tac []") 

67 
done 

68 

69 
end 