Theory Quantum_Extra2

section ‹More derived facts about quantum registers›

text ‹This theory contains some derived facts that cannot be placed in theory ‹Quantum_Extra› 
      because they depend on ‹Laws_Complement_Quantum›.›

theory Quantum_Extra2
  imports
    Laws_Complement_Quantum
    Quantum
begin

unbundle register_syntax

definition empty_var :: ‹'a::{CARD_1,enum} update ⇒ 'b update› where
  "empty_var a = one_dim_iso a *⇩C id_cblinfun"

lemma is_unit_register_empty_var[register]: ‹is_unit_register empty_var› (is ‹is_unit_register ?e›)
proof -
  note continuous_map_compose[trans]
  have ‹continuous_map weak_star_topology euclidean (id :: 'a update ⇒ _)›
    by simp
  also have ‹continuous_map euclidean euclidean one_dim_iso›
    by (simp add: clinear_continuous_at continuous_at_imp_continuous_on)
  also have ‹continuous_map euclidean euclidean (λa. a *⇩C id_cblinfun)›
    by (simp add: continuous_at_imp_continuous_on)
  also have ‹continuous_map euclidean weak_star_topology (id :: 'b update ⇒ _)›
    by (metis comp_id fun.map_ident weak_star_topology_weaker_than_euclidean)
  finally have ‹continuous_map weak_star_topology weak_star_topology (λa :: 'a update. one_dim_iso a *⇩C id_cblinfun :: 'b update)›
    by (simp add: o_def)
  then have [simp]: ‹register ?e›
    unfolding register_def empty_var_def
    by (simp add: clinearI scaleC_left.add)
  have [simp]: ‹compatible ?e id›
    by (auto intro!: compatibleI simp: empty_var_def)
  have [simp]: ‹iso_register (?e; id)›
    by (auto intro!: same_range_equivalent range_eqI[where x=‹id_cblinfun ⊗⇩o _›] 
        simp del: id_cblinfun_eq_1 simp flip: iso_register_equivalent_id simp: register_pair_apply)
  show ?thesis
    by (auto intro!: complementsI simp: is_unit_register_def)
qed

instance complement_domain_simple :: (type, type) default ..

unbundle no register_syntax

end