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