Theory Silent_Step_Spectroscopy

subsection ‹Correctness Theorem›

theory Silent_Step_Spectroscopy
  imports
    Distinction_Implies_Winning_Budgets
    Strategy_Formulas
begin

context weak_spectroscopy_game
begin

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 φ_spec:
    ‹distinguishes_from φ p Q› ‹expressiveness_price φ ≤ e›
    by blast
  from distinction_implies_winning_budgets φ_spec(1) have
    ‹attacker_wins (expressiveness_price φ) (Attacker_Immediate p Q)› .
  thus ‹attacker_wins e (Attacker_Immediate p Q)›
    using win_a_upwards_closure φ_spec(2) 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›
    by blast
  thus ‹∃φ. distinguishes_from φ p Q ∧ expressiveness_price φ ≤ e›
    using strategy_formulas_distinguish by fastforce
qed

proposition attacker_subet_wins:
  assumes
    ‹attacker_wins e (Attacker_Immediate p Q)›
    ‹Q' ⊆ Q›
  shows
    ‹attacker_wins e (Attacker_Immediate p Q')›
  using assms spectroscopy_game_correctness
  unfolding distinguishes_from_def subset_iff
  by meson

end (* context weak_spectroscopy_game *)

end