(* Title: CTT/ex/Equality.thy Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1991 University of Cambridge "Equality reasoning by rewriting" theory Equalityimports "../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 rewdone 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 rewdone text \<open>in the "rec" formulation of addition, $0+n=n$\<close> lemma "p:N \ rec(p,0, \y z. succ(y)) = p : N" apply (rule EqE)apply (rule elim_rls, assumption)apply rewdone text \<open>the harder version, $n+0=n$: recursive, uses induction hypothesis\<close> lemma "p:N \ rec(p,0, \y z. succ(z)) = p : N" apply (rule EqE)apply (rule elim_rls, assumption)apply hyp_rewdone text \<open>Associativity of addition\<close> lemma "\a:N; b:N; c:N\ \<Longrightarrow> rec(rec(a, b, \<lambda>x y. succ(y)), c, \<lambda>x y. succ(y)) = \<lambda>x y. succ(y)), \<lambda>x y. succ(y)) : N" apply (NE a)apply hyp_rewdone text \<open>Martin-Löf (1984) page 62: pairing is surjective\<close> 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" by rewtext \<open>a contrived, complicated simplication, requires sum-elimination also\<close> 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 rewdone end quality 100%
¤ Dauer der Verarbeitung: 0.11 Sekunden
(vorverarbeitet)
¤ *© Formatika GbR, Deutschland
