summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

src/HOL/Library/NatPair.thy

author | nipkow |

Wed, 18 Aug 2004 11:09:40 +0200 | |

changeset 15140 | 322485b816ac |

parent 15131 | c69542757a4d |

child 19736 | d8d0f8f51d69 |

permissions | -rw-r--r-- |

import -> imports

(* 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{* An injective function from @{text "\<nat>\<twosuperior>"} to @{text \<nat>}. Definition and proofs are from \cite[page 85]{Oberschelp:1993}. *} constdefs nat2_to_nat:: "(nat * nat) \<Rightarrow> nat" "nat2_to_nat pair \<equiv> let (n,m) = pair in (n+m) * Suc (n+m) div 2 + n" lemma dvd2_a_x_suc_a: "2 dvd a * (Suc a)" proof (cases "2 dvd a") case True thus ?thesis by (rule dvd_mult2) next case False hence "Suc (a mod 2) = 2" by (simp add: dvd_eq_mod_eq_0) hence "Suc a mod 2 = 0" by (simp add: mod_Suc) hence "2 dvd Suc a" by (simp only:dvd_eq_mod_eq_0) thus ?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 \<le> x+y" proof (rule classical) assume "\<not> ?thesis" hence 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 "\<dots> = (x+y)*Suc(x+y) div 2 + 2 * Suc(x+y) div 2" by (simp only: div_mult_self1_is_m) also have "\<dots> = (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) hence "(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 thus ?thesis by simp qed also have "\<dots> = ((x+y)*Suc(x+y) + 2*Suc(x+y)) div 2" by (rule div_add1_eq [symmetric]) also have "\<dots> = ((x+y+2)*Suc(x+y)) div 2" by (simp only: add_mult_distrib [symmetric]) also from contrapos have "\<dots> \<le> ((Suc(u+v))*(u+v)) div 2" by (simp only: mult_le_mono div_le_mono) also have "\<dots> \<le> 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 "nat2_to_nat (u,v) = nat2_to_nat (x,y)" hence "u+v \<le> x+y" by (rule nat2_to_nat_help) also from prems [symmetric] have "x+y \<le> u+v" by (rule nat2_to_nat_help) finally have eq: "u+v = x+y" . with prems have ux: "u=x" by (simp add: nat2_to_nat_def Let_def) with eq have vy: "v=y" by simp with ux have "(u,v) = (x,y)" by simp } hence "\<And>x y. nat2_to_nat x = nat2_to_nat y \<Longrightarrow> x=y" by fast thus ?thesis by (unfold inj_on_def) simp qed end