Moved Nat_Int_Bij into Library
authornipkow
Fri Feb 13 09:54:47 2009 +0100 (2009-02-13)
changeset 29888ab97183f1694
parent 29886 b8a6b9c56fdd
child 29889 95e6eb9044fe
Moved Nat_Int_Bij into Library
src/HOL/Auth/TLS.thy
src/HOL/IsaMakefile
src/HOL/Library/Nat_Int_Bij.thy
src/HOL/Main.thy
src/HOL/Nat_Int_Bij.thy
src/HOL/SET-Protocol/MessageSET.thy
     1.1 --- a/src/HOL/Auth/TLS.thy	Thu Feb 12 21:24:14 2009 -0800
     1.2 +++ b/src/HOL/Auth/TLS.thy	Fri Feb 13 09:54:47 2009 +0100
     1.3 @@ -41,7 +41,7 @@
     1.4  
     1.5  header{*The TLS Protocol: Transport Layer Security*}
     1.6  
     1.7 -theory TLS imports Public begin
     1.8 +theory TLS imports Public Nat_Int_Bij begin
     1.9  
    1.10  constdefs
    1.11    certificate      :: "[agent,key] => msg"
     2.1 --- a/src/HOL/IsaMakefile	Thu Feb 12 21:24:14 2009 -0800
     2.2 +++ b/src/HOL/IsaMakefile	Fri Feb 13 09:54:47 2009 +0100
     2.3 @@ -216,7 +216,6 @@
     2.4    Main.thy \
     2.5    Map.thy \
     2.6    NatBin.thy \
     2.7 -  Nat_Int_Bij.thy \
     2.8    Presburger.thy \
     2.9    Recdef.thy \
    2.10    Relation_Power.thy \
    2.11 @@ -318,7 +317,7 @@
    2.12    Library/Finite_Cartesian_Product.thy \
    2.13    Library/Fundamental_Theorem_Algebra.thy \
    2.14    Library/Library.thy Library/List_Prefix.thy Library/State_Monad.thy	\
    2.15 -  Library/Multiset.thy Library/Permutation.thy	\
    2.16 +  Library/Nat_Int_Bij.thy Library/Multiset.thy Library/Permutation.thy	\
    2.17    Library/Primes.thy Library/Pocklington.thy Library/Quotient.thy	\
    2.18    Library/Quicksort.thy Library/Nat_Infinity.thy Library/Word.thy	\
    2.19    Library/README.html Library/Continuity.thy Library/Order_Relation.thy \
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/Library/Nat_Int_Bij.thy	Fri Feb 13 09:54:47 2009 +0100
     3.3 @@ -0,0 +1,170 @@
     3.4 +(*  Title:      HOL/Nat_Int_Bij.thy
     3.5 +    ID:         $Id$
     3.6 +    Author:     Stefan Richter, Tobias Nipkow
     3.7 +*)
     3.8 +
     3.9 +header{* Bijections $\mathbb{N}\to\mathbb{N}^2$ and $\mathbb{N}\to\mathbb{Z}$*}
    3.10 +
    3.11 +theory Nat_Int_Bij
    3.12 +imports Hilbert_Choice Presburger
    3.13 +begin
    3.14 +
    3.15 +subsection{*  A bijection between @{text "\<nat>"} and @{text "\<nat>\<twosuperior>"} *}
    3.16 +
    3.17 +text{* Definition and proofs are from \cite[page 85]{Oberschelp:1993}. *}
    3.18 +
    3.19 +definition nat2_to_nat:: "(nat * nat) \<Rightarrow> nat" where
    3.20 +"nat2_to_nat pair = (let (n,m) = pair in (n+m) * Suc (n+m) div 2 + n)"
    3.21 +definition nat_to_nat2::  "nat \<Rightarrow> (nat * nat)" where
    3.22 +"nat_to_nat2 = inv nat2_to_nat"
    3.23 +
    3.24 +lemma dvd2_a_x_suc_a: "2 dvd a * (Suc a)"
    3.25 +proof (cases "2 dvd a")
    3.26 +  case True
    3.27 +  then show ?thesis by (rule dvd_mult2)
    3.28 +next
    3.29 +  case False
    3.30 +  then have "Suc (a mod 2) = 2" by (simp add: dvd_eq_mod_eq_0)
    3.31 +  then have "Suc a mod 2 = 0" by (simp add: mod_Suc)
    3.32 +  then have "2 dvd Suc a" by (simp only:dvd_eq_mod_eq_0)
    3.33 +  then show ?thesis by (rule dvd_mult)
    3.34 +qed
    3.35 +
    3.36 +lemma
    3.37 +  assumes eq: "nat2_to_nat (u,v) = nat2_to_nat (x,y)"
    3.38 +  shows nat2_to_nat_help: "u+v \<le> x+y"
    3.39 +proof (rule classical)
    3.40 +  assume "\<not> ?thesis"
    3.41 +  then have contrapos: "x+y < u+v"
    3.42 +    by simp
    3.43 +  have "nat2_to_nat (x,y) < (x+y) * Suc (x+y) div 2 + Suc (x + y)"
    3.44 +    by (unfold nat2_to_nat_def) (simp add: Let_def)
    3.45 +  also have "\<dots> = (x+y)*Suc(x+y) div 2 + 2 * Suc(x+y) div 2"
    3.46 +    by (simp only: div_mult_self1_is_m)
    3.47 +  also have "\<dots> = (x+y)*Suc(x+y) div 2 + 2 * Suc(x+y) div 2
    3.48 +    + ((x+y)*Suc(x+y) mod 2 + 2 * Suc(x+y) mod 2) div 2"
    3.49 +  proof -
    3.50 +    have "2 dvd (x+y)*Suc(x+y)"
    3.51 +      by (rule dvd2_a_x_suc_a)
    3.52 +    then have "(x+y)*Suc(x+y) mod 2 = 0"
    3.53 +      by (simp only: dvd_eq_mod_eq_0)
    3.54 +    also
    3.55 +    have "2 * Suc(x+y) mod 2 = 0"
    3.56 +      by (rule mod_mult_self1_is_0)
    3.57 +    ultimately have
    3.58 +      "((x+y)*Suc(x+y) mod 2 + 2 * Suc(x+y) mod 2) div 2 = 0"
    3.59 +      by simp
    3.60 +    then show ?thesis
    3.61 +      by simp
    3.62 +  qed
    3.63 +  also have "\<dots> = ((x+y)*Suc(x+y) + 2*Suc(x+y)) div 2"
    3.64 +    by (rule div_add1_eq [symmetric])
    3.65 +  also have "\<dots> = ((x+y+2)*Suc(x+y)) div 2"
    3.66 +    by (simp only: add_mult_distrib [symmetric])
    3.67 +  also from contrapos have "\<dots> \<le> ((Suc(u+v))*(u+v)) div 2"
    3.68 +    by (simp only: mult_le_mono div_le_mono)
    3.69 +  also have "\<dots> \<le> nat2_to_nat (u,v)"
    3.70 +    by (unfold nat2_to_nat_def) (simp add: Let_def)
    3.71 +  finally show ?thesis
    3.72 +    by (simp only: eq)
    3.73 +qed
    3.74 +
    3.75 +theorem nat2_to_nat_inj: "inj nat2_to_nat"
    3.76 +proof -
    3.77 +  {
    3.78 +    fix u v x y
    3.79 +    assume eq1: "nat2_to_nat (u,v) = nat2_to_nat (x,y)"
    3.80 +    then have "u+v \<le> x+y" by (rule nat2_to_nat_help)
    3.81 +    also from eq1 [symmetric] have "x+y \<le> u+v"
    3.82 +      by (rule nat2_to_nat_help)
    3.83 +    finally have eq2: "u+v = x+y" .
    3.84 +    with eq1 have ux: "u=x"
    3.85 +      by (simp add: nat2_to_nat_def Let_def)
    3.86 +    with eq2 have vy: "v=y" by simp
    3.87 +    with ux have "(u,v) = (x,y)" by simp
    3.88 +  }
    3.89 +  then have "\<And>x y. nat2_to_nat x = nat2_to_nat y \<Longrightarrow> x=y" by fast
    3.90 +  then show ?thesis unfolding inj_on_def by simp
    3.91 +qed
    3.92 +
    3.93 +lemma nat_to_nat2_surj: "surj nat_to_nat2"
    3.94 +by (simp only: nat_to_nat2_def nat2_to_nat_inj inj_imp_surj_inv)
    3.95 +
    3.96 +
    3.97 +lemma gauss_sum_nat_upto: "2 * (\<Sum>i\<le>n::nat. i) = n * (n + 1)"
    3.98 +using gauss_sum[where 'a = nat]
    3.99 +by (simp add:atLeast0AtMost setsum_shift_lb_Suc0_0 numeral_2_eq_2)
   3.100 +
   3.101 +lemma nat2_to_nat_surj: "surj nat2_to_nat"
   3.102 +proof (unfold surj_def)
   3.103 +  {
   3.104 +    fix z::nat 
   3.105 +    def r \<equiv> "Max {r. (\<Sum>i\<le>r. i) \<le> z}" 
   3.106 +    def x \<equiv> "z - (\<Sum>i\<le>r. i)"
   3.107 +
   3.108 +    hence "finite  {r. (\<Sum>i\<le>r. i) \<le> z}"
   3.109 +      by (simp add: lessThan_Suc_atMost[symmetric] lessThan_Suc finite_less_ub)
   3.110 +    also have "0 \<in> {r. (\<Sum>i\<le>r. i) \<le> z}"  by simp
   3.111 +    hence "{r::nat. (\<Sum>i\<le>r. i) \<le> z} \<noteq> {}"  by fast
   3.112 +    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)"
   3.113 +      by (simp add: r_def del:mem_Collect_eq)
   3.114 +    {
   3.115 +      assume "r<x"
   3.116 +      hence "r+1\<le>x"  by simp
   3.117 +      hence "(\<Sum>i\<le>r. i)+(r+1)\<le>z"  using x_def by arith
   3.118 +      hence "(r+1) \<in>  {r. (\<Sum>i\<le>r. i) \<le> z}"  by simp
   3.119 +      with a have "(r+1)\<le>r"  by simp
   3.120 +    }
   3.121 +    hence b: "x\<le>r"  by force
   3.122 +    
   3.123 +    def y \<equiv> "r-x"
   3.124 +    have "2*z=2*(\<Sum>i\<le>r. i)+2*x"  using x_def a by simp arith
   3.125 +    also have "\<dots> = r * (r+1) + 2*x"   using gauss_sum_nat_upto by simp
   3.126 +    also have "\<dots> = (x+y)*(x+y+1)+2*x" using y_def b by simp
   3.127 +    also { have "2 dvd ((x+y)*(x+y+1))"	using dvd2_a_x_suc_a by simp }
   3.128 +    hence "\<dots> = 2 * nat2_to_nat(x,y)"
   3.129 +      using nat2_to_nat_def by (simp add: Let_def dvd_mult_div_cancel)
   3.130 +    finally have "z=nat2_to_nat (x, y)"  by simp
   3.131 +  }
   3.132 +  thus "\<forall>y. \<exists>x. y = nat2_to_nat x"  by fast
   3.133 +qed
   3.134 +
   3.135 +
   3.136 +subsection{*  A bijection between @{text "\<nat>"} and @{text "\<int>"} *}
   3.137 +
   3.138 +definition nat_to_int_bij :: "nat \<Rightarrow> int" where
   3.139 +"nat_to_int_bij n = (if 2 dvd n then int(n div 2) else -int(Suc n div 2))"
   3.140 +
   3.141 +definition int_to_nat_bij :: "int \<Rightarrow> nat" where
   3.142 +"int_to_nat_bij i = (if 0<=i then 2*nat(i) else 2*nat(-i) - 1)"
   3.143 +
   3.144 +lemma  i2n_n2i_id: "int_to_nat_bij (nat_to_int_bij n) = n"
   3.145 +by (simp add: int_to_nat_bij_def nat_to_int_bij_def) presburger
   3.146 +
   3.147 +lemma n2i_i2n_id: "nat_to_int_bij(int_to_nat_bij i) = i"
   3.148 +proof -
   3.149 +  have "ALL m n::nat. m>0 \<longrightarrow> 2 * m - Suc 0 \<noteq> 2 * n" by presburger
   3.150 +  thus ?thesis
   3.151 +    by(simp add: nat_to_int_bij_def int_to_nat_bij_def, simp add:dvd_def)
   3.152 +qed
   3.153 +
   3.154 +lemma inv_nat_to_int_bij: "inv nat_to_int_bij = int_to_nat_bij"
   3.155 +by (simp add: i2n_n2i_id inv_equality n2i_i2n_id)
   3.156 +
   3.157 +lemma inv_int_to_nat_bij: "inv int_to_nat_bij = nat_to_int_bij"
   3.158 +by (simp add: i2n_n2i_id inv_equality n2i_i2n_id)
   3.159 +
   3.160 +lemma surj_nat_to_int_bij: "surj nat_to_int_bij"
   3.161 +by (blast intro: n2i_i2n_id surjI)
   3.162 +
   3.163 +lemma surj_int_to_nat_bij: "surj int_to_nat_bij"
   3.164 +by (blast intro: i2n_n2i_id surjI)
   3.165 +
   3.166 +lemma inj_nat_to_int_bij: "inj nat_to_int_bij"
   3.167 +by(simp add:inv_int_to_nat_bij[symmetric] surj_int_to_nat_bij surj_imp_inj_inv)
   3.168 +
   3.169 +lemma inj_int_to_nat_bij: "inj int_to_nat_bij"
   3.170 +by(simp add:inv_nat_to_int_bij[symmetric] surj_nat_to_int_bij surj_imp_inj_inv)
   3.171 +
   3.172 +
   3.173 +end
     4.1 --- a/src/HOL/Main.thy	Thu Feb 12 21:24:14 2009 -0800
     4.2 +++ b/src/HOL/Main.thy	Fri Feb 13 09:54:47 2009 +0100
     4.3 @@ -1,7 +1,7 @@
     4.4  header {* Main HOL *}
     4.5  
     4.6  theory Main
     4.7 -imports Plain Code_Eval Map Nat_Int_Bij Recdef SAT
     4.8 +imports Plain Code_Eval Map Recdef SAT
     4.9  begin
    4.10  
    4.11  text {*
     5.1 --- a/src/HOL/Nat_Int_Bij.thy	Thu Feb 12 21:24:14 2009 -0800
     5.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.3 @@ -1,170 +0,0 @@
     5.4 -(*  Title:      HOL/Nat_Int_Bij.thy
     5.5 -    ID:         $Id$
     5.6 -    Author:     Stefan Richter, Tobias Nipkow
     5.7 -*)
     5.8 -
     5.9 -header{* Bijections $\mathbb{N}\to\mathbb{N}^2$ and $\mathbb{N}\to\mathbb{Z}$*}
    5.10 -
    5.11 -theory Nat_Int_Bij
    5.12 -imports Hilbert_Choice Presburger
    5.13 -begin
    5.14 -
    5.15 -subsection{*  A bijection between @{text "\<nat>"} and @{text "\<nat>\<twosuperior>"} *}
    5.16 -
    5.17 -text{* Definition and proofs are from \cite[page 85]{Oberschelp:1993}. *}
    5.18 -
    5.19 -definition nat2_to_nat:: "(nat * nat) \<Rightarrow> nat" where
    5.20 -"nat2_to_nat pair = (let (n,m) = pair in (n+m) * Suc (n+m) div 2 + n)"
    5.21 -definition nat_to_nat2::  "nat \<Rightarrow> (nat * nat)" where
    5.22 -"nat_to_nat2 = inv nat2_to_nat"
    5.23 -
    5.24 -lemma dvd2_a_x_suc_a: "2 dvd a * (Suc a)"
    5.25 -proof (cases "2 dvd a")
    5.26 -  case True
    5.27 -  then show ?thesis by (rule dvd_mult2)
    5.28 -next
    5.29 -  case False
    5.30 -  then have "Suc (a mod 2) = 2" by (simp add: dvd_eq_mod_eq_0)
    5.31 -  then have "Suc a mod 2 = 0" by (simp add: mod_Suc)
    5.32 -  then have "2 dvd Suc a" by (simp only:dvd_eq_mod_eq_0)
    5.33 -  then show ?thesis by (rule dvd_mult)
    5.34 -qed
    5.35 -
    5.36 -lemma
    5.37 -  assumes eq: "nat2_to_nat (u,v) = nat2_to_nat (x,y)"
    5.38 -  shows nat2_to_nat_help: "u+v \<le> x+y"
    5.39 -proof (rule classical)
    5.40 -  assume "\<not> ?thesis"
    5.41 -  then have contrapos: "x+y < u+v"
    5.42 -    by simp
    5.43 -  have "nat2_to_nat (x,y) < (x+y) * Suc (x+y) div 2 + Suc (x + y)"
    5.44 -    by (unfold nat2_to_nat_def) (simp add: Let_def)
    5.45 -  also have "\<dots> = (x+y)*Suc(x+y) div 2 + 2 * Suc(x+y) div 2"
    5.46 -    by (simp only: div_mult_self1_is_m)
    5.47 -  also have "\<dots> = (x+y)*Suc(x+y) div 2 + 2 * Suc(x+y) div 2
    5.48 -    + ((x+y)*Suc(x+y) mod 2 + 2 * Suc(x+y) mod 2) div 2"
    5.49 -  proof -
    5.50 -    have "2 dvd (x+y)*Suc(x+y)"
    5.51 -      by (rule dvd2_a_x_suc_a)
    5.52 -    then have "(x+y)*Suc(x+y) mod 2 = 0"
    5.53 -      by (simp only: dvd_eq_mod_eq_0)
    5.54 -    also
    5.55 -    have "2 * Suc(x+y) mod 2 = 0"
    5.56 -      by (rule mod_mult_self1_is_0)
    5.57 -    ultimately have
    5.58 -      "((x+y)*Suc(x+y) mod 2 + 2 * Suc(x+y) mod 2) div 2 = 0"
    5.59 -      by simp
    5.60 -    then show ?thesis
    5.61 -      by simp
    5.62 -  qed
    5.63 -  also have "\<dots> = ((x+y)*Suc(x+y) + 2*Suc(x+y)) div 2"
    5.64 -    by (rule div_add1_eq [symmetric])
    5.65 -  also have "\<dots> = ((x+y+2)*Suc(x+y)) div 2"
    5.66 -    by (simp only: add_mult_distrib [symmetric])
    5.67 -  also from contrapos have "\<dots> \<le> ((Suc(u+v))*(u+v)) div 2"
    5.68 -    by (simp only: mult_le_mono div_le_mono)
    5.69 -  also have "\<dots> \<le> nat2_to_nat (u,v)"
    5.70 -    by (unfold nat2_to_nat_def) (simp add: Let_def)
    5.71 -  finally show ?thesis
    5.72 -    by (simp only: eq)
    5.73 -qed
    5.74 -
    5.75 -theorem nat2_to_nat_inj: "inj nat2_to_nat"
    5.76 -proof -
    5.77 -  {
    5.78 -    fix u v x y
    5.79 -    assume eq1: "nat2_to_nat (u,v) = nat2_to_nat (x,y)"
    5.80 -    then have "u+v \<le> x+y" by (rule nat2_to_nat_help)
    5.81 -    also from eq1 [symmetric] have "x+y \<le> u+v"
    5.82 -      by (rule nat2_to_nat_help)
    5.83 -    finally have eq2: "u+v = x+y" .
    5.84 -    with eq1 have ux: "u=x"
    5.85 -      by (simp add: nat2_to_nat_def Let_def)
    5.86 -    with eq2 have vy: "v=y" by simp
    5.87 -    with ux have "(u,v) = (x,y)" by simp
    5.88 -  }
    5.89 -  then have "\<And>x y. nat2_to_nat x = nat2_to_nat y \<Longrightarrow> x=y" by fast
    5.90 -  then show ?thesis unfolding inj_on_def by simp
    5.91 -qed
    5.92 -
    5.93 -lemma nat_to_nat2_surj: "surj nat_to_nat2"
    5.94 -by (simp only: nat_to_nat2_def nat2_to_nat_inj inj_imp_surj_inv)
    5.95 -
    5.96 -
    5.97 -lemma gauss_sum_nat_upto: "2 * (\<Sum>i\<le>n::nat. i) = n * (n + 1)"
    5.98 -using gauss_sum[where 'a = nat]
    5.99 -by (simp add:atLeast0AtMost setsum_shift_lb_Suc0_0 numeral_2_eq_2)
   5.100 -
   5.101 -lemma nat2_to_nat_surj: "surj nat2_to_nat"
   5.102 -proof (unfold surj_def)
   5.103 -  {
   5.104 -    fix z::nat 
   5.105 -    def r \<equiv> "Max {r. (\<Sum>i\<le>r. i) \<le> z}" 
   5.106 -    def x \<equiv> "z - (\<Sum>i\<le>r. i)"
   5.107 -
   5.108 -    hence "finite  {r. (\<Sum>i\<le>r. i) \<le> z}"
   5.109 -      by (simp add: lessThan_Suc_atMost[symmetric] lessThan_Suc finite_less_ub)
   5.110 -    also have "0 \<in> {r. (\<Sum>i\<le>r. i) \<le> z}"  by simp
   5.111 -    hence "{r::nat. (\<Sum>i\<le>r. i) \<le> z} \<noteq> {}"  by fast
   5.112 -    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)"
   5.113 -      by (simp add: r_def del:mem_Collect_eq)
   5.114 -    {
   5.115 -      assume "r<x"
   5.116 -      hence "r+1\<le>x"  by simp
   5.117 -      hence "(\<Sum>i\<le>r. i)+(r+1)\<le>z"  using x_def by arith
   5.118 -      hence "(r+1) \<in>  {r. (\<Sum>i\<le>r. i) \<le> z}"  by simp
   5.119 -      with a have "(r+1)\<le>r"  by simp
   5.120 -    }
   5.121 -    hence b: "x\<le>r"  by force
   5.122 -    
   5.123 -    def y \<equiv> "r-x"
   5.124 -    have "2*z=2*(\<Sum>i\<le>r. i)+2*x"  using x_def a by simp arith
   5.125 -    also have "\<dots> = r * (r+1) + 2*x"   using gauss_sum_nat_upto by simp
   5.126 -    also have "\<dots> = (x+y)*(x+y+1)+2*x" using y_def b by simp
   5.127 -    also { have "2 dvd ((x+y)*(x+y+1))"	using dvd2_a_x_suc_a by simp }
   5.128 -    hence "\<dots> = 2 * nat2_to_nat(x,y)"
   5.129 -      using nat2_to_nat_def by (simp add: Let_def dvd_mult_div_cancel)
   5.130 -    finally have "z=nat2_to_nat (x, y)"  by simp
   5.131 -  }
   5.132 -  thus "\<forall>y. \<exists>x. y = nat2_to_nat x"  by fast
   5.133 -qed
   5.134 -
   5.135 -
   5.136 -subsection{*  A bijection between @{text "\<nat>"} and @{text "\<int>"} *}
   5.137 -
   5.138 -definition nat_to_int_bij :: "nat \<Rightarrow> int" where
   5.139 -"nat_to_int_bij n = (if 2 dvd n then int(n div 2) else -int(Suc n div 2))"
   5.140 -
   5.141 -definition int_to_nat_bij :: "int \<Rightarrow> nat" where
   5.142 -"int_to_nat_bij i = (if 0<=i then 2*nat(i) else 2*nat(-i) - 1)"
   5.143 -
   5.144 -lemma  i2n_n2i_id: "int_to_nat_bij (nat_to_int_bij n) = n"
   5.145 -by (simp add: int_to_nat_bij_def nat_to_int_bij_def) presburger
   5.146 -
   5.147 -lemma n2i_i2n_id: "nat_to_int_bij(int_to_nat_bij i) = i"
   5.148 -proof -
   5.149 -  have "ALL m n::nat. m>0 \<longrightarrow> 2 * m - Suc 0 \<noteq> 2 * n" by presburger
   5.150 -  thus ?thesis
   5.151 -    by(simp add: nat_to_int_bij_def int_to_nat_bij_def, simp add:dvd_def)
   5.152 -qed
   5.153 -
   5.154 -lemma inv_nat_to_int_bij: "inv nat_to_int_bij = int_to_nat_bij"
   5.155 -by (simp add: i2n_n2i_id inv_equality n2i_i2n_id)
   5.156 -
   5.157 -lemma inv_int_to_nat_bij: "inv int_to_nat_bij = nat_to_int_bij"
   5.158 -by (simp add: i2n_n2i_id inv_equality n2i_i2n_id)
   5.159 -
   5.160 -lemma surj_nat_to_int_bij: "surj nat_to_int_bij"
   5.161 -by (blast intro: n2i_i2n_id surjI)
   5.162 -
   5.163 -lemma surj_int_to_nat_bij: "surj int_to_nat_bij"
   5.164 -by (blast intro: i2n_n2i_id surjI)
   5.165 -
   5.166 -lemma inj_nat_to_int_bij: "inj nat_to_int_bij"
   5.167 -by(simp add:inv_int_to_nat_bij[symmetric] surj_int_to_nat_bij surj_imp_inj_inv)
   5.168 -
   5.169 -lemma inj_int_to_nat_bij: "inj int_to_nat_bij"
   5.170 -by(simp add:inv_nat_to_int_bij[symmetric] surj_nat_to_int_bij surj_imp_inj_inv)
   5.171 -
   5.172 -
   5.173 -end
     6.1 --- a/src/HOL/SET-Protocol/MessageSET.thy	Thu Feb 12 21:24:14 2009 -0800
     6.2 +++ b/src/HOL/SET-Protocol/MessageSET.thy	Fri Feb 13 09:54:47 2009 +0100
     6.3 @@ -6,7 +6,7 @@
     6.4  header{*The Message Theory, Modified for SET*}
     6.5  
     6.6  theory MessageSET
     6.7 -imports Main
     6.8 +imports Main Nat_Int_Bij
     6.9  begin
    6.10  
    6.11  subsection{*General Lemmas*}