diff -r 0846c45cedbb -r 0546ae452747 thys/NatBijection.thy
--- a/thys/NatBijection.thy	Mon May 13 14:08:54 2013 +0100
+++ b/thys/NatBijection.thy	Mon May 13 15:28:48 2013 +0100
@@ -6,18 +6,44 @@
 
 fun oddfactor :: "nat \<Rightarrow> nat" where
   [simp del]: "oddfactor n = (if n = 0 then 0 
-                              else if even n then oddfactor (n div 2) else n)"
+                              else if even n then oddfactor (n div 2) else ((n - 1) div 2))"
 
 fun evenfactor :: "nat \<Rightarrow> nat" where
   [simp del]: "evenfactor n = (if n = 0 then 0 
                                else if even n then 2 * evenfactor (n div 2) else 1)"
 
-lemma oddfactor[simp]:
+lemma oddfactor [simp]:
   "oddfactor 0 = 0"
-  "odd n \<Longrightarrow> oddfactor n = n"
+  "odd n \<Longrightarrow> oddfactor n = (n - 1) div 2"
   "even n \<Longrightarrow> oddfactor n = oddfactor (n div 2)"
 by (simp_all add: oddfactor.simps)
 
+lemma evenfactor [simp]:
+  "evenfactor 0 = 0"
+  "odd n \<Longrightarrow> evenfactor n = 1"
+  "even n \<Longrightarrow> evenfactor n = 2 * evenfactor (n div 2)"
+apply(simp_all add: evenfactor.simps)
+apply(case_tac n)
+apply(simp_all)
+done
+
+fun penc :: "(nat \<times> nat) \<Rightarrow> nat" where
+  "penc (m, n) = (2 ^ m) * (2 * n + 1) - 1"
+
+fun pdec :: "nat \<Rightarrow> nat \<times> nat" where
+  "pdec z = (Discrete.log (evenfactor (Suc z)), oddfactor (Suc z))"
+
+lemma q2: "pdec (penc m) = m"
+apply(case_tac m)
+apply(simp)
+apply(simp only: penc.simps pdec.simps)
+apply(case_tac m)
+apply(simp only: penc.simps pdec.simps)
+apply(subst y1)
+apply(subst y2)
+apply(simp)
+done
+
 
 lemma oddfactor_odd:
   "oddfactor n = 0 \<or> odd (oddfactor n)"