Theory Natural_Galois_Energy_Game

section ‹Galois Energy Games over Naturals›

theory Natural_Galois_Energy_Game
  imports Energy_Game Energy_Order Decidability Update
begin

text‹We now define Galois energy games over vectors of naturals with the component-wise order. 
We formalise this in this theory as an ‹energy_game› with a fixed dimension. In particular, we assume all updates to have an upward-closed domain (as ‹domain_upw_closed›) and be length-preserving (as ‹upd_preserves_length›). 
We assume the latter for the inversion of updates too (as ‹inv_preserves_length›) and assume that the inversion of an update is a total mapping from energies to the domain of the update (as ‹domain_inv›). 
(This corresponds to section 4.2 in the preprint~\cite{preprint}.)›

locale natural_galois_energy_game = energy_game attacker weight application
  for   attacker ::  "'position set" and 
        weight :: "'position ⇒ 'position ⇒ 'label option" and
        application :: "'label ⇒ energy ⇒ energy option" and
        inverse_application :: "'label ⇒ energy ⇒ energy option"
+ 
  fixes dimension :: "nat"
  assumes
    domain_upw_closed: "⋀p p' e e'. weight p p' ≠ None ⟹ e e≤ e' ⟹ application (the (weight p p')) e ≠ None ⟹ application (the (weight p p')) e' ≠ None"
    and updgalois: "⋀p p' e. weight p p' ≠ None ⟹ application (the (weight p p')) e ≠ None ⟹ length (the (application (the (weight p p')) e)) = length e"
    and inv_preserves_length: "⋀p p' e. weight p p' ≠ None ⟹ length e = dimension ⟹ length (the (inverse_application (the (weight p p')) e)) = length e"
    and domain_inv: "⋀p p' e. weight p p' ≠ None ⟹ length e = dimension ⟹ (inverse_application (the (weight p p')) e) ≠ None ∧ application (the (weight p p')) (the (inverse_application (the (weight p p')) e)) ≠ None"
    and galois: "⋀p p' e e'. weight p p' ≠ None ⟹ application (the (weight p p')) e' ≠ None ⟹ length e = dimension ⟹ length e' = dimension ⟹ (the (inverse_application (the (weight p p')) e)) e≤ e' = e e≤ (the (application (the (weight p p')) e'))"

sublocale natural_galois_energy_game ⊆ galois_energy_game attacker weight application inverse_application "{e::energy. length e = dimension}" energy_leq "λs. energy_sup dimension s"
proof
  show "wqo_on energy_leq {e::energy. length e = dimension}" 
    using Energy_Order.energy_leq_wqo . 

  show "⋀ set s'. set ⊆ {e::energy. length e = dimension} ⟹ finite set ⟹ energy_sup dimension set ∈ {e::energy. length e = dimension} ∧ (∀s. s ∈ set ⟶ energy_leq s (energy_sup dimension set)) ∧ (s' ∈ {e::energy. length e = dimension} ∧ (∀s. s ∈ set ⟶ energy_leq s s') ⟶ energy_leq (energy_sup dimension set) s')"
  proof-
    fix set
    show "⋀s'. set ⊆ {e::energy. length e = dimension} ⟹ finite set ⟹ energy_sup dimension set ∈ {e::energy. length e = dimension} ∧ (∀s. s ∈ set ⟶ energy_leq s (energy_sup dimension set)) ∧ (s' ∈ {e::energy. length e = dimension} ∧ (∀s. s ∈ set ⟶ energy_leq s s') ⟶ energy_leq (energy_sup dimension set) s')"
    proof
      fix s'
      assume "set ⊆ {e. length e = dimension}" and "finite set"
      show "energy_sup dimension set ∈ {e. length e = dimension}"
        unfolding energy_sup_def
        by simp 
      show "(∀s. s ∈ set ⟶ energy_leq s (energy_sup dimension set)) ∧ (s' ∈ {e::energy. length e = dimension} ∧ (∀s. s ∈ set ⟶ energy_leq s s') ⟶ energy_leq (energy_sup dimension set) s')"
      proof
        show "(∀s. s ∈ set ⟶ s e≤ energy_sup dimension set)"
          using energy_sup_is_sup(1) ‹set ⊆ {e. length e = dimension}›
          by auto
        show "s' ∈ {e. length e = dimension} ∧ (∀s. s ∈ set ⟶ s e≤ s') ⟶ energy_sup dimension set e≤ s' "
        proof
          assume "s' ∈ {e. length e = dimension} ∧ (∀s. s ∈ set ⟶ s e≤ s')"
          show "energy_sup dimension set e≤ s'"
          proof(rule energy_sup_is_sup(2))
            show "⋀a. a ∈ set ⟹ a e≤ s'"
              by (simp add: ‹s' ∈ {e. length e = dimension} ∧ (∀s. s ∈ set ⟶ s e≤ s')›) 
            show "length s' = dimension"
              using ‹s' ∈ {e. length e = dimension} ∧ (∀s. s ∈ set ⟶ s e≤ s')› by auto
          qed
        qed
      qed
    qed
  qed

  show "⋀e e'. e ∈ {e::energy. length e = dimension} ⟹ e e≤ e' ⟹ e' ∈ {e::energy. length e = dimension}"
    unfolding Energy_Order.energy_leq_def by simp

  show "⋀p p' e. weight p p' ≠ None ⟹ application (the (weight p p')) e ≠ None ⟹ e ∈ {e::energy. length e = dimension} ⟹ (the (application (the (weight p p')) e)) ∈ {e::energy. length e = dimension}"
    using inv_preserves_length
    by (simp add: updgalois) 

  show  "⋀p p' e. weight p p' ≠ None ⟹ e ∈ {e::energy. length e = dimension} ⟹ (inverse_application (the (weight p p')) e) ≠ None ∧ (the (inverse_application (the (weight p p')) e)) ∈ {e::energy. length e = dimension} ∧ application (the (weight p p')) (the (inverse_application (the (weight p p')) e)) ≠ None" 
    using inv_preserves_length domain_inv by simp

  show "⋀p p' e e'. weight p p' ≠ None ⟹ energy_leq e e' ⟹ application (the (weight p p')) e ≠ None ⟹ application (the (weight p p')) e' ≠ None"
    using local.domain_upw_closed .

  show  "⋀p p' e e'. weight p p' ≠ None ⟹ application (the (weight p p')) e' ≠ None ⟹ e ∈ {e::energy. length e = dimension} ⟹ e' ∈ {e::energy. length e = dimension} ⟹ energy_leq (the (inverse_application (the (weight p p')) e)) e' = energy_leq e (the (application (the (weight p p')) e'))"
    using galois by simp
