Theory Sigma_Commit_Crypto.Xor

theory Xor imports 
  "HOL-Algebra.Complete_Lattice" 
  "CryptHOL.Misc_CryptHOL" 
begin

unbundle no lattice_syntax

context bounded_lattice begin

lemma top_join [simp]: "x ∈ carrier L ⟹ ⊤ ⊔ x = ⊤"
  using eq_is_equal top_join by auto

lemma join_top [simp]: "x ∈ carrier L ⟹ x ⊔ ⊤ = ⊤"
  using le_iff_meet by blast

lemma bot_join [simp]: "x ∈ carrier L ⟹ ⊥ ⊔ x = x"
  using le_iff_meet by blast

lemma join_bot [simp]: "x ∈ carrier L ⟹ x ⊔ ⊥ = x"
  by (metis bot_join join_comm)

lemma bot_meet [simp]: "x ∈ carrier L ⟹ ⊥ ⊓ x = ⊥"
  using bottom_meet by auto

lemma meet_bot [simp]: "x ∈ carrier L ⟹ x ⊓ ⊥ = ⊥"
  by (metis bot_meet meet_comm)

lemma top_meet [simp]: "x ∈ carrier L ⟹ ⊤ ⊓ x = x"
  by (metis le_iff_join meet_comm top_closed top_higher)

lemma meet_top [simp]: "x ∈ carrier L ⟹ x ⊓ ⊤ = x"
  by (metis meet_comm top_meet)

lemma join_idem [simp]: "x ∈ carrier L ⟹ x ⊔ x = x"
  using le_iff_meet by blast

lemma meet_idem [simp]: "x ∈ carrier L ⟹ x ⊓ x = x"
  using le_iff_join le_refl by presburger

lemma meet_leftcomm: "x ⊓ (y ⊓ z) = y ⊓ (x ⊓ z)" if "x ∈ carrier L" "y ∈ carrier L" "z ∈ carrier L"
  by (metis meet_assoc meet_comm that)

lemma join_leftcomm: "x ⊔ (y ⊔ z) = y ⊔ (x ⊔ z)" if "x ∈ carrier L" "y ∈ carrier L" "z ∈ carrier L"
  by (metis join_assoc join_comm that)

lemmas meet_ac = meet_assoc meet_comm meet_leftcomm
lemmas join_ac = join_assoc join_comm join_leftcomm

end

record 'a boolean_algebra = "'a gorder" +
  compl :: "'a ⇒ 'a" (‹❙-ı› 1000)

definition xor :: "('a, 'b) boolean_algebra_scheme ⇒ 'a ⇒ 'a ⇒ 'a" (infixr ‹⊕ı› 100) where
  "x ⊕ y = (x ⊔ y) ⊓ (❙- (x ⊓ y))" for L (structure)

locale boolean_algebra = bounded_lattice L
  for L (structure) +
  assumes compl_closed [intro, simp]: "x ∈ carrier L ⟹ ❙- x ∈ carrier L"
    and meet_compl_bot [simp]: "x ∈ carrier L ⟹ ❙- x ⊓ x = ⊥"
    and join_compl_top [simp]: "x ∈ carrier L ⟹ ❙- x ⊔ x = ⊤"
    and join_meet_distrib1: "⟦ x ∈ carrier L; y ∈ carrier L; z ∈ carrier L ⟧ ⟹ x ⊔ (y ⊓ z) = (x ⊔ y) ⊓ (x ⊔ z)"
begin

lemma join_meet_distrib2: "(y ⊓ z) ⊔ x = (y ⊔ x) ⊓ (z ⊔ x)"
  if "x ∈ carrier L" "y ∈ carrier L" "z ∈ carrier L"
  by (simp add: join_comm join_meet_distrib1 that)

lemma meet_join_distrib1: "x ⊓ (y ⊔ z) = (x ⊓ y) ⊔ (x ⊓ z)"
  if [simp]: "x ∈ carrier L" "y ∈ carrier L" "z ∈ carrier L"
proof -
  have "x ⊓ (y ⊔ z) = (x ⊓ (x ⊔ z)) ⊓ (y ⊔ z)"
    using join_left le_iff_join by auto
  also have "… = x ⊓ (z ⊔ (x ⊓ y))"
    by (simp add: join_comm join_meet_distrib1 meet_assoc)
  also have "… = ((x ⊓ y) ⊔ x) ⊓ ((x ⊓ y) ⊔ z)"
    by (metis join_comm le_iff_meet meet_closed meet_left that(1) that(2))
  also have "… = (x ⊓ y) ⊔ (x ⊓ z)"
    by (simp add: join_meet_distrib1)
  finally show ?thesis .
