Theory Xor

theory Xor
imports
  Main
begin

text ‹This theory abstractly defines
\begin{itemize}
\item the binary operator ‹xor› (aliases ‹(XOR)› ‹(⊕)›)
\item the n-ary version ‹xor_fold›
\item and the Big version ‹xor_sum› (alias ‹⨁i∈J. f i›).
\end{itemize}

An implementation of xor should abide by the following laws:
\begin{itemize}
\item identity element
\item commutative
\item associative
\item left/right neutrality
\item self-inverse
\end{itemize}

which constitutes an abelian group.

Instantiations of abel\_group\_xor have been provided for bool, nat and int.

Other theories relating to xor:
\begin{itemize}
\item @{const Boolean_Algebras.abstract_boolean_algebra_sym_diff}
\item @{const Bit_Operations.semiring_bit_operations_class.xor}
\item (AFP) \verb|Approximate_Model_Counting.RandomXOR| \cite{Approximate_Model_Counting-AFP}
\end{itemize}
›

section ‹Preliminaries›
subsection ‹The XOR operator›

lemma (in monoid_list) list_conv_take_drop:
  shows "F xs = F (take i xs) ❙* F (drop i xs)"
  by (metis append append_take_drop_id)

lemma (in monoid_list) list_conv_take_nth_drop:
  assumes "i < length xs"
  shows "F xs = F (take i xs) ❙* xs ! i ❙* F (drop (Suc i) xs)"
  by (metis Cons_nth_drop_Suc append append_take_drop_id assms assoc local.Cons)

lemma (in comm_monoid_list) absorb_right:
  assumes "i < length xs"
  shows "F xs ❙* v = F (xs[i := xs ! i ❙* v])"
  by (smt (verit, del_insts) append assms assoc commute list_conv_take_nth_drop local.Cons
    upd_conv_take_nth_drop)

lemma (in semiring_bit_operations) eq_iff:
  shows "semiring_bit_operations_class.xor a b = 0 ⟷ a = b"
  by (metis local.xor.assoc local.xor.left_neutral local.xor_self_eq)

subsubsection ‹Definition of XOR›

class xor =
  fixes xor :: ‹'a ⇒ 'a ⇒ 'a› (infixr ‹XOR› 59) ― ‹Definition of 2-ary xor›

class abel_group_xor = zero + xor +
  assumes xor_commute: "a XOR b = b XOR a"
  assumes xor_assoc: "(a XOR b) XOR c = a XOR b XOR c"
  assumes xor_right_neutral: "a XOR 0 = a"
  assumes eq_iff [iff]: "a XOR b = 0 ⟷ a = b"
begin

lemma self_inv [simp]:
  shows "a XOR a = 0"
  by simp

text ‹The above properties show that XOR forms an abelian group›
sublocale group xor 0 id
  using xor_commute xor_assoc by unfold_locales (simp_all add: xor_right_neutral)

sublocale abel_semigroup xor by unfold_locales (simp add: xor_commute)

sublocale comm_monoid xor 0 by unfold_locales simp

sublocale xor_sum: comm_monoid_set xor 0
  defines xor_sum = xor_sum.F ..

abbreviation "Xor_Sum ≡ xor_sum (λx. x)"

sublocale xor_list: monoid_list xor 0
  defines xor_fold = xor_list.F .. ― ‹Definition of n-ary xor›

sublocale xor_comm_list: comm_monoid_list xor 0
  rewrites "monoid_list.F xor 0 = xor_fold"
proof -
  show "comm_monoid_list xor 0" ..
  then interpret comm_monoid_list xor 0 .
  from xor_fold_def show "monoid_list.F xor 0 = xor_fold" by simp
qed

sublocale xor_list: comm_monoid_list_set xor 0
  rewrites "monoid_list.F xor 0 = xor_fold" and "comm_monoid_set.F xor 0 = xor_sum"
proof -
  show "comm_monoid_list_set xor 0" ..
  then interpret xor_sum: comm_monoid_list_set xor 0 .
  from xor_fold_def show "monoid_list.F xor 0 = xor_fold" by simp
  from xor_sum_def show "comm_monoid_set.F xor 0 = xor_sum" by (auto intro: sym)
qed

lemma xor_cong:
  assumes "a XOR b = 0"
  shows "a = b"
  using assms eq_iff by blast

lemma inj_on_UNIV:
  shows "inj_on xor UNIV"
  by (rule inj_onI) (metis right_neutral)

lemma map_indices_conv_list_update_conv:
  shows "map (λj. if j = i then g j else xs ! j) [0..<length xs] = xs[i := g i]"
  by (fastforce intro: nth_equalityI)

lemma ✐‹tag important› fold_absorb:
  assumes "i < length xs"
  shows "xor_fold xs XOR v =
    xor_fold (map (λj. if j = i then xs ! j XOR v else xs ! j) [0..<length xs])"
  unfolding map_indices_conv_list_update_conv
  using xor_comm_list.absorb_right[OF assms] .
end (*class xor*)

hide_fact xor_commute xor_assoc xor_right_neutral

subsubsection ‹Standard Instantiations›

instantiation bool :: abel_group_xor begin
definition (*tag:review*) "zero_bool ≡ False" (* since ‹of_bool False = 0› this should be okay *)
definition xor_bool :: "bool ⇒ bool ⇒ bool" where "xor_bool a b ≡ (a ≠ b)"
instance by standard (auto simp add: xor_bool_def zero_bool_def)
end (*instance bool::abel_group_xor*)

instantiation nat and int :: abel_group_xor begin
(* note: any type that implements semiring_bit_operations can be implemented this way, i.e. 'a word *)
definition xor_nat :: "nat ⇒ nat ⇒ nat" where "xor_nat ≡ semiring_bit_operations_class.xor"
definition xor_int :: "int ⇒ int ⇒ int" where "xor_int ≡ semiring_bit_operations_class.xor"
instance by standard (simp_all add: xor_nat_def xor_int_def ac_simps semiring_bit_operations_class.eq_iff)
end (*instance nat int :: abel_group_xor*)

subsubsection ‹Syntactic sugar›

open_bundle xor_syntax begin

notation xor (infixr ‹⊕› 59)
notation Xor_Sum (‹⨁›)

(* directly lifted from Groups_Big.thy *)
text ‹Now: lots of fancy syntax. First, \<^term>‹xor_sum (λx. e) A› is written ‹⨁x∈A. e›.›

syntax (ASCII)
  "_xor_sum" :: "pttrn ⇒ 'a set ⇒ 'b ⇒ 'b::abel_group_xor"  (‹(‹indent=3 notation=‹binder XORSUM››XORSUM (_/:_)./ _)› [0, 51, 10] 10)
syntax
  "_xor_sum" :: "pttrn ⇒ 'a set ⇒ 'b ⇒ 'b::abel_group_xor"  (‹(‹indent=2 notation=‹binder ⨁››⨁(_/∈_)./ _)› [0, 51, 10] 10)

syntax_consts
  "_xor_sum" ⇌ xor_sum

translations ― ‹Beware of argument permutation!›
  "⨁i∈A. b" ⇌ "CONST xor_sum (λi. b) A"
end

unbundle no xor_syntax
end (* theory *)