Theory Silent_Step_Spectroscopy

(* License: LGPL *)

subsection ‹Correctness Theorem›

theory Silent_Step_Spectroscopy
  imports
    Distinction_Implies_Winning_Budgets
    Strategy_Formulas
begin


text ‹
  We now only combine the results of ‹Distinction_Implies_Winning_Budgets› and ‹Strategy_Formulas› to obtain the main characterization theorem of the weak spectroscopy game characterizing a whole spectrum of weak equivalences.
›

context lts_tau
begin

theorem spectroscopy_game_correctness:
  fixes e p Q
  shows ‹(∃φ. distinguishes_from φ p Q ∧ expressiveness_price φ ≤ e)
       ⟷ spectro_att_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
    ‹spectro_att_wins (expressiveness_price φ) (Attacker_Immediate p Q)› .
  thus ‹spectro_att_wins e (Attacker_Immediate p Q)›
    using weak_spectroscopy_game.win_a_upwards_closure φ_spec(2) by simp
next
  assume ‹spectro_att_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

text ‹An implicit result of the correctness theorem is that attacker wins on bigger ‹Q› imply wins on smaller ones.›

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

end

end