remove obsolete theory Nat_Int_Bij
authorhuffman
Wed Mar 10 16:00:51 2010 -0800 (2010-03-10)
changeset 357068305122d0350
parent 35705 0e5251adb9cc
child 35707 44936737902d
remove obsolete theory Nat_Int_Bij
src/HOL/IsaMakefile
src/HOL/Library/Nat_Int_Bij.thy
     1.1 --- a/src/HOL/IsaMakefile	Wed Mar 10 15:58:53 2010 -0800
     1.2 +++ b/src/HOL/IsaMakefile	Wed Mar 10 16:00:51 2010 -0800
     1.3 @@ -393,7 +393,7 @@
     1.4    Library/Inner_Product.thy Library/Kleene_Algebra.thy			\
     1.5    Library/Lattice_Algebras.thy Library/Lattice_Syntax.thy		\
     1.6    Library/Library.thy Library/List_Prefix.thy Library/List_Set.thy	\
     1.7 -  Library/State_Monad.thy Library/Nat_Int_Bij.thy Library/Multiset.thy	\
     1.8 +  Library/State_Monad.thy Library/Multiset.thy				\
     1.9    Library/Permutation.thy Library/Quotient_Type.thy			\
    1.10    Library/Quicksort.thy Library/Nat_Infinity.thy Library/Word.thy	\
    1.11    Library/README.html Library/Continuity.thy				\
     2.1 --- a/src/HOL/Library/Nat_Int_Bij.thy	Wed Mar 10 15:58:53 2010 -0800
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,178 +0,0 @@
     2.4 -(*  Title:      HOL/Nat_Int_Bij.thy
     2.5 -    Author:     Stefan Richter, Tobias Nipkow
     2.6 -*)
     2.7 -
     2.8 -header{* Bijections $\mathbb{N}\to\mathbb{N}^2$ and $\mathbb{N}\to\mathbb{Z}$*}
     2.9 -
    2.10 -theory Nat_Int_Bij
    2.11 -imports Main
    2.12 -begin
    2.13 -
    2.14 -subsection{*  A bijection between @{text "\<nat>"} and @{text "\<nat>\<twosuperior>"} *}
    2.15 -
    2.16 -text{* Definition and proofs are from \cite[page 85]{Oberschelp:1993}. *}
    2.17 -
    2.18 -definition nat2_to_nat:: "(nat * nat) \<Rightarrow> nat" where
    2.19 -"nat2_to_nat pair = (let (n,m) = pair in (n+m) * Suc (n+m) div 2 + n)"
    2.20 -definition nat_to_nat2::  "nat \<Rightarrow> (nat * nat)" where
    2.21 -"nat_to_nat2 = inv nat2_to_nat"
    2.22 -
    2.23 -lemma dvd2_a_x_suc_a: "2 dvd a * (Suc a)"
    2.24 -proof (cases "2 dvd a")
    2.25 -  case True
    2.26 -  then show ?thesis by (rule dvd_mult2)
    2.27 -next
    2.28 -  case False
    2.29 -  then have "Suc (a mod 2) = 2" by (simp add: dvd_eq_mod_eq_0)
    2.30 -  then have "Suc a mod 2 = 0" by (simp add: mod_Suc)
    2.31 -  then have "2 dvd Suc a" by (simp only:dvd_eq_mod_eq_0)
    2.32 -  then show ?thesis by (rule dvd_mult)
    2.33 -qed
    2.34 -
    2.35 -lemma
    2.36 -  assumes eq: "nat2_to_nat (u,v) = nat2_to_nat (x,y)"
    2.37 -  shows nat2_to_nat_help: "u+v \<le> x+y"
    2.38 -proof (rule classical)
    2.39 -  assume "\<not> ?thesis"
    2.40 -  then have contrapos: "x+y < u+v"
    2.41 -    by simp
    2.42 -  have "nat2_to_nat (x,y) < (x+y) * Suc (x+y) div 2 + Suc (x + y)"
    2.43 -    by (unfold nat2_to_nat_def) (simp add: Let_def)
    2.44 -  also have "\<dots> = (x+y)*Suc(x+y) div 2 + 2 * Suc(x+y) div 2"
    2.45 -    by (simp only: div_mult_self1_is_m)
    2.46 -  also have "\<dots> = (x+y)*Suc(x+y) div 2 + 2 * Suc(x+y) div 2
    2.47 -    + ((x+y)*Suc(x+y) mod 2 + 2 * Suc(x+y) mod 2) div 2"
    2.48 -  proof -
    2.49 -    have "2 dvd (x+y)*Suc(x+y)"
    2.50 -      by (rule dvd2_a_x_suc_a)
    2.51 -    then have "(x+y)*Suc(x+y) mod 2 = 0"
    2.52 -      by (simp only: dvd_eq_mod_eq_0)
    2.53 -    also
    2.54 -    have "2 * Suc(x+y) mod 2 = 0"
    2.55 -      by (rule mod_mult_self1_is_0)
    2.56 -    ultimately have
    2.57 -      "((x+y)*Suc(x+y) mod 2 + 2 * Suc(x+y) mod 2) div 2 = 0"
    2.58 -      by simp
    2.59 -    then show ?thesis
    2.60 -      by simp
    2.61 -  qed
    2.62 -  also have "\<dots> = ((x+y)*Suc(x+y) + 2*Suc(x+y)) div 2"
    2.63 -    by (rule div_add1_eq [symmetric])
    2.64 -  also have "\<dots> = ((x+y+2)*Suc(x+y)) div 2"
    2.65 -    by (simp only: add_mult_distrib [symmetric])
    2.66 -  also from contrapos have "\<dots> \<le> ((Suc(u+v))*(u+v)) div 2"
    2.67 -    by (simp only: mult_le_mono div_le_mono)
    2.68 -  also have "\<dots> \<le> nat2_to_nat (u,v)"
    2.69 -    by (unfold nat2_to_nat_def) (simp add: Let_def)
    2.70 -  finally show ?thesis
    2.71 -    by (simp only: eq)
    2.72 -qed
    2.73 -
    2.74 -theorem nat2_to_nat_inj: "inj nat2_to_nat"
    2.75 -proof -
    2.76 -  {
    2.77 -    fix u v x y
    2.78 -    assume eq1: "nat2_to_nat (u,v) = nat2_to_nat (x,y)"
    2.79 -    then have "u+v \<le> x+y" by (rule nat2_to_nat_help)
    2.80 -    also from eq1 [symmetric] have "x+y \<le> u+v"
    2.81 -      by (rule nat2_to_nat_help)
    2.82 -    finally have eq2: "u+v = x+y" .
    2.83 -    with eq1 have ux: "u=x"
    2.84 -      by (simp add: nat2_to_nat_def Let_def)
    2.85 -    with eq2 have vy: "v=y" by simp
    2.86 -    with ux have "(u,v) = (x,y)" by simp
    2.87 -  }
    2.88 -  then have "\<And>x y. nat2_to_nat x = nat2_to_nat y \<Longrightarrow> x=y" by fast
    2.89 -  then show ?thesis unfolding inj_on_def by simp
    2.90 -qed
    2.91 -
    2.92 -lemma nat_to_nat2_surj: "surj nat_to_nat2"
    2.93 -by (simp only: nat_to_nat2_def nat2_to_nat_inj inj_imp_surj_inv)
    2.94 -
    2.95 -
    2.96 -lemma gauss_sum_nat_upto: "2 * (\<Sum>i\<le>n::nat. i) = n * (n + 1)"
    2.97 -using gauss_sum[where 'a = nat]
    2.98 -by (simp add:atLeast0AtMost setsum_shift_lb_Suc0_0 numeral_2_eq_2)
    2.99 -
   2.100 -lemma nat2_to_nat_surj: "surj nat2_to_nat"
   2.101 -proof (unfold surj_def)
   2.102 -  {
   2.103 -    fix z::nat 
   2.104 -    def r \<equiv> "Max {r. (\<Sum>i\<le>r. i) \<le> z}" 
   2.105 -    def x \<equiv> "z - (\<Sum>i\<le>r. i)"
   2.106 -
   2.107 -    hence "finite  {r. (\<Sum>i\<le>r. i) \<le> z}"
   2.108 -      by (simp add: lessThan_Suc_atMost[symmetric] lessThan_Suc finite_less_ub)
   2.109 -    also have "0 \<in> {r. (\<Sum>i\<le>r. i) \<le> z}"  by simp
   2.110 -    hence "{r::nat. (\<Sum>i\<le>r. i) \<le> z} \<noteq> {}"  by fast
   2.111 -    ultimately have a: "r \<in> {r. (\<Sum>i\<le>r. i) \<le> z} \<and> (\<forall>s \<in> {r. (\<Sum>i\<le>r. i) \<le> z}. s \<le> r)"
   2.112 -      by (simp add: r_def del:mem_Collect_eq)
   2.113 -    {
   2.114 -      assume "r<x"
   2.115 -      hence "r+1\<le>x"  by simp
   2.116 -      hence "(\<Sum>i\<le>r. i)+(r+1)\<le>z"  using x_def by arith
   2.117 -      hence "(r+1) \<in>  {r. (\<Sum>i\<le>r. i) \<le> z}"  by simp
   2.118 -      with a have "(r+1)\<le>r"  by simp
   2.119 -    }
   2.120 -    hence b: "x\<le>r"  by force
   2.121 -    
   2.122 -    def y \<equiv> "r-x"
   2.123 -    have "2*z=2*(\<Sum>i\<le>r. i)+2*x"  using x_def a by simp arith
   2.124 -    also have "\<dots> = r * (r+1) + 2*x"   using gauss_sum_nat_upto by simp
   2.125 -    also have "\<dots> = (x+y)*(x+y+1)+2*x" using y_def b by simp
   2.126 -    also { have "2 dvd ((x+y)*(x+y+1))" using dvd2_a_x_suc_a by simp }
   2.127 -    hence "\<dots> = 2 * nat2_to_nat(x,y)"
   2.128 -      using nat2_to_nat_def by (simp add: Let_def dvd_mult_div_cancel)
   2.129 -    finally have "z=nat2_to_nat (x, y)"  by simp
   2.130 -  }
   2.131 -  thus "\<forall>y. \<exists>x. y = nat2_to_nat x"  by fast
   2.132 -qed
   2.133 -
   2.134 -lemma nat_to_nat2_inj: "inj nat_to_nat2"
   2.135 -  by (simp add: nat_to_nat2_def surj_imp_inj_inv nat2_to_nat_surj) 
   2.136 -
   2.137 -
   2.138 -subsection{*  A bijection between @{text "\<nat>"} and @{text "\<int>"} *}
   2.139 -
   2.140 -definition nat_to_int_bij :: "nat \<Rightarrow> int" where
   2.141 -"nat_to_int_bij n = (if 2 dvd n then int(n div 2) else -int(Suc n div 2))"
   2.142 -
   2.143 -definition int_to_nat_bij :: "int \<Rightarrow> nat" where
   2.144 -"int_to_nat_bij i = (if 0<=i then 2*nat(i) else 2*nat(-i) - 1)"
   2.145 -
   2.146 -lemma  i2n_n2i_id: "int_to_nat_bij (nat_to_int_bij n) = n"
   2.147 -by (simp add: int_to_nat_bij_def nat_to_int_bij_def) presburger
   2.148 -
   2.149 -lemma n2i_i2n_id: "nat_to_int_bij(int_to_nat_bij i) = i"
   2.150 -proof -
   2.151 -  have "ALL m n::nat. m>0 \<longrightarrow> 2 * m - Suc 0 \<noteq> 2 * n" by presburger
   2.152 -  thus ?thesis
   2.153 -    by(simp add: nat_to_int_bij_def int_to_nat_bij_def, simp add:dvd_def)
   2.154 -qed
   2.155 -
   2.156 -lemma inv_nat_to_int_bij: "inv nat_to_int_bij = int_to_nat_bij"
   2.157 -by (simp add: i2n_n2i_id inv_equality n2i_i2n_id)
   2.158 -
   2.159 -lemma inv_int_to_nat_bij: "inv int_to_nat_bij = nat_to_int_bij"
   2.160 -by (simp add: i2n_n2i_id inv_equality n2i_i2n_id)
   2.161 -
   2.162 -lemma surj_nat_to_int_bij: "surj nat_to_int_bij"
   2.163 -by (blast intro: n2i_i2n_id surjI)
   2.164 -
   2.165 -lemma surj_int_to_nat_bij: "surj int_to_nat_bij"
   2.166 -by (blast intro: i2n_n2i_id surjI)
   2.167 -
   2.168 -lemma inj_nat_to_int_bij: "inj nat_to_int_bij"
   2.169 -by(simp add:inv_int_to_nat_bij[symmetric] surj_int_to_nat_bij surj_imp_inj_inv)
   2.170 -
   2.171 -lemma inj_int_to_nat_bij: "inj int_to_nat_bij"
   2.172 -by(simp add:inv_nat_to_int_bij[symmetric] surj_nat_to_int_bij surj_imp_inj_inv)
   2.173 -
   2.174 -lemma bij_nat_to_int_bij: "bij nat_to_int_bij"
   2.175 -by(simp add:bij_def inj_nat_to_int_bij surj_nat_to_int_bij)
   2.176 -
   2.177 -lemma bij_int_to_nat_bij: "bij int_to_nat_bij"
   2.178 -by(simp add:bij_def inj_int_to_nat_bij surj_int_to_nat_bij)
   2.179 -
   2.180 -
   2.181 -end