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