Theory Laws_Quantum
section ‹Generic laws about registers, instantiated quantumly›
theory Laws_Quantum
imports Axioms_Quantum
begin
text ‹This notation is only used inside this file›
notation cblinfun_compose (infixl "*⇩u" 55)
notation tensor_op (infixr "⊗⇩u" 70)
notation register_pair ("'(_;_')")
subsection ‹Elementary facts›
declare complex_vector.linear_id[simp]
declare cblinfun_compose_id_left[simp]
declare cblinfun_compose_id_right[simp]
declare register_preregister[simp]
declare register_comp[simp]
declare register_of_id[simp]
declare register_tensor_left[simp]
declare register_tensor_right[simp]
declare preregister_mult_right[simp]
declare preregister_mult_left[simp]
declare register_id[simp]
subsection ‹Preregisters›
lemma preregister_tensor_left[simp]: ‹clinear (λb::'b::finite update. tensor_op a b)›
for a :: ‹'a::finite update›
proof -
have ‹clinear ((λb1::('a×'b) update. (a ⊗⇩u id_cblinfun) *⇩u b1) o (λb. tensor_op id_cblinfun b))›
by (rule clinear_compose; simp)
then show ?thesis
by (simp add: o_def comp_tensor_op)
qed
lemma preregister_tensor_right[simp]: ‹clinear (λa::'a::finite update. tensor_op a b)›
for b :: ‹'b::finite update›
proof -
have ‹clinear ((λa1::('a×'b) update. (id_cblinfun ⊗⇩u b) *⇩u a1) o (λa. tensor_op a id_cblinfun))›
by (rule clinear_compose, simp_all)
then show ?thesis
by (simp add: o_def comp_tensor_op)
qed
subsection ‹Registers›
lemma id_update_tensor_register[simp]:
assumes ‹register F›
shows ‹register (λa::'a::finite update. id_cblinfun ⊗⇩u F a)›
using assms apply (rule register_comp[unfolded o_def])
by simp
lemma register_tensor_id_update[simp]:
assumes ‹register F›
shows ‹register (λa::'a::finite update. F a ⊗⇩u id_cblinfun)›
using assms apply (rule register_comp[unfolded o_def])
by simp
subsection ‹Tensor product of registers›
definition register_tensor (infixr "⊗⇩r" 70) where
"register_tensor F G = register_pair (λa. tensor_op (F a) id_cblinfun) (λb. tensor_op id_cblinfun (G b))"
lemma register_tensor_is_register:
fixes F :: "'a::finite update ⇒ 'b::finite update" and G :: "'c::finite update ⇒ 'd::finite update"
shows "register F ⟹ register G ⟹ register (F ⊗⇩r G)"
unfolding register_tensor_def
apply (rule register_pair_is_register)
by (simp_all add: comp_tensor_op)
lemma register_tensor_apply[simp]:
fixes F :: "'a::finite update ⇒ 'b::finite update" and G :: "'c::finite update ⇒ 'd::finite update"
assumes ‹register F› and ‹register G›
shows "(F ⊗⇩r G) (a ⊗⇩u b) = F a ⊗⇩u G b"
unfolding register_tensor_def
apply (subst register_pair_apply)
unfolding register_tensor_def
by (simp_all add: assms comp_tensor_op)
definition "separating (_::'b::finite itself) A ⟷
(∀F G :: 'a::finite update ⇒ 'b update. clinear F ⟶ clinear G ⟶ (∀x∈A. F x = G x) ⟶ F = G)"
lemma separating_UNIV[simp]: ‹separating TYPE(_) UNIV›
unfolding separating_def by auto
lemma separating_mono: ‹A ⊆ B ⟹ separating TYPE('a::finite) A ⟹ separating TYPE('a) B›
unfolding separating_def by (meson in_mono)
lemma register_eqI: ‹separating TYPE('b::finite) A ⟹ clinear F ⟹ clinear G ⟹ (⋀x. x∈A ⟹ F x = G x) ⟹ F = (G::_ ⇒ 'b update)›
unfolding separating_def by auto
lemma separating_tensor:
fixes A :: ‹'a::finite update set› and B :: ‹'b::finite update set›
assumes [simp]: ‹separating TYPE('c::finite) A›
assumes [simp]: ‹separating TYPE('c) B›
shows ‹separating TYPE('c) {a ⊗⇩u b | a b. a∈A ∧ b∈B}›
proof (unfold separating_def, intro allI impI)
fix F G :: ‹('a×'b) update ⇒ 'c update›
assume [simp]: ‹clinear F› ‹clinear G›
have [simp]: ‹clinear (λx. F (a ⊗⇩u x))› for a
using _ ‹clinear F› apply (rule clinear_compose[unfolded o_def])
by simp
have [simp]: ‹clinear (λx. G (a ⊗⇩u x))› for a
using _ ‹clinear G› apply (rule clinear_compose[unfolded o_def])
by simp
have [simp]: ‹clinear (λx. F (x ⊗⇩u b))› for b
using _ ‹clinear F› apply (rule clinear_compose[unfolded o_def])
by simp
have [simp]: ‹clinear (λx. G (x ⊗⇩u b))› for b
using _ ‹clinear G› apply (rule clinear_compose[unfolded o_def])
by simp
assume ‹∀x∈{a ⊗⇩u b |a b. a∈A ∧ b∈B}. F x = G x›
then have EQ: ‹F (a ⊗⇩u b) = G (a ⊗⇩u b)› if ‹a ∈ A› and ‹b ∈ B› for a b
using that by auto
then have ‹F (a ⊗⇩u b) = G (a ⊗⇩u b)› if ‹a ∈ A› for a b
apply (rule register_eqI[where A=B, THEN fun_cong, where x=b, rotated -1])
using that by auto
then have ‹F (a ⊗⇩u b) = G (a ⊗⇩u b)› for a b
apply (rule register_eqI[where A=A, THEN fun_cong, where x=a, rotated -1])
by auto
then show "F = G"
apply (rule tensor_extensionality[rotated -1])
by auto
qed
lemma register_tensor_distrib:
assumes [simp]: ‹register F› ‹register G› ‹register H› ‹register L›
shows ‹(F ⊗⇩r G) o (H ⊗⇩r L) = (F o H) ⊗⇩r (G o L)›
apply (rule tensor_extensionality)
by (auto intro!: register_comp register_preregister register_tensor_is_register)
text ‹The following is easier to apply using the @{method rule}-method than @{thm [source] separating_tensor}›
lemma separating_tensor':
fixes A :: ‹'a::finite update set› and B :: ‹'b::finite update set›
assumes ‹separating TYPE('c::finite) A›
assumes ‹separating TYPE('c) B›
assumes ‹C = {a ⊗⇩u b | a b. a∈A ∧ b∈B}›
shows ‹separating TYPE('c) C›
using assms
by (simp add: separating_tensor)
lemma tensor_extensionality3:
fixes F G :: ‹('a::finite×'b::finite×'c::finite) update ⇒ 'd::finite update›
assumes [simp]: ‹register F› ‹register G›
assumes "⋀f g h. F (f ⊗⇩u g ⊗⇩u h) = G (f ⊗⇩u g ⊗⇩u h)"
shows "F = G"
proof (rule register_eqI[where A=‹{a⊗⇩ub⊗⇩uc| a b c. True}›])
have ‹separating TYPE('d) {b ⊗⇩u c |b c. True}›
apply (rule separating_tensor'[where A=UNIV and B=UNIV])
by auto
then show ‹separating TYPE('d) {a ⊗⇩u b ⊗⇩u c |a b c. True}›
apply (rule_tac separating_tensor'[where A=UNIV and B=‹{b⊗⇩uc| b c. True}›])
by auto
show ‹clinear F› ‹clinear G› by auto
show ‹x ∈ {a ⊗⇩u b ⊗⇩u c |a b c. True} ⟹ F x = G x› for x
using assms(3) by auto
qed
lemma tensor_extensionality3':
fixes F G :: ‹(('a::finite×'b::finite)×'c::finite) update ⇒ 'd::finite update›
assumes [simp]: ‹register F› ‹register G›
assumes "⋀f g h. F ((f ⊗⇩u g) ⊗⇩u h) = G ((f ⊗⇩u g) ⊗⇩u h)"
shows "F = G"
proof (rule register_eqI[where A=‹{(a⊗⇩ub)⊗⇩uc| a b c. True}›])
have ‹separating TYPE('d) {a ⊗⇩u b | a b. True}›
apply (rule separating_tensor'[where A=UNIV and B=UNIV])
by auto
then show ‹separating TYPE('d) {(a ⊗⇩u b) ⊗⇩u c |a b c. True}›
apply (rule_tac separating_tensor'[where B=UNIV and A=‹{a⊗⇩ub| a b. True}›])
by auto
show ‹clinear F› ‹clinear G› by auto
show ‹x ∈ {(a ⊗⇩u b) ⊗⇩u c |a b c. True} ⟹ F x = G x› for x
using assms(3) by auto
qed
lemma register_tensor_id[simp]: ‹id ⊗⇩r id = id›
apply (rule tensor_extensionality)
by (auto simp add: register_tensor_is_register)
subsection ‹Pairs and compatibility›
definition compatible :: ‹('a::finite update ⇒ 'c::finite update)
⇒ ('b::finite update ⇒ 'c update) ⇒ bool› where
‹compatible F G ⟷ register F ∧ register G ∧ (∀a b. F a *⇩u G b = G b *⇩u F a)›
lemma compatibleI:
assumes "register F" and "register G"
assumes ‹⋀a b. (F a) *⇩u (G b) = (G b) *⇩u (F a)›
shows "compatible F G"
using assms unfolding compatible_def by simp
lemma swap_registers:
assumes "compatible R S"
shows "R a *⇩u S b = S b *⇩u R a"
using assms unfolding compatible_def by metis
lemma compatible_sym: "compatible x y ⟹ compatible y x"
by (simp add: compatible_def)
lemma pair_is_register[simp]:
assumes "compatible F G"
shows "register (F; G)"
by (metis assms compatible_def register_pair_is_register)
lemma register_pair_apply:
assumes ‹compatible F G›
shows ‹(F; G) (a ⊗⇩u b) = (F a) *⇩u (G b)›
apply (rule register_pair_apply)
using assms unfolding compatible_def by metis+
lemma register_pair_apply':
assumes ‹compatible F G›
shows ‹(F; G) (a ⊗⇩u b) = (G b) *⇩u (F a)›
apply (subst register_pair_apply)
using assms by (auto simp: compatible_def intro: register_preregister)
lemma compatible_comp_left[simp]: "compatible F G ⟹ register H ⟹ compatible (F ∘ H) G"
by (simp add: compatible_def)
lemma compatible_comp_right[simp]: "compatible F G ⟹ register H ⟹ compatible F (G ∘ H)"
by (simp add: compatible_def)
lemma compatible_comp_inner[simp]:
"compatible F G ⟹ register H ⟹ compatible (H ∘ F) (H ∘ G)"
by (smt (verit, best) comp_apply compatible_def register_comp register_mult)
lemma compatible_register1: ‹compatible F G ⟹ register F›
by (simp add: compatible_def)
lemma compatible_register2: ‹compatible F G ⟹ register G›
by (simp add: compatible_def)
lemma pair_o_tensor:
assumes "compatible A B" and [simp]: ‹register C› and [simp]: ‹register D›
shows "(A; B) o (C ⊗⇩r D) = (A o C; B o D)"
apply (rule tensor_extensionality)
using assms by (simp_all add: register_tensor_is_register register_pair_apply clinear_compose)
lemma compatible_tensor_id_update_left[simp]:
fixes F :: "'a::finite update ⇒ 'c::finite update" and G :: "'b::finite update ⇒ 'c::finite update"
assumes "compatible F G"
shows "compatible (λa. id_cblinfun ⊗⇩u F a) (λa. id_cblinfun ⊗⇩u G a)"
using assms apply (rule compatible_comp_inner[unfolded o_def])
by simp
lemma compatible_tensor_id_update_right[simp]:
fixes F :: "'a::finite update ⇒ 'c::finite update" and G :: "'b::finite update ⇒ 'c::finite update"
assumes "compatible F G"
shows "compatible (λa. F a ⊗⇩u id_cblinfun) (λa. G a ⊗⇩u id_cblinfun)"
using assms apply (rule compatible_comp_inner[unfolded o_def])
by simp
lemma compatible_tensor_id_update_rl[simp]:
assumes "register F" and "register G"
shows "compatible (λa. F a ⊗⇩u id_cblinfun) (λa. id_cblinfun ⊗⇩u G a)"
apply (rule compatibleI)
using assms by (auto simp: comp_tensor_op)
lemma compatible_tensor_id_update_lr[simp]:
assumes "register F" and "register G"
shows "compatible (λa. id_cblinfun ⊗⇩u F a) (λa. G a ⊗⇩u id_cblinfun)"
apply (rule compatibleI)
using assms by (auto simp: comp_tensor_op)
lemma register_comp_pair:
assumes [simp]: ‹register F› and [simp]: ‹compatible G H›
shows "(F o G; F o H) = F o (G; H)"
proof (rule tensor_extensionality)
show ‹clinear (F ∘ G;F ∘ H)› and ‹clinear (F ∘ (G;H))›
by simp_all
have [simp]: ‹compatible (F o G) (F o H)›
apply (rule compatible_comp_inner, simp)
by simp
then have [simp]: ‹register (F ∘ G)› ‹register (F ∘ H)›
unfolding compatible_def by auto
from assms have [simp]: ‹register G› ‹register H›
unfolding compatible_def by auto
fix a b
show ‹(F ∘ G;F ∘ H) (a ⊗⇩u b) = (F ∘ (G;H)) (a ⊗⇩u b)›
by (auto simp: register_pair_apply register_mult comp_tensor_op)
qed
lemma swap_registers_left:
assumes "compatible R S"
shows "R a *⇩u S b *⇩u c = S b *⇩u R a *⇩u c"
using assms unfolding compatible_def by metis
lemma swap_registers_right:
assumes "compatible R S"
shows "c *⇩u R a *⇩u S b = c *⇩u S b *⇩u R a"
by (metis assms cblinfun_compose_assoc compatible_def)
lemmas compatible_ac_rules = swap_registers cblinfun_compose_assoc[symmetric] swap_registers_right
subsection ‹Fst and Snd›
definition Fst where ‹Fst a = a ⊗⇩u id_cblinfun›
definition Snd where ‹Snd a = id_cblinfun ⊗⇩u a›
lemma register_Fst[simp]: ‹register Fst›
unfolding Fst_def by (rule register_tensor_left)
lemma register_Snd[simp]: ‹register Snd›
unfolding Snd_def by (rule register_tensor_right)
lemma compatible_Fst_Snd[simp]: ‹compatible Fst Snd›
apply (rule compatibleI, simp, simp)
by (simp add: Fst_def Snd_def comp_tensor_op)
lemmas compatible_Snd_Fst[simp] = compatible_Fst_Snd[THEN compatible_sym]
definition ‹swap = (Snd; Fst)›
lemma swap_apply[simp]: "swap (a ⊗⇩u b) = (b ⊗⇩u a)"
unfolding swap_def
by (simp add: Axioms_Quantum.register_pair_apply Fst_def Snd_def comp_tensor_op)
lemma swap_o_Fst: "swap o Fst = Snd"
by (auto simp add: Fst_def Snd_def)
lemma swap_o_Snd: "swap o Snd = Fst"
by (auto simp add: Fst_def Snd_def)
lemma register_swap[simp]: ‹register swap›
by (simp add: swap_def)
lemma pair_Fst_Snd: ‹(Fst; Snd) = id›
apply (rule tensor_extensionality)
by (simp_all add: register_pair_apply Fst_def Snd_def comp_tensor_op)
lemma swap_o_swap[simp]: ‹swap o swap = id›
by (metis swap_def compatible_Snd_Fst pair_Fst_Snd register_comp_pair register_swap swap_o_Fst swap_o_Snd)
lemma swap_swap[simp]: ‹swap (swap x) = x›
by (simp add: pointfree_idE)
lemma inv_swap[simp]: ‹inv swap = swap›
by (meson inv_unique_comp swap_o_swap)
lemma register_pair_Fst:
assumes ‹compatible F G›
shows ‹(F;G) o Fst = F›
using assms by (auto intro!: ext simp: Fst_def register_pair_apply compatible_register2)
lemma register_pair_Snd:
assumes ‹compatible F G›
shows ‹(F;G) o Snd = G›
using assms by (auto intro!: ext simp: Snd_def register_pair_apply compatible_register1)
lemma register_Fst_register_Snd[simp]:
assumes ‹register F›
shows ‹(F o Fst; F o Snd) = F›
apply (rule tensor_extensionality)
using assms by (auto simp: register_pair_apply Fst_def Snd_def register_mult comp_tensor_op)
lemma register_Snd_register_Fst[simp]:
assumes ‹register F›
shows ‹(F o Snd; F o Fst) = F o swap›
apply (rule tensor_extensionality)
using assms by (auto simp: register_pair_apply Fst_def Snd_def register_mult comp_tensor_op)
lemma compatible3[simp]:
assumes [simp]: "compatible F G" and "compatible G H" and "compatible F H"
shows "compatible (F; G) H"
proof (rule compatibleI)
have [simp]: ‹register F› ‹register G› ‹register H›
using assms compatible_def by auto
then have [simp]: ‹clinear F› ‹clinear G› ‹clinear H›
using register_preregister by blast+
have [simp]: ‹clinear (λa. (F;G) a *⇩u z)› for z
apply (rule clinear_compose[unfolded o_def, of ‹(F;G)›])
by simp_all
have [simp]: ‹clinear (λa. z *⇩u (F;G) a)› for z
apply (rule clinear_compose[unfolded o_def, of ‹(F;G)›])
by simp_all
have "(F; G) (f ⊗⇩u g) *⇩u H h = H h *⇩u (F; G) (f ⊗⇩u g)" for f g h
proof -
have FH: "F f *⇩u H h = H h *⇩u F f"
using assms compatible_def by metis
have GH: "G g *⇩u H h = H h *⇩u G g"
using assms compatible_def by metis
have ‹(F; G) (f ⊗⇩u g) *⇩u (H h) = F f *⇩u G g *⇩u H h›
using ‹compatible F G› by (subst register_pair_apply, auto)
also have ‹… = H h *⇩u F f *⇩u G g›
using FH GH by (metis cblinfun_compose_assoc)
also have ‹… = H h *⇩u (F; G) (f ⊗⇩u g)›
using ‹compatible F G› by (subst register_pair_apply, auto simp: cblinfun_compose_assoc)
finally show ?thesis
by -
qed
then show "(F; G) fg *⇩u (H h) = (H h) *⇩u (F; G) fg" for fg h
apply (rule_tac tensor_extensionality[THEN fun_cong])
by auto
show "register H" and "register (F; G)"
by simp_all
qed
lemma compatible3'[simp]:
assumes "compatible F G" and "compatible G H" and "compatible F H"
shows "compatible F (G; H)"
apply (rule compatible_sym)
apply (rule compatible3)
using assms by (auto simp: compatible_sym)
lemma pair_o_swap[simp]:
assumes [simp]: "compatible A B"
shows "(A; B) o swap = (B; A)"
proof (rule tensor_extensionality)
have [simp]: "clinear A" "clinear B"
apply (metis (no_types, opaque_lifting) assms compatible_register1 register_preregister)
by (metis (full_types) assms compatible_register2 register_preregister)
then show ‹clinear ((A; B) ∘ swap)›
by simp
show ‹clinear (B; A)›
by (metis (no_types, lifting) assms compatible_sym register_preregister pair_is_register)
show ‹((A; B) ∘ swap) (a ⊗⇩u b) = (B; A) (a ⊗⇩u b)› for a b
apply (simp only: o_def swap_apply)
apply (subst register_pair_apply, simp)
apply (subst register_pair_apply, simp add: compatible_sym)
by (metis (no_types, lifting) assms compatible_def)
qed
subsection ‹Compatibility of register tensor products›
lemma compatible_register_tensor:
fixes F :: ‹'a::finite update ⇒ 'e::finite update› and G :: ‹'b::finite update ⇒ 'f::finite update›
and F' :: ‹'c::finite update ⇒ 'e update› and G' :: ‹'d::finite update ⇒ 'f update›
assumes [simp]: ‹compatible F F'›
assumes [simp]: ‹compatible G G'›
shows ‹compatible (F ⊗⇩r G) (F' ⊗⇩r G')›
proof -
note [intro!] =
clinear_compose[OF _ preregister_mult_right, unfolded o_def]
clinear_compose[OF _ preregister_mult_left, unfolded o_def]
clinear_compose
register_tensor_is_register
have [simp]: ‹register F› ‹register G› ‹register F'› ‹register G'›
using assms compatible_def by blast+
have [simp]: ‹register (F ⊗⇩r G)› ‹register (F' ⊗⇩r G')›
by (auto simp add: register_tensor_def)
have [simp]: ‹register (F;F')› ‹register (G;G')›
by auto
define reorder :: ‹(('a×'b) × ('c×'d)) update ⇒ (('a×'c) × ('b×'d)) update›
where ‹reorder = ((Fst o Fst; Snd o Fst); (Fst o Snd; Snd o Snd))›
have [simp]: ‹clinear reorder›
by (auto simp: reorder_def)
have [simp]: ‹reorder ((a ⊗⇩u b) ⊗⇩u (c ⊗⇩u d)) = ((a ⊗⇩u c) ⊗⇩u (b ⊗⇩u d))› for a b c d
apply (simp add: reorder_def register_pair_apply)
by (simp add: Fst_def Snd_def comp_tensor_op)
define Φ where ‹Φ c d = ((F;F') ⊗⇩r (G;G')) o reorder o (λσ. σ ⊗⇩u (c ⊗⇩u d))› for c d
have [simp]: ‹clinear (Φ c d)› for c d
unfolding Φ_def
by (auto intro: register_preregister)
have ‹Φ c d (a ⊗⇩u b) = (F ⊗⇩r G) (a ⊗⇩u b) *⇩u (F' ⊗⇩r G') (c ⊗⇩u d)› for a b c d
unfolding Φ_def by (auto simp: register_pair_apply comp_tensor_op)
then have Φ1: ‹Φ c d σ = (F ⊗⇩r G) σ *⇩u (F' ⊗⇩r G') (c ⊗⇩u d)› for c d σ
apply (rule_tac fun_cong[of _ _ σ])
apply (rule tensor_extensionality)
by auto
have ‹Φ c d (a ⊗⇩u b) = (F' ⊗⇩r G') (c ⊗⇩u d) *⇩u (F ⊗⇩r G) (a ⊗⇩u b)› for a b c d
unfolding Φ_def apply (auto simp: register_pair_apply)
by (metis assms(1) assms(2) compatible_def comp_tensor_op)
then have Φ2: ‹Φ c d σ = (F' ⊗⇩r G') (c ⊗⇩u d) *⇩u (F ⊗⇩r G) σ› for c d σ
apply (rule_tac fun_cong[of _ _ σ])
apply (rule tensor_extensionality)
by auto
from Φ1 Φ2 have ‹(F ⊗⇩r G) σ *⇩u (F' ⊗⇩r G') τ = (F' ⊗⇩r G') τ *⇩u (F ⊗⇩r G) σ› for τ σ
apply (rule_tac fun_cong[of _ _ τ])
apply (rule tensor_extensionality)
by auto
then show ?thesis
apply (rule compatibleI[rotated -1])
by auto
qed
subsection ‹Associativity of the tensor product›
definition assoc :: ‹(('a::finite×'b::finite)×'c::finite) update ⇒ ('a×('b×'c)) update› where
‹assoc = ((Fst; Snd o Fst); Snd o Snd)›
lemma assoc_is_hom[simp]: ‹clinear assoc›
by (auto simp: assoc_def)
lemma assoc_apply[simp]: ‹assoc ((a ⊗⇩u b) ⊗⇩u c) = (a ⊗⇩u (b ⊗⇩u c))›
by (auto simp: assoc_def register_pair_apply Fst_def Snd_def comp_tensor_op)
definition assoc' :: ‹('a×('b×'c)) update ⇒ (('a::finite×'b::finite)×'c::finite) update› where
‹assoc' = (Fst o Fst; (Fst o Snd; Snd))›
lemma assoc'_is_hom[simp]: ‹clinear assoc'›
by (auto simp: assoc'_def)
lemma assoc'_apply[simp]: ‹assoc' (a ⊗⇩u (b ⊗⇩u c)) = ((a ⊗⇩u b) ⊗⇩u c)›
by (auto simp: assoc'_def register_pair_apply Fst_def Snd_def comp_tensor_op)
lemma register_assoc[simp]: ‹register assoc›
unfolding assoc_def
by force
lemma register_assoc'[simp]: ‹register assoc'›
unfolding assoc'_def
by force
lemma pair_o_assoc[simp]:
assumes [simp]: ‹compatible F G› ‹compatible G H› ‹compatible F H›
shows ‹(F; (G; H)) ∘ assoc = ((F; G); H)›
proof (rule tensor_extensionality3')
show ‹register ((F; (G; H)) ∘ assoc)›
by simp
show ‹register ((F; G); H)›
by simp
show ‹((F; (G; H)) ∘ assoc) ((f ⊗⇩u g) ⊗⇩u h) = ((F; G); H) ((f ⊗⇩u g) ⊗⇩u h)› for f g h
by (simp add: register_pair_apply assoc_apply cblinfun_compose_assoc)
qed
lemma pair_o_assoc'[simp]:
assumes [simp]: ‹compatible F G› ‹compatible G H› ‹compatible F H›
shows ‹((F; G); H) ∘ assoc' = (F; (G; H))›
proof (rule tensor_extensionality3)
show ‹register (((F; G); H) ∘ assoc')›
by simp
show ‹register (F; (G; H))›
by simp
show ‹(((F; G); H) ∘ assoc') (f ⊗⇩u g ⊗⇩u h) = (F; (G; H)) (f ⊗⇩u g ⊗⇩u h)› for f g h
by (simp add: register_pair_apply assoc'_apply cblinfun_compose_assoc)
qed
lemma assoc'_o_assoc[simp]: ‹assoc' o assoc = id›
apply (rule tensor_extensionality3')
by auto
lemma assoc'_assoc[simp]: ‹assoc' (assoc x) = x›
by (simp add: pointfree_idE)
lemma assoc_o_assoc'[simp]: ‹assoc o assoc' = id›
apply (rule tensor_extensionality3)
by auto
lemma assoc_assoc'[simp]: ‹assoc (assoc' x) = x›
by (simp add: pointfree_idE)
lemma inv_assoc[simp]: ‹inv assoc = assoc'›
using assoc'_o_assoc assoc_o_assoc' inv_unique_comp by blast
lemma inv_assoc'[simp]: ‹inv assoc' = assoc›
by (simp add: inv_equality)
lemma [simp]: ‹bij assoc›
using assoc'_o_assoc assoc_o_assoc' o_bij by blast
lemma [simp]: ‹bij assoc'›
using assoc'_o_assoc assoc_o_assoc' o_bij by blast
subsection ‹Iso-registers›
definition ‹iso_register F ⟷ register F ∧ (∃G. register G ∧ F o G = id ∧ G o F = id)›
for F :: ‹_::finite update ⇒ _::finite update›
lemma iso_registerI:
assumes ‹register F› ‹register G› ‹F o G = id› ‹G o F = id›
shows ‹iso_register F›
using assms(1) assms(2) assms(3) assms(4) iso_register_def by blast
lemma iso_register_inv: ‹iso_register F ⟹ iso_register (inv F)›
by (metis inv_unique_comp iso_register_def)
lemma iso_register_inv_comp1: ‹iso_register F ⟹ inv F o F = id›
using inv_unique_comp iso_register_def by blast
lemma iso_register_inv_comp2: ‹iso_register F ⟹ F o inv F = id›
using inv_unique_comp iso_register_def by blast
lemma iso_register_id[simp]: ‹iso_register id›
by (simp add: iso_register_def)
lemma iso_register_is_register: ‹iso_register F ⟹ register F›
using iso_register_def by blast
lemma iso_register_comp[simp]:
assumes [simp]: ‹iso_register F› ‹iso_register G›
shows ‹iso_register (F o G)›
proof -
from assms obtain F' G' where [simp]: ‹register F'› ‹register G'› ‹F o F' = id› ‹F' o F = id›
‹G o G' = id› ‹G' o G = id›
by (meson iso_register_def)
show ?thesis
apply (rule iso_registerI[where G=‹G' o F'›])
apply (auto simp: register_tensor_is_register iso_register_is_register register_tensor_distrib)
apply (metis ‹F ∘ F' = id› ‹G ∘ G' = id› fcomp_assoc fcomp_comp id_fcomp)
by (metis (no_types, lifting) ‹F ∘ F' = id› ‹F' ∘ F = id› ‹G' ∘ G = id› fun.map_comp inj_iff inv_unique_comp o_inv_o_cancel)
qed
lemma iso_register_tensor_is_iso_register[simp]:
assumes [simp]: ‹iso_register F› ‹iso_register G›
shows ‹iso_register (F ⊗⇩r G)›
proof -
from assms obtain F' G' where [simp]: ‹register F'› ‹register G'› ‹F o F' = id› ‹F' o F = id›
‹G o G' = id› ‹G' o G = id›
by (meson iso_register_def)
show ?thesis
apply (rule iso_registerI[where G=‹F' ⊗⇩r G'›])
by (auto simp: register_tensor_is_register iso_register_is_register register_tensor_distrib)
qed
lemma iso_register_bij: ‹iso_register F ⟹ bij F›
using iso_register_def o_bij by auto
lemma inv_register_tensor[simp]:
assumes [simp]: ‹iso_register F› ‹iso_register G›
shows ‹inv (F ⊗⇩r G) = inv F ⊗⇩r inv G›
apply (auto intro!: inj_imp_inv_eq bij_is_inj iso_register_bij
simp: register_tensor_distrib[unfolded o_def, THEN fun_cong] iso_register_is_register
iso_register_inv bij_is_surj iso_register_bij surj_f_inv_f)
by (metis eq_id_iff register_tensor_id)
lemma iso_register_swap[simp]: ‹iso_register swap›
apply (rule iso_registerI[of _ swap])
by auto
lemma iso_register_assoc[simp]: ‹iso_register assoc›
apply (rule iso_registerI[of _ assoc'])
by auto
lemma iso_register_assoc'[simp]: ‹iso_register assoc'›
apply (rule iso_registerI[of _ assoc])
by auto
definition ‹equivalent_registers F G ⟷ (register F ∧ (∃I. iso_register I ∧ F o I = G))›
for F G :: ‹_::finite update ⇒ _::finite update›
lemma iso_register_equivalent_id[simp]: ‹equivalent_registers id F ⟷ iso_register F›
by (simp add: equivalent_registers_def)
lemma equivalent_registersI:
assumes ‹register F›
assumes ‹iso_register I›
assumes ‹F o I = G›
shows ‹equivalent_registers F G›
using assms unfolding equivalent_registers_def by blast
lemma equivalent_registers_register_left: ‹equivalent_registers F G ⟹ register F›
using equivalent_registers_def by auto
lemma equivalent_registers_register_right: ‹register G› if ‹equivalent_registers F G›
by (metis equivalent_registers_def iso_register_def register_comp that)
lemma equivalent_registers_sym:
assumes ‹equivalent_registers F G›
shows ‹equivalent_registers G F›
by (smt (verit) assms comp_id equivalent_registers_def equivalent_registers_register_right fun.map_comp iso_register_def)
lemma equivalent_registers_trans[trans]:
assumes ‹equivalent_registers F G› and ‹equivalent_registers G H›
shows ‹equivalent_registers F H›
proof -
from assms have [simp]: ‹register F› ‹register G›
by (auto simp: equivalent_registers_def)
from assms(1) obtain I where [simp]: ‹iso_register I› and ‹F o I = G›
using equivalent_registers_def by blast
from assms(2) obtain J where [simp]: ‹iso_register J› and ‹G o J = H›
using equivalent_registers_def by blast
have ‹register F›
by (auto simp: equivalent_registers_def)
moreover have ‹iso_register (I o J)›
using ‹iso_register I› ‹iso_register J› iso_register_comp by blast
moreover have ‹F o (I o J) = H›
by (simp add: ‹F ∘ I = G› ‹G ∘ J = H› o_assoc)
ultimately show ?thesis
by (rule equivalent_registersI)
qed
lemma equivalent_registers_assoc[simp]:
assumes [simp]: ‹compatible F G› ‹compatible F H› ‹compatible G H›
shows ‹equivalent_registers (F;(G;H)) ((F;G);H)›
apply (rule equivalent_registersI[where I=assoc])
by auto
lemma equivalent_registers_pair_right:
assumes [simp]: ‹compatible F G›
assumes eq: ‹equivalent_registers G H›
shows ‹equivalent_registers (F;G) (F;H)›
proof -
from eq obtain I where [simp]: ‹iso_register I› and ‹G o I = H›
by (metis equivalent_registers_def)
then have *: ‹(F;G) ∘ (id ⊗⇩r I) = (F;H)›
by (auto intro!: tensor_extensionality register_comp register_preregister register_tensor_is_register
simp: register_pair_apply iso_register_is_register)
show ?thesis
apply (rule equivalent_registersI[where I=‹id ⊗⇩r I›])
using * by (auto intro!: iso_register_tensor_is_iso_register)
qed
lemma equivalent_registers_pair_left:
assumes [simp]: ‹compatible F G›
assumes eq: ‹equivalent_registers F H›
shows ‹equivalent_registers (F;G) (H;G)›
proof -
from eq obtain I where [simp]: ‹iso_register I› and ‹F o I = H›
by (metis equivalent_registers_def)
then have *: ‹(F;G) ∘ (I ⊗⇩r id) = (H;G)›
by (auto intro!: tensor_extensionality register_comp register_preregister register_tensor_is_register
simp: register_pair_apply iso_register_is_register)
show ?thesis
apply (rule equivalent_registersI[where I=‹I ⊗⇩r id›])
using * by (auto intro!: iso_register_tensor_is_iso_register)
qed
lemma equivalent_registers_comp:
assumes ‹register H›
assumes ‹equivalent_registers F G›
shows ‹equivalent_registers (H o F) (H o G)›
by (metis (no_types, lifting) assms(1) assms(2) comp_assoc equivalent_registers_def register_comp)
subsection ‹Compatibility simplification›
text ‹The simproc ‹compatibility_warn› produces helpful warnings for subgoals of the form
\<^term>‹compatible x y› that are probably unsolvable due to missing declarations of
variable compatibility facts. Same for subgoals of the form \<^term>‹register x›.›
simproc_setup "compatibility_warn" ("compatible x y" | "register x") = ‹
let val thy_string = Markup.markup (Theory.get_markup \<^theory>) (Context.theory_base_name \<^theory>)
in
fn m => fn ctxt => fn ct => let
val (x,y) = case Thm.term_of ct of
Const(\<^const_name>‹compatible›,_ ) $ x $ y => (x, SOME y)
| Const(\<^const_name>‹register›,_ ) $ x => (x, NONE)
val str : string lazy = Lazy.lazy (fn () => Syntax.string_of_term ctxt (Thm.term_of ct))
fun w msg = warning (msg ^ "\n(Disable these warnings with: using [[simproc del: "^thy_string^".compatibility_warn]])")
val _ = case (x,y) of
(Free(n,T), SOME (Free(n',T'))) =>
if String.isPrefix ":" n orelse String.isPrefix ":" n' then
w ("Simplification subgoal " ^ Lazy.force str ^ " contains a bound variable.\n" ^
"Try to add some assumptions that makes this goal solvable by the simplifier")
else if n=n' then (if T=T' then ()
else w ("In simplification subgoal " ^ Lazy.force str ^
", variables have same name and different types.\n" ^
"Probably something is wrong."))
else w ("Simplification subgoal " ^ Lazy.force str ^
" occurred but cannot be solved.\n" ^
"Please add assumption/fact [simp]: ‹" ^ Lazy.force str ^
"› somewhere.")
| (Free(n,T), NONE) =>
if String.isPrefix ":" n then
w ("Simplification subgoal '" ^ Lazy.force str ^ "' contains a bound variable.\n" ^
"Try to add some assumptions that makes this goal solvable by the simplifier")
else w ("Simplification subgoal " ^ Lazy.force str ^ " occurred but cannot be solved.\n" ^
"Please add assumption/fact [simp]: ‹" ^ Lazy.force str ^ "› somewhere.")
| _ => ()
in NONE end
end›
named_theorems register_attribute_rule_immediate
named_theorems register_attribute_rule
lemmas [register_attribute_rule] = conjunct1 conjunct2 iso_register_is_register iso_register_is_register[OF iso_register_inv]
lemmas [register_attribute_rule_immediate] = compatible_sym compatible_register1 compatible_register2
asm_rl[of ‹compatible _ _›] asm_rl[of ‹iso_register _›] asm_rl[of ‹register _›] iso_register_inv
text ‹The following declares an attribute ‹[register]›. When the attribute is applied to a fact
of the form \<^term>‹register F›, \<^term>‹iso_register F›, \<^term>‹compatible F G› or a conjunction of these,
then those facts are added to the simplifier together with some derived theorems
(e.g., \<^term>‹compatible F G› also adds \<^term>‹register F›).
In theory ‹Laws_Complement›, support for \<^term>‹is_unit_register F› and \<^term>‹complements F G› is
added to this attribute.›
setup ‹
let
fun add thm results =
Net.insert_term (K true) (Thm.concl_of thm, thm) results
handle Net.INSERT => results
fun try_rule f thm rule state = case SOME (rule OF [thm]) handle THM _ => NONE of
NONE => state | SOME th => f th state
fun collect (rules,rules_immediate) thm results =
results |> fold (try_rule add thm) rules_immediate |> fold (try_rule (collect (rules,rules_immediate)) thm) rules
fun declare thm context = let
val ctxt = Context.proof_of context
val rules = Named_Theorems.get ctxt @{named_theorems register_attribute_rule}
val rules_immediate = Named_Theorems.get ctxt @{named_theorems register_attribute_rule_immediate}
val thms = collect (rules,rules_immediate) thm Net.empty |> Net.entries
in Simplifier.map_ss (fn ctxt => ctxt addsimps thms) context end
in
Attrib.setup \<^binding>‹register›
(Scan.succeed (Thm.declaration_attribute declare))
"Add register-related rules to the simplifier"
end
›
subsection ‹Notation›
no_notation cblinfun_compose (infixl "*⇩u" 55)
no_notation tensor_op (infixr "⊗⇩u" 70)
bundle register_notation begin
notation register_tensor (infixr "⊗⇩r" 70)
notation register_pair ("'(_;_')")
end
bundle no_register_notation begin
no_notation register_tensor (infixr "⊗⇩r" 70)
no_notation register_pair ("'(_;_')")
end
end