# Theory Primrec

Up to index of Isabelle/ZF/Induct

theory Primrec
imports Main
begin

    (*  Title:      ZF/Induct/Primrec.thy
        ID:         $Id: Primrec.thy,v 1.5 2005/06/17 14:15:11 haftmann Exp $
        Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
        Copyright   1994  University of Cambridge
    *)

    header {* Primitive Recursive Functions: the inductive definition *}

    theory Primrec imports Main begin

    text {*
      Proof adopted from \cite{szasz}.

      See also \cite[page 250, exercise 11]{mendelson}.
    *}

    subsection {* Basic definitions *}

    constdefs
      SC :: "i"
      "SC == λl ∈ list(nat). list_case(0, λx xs. succ(x), l)"

      CONST :: "i=>i"
      "CONST(k) == λl ∈ list(nat). k"

      PROJ :: "i=>i"
      "PROJ(i) == λl ∈ list(nat). list_case(0, λx xs. x, drop(i,l))"

      COMP :: "[i,i]=>i"
      "COMP(g,fs) == λl ∈ list(nat). g ` List.map(λf. f`l, fs)"

      PREC :: "[i,i]=>i"
      "PREC(f,g) ==
         λl ∈ list(nat). list_case(0,
                          λx xs. rec(x, f`xs, λy r. g ` Cons(r, Cons(y, xs))), l)"
      -- {* Note that @{text g} is applied first to @{term "PREC(f,g)`y"} and then to @{text y}! *}

    consts
      ACK :: "i=>i"
    primrec
      "ACK(0) = SC"
      "ACK(succ(i)) = PREC (CONST (ACK(i) ` [1]), COMP(ACK(i), [PROJ(0)]))"

    syntax
      ack :: "[i,i]=>i"
    translations
      "ack(x,y)" == "ACK(x) ` [y]"

    text {*
      \medskip Useful special cases of evaluation.
    *}

    lemma SC: "[| x ∈ nat;  l ∈ list(nat) |] ==> SC ` (Cons(x,l)) = succ(x)"
      by (simp add: SC_def)

    lemma CONST: "l ∈ list(nat) ==> CONST(k) ` l = k"
      by (simp add: CONST_def)

    lemma PROJ_0: "[| x ∈ nat;  l ∈ list(nat) |] ==> PROJ(0) ` (Cons(x,l)) = x"
      by (simp add: PROJ_def)

    lemma COMP_1: "l ∈ list(nat) ==> COMP(g,[f]) ` l = g` [f`l]"
      by (simp add: COMP_def)

    lemma PREC_0: "l ∈ list(nat) ==> PREC(f,g) ` (Cons(0,l)) = f`l"
      by (simp add: PREC_def)

    lemma PREC_succ:
      "[| x ∈ nat;  l ∈ list(nat) |]
        ==> PREC(f,g) ` (Cons(succ(x),l)) =
          g ` Cons(PREC(f,g)`(Cons(x,l)), Cons(x,l))"
      by (simp add: PREC_def)

    subsection {* Inductive definition of the PR functions *}

    consts
      prim_rec :: i

    inductive
      domains prim_rec ⊆ "list(nat)->nat"
      intros
        "SC ∈ prim_rec"
        "k ∈ nat ==> CONST(k) ∈ prim_rec"
        "i ∈ nat ==> PROJ(i) ∈ prim_rec"
        "[| g ∈ prim_rec; fs∈list(prim_rec) |] ==> COMP(g,fs) ∈ prim_rec"
        "[| f ∈ prim_rec; g ∈ prim_rec |] ==> PREC(f,g) ∈ prim_rec"
      monos list_mono
      con_defs SC_def CONST_def PROJ_def COMP_def PREC_def
      type_intros nat_typechecks list.intros
        lam_type list_case_type drop_type List.map_type
        apply_type rec_type

    lemma prim_rec_into_fun [TC]: "c ∈ prim_rec ==> c ∈ list(nat) -> nat"
      by (erule subsetD [OF prim_rec.dom_subset])

    lemmas [TC] = apply_type [OF prim_rec_into_fun]

    declare prim_rec.intros [TC]
    declare nat_into_Ord [TC]
    declare rec_type [TC]

    lemma ACK_in_prim_rec [TC]: "i ∈ nat ==> ACK(i) ∈ prim_rec"
      by (induct_tac i) simp_all

    lemma ack_type [TC]: "[| i ∈ nat;  j ∈ nat |] ==>  ack(i,j) ∈ nat"
      by auto

    subsection {* Ackermann's function cases *}

    lemma ack_0: "j ∈ nat ==> ack(0,j) = succ(j)"
      -- {* PROPERTY A 1 *}
      by (simp add: SC)

    lemma ack_succ_0: "ack(succ(i), 0) = ack(i,1)"
      -- {* PROPERTY A 2 *}
      by (simp add: CONST PREC_0)

    lemma ack_succ_succ:
      "[| i∈nat;  j∈nat |] ==> ack(succ(i), succ(j)) = ack(i, ack(succ(i), j))"
      -- {* PROPERTY A 3 *}
      by (simp add: CONST PREC_succ COMP_1 PROJ_0)

    lemmas [simp] = ack_0 ack_succ_0 ack_succ_succ ack_type
      and [simp del] = ACK.simps

    lemma lt_ack2 [rule_format]: "i ∈ nat ==> ∀j ∈ nat. j < ack(i,j)"
      -- {* PROPERTY A 4 *}
      apply (induct_tac i)
       apply simp
      apply (rule ballI)
      apply (induct_tac j)
       apply (erule_tac [2] succ_leI [THEN lt_trans1])
       apply (rule nat_0I [THEN nat_0_le, THEN lt_trans])
       apply auto
      done

    lemma ack_lt_ack_succ2: "[|i∈nat; j∈nat|] ==> ack(i,j) < ack(i, succ(j))"
      -- {* PROPERTY A 5-, the single-step lemma *}
      by (induct_tac i) (simp_all add: lt_ack2)

    lemma ack_lt_mono2: "[| j<k; i ∈ nat; k ∈ nat |] ==> ack(i,j) < ack(i,k)"
      -- {* PROPERTY A 5, monotonicity for @{text "<"} *}
      apply (frule lt_nat_in_nat, assumption)
      apply (erule succ_lt_induct)
        apply assumption
       apply (rule_tac [2] lt_trans)
        apply (auto intro: ack_lt_ack_succ2)
      done

    lemma ack_le_mono2: "[|j≤k;  i∈nat;  k∈nat|] ==> ack(i,j) ≤ ack(i,k)"
      -- {* PROPERTY A 5', monotonicity for @{text ≤} *}
      apply (rule_tac f = "λj. ack (i,j) " in Ord_lt_mono_imp_le_mono)
         apply (assumption | rule ack_lt_mono2 ack_type [THEN nat_into_Ord])+
      done

    lemma ack2_le_ack1:
      "[| i∈nat;  j∈nat |] ==> ack(i, succ(j)) ≤ ack(succ(i), j)"
      -- {* PROPERTY A 6 *}
      apply (induct_tac j)
       apply simp_all
      apply (rule ack_le_mono2)
        apply (rule lt_ack2 [THEN succ_leI, THEN le_trans])
          apply auto
      done

    lemma ack_lt_ack_succ1: "[| i ∈ nat; j ∈ nat |] ==> ack(i,j) < ack(succ(i),j)"
      -- {* PROPERTY A 7-, the single-step lemma *}
      apply (rule ack_lt_mono2 [THEN lt_trans2])
         apply (rule_tac [4] ack2_le_ack1)
          apply auto
      done

    lemma ack_lt_mono1: "[| i<j; j ∈ nat; k ∈ nat |] ==> ack(i,k) < ack(j,k)"
      -- {* PROPERTY A 7, monotonicity for @{text "<"} *}
      apply (frule lt_nat_in_nat, assumption)
      apply (erule succ_lt_induct)
        apply assumption
       apply (rule_tac [2] lt_trans)
        apply (auto intro: ack_lt_ack_succ1)
      done

    lemma ack_le_mono1: "[| i≤j; j ∈ nat; k ∈ nat |] ==> ack(i,k) ≤ ack(j,k)"
      -- {* PROPERTY A 7', monotonicity for @{text ≤} *}
      apply (rule_tac f = "λj. ack (j,k) " in Ord_lt_mono_imp_le_mono)
         apply (assumption | rule ack_lt_mono1 ack_type [THEN nat_into_Ord])+
      done

    lemma ack_1: "j ∈ nat ==> ack(1,j) = succ(succ(j))"
      -- {* PROPERTY A 8 *}
      by (induct_tac j) simp_all

    lemma ack_2: "j ∈ nat ==> ack(succ(1),j) = succ(succ(succ(j#+j)))"
      -- {* PROPERTY A 9 *}
      by (induct_tac j) (simp_all add: ack_1)

    lemma ack_nest_bound:
      "[| i1 ∈ nat; i2 ∈ nat; j ∈ nat |]
        ==> ack(i1, ack(i2,j)) < ack(succ(succ(i1#+i2)), j)"
      -- {* PROPERTY A 10 *}
      apply (rule lt_trans2 [OF _ ack2_le_ack1])
        apply simp
        apply (rule add_le_self [THEN ack_le_mono1, THEN lt_trans1])
           apply auto
      apply (force intro: add_le_self2 [THEN ack_lt_mono1, THEN ack_lt_mono2])
      done

    lemma ack_add_bound:
      "[| i1 ∈ nat; i2 ∈ nat; j ∈ nat |]
        ==> ack(i1,j) #+ ack(i2,j) < ack(succ(succ(succ(succ(i1#+i2)))), j)"
      -- {* PROPERTY A 11 *}
      apply (rule_tac j = "ack (succ (1), ack (i1 #+ i2, j))" in lt_trans)
       apply (simp add: ack_2)
       apply (rule_tac [2] ack_nest_bound [THEN lt_trans2])
          apply (rule add_le_mono [THEN leI, THEN leI])
             apply (auto intro: add_le_self add_le_self2 ack_le_mono1)
      done

    lemma ack_add_bound2:
         "[| i < ack(k,j);  j ∈ nat;  k ∈ nat |]
          ==> i#+j < ack(succ(succ(succ(succ(k)))), j)"
      -- {* PROPERTY A 12. *}
      -- {* Article uses existential quantifier but the ALF proof used @{term "k#+#4"}. *}
      -- {* Quantified version must be nested @{text "∃k'. ∀i,j …"}. *}
      apply (rule_tac j = "ack (k,j) #+ ack (0,j) " in lt_trans)
       apply (rule_tac [2] ack_add_bound [THEN lt_trans2])
          apply (rule add_lt_mono)
             apply auto
      done

    subsection {* Main result *}

    declare list_add_type [simp]

    lemma SC_case: "l ∈ list(nat) ==> SC ` l < ack(1, list_add(l))"
      apply (unfold SC_def)
      apply (erule list.cases)
       apply (simp add: succ_iff)
      apply (simp add: ack_1 add_le_self)
      done

    lemma lt_ack1: "[| i ∈ nat; j ∈ nat |] ==> i < ack(i,j)"
      -- {* PROPERTY A 4'? Extra lemma needed for @{text CONST} case, constant functions. *}
      apply (induct_tac i)
       apply (simp add: nat_0_le)
      apply (erule lt_trans1 [OF succ_leI ack_lt_ack_succ1])
       apply auto
      done

    lemma CONST_case:
        "[| l ∈ list(nat);  k ∈ nat |] ==> CONST(k) ` l < ack(k, list_add(l))"
      by (simp add: CONST_def lt_ack1)

    lemma PROJ_case [rule_format]:
        "l ∈ list(nat) ==> ∀i ∈ nat. PROJ(i) ` l < ack(0, list_add(l))"
      apply (unfold PROJ_def)
      apply simp
      apply (erule list.induct)
       apply (simp add: nat_0_le)
      apply simp
      apply (rule ballI)
      apply (erule_tac n = i in natE)
       apply (simp add: add_le_self)
      apply simp
      apply (erule bspec [THEN lt_trans2])
       apply (rule_tac [2] add_le_self2 [THEN succ_leI])
       apply auto
      done

    text {*
      \medskip @{text COMP} case.
    *}

    lemma COMP_map_lemma:
      "fs ∈ list({f ∈ prim_rec. ∃kf ∈ nat. ∀l ∈ list(nat). f`l < ack(kf, list_add(l))})
        ==> ∃k ∈ nat. ∀l ∈ list(nat).
          list_add(map(λf. f ` l, fs)) < ack(k, list_add(l))"
      apply (erule list.induct)
       apply (rule_tac x = 0 in bexI)
        apply (simp_all add: lt_ack1 nat_0_le)
      apply clarify
      apply (rule ballI [THEN bexI])
      apply (rule add_lt_mono [THEN lt_trans])
           apply (rule_tac [5] ack_add_bound)
             apply blast
            apply auto
      done

    lemma COMP_case:
     "[| kg∈nat;
         ∀l ∈ list(nat). g`l < ack(kg, list_add(l));
         fs ∈ list({f ∈ prim_rec .
                     ∃kf ∈ nat. ∀l ∈ list(nat).
                            f`l < ack(kf, list_add(l))}) |]
       ==> ∃k ∈ nat. ∀l ∈ list(nat). COMP(g,fs)`l < ack(k, list_add(l))"
      apply (simp add: COMP_def)
      apply (frule list_CollectD)
      apply (erule COMP_map_lemma [THEN bexE])
      apply (rule ballI [THEN bexI])
       apply (erule bspec [THEN lt_trans])
        apply (rule_tac [2] lt_trans)
         apply (rule_tac [3] ack_nest_bound)
           apply (erule_tac [2] bspec [THEN ack_lt_mono2])
             apply auto
      done

    text {*
      \medskip @{text PREC} case.
    *}

    lemma PREC_case_lemma:
     "[| ∀l ∈ list(nat). f`l #+ list_add(l) < ack(kf, list_add(l));
         ∀l ∈ list(nat). g`l #+ list_add(l) < ack(kg, list_add(l));
         f ∈ prim_rec;  kf∈nat;
         g ∈ prim_rec;  kg∈nat;
         l ∈ list(nat) |]
      ==> PREC(f,g)`l #+ list_add(l) < ack(succ(kf#+kg), list_add(l))"
      apply (unfold PREC_def)
      apply (erule list.cases)
       apply (simp add: lt_trans [OF nat_le_refl lt_ack2])
      apply simp
      apply (erule ssubst)  -- {* get rid of the needless assumption *}
      apply (induct_tac a)
       apply simp_all
       txt {* base case *}
       apply (rule lt_trans, erule bspec, assumption)
       apply (simp add: add_le_self [THEN ack_lt_mono1])
      txt {* ind step *}
      apply (rule succ_leI [THEN lt_trans1])
       apply (rule_tac j = "g ` ?ll #+ ?mm" in lt_trans1)
        apply (erule_tac [2] bspec)
        apply (rule nat_le_refl [THEN add_le_mono])
           apply typecheck
       apply (simp add: add_le_self2)
       txt {* final part of the simplification *}
      apply simp
      apply (rule add_le_self2 [THEN ack_le_mono1, THEN lt_trans1])
         apply (erule_tac [4] ack_lt_mono2)
          apply auto
      done

    lemma PREC_case:
       "[| f ∈ prim_rec;  kf∈nat;
           g ∈ prim_rec;  kg∈nat;
           ∀l ∈ list(nat). f`l < ack(kf, list_add(l));
           ∀l ∈ list(nat). g`l < ack(kg, list_add(l)) |]
        ==> ∃k ∈ nat. ∀l ∈ list(nat). PREC(f,g)`l< ack(k, list_add(l))"
      apply (rule ballI [THEN bexI])
       apply (rule lt_trans1 [OF add_le_self PREC_case_lemma])
              apply typecheck
         apply (blast intro: ack_add_bound2 list_add_type)+
      done

    lemma ack_bounds_prim_rec:
        "f ∈ prim_rec ==> ∃k ∈ nat. ∀l ∈ list(nat). f`l < ack(k, list_add(l))"
      apply (erule prim_rec.induct)
      apply (auto intro: SC_case CONST_case PROJ_case COMP_case PREC_case)
      done

    theorem ack_not_prim_rec:
        "(λl ∈ list(nat). list_case(0, λx xs. ack(x,x), l)) ∉ prim_rec"
      apply (rule notI)
      apply (drule ack_bounds_prim_rec)
      apply force
      done

    end

### Basic definitions

lemma SC:

      [| x ∈ nat; l ∈ list(nat) |] ==> SC ` Cons(x, l) = succ(x)

lemma CONST:

      l ∈ list(nat) ==> CONST(k) ` l = k

lemma PROJ_0:

      [| x ∈ nat; l ∈ list(nat) |] ==> PROJ(0) ` Cons(x, l) = x

lemma COMP_1:

      l ∈ list(nat) ==> COMP(g, [f]) ` l = g ` [f ` l]

lemma PREC_0:

      l ∈ list(nat) ==> PREC(f, g) ` Cons(0, l) = f ` l

lemma PREC_succ:

      [| x ∈ nat; l ∈ list(nat) |]
      ==> PREC(f, g) ` Cons(succ(x), l) =
          g ` Cons(PREC(f, g) ` Cons(x, l), Cons(x, l))

### Inductive definition of the PR functions

lemma prim_rec_into_fun:

      c ∈ prim_rec ==> c ∈ list(nat) -> nat

lemmas

      [| f ∈ prim_rec; a ∈ list(nat) |] ==> f ` a ∈ nat

lemmas

      [| f ∈ prim_rec; a ∈ list(nat) |] ==> f ` a ∈ nat

lemma ACK_in_prim_rec:

      i ∈ nat ==> ACK(i) ∈ prim_rec

lemma ack_type:

      [| i ∈ nat; j ∈ nat |] ==> ack(i, j) ∈ nat

### Ackermann's function cases

lemma ack_0:

      j ∈ nat ==> ack(0, j) = succ(j)

lemma ack_succ_0:

      ack(succ(i), 0) = ack(i, 1)

lemma ack_succ_succ:

      [| i ∈ nat; j ∈ nat |] ==> ack(succ(i), succ(j)) = ack(i, ack(succ(i), j))

lemmas

      j ∈ nat ==> ack(0, j) = succ(j)

      ack(succ(i), 0) = ack(i, 1)

      [| i ∈ nat; j ∈ nat |] ==> ack(succ(i), succ(j)) = ack(i, ack(succ(i), j))

      [| i ∈ nat; j ∈ nat |] ==> ack(i, j) ∈ nat

and

      ACK(0) = SC

      ACK(succ(i)) = PREC(CONST(ack(i, 1)), COMP(ACK(i), [PROJ(0)]))

lemmas

      j ∈ nat ==> ack(0, j) = succ(j)

      ack(succ(i), 0) = ack(i, 1)

      [| i ∈ nat; j ∈ nat |] ==> ack(succ(i), succ(j)) = ack(i, ack(succ(i), j))

      [| i ∈ nat; j ∈ nat |] ==> ack(i, j) ∈ nat

and

      ACK(0) = SC

      ACK(succ(i)) = PREC(CONST(ack(i, 1)), COMP(ACK(i), [PROJ(0)]))

lemma lt_ack2:

      [| i ∈ nat; j ∈ nat |] ==> j < ack(i, j)

lemma ack_lt_ack_succ2:

      [| i ∈ nat; j ∈ nat |] ==> ack(i, j) < ack(i, succ(j))

lemma ack_lt_mono2:

      [| j < k; i ∈ nat; k ∈ nat |] ==> ack(i, j) < ack(i, k)

lemma ack_le_mono2:

      [| j ≤ k; i ∈ nat; k ∈ nat |] ==> ack(i, j) ≤ ack(i, k)

lemma ack2_le_ack1:

      [| i ∈ nat; j ∈ nat |] ==> ack(i, succ(j)) ≤ ack(succ(i), j)

lemma ack_lt_ack_succ1:

      [| i ∈ nat; j ∈ nat |] ==> ack(i, j) < ack(succ(i), j)

lemma ack_lt_mono1:

      [| i < j; j ∈ nat; k ∈ nat |] ==> ack(i, k) < ack(j, k)

lemma ack_le_mono1:

      [| i ≤ j; j ∈ nat; k ∈ nat |] ==> ack(i, k) ≤ ack(j, k)

lemma ack_1:

      j ∈ nat ==> ack(1, j) = succ(succ(j))

lemma ack_2:

      j ∈ nat ==> ack(2, j) = succ(succ(succ(j #+ j)))

lemma ack_nest_bound:

      [| i1.0 ∈ nat; i2.0 ∈ nat; j ∈ nat |]
      ==> ack(i1.0, ack(i2.0, j)) < ack(succ(succ(i1.0 #+ i2.0)), j)

lemma ack_add_bound:

      [| i1.0 ∈ nat; i2.0 ∈ nat; j ∈ nat |]
      ==> ack(i1.0, j) #+ ack(i2.0, j) < ack(succ(succ(succ(succ(i1.0 #+ i2.0)))), j)

lemma ack_add_bound2:

      [| i < ack(k, j); j ∈ nat; k ∈ nat |]
      ==> i #+ j < ack(succ(succ(succ(succ(k)))), j)

### Main result

lemma SC_case:

      l ∈ list(nat) ==> SC ` l < ack(1, list_add(l))

lemma lt_ack1:

      [| i ∈ nat; j ∈ nat |] ==> i < ack(i, j)

lemma CONST_case:

      [| l ∈ list(nat); k ∈ nat |] ==> CONST(k) ` l < ack(k, list_add(l))

lemma PROJ_case:

      [| l ∈ list(nat); i ∈ nat |] ==> PROJ(i) ` l < ack(0, list_add(l))

lemma COMP_map_lemma:

      fs ∈ list({f ∈ prim_rec . ∃kf∈nat. ∀l∈list(nat). f ` l < ack(kf, list_add(l))})
      ==> ∃k∈nat. ∀l∈list(nat). list_add(map(%f. f ` l, fs)) < ack(k, list_add(l))

lemma COMP_case:

      [| kg ∈ nat; ∀l∈list(nat). g ` l < ack(kg, list_add(l));
         fs ∈
         list({f ∈ prim_rec . ∃kf∈nat. ∀l∈list(nat). f ` l < ack(kf, list_add(l))}) |]
      ==> ∃k∈nat. ∀l∈list(nat). COMP(g, fs) ` l < ack(k, list_add(l))

lemma PREC_case_lemma:

      [| ∀l∈list(nat). f ` l #+ list_add(l) < ack(kf, list_add(l));
         ∀l∈list(nat). g ` l #+ list_add(l) < ack(kg, list_add(l)); f ∈ prim_rec;
         kf ∈ nat; g ∈ prim_rec; kg ∈ nat; l ∈ list(nat) |]
      ==> PREC(f, g) ` l #+ list_add(l) < ack(succ(kf #+ kg), list_add(l))

lemma PREC_case:

      [| f ∈ prim_rec; kf ∈ nat; g ∈ prim_rec; kg ∈ nat;
         ∀l∈list(nat). f ` l < ack(kf, list_add(l));
         ∀l∈list(nat). g ` l < ack(kg, list_add(l)) |]
      ==> ∃k∈nat. ∀l∈list(nat). PREC(f, g) ` l < ack(k, list_add(l))

lemma ack_bounds_prim_rec:

      f ∈ prim_rec ==> ∃k∈nat. ∀l∈list(nat). f ` l < ack(k, list_add(l))

theorem ack_not_prim_rec:

      (λl∈list(nat). list_case(0, %x xs. ack(x, x), l)) ∉ prim_rec