--- a/thys/Rec_Def.thy	Wed Apr 24 09:49:00 2013 +0100
+++ b/thys/Rec_Def.thy	Thu Apr 25 21:37:05 2013 +0100
@@ -9,14 +9,10 @@
               |  Pr nat recf recf
               |  Mn nat recf 
 
-definition pred_of_nl :: "nat list \<Rightarrow> nat list"
-  where
-  "pred_of_nl xs = butlast xs @ [last xs - 1]"
-
 function rec_exec :: "recf \<Rightarrow> nat list \<Rightarrow> nat"
   where
   "rec_exec z xs = 0" |
-  "rec_exec s xs = (Suc (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)" | 
@@ -31,32 +27,33 @@
 apply(auto simp add: less_Suc_eq_le intro: trans_le_add2 list_size_estimation')
 done
 
-inductive 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: "\<lbrakk>\<forall> y < x. terminate g (xs @ y # [rec_exec (Pr n f g) (xs @ [y])]);
-              terminate f xs;
+inductive 
+  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> terminate (Pr n f g) (xs @ [x])"
-| termi_mn: "\<lbrakk>length xs = n; terminate f (xs @ [r]); 
+              \<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. terminate f (xs @ [i]) \<and> rec_exec f (xs @ [i]) > 0\<rbrakk> \<Longrightarrow> terminate (Mn n f) xs"
+              \<forall> i < r. terminates f (xs @ [i]) \<and> rec_exec f (xs @ [i]) > 0\<rbrakk> \<Longrightarrow> terminates (Mn n f) xs"
 
 
-inductive_cases terminate_pr_reverse: "terminate (Pr n f g) xs"
+inductive_cases terminates_pr_reverse: "terminates (Pr n f g) xs"
 
-inductive_cases terminate_z_reverse[elim!]: "terminate z xs"
+inductive_cases terminates_z_reverse[elim!]: "terminates z xs"
 
-inductive_cases terminate_s_reverse[elim!]: "terminate s xs"
+inductive_cases terminates_s_reverse[elim!]: "terminates s xs"
 
-inductive_cases terminate_id_reverse[elim!]: "terminate (id m n) xs"
+inductive_cases terminates_id_reverse[elim!]: "terminates (id m n) xs"
 
-inductive_cases terminate_cn_reverse[elim!]: "terminate (Cn n f gs) xs"
+inductive_cases terminates_cn_reverse[elim!]: "terminates (Cn n f gs) xs"
 
-inductive_cases terminate_mn_reverse[elim!]:"terminate (Mn n f) xs"
+inductive_cases terminates_mn_reverse[elim!]:"terminates (Mn n f) xs"
 
 end
\ No newline at end of file