Quelle  Wordarith.thy

(*  Title:      RSAPSS/Wordarith.thy
    Author:     Christina Lindenberg, Kai Wirt, Technische Universität Darmstadt
    Copyright:  2005 - Technische Universität Darmstadt
*)


section "Extensions to the Word theory required for PSS"

theory Wordarith
imports WordOperations "HOL-Computational_Algebra.Primes"
begin

definition
  nat_to_bv_length :: "nat ==> nat ==> bv" where
    (* nat_to_bv_length converts nat (if 0 \<le> nat \<and> nat < 2^nat) nato a bit string of length l *)
  nat_to_bv_length:
  "nat_to_bv_length n l = (if length(nat_to_bv n) ≤ l then bv_extend l 0 (nat_to_bv n) else [])"


lemma length_nat_to_bv_length:
  "nat_to_bv_length x y ≠ [] ==> length (nat_to_bv_length x y) = y"
  unfolding nat_to_bv_length by auto

lemma bv_to_nat_nat_to_bv_length:
  "nat_to_bv_length x y ≠ [] ==> bv_to_nat (nat_to_bv_length x y) = x"
  unfolding nat_to_bv_length by auto


definition
  roundup :: "nat ==> nat ==> nat" where
  roundup: "roundup x y = (if (x mod y = 0) then (x div y) else (x div y) + 1)"


lemma rnddvd: "b dvd a ==> roundup a b * b = a"
  by (auto simp add: roundup dvd_eq_mod_eq_0)

lemma bv_to_nat_zero_prepend: "bv_to_nat a = bv_to_nat (0#a)"
  by auto

primrec remzero:: "bv ==> bv" where
  "remzero [] = []"
| "remzero (a#b) = (if a = 1 then (a#b) else remzero b)"

lemma remzeroeq: "bv_to_nat a = bv_to_nat (remzero a)"
proof (induct a)
  show "bv_to_nat [] = bv_to_nat (remzero [])"
    by simp
