(* Title: thys/UF.thy

   Author: Jian Xu, Xingyuan Zhang, and Christian Urban

*)

chapter {* Construction of a Universal Function *}

theory UF

imports Rec_Def HOL.GCD Abacus

begin

text {*

  This theory file constructs the Universal Function @{text "rec_F"}, which is the UTM defined

  in terms of recursive functions. This @{text "rec_F"} is essentially an 

  interpreter of Turing Machines. Once the correctness of @{text "rec_F"} is established,

  UTM can easil be obtained by compling @{text "rec_F"} into the corresponding Turing Machine.

*}

section {* Universal Function *}

subsection {* The construction of component functions *}

text {*

*}

definition rec_add :: "recf"

  where

  "rec_add \<equiv>  Pr 1 (id 1 0) (Cn 3 s [id 3 2])"

text {*

*}

definition rec_mult :: "recf"

  where

  "rec_mult = Pr 1 z (Cn 3 rec_add [id 3 0, id 3 2])"

text {*

*}

definition rec_pred :: "recf"

  where

  "rec_pred = Cn 1 (Pr 1 z (id 3 1)) [id 1 0, id 1 0]"

text {*

*}

definition rec_minus :: "recf" 

  where

  "rec_minus = Pr 1 (id 1 0) (Cn 3 rec_pred [id 3 2])"

text {*

  @{text "constn n"} is the recursive function which computes 

  nature number @{text "n"}.

*}

fun constn :: "nat \<Rightarrow> recf"

  where

  "constn 0 = z"  |

  "constn (Suc n) = Cn 1 s [constn n]"

text {*

  Sign function, which returns 1 when the input argument is greater than @{text "0"}.

*}

definition rec_sg :: "recf"

  where

  "rec_sg = Cn 1 rec_minus [constn 1, 

                  Cn 1 rec_minus [constn 1, id 1 0]]"

text {*

  @{text "rec_less"} compares its two arguments, returns @{text "1"} if

  the first is less than the second; otherwise returns @{text "0"}.

  *}

definition rec_less :: "recf"

  where

  "rec_less = Cn 2 rec_sg [Cn 2 rec_minus [id 2 1, id 2 0]]"

text {*

  @{text "rec_not"} inverse its argument: returns @{text "1"} when the

  argument is @{text "0"}; returns @{text "0"} otherwise.

  *}

definition rec_not :: "recf"

  where

  "rec_not = Cn 1 rec_minus [constn 1, id 1 0]"

text {*

  @{text "rec_eq"} compares its two arguments: returns @{text "1"}

  if they are equal; return @{text "0"} otherwise.

  *}

definition rec_eq :: "recf"

  where

  "rec_eq = Cn 2 rec_minus [Cn 2 (constn 1) [id 2 0], 

             Cn 2 rec_add [Cn 2 rec_minus [id 2 0, id 2 1], 

               Cn 2 rec_minus [id 2 1, id 2 0]]]"

text {*

  @{text "rec_conj"} computes the conjunction of its two arguments, 

  returns @{text "1"} if both of them are non-zero; returns @{text "0"}

  otherwise.

  *}

definition rec_conj :: "recf"

  where

  "rec_conj = Cn 2 rec_sg [Cn 2 rec_mult [id 2 0, id 2 1]] "

text {*

  @{text "rec_disj"} computes the disjunction of its two arguments, 

  returns @{text "0"} if both of them are zero; returns @{text "0"}

  otherwise.

  *}

definition rec_disj :: "recf"

  where

  "rec_disj = Cn 2 rec_sg [Cn 2 rec_add [id 2 0, id 2 1]]"

text {*

  Computes the arity of recursive function.

  *}

fun arity :: "recf \<Rightarrow> nat"

  where

  "arity z = 1" 

| "arity s = 1"

| "arity (id m n) = m"

| "arity (Cn n f gs) = n"

| "arity (Pr n f g) = Suc n"

| "arity (Mn n f) = n"

text {*

  @{text "get_fstn_args n (Suc k)"} returns

  @{text "[id n 0, id n 1, id n 2, \<dots>, id n k]"}, 

  the effect of which is to take out the first @{text "Suc k"} 

  arguments out of the @{text "n"} input arguments.

  *}

fun get_fstn_args :: "nat \<Rightarrow>  nat \<Rightarrow> recf list"

  where

  "get_fstn_args n 0 = []"

| "get_fstn_args n (Suc y) = get_fstn_args n y @ [id n y]"

