author  nipkow 
Wed, 18 Aug 2004 11:09:40 +0200  
changeset 15140  322485b816ac 
parent 15131  c69542757a4d 
child 19736  d8d0f8f51d69 
permissions  rwrr 
14127
40a4768c8e0b
new theory NatPair of the injection from nat*nat > nat
paulson
parents:
diff
changeset

1 
(* Title: HOL/Library/NatPair.thy 
40a4768c8e0b
new theory NatPair of the injection from nat*nat > nat
paulson
parents:
diff
changeset

2 
ID: $Id$ 
14414  3 
Author: Stefan Richter 
4 
Copyright 2003 Technische Universitaet Muenchen 

14127
40a4768c8e0b
new theory NatPair of the injection from nat*nat > nat
paulson
parents:
diff
changeset

5 
*) 
40a4768c8e0b
new theory NatPair of the injection from nat*nat > nat
paulson
parents:
diff
changeset

6 

14706  7 
header {* Pairs of Natural Numbers *} 
14127
40a4768c8e0b
new theory NatPair of the injection from nat*nat > nat
paulson
parents:
diff
changeset

8 

15131  9 
theory NatPair 
15140  10 
imports Main 
15131  11 
begin 
14127
40a4768c8e0b
new theory NatPair of the injection from nat*nat > nat
paulson
parents:
diff
changeset

12 

14706  13 
text{* 
14 
An injective function from @{text "\<nat>\<twosuperior>"} to @{text 

15 
\<nat>}. Definition and proofs are from \cite[page 

16 
85]{Oberschelp:1993}. 

17 
*} 

14127
40a4768c8e0b
new theory NatPair of the injection from nat*nat > nat
paulson
parents:
diff
changeset

18 

14706  19 
constdefs 
14127
40a4768c8e0b
new theory NatPair of the injection from nat*nat > nat
paulson
parents:
diff
changeset

20 
nat2_to_nat:: "(nat * nat) \<Rightarrow> nat" 
40a4768c8e0b
new theory NatPair of the injection from nat*nat > nat
paulson
parents:
diff
changeset

21 
"nat2_to_nat pair \<equiv> let (n,m) = pair in (n+m) * Suc (n+m) div 2 + n" 
40a4768c8e0b
new theory NatPair of the injection from nat*nat > nat
paulson
parents:
diff
changeset

22 

14706  23 
lemma dvd2_a_x_suc_a: "2 dvd a * (Suc a)" 
24 
proof (cases "2 dvd a") 

14127
40a4768c8e0b
new theory NatPair of the injection from nat*nat > nat
paulson
parents:
diff
changeset

25 
case True 
40a4768c8e0b
new theory NatPair of the injection from nat*nat > nat
paulson
parents:
diff
changeset

26 
thus ?thesis by (rule dvd_mult2) 
40a4768c8e0b
new theory NatPair of the injection from nat*nat > nat
paulson
parents:
diff
changeset

27 
next 
14706  28 
case False 
14127
40a4768c8e0b
new theory NatPair of the injection from nat*nat > nat
paulson
parents:
diff
changeset

29 
hence "Suc (a mod 2) = 2" by (simp add: dvd_eq_mod_eq_0) 
14706  30 
hence "Suc a mod 2 = 0" by (simp add: mod_Suc) 
31 
hence "2 dvd Suc a" by (simp only:dvd_eq_mod_eq_0) 

14127
40a4768c8e0b
new theory NatPair of the injection from nat*nat > nat
paulson
parents:
diff
changeset

32 
thus ?thesis by (rule dvd_mult) 
40a4768c8e0b
new theory NatPair of the injection from nat*nat > nat
paulson
parents:
diff
changeset

33 
qed 
40a4768c8e0b
new theory NatPair of the injection from nat*nat > nat
paulson
parents:
diff
changeset

34 

14706  35 
lemma 
36 
assumes eq: "nat2_to_nat (u,v) = nat2_to_nat (x,y)" 

14127
40a4768c8e0b
new theory NatPair of the injection from nat*nat > nat
paulson
parents:
diff
changeset

37 
shows nat2_to_nat_help: "u+v \<le> x+y" 
40a4768c8e0b
new theory NatPair of the injection from nat*nat > nat
paulson
parents:
diff
changeset

38 
proof (rule classical) 
40a4768c8e0b
new theory NatPair of the injection from nat*nat > nat
paulson
parents:
diff
changeset

39 
assume "\<not> ?thesis" 
14706  40 
hence contrapos: "x+y < u+v" 
14127
40a4768c8e0b
new theory NatPair of the injection from nat*nat > nat
paulson
parents:
diff
changeset

41 
by simp 
14706  42 
have "nat2_to_nat (x,y) < (x+y) * Suc (x+y) div 2 + Suc (x + y)" 
14127
40a4768c8e0b
new theory NatPair of the injection from nat*nat > nat
paulson
parents:
diff
changeset

43 
by (unfold nat2_to_nat_def) (simp add: Let_def) 
14706  44 
also have "\<dots> = (x+y)*Suc(x+y) div 2 + 2 * Suc(x+y) div 2" 
45 
by (simp only: div_mult_self1_is_m) 

46 
also have "\<dots> = (x+y)*Suc(x+y) div 2 + 2 * Suc(x+y) div 2 

