theory rec_defimports Mainbeginsection {* Recursive functions*}text {* Datatype of recursive operators.*}datatype recf = -- {* The zero function, which always resturns @{text "0"} as result. *} z | -- {* The successor function, which increments its arguments. *} 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