diff -r 745547bdc1c7 -r ff54a3308fd6 thys/Recs.thy --- 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 \ 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 \ 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 \ divby2 n = n" - "even n \ divby2 n = divby2 (n div 2)" -apply(simp_all add: divby2.simps) +lemma oddfactor[simp]: + "oddfactor 0 = 0" + "odd n \ oddfactor n = n" + "even n \ oddfactor n = oddfactor (n div 2)" +apply(simp_all add: oddfactor.simps) done -lemma divby2_odd: - "divby2 n = 0 \ odd (divby2 n)" +lemma oddfactor_odd: + "oddfactor n = 0 \ 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 \ nat" where - "pdecode2 z = (divby2 (Suc z) - 1) div 2" + "pdecode2 z = (oddfactor (Suc z) - 1) div 2" fun pdecode1 :: "nat \ nat" where - "pdecode1 z = log ((Suc z) div (divby2 (Suc z)))" + "pdecode1 z = log ((Suc z) div (oddfactor (Suc z)))" lemma k: - "odd n \ divby2 (2 ^ m * n) = n" + "odd n \ oddfactor (2 ^ m * n) = n" apply(induct m) apply(simp_all) done -lemma ww: "\k. n = 2 ^ k * divby2 n" +lemma ww: "\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 \ 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)