text {*

  @{text "rec_sigma f"} returns the recursive functions which 

  sums up the results of @{text "f"}:

  \[

  (rec\_sigma f)(x, y) = f(x, 0) + f(x, 1) + \cdots + f(x, y)

  \]

*}

fun rec_sigma :: "recf \<Rightarrow> recf"

  where

  "rec_sigma rf = 

       (let vl = arity rf in 

          Pr (vl - 1) (Cn (vl - 1) rf (get_fstn_args (vl - 1) (vl - 1) @ 

                    [Cn (vl - 1) (constn 0) [id (vl - 1) 0]])) 

             (Cn (Suc vl) rec_add [id (Suc vl) vl, 

                    Cn (Suc vl) rf (get_fstn_args (Suc vl) (vl - 1) 

                        @ [Cn (Suc vl) s [id (Suc vl) (vl - 1)]])]))"

text {*

  @{text "rec_exec"} is the interpreter function for

  reursive functions. The function is defined such that 

  it always returns meaningful results for primitive recursive 

  functions.

  *}

declare rec_exec.simps[simp del] constn.simps[simp del]

text {*

  Correctness of @{text "rec_add"}.

  *}

lemma add_lemma: "\<And> x y. rec_exec rec_add [x, y] =  x + y"

by(induct_tac y, auto simp: rec_add_def rec_exec.simps)

text {*

  Correctness of @{text "rec_mult"}.

  *}

lemma mult_lemma: "\<And> x y. rec_exec rec_mult [x, y] = x * y"

by(induct_tac y, auto simp: rec_mult_def rec_exec.simps add_lemma)

text {*

  Correctness of @{text "rec_pred"}.

  *}

lemma pred_lemma: "\<And> x. rec_exec rec_pred [x] =  x - 1"

by(induct_tac x, auto simp: rec_pred_def rec_exec.simps)

text {*

  Correctness of @{text "rec_minus"}.

  *}

lemma minus_lemma: "\<And> x y. rec_exec rec_minus [x, y] = x - y"

by(induct_tac y, auto simp: rec_exec.simps rec_minus_def pred_lemma)

text {*

  Correctness of @{text "rec_sg"}.

  *}

lemma sg_lemma: "\<And> x. rec_exec rec_sg [x] = (if x = 0 then 0 else 1)"

by(auto simp: rec_sg_def minus_lemma rec_exec.simps constn.simps)

text {*

  Correctness of @{text "constn"}.

  *}

lemma constn_lemma: "rec_exec (constn n) [x] = n"

by(induct n, auto simp: rec_exec.simps constn.simps)

text {*

  Correctness of @{text "rec_less"}.

  *}

lemma less_lemma: "\<And> x y. rec_exec rec_less [x, y] = 

  (if x < y then 1 else 0)"

by(induct_tac y, auto simp: rec_exec.simps 

  rec_less_def minus_lemma sg_lemma)

text {*

  Correctness of @{text "rec_not"}.

  *}

lemma not_lemma: 

  "\<And> x. rec_exec rec_not [x] = (if x = 0 then 1 else 0)"

by(induct_tac x, auto simp: rec_exec.simps rec_not_def

  constn_lemma minus_lemma)

text {*

  Correctness of @{text "rec_eq"}.

  *}

lemma eq_lemma: "\<And> x y. rec_exec rec_eq [x, y] = (if x = y then 1 else 0)"

by(induct_tac y, auto simp: rec_exec.simps rec_eq_def constn_lemma add_lemma minus_lemma)

text {*

  Correctness of @{text "rec_conj"}.

  *}

lemma conj_lemma: "\<And> x y. rec_exec rec_conj [x, y] = (if x = 0 \<or> y = 0 then 0 

                                                       else 1)"

by(induct_tac y, auto simp: rec_exec.simps sg_lemma rec_conj_def mult_lemma)

text {*

  Correctness of @{text "rec_disj"}.

  *}

lemma disj_lemma: "\<And> x y. rec_exec rec_disj [x, y] = (if x = 0 \<and> y = 0 then 0

                                                     else 1)"

by(induct_tac y, auto simp: rec_disj_def sg_lemma add_lemma rec_exec.simps)

text {*

  @{text "primrec recf n"} is true iff 

  @{text "recf"} is a primitive recursive function 

  with arity @{text "n"}.

  *}

inductive primerec :: "recf \<Rightarrow> nat \<Rightarrow> bool"

  where

prime_z[intro]:  "primerec z (Suc 0)" |

