Theory Laws_Complement

section ‹Generic laws about complements›

theory Laws_Complement
  imports Laws Axioms_Complement
begin

unbundle register_syntax
notation comp_update (infixl "*⇩u" 55)
notation tensor_update (infixr "⊗⇩u" 70)

definition ‹complements F G ⟷ compatible F G ∧ iso_register (F;G)›

lemma complementsI: ‹compatible F G ⟹ iso_register (F;G) ⟹ complements F G›
  using complements_def by blast

lemma complement_exists: 
  fixes F :: ‹'a::domain update ⇒ 'b::domain update›
  assumes ‹register F›
  shows ‹let 'c::domain = cdc F in
          ∃G :: 'c update ⇒ 'b update. complements F G›
  by (simp add: assms complement_exists complements_def)

lemma complements_sym: ‹complements G F› if ‹complements F G›
proof (rule complementsI)
  show [simp]: ‹compatible G F›
    using compatible_sym complements_def that by blast
  from that have ‹iso_register (F;G)›
    by (meson complements_def)
  then obtain I where [simp]: ‹register I› and ‹(F;G) o I = id› and ‹I o (F;G) = id›
    using iso_register_def by blast
  have ‹register (swap o I)›
    using ‹register I› register_comp register_swap by blast
  moreover have ‹(G;F) o (swap o I) = id›
    by (simp add: ‹(F;G) ∘ I = id› rewriteL_comp_comp)
  moreover have ‹(swap o I) o (G;F) = id›
    by (metis (no_types, opaque_lifting) swap_swap ‹I ∘ (F;G) = id› calculation(2) comp_def eq_id_iff)
  ultimately show ‹iso_register (G;F)›
    using ‹compatible G F› iso_register_def pair_is_register by blast
qed

