Theory Definition_Pure_O2H

theory Definition_Pure_O2H

imports Definition_O2H 
  Run_Adversary

begin

unbundle cblinfun_syntax
unbundle lattice_syntax
unbundle register_syntax

subsection ‹Locale for the pure O2H setting›

text ‹For the pure state case, we define a separate locale for the pure one-way to hiding lemma.›

locale pure_o2h = o2h_setting "TYPE('x)" "TYPE('y::group_add)" "TYPE('mem)" "TYPE('l)" +
  ― ‹We fix the oracle function ‹H›, a subset of the oracle domain ‹S› and the sequence of 
  operations the adversary $A$ undertakes in the function ‹UA›.›
  fixes H :: ‹'x ⇒ ('y::group_add)› 
    and S :: ‹'x ⇒ bool› 
    and UA :: ‹nat ⇒ 'mem update› 

― ‹All operations by the adversary $A$ must be isometries.›
assumes norm_UA: ‹⋀i. i<d+1 ⟹ norm (UA i) ≤ 1› 
begin

text ‹Given the initial register state ‹init›, ‹run_A› returns the register state after 
performing the algorithm describing the adversary $A$.›
definition ‹run_A = run_pure_adv d UA (λ_. id_cblinfun::'mem update) init X Y H›
  (* An adversary run looks like this:
  init ⇒ UA ⇒ Uquery H ⇒ UA ⇒ Uquery H ⇒ … ⇒ Uquery H ⇒ UA *)

lemma norm_UA_Suc: "n <d ⟹ norm (UA (Suc n)) ≤ 1"
  by (simp add: norm_UA)

lemma norm_UA_0_init:
  "norm (UA 0 *⇩V init) ≤ 1"
  using norm_UA[of 0] norm_init d_gr_0 
  by (metis basic_trans_rules(23) mult_cancel_left2 norm_cblinfun semiring_norm(174) zero_less_Suc)

lemma tensor_proj_UA_tensor_commute:
  "(id_cblinfun ⊗⇩o proj_classical_set A) o⇩C⇩L (UA (Suc n) ⊗⇩o id_cblinfun) =
   (UA (Suc n) ⊗⇩o id_cblinfun) o⇩C⇩L (id_cblinfun ⊗⇩o proj_classical_set A)"
  by (auto intro!: tensor_ell2_extensionality simp add: tensor_op_ell2)


end

unbundle no cblinfun_syntax
unbundle no lattice_syntax
unbundle no register_syntax

end