--- a/thys/Recs.thy	Thu May 09 18:16:36 2013 +0100
+++ b/thys/Recs.thy	Fri May 10 09:06:48 2013 +0100
@@ -627,19 +627,18 @@
   "log (2 ^ n) = n"
   by (induct n) simp_all
 
-fun divby2 :: "nat \<Rightarrow> nat" where
-  [simp del]: "divby2 n = (if n = 0 then 0
-                           else if even n then divby2 (n div 2) else n)"
+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)"
 
-lemma divby2[simp]:
-  "divby2 0 = 0"
-  "odd n \<Longrightarrow> divby2 n = n"
-  "even n \<Longrightarrow> divby2 n = divby2 (n div 2)"
-apply(simp_all add: divby2.simps)
+lemma oddfactor[simp]:
+  "oddfactor 0 = 0"
+  "odd n \<Longrightarrow> oddfactor n = n"
+  "even n \<Longrightarrow> oddfactor n = oddfactor (n div 2)"
+apply(simp_all add: oddfactor.simps)
 done
 
-lemma divby2_odd:
-  "divby2 n = 0 \<or> odd (divby2 n)" 
+lemma oddfactor_odd:
+  "oddfactor n = 0 \<or> odd (oddfactor n)" 
 apply(induct n rule: nat_less_induct)
 apply(case_tac "n = 0")
 apply(simp)
@@ -647,7 +646,7 @@
 apply(auto)
 done
 
-lemma bigger: "divby2 (Suc n) > 0"
+lemma bigger: "oddfactor (Suc n) > 0"
 apply(induct n rule: nat_less_induct)
 apply(case_tac "n = 0")
 apply(simp)
@@ -662,18 +661,18 @@
   "pencode m n = (2 ^ m) * ((2 * n) + 1) - 1"
 
 fun pdecode2 :: "nat \<Rightarrow> nat" where
-  "pdecode2 z = (divby2 (Suc z) - 1) div 2"
+  "pdecode2 z = (oddfactor (Suc z) - 1) div 2"
 
 fun pdecode1 :: "nat \<Rightarrow> nat" where
-  "pdecode1 z = log ((Suc z) div (divby2 (Suc z)))"
+  "pdecode1 z = log ((Suc z) div (oddfactor (Suc z)))"
 
 lemma k:
-  "odd n \<Longrightarrow> divby2 (2 ^ m * n) = n"
+  "odd n \<Longrightarrow> oddfactor (2 ^ m * n) = n"
 apply(induct m)
 apply(simp_all)
 done
 
-lemma ww: "\<exists>k. n = 2 ^ k * divby2 n"
+lemma ww: "\<exists>k. n = 2 ^ k * oddfactor n"
 apply(induct n rule: nat_less_induct)
 apply(case_tac "n=0")
 apply(simp)
@@ -707,7 +706,7 @@
 lemma test: "x = y \<Longrightarrow> 2 * x = 2 * y"
 by simp
 
-lemma m: "0 < n ==> 2 ^ log (n div (divby2 n)) = n div (divby2 n)"
+lemma m: "0 < n ==> 2 ^ log (n div (oddfactor n)) = n div (oddfactor n)"
 apply(induct n rule: nat_less_induct)
 apply(case_tac "n=0")
 apply(simp)
@@ -718,29 +717,29 @@
 apply(auto)[1]
 apply(drule mp)
 apply (metis One_nat_def Suc_lessI div_2_gt_zero odd_1_nat)
-apply(subst (asm) divby2(3)[symmetric])
+apply(subst (asm) oddfactor(3)[symmetric])
 apply(simp)
-apply(subst (asm) divby2(3)[symmetric])
+apply(subst (asm) oddfactor(3)[symmetric])
 apply(simp)
-apply(subgoal_tac "n div 2 div divby2 n = n div (divby2 n) div 2")
+apply(subgoal_tac "n div 2 div oddfactor n = n div (oddfactor n) div 2")
 prefer 2
 apply (metis div_mult2_eq nat_mult_commute)
 apply(simp only: log_half)
-apply(case_tac "n div divby2 n = 0")
+apply(case_tac "n div oddfactor n = 0")
 apply(simp)
-apply(simp del: divby2)
+apply(simp del: oddfactor)
 apply(drule test)
 apply(subst (asm) power.simps(2)[symmetric])
-apply(subgoal_tac "Suc (log (n div divby2 n) - 1) = log (n div divby2 n)")
+apply(subgoal_tac "Suc (log (n div oddfactor n) - 1) = log (n div oddfactor n)")
 prefer 2
 apply (smt Recs.log.simps Suc_1 div_less div_mult_self1_is_id log_half log_zero numeral_1_eq_Suc_0 numeral_One odd_1_nat odd_nat_plus_one_div_two one_less_numeral_iff power_one_right semiring_norm(76))
 apply(simp only:)
 apply(subst dvd_mult_div_cancel)
-apply (smt Suc_1 div_by_0 div_mult_self2_is_id divby2_odd dvd_power even_Suc even_numeral_nat even_product_nat nat_even_iff_2_dvd power_0 ww)
+apply (smt Suc_1 div_by_0 div_mult_self2_is_id oddfactor_odd dvd_power even_Suc even_numeral_nat even_product_nat nat_even_iff_2_dvd power_0 ww)
 apply(simp (no_asm))
 done
 
-lemma m1: "n div divby2 n * divby2 n = n"
+lemma m1: "n div oddfactor n * oddfactor n = n"
 apply(induct n rule: nat_less_induct)
 apply(case_tac "n=0")
 apply(simp)
@@ -750,10 +749,10 @@
 apply(drule_tac x="n div 2" in spec)
 apply(drule mp)
 apply(auto)[1]
-by (metis add_eq_if diff_add_inverse divby2(3) mod_eq_0_iff mult_div_cancel nat_mult_commute ww)
+by (metis add_eq_if diff_add_inverse oddfactor(3) mod_eq_0_iff mult_div_cancel nat_mult_commute ww)
 
 
-lemma m2: "0 < n ==> 2 ^ log (n div (divby2 n)) * (divby2 n) = n"
+lemma m2: "0 < n ==> 2 ^ log (n div (oddfactor n)) * (oddfactor n) = n"
 apply(subst m)
 apply(simp)
 apply(subst m1)
@@ -769,9 +768,11 @@
 
 lemma y2:
   "pdecode1 (pencode m n) = m"
+using [[simp_trace]]
 apply(simp)
 apply(subst k)
 apply(auto)[1]
+using [[simp_trace_depth_limit=10]]
 apply(simp)
 done
 
@@ -782,7 +783,7 @@
 apply(case_tac "n = 0")
 apply(simp)
 apply(subst dvd_mult_div_cancel)
-using divby2_odd
+using oddfactor_odd
 apply -
 apply(drule_tac x="Suc n" in meta_spec)
 apply(erule disjE)