(* 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 ≤ nat ∧ 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 𝟬 (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 (𝟬#a)" by auto primrec remzero:: "bv ⇒ bv" where "remzero [] = []" | "remzero (a#b) = (if a = 𝟭 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=𝟬" 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=𝟭" 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 𝟬)@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 [] = [𝟭, 𝟬]" 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 [] = [𝟭, 𝟭]" 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 = [𝟭]" 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) ~= 𝟬" 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 = 𝟬 " then show "bitval (hd b) = 1" using b by simp next assume "hd b = 𝟭" 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 𝟬 else 𝟭]" 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 []) = 𝟭" 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) []) = 𝟭" and "0 < n" show "hd (nat_to_bv_helper n []) = 𝟭" proof (cases "1<n") assume a: "1<n" with * have b: "0 < n div 2 ⟶ hd (nat_to_bv_helper (n div 2) []) = 𝟭" by simp from a have c: "0<n div 2" by arith then have d: "hd (nat_to_bv_helper (n div 2) []) = 𝟭" 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 𝟬 else 𝟭])" 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 []) = 𝟭" 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 [] = [𝟭]" by (simp add: nat_to_bv_helper.simps) then show "hd (nat_to_bv_helper n []) = 𝟭" 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)) ~= 𝟬" 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