wenzelm@11355: (* Title: HOL/Library/Nat_Infinity.thy haftmann@27110: Author: David von Oheimb, TU Muenchen; Florian Haftmann, TU Muenchen oheimb@11351: *) oheimb@11351: wenzelm@14706: header {* Natural numbers with infinity *} oheimb@11351: nipkow@15131: theory Nat_Infinity haftmann@30663: imports Main nipkow@15131: begin oheimb@11351: haftmann@27110: subsection {* Type definition *} oheimb@11351: oheimb@11351: text {* wenzelm@11355: We extend the standard natural numbers by a special value indicating haftmann@27110: infinity. oheimb@11351: *} oheimb@11351: oheimb@11351: datatype inat = Fin nat | Infty oheimb@11351: wenzelm@21210: notation (xsymbols) wenzelm@19736: Infty ("\") wenzelm@19736: wenzelm@21210: notation (HTML output) wenzelm@19736: Infty ("\") wenzelm@19736: oheimb@11351: nipkow@31077: lemma not_Infty_eq[simp]: "(x ~= Infty) = (EX i. x = Fin i)" nipkow@31077: by (cases x) auto nipkow@31077: nipkow@31077: haftmann@27110: subsection {* Constructors and numbers *} haftmann@27110: haftmann@27110: instantiation inat :: "{zero, one, number}" haftmann@25594: begin haftmann@25594: haftmann@25594: definition haftmann@27110: "0 = Fin 0" haftmann@25594: haftmann@25594: definition haftmann@27110: [code inline]: "1 = Fin 1" haftmann@25594: haftmann@25594: definition haftmann@28562: [code inline, code del]: "number_of k = Fin (number_of k)" oheimb@11351: haftmann@25594: instance .. haftmann@25594: haftmann@25594: end haftmann@25594: haftmann@27110: definition iSuc :: "inat \ inat" where haftmann@27110: "iSuc i = (case i of Fin n \ Fin (Suc n) | \ \ \)" oheimb@11351: oheimb@11351: lemma Fin_0: "Fin 0 = 0" haftmann@27110: by (simp add: zero_inat_def) haftmann@27110: haftmann@27110: lemma Fin_1: "Fin 1 = 1" haftmann@27110: by (simp add: one_inat_def) haftmann@27110: haftmann@27110: lemma Fin_number: "Fin (number_of k) = number_of k" haftmann@27110: by (simp add: number_of_inat_def) haftmann@27110: haftmann@27110: lemma one_iSuc: "1 = iSuc 0" haftmann@27110: by (simp add: zero_inat_def one_inat_def iSuc_def) oheimb@11351: oheimb@11351: lemma Infty_ne_i0 [simp]: "\ \ 0" haftmann@27110: by (simp add: zero_inat_def) oheimb@11351: oheimb@11351: lemma i0_ne_Infty [simp]: "0 \ \" haftmann@27110: by (simp add: zero_inat_def) haftmann@27110: haftmann@27110: lemma zero_inat_eq [simp]: haftmann@27110: "number_of k = (0\inat) \ number_of k = (0\nat)" haftmann@27110: "(0\inat) = number_of k \ number_of k = (0\nat)" haftmann@27110: unfolding zero_inat_def number_of_inat_def by simp_all haftmann@27110: haftmann@27110: lemma one_inat_eq [simp]: haftmann@27110: "number_of k = (1\inat) \ number_of k = (1\nat)" haftmann@27110: "(1\inat) = number_of k \ number_of k = (1\nat)" haftmann@27110: unfolding one_inat_def number_of_inat_def by simp_all haftmann@27110: haftmann@27110: lemma zero_one_inat_neq [simp]: haftmann@27110: "\ 0 = (1\inat)" haftmann@27110: "\ 1 = (0\inat)" haftmann@27110: unfolding zero_inat_def one_inat_def by simp_all oheimb@11351: haftmann@27110: lemma Infty_ne_i1 [simp]: "\ \ 1" haftmann@27110: by (simp add: one_inat_def) haftmann@27110: haftmann@27110: lemma i1_ne_Infty [simp]: "1 \ \" haftmann@27110: by (simp add: one_inat_def) haftmann@27110: haftmann@27110: lemma Infty_ne_number [simp]: "\ \ number_of k" haftmann@27110: by (simp add: number_of_inat_def) haftmann@27110: haftmann@27110: lemma number_ne_Infty [simp]: "number_of k \ \" haftmann@27110: by (simp add: number_of_inat_def) haftmann@27110: haftmann@27110: lemma iSuc_Fin: "iSuc (Fin n) = Fin (Suc n)" haftmann@27110: by (simp add: iSuc_def) haftmann@27110: haftmann@27110: lemma iSuc_number_of: "iSuc (number_of k) = Fin (Suc (number_of k))" haftmann@27110: by (simp add: iSuc_Fin number_of_inat_def) oheimb@11351: oheimb@11351: lemma iSuc_Infty [simp]: "iSuc \ = \" haftmann@27110: by (simp add: iSuc_def) oheimb@11351: oheimb@11351: lemma iSuc_ne_0 [simp]: "iSuc n \ 0" haftmann@27110: by (simp add: iSuc_def zero_inat_def split: inat.splits) haftmann@27110: haftmann@27110: lemma zero_ne_iSuc [simp]: "0 \ iSuc n" haftmann@27110: by (rule iSuc_ne_0 [symmetric]) oheimb@11351: haftmann@27110: lemma iSuc_inject [simp]: "iSuc m = iSuc n \ m = n" haftmann@27110: by (simp add: iSuc_def split: inat.splits) haftmann@27110: haftmann@27110: lemma number_of_inat_inject [simp]: haftmann@27110: "(number_of k \ inat) = number_of l \ (number_of k \ nat) = number_of l" haftmann@27110: by (simp add: number_of_inat_def) oheimb@11351: oheimb@11351: haftmann@27110: subsection {* Addition *} haftmann@27110: haftmann@27110: instantiation inat :: comm_monoid_add haftmann@27110: begin haftmann@27110: haftmann@27110: definition haftmann@27110: [code del]: "m + n = (case m of \ \ \ | Fin m \ (case n of \ \ \ | Fin n \ Fin (m + n)))" oheimb@11351: haftmann@27110: lemma plus_inat_simps [simp, code]: haftmann@27110: "Fin m + Fin n = Fin (m + n)" haftmann@27110: "\ + q = \" haftmann@27110: "q + \ = \" haftmann@27110: by (simp_all add: plus_inat_def split: inat.splits) haftmann@27110: haftmann@27110: instance proof haftmann@27110: fix n m q :: inat haftmann@27110: show "n + m + q = n + (m + q)" haftmann@27110: by (cases n, auto, cases m, auto, cases q, auto) haftmann@27110: show "n + m = m + n" haftmann@27110: by (cases n, auto, cases m, auto) haftmann@27110: show "0 + n = n" haftmann@27110: by (cases n) (simp_all add: zero_inat_def) huffman@26089: qed huffman@26089: haftmann@27110: end oheimb@11351: haftmann@27110: lemma plus_inat_0 [simp]: haftmann@27110: "0 + (q\inat) = q" haftmann@27110: "(q\inat) + 0 = q" haftmann@27110: by (simp_all add: plus_inat_def zero_inat_def split: inat.splits) oheimb@11351: haftmann@27110: lemma plus_inat_number [simp]: huffman@29012: "(number_of k \ inat) + number_of l = (if k < Int.Pls then number_of l huffman@29012: else if l < Int.Pls then number_of k else number_of (k + l))" haftmann@27110: unfolding number_of_inat_def plus_inat_simps nat_arith(1) if_distrib [symmetric, of _ Fin] .. oheimb@11351: haftmann@27110: lemma iSuc_number [simp]: haftmann@27110: "iSuc (number_of k) = (if neg (number_of k \ int) then 1 else number_of (Int.succ k))" haftmann@27110: unfolding iSuc_number_of haftmann@27110: unfolding one_inat_def number_of_inat_def Suc_nat_number_of if_distrib [symmetric] .. oheimb@11351: haftmann@27110: lemma iSuc_plus_1: haftmann@27110: "iSuc n = n + 1" haftmann@27110: by (cases n) (simp_all add: iSuc_Fin one_inat_def) haftmann@27110: haftmann@27110: lemma plus_1_iSuc: haftmann@27110: "1 + q = iSuc q" haftmann@27110: "q + 1 = iSuc q" haftmann@27110: unfolding iSuc_plus_1 by (simp_all add: add_ac) oheimb@11351: oheimb@11351: huffman@29014: subsection {* Multiplication *} huffman@29014: huffman@29014: instantiation inat :: comm_semiring_1 huffman@29014: begin huffman@29014: huffman@29014: definition huffman@29014: times_inat_def [code del]: huffman@29014: "m * n = (case m of \ \ if n = 0 then 0 else \ | Fin m \ huffman@29014: (case n of \ \ if m = 0 then 0 else \ | Fin n \ Fin (m * n)))" huffman@29014: huffman@29014: lemma times_inat_simps [simp, code]: huffman@29014: "Fin m * Fin n = Fin (m * n)" huffman@29014: "\ * \ = \" huffman@29014: "\ * Fin n = (if n = 0 then 0 else \)" huffman@29014: "Fin m * \ = (if m = 0 then 0 else \)" huffman@29014: unfolding times_inat_def zero_inat_def huffman@29014: by (simp_all split: inat.split) huffman@29014: huffman@29014: instance proof huffman@29014: fix a b c :: inat huffman@29014: show "(a * b) * c = a * (b * c)" huffman@29014: unfolding times_inat_def zero_inat_def huffman@29014: by (simp split: inat.split) huffman@29014: show "a * b = b * a" huffman@29014: unfolding times_inat_def zero_inat_def huffman@29014: by (simp split: inat.split) huffman@29014: show "1 * a = a" huffman@29014: unfolding times_inat_def zero_inat_def one_inat_def huffman@29014: by (simp split: inat.split) huffman@29014: show "(a + b) * c = a * c + b * c" huffman@29014: unfolding times_inat_def zero_inat_def huffman@29014: by (simp split: inat.split add: left_distrib) huffman@29014: show "0 * a = 0" huffman@29014: unfolding times_inat_def zero_inat_def huffman@29014: by (simp split: inat.split) huffman@29014: show "a * 0 = 0" huffman@29014: unfolding times_inat_def zero_inat_def huffman@29014: by (simp split: inat.split) huffman@29014: show "(0::inat) \ 1" huffman@29014: unfolding zero_inat_def one_inat_def huffman@29014: by simp huffman@29014: qed huffman@29014: huffman@29014: end huffman@29014: huffman@29014: lemma mult_iSuc: "iSuc m * n = n + m * n" nipkow@29667: unfolding iSuc_plus_1 by (simp add: algebra_simps) huffman@29014: huffman@29014: lemma mult_iSuc_right: "m * iSuc n = m + m * n" nipkow@29667: unfolding iSuc_plus_1 by (simp add: algebra_simps) huffman@29014: huffman@29023: lemma of_nat_eq_Fin: "of_nat n = Fin n" huffman@29023: apply (induct n) huffman@29023: apply (simp add: Fin_0) huffman@29023: apply (simp add: plus_1_iSuc iSuc_Fin) huffman@29023: done huffman@29023: huffman@29023: instance inat :: semiring_char_0 huffman@29023: by default (simp add: of_nat_eq_Fin) huffman@29023: huffman@29014: haftmann@27110: subsection {* Ordering *} haftmann@27110: haftmann@27110: instantiation inat :: ordered_ab_semigroup_add haftmann@27110: begin oheimb@11351: haftmann@27110: definition haftmann@27110: [code del]: "m \ n = (case n of Fin n1 \ (case m of Fin m1 \ m1 \ n1 | \ \ False) haftmann@27110: | \ \ True)" oheimb@11351: haftmann@27110: definition haftmann@27110: [code del]: "m < n = (case m of Fin m1 \ (case n of Fin n1 \ m1 < n1 | \ \ True) haftmann@27110: | \ \ False)" oheimb@11351: haftmann@27110: lemma inat_ord_simps [simp]: haftmann@27110: "Fin m \ Fin n \ m \ n" haftmann@27110: "Fin m < Fin n \ m < n" haftmann@27110: "q \ \" haftmann@27110: "q < \ \ q \ \" haftmann@27110: "\ \ q \ q = \" haftmann@27110: "\ < q \ False" haftmann@27110: by (simp_all add: less_eq_inat_def less_inat_def split: inat.splits) oheimb@11351: haftmann@27110: lemma inat_ord_code [code]: haftmann@27110: "Fin m \ Fin n \ m \ n" haftmann@27110: "Fin m < Fin n \ m < n" haftmann@27110: "q \ \ \ True" haftmann@27110: "Fin m < \ \ True" haftmann@27110: "\ \ Fin n \ False" haftmann@27110: "\ < q \ False" haftmann@27110: by simp_all oheimb@11351: haftmann@27110: instance by default haftmann@27110: (auto simp add: less_eq_inat_def less_inat_def plus_inat_def split: inat.splits) oheimb@11351: haftmann@27110: end haftmann@27110: nipkow@31077: instance inat :: linorder nipkow@31077: by intro_classes (auto simp add: less_eq_inat_def split: inat.splits) nipkow@31077: huffman@29014: instance inat :: pordered_comm_semiring huffman@29014: proof huffman@29014: fix a b c :: inat huffman@29014: assume "a \ b" and "0 \ c" huffman@29014: thus "c * a \ c * b" huffman@29014: unfolding times_inat_def less_eq_inat_def zero_inat_def huffman@29014: by (simp split: inat.splits) huffman@29014: qed huffman@29014: haftmann@27110: lemma inat_ord_number [simp]: haftmann@27110: "(number_of m \ inat) \ number_of n \ (number_of m \ nat) \ number_of n" haftmann@27110: "(number_of m \ inat) < number_of n \ (number_of m \ nat) < number_of n" haftmann@27110: by (simp_all add: number_of_inat_def) oheimb@11351: haftmann@27110: lemma i0_lb [simp]: "(0\inat) \ n" haftmann@27110: by (simp add: zero_inat_def less_eq_inat_def split: inat.splits) oheimb@11351: haftmann@27110: lemma i0_neq [simp]: "n \ (0\inat) \ n = 0" haftmann@27110: by (simp add: zero_inat_def less_eq_inat_def split: inat.splits) haftmann@27110: haftmann@27110: lemma Infty_ileE [elim!]: "\ \ Fin m \ R" haftmann@27110: by (simp add: zero_inat_def less_eq_inat_def split: inat.splits) oheimb@11351: haftmann@27110: lemma Infty_ilessE [elim!]: "\ < Fin m \ R" haftmann@27110: by simp oheimb@11351: haftmann@27110: lemma not_ilessi0 [simp]: "\ n < (0\inat)" haftmann@27110: by (simp add: zero_inat_def less_inat_def split: inat.splits) haftmann@27110: haftmann@27110: lemma i0_eq [simp]: "(0\inat) < n \ n \ 0" haftmann@27110: by (simp add: zero_inat_def less_inat_def split: inat.splits) oheimb@11351: haftmann@27110: lemma iSuc_ile_mono [simp]: "iSuc n \ iSuc m \ n \ m" haftmann@27110: by (simp add: iSuc_def less_eq_inat_def split: inat.splits) haftmann@27110: haftmann@27110: lemma iSuc_mono [simp]: "iSuc n < iSuc m \ n < m" haftmann@27110: by (simp add: iSuc_def less_inat_def split: inat.splits) oheimb@11351: haftmann@27110: lemma ile_iSuc [simp]: "n \ iSuc n" haftmann@27110: by (simp add: iSuc_def less_eq_inat_def split: inat.splits) oheimb@11351: wenzelm@11355: lemma not_iSuc_ilei0 [simp]: "\ iSuc n \ 0" haftmann@27110: by (simp add: zero_inat_def iSuc_def less_eq_inat_def split: inat.splits) haftmann@27110: haftmann@27110: lemma i0_iless_iSuc [simp]: "0 < iSuc n" haftmann@27110: by (simp add: zero_inat_def iSuc_def less_inat_def split: inat.splits) haftmann@27110: haftmann@27110: lemma ileI1: "m < n \ iSuc m \ n" haftmann@27110: by (simp add: iSuc_def less_eq_inat_def less_inat_def split: inat.splits) haftmann@27110: haftmann@27110: lemma Suc_ile_eq: "Fin (Suc m) \ n \ Fin m < n" haftmann@27110: by (cases n) auto haftmann@27110: haftmann@27110: lemma iless_Suc_eq [simp]: "Fin m < iSuc n \ Fin m \ n" haftmann@27110: by (auto simp add: iSuc_def less_inat_def split: inat.splits) oheimb@11351: haftmann@27110: lemma min_inat_simps [simp]: haftmann@27110: "min (Fin m) (Fin n) = Fin (min m n)" haftmann@27110: "min q 0 = 0" haftmann@27110: "min 0 q = 0" haftmann@27110: "min q \ = q" haftmann@27110: "min \ q = q" haftmann@27110: by (auto simp add: min_def) oheimb@11351: haftmann@27110: lemma max_inat_simps [simp]: haftmann@27110: "max (Fin m) (Fin n) = Fin (max m n)" haftmann@27110: "max q 0 = q" haftmann@27110: "max 0 q = q" haftmann@27110: "max q \ = \" haftmann@27110: "max \ q = \" haftmann@27110: by (simp_all add: max_def) haftmann@27110: haftmann@27110: lemma Fin_ile: "n \ Fin m \ \k. n = Fin k" haftmann@27110: by (cases n) simp_all haftmann@27110: haftmann@27110: lemma Fin_iless: "n < Fin m \ \k. n = Fin k" haftmann@27110: by (cases n) simp_all oheimb@11351: oheimb@11351: lemma chain_incr: "\i. \j. Y i < Y j ==> \j. Fin k < Y j" nipkow@25134: apply (induct_tac k) nipkow@25134: apply (simp (no_asm) only: Fin_0) haftmann@27110: apply (fast intro: le_less_trans [OF i0_lb]) nipkow@25134: apply (erule exE) nipkow@25134: apply (drule spec) nipkow@25134: apply (erule exE) nipkow@25134: apply (drule ileI1) nipkow@25134: apply (rule iSuc_Fin [THEN subst]) nipkow@25134: apply (rule exI) haftmann@27110: apply (erule (1) le_less_trans) nipkow@25134: done oheimb@11351: haftmann@29337: instantiation inat :: "{bot, top}" haftmann@29337: begin haftmann@29337: haftmann@29337: definition bot_inat :: inat where haftmann@29337: "bot_inat = 0" haftmann@29337: haftmann@29337: definition top_inat :: inat where haftmann@29337: "top_inat = \" haftmann@29337: haftmann@29337: instance proof haftmann@29337: qed (simp_all add: bot_inat_def top_inat_def) haftmann@29337: haftmann@29337: end haftmann@29337: huffman@26089: haftmann@27110: subsection {* Well-ordering *} huffman@26089: huffman@26089: lemma less_FinE: huffman@26089: "[| n < Fin m; !!k. n = Fin k ==> k < m ==> P |] ==> P" huffman@26089: by (induct n) auto huffman@26089: huffman@26089: lemma less_InftyE: huffman@26089: "[| n < Infty; !!k. n = Fin k ==> P |] ==> P" huffman@26089: by (induct n) auto huffman@26089: huffman@26089: lemma inat_less_induct: huffman@26089: assumes prem: "!!n. \m::inat. m < n --> P m ==> P n" shows "P n" huffman@26089: proof - huffman@26089: have P_Fin: "!!k. P (Fin k)" huffman@26089: apply (rule nat_less_induct) huffman@26089: apply (rule prem, clarify) huffman@26089: apply (erule less_FinE, simp) huffman@26089: done huffman@26089: show ?thesis huffman@26089: proof (induct n) huffman@26089: fix nat huffman@26089: show "P (Fin nat)" by (rule P_Fin) huffman@26089: next huffman@26089: show "P Infty" huffman@26089: apply (rule prem, clarify) huffman@26089: apply (erule less_InftyE) huffman@26089: apply (simp add: P_Fin) huffman@26089: done huffman@26089: qed huffman@26089: qed huffman@26089: huffman@26089: instance inat :: wellorder huffman@26089: proof haftmann@27823: fix P and n haftmann@27823: assume hyp: "(\n\inat. (\m\inat. m < n \ P m) \ P n)" haftmann@27823: show "P n" by (blast intro: inat_less_induct hyp) huffman@26089: qed huffman@26089: haftmann@27110: haftmann@27110: subsection {* Traditional theorem names *} haftmann@27110: haftmann@27110: lemmas inat_defs = zero_inat_def one_inat_def number_of_inat_def iSuc_def haftmann@27110: plus_inat_def less_eq_inat_def less_inat_def haftmann@27110: haftmann@27110: lemmas inat_splits = inat.splits haftmann@27110: nipkow@31077: nipkow@31077: instance inat :: linorder nipkow@31077: by intro_classes (auto simp add: inat_defs split: inat.splits) nipkow@31077: oheimb@11351: end