qed

locale natural_galois_energy_game_decidable = natural_galois_energy_game attacker weight application inverse_application dimension
  for attacker ::  "'position set" and 
      weight :: "'position ⇒ 'position ⇒ 'label option" and
      application :: "'label ⇒ energy ⇒ energy option" and
      inverse_application :: "'label ⇒ energy ⇒ energy option" and
      dimension :: "nat"
+
assumes nonpos_eq_pos: "nonpos_winning_budget = winning_budget" and
        finite_positions: "finite positions"
                                 
sublocale natural_galois_energy_game_decidable ⊆ galois_energy_game_decidable attacker weight application inverse_application "{e::energy. length e = dimension}" energy_leq "λs. energy_sup dimension s"
proof
  show "nonpos_winning_budget = winning_budget" and "finite positions" using nonpos_eq_pos finite_positions by auto
qed

text‹Bisping's only considers declining energy games over vectors of naturals. We generalise this by considering all valid updates. 
We formalise this in this theory as an ‹energy_game› with a fixed dimension and show that such games are Galois energy games. ›

locale bispings_energy_game = energy_game attacker weight apply_update 
  for attacker ::  "'position set" and 
      weight :: "'position ⇒ 'position ⇒ update option"
+ 
  fixes dimension :: "nat"
  assumes
    valid_updates: "∀p. ∀p'. ((weight p p' ≠ None ) 
                    ⟶ ((length (the (weight p p')) = dimension) 
                    ∧ valid_update (the (weight p p'))))"

sublocale bispings_energy_game ⊆ natural_galois_energy_game attacker weight apply_update apply_inv_update dimension
proof
  show "⋀p p' e e'. weight p p' ≠ None ⟹ e e≤ e' ⟹ apply_w p p' e ≠ None ⟹ apply_w p p' e' ≠ None"
    using upd_domain_upward_closed
    by blast
  show "⋀p p' e. weight p p' ≠ None ⟹ apply_w p p' e ≠ None ⟹ length (upd (the (weight p p')) e) = length e"
    using len_appl
    by simp
  show "⋀p p' e. weight p p' ≠ None ⟹ length e = dimension ⟹ length (inv_upd (the (weight p p')) e) = length e"
    using len_inv_appl valid_updates
    by blast
  show "⋀p p' e.
       weight p p' ≠ None ⟹
       length e = dimension ⟹
       apply_inv_update (the (weight p p')) e ≠ None ∧ apply_w p p' (inv_upd (the (weight p p')) e) ≠ None"
    using  inv_not_none  inv_not_none_then
    using valid_updates by presburger
  show "⋀p p' e e'.
       weight p p' ≠ None ⟹
       apply_w p p' e' ≠ None ⟹
       length e = dimension ⟹
       length e' = dimension ⟹ inv_upd (the (weight p p')) e e≤ e' = e e≤ upd (the (weight p p')) e'"
    using galois_connection
    by (metis valid_updates) 
qed

locale bispings_energy_game_decidable = bispings_energy_game attacker weight dimension
  for attacker ::  "'position set" and 
      weight :: "'position ⇒ 'position ⇒ update option" and 
      dimension :: "nat"
+
assumes nonpos_eq_pos: "nonpos_winning_budget = winning_budget" and
        finite_positions: "finite positions"

sublocale bispings_energy_game_decidable ⊆ natural_galois_energy_game_decidable attacker weight apply_update apply_inv_update dimension
proof
  show "nonpos_winning_budget = winning_budget" using nonpos_eq_pos.
  show "finite positions" using finite_positions .
qed

end