Theory Silent_Step_Spectroscopy

subsection ‹Correctness Theorem›

theory Silent_Step_Spectroscopy
  imports
    Distinction_Implies_Winning_Budgets
    Strategy_Formulas
begin

context weak_spectroscopy_game
begin

text ‹\label{th1}›

theorem spectroscopy_game_correctness:
  fixes e p Q
  shows ‹(∃φ. distinguishes_from φ p Q ∧ expressiveness_price φ ≤ e)
       = (attacker_wins e (Attacker_Immediate p Q))›
proof
  assume ‹∃φ. distinguishes_from φ p Q ∧ expressiveness_price φ ≤ e›
  then obtain φ where
    ‹distinguishes_from φ p Q› and le: ‹expressiveness_price φ ≤ e›
    unfolding 𝒪_def by blast
  from distinction_implies_winning_budgets this(1)
    have budget: ‹attacker_wins (expressiveness_price φ) (Attacker_Immediate p Q)› .
  thus ‹attacker_wins e (Attacker_Immediate p Q)› using win_a_upwards_closure le by simp
next
  assume ‹attacker_wins e (Attacker_Immediate p Q)›
  with winning_budget_implies_strategy_formula have
    ‹∃φ. strategy_formula (Attacker_Immediate p Q) e φ ∧ expressiveness_price φ ≤ e›
    by force
  hence ‹∃φ. strategy_formula (Attacker_Immediate p Q) e φ ∧ expressiveness_price φ ≤ e›
    unfolding 𝒪_def by blast
  thus ‹∃φ. distinguishes_from φ p Q ∧ expressiveness_price φ ≤ e›
    using strategy_formulas_distinguish by fastforce
qed

end (* context weak_spectroscopy_game *)

end