47 
+ ((x+y)*Suc(x+y) mod 2 + 2 * Suc(x+y) mod 2) div 2" 

14127
40a4768c8e0b
new theory NatPair of the injection from nat*nat > nat
paulson
parents:
diff
changeset

48 
proof  
14706  49 
have "2 dvd (x+y)*Suc(x+y)" 
14127
40a4768c8e0b
new theory NatPair of the injection from nat*nat > nat
paulson
parents:
diff
changeset

50 
by (rule dvd2_a_x_suc_a) 
14706  51 
hence "(x+y)*Suc(x+y) mod 2 = 0" 
14127
40a4768c8e0b
new theory NatPair of the injection from nat*nat > nat
paulson
parents:
diff
changeset

52 
by (simp only: dvd_eq_mod_eq_0) 
40a4768c8e0b
new theory NatPair of the injection from nat*nat > nat
paulson
parents:
diff
changeset

53 
also 
14706  54 
have "2 * Suc(x+y) mod 2 = 0" 
14127
40a4768c8e0b
new theory NatPair of the injection from nat*nat > nat
paulson
parents:
diff
changeset

55 
by (rule mod_mult_self1_is_0) 
14706  56 
ultimately have 
57 
"((x+y)*Suc(x+y) mod 2 + 2 * Suc(x+y) mod 2) div 2 = 0" 

58 
by simp 

59 
thus ?thesis 

14127
40a4768c8e0b
new theory NatPair of the injection from nat*nat > nat
paulson
parents:
diff
changeset

60 
by simp 
14706  61 
qed 
62 
also have "\<dots> = ((x+y)*Suc(x+y) + 2*Suc(x+y)) div 2" 

63 
by (rule div_add1_eq [symmetric]) 

64 
also have "\<dots> = ((x+y+2)*Suc(x+y)) div 2" 

65 
by (simp only: add_mult_distrib [symmetric]) 

66 
also from contrapos have "\<dots> \<le> ((Suc(u+v))*(u+v)) div 2" 

67 
by (simp only: mult_le_mono div_le_mono) 

68 
also have "\<dots> \<le> nat2_to_nat (u,v)" 

14127
40a4768c8e0b
new theory NatPair of the injection from nat*nat > nat
paulson
parents:
diff
changeset

69 
by (unfold nat2_to_nat_def) (simp add: Let_def) 
14706  70 
finally show ?thesis 
14127
40a4768c8e0b
new theory NatPair of the injection from nat*nat > nat
paulson
parents:
diff
changeset

71 
by (simp only: eq) 
40a4768c8e0b
new theory NatPair of the injection from nat*nat > nat
paulson
parents:
diff
changeset

72 
qed 
40a4768c8e0b
new theory NatPair of the injection from nat*nat > nat
paulson
parents:
diff
changeset

73 

14706  74 
theorem nat2_to_nat_inj: "inj nat2_to_nat" 
14127
40a4768c8e0b
new theory NatPair of the injection from nat*nat > nat
paulson
parents:
diff
changeset

75 
proof  
14706  76 
{ 
77 
fix u v x y assume "nat2_to_nat (u,v) = nat2_to_nat (x,y)" 

14127
40a4768c8e0b
new theory NatPair of the injection from nat*nat > nat
paulson
parents:
diff
changeset

78 
hence "u+v \<le> x+y" by (rule nat2_to_nat_help) 
14706  79 
also from prems [symmetric] have "x+y \<le> u+v" 
14127
40a4768c8e0b
new theory NatPair of the injection from nat*nat > nat
paulson
parents:
diff
changeset

80 
by (rule nat2_to_nat_help) 
40a4768c8e0b
new theory NatPair of the injection from nat*nat > nat
paulson
parents:
diff
changeset

81 
finally have eq: "u+v = x+y" . 
14706  82 
with prems have ux: "u=x" 
14127
40a4768c8e0b
new theory NatPair of the injection from nat*nat > nat
paulson
parents:
diff
changeset

83 
by (simp add: nat2_to_nat_def Let_def) 
14706  84 
with eq have vy: "v=y" 
14127
40a4768c8e0b
new theory NatPair of the injection from nat*nat > nat
paulson
parents:
diff
changeset

85 
by simp 
14706  86 
with ux have "(u,v) = (x,y)" 
14127
40a4768c8e0b
new theory NatPair of the injection from nat*nat > nat
paulson
parents:
diff
changeset

87 
by simp 
40a4768c8e0b
new theory NatPair of the injection from nat*nat > nat
paulson
parents:
diff
changeset

88 
} 
14706  89 
hence "\<And>x y. nat2_to_nat x = nat2_to_nat y \<Longrightarrow> x=y" 
14127
40a4768c8e0b
new theory NatPair of the injection from nat*nat > nat
paulson
parents:
diff
changeset

90 
by fast 
14706  91 
thus ?thesis 
14127
40a4768c8e0b
new theory NatPair of the injection from nat*nat > nat
paulson
parents:
diff
changeset

92 
by (unfold inj_on_def) simp 
40a4768c8e0b
new theory NatPair of the injection from nat*nat > nat
paulson
parents:
diff
changeset

93 
qed 
40a4768c8e0b
new theory NatPair of the injection from nat*nat > nat
paulson
parents:
diff
changeset

94 

40a4768c8e0b
new theory NatPair of the injection from nat*nat > nat
paulson
parents:
diff
changeset

95 
end 