next
  case (Cons a1 a2)
  show "bv_to_nat a2 = bv_to_nat (remzero a2) ==>
       bv_to_nat (a1 # a2) = bv_to_nat (remzero (a1 # a2))"
  proof (cases a1)
    assume a: "a1=0" then have "bv_to_nat (a1#a2) = bv_to_nat a2"
      using bv_to_nat_zero_prepend by simp
    moreover have "remzero (a1 # a2) = remzero a2" using a by simp
    ultimately show ?thesis using Cons by simp
  next
    assume "a1=1" then show ?thesis by simp
  qed
qed

lemma len_nat_to_bv_pos: assumes x: "1 < a" shows "0< length (nat_to_bv a)"
proof (auto)
  assume b: "nat_to_bv a = []"
  have a: "bv_to_nat [] = 0" by simp
  have c: "bv_to_nat (nat_to_bv a) = 0" using a and b by simp
  from x have d: "bv_to_nat (nat_to_bv a) = a" by simp
  from d and c have "a=0" by simp
  then show False using x by simp
qed

lemma remzero_replicate: "remzero ((replicate n 0)@l) = remzero l"
by (induct n, auto)

lemma length_bvxor_bound: "a <= length l ==> a <= length (bvxor l l2)"
proof (induct a)
  case 0
  then show ?case by simp
next
  case (Suc a)
  have a: "Suc a ≤ length l" by fact
  with Suc.hyps have b: "a ≤ length (bvxor l l2)" by simp
  show "Suc a ≤ length (bvxor l l2)"
  proof cases
    assume c: "a = length (bvxor l l2)"
    show "Suc a ≤ length (bvxor l l2)"
    proof (simp add: bvxor)
      have "length l <= max (length l) (length l2)" by simp
      then show "Suc a ≤ max (length l) (length l2)" using a by simp
    qed
  next
    assume "a ≠ length (bvxor l l2)"
    then have "a < length (bvxor l l2)" using b by simp
    then show ?thesis by simp
  qed
qed

lemma nat_to_bv_helper_legacy_induct:
  "(∧n. n ≠ (0::nat) ⟶ P (n div 2) ==> P n) ==> P x"
unfolding atomize_imp[symmetric]
by (induction_schema, simp, lexicographic_order)

lemma len_lower_bound:
  assumes "0 < n"
  shows "2^(length (nat_to_bv n) - Suc 0) ≤ n"
proof (cases "1<n")
  assume l1: "1<n"
  then show ?thesis
  proof (simp add: nat_to_bv_def, induct n rule: nat_to_bv_helper_legacy_induct, auto)
    fix n
    assume a: "Suc 0 < (n::nat)" and b: "~Suc 0<n div 2"
    then have "n=2 ∨ n=3"
    proof (cases "n<=3")
      assume "n<=3" and "Suc 0<n"
      then show "n=2 ∨ n=3" by auto
    next
      assume "~n<=3" then have "3<n" by simp
      then have "1 < n div 2" by arith
      then show "n=2 ∨ n=3" using b by simp
    qed
    then show "2 ^ (length (nat_to_bv_helper n []) - Suc 0) ≤ n"
    proof (cases "n=2")
      assume a: "n=2" then have "nat_to_bv_helper n [] = [1, 0]"
      proof -
        have "nat_to_bv_helper n [] = nat_to_bv n" using b by (simp add: nat_to_bv_def)
        then show ?thesis using a by (simp add: nat_to_bv_non0)
      qed
      then show "2 ^ (length (nat_to_bv_helper n []) - Suc 0) ≤ n" using a by simp
    next
      assume "n=2 ∨ n=3" and "n~=2"
      then have a: "n=3" by simp
      then have "nat_to_bv_helper n [] = [1, 1]"
      proof -
        have "nat_to_bv_helper n [] = nat_to_bv n" using a by (simp add: nat_to_bv_def)
        then show ?thesis using a by (simp add: nat_to_bv_non0)
      qed
      then show "2^(length (nat_to_bv_helper n []) - Suc 0) <=n" using a by simp
    qed
  next
    fix n
    assume a: "Suc 0<n" and
      b: "2 ^ (length (nat_to_bv_helper (n div 2) []) - Suc 0) ≤ n div 2"
    have "(2::nat) ^ (length (nat_to_bv_helper n []) - Suc 0) =
      2^(length (nat_to_bv_helper (n div 2) []) + 1 - Suc 0)"
    proof -
      have "length (nat_to_bv n) = length (nat_to_bv (n div 2)) + 1"
        using a by (simp add: nat_to_bv_non0)
      then show ?thesis by (simp add: nat_to_bv_def)
    qed
    moreover have "(2::nat)^(length (nat_to_bv_helper (n div 2) []) + 1 - Suc 0) =
      2^(length (nat_to_bv_helper (n div 2) []) - Suc 0) * 2"
    proof auto
      have "(2::nat)^(length (nat_to_bv_helper (n div 2) []) -Suc 0)*2 =
        2^(length (nat_to_bv_helper (n div 2) []) - Suc 0 + 1)" by simp
      moreover have "(2::nat)^(length (nat_to_bv_helper (n div 2) []) - Suc 0 + 1) =
        2^(length (nat_to_bv_helper (n div 2) []))"
      proof -
        have "0<n div 2" using a by arith
        then have "0<length (nat_to_bv (n div 2))" by (simp add: nat_to_bv_non0)
        then have "0< length (nat_to_bv_helper (n div 2) [])" using a by (simp add: nat_to_bv_def)
        then show ?thesis by simp
      qed
      ultimately show "(2::nat) ^ length (nat_to_bv_helper (n div 2) []) =
        2 ^ (length (nat_to_bv_helper (n div 2) []) - Suc 0) * 2" by simp
    qed
    ultimately show  "2 ^ (length (nat_to_bv_helper n []) - Suc 0) <= n"
      using b by (simp add: nat_to_bv_def) arith
  qed
next
  assume c: "~1<n"
  show ?thesis
  proof (cases "n=1")
    assume a: "n=1" then have "nat_to_bv n = [1]" by (simp add: nat_to_bv_non0)
    then show "2^(length (nat_to_bv n) - Suc 0) <= n" using a by simp
  next
    assume "n~=1"
    with ‹0 < n› show "2^(length (nat_to_bv n) - Suc 0) <= n" using c by simp
  qed
qed

lemma length_lower: assumes a: "length a < length b" and b: "(hd b) ~= 0" shows "bv_to_nat a < bv_to_nat b"
proof -
  have ha: "bv_to_nat a < 2^length a" by (simp add: bv_to_nat_upper_range)
  have "b ~= []" using a by auto
  then have "b=(hd b)#(tl b)" by simp
  then have "bv_to_nat b = bitval (hd b) * 2^(length (tl b)) + bv_to_nat (tl b)" using bv_to_nat_helper[of "hd b" "tl b"] by simp
  moreover have "bitval (hd b) = 1"
  proof (cases "hd b")
    assume "hd b = 0 "
    then show  "bitval (hd b) = 1" using b by simp
  next
    assume "hd b = 1"
    then show "bitval (hd b) = 1" by simp
  qed
  ultimately have hb: "2^length (tl b) <= bv_to_nat b" by simp
  have "2^(length a) <= (2::nat)^length (tl b)" using a by auto
  then show ?thesis using hb and ha by arith
qed

lemma nat_to_bv_non_empty: assumes a: "0<n" shows "nat_to_bv n ~= []"
proof -
  from nat_to_bv_non0[of n] have "∃x. nat_to_bv n = x@[if n mod 2 = 0 then 0 else 1]" using a by simp
  then show ?thesis by auto
qed

lemma hd_append: "x ~= [] ==> hd (x @ xs) = hd x"
  by (induct x) auto

lemma hd_one: "0<n ==> hd (nat_to_bv_helper n []) = 1"
proof (induct n rule: nat_to_bv_helper_legacy_induct)
  fix n
  assume *: "n ≠ 0 ⟶ 0 < n div 2 ⟶ hd (nat_to_bv_helper (n div 2) []) = 1"
    and "0 < n"
  show "hd (nat_to_bv_helper n []) = 1"
  proof (cases "1<n")
    assume a: "1<n"
    with * have b: "0 < n div 2 ⟶ hd (nat_to_bv_helper (n div 2) []) = 1" by simp
    from a have c: "0<n div 2" by arith
    then have d: "hd (nat_to_bv_helper (n div 2) []) = 1" using b by simp
    also from a have "0<n" by simp
    then have "hd (nat_to_bv_helper n []) =
        hd (nat_to_bv (n div 2) @ [if n mod 2 = 0 then 0 else 1])"
      using nat_to_bv_def and nat_to_bv_non0[of n] by auto
    then have "hd (nat_to_bv_helper n []) =
        hd (nat_to_bv (n div 2))"
      using nat_to_bv_non0[of "n div 2"] and c and
        nat_to_bv_non_empty[of "n div 2"] and hd_append[of " nat_to_bv (n div 2)"] by auto
    then have "hd (nat_to_bv_helper n []) = hd (nat_to_bv_helper (n div 2) [])"
      using nat_to_bv_def by simp
    then show "hd (nat_to_bv_helper n []) = 1" using b and c by simp
  next
    assume "~1 < n" with ‹0<n\› have c: "n=1" by simp
    have "nat_to_bv_helper 1 [] = [1]" by (simp add: nat_to_bv_helper.simps)
    then show "hd (nat_to_bv_helper n []) = 1" using c by simp
  qed
qed

lemma prime_hd_non_zero: 
  fixes p::nat assumes a: "prime p" and b: "prime q" shows "hd (nat_to_bv (p*q)) ~= 0"
proof -
  have "0 < p*q"
    by (metis a b mult_is_0 neq0_conv not_prime_0) 
  then show ?thesis using hd_one[of "p*q"] and nat_to_bv_def by auto
qed

lemma primerew: fixes p::nat shows  "[m dvd p; m~=1; m~=p] ==> ~ prime p"
  by (auto simp add: prime_nat_iff)


lemma two_dvd_exp: "0<x ==> (2::nat) dvd 2^x"
  by (induct x) auto

lemma exp_prod1: "[1<b;2^x=2*(b::nat)] ==> 2 dvd b"
proof -
  assume a: "1<b" and b: "2^x=2*(b::nat)"
  have s1: "1<x"
  proof (cases "1<x")
    assume "1<x" then show ?thesis by simp
  next
   assume x: "~1 < x" then have "2^x <= (2::nat)" using b
   proof (cases "x=0")
      assume "x=0" then show "2^x <= (2::nat)" by simp
    next
      assume "x~=0" then have "x=1" using x by simp
      then show "2^x <= (2::nat)" by simp
    qed
    then have "b<=1" using b by simp
    then show ?thesis using a by simp
  qed
  have s2: "2^(x-(1::nat)) = b"
  proof -
    from s1 b have "2^((x-Suc 0)+1) = 2*b" by simp
    then have "2*2^(x-Suc 0) = 2*b" by simp
    then show "2^(x-(1::nat)) = b" by simp
  qed
  from s1 and s2 show ?thesis using two_dvd_exp[of "x-(1::nat)"] by simp
qed

lemma exp_prod2: "[1<a; 2^x=a*2] ==> (2::nat) dvd a"
proof -
  assume "2^x=a*2"
  then have "2^x=2*a" by simp
  moreover assume "1<a"
  ultimately show "2 dvd a" using exp_prod1 by simp
qed

lemma odd_mul_odd: "[~(2::nat) dvd p; ~2 dvd q] ==> ~2 dvd p*q"
  by simp

lemma prime_equal: fixes p::nat shows "[prime p; prime q; 2^x=p*q] ==> (p=q)"
proof -
  assume a: "prime p" and b: "prime q" and c: "2^x=p*q"
  from a have d: "1 < p" by (simp add: prime_nat_iff)
  moreover from b have e: "1<q" by (simp add: prime_nat_iff)
  show "p=q"
  proof (cases "p=2")
    assume p: "p=2" then have "2 dvd q" using c and exp_prod1[of q x] and e by simp
    then have "2=q" using primerew[of 2 q] and b by auto
    then show ?thesis using p by simp
  next
    assume p: "p~=2" show "p=q"
    proof (cases "q=2")
      assume q: "q=2" then have "2 dvd p" using c and exp_prod1[of p x] and d by simp
      then have "2=p" using primerew[of 2 p] and a by auto
      then show ?thesis using p by simp
    next
      assume q: "q~=2" show "p=q"
      proof -
        from p have "~ 2 dvd p" using primerew and a by auto
        moreover from q have "~2 dvd q" using primerew and b by auto
        ultimately have "~2 dvd p*q" by (simp add: odd_mul_odd)
        then have "odd ((2 :: nat) ^ x)" by (simp only: c) simp
        moreover have "(2::nat) dvd 2^x"
        proof (cases "x=0")
          assume "x=0" then have "(2::nat)^x=1" by simp
          then show ?thesis using c and d and e by simp
        next
          assume "x~=0" then have "0<x" by simp
          then show ?thesis using two_dvd_exp by simp
        qed
        ultimately show ?thesis by simp
      qed
    qed
  qed
qed

lemma nat_to_bv_length_bv_to_nat:
  "length xs = n ==> xs ≠ [] ==> nat_to_bv_length (bv_to_nat xs) n = xs"
  apply (simp only: nat_to_bv_length)
  apply (auto)
  apply (simp add: bv_extend_norm_unsigned)
  done

end