
diff -r 002b07ea0a57 -r fa40fd8abb54 thys2/Recs.thy
--- a/thys2/Recs.thy	Thu Jun 06 17:27:45 2013 +0100
+++ b/thys2/Recs.thy	Wed Jun 26 14:35:43 2013 +0100
@@ -213,7 +213,7 @@
 | termi_pr: "\<lbrakk>\<forall> y < x. terminates g (y # (rec_eval (Pr n f g) (y # xs) # xs));
               terminates f xs;
               length xs = n\<rbrakk> 
-              \<Longrightarrow> terminates (Pr n f g) (xs @ [x])"
+              \<Longrightarrow> terminates (Pr n f g) (x # xs)"
 | termi_mn: "\<lbrakk>length xs = n; terminates f (r # xs); 
               rec_eval f (r # xs) = 0;
               \<forall> i < r. terminates f (i # xs) \<and> rec_eval f (i # xs) > 0\<rbrakk> \<Longrightarrow> terminates (Mn n f) xs"
@@ -242,8 +242,11 @@
 definition 
   "rec_power = rec_swap (PR (constn 1) (CN rec_mult [Id 3 1, Id 3 2]))"
 
+definition 
+  "rec_fact_aux = PR (constn 1) (CN rec_mult [CN S [Id 3 0], Id 3 1])"
+
 definition
-  "rec_fact = PR (constn 1) (CN rec_mult [CN S [Id 3 0], Id 3 1])"
+  "rec_fact = CN rec_fact_aux [Id 1 0, Id 1 0]"
 
 definition 
   "rec_pred = CN (PR Z (Id 3 0)) [Id 1 0, Id 1 0]"
@@ -271,9 +274,13 @@
   "rec_eval rec_power [x, y] = x ^ y"
 by (induct y) (simp_all add: rec_power_def)
 
+lemma fact_aux_lemma [simp]: 
+  "rec_eval rec_fact_aux [x, y] = fact x"
+by (induct x) (simp_all add: rec_fact_aux_def)
+
 lemma fact_lemma [simp]: 
   "rec_eval rec_fact [x] = fact x"
-by (induct x) (simp_all add: rec_fact_def)
+by (simp add: rec_fact_def)
 
 lemma pred_lemma [simp]: 
   "rec_eval rec_pred [x] =  x - 1"
@@ -300,7 +307,7 @@
   @{text "rec_eq"} compares two arguments: returns @{text "1"}
   if they are equal; @{text "0"} otherwise. *}
 definition 
-  "rec_eq = CN rec_minus [constn 1, CN rec_add [rec_minus, rec_swap rec_minus]]"
+  "rec_eq = CN rec_minus [CN (constn 1) [Id 2 0], CN rec_add [rec_minus, rec_swap rec_minus]]"
 
 definition 
   "rec_noteq = CN rec_not [rec_eq]"
@@ -385,36 +392,40 @@
 section {* Summation and Product Functions *}
 
 definition 
-  "rec_sigma1 f = PR (CN f [Z, Id 1 0]) (CN rec_add [Id 3 1, CN f [S, Id 3 2]])"
+  "rec_sigma1 f = PR (CN f [CN Z [Id 1 0], Id 1 0]) 
+                     (CN rec_add [Id 3 1, CN f [CN S [Id 3 0], Id 3 2]])"
 
 definition 
-  "rec_sigma2 f = PR (CN f [Z, Id 2 0, Id 2 1]) (CN rec_add [Id 4 1, CN f [S, Id 4 2, Id 4 3]])"
+  "rec_sigma2 f = PR (CN f [CN Z [Id 2 0], Id 2 0, Id 2 1]) 
+                     (CN rec_add [Id 4 1, CN f [CN S [Id 4 0], Id 4 2, Id 4 3]])"
 
 definition 
-  "rec_accum1 f = PR (CN f [Z, Id 1 0]) (CN rec_mult [Id 3 1, CN f [S, Id 3 2]])"
+  "rec_accum1 f = PR (CN f [CN Z [Id 1 0], Id 1 0]) 
+                     (CN rec_mult [Id 3 1, CN f [CN S [Id 3 0], Id 3 2]])"
 
 definition 
-  "rec_accum2 f = PR (CN f [Z, Id 2 0, Id 2 1]) (CN rec_mult [Id 4 1, CN f [S, Id 4 2, Id 4 3]])"
+  "rec_accum2 f = PR (CN f [CN Z [Id 2 0], Id 2 0, Id 2 1]) 
+                     (CN rec_mult [Id 4 1, CN f [CN S [Id 4 0], Id 4 2, Id 4 3]])"
 
 definition 
-  "rec_accum3 f = PR (CN f [Z, Id 3 0, Id 3 1, Id 3 2]) 
-                     (CN rec_mult [Id 5 1, CN f [S, Id 5 2, Id 5 3, Id 5 4]])"
+  "rec_accum3 f = PR (CN f [CN Z [Id 3 0], Id 3 0, Id 3 1, Id 3 2]) 
+                     (CN rec_mult [Id 5 1, CN f [CN S [Id 5 0], Id 5 2, Id 5 3, Id 5 4]])"
 
 
 lemma sigma1_lemma [simp]: 
-  shows "rec_eval (rec_sigma1 f) [x, y] = (\<Sum> z \<le> x. (rec_eval f)  [z, y])"
+  shows "rec_eval (rec_sigma1 f) [x, y] = (\<Sum> z \<le> x. rec_eval f [z, y])"
 by (induct x) (simp_all add: rec_sigma1_def)
 
 lemma sigma2_lemma [simp]: 
-  shows "rec_eval (rec_sigma2 f) [x, y1, y2] = (\<Sum> z \<le> x. (rec_eval f)  [z, y1, y2])"
+  shows "rec_eval (rec_sigma2 f) [x, y1, y2] = (\<Sum> z \<le> x. rec_eval f  [z, y1, y2])"
 by (induct x) (simp_all add: rec_sigma2_def)
 
 lemma accum1_lemma [simp]: 
-  shows "rec_eval (rec_accum1 f) [x, y] = (\<Prod> z \<le> x. (rec_eval f)  [z, y])"
+  shows "rec_eval (rec_accum1 f) [x, y] = (\<Prod> z \<le> x. rec_eval f  [z, y])"
 by (induct x) (simp_all add: rec_accum1_def)
 
 lemma accum2_lemma [simp]: 
-  shows "rec_eval (rec_accum2 f) [x, y1, y2] = (\<Prod> z \<le> x. (rec_eval f)  [z, y1, y2])"
+  shows "rec_eval (rec_accum2 f) [x, y1, y2] = (\<Prod> z \<le> x. rec_eval f  [z, y1, y2])"
 by (induct x) (simp_all add: rec_accum2_def)
 
 lemma accum3_lemma [simp]: 
@@ -434,8 +445,9 @@
   "rec_all3 f = CN rec_sign [rec_accum3 f]"
 
 definition
-  "rec_all1_less f = (let f' = CN rec_disj [CN rec_eq [Id 3 0, Id 3 1], CN f [Id 3 0, Id 3 2]] 
-                      in CN (rec_all2 f') [Id 2 0, Id 2 0, Id 2 1])"
+  "rec_all1_less f = (let cond1 = CN rec_eq [Id 3 0, Id 3 1] in
+                      let cond2 = CN f [Id 3 0, Id 3 2] 
+                      in CN (rec_all2 (CN rec_disj [cond1, cond2])) [Id 2 0, Id 2 0, Id 2 1])"
 
 definition
   "rec_all2_less f = (let cond1 = CN rec_eq [Id 4 0, Id 4 1] in 
@@ -540,7 +552,7 @@
 section {* Iteration *}
 
 definition
-   "rec_iter f = PR (Id 2 0) (CN f [Id 3 1])"
+   "rec_iter f = PR (Id 1 0) (CN f [Id 3 1])"
 
 fun Iter where
   "Iter f 0 = id"
@@ -585,14 +597,14 @@
 by (simp add: BMax_rec_eq2 Set.filter_def)
 
 definition 
-  "rec_max1 f = PR (constn 0) (CN rec_ifz [CN f [CN S [Id 3 0], Id 3 2], CN S [Id 4 0], Id 4 1])"
+  "rec_max1 f = PR Z (CN rec_ifz [CN f [CN S [Id 3 0], Id 3 2], CN S [Id 3 0], Id 3 1])"
  
 lemma max1_lemma [simp]:
   "rec_eval (rec_max1 f) [x, y] = BMax_rec (\<lambda>u. rec_eval f [u, y] = 0) x"
 by (induct x) (simp_all add: rec_max1_def)
 
 definition 
-  "rec_max2 f = PR (constn 0) (CN rec_ifz [CN f [CN S [Id 4 0], Id 4 2, Id 4 3], CN S [Id 4 0], Id 4 1])"
+  "rec_max2 f = PR Z (CN rec_ifz [CN f [CN S [Id 4 0], Id 4 2, Id 4 3], CN S [Id 4 0], Id 4 1])"
  
 lemma max2_lemma [simp]:
   "rec_eval (rec_max2 f) [x, y1, y2] = BMax_rec (\<lambda>u. rec_eval f [u, y1, y2] = 0) x"
@@ -801,7 +813,7 @@
 by (simp add: enclen_def)
 
 
-text {* Recursive De3finitions for List Encodings *}
+text {* Recursive Definitions for List Encodings *}
 
 fun 
   rec_lenc :: "recf list \<Rightarrow> recf" 




