diff -r 14b2c22a7e40 -r 71590b7733b7 src/HOL/Library/NatPair.thy --- a/src/HOL/Library/NatPair.thy Thu May 06 12:43:00 2004 +0200 +++ b/src/HOL/Library/NatPair.thy Thu May 06 14:14:18 2004 +0200 @@ -4,89 +4,89 @@ Copyright 2003 Technische Universitaet Muenchen *) -header {* - \title{Pairs of Natural Numbers} - \author{Stefan Richter} -*} +header {* Pairs of Natural Numbers *} theory NatPair = Main: -text{*An injective function from $\mathbf{N}^2$ to - $\mathbf{N}$. Definition and proofs are from - Arnold Oberschelp. Rekursionstheorie. BI-Wissenschafts-Verlag, 1993 - (page 85). *} +text{* + An injective function from @{text "\\"} to @{text + \}. Definition and proofs are from \cite[page + 85]{Oberschelp:1993}. +*} -constdefs +constdefs nat2_to_nat:: "(nat * nat) \ nat" "nat2_to_nat pair \ let (n,m) = pair in (n+m) * Suc (n+m) div 2 + n" -lemma dvd2_a_x_suc_a: "2 dvd a * (Suc a)" -proof (cases "2 dvd a") +lemma dvd2_a_x_suc_a: "2 dvd a * (Suc a)" +proof (cases "2 dvd a") case True thus ?thesis by (rule dvd_mult2) next - case False + case False hence "Suc (a mod 2) = 2" by (simp add: dvd_eq_mod_eq_0) - hence "Suc a mod 2 = 0" by (simp add: mod_Suc) - hence "2 dvd Suc a" by (simp only:dvd_eq_mod_eq_0) + hence "Suc a mod 2 = 0" by (simp add: mod_Suc) + hence "2 dvd Suc a" by (simp only:dvd_eq_mod_eq_0) thus ?thesis by (rule dvd_mult) qed -lemma assumes eq: "nat2_to_nat (u,v) = nat2_to_nat (x,y)" +lemma + assumes eq: "nat2_to_nat (u,v) = nat2_to_nat (x,y)" shows nat2_to_nat_help: "u+v \ x+y" proof (rule classical) assume "\ ?thesis" - hence contrapos: "x+y < u+v" + hence contrapos: "x+y < u+v" by simp - have "nat2_to_nat (x,y) < (x+y) * Suc (x+y) div 2 + Suc (x + y)" + have "nat2_to_nat (x,y) < (x+y) * Suc (x+y) div 2 + Suc (x + y)" by (unfold nat2_to_nat_def) (simp add: Let_def) - also have "\ = (x+y)*Suc(x+y) div 2 + 2 * Suc(x+y) div 2" - by (simp only: div_mult_self1_is_m) - also have "\ = (x+y)*Suc(x+y) div 2 + 2 * Suc(x+y) div 2 - + ((x+y)*Suc(x+y) mod 2 + 2 * Suc(x+y) mod 2) div 2" + also have "\ = (x+y)*Suc(x+y) div 2 + 2 * Suc(x+y) div 2" + by (simp only: div_mult_self1_is_m) + also have "\ = (x+y)*Suc(x+y) div 2 + 2 * Suc(x+y) div 2 + + ((x+y)*Suc(x+y) mod 2 + 2 * Suc(x+y) mod 2) div 2" proof - - have "2 dvd (x+y)*Suc(x+y)" + have "2 dvd (x+y)*Suc(x+y)" by (rule dvd2_a_x_suc_a) - hence "(x+y)*Suc(x+y) mod 2 = 0" + hence "(x+y)*Suc(x+y) mod 2 = 0" by (simp only: dvd_eq_mod_eq_0) also - have "2 * Suc(x+y) mod 2 = 0" + have "2 * Suc(x+y) mod 2 = 0" by (rule mod_mult_self1_is_0) - ultimately have - "((x+y)*Suc(x+y) mod 2 + 2 * Suc(x+y) mod 2) div 2 = 0" - by simp - thus ?thesis + ultimately have + "((x+y)*Suc(x+y) mod 2 + 2 * Suc(x+y) mod 2) div 2 = 0" + by simp + thus ?thesis by simp - qed - also have "\ = ((x+y)*Suc(x+y) + 2*Suc(x+y)) div 2" - by (rule div_add1_eq[THEN sym]) - also have "\ = ((x+y+2)*Suc(x+y)) div 2" - by (simp only: add_mult_distrib[THEN sym]) - also from contrapos have "\ \ ((Suc(u+v))*(u+v)) div 2" - by (simp only: mult_le_mono div_le_mono) - also have "\ \ nat2_to_nat (u,v)" + qed + also have "\ = ((x+y)*Suc(x+y) + 2*Suc(x+y)) div 2" + by (rule div_add1_eq [symmetric]) + also have "\ = ((x+y+2)*Suc(x+y)) div 2" + by (simp only: add_mult_distrib [symmetric]) + also from contrapos have "\ \ ((Suc(u+v))*(u+v)) div 2" + by (simp only: mult_le_mono div_le_mono) + also have "\ \ nat2_to_nat (u,v)" by (unfold nat2_to_nat_def) (simp add: Let_def) - finally show ?thesis + finally show ?thesis by (simp only: eq) qed -lemma nat2_to_nat_inj: "inj nat2_to_nat" +theorem nat2_to_nat_inj: "inj nat2_to_nat" proof - - {fix u v x y assume "nat2_to_nat (u,v) = nat2_to_nat (x,y)" + { + fix u v x y assume "nat2_to_nat (u,v) = nat2_to_nat (x,y)" hence "u+v \ x+y" by (rule nat2_to_nat_help) - also from prems[THEN sym] have "x+y \ u+v" + also from prems [symmetric] have "x+y \ u+v" by (rule nat2_to_nat_help) finally have eq: "u+v = x+y" . - with prems have ux: "u=x" + with prems have ux: "u=x" by (simp add: nat2_to_nat_def Let_def) - with eq have vy: "v=y" + with eq have vy: "v=y" by simp - with ux have "(u,v) = (x,y)" + with ux have "(u,v) = (x,y)" by simp } - hence "\x y. nat2_to_nat x = nat2_to_nat y \ x=y" + hence "\x y. nat2_to_nat x = nat2_to_nat y \ x=y" by fast - thus ?thesis + thus ?thesis by (unfold inj_on_def) simp qed