Theory Laws_Complement_Quantum

(*
 * This is an autogenerated file. Do not edit.
 * The original is Laws_Complement.thy. It was converted using instantiate_laws.py.
 *)

section ‹Generic laws about complements, instantiated quantumly›

theory Laws_Complement_Quantum
  imports Laws_Quantum Axioms_Complement_Quantum
begin

notation cblinfun_compose (infixl ‹*⇩u› 55)
notation tensor_op (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 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::finite update ⇒ 'b::finite update) ⇒ (('a,'b) complement_domain update ⇒ 'b update)› where
  ‹complement F = (SOME G :: ('a, 'b) complement_domain update ⇒ 'b update. compatible F G ∧ iso_register (F;G))›

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

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

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 sep4: ‹separating TYPE('z::finite) {(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::finite update› and b::‹'u::finite update› and c::‹'v::finite update› and d::‹'w::finite update›
    by (simp add: register_pair_apply Fst_def Snd_def comp_tensor_op)
  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 comp_tensor_op)
  moreover have ‹iso_register …›
    apply (auto intro!: iso_register_comp iso_register_tensor_is_iso_register)
    using assms complement_is_complement complements_def by blast+
  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 -
  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; complement X))›
    apply (rule equivalent_registers_pair_right)
     apply (auto intro!: unit_register_compatible)
    using complement_is_complement complements_def equivalent_registersI id_comp register_id that(2) by blast
  also have ‹equivalent_registers … ((U; X); complement X)›
    apply (rule equivalent_registers_assoc)
    by auto
  finally have ‹complements (U; X) (complement X)›
    by (auto simp: equivalent_registers_def complements_def)
  moreover have ‹equivalent_registers (X; complement X) id›
    by (metis complement_is_complement complements_def equivalent_registers_def iso_register_def that)
  ultimately show ?thesis
    by (meson complement_unique complement_is_complement complements_sym equivalent_registers_sym equivalent_registers_trans that)
qed

lemma unit_register_compose_left:
  assumes [simp]: ‹is_unit_register U›
  assumes [simp]: ‹register A›
  shows ‹is_unit_register (A o U)›
