summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Library/NatPair.thy

author | haftmann |

Mon Jul 07 08:47:17 2008 +0200 (2008-07-07) | |

changeset 27487 | c8a6ce181805 |

parent 27368 | 9f90ac19e32b |

child 28070 | f329e59cebab |

permissions | -rw-r--r-- |

absolute imports of HOL/*.thy theories

1 (* Title: HOL/Library/NatPair.thy

2 ID: $Id$

3 Author: Stefan Richter

4 Copyright 2003 Technische Universitaet Muenchen

5 *)

7 header {* Pairs of Natural Numbers *}

9 theory NatPair

10 imports Plain "~~/src/HOL/Presburger"

11 begin

13 text{*

14 An injective function from @{text "\<nat>\<twosuperior>"} to @{text \<nat>}. Definition

15 and proofs are from \cite[page 85]{Oberschelp:1993}.

16 *}

18 definition

19 nat2_to_nat:: "(nat * nat) \<Rightarrow> nat" where

20 "nat2_to_nat pair = (let (n,m) = pair in (n+m) * Suc (n+m) div 2 + n)"

22 lemma dvd2_a_x_suc_a: "2 dvd a * (Suc a)"

23 proof (cases "2 dvd a")

24 case True

25 then show ?thesis by (rule dvd_mult2)

26 next

27 case False

28 then have "Suc (a mod 2) = 2" by (simp add: dvd_eq_mod_eq_0)

29 then have "Suc a mod 2 = 0" by (simp add: mod_Suc)

30 then have "2 dvd Suc a" by (simp only:dvd_eq_mod_eq_0)

31 then show ?thesis by (rule dvd_mult)

32 qed

34 lemma

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

36 shows nat2_to_nat_help: "u+v \<le> x+y"

37 proof (rule classical)

38 assume "\<not> ?thesis"

39 then have contrapos: "x+y < u+v"

40 by simp

41 have "nat2_to_nat (x,y) < (x+y) * Suc (x+y) div 2 + Suc (x + y)"

42 by (unfold nat2_to_nat_def) (simp add: Let_def)

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

44 by (simp only: div_mult_self1_is_m)

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

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

47 proof -

48 have "2 dvd (x+y)*Suc(x+y)"

49 by (rule dvd2_a_x_suc_a)

50 then have "(x+y)*Suc(x+y) mod 2 = 0"

51 by (simp only: dvd_eq_mod_eq_0)

52 also

53 have "2 * Suc(x+y) mod 2 = 0"

54 by (rule mod_mult_self1_is_0)

55 ultimately have

56 "((x+y)*Suc(x+y) mod 2 + 2 * Suc(x+y) mod 2) div 2 = 0"

57 by simp

58 then show ?thesis

59 by simp

60 qed

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

62 by (rule div_add1_eq [symmetric])

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

64 by (simp only: add_mult_distrib [symmetric])

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

66 by (simp only: mult_le_mono div_le_mono)

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

68 by (unfold nat2_to_nat_def) (simp add: Let_def)

69 finally show ?thesis

70 by (simp only: eq)

71 qed

73 theorem nat2_to_nat_inj: "inj nat2_to_nat"

74 proof -

75 {

76 fix u v x y

77 assume eq1: "nat2_to_nat (u,v) = nat2_to_nat (x,y)"

78 then have "u+v \<le> x+y" by (rule nat2_to_nat_help)

79 also from eq1 [symmetric] have "x+y \<le> u+v"

80 by (rule nat2_to_nat_help)

81 finally have eq2: "u+v = x+y" .

82 with eq1 have ux: "u=x"

83 by (simp add: nat2_to_nat_def Let_def)

84 with eq2 have vy: "v=y" by simp

85 with ux have "(u,v) = (x,y)" by simp

86 }

87 then have "\<And>x y. nat2_to_nat x = nat2_to_nat y \<Longrightarrow> x=y" by fast

88 then show ?thesis unfolding inj_on_def by simp

89 qed

91 end