equal
deleted
inserted
replaced
26 "rec_exec (Mn n f) xs = (LEAST x. rec_exec f (xs @ [x]) = 0)" |
26 "rec_exec (Mn n f) xs = (LEAST x. rec_exec f (xs @ [x]) = 0)" |
27 by pat_completeness auto |
27 by pat_completeness auto |
28 |
28 |
29 termination |
29 termination |
30 apply(relation "measures [\<lambda> (r, xs). size r, (\<lambda> (r, xs). last xs)]") |
30 apply(relation "measures [\<lambda> (r, xs). size r, (\<lambda> (r, xs). last xs)]") |
31 apply(auto simp add: less_Suc_eq_le intro: trans_le_add2 list_size_estimation') |
31 apply(auto simp add: less_Suc_eq_le intro: trans_le_add2 size_list_estimation'[THEN trans_le_add1]) |
32 done |
32 done |
33 |
33 |
34 inductive terminate :: "recf \<Rightarrow> nat list \<Rightarrow> bool" |
34 inductive terminate :: "recf \<Rightarrow> nat list \<Rightarrow> bool" |
35 where |
35 where |
36 termi_z: "terminate z [n]" |
36 termi_z: "terminate z [n]" |