src/HOL/Nat.thy

simplified a proof

(*  Title:      HOL/Nat.thy
    ID:         $Id$
    Author:     Tobias Nipkow and Lawrence C Paulson and Markus Wenzel

Type "nat" is a linear order, and a datatype; arithmetic operators + -
and * (for div, mod and dvd, see theory Divides).
*)

header {* Natural numbers *}

theory Nat
imports Wellfounded_Recursion Ring_and_Field
uses
  "~~/src/Tools/rat.ML"
  "~~/src/Provers/Arith/fast_lin_arith.ML"
  "~~/src/Provers/Arith/cancel_sums.ML"
  ("arith_data.ML")
begin

subsection {* Type @{text ind} *}

typedecl ind

axiomatization
  Zero_Rep :: ind and
  Suc_Rep :: "ind => ind"
where
  -- {* the axiom of infinity in 2 parts *}
  inj_Suc_Rep:          "inj Suc_Rep" and
  Suc_Rep_not_Zero_Rep: "Suc_Rep x \<noteq> Zero_Rep"


subsection {* Type nat *}

text {* Type definition *}

inductive2 Nat :: "ind \<Rightarrow> bool"
where
    Zero_RepI: "Nat Zero_Rep"
  | Suc_RepI: "Nat i ==> Nat (Suc_Rep i)"

global

typedef (open Nat)
  nat = "Collect Nat"
proof
  from Nat.Zero_RepI
  show "Zero_Rep : Collect Nat" ..
qed

text {* Abstract constants and syntax *}

consts
  Suc :: "nat => nat"

local

defs
  Suc_def:      "Suc == (%n. Abs_Nat (Suc_Rep (Rep_Nat n)))"

definition
  pred_nat :: "(nat * nat) set" where
  "pred_nat = {(m, n). n = Suc m}"

instance nat :: "{ord, zero, one}"
  Zero_nat_def: "0 == Abs_Nat Zero_Rep"
  One_nat_def [simp]: "1 == Suc 0"
  less_def: "m < n == (m, n) : pred_nat^+"
  le_def:   "m \<le> (n::nat) == ~ (n < m)" ..

lemmas [code func del] = less_def le_def

text {* Induction *}

lemma Rep_Nat': "Nat (Rep_Nat x)"
  by (rule Rep_Nat [simplified mem_Collect_eq])

lemma Abs_Nat_inverse': "Nat y \<Longrightarrow> Rep_Nat (Abs_Nat y) = y"
  by (rule Abs_Nat_inverse [simplified mem_Collect_eq])

