Theory Energy_Games

text ‹\newpage›
section ‹Energy Games›

theory Energy_Games
  imports Main Misc
begin

text‹In this theory, we introduce energy games and give basic definitions such as winning budgets.
Energy games are the foundation for the later introduced weak spectroscopy game, which is an
energy game itself, characterizing equivalence problems. \label{energy games}›

subsection ‹Fundamentals›
text‹We use an abstract concept of energies and only later consider eight-dimensional energy games.
Through our later given definition of energies as a data type, we obtain certain
properties that we enforce for all energy games. We therefore assume that an energy game
has a partial order on energies such that all updates are monotonic and have sink where the defender wins.›

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

text‹An energy game is played by two players on a directed graph labelled by energy updates.
These updates represent the costs of choosing a certain move.
Since we will only consider cases in which the attacker's moves may actually have non-zero costs, only they can run
out of energy. This is the case when the energy level reaches the ‹defender_win_level›.
In contrast to other definitions of games, we do not fix a starting position.›
locale energy_game =
fixes
  weight_opt :: ‹'gstate ⇒ 'gstate ⇒ 'energy update option› and
  defender :: ‹'gstate ⇒ bool› (‹Gd›) 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

text‹In the following, we introduce some abbreviations for attacker positions and moves.›

abbreviation attacker :: ‹'gstate ⇒ bool› (‹Ga›) where ‹Ga p ≡ ¬ Gd 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)›

subsubsection ‹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. The needed amount of energy is described by winning budgets: ‹e› is in the
winning budget of ‹g› if and only if there exists a winning strategy for the attacker when starting in ‹g›
with energy ‹e›. In more detail, this yields the following definition:

\begin{itemize}
  \item If ‹g› is an attacker position and ‹e› is not the ‹defender_win_level› then ‹e› is in the winning budget
  of ‹g› if and only if there exists a position ‹g'› the attacker can move to. In other words, if the updated energy
  level is in the winning budget of ‹g'›. (This corresponds to the second case of the following definition.)
  \item  If ‹g› is a defender position and ‹e› is not the ‹defender_win_level› then ‹e› is in the winning budget
   of ‹g› if and only if for all successors ‹g'› the accordingly updated energy is in the winning
   budget of ‹g'›. In other words, if the attacker will win from every successor the defender can move to.
\end{itemize}
›

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

lemma %invisible attacker_wins_GaE:
  assumes ‹attacker_wins e g› and ‹Ga g›
  shows ‹∃g'. ((g ↣ g') ∧ (attacker_wins (the (weight g g' e)) g'))›
  using assms attacker_wins.simps option.sel by metis

lemma %invisible attacker_wins_Ga:
  assumes ‹u e = Some e'› ‹attacker_wins e' g'› ‹g ↣wgt u g'› ‹Ga g›
  shows ‹attacker_wins e g›
  using assms attacker_wins.simps by blast

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

lemma %invisible attacker_wins_Gd:
  fixes update
  assumes ‹Gd g›
  ‹⋀g'. g ↣ g' ⟹ weight g g' = update›
  ‹⋀g'. g ↣ g' ⟹ ∃e'. update e = Some e' ∧ attacker_wins e' g'›
shows ‹attacker_wins e g› using assms attacker_wins.Defense by metis

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.
This is proven using the inductive definition of winning budgets and the given properties of the partial order ‹ord›.›

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_Ga 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 (*End of context energy_game*)

end