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