new theory NatPair of the injection from nat*nat -> nat
authorpaulson
Thu Jul 24 16:37:04 2003 +0200 (2003-07-24)
changeset 1412740a4768c8e0b
parent 14126 28824746d046
child 14128 fd6d20c2371c
new theory NatPair of the injection from nat*nat -> nat
src/HOL/Library/Library.thy
src/HOL/Library/NatPair.thy
     1.1 --- a/src/HOL/Library/Library.thy	Thu Jul 24 16:36:29 2003 +0200
     1.2 +++ b/src/HOL/Library/Library.thy	Thu Jul 24 16:37:04 2003 +0200
     1.3 @@ -10,6 +10,7 @@
     1.4    Continuity +
     1.5    Multiset +
     1.6    Permutation +
     1.7 +  NatPair +
     1.8    Primes +
     1.9    While_Combinator:
    1.10  end
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/Library/NatPair.thy	Thu Jul 24 16:37:04 2003 +0200
     2.3 @@ -0,0 +1,93 @@
     2.4 +(*  Title:      HOL/Library/NatPair.thy
     2.5 +    ID:         $Id$
     2.6 +    Author:     Christophe Tabacznyj and Lawrence C Paulson
     2.7 +    Copyright   1996  University of Cambridge
     2.8 +*)
     2.9 +
    2.10 +header {*
    2.11 +  \title{Pairs of Natural Numbers}
    2.12 +  \author{Stefan Richter}
    2.13 +*}
    2.14 +
    2.15 +theory NatPair = Main:
    2.16 +
    2.17 +text{*An injective function from $\mathbf{N}^2$ to
    2.18 +  $\mathbf{N}$.  Definition and proofs are from 
    2.19 +  Arnold Oberschelp.  Rekursionstheorie.  BI-Wissenschafts-Verlag, 1993
    2.20 +  (page 85).  *}
    2.21 +
    2.22 +constdefs 
    2.23 +  nat2_to_nat:: "(nat * nat) \<Rightarrow> nat"
    2.24 +  "nat2_to_nat pair \<equiv> let (n,m) = pair in (n+m) * Suc (n+m) div 2 + n"
    2.25 +
    2.26 +lemma dvd2_a_x_suc_a: "2 dvd a * (Suc a)" 
    2.27 +proof (cases "2 dvd a") 
    2.28 +  case True
    2.29 +  thus ?thesis by (rule dvd_mult2)
    2.30 +next
    2.31 +  case False 
    2.32 +  hence "Suc (a mod 2) = 2" by (simp add: dvd_eq_mod_eq_0)
    2.33 +  hence "Suc a mod 2 = 0" by (simp add: mod_Suc) 
    2.34 +  hence "2 dvd Suc a" by (simp only:dvd_eq_mod_eq_0) 
    2.35 +  thus ?thesis by (rule dvd_mult)
    2.36 +qed
    2.37 +
    2.38 +lemma assumes eq: "nat2_to_nat (u,v) = nat2_to_nat (x,y)" 
    2.39 +  shows nat2_to_nat_help: "u+v \<le> x+y"
    2.40 +proof (rule classical)
    2.41 +  assume "\<not> ?thesis"
    2.42 +  hence contrapos: "x+y < u+v" 
    2.43 +    by simp
    2.44 +  have "nat2_to_nat (x,y) < (x+y) * Suc (x+y) div 2 + Suc (x + y)" 
    2.45 +    by (unfold nat2_to_nat_def) (simp add: Let_def)
    2.46 +  also have "\<dots> = (x+y)*Suc(x+y) div 2 + 2 * Suc(x+y) div 2" 
    2.47 +    by (simp only: div_mult_self1_is_m) 
    2.48 +  also have "\<dots> = (x+y)*Suc(x+y) div 2 + 2 * Suc(x+y) div 2 
    2.49 +    + ((x+y)*Suc(x+y) mod 2 + 2 * Suc(x+y) mod 2) div 2" 
    2.50 +  proof -
    2.51 +    have "2 dvd (x+y)*Suc(x+y)" 
    2.52 +      by (rule dvd2_a_x_suc_a)
    2.53 +    hence "(x+y)*Suc(x+y) mod 2 = 0" 
    2.54 +      by (simp only: dvd_eq_mod_eq_0)
    2.55 +    also
    2.56 +    have "2 * Suc(x+y) mod 2 = 0" 
    2.57 +      by (rule mod_mult_self1_is_0)
    2.58 +    ultimately have 
    2.59 +      "((x+y)*Suc(x+y) mod 2 + 2 * Suc(x+y) mod 2) div 2 = 0" 
    2.60 +      by simp 
    2.61 +    thus ?thesis 
    2.62 +      by simp
    2.63 +  qed 
    2.64 +  also have "\<dots> = ((x+y)*Suc(x+y) + 2*Suc(x+y)) div 2" 
    2.65 +    by (rule div_add1_eq[THEN sym])
    2.66 +  also have "\<dots> = ((x+y+2)*Suc(x+y)) div 2" 
    2.67 +    by (simp only: add_mult_distrib[THEN sym])
    2.68 +  also from contrapos have "\<dots> \<le> ((Suc(u+v))*(u+v)) div 2" 
    2.69 +    by (simp only: mult_le_mono div_le_mono) 
    2.70 +  also have "\<dots> \<le> nat2_to_nat (u,v)" 
    2.71 +    by (unfold nat2_to_nat_def) (simp add: Let_def)
    2.72 +  finally show ?thesis 
    2.73 +    by (simp only: eq)
    2.74 +qed
    2.75 +
    2.76 +lemma nat2_to_nat_inj: "inj nat2_to_nat"
    2.77 +proof -
    2.78 +  {fix u v x y assume "nat2_to_nat (u,v) = nat2_to_nat (x,y)"
    2.79 +    hence "u+v \<le> x+y" by (rule nat2_to_nat_help)
    2.80 +    also from prems[THEN sym] have "x+y \<le> u+v" 
    2.81 +      by (rule nat2_to_nat_help)
    2.82 +    finally have eq: "u+v = x+y" .
    2.83 +    with prems have ux: "u=x" 
    2.84 +      by (simp add: nat2_to_nat_def Let_def)
    2.85 +    with eq have vy: "v=y" 
    2.86 +      by simp
    2.87 +    with ux have "(u,v) = (x,y)" 
    2.88 +      by simp
    2.89 +  }
    2.90 +  hence "\<And>x y. nat2_to_nat x = nat2_to_nat y \<Longrightarrow> x=y" 
    2.91 +    by fast
    2.92 +  thus ?thesis 
    2.93 +    by (unfold inj_on_def) simp
    2.94 +qed
    2.95 +
    2.96 +end