theory Rec_def2imports Mainbegindatatype recf = z | s | id nat nat | Cn nat recf "recf list" | Pr nat recf recf | Mn nat recf function rec_exec :: "recf \<Rightarrow> nat list \<Rightarrow> nat" where "rec_exec z xs = 0" | "rec_exec s xs = (Suc (xs ! 0))" | "rec_exec (id m n) xs = (xs ! n)" | "rec_exec (Cn n f gs) xs = (let ys = (map (\<lambda> a. rec_exec a xs) gs) in rec_exec f ys)" | "rec_exec (Pr n f g) xs = (if hd xs = 0 then rec_exec f (tl xs) else rec_exec g ((hd xs - 1) # tl xs @ [rec_exec (Pr n f g) ((hd xs - 1) # tl xs)]))" | "rec_exec (Mn n f) xs = (LEAST x. rec_exec f (x # xs) = 0)"by pat_completeness autoterminationapply(relation "measures [\<lambda> (r, xs). size r, (\<lambda> (r, xs). hd xs)]")apply(auto simp add: less_Suc_eq_le intro: trans_le_add2 list_size_estimation')doneinductive terminate :: "recf \<Rightarrow> nat list \<Rightarrow> bool" where termi_z: "terminate z [n]"| termi_s: "terminate s [n]"| termi_id: "\<lbrakk>n < m; length xs = m\<rbrakk> \<Longrightarrow> terminate (id m n) xs"| termi_cn: "\<lbrakk>terminate f (map (\<lambda>g. rec_exec g xs) gs); \<forall>g \<in> set gs. terminate g xs; length xs = n\<rbrakk> \<Longrightarrow> terminate (Cn n f gs) xs"| termi_pr_0: "\<lbrakk>terminate f xs; length xs = n\<rbrakk> \<Longrightarrow> terminate (Pr n f g) (0 # xs)"| termi_pr_suc: "\<lbrakk>terminate (Pr n f gs) (x # xs); terminate g (x # rec_exec (Pr n f gs) (x # xs) # xs)\<rbrakk> \<Longrightarrow> terminate (Pr n f gs) (Suc x # xs)"| termi_mn: "\<lbrakk>length xs = n; rec_exec f (r # xs) = 0; \<forall> i < r. terminate f (i # xs) \<and> rec_exec f (i # xs) > 0\<rbrakk> \<Longrightarrow> terminate (Mn n f) xs"end