src/HOL/Library/NatPair.thy
 author nipkow Mon Aug 16 14:22:27 2004 +0200 (2004-08-16) changeset 15131 c69542757a4d parent 14706 71590b7733b7 child 15140 322485b816ac permissions -rw-r--r--
```     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
```
```    10 import Main
```
```    11 begin
```
```    12
```
```    13 text{*
```
```    14   An injective function from @{text "\<nat>\<twosuperior>"} to @{text
```
```    15   \<nat>}.  Definition and proofs are from \cite[page
```
```    16   85]{Oberschelp:1993}.
```
```    17 *}
```
```    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
```
```    36   assumes eq: "nat2_to_nat (u,v) = nat2_to_nat (x,y)"
```
```    37   shows nat2_to_nat_help: "u+v \<le> x+y"
```
```    38 proof (rule classical)
```
```    39   assume "\<not> ?thesis"
```
```    40   hence contrapos: "x+y < u+v"
```
```    41     by simp
```
```    42   have "nat2_to_nat (x,y) < (x+y) * Suc (x+y) div 2 + Suc (x + y)"
```
```    43     by (unfold nat2_to_nat_def) (simp add: Let_def)
```
```    44   also have "\<dots> = (x+y)*Suc(x+y) div 2 + 2 * Suc(x+y) div 2"
```
```    45     by (simp only: div_mult_self1_is_m)
```
```    46   also have "\<dots> = (x+y)*Suc(x+y) div 2 + 2 * Suc(x+y) div 2
```
```    47     + ((x+y)*Suc(x+y) mod 2 + 2 * Suc(x+y) mod 2) div 2"
```
```    48   proof -
```
```    49     have "2 dvd (x+y)*Suc(x+y)"
```
```    50       by (rule dvd2_a_x_suc_a)
```
```    51     hence "(x+y)*Suc(x+y) mod 2 = 0"
```
```    52       by (simp only: dvd_eq_mod_eq_0)
```
```    53     also
```
```    54     have "2 * Suc(x+y) mod 2 = 0"
```
```    55       by (rule mod_mult_self1_is_0)
```
```    56     ultimately have
```
```    57       "((x+y)*Suc(x+y) mod 2 + 2 * Suc(x+y) mod 2) div 2 = 0"
```
```    58       by simp
```
```    59     thus ?thesis
```
```    60       by simp
```
```    61   qed
```
```    62   also have "\<dots> = ((x+y)*Suc(x+y) + 2*Suc(x+y)) div 2"
```
```    63     by (rule div_add1_eq [symmetric])
```
```    64   also have "\<dots> = ((x+y+2)*Suc(x+y)) div 2"
```
```    65     by (simp only: add_mult_distrib [symmetric])
```
```    66   also from contrapos have "\<dots> \<le> ((Suc(u+v))*(u+v)) div 2"
```
```    67     by (simp only: mult_le_mono div_le_mono)
```
```    68   also have "\<dots> \<le> nat2_to_nat (u,v)"
```
```    69     by (unfold nat2_to_nat_def) (simp add: Let_def)
```
```    70   finally show ?thesis
```
```    71     by (simp only: eq)
```
```    72 qed
```
```    73
```
```    74 theorem nat2_to_nat_inj: "inj nat2_to_nat"
```
```    75 proof -
```
```    76   {
```
```    77     fix u v x y assume "nat2_to_nat (u,v) = nat2_to_nat (x,y)"
```
```    78     hence "u+v \<le> x+y" by (rule nat2_to_nat_help)
```
```    79     also from prems [symmetric] have "x+y \<le> u+v"
```
```    80       by (rule nat2_to_nat_help)
```
```    81     finally have eq: "u+v = x+y" .
```
```    82     with prems have ux: "u=x"
```
```    83       by (simp add: nat2_to_nat_def Let_def)
```
```    84     with eq have vy: "v=y"
```
```    85       by simp
```
```    86     with ux have "(u,v) = (x,y)"
```
```    87       by simp
```
```    88   }
```
```    89   hence "\<And>x y. nat2_to_nat x = nat2_to_nat y \<Longrightarrow> x=y"
```
```    90     by fast
```
```    91   thus ?thesis
```
```    92     by (unfold inj_on_def) simp
```
```    93 qed
```
```    94
```
```    95 end
```