(* 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 

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