qed

lemma meet_join_distrib2: "(y ⊔ z) ⊓ x = (y ⊓ x) ⊔ (z ⊓ x)"
  if [simp]: "x ∈ carrier L" "y ∈ carrier L" "z ∈ carrier L"
  by (simp add: meet_comm meet_join_distrib1)

lemmas join_meet_distrib = join_meet_distrib1 join_meet_distrib2

lemmas meet_join_distrib = meet_join_distrib1 meet_join_distrib2

lemmas distrib = join_meet_distrib meet_join_distrib

lemma meet_compl2_bot [simp]: "x ∈ carrier L ⟹ x ⊓ ❙- x = ⊥"
  by (metis meet_comm meet_compl_bot)

lemma join_compl2_top [simp]: "x ∈ carrier L ⟹ x ⊔ ❙- x = ⊤"
  by (metis join_comm join_compl_top)

lemma compl_unique:
  assumes "x ⊓ y = ⊥"
    and "x ⊔ y = ⊤"
    and [simp]: "x ∈ carrier L" "y ∈ carrier L"
  shows "❙- x = y"
proof -
  have "(x ⊓ ❙- x) ⊔ (❙- x ⊓ y) = (x ⊓ y) ⊔ (❙- x ⊓ y)"
    using inf_compl_bot assms(1) by simp
  then have "(❙- x ⊓ x) ⊔ (❙- x ⊓ y) = (y ⊓ x) ⊔ (y ⊓ ❙- x)"
    by (simp add: meet_comm)
  then have "❙- x ⊓ (x ⊔ y) = y ⊓ (x ⊔ ❙- x)"
    using assms(3) assms(4) compl_closed meet_join_distrib1 by presburger
  then have "❙- x ⊓ ⊤ = y ⊓ ⊤"
    by (simp add: assms(2))
  then show "❙- x = y"
    using le_iff_join top_higher by auto
qed

lemma double_compl [simp]: "❙- (❙- x) = x" if [simp]: "x ∈ carrier L"
  by(rule compl_unique)(simp_all)

lemma compl_eq_compl_iff [simp]: "❙- x = ❙- y ⟷ x = y" if "x ∈ carrier L" "y ∈ carrier L"
  by (metis double_compl that that)

lemma compl_bot_eq [simp]: "❙- ⊥ = ⊤"
  using le_iff_join le_iff_meet local.compl_unique top_higher by auto

lemma compl_top_eq [simp]: "❙- ⊤ = ⊥"
  by (metis bottom_closed compl_bot_eq double_compl)

lemma compl_inf [simp]: "❙- (x ⊓ y) = ❙- x ⊔ ❙- y" if [simp]: "x ∈ carrier L" "y ∈ carrier L"
proof (rule compl_unique)
  have "(x ⊓ y) ⊓ (❙- x ⊔ ❙- y) = (y ⊓ (x ⊓ ❙- x)) ⊔ (x ⊓ (y ⊓ ❙- y))"
    by (smt compl_closed meet_assoc meet_closed meet_comm meet_join_distrib1 that)
  then show "(x ⊓ y) ⊓ (❙- x ⊔ ❙- y) = ⊥"
    by (metis bottom_closed bottom_lower le_iff_join le_iff_meet meet_comm meet_compl2_bot that)
next
  have "(x ⊓ y) ⊔ (❙- x ⊔ ❙- y) = (❙- y ⊔ (x ⊔ ❙- x)) ⊓ (❙- x ⊔ (y ⊔ ❙- y))"
    by (smt compl_closed join_meet_distrib2 join_assoc join_comm local.boolean_algebra_axioms that join_closed)
  then show "(x ⊓ y) ⊔ (❙- x ⊔ ❙- y) = ⊤"
    by (metis compl_closed join_compl2_top join_right le_iff_join le_iff_meet that top_closed)
qed simp_all

lemma compl_sup [simp]: "❙- (x ⊔ y) = ❙- x ⊓ ❙- y" if "x ∈ carrier L" "y ∈ carrier L"
  by (metis compl_closed compl_inf double_compl meet_closed that)

lemma compl_mono:
  assumes "x ⊑ y"
    and "x ∈ carrier L" "y ∈ carrier L"
  shows "❙- y ⊑ ❙- x"
  by (metis assms(1) assms(2) assms(3) compl_closed join_comm le_iff_join le_iff_meet compl_inf)

