--- a/thys/UF_Rec.thy	Wed May 15 15:07:27 2013 +0100
+++ b/thys/UF_Rec.thy	Thu May 16 07:19:26 2013 +0100
@@ -4,8 +4,6 @@
 
 
 
-
-
 section {* Universal Function in HOL *}
 
 text {*
@@ -73,36 +71,21 @@
 
 fun Trpl :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
   where
-  "Trpl p q r = (Pi 0) ^ p * (Pi 1) ^ q * (Pi 2) ^ r"
+  "Trpl p q r = list_encode [p, q, r]"
 
 fun Left where
-  "Left c = Lo c (Pi 0)"
+  "Left c = list_decode c ! 0"
 
 fun Right where
-  "Right c = Lo c (Pi 2)"
+  "Right c = list_decode c ! 1"
 
 fun Stat where
-  "Stat c = Lo c (Pi 1)"
+  "Stat c = list_decode c ! 2"
 
 lemma mod_dvd_simp: 
   "(x mod y = (0::nat)) = (y dvd x)"
 by(auto simp add: dvd_def)
 
-lemma Trpl_Left [simp]:
-  "Left (Trpl p q r) = p"
-apply(simp)
-apply(subst Lo_def)
-apply(subst dvd_eq_mod_eq_0[symmetric])
-apply(simp)
-apply(auto)
-thm Lo_def
-thm mod_dvd_simp
-apply(simp add: left.simps trpl.simps lo.simps 
-              loR.simps mod_dvd_simp, auto simp: conf_decode1)
-apply(case_tac "Pi 0 ^ l * Pi (Suc 0) ^ st * Pi (Suc (Suc 0)) ^ r",
-      auto)
-apply(erule_tac x = l in allE, auto)
-
 
 fun Inpt :: "nat \<Rightarrow> nat list \<Rightarrow> nat"
   where
@@ -312,19 +295,16 @@
                   in CN rec_if [Id 3 1, entry, Z])"
 
 definition 
-  "rec_trpl = CN rec_mult [CN rec_mult 
-       [CN rec_power [constn (Pi 0), Id 3 0], 
-        CN rec_power [constn (Pi 1), Id 3 1]],
-        CN rec_power [constn (Pi 2), Id 3 2]]"
+  "rec_trpl = CN rec_penc [CN rec_penc [Id 3 0, Id 3 1], Id 3 2]"
 
 definition
-  "rec_left = CN rec_lo [Id 1 0, constn (Pi 0)]"
+  "rec_left = rec_pdec1"
 
 definition 
-  "rec_right = CN rec_lo [Id 1 0, constn (Pi 2)]"
+  "rec_right = CN rec_pdec2 [rec_pdec1]"
 
 definition 
-  "rec_stat = CN rec_lo [Id 1 0, constn (Pi 1)]"
+  "rec_stat = CN rec_pdec2 [rec_pdec2]"
 
 definition 
   "rec_newconf = (let act = CN rec_actn [Id 2 0, CN rec_stat [Id 2 1], CN rec_right [Id 2 1]] in
@@ -412,7 +392,8 @@
 
 lemma trpl_lemma [simp]: 
   "rec_eval rec_trpl [p, q, r] = Trpl p q r"
-by (simp add: rec_trpl_def)
+apply(simp)
+apply (simp add: rec_trpl_def)
 
 lemma left_lemma [simp]:
   "rec_eval rec_left [c] = Left c"