# Theory Nat

Up to index of Isabelle/ZF

theory Nat
imports OrdQuant Bool
begin

    (*  Title:      ZF/Nat.thy
        ID:         $Id: Nat.thy,v 1.26 2005/06/17 14:15:09 haftmann Exp $
        Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
        Copyright   1994  University of Cambridge

    *)

    header{*The Natural numbers As a Least Fixed Point*}

    theory Nat imports OrdQuant Bool begin

    constdefs
      nat :: i
        "nat == lfp(Inf, %X. {0} Un {succ(i). i:X})"

      quasinat :: "i => o"
        "quasinat(n) == n=0 | (∃m. n = succ(m))"

      (*Has an unconditional succ case, which is used in "recursor" below.*)
      nat_case :: "[i, i=>i, i]=>i"
        "nat_case(a,b,k) == THE y. k=0 & y=a | (EX x. k=succ(x) & y=b(x))"

      nat_rec :: "[i, i, [i,i]=>i]=>i"
        "nat_rec(k,a,b) ==
              wfrec(Memrel(nat), k, %n f. nat_case(a, %m. b(m, f`m), n))"

      (*Internalized relations on the naturals*)

      Le :: i
        "Le == {<x,y>:nat*nat. x le y}"

      Lt :: i
        "Lt == {<x, y>:nat*nat. x < y}"

      Ge :: i
        "Ge == {<x,y>:nat*nat. y le x}"

      Gt :: i
        "Gt == {<x,y>:nat*nat. y < x}"

      greater_than :: "i=>i"
        "greater_than(n) == {i:nat. n < i}"

    text{*No need for a less-than operator: a natural number is its list of
    predecessors!*}

    lemma nat_bnd_mono: "bnd_mono(Inf, %X. {0} Un {succ(i). i:X})"
    apply (rule bnd_monoI)
    apply (cut_tac infinity, blast, blast)
    done

    (* nat = {0} Un {succ(x). x:nat} *)
    lemmas nat_unfold = nat_bnd_mono [THEN nat_def [THEN def_lfp_unfold], standard]

    (** Type checking of 0 and successor **)

    lemma nat_0I [iff,TC]: "0 : nat"
    apply (subst nat_unfold)
    apply (rule singletonI [THEN UnI1])
    done

    lemma nat_succI [intro!,TC]: "n : nat ==> succ(n) : nat"
    apply (subst nat_unfold)
    apply (erule RepFunI [THEN UnI2])
    done

    lemma nat_1I [iff,TC]: "1 : nat"
    by (rule nat_0I [THEN nat_succI])

    lemma nat_2I [iff,TC]: "2 : nat"
    by (rule nat_1I [THEN nat_succI])

    lemma bool_subset_nat: "bool <= nat"
    by (blast elim!: boolE)

    lemmas bool_into_nat = bool_subset_nat [THEN subsetD, standard]

    subsection{*Injectivity Properties and Induction*}

    (*Mathematical induction*)
    lemma nat_induct [case_names 0 succ, induct set: nat]:
        "[| n: nat;  P(0);  !!x. [| x: nat;  P(x) |] ==> P(succ(x)) |] ==> P(n)"
    by (erule def_induct [OF nat_def nat_bnd_mono], blast)

    lemma natE:
        "[| n: nat;  n=0 ==> P;  !!x. [| x: nat; n=succ(x) |] ==> P |] ==> P"
    by (erule nat_unfold [THEN equalityD1, THEN subsetD, THEN UnE], auto)

    lemma nat_into_Ord [simp]: "n: nat ==> Ord(n)"
    by (erule nat_induct, auto)

    (* i: nat ==> 0 le i; same thing as 0<succ(i)  *)
    lemmas nat_0_le = nat_into_Ord [THEN Ord_0_le, standard]

    (* i: nat ==> i le i; same thing as i<succ(i)  *)
    lemmas nat_le_refl = nat_into_Ord [THEN le_refl, standard]

    lemma Ord_nat [iff]: "Ord(nat)"
    apply (rule OrdI)
    apply (erule_tac [2] nat_into_Ord [THEN Ord_is_Transset])
    apply (unfold Transset_def)
    apply (rule ballI)
    apply (erule nat_induct, auto)
    done

    lemma Limit_nat [iff]: "Limit(nat)"
    apply (unfold Limit_def)
    apply (safe intro!: ltI Ord_nat)
    apply (erule ltD)
    done

    lemma naturals_not_limit: "a ∈ nat ==> ~ Limit(a)"
    by (induct a rule: nat_induct, auto)

    lemma succ_natD: "succ(i): nat ==> i: nat"
    by (rule Ord_trans [OF succI1], auto)

    lemma nat_succ_iff [iff]: "succ(n): nat <-> n: nat"
    by (blast dest!: succ_natD)

    lemma nat_le_Limit: "Limit(i) ==> nat le i"
    apply (rule subset_imp_le)
    apply (simp_all add: Limit_is_Ord)
    apply (rule subsetI)
    apply (erule nat_induct)
     apply (erule Limit_has_0 [THEN ltD])
    apply (blast intro: Limit_has_succ [THEN ltD] ltI Limit_is_Ord)
    done

    (* [| succ(i): k;  k: nat |] ==> i: k *)
    lemmas succ_in_naturalD = Ord_trans [OF succI1 _ nat_into_Ord]

    lemma lt_nat_in_nat: "[| m<n;  n: nat |] ==> m: nat"
    apply (erule ltE)
    apply (erule Ord_trans, assumption, simp)
    done

    lemma le_in_nat: "[| m le n; n:nat |] ==> m:nat"
    by (blast dest!: lt_nat_in_nat)

    subsection{*Variations on Mathematical Induction*}

    (*complete induction*)

    lemmas complete_induct = Ord_induct [OF _ Ord_nat, case_names less, consumes 1]

    lemmas complete_induct_rule =
            complete_induct [rule_format, case_names less, consumes 1]

    lemma nat_induct_from_lemma [rule_format]:
        "[| n: nat;  m: nat;
            !!x. [| x: nat;  m le x;  P(x) |] ==> P(succ(x)) |]
         ==> m le n --> P(m) --> P(n)"
    apply (erule nat_induct)
    apply (simp_all add: distrib_simps le0_iff le_succ_iff)
    done

    (*Induction starting from m rather than 0*)
    lemma nat_induct_from:
        "[| m le n;  m: nat;  n: nat;
            P(m);
            !!x. [| x: nat;  m le x;  P(x) |] ==> P(succ(x)) |]
         ==> P(n)"
    apply (blast intro: nat_induct_from_lemma)
    done

    (*Induction suitable for subtraction and less-than*)
    lemma diff_induct [case_names 0 0_succ succ_succ, consumes 2]:
        "[| m: nat;  n: nat;
            !!x. x: nat ==> P(x,0);
            !!y. y: nat ==> P(0,succ(y));
            !!x y. [| x: nat;  y: nat;  P(x,y) |] ==> P(succ(x),succ(y)) |]
         ==> P(m,n)"
    apply (erule_tac x = m in rev_bspec)
    apply (erule nat_induct, simp)
    apply (rule ballI)
    apply (rename_tac i j)
    apply (erule_tac n=j in nat_induct, auto)
    done

    (** Induction principle analogous to trancl_induct **)

    lemma succ_lt_induct_lemma [rule_format]:
         "m: nat ==> P(m,succ(m)) --> (ALL x: nat. P(m,x) --> P(m,succ(x))) -->
                     (ALL n:nat. m<n --> P(m,n))"
    apply (erule nat_induct)
     apply (intro impI, rule nat_induct [THEN ballI])
       prefer 4 apply (intro impI, rule nat_induct [THEN ballI])
    apply (auto simp add: le_iff)
    done

    lemma succ_lt_induct:
        "[| m<n;  n: nat;
            P(m,succ(m));
            !!x. [| x: nat;  P(m,x) |] ==> P(m,succ(x)) |]
         ==> P(m,n)"
    by (blast intro: succ_lt_induct_lemma lt_nat_in_nat)

    subsection{*quasinat: to allow a case-split rule for @{term nat_case}*}

    text{*True if the argument is zero or any successor*}
    lemma [iff]: "quasinat(0)"
    by (simp add: quasinat_def)

    lemma [iff]: "quasinat(succ(x))"
    by (simp add: quasinat_def)

    lemma nat_imp_quasinat: "n ∈ nat ==> quasinat(n)"
    by (erule natE, simp_all)

    lemma non_nat_case: "~ quasinat(x) ==> nat_case(a,b,x) = 0"
    by (simp add: quasinat_def nat_case_def)

    lemma nat_cases_disj: "k=0 | (∃y. k = succ(y)) | ~ quasinat(k)"
    apply (case_tac "k=0", simp)
    apply (case_tac "∃m. k = succ(m)")
    apply (simp_all add: quasinat_def)
    done

    lemma nat_cases:
         "[|k=0 ==> P;  !!y. k = succ(y) ==> P; ~ quasinat(k) ==> P|] ==> P"
    by (insert nat_cases_disj [of k], blast)

    (** nat_case **)

    lemma nat_case_0 [simp]: "nat_case(a,b,0) = a"
    by (simp add: nat_case_def)

    lemma nat_case_succ [simp]: "nat_case(a,b,succ(n)) = b(n)"
    by (simp add: nat_case_def)

    lemma nat_case_type [TC]:
        "[| n: nat;  a: C(0);  !!m. m: nat ==> b(m): C(succ(m)) |]
         ==> nat_case(a,b,n) : C(n)";
    by (erule nat_induct, auto)

    lemma split_nat_case:
      "P(nat_case(a,b,k)) <->
       ((k=0 --> P(a)) & (∀x. k=succ(x) --> P(b(x))) & (~ quasinat(k) --> P(0)))"
    apply (rule nat_cases [of k])
    apply (auto simp add: non_nat_case)
    done

    subsection{*Recursion on the Natural Numbers*}

    (** nat_rec is used to define eclose and transrec, then becomes obsolete.
        The operator rec, from arith.thy, has fewer typing conditions **)

    lemma nat_rec_0: "nat_rec(0,a,b) = a"
    apply (rule nat_rec_def [THEN def_wfrec, THEN trans])
     apply (rule wf_Memrel)
    apply (rule nat_case_0)
    done

    lemma nat_rec_succ: "m: nat ==> nat_rec(succ(m),a,b) = b(m, nat_rec(m,a,b))"
    apply (rule nat_rec_def [THEN def_wfrec, THEN trans])
     apply (rule wf_Memrel)
    apply (simp add: vimage_singleton_iff)
    done

    (** The union of two natural numbers is a natural number -- their maximum **)

    lemma Un_nat_type [TC]: "[| i: nat; j: nat |] ==> i Un j: nat"
    apply (rule Un_least_lt [THEN ltD])
    apply (simp_all add: lt_def)
    done

    lemma Int_nat_type [TC]: "[| i: nat; j: nat |] ==> i Int j: nat"
    apply (rule Int_greatest_lt [THEN ltD])
    apply (simp_all add: lt_def)
    done

    (*needed to simplify unions over nat*)
    lemma nat_nonempty [simp]: "nat ~= 0"
    by blast

    text{*A natural number is the set of its predecessors*}
    lemma nat_eq_Collect_lt: "i ∈ nat ==> {j∈nat. j<i} = i"
    apply (rule equalityI)
    apply (blast dest: ltD)
    apply (auto simp add: Ord_mem_iff_lt)
    apply (blast intro: lt_trans)
    done

    lemma Le_iff [iff]: "<x,y> : Le <-> x le y & x : nat & y : nat"
    by (force simp add: Le_def)

    ML
    {*
    val Le_def = thm "Le_def";
    val Lt_def = thm "Lt_def";
    val Ge_def = thm "Ge_def";
    val Gt_def = thm "Gt_def";
    val greater_than_def = thm "greater_than_def";

    val nat_bnd_mono = thm "nat_bnd_mono";
    val nat_unfold = thm "nat_unfold";
    val nat_0I = thm "nat_0I";
    val nat_succI = thm "nat_succI";
    val nat_1I = thm "nat_1I";
    val nat_2I = thm "nat_2I";
    val bool_subset_nat = thm "bool_subset_nat";
    val bool_into_nat = thm "bool_into_nat";
    val nat_induct = thm "nat_induct";
    val natE = thm "natE";
    val nat_into_Ord = thm "nat_into_Ord";
    val nat_0_le = thm "nat_0_le";
    val nat_le_refl = thm "nat_le_refl";
    val Ord_nat = thm "Ord_nat";
    val Limit_nat = thm "Limit_nat";
    val succ_natD = thm "succ_natD";
    val nat_succ_iff = thm "nat_succ_iff";
    val nat_le_Limit = thm "nat_le_Limit";
    val succ_in_naturalD = thm "succ_in_naturalD";
    val lt_nat_in_nat = thm "lt_nat_in_nat";
    val le_in_nat = thm "le_in_nat";
    val complete_induct = thm "complete_induct";
    val nat_induct_from = thm "nat_induct_from";
    val diff_induct = thm "diff_induct";
    val succ_lt_induct = thm "succ_lt_induct";
    val nat_case_0 = thm "nat_case_0";
    val nat_case_succ = thm "nat_case_succ";
    val nat_case_type = thm "nat_case_type";
    val nat_rec_0 = thm "nat_rec_0";
    val nat_rec_succ = thm "nat_rec_succ";
    val Un_nat_type = thm "Un_nat_type";
    val Int_nat_type = thm "Int_nat_type";
    val nat_nonempty = thm "nat_nonempty";
    *}

    end

lemma nat_bnd_mono:

      bnd_mono(Inf, %X. {0} ∪ {succ(i) . i ∈ X})

lemmas nat_unfold:

      nat = {0} ∪ {succ(i) . i ∈ nat}

lemmas nat_unfold:

      nat = {0} ∪ {succ(i) . i ∈ nat}

lemma nat_0I:

      0 ∈ nat

lemma nat_succI:

      n ∈ nat ==> succ(n) ∈ nat

lemma nat_1I:

      1 ∈ nat

lemma nat_2I:

      2 ∈ nat

lemma bool_subset_nat:

      bool ⊆ nat

lemmas bool_into_nat:

      c ∈ bool ==> c ∈ nat

lemmas bool_into_nat:

      c ∈ bool ==> c ∈ nat

### Injectivity Properties and Induction

lemma nat_induct:

      [| n ∈ nat; P(0); !!x. [| x ∈ nat; P(x) |] ==> P(succ(x)) |] ==> P(n)

lemma natE:

      [| n ∈ nat; n = 0 ==> P; !!x. [| x ∈ nat; n = succ(x) |] ==> P |] ==> P

lemma nat_into_Ord:

      n ∈ nat ==> Ord(n)

lemmas nat_0_le:

      i ∈ nat ==> 0 ≤ i

lemmas nat_0_le:

      i ∈ nat ==> 0 ≤ i

lemmas nat_le_refl:

      i ∈ nat ==> i ≤ i

lemmas nat_le_refl:

      i ∈ nat ==> i ≤ i

lemma Ord_nat:

      Ord(nat)

lemma Limit_nat:

      Limit(nat)

lemma naturals_not_limit:

      a ∈ nat ==> ¬ Limit(a)

lemma succ_natD:

      succ(i) ∈ nat ==> i ∈ nat

lemma nat_succ_iff:

      succ(n) ∈ nat <-> n ∈ nat

lemma nat_le_Limit:

      Limit(i) ==> nat ≤ i

lemmas succ_in_naturalD:

      [| succ(i) ∈ k; k ∈ nat |] ==> i ∈ k

lemmas succ_in_naturalD:

      [| succ(i) ∈ k; k ∈ nat |] ==> i ∈ k

lemma lt_nat_in_nat:

      [| m < n; n ∈ nat |] ==> m ∈ nat

lemma le_in_nat:

      [| m ≤ n; n ∈ nat |] ==> m ∈ nat

### Variations on Mathematical Induction

lemmas complete_induct:

      [| i ∈ nat; !!x. [| x ∈ nat; ∀y∈x. P(y) |] ==> P(x) |] ==> P(i)

lemmas complete_induct:

      [| i ∈ nat; !!x. [| x ∈ nat; ∀y∈x. P(y) |] ==> P(x) |] ==> P(i)

lemmas complete_induct_rule:

      [| i ∈ nat; !!x. [| x ∈ nat; !!xa. xa ∈ x ==> P(xa) |] ==> P(x) |] ==> P(i)

lemmas complete_induct_rule:

      [| i ∈ nat; !!x. [| x ∈ nat; !!xa. xa ∈ x ==> P(xa) |] ==> P(x) |] ==> P(i)

lemma nat_induct_from_lemma:

      [| n ∈ nat; m ∈ nat; !!x. [| x ∈ nat; m ≤ x; P(x) |] ==> P(succ(x)); m ≤ n;
         P(m) |]
      ==> P(n)

lemma nat_induct_from:

      [| m ≤ n; m ∈ nat; n ∈ nat; P(m);
         !!x. [| x ∈ nat; m ≤ x; P(x) |] ==> P(succ(x)) |]
      ==> P(n)

lemma diff_induct:

      [| m ∈ nat; n ∈ nat; !!x. x ∈ nat ==> P(x, 0); !!y. y ∈ nat ==> P(0, succ(y));
         !!x y. [| x ∈ nat; y ∈ nat; P(x, y) |] ==> P(succ(x), succ(y)) |]
      ==> P(m, n)

lemma succ_lt_induct_lemma:

      [| m ∈ nat; P(m, succ(m)); !!x. [| x ∈ nat; P(m, x) |] ==> P(m, succ(x));
         n ∈ nat; m < n |]
      ==> P(m, n)

lemma succ_lt_induct:

      [| m < n; n ∈ nat; P(m, succ(m));
         !!x. [| x ∈ nat; P(m, x) |] ==> P(m, succ(x)) |]
      ==> P(m, n)

### quasinat: to allow a case-split rule for @{term nat_case}

lemma

      quasinat(0)

lemma

      quasinat(succ(x))

lemma nat_imp_quasinat:

      n ∈ nat ==> quasinat(n)

lemma non_nat_case:

      ¬ quasinat(x) ==> nat_case(a, b, x) = 0

lemma nat_cases_disj:

      k = 0 ∨ (∃y. k = succ(y)) ∨ ¬ quasinat(k)

lemma nat_cases:

      [| k = 0 ==> P; !!y. k = succ(y) ==> P; ¬ quasinat(k) ==> P |] ==> P

lemma nat_case_0:

      nat_case(a, b, 0) = a

lemma nat_case_succ:

      nat_case(a, b, succ(n)) = b(n)

lemma nat_case_type:

      [| n ∈ nat; a ∈ C(0); !!m. m ∈ nat ==> b(m) ∈ C(succ(m)) |]
      ==> nat_case(a, b, n) ∈ C(n)

lemma split_nat_case:

      P(nat_case(a, b, k)) <->
      (k = 0 --> P(a)) ∧ (∀x. k = succ(x) --> P(b(x))) ∧ (¬ quasinat(k) --> P(0))

### Recursion on the Natural Numbers

lemma nat_rec_0:

      nat_rec(0, a, b) = a

lemma nat_rec_succ:

      m ∈ nat ==> nat_rec(succ(m), a, b) = b(m, nat_rec(m, a, b))

lemma Un_nat_type:

      [| i ∈ nat; j ∈ nat |] ==> i ∪ j ∈ nat

lemma Int_nat_type:

      [| i ∈ nat; j ∈ nat |] ==> i ∩ j ∈ nat

lemma nat_nonempty:

      nat ≠ 0

lemma nat_eq_Collect_lt:

      i ∈ nat ==> {j ∈ nat . j < i} = i

lemma Le_iff:

      ⟨x, y⟩ ∈ Le <-> x ≤ y ∧ x ∈ nat ∧ y ∈ nat