prime_s[intro]:  "primerec s (Suc 0)" |

prime_id[intro!]: "\<lbrakk>n < m\<rbrakk> \<Longrightarrow> primerec (id m n) m" |

prime_cn[intro!]: "\<lbrakk>primerec f k; length gs = k; 

  \<forall> i < length gs. primerec (gs ! i) m; m = n\<rbrakk> 

  \<Longrightarrow> primerec (Cn n f gs) m" |

prime_pr[intro!]: "\<lbrakk>primerec f n; 

  primerec g (Suc (Suc n)); m = Suc n\<rbrakk> 

  \<Longrightarrow> primerec (Pr n f g) m" 

inductive_cases prime_cn_reverse'[elim]: "primerec (Cn n f gs) n" 

inductive_cases prime_mn_reverse: "primerec (Mn n f) m" 

inductive_cases prime_z_reverse[elim]: "primerec z n"

inductive_cases prime_s_reverse[elim]: "primerec s n"

inductive_cases prime_id_reverse[elim]: "primerec (id m n) k"

inductive_cases prime_cn_reverse[elim]: "primerec (Cn n f gs) m"

inductive_cases prime_pr_reverse[elim]: "primerec (Pr n f g) m"

declare mult_lemma[simp] add_lemma[simp] pred_lemma[simp] 

        minus_lemma[simp] sg_lemma[simp] constn_lemma[simp] 

        less_lemma[simp] not_lemma[simp] eq_lemma[simp]

        conj_lemma[simp] disj_lemma[simp]

text {*

  @{text "Sigma"} is the logical specification of 

  the recursive function @{text "rec_sigma"}.

  *}

function Sigma :: "(nat list \<Rightarrow> nat) \<Rightarrow> nat list \<Rightarrow> nat"

  where

  "Sigma g xs = (if last xs = 0 then g xs

                 else (Sigma g (butlast xs @ [last xs - 1]) +

                       g xs)) "

by pat_completeness auto

termination

proof

  show "wf (measure (\<lambda> (f, xs). last xs))" by auto

next

  fix g xs

  assume "last (xs::nat list) \<noteq> 0"

  thus "((g, butlast xs @ [last xs - 1]), g, xs)  

                   \<in> measure (\<lambda>(f, xs). last xs)"

    by auto

qed

declare rec_exec.simps[simp del] get_fstn_args.simps[simp del]

        arity.simps[simp del] Sigma.simps[simp del]

        rec_sigma.simps[simp del]

lemma rec_pr_Suc_simp_rewrite: 

  "rec_exec (Pr n f g) (xs @ [Suc x]) =

                       rec_exec g (xs @ [x] @ 

                        [rec_exec (Pr n f g) (xs @ [x])])"

by(simp add: rec_exec.simps)

lemma Sigma_0_simp_rewrite:

  "Sigma f (xs @ [0]) = f (xs @ [0])"

by(simp add: Sigma.simps)

lemma Sigma_Suc_simp_rewrite: 

  "Sigma f (xs @ [Suc x]) = Sigma f (xs @ [x]) + f (xs @ [Suc x])"

by(simp add: Sigma.simps)

by(simp add: nth_append)

lemma get_fstn_args_take: "\<lbrakk>length xs = m; n \<le> m\<rbrakk> \<Longrightarrow> 

  map (\<lambda> f. rec_exec f xs) (get_fstn_args m n)= take n xs"

proof(induct n)

  case 0 thus "?case"

    by(simp add: get_fstn_args.simps)

next

  case (Suc n) thus "?case"

    by(simp add: get_fstn_args.simps rec_exec.simps 

             take_Suc_conv_app_nth)

qed

lemma arity_primerec[simp]: "primerec f n \<Longrightarrow> arity f = n"

  apply(case_tac f)

  apply(auto simp: arity.simps )

  apply(erule_tac prime_mn_reverse)

  done

lemma rec_sigma_Suc_simp_rewrite: 

  "primerec f (Suc (length xs))

    \<Longrightarrow> rec_exec (rec_sigma f) (xs @ [Suc x]) = 

    rec_exec (rec_sigma f) (xs @ [x]) + rec_exec f (xs @ [Suc x])"

  apply(induct x)

  apply(auto simp: rec_sigma.simps Let_def rec_pr_Suc_simp_rewrite

                   rec_exec.simps get_fstn_args_take)

  done      

text {*

  The correctness of @{text "rec_sigma"} with respect to its specification.

  *}

