Theory Abstract_XOR
section ‹Abstract XOR›
theory "Abstract_XOR"
imports
"HOL.Finite_Set" "HOL-Library.FSet" "Message"
begin
subsection‹Abstract XOR definition and lemmas›
text‹We model xor as an operation on finite sets (fset). @{term "{||}"} is defined as the identity element.›
text‹xor of two fsets is the symmetric difference›
definition xor :: "'a fset ⇒ 'a fset ⇒ 'a fset" where
"xor xs ys = (xs |∪| ys) |-| (xs |∩| ys)"
lemma xor_singleton:
"xor xs {| z |} = (if z |∈| xs then xs |-| {| z |} else finsert z xs)"
"xor {| z |} xs = (if z |∈| xs then xs |-| {| z |} else finsert z xs)"
by (auto simp add: xor_def)
declare finsertCI[rule del]
declare finsertCI[intro]
lemma xor_assoc: "xor (xor xs ys) zs = xor xs (xor ys zs)"
by (auto simp add: xor_def)
lemma xor_commut: "xor xs ys = xor ys xs"
by (auto simp add: xor_def)
lemma xor_self_inv: "⟦xor xs ys = zs; xs = ys⟧ ⟹ zs = {||}"
by (auto simp add: xor_def)
lemma xor_self_inv': "xor xs xs = {||}"
by (auto simp add: xor_def)
lemma xor_self_inv''[dest!]: "xor xs ys = {||} ⟹ xs = ys"
by (auto simp add: xor_def)
lemma xor_identity1[simp]: "xor xs {||} = xs"
by (auto simp add: xor_def)
lemma xor_identity2[simp]: "xor {||} xs = xs"
by (auto simp add: xor_def)
lemma xor_in: "z |∈| xs ⟹ z |∉| (xor xs {| z |})"
by (auto simp add: xor_singleton)
lemma xor_out: "z |∉| xs ⟹ z |∈| (xor xs {| z |})"
by (auto simp add: xor_singleton)
lemma xor_elem1[dest]: "⟦x ∈ fset (xor X Y); x |∉| X⟧ ⟹ x |∈| Y"
by(auto simp add: xor_def)
lemma xor_elem2[dest]: "⟦x ∈ fset (xor X Y); x |∉| Y⟧ ⟹ x |∈| X"
by(auto simp add: xor_def)
lemma xor_finsert_self: "xor (finsert x xs) {|x|} = xs - {| x |}"
by(auto simp add: xor_def)
subsection‹Lemmas refering to XOR and msgterm›
lemma FS_contains_elem:
assumes "elem = f (FS zs_s)" "zs_s = xor zs_b {| elem |}" "⋀ x. size (f x) > size x"
shows "elem ∈ fset zs_b"
using assms(1)
apply(auto simp add: xor_def)
using FS_mono assms xor_singleton(1)
by (metis)
lemma FS_is_finsert_elem:
assumes "elem = f (FS zs_s)" "zs_s = xor zs_b {| elem |}" "⋀ x. size (f x) > size x"
shows "zs_b = finsert elem zs_s"
using assms FS_contains_elem finsert_fminus xor_singleton(1) FS_mono
by (metis FS_mono)
lemma FS_update_eq:
assumes "xs = f (FS (xor zs {|xs|}))"
and "ys = g (FS (xor zs {|ys|}))"
and "⋀ x. size (f x) > size x"
and "⋀ x. size (g x) > size x"
shows "xs = ys"
proof(rule ccontr)
assume elem_neq: "xs ≠ ys"
obtain zs_s1 zs_s2 where zs_defs:
"zs_s1 = xor zs {|xs|}" "zs_s2 = xor zs {|ys|}" by simp
have elems_contained_zs: "xs ∈ fset zs" "ys ∈ fset zs"
using assms FS_contains_elem by blast+
then have elems_elem: "ys |∈| zs_s1" "xs |∈| zs_s2"
using elem_neq by(auto simp add: xor_def zs_defs)
have zs_finsert: "finsert xs zs_s2 = zs_s2" "finsert ys zs_s1 = zs_s1"
using elems_elem by fastforce+
have f1: "∀m f fa. ¬ sum fa (fset (finsert (m::msgterm) f)) < (fa m::nat)"
by (simp add: sum.insert_remove)
from assms(1-2) have "size xs > size (f (FS {| ys |}))" "size ys > size (g (FS {| xs |}))"
apply(simp_all add: zs_defs[symmetric])
using zs_finsert f1 by (metis (no_types) add_Suc_right assms(3-4) dual_order.strict_trans
less_add_Suc1 msgterm.size(17) not_less_eq size_fset_simps)+
then show False using assms(3,4) elems_elem
by (metis add.right_neutral add_Suc_right f1 less_add_Suc1 msgterm.size(17) not_less_eq
not_less_iff_gr_or_eq order.strict_trans size_fset_simps)
qed
declare fminusE[rule del]
declare finsertCI[rule del]
declare fminusE[elim]
declare finsertCI[intro]
lemma fset_size_le:
assumes "x ∈ fset xs"
shows "size x < Suc (∑x∈fset xs. Suc (size x))"
proof-
have "size x ≤ (∑x∈fset xs. size x)" using assms
by (auto intro: member_le_sum)
moreover have "(∑x∈fset xs. size x) < (∑x∈fset xs. Suc (size x))"
by (metis assms empty_iff finite_fset lessI sum_strict_mono)
ultimately show ?thesis by auto
qed
text‹We can show that xor is a commutative function.›
locale abstract_xor
begin
sublocale comp_fun_commute xor
by(auto simp add: comp_fun_commute_def xor_def)
end
end