theory Rec_Defimports 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 = rec_exec f (map (\<lambda> a. rec_exec a xs) gs)" | "rec_exec (Pr n f g) xs = (if last xs = 0 then rec_exec f (butlast xs) else rec_exec g (butlast xs @ (last xs - 1) # [rec_exec (Pr n f g) (butlast xs @ [last xs - 1])]))" | "rec_exec (Mn n f) xs = (LEAST x. rec_exec f (xs @ [x]) = 0)"by pat_completeness autoterminationapply(relation "measures [\<lambda> (r, xs). size r, (\<lambda> (r, xs). last xs)]")apply(auto simp add: less_Suc_eq_le intro: trans_le_add2 list_size_estimation')doneinductive terminates :: "recf \<Rightarrow> nat list \<Rightarrow> bool"where termi_z: "terminates z [n]"| termi_s: "terminates s [n]"| termi_id: "\<lbrakk>n < m; length xs = m\<rbrakk> \<Longrightarrow> terminates (id m n) xs"| termi_cn: "\<lbrakk>terminates f (map (\<lambda>g. rec_exec g xs) gs); \<forall>g \<in> set gs. terminates g xs; length xs = n\<rbrakk> \<Longrightarrow> terminates (Cn n f gs) xs"| termi_pr: "\<lbrakk>\<forall> y < x. terminates g (xs @ y # [rec_exec (Pr n f g) (xs @ [y])]); terminates f xs; length xs = n\<rbrakk> \<Longrightarrow> terminates (Pr n f g) (xs @ [x])"| termi_mn: "\<lbrakk>length xs = n; terminates f (xs @ [r]); rec_exec f (xs @ [r]) = 0; \<forall> i < r. terminates f (xs @ [i]) \<and> rec_exec f (xs @ [i]) > 0\<rbrakk> \<Longrightarrow> terminates (Mn n f) xs"inductive_cases terminates_pr_reverse: "terminates (Pr n f g) xs"inductive_cases terminates_z_reverse[elim!]: "terminates z xs"inductive_cases terminates_s_reverse[elim!]: "terminates s xs"inductive_cases terminates_id_reverse[elim!]: "terminates (id m n) xs"inductive_cases terminates_cn_reverse[elim!]: "terminates (Cn n f gs) xs"inductive_cases terminates_mn_reverse[elim!]:"terminates (Mn n f) xs"end