diff --git a/thys/Registers/Axioms_Complement_Quantum.thy b/thys/Registers/Axioms_Complement_Quantum.thy --- a/thys/Registers/Axioms_Complement_Quantum.thy +++ b/thys/Registers/Axioms_Complement_Quantum.thy @@ -1,711 +1,711 @@ section \Quantum instantiation of complements\ theory Axioms_Complement_Quantum imports Laws_Quantum Finite_Tensor_Product Quantum_Extra begin no_notation m_inv ("inv\ _" [81] 80) no_notation Lattice.join (infixl "\\" 65) typedef ('a::finite,'b::finite) complement_domain = \{..< if CARD('b) div CARD('a) \ 0 then CARD('b) div CARD('a) else 1}\ by auto instance complement_domain :: (finite, finite) finite proof intro_classes have \inj Rep_complement_domain\ by (simp add: Rep_complement_domain_inject inj_on_def) moreover have \finite (range Rep_complement_domain)\ by (metis finite_lessThan type_definition.Rep_range type_definition_complement_domain) ultimately show \finite (UNIV :: ('a,'b) complement_domain set)\ - using Missing_Permutations.inj_on_finite by blast + using finite_image_iff by blast qed lemma CARD_complement_domain: assumes \CARD('b::finite) = n * CARD('a::finite)\ shows \CARD(('a,'b) complement_domain) = n\ proof - from assms have \n > 0\ by (metis zero_less_card_finite zero_less_mult_pos2) have *: \inj Rep_complement_domain\ by (simp add: Rep_complement_domain_inject inj_on_def) moreover have \card (range (Rep_complement_domain :: ('a,'b) complement_domain \ _)) = n\ apply (subst type_definition.Rep_range[OF type_definition_complement_domain]) using assms \n > 0\ by simp ultimately show ?thesis by (metis card_image) qed lemma register_decomposition: fixes \ :: \'a::finite update \ 'b::finite update\ assumes [simp]: \register \\ shows \\U :: ('a \ ('a, 'b) complement_domain) ell2 \\<^sub>C\<^sub>L 'b ell2. unitary U \ (\\. \ \ = sandwich U (\ \\<^sub>o id_cblinfun))\ \ \Proof based on @{cite daws21unitalanswer}\ proof - note [[simproc del: compatibility_warn]] fix \0 :: 'a have [simp]: \clinear \\ by simp define P where \P i = Proj (ccspan {ket i})\ for i :: 'a have P_butter: \P i = selfbutterket i\ for i by (simp add: P_def butterfly_eq_proj) define P' where \P' i = \ (P i)\ for i :: 'a have proj_P': \is_Proj (P' i)\ for i by (simp add: P_def P'_def register_projector) have \(\i\UNIV. P i) = id_cblinfun\ using sum_butterfly_ket P_butter by simp then have sumP'id: \(\i\UNIV. P' i) = id_cblinfun\ unfolding P'_def apply (subst complex_vector.linear_sum[OF \clinear \\, symmetric]) by auto define S where \S i = P' i *\<^sub>S \\ for i :: 'a have P'id: \P' i *\<^sub>V \ = \\ if \\ \ space_as_set (S i)\ for i \ using S_def that proj_P' by (metis cblinfun_fixes_range is_Proj_algebraic) obtain B0 where finiteB0: \finite (B0 i)\ and cspanB0: \cspan (B0 i) = space_as_set (S i)\ for i apply atomize_elim apply (simp flip: all_conj_distrib) apply (rule choice) by (meson cfinite_dim_finite_subspace_basis csubspace_space_as_set) obtain B where orthoB: \is_ortho_set (B i)\ and normalB: \\b. b \ B i \ norm b = 1\ and cspanB: \cspan (B i) = cspan (B0 i)\ and finiteB: \finite (B i)\ for i apply atomize_elim apply (simp flip: all_conj_distrib) apply (rule choice) using orthonormal_basis_of_cspan[OF finiteB0] by blast from cspanB cspanB0 have cspanB: \cspan (B i) = space_as_set (S i)\ for i by simp then have ccspanB: \ccspan (B i) = S i\ for i by (metis ccspan.rep_eq closure_finite_cspan finiteB space_as_set_inject) from orthoB have indepB: \cindependent (B i)\ for i by (simp add: Complex_Inner_Product.is_ortho_set_cindependent) have orthoBiBj: \is_orthogonal x y\ if \x \ B i\ and \y \ B j\ and \i \ j\ for x y i j proof - from \x \ B i\ obtain x' where x: \x = P' i *\<^sub>V x'\ by (metis S_def cblinfun_fixes_range complex_vector.span_base cspanB is_Proj_idempotent proj_P') from \y \ B j\ obtain y' where y: \y = P' j *\<^sub>V y'\ by (metis S_def cblinfun_fixes_range complex_vector.span_base cspanB is_Proj_idempotent proj_P') have \cinner x y = cinner (P' i *\<^sub>V x') (P' j *\<^sub>V y')\ using x y by simp also have \\ = cinner (P' j *\<^sub>V P' i *\<^sub>V x') y'\ by (metis cinner_adj_left is_Proj_algebraic proj_P') also have \\ = cinner (\ (P j o\<^sub>C\<^sub>L P i) *\<^sub>V x') y'\ unfolding P'_def register_mult[OF \register \\, symmetric] by simp also have \\ = cinner (\ (selfbutterket j o\<^sub>C\<^sub>L selfbutterket i) *\<^sub>V x') y'\ unfolding P_butter by simp also have \\ = cinner (\ 0 *\<^sub>V x') y'\ by (metis butterfly_comp_butterfly complex_vector.scale_eq_0_iff orthogonal_ket that(3)) also have \\ = 0\ by (simp add: complex_vector.linear_0) finally show ?thesis by - qed define B' where \B' = (\i\UNIV. B i)\ have P'B: \P' i = Proj (ccspan (B i))\ for i unfolding ccspanB S_def using proj_P' Proj_on_own_range'[symmetric] is_Proj_algebraic by blast have \(\i\UNIV. P' i) = Proj (ccspan B')\ proof (unfold B'_def, use finite[of UNIV] in induction) case empty show ?case by auto next case (insert j M) have \(\i\insert j M. P' i) = P' j + (\i\M. P' i)\ by (meson insert.hyps(1) insert.hyps(2) sum.insert) also have \\ = Proj (ccspan (B j)) + Proj (ccspan (\i\M. B i))\ unfolding P'B insert.IH[symmetric] by simp also have \\ = Proj (ccspan (B j \ (\i\M. B i)))\ apply (rule Proj_orthog_ccspan_union[symmetric]) using orthoBiBj insert.hyps(2) by auto also have \\ = Proj (ccspan (\i\insert j M. B i))\ by auto finally show ?case by simp qed with sumP'id have ccspanB': \ccspan B' = \\ by (metis Proj_range cblinfun_image_id) hence cspanB': \cspan B' = UNIV\ by (metis B'_def finiteB ccspan.rep_eq finite_UN_I finite_class.finite_UNIV closure_finite_cspan top_ccsubspace.rep_eq) from orthoBiBj orthoB have orthoB': \is_ortho_set B'\ unfolding B'_def is_ortho_set_def by blast then have indepB': \cindependent B'\ using is_ortho_set_cindependent by blast have cardB': \card B' = CARD('b)\ apply (subst complex_vector.dim_span_eq_card_independent[symmetric]) apply (rule indepB') apply (subst cspanB') using cdim_UNIV_ell2 by auto from orthoBiBj orthoB have Bdisj: \B i \ B j = {}\ if \i \ j\ for i j unfolding is_ortho_set_def apply auto by (metis cinner_eq_zero_iff that) have cardBsame: \card (B i) = card (B j)\ for i j proof - define Si_to_Sj where \Si_to_Sj i j \ = \ (butterket j i) *\<^sub>V \\ for i j \ have S2S2S: \Si_to_Sj j i (Si_to_Sj i j \) = \\ if \\ \ space_as_set (S i)\ for i j \ using that P'id by (simp add: Si_to_Sj_def cblinfun_apply_cblinfun_compose[symmetric] register_mult P_butter P'_def) also have lin[simp]: \clinear (Si_to_Sj i j)\ for i j unfolding Si_to_Sj_def by simp have S2S: \Si_to_Sj i j x \ space_as_set (S j)\ for i j x proof - have \Si_to_Sj i j x = P' j *\<^sub>V Si_to_Sj i j x\ by (simp add: Si_to_Sj_def cblinfun_apply_cblinfun_compose[symmetric] register_mult P_butter P'_def) also have \P' j *\<^sub>V Si_to_Sj i j x \ space_as_set (S j)\ by (simp add: S_def) finally show ?thesis by - qed have bij: \bij_betw (Si_to_Sj i j) (space_as_set (S i)) (space_as_set (S j))\ apply (rule bij_betwI[where g=\Si_to_Sj j i\]) using S2S S2S2S by (auto intro!: funcsetI) have \cdim (space_as_set (S i)) = cdim (space_as_set (S j))\ using lin apply (rule isomorphic_equal_cdim[where f=\Si_to_Sj i j\]) using bij apply (auto simp: bij_betw_def) by (metis complex_vector.span_span cspanB) then show ?thesis by (metis complex_vector.dim_span_eq_card_independent cspanB indepB) qed have CARD'b: \CARD('b) = card (B \0) * CARD('a)\ proof - have \CARD('b) = card B'\ using cardB' by simp also have \\ = (\i\UNIV. card (B i))\ unfolding B'_def apply (rule card_UN_disjoint) using finiteB Bdisj by auto also have \\ = (\(i::'a)\UNIV. card (B \0))\ using cardBsame by metis also have \\ = card (B \0) * CARD('a)\ by auto finally show ?thesis by - qed obtain f where bij_f: \bij_betw f (UNIV::('a,'b) complement_domain set) (B \0)\ apply atomize_elim apply (rule finite_same_card_bij) using finiteB CARD_complement_domain[OF CARD'b] by auto define u where \u = (\(\,\). \ (butterket \ \0) *\<^sub>V f \)\ for \ :: 'a and \ :: \('a,'b) complement_domain\ obtain U where Uapply: \U *\<^sub>V ket \\ = u \\\ for \\ apply atomize_elim apply (rule exI[of _ \cblinfun_extension (range ket) (\k. u (inv ket k))\]) apply (subst cblinfun_extension_apply) apply (rule cblinfun_extension_exists_finite_dim) by (auto simp add: inj_ket cindependent_ket) define eqa where \eqa a b = (if a = b then 1 else 0 :: complex)\ for a b :: 'a define eqc where \eqc a b = (if a = b then 1 else 0 :: complex)\ for a b :: \('a,'b) complement_domain\ define eqac where \eqac a b = (if a = b then 1 else 0 :: complex)\ for a b :: \'a * ('a,'b) complement_domain\ have \cinner (U *\<^sub>V ket \\) (U *\<^sub>V ket \'\') = eqac \\ \'\'\ for \\ \'\' proof - obtain \ \ \' \' where \\: \\\ = (\,\)\ and \'\': \\'\' = (\',\')\ apply atomize_elim by auto have \cinner (U *\<^sub>V ket (\,\)) (U *\<^sub>V ket (\', \')) = cinner (\ (butterket \ \0) *\<^sub>V f \) (\ (butterket \' \0) *\<^sub>V f \')\ unfolding Uapply u_def by simp also have \\ = cinner ((\ (butterket \' \0))* *\<^sub>V \ (butterket \ \0) *\<^sub>V f \) (f \')\ by (simp add: cinner_adj_left) also have \\ = cinner (\ (butterket \' \0 *) *\<^sub>V \ (butterket \ \0) *\<^sub>V f \) (f \')\ by (metis (no_types, lifting) assms register_def) also have \\ = cinner (\ (butterket \0 \' o\<^sub>C\<^sub>L butterket \ \0) *\<^sub>V f \) (f \')\ by (simp add: register_mult cblinfun_apply_cblinfun_compose[symmetric]) also have \\ = cinner (\ (eqa \' \ *\<^sub>C selfbutterket \0) *\<^sub>V f \) (f \')\ apply simp by (metis eqa_def cinner_ket) also have \\ = eqa \' \ * cinner (\ (selfbutterket \0) *\<^sub>V f \) (f \')\ by (smt (verit, ccfv_threshold) \clinear \\ eqa_def cblinfun.scaleC_left cinner_commute cinner_scaleC_left cinner_zero_right complex_cnj_one complex_vector.linear_scale) also have \\ = eqa \' \ * cinner (P' \0 *\<^sub>V f \) (f \')\ using P_butter P'_def by simp also have \\ = eqa \' \ * cinner (f \) (f \')\ apply (subst P'id) apply (metis bij_betw_imp_surj_on bij_f complex_vector.span_base cspanB rangeI) by simp also have \\ = eqa \' \ * eqc \ \'\ using bij_f orthoB normalB unfolding is_ortho_set_def eqc_def apply auto apply (metis bij_betw_imp_surj_on cnorm_eq_1 rangeI) by (smt (z3) bij_betw_iff_bijections iso_tuple_UNIV_I) finally show ?thesis by (simp add: eqa_def eqac_def eqc_def \'\' \\) qed then have \isometry U\ apply (rule_tac orthogonal_on_basis_is_isometry[where B=\range ket\]) using eqac_def by auto have \U* o\<^sub>C\<^sub>L \ (butterket \ \) o\<^sub>C\<^sub>L U = butterket \ \ \\<^sub>o id_cblinfun\ for \ \ proof (rule equal_ket, rename_tac \1\) fix \1\ obtain \1 :: 'a and \ :: \('a,'b) complement_domain\ where \1\: \\1\ = (\1,\)\ apply atomize_elim by auto have \(U* o\<^sub>C\<^sub>L \ (butterket \ \) o\<^sub>C\<^sub>L U) *\<^sub>V ket \1\ = U* *\<^sub>V \ (butterket \ \) *\<^sub>V \ (butterket \1 \0) *\<^sub>V f \\ unfolding cblinfun_apply_cblinfun_compose \1\ Uapply u_def by simp also have \\ = U* *\<^sub>V \ (butterket \ \ o\<^sub>C\<^sub>L butterket \1 \0) *\<^sub>V f \\ by (metis (no_types, lifting) assms butterfly_comp_butterfly lift_cblinfun_comp(4) register_mult) also have \\ = U* *\<^sub>V \ (eqa \ \1 *\<^sub>C butterket \ \0) *\<^sub>V f \\ by (simp add: eqa_def cinner_ket) also have \\ = eqa \ \1 *\<^sub>C U* *\<^sub>V \ (butterket \ \0) *\<^sub>V f \\ by (simp add: complex_vector.linear_scale) also have \\ = eqa \ \1 *\<^sub>C U* *\<^sub>V U *\<^sub>V ket (\, \)\ unfolding Uapply u_def by simp also from \isometry U\ have \\ = eqa \ \1 *\<^sub>C ket (\, \)\ unfolding cblinfun_apply_cblinfun_compose[symmetric] by simp also have \\ = (butterket \ \ *\<^sub>V ket \1) \\<^sub>s ket \\ by (simp add: eqa_def tensor_ell2_scaleC1) also have \\ = (butterket \ \ \\<^sub>o id_cblinfun) *\<^sub>V ket \1\\ by (simp add: \1\ tensor_op_ket) finally show \(U* o\<^sub>C\<^sub>L \ (butterket \ \) o\<^sub>C\<^sub>L U) *\<^sub>V ket \1\ = (butterket \ \ \\<^sub>o id_cblinfun) *\<^sub>V ket \1\\ by - qed then have 1: \U* o\<^sub>C\<^sub>L \ \ o\<^sub>C\<^sub>L U = \ \\<^sub>o id_cblinfun\ for \ apply (rule_tac clinear_eq_butterfly_ketI[THEN fun_cong, where x=\]) by (auto intro!: clinearI simp add: bounded_cbilinear.add_left bounded_cbilinear_cblinfun_compose complex_vector.linear_add complex_vector.linear_scale) have \unitary U\ proof - have \\ (butterket \ \1) *\<^sub>S \ \ U *\<^sub>S \\ for \ \1 proof - have *: \\ (butterket \ \0) *\<^sub>V b \ space_as_set (U *\<^sub>S \)\ if \b \ B \0\ for b apply (subst asm_rl[of \\ (butterket \ \0) *\<^sub>V b = u (\, inv f b)\]) apply (simp add: u_def, metis bij_betw_inv_into_right bij_f that) by (metis Uapply cblinfun_apply_in_image) have \\ (butterket \ \1) *\<^sub>S \ = \ (butterket \ \0) *\<^sub>S \ (butterket \0 \0) *\<^sub>S \ (butterket \0 \1) *\<^sub>S \\ unfolding cblinfun_compose_image[symmetric] register_mult[OF assms] by simp also have \\ \ \ (butterket \ \0) *\<^sub>S \ (butterket \0 \0) *\<^sub>S \\ by (meson cblinfun_image_mono top_greatest) also have \\ = \ (butterket \ \0) *\<^sub>S S \0\ by (simp add: S_def P'_def P_butter) also have \\ = \ (butterket \ \0) *\<^sub>S ccspan (B \0)\ by (simp add: ccspanB) also have \\ = ccspan (\ (butterket \ \0) ` B \0)\ by (meson cblinfun_image_ccspan) also have \\ \ U *\<^sub>S \\ by (rule ccspan_leqI, use * in auto) finally show ?thesis by - qed moreover have \\ id_cblinfun *\<^sub>S \ \ (SUP \\UNIV. \ (selfbutterket \) *\<^sub>S \)\ unfolding sum_butterfly_ket[symmetric] apply (subst complex_vector.linear_sum, simp) by (rule cblinfun_sum_image_distr) ultimately have \\ id_cblinfun *\<^sub>S \ \ U *\<^sub>S \\ apply auto by (meson SUP_le_iff order.trans) then have \U *\<^sub>S \ = \\ apply auto using top.extremum_unique by blast with \isometry U\ show \unitary U\ by (rule surj_isometry_is_unitary) qed have \\ \ = U o\<^sub>C\<^sub>L (\ \\<^sub>o id_cblinfun) o\<^sub>C\<^sub>L U*\ for \ proof - from \unitary U\ have \\ \ = (U o\<^sub>C\<^sub>L U*) o\<^sub>C\<^sub>L \ \ o\<^sub>C\<^sub>L (U o\<^sub>C\<^sub>L U*)\ by simp also have \\ = U o\<^sub>C\<^sub>L (U* o\<^sub>C\<^sub>L \ \ o\<^sub>C\<^sub>L U) o\<^sub>C\<^sub>L U*\ by (simp add: cblinfun_assoc_left) also have \\ = U o\<^sub>C\<^sub>L (\ \\<^sub>o id_cblinfun) o\<^sub>C\<^sub>L U*\ using 1 by simp finally show ?thesis by - qed with \unitary U\ show ?thesis by (auto simp: sandwich_def) qed lemma register_decomposition_converse: assumes \unitary U\ shows \register (\x. sandwich U (id_cblinfun \\<^sub>o x))\ using _ unitary_sandwich_register apply (rule register_comp[unfolded o_def]) using assms by auto lemma register_inj: \inj F\ if \register F\ proof - obtain U :: \('a \ ('a, 'b) complement_domain) ell2 \\<^sub>C\<^sub>L 'b ell2\ where \unitary U\ and F: \F a = sandwich U (a \\<^sub>o id_cblinfun)\ for a apply atomize_elim using \register F\ by (rule register_decomposition) have \inj (sandwich U)\ by (smt (verit, best) \unitary U\ cblinfun_assoc_left inj_onI sandwich_def cblinfun_compose_id_right cblinfun_compose_id_left unitary_def) moreover have \inj (\a::'a::finite ell2 \\<^sub>C\<^sub>L _. a \\<^sub>o id_cblinfun)\ by (rule inj_tensor_left, simp) ultimately show \inj F\ unfolding F by (smt (z3) inj_def) qed lemma iso_register_decomposition: assumes [simp]: \iso_register F\ shows \\U. unitary U \ F = sandwich U\ proof - have [simp]: \register F\ using assms iso_register_is_register by blast let ?ida = \id_cblinfun :: ('a, 'b) complement_domain ell2 \\<^sub>C\<^sub>L _\ from register_decomposition[OF \register F\] obtain V :: \('a \ ('a, 'b) complement_domain) ell2 \\<^sub>C\<^sub>L 'b ell2\ where \unitary V\ and FV: \F \ = sandwich V (\ \\<^sub>o ?ida)\ for \ by auto have \surj F\ by (meson assms iso_register_inv_comp2 surj_iff) have surj_tensor: \surj (\a::'a ell2 \\<^sub>C\<^sub>L 'a ell2. a \\<^sub>o ?ida)\ apply (rule surj_from_comp[where g=\sandwich V\]) using \surj F\ apply (auto simp: FV) by (meson \unitary V\ register_inj unitary_sandwich_register) then obtain a :: \'a ell2 \\<^sub>C\<^sub>L _\ where a: \a \\<^sub>o ?ida = selfbutterket undefined \\<^sub>o selfbutterket undefined\ by (smt (verit, best) surjD) then have \a \ 0\ apply auto by (metis butterfly_apply cblinfun.zero_left complex_vector.scale_eq_0_iff ket_nonzero orthogonal_ket) obtain \ where \: \?ida = \ *\<^sub>C selfbutterket undefined\ apply atomize_elim using a \a \ 0\ by (rule tensor_op_almost_injective) then have \?ida (ket undefined) = \ *\<^sub>C (selfbutterket undefined *\<^sub>V ket undefined)\ by (simp add: \id_cblinfun = \ *\<^sub>C selfbutterket undefined\ scaleC_cblinfun.rep_eq) then have \ket undefined = \ *\<^sub>C ket undefined\ by (metis butterfly_apply cinner_scaleC_right id_cblinfun_apply cinner_ket_same mult.right_neutral scaleC_one) then have \\ = 1\ by (smt (z3) \ butterfly_apply butterfly_scaleC_left cblinfun_id_cblinfun_apply complex_vector.scale_cancel_right cinner_ket_same ket_nonzero) define T U where \T = CBlinfun (\\. \ \\<^sub>s ket undefined)\ and \U = V o\<^sub>C\<^sub>L T\ have T: \T \ = \ \\<^sub>s ket undefined\ for \ unfolding T_def apply (subst bounded_clinear_CBlinfun_apply) by (auto intro!: bounded_clinear_finite_dim clinear_tensor_ell22) have sandwich_T: \sandwich T a = a \\<^sub>o ?ida\ for a apply (rule fun_cong[where x=a]) apply (rule clinear_eq_butterfly_ketI) apply auto - by (metis (no_types, hide_lams) Misc.sandwich_def T \ \\ = 1\ adj_cblinfun_compose butterfly_adjoint cblinfun_comp_butterfly scaleC_one tensor_butterfly) + by (metis (no_types, opaque_lifting) Misc.sandwich_def T \ \\ = 1\ adj_cblinfun_compose butterfly_adjoint cblinfun_comp_butterfly scaleC_one tensor_butterfly) have \F (butterfly x y) = V o\<^sub>C\<^sub>L (butterfly x y \\<^sub>o ?ida) o\<^sub>C\<^sub>L V*\ for x y by (simp add: Misc.sandwich_def FV) also have \\ x y = V o\<^sub>C\<^sub>L (butterfly (T x) (T y)) o\<^sub>C\<^sub>L V*\ for x y by (simp add: T \ \\ = 1\) also have \\ x y = U o\<^sub>C\<^sub>L (butterfly x y) o\<^sub>C\<^sub>L U*\ for x y by (simp add: U_def butterfly_comp_cblinfun cblinfun_comp_butterfly) finally have F_rep: \F a = U o\<^sub>C\<^sub>L a o\<^sub>C\<^sub>L U*\ for a apply (rule_tac fun_cong[where x=a]) apply (rule_tac clinear_eq_butterfly_ketI) apply auto by (metis (no_types, lifting) cblinfun_apply_clinear clinear_iff sandwich_apply) have \isometry T\ apply (rule orthogonal_on_basis_is_isometry[where B=\range ket\]) by (auto simp: T) moreover have \T *\<^sub>S \ = \\ proof - have 1: \\ \\<^sub>s \ \ range ((*\<^sub>V) T)\ for \ \ proof - have \T *\<^sub>V (cinner (ket undefined) \ *\<^sub>C \) = \ \\<^sub>s (cinner (ket undefined) \ *\<^sub>C ket undefined)\ by (simp add: T tensor_ell2_scaleC2) also have \\ = \ \\<^sub>s (selfbutterket undefined *\<^sub>V \)\ by simp also have \\ = \ \\<^sub>s (?ida *\<^sub>V \)\ by (simp add: \ \\ = 1\) also have \\ = \ \\<^sub>s \\ by simp finally show ?thesis by (metis range_eqI) qed have \\ \ ccspan {ket x | x. True}\ by (simp add: full_SetCompr_eq) also have \\ \ ccspan {\ \\<^sub>s \ | \ \. True}\ apply (rule ccspan_mono) by (auto simp flip: tensor_ell2_ket) also from 1 have \\ \ ccspan (range ((*\<^sub>V) T))\ by (auto intro!: ccspan_mono) also have \\ = T *\<^sub>S \\ - by (metis (mono_tags, hide_lams) calculation cblinfun_image_ccspan cblinfun_image_mono eq_iff top_greatest) + by (metis (mono_tags, opaque_lifting) calculation cblinfun_image_ccspan cblinfun_image_mono eq_iff top_greatest) finally show \T *\<^sub>S \ = \\ using top.extremum_uniqueI by blast qed ultimately have \unitary T\ by (rule surj_isometry_is_unitary) then have \unitary U\ by (simp add: U_def \unitary V\) from F_rep \unitary U\ show ?thesis by (auto simp: sandwich_def[abs_def]) qed lemma complement_exists: fixes F :: \'a::finite update \ 'b::finite update\ assumes \register F\ shows \\G :: ('a, 'b) complement_domain update \ 'b update. compatible F G \ iso_register (F;G)\ proof - note [[simproc del: Laws_Quantum.compatibility_warn]] obtain U :: \('a \ ('a, 'b) complement_domain) ell2 \\<^sub>C\<^sub>L 'b ell2\ where [simp]: "unitary U" and F: \F a = sandwich U (a \\<^sub>o id_cblinfun)\ for a apply atomize_elim using assms by (rule register_decomposition) define G :: \(('a, 'b) complement_domain) update \ 'b update\ where \G b = sandwich U (id_cblinfun \\<^sub>o b)\ for b have [simp]: \register G\ unfolding G_def apply (rule register_decomposition_converse) by simp have \F a o\<^sub>C\<^sub>L G b = G b o\<^sub>C\<^sub>L F a\ for a b proof - have \F a o\<^sub>C\<^sub>L G b = sandwich U (a \\<^sub>o b)\ apply (auto simp: F G_def sandwich_def) by (metis (no_types, lifting) \unitary U\ isometryD cblinfun_assoc_left(1) comp_tensor_op cblinfun_compose_id_right cblinfun_compose_id_left unitary_isometry) moreover have \G b o\<^sub>C\<^sub>L F a = sandwich U (a \\<^sub>o b)\ apply (auto simp: F G_def sandwich_def) by (metis (no_types, lifting) \unitary U\ isometryD cblinfun_assoc_left(1) comp_tensor_op cblinfun_compose_id_right cblinfun_compose_id_left unitary_isometry) ultimately show ?thesis by simp qed then have [simp]: \compatible F G\ by (auto simp: compatible_def \register F\ \register G\) moreover have \iso_register (F;G)\ proof - have \(F;G) (a \\<^sub>o b) = sandwich U (a \\<^sub>o b)\ for a b apply (auto simp: register_pair_apply F G_def sandwich_def) by (metis (no_types, lifting) \unitary U\ isometryD cblinfun_assoc_left(1) comp_tensor_op cblinfun_compose_id_right cblinfun_compose_id_left unitary_isometry) then have FG: \(F;G) = sandwich U\ apply (rule tensor_extensionality[rotated -1]) by (simp_all add: bounded_cbilinear.add_left bounded_cbilinear_cblinfun_compose bounded_cbilinear.add_right clinearI) define I where \I = sandwich (U*)\ for x have [simp]: \register I\ by (simp add: I_def unitary_sandwich_register) have \I o (F;G) = id\ and FGI: \(F;G) o I = id\ apply (auto intro!:ext simp: I_def[abs_def] FG sandwich_def) - apply (metis (no_types, hide_lams) \unitary U\ isometryD cblinfun_assoc_left(1) cblinfun_compose_id_right cblinfun_compose_id_left unitary_isometry) + apply (metis (no_types, opaque_lifting) \unitary U\ isometryD cblinfun_assoc_left(1) cblinfun_compose_id_right cblinfun_compose_id_left unitary_isometry) by (metis (no_types, lifting) \unitary U\ cblinfun_assoc_left(1) cblinfun_compose_id_left cblinfun_compose_id_right unitaryD2) then show \iso_register (F;G)\ by (auto intro!: iso_registerI) qed ultimately show ?thesis apply (rule_tac exI[of _ G]) by (auto) qed definition \commutant F = {x. \y\F. x o\<^sub>C\<^sub>L y = y o\<^sub>C\<^sub>L x}\ lemma commutant_exchange: fixes F :: \'a::finite update \ 'b::finite update\ assumes \iso_register F\ shows \commutant (F ` X) = F ` commutant X\ proof (rule Set.set_eqI) fix x :: \'b update\ from assms obtain G where \F o G = id\ and \G o F = id\ and [simp]: \register G\ using iso_register_def by blast from assms have [simp]: \register F\ using iso_register_def by blast have \x \ commutant (F ` X) \ (\y \ F ` X. x o\<^sub>C\<^sub>L y = y o\<^sub>C\<^sub>L x)\ by (simp add: commutant_def) also have \\ \ (\y \ F ` X. G x o\<^sub>C\<^sub>L G y = G y o\<^sub>C\<^sub>L G x)\ - by (metis (no_types, hide_lams) \F \ G = id\ \G o F = id\ \register G\ comp_def eq_id_iff register_def) + by (metis (no_types, opaque_lifting) \F \ G = id\ \G o F = id\ \register G\ comp_def eq_id_iff register_def) also have \\ \ (\y \ X. G x o\<^sub>C\<^sub>L y = y o\<^sub>C\<^sub>L G x)\ by (simp add: \G \ F = id\ pointfree_idE) also have \\ \ G x \ commutant X\ by (simp add: commutant_def) also have \\ \ x \ F ` commutant X\ - by (metis (no_types, hide_lams) \G \ F = id\ \F \ G = id\ image_iff pointfree_idE) + by (metis (no_types, opaque_lifting) \G \ F = id\ \F \ G = id\ image_iff pointfree_idE) finally show \x \ commutant (F ` X) \ x \ F ` commutant X\ by - qed lemma commutant_tensor1: \commutant (range (\a. a \\<^sub>o id_cblinfun)) = range (\b. id_cblinfun \\<^sub>o b)\ proof (rule Set.set_eqI, rule iffI) fix x :: \('a \ 'b) ell2 \\<^sub>C\<^sub>L ('a \ 'b) ell2\ fix \ :: 'a assume \x \ commutant (range (\a. a \\<^sub>o id_cblinfun))\ then have comm: \(a \\<^sub>o id_cblinfun) *\<^sub>V x *\<^sub>V \ = x *\<^sub>V (a \\<^sub>o id_cblinfun) *\<^sub>V \\ for a \ by (metis (mono_tags, lifting) commutant_def mem_Collect_eq rangeI cblinfun_apply_cblinfun_compose) obtain x' where x': \cinner (ket j) (x' *\<^sub>V ket l) = cinner (ket (\,j)) (x *\<^sub>V ket (\,l))\ for j l proof atomize_elim obtain \ where \: \cinner (ket j) (\ l) = cinner (ket (\, j)) (x *\<^sub>V ket (\, l))\ for l j apply (atomize_elim, rule choice, rule allI) apply (rule_tac x=\Abs_ell2 (\j. cinner (ket (\, j)) (x *\<^sub>V ket (\, l)))\ in exI) by (simp add: cinner_ket_left Abs_ell2_inverse) obtain x' where \x' *\<^sub>V ket l = \ l\ for l apply atomize_elim apply (rule exI[of _ \cblinfun_extension (range ket) (\l. \ (inv ket l))\]) apply (subst cblinfun_extension_apply) apply (rule cblinfun_extension_exists_finite_dim) by (auto simp add: inj_ket cindependent_ket) with \ have \cinner (ket j) (x' *\<^sub>V ket l) = cinner (ket (\, j)) (x *\<^sub>V ket (\, l))\ for j l by auto then show \\x'. \j l. cinner (ket j) (x' *\<^sub>V ket l) = cinner (ket (\, j)) (x *\<^sub>V ket (\, l))\ by auto qed have \cinner (ket (i,j)) (x *\<^sub>V ket (k,l)) = cinner (ket (i,j)) ((id_cblinfun \\<^sub>o x') *\<^sub>V ket (k,l))\ for i j k l proof - have \cinner (ket (i,j)) (x *\<^sub>V ket (k,l)) = cinner ((butterket i \ \\<^sub>o id_cblinfun) *\<^sub>V ket (\,j)) (x *\<^sub>V (butterket k \ \\<^sub>o id_cblinfun) *\<^sub>V ket (\,l))\ by (auto simp: tensor_op_ket) also have \\ = cinner (ket (\,j)) ((butterket \ i \\<^sub>o id_cblinfun) *\<^sub>V x *\<^sub>V (butterket k \ \\<^sub>o id_cblinfun) *\<^sub>V ket (\,l))\ by (metis (no_types, lifting) cinner_adj_left butterfly_adjoint id_cblinfun_adjoint tensor_op_adjoint) also have \\ = cinner (ket (\,j)) (x *\<^sub>V (butterket \ i \\<^sub>o id_cblinfun o\<^sub>C\<^sub>L butterket k \ \\<^sub>o id_cblinfun) *\<^sub>V ket (\,l))\ unfolding comm by (simp add: cblinfun_apply_cblinfun_compose) also have \\ = cinner (ket i) (ket k) * cinner (ket (\,j)) (x *\<^sub>V ket (\,l))\ by (simp add: comp_tensor_op tensor_op_ket tensor_op_scaleC_left) also have \\ = cinner (ket i) (ket k) * cinner (ket j) (x' *\<^sub>V ket l)\ by (simp add: x') also have \\ = cinner (ket (i,j)) ((id_cblinfun \\<^sub>o x') *\<^sub>V ket (k,l))\ apply (simp add: tensor_op_ket) by (simp flip: tensor_ell2_ket) finally show ?thesis by - qed then have \x = (id_cblinfun \\<^sub>o x')\ by (auto intro!: equal_ket cinner_ket_eqI) then show \x \ range (\b. id_cblinfun \\<^sub>o b)\ by auto next fix x :: \('a \ 'b) ell2 \\<^sub>C\<^sub>L ('a \ 'b) ell2\ assume \x \ range (\b. id_cblinfun \\<^sub>o b)\ then obtain b where x: \x = id_cblinfun \\<^sub>o b\ by auto then show \x \ commutant (range (\a. a \\<^sub>o id_cblinfun))\ by (auto simp: x commutant_def comp_tensor_op) qed lemma complement_range: assumes [simp]: \compatible F G\ and [simp]: \iso_register (F;G)\ shows \range G = commutant (range F)\ proof - have [simp]: \register F\ \register G\ using assms compatible_def by metis+ have [simp]: \(F;G) (a \\<^sub>o b) = F a o\<^sub>C\<^sub>L G b\ for a b using Laws_Quantum.register_pair_apply assms by blast have [simp]: \range F = (F;G) ` range (\a. a \\<^sub>o id_cblinfun)\ by force have [simp]: \range G = (F;G) ` range (\b. id_cblinfun \\<^sub>o b)\ by force show \range G = commutant (range F)\ by (simp add: commutant_exchange commutant_tensor1) qed lemma same_range_equivalent: fixes F :: \'a::finite update \ 'c::finite update\ and G :: \'b::finite update \ 'c::finite update\ assumes [simp]: \register F\ and [simp]: \register G\ assumes \range F = range G\ shows \equivalent_registers F G\ proof - have G_rangeF[simp]: \G x \ range F\ for x by (simp add: assms) have F_rangeG[simp]: \F x \ range G\ for x by (simp add: assms(3)[symmetric]) have [simp]: \inj F\ and [simp]: \inj G\ by (simp_all add: register_inj) have [simp]: \clinear F\ \clinear G\ by simp_all define I J where \I x = inv F (G x)\ and \J y = inv G (F y)\ for x y have addI: \I (x + y) = I x + I y\ for x y unfolding I_def apply (rule injD[OF \inj F\]) apply (subst complex_vector.linear_add[OF \clinear F\]) apply (subst Hilbert_Choice.f_inv_into_f[where f=F], simp)+ by (simp add: complex_vector.linear_add) have addJ: \J (x + y) = J x + J y\ for x y unfolding J_def apply (rule injD[OF \inj G\]) apply (subst complex_vector.linear_add[OF \clinear G\]) apply (subst Hilbert_Choice.f_inv_into_f[where f=G], simp)+ by (simp add: complex_vector.linear_add) have scaleI: \I (r *\<^sub>C x) = r *\<^sub>C I x\ for r x unfolding I_def apply (rule injD[OF \inj F\]) apply (subst complex_vector.linear_scale[OF \clinear F\]) apply (subst Hilbert_Choice.f_inv_into_f[where f=F], simp)+ by (simp add: complex_vector.linear_scale) have scaleJ: \J (r *\<^sub>C x) = r *\<^sub>C J x\ for r x unfolding J_def apply (rule injD[OF \inj G\]) apply (subst complex_vector.linear_scale[OF \clinear G\]) apply (subst Hilbert_Choice.f_inv_into_f[where f=G], simp)+ by (simp add: complex_vector.linear_scale) have unitalI: \I id_cblinfun = id_cblinfun\ unfolding I_def apply (rule injD[OF \inj F\]) apply (subst Hilbert_Choice.f_inv_into_f[where f=F]) apply auto by (metis register_of_id G_rangeF assms(2)) have unitalJ: \J id_cblinfun = id_cblinfun\ unfolding J_def apply (rule injD[OF \inj G\]) apply (subst Hilbert_Choice.f_inv_into_f[where f=G]) apply auto by (metis register_of_id F_rangeG assms(1)) have multI: \I (a o\<^sub>C\<^sub>L b) = I a o\<^sub>C\<^sub>L I b\ for a b unfolding I_def apply (rule injD[OF \inj F\]) apply (subst register_mult[symmetric, OF \register F\]) apply (subst Hilbert_Choice.f_inv_into_f[where f=F], simp)+ by (simp add: register_mult) have multJ: \J (a o\<^sub>C\<^sub>L b) = J a o\<^sub>C\<^sub>L J b\ for a b unfolding J_def apply (rule injD[OF \inj G\]) apply (subst register_mult[symmetric, OF \register G\]) apply (subst Hilbert_Choice.f_inv_into_f[where f=G], simp)+ by (simp add: register_mult) have adjI: \I (a*) = (I a)*\ for a unfolding I_def apply (rule injD[OF \inj F\]) apply (subst register_adjoint[OF \register F\]) apply (subst Hilbert_Choice.f_inv_into_f[where f=F], simp)+ using assms(2) register_adjoint by blast have adjJ: \J (a*) = (J a)*\ for a unfolding J_def apply (rule injD[OF \inj G\]) apply (subst register_adjoint[OF \register G\]) apply (subst Hilbert_Choice.f_inv_into_f[where f=G], simp)+ using assms(1) register_adjoint by blast from addI scaleI unitalI multI adjI have \register I\ unfolding register_def by (auto intro!: clinearI) from addJ scaleJ unitalJ multJ adjJ have \register J\ unfolding register_def by (auto intro!: clinearI) have \I o J = id\ unfolding I_def J_def o_def apply (subst Hilbert_Choice.f_inv_into_f[where f=G], simp) apply (subst Hilbert_Choice.inv_f_f[OF \inj F\]) by auto have \J o I = id\ unfolding I_def J_def o_def apply (subst Hilbert_Choice.f_inv_into_f[where f=F], simp) apply (subst Hilbert_Choice.inv_f_f[OF \inj G\]) by auto from \I o J = id\ \J o I = id\ \register I\ \register J\ have \iso_register I\ using iso_register_def by blast have \F o I = G\ unfolding I_def o_def by (subst Hilbert_Choice.f_inv_into_f[where f=F], auto) with \iso_register I\ show ?thesis unfolding equivalent_registers_def by auto qed lemma complement_unique: assumes "compatible F G" and \iso_register (F;G)\ assumes "compatible F H" and \iso_register (F;H)\ shows \equivalent_registers G H\ by (metis assms compatible_def complement_range same_range_equivalent) end diff --git a/thys/Registers/Laws.thy b/thys/Registers/Laws.thy --- a/thys/Registers/Laws.thy +++ b/thys/Registers/Laws.thy @@ -1,814 +1,814 @@ section \Generic laws about registers\ theory Laws imports Axioms begin text \This notation is only used inside this file\ notation comp_update (infixl "*\<^sub>u" 55) notation tensor_update (infixr "\\<^sub>u" 70) notation register_pair ("'(_;_')") subsection \Elementary facts\ declare id_preregister[simp] declare id_update_left[simp] declare id_update_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]: \preregister (\b::'b::domain update. tensor_update a b)\ for a :: \'a::domain update\ proof - have \preregister ((\b1::('a\'b) update. (a \\<^sub>u id_update) *\<^sub>u b1) o (\b. tensor_update id_update b))\ by (rule comp_preregister; simp) then show ?thesis by (simp add: o_def tensor_update_mult) qed lemma preregister_tensor_right[simp]: \preregister (\a::'a::domain update. tensor_update a b)\ for b :: \'b::domain update\ proof - have \preregister ((\a1::('a\'b) update. (id_update \\<^sub>u b) *\<^sub>u a1) o (\a. tensor_update a id_update))\ by (rule comp_preregister, simp_all) then show ?thesis by (simp add: o_def tensor_update_mult) qed subsection \Registers\ lemma id_update_tensor_register[simp]: assumes \register F\ shows \register (\a::'a::domain update. id_update \\<^sub>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::domain update. F a \\<^sub>u id_update)\ using assms apply (rule register_comp[unfolded o_def]) by simp subsection \Tensor product of registers\ definition register_tensor (infixr "\\<^sub>r" 70) where "register_tensor F G = register_pair (\a. tensor_update (F a) id_update) (\b. tensor_update id_update (G b))" lemma register_tensor_is_register: fixes F :: "'a::domain update \ 'b::domain update" and G :: "'c::domain update \ 'd::domain update" shows "register F \ register G \ register (F \\<^sub>r G)" unfolding register_tensor_def apply (rule register_pair_is_register) by (simp_all add: tensor_update_mult) lemma register_tensor_apply[simp]: fixes F :: "'a::domain update \ 'b::domain update" and G :: "'c::domain update \ 'd::domain update" assumes \register F\ and \register G\ shows "(F \\<^sub>r G) (a \\<^sub>u b) = F a \\<^sub>u G b" unfolding register_tensor_def apply (subst register_pair_apply) unfolding register_tensor_def by (simp_all add: assms tensor_update_mult) definition "separating (_::'b::domain itself) A \ (\F G :: 'a::domain update \ 'b update. preregister F \ preregister 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::domain) A \ separating TYPE('a) B\ unfolding separating_def by (meson in_mono) lemma register_eqI: \separating TYPE('b::domain) A \ preregister F \ preregister G \ (\x. x\A \ F x = G x) \ F = (G::_ \ 'b update)\ unfolding separating_def by auto lemma separating_tensor: fixes A :: \'a::domain update set\ and B :: \'b::domain update set\ assumes [simp]: \separating TYPE('c::domain) A\ assumes [simp]: \separating TYPE('c) B\ shows \separating TYPE('c) {a \\<^sub>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]: \preregister F\ \preregister G\ have [simp]: \preregister (\x. F (a \\<^sub>u x))\ for a using _ \preregister F\ apply (rule comp_preregister[unfolded o_def]) by simp have [simp]: \preregister (\x. G (a \\<^sub>u x))\ for a using _ \preregister G\ apply (rule comp_preregister[unfolded o_def]) by simp have [simp]: \preregister (\x. F (x \\<^sub>u b))\ for b using _ \preregister F\ apply (rule comp_preregister[unfolded o_def]) by simp have [simp]: \preregister (\x. G (x \\<^sub>u b))\ for b using _ \preregister G\ apply (rule comp_preregister[unfolded o_def]) by simp assume \\x\{a \\<^sub>u b |a b. a\A \ b\B}. F x = G x\ then have EQ: \F (a \\<^sub>u b) = G (a \\<^sub>u b)\ if \a \ A\ and \b \ B\ for a b using that by auto then have \F (a \\<^sub>u b) = G (a \\<^sub>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 \\<^sub>u b) = G (a \\<^sub>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 \\<^sub>r G) o (H \\<^sub>r L) = (F o H) \\<^sub>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::domain update set\ and B :: \'b::domain update set\ assumes \separating TYPE('c::domain) A\ assumes \separating TYPE('c) B\ assumes \C = {a \\<^sub>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::domain\'b::domain\'c::domain) update \ 'd::domain update\ assumes [simp]: \register F\ \register G\ assumes "\f g h. F (f \\<^sub>u g \\<^sub>u h) = G (f \\<^sub>u g \\<^sub>u h)" shows "F = G" proof (rule register_eqI[where A=\{a\\<^sub>ub\\<^sub>uc| a b c. True}\]) have \separating TYPE('d) {b \\<^sub>u c |b c. True}\ apply (rule separating_tensor'[where A=UNIV and B=UNIV]) by auto then show \separating TYPE('d) {a \\<^sub>u b \\<^sub>u c |a b c. True}\ apply (rule_tac separating_tensor'[where A=UNIV and B=\{b\\<^sub>uc| b c. True}\]) by auto show \preregister F\ \preregister G\ by auto show \x \ {a \\<^sub>u b \\<^sub>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::domain\'b::domain)\'c::domain) update \ 'd::domain update\ assumes [simp]: \register F\ \register G\ assumes "\f g h. F ((f \\<^sub>u g) \\<^sub>u h) = G ((f \\<^sub>u g) \\<^sub>u h)" shows "F = G" proof (rule register_eqI[where A=\{(a\\<^sub>ub)\\<^sub>uc| a b c. True}\]) have \separating TYPE('d) {a \\<^sub>u b | a b. True}\ apply (rule separating_tensor'[where A=UNIV and B=UNIV]) by auto then show \separating TYPE('d) {(a \\<^sub>u b) \\<^sub>u c |a b c. True}\ apply (rule_tac separating_tensor'[where B=UNIV and A=\{a\\<^sub>ub| a b. True}\]) by auto show \preregister F\ \preregister G\ by auto show \x \ {(a \\<^sub>u b) \\<^sub>u c |a b c. True} \ F x = G x\ for x using assms(3) by auto qed lemma register_tensor_id[simp]: \id \\<^sub>r id = id\ apply (rule tensor_extensionality) by (auto simp add: register_tensor_is_register) subsection \Pairs and compatibility\ definition compatible :: \('a::domain update \ 'c::domain update) \ ('b::domain update \ 'c update) \ bool\ where \compatible F G \ register F \ register G \ (\a b. F a *\<^sub>u G b = G b *\<^sub>u F a)\ lemma compatibleI: assumes "register F" and "register G" assumes \\a b. (F a) *\<^sub>u (G b) = (G b) *\<^sub>u (F a)\ shows "compatible F G" using assms unfolding compatible_def by simp lemma swap_registers: assumes "compatible R S" shows "R a *\<^sub>u S b = S b *\<^sub>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 \\<^sub>u b) = (F a) *\<^sub>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 \\<^sub>u b) = (G b) *\<^sub>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 \\<^sub>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 comp_preregister) lemma compatible_tensor_id_update_left[simp]: fixes F :: "'a::domain update \ 'c::domain update" and G :: "'b::domain update \ 'c::domain update" assumes "compatible F G" shows "compatible (\a. id_update \\<^sub>u F a) (\a. id_update \\<^sub>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::domain update \ 'c::domain update" and G :: "'b::domain update \ 'c::domain update" assumes "compatible F G" shows "compatible (\a. F a \\<^sub>u id_update) (\a. G a \\<^sub>u id_update)" 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 \\<^sub>u id_update) (\a. id_update \\<^sub>u G a)" apply (rule compatibleI) using assms by (auto simp: tensor_update_mult) lemma compatible_tensor_id_update_lr[simp]: assumes "register F" and "register G" shows "compatible (\a. id_update \\<^sub>u F a) (\a. G a \\<^sub>u id_update)" apply (rule compatibleI) using assms by (auto simp: tensor_update_mult) 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 \preregister (F \ G;F \ H)\ and \preregister (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 \\<^sub>u b) = (F \ (G;H)) (a \\<^sub>u b)\ by (auto simp: register_pair_apply register_mult tensor_update_mult) qed lemma swap_registers_left: assumes "compatible R S" shows "R a *\<^sub>u S b *\<^sub>u c = S b *\<^sub>u R a *\<^sub>u c" using assms unfolding compatible_def by metis lemma swap_registers_right: assumes "compatible R S" shows "c *\<^sub>u R a *\<^sub>u S b = c *\<^sub>u S b *\<^sub>u R a" by (metis assms comp_update_assoc compatible_def) lemmas compatible_ac_rules = swap_registers comp_update_assoc[symmetric] swap_registers_right subsection \Fst and Snd\ definition Fst where \Fst a = a \\<^sub>u id_update\ definition Snd where \Snd a = id_update \\<^sub>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 tensor_update_mult) lemmas compatible_Snd_Fst[simp] = compatible_Fst_Snd[THEN compatible_sym] definition \swap = (Snd; Fst)\ lemma swap_apply[simp]: "swap (a \\<^sub>u b) = (b \\<^sub>u a)" unfolding swap_def by (simp add: Axioms.register_pair_apply Fst_def Snd_def tensor_update_mult) 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 tensor_update_mult) 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 tensor_update_mult) 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 tensor_update_mult) 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]: \preregister F\ \preregister G\ \preregister H\ using register_preregister by blast+ have [simp]: \preregister (\a. (F;G) a *\<^sub>u z)\ for z apply (rule comp_preregister[unfolded o_def, of \(F;G)\]) by simp_all have [simp]: \preregister (\a. z *\<^sub>u (F;G) a)\ for z apply (rule comp_preregister[unfolded o_def, of \(F;G)\]) by simp_all have "(F; G) (f \\<^sub>u g) *\<^sub>u H h = H h *\<^sub>u (F; G) (f \\<^sub>u g)" for f g h proof - have FH: "F f *\<^sub>u H h = H h *\<^sub>u F f" using assms compatible_def by metis have GH: "G g *\<^sub>u H h = H h *\<^sub>u G g" using assms compatible_def by metis have \(F; G) (f \\<^sub>u g) *\<^sub>u (H h) = F f *\<^sub>u G g *\<^sub>u H h\ using \compatible F G\ by (subst register_pair_apply, auto) also have \\ = H h *\<^sub>u F f *\<^sub>u G g\ using FH GH by (metis comp_update_assoc) also have \\ = H h *\<^sub>u (F; G) (f \\<^sub>u g)\ using \compatible F G\ by (subst register_pair_apply, auto simp: comp_update_assoc) finally show ?thesis by - qed then show "(F; G) fg *\<^sub>u (H h) = (H h) *\<^sub>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]: "preregister A" "preregister B" - apply (metis (no_types, hide_lams) assms compatible_register1 register_preregister) + apply (metis (no_types, opaque_lifting) assms compatible_register1 register_preregister) by (metis (full_types) assms compatible_register2 register_preregister) then show \preregister ((A; B) \ swap)\ by simp show \preregister (B; A)\ by (metis (no_types, lifting) assms compatible_sym register_preregister pair_is_register) show \((A; B) \ swap) (a \\<^sub>u b) = (B; A) (a \\<^sub>u b)\ for a b (* Without the "only:", we would not need the "apply subst", but that proof fails when instantiated in Classical.thy *) 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::domain update \ 'e::domain update\ and G :: \'b::domain update \ 'f::domain update\ and F' :: \'c::domain update \ 'e update\ and G' :: \'d::domain update \ 'f update\ assumes [simp]: \compatible F F'\ assumes [simp]: \compatible G G'\ shows \compatible (F \\<^sub>r G) (F' \\<^sub>r G')\ proof - note [intro!] = comp_preregister[OF _ preregister_mult_right, unfolded o_def] comp_preregister[OF _ preregister_mult_left, unfolded o_def] comp_preregister register_tensor_is_register have [simp]: \register F\ \register G\ \register F'\ \register G'\ using assms compatible_def by blast+ have [simp]: \register (F \\<^sub>r G)\ \register (F' \\<^sub>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]: \preregister reorder\ by (auto simp: reorder_def) have [simp]: \reorder ((a \\<^sub>u b) \\<^sub>u (c \\<^sub>u d)) = ((a \\<^sub>u c) \\<^sub>u (b \\<^sub>u d))\ for a b c d apply (simp add: reorder_def register_pair_apply) by (simp add: Fst_def Snd_def tensor_update_mult) define \ where \\ c d = ((F;F') \\<^sub>r (G;G')) o reorder o (\\. \ \\<^sub>u (c \\<^sub>u d))\ for c d have [simp]: \preregister (\ c d)\ for c d unfolding \_def by (auto intro: register_preregister) have \\ c d (a \\<^sub>u b) = (F \\<^sub>r G) (a \\<^sub>u b) *\<^sub>u (F' \\<^sub>r G') (c \\<^sub>u d)\ for a b c d unfolding \_def by (auto simp: register_pair_apply tensor_update_mult) then have \1: \\ c d \ = (F \\<^sub>r G) \ *\<^sub>u (F' \\<^sub>r G') (c \\<^sub>u d)\ for c d \ apply (rule_tac fun_cong[of _ _ \]) apply (rule tensor_extensionality) by auto have \\ c d (a \\<^sub>u b) = (F' \\<^sub>r G') (c \\<^sub>u d) *\<^sub>u (F \\<^sub>r G) (a \\<^sub>u b)\ for a b c d unfolding \_def apply (auto simp: register_pair_apply) by (metis assms(1) assms(2) compatible_def tensor_update_mult) then have \2: \\ c d \ = (F' \\<^sub>r G') (c \\<^sub>u d) *\<^sub>u (F \\<^sub>r G) \\ for c d \ apply (rule_tac fun_cong[of _ _ \]) apply (rule tensor_extensionality) by auto from \1 \2 have \(F \\<^sub>r G) \ *\<^sub>u (F' \\<^sub>r G') \ = (F' \\<^sub>r G') \ *\<^sub>u (F \\<^sub>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::domain\'b::domain)\'c::domain) update \ ('a\('b\'c)) update\ where \assoc = ((Fst; Snd o Fst); Snd o Snd)\ lemma assoc_is_hom[simp]: \preregister assoc\ by (auto simp: assoc_def) lemma assoc_apply[simp]: \assoc ((a \\<^sub>u b) \\<^sub>u c) = (a \\<^sub>u (b \\<^sub>u c))\ by (auto simp: assoc_def register_pair_apply Fst_def Snd_def tensor_update_mult) definition assoc' :: \('a\('b\'c)) update \ (('a::domain\'b::domain)\'c::domain) update\ where \assoc' = (Fst o Fst; (Fst o Snd; Snd))\ lemma assoc'_is_hom[simp]: \preregister assoc'\ by (auto simp: assoc'_def) lemma assoc'_apply[simp]: \assoc' (a \\<^sub>u (b \\<^sub>u c)) = ((a \\<^sub>u b) \\<^sub>u c)\ by (auto simp: assoc'_def register_pair_apply Fst_def Snd_def tensor_update_mult) 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 \\<^sub>u g) \\<^sub>u h) = ((F; G); H) ((f \\<^sub>u g) \\<^sub>u h)\ for f g h by (simp add: register_pair_apply assoc_apply comp_update_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 \\<^sub>u g \\<^sub>u h) = (F; (G; H)) (f \\<^sub>u g \\<^sub>u h)\ for f g h by (simp add: register_pair_apply assoc'_apply comp_update_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 :: \_::domain update \ _::domain 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 \\<^sub>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' \\<^sub>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 \\<^sub>r G) = inv F \\<^sub>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 :: \_::domain update \ _::domain 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 \\<^sub>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 \\<^sub>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 \\<^sub>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 \\<^sub>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_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 (* val _ = \<^print> thms *) 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 comp_update (infixl "*\<^sub>u" 55) no_notation tensor_update (infixr "\\<^sub>u" 70) bundle register_notation begin notation register_tensor (infixr "\\<^sub>r" 70) notation register_pair ("'(_;_')") end bundle no_register_notation begin no_notation register_tensor (infixr "\\<^sub>r" 70) no_notation register_pair ("'(_;_')") end end diff --git a/thys/Registers/Laws_Classical.thy b/thys/Registers/Laws_Classical.thy --- a/thys/Registers/Laws_Classical.thy +++ b/thys/Registers/Laws_Classical.thy @@ -1,819 +1,819 @@ (* * This is an autogenerated file. Do not edit. * The original is Laws.thy. It was converted using instantiate_laws.py. *) section \Generic laws about registers, instantiated classically\ theory Laws_Classical imports Axioms_Classical begin text \This notation is only used inside this file\ notation map_comp (infixl "*\<^sub>u" 55) notation tensor_update (infixr "\\<^sub>u" 70) notation register_pair ("'(_;_')") subsection \Elementary facts\ declare id_preregister[simp] declare id_update_left[simp] declare id_update_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]: \preregister (\b::'b::type update. tensor_update a b)\ for a :: \'a::type update\ proof - have \preregister ((\b1::('a\'b) update. (a \\<^sub>u Some) *\<^sub>u b1) o (\b. tensor_update Some b))\ by (rule comp_preregister; simp) then show ?thesis by (simp add: o_def tensor_update_mult) qed lemma preregister_tensor_right[simp]: \preregister (\a::'a::type update. tensor_update a b)\ for b :: \'b::type update\ proof - have \preregister ((\a1::('a\'b) update. (Some \\<^sub>u b) *\<^sub>u a1) o (\a. tensor_update a Some))\ by (rule comp_preregister, simp_all) then show ?thesis by (simp add: o_def tensor_update_mult) qed subsection \Registers\ lemma id_update_tensor_register[simp]: assumes \register F\ shows \register (\a::'a::type update. Some \\<^sub>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::type update. F a \\<^sub>u Some)\ using assms apply (rule register_comp[unfolded o_def]) by simp subsection \Tensor product of registers\ definition register_tensor (infixr "\\<^sub>r" 70) where "register_tensor F G = register_pair (\a. tensor_update (F a) Some) (\b. tensor_update Some (G b))" lemma register_tensor_is_register: fixes F :: "'a::type update \ 'b::type update" and G :: "'c::type update \ 'd::type update" shows "register F \ register G \ register (F \\<^sub>r G)" unfolding register_tensor_def apply (rule register_pair_is_register) by (simp_all add: tensor_update_mult) lemma register_tensor_apply[simp]: fixes F :: "'a::type update \ 'b::type update" and G :: "'c::type update \ 'd::type update" assumes \register F\ and \register G\ shows "(F \\<^sub>r G) (a \\<^sub>u b) = F a \\<^sub>u G b" unfolding register_tensor_def apply (subst register_pair_apply) unfolding register_tensor_def by (simp_all add: assms tensor_update_mult) definition "separating (_::'b::type itself) A \ (\F G :: 'a::type update \ 'b update. preregister F \ preregister 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::type) A \ separating TYPE('a) B\ unfolding separating_def by (meson in_mono) lemma register_eqI: \separating TYPE('b::type) A \ preregister F \ preregister G \ (\x. x\A \ F x = G x) \ F = (G::_ \ 'b update)\ unfolding separating_def by auto lemma separating_tensor: fixes A :: \'a::type update set\ and B :: \'b::type update set\ assumes [simp]: \separating TYPE('c::type) A\ assumes [simp]: \separating TYPE('c) B\ shows \separating TYPE('c) {a \\<^sub>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]: \preregister F\ \preregister G\ have [simp]: \preregister (\x. F (a \\<^sub>u x))\ for a using _ \preregister F\ apply (rule comp_preregister[unfolded o_def]) by simp have [simp]: \preregister (\x. G (a \\<^sub>u x))\ for a using _ \preregister G\ apply (rule comp_preregister[unfolded o_def]) by simp have [simp]: \preregister (\x. F (x \\<^sub>u b))\ for b using _ \preregister F\ apply (rule comp_preregister[unfolded o_def]) by simp have [simp]: \preregister (\x. G (x \\<^sub>u b))\ for b using _ \preregister G\ apply (rule comp_preregister[unfolded o_def]) by simp assume \\x\{a \\<^sub>u b |a b. a\A \ b\B}. F x = G x\ then have EQ: \F (a \\<^sub>u b) = G (a \\<^sub>u b)\ if \a \ A\ and \b \ B\ for a b using that by auto then have \F (a \\<^sub>u b) = G (a \\<^sub>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 \\<^sub>u b) = G (a \\<^sub>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 \\<^sub>r G) o (H \\<^sub>r L) = (F o H) \\<^sub>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::type update set\ and B :: \'b::type update set\ assumes \separating TYPE('c::type) A\ assumes \separating TYPE('c) B\ assumes \C = {a \\<^sub>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::type\'b::type\'c::type) update \ 'd::type update\ assumes [simp]: \register F\ \register G\ assumes "\f g h. F (f \\<^sub>u g \\<^sub>u h) = G (f \\<^sub>u g \\<^sub>u h)" shows "F = G" proof (rule register_eqI[where A=\{a\\<^sub>ub\\<^sub>uc| a b c. True}\]) have \separating TYPE('d) {b \\<^sub>u c |b c. True}\ apply (rule separating_tensor'[where A=UNIV and B=UNIV]) by auto then show \separating TYPE('d) {a \\<^sub>u b \\<^sub>u c |a b c. True}\ apply (rule_tac separating_tensor'[where A=UNIV and B=\{b\\<^sub>uc| b c. True}\]) by auto show \preregister F\ \preregister G\ by auto show \x \ {a \\<^sub>u b \\<^sub>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::type\'b::type)\'c::type) update \ 'd::type update\ assumes [simp]: \register F\ \register G\ assumes "\f g h. F ((f \\<^sub>u g) \\<^sub>u h) = G ((f \\<^sub>u g) \\<^sub>u h)" shows "F = G" proof (rule register_eqI[where A=\{(a\\<^sub>ub)\\<^sub>uc| a b c. True}\]) have \separating TYPE('d) {a \\<^sub>u b | a b. True}\ apply (rule separating_tensor'[where A=UNIV and B=UNIV]) by auto then show \separating TYPE('d) {(a \\<^sub>u b) \\<^sub>u c |a b c. True}\ apply (rule_tac separating_tensor'[where B=UNIV and A=\{a\\<^sub>ub| a b. True}\]) by auto show \preregister F\ \preregister G\ by auto show \x \ {(a \\<^sub>u b) \\<^sub>u c |a b c. True} \ F x = G x\ for x using assms(3) by auto qed lemma register_tensor_id[simp]: \id \\<^sub>r id = id\ apply (rule tensor_extensionality) by (auto simp add: register_tensor_is_register) subsection \Pairs and compatibility\ definition compatible :: \('a::type update \ 'c::type update) \ ('b::type update \ 'c update) \ bool\ where \compatible F G \ register F \ register G \ (\a b. F a *\<^sub>u G b = G b *\<^sub>u F a)\ lemma compatibleI: assumes "register F" and "register G" assumes \\a b. (F a) *\<^sub>u (G b) = (G b) *\<^sub>u (F a)\ shows "compatible F G" using assms unfolding compatible_def by simp lemma swap_registers: assumes "compatible R S" shows "R a *\<^sub>u S b = S b *\<^sub>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 \\<^sub>u b) = (F a) *\<^sub>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 \\<^sub>u b) = (G b) *\<^sub>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 \\<^sub>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 comp_preregister) lemma compatible_tensor_id_update_left[simp]: fixes F :: "'a::type update \ 'c::type update" and G :: "'b::type update \ 'c::type update" assumes "compatible F G" shows "compatible (\a. Some \\<^sub>u F a) (\a. Some \\<^sub>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::type update \ 'c::type update" and G :: "'b::type update \ 'c::type update" assumes "compatible F G" shows "compatible (\a. F a \\<^sub>u Some) (\a. G a \\<^sub>u Some)" 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 \\<^sub>u Some) (\a. Some \\<^sub>u G a)" apply (rule compatibleI) using assms by (auto simp: tensor_update_mult) lemma compatible_tensor_id_update_lr[simp]: assumes "register F" and "register G" shows "compatible (\a. Some \\<^sub>u F a) (\a. G a \\<^sub>u Some)" apply (rule compatibleI) using assms by (auto simp: tensor_update_mult) 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 \preregister (F \ G;F \ H)\ and \preregister (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 \\<^sub>u b) = (F \ (G;H)) (a \\<^sub>u b)\ by (auto simp: register_pair_apply register_mult tensor_update_mult) qed lemma swap_registers_left: assumes "compatible R S" shows "R a *\<^sub>u S b *\<^sub>u c = S b *\<^sub>u R a *\<^sub>u c" using assms unfolding compatible_def by metis lemma swap_registers_right: assumes "compatible R S" shows "c *\<^sub>u R a *\<^sub>u S b = c *\<^sub>u S b *\<^sub>u R a" by (metis assms comp_update_assoc compatible_def) lemmas compatible_ac_rules = swap_registers comp_update_assoc[symmetric] swap_registers_right subsection \Fst and Snd\ definition Fst where \Fst a = a \\<^sub>u Some\ definition Snd where \Snd a = Some \\<^sub>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 tensor_update_mult) lemmas compatible_Snd_Fst[simp] = compatible_Fst_Snd[THEN compatible_sym] definition \swap = (Snd; Fst)\ lemma swap_apply[simp]: "swap (a \\<^sub>u b) = (b \\<^sub>u a)" unfolding swap_def by (simp add: Axioms_Classical.register_pair_apply Fst_def Snd_def tensor_update_mult) 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 tensor_update_mult) 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 tensor_update_mult) 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 tensor_update_mult) 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]: \preregister F\ \preregister G\ \preregister H\ using register_preregister by blast+ have [simp]: \preregister (\a. (F;G) a *\<^sub>u z)\ for z apply (rule comp_preregister[unfolded o_def, of \(F;G)\]) by simp_all have [simp]: \preregister (\a. z *\<^sub>u (F;G) a)\ for z apply (rule comp_preregister[unfolded o_def, of \(F;G)\]) by simp_all have "(F; G) (f \\<^sub>u g) *\<^sub>u H h = H h *\<^sub>u (F; G) (f \\<^sub>u g)" for f g h proof - have FH: "F f *\<^sub>u H h = H h *\<^sub>u F f" using assms compatible_def by metis have GH: "G g *\<^sub>u H h = H h *\<^sub>u G g" using assms compatible_def by metis have \(F; G) (f \\<^sub>u g) *\<^sub>u (H h) = F f *\<^sub>u G g *\<^sub>u H h\ using \compatible F G\ by (subst register_pair_apply, auto) also have \\ = H h *\<^sub>u F f *\<^sub>u G g\ using FH GH by (metis comp_update_assoc) also have \\ = H h *\<^sub>u (F; G) (f \\<^sub>u g)\ using \compatible F G\ by (subst register_pair_apply, auto simp: comp_update_assoc) finally show ?thesis by - qed then show "(F; G) fg *\<^sub>u (H h) = (H h) *\<^sub>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]: "preregister A" "preregister B" - apply (metis (no_types, hide_lams) assms compatible_register1 register_preregister) + apply (metis (no_types, opaque_lifting) assms compatible_register1 register_preregister) by (metis (full_types) assms compatible_register2 register_preregister) then show \preregister ((A; B) \ swap)\ by simp show \preregister (B; A)\ by (metis (no_types, lifting) assms compatible_sym register_preregister pair_is_register) show \((A; B) \ swap) (a \\<^sub>u b) = (B; A) (a \\<^sub>u b)\ for a b (* Without the "only:", we would not need the "apply subst", but that proof fails when instantiated in Classical.thy *) 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::type update \ 'e::type update\ and G :: \'b::type update \ 'f::type update\ and F' :: \'c::type update \ 'e update\ and G' :: \'d::type update \ 'f update\ assumes [simp]: \compatible F F'\ assumes [simp]: \compatible G G'\ shows \compatible (F \\<^sub>r G) (F' \\<^sub>r G')\ proof - note [intro!] = comp_preregister[OF _ preregister_mult_right, unfolded o_def] comp_preregister[OF _ preregister_mult_left, unfolded o_def] comp_preregister register_tensor_is_register have [simp]: \register F\ \register G\ \register F'\ \register G'\ using assms compatible_def by blast+ have [simp]: \register (F \\<^sub>r G)\ \register (F' \\<^sub>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]: \preregister reorder\ by (auto simp: reorder_def) have [simp]: \reorder ((a \\<^sub>u b) \\<^sub>u (c \\<^sub>u d)) = ((a \\<^sub>u c) \\<^sub>u (b \\<^sub>u d))\ for a b c d apply (simp add: reorder_def register_pair_apply) by (simp add: Fst_def Snd_def tensor_update_mult) define \ where \\ c d = ((F;F') \\<^sub>r (G;G')) o reorder o (\\. \ \\<^sub>u (c \\<^sub>u d))\ for c d have [simp]: \preregister (\ c d)\ for c d unfolding \_def by (auto intro: register_preregister) have \\ c d (a \\<^sub>u b) = (F \\<^sub>r G) (a \\<^sub>u b) *\<^sub>u (F' \\<^sub>r G') (c \\<^sub>u d)\ for a b c d unfolding \_def by (auto simp: register_pair_apply tensor_update_mult) then have \1: \\ c d \ = (F \\<^sub>r G) \ *\<^sub>u (F' \\<^sub>r G') (c \\<^sub>u d)\ for c d \ apply (rule_tac fun_cong[of _ _ \]) apply (rule tensor_extensionality) by auto have \\ c d (a \\<^sub>u b) = (F' \\<^sub>r G') (c \\<^sub>u d) *\<^sub>u (F \\<^sub>r G) (a \\<^sub>u b)\ for a b c d unfolding \_def apply (auto simp: register_pair_apply) by (metis assms(1) assms(2) compatible_def tensor_update_mult) then have \2: \\ c d \ = (F' \\<^sub>r G') (c \\<^sub>u d) *\<^sub>u (F \\<^sub>r G) \\ for c d \ apply (rule_tac fun_cong[of _ _ \]) apply (rule tensor_extensionality) by auto from \1 \2 have \(F \\<^sub>r G) \ *\<^sub>u (F' \\<^sub>r G') \ = (F' \\<^sub>r G') \ *\<^sub>u (F \\<^sub>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::type\'b::type)\'c::type) update \ ('a\('b\'c)) update\ where \assoc = ((Fst; Snd o Fst); Snd o Snd)\ lemma assoc_is_hom[simp]: \preregister assoc\ by (auto simp: assoc_def) lemma assoc_apply[simp]: \assoc ((a \\<^sub>u b) \\<^sub>u c) = (a \\<^sub>u (b \\<^sub>u c))\ by (auto simp: assoc_def register_pair_apply Fst_def Snd_def tensor_update_mult) definition assoc' :: \('a\('b\'c)) update \ (('a::type\'b::type)\'c::type) update\ where \assoc' = (Fst o Fst; (Fst o Snd; Snd))\ lemma assoc'_is_hom[simp]: \preregister assoc'\ by (auto simp: assoc'_def) lemma assoc'_apply[simp]: \assoc' (a \\<^sub>u (b \\<^sub>u c)) = ((a \\<^sub>u b) \\<^sub>u c)\ by (auto simp: assoc'_def register_pair_apply Fst_def Snd_def tensor_update_mult) 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 \\<^sub>u g) \\<^sub>u h) = ((F; G); H) ((f \\<^sub>u g) \\<^sub>u h)\ for f g h by (simp add: register_pair_apply assoc_apply comp_update_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 \\<^sub>u g \\<^sub>u h) = (F; (G; H)) (f \\<^sub>u g \\<^sub>u h)\ for f g h by (simp add: register_pair_apply assoc'_apply comp_update_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 :: \_::type update \ _::type 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 \\<^sub>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' \\<^sub>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 \\<^sub>r G) = inv F \\<^sub>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 :: \_::type update \ _::type 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 \\<^sub>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 \\<^sub>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 \\<^sub>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 \\<^sub>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_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 (* val _ = \<^print> thms *) 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 map_comp (infixl "*\<^sub>u" 55) no_notation tensor_update (infixr "\\<^sub>u" 70) bundle register_notation begin notation register_tensor (infixr "\\<^sub>r" 70) notation register_pair ("'(_;_')") end bundle no_register_notation begin no_notation register_tensor (infixr "\\<^sub>r" 70) no_notation register_pair ("'(_;_')") end end diff --git a/thys/Registers/Laws_Complement.thy b/thys/Registers/Laws_Complement.thy --- a/thys/Registers/Laws_Complement.thy +++ b/thys/Registers/Laws_Complement.thy @@ -1,358 +1,358 @@ section \Generic laws about complements\ theory Laws_Complement imports Laws Axioms_Complement begin notation comp_update (infixl "*\<^sub>u" 55) notation tensor_update (infixr "\\<^sub>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, hide_lams) swap_swap \I \ (F;G) = id\ calculation(2) comp_def eq_id_iff) + 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 \\<^sub>r G) (complement F \\<^sub>r complement G)\ proof (rule complementsI) have sep4: \separating TYPE('z::domain) {(a \\<^sub>u b) \\<^sub>u (c \\<^sub>u d) |a b c d. True}\ apply (rule separating_tensor'[where A=\{(a \\<^sub>u b) |a b. True}\ and B=\{(c \\<^sub>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 \\<^sub>r G) (complement F \\<^sub>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 \\<^sub>u b) \\<^sub>u (c \\<^sub>u d)) = ((a \\<^sub>u c) \\<^sub>u (b \\<^sub>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 \\<^sub>r G; complement F \\<^sub>r complement G) = ((F; complement F) \\<^sub>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 \\<^sub>r G;complement F \\<^sub>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, hide_lams) 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) + 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, hide_lams) assms(1) assms(2) calculation complements_def equivalent_registers_sym equivalent_registers_trans is_unit_register_def register_comp_pair) + 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 \\<^sub>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 \\<^sub>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\ (* 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 \\<^sub>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 \\<^sub>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 "*\<^sub>u" 55) no_notation tensor_update (infixr "\\<^sub>u" 70) end diff --git a/thys/Registers/Laws_Complement_Quantum.thy b/thys/Registers/Laws_Complement_Quantum.thy --- a/thys/Registers/Laws_Complement_Quantum.thy +++ b/thys/Registers/Laws_Complement_Quantum.thy @@ -1,363 +1,363 @@ (* * 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 "*\<^sub>u" 55) notation tensor_op (infixr "\\<^sub>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, hide_lams) swap_swap \I \ (F;G) = id\ calculation(2) comp_def eq_id_iff) + 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 \\<^sub>r G) (complement F \\<^sub>r complement G)\ proof (rule complementsI) have sep4: \separating TYPE('z::finite) {(a \\<^sub>u b) \\<^sub>u (c \\<^sub>u d) |a b c d. True}\ apply (rule separating_tensor'[where A=\{(a \\<^sub>u b) |a b. True}\ and B=\{(c \\<^sub>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 \\<^sub>r G) (complement F \\<^sub>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 \\<^sub>u b) \\<^sub>u (c \\<^sub>u d)) = ((a \\<^sub>u c) \\<^sub>u (b \\<^sub>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 \\<^sub>r G; complement F \\<^sub>r complement G) = ((F; complement F) \\<^sub>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 \\<^sub>r G;complement F \\<^sub>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, hide_lams) 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) + 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, hide_lams) assms(1) assms(2) calculation complements_def equivalent_registers_sym equivalent_registers_trans is_unit_register_def register_comp_pair) + 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 \\<^sub>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 \\<^sub>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 \\<^sub>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 \\<^sub>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 "*\<^sub>u" 55) no_notation tensor_op (infixr "\\<^sub>u" 70) end diff --git a/thys/Registers/Laws_Quantum.thy b/thys/Registers/Laws_Quantum.thy --- a/thys/Registers/Laws_Quantum.thy +++ b/thys/Registers/Laws_Quantum.thy @@ -1,819 +1,819 @@ (* * This is an autogenerated file. Do not edit. * The original is Laws.thy. It was converted using instantiate_laws.py. *) 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 "*\<^sub>u" 55) notation tensor_op (infixr "\\<^sub>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 \\<^sub>u id_cblinfun) *\<^sub>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 \\<^sub>u b) *\<^sub>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 \\<^sub>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 \\<^sub>u id_cblinfun)\ using assms apply (rule register_comp[unfolded o_def]) by simp subsection \Tensor product of registers\ definition register_tensor (infixr "\\<^sub>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 \\<^sub>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 \\<^sub>r G) (a \\<^sub>u b) = F a \\<^sub>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 \\<^sub>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 \\<^sub>u x))\ for a using _ \clinear F\ apply (rule clinear_compose[unfolded o_def]) by simp have [simp]: \clinear (\x. G (a \\<^sub>u x))\ for a using _ \clinear G\ apply (rule clinear_compose[unfolded o_def]) by simp have [simp]: \clinear (\x. F (x \\<^sub>u b))\ for b using _ \clinear F\ apply (rule clinear_compose[unfolded o_def]) by simp have [simp]: \clinear (\x. G (x \\<^sub>u b))\ for b using _ \clinear G\ apply (rule clinear_compose[unfolded o_def]) by simp assume \\x\{a \\<^sub>u b |a b. a\A \ b\B}. F x = G x\ then have EQ: \F (a \\<^sub>u b) = G (a \\<^sub>u b)\ if \a \ A\ and \b \ B\ for a b using that by auto then have \F (a \\<^sub>u b) = G (a \\<^sub>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 \\<^sub>u b) = G (a \\<^sub>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 \\<^sub>r G) o (H \\<^sub>r L) = (F o H) \\<^sub>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 \\<^sub>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 \\<^sub>u g \\<^sub>u h) = G (f \\<^sub>u g \\<^sub>u h)" shows "F = G" proof (rule register_eqI[where A=\{a\\<^sub>ub\\<^sub>uc| a b c. True}\]) have \separating TYPE('d) {b \\<^sub>u c |b c. True}\ apply (rule separating_tensor'[where A=UNIV and B=UNIV]) by auto then show \separating TYPE('d) {a \\<^sub>u b \\<^sub>u c |a b c. True}\ apply (rule_tac separating_tensor'[where A=UNIV and B=\{b\\<^sub>uc| b c. True}\]) by auto show \clinear F\ \clinear G\ by auto show \x \ {a \\<^sub>u b \\<^sub>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 \\<^sub>u g) \\<^sub>u h) = G ((f \\<^sub>u g) \\<^sub>u h)" shows "F = G" proof (rule register_eqI[where A=\{(a\\<^sub>ub)\\<^sub>uc| a b c. True}\]) have \separating TYPE('d) {a \\<^sub>u b | a b. True}\ apply (rule separating_tensor'[where A=UNIV and B=UNIV]) by auto then show \separating TYPE('d) {(a \\<^sub>u b) \\<^sub>u c |a b c. True}\ apply (rule_tac separating_tensor'[where B=UNIV and A=\{a\\<^sub>ub| a b. True}\]) by auto show \clinear F\ \clinear G\ by auto show \x \ {(a \\<^sub>u b) \\<^sub>u c |a b c. True} \ F x = G x\ for x using assms(3) by auto qed lemma register_tensor_id[simp]: \id \\<^sub>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 *\<^sub>u G b = G b *\<^sub>u F a)\ lemma compatibleI: assumes "register F" and "register G" assumes \\a b. (F a) *\<^sub>u (G b) = (G b) *\<^sub>u (F a)\ shows "compatible F G" using assms unfolding compatible_def by simp lemma swap_registers: assumes "compatible R S" shows "R a *\<^sub>u S b = S b *\<^sub>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 \\<^sub>u b) = (F a) *\<^sub>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 \\<^sub>u b) = (G b) *\<^sub>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 \\<^sub>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 \\<^sub>u F a) (\a. id_cblinfun \\<^sub>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 \\<^sub>u id_cblinfun) (\a. G a \\<^sub>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 \\<^sub>u id_cblinfun) (\a. id_cblinfun \\<^sub>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 \\<^sub>u F a) (\a. G a \\<^sub>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 \\<^sub>u b) = (F \ (G;H)) (a \\<^sub>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 *\<^sub>u S b *\<^sub>u c = S b *\<^sub>u R a *\<^sub>u c" using assms unfolding compatible_def by metis lemma swap_registers_right: assumes "compatible R S" shows "c *\<^sub>u R a *\<^sub>u S b = c *\<^sub>u S b *\<^sub>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 \\<^sub>u id_cblinfun\ definition Snd where \Snd a = id_cblinfun \\<^sub>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 \\<^sub>u b) = (b \\<^sub>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 *\<^sub>u z)\ for z apply (rule clinear_compose[unfolded o_def, of \(F;G)\]) by simp_all have [simp]: \clinear (\a. z *\<^sub>u (F;G) a)\ for z apply (rule clinear_compose[unfolded o_def, of \(F;G)\]) by simp_all have "(F; G) (f \\<^sub>u g) *\<^sub>u H h = H h *\<^sub>u (F; G) (f \\<^sub>u g)" for f g h proof - have FH: "F f *\<^sub>u H h = H h *\<^sub>u F f" using assms compatible_def by metis have GH: "G g *\<^sub>u H h = H h *\<^sub>u G g" using assms compatible_def by metis have \(F; G) (f \\<^sub>u g) *\<^sub>u (H h) = F f *\<^sub>u G g *\<^sub>u H h\ using \compatible F G\ by (subst register_pair_apply, auto) also have \\ = H h *\<^sub>u F f *\<^sub>u G g\ using FH GH by (metis cblinfun_compose_assoc) also have \\ = H h *\<^sub>u (F; G) (f \\<^sub>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 *\<^sub>u (H h) = (H h) *\<^sub>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, hide_lams) assms compatible_register1 register_preregister) + 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 \\<^sub>u b) = (B; A) (a \\<^sub>u b)\ for a b (* Without the "only:", we would not need the "apply subst", but that proof fails when instantiated in Classical.thy *) 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 \\<^sub>r G) (F' \\<^sub>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 \\<^sub>r G)\ \register (F' \\<^sub>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 \\<^sub>u b) \\<^sub>u (c \\<^sub>u d)) = ((a \\<^sub>u c) \\<^sub>u (b \\<^sub>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') \\<^sub>r (G;G')) o reorder o (\\. \ \\<^sub>u (c \\<^sub>u d))\ for c d have [simp]: \clinear (\ c d)\ for c d unfolding \_def by (auto intro: register_preregister) have \\ c d (a \\<^sub>u b) = (F \\<^sub>r G) (a \\<^sub>u b) *\<^sub>u (F' \\<^sub>r G') (c \\<^sub>u d)\ for a b c d unfolding \_def by (auto simp: register_pair_apply comp_tensor_op) then have \1: \\ c d \ = (F \\<^sub>r G) \ *\<^sub>u (F' \\<^sub>r G') (c \\<^sub>u d)\ for c d \ apply (rule_tac fun_cong[of _ _ \]) apply (rule tensor_extensionality) by auto have \\ c d (a \\<^sub>u b) = (F' \\<^sub>r G') (c \\<^sub>u d) *\<^sub>u (F \\<^sub>r G) (a \\<^sub>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' \\<^sub>r G') (c \\<^sub>u d) *\<^sub>u (F \\<^sub>r G) \\ for c d \ apply (rule_tac fun_cong[of _ _ \]) apply (rule tensor_extensionality) by auto from \1 \2 have \(F \\<^sub>r G) \ *\<^sub>u (F' \\<^sub>r G') \ = (F' \\<^sub>r G') \ *\<^sub>u (F \\<^sub>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 \\<^sub>u b) \\<^sub>u c) = (a \\<^sub>u (b \\<^sub>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 \\<^sub>u (b \\<^sub>u c)) = ((a \\<^sub>u b) \\<^sub>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 \\<^sub>u g) \\<^sub>u h) = ((F; G); H) ((f \\<^sub>u g) \\<^sub>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 \\<^sub>u g \\<^sub>u h) = (F; (G; H)) (f \\<^sub>u g \\<^sub>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 \\<^sub>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' \\<^sub>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 \\<^sub>r G) = inv F \\<^sub>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 \\<^sub>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 \\<^sub>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 \\<^sub>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 \\<^sub>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_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 (* val _ = \<^print> thms *) 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 "*\<^sub>u" 55) no_notation tensor_op (infixr "\\<^sub>u" 70) bundle register_notation begin notation register_tensor (infixr "\\<^sub>r" 70) notation register_pair ("'(_;_')") end bundle no_register_notation begin no_notation register_tensor (infixr "\\<^sub>r" 70) no_notation register_pair ("'(_;_')") end end diff --git a/thys/Registers/Misc.thy b/thys/Registers/Misc.thy --- a/thys/Registers/Misc.thy +++ b/thys/Registers/Misc.thy @@ -1,160 +1,161 @@ section \Miscellaneous facts\ text \This theory proves various facts that are not directly related to this developments but do not occur in the imported theories.\ theory Misc imports Complex_Bounded_Operators.Cblinfun_Code "HOL-Library.Z2" Jordan_Normal_Form.Matrix begin \ \Remove notation that collides with the notation we use\ no_notation Order.top ("\\") no_notation m_inv ("inv\ _" [81] 80) unbundle no_vec_syntax unbundle no_inner_syntax \ \Import notation from Bounded Operator and Jordan Normal Form libraries\ unbundle cblinfun_notation unbundle jnf_notation abbreviation "butterket i j \ butterfly (ket i) (ket j)" abbreviation "selfbutterket i \ butterfly (ket i) (ket i)" text \The following declares the ML antiquotation \<^verbatim>\fact\. In ML code, \<^verbatim>\@{fact f}\ for a theorem/fact name f is replaced by an ML string containing a printable(!) representation of fact. (I.e., if you print that string using writeln, the user can ctrl-click on it.) This is useful when constructing diagnostic messages in ML code, e.g., \<^verbatim>\"Use the theorem " ^ @{fact thmname} ^ "here."\\ setup \ML_Antiquotation.inline_embedded \<^binding>\fact\ ((Args.context -- Scan.lift Args.name_position) >> (fn (ctxt,namepos) => let val facts = Proof_Context.facts_of ctxt val fullname = Facts.check (Context.Proof ctxt) facts namepos val (markup, shortname) = Proof_Context.markup_extern_fact ctxt fullname val string = Markup.markups markup shortname in ML_Syntax.print_string string end )) \ instantiation bit :: enum begin definition "enum_bit = [0::bit,1]" definition "enum_all_bit P \ P (0::bit) \ P 1" definition "enum_ex_bit P \ P (0::bit) \ P 1" instance apply intro_classes apply (auto simp: enum_bit_def enum_all_bit_def enum_ex_bit_def) - by (metis bit_not_one_imp)+ + apply (metis bit_not_one_iff) + by (metis bit_not_zero_iff) end lemma card_bit[simp]: "CARD(bit) = 2" using card_2_iff' by force instantiation bit :: card_UNIV begin definition "finite_UNIV = Phantom(bit) True" definition "card_UNIV = Phantom(bit) 2" instance apply intro_classes by (simp_all add: finite_UNIV_bit_def card_UNIV_bit_def) end lemma mat_of_rows_list_carrier[simp]: "mat_of_rows_list n vs \ carrier_mat (length vs) n" "dim_row (mat_of_rows_list n vs) = length vs" "dim_col (mat_of_rows_list n vs) = n" unfolding mat_of_rows_list_def by auto lemma apply_id_cblinfun[simp]: \(*\<^sub>V) id_cblinfun = id\ by auto text \Overriding \\<^theory>\Complex_Bounded_Operators.Complex_Bounded_Linear_Function\.\<^term>\sandwich\. The latter is the same function but defined as a \<^typ>\(_,_) cblinfun\ which is less convenient for us.\ definition sandwich where \sandwich a b = a o\<^sub>C\<^sub>L b o\<^sub>C\<^sub>L a*\ lemma clinear_sandwich[simp]: \clinear (sandwich a)\ apply (rule clinearI) apply (simp add: bounded_cbilinear.add_left bounded_cbilinear_cblinfun_compose bounded_cbilinear.add_right sandwich_def) by (simp add: sandwich_def) lemma sandwich_id[simp]: \sandwich id_cblinfun = id\ by (auto simp: sandwich_def) lemma mat_of_cblinfun_sandwich: fixes a :: "(_::onb_enum, _::onb_enum) cblinfun" shows \mat_of_cblinfun (sandwich a b) = (let a' = mat_of_cblinfun a in a' * mat_of_cblinfun b * mat_adjoint a')\ by (simp add: mat_of_cblinfun_compose sandwich_def Let_def mat_of_cblinfun_adj) lemma prod_cases3' [cases type]: obtains (fields) a b c where "y = ((a, b), c)" by (cases y, case_tac a) blast lemma lift_cblinfun_comp: assumes \a o\<^sub>C\<^sub>L b = c\ shows \a o\<^sub>C\<^sub>L b = c\ and \a o\<^sub>C\<^sub>L (b o\<^sub>C\<^sub>L d) = c o\<^sub>C\<^sub>L d\ and \a *\<^sub>S (b *\<^sub>S S) = c *\<^sub>S S\ and \a *\<^sub>V (b *\<^sub>V x) = c *\<^sub>V x\ apply (fact assms) apply (simp add: assms cblinfun_assoc_left(1)) using assms cblinfun_assoc_left(2) apply force using assms by force text \We define the following abbreviations: \<^item> \mutually f (x\<^sub>1,x\<^sub>2,\,x\<^sub>n)\ expands to the conjuction of all \<^term>\f x\<^sub>i x\<^sub>j\ with \<^term>\i\j\. \<^item> \each f (x\<^sub>1,x\<^sub>2,\,x\<^sub>n)\ expands to the conjuction of all \<^term>\f x\<^sub>i\.\ syntax "_mutually" :: "'a \ args \ 'b" ("mutually _ '(_')") syntax "_mutually2" :: "'a \ 'b \ args \ args \ 'c" translations "mutually f (x)" => "CONST True" translations "mutually f (_args x y)" => "f x y \ f y x" translations "mutually f (_args x (_args x' xs))" => "_mutually2 f x (_args x' xs) (_args x' xs)" translations "_mutually2 f x y zs" => "f x y \ f y x \ _mutually f zs" translations "_mutually2 f x (_args y ys) zs" => "f x y \ f y x \ _mutually2 f x ys zs" syntax "_each" :: "'a \ args \ 'b" ("each _ '(_')") translations "each f (x)" => "f x" translations "_each f (_args x xs)" => "f x \ _each f xs" lemma enum_inj: assumes "i < CARD('a)" and "j < CARD('a)" shows "(Enum.enum ! i :: 'a::enum) = Enum.enum ! j \ i = j" using inj_on_nth[OF enum_distinct, where I=\{..] using assms by (auto dest: inj_onD simp flip: card_UNIV_length_enum) lemma [simp]: "dim_col (mat_adjoint m) = dim_row m" unfolding mat_adjoint_def by simp lemma [simp]: "dim_row (mat_adjoint m) = dim_col m" unfolding mat_adjoint_def by simp lemma invI: assumes \inj f\ assumes \x = f y\ shows \inv f x = y\ by (simp add: assms(1) assms(2)) instantiation prod :: (default,default) default begin definition \default_prod = (default, default)\ instance.. end instance bit :: default.. lemma surj_from_comp: assumes \surj (g o f)\ assumes \inj g\ shows \surj f\ by (metis assms(1) assms(2) f_inv_into_f fun.set_map inj_image_mem_iff iso_tuple_UNIV_I surj_iff_all) lemma double_exists: \(\x y. Q x y) \ (\z. Q (fst z) (snd z))\ by simp end diff --git a/thys/Registers/Pure_States.thy b/thys/Registers/Pure_States.thy --- a/thys/Registers/Pure_States.thy +++ b/thys/Registers/Pure_States.thy @@ -1,575 +1,577 @@ theory Pure_States imports Quantum_Extra2 "HOL-Eisbach.Eisbach" begin definition \pure_state_target_vector F \\<^sub>F = (if ket default \ range (cblinfun_apply (F (butterfly \\<^sub>F \\<^sub>F))) then ket default else (SOME \'. norm \' = 1 \ \' \ range (cblinfun_apply (F (butterfly \\<^sub>F \\<^sub>F)))))\ lemma pure_state_target_vector_eqI: assumes \F (butterfly \\<^sub>F \\<^sub>F) = G (butterfly \\<^sub>G \\<^sub>G)\ shows \pure_state_target_vector F \\<^sub>F = pure_state_target_vector G \\<^sub>G\ by (simp add: assms pure_state_target_vector_def) lemma pure_state_target_vector_ket_default: \pure_state_target_vector F \\<^sub>F = ket default\ if \ket default \ range (cblinfun_apply (F (butterfly \\<^sub>F \\<^sub>F)))\ by (simp add: pure_state_target_vector_def that) lemma assumes [simp]: \\\<^sub>F \ 0\ \register F\ shows pure_state_target_vector_in_range: \pure_state_target_vector F \\<^sub>F \ range ((*\<^sub>V) (F (selfbutter \\<^sub>F)))\ (is ?range) and pure_state_target_vector_norm: \norm (pure_state_target_vector F \\<^sub>F) = 1\ (is ?norm) proof - from assms have \selfbutter \\<^sub>F \ 0\ by (metis butterfly_0_right complex_vector.scale_zero_right inj_selfbutter_upto_phase) then have \F (selfbutter \\<^sub>F) \ 0\ using register_inj[OF \register F\, THEN injD, where y=0] by (auto simp: complex_vector.linear_0) then obtain \' where \': \F (selfbutter \\<^sub>F) *\<^sub>V \' \ 0\ by (meson cblinfun_eq_0_on_UNIV_span complex_vector.span_UNIV) have ex: \\\. norm \ = 1 \ \ \ range ((*\<^sub>V) (F (selfbutter \\<^sub>F)))\ apply (rule exI[of _ \(F (selfbutter \\<^sub>F) *\<^sub>V \') /\<^sub>C norm (F (selfbutter \\<^sub>F) *\<^sub>V \')\]) using \' apply (auto simp add: norm_inverse) by (metis cblinfun.scaleC_right rangeI) then show ?range by (metis (mono_tags, lifting) pure_state_target_vector_def verit_sko_ex') show ?norm apply (simp add: pure_state_target_vector_def) using ex by (metis (mono_tags, lifting) verit_sko_ex') qed lemma pure_state_target_vector_correct: assumes [simp]: \\ \ 0\ \register F\ shows \F (selfbutter \) *\<^sub>V pure_state_target_vector F \ \ 0\ proof - obtain \ where \: \F (selfbutter \) \ = pure_state_target_vector F \\ apply atomize_elim using pure_state_target_vector_in_range[OF assms] by (smt (verit, best) image_iff top_ccsubspace.rep_eq top_set_def) define n where \n = cinner \ \\ then have \n \ 0\ by auto have pure_state_target_vector_neq0: \pure_state_target_vector F \ \ 0\ using pure_state_target_vector_norm[OF assms] by auto have \F (selfbutter \) *\<^sub>V pure_state_target_vector F \ = F (selfbutter \) *\<^sub>V F (selfbutter \) *\<^sub>V \\ by (simp add: \) also have \\ = n *\<^sub>C F (selfbutter \) *\<^sub>V \\ by (simp flip: cblinfun_apply_cblinfun_compose add: register_mult register_scaleC n_def) also have \\ = n *\<^sub>C pure_state_target_vector F \\ by (simp add: \) also have \\ \ 0\ using pure_state_target_vector_neq0 \n \ 0\ by auto finally show ?thesis by - qed definition \pure_state' F \ \\<^sub>F = F (butterfly \ \\<^sub>F) *\<^sub>V pure_state_target_vector F \\<^sub>F\ abbreviation \pure_state F \ \ pure_state' F \ (ket default)\ nonterminal pure_tensor syntax "_pure_tensor" :: \'a \ 'b \ pure_tensor \ pure_tensor\ ("_ _ \\<^sub>p _" [1000, 0, 0] 1000) syntax "_pure_tensor2" :: \'a \ 'b \ 'c \ 'd \ pure_tensor\ ("_ _ \\<^sub>p _ _" [1000, 0, 1000, 0] 1000) syntax "_pure_tensor1" :: \'a \ 'b \ pure_tensor\ syntax "_pure_tensor_start" :: \pure_tensor \ 'a\ ("'(_')") translations "_pure_tensor2 F \ G \" \ "CONST pure_state (F; G) (\ \\<^sub>s \)" "_pure_tensor F \ (CONST pure_state G \)" \ "CONST pure_state (F; G) (\ \\<^sub>s \)" "_pure_tensor_start x" \ "x" "_pure_tensor_start (_pure_tensor2 F \ G \)" \ "CONST pure_state (F; G) (\ \\<^sub>s \)" "_pure_tensor F \ (_pure_tensor2 G \ H \)" \ "_pure_tensor2 F \ (G;H) (\ \\<^sub>s \)" term \(F \ \\<^sub>p G \ \\<^sub>p H z)\ term \pure_state (F; G) (a \\<^sub>s b)\ lemma register_pair_butterfly_tensor: \(F; G) (butterfly (a \\<^sub>s b) (c \\<^sub>s d)) = F (butterfly a c) o\<^sub>C\<^sub>L G (butterfly b d)\ if [simp]: \compatible F G\ by (auto simp: default_prod_def simp flip: tensor_ell2_ket tensor_butterfly register_pair_apply) lemma pure_state_eqI: assumes \F (selfbutter \\<^sub>F) = G (selfbutter \\<^sub>G)\ assumes \F (butterfly \ \\<^sub>F) = G (butterfly \ \\<^sub>G)\ shows \pure_state' F \ \\<^sub>F = pure_state' G \ \\<^sub>G\ proof - from assms(1) have \pure_state_target_vector F \\<^sub>F = pure_state_target_vector G \\<^sub>G\ by (rule pure_state_target_vector_eqI) with assms(2) show ?thesis unfolding pure_state'_def by simp qed definition \regular_register F \ register F \ (\a. (F; complement F) (selfbutterket default \\<^sub>o a) = selfbutterket default)\ lemma regular_registerI: assumes [simp]: \register F\ assumes [simp]: \complements F G\ assumes eq: \(F; G) (selfbutterket default \\<^sub>o a) = selfbutterket default\ shows \regular_register F\ proof - have [simp]: \compatible F G\ using assms by (simp add: complements_def) from \complements F G\ obtain I where cFI: \complement F o I = G\ and \iso_register I\ apply atomize_elim by (meson Laws_Complement_Quantum.complement_unique equivalent_registers_def equivalent_registers_sym) have \(F; complement F) (selfbutterket default \\<^sub>o I a) = (F; G) (selfbutterket default \\<^sub>o a)\ using cFI by (auto simp: register_pair_apply) also have \\ = selfbutterket default\ by (rule eq) finally show ?thesis unfolding regular_register_def by auto qed lemma regular_register_pair: assumes [simp]: \compatible F G\ assumes \regular_register F\ and \regular_register G\ shows \regular_register (F;G)\ proof - have [simp]: \bij (F;complement F)\ \bij (G;complement G)\ using assms(1) compatible_def complement_is_complement complements_def iso_register_bij by blast+ have [simp]: \bij ((F;G);complement (F;G))\ using assms(1) complement_is_complement complements_def iso_register_bij pair_is_register by blast have [simp]: \register F\ \register G\ using assms(1) unfolding compatible_def by auto obtain aF where [simp]: \inv (F;complement F) (selfbutterket default) = selfbutterket default \\<^sub>o aF\ by (metis assms(2) compatible_complement_right invI pair_is_register register_inj regular_register_def) obtain aG where [simp]: \inv (G;complement G) (selfbutterket default) = selfbutterket default \\<^sub>o aG\ by (metis assms(3) complement_is_complement complements_def inj_iff inv_f_f iso_register_inv_comp1 regular_register_def) define t1 where \t1 = inv ((F;G); complement (F;G)) (selfbutterket default)\ define t2 where \t2 = inv (F; (G; complement (F;G))) (selfbutterket default)\ define t3 where \t3 = inv (G; (F; complement (F;G))) (selfbutterket default)\ have \complements F (G; complement (F;G))\ apply (rule complements_complement_pair) by simp then have \equivalent_registers (complement F) (G; complement (F;G))\ using Laws_Complement_Quantum.complement_unique equivalent_registers_sym by blast then obtain I where [simp]: \iso_register I\ and I: \(G; complement (F;G)) = complement F o I\ by (metis equivalent_registers_def) then have [simp]: \register I\ by (meson iso_register_is_register) have [simp]: \bij (id \\<^sub>r I)\ by (rule iso_register_bij, simp) have [simp]: \inv (id \\<^sub>r I) = id \\<^sub>r inv I\ by auto have \t2 = (inv (id \\<^sub>r I) o inv (F;complement F)) (selfbutterket default)\ unfolding t2_def I apply (subst o_inv_distrib[symmetric]) by (auto simp: pair_o_tensor) also have \\ = (selfbutterket default \\<^sub>o inv I aF)\ apply auto by (metis \iso_register I\ id_def iso_register_def iso_register_inv register_id register_tensor_apply) finally have t2': \t2 = selfbutterket default \\<^sub>o inv I aF\ by simp have *: \complements G (F; complement (F;G))\ apply (rule complements_complement_pair') by simp then have [simp]: \compatible G (F; complement (F;G))\ using complements_def by blast from * have \equivalent_registers (complement G) (F; complement (F;G))\ using complement_unique equivalent_registers_sym by blast then obtain J where [simp]: \iso_register J\ and I: \(F; complement (F;G)) = complement G o J\ by (metis equivalent_registers_def) then have [simp]: \register J\ by (meson iso_register_is_register) have [simp]: \bij (id \\<^sub>r J)\ by (rule iso_register_bij, simp) have [simp]: \inv (id \\<^sub>r J) = id \\<^sub>r inv J\ by auto have \t3 = (inv (id \\<^sub>r J) o inv (G;complement G)) (selfbutterket default)\ unfolding t3_def I apply (subst o_inv_distrib[symmetric]) by (auto simp: pair_o_tensor) also have \\ = (selfbutterket default \\<^sub>o inv J aG)\ apply auto by (metis \iso_register J\ id_def iso_register_def iso_register_inv register_id register_tensor_apply) finally have t3': \t3 = selfbutterket default \\<^sub>o inv J aG\ by simp have *: \((F;G); complement (F;G)) o assoc' = (F; (G; complement (F;G)))\ apply (rule tensor_extensionality3) by (auto simp: register_pair_apply compatible_complement_pair1 compatible_complement_pair2) have t2_t1: \t2 = assoc t1\ unfolding t1_def t2_def *[symmetric] apply (subst o_inv_distrib) by auto have *: \((F;G); complement (F;G)) o (swap \\<^sub>r id) o assoc' = (G; (F; complement (F;G)))\ apply (rule tensor_extensionality3) apply (auto intro!: register_comp register_tensor_is_register pair_is_register complements_complement_pair simp: register_pair_apply compatible_complement_pair1) by (metis assms(1) cblinfun_assoc_left(1) swap_registers_left) have t3_t1: \t3 = assoc ((swap \\<^sub>r id) t1)\ unfolding t1_def t3_def *[symmetric] apply (subst o_inv_distrib) by (auto intro!: bij_comp simp: iso_register_bij o_inv_distrib) from \t2 = assoc t1\ \t3 = assoc ((swap \\<^sub>r id) t1)\ have *: \selfbutterket default \\<^sub>o inv J aG = assoc ((swap \\<^sub>r id) (assoc' (selfbutterket default \\<^sub>o inv I aF)))\ by (simp add: t2' t3') have \selfbutterket default \\<^sub>o swap (inv J aG) = (id \\<^sub>r swap) (selfbutterket default \\<^sub>o inv J aG)\ by auto also have \\ = ((id \\<^sub>r swap) o assoc o (swap \\<^sub>r id) o assoc') (selfbutterket default \\<^sub>o inv I aF)\ by (simp add: *) also have \\ = (assoc o swap) (selfbutterket default \\<^sub>o inv I aF)\ apply (rule fun_cong[where g=\assoc o swap\]) apply (intro tensor_extensionality3 register_comp register_tensor_is_register) by auto also have \\ = assoc (inv I aF \\<^sub>o selfbutterket default)\ by auto finally have *: \selfbutterket default \\<^sub>o swap (inv J aG) = assoc (inv I aF \\<^sub>o selfbutterket default)\ by - obtain c where *: \selfbutterket (default::'c) \\<^sub>o swap (inv J aG) = selfbutterket default \\<^sub>o c \\<^sub>o selfbutterket default\ apply atomize_elim apply (rule overlapping_tensor) using * unfolding assoc_ell2_sandwich sandwich_def by auto have \t1 = ((swap \\<^sub>r id) o assoc') t3\ by (simp add: t3_t1 register_tensor_distrib[unfolded o_def, THEN fun_cong] flip: id_def) also have \\ = ((swap \\<^sub>r id) o assoc' o (id \\<^sub>r swap)) (selfbutterket (default::'c) \\<^sub>o swap (inv J aG))\ unfolding t3' by auto also have \\ = ((swap \\<^sub>r id) o assoc' o (id \\<^sub>r swap)) (selfbutterket default \\<^sub>o c \\<^sub>o selfbutterket default)\ unfolding * by simp also have \\ = selfbutterket default \\<^sub>o c\ apply (simp del: tensor_butterfly) by (simp add: default_prod_def) finally have \t1 = selfbutterket default \\<^sub>o c\ by - then show ?thesis apply (auto intro!: exI[of _ c] simp: regular_register_def t1_def) by (metis \bij ((F;G);complement (F;G))\ bij_inv_eq_iff) qed lemma regular_register_comp: \regular_register (F o G)\ if \regular_register F\ \regular_register G\ proof - have [simp]: \register F\ \register G\ using regular_register_def that by blast+ from that obtain a where a: \(F; complement F) (selfbutterket default \\<^sub>o a) = selfbutterket default\ unfolding regular_register_def by metis from that obtain b where b: \(G; complement G) (selfbutterket default \\<^sub>o b) = selfbutterket default\ unfolding regular_register_def by metis have \complements (F o G) (complement F; F o complement G)\ by (simp add: complements_chain) then have \equivalent_registers (complement F; F o complement G) (complement (F o G))\ using complement_unique by blast then obtain J where [simp]: \iso_register J\ and 1: \(complement F; F o complement G) o J = (complement (F o G))\ using equivalent_registers_def by blast have [simp]: \register J\ by (simp add: iso_register_is_register) define c where \c = inv J (a \\<^sub>o b)\ have \((F o G); complement (F o G)) (selfbutterket default \\<^sub>o c) = ((F o G); (complement F; F o complement G)) (selfbutterket default \\<^sub>o J c)\ by (auto simp flip: 1 simp: register_pair_apply) also have \\ = ((F o (G; complement G); complement F) o assoc' o (id \\<^sub>r swap)) (selfbutterket default \\<^sub>o J c)\ apply (subst register_comp_pair[symmetric]) apply auto[2] apply (subst pair_o_assoc') apply auto[3] apply (subst pair_o_tensor) by auto also have \\ = ((F o (G; complement G); complement F) o assoc') (selfbutterket default \\<^sub>o swap (J c))\ by auto also have \\ = ((F o (G; complement G); complement F) o assoc') (selfbutterket default \\<^sub>o (b \\<^sub>o a))\ unfolding c_def apply (subst surj_f_inv_f[where f=J]) apply (meson \iso_register J\ bij_betw_inv_into_right iso_register_inv_comp1 iso_register_inv_comp2 iso_tuple_UNIV_I o_bij surj_iff_all) by auto also have \\ = (F \ (G;complement G);complement F) ((selfbutterket default \\<^sub>o b) \\<^sub>o a)\ by (simp add: assoc'_apply) also have \\ = (F; complement F) ((G;complement G) (selfbutterket default \\<^sub>o b) \\<^sub>o a)\ by (simp add: register_pair_apply') also have \\ = selfbutterket default\ by (auto simp: a b) finally have \(F \ G;complement (F \ G)) (selfbutterket default \\<^sub>o c) = selfbutterket default\ by - then show ?thesis using \register F\ \register G\ register_comp regular_register_def by blast qed lemma regular_iso_register: assumes \regular_register F\ assumes [register]: \iso_register F\ shows \F (selfbutterket default) = selfbutterket default\ proof - from assms(1) obtain a where a: \(F;complement F) (selfbutterket default \\<^sub>o a) = selfbutterket default\ using regular_register_def by blast let ?u = \empty_var :: (unit ell2 \\<^sub>C\<^sub>L unit ell2) \ _\ have \is_unit_register ?u\ and \is_unit_register (complement F)\ by auto then have \equivalent_registers (complement F) ?u\ using unit_register_unique by blast then obtain I where \iso_register I\ and \complement F = ?u o I\ by (metis \is_unit_register (complement F)\ equivalent_registers_def is_unit_register_empty_var unit_register_unique) have \selfbutterket default = (F; ?u o I) (selfbutterket default \\<^sub>o a)\ using \complement F = empty_var \ I\ a by presburger also have \\ = (F; ?u) (selfbutterket default \\<^sub>o I a)\ by (metis Laws_Quantum.register_pair_apply \complement F = empty_var \ I\ \equivalent_registers (complement F) empty_var\ assms(2) comp_apply complement_is_complement complements_def equivalent_complements iso_register_is_register) also have \\ = (F; ?u) (selfbutterket default \\<^sub>o (one_dim_iso (I a) *\<^sub>C id_cblinfun))\ by simp also have \\ = one_dim_iso (I a) *\<^sub>C (F; ?u) (selfbutterket default \\<^sub>o id_cblinfun)\ by (simp add: Axioms_Quantum.register_pair_apply empty_var_def iso_register_is_register) also have \\ = one_dim_iso (I a) *\<^sub>C F (selfbutterket default)\ by (auto simp: register_pair_apply iso_register_is_register simp del: id_cblinfun_eq_1) finally have F: \one_dim_iso (I a) *\<^sub>C F (selfbutterket default) = selfbutterket default\ by simp from F have \one_dim_iso (I a) \ (0::complex)\ by (metis butterfly_apply butterfly_scaleC_left complex_vector.scale_eq_0_iff id_cblinfun_eq_1 id_cblinfun_not_0 cinner_ket_same ket_nonzero one_dim_iso_of_one one_dim_iso_of_zero') have \selfbutterket default = one_dim_iso (I a) *\<^sub>C F (selfbutterket default)\ using F by simp also have \\ = one_dim_iso (I a) *\<^sub>C F (selfbutterket default o\<^sub>C\<^sub>L selfbutterket default)\ by auto also have \\ = one_dim_iso (I a) *\<^sub>C (F (selfbutterket default) o\<^sub>C\<^sub>L F (selfbutterket default))\ by (simp add: assms(2) iso_register_is_register register_mult) also have \\ = one_dim_iso (I a) *\<^sub>C ((selfbutterket default /\<^sub>C one_dim_iso (I a)) o\<^sub>C\<^sub>L (selfbutterket default /\<^sub>C one_dim_iso (I a)))\ by (metis (no_types, lifting) F \one_dim_iso (I a) \ 0\ complex_vector.scale_left_imp_eq inverse_1 left_inverse scaleC_scaleC zero_neq_one) also have \\ = one_dim_iso (I a) *\<^sub>C selfbutterket default\ by (smt (verit, best) butterfly_comp_butterfly calculation cblinfun_compose_scaleC_left cblinfun_compose_scaleC_right complex_vector.scale_cancel_left cinner_ket_same left_inverse scaleC_one scaleC_scaleC) finally have \one_dim_iso (I a) = (1::complex)\ by (metis butterfly_0_left butterfly_apply complex_vector.scale_cancel_right cinner_ket_same ket_nonzero scaleC_one) with F show \F (selfbutterket default) = selfbutterket default\ by simp qed lemma pure_state_nested: assumes [simp]: \compatible F G\ assumes \regular_register H\ assumes \iso_register H\ shows \pure_state (F;G) (pure_state H h \\<^sub>s g) = pure_state ((F o H);G) (h \\<^sub>s g)\ proof - note [[simproc del: Laws_Quantum.compatibility_warn]] have [simp]: \register H\ by (meson assms(3) iso_register_is_register) have [simp]: \H (selfbutterket default) = selfbutterket default\ apply (rule regular_iso_register) using assms by auto have 1: \pure_state_target_vector H (ket default) = ket default\ apply (rule pure_state_target_vector_ket_default) apply auto by (metis (no_types, lifting) cinner_ket_same rangeI scaleC_one) have \butterfly (pure_state H h) (ket default) = butterfly (H (butterfly h (ket default)) *\<^sub>V ket default) (ket default)\ by (simp add: pure_state'_def 1) also have \\ = H (butterfly h (ket default)) o\<^sub>C\<^sub>L selfbutterket default\ - by (metis (no_types, hide_lams) adj_cblinfun_compose butterfly_adjoint butterfly_comp_cblinfun double_adj) + by (metis (no_types, opaque_lifting) adj_cblinfun_compose butterfly_adjoint butterfly_comp_cblinfun double_adj) also have \\ = H (butterfly h (ket default)) o\<^sub>C\<^sub>L H (selfbutterket default)\ by simp also have \\ = H (butterfly h (ket default) o\<^sub>C\<^sub>L selfbutterket default)\ by (meson \register H\ register_mult) also have \\ = H (butterfly h (ket default))\ by auto finally have 2: \butterfly (pure_state H h) (ket default) = H (butterfly h (ket default))\ by simp show ?thesis apply (rule pure_state_eqI) using 1 2 by (auto simp: register_pair_butterfly_tensor compatible_ac_rules default_prod_def simp flip: tensor_ell2_ket) qed lemma state_apply1: assumes [register]: \compatible F G\ shows \F U *\<^sub>V (F \ \\<^sub>p G \) = (F (U \) \\<^sub>p G \)\ proof - have [register]: \compatible F G\ using assms(1) complements_def by blast have \F U *\<^sub>V (F \ \\<^sub>p G \) = (F;G) (U \\<^sub>o id_cblinfun) *\<^sub>V (F \ \\<^sub>p G \)\ apply (subst register_pair_apply) by auto also have \\ = (F (U \) \\<^sub>p G \)\ unfolding pure_state'_def by (auto simp: register_mult' cblinfun_comp_butterfly tensor_op_ell2) finally show ?thesis by - qed lemma Fst_regular[simp]: \regular_register Fst\ apply (rule regular_registerI[where a=\selfbutterket default\ and G=Snd]) by (auto simp: pair_Fst_Snd default_prod_def) lemma Snd_regular[simp]: \regular_register Snd\ apply (rule regular_registerI[where a=\selfbutterket default\ and G=Fst]) apply auto[2] apply (auto simp only: default_prod_def swap_apply simp flip: swap_def) by auto lemma id_regular[simp]: \regular_register id\ apply (rule regular_registerI[where G=unit_register and a=id_cblinfun]) by (auto simp: register_pair_apply) lemma swap_regular[simp]: \regular_register swap\ by (auto intro!: regular_register_pair simp: swap_def) lemma assoc_regular[simp]: \regular_register assoc\ by (auto intro!: regular_register_pair regular_register_comp simp: assoc_def) lemma assoc'_regular[simp]: \regular_register assoc'\ by (auto intro!: regular_register_pair regular_register_comp simp: assoc'_def) lemma cspan_pure_state': assumes \iso_register F\ assumes \cspan (g ` X) = UNIV\ assumes \_cond: \F (selfbutter \) *\<^sub>V pure_state_target_vector F \ \ 0\ shows \cspan ((\z. pure_state' F (g z) \) ` X) = UNIV\ proof - from iso_register_decomposition[of F] obtain U where [simp]: \unitary U\ and F: \F = sandwich U\ using assms(1) by blast define \' c where \\' = pure_state_target_vector F \\ and \c = cinner (U *\<^sub>V \) \'\ from \_cond have \c \ 0\ by (simp add: \'_def F sandwich_def c_def cinner_adj_right) have \cspan ((\z. pure_state' F (g z) \) ` X) = cspan ((\z. F (butterfly (g z) \) *\<^sub>V \') ` X)\ by (simp add: \'_def pure_state'_def) also have \\ = cspan ((\z. (butterfly (U *\<^sub>V g z) (U *\<^sub>V \)) *\<^sub>V \') ` X)\ by (simp add: F sandwich_def cinner_adj_right) also have \\ = cspan ((\z. c *\<^sub>C U *\<^sub>V g z) ` X)\ by (simp add: c_def) also have \\ = (\z. c *\<^sub>C U *\<^sub>V z) ` cspan (g ` X)\ apply (subst complex_vector.linear_span_image[symmetric]) by (auto simp: image_image) also have \\ = (\z. c *\<^sub>C U *\<^sub>V z) ` UNIV\ using assms(2) by presburger also have \\ = UNIV\ apply (rule surjI[where f=\\z. (U* *\<^sub>V z) /\<^sub>C c\]) using \c \ 0\ by (auto simp flip: cblinfun_apply_cblinfun_compose) finally show ?thesis by - qed lemma cspan_pure_state: assumes [simp]: \iso_register F\ assumes \cspan (g ` X) = UNIV\ shows \cspan ((\z. pure_state F (g z)) ` X) = UNIV\ apply (rule cspan_pure_state') using assms apply auto[2] apply (rule pure_state_target_vector_correct) by (auto simp: iso_register_is_register) lemma pure_state_bounded_clinear: assumes [register]: \compatible F G\ shows \bounded_clinear (\\. (F \ \\<^sub>p G \))\ proof - have [bounded_clinear]: \bounded_clinear (F;G)\ using assms pair_is_register register_bounded_clinear by blast show ?thesis unfolding pure_state'_def by (auto intro!: bounded_linear_intros) qed lemma pure_state_bounded_clinear_right: assumes [register]: \compatible F G\ shows \bounded_clinear (\\. (F \ \\<^sub>p G \))\ proof - have [bounded_clinear]: \bounded_clinear (F;G)\ using assms pair_is_register register_bounded_clinear by blast show ?thesis unfolding pure_state'_def by (auto intro!: bounded_linear_intros) qed lemma pure_state_clinear: assumes [register]: \compatible F G\ shows \clinear (\\. (F \ \\<^sub>p G \))\ using assms bounded_clinear.clinear pure_state_bounded_clinear by blast method pure_state_flatten_nested = (subst pure_state_nested, (auto; fail)[3])+ text \The following method \pure_state_eq\ tries to solve a equality where both sides are of the form \F\<^sub>1(\\<^sub>1) \\<^sub>p F\<^sub>2(\\<^sub>2) \\<^sub>p \ \\<^sub>p F\<^sub>n(\\<^sub>n)\ by reordering the registers and unfolding nested register pairs. (For the unfolding of nested pairs, it is necessary that the corresponding \<^term>\compatible F G\ facts are provable by the simplifier.) If the some of the pure states \<^term>\\\<^sub>i\ themselves are \\\<^sub>p\-tensors, they will be flattened if possible. (If all necessary conditions can be proven, such as \regular_register\ etc.) The method may either succeed, fail, or reduce the equality to a hopefully simpler one.\ method pure_state_eq = (pure_state_flatten_nested?, rule pure_state_eqI; auto simp: register_pair_butterfly_tensor compatible_ac_rules default_prod_def simp flip: tensor_ell2_ket) lemma example: fixes F :: \bit update \ 'c::{finite,default} update\ and G :: \bit update \ 'c update\ assumes [register]: \compatible F G\ shows \(F;G) CNOT o\<^sub>C\<^sub>L (G;F) CNOT o\<^sub>C\<^sub>L (F;G) CNOT = (F;G) swap_ell2\ proof - define Z where \Z = complement (F;G)\ then have [register]: \compatible Z F\ \compatible Z G\ using assms compatible_complement_pair1 compatible_complement_pair2 compatible_sym by blast+ have [simp]: \iso_register (F;(G;Z))\ using Z_def assms complements_complement_pair complements_def by blast have eq1: \((F;G) CNOT o\<^sub>C\<^sub>L (G;F) CNOT o\<^sub>C\<^sub>L (F;G) CNOT) *\<^sub>V (F(ket f) \\<^sub>p G(ket g) \\<^sub>p Z(ket z)) = (F;G) swap_ell2 *\<^sub>V (F(ket f) \\<^sub>p G(ket g) \\<^sub>p Z(ket z))\ for f g z proof - have \(F(ket f) \\<^sub>p G(ket g) \\<^sub>p Z(ket z)) = ((F;G) (ket f \\<^sub>s ket g) \\<^sub>p Z(ket z))\ by pure_state_eq also have \(F;G) CNOT *\<^sub>V \ = ((F;G) (ket f \\<^sub>s ket (g+f)) \\<^sub>p Z(ket z))\ apply (subst state_apply1) by auto also have \\ = ((G;F) (ket (g+f) \\<^sub>s ket f) \\<^sub>p Z(ket z))\ by pure_state_eq also have \(G;F) CNOT *\<^sub>V \ = ((G;F) (ket (g+f) \\<^sub>s ket g) \\<^sub>p Z ket z)\ apply (subst state_apply1) by auto also have \\ = ((F;G) (ket g \\<^sub>s ket (g+f)) \\<^sub>p Z ket z)\ by pure_state_eq also have \(F;G) CNOT *\<^sub>V \ = ((F;G) ket g \\<^sub>s ket f \\<^sub>p Z ket z)\ - apply (subst state_apply1) by auto + apply (subst state_apply1) + apply simp + using add_right_imp_eq by fastforce also have \\ = (F(ket g) \\<^sub>p G(ket f) \\<^sub>p Z(ket z))\ by pure_state_eq finally have 1: \((F;G) CNOT o\<^sub>C\<^sub>L (G;F) CNOT o\<^sub>C\<^sub>L (F;G) CNOT) *\<^sub>V (F(ket f) \\<^sub>p G(ket g) \\<^sub>p Z(ket z)) = (F(ket g) \\<^sub>p G(ket f) \\<^sub>p Z(ket z))\ by auto have \(F(ket f) \\<^sub>p G(ket g) \\<^sub>p Z(ket z)) = ((F;G) (ket f \\<^sub>s ket g) \\<^sub>p Z(ket z))\ by pure_state_eq also have \(F;G) swap_ell2 *\<^sub>V \ = ((F;G) (ket g \\<^sub>s ket f) \\<^sub>p Z(ket z))\ by (auto simp: state_apply1 swap_ell2_tensor simp del: tensor_ell2_ket) also have \\ = (F(ket g) \\<^sub>p G(ket f) \\<^sub>p Z(ket z))\ by pure_state_eq finally have 2: \(F;G) swap_ell2 *\<^sub>V (F(ket f) \\<^sub>p G(ket g) \\<^sub>p Z(ket z)) = (F(ket g) \\<^sub>p G(ket f) \\<^sub>p Z(ket z))\ by - from 1 2 show ?thesis by simp qed then have eq1: \((F;G) CNOT o\<^sub>C\<^sub>L (G;F) CNOT o\<^sub>C\<^sub>L (F;G) CNOT) *\<^sub>V \ = (F;G) swap_ell2 *\<^sub>V \\ if \\ \ {(F(ket f) \\<^sub>p G(ket g) \\<^sub>p Z(ket z))| f g z. True}\ for \ using that by auto moreover have \cspan {(F(ket f) \\<^sub>p G(ket g) \\<^sub>p Z(ket z))| f g z. True} = UNIV\ apply (simp only: double_exists setcompr_eq_image full_SetCompr_eq) apply simp apply (rule cspan_pure_state) by auto ultimately show ?thesis using cblinfun_eq_on_UNIV_span by blast qed end diff --git a/thys/Registers/Quantum.thy b/thys/Registers/Quantum.thy --- a/thys/Registers/Quantum.thy +++ b/thys/Registers/Quantum.thy @@ -1,132 +1,142 @@ section \Quantum mechanics basics\ theory Quantum imports Finite_Tensor_Product "HOL-Library.Z2" Jordan_Normal_Form.Matrix_Impl Real_Impl.Real_Impl "HOL-Library.Code_Target_Numeral" begin type_synonym ('a,'b) matrix = \('a ell2, 'b ell2) cblinfun\ subsection \Basic quantum states\ subsubsection \EPR pair\ definition "vector_\00 = vec_of_list [ 1/sqrt 2::complex, 0, 0, 1/sqrt 2 ]" definition \00 :: \(bit\bit) ell2\ where [code del]: "\00 = basis_enum_of_vec vector_\00" lemma vec_of_basis_enum_\00[simp]: "vec_of_basis_enum \00 = vector_\00" by (auto simp add: \00_def vector_\00_def) lemma vec_of_ell2_\00[simp, code]: "vec_of_ell2 \00 = vector_\00" by (simp add: vec_of_ell2_def) lemma norm_\00[simp]: "norm \00 = 1" by eval subsubsection \Ket plus\ definition "vector_ketplus = vec_of_list [ 1/sqrt 2::complex, 1/sqrt 2 ]" definition ketplus :: \bit ell2\ ("|+\") where [code del]: \ketplus = basis_enum_of_vec vector_ketplus\ lemma vec_of_basis_enum_ketplus[simp]: "vec_of_basis_enum ketplus = vector_ketplus" by (auto simp add: ketplus_def vector_ketplus_def) lemma vec_of_ell2_ketplus[simp, code]: "vec_of_ell2 ketplus = vector_ketplus" by (simp add: vec_of_ell2_def) subsection \Basic quantum gates\ subsubsection \Pauli X\ definition "matrix_pauliX = mat_of_rows_list 2 [ [0::complex, 1], [1, 0] ]" definition pauliX :: \(bit, bit) matrix\ where [code del]: "pauliX = cblinfun_of_mat matrix_pauliX" lemma [simp, code]: "mat_of_cblinfun pauliX = matrix_pauliX" apply (auto simp add: pauliX_def matrix_pauliX_def) apply (subst cblinfun_of_mat_inverse) by (auto) +derive (eq) ceq bit + +instantiation bit :: ccompare begin +definition "CCOMPARE(bit) = Some (\b1 b2. case (b1, b2) of (0, 0) \ order.Eq | (0, 1) \ order.Lt | (1, 0) \ order.Gt | (1, 1) \ order.Eq)" +instance + by intro_classes(unfold_locales; auto simp add: ccompare_bit_def split!: bit.splits) +end + +derive (dlist) set_impl bit + lemma pauliX_adjoint[simp]: "pauliX* = pauliX" by eval lemma pauliXX[simp]: "pauliX o\<^sub>C\<^sub>L pauliX = id_cblinfun" by eval subsubsection \Pauli Z\ definition "matrix_pauliZ = mat_of_rows_list 2 [ [1::complex, 0], [0, -1] ]" definition pauliZ :: \(bit, bit) matrix\ where [code del]: "pauliZ = cblinfun_of_mat matrix_pauliZ" lemma [simp, code]: "mat_of_cblinfun pauliZ = matrix_pauliZ" apply (auto simp add: pauliZ_def matrix_pauliZ_def) apply (subst cblinfun_of_mat_inverse) by (auto) lemma pauliZ_adjoint[simp]: "pauliZ* = pauliZ" by eval lemma pauliZZ[simp]: "pauliZ o\<^sub>C\<^sub>L pauliZ = id_cblinfun" by eval subsubsection Hadamard definition "matrix_hadamard = mat_of_rows_list 2 [ [1/sqrt 2::complex, 1/sqrt 2], [1/sqrt 2, -1/sqrt 2] ]" definition hadamard :: \(bit,bit) matrix\ where [code del]: "hadamard = cblinfun_of_mat matrix_hadamard" lemma [simp, code]: "mat_of_cblinfun hadamard = matrix_hadamard" apply (auto simp add: hadamard_def matrix_hadamard_def) apply (subst cblinfun_of_mat_inverse) by (auto) lemma hada_adj[simp]: "hadamard* = hadamard" by eval subsubsection CNOT definition "matrix_CNOT = mat_of_rows_list 4 [ [1::complex,0,0,0], [0,1,0,0], [0,0,0,1], [0,0,1,0] ]" definition CNOT :: \(bit*bit, bit*bit) matrix\ where [code del]: "CNOT = cblinfun_of_mat matrix_CNOT" lemma [simp, code]: "mat_of_cblinfun CNOT = matrix_CNOT" apply (auto simp add: CNOT_def matrix_CNOT_def) apply (subst cblinfun_of_mat_inverse) by (auto) lemma [simp]: "CNOT* = CNOT" by eval lemma cnot_apply[simp]: \CNOT *\<^sub>V ket (i,j) = ket (i,j+i)\ apply (rule spec[where x=i], rule spec[where x=j]) by eval subsubsection \Qubit swap\ definition "matrix_Uswap = mat_of_rows_list 4 [ [1::complex, 0, 0, 0], [0,0,1,0], [0,1,0,0], [0,0,0,1] ]" definition Uswap :: \(bit\bit, bit\bit) matrix\ where [code del]: \Uswap = cblinfun_of_mat matrix_Uswap\ lemma mat_of_cblinfun_Uswap[simp, code]: "mat_of_cblinfun Uswap = matrix_Uswap" apply (auto simp add: Uswap_def matrix_Uswap_def) apply (subst cblinfun_of_mat_inverse) by (auto) lemma dim_col_Uswap[simp]: "dim_col matrix_Uswap = 4" unfolding matrix_Uswap_def by simp lemma dim_row_Uswap[simp]: "dim_row matrix_Uswap = 4" unfolding matrix_Uswap_def by simp lemma Uswap_adjoint[simp]: "Uswap* = Uswap" by eval lemma Uswap_involution[simp]: "Uswap o\<^sub>C\<^sub>L Uswap = id_cblinfun" by eval lemma unitary_Uswap[simp]: "unitary Uswap" unfolding unitary_def by simp lemma Uswap_apply[simp]: \Uswap *\<^sub>V s \\<^sub>s t = t \\<^sub>s s\ apply (rule clinear_equal_ket[where f=\\s. Uswap *\<^sub>V s \\<^sub>s t\, THEN fun_cong]) apply (simp add: cblinfun.add_right clinearI tensor_ell2_add1 tensor_ell2_scaleC1) apply (simp add: clinear_tensor_ell21) apply (rule clinear_equal_ket[where f=\\t. Uswap *\<^sub>V _ \\<^sub>s t\, THEN fun_cong]) apply (simp add: cblinfun.add_right clinearI tensor_ell2_add2 tensor_ell2_scaleC2) apply (simp add: clinear_tensor_ell22) apply (rule basis_enum_eq_vec_of_basis_enumI) apply (simp add: mat_of_cblinfun_cblinfun_apply vec_of_basis_enum_ket) by (case_tac i; case_tac ia; hypsubst_thin; normalization) end