lemma sigma_lemma: 

  "primerec rg (Suc (length xs))

     \<Longrightarrow> rec_exec (rec_sigma rg) (xs @ [x]) = Sigma (rec_exec rg) (xs @ [x])"

apply(induct x)

apply(auto simp: rec_exec.simps rec_sigma.simps Let_def 

         get_fstn_args_take Sigma_0_simp_rewrite

         Sigma_Suc_simp_rewrite) 

done

text {*

  @{text "rec_accum f (x1, x2, \<dots>, xn, k) = 

           f(x1, x2, \<dots>, xn, 0) * 

           f(x1, x2, \<dots>, xn, 1) *

               \<dots> 

           f(x1, x2, \<dots>, xn, k)"}

*}

fun rec_accum :: "recf \<Rightarrow> recf"

  where

  "rec_accum rf = 

       (let vl = arity rf in 

          Pr (vl - 1) (Cn (vl - 1) rf (get_fstn_args (vl - 1) (vl - 1) @ 

                     [Cn (vl - 1) (constn 0) [id (vl - 1) 0]])) 

             (Cn (Suc vl) rec_mult [id (Suc vl) (vl), 

                    Cn (Suc vl) rf (get_fstn_args (Suc vl) (vl - 1) 

                      @ [Cn (Suc vl) s [id (Suc vl) (vl - 1)]])]))"

text {*

  @{text "Accum"} is the formal specification of @{text "rec_accum"}.

  *}

function Accum :: "(nat list \<Rightarrow> nat) \<Rightarrow> nat list \<Rightarrow> nat"

  where

  "Accum f xs = (if last xs = 0 then f xs 

                     else (Accum f (butlast xs @ [last xs - 1]) *

                       f xs))"

by pat_completeness auto

termination

proof

  show "wf (measure (\<lambda> (f, xs). last xs))"

    by auto

next

  fix f xs

  assume "last xs \<noteq> (0::nat)"

  thus "((f, butlast xs @ [last xs - 1]), f, xs) \<in> 

            measure (\<lambda>(f, xs). last xs)"

    by auto

qed

lemma rec_accum_Suc_simp_rewrite: 

  "primerec f (Suc (length xs))

    \<Longrightarrow> rec_exec (rec_accum f) (xs @ [Suc x]) = 

    rec_exec (rec_accum f) (xs @ [x]) * rec_exec f (xs @ [Suc x])"

  apply(induct x)

  apply(auto simp: rec_sigma.simps Let_def rec_pr_Suc_simp_rewrite

                   rec_exec.simps get_fstn_args_take)

  done  

text {*

  The correctness of @{text "rec_accum"} with respect to its specification.

*}

lemma accum_lemma :

  "primerec rg (Suc (length xs))

     \<Longrightarrow> rec_exec (rec_accum rg) (xs @ [x]) = Accum (rec_exec rg) (xs @ [x])"

apply(induct x)

apply(auto simp: rec_exec.simps rec_sigma.simps Let_def 

                     get_fstn_args_take)

done

declare rec_accum.simps [simp del]

text {*

  @{text "rec_all t f (x1, x2, \<dots>, xn)"} 

  computes the charactrization function of the following FOL formula:

  @{text "(\<forall> x \<le> t(x1, x2, \<dots>, xn). (f(x1, x2, \<dots>, xn, x) > 0))"}

*}

fun rec_all :: "recf \<Rightarrow> recf \<Rightarrow> recf"

  where

  "rec_all rt rf = 

    (let vl = arity rf in

       Cn (vl - 1) rec_sg [Cn (vl - 1) (rec_accum rf) 

                 (get_fstn_args (vl - 1) (vl - 1) @ [rt])])"

lemma rec_accum_ex: "primerec rf (Suc (length xs)) \<Longrightarrow>

     (rec_exec (rec_accum rf) (xs @ [x]) = 0) = 

      (\<exists> t \<le> x. rec_exec rf (xs @ [t]) = 0)"

apply(induct x, simp_all add: rec_accum_Suc_simp_rewrite)

apply(simp add: rec_exec.simps rec_accum.simps get_fstn_args_take, 

      auto)

apply(rule_tac x = ta in exI, simp)

apply(case_tac "t = Suc x", simp_all)

apply(rule_tac x = t in exI, simp)

done

text {*

  The correctness of @{text "rec_all"}.

  *}

