paulson@14127: (*  Title:      HOL/Library/NatPair.thy
paulson@14127:     ID:         $Id$
nipkow@14414:     Author:     Stefan Richter
nipkow@14414:     Copyright   2003 Technische Universitaet Muenchen
paulson@14127: *)
paulson@14127: 
wenzelm@14706: header {* Pairs of Natural Numbers *}
paulson@14127: 
nipkow@15131: theory NatPair
nipkow@15131: import Main
nipkow@15131: begin
paulson@14127: 
wenzelm@14706: text{*
wenzelm@14706:   An injective function from @{text "\<nat>\<twosuperior>"} to @{text
wenzelm@14706:   \<nat>}.  Definition and proofs are from \cite[page
wenzelm@14706:   85]{Oberschelp:1993}.
wenzelm@14706: *}
paulson@14127: 
wenzelm@14706: constdefs
paulson@14127:   nat2_to_nat:: "(nat * nat) \<Rightarrow> nat"
paulson@14127:   "nat2_to_nat pair \<equiv> let (n,m) = pair in (n+m) * Suc (n+m) div 2 + n"
paulson@14127: 
wenzelm@14706: lemma dvd2_a_x_suc_a: "2 dvd a * (Suc a)"
wenzelm@14706: proof (cases "2 dvd a")
paulson@14127:   case True
paulson@14127:   thus ?thesis by (rule dvd_mult2)
paulson@14127: next
wenzelm@14706:   case False
paulson@14127:   hence "Suc (a mod 2) = 2" by (simp add: dvd_eq_mod_eq_0)
wenzelm@14706:   hence "Suc a mod 2 = 0" by (simp add: mod_Suc)
wenzelm@14706:   hence "2 dvd Suc a" by (simp only:dvd_eq_mod_eq_0)
paulson@14127:   thus ?thesis by (rule dvd_mult)
paulson@14127: qed
paulson@14127: 
wenzelm@14706: lemma
wenzelm@14706:   assumes eq: "nat2_to_nat (u,v) = nat2_to_nat (x,y)"
paulson@14127:   shows nat2_to_nat_help: "u+v \<le> x+y"
paulson@14127: proof (rule classical)
paulson@14127:   assume "\<not> ?thesis"
wenzelm@14706:   hence contrapos: "x+y < u+v"
paulson@14127:     by simp
wenzelm@14706:   have "nat2_to_nat (x,y) < (x+y) * Suc (x+y) div 2 + Suc (x + y)"
paulson@14127:     by (unfold nat2_to_nat_def) (simp add: Let_def)
wenzelm@14706:   also have "\<dots> = (x+y)*Suc(x+y) div 2 + 2 * Suc(x+y) div 2"
wenzelm@14706:     by (simp only: div_mult_self1_is_m)
wenzelm@14706:   also have "\<dots> = (x+y)*Suc(x+y) div 2 + 2 * Suc(x+y) div 2
wenzelm@14706:     + ((x+y)*Suc(x+y) mod 2 + 2 * Suc(x+y) mod 2) div 2"
paulson@14127:   proof -
wenzelm@14706:     have "2 dvd (x+y)*Suc(x+y)"
paulson@14127:       by (rule dvd2_a_x_suc_a)
wenzelm@14706:     hence "(x+y)*Suc(x+y) mod 2 = 0"
paulson@14127:       by (simp only: dvd_eq_mod_eq_0)
paulson@14127:     also
wenzelm@14706:     have "2 * Suc(x+y) mod 2 = 0"
paulson@14127:       by (rule mod_mult_self1_is_0)
wenzelm@14706:     ultimately have
wenzelm@14706:       "((x+y)*Suc(x+y) mod 2 + 2 * Suc(x+y) mod 2) div 2 = 0"
wenzelm@14706:       by simp
wenzelm@14706:     thus ?thesis
paulson@14127:       by simp
wenzelm@14706:   qed
wenzelm@14706:   also have "\<dots> = ((x+y)*Suc(x+y) + 2*Suc(x+y)) div 2"
wenzelm@14706:     by (rule div_add1_eq [symmetric])
wenzelm@14706:   also have "\<dots> = ((x+y+2)*Suc(x+y)) div 2"
wenzelm@14706:     by (simp only: add_mult_distrib [symmetric])
wenzelm@14706:   also from contrapos have "\<dots> \<le> ((Suc(u+v))*(u+v)) div 2"
wenzelm@14706:     by (simp only: mult_le_mono div_le_mono)
wenzelm@14706:   also have "\<dots> \<le> nat2_to_nat (u,v)"
paulson@14127:     by (unfold nat2_to_nat_def) (simp add: Let_def)
wenzelm@14706:   finally show ?thesis
paulson@14127:     by (simp only: eq)
paulson@14127: qed
paulson@14127: 
wenzelm@14706: theorem nat2_to_nat_inj: "inj nat2_to_nat"
paulson@14127: proof -
wenzelm@14706:   {
wenzelm@14706:     fix u v x y assume "nat2_to_nat (u,v) = nat2_to_nat (x,y)"
paulson@14127:     hence "u+v \<le> x+y" by (rule nat2_to_nat_help)
wenzelm@14706:     also from prems [symmetric] have "x+y \<le> u+v"
paulson@14127:       by (rule nat2_to_nat_help)
paulson@14127:     finally have eq: "u+v = x+y" .
wenzelm@14706:     with prems have ux: "u=x"
paulson@14127:       by (simp add: nat2_to_nat_def Let_def)
wenzelm@14706:     with eq have vy: "v=y"
paulson@14127:       by simp
wenzelm@14706:     with ux have "(u,v) = (x,y)"
paulson@14127:       by simp
paulson@14127:   }
wenzelm@14706:   hence "\<And>x y. nat2_to_nat x = nat2_to_nat y \<Longrightarrow> x=y"
paulson@14127:     by fast
wenzelm@14706:   thus ?thesis
paulson@14127:     by (unfold inj_on_def) simp
paulson@14127: qed
paulson@14127: 
paulson@14127: end