src/HOL/Library/NatPair.thy
 changeset 14706 71590b7733b7 parent 14414 3fd75e96145d child 15131 c69542757a4d
     1.1 --- a/src/HOL/Library/NatPair.thy	Thu May 06 12:43:00 2004 +0200
1.2 +++ b/src/HOL/Library/NatPair.thy	Thu May 06 14:14:18 2004 +0200
1.3 @@ -4,89 +4,89 @@
1.4      Copyright   2003 Technische Universitaet Muenchen
1.5  *)
1.6
1.8 -  \title{Pairs of Natural Numbers}
1.9 -  \author{Stefan Richter}
1.10 -*}
1.11 +header {* Pairs of Natural Numbers *}
1.12
1.13  theory NatPair = Main:
1.14
1.15 -text{*An injective function from $\mathbf{N}^2$ to
1.16 -  $\mathbf{N}$.  Definition and proofs are from
1.17 -  Arnold Oberschelp.  Rekursionstheorie.  BI-Wissenschafts-Verlag, 1993
1.18 -  (page 85).  *}
1.19 +text{*
1.20 +  An injective function from @{text "\<nat>\<twosuperior>"} to @{text
1.21 +  \<nat>}.  Definition and proofs are from \cite[page
1.22 +  85]{Oberschelp:1993}.
1.23 +*}
1.24
1.25 -constdefs
1.26 +constdefs
1.27    nat2_to_nat:: "(nat * nat) \<Rightarrow> nat"
1.28    "nat2_to_nat pair \<equiv> let (n,m) = pair in (n+m) * Suc (n+m) div 2 + n"
1.29
1.30 -lemma dvd2_a_x_suc_a: "2 dvd a * (Suc a)"
1.31 -proof (cases "2 dvd a")
1.32 +lemma dvd2_a_x_suc_a: "2 dvd a * (Suc a)"
1.33 +proof (cases "2 dvd a")
1.34    case True
1.35    thus ?thesis by (rule dvd_mult2)
1.36  next
1.37 -  case False
1.38 +  case False
1.39    hence "Suc (a mod 2) = 2" by (simp add: dvd_eq_mod_eq_0)
1.40 -  hence "Suc a mod 2 = 0" by (simp add: mod_Suc)
1.41 -  hence "2 dvd Suc a" by (simp only:dvd_eq_mod_eq_0)
1.42 +  hence "Suc a mod 2 = 0" by (simp add: mod_Suc)
1.43 +  hence "2 dvd Suc a" by (simp only:dvd_eq_mod_eq_0)
1.44    thus ?thesis by (rule dvd_mult)
1.45  qed
1.46
1.47 -lemma assumes eq: "nat2_to_nat (u,v) = nat2_to_nat (x,y)"
1.48 +lemma
1.49 +  assumes eq: "nat2_to_nat (u,v) = nat2_to_nat (x,y)"
1.50    shows nat2_to_nat_help: "u+v \<le> x+y"
1.51  proof (rule classical)
1.52    assume "\<not> ?thesis"
1.53 -  hence contrapos: "x+y < u+v"
1.54 +  hence contrapos: "x+y < u+v"
1.55      by simp
1.56 -  have "nat2_to_nat (x,y) < (x+y) * Suc (x+y) div 2 + Suc (x + y)"
1.57 +  have "nat2_to_nat (x,y) < (x+y) * Suc (x+y) div 2 + Suc (x + y)"
1.58      by (unfold nat2_to_nat_def) (simp add: Let_def)
1.59 -  also have "\<dots> = (x+y)*Suc(x+y) div 2 + 2 * Suc(x+y) div 2"
1.60 -    by (simp only: div_mult_self1_is_m)
1.61 -  also have "\<dots> = (x+y)*Suc(x+y) div 2 + 2 * Suc(x+y) div 2
1.62 -    + ((x+y)*Suc(x+y) mod 2 + 2 * Suc(x+y) mod 2) div 2"
1.63 +  also have "\<dots> = (x+y)*Suc(x+y) div 2 + 2 * Suc(x+y) div 2"
1.64 +    by (simp only: div_mult_self1_is_m)
1.65 +  also have "\<dots> = (x+y)*Suc(x+y) div 2 + 2 * Suc(x+y) div 2
1.66 +    + ((x+y)*Suc(x+y) mod 2 + 2 * Suc(x+y) mod 2) div 2"
1.67    proof -
1.68 -    have "2 dvd (x+y)*Suc(x+y)"
1.69 +    have "2 dvd (x+y)*Suc(x+y)"
1.70        by (rule dvd2_a_x_suc_a)
1.71 -    hence "(x+y)*Suc(x+y) mod 2 = 0"
1.72 +    hence "(x+y)*Suc(x+y) mod 2 = 0"
1.73        by (simp only: dvd_eq_mod_eq_0)
1.74      also
1.75 -    have "2 * Suc(x+y) mod 2 = 0"
1.76 +    have "2 * Suc(x+y) mod 2 = 0"
1.77        by (rule mod_mult_self1_is_0)
1.78 -    ultimately have
1.79 -      "((x+y)*Suc(x+y) mod 2 + 2 * Suc(x+y) mod 2) div 2 = 0"
1.80 -      by simp
1.81 -    thus ?thesis
1.82 +    ultimately have
1.83 +      "((x+y)*Suc(x+y) mod 2 + 2 * Suc(x+y) mod 2) div 2 = 0"
1.84 +      by simp
1.85 +    thus ?thesis
1.86        by simp
1.87 -  qed
1.88 -  also have "\<dots> = ((x+y)*Suc(x+y) + 2*Suc(x+y)) div 2"
1.89 -    by (rule div_add1_eq[THEN sym])
1.90 -  also have "\<dots> = ((x+y+2)*Suc(x+y)) div 2"
1.91 -    by (simp only: add_mult_distrib[THEN sym])
1.92 -  also from contrapos have "\<dots> \<le> ((Suc(u+v))*(u+v)) div 2"
1.93 -    by (simp only: mult_le_mono div_le_mono)
1.94 -  also have "\<dots> \<le> nat2_to_nat (u,v)"
1.95 +  qed
1.96 +  also have "\<dots> = ((x+y)*Suc(x+y) + 2*Suc(x+y)) div 2"
1.97 +    by (rule div_add1_eq [symmetric])
1.98 +  also have "\<dots> = ((x+y+2)*Suc(x+y)) div 2"
1.99 +    by (simp only: add_mult_distrib [symmetric])
1.100 +  also from contrapos have "\<dots> \<le> ((Suc(u+v))*(u+v)) div 2"
1.101 +    by (simp only: mult_le_mono div_le_mono)
1.102 +  also have "\<dots> \<le> nat2_to_nat (u,v)"
1.103      by (unfold nat2_to_nat_def) (simp add: Let_def)
1.104 -  finally show ?thesis
1.105 +  finally show ?thesis
1.106      by (simp only: eq)
1.107  qed
1.108
1.109 -lemma nat2_to_nat_inj: "inj nat2_to_nat"
1.110 +theorem nat2_to_nat_inj: "inj nat2_to_nat"
1.111  proof -
1.112 -  {fix u v x y assume "nat2_to_nat (u,v) = nat2_to_nat (x,y)"
1.113 +  {
1.114 +    fix u v x y assume "nat2_to_nat (u,v) = nat2_to_nat (x,y)"
1.115      hence "u+v \<le> x+y" by (rule nat2_to_nat_help)
1.116 -    also from prems[THEN sym] have "x+y \<le> u+v"
1.117 +    also from prems [symmetric] have "x+y \<le> u+v"
1.118        by (rule nat2_to_nat_help)
1.119      finally have eq: "u+v = x+y" .
1.120 -    with prems have ux: "u=x"
1.121 +    with prems have ux: "u=x"
1.122        by (simp add: nat2_to_nat_def Let_def)
1.123 -    with eq have vy: "v=y"
1.124 +    with eq have vy: "v=y"
1.125        by simp
1.126 -    with ux have "(u,v) = (x,y)"
1.127 +    with ux have "(u,v) = (x,y)"
1.128        by simp
1.129    }
1.130 -  hence "\<And>x y. nat2_to_nat x = nat2_to_nat y \<Longrightarrow> x=y"
1.131 +  hence "\<And>x y. nat2_to_nat x = nat2_to_nat y \<Longrightarrow> x=y"
1.132      by fast
1.133 -  thus ?thesis
1.134 +  thus ?thesis
1.135      by (unfold inj_on_def) simp
1.136  qed
1.137