Replaced Library/NatPair by Nat_Int_Bij.
authornipkow
Tue Sep 02 22:37:20 2008 +0200 (2008-09-02)
changeset 28098c92850d2d16c
parent 28097 003dff7410c1
child 28099 fb16a07d6580
Replaced Library/NatPair by Nat_Int_Bij.
src/HOL/Auth/ROOT.ML
src/HOL/Auth/TLS.thy
src/HOL/Complex/ex/DenumRat.thy
src/HOL/IsaMakefile
src/HOL/Library/Library.thy
src/HOL/Library/NatPair.thy
src/HOL/Nat_Int_Bij.thy
src/HOL/SET-Protocol/MessageSET.thy
src/HOL/SET-Protocol/ROOT.ML
src/HOL/ex/ExecutableContent.thy
src/HOL/ex/ROOT.ML
     1.1 --- a/src/HOL/Auth/ROOT.ML	Tue Sep 02 22:20:27 2008 +0200
     1.2 +++ b/src/HOL/Auth/ROOT.ML	Tue Sep 02 22:37:20 2008 +0200
     1.3 @@ -6,8 +6,6 @@
     1.4  Root file for protocol proofs.
     1.5  *)
     1.6  
     1.7 -no_document use_thy "NatPair";
     1.8 -
     1.9  use_thys [
    1.10  
    1.11  (* Conventional protocols: rely on 
     2.1 --- a/src/HOL/Auth/TLS.thy	Tue Sep 02 22:20:27 2008 +0200
     2.2 +++ b/src/HOL/Auth/TLS.thy	Tue Sep 02 22:37:20 2008 +0200
     2.3 @@ -41,7 +41,7 @@
     2.4  
     2.5  header{*The TLS Protocol: Transport Layer Security*}
     2.6  
     2.7 -theory TLS imports Public NatPair begin
     2.8 +theory TLS imports Public begin
     2.9  
    2.10  constdefs
    2.11    certificate      :: "[agent,key] => msg"
     3.1 --- a/src/HOL/Complex/ex/DenumRat.thy	Tue Sep 02 22:20:27 2008 +0200
     3.2 +++ b/src/HOL/Complex/ex/DenumRat.thy	Tue Sep 02 22:37:20 2008 +0200
     3.3 @@ -6,8 +6,7 @@
     3.4  header "Denumerability of the Rationals"
     3.5  
     3.6  theory DenumRat
     3.7 -imports
     3.8 -  Complex_Main NatPair
     3.9 +imports Complex_Main
    3.10  begin
    3.11  
    3.12  lemma nat_to_int_surj: "\<exists>f::nat\<Rightarrow>int. surj f"
     4.1 --- a/src/HOL/IsaMakefile	Tue Sep 02 22:20:27 2008 +0200
     4.2 +++ b/src/HOL/IsaMakefile	Tue Sep 02 22:37:20 2008 +0200
     4.3 @@ -215,6 +215,7 @@
     4.4    Main.thy \
     4.5    Map.thy \
     4.6    NatBin.thy \
     4.7 +  Nat_Int_Bij.thy \
     4.8    nat_simprocs.ML \
     4.9    Presburger.thy \
    4.10    Real/ContNotDenum.thy \
    4.11 @@ -288,7 +289,7 @@
    4.12    Library/Executable_Set.thy Library/Infinite_Set.thy			\
    4.13    Library/FuncSet.thy			\
    4.14    Library/Library.thy Library/List_Prefix.thy Library/State_Monad.thy	\
    4.15 -  Library/Multiset.thy Library/NatPair.thy Library/Permutation.thy	\
    4.16 +  Library/Multiset.thy Library/Permutation.thy	\
    4.17    Library/Primes.thy Library/Pocklington.thy Library/Quotient.thy	\
    4.18    Library/Quicksort.thy Library/Nat_Infinity.thy Library/Word.thy	\
    4.19    Library/README.html Library/Continuity.thy				\
    4.20 @@ -530,7 +531,7 @@
    4.21  
    4.22  HOL-Auth: HOL $(LOG)/HOL-Auth.gz
    4.23  
    4.24 -$(LOG)/HOL-Auth.gz: $(OUT)/HOL Library/NatPair.thy			\
    4.25 +$(LOG)/HOL-Auth.gz: $(OUT)/HOL 						\
    4.26    Auth/CertifiedEmail.thy Auth/Event.thy Auth/Message.thy		\
    4.27    Auth/NS_Public.thy Auth/NS_Public_Bad.thy Auth/NS_Shared.thy		\
    4.28    Auth/OtwayRees.thy Auth/OtwayReesBella.thy Auth/OtwayRees_AN.thy	\
     5.1 --- a/src/HOL/Library/Library.thy	Tue Sep 02 22:20:27 2008 +0200
     5.2 +++ b/src/HOL/Library/Library.thy	Tue Sep 02 22:37:20 2008 +0200
     5.3 @@ -28,7 +28,6 @@
     5.4    Infinite_Set
     5.5    ListVector
     5.6    Multiset
     5.7 -  NatPair
     5.8    Nat_Infinity
     5.9    Nested_Environment
    5.10    Numeral_Type
     6.1 --- a/src/HOL/Library/NatPair.thy	Tue Sep 02 22:20:27 2008 +0200
     6.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.3 @@ -1,134 +0,0 @@
     6.4 -(*  Title:      HOL/Library/NatPair.thy
     6.5 -    ID:         $Id$
     6.6 -    Author:     Stefan Richter
     6.7 -    Copyright   2003 Technische Universitaet Muenchen
     6.8 -*)
     6.9 -
    6.10 -header {* Pairs of Natural Numbers *}
    6.11 -
    6.12 -theory NatPair
    6.13 -imports Main
    6.14 -begin
    6.15 -
    6.16 -text{*
    6.17 -  A bijection between @{text "\<nat>\<twosuperior>"} and @{text \<nat>}.  Definition
    6.18 -  and proofs are from \cite[page 85]{Oberschelp:1993}.
    6.19 -*}
    6.20 -
    6.21 -definition nat2_to_nat:: "(nat * nat) \<Rightarrow> nat" where
    6.22 -"nat2_to_nat pair = (let (n,m) = pair in (n+m) * Suc (n+m) div 2 + n)"
    6.23 -definition nat_to_nat2::  "nat \<Rightarrow> (nat * nat)" where
    6.24 -"nat_to_nat2 = inv nat2_to_nat"
    6.25 -
    6.26 -lemma dvd2_a_x_suc_a: "2 dvd a * (Suc a)"
    6.27 -proof (cases "2 dvd a")
    6.28 -  case True
    6.29 -  then show ?thesis by (rule dvd_mult2)
    6.30 -next
    6.31 -  case False
    6.32 -  then have "Suc (a mod 2) = 2" by (simp add: dvd_eq_mod_eq_0)
    6.33 -  then have "Suc a mod 2 = 0" by (simp add: mod_Suc)
    6.34 -  then have "2 dvd Suc a" by (simp only:dvd_eq_mod_eq_0)
    6.35 -  then show ?thesis by (rule dvd_mult)
    6.36 -qed
    6.37 -
    6.38 -lemma
    6.39 -  assumes eq: "nat2_to_nat (u,v) = nat2_to_nat (x,y)"
    6.40 -  shows nat2_to_nat_help: "u+v \<le> x+y"
    6.41 -proof (rule classical)
    6.42 -  assume "\<not> ?thesis"
    6.43 -  then have contrapos: "x+y < u+v"
    6.44 -    by simp
    6.45 -  have "nat2_to_nat (x,y) < (x+y) * Suc (x+y) div 2 + Suc (x + y)"
    6.46 -    by (unfold nat2_to_nat_def) (simp add: Let_def)
    6.47 -  also have "\<dots> = (x+y)*Suc(x+y) div 2 + 2 * Suc(x+y) div 2"
    6.48 -    by (simp only: div_mult_self1_is_m)
    6.49 -  also have "\<dots> = (x+y)*Suc(x+y) div 2 + 2 * Suc(x+y) div 2
    6.50 -    + ((x+y)*Suc(x+y) mod 2 + 2 * Suc(x+y) mod 2) div 2"
    6.51 -  proof -
    6.52 -    have "2 dvd (x+y)*Suc(x+y)"
    6.53 -      by (rule dvd2_a_x_suc_a)
    6.54 -    then have "(x+y)*Suc(x+y) mod 2 = 0"
    6.55 -      by (simp only: dvd_eq_mod_eq_0)
    6.56 -    also
    6.57 -    have "2 * Suc(x+y) mod 2 = 0"
    6.58 -      by (rule mod_mult_self1_is_0)
    6.59 -    ultimately have
    6.60 -      "((x+y)*Suc(x+y) mod 2 + 2 * Suc(x+y) mod 2) div 2 = 0"
    6.61 -      by simp
    6.62 -    then show ?thesis
    6.63 -      by simp
    6.64 -  qed
    6.65 -  also have "\<dots> = ((x+y)*Suc(x+y) + 2*Suc(x+y)) div 2"
    6.66 -    by (rule div_add1_eq [symmetric])
    6.67 -  also have "\<dots> = ((x+y+2)*Suc(x+y)) div 2"
    6.68 -    by (simp only: add_mult_distrib [symmetric])
    6.69 -  also from contrapos have "\<dots> \<le> ((Suc(u+v))*(u+v)) div 2"
    6.70 -    by (simp only: mult_le_mono div_le_mono)
    6.71 -  also have "\<dots> \<le> nat2_to_nat (u,v)"
    6.72 -    by (unfold nat2_to_nat_def) (simp add: Let_def)
    6.73 -  finally show ?thesis
    6.74 -    by (simp only: eq)
    6.75 -qed
    6.76 -
    6.77 -theorem nat2_to_nat_inj: "inj nat2_to_nat"
    6.78 -proof -
    6.79 -  {
    6.80 -    fix u v x y
    6.81 -    assume eq1: "nat2_to_nat (u,v) = nat2_to_nat (x,y)"
    6.82 -    then have "u+v \<le> x+y" by (rule nat2_to_nat_help)
    6.83 -    also from eq1 [symmetric] have "x+y \<le> u+v"
    6.84 -      by (rule nat2_to_nat_help)
    6.85 -    finally have eq2: "u+v = x+y" .
    6.86 -    with eq1 have ux: "u=x"
    6.87 -      by (simp add: nat2_to_nat_def Let_def)
    6.88 -    with eq2 have vy: "v=y" by simp
    6.89 -    with ux have "(u,v) = (x,y)" by simp
    6.90 -  }
    6.91 -  then have "\<And>x y. nat2_to_nat x = nat2_to_nat y \<Longrightarrow> x=y" by fast
    6.92 -  then show ?thesis unfolding inj_on_def by simp
    6.93 -qed
    6.94 -
    6.95 -lemma nat_to_nat2_surj: "surj nat_to_nat2"
    6.96 -by (simp only: nat_to_nat2_def nat2_to_nat_inj inj_imp_surj_inv)
    6.97 -
    6.98 -
    6.99 -lemma gauss_sum_nat_upto: "2 * (\<Sum>i\<le>n::nat. i) = n * (n + 1)"
   6.100 -using gauss_sum[where 'a = nat]
   6.101 -by (simp add:atLeast0AtMost setsum_shift_lb_Suc0_0 numeral_2_eq_2)
   6.102 -
   6.103 -lemma nat2_to_nat_surj: "surj nat2_to_nat"
   6.104 -proof (unfold surj_def)
   6.105 -  {
   6.106 -    fix z::nat 
   6.107 -    def r \<equiv> "Max {r. (\<Sum>i\<le>r. i) \<le> z}" 
   6.108 -    def x \<equiv> "z - (\<Sum>i\<le>r. i)"
   6.109 -
   6.110 -    hence "finite  {r. (\<Sum>i\<le>r. i) \<le> z}"
   6.111 -      by (simp add: lessThan_Suc_atMost[symmetric] lessThan_Suc finite_less_ub)
   6.112 -    also have "0 \<in> {r. (\<Sum>i\<le>r. i) \<le> z}"  by simp
   6.113 -    hence "{r::nat. (\<Sum>i\<le>r. i) \<le> z} \<noteq> {}"  by fast
   6.114 -    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)"
   6.115 -      by (simp add: r_def del:mem_Collect_eq)
   6.116 -    {
   6.117 -      assume "r<x"
   6.118 -      hence "r+1\<le>x"  by simp
   6.119 -      hence "(\<Sum>i\<le>r. i)+(r+1)\<le>z"  using x_def by arith
   6.120 -      hence "(r+1) \<in>  {r. (\<Sum>i\<le>r. i) \<le> z}"  by simp
   6.121 -      with a have "(r+1)\<le>r"  by simp
   6.122 -    }
   6.123 -    hence b: "x\<le>r"  by force
   6.124 -    
   6.125 -    def y \<equiv> "r-x"
   6.126 -    have "2*z=2*(\<Sum>i\<le>r. i)+2*x"  using x_def a by simp arith
   6.127 -    also have "\<dots> = r * (r+1) + 2*x"   using gauss_sum_nat_upto by simp
   6.128 -    also have "\<dots> = (x+y)*(x+y+1)+2*x" using y_def b by simp
   6.129 -    also { have "2 dvd ((x+y)*(x+y+1))"	using dvd2_a_x_suc_a by simp }
   6.130 -    hence "\<dots> = 2 * nat2_to_nat(x,y)"
   6.131 -      using nat2_to_nat_def by (simp add: Let_def dvd_mult_div_cancel)
   6.132 -    finally have "z=nat2_to_nat (x, y)"  by simp
   6.133 -  }
   6.134 -  thus "\<forall>y. \<exists>x. y = nat2_to_nat x"  by fast
   6.135 -qed
   6.136 -
   6.137 -end
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/src/HOL/Nat_Int_Bij.thy	Tue Sep 02 22:37:20 2008 +0200
     7.3 @@ -0,0 +1,170 @@
     7.4 +(*  Title:      HOL/Nat_Int_Bij.thy
     7.5 +    ID:         $Id$
     7.6 +    Author:     Stefan Richter, Tobias Nipkow
     7.7 +*)
     7.8 +
     7.9 +header{* Bijections $\mathbb{N}\to\mathbb{N}^2$ and $\mathbb{N}\to\mathbb{Z}$*}
    7.10 +
    7.11 +theory Nat_Int_Bij
    7.12 +imports Hilbert_Choice Presburger
    7.13 +begin
    7.14 +
    7.15 +subsection{*  A bijection between @{text "\<nat>"} and @{text "\<nat>\<twosuperior>"} *}
    7.16 +
    7.17 +text{* Definition and proofs are from \cite[page 85]{Oberschelp:1993}. *}
    7.18 +
    7.19 +definition nat2_to_nat:: "(nat * nat) \<Rightarrow> nat" where
    7.20 +"nat2_to_nat pair = (let (n,m) = pair in (n+m) * Suc (n+m) div 2 + n)"
    7.21 +definition nat_to_nat2::  "nat \<Rightarrow> (nat * nat)" where
    7.22 +"nat_to_nat2 = inv nat2_to_nat"
    7.23 +
    7.24 +lemma dvd2_a_x_suc_a: "2 dvd a * (Suc a)"
    7.25 +proof (cases "2 dvd a")
    7.26 +  case True
    7.27 +  then show ?thesis by (rule dvd_mult2)
    7.28 +next
    7.29 +  case False
    7.30 +  then have "Suc (a mod 2) = 2" by (simp add: dvd_eq_mod_eq_0)
    7.31 +  then have "Suc a mod 2 = 0" by (simp add: mod_Suc)
    7.32 +  then have "2 dvd Suc a" by (simp only:dvd_eq_mod_eq_0)
    7.33 +  then show ?thesis by (rule dvd_mult)
    7.34 +qed
    7.35 +
    7.36 +lemma
    7.37 +  assumes eq: "nat2_to_nat (u,v) = nat2_to_nat (x,y)"
    7.38 +  shows nat2_to_nat_help: "u+v \<le> x+y"
    7.39 +proof (rule classical)
    7.40 +  assume "\<not> ?thesis"
    7.41 +  then have contrapos: "x+y < u+v"
    7.42 +    by simp
    7.43 +  have "nat2_to_nat (x,y) < (x+y) * Suc (x+y) div 2 + Suc (x + y)"
    7.44 +    by (unfold nat2_to_nat_def) (simp add: Let_def)
    7.45 +  also have "\<dots> = (x+y)*Suc(x+y) div 2 + 2 * Suc(x+y) div 2"
    7.46 +    by (simp only: div_mult_self1_is_m)
    7.47 +  also have "\<dots> = (x+y)*Suc(x+y) div 2 + 2 * Suc(x+y) div 2
    7.48 +    + ((x+y)*Suc(x+y) mod 2 + 2 * Suc(x+y) mod 2) div 2"
    7.49 +  proof -
    7.50 +    have "2 dvd (x+y)*Suc(x+y)"
    7.51 +      by (rule dvd2_a_x_suc_a)
    7.52 +    then have "(x+y)*Suc(x+y) mod 2 = 0"
    7.53 +      by (simp only: dvd_eq_mod_eq_0)
    7.54 +    also
    7.55 +    have "2 * Suc(x+y) mod 2 = 0"
    7.56 +      by (rule mod_mult_self1_is_0)
    7.57 +    ultimately have
    7.58 +      "((x+y)*Suc(x+y) mod 2 + 2 * Suc(x+y) mod 2) div 2 = 0"
    7.59 +      by simp
    7.60 +    then show ?thesis
    7.61 +      by simp
    7.62 +  qed
    7.63 +  also have "\<dots> = ((x+y)*Suc(x+y) + 2*Suc(x+y)) div 2"
    7.64 +    by (rule div_add1_eq [symmetric])
    7.65 +  also have "\<dots> = ((x+y+2)*Suc(x+y)) div 2"
    7.66 +    by (simp only: add_mult_distrib [symmetric])
    7.67 +  also from contrapos have "\<dots> \<le> ((Suc(u+v))*(u+v)) div 2"
    7.68 +    by (simp only: mult_le_mono div_le_mono)
    7.69 +  also have "\<dots> \<le> nat2_to_nat (u,v)"
    7.70 +    by (unfold nat2_to_nat_def) (simp add: Let_def)
    7.71 +  finally show ?thesis
    7.72 +    by (simp only: eq)
    7.73 +qed
    7.74 +
    7.75 +theorem nat2_to_nat_inj: "inj nat2_to_nat"
    7.76 +proof -
    7.77 +  {
    7.78 +    fix u v x y
    7.79 +    assume eq1: "nat2_to_nat (u,v) = nat2_to_nat (x,y)"
    7.80 +    then have "u+v \<le> x+y" by (rule nat2_to_nat_help)
    7.81 +    also from eq1 [symmetric] have "x+y \<le> u+v"
    7.82 +      by (rule nat2_to_nat_help)
    7.83 +    finally have eq2: "u+v = x+y" .
    7.84 +    with eq1 have ux: "u=x"
    7.85 +      by (simp add: nat2_to_nat_def Let_def)
    7.86 +    with eq2 have vy: "v=y" by simp
    7.87 +    with ux have "(u,v) = (x,y)" by simp
    7.88 +  }
    7.89 +  then have "\<And>x y. nat2_to_nat x = nat2_to_nat y \<Longrightarrow> x=y" by fast
    7.90 +  then show ?thesis unfolding inj_on_def by simp
    7.91 +qed
    7.92 +
    7.93 +lemma nat_to_nat2_surj: "surj nat_to_nat2"
    7.94 +by (simp only: nat_to_nat2_def nat2_to_nat_inj inj_imp_surj_inv)
    7.95 +
    7.96 +
    7.97 +lemma gauss_sum_nat_upto: "2 * (\<Sum>i\<le>n::nat. i) = n * (n + 1)"
    7.98 +using gauss_sum[where 'a = nat]
    7.99 +by (simp add:atLeast0AtMost setsum_shift_lb_Suc0_0 numeral_2_eq_2)
   7.100 +
   7.101 +lemma nat2_to_nat_surj: "surj nat2_to_nat"
   7.102 +proof (unfold surj_def)
   7.103 +  {
   7.104 +    fix z::nat 
   7.105 +    def r \<equiv> "Max {r. (\<Sum>i\<le>r. i) \<le> z}" 
   7.106 +    def x \<equiv> "z - (\<Sum>i\<le>r. i)"
   7.107 +
   7.108 +    hence "finite  {r. (\<Sum>i\<le>r. i) \<le> z}"
   7.109 +      by (simp add: lessThan_Suc_atMost[symmetric] lessThan_Suc finite_less_ub)
   7.110 +    also have "0 \<in> {r. (\<Sum>i\<le>r. i) \<le> z}"  by simp
   7.111 +    hence "{r::nat. (\<Sum>i\<le>r. i) \<le> z} \<noteq> {}"  by fast
   7.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)"
   7.113 +      by (simp add: r_def del:mem_Collect_eq)
   7.114 +    {
   7.115 +      assume "r<x"
   7.116 +      hence "r+1\<le>x"  by simp
   7.117 +      hence "(\<Sum>i\<le>r. i)+(r+1)\<le>z"  using x_def by arith
   7.118 +      hence "(r+1) \<in>  {r. (\<Sum>i\<le>r. i) \<le> z}"  by simp
   7.119 +      with a have "(r+1)\<le>r"  by simp
   7.120 +    }
   7.121 +    hence b: "x\<le>r"  by force
   7.122 +    
   7.123 +    def y \<equiv> "r-x"
   7.124 +    have "2*z=2*(\<Sum>i\<le>r. i)+2*x"  using x_def a by simp arith
   7.125 +    also have "\<dots> = r * (r+1) + 2*x"   using gauss_sum_nat_upto by simp
   7.126 +    also have "\<dots> = (x+y)*(x+y+1)+2*x" using y_def b by simp
   7.127 +    also { have "2 dvd ((x+y)*(x+y+1))"	using dvd2_a_x_suc_a by simp }
   7.128 +    hence "\<dots> = 2 * nat2_to_nat(x,y)"
   7.129 +      using nat2_to_nat_def by (simp add: Let_def dvd_mult_div_cancel)
   7.130 +    finally have "z=nat2_to_nat (x, y)"  by simp
   7.131 +  }
   7.132 +  thus "\<forall>y. \<exists>x. y = nat2_to_nat x"  by fast
   7.133 +qed
   7.134 +
   7.135 +
   7.136 +subsection{*  A bijection between @{text "\<nat>"} and @{text "\<int>"} *}
   7.137 +
   7.138 +definition nat_to_int_bij :: "nat \<Rightarrow> int" where
   7.139 +"nat_to_int_bij n = (if 2 dvd n then int(n div 2) else -int(Suc n div 2))"
   7.140 +
   7.141 +definition int_to_nat_bij :: "int \<Rightarrow> nat" where
   7.142 +"int_to_nat_bij i = (if 0<=i then 2*nat(i) else 2*nat(-i) - 1)"
   7.143 +
   7.144 +lemma  i2n_n2i_id: "int_to_nat_bij (nat_to_int_bij n) = n"
   7.145 +by (simp add: int_to_nat_bij_def nat_to_int_bij_def) presburger
   7.146 +
   7.147 +lemma n2i_i2n_id: "nat_to_int_bij(int_to_nat_bij i) = i"
   7.148 +proof -
   7.149 +  have "ALL m n::nat. m>0 \<longrightarrow> 2 * m - Suc 0 \<noteq> 2 * n" by presburger
   7.150 +  thus ?thesis
   7.151 +    by(simp add: nat_to_int_bij_def int_to_nat_bij_def, simp add:dvd_def)
   7.152 +qed
   7.153 +
   7.154 +lemma inv_nat_to_int_bij: "inv nat_to_int_bij = int_to_nat_bij"
   7.155 +by (simp add: i2n_n2i_id inv_equality n2i_i2n_id)
   7.156 +
   7.157 +lemma inv_int_to_nat_bij: "inv int_to_nat_bij = nat_to_int_bij"
   7.158 +by (simp add: i2n_n2i_id inv_equality n2i_i2n_id)
   7.159 +
   7.160 +lemma surj_nat_to_int_bij: "surj nat_to_int_bij"
   7.161 +by (blast intro: n2i_i2n_id surjI)
   7.162 +
   7.163 +lemma surj_int_to_nat_bij: "surj int_to_nat_bij"
   7.164 +by (blast intro: i2n_n2i_id surjI)
   7.165 +
   7.166 +lemma inj_nat_to_int_bij: "inj nat_to_int_bij"
   7.167 +by(simp add:inv_int_to_nat_bij[symmetric] surj_int_to_nat_bij surj_imp_inj_inv)
   7.168 +
   7.169 +lemma inj_int_to_nat_bij: "inj int_to_nat_bij"
   7.170 +by(simp add:inv_nat_to_int_bij[symmetric] surj_nat_to_int_bij surj_imp_inj_inv)
   7.171 +
   7.172 +
   7.173 +end
     8.1 --- a/src/HOL/SET-Protocol/MessageSET.thy	Tue Sep 02 22:20:27 2008 +0200
     8.2 +++ b/src/HOL/SET-Protocol/MessageSET.thy	Tue Sep 02 22:37:20 2008 +0200
     8.3 @@ -6,7 +6,7 @@
     8.4  header{*The Message Theory, Modified for SET*}
     8.5  
     8.6  theory MessageSET
     8.7 -imports Main NatPair
     8.8 +imports Main
     8.9  begin
    8.10  
    8.11  subsection{*General Lemmas*}
     9.1 --- a/src/HOL/SET-Protocol/ROOT.ML	Tue Sep 02 22:20:27 2008 +0200
     9.2 +++ b/src/HOL/SET-Protocol/ROOT.ML	Tue Sep 02 22:37:20 2008 +0200
     9.3 @@ -6,5 +6,4 @@
     9.4  Root file for the SET protocol proofs.
     9.5  *)
     9.6  
     9.7 -no_document use_thy "NatPair";
     9.8  use_thys ["Cardholder_Registration", "Merchant_Registration", "Purchase"];
    10.1 --- a/src/HOL/ex/ExecutableContent.thy	Tue Sep 02 22:20:27 2008 +0200
    10.2 +++ b/src/HOL/ex/ExecutableContent.thy	Tue Sep 02 22:37:20 2008 +0200
    10.3 @@ -14,7 +14,6 @@
    10.4    Eval
    10.5    List_Prefix
    10.6    Nat_Infinity
    10.7 -  NatPair
    10.8    Nested_Environment
    10.9    Option_ord
   10.10    Permutation
    11.1 --- a/src/HOL/ex/ROOT.ML	Tue Sep 02 22:20:27 2008 +0200
    11.2 +++ b/src/HOL/ex/ROOT.ML	Tue Sep 02 22:37:20 2008 +0200
    11.3 @@ -92,8 +92,7 @@
    11.4  
    11.5  no_document use_thys [
    11.6    "../NumberTheory/Factorization",
    11.7 -  "../Library/BigO",
    11.8 -  "../Library/NatPair"
    11.9 +  "../Library/BigO"
   11.10  ];
   11.11  
   11.12  use_thys [