src/HOL/Library/NatPair.thy
author wenzelm
Thu May 06 14:14:18 2004 +0200 (2004-05-06)
changeset 14706 71590b7733b7
parent 14414 3fd75e96145d
child 15131 c69542757a4d
permissions -rw-r--r--
tuned document;
     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 = Main:
    10 
    11 text{*
    12   An injective function from @{text "\<nat>\<twosuperior>"} to @{text
    13   \<nat>}.  Definition and proofs are from \cite[page
    14   85]{Oberschelp:1993}.
    15 *}
    16 
    17 constdefs
    18   nat2_to_nat:: "(nat * nat) \<Rightarrow> nat"
    19   "nat2_to_nat pair \<equiv> let (n,m) = pair in (n+m) * Suc (n+m) div 2 + n"
    20 
    21 lemma dvd2_a_x_suc_a: "2 dvd a * (Suc a)"
    22 proof (cases "2 dvd a")
    23   case True
    24   thus ?thesis by (rule dvd_mult2)
    25 next
    26   case False
    27   hence "Suc (a mod 2) = 2" by (simp add: dvd_eq_mod_eq_0)
    28   hence "Suc a mod 2 = 0" by (simp add: mod_Suc)
    29   hence "2 dvd Suc a" by (simp only:dvd_eq_mod_eq_0)
    30   thus ?thesis by (rule dvd_mult)
    31 qed
    32 
    33 lemma
    34   assumes eq: "nat2_to_nat (u,v) = nat2_to_nat (x,y)"
    35   shows nat2_to_nat_help: "u+v \<le> x+y"
    36 proof (rule classical)
    37   assume "\<not> ?thesis"
    38   hence contrapos: "x+y < u+v"
    39     by simp
    40   have "nat2_to_nat (x,y) < (x+y) * Suc (x+y) div 2 + Suc (x + y)"
    41     by (unfold nat2_to_nat_def) (simp add: Let_def)
    42   also have "\<dots> = (x+y)*Suc(x+y) div 2 + 2 * Suc(x+y) div 2"
    43     by (simp only: div_mult_self1_is_m)
    44   also have "\<dots> = (x+y)*Suc(x+y) div 2 + 2 * Suc(x+y) div 2
    45     + ((x+y)*Suc(x+y) mod 2 + 2 * Suc(x+y) mod 2) div 2"
    46   proof -
    47     have "2 dvd (x+y)*Suc(x+y)"
    48       by (rule dvd2_a_x_suc_a)
    49     hence "(x+y)*Suc(x+y) mod 2 = 0"
    50       by (simp only: dvd_eq_mod_eq_0)
    51     also
    52     have "2 * Suc(x+y) mod 2 = 0"
    53       by (rule mod_mult_self1_is_0)
    54     ultimately have
    55       "((x+y)*Suc(x+y) mod 2 + 2 * Suc(x+y) mod 2) div 2 = 0"
    56       by simp
    57     thus ?thesis
    58       by simp
    59   qed
    60   also have "\<dots> = ((x+y)*Suc(x+y) + 2*Suc(x+y)) div 2"
    61     by (rule div_add1_eq [symmetric])
    62   also have "\<dots> = ((x+y+2)*Suc(x+y)) div 2"
    63     by (simp only: add_mult_distrib [symmetric])
    64   also from contrapos have "\<dots> \<le> ((Suc(u+v))*(u+v)) div 2"
    65     by (simp only: mult_le_mono div_le_mono)
    66   also have "\<dots> \<le> nat2_to_nat (u,v)"
    67     by (unfold nat2_to_nat_def) (simp add: Let_def)
    68   finally show ?thesis
    69     by (simp only: eq)
    70 qed
    71 
    72 theorem nat2_to_nat_inj: "inj nat2_to_nat"
    73 proof -
    74   {
    75     fix u v x y assume "nat2_to_nat (u,v) = nat2_to_nat (x,y)"
    76     hence "u+v \<le> x+y" by (rule nat2_to_nat_help)
    77     also from prems [symmetric] have "x+y \<le> u+v"
    78       by (rule nat2_to_nat_help)
    79     finally have eq: "u+v = x+y" .
    80     with prems have ux: "u=x"
    81       by (simp add: nat2_to_nat_def Let_def)
    82     with eq have vy: "v=y"
    83       by simp
    84     with ux have "(u,v) = (x,y)"
    85       by simp
    86   }
    87   hence "\<And>x y. nat2_to_nat x = nat2_to_nat y \<Longrightarrow> x=y"
    88     by fast
    89   thus ?thesis
    90     by (unfold inj_on_def) simp
    91 qed
    92 
    93 end