--- a/thys/Recs.thy	Thu May 16 07:19:26 2013 +0100
+++ b/thys/Recs.thy	Tue May 21 13:49:31 2013 +0100
@@ -587,8 +587,11 @@
 section {* Encodings using Cantor's pairing function *}
 
 text {*
-  We first have to prove that we can extract the maximal
-  triangle number using @{term prod_decode}.
+  We use Cantor's pairing function from Nat_Bijection.
+  However, we need to prove that the formulation of the
+  decoding function there is recursive. For this we first 
+  prove that we can extract the maximal triangle number 
+  using @{term prod_decode}.
 *}
 
 abbreviation Max_triangle_aux where
@@ -597,35 +600,41 @@
 abbreviation Max_triangle where
   "Max_triangle z \<equiv> Max_triangle_aux 0 z"
 
+abbreviation
+  "pdec1 z \<equiv> fst (prod_decode z)"
+
+abbreviation
+  "pdec2 z \<equiv> snd (prod_decode z)"
+
+abbreviation 
+  "penc m n \<equiv> prod_encode (m, n)"
+
 lemma fst_prod_decode: 
-  "fst (prod_decode z) = z - triangle (Max_triangle z)"
-apply(subst (3) prod_decode_inverse[symmetric]) 
-apply(simp add: prod_encode_def)
-apply(case_tac "prod_decode z")
-apply(simp add: prod_decode_def)
-done
+  "pdec1 z = z - triangle (Max_triangle z)"
+by (subst (3) prod_decode_inverse[symmetric]) 
+   (simp add: prod_encode_def prod_decode_def split: prod.split)
 
 lemma snd_prod_decode: 
-  "snd (prod_decode z) = Max_triangle z - fst (prod_decode z)"
+  "pdec2 z = Max_triangle z - pdec1 z"
 by (simp only: prod_decode_def)
 
 lemma le_triangle:
   "m \<le> triangle (n + m)"
 by (induct_tac m) (simp_all)
 
-lemma k_aux: 
-  "Max_triangle z \<le> z"
-apply(subst (8) prod_decode_inverse[symmetric])
-apply(case_tac "prod_decode z")
-apply(simp add: prod_decode_def prod_encode_def le_triangle)
-done
+lemma Max_triangle_triangle_le:
+  "triangle (Max_triangle z) \<le> z"
+by (subst (9) prod_decode_inverse[symmetric])
+   (simp add: prod_decode_def prod_encode_def split: prod.split)
 
-lemma t_aux:
-  "triangle (Max_triangle z) \<le> z"
-apply(subst (9) prod_decode_inverse[symmetric])
-apply(case_tac "prod_decode z")
-apply(simp add: prod_decode_def prod_encode_def)
-done
+lemma Max_triangle_le: 
+  "Max_triangle z \<le> z"
+proof -
+  have "Max_triangle z \<le> triangle (Max_triangle z)"
+    using le_triangle[of _ 0, simplified] by simp
+  also have "... \<le> z" by (rule Max_triangle_triangle_le)
+  finally show "Max_triangle z \<le> z" .
+qed
 
 lemma w_aux: 
   "Max_triangle (triangle k + m) = Max_triangle_aux k m"
@@ -648,8 +657,8 @@
 apply(rule Greatest_equality[symmetric])
 apply(rule disjI1)
 apply(rule conjI)
-apply(rule t_aux)
-apply(rule k_aux)
+apply(rule Max_triangle_triangle_le)
+apply(rule Max_triangle_le)
 apply(erule disjE)
 apply(erule conjE)
 apply(subst (asm) (1) le_iff_add)
@@ -686,18 +695,50 @@
   "rec_pdec2 = CN rec_minus [CN rec_max_triangle [Id 1 0], CN rec_pdec1 [Id 1 0]]" 
 
 lemma pdec1_lemma [simp]:
-  "rec_eval rec_pdec1 [z] = fst (prod_decode z)"
+  "rec_eval rec_pdec1 [z] = pdec1 z"
 by (simp add: rec_pdec1_def fst_prod_decode)
 
 lemma pdec2_lemma [simp]:
-  "rec_eval rec_pdec2 [z] = snd (prod_decode z)"
+  "rec_eval rec_pdec2 [z] = pdec2 z"
 by (simp add: rec_pdec2_def snd_prod_decode)
 
 lemma penc_lemma [simp]:
-  "rec_eval rec_penc [m, n] = prod_encode (m, n)"
+  "rec_eval rec_penc [m, n] = penc m n"
 by (simp add: rec_penc_def prod_encode_def)
 
+fun 
+  lenc :: "nat list \<Rightarrow> nat" 
+where
+  "lenc [] = 0"
+| "lenc (x # xs) = penc (Suc x) (lenc xs)"
 
+fun
+  ldec :: "nat \<Rightarrow> nat \<Rightarrow> nat"
+where
+  "ldec z 0 = (pdec1 z) - 1"
+| "ldec z (Suc n) = ldec (pdec2 z) n"
+
+lemma pdec_zero_simps [simp]:
+  "pdec1 0 = 0" 
+  "pdec2 0 = 0"
+by (simp_all add: prod_decode_def prod_decode_aux.simps)
+
+lemma w:
+  "ldec 0 n = 0"
+by (induct n) (simp_all add: prod_decode_def prod_decode_aux.simps)
+
+lemma list_encode_inverse: 
+  "ldec (lenc xs) n = (if n < length xs then xs ! n else 0)"
+apply(induct xs arbitrary: n rule: lenc.induct) 
+apply(simp_all add: w)
+apply(case_tac n)
+apply(simp_all)
+done
+
+fun within :: "nat \<Rightarrow> nat \<Rightarrow> bool" where
+  "within z 0 = (0 < z)"
+| "within z (Suc n) = within (pdec2 z) n"
+    
 
 section {* Discrete Logarithms *}