src/HOL/Library/NatPair.thy
author haftmann
Tue Dec 18 14:37:00 2007 +0100 (2007-12-18)
changeset 25691 8f8d83af100a
parent 25594 43c718438f9f
child 27368 9f90ac19e32b
permissions -rw-r--r--
switched from PreList to ATP_Linkup
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
wenzelm@14706
     7
header {* Pairs of Natural Numbers *}
paulson@14127
     8
nipkow@15131
     9
theory NatPair
haftmann@25691
    10
imports ATP_Linkup
nipkow@15131
    11
begin
paulson@14127
    12
wenzelm@14706
    13
text{*
wenzelm@19736
    14
  An injective function from @{text "\<nat>\<twosuperior>"} to @{text \<nat>}.  Definition
wenzelm@19736
    15
  and proofs are from \cite[page 85]{Oberschelp:1993}.
wenzelm@14706
    16
*}
paulson@14127
    17
wenzelm@19736
    18
definition
wenzelm@21404
    19
  nat2_to_nat:: "(nat * nat) \<Rightarrow> nat" where
wenzelm@19736
    20
  "nat2_to_nat pair = (let (n,m) = pair in (n+m) * Suc (n+m) div 2 + n)"
paulson@14127
    21
wenzelm@14706
    22
lemma dvd2_a_x_suc_a: "2 dvd a * (Suc a)"
wenzelm@14706
    23
proof (cases "2 dvd a")
paulson@14127
    24
  case True
wenzelm@19736
    25
  then show ?thesis by (rule dvd_mult2)
paulson@14127
    26
next
wenzelm@14706
    27
  case False
wenzelm@19736
    28
  then have "Suc (a mod 2) = 2" by (simp add: dvd_eq_mod_eq_0)
wenzelm@19736
    29
  then have "Suc a mod 2 = 0" by (simp add: mod_Suc)
wenzelm@19736
    30
  then have "2 dvd Suc a" by (simp only:dvd_eq_mod_eq_0)
wenzelm@19736
    31
  then show ?thesis by (rule dvd_mult)
paulson@14127
    32
qed
paulson@14127
    33
wenzelm@14706
    34
lemma
wenzelm@14706
    35
  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"
wenzelm@19736
    39
  then have contrapos: "x+y < u+v"
paulson@14127
    40
    by simp
wenzelm@14706
    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)
wenzelm@14706
    43
  also have "\<dots> = (x+y)*Suc(x+y) div 2 + 2 * Suc(x+y) div 2"
wenzelm@14706
    44
    by (simp only: div_mult_self1_is_m)
wenzelm@14706
    45
  also have "\<dots> = (x+y)*Suc(x+y) div 2 + 2 * Suc(x+y) div 2
wenzelm@14706
    46
    + ((x+y)*Suc(x+y) mod 2 + 2 * Suc(x+y) mod 2) div 2"
paulson@14127
    47
  proof -
wenzelm@14706
    48
    have "2 dvd (x+y)*Suc(x+y)"
paulson@14127
    49
      by (rule dvd2_a_x_suc_a)
wenzelm@19736
    50
    then have "(x+y)*Suc(x+y) mod 2 = 0"
paulson@14127
    51
      by (simp only: dvd_eq_mod_eq_0)
paulson@14127
    52
    also
wenzelm@14706
    53
    have "2 * Suc(x+y) mod 2 = 0"
paulson@14127
    54
      by (rule mod_mult_self1_is_0)
wenzelm@14706
    55
    ultimately have
wenzelm@14706
    56
      "((x+y)*Suc(x+y) mod 2 + 2 * Suc(x+y) mod 2) div 2 = 0"
wenzelm@14706
    57
      by simp
wenzelm@19736
    58
    then show ?thesis
paulson@14127
    59
      by simp
wenzelm@14706
    60
  qed
wenzelm@14706
    61
  also have "\<dots> = ((x+y)*Suc(x+y) + 2*Suc(x+y)) div 2"
wenzelm@14706
    62
    by (rule div_add1_eq [symmetric])
wenzelm@14706
    63
  also have "\<dots> = ((x+y+2)*Suc(x+y)) div 2"
wenzelm@14706
    64
    by (simp only: add_mult_distrib [symmetric])
wenzelm@14706
    65
  also from contrapos have "\<dots> \<le> ((Suc(u+v))*(u+v)) div 2"
wenzelm@14706
    66
    by (simp only: mult_le_mono div_le_mono)
wenzelm@14706
    67
  also have "\<dots> \<le> nat2_to_nat (u,v)"
paulson@14127
    68
    by (unfold nat2_to_nat_def) (simp add: Let_def)
wenzelm@14706
    69
  finally show ?thesis
paulson@14127
    70
    by (simp only: eq)
paulson@14127
    71
qed
paulson@14127
    72
wenzelm@14706
    73
theorem nat2_to_nat_inj: "inj nat2_to_nat"
paulson@14127
    74
proof -
wenzelm@14706
    75
  {
wenzelm@23394
    76
    fix u v x y
wenzelm@23394
    77
    assume eq1: "nat2_to_nat (u,v) = nat2_to_nat (x,y)"
wenzelm@19736
    78
    then have "u+v \<le> x+y" by (rule nat2_to_nat_help)
wenzelm@23394
    79
    also from eq1 [symmetric] have "x+y \<le> u+v"
paulson@14127
    80
      by (rule nat2_to_nat_help)
wenzelm@23394
    81
    finally have eq2: "u+v = x+y" .
wenzelm@23394
    82
    with eq1 have ux: "u=x"
paulson@14127
    83
      by (simp add: nat2_to_nat_def Let_def)
wenzelm@23394
    84
    with eq2 have vy: "v=y" by simp
wenzelm@23394
    85
    with ux have "(u,v) = (x,y)" by simp
paulson@14127
    86
  }
wenzelm@23394
    87
  then have "\<And>x y. nat2_to_nat x = nat2_to_nat y \<Longrightarrow> x=y" by fast
wenzelm@23394
    88
  then show ?thesis unfolding inj_on_def by simp
paulson@14127
    89
qed
paulson@14127
    90
paulson@14127
    91
end