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

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

lemma is_unit_register_empty_var[register]: ‹is_unit_register empty_var›
proof -
  have [simp]: ‹register empty_var›
    unfolding register_def empty_var_def
    by (simp add: clinearI scaleC_left.add)
  have [simp]: ‹compatible empty_var id›
    by (auto intro!: compatibleI simp: empty_var_def)
  have [simp]: ‹iso_register (empty_var;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 :: (type, type) default ..

end