Theory List_Bits

(* Title: List_Bits.thy
  Author: Andreas Lochbihler, ETH Zurich *)

subsection ‹Exclusive or on lists›

theory List_Bits imports Misc_CryptHOL begin

definition xor :: "'a ⇒ 'a ⇒ 'a :: {uminus,inf,sup}" (infixr "⊕" 67)
where "x ⊕ y = inf (sup x y) (- (inf x y))"

lemma xor_bool_def [iff]: fixes x y :: bool shows "x ⊕ y ⟷ x ≠ y"
by(auto simp add: xor_def)

lemma xor_commute:
  fixes x y :: "'a :: {semilattice_sup,semilattice_inf,uminus}"
  shows "x ⊕ y = y ⊕ x"
by(simp add: xor_def sup.commute inf.commute)

lemma xor_assoc:
  fixes x y :: "'a :: boolean_algebra"
  shows "(x ⊕ y) ⊕ z = x ⊕ (y ⊕ z)"
by(simp add: xor_def inf_sup_aci inf_sup_distrib1 inf_sup_distrib2)

lemma xor_left_commute:
  fixes x y :: "'a :: boolean_algebra"
  shows "x ⊕ (y ⊕ z) = y ⊕ (x ⊕ z)"
by (metis xor_assoc xor_commute)

lemma [simp]:
  fixes x :: "'a :: boolean_algebra"
  shows xor_bot: "x ⊕ bot = x"
  and bot_xor: "bot ⊕ x = x"
  and xor_top: "x ⊕ top = - x"
  and top_xor: "top ⊕ x = - x"
by(simp_all add: xor_def)

lemma xor_inverse [simp]:
  fixes x :: "'a :: boolean_algebra"
  shows "x ⊕ x = bot"
by(simp add: xor_def)

lemma xor_left_inverse [simp]:
  fixes x :: "'a :: boolean_algebra"
  shows "x ⊕ x ⊕ y = y"
by(metis xor_left_commute xor_inverse xor_bot)

lemmas xor_ac = xor_assoc xor_commute xor_left_commute


definition xor_list :: "'a :: {uminus,inf,sup} list ⇒ 'a list ⇒ 'a list"  (infixr "[⊕]" 67)
where "xor_list xs ys = map (case_prod (⊕)) (zip xs ys)"

lemma xor_list_unfold:
  "xs [⊕] ys = (case xs of [] ⇒ [] | x # xs' ⇒ (case ys of [] ⇒ [] | y # ys' ⇒ x ⊕ y # xs' [⊕] ys'))"
by(simp add: xor_list_def split: list.split)

lemma xor_list_commute: fixes xs ys :: "'a :: {semilattice_sup,semilattice_inf,uminus} list"
  shows "xs [⊕] ys = ys [⊕] xs"
unfolding xor_list_def by(subst zip_commute)(auto simp add: split_def xor_commute)

lemma xor_list_assoc [simp]: 
  fixes xs ys :: "'a :: boolean_algebra list"
  shows "(xs [⊕] ys) [⊕] zs = xs [⊕] (ys [⊕] zs)"
unfolding xor_list_def zip_map1 zip_map2
apply(subst (2) zip_commute)
apply(subst zip_left_commute)
apply(subst (2) zip_commute)
apply(auto simp add: zip_map2 split_def xor_assoc)
done

lemma xor_list_left_commute:
  fixes xs ys zs :: "'a :: boolean_algebra list"
  shows "xs [⊕] (ys [⊕] zs) = ys [⊕] (xs [⊕] zs)"
by(metis xor_list_assoc xor_list_commute)

lemmas xor_list_ac = xor_list_assoc xor_list_commute xor_list_left_commute

lemma xor_list_inverse [simp]: 
  fixes xs :: "'a :: boolean_algebra list"
  shows "xs [⊕] xs = replicate (length xs) bot"
by(simp add: xor_list_def zip_same_conv_map o_def map_replicate_const)

lemma xor_replicate_bot_right [simp]:
  fixes xs :: "'a :: boolean_algebra list"
  shows "⟦ length xs ≤ n; x = bot ⟧ ⟹ xs [⊕] replicate n x = xs"
by(simp add: xor_list_def zip_replicate2 o_def)

lemma xor_replicate_bot_left [simp]:
  fixes xs :: "'a :: boolean_algebra list"
  shows "⟦ length xs ≤ n; x = bot ⟧ ⟹ replicate n x [⊕] xs = xs"
by(simp add: xor_list_commute)

lemma xor_list_left_inverse [simp]:
  fixes xs :: "'a :: boolean_algebra list"
  shows "length ys ≤ length xs ⟹ xs [⊕] (xs [⊕] ys) = ys"
by(subst xor_list_assoc[symmetric])(simp)

lemma length_xor_list [simp]: "length (xor_list xs ys) = min (length xs) (length ys)"
by(simp add: xor_list_def)

lemma inj_on_xor_list_nlists [simp]:
  fixes xs :: "'a :: boolean_algebra list"
  shows "n ≤ length xs ⟹ inj_on (xor_list xs) (nlists UNIV n)"
apply(clarsimp simp add: inj_on_def in_nlists_UNIV)
using xor_list_left_inverse by fastforce

lemma one_time_pad:
  fixes xs :: "_ :: boolean_algebra list"
  shows "length xs ≥ n ⟹ map_spmf (xor_list xs) (spmf_of_set (nlists UNIV n)) = spmf_of_set (nlists UNIV n)"
by(auto 4 3 simp add: in_nlists_UNIV intro: xor_list_left_inverse[symmetric] rev_image_eqI intro!: arg_cong[where f=spmf_of_set])

end