theorem nat_induct: "P 0 ==> (!!n. P n ==> P (Suc n)) ==> P n"
  apply (unfold Zero_nat_def Suc_def)
  apply (rule Rep_Nat_inverse [THEN subst]) -- {* types force good instantiation *}
  apply (erule Rep_Nat' [THEN Nat.induct])
  apply (iprover elim: Abs_Nat_inverse' [THEN subst])
  done

text {* Distinctness of constructors *}

lemma Suc_not_Zero [iff]: "Suc m \<noteq> 0"
  by (simp add: Zero_nat_def Suc_def Abs_Nat_inject Rep_Nat' Suc_RepI Zero_RepI
                Suc_Rep_not_Zero_Rep)

lemma Zero_not_Suc [iff]: "0 \<noteq> Suc m"
  by (rule not_sym, rule Suc_not_Zero not_sym)

lemma Suc_neq_Zero: "Suc m = 0 ==> R"
  by (rule notE, rule Suc_not_Zero)

lemma Zero_neq_Suc: "0 = Suc m ==> R"
  by (rule Suc_neq_Zero, erule sym)

text {* Injectiveness of @{term Suc} *}

lemma inj_Suc[simp]: "inj_on Suc N"
  by (simp add: Suc_def inj_on_def Abs_Nat_inject Rep_Nat' Suc_RepI
                inj_Suc_Rep [THEN inj_eq] Rep_Nat_inject)

lemma Suc_inject: "Suc x = Suc y ==> x = y"
  by (rule inj_Suc [THEN injD])

lemma Suc_Suc_eq [iff]: "(Suc m = Suc n) = (m = n)"
  by (rule inj_Suc [THEN inj_eq])

lemma nat_not_singleton: "(\<forall>x. x = (0::nat)) = False"
  by auto

text {* size of a datatype value *}

class size = type +
  fixes size :: "'a \<Rightarrow> nat"

text {* @{typ nat} is a datatype *}

rep_datatype nat
  distinct  Suc_not_Zero Zero_not_Suc
  inject    Suc_Suc_eq
  induction nat_induct

declare nat.induct [case_names 0 Suc, induct type: nat]
declare nat.exhaust [case_names 0 Suc, cases type: nat]

lemmas nat_rec_0 = nat.recs(1)
  and nat_rec_Suc = nat.recs(2)

lemmas nat_case_0 = nat.cases(1)
  and nat_case_Suc = nat.cases(2)


lemma n_not_Suc_n: "n \<noteq> Suc n"
  by (induct n) simp_all

lemma Suc_n_not_n: "Suc t \<noteq> t"
  by (rule not_sym, rule n_not_Suc_n)

text {* A special form of induction for reasoning
  about @{term "m < n"} and @{term "m - n"} *}

theorem diff_induct: "(!!x. P x 0) ==> (!!y. P 0 (Suc y)) ==>
    (!!x y. P x y ==> P (Suc x) (Suc y)) ==> P m n"
  apply (rule_tac x = m in spec)
  apply (induct n)
  prefer 2
  apply (rule allI)
  apply (induct_tac x, iprover+)
  done

subsection {* Basic properties of "less than" *}

lemma wf_pred_nat: "wf pred_nat"
  apply (unfold wf_def pred_nat_def, clarify)
  apply (induct_tac x, blast+)
  done

lemma wf_less: "wf {(x, y::nat). x < y}"
  apply (unfold less_def)
  apply (rule wf_pred_nat [THEN wf_trancl, THEN wf_subset], blast)
  done

lemma less_eq: "((m, n) : pred_nat^+) = (m < n)"
  apply (unfold less_def)
  apply (rule refl)
  done

subsubsection {* Introduction properties *}

lemma less_trans: "i < j ==> j < k ==> i < (k::nat)"
  apply (unfold less_def)
  apply (rule trans_trancl [THEN transD], assumption+)
  done

lemma lessI [iff]: "n < Suc n"
  apply (unfold less_def pred_nat_def)
  apply (simp add: r_into_trancl)
  done

lemma less_SucI: "i < j ==> i < Suc j"
  apply (rule less_trans, assumption)
  apply (rule lessI)
  done

lemma zero_less_Suc [iff]: "0 < Suc n"
  apply (induct n)
  apply (rule lessI)
  apply (erule less_trans)
  apply (rule lessI)
  done

subsubsection {* Elimination properties *}

lemma less_not_sym: "n < m ==> ~ m < (n::nat)"
  apply (unfold less_def)
  apply (blast intro: wf_pred_nat wf_trancl [THEN wf_asym])
  done

lemma less_asym:
  assumes h1: "(n::nat) < m" and h2: "~ P ==> m < n" shows P
  apply (rule contrapos_np)
  apply (rule less_not_sym)
  apply (rule h1)
  apply (erule h2)
  done

lemma less_not_refl: "~ n < (n::nat)"
  apply (unfold less_def)
  apply (rule wf_pred_nat [THEN wf_trancl, THEN wf_not_refl])
  done

lemma less_irrefl [elim!]: "(n::nat) < n ==> R"
  by (rule notE, rule less_not_refl)

lemma less_not_refl2: "n < m ==> m \<noteq> (n::nat)" by blast

lemma less_not_refl3: "(s::nat) < t ==> s \<noteq> t"
  by (rule not_sym, rule less_not_refl2)

lemma lessE:
  assumes major: "i < k"
  and p1: "k = Suc i ==> P" and p2: "!!j. i < j ==> k = Suc j ==> P"
  shows P
  apply (rule major [unfolded less_def pred_nat_def, THEN tranclE], simp_all)
  apply (erule p1)
  apply (rule p2)
  apply (simp add: less_def pred_nat_def, assumption)
  done

lemma not_less0 [iff]: "~ n < (0::nat)"
  by (blast elim: lessE)

lemma less_zeroE: "(n::nat) < 0 ==> R"
  by (rule notE, rule not_less0)

lemma less_SucE: assumes major: "m < Suc n"
  and less: "m < n ==> P" and eq: "m = n ==> P" shows P
  apply (rule major [THEN lessE])
  apply (rule eq, blast)
  apply (rule less, blast)
  done

lemma less_Suc_eq: "(m < Suc n) = (m < n | m = n)"
  by (blast elim!: less_SucE intro: less_trans)

lemma less_one [iff]: "(n < (1::nat)) = (n = 0)"
  by (simp add: less_Suc_eq)

lemma less_Suc0 [iff]: "(n < Suc 0) = (n = 0)"
  by (simp add: less_Suc_eq)

lemma Suc_mono: "m < n ==> Suc m < Suc n"
  by (induct n) (fast elim: less_trans lessE)+

text {* "Less than" is a linear ordering *}
lemma less_linear: "m < n | m = n | n < (m::nat)"
  apply (induct m)
  apply (induct n)
  apply (rule refl [THEN disjI1, THEN disjI2])
  apply (rule zero_less_Suc [THEN disjI1])
  apply (blast intro: Suc_mono less_SucI elim: lessE)
  done

text {* "Less than" is antisymmetric, sort of *}
lemma less_antisym: "\<lbrakk> \<not> n < m; n < Suc m \<rbrakk> \<Longrightarrow> m = n"
  apply(simp only:less_Suc_eq)
  apply blast
  done

lemma nat_neq_iff: "((m::nat) \<noteq> n) = (m < n | n < m)"
  using less_linear by blast

lemma nat_less_cases: assumes major: "(m::nat) < n ==> P n m"
  and eqCase: "m = n ==> P n m" and lessCase: "n<m ==> P n m"
  shows "P n m"
  apply (rule less_linear [THEN disjE])
  apply (erule_tac [2] disjE)
  apply (erule lessCase)
  apply (erule sym [THEN eqCase])
  apply (erule major)
  done


subsubsection {* Inductive (?) properties *}

lemma Suc_lessI: "m < n ==> Suc m \<noteq> n ==> Suc m < n"
  apply (simp add: nat_neq_iff)
  apply (blast elim!: less_irrefl less_SucE elim: less_asym)
  done

lemma Suc_lessD: "Suc m < n ==> m < n"
  apply (induct n)
  apply (fast intro!: lessI [THEN less_SucI] elim: less_trans lessE)+
  done

lemma Suc_lessE: assumes major: "Suc i < k"
  and minor: "!!j. i < j ==> k = Suc j ==> P" shows P
  apply (rule major [THEN lessE])
  apply (erule lessI [THEN minor])
  apply (erule Suc_lessD [THEN minor], assumption)
  done

lemma Suc_less_SucD: "Suc m < Suc n ==> m < n"
  by (blast elim: lessE dest: Suc_lessD)

lemma Suc_less_eq [iff, code]: "(Suc m < Suc n) = (m < n)"
  apply (rule iffI)
  apply (erule Suc_less_SucD)
  apply (erule Suc_mono)
  done

lemma less_trans_Suc:
  assumes le: "i < j" shows "j < k ==> Suc i < k"
  apply (induct k, simp_all)
  apply (insert le)
  apply (simp add: less_Suc_eq)
  apply (blast dest: Suc_lessD)
  done

lemma [code]: "((n::nat) < 0) = False" by simp
lemma [code]: "(0 < Suc n) = True" by simp

text {* Can be used with @{text less_Suc_eq} to get @{term "n = m | n < m"} *}
lemma not_less_eq: "(~ m < n) = (n < Suc m)"
  by (induct m n rule: diff_induct) simp_all

text {* Complete induction, aka course-of-values induction *}
lemma nat_less_induct:
  assumes prem: "!!n. \<forall>m::nat. m < n --> P m ==> P n" shows "P n"
  apply (induct n rule: wf_induct [OF wf_pred_nat [THEN wf_trancl]])
  apply (rule prem)
  apply (unfold less_def, assumption)
  done

lemmas less_induct = nat_less_induct [rule_format, case_names less]


subsection {* Properties of "less than or equal" *}

text {* Was @{text le_eq_less_Suc}, but this orientation is more useful *}
lemma less_Suc_eq_le: "(m < Suc n) = (m \<le> n)"
  unfolding le_def by (rule not_less_eq [symmetric])

lemma le_imp_less_Suc: "m \<le> n ==> m < Suc n"
  by (rule less_Suc_eq_le [THEN iffD2])

lemma le0 [iff]: "(0::nat) \<le> n"
  unfolding le_def by (rule not_less0)

lemma Suc_n_not_le_n: "~ Suc n \<le> n"
  by (simp add: le_def)

lemma le_0_eq [iff]: "((i::nat) \<le> 0) = (i = 0)"
  by (induct i) (simp_all add: le_def)

lemma le_Suc_eq: "(m \<le> Suc n) = (m \<le> n | m = Suc n)"
  by (simp del: less_Suc_eq_le add: less_Suc_eq_le [symmetric] less_Suc_eq)

lemma le_SucE: "m \<le> Suc n ==> (m \<le> n ==> R) ==> (m = Suc n ==> R) ==> R"
  by (drule le_Suc_eq [THEN iffD1], iprover+)

lemma Suc_leI: "m < n ==> Suc(m) \<le> n"
  apply (simp add: le_def less_Suc_eq)
  apply (blast elim!: less_irrefl less_asym)
  done -- {* formerly called lessD *}

lemma Suc_leD: "Suc(m) \<le> n ==> m \<le> n"
  by (simp add: le_def less_Suc_eq)

text {* Stronger version of @{text Suc_leD} *}
lemma Suc_le_lessD: "Suc m \<le> n ==> m < n"
  apply (simp add: le_def less_Suc_eq)
  using less_linear
  apply blast
  done

lemma Suc_le_eq: "(Suc m \<le> n) = (m < n)"
  by (blast intro: Suc_leI Suc_le_lessD)

lemma le_SucI: "m \<le> n ==> m \<le> Suc n"
  by (unfold le_def) (blast dest: Suc_lessD)

lemma less_imp_le: "m < n ==> m \<le> (n::nat)"
  by (unfold le_def) (blast elim: less_asym)

text {* For instance, @{text "(Suc m < Suc n) = (Suc m \<le> n) = (m < n)"} *}
lemmas le_simps = less_imp_le less_Suc_eq_le Suc_le_eq


text {* Equivalence of @{term "m \<le> n"} and @{term "m < n | m = n"} *}

lemma le_imp_less_or_eq: "m \<le> n ==> m < n | m = (n::nat)"
  unfolding le_def
  using less_linear
  by (blast elim: less_irrefl less_asym)

lemma less_or_eq_imp_le: "m < n | m = n ==> m \<le> (n::nat)"
  unfolding le_def
  using less_linear
  by (blast elim!: less_irrefl elim: less_asym)

lemma le_eq_less_or_eq: "(m \<le> (n::nat)) = (m < n | m=n)"
  by (iprover intro: less_or_eq_imp_le le_imp_less_or_eq)

text {* Useful with @{text blast}. *}
lemma eq_imp_le: "(m::nat) = n ==> m \<le> n"
  by (rule less_or_eq_imp_le) (rule disjI2)

lemma le_refl: "n \<le> (n::nat)"
  by (simp add: le_eq_less_or_eq)