theory Rec_Def

imports Main

begin

datatype recf = 

  id nat nat | 

  computes @{text "f (g1(x1, x2, \<dots>, xn), g2(x1, x2, \<dots>, xn), \<dots> , 

  Cn nat recf "recf list" | 

  @{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 nat recf recf | 

  computes the first i such that @{text "f (x1, \<dots>, xn, i) = 0"} and for all

  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_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