Theory Laws_Complement

section Generic laws about complements

theory Laws_Complement
  imports Laws Axioms_Complement

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 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

definition complement :: ('a::domain update  'b::domain 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::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 
    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

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)

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

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

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)

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

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
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 -
  let ?U0 = complement id :: unit_register_domain update  some_domain 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)

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 -
  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

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)

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

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)

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)

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

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 termis_unit_register F and termcomplements 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)