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