19761

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


2 
ID: $Id$


3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory


4 
Copyright 1991 University of Cambridge


5 
*)


6 


7 
header "Equality reasoning by rewriting"


8 


9 
theory Equality


10 
imports CTT


11 
begin


12 


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


14 
apply (rule EqE)


15 
apply (rule elim_rls, assumption)


16 
apply (tactic "rew_tac []")


17 
done


18 


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


20 
apply (rule EqE)


21 
apply (rule elim_rls, assumption)


22 
apply (tactic "rew_tac []")


23 
done


24 


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


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


27 
apply (rule EqE)


28 
apply (rule elim_rls, assumption)


29 
apply (tactic "rew_tac []")


30 
done


31 


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


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


34 
apply (rule EqE)


35 
apply (rule elim_rls, assumption)


36 
apply (tactic "hyp_rew_tac []")


37 
done


38 


39 
(*Associativity of addition*)


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


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"


43 
apply (tactic {* NE_tac "a" 1 *})


44 
apply (tactic "hyp_rew_tac []")


45 
done


46 


47 
(*MartinLof (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)"


49 
apply (rule EqE)


50 
apply (rule elim_rls, assumption)


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


52 
done


53 


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


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


56 
apply (tactic "rew_tac []")


57 
done


58 


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


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


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


62 
apply (rule reduction_rls)


63 
apply (rule_tac [3] intrL_rls)


64 
apply (rule_tac [4] EqE)


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


66 
(*order of unifiers is essential here*)


67 
apply (tactic "rew_tac []")


68 
done


69 


70 
end