lemma all_lemma: 

  "\<lbrakk>primerec rf (Suc (length xs));

    primerec rt (length xs)\<rbrakk>

  \<Longrightarrow> rec_exec (rec_all rt rf) xs = (if (\<forall> x \<le> (rec_exec rt xs). 0 < rec_exec rf (xs @ [x])) then 1

                                                                                              else 0)"

apply(auto simp: rec_all.simps)

apply(simp add: rec_exec.simps map_append get_fstn_args_take split: if_splits)

apply(drule_tac x = "rec_exec rt xs" in rec_accum_ex)

apply(case_tac "rec_exec (rec_accum rf) (xs @ [rec_exec rt xs]) = 0", simp_all)

apply(erule_tac exE, erule_tac x = t in allE, simp)

apply(simp add: rec_exec.simps map_append get_fstn_args_take)

apply(drule_tac x = "rec_exec rt xs" in rec_accum_ex)

apply(case_tac "rec_exec (rec_accum rf) (xs @ [rec_exec rt xs]) = 0", simp, simp)

apply(erule_tac x = x in allE, simp)

done

text {*

  @{text "rec_ex t f (x1, x2, \<dots>, xn)"} 

  computes the charactrization function of the following FOL formula:

  @{text "(\<exists> x \<le> t(x1, x2, \<dots>, xn). (f(x1, x2, \<dots>, xn, x) > 0))"}

*}

fun rec_ex :: "recf \<Rightarrow> recf \<Rightarrow> recf"

  where

  "rec_ex rt rf = 

       (let vl = arity rf in 

         Cn (vl - 1) rec_sg [Cn (vl - 1) (rec_sigma rf) 

                  (get_fstn_args (vl - 1) (vl - 1) @ [rt])])"

lemma rec_sigma_ex: "primerec rf (Suc (length xs))

          \<Longrightarrow> (rec_exec (rec_sigma rf) (xs @ [x]) = 0) = 

                          (\<forall> t \<le> x. rec_exec rf (xs @ [t]) = 0)"

apply(induct x, simp_all add: rec_sigma_Suc_simp_rewrite)

apply(simp add: rec_exec.simps rec_sigma.simps 

                get_fstn_args_take, auto)

apply(case_tac "t = Suc x", simp_all)

done

text {*

  The correctness of @{text "ex_lemma"}.

  *}

lemma ex_lemma:"

  \<lbrakk>primerec rf (Suc (length xs));

   primerec rt (length xs)\<rbrakk>

\<Longrightarrow> (rec_exec (rec_ex rt rf) xs =

    (if (\<exists> x \<le> (rec_exec rt xs). 0 <rec_exec rf (xs @ [x])) then 1

     else 0))"

apply(auto simp: rec_ex.simps rec_exec.simps map_append get_fstn_args_take 

            split: if_splits)

apply(drule_tac x = "rec_exec rt xs" in rec_sigma_ex, simp)

apply(drule_tac x = "rec_exec rt xs" in rec_sigma_ex, simp)

done

text {*

  Definition of @{text "Min[R]"} on page 77 of Boolos's book.

*}

fun Minr :: "(nat list \<Rightarrow> bool) \<Rightarrow> nat list \<Rightarrow> nat \<Rightarrow> nat"

  where "Minr Rr xs w = (let setx = {y | y. (y \<le> w) \<and> Rr (xs @ [y])} in 

                        if (setx = {}) then (Suc w)

                                       else (Min setx))"

declare Minr.simps[simp del] rec_all.simps[simp del]

text {*

  The following is a set of auxilliary lemmas about @{text "Minr"}.

*}

lemma Minr_range: "Minr Rr xs w \<le> w \<or> Minr Rr xs w = Suc w"

apply(auto simp: Minr.simps)

apply(subgoal_tac "Min {x. x \<le> w \<and> Rr (xs @ [x])} \<le> x")

apply(erule_tac order_trans, simp)

apply(rule_tac Min_le, auto)

done

lemma expand_conj_in_set: "{x. x \<le> Suc w \<and> Rr (xs @ [x])}

    = (if Rr (xs @ [Suc w]) then insert (Suc w) 

                              {x. x \<le> w \<and> Rr (xs @ [x])}

      else {x. x \<le> w \<and> Rr (xs @ [x])})"

by(auto, case_tac "x = Suc w", auto)

lemma Minr_strip_Suc[simp]: "Minr Rr xs w \<le> w \<Longrightarrow> Minr Rr xs (Suc w) = Minr Rr xs w"

by(cases "\<forall>x\<le>w. \<not> Rr (xs @ [x])",auto simp add: Minr.simps expand_conj_in_set)