lemma compl_le_compl_iff [simp]: "❙- x ⊑ ❙- y ⟷ y ⊑ x" if "x ∈ carrier L" "y ∈ carrier L"
  using that by (auto dest: compl_mono)

lemma compl_le_swap1:
  assumes "y ⊑ ❙- x" "x ∈ carrier L" "y ∈ carrier L"
  shows "x ⊑ ❙- y"
  by (metis assms compl_closed compl_le_compl_iff double_compl)

lemma compl_le_swap2:
  assumes "❙- y ⊑ x" "x ∈ carrier L" "y ∈ carrier L"
  shows "❙- x ⊑ y"
  by (metis assms compl_closed compl_le_compl_iff double_compl)

lemma join_compl_top_left1 [simp]: "❙- x ⊔ (x ⊔ y) = ⊤" if [simp]: "x ∈ carrier L" "y ∈ carrier L"
  by (simp add: join_assoc[symmetric])

lemma join_compl_top_left2 [simp]: "x ⊔ (❙- x ⊔ y) = ⊤" if [simp]: "x ∈ carrier L" "y ∈ carrier L"
  using join_compl_top_left1[of "❙- x" y] by simp

lemma meet_compl_bot_left1 [simp]: "❙- x ⊓ (x ⊓ y) = ⊥" if [simp]: "x ∈ carrier L" "y ∈ carrier L"
  by (simp add: meet_assoc[symmetric])

lemma meet_compl_bot_left2 [simp]: "x ⊓ (❙- x ⊓ y) = ⊥" if [simp]: "x ∈ carrier L" "y ∈ carrier L"
  using meet_compl_bot_left1[of "❙- x" y] by simp

lemma meet_compl_bot_right [simp]: "x ⊓ (y ⊓ ❙- x) = ⊥" if [simp]: "x ∈ carrier L" "y ∈ carrier L"
  by (metis meet_compl_bot_left2 meet_comm that)

lemma xor_closed [intro, simp]: "⟦ x ∈ carrier L; y ∈ carrier L ⟧ ⟹ x ⊕ y ∈ carrier L"
  by(simp add: xor_def)

lemma xor_comm: "⟦ x ∈ carrier L; y ∈ carrier L ⟧ ⟹ x ⊕ y = y ⊕ x"
  by(simp add: xor_def meet_join_distrib join_comm)

lemma xor_assoc: "(x ⊕ y) ⊕ z = x ⊕ (y ⊕ z)"
  if [simp]: "x ∈ carrier L" "y ∈ carrier L" "z ∈ carrier L"
  by(simp add: xor_def)(simp add: meet_join_distrib meet_ac join_ac)

lemma xor_left_comm: "x ⊕ (y ⊕ z) = y ⊕ (x ⊕ z)" if "x ∈ carrier L" "y ∈ carrier L" "z ∈ carrier L"
  using that xor_assoc xor_comm by auto

lemma [simp]:
  assumes "x ∈ carrier L"
  shows xor_bot: "x ⊕ ⊥ = x"
  and bot_xor: "⊥ ⊕ x = x"
  and xor_top: "x ⊕ ⊤ = ❙- x"
  and top_xor: "⊤ ⊕ x = ❙- x"
  by(simp_all add: xor_def assms)

lemma xor_inverse [simp]: "x ⊕ x = ⊥" if "x ∈ carrier L"
  by(simp add: xor_def that)

lemma xor_left_inverse [simp]: "x ⊕ x ⊕ y = y" if "x ∈ carrier L" "y ∈ carrier L"
  using that xor_assoc by fastforce

lemmas xor_ac = xor_assoc xor_comm xor_left_comm

lemma inj_on_xor: "inj_on ((⊕) x) (carrier L)" if "x ∈ carrier L"
  by(rule inj_onI)(metis that xor_left_inverse)

lemma surj_xor: "(⊕) x ` carrier L = carrier L" if [simp]: "x ∈ carrier L"
proof(rule Set.set_eqI, rule iffI)
  fix y
  assume [simp]: "y ∈ carrier L"
  have "x ⊕ y ∈ carrier L" by(simp)
  moreover have "y = x ⊕ (x ⊕ y)" by simp
  ultimately show "y ∈ (⊕) x ` carrier L" by(rule rev_image_eqI)
qed auto

lemma one_time_pad: "map_spmf ((⊕) x) (spmf_of_set (carrier L)) = spmf_of_set (carrier L)"
  if "x ∈ carrier L"
  apply(subst map_spmf_of_set_inj_on)
   apply(rule inj_on_xor[OF that])
  by(simp add: surj_xor that)

end

end