Theory Laws_Complement
section ‹Generic laws about complements›
theory Laws_Complement
imports Laws Axioms_Complement
begin
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
qed
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
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::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›
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)
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›
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 comp_update (infixl ‹*⇩u› 55)
no_notation tensor_update (infixr ‹⊗⇩u› 70)
end