# HG changeset patch # User nipkow # Date 1220387840 -7200 # Node ID c92850d2d16cdba65de28b57e68250274501d740 # Parent 003dff7410c14e5acee27750aba75c8d9ac67efc Replaced Library/NatPair by Nat_Int_Bij. diff -r 003dff7410c1 -r c92850d2d16c src/HOL/Auth/ROOT.ML --- a/src/HOL/Auth/ROOT.ML Tue Sep 02 22:20:27 2008 +0200 +++ b/src/HOL/Auth/ROOT.ML Tue Sep 02 22:37:20 2008 +0200 @@ -6,8 +6,6 @@ Root file for protocol proofs. *) -no_document use_thy "NatPair"; - use_thys [ (* Conventional protocols: rely on diff -r 003dff7410c1 -r c92850d2d16c src/HOL/Auth/TLS.thy --- a/src/HOL/Auth/TLS.thy Tue Sep 02 22:20:27 2008 +0200 +++ b/src/HOL/Auth/TLS.thy Tue Sep 02 22:37:20 2008 +0200 @@ -41,7 +41,7 @@ header{*The TLS Protocol: Transport Layer Security*} -theory TLS imports Public NatPair begin +theory TLS imports Public begin constdefs certificate :: "[agent,key] => msg" diff -r 003dff7410c1 -r c92850d2d16c src/HOL/Complex/ex/DenumRat.thy --- a/src/HOL/Complex/ex/DenumRat.thy Tue Sep 02 22:20:27 2008 +0200 +++ b/src/HOL/Complex/ex/DenumRat.thy Tue Sep 02 22:37:20 2008 +0200 @@ -6,8 +6,7 @@ header "Denumerability of the Rationals" theory DenumRat -imports - Complex_Main NatPair +imports Complex_Main begin lemma nat_to_int_surj: "\f::nat\int. surj f" diff -r 003dff7410c1 -r c92850d2d16c src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Tue Sep 02 22:20:27 2008 +0200 +++ b/src/HOL/IsaMakefile Tue Sep 02 22:37:20 2008 +0200 @@ -215,6 +215,7 @@ Main.thy \ Map.thy \ NatBin.thy \ + Nat_Int_Bij.thy \ nat_simprocs.ML \ Presburger.thy \ Real/ContNotDenum.thy \ @@ -288,7 +289,7 @@ Library/Executable_Set.thy Library/Infinite_Set.thy \ Library/FuncSet.thy \ Library/Library.thy Library/List_Prefix.thy Library/State_Monad.thy \ - Library/Multiset.thy Library/NatPair.thy Library/Permutation.thy \ + Library/Multiset.thy Library/Permutation.thy \ Library/Primes.thy Library/Pocklington.thy Library/Quotient.thy \ Library/Quicksort.thy Library/Nat_Infinity.thy Library/Word.thy \ Library/README.html Library/Continuity.thy \ @@ -530,7 +531,7 @@ HOL-Auth: HOL $(LOG)/HOL-Auth.gz -$(LOG)/HOL-Auth.gz: $(OUT)/HOL Library/NatPair.thy \ +$(LOG)/HOL-Auth.gz: $(OUT)/HOL \ Auth/CertifiedEmail.thy Auth/Event.thy Auth/Message.thy \ Auth/NS_Public.thy Auth/NS_Public_Bad.thy Auth/NS_Shared.thy \ Auth/OtwayRees.thy Auth/OtwayReesBella.thy Auth/OtwayRees_AN.thy \ diff -r 003dff7410c1 -r c92850d2d16c src/HOL/Library/Library.thy --- a/src/HOL/Library/Library.thy Tue Sep 02 22:20:27 2008 +0200 +++ b/src/HOL/Library/Library.thy Tue Sep 02 22:37:20 2008 +0200 @@ -28,7 +28,6 @@ Infinite_Set ListVector Multiset - NatPair Nat_Infinity Nested_Environment Numeral_Type diff -r 003dff7410c1 -r c92850d2d16c src/HOL/Library/NatPair.thy --- a/src/HOL/Library/NatPair.thy Tue Sep 02 22:20:27 2008 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,134 +0,0 @@ -(* Title: HOL/Library/NatPair.thy - ID: $Id$ - Author: Stefan Richter - Copyright 2003 Technische Universitaet Muenchen -*) - -header {* Pairs of Natural Numbers *} - -theory NatPair -imports Main -begin - -text{* - A bijection between @{text "\\"} and @{text \}. Definition - and proofs are from \cite[page 85]{Oberschelp:1993}. -*} - -definition nat2_to_nat:: "(nat * nat) \ nat" where -"nat2_to_nat pair = (let (n,m) = pair in (n+m) * Suc (n+m) div 2 + n)" -definition nat_to_nat2:: "nat \ (nat * nat)" where -"nat_to_nat2 = inv nat2_to_nat" - -lemma dvd2_a_x_suc_a: "2 dvd a * (Suc a)" -proof (cases "2 dvd a") - case True - then show ?thesis by (rule dvd_mult2) -next - case False - then have "Suc (a mod 2) = 2" by (simp add: dvd_eq_mod_eq_0) - then have "Suc a mod 2 = 0" by (simp add: mod_Suc) - then have "2 dvd Suc a" by (simp only:dvd_eq_mod_eq_0) - then show ?thesis by (rule dvd_mult) -qed - -lemma - assumes eq: "nat2_to_nat (u,v) = nat2_to_nat (x,y)" - shows nat2_to_nat_help: "u+v \ x+y" -proof (rule classical) - assume "\ ?thesis" - then have contrapos: "x+y < u+v" - by simp - have "nat2_to_nat (x,y) < (x+y) * Suc (x+y) div 2 + Suc (x + y)" - by (unfold nat2_to_nat_def) (simp add: Let_def) - also have "\ = (x+y)*Suc(x+y) div 2 + 2 * Suc(x+y) div 2" - by (simp only: div_mult_self1_is_m) - also have "\ = (x+y)*Suc(x+y) div 2 + 2 * Suc(x+y) div 2 - + ((x+y)*Suc(x+y) mod 2 + 2 * Suc(x+y) mod 2) div 2" - proof - - have "2 dvd (x+y)*Suc(x+y)" - by (rule dvd2_a_x_suc_a) - then have "(x+y)*Suc(x+y) mod 2 = 0" - by (simp only: dvd_eq_mod_eq_0) - also - have "2 * Suc(x+y) mod 2 = 0" - by (rule mod_mult_self1_is_0) - ultimately have - "((x+y)*Suc(x+y) mod 2 + 2 * Suc(x+y) mod 2) div 2 = 0" - by simp - then show ?thesis - by simp - qed - also have "\ = ((x+y)*Suc(x+y) + 2*Suc(x+y)) div 2" - by (rule div_add1_eq [symmetric]) - also have "\ = ((x+y+2)*Suc(x+y)) div 2" - by (simp only: add_mult_distrib [symmetric]) - also from contrapos have "\ \ ((Suc(u+v))*(u+v)) div 2" - by (simp only: mult_le_mono div_le_mono) - also have "\ \ nat2_to_nat (u,v)" - by (unfold nat2_to_nat_def) (simp add: Let_def) - finally show ?thesis - by (simp only: eq) -qed - -theorem nat2_to_nat_inj: "inj nat2_to_nat" -proof - - { - fix u v x y - assume eq1: "nat2_to_nat (u,v) = nat2_to_nat (x,y)" - then have "u+v \ x+y" by (rule nat2_to_nat_help) - also from eq1 [symmetric] have "x+y \ u+v" - by (rule nat2_to_nat_help) - finally have eq2: "u+v = x+y" . - with eq1 have ux: "u=x" - by (simp add: nat2_to_nat_def Let_def) - with eq2 have vy: "v=y" by simp - with ux have "(u,v) = (x,y)" by simp - } - then have "\x y. nat2_to_nat x = nat2_to_nat y \ x=y" by fast - then show ?thesis unfolding inj_on_def by simp -qed - -lemma nat_to_nat2_surj: "surj nat_to_nat2" -by (simp only: nat_to_nat2_def nat2_to_nat_inj inj_imp_surj_inv) - - -lemma gauss_sum_nat_upto: "2 * (\i\n::nat. i) = n * (n + 1)" -using gauss_sum[where 'a = nat] -by (simp add:atLeast0AtMost setsum_shift_lb_Suc0_0 numeral_2_eq_2) - -lemma nat2_to_nat_surj: "surj nat2_to_nat" -proof (unfold surj_def) - { - fix z::nat - def r \ "Max {r. (\i\r. i) \ z}" - def x \ "z - (\i\r. i)" - - hence "finite {r. (\i\r. i) \ z}" - by (simp add: lessThan_Suc_atMost[symmetric] lessThan_Suc finite_less_ub) - also have "0 \ {r. (\i\r. i) \ z}" by simp - hence "{r::nat. (\i\r. i) \ z} \ {}" by fast - ultimately have a: "r \ {r. (\i\r. i) \ z} \ (\s \ {r. (\i\r. i) \ z}. s \ r)" - by (simp add: r_def del:mem_Collect_eq) - { - assume "rx" by simp - hence "(\i\r. i)+(r+1)\z" using x_def by arith - hence "(r+1) \ {r. (\i\r. i) \ z}" by simp - with a have "(r+1)\r" by simp - } - hence b: "x\r" by force - - def y \ "r-x" - have "2*z=2*(\i\r. i)+2*x" using x_def a by simp arith - also have "\ = r * (r+1) + 2*x" using gauss_sum_nat_upto by simp - also have "\ = (x+y)*(x+y+1)+2*x" using y_def b by simp - also { have "2 dvd ((x+y)*(x+y+1))" using dvd2_a_x_suc_a by simp } - hence "\ = 2 * nat2_to_nat(x,y)" - using nat2_to_nat_def by (simp add: Let_def dvd_mult_div_cancel) - finally have "z=nat2_to_nat (x, y)" by simp - } - thus "\y. \x. y = nat2_to_nat x" by fast -qed - -end diff -r 003dff7410c1 -r c92850d2d16c src/HOL/Nat_Int_Bij.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Nat_Int_Bij.thy Tue Sep 02 22:37:20 2008 +0200 @@ -0,0 +1,170 @@ +(* Title: HOL/Nat_Int_Bij.thy + ID: $Id$ + Author: Stefan Richter, Tobias Nipkow +*) + +header{* Bijections $\mathbb{N}\to\mathbb{N}^2$ and $\mathbb{N}\to\mathbb{Z}$*} + +theory Nat_Int_Bij +imports Hilbert_Choice Presburger +begin + +subsection{* A bijection between @{text "\"} and @{text "\\"} *} + +text{* Definition and proofs are from \cite[page 85]{Oberschelp:1993}. *} + +definition nat2_to_nat:: "(nat * nat) \ nat" where +"nat2_to_nat pair = (let (n,m) = pair in (n+m) * Suc (n+m) div 2 + n)" +definition nat_to_nat2:: "nat \ (nat * nat)" where +"nat_to_nat2 = inv nat2_to_nat" + +lemma dvd2_a_x_suc_a: "2 dvd a * (Suc a)" +proof (cases "2 dvd a") + case True + then show ?thesis by (rule dvd_mult2) +next + case False + then have "Suc (a mod 2) = 2" by (simp add: dvd_eq_mod_eq_0) + then have "Suc a mod 2 = 0" by (simp add: mod_Suc) + then have "2 dvd Suc a" by (simp only:dvd_eq_mod_eq_0) + then show ?thesis by (rule dvd_mult) +qed + +lemma + assumes eq: "nat2_to_nat (u,v) = nat2_to_nat (x,y)" + shows nat2_to_nat_help: "u+v \ x+y" +proof (rule classical) + assume "\ ?thesis" + then have contrapos: "x+y < u+v" + by simp + have "nat2_to_nat (x,y) < (x+y) * Suc (x+y) div 2 + Suc (x + y)" + by (unfold nat2_to_nat_def) (simp add: Let_def) + also have "\ = (x+y)*Suc(x+y) div 2 + 2 * Suc(x+y) div 2" + by (simp only: div_mult_self1_is_m) + also have "\ = (x+y)*Suc(x+y) div 2 + 2 * Suc(x+y) div 2 + + ((x+y)*Suc(x+y) mod 2 + 2 * Suc(x+y) mod 2) div 2" + proof - + have "2 dvd (x+y)*Suc(x+y)" + by (rule dvd2_a_x_suc_a) + then have "(x+y)*Suc(x+y) mod 2 = 0" + by (simp only: dvd_eq_mod_eq_0) + also + have "2 * Suc(x+y) mod 2 = 0" + by (rule mod_mult_self1_is_0) + ultimately have + "((x+y)*Suc(x+y) mod 2 + 2 * Suc(x+y) mod 2) div 2 = 0" + by simp + then show ?thesis + by simp + qed + also have "\ = ((x+y)*Suc(x+y) + 2*Suc(x+y)) div 2" + by (rule div_add1_eq [symmetric]) + also have "\ = ((x+y+2)*Suc(x+y)) div 2" + by (simp only: add_mult_distrib [symmetric]) + also from contrapos have "\ \ ((Suc(u+v))*(u+v)) div 2" + by (simp only: mult_le_mono div_le_mono) + also have "\ \ nat2_to_nat (u,v)" + by (unfold nat2_to_nat_def) (simp add: Let_def) + finally show ?thesis + by (simp only: eq) +qed + +theorem nat2_to_nat_inj: "inj nat2_to_nat" +proof - + { + fix u v x y + assume eq1: "nat2_to_nat (u,v) = nat2_to_nat (x,y)" + then have "u+v \ x+y" by (rule nat2_to_nat_help) + also from eq1 [symmetric] have "x+y \ u+v" + by (rule nat2_to_nat_help) + finally have eq2: "u+v = x+y" . + with eq1 have ux: "u=x" + by (simp add: nat2_to_nat_def Let_def) + with eq2 have vy: "v=y" by simp + with ux have "(u,v) = (x,y)" by simp + } + then have "\x y. nat2_to_nat x = nat2_to_nat y \ x=y" by fast + then show ?thesis unfolding inj_on_def by simp +qed + +lemma nat_to_nat2_surj: "surj nat_to_nat2" +by (simp only: nat_to_nat2_def nat2_to_nat_inj inj_imp_surj_inv) + + +lemma gauss_sum_nat_upto: "2 * (\i\n::nat. i) = n * (n + 1)" +using gauss_sum[where 'a = nat] +by (simp add:atLeast0AtMost setsum_shift_lb_Suc0_0 numeral_2_eq_2) + +lemma nat2_to_nat_surj: "surj nat2_to_nat" +proof (unfold surj_def) + { + fix z::nat + def r \ "Max {r. (\i\r. i) \ z}" + def x \ "z - (\i\r. i)" + + hence "finite {r. (\i\r. i) \ z}" + by (simp add: lessThan_Suc_atMost[symmetric] lessThan_Suc finite_less_ub) + also have "0 \ {r. (\i\r. i) \ z}" by simp + hence "{r::nat. (\i\r. i) \ z} \ {}" by fast + ultimately have a: "r \ {r. (\i\r. i) \ z} \ (\s \ {r. (\i\r. i) \ z}. s \ r)" + by (simp add: r_def del:mem_Collect_eq) + { + assume "rx" by simp + hence "(\i\r. i)+(r+1)\z" using x_def by arith + hence "(r+1) \ {r. (\i\r. i) \ z}" by simp + with a have "(r+1)\r" by simp + } + hence b: "x\r" by force + + def y \ "r-x" + have "2*z=2*(\i\r. i)+2*x" using x_def a by simp arith + also have "\ = r * (r+1) + 2*x" using gauss_sum_nat_upto by simp + also have "\ = (x+y)*(x+y+1)+2*x" using y_def b by simp + also { have "2 dvd ((x+y)*(x+y+1))" using dvd2_a_x_suc_a by simp } + hence "\ = 2 * nat2_to_nat(x,y)" + using nat2_to_nat_def by (simp add: Let_def dvd_mult_div_cancel) + finally have "z=nat2_to_nat (x, y)" by simp + } + thus "\y. \x. y = nat2_to_nat x" by fast +qed + + +subsection{* A bijection between @{text "\"} and @{text "\"} *} + +definition nat_to_int_bij :: "nat \ int" where +"nat_to_int_bij n = (if 2 dvd n then int(n div 2) else -int(Suc n div 2))" + +definition int_to_nat_bij :: "int \ nat" where +"int_to_nat_bij i = (if 0<=i then 2*nat(i) else 2*nat(-i) - 1)" + +lemma i2n_n2i_id: "int_to_nat_bij (nat_to_int_bij n) = n" +by (simp add: int_to_nat_bij_def nat_to_int_bij_def) presburger + +lemma n2i_i2n_id: "nat_to_int_bij(int_to_nat_bij i) = i" +proof - + have "ALL m n::nat. m>0 \ 2 * m - Suc 0 \ 2 * n" by presburger + thus ?thesis + by(simp add: nat_to_int_bij_def int_to_nat_bij_def, simp add:dvd_def) +qed + +lemma inv_nat_to_int_bij: "inv nat_to_int_bij = int_to_nat_bij" +by (simp add: i2n_n2i_id inv_equality n2i_i2n_id) + +lemma inv_int_to_nat_bij: "inv int_to_nat_bij = nat_to_int_bij" +by (simp add: i2n_n2i_id inv_equality n2i_i2n_id) + +lemma surj_nat_to_int_bij: "surj nat_to_int_bij" +by (blast intro: n2i_i2n_id surjI) + +lemma surj_int_to_nat_bij: "surj int_to_nat_bij" +by (blast intro: i2n_n2i_id surjI) + +lemma inj_nat_to_int_bij: "inj nat_to_int_bij" +by(simp add:inv_int_to_nat_bij[symmetric] surj_int_to_nat_bij surj_imp_inj_inv) + +lemma inj_int_to_nat_bij: "inj int_to_nat_bij" +by(simp add:inv_nat_to_int_bij[symmetric] surj_nat_to_int_bij surj_imp_inj_inv) + + +end diff -r 003dff7410c1 -r c92850d2d16c src/HOL/SET-Protocol/MessageSET.thy --- a/src/HOL/SET-Protocol/MessageSET.thy Tue Sep 02 22:20:27 2008 +0200 +++ b/src/HOL/SET-Protocol/MessageSET.thy Tue Sep 02 22:37:20 2008 +0200 @@ -6,7 +6,7 @@ header{*The Message Theory, Modified for SET*} theory MessageSET -imports Main NatPair +imports Main begin subsection{*General Lemmas*} diff -r 003dff7410c1 -r c92850d2d16c src/HOL/SET-Protocol/ROOT.ML --- a/src/HOL/SET-Protocol/ROOT.ML Tue Sep 02 22:20:27 2008 +0200 +++ b/src/HOL/SET-Protocol/ROOT.ML Tue Sep 02 22:37:20 2008 +0200 @@ -6,5 +6,4 @@ Root file for the SET protocol proofs. *) -no_document use_thy "NatPair"; use_thys ["Cardholder_Registration", "Merchant_Registration", "Purchase"]; diff -r 003dff7410c1 -r c92850d2d16c src/HOL/ex/ExecutableContent.thy --- a/src/HOL/ex/ExecutableContent.thy Tue Sep 02 22:20:27 2008 +0200 +++ b/src/HOL/ex/ExecutableContent.thy Tue Sep 02 22:37:20 2008 +0200 @@ -14,7 +14,6 @@ Eval List_Prefix Nat_Infinity - NatPair Nested_Environment Option_ord Permutation diff -r 003dff7410c1 -r c92850d2d16c src/HOL/ex/ROOT.ML --- a/src/HOL/ex/ROOT.ML Tue Sep 02 22:20:27 2008 +0200 +++ b/src/HOL/ex/ROOT.ML Tue Sep 02 22:37:20 2008 +0200 @@ -92,8 +92,7 @@ no_document use_thys [ "../NumberTheory/Factorization", - "../Library/BigO", - "../Library/NatPair" + "../Library/BigO" ]; use_thys [