2 imports Main 

     2 imports Main Fact 

     4          Fact

     4         "~~/src/HOL/Library/Nat_Bijection"

     5         "~~/src/HOL/Library/Discrete"

   593 fun log :: "nat \<Rightarrow> nat" where

   600 fun prod_decode1 where

   594   [simp del]: "log n = (if n < 2 then 0 else Suc (log (n div 2)))"

   601   "prod_decode1 z = z - (triangle (BMax_rec (\<lambda>k. triangle k \<le> z) z))"

   595 

   602 

   596 lemma log_zero [simp]:

   603 fun prod_decode2 where

   597   "log 0 = 0"

   604   "prod_decode2 z = BMax_rec (\<lambda>k. triangle k \<le> z) z - prod_decode1 z"

   598   by (simp add: log.simps)

   605 

   599 

   606 section {* Encodings *}

   600 lemma log_one [simp]:

   607 

   601   "log 1 = 0"

   608 lemma triangle_sum:

   602   by (simp add: log.simps)

   609   "triangle k = (\<Sum>i \<le> k. i)"

   603 

   610 by (induct k) (simp_all)

   604 lemma log_suc [simp]:

   611 

   605   "log (Suc 0) = 0"

   612 fun sqrt where

   606   by (simp add: log.simps)

   613   "sqrt z = BMax_rec (\<lambda>x. x * x \<le> z) z" 

   607 

   614 

   608 lemma log_rec:

   615 lemma sqrt_bounded_Max:

   609   "n \<ge> 2 \<Longrightarrow> log n = Suc (log (n div 2))"

   616   "Discrete.sqrt n = Max (Set.filter (\<lambda>m. m\<twosuperior> \<le> n) {0..n})"

   610   by (simp add: log.simps)

   617 proof -

   611 

   618   from power2_nat_le_imp_le [of _ n] have "{m. m \<le> n \<and> m\<twosuperior> \<le> n} = {m. m\<twosuperior> \<le> n}" by auto

   612 lemma log_twice [simp]:

   619   then show ?thesis by (simp add: Discrete.sqrt_def Set.filter_def)

   613   "n \<noteq> 0 \<Longrightarrow> log (2 * n) = Suc (log n)"

   614   by (simp add: log_rec)

   615 

   616 lemma log_half [simp]:

   617   "log (n div 2) = log n - 1"

   618 proof (cases "n < 2")

   619   case True

   620   then have "n = 0 \<or> n = 1" by arith

   621   then show ?thesis by (auto simp del: One_nat_def)

   622 next

   623   case False then show ?thesis by (simp add: log_rec)

   626 lemma log_exp [simp]:

   622 lemma sqrt: "Discrete.sqrt z = sqrt z"

   627   "log (2 ^ n) = n"

   623 apply(simp add: BMax_rec_eq3 sqrt_bounded_Max Set.filter_def power2_eq_square)

   628   by (induct n) simp_all

   624 apply(rule_tac f="Max" in arg_cong)

   629 

   625 apply(auto)

   630 fun oddfactor :: "nat \<Rightarrow> nat" where

   626 done

   631   [simp del]: "oddfactor n = (if n = 0 then 0 else if even n then oddfactor (n div 2) else n)"

   627 

   632 

   628 fun i where

   633 lemma oddfactor[simp]:

   629   "i z = (Discrete.sqrt (1 + 8 * z) - 1) div 2"

   634   "oddfactor 0 = 0"

   630 

   635   "odd n \<Longrightarrow> oddfactor n = n"

   631 lemma "map prod_decode [0,1,2,3,4,5,6,7,8,9,10,11,12] = 

   636   "even n \<Longrightarrow> oddfactor n = oddfactor (n div 2)"

   632          [(0, 0), (0, 1), (1, 0), (0, 2), (1, 1), (2, 0), (0, 3), 

   637 apply(simp_all add: oddfactor.simps)

   633           (1, 2), (2, 1), (3, 0), (0, 4), (1, 3), (2, 2)]"

   638 done

   634 apply(simp add: prod_decode_def prod_decode_aux.simps)

   639 

   635 done

   640 lemma oddfactor_odd:

   636 

   641   "oddfactor n = 0 \<or> odd (oddfactor n)" 

   637 lemma "map triangle [0, 1, 2, 3, 4, 5, 6 ] = [0, 1, 3, 6, 10, 15, 21]"

   642 apply(induct n rule: nat_less_induct)

   638 by(simp add: numeral_eq_Suc One_nat_def)

   643 apply(case_tac "n = 0")

   639 

   644 apply(simp)

   640 lemma "map (\<lambda>z. (z - (i(z) * (1 + i(z))) div 2, (i(z) * (3 + i(z))) div 2 - z)) 

   645 apply(case_tac "odd n")

   641        [0,1,2,3,4,5,6,7,8,9,10,11,12] = 

   646 apply(auto)

   642        [(0, 0), (0, 1), (1, 0), (0, 2), (1, 1), (2, 0), (0, 3), 

   647 done

   643         (1, 2), (2, 1), (3, 0), (0, 4), (1, 3), (2, 2)]"

   648 

   644 apply(simp add: sqrt) 

   649 lemma bigger: "oddfactor (Suc n) > 0"

   645 by eval

   650 apply(induct n rule: nat_less_induct)

   646 

   651 apply(case_tac "n = 0")

   647 fun

   652 apply(simp)

   648   prod_decode_max :: "nat \<Rightarrow> nat \<Rightarrow> nat"

   653 apply(case_tac "odd n")

   649 where

   654 apply(auto)

   650   "prod_decode_max k m =

   655 apply(drule_tac x="n div 2" in spec)

   651      (if m \<le> k then k else prod_decode_max (Suc k) (m - Suc k))"

   656 apply(drule mp)

   652 

   657 apply(auto)

   653 lemma t: "triangle (prod_decode_max k m) \<le> triangle k + m"

   658 by (smt numeral_2_eq_2 odd_nat_plus_one_div_two)

   654 apply (induct k m rule: prod_decode_max.induct)

   659 

   655 apply (subst prod_decode_max.simps)

   660 fun pencode :: "nat \<Rightarrow> nat \<Rightarrow> nat" where

   656 apply (simp)

   661   "pencode m n = (2 ^ m) * ((2 * n) + 1) - 1"

   657 done

   662 

   658 

   663 fun pdecode2 :: "nat \<Rightarrow> nat" where

   659 lemma "prod_decode_max 0 z = (GREAT k. triangle k \<le> z)"

   664   "pdecode2 z = (oddfactor (Suc z) - 1) div 2"

   660 apply(rule sym)

   665 

   661 apply(rule Great_equality)

   666 fun pdecode1 :: "nat \<Rightarrow> nat" where

   662 using t

   667   "pdecode1 z = log ((Suc z) div (oddfactor (Suc z)))"

   663 apply -[1]

   668 

   664 apply (smt triangle_0)

   669 lemma k:

   665 apply(induct z arbitrary: y rule: nat_less_induct)

   670   "odd n \<Longrightarrow> oddfactor (2 ^ m * n) = n"

   666 apply (subst prod_decode_max.simps)

   671 apply(induct m)

   667 apply (auto simp del: prod_decode_max.simps)

   672 apply(simp_all)

   668 apply(case_tac y)

   673 done

   669 apply(simp)

   674 

   670 apply(simp)

   675 lemma ww: "\<exists>k. n = 2 ^ k * oddfactor n"

   671 

   676 apply(induct n rule: nat_less_induct)

   672 apply (subst prod_decode_max.simps)

   677 apply(case_tac "n=0")

   673 apply (auto simp del: prod_decode_max.simps)

   678 apply(simp)

   674 

   679 apply(case_tac "odd n")

   675 

   680 apply(simp)

   676 

   681 apply(rule_tac x="0" in exI)

   677 apply(blast)

   682 apply(simp)

   678 

   683 apply(simp)

   679 lemma "prod_decode z = (z - (i(z) * (1 + i(z))) div 2, (i(z) * (3 + i(z))) div 2 - z)"

   684 apply(drule_tac x="n div 2" in spec)

   680 apply(simp add: prod_decode_def)

   685 apply(erule impE)

   681 apply(case_tac z)

   686 apply(simp)

   682 apply(simp add: prod_decode_aux.simps)

   687 apply(erule exE)

   683 apply(simp)

   688 apply(rule_tac x="Suc k" in exI)

   689 apply(simp)

   690 by (metis div_mult_self2_is_id even_mult_two_ex nat_mult_assoc nat_mult_commute zero_neq_numeral)

   691 

   692 

   693 

   694 lemma t:

   695   "(Suc (Suc m)) div 2 = Suc (m div 2)"

   696 by (induct m) (auto)

   697 

   698 lemma u:

   699   "((Suc (Suc m)) mod 2 = 0) <-> m mod 2 = 0"

   700 by (auto)

   701 

   702 lemma u2: 

   703   "0 < n ==> 2 * 2 ^ (n - 1) = (2::nat) ^ (n::nat)"

   704 by (induct n) (simp_all)

   705 

   706 lemma test: "x = y \<Longrightarrow> 2 * x = 2 * y"

   707 by simp

   708 

   709 lemma m: "0 < n ==> 2 ^ log (n div (oddfactor n)) = n div (oddfactor n)"

   710 apply(induct n rule: nat_less_induct)

   711 apply(case_tac "n=0")

   712 apply(simp)

   713 apply(case_tac "odd n")

   714 apply(simp)

   715 apply(drule_tac x="n div 2" in spec)

   716 apply(drule mp)

   717 apply(auto)[1]

   718 apply(drule mp)

   719 apply (metis One_nat_def Suc_lessI div_2_gt_zero odd_1_nat)

   720 apply(subst (asm) oddfactor(3)[symmetric])

   721 apply(simp)

   722 apply(subst (asm) oddfactor(3)[symmetric])

   723 apply(simp)

   724 apply(subgoal_tac "n div 2 div oddfactor n = n div (oddfactor n) div 2")

   725 prefer 2

   726 apply (metis div_mult2_eq nat_mult_commute)

   727 apply(simp only: log_half)

   728 apply(case_tac "n div oddfactor n = 0")

   729 apply(simp)

   730 apply(simp del: oddfactor)

   731 apply(drule test)

   732 apply(subst (asm) power.simps(2)[symmetric])

   733 apply(subgoal_tac "Suc (log (n div oddfactor n) - 1) = log (n div oddfactor n)")

   734 prefer 2

   735 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))

   736 apply(simp only:)

   737 apply(subst dvd_mult_div_cancel)

   738 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)

   739 apply(simp (no_asm))

   740 done

   741 

   742 lemma m1: "n div oddfactor n * oddfactor n = n"

   743 apply(induct n rule: nat_less_induct)

   744 apply(case_tac "n=0")

   745 apply(simp)

   746 apply(case_tac "odd n")

   747 apply(simp)

   748 apply(simp)

   749 apply(drule_tac x="n div 2" in spec)

   750 apply(drule mp)

   751 apply(auto)[1]

   752 by (metis add_eq_if diff_add_inverse oddfactor(3) mod_eq_0_iff mult_div_cancel nat_mult_commute ww)

   753 

   754 

   755 lemma m2: "0 < n ==> 2 ^ log (n div (oddfactor n)) * (oddfactor n) = n"

   756 apply(subst m)

   757 apply(simp)

   758 apply(subst m1)

   759 apply(simp)

   760 done

   761 

   762 lemma y1:

   763   "pdecode2 (pencode m n) = n"

   764 apply(simp)

   765 apply(subst k)

   766 apply(auto)

   767 done

   768 

   769 lemma y2:

   770   "pdecode1 (pencode m n) = m"

   771 using [[simp_trace]]

   772 apply(simp)

   773 apply(subst k)

   774 apply(auto)[1]

   775 using [[simp_trace_depth_limit=10]]

   776 apply(simp)

   777 done

   778 

   779 lemma yy: 

   780   "pencode (pdecode1 m) (pdecode2 m) = m"

   781 apply(induct m rule: nat_less_induct)

   782 apply(simp (no_asm))

   783 apply(case_tac "n = 0")

   784 apply(simp)

   785 apply(subst dvd_mult_div_cancel)

   786 using oddfactor_odd

   787 apply -

   788 apply(drule_tac x="Suc n" in meta_spec)

   789 apply(erule disjE)

   790 apply(auto)[1]

   791 apply (metis even_num_iff nat_even_iff_2_dvd odd_pos)

   792 using bigger

   793 apply -

   794 apply(rotate_tac 3)

   795 apply(drule_tac x="n" in meta_spec)

   796 apply(simp del: pencode.simps pdecode2.simps pdecode1.simps)

   797 apply(subst m2)

   798 apply(simp)

   799 apply(simp)

   800 done

   801 

   802 fun penc where

   803  "penc (m, n) = pencode m n"

   804 

   805 fun pdec where

   806  "pdec m = (pdecode1 m, pdecode2 m)"

   807 

   808 lemma q1: "penc (pdec m) = m"

   809 apply(simp only: penc.simps pdec.simps)

   810 apply(rule yy)

   811 done

   812 

   813 lemma q2: "pdec (penc m) = m"

   814 apply(simp only: penc.simps pdec.simps)

   815 apply(case_tac m)

   816 apply(simp only: penc.simps pdec.simps)

   817 apply(subst y1)

   818 apply(subst y2)

   819 apply(simp)

   820 done

   821 

   822 lemma inj_penc: "inj_on penc A"

   823 apply(rule inj_on_inverseI)

   824 apply(rule q2)

   825 done

   826 

   827 lemma inj_pdec: "inj_on pdec A"

   828 apply(rule inj_on_inverseI)

   829 apply(rule q1)

   830 done

   831 

   832 lemma surj_penc: "surj penc"

   833 apply(rule surjI)

   834 apply(rule q1)

   835 done

   836 

   837 lemma surj_pdec: "surj pdec"

   838 apply(rule surjI)

   839 apply(rule q2)

   840 done

   841 

   842 lemma 

   843   "bij pdec"

   844 by(simp add: bij_def surj_pdec inj_pdec)

   845 

   846 lemma 

   847   "bij penc"

   848 by(simp add: bij_def surj_penc inj_penc)

   849 

   850 lemma "a \<le> penc (a, 0)"

   851 apply(induct a)

   852 apply(simp)

   853 apply(simp)

   854 by (smt nat_one_le_power)

   855 

   856 lemma "penc(a, 0) \<le> penc (a, b)"

   857 apply(simp)

   858 by (metis diff_le_mono le_add1 mult_2_right mult_le_mono1 nat_add_commute nat_mult_1 nat_mult_commute)

   859 

   860 lemma "b \<le> penc (a, b)"

   861 apply(simp)

   862 proof -

   863   have f1: "(1\<Colon>nat) + 1 = 2"

   864     by (metis mult_2 nat_mult_1_right)

   865   have f2: "\<And>x\<^isub>1 x\<^isub>2. (x\<^isub>1\<Colon>nat) \<le> x\<^isub>1 * x\<^isub>2 \<or> \<not> 1 \<le> x\<^isub>2"

   866     by (metis mult_le_mono2 nat_mult_1_right)

   867   have "1 + (b + b) \<le> 1 + b \<longrightarrow> b \<le> (1 + (b + b)) * (1 + 1) ^ a - 1"

   868     by (metis le_add1 le_trans nat_add_left_cancel_le)

   869   hence "(1 + (b + b)) * (1 + 1) ^ a \<le> 1 + b \<longrightarrow> b \<le> (1 + (b + b)) * (1 + 1) ^ a - 1"

   870     using f2 by (metis le_add1 le_trans one_le_power)

   871   hence "b \<le> 2 ^ a * (b + b + 1) - 1"

   872     using f1 by (metis le_diff_conv nat_add_commute nat_le_linear nat_mult_commute)

   873   thus "b \<le> 2 ^ a * (2 * b + 1) - 1"

   874     by (metis mult_2)

   875 qed