# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1547213874 0
# Node ID bee184c830718ddf0c1dc6c868967142fd36f8ac
# Parent  3fee65a4083836f717b2496efeab3a471802025f
added some text  at the beginning

diff -r 3fee65a40838 -r bee184c83071 thys2/Recs.thy
--- a/thys2/Recs.thy	Thu Jan 10 13:18:07 2019 +0000
+++ b/thys2/Recs.thy	Fri Jan 11 13:37:54 2019 +0000
@@ -4,19 +4,22 @@
      "~~/src/HOL/Library/Discrete"
 begin
 
-declare One_nat_def[simp del]
 
-(*
-  some definitions from 
+text{*
+  A more streamlined and cleaned-up version of Recursive 
+  Functions following 
 
     A Course in Formal Languages, Automata and Groups
-    I M Chiswell 
+    I. M. Chiswell 
 
   and
 
-    Lecture on undecidability
+    Lecture on Undecidability
     Michael M. Wolf 
-*)
+*}
+
+declare One_nat_def[simp del]
+
 
 lemma if_zero_one [simp]:
   "(if P then 1 else 0) = (0::nat) \<longleftrightarrow> \<not> P"
@@ -248,10 +251,10 @@
   "rec_fact = CN rec_fact_aux [Id 1 0, Id 1 0]"
 
 definition 
-  "rec_predi = CN (PR Z (Id 3 0)) [Id 1 0, Id 1 0]"
+  "rec_predecessor = CN (PR Z (Id 3 0)) [Id 1 0, Id 1 0]"
 
 definition 
-  "rec_minus = rec_swap (PR (Id 1 0) (CN rec_predi [Id 3 1]))"
+  "rec_minus = rec_swap (PR (Id 1 0) (CN rec_predecessor [Id 3 1]))"
 
 lemma constn_lemma [simp]: 
   "rec_eval (constn n) xs = n"
@@ -282,8 +285,8 @@
 by (simp add: rec_fact_def)
 
 lemma pred_lemma [simp]: 
-  "rec_eval rec_predi [x] =  x - 1"
-by (induct x) (simp_all add: rec_predi_def)
+  "rec_eval rec_predecessor [x] =  x - 1"
+by (induct x) (simp_all add: rec_predecessor_def)
 
 lemma minus_lemma [simp]: 
   "rec_eval rec_minus [x, y] = x - y"
@@ -818,13 +821,13 @@
 | "rec_lenc (f # fs) = CN rec_penc [CN S [f], rec_lenc fs]"
 
 definition 
-  "rec_ldec = CN rec_predi [CN rec_pdec1 [rec_swap (rec_iter rec_pdec2)]]"
+  "rec_ldec = CN rec_predecessor [CN rec_pdec1 [rec_swap (rec_iter rec_pdec2)]]"
 
 definition 
   "rec_inside = CN rec_less [Z, rec_swap (rec_iter rec_pdec2)]"
 
 definition
-  "rec_enclen = CN (rec_max1 (CN rec_not [CN rec_inside [Id 2 1, CN rec_predi [Id 2 0]]])) [Id 1 0, Id 1 0]"
+  "rec_enclen = CN (rec_max1 (CN rec_not [CN rec_inside [Id 2 1, CN rec_predecessor [Id 2 0]]])) [Id 1 0, Id 1 0]"
 
 lemma ldec_iter:
   "ldec z n = pdec1 (Iter pdec2 n z) - 1"