proof -
  have ‹compatible (A o U) (A; complement A)›
    apply (auto intro!: compatible3')
    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) id›
    by (metis assms(2) compatible_comp_right complement_is_complement complements_def iso_register_def)
  have ‹equivalent_registers (A o U; id) (A o U; (A; complement A))›
    apply (auto intro!: equivalent_registers_pair_right)
    using assms(2) complement_is_complement complements_def equivalent_registers_def id_comp register_id by blast
  also have ‹equivalent_registers … ((A o U; A o id); complement A)›
    apply auto
    by (metis (no_types, opaque_lifting) compat assms(1) assms(2) compatible_comp_left compatible_def compatible_register1 complement_is_complement complements_def equivalent_registers_assoc id_apply register_unit_register)
  also have ‹equivalent_registers … (A o (U; id); complement A)›
    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; complement A)›
    apply (intro equivalent_registers_pair_left equivalent_registers_comp)
      apply (auto simp: assms)
    using assms(1) equivalent_registers_sym register_id unit_register_pair by blast
  also have ‹equivalent_registers … id›
    by (metis assms(2) comp_id complement_is_complement complements_def equivalent_registers_def iso_register_inv iso_register_inv_comp2 pair_is_register)
  finally show ?thesis
    using compat complementsI equivalent_registers_sym is_unit_register_def iso_register_equivalent_id by blast
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::finite update ⇒ 'c::finite update›
  fixes G :: ‹'b::finite update ⇒ 'd::finite 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_op id_cblinfun d) o G)›
    by (simp add: assms(2) unit_register_compose_left)
  moreover have ‹is_unit_register ((λc. tensor_op c id_cblinfun) o F)›
    using assms(1) register_tensor_left unit_register_compose_left by blast
  ultimately have ‹equivalent_registers ((λd. tensor_op id_cblinfun d) o G) ((λc. tensor_op c id_cblinfun) 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 = ‹(unit, unit) complement_domain›
definition unit_register :: ‹unit_register_domain update ⇒ 'a::finite 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::finite update)›
proof -
  let ?U0 = ‹complement id :: unit_register_domain update ⇒ unit update›
  let ?U1 = ‹complement id :: ('a, 'a) complement_domain update ⇒ 'a update›
  have ‹is_unit_register ?U0› ‹is_unit_register ?U1›
    by auto
  then obtain I :: ‹unit_register_domain update ⇒ ('a, 'a) complement_domain update› where ‹iso_register I›
    apply atomize_elim by (rule unit_register_domains_isomorphic)
  with ‹is_unit_register ?U1› have ‹is_unit_register (?U1 o I)›
    by (rule unit_register_compose_right)
  then show ?thesis
    by (metis someI_ex unit_register_def)
qed

lemma unit_register_domain_tensor_unit:
  fixes U :: ‹'a::finite update ⇒ _›
  assumes ‹is_unit_register U›
  shows ‹∃I :: 'b::finite update ⇒ ('a*'b) update. iso_register I›
  (* Can we show that I = (λx. tensor_op id_cblinfun x) ? It would be nice but I do not see how to prove it. *)
proof -
  have ‹equivalent_registers (id :: 'b update ⇒ _) (complement id; id)›
    using id_complement_is_unit_register iso_register_equivalent_id register_id unit_register_pair by blast
  then obtain J :: ‹'b update ⇒ ((('b, 'b) complement_domain * 'b) update)› where ‹iso_register J›
    using equivalent_registers_def iso_register_inv by blast
  moreover obtain K :: ‹('b, 'b) complement_domain update ⇒ 'a update› where ‹iso_register K›
    using assms id_complement_is_unit_register unit_register_domains_isomorphic by blast
  ultimately have ‹iso_register ((K ⊗⇩r id) o J)›
    by auto
  then show ?thesis   
    by auto
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›
  shows ‹complements F (G; complement (F;G))›
proof (rule complementsI)
  have ‹equivalent_registers (F; (G; complement (F;G))) ((F;G); complement (F;G))›
    apply (rule equivalent_registers_assoc)
    by (auto simp add: compatible_complement_pair1 compatible_complement_pair2)
  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;complement (F;G)))›
    using equivalent_registers_sym iso_register_equivalent_id by blast
  show ‹compatible F (G;complement (F;G))›
    using assms compatible3' compatible_complement_pair1 compatible_complement_pair2 by blast
qed

lemma equivalent_registers_complement:
  assumes ‹equivalent_registers F G›
  shows ‹equivalent_registers (complement F) (complement G)›
proof -
  have ‹complements F (complement F)›
    using assms complement_is_complement equivalent_registers_register_left by blast
  with assms have ‹complements G (complement F)›
    by (meson complements_sym equivalent_complements)
  then show ?thesis
    by (rule complement_unique)
qed


lemma complements_complement_pair':
  assumes [simp]: ‹compatible F G›
  shows ‹complements G (F; complement (F;G))›
proof -
  have ‹equivalent_registers (F;G) (G;F)›
    apply (rule equivalent_registersI[where I=swap])
    by auto
  then have ‹equivalent_registers (complement (F;G)) (complement (G;F))›
    by (rule equivalent_registers_complement)
  then have ‹equivalent_registers (F; (complement (F;G))) (F; (complement (G;F)))›
    apply (rule equivalent_registers_pair_right[rotated])
    using assms compatible_complement_pair1 by blast
  moreover have ‹complements G (F; complement (G;F))›
    apply (rule complements_complement_pair)
    using assms compatible_sym by blast
  ultimately show ?thesis
    by (meson equivalent_complements equivalent_registers_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 cblinfun_compose (infixl ‹*⇩u› 55)
no_notation tensor_op (infixr ‹⊗⇩u› 70)

end