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 *)
     6 
     7 header {* Pairs of Natural Numbers *}
     8 
     9 theory NatPair
    10 imports Plain "~~/src/HOL/Presburger"
    11 begin
    12 
    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 *}
    17 
    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)"
    21 
    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
    33 
    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
    72 
    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
    90 
    91 end