definition complement :: ‹('a::domain update ⇒ 'b::domain_with_simple_complement update) ⇒ (('a,'b) complement_domain_simple update ⇒ 'b update)› where
  ‹complement F = (SOME G :: ('a, 'b) complement_domain_simple update ⇒ 'b update. compatible F G ∧ iso_register (F;G))›

lemma register_complement[simp]: ‹register (complement F)› if ‹register F›
  using complement_exists_simple[OF that]
  by (metis (no_types, lifting) compatible_def complement_def some_eq_imp)

lemma complement_is_complement[simp]:
  assumes ‹register F›
  shows ‹complements F (complement F)›
  using complement_exists_simple[OF assms] unfolding complements_def
  by (metis (mono_tags, lifting) complement_def some_eq_imp)

lemma complement_unique:
  assumes ‹complements F G›
  assumes ‹complements F G'›
  shows ‹equivalent_registers G G'›
  apply (rule complement_unique[where F=F])
  using assms unfolding complements_def by auto

lemma complement_unique':
  assumes ‹complements F G›
  shows ‹equivalent_registers G (complement F)›
  apply (rule complement_unique[where F=F])
  using assms unfolding complements_def using compatible_register1 complement_is_complement complements_def by blast+

lemma compatible_complement[simp]: ‹register F ⟹ compatible F (complement F)›
  using complement_is_complement complements_def by blast

lemma complements_register_tensor:
  assumes [simp]: ‹register F› ‹register G›
  shows ‹complements (F ⊗⇩r G) (complement F ⊗⇩r complement G)›
proof (rule complementsI)
  have [iff]: ‹iso_register (F;complement F)›   ‹iso_register (G;complement G)›
    using complements_def by fastforce+

  have sep4: ‹separating TYPE('z::domain) {(a ⊗⇩u b) ⊗⇩u (c ⊗⇩u d) |a b c d. True}›
    apply (rule separating_tensor'[where A=‹{(a ⊗⇩u b) |a b. True}› and B=‹{(c ⊗⇩u d) |c d. True}›])
      apply (rule separating_tensor'[where A=UNIV and B=UNIV]) apply auto[3]
     apply (rule separating_tensor'[where A=UNIV and B=UNIV]) apply auto[3]
    by auto
  show compat: ‹compatible (F ⊗⇩r G) (complement F ⊗⇩r complement G)›
    by (metis assms(1) assms(2) compatible_register_tensor complement_is_complement complements_def)
  let ?reorder = ‹((Fst o Fst; Snd o Fst); (Fst o Snd; Snd o Snd))›
  have [simp]: ‹register ?reorder›
    by auto
  have [simp]: ‹?reorder ((a ⊗⇩u b) ⊗⇩u (c ⊗⇩u d)) = ((a ⊗⇩u c) ⊗⇩u (b ⊗⇩u d))› 
    for a::‹'t::domain update› and b::‹'u::domain update› and c::‹'v::domain update› and d::‹'w::domain update›
    by (simp add: register_pair_apply Fst_def Snd_def tensor_update_mult)
  have [simp]: ‹iso_register ?reorder›
    apply (rule iso_registerI[of _ ?reorder]) apply auto[2]
     apply (rule register_eqI[OF sep4]) apply auto[3]
    apply (rule register_eqI[OF sep4]) by auto
  have ‹(F ⊗⇩r G; complement F ⊗⇩r complement G) = ((F; complement F) ⊗⇩r (G; complement G)) o ?reorder›
    apply (rule register_eqI[OF sep4])
    by (auto intro!: register_preregister register_comp register_tensor_is_register pair_is_register
        simp: compat register_pair_apply tensor_update_mult)
  moreover have ‹iso_register …›
    using assms complement_is_complement complements_def 
    by (auto intro!: iso_register_comp iso_register_tensor_is_iso_register)
  ultimately show ‹iso_register (F ⊗⇩r G;complement F ⊗⇩r complement G)›
    by simp
qed

definition is_unit_register where
  ‹is_unit_register U ⟷ complements U id›

lemma register_unit_register[simp]: ‹is_unit_register U ⟹ register U›
  by (simp add: compatible_def complements_def is_unit_register_def)

lemma unit_register_compatible[simp]: ‹compatible U X› if ‹is_unit_register U› ‹register X›
  by (metis compatible_comp_right complements_def id_comp is_unit_register_def that(1) that(2))

lemma unit_register_compatible'[simp]: ‹compatible X U› if ‹is_unit_register U› ‹register X›
  using compatible_sym that(1) that(2) unit_register_compatible by blast

lemma compatible_complement_left[simp]: ‹register X ⟹ compatible (complement X) X›
  using compatible_sym complement_is_complement complements_def by blast

lemma compatible_complement_right[simp]: ‹register X ⟹ compatible X (complement X)›
  using complement_is_complement complements_def by blast

lemma unit_register_pair[simp]: ‹equivalent_registers X (U; X)› if [simp]: ‹is_unit_register U› ‹register X›
proof -
  from complement_exists[OF ‹register X›]
  have ‹let 'x::domain = cdc X in equivalent_registers X (U; X)›
  proof with_type_mp
    note [[simproc del: compatibility_warn]]
    (* assume ‹∃G :: 'x update ⇒ 'b update. complements X G› *)
    with_type_case
    then obtain compX :: ‹'x update ⇒ 'b update› where compX: ‹complements X compX›
      by blast
    then have [simp]: ‹register compX› ‹compatible X compX›
      by (auto simp add: compatible_def complements_def)
    have [iff]: ‹iso_register (X;compX)›
      using compX complements_def by blast

    have ‹equivalent_registers id (U; id)›
      using complements_def is_unit_register_def iso_register_equivalent_id that(1) by blast
    also have ‹equivalent_registers … (U; (X; compX))›
      apply (rule equivalent_registers_pair_right)
      by (auto intro!: unit_register_compatible)
    also have ‹equivalent_registers … ((U; X); compX)›
      apply (rule equivalent_registers_assoc)
      by auto
    finally have ‹complements (U; X) compX›
      by (auto simp: equivalent_registers_def complements_def)
    moreover have ‹equivalent_registers (X; compX) id›
      using compX complements_def equivalent_registers_sym iso_register_equivalent_id by blast
    ultimately show ‹equivalent_registers X (U; X)›
      by (meson complement_unique compX complements_sym)
  qed
  from this[cancel_with_type]
  show ‹equivalent_registers X (U; X)›
    by -
qed


lemma unit_register_compose_left:
  assumes [simp]: ‹is_unit_register U›
  assumes [simp]: ‹register A›
  shows ‹is_unit_register (A o U)›
proof -
  from complement_exists[OF ‹register A›]
  have ‹let 'x::domain = cdc A in is_unit_register (A o U)›
  proof with_type_mp
    note [[simproc del: compatibility_warn]]
    with_type_case 
    then obtain compA :: ‹'x update ⇒ 'c update› where compX: ‹complements A compA›
      by blast
    then have [simp]: ‹register compA› ‹compatible A compA›
      by (auto simp add: compatible_def complements_def)
    have [iff]: ‹iso_register (A;compA)›
      using compX complements_def by blast

    have ‹compatible (A ∘ U) A›
      by (metis assms(1) assms(2) comp_id compatible_comp_inner complements_def is_unit_register_def)
    then have compat'[simp]: ‹compatible (A o U) (A; compA)›
      by (auto intro!: compatible3')
    moreover have ‹equivalent_registers (A; compA) id›
      using compX complements_def equivalent_registers_sym iso_register_equivalent_id by blast
    ultimately have compat[simp]: ‹compatible (A o U) id›
      using equivalent_registers_compatible2 by blast

    have aux: ‹equivalent_registers (U;id) id›
      using assms(1) equivalent_registers_sym register_id unit_register_pair by blast

    have ‹equivalent_registers (A o U; id) (A o U; (A; compA))›
      by (auto intro!: equivalent_registers_pair_right)
    also have ‹equivalent_registers … (A o U; (A o id; compA))›
      by (auto intro!: equivalent_registers_refl pair_is_register)
    also have ‹equivalent_registers … ((A o U; A o id); compA)›
      apply (intro equivalent_registers_assoc compatible_comp_inner)
      by auto
    also have ‹equivalent_registers … (A o (U; id); compA)›
      by (metis (no_types, opaque_lifting) assms(1) assms(2) calculation complements_def equivalent_registers_sym equivalent_registers_trans is_unit_register_def register_comp_pair)
    also have ‹equivalent_registers … (A o id; compA)›
      apply (intro equivalent_registers_pair_left equivalent_registers_comp)
      using aux by (auto simp: assms)
    also have ‹equivalent_registers … id›
      by (simp add: ‹equivalent_registers (A;compA) id›)
    finally show ‹is_unit_register (A o U)›
      using compat complementsI equivalent_registers_sym is_unit_register_def iso_register_equivalent_id by blast
  qed
  from this[cancel_with_type]
  show ?thesis
    by -
qed

lemma unit_register_compose_right:
  assumes [simp]: ‹is_unit_register U›
  assumes [simp]: ‹iso_register A›
  shows ‹is_unit_register (U o A)›
proof (unfold is_unit_register_def, rule complementsI)
  show ‹compatible (U ∘ A) id›
    by (simp add: iso_register_is_register)
  have 1: ‹iso_register ((U;id) ∘ A ⊗⇩r id)›
    by (meson assms(1) assms(2) complements_def is_unit_register_def iso_register_comp iso_register_id iso_register_tensor_is_iso_register)
  have 2: ‹id ∘ ((U;id) ∘ A ⊗⇩r id) = (U ∘ A;id)›
    by (metis assms(1) assms(2) complements_def fun.map_id is_unit_register_def iso_register_id iso_register_is_register pair_o_tensor)
  show ‹iso_register (U ∘ A;id)›
    using 1 2 by auto
qed

lemma unit_register_unique:
  assumes ‹is_unit_register F›
  assumes ‹is_unit_register G›
  shows ‹equivalent_registers F G›
proof -
  have ‹complements F id› ‹complements G id›
    using assms by (metis complements_def equivalent_registers_def id_comp is_unit_register_def)+
  then show ?thesis
    by (meson complement_unique complements_sym equivalent_registers_sym equivalent_registers_trans)
qed

lemma unit_register_domains_isomorphic:
  fixes F :: ‹'a::domain update ⇒ 'c::domain update›
  fixes G :: ‹'b::domain update ⇒ 'd::domain update›
  assumes ‹is_unit_register F›
  assumes ‹is_unit_register G›
  shows ‹∃I :: 'a update ⇒ 'b update. iso_register I›
proof -
  have ‹is_unit_register ((λd. tensor_update id_update d) o G)›
    by (simp add: assms(2) unit_register_compose_left)
  moreover have ‹is_unit_register ((λc. tensor_update c id_update) o F)›
    using assms(1) register_tensor_left unit_register_compose_left by blast
  ultimately have ‹equivalent_registers ((λd. tensor_update id_update d) o G) ((λc. tensor_update c id_update) o F)›
    using unit_register_unique by blast
  then show ?thesis
    unfolding equivalent_registers_def by auto
qed


lemma id_complement_is_unit_register[simp]: ‹is_unit_register (complement id)›
  by (metis is_unit_register_def complement_is_complement complements_def complements_sym equivalent_registers_def id_comp register_id)

type_synonym unit_register_domain = ‹(some_domain, some_domain) complement_domain_simple›
definition unit_register :: ‹unit_register_domain update ⇒ 'a::domain update› where ‹unit_register = (SOME U. is_unit_register U)›

lemma unit_register_is_unit_register[simp]: ‹is_unit_register (unit_register :: unit_register_domain update ⇒ 'a::domain update)›
proof -
  note [[simproc del: compatibility_warn]]
  let ?U = ‹unit_register :: unit_register_domain update ⇒ 'a::domain update›
  let ?U1 = ‹complement id :: unit_register_domain update ⇒ some_domain update›
  from complement_exists[OF register_id[where 'a='a]]
  have ‹let 'x::domain = cdc (id::'a update ⇒ _) in is_unit_register ?U›
  proof with_type_mp
    with_type_case
    then obtain U2 :: ‹'x update ⇒ 'a update› where comp1: ‹complements id U2›
      by blast
    then have [simp]: ‹register U2› ‹compatible id U2› ‹compatible id U2›
      by (auto simp add: compatible_def complements_def)

    have ‹is_unit_register ?U1› ‹is_unit_register U2›
       by (auto simp: comp1 complements_sym is_unit_register_def)

    then obtain I :: ‹unit_register_domain update ⇒ 'x update› where ‹iso_register I›
      apply atomize_elim by (rule unit_register_domains_isomorphic)
    with ‹is_unit_register U2› have ‹is_unit_register (U2 o I)›
      by (rule unit_register_compose_right)
    then show ‹is_unit_register ?U›
      by (metis someI_ex unit_register_def)
  qed
  from this[cancel_with_type]
  show ?thesis
    by -
qed

lemma unit_register_domain_tensor_unit:
  fixes U :: ‹'a::domain update ⇒ _›
  assumes ‹is_unit_register U›
  shows ‹∃I :: 'b::domain update ⇒ ('a*'b) update. iso_register I›
  (* Can we show that I = (λx. tensor_update id_update x) ? It would be nice but I do not see how to prove it. *)
proof -
  from complement_exists[OF register_id[where 'a='b]]
  have ‹let 'x::domain = cdc (id :: 'b update ⇒ _) in
        ∃I :: 'b::domain update ⇒ ('a*'b) update. iso_register I›
  proof with_type_mp
    note [[simproc del: compatibility_warn]]
    with_type_case
    assume ‹∃G :: 'x update ⇒ 'b update. complements id G›
    then obtain U' :: ‹'x update ⇒ 'b update› where comp: ‹complements id U'›
      by blast
    then have [simp]: ‹register U'› ‹compatible id U'› ‹compatible U' id›
      by (auto simp add: compatible_def complements_def)
    have ‹is_unit_register U'›
      by (simp add: comp complements_sym is_unit_register_def)

    have ‹equivalent_registers (id :: 'b update ⇒ _) (U'; id)›
      using comp complements_def complements_sym iso_register_equivalent_id by blast
    then obtain J :: ‹'b update ⇒ (('x * 'b) update)› where ‹iso_register J›
      using equivalent_registers_def iso_register_inv by blast
    moreover obtain K :: ‹'x update ⇒ 'a update› where ‹iso_register K›
      apply atomize_elim 
      using ‹is_unit_register U'› assms
      by (rule unit_register_domains_isomorphic)
    ultimately have ‹iso_register ((K ⊗⇩r id) o J)›
      by auto
    then show ‹∃I :: 'b::domain update ⇒ ('a*'b) update. iso_register I›
      by auto
  qed
  from this[cancel_with_type]
  show ?thesis
    by-
qed

lemma compatible_complement_pair1:
  assumes ‹compatible F G›
  shows ‹compatible F (complement (F;G))›
  by (metis assms compatible_comp_left compatible_complement_right pair_is_register register_Fst register_pair_Fst)

lemma compatible_complement_pair2:
  assumes [simp]: ‹compatible F G›
  shows ‹compatible G (complement (F;G))›
proof -
  have ‹compatible (F;G) (complement (F;G))›
    by simp
  then have ‹compatible ((F;G) o Snd) (complement (F;G))›
    by auto
  then show ?thesis
    by (auto simp: register_pair_Snd)
qed

lemma equivalent_complements:
  assumes ‹complements F G›
  assumes ‹equivalent_registers G G'›
  shows ‹complements F G'›
  apply (rule complementsI)
   apply (metis assms(1) assms(2) compatible_comp_right complements_def equivalent_registers_def iso_register_is_register)
  by (metis assms(1) assms(2) complements_def equivalent_registers_def equivalent_registers_pair_right iso_register_comp)

lemma complements_complement_pair:
  assumes [simp]: ‹compatible F G›
  assumes FG': ‹complements (F;G) FG'›
  shows ‹complements F (G; FG')›
proof (rule complementsI)
  note [[simproc del: compatibility_warn]]
  have ‹compatible (F;G) FG'›
    using FG' complements_def by auto
  then have [simp]: ‹compatible F FG'›
    by (smt (verit)assms(1) compatibleI compatible_register1 compatible_register2 id_update_right register_of_id register_pair_apply' swap_registers)
  have [simp]: ‹compatible G FG'›
    by (smt (verit) register_pair_apply ‹compatible (F;G) FG'› assms(1) compatibleI compatible_register1 compatible_register2 id_update_right register_of_id swap_registers)

  have ‹equivalent_registers (F; (G; FG')) ((F;G); FG')›
    apply (rule equivalent_registers_assoc)
      apply simp
     apply (smt (verit) ‹compatible (F;G) FG'› assms(1) compatibleI compatible_register1 compatible_register2 id_update_right register_of_id register_pair_apply' swap_registers)
    by (smt (verit) register_pair_apply ‹compatible (F;G) FG'› assms(1) compatibleI compatible_register1 compatible_register2 id_update_right register_of_id swap_registers)
  also have ‹equivalent_registers … id›
    by (meson assms complement_is_complement complements_def equivalent_registers_sym iso_register_equivalent_id pair_is_register)
  finally show ‹iso_register (F;(G;FG'))›
    using equivalent_registers_sym iso_register_equivalent_id by blast
  show ‹compatible F (G;FG')›
    by (auto intro!: compatible3')
qed

lemma equivalent_registers_complement:
  assumes ‹equivalent_registers F G›
  assumes ‹complements F F'›
  assumes ‹complements G G'›
  shows ‹equivalent_registers F' G'›
  by (meson complement_unique assms(1) assms(2) assms(3) complements_sym equivalent_complements)

lemma equivalent_registers_complement':
  assumes ‹equivalent_registers F G›
  shows ‹equivalent_registers (complement F) (complement G)›
  using assms apply (rule equivalent_registers_complement)
  using assms complement_is_complement equivalent_registers_register_left equivalent_registers_register_right
  by blast+

lemma complements_complement_pair':
  assumes [simp]: ‹compatible F G›
  assumes FG': ‹complements (F;G) FG'›
  shows ‹complements G (F; FG')›
proof -
  have ‹equivalent_registers (F;G) (G;F)›
    using assms(1) equivalent_registers_def iso_register_swap pair_is_register pair_o_swap by blast
  with FG' have *: ‹complements (G;F) FG'›
    by (meson complements_sym equivalent_complements)
  show ?thesis
    apply (rule complements_complement_pair)
    using * by (simp_all add: compatible_sym)
qed

lemma complements_chain: 
  assumes [simp]: ‹register F› ‹register G›
  shows ‹complements (F o G) (complement F; F o complement G)›
proof (rule complementsI)
  show ‹compatible (F o G) (complement F; F o complement G)›
    by auto
  have ‹equivalent_registers (F ∘ G;(complement F;F ∘ complement G)) (F ∘ G;(F ∘ complement G;complement F))›
    apply (rule equivalent_registersI[where I=‹id ⊗⇩r swap›])
    by (auto intro!: iso_register_tensor_is_iso_register simp: pair_o_tensor)
  also have ‹equivalent_registers … ((F ∘ G;F ∘ complement G);complement F)›
    apply (rule equivalent_registersI[where I=assoc])
    by (auto intro!: iso_register_tensor_is_iso_register simp: pair_o_tensor)
  also have ‹equivalent_registers … (F o (G; complement G);complement F)›
    by (metis (no_types, lifting) assms(1) assms(2) calculation compatible_complement_right
        equivalent_registers_sym equivalent_registers_trans register_comp_pair)
  also have ‹equivalent_registers … (F o id;complement F)›
    apply (rule equivalent_registers_pair_left, simp)
    apply (rule equivalent_registers_comp, simp)
    by (metis assms(2) complement_is_complement complements_def equivalent_registers_def iso_register_def)
  also have ‹equivalent_registers … id›
    by (metis assms(1) comp_id complement_is_complement complements_def equivalent_registers_def iso_register_def)
  finally show ‹iso_register (F ∘ G;(complement F;F ∘ complement G))›
    using equivalent_registers_sym iso_register_equivalent_id by blast
qed

lemma complements_Fst_Snd[simp]: ‹complements Fst Snd›
  by (auto intro!: complementsI simp: pair_Fst_Snd)

lemma complements_Snd_Fst[simp]: ‹complements Snd Fst›
  by (auto intro!: complementsI simp flip: swap_def)

lemma compatible_unit_register[simp]: ‹register F ⟹ compatible F unit_register›
  using compatible_sym unit_register_compatible unit_register_is_unit_register by blast

lemma complements_id_unit_register[simp]: ‹complements id unit_register›
  using complements_sym is_unit_register_def unit_register_is_unit_register by blast

lemma complements_iso_unit_register: ‹iso_register I ⟹ is_unit_register U ⟹ complements I U›
  using complements_sym equivalent_complements is_unit_register_def iso_register_equivalent_id by blast

lemma iso_register_complement_is_unit_register[simp]:
  assumes ‹iso_register F›
  shows ‹is_unit_register (complement F)›
  by (meson assms complement_is_complement complements_sym equivalent_complements equivalent_registers_sym is_unit_register_def iso_register_equivalent_id iso_register_is_register)

text ‹Adding support for \<^term>‹is_unit_register F› and \<^term>‹complements F G› to the [@{attribute register}] attribute›
lemmas [register_attribute_rule] = is_unit_register_def[THEN iffD1] complements_def[THEN iffD1]
lemmas [register_attribute_rule_immediate] = asm_rl[of ‹is_unit_register _›]

no_notation comp_update (infixl "*⇩u" 55)
no_notation tensor_update (infixr "⊗⇩u" 70)
unbundle no register_syntax


end