19761

1 
(* Title: CTT/ex/Equality.thy


2 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory


3 
Copyright 1991 University of Cambridge


4 
*)


5 

58889

6 
section "Equality reasoning by rewriting"

19761

7 


8 
theory Equality

58974

9 
imports "../CTT"

19761

10 
begin


11 

58977

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

19761

13 
apply (rule EqE)


14 
apply (rule elim_rls, assumption)

58972

15 
apply rew

19761

16 
done


17 

58977

18 
lemma when_eq: "\<lbrakk>A type; B type; p : A+B\<rbrakk> \<Longrightarrow> when(p,inl,inr) = p : A + B"

19761

19 
apply (rule EqE)


20 
apply (rule elim_rls, assumption)

58972

21 
apply rew

19761

22 
done


23 


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

58977

25 
lemma "p:N \<Longrightarrow> rec(p,0, \<lambda>y z. succ(y)) = p : N"

19761

26 
apply (rule EqE)


27 
apply (rule elim_rls, assumption)

58972

28 
apply rew

19761

29 
done


30 


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

58977

32 
lemma "p:N \<Longrightarrow> rec(p,0, \<lambda>y z. succ(z)) = p : N"

19761

33 
apply (rule EqE)


34 
apply (rule elim_rls, assumption)

58972

35 
apply hyp_rew

19761

36 
done


37 


38 
(*Associativity of addition*)

58977

39 
lemma "\<lbrakk>a:N; b:N; c:N\<rbrakk>


40 
\<Longrightarrow> rec(rec(a, b, \<lambda>x y. succ(y)), c, \<lambda>x y. succ(y)) =


41 
rec(a, rec(b, c, \<lambda>x y. succ(y)), \<lambda>x y. succ(y)) : N"

58972

42 
apply (NE a)


43 
apply hyp_rew

19761

44 
done


45 

61391

46 
(*MartinLöf (1984) page 62: pairing is surjective*)

58977

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

19761

48 
apply (rule EqE)


49 
apply (rule elim_rls, assumption)

60770

50 
apply (tactic \<open>DEPTH_SOLVE_1 (rew_tac @{context} [])\<close>) (*!!!!!!!*)

19761

51 
done


52 

61391

53 
lemma "\<lbrakk>a : A; b : B\<rbrakk> \<Longrightarrow> (\<^bold>\<lambda>u. split(u, \<lambda>v w.<w,v>)) ` <a,b> = <b,a> : \<Sum>x:B. A"

58972

54 
apply rew

19761

55 
done


56 


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

61391

58 
lemma "(\<^bold>\<lambda>f. \<^bold>\<lambda>x. f`(f`x)) ` (\<^bold>\<lambda>u. split(u, \<lambda>v w.<w,v>)) =


59 
\<^bold>\<lambda>x. x : \<Prod>x:(\<Sum>y:N. N). (\<Sum>y:N. N)"

19761

60 
apply (rule reduction_rls)


61 
apply (rule_tac [3] intrL_rls)


62 
apply (rule_tac [4] EqE)

58972

63 
apply (erule_tac [4] SumE)

19761

64 
(*order of unifiers is essential here*)

58972

65 
apply rew

19761

66 
done


67 


68 
end
