Theory Energy_Games

(* License: LGPL *)

section ‹Energy Games›

theory Energy_Games
  imports Main
begin

text ‹
  Energy games are the foundation for the weak spectroscopy game.
  We introduce them through a recursive definition of attacker's winning budgets in energy reachability games.
›

subsection ‹Fundamentals›

type_synonym 'energy update = ‹'energy ⇒ 'energy option›

text ‹An energy game is played by two players on a directed graph labeled by energy updates.
These updates represent the costs of choosing a certain move, in our case, for the attacker.›
locale energy_game =
fixes
  weight_opt :: ‹'gstate ⇒ 'gstate ⇒ 'energy update option› and
  defender :: ‹'gstate ⇒ bool› and
  ord:: ‹'energy ⇒ 'energy ⇒ bool›
assumes
  antisim: ‹⋀e e'. (ord e e') ⟹ (ord e' e) ⟹ e = e'› and
  monotonicity: ‹⋀g g' e e' eu eu'.
    weight_opt g g' ≠ None ⟹ the (weight_opt g g') e = Some eu
    ⟹ the (weight_opt g g') e' = Some eu' ⟹ ord e e' ⟹ ord eu eu'› and
  defender_win_min: ‹⋀g g' e e'. ord e e' ⟹ weight_opt g g' ≠ None
    ⟹ the (weight_opt g g') e' = None ⟹ the (weight_opt g g') e = None›
begin

abbreviation attacker :: ‹'gstate ⇒ bool› where
  ‹attacker p ≡ ¬ defender p›

abbreviation moves :: ‹'gstate ⇒ 'gstate ⇒ bool› (infix ‹↣› 70) where
  ‹g1 ↣ g2 ≡ weight_opt g1 g2 ≠ None›

abbreviation weighted_move
  :: ‹'gstate ⇒ 'energy update ⇒ 'gstate ⇒  bool› (‹_ ↣wgt _ _› [60,60,60] 70) where
  ‹weighted_move g1 u g2 ≡ g1 ↣ g2 ∧ (the (weight_opt g1 g2) = u)›

abbreviation ‹weight g1 g2 ≡ the (weight_opt g1 g2)›

abbreviation ‹updated g g' e ≡ the (weight g g' e)›

subsection ‹Winning Budgets›

text ‹The attacker wins a game if and only if they manage to force the defender to get stuck before
running out of energy.›

inductive attacker_wins:: ‹'energy ⇒ 'gstate ⇒ bool› where
  Attack: ‹attacker_wins e g› if
    ‹attacker g› ‹g ↣ g'› ‹weight g g' e = Some e'› ‹attacker_wins e' g'› |
  Defense: ‹attacker_wins e g› if
    ‹defender g› ‹∀g'. (g ↣ g') ⟶ (∃e'. weight g g' e = Some e' ∧ attacker_wins e' g')›

lemma attacker_wins_Ga_with_id_step:
  assumes ‹attacker_wins e g'› ‹g ↣wgt Some g'› ‹attacker g›
  shows ‹attacker_wins e g›
  using assms by (metis attacker_wins.simps)

text ‹If from a certain starting position ‹g› a game is won by the attacker with some energy ‹e› (i.e. ‹e› is in the winning budget of ‹g›), then the game is also won by the attacker with more energy.›

lemma win_a_upwards_closure:
  assumes
    ‹attacker_wins e g›
    ‹ord e e'›
  shows
    ‹attacker_wins e' g›
using assms proof (induct arbitrary: e' rule: attacker_wins.induct)
  case (Attack g g' e eu e')
  with defender_win_min obtain eu' where ‹weight g g' e' = Some eu'› by fastforce
  then show ?case
    using Attack monotonicity attacker_wins.simps by blast
next
  case (Defense g e)
  with defender_win_min have ‹∀g'. g ↣ g' ⟶ (∃eu'. weight g g' e' = Some eu')› by fastforce
  then show ?case
    using Defense attacker_wins.Defense monotonicity by meson
qed

end ― ‹context ‹energy_game››

end