(* Title: CTT/ex/Equality.thy
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1991 University of Cambridge
*)
section "Equality reasoning by rewriting"
theory Equality
imports "../CTT"
begin
lemma split_eq: "p : Sum(A,B) \ split(p,pair) = p : Sum(A,B)"
apply (rule EqE)
apply (rule elim_rls, assumption)
apply rew
done
lemma when_eq: "\A type; B type; p : A+B\ \ when(p,inl,inr) = p : A + B"
apply (rule EqE)
apply (rule elim_rls, assumption)
apply rew
done
(*in the "rec" formulation of addition, 0+n=n *)
lemma "p:N \ rec(p,0, \y z. succ(y)) = p : N"
apply (rule EqE)
apply (rule elim_rls, assumption)
apply rew
done
(*the harder version, n+0=n: recursive, uses induction hypothesis*)
lemma "p:N \ rec(p,0, \y z. succ(z)) = p : N"
apply (rule EqE)
apply (rule elim_rls, assumption)
apply hyp_rew
done
(*Associativity of addition*)
lemma "\a:N; b:N; c:N\
\<Longrightarrow> rec(rec(a, b, \<lambda>x y. succ(y)), c, \<lambda>x y. succ(y)) =
rec(a, rec(b, c, \<lambda>x y. succ(y)), \<lambda>x y. succ(y)) : N"
apply (NE a)
apply hyp_rew
done
(*Martin-Löf (1984) page 62: pairing is surjective*)
lemma "p : Sum(A,B) \ x y. x), split(p,\x y. y)> = p : Sum(A,B)"
apply (rule EqE)
apply (rule elim_rls, assumption)
apply (tactic \<open>DEPTH_SOLVE_1 (rew_tac \<^context> [])\<close>) (*!!!!!!!*)
done
lemma "\a : A; b : B\ \ (\<^bold>\u. split(u, \v w.)) ` = : \x:B. A"
apply rew
done
(*a contrived, complicated simplication, requires sum-elimination also*)
lemma "(\<^bold>\f. \<^bold>\x. f`(f`x)) ` (\<^bold>\u. split(u, \v w.)) =
\<^bold>\<lambda>x. x : \<Prod>x:(\<Sum>y:N. N). (\<Sum>y:N. N)"
apply (rule reduction_rls)
apply (rule_tac [3] intrL_rls)
apply (rule_tac [4] EqE)
apply (erule_tac [4] SumE)
(*order of unifiers is essential here*)
apply rew
done
end
¤ Dauer der Verarbeitung: 0.0 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
