(* Title: thys/Rec_Def.thy
   Author: Jian Xu, Xingyuan Zhang, and Christian Urban
*)

header {* Definition of Recursive Functions *}


theory Rec_Def
imports Main
begin

section {* Recursive functions *}

datatype recf = 
  z | s | 
  -- {* The projection function, where @{text "id i j"} returns the @{text "j"}-th
  argment out of the @{text "i"} arguments. *}
  id nat nat | 
  -- {* The compostion operator, where "@{text "Cn n f [g1; g2; \<dots> ;gm]"} 
  computes @{text "f (g1(x1, x2, \<dots>, xn), g2(x1, x2, \<dots>, xn), \<dots> , 
  gm(x1, x2, \<dots> , xn))"} for input argments @{text "x1, \<dots>, xn"}. *}
  Cn nat recf "recf list" | 
  -- {* The primitive resursive operator, where @{text "Pr n f g"} computes:
  @{text "Pr n f g (x1, x2, \<dots>, xn-1, 0) = f(x1, \<dots>, xn-1)"} 
  and @{text "Pr n f g (x1, x2, \<dots>, xn-1, k') = g(x1, x2, \<dots>, xn-1, k, 
                                            Pr n f g (x1, \<dots>, xn-1, k))"}.
  *}
  Pr nat recf recf | 
  -- {* The minimization operator, where @{text "Mn n f (x1, x2, \<dots> , xn)"} 
  computes the first i such that @{text "f (x1, \<dots>, xn, i) = 0"} and for all
  @{text "j"}, @{text "f (x1, x2, \<dots>, xn, j) > 0"}. *}
  Mn nat recf 

(*
partial_function (tailrec) 
  rec_exec :: "recf \<Rightarrow> nat list \<Rightarrow> nat"
where
  "rec_exec f ns = (case (f, ns) of
      (z, xs) => 0
   |  (s, xs) => Suc (xs ! 0)
   |  (id m n, xs) => (xs ! n) 
   |  (Cn n f gs, xs) => 
             (let ys = (map (\<lambda> a. rec_exec a xs) gs) in 
                                  rec_exec f ys)
   |  (Pr n f g, xs) => 
         (if last xs = 0 then rec_exec f (butlast xs)
          else rec_exec g (butlast xs @ [last xs - 1] @
            [rec_exec (Pr n f g) (butlast xs @ [last xs - 1])]))
   |  (Mn n f, xs) => (LEAST x. rec_exec f (xs @ [x]) = 0))"
*)

text {* 
  The semantis of recursive operators is given by an inductively defined
  relation as follows, where  
  @{text "rec_calc_rel R [x1, x2, \<dots>, xn] r"} means the computation of 
  @{text "R"} over input arguments @{text "[x1, x2, \<dots>, xn"} terminates
  and gives rise to a result @{text "r"}
*}

inductive rec_calc_rel :: "recf \<Rightarrow> nat list \<Rightarrow> nat \<Rightarrow> bool"
where
  calc_z: "rec_calc_rel z [n] 0" |
  calc_s: "rec_calc_rel s [n] (Suc n)" |
  calc_id: "\<lbrakk>length args = i; j < i; args!j = r\<rbrakk> \<Longrightarrow> rec_calc_rel (id i j) args r" |
  calc_cn: "\<lbrakk>length args = n;
             \<forall> k < length gs. rec_calc_rel (gs ! k) args (rs ! k);
             length rs = length gs; 
             rec_calc_rel f rs r\<rbrakk> 
            \<Longrightarrow> rec_calc_rel (Cn n f gs) args r" |
  calc_pr_zero: 
           "\<lbrakk>length args = n;
             rec_calc_rel f args r0 \<rbrakk> 
            \<Longrightarrow> rec_calc_rel (Pr n f g) (args @ [0]) r0" |
  calc_pr_ind: "
           \<lbrakk> length args = n;
             rec_calc_rel (Pr n f g) (args @ [k]) rk; 
             rec_calc_rel g (args @ [k] @ [rk]) rk'\<rbrakk>
            \<Longrightarrow> rec_calc_rel (Pr n f g) (args @ [Suc k]) rk'"  |
  calc_mn: "\<lbrakk>length args = n; 
             rec_calc_rel f (args@[r]) 0; 
             \<forall> i < r. (\<exists> ri. rec_calc_rel f (args@[i]) ri \<and> ri \<noteq> 0)\<rbrakk> 
            \<Longrightarrow> rec_calc_rel (Mn n f) args r" 

inductive_cases calc_pr_reverse: "rec_calc_rel (Pr n f g) (lm) rSucy"

inductive_cases calc_z_reverse: "rec_calc_rel z lm x"

inductive_cases calc_s_reverse: "rec_calc_rel s lm x"

inductive_cases calc_id_reverse: "rec_calc_rel (id m n) lm x"

inductive_cases calc_cn_reverse: "rec_calc_rel (Cn n f gs) lm x"

inductive_cases calc_mn_reverse:"rec_calc_rel (Mn n f) lm x"
end