src/HOL/Library/NatPair.thy
author nipkow
Thu Feb 26 01:04:39 2004 +0100 (2004-02-26)
changeset 14414 3fd75e96145d
parent 14127 40a4768c8e0b
child 14706 71590b7733b7
permissions -rw-r--r--
corrected authors
paulson@14127
     1
(*  Title:      HOL/Library/NatPair.thy
paulson@14127
     2
    ID:         $Id$
nipkow@14414
     3
    Author:     Stefan Richter
nipkow@14414
     4
    Copyright   2003 Technische Universitaet Muenchen
paulson@14127
     5
*)
paulson@14127
     6
paulson@14127
     7
header {*
paulson@14127
     8
  \title{Pairs of Natural Numbers}
paulson@14127
     9
  \author{Stefan Richter}
paulson@14127
    10
*}
paulson@14127
    11
paulson@14127
    12
theory NatPair = Main:
paulson@14127
    13
paulson@14127
    14
text{*An injective function from $\mathbf{N}^2$ to
paulson@14127
    15
  $\mathbf{N}$.  Definition and proofs are from 
paulson@14127
    16
  Arnold Oberschelp.  Rekursionstheorie.  BI-Wissenschafts-Verlag, 1993
paulson@14127
    17
  (page 85).  *}
paulson@14127
    18
paulson@14127
    19
constdefs 
paulson@14127
    20
  nat2_to_nat:: "(nat * nat) \<Rightarrow> nat"
paulson@14127
    21
  "nat2_to_nat pair \<equiv> let (n,m) = pair in (n+m) * Suc (n+m) div 2 + n"
paulson@14127
    22
paulson@14127
    23
lemma dvd2_a_x_suc_a: "2 dvd a * (Suc a)" 
paulson@14127
    24
proof (cases "2 dvd a") 
paulson@14127
    25
  case True
paulson@14127
    26
  thus ?thesis by (rule dvd_mult2)
paulson@14127
    27
next
paulson@14127
    28
  case False 
paulson@14127
    29
  hence "Suc (a mod 2) = 2" by (simp add: dvd_eq_mod_eq_0)
paulson@14127
    30
  hence "Suc a mod 2 = 0" by (simp add: mod_Suc) 
paulson@14127
    31
  hence "2 dvd Suc a" by (simp only:dvd_eq_mod_eq_0) 
paulson@14127
    32
  thus ?thesis by (rule dvd_mult)
paulson@14127
    33
qed
paulson@14127
    34
paulson@14127
    35
lemma assumes eq: "nat2_to_nat (u,v) = nat2_to_nat (x,y)" 
paulson@14127
    36
  shows nat2_to_nat_help: "u+v \<le> x+y"
paulson@14127
    37
proof (rule classical)
paulson@14127
    38
  assume "\<not> ?thesis"
paulson@14127
    39
  hence contrapos: "x+y < u+v" 
paulson@14127
    40
    by simp
paulson@14127
    41
  have "nat2_to_nat (x,y) < (x+y) * Suc (x+y) div 2 + Suc (x + y)" 
paulson@14127
    42
    by (unfold nat2_to_nat_def) (simp add: Let_def)
paulson@14127
    43
  also have "\<dots> = (x+y)*Suc(x+y) div 2 + 2 * Suc(x+y) div 2" 
paulson@14127
    44
    by (simp only: div_mult_self1_is_m) 
paulson@14127
    45
  also have "\<dots> = (x+y)*Suc(x+y) div 2 + 2 * Suc(x+y) div 2 
paulson@14127
    46
    + ((x+y)*Suc(x+y) mod 2 + 2 * Suc(x+y) mod 2) div 2" 
paulson@14127
    47
  proof -
paulson@14127
    48
    have "2 dvd (x+y)*Suc(x+y)" 
paulson@14127
    49
      by (rule dvd2_a_x_suc_a)
paulson@14127
    50
    hence "(x+y)*Suc(x+y) mod 2 = 0" 
paulson@14127
    51
      by (simp only: dvd_eq_mod_eq_0)
paulson@14127
    52
    also
paulson@14127
    53
    have "2 * Suc(x+y) mod 2 = 0" 
paulson@14127
    54
      by (rule mod_mult_self1_is_0)
paulson@14127
    55
    ultimately have 
paulson@14127
    56
      "((x+y)*Suc(x+y) mod 2 + 2 * Suc(x+y) mod 2) div 2 = 0" 
paulson@14127
    57
      by simp 
paulson@14127
    58
    thus ?thesis 
paulson@14127
    59
      by simp
paulson@14127
    60
  qed 
paulson@14127
    61
  also have "\<dots> = ((x+y)*Suc(x+y) + 2*Suc(x+y)) div 2" 
paulson@14127
    62
    by (rule div_add1_eq[THEN sym])
paulson@14127
    63
  also have "\<dots> = ((x+y+2)*Suc(x+y)) div 2" 
paulson@14127
    64
    by (simp only: add_mult_distrib[THEN sym])
paulson@14127
    65
  also from contrapos have "\<dots> \<le> ((Suc(u+v))*(u+v)) div 2" 
paulson@14127
    66
    by (simp only: mult_le_mono div_le_mono) 
paulson@14127
    67
  also have "\<dots> \<le> nat2_to_nat (u,v)" 
paulson@14127
    68
    by (unfold nat2_to_nat_def) (simp add: Let_def)
paulson@14127
    69
  finally show ?thesis 
paulson@14127
    70
    by (simp only: eq)
paulson@14127
    71
qed
paulson@14127
    72
paulson@14127
    73
lemma nat2_to_nat_inj: "inj nat2_to_nat"
paulson@14127
    74
proof -
paulson@14127
    75
  {fix u v x y assume "nat2_to_nat (u,v) = nat2_to_nat (x,y)"
paulson@14127
    76
    hence "u+v \<le> x+y" by (rule nat2_to_nat_help)
paulson@14127
    77
    also from prems[THEN sym] have "x+y \<le> u+v" 
paulson@14127
    78
      by (rule nat2_to_nat_help)
paulson@14127
    79
    finally have eq: "u+v = x+y" .
paulson@14127
    80
    with prems have ux: "u=x" 
paulson@14127
    81
      by (simp add: nat2_to_nat_def Let_def)
paulson@14127
    82
    with eq have vy: "v=y" 
paulson@14127
    83
      by simp
paulson@14127
    84
    with ux have "(u,v) = (x,y)" 
paulson@14127
    85
      by simp
paulson@14127
    86
  }
paulson@14127
    87
  hence "\<And>x y. nat2_to_nat x = nat2_to_nat y \<Longrightarrow> x=y" 
paulson@14127
    88
    by fast
paulson@14127
    89
  thus ?thesis 
paulson@14127
    90
    by (unfold inj_on_def) simp
paulson@14127
    91
qed
paulson@14127
    92
paulson@14127
    93
end