src/HOL/Library/NatPair.thy
author paulson
Thu Jul 24 16:37:04 2003 +0200 (2003-07-24)
changeset 14127 40a4768c8e0b
child 14414 3fd75e96145d
permissions -rw-r--r--
new theory NatPair of the injection from nat*nat -> nat
     1 (*  Title:      HOL/Library/NatPair.thy
     2     ID:         $Id$
     3     Author:     Christophe Tabacznyj and Lawrence C Paulson
     4     Copyright   1996  University of Cambridge
     5 *)
     6 
     7 header {*
     8   \title{Pairs of Natural Numbers}
     9   \author{Stefan Richter}
    10 *}
    11 
    12 theory NatPair = Main:
    13 
    14 text{*An injective function from $\mathbf{N}^2$ to
    15   $\mathbf{N}$.  Definition and proofs are from 
    16   Arnold Oberschelp.  Rekursionstheorie.  BI-Wissenschafts-Verlag, 1993
    17   (page 85).  *}
    18 
    19 constdefs 
    20   nat2_to_nat:: "(nat * nat) \<Rightarrow> nat"
    21   "nat2_to_nat pair \<equiv> let (n,m) = pair in (n+m) * Suc (n+m) div 2 + n"
    22 
    23 lemma dvd2_a_x_suc_a: "2 dvd a * (Suc a)" 
    24 proof (cases "2 dvd a") 
    25   case True
    26   thus ?thesis by (rule dvd_mult2)
    27 next
    28   case False 
    29   hence "Suc (a mod 2) = 2" by (simp add: dvd_eq_mod_eq_0)
    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) 
    32   thus ?thesis by (rule dvd_mult)
    33 qed
    34 
    35 lemma 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   hence 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     hence "(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     thus ?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[THEN sym])
    63   also have "\<dots> = ((x+y+2)*Suc(x+y)) div 2" 
    64     by (simp only: add_mult_distrib[THEN sym])
    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 lemma nat2_to_nat_inj: "inj nat2_to_nat"
    74 proof -
    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[THEN sym] 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