Theory Galois_Energy_Game

section ‹Galois Energy Games›

theory Galois_Energy_Game
  imports Energy_Game Well_Quasi_Orders.Well_Quasi_Orders
begin

text‹We now define Galois energy games over well-founded bounded join-semilattices.
We do this by building on a previously defined energy_game›.
In particular, we add a set of energies energies› with an order order› and a supremum mapping energy_sup›.
Then, we assume the set to be partially ordered in energy_order›, the order to be well-founded in energy_wqo›, 
the supremum to map finite sets to the least upper bound bounded_join_semilattice› and the set to be upward-closed w.r.t\ the order in upward_closed_energies›. 
Further, we assume the updates to actually map energies (elements of the set enegies›) to energies with upd_well_defined›
and assume the inversion to map updates to total functions between the set of energies and the domain of the update in inv_well_defined›.
The latter is assumed to be upward-closed in domain_upw_closed›.
Finally, we assume the updates to be Galois-connected with their inverse in galois›. 
(This corresponds to section 2.3 in the preprint~\cite{preprint}.)
 ›

locale 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 energies :: "'energy set" and
        order :: "'energy  'energy  bool" (infix "e≤" 80)and 
        energy_sup :: "'energy set  'energy"
      assumes 
        energy_order: "ordering order (λe e'. order e e'  e  e')" and 
        energy_wqo: "wqo_on order energies" and 
        bounded_join_semilattice: " set s'. set  energies  finite set 
         energy_sup set  energies 
             (s. s  set  order s (energy_sup set)) 
             (s'  energies  (s. s  set  order s s')  order (energy_sup set) s')" and
        upward_closed_energies: "e e'. e  energies  e e≤ e'  e'  energies" and
        upd_well_defined: "p p' e. weight p p'  None 
         application (the (weight p p')) e  None  e  energies 
         (the (application (the (weight p p')) e))  energies" and
        inv_well_defined: "p p' e. weight p p'  None  e  energies 
         (inverse_application (the (weight p p')) e)  None 
         (the (inverse_application (the (weight p p')) e))  energies 
         application (the (weight p p')) (the (inverse_application (the (weight p p')) e))  None" and        
        domain_upw_closed: "p p' e e'. weight p p'  None  order e e' 
         application (the (weight p p')) e  None 
         application (the (weight p p')) e'  None" and
        galois: "p p' e e'. weight p p'  None 
         application (the (weight p p')) e'  None 
         e  energies  e'  energies 
         order (the (inverse_application (the (weight p p')) e)) e' = order e (the (application (the (weight p p')) e'))"
begin

abbreviation "upd u e  the (application u e)"
abbreviation "inv_upd u e  the (inverse_application u e)"

abbreviation energy_l:: "'energy  'energy  bool" (infix "e<" 80) where 
  "energy_l e e'   e e≤ e'  e  e'"

subsection‹Properties of Galois connections›
text‹The following properties are described by Erné et al.~\cite{galois}. ›


lemma galois_properties: 
  shows upd_inv_increasing: 
   "p p' e. weight p p'  None  eenergies 
     order e (the (application (the (weight p p')) (the (inverse_application (the (weight p p')) e))))"
   and inv_upd_decreasing: 
  "p p' e. weight p p'  None  eenergies 
   application (the (weight p p')) e  None 
   the (inverse_application (the (weight p p')) (the (application (the (weight p p')) e))) e≤ e"
  and updates_monotonic: 
  "p p' e e'. weight p p'  None eenergies  e e≤ e' 
   application (the (weight p p')) e  None 
   the( application (the (weight p p')) e) e≤ the (application (the (weight p p')) e')"
  and inverse_monotonic: 
  "p p' e e'. weight p p'  None  eenergies  e e≤ e' 
   inverse_application (the (weight p p')) e  None 
   the( inverse_application (the (weight p p')) e) e≤ the (inverse_application (the (weight p p')) e')"
proof-
  show upd_inv_increasing: "p p' e. weight p p'  None  eenergies 
     order e (the (application (the (weight p p')) (the (inverse_application (the (weight p p')) e))))"
  proof-
    fix p p' e 
    assume "weight p p'  None" 
    define u where "u= the (weight p p')"
    show "eenergies   order e (the (application (the (weight p p')) (the (inverse_application (the (weight p p')) e))))"
    proof-
      assume "eenergies"
      have "order (inv_upd u e) (inv_upd u e)"
        by (meson local.energy_order ordering.eq_iff)

      define e' where "e' = inv_upd u e"
      have "(inv_upd u e e≤ e') = e e≤ upd u e'"
        unfolding u_def using weight p p'  None proof(rule galois)
        show "apply_w p p' e'  None"
          using eenergies weight p p'  None e'_def inv_well_defined u_def by presburger
        show "eenergies" using eenergies.
        show "e'energies" unfolding e'_def
          using eenergies weight p p'  None inv_well_defined u_def
          by blast
      qed   
      hence "e e≤ upd u (inv_upd u e)"
        using  inv_upd u e e≤ inv_upd u e e'_def by auto
      thus "order e (the (application (the (weight p p')) (the (inverse_application (the (weight p p')) e))))"
        using u_def by auto
    qed
  qed

  show inv_upd_decreasing: "p p' e. weight p p'  None  eenergies 
   application (the (weight p p')) e  None 
   the (inverse_application (the (weight p p')) (the (application (the (weight p p')) e))) e≤ e"
  proof-
    fix p p' e 
    assume "weight p p'  None" 
    define u where "u= the (weight p p')"
    show "eenergies  application (the (weight p p')) e  None  the (inverse_application (the (weight p p')) (the (application (the (weight p p')) e))) e≤ e"
    proof-
      assume "eenergies" and "application (the (weight p p')) e  None"
      define e' where "e'= upd u e"
      have "(inv_upd u e' e≤ e) = e' e≤ upd u e"
        unfolding u_def using weight p p'  None application (the (weight p p')) e  None proof(rule galois)
        show eenergies  using eenergies .
        show e'energies unfolding e'_def using eenergies
          using apply_w p p' e  None weight p p'  None u_def upd_well_defined by auto 
      qed
      hence "inv_upd u (upd u e) e≤ e" using e'_def
        by (meson energy_order ordering.eq_iff) 
      thus "the (inverse_application (the (weight p p')) (the (application (the (weight p p')) e))) e≤ e"
        using u_def by simp
    qed
  qed

  show updates_monotonic:"p p' e e'. weight p p'  None eenergies  e e≤ e' 
   application (the (weight p p')) e  None 
   the( application (the (weight p p')) e) e≤ the (application (the (weight p p')) e')"
  proof-
    fix p p' e e' 
    assume "weight p p'  None" and "eenergies" and "e e≤ e'" and "application (the (weight p p')) e  None"
    define u where "u= the (weight p p')"
    define e'' where "e'' = upd u e"
    have "inv_upd u (upd u e) e≤ e' = (upd u e) e≤ upd u e'" 
      unfolding u_def using weight p p'  None proof(rule galois)
      show "apply_w p p' e'  None"
        using application (the (weight p p')) e  None e e≤ e' domain_upw_closed
        using weight p p'  None by blast 
      show "(upd (the (weight p p')) e)energies"
        using eenergies weight p p'  None upd_well_defined
        using apply_w p p' e  None by blast
      show "e'energies"
        using eenergies e e≤ e' upward_closed_energies by auto
    qed

    have "inv_upd u (upd u e) e≤ e" 
      unfolding u_def using weight p p'  None eenergies application (the (weight p p')) e  None 
    proof(rule inv_upd_decreasing)
    qed

    hence "inv_upd u (upd u e) e≤ e'" using e e≤ e' energy_order ordering_def
      by (metis (mono_tags, lifting) partial_preordering.trans) 
    hence "upd u e e≤ upd u e'" 
      using inv_upd u (upd u e) e≤ e' = (upd u e) e≤ upd u e' by auto
    thus "the( application (the (weight p p')) e) e≤ the (application (the (weight p p')) e')"
      using u_def by auto
  qed

  show inverse_monotonic: "p p' e e'. weight p p'  None  eenergies  e e≤ e' 
   inverse_application (the (weight p p')) e  None 
   the( inverse_application (the (weight p p')) e) e≤ the (inverse_application (the (weight p p')) e')"
  proof-
    fix p p' e e'
    assume "weight p p'  None"
    define u where "u= the (weight p p')"
    show "eenergies  e e≤ e'  inverse_application (the (weight p p')) e  None  the( inverse_application (the (weight p p')) e) e≤ the (inverse_application (the (weight p p')) e')"
    proof-
      assume "eenergies" and " e e≤ e'" and " inverse_application (the (weight p p')) e  None"

      define e'' where "e'' = inv_upd u e'"
      have "inv_upd u e e≤ e'' = e e≤ upd u e''"
        unfolding u_def using weight p p'  None proof(rule galois)
        show "apply_w p p' e''  None"
          unfolding e''_def using inverse_application (the (weight p p')) e  None
          using e  energies e e≤ e' weight p p'  None inv_well_defined u_def upward_closed_energies by blast
        show "eenergies" using eenergies.
        hence "e'energies"
          using e e≤ e' energy_order ordering_def
          using upward_closed_energies by blast
        thus "e''energies"
          unfolding e''_def
          using weight p p'  None inv_well_defined u_def by blast 
      qed

      have "e' e≤ upd u e''"
        unfolding e''_def u_def using weight p p'  None 
      proof(rule upd_inv_increasing)
        from eenergies show "e'energies"
          using e e≤ e' energy_order ordering_def
          using upward_closed_energies by blast
      qed
    
      hence "inv_upd u e e≤ inv_upd u e'"
        using inv_upd u e e≤ e'' = e e≤ upd u e'' e''_def
        using e e≤ e' energy_order ordering_def
        using upward_closed_energies
        by (metis (no_types, lifting) partial_preordering.trans) 
      thus "the( inverse_application (the (weight p p')) e) e≤ the (inverse_application (the (weight p p')) e')"
        using u_def by auto
    qed
  qed
qed

text‹Galois connections compose. In particular, the ``inverse'' of $u_g$ composed with that of $u_p$ is the ``inverse'' of $u_p \circ u_g$. 
This forms a Galois connection between the set of energies and the reverse image under $u_g$ of the domain of $u_p$, i.e.\ $u_g^{-1} (\text{dom}(u_p))$›

lemma galois_composition:
  assumes "weight g g'  None" and "weight p p'  None"
  shows  "inv. e  energies. e' energies. (application (the (weight g g')) e'  None 
           application (the (weight p p')) ((upd (the (weight g g')) e'))  None) 
           (order (inv e) e') = (order e (upd (the (weight p p')) ((upd (the (weight g g')) e'))))"
proof
  define inv where "inv  λx. inv_upd (the (weight g g')) (inv_upd (the (weight p p')) x)"
  show "eenergies. e'energies. apply_w g g' e'  None  apply_w p p' (upd (the (weight g g')) e')  None  inv e e≤ e' = e e≤ upd (the (weight p p')) (upd (the (weight g g')) e')"
  proof
    fix e 
    assume E: "eenergies"
    show "e'energies. apply_w g g' e'  None  apply_w p p' (upd (the (weight g g')) e')  None  inv e e≤ e' = e e≤ upd (the (weight p p')) (upd (the (weight g g')) e')"
    proof
      fix e'
      assume E': "e'energies"
      show "apply_w g g' e'  None  apply_w p p' (upd (the (weight g g')) e')  None  inv e e≤ e' = e e≤ upd (the (weight p p')) (upd (the (weight g g')) e')"
      proof
        assume dom: "apply_w g g' e'  None  apply_w p p' (upd (the (weight g g')) e')  None"

        define x where "x=inv_upd (the (weight p p')) e "
        have "inv_upd (the (weight g g')) x e≤ e' = x e≤ upd (the (weight g g')) e'"
        proof(rule galois)
          show "weight g g'  None" using assms by simp
          show "apply_w g g' e'  None" using dom by simp
          show "x  energies"
            unfolding x_def using dom
            using E assms(2) inv_well_defined by blast 
          show "e'  energies" using E' .
        qed
        hence A1: "inv e e≤ e' = inv_upd (the (weight p p')) e e≤ upd (the (weight g g')) e'"
          unfolding inv_def x_def .

        define y where "y = (upd (the (weight g g')) e')"
        have "inv_upd (the (weight p p')) e e≤ y = e e≤ upd (the (weight p p')) y"
        proof(rule galois)
          show "weight p p'  None" using assms by simp
          show "apply_w p p' y  None" unfolding y_def using dom by simp
          show "e  energies" using E .
          show "y  energies" unfolding y_def
            using E' assms(1) dom upd_well_defined by auto 
        qed
        hence A2: "inv_upd (the (weight p p')) e e≤ upd (the (weight g g')) e' = e e≤ upd (the (weight p p')) (upd (the (weight g g')) e')"
          unfolding inv_def y_def .
        show "inv e e≤ e' = e e≤ upd (the (weight p p')) (upd (the (weight g g')) e')"
          using A1 A2 by simp
      qed
    qed
  qed
qed

subsection‹Properties of the Partial Order›
text‹We now establish some properties of the partial order focusing on the set of minimal elements.›

definition energy_Min:: "'energy set  'energy set" where
  "energy_Min A = {eA . e'A. ee'  ¬ (e' e≤ e)}"

fun enumerate_arbitrary :: "'a set  nat  'a"  where
  "enumerate_arbitrary A 0 = (SOME a. a  A)" |
  "enumerate_arbitrary A (Suc n) 
    = enumerate_arbitrary (A - {enumerate_arbitrary A 0}) n"

lemma enumerate_arbitrary_in: 
  shows "infinite A  enumerate_arbitrary A i  A"
proof(induct i arbitrary: A)
  case 0
  then show ?case using enumerate_arbitrary.simps finite.simps some_in_eq by auto 
next
  case (Suc i)
  hence "infinite (A - {enumerate_arbitrary A 0})" using infinite_remove by simp
  hence "enumerate_arbitrary (A - {enumerate_arbitrary A 0}) i  (A - {enumerate_arbitrary A 0})" using Suc.hyps by blast
  hence "enumerate_arbitrary A (Suc i)  (A - {enumerate_arbitrary A 0})" using enumerate_arbitrary.simps by simp
  then show ?case by auto
qed

lemma enumerate_arbitrary_neq:
  shows "infinite A  i < j 
         enumerate_arbitrary A i  enumerate_arbitrary A j"
proof(induct i arbitrary: j A)
  case 0
  then show ?case using enumerate_arbitrary.simps
    by (metis Diff_empty Diff_iff enumerate_arbitrary_in finite_Diff_insert gr0_implies_Suc insert_iff)
next
  case (Suc i)
  hence "j'. j = Suc j'"
    by (simp add: not0_implies_Suc) 
  from this obtain j' where "j = Suc j'" by auto
  hence "i < j'" using Suc by simp
  from Suc have "infinite (A - {enumerate_arbitrary A 0})" using infinite_remove by simp
  hence "enumerate_arbitrary (A - {enumerate_arbitrary A 0}) i  enumerate_arbitrary (A - {enumerate_arbitrary A 0}) j'" using Suc i < j'
    by force
  then show ?case using enumerate_arbitrary.simps
    by (simp add: j = Suc j') 
qed

lemma energy_Min_finite:
  assumes "A  energies"
  shows "finite (energy_Min A)"
proof-
  have "wqo_on order (energy_Min A)" using energy_wqo assms energy_Min_def wqo_on_subset
    by (metis (no_types, lifting) mem_Collect_eq subsetI) 
  hence wqoMin: "(f  SEQ (energy_Min A). (i j. i < j  order (f i) (f j)))" unfolding wqo_on_def almost_full_on_def good_def by simp
  have "¬ finite (energy_Min A)  False" 
  proof-
    assume "¬ finite (energy_Min A)"
    hence "infinite (energy_Min A)"
      by simp

    define f where "f  enumerate_arbitrary (energy_Min A)"
    have fneq: "i j. f i  energy_Min A  (j  i  f j  f i)"
    proof
      fix i j 
      show "f i  energy_Min A" unfolding f_def using enumerate_arbitrary_in infinite (energy_Min A) by auto 
      show "j  i  f j  f i" proof
        assume "j  i"
        show "f j  f i" proof(cases "j < i")
          case True
          then show ?thesis unfolding f_def using enumerate_arbitrary_neq infinite (energy_Min A) by auto 
        next
          case False
          hence "i < j" using j  i by auto
          then show ?thesis unfolding f_def using enumerate_arbitrary_neq infinite (energy_Min A)
            by metis 
        qed
      qed
    qed
    hence "i j. i < j  order (f i) (f j)" using wqoMin SEQ_def by simp
    thus "False" using energy_Min_def fneq by force
  qed
  thus ?thesis by auto
qed

fun enumerate_decreasing :: "'energy set  nat  'energy"  where
  "enumerate_decreasing A 0 = (SOME a. a  A)" |
  "enumerate_decreasing A (Suc n) 
    = (SOME x. (x  A  x e< enumerate_decreasing A n))"

lemma energy_Min_not_empty:
  assumes "A  {}" and "A  energies" 
  shows "energy_Min A  {}"
proof
  have "wqo_on order A" using energy_wqo assms wqo_on_subset
    by (metis (no_types, lifting)) 
  hence wqoA: "(f  SEQ A. (i j. i < j  (f i) e≤ (f j)))" unfolding wqo_on_def almost_full_on_def good_def by simp
  assume "energy_Min A = {}"
  have seq: "enumerate_decreasing A  SEQ A"
    unfolding SEQ_def proof
    show "i. enumerate_decreasing A i  A"
    proof
      fix i 
      show "enumerate_decreasing A i  A"
      proof(induct i)
        case 0
        then show ?case using assms
          by (simp add: some_in_eq) 
      next
        case (Suc i)
        show ?case 
        proof(rule ccontr)
          assume "enumerate_decreasing A (Suc i)  A"
          hence "{x. (x  A  x e< enumerate_decreasing A i)}={}" unfolding enumerate_decreasing.simps
            by (metis (no_types, lifting) empty_Collect_eq someI_ex)
          thus "False"
            using Suc energy_Min A = {} energy_Min_def by auto 
        qed
      qed
    qed
  qed

  have "¬(i j. i < j  (enumerate_decreasing A i) e≤ (enumerate_decreasing A j))"
  proof-
    have "i j. ¬(i < j  (enumerate_decreasing A i) e≤ (enumerate_decreasing A j))"
    proof
      fix i
      show "j. ¬(i < j  (enumerate_decreasing A i) e≤ (enumerate_decreasing A j))"
      proof
        fix j
        have leq: "i < j  (enumerate_decreasing A j) e< (enumerate_decreasing A i)"
        proof(induct "j-i" arbitrary: j i)
          case 0
          then show ?case
            using i < j by linarith
        next
          case (Suc x)

          have suc_i: "enumerate_decreasing A (Suc i) e< enumerate_decreasing A i"
          proof-
            have "{x. (x  A  x e< enumerate_decreasing A i)}{} "
            proof
              assume "{x  A. x e< enumerate_decreasing A i} = {}"
              hence "enumerate_decreasing A i  energy_Min A" unfolding energy_Min_def
                using seq by auto 
              thus "False" using energy_Min A = {} by auto
            qed
            thus ?thesis unfolding enumerate_decreasing.simps
              by (metis (mono_tags, lifting) empty_Collect_eq verit_sko_ex')
          qed

          have "j - (Suc i) = x" using Suc
            by (metis Suc_diff_Suc nat.inject) 
          then show ?case proof(cases "j = Suc i")
            case True
            then show ?thesis using suc_i
              by simp 
          next
            case False
            hence "enumerate_decreasing A j e< enumerate_decreasing A (Suc i)"
              using Suc j - (Suc i) = x
              using Suc_lessI by blast
            then show ?thesis using suc_i energy_order ordering_def
              by (metis (no_types, lifting) ordering_axioms_def partial_preordering.trans) 
          qed
        qed
        
        hence "i <j  ¬(enumerate_decreasing A i) e≤ (enumerate_decreasing A j)"
        proof-
          assume "i <j"
          hence "(enumerate_decreasing A j) e< (enumerate_decreasing A i)" using leq by auto
          hence leq: "(enumerate_decreasing A j) e≤ (enumerate_decreasing A i)" by simp
          have neq: "(enumerate_decreasing A j)  (enumerate_decreasing A i)"
            using (enumerate_decreasing A j) e< (enumerate_decreasing A i)
            by simp
          show "¬(enumerate_decreasing A i) e≤ (enumerate_decreasing A j)"
          proof
            assume "(enumerate_decreasing A i) e≤ (enumerate_decreasing A j)"
            hence "(enumerate_decreasing A i) = (enumerate_decreasing A j)" using leq leq energy_order ordering_def
              by (simp add: ordering.antisym) 
            thus "False" using neq by simp
          qed
        qed
        thus "¬(i < j  (enumerate_decreasing A i) e≤ (enumerate_decreasing A j))" by auto
      qed
    qed
    thus ?thesis
      by simp
    qed
  thus "False" using seq wqoA
    by blast 
qed

lemma energy_Min_contains_smaller:
  assumes "a  A" and "A  energies" 
  shows "b  energy_Min A. b e≤ a"
proof-
  define set where "set  {e. e  A  e e≤ a}"
  hence "a  set" using energy_order ordering_def
    using assms ordering.eq_iff by fastforce  
  hence "set  {}" by auto
  have "s. s set  s energies" using energy_order set_def assms
    by auto
  hence "energy_Min set  {}" using set  {} energy_Min_not_empty
    by (simp add: subsetI) 
  hence "b. b  energy_Min set" by auto
  from this obtain b where "b  energy_Min set" by auto
  hence "b'. b' A  b'  b  ¬ (b' e≤ b)"
  proof-
    fix b'
    assume "b'  A"
    assume "b'  b"
    show "¬ (b' e≤ b)"
    proof
      assume "(b' e≤ b)"
      hence "b' e≤ a" using b  energy_Min set energy_Min_def energy_order ordering_def
        by (metis (no_types, lifting) local.set_def mem_Collect_eq partial_preordering.trans) 
      hence "b'  set" using b'  A set_def by simp
      thus "False" using b  energy_Min set energy_Min_def b' e≤ b b'  b by auto 
    qed
  qed
  hence "b energy_Min A" using energy_Min_def
    using b  energy_Min set local.set_def by auto 
  thus ?thesis using b  energy_Min set energy_Min_def set_def by auto
qed

lemma energy_sup_leq_energy_sup:
  assumes "A  {}" and "a. a A  b B. order a b" and 
          "a. a A  a energies" and "finite A" and "finite B" and "B  energies"
        shows "order (energy_sup A) (energy_sup B)"
proof-
  have A: "s'. energy_sup A  energies  (s. s  A  s e≤ energy_sup A)  (s'  energies (s. s  A  s e≤ s')  energy_sup A e≤ s')" 
  proof(rule bounded_join_semilattice)
    fix s'
    show "finite A" using assms by simp
    show "A  energies" using assms
      by (simp add: subsetI) 
  qed

  have B: "s'. energy_sup B  energies  (s. s  B  s e≤ energy_sup B)  (s'  energies (s. s  B  s e≤ s')  energy_sup B e≤ s')" 
  proof(rule bounded_join_semilattice)
    fix s'
    show " finite B" using assms by simp
    show "B  energies"
      using assms by simp
  qed

  have "energy_sup B  energies  (s. s  A  s e≤ energy_sup B)"
  proof
    show "energy_sup B  energies"
      using B by simp
    show " s. s  A  s e≤ energy_sup B "
    proof
      fix s
      show "s  A  s e≤ energy_sup B"
      proof
        assume "s  A"
        from this obtain b where "s e≤ b" and "b  B" using assms
          by blast
        hence "b e≤ energy_sup B" using B by auto
        thus "s e≤ energy_sup B" using s e≤ b energy_order ordering_def
          by (metis (mono_tags, lifting) partial_preordering.trans) 
      qed
    qed
  qed
  thus ?thesis using A by auto
qed


subsection‹Winning Budgets Revisited›
text‹We now redefine attacker winning budgets to only include energies in the set energies›.›

inductive winning_budget_len::"'energy  'position  bool" where
 defender: "winning_budget_len e g" if "eenergies  g  attacker 
             (g'. (weight g g'  None)  
                    ((application (the (weight g g')) e) None 
                      (winning_budget_len (the (application (the (weight g g')) e))) g'))" |
 attacker: "winning_budget_len e g" if "eenergies  g  attacker 
             (g'. (weight g g'  None) 
                     (application (the (weight g g')) e) None 
                     (winning_budget_len (the (application (the (weight g g')) e)) g'))"

text‹We first restate the upward-closure of winning budgets.›

lemma upwards_closure_wb_len:
  assumes "winning_budget_len e g" and "e e≤ e'"
  shows "winning_budget_len e' g"
using assms proof (induct arbitrary: e' rule: winning_budget_len.induct)
  case (defender e g)
  have "(g'. weight g g'  None 
          application (the (weight g g')) e'  None 
          winning_budget_len (the (application (the (weight g g')) e')) g')" 
  proof
    fix g'
    show " weight g g'  None 
          application (the (weight g g')) e'  None 
          winning_budget_len (the (application (the (weight g g')) e')) g'" 
    proof
      assume "weight g g'  None"
      hence A: "application (the (weight g g')) e  None 
          winning_budget_len (the (application (the (weight g g')) e)) g'" using assms(1) winning_budget_len.simps defender by blast
      show "application (the (weight g g')) e'  None 
          winning_budget_len (the (application (the (weight g g')) e')) g'" 
      proof
        show "application (the (weight g g')) e'  None" using domain_upw_closed assms(2) A defender weight g g'  None by blast
        have "order (the (application (the (weight g g')) e)) (the (application (the (weight g g')) e'))" using assms A updates_monotonic
          using weight g g'  None defender.hyps defender.prems by presburger  
        thus "winning_budget_len (the (application (the (weight g g')) e')) g'" using defender weight g g'  None by blast
      qed
    qed
  qed
thus ?case using winning_budget_len.intros(1) defender
  by (meson upward_closed_energies)
next
  case (attacker e g)
  from this obtain g' where G: "weight g g'  None 
          application (the (weight g g')) e  None 
          winning_budget_len (the (application (the (weight g g')) e)) g' 
          (x. order (the (application (the (weight g g')) e)) x  winning_budget_len x g')" by blast
  have "weight g g'  None 
          application (the (weight g g')) e'  None 
          winning_budget_len (the (application (the (weight g g')) e')) g'" 
  proof
    show "weight g g'  None" using G by auto
    show "application (the (weight g g')) e'  None  winning_budget_len (the (application (the (weight g g')) e')) g' " 
    proof
      show "application (the (weight g g')) e'  None" using G  domain_upw_closed assms attacker by blast
      have "order (the (application (the (weight g g')) e)) (the (application (the (weight g g')) e'))" using assms G updates_monotonic
        using attacker.hyps attacker.prems by blast
      thus "winning_budget_len (the (application (the (weight g g')) e')) g' " using G by blast
    qed
  qed
  thus ?case using winning_budget_len.intros(2) attacker
    using upward_closed_energies by blast
qed

text‹We now show that this definition is consistent with our previous definition of winning budgets.
We show this by well-founded induction.›

abbreviation "reachable_positions_len s g e  {(g',e')  reachable_positions s g e . e'energies}"

lemma winning_bugget_len_is_wb:
  assumes "nonpos_winning_budget = winning_budget"
  shows "winning_budget_len e g = (winning_budget e g   e energies)"
proof
  assume "winning_budget_len e g"
  show "winning_budget e g  e energies"
  proof
    have "winning_budget_ind e g" 
      using winning_budget_len e g proof(rule winning_budget_len.induct)
      show "e g. e energies 
           g  attacker 
           (g'. weight g g'  None 
                 apply_w g g' e  None 
                 winning_budget_len (upd (the (weight g g')) e) g' 
                 winning_budget_ind (upd (the (weight g g')) e) g') 
           winning_budget_ind e g"
        using winning_budget_ind.simps
        by meson 
      show "e g. e energies 
           g  attacker 
           (g'. weight g g'  None 
                 apply_w g g' e  None 
                 winning_budget_len (upd (the (weight g g')) e) g' 
                 winning_budget_ind (upd (the (weight g g')) e) g') 
           winning_budget_ind e g "
        using winning_budget_ind.simps
        by meson 
    qed
    thus "winning_budget e g" using assms inductive_winning_budget
      by fastforce 
    show "e energies" using winning_budget_len e g winning_budget_len.simps by blast 
  qed
next
  show "winning_budget e g  e energies  winning_budget_len e g" 
  proof-
    assume A: "winning_budget e g  e energies"
    hence "winning_budget_ind e g" using assms inductive_winning_budget by fastforce
    show "winning_budget_len e g" 
    proof-

      define wb where "wb  λ(g,e). winning_budget_len e g"

      from A have "s. attacker_winning_strategy s e g" using winning_budget.simps by blast
      from this obtain s where S: "attacker_winning_strategy s e g" by auto

      have "reachable_positions_len s g e  reachable_positions s g e" by auto
      hence "wfp_on (strategy_order s) (reachable_positions_len s g e)" 
        using strategy_order_well_founded S
        using Restricted_Predicates.wfp_on_subset by blast
      hence "inductive_on (strategy_order s) (reachable_positions_len s g e)"
        by (simp add: wfp_on_iff_inductive_on)

      hence "wb (g,e)" 
      proof(rule inductive_on_induct)
        show "(g,e)  reachable_positions_len s g e"
          unfolding reachable_positions_def proof-
          have "lfinite LNil 
             llast (LCons g LNil) = g 
             valid_play (LCons g LNil)  play_consistent_attacker s (LCons g LNil) e 
            Some e = energy_level e (LCons g LNil) (the_enat (llength LNil))"
            using valid_play.simps play_consistent_attacker.simps energy_level.simps
            by (metis lfinite_code(1) llast_singleton llength_LNil neq_LNil_conv the_enat_0) 
          thus "(g, e)  {(g', e').
        (g', e')
         {(g', e') |g' e'.
            p. lfinite p 
                llast (LCons g p) = g' 
                valid_play (LCons g p) 
                play_consistent_attacker s (LCons g p) e 
                Some e' = energy_level e (LCons g p) (the_enat (llength p))} 
         e'energies}" using A

            by blast 
        qed

        show "y. y  reachable_positions_len s g e 
              (x. x  reachable_positions_len s g e  strategy_order s x y  wb x)  wb y"
        proof-
          fix y 
          assume "y  reachable_positions_len s g e"
          hence "e' g'. y = (g', e')" using reachable_positions_def by auto
          from this obtain e' g' where "y = (g', e')" by auto

          hence y_len: "(p. lfinite p  llast (LCons g p) = g' 
                                                     valid_play (LCons g p) 
                                                     play_consistent_attacker s (LCons g p) e
                                                     (Some e' = energy_level e (LCons g p) (the_enat (llength p))))
                 e'energies"
            using y  reachable_positions_len s g e unfolding reachable_positions_def
            by auto 
          from this obtain p where P: "(lfinite p  llast (LCons g p) = g' 
                                                     valid_play (LCons g p) 
                                                     play_consistent_attacker s (LCons g p) e) 
                                                     (Some e' = energy_level e (LCons g p) (the_enat (llength p)))" by auto
       
          show "(x. x  reachable_positions_len s g e  strategy_order s x y  wb x)  wb y"
          proof-
            assume ind: "(x. x  reachable_positions_len s g e  strategy_order s x y  wb x)"
            have "winning_budget_len e' g'" 
            proof(cases "g'  attacker")
              case True 
              then show ?thesis 
              proof(cases "deadend g'")
                case True (* wiederspruchsbeweis *)
                hence "attacker_stuck (LCons g p)" using g'  attacker P
                  by (meson A defender_wins_play_def attacker_winning_strategy.elims(2)) 
                hence "defender_wins_play e (LCons g p)" using defender_wins_play_def by simp
                have "¬defender_wins_play e (LCons g p)" using P A S by simp
                then show ?thesis using defender_wins_play e (LCons g p) by simp
              next
                case False (* nehme s e' g' und wende ind.hyps. darauf an *)
                hence "(s e' g')  None  (weight g' (the (s e' g')))None" using S attacker_winning_strategy.simps
                  by (simp add: True attacker_strategy_def)

                define x where "x = (the (s e' g'), the (apply_w g' (the (s e' g')) e'))"
                define p' where "p' =  (lappend p (LCons (the (s e' g')) LNil))"
                hence "lfinite p'" using P by simp
                have "llast (LCons g p') = the (s e' g')" using p'_def lfinite p'
                  by (simp add: llast_LCons)

                have "the_enat (llength p') > 0" using P
                  by (metis LNil_eq_lappend_iff lfinite p' bot_nat_0.not_eq_extremum enat_0_iff(2) lfinite_conv_llength_enat llength_eq_0 llist.collapse(1) llist.distinct(1) p'_def the_enat.simps) 
                hence "i. Suc i = the_enat (llength p')"
                  using less_iff_Suc_add by auto 
                from this obtain i where "Suc i = the_enat (llength p')" by auto
                hence "i = the_enat (llength p)" using p'_def P                     
                  by (metis Suc_leI lfinite p' length_append_singleton length_list_of_conv_the_enat less_Suc_eq_le less_irrefl_nat lfinite_LConsI lfinite_LNil list_of_LCons list_of_LNil list_of_lappend not_less_less_Suc_eq)
                hence "Some e' = (energy_level e (LCons g p) i)" using P by simp

                have A: "lfinite (LCons g p)  i < the_enat (llength (LCons g p))  energy_level e (LCons g p) (the_enat (llength (LCons g p)) - 1)  None"
                proof
                  show "lfinite (LCons g p)" using P by simp
                  show "i < the_enat (llength (LCons g p))  energy_level e (LCons g p) (the_enat (llength (LCons g p)) - 1)  None"
                  proof
                    show "i < the_enat (llength (LCons g p))" using i = the_enat (llength p) P
                      by (metis lfinite (LCons g p) length_Cons length_list_of_conv_the_enat lessI list_of_LCons) 
                    show "energy_level e (LCons g p) (the_enat (llength (LCons g p)) - 1)  None" using P i = the_enat (llength p)
                      using S defender_wins_play_def by auto
                  qed
                qed

                hence "Some e' = (energy_level e (LCons g p') i)" using p'_def energy_level_append P Some e' = (energy_level e (LCons g p) i)
                  by (metis lappend_code(2))
                hence "energy_level e (LCons g p') i  None"
                  by (metis option.distinct(1))

                have "enat (Suc i) = llength p'" using Suc i = the_enat (llength p')
                  by (metis lfinite p' lfinite_conv_llength_enat the_enat.simps)
                also have "... < eSuc (llength p')"
                  by (metis calculation iless_Suc_eq order_refl) 
                also have "... = llength (LCons g p')" using lfinite p' by simp
                finally have "enat (Suc i) < llength (LCons g p')".

                have "(lnth (LCons g p) i) = g'" using i = the_enat (llength p) P
                  by (metis lfinite_conv_llength_enat llast_conv_lnth llength_LCons the_enat.simps) 
                hence "(lnth (LCons g p') i) = g'" using p'_def
                  by (metis P i = the_enat (llength p) enat_ord_simps(2) energy_level.elims lessI lfinite_llength_enat lnth_0 lnth_Suc_LCons lnth_lappend1 the_enat.simps) 

                have "energy_level e (LCons g p') (the_enat (llength p')) = energy_level e (LCons g p') (Suc i)" 
                  using Suc i = the_enat (llength p') by simp
                also have "... = apply_w (lnth (LCons g p') i) (lnth (LCons g p') (Suc i)) (the (energy_level e (LCons g p') i))" 
                  using energy_level.simps enat (Suc i) < llength (LCons g p') energy_level e (LCons g p') i  None
                  by (meson leD)
                also have "... =  apply_w (lnth (LCons g p') i) (lnth (LCons g p') (Suc i)) e'" using Some e' = (energy_level e (LCons g p') i)
                  by (metis option.sel) 
                also have "... =  apply_w (lnth (LCons g p') i) (the (s e' g')) e'" using p'_def enat (Suc i) = llength p'
                  by (metis eSuc (llength p') = llength (LCons g p') llast (LCons g p') = the (s e' g') llast_conv_lnth) 
                also have  "... =  apply_w g' (the (s e' g')) e'" using (lnth (LCons g p') i) = g' by simp
                finally have "energy_level e (LCons g p') (the_enat (llength p')) = apply_w g' (the (s e' g')) e'" .
            
                have P': "lfinite p'
             llast (LCons g p') = (the (s e' g')) 
             valid_play (LCons g p')  play_consistent_attacker s (LCons g p') e 
            Some (the (apply_w g' (the (s e' g')) e')) = energy_level e (LCons g p') (the_enat (llength p'))"
                proof
                  show "lfinite p'" using p'_def P by simp
                  show "llast (LCons g p') = the (s e' g') 
    valid_play (LCons g p') 
    play_consistent_attacker s (LCons g p') e 
    Some (the (apply_w g' (the (s e' g')) e')) = energy_level e (LCons g p') (the_enat (llength p'))"
                  proof
                    show "llast (LCons g p') = the (s e' g')" using p'_def lfinite p'
                      by (simp add: llast_LCons) 
                    show "valid_play (LCons g p') 
    play_consistent_attacker s (LCons g p') e 
    Some (the (apply_w g' (the (s e' g')) e')) = energy_level e (LCons g p') (the_enat (llength p'))"
                    proof
                      show "valid_play (LCons g p')" using p'_def P
                        using s e' g'  None  weight g' (the (s e' g'))  None valid_play.intros(2) valid_play_append by auto
                      show "play_consistent_attacker s (LCons g p') e 
    Some (the (apply_w g' (the (s e' g')) e')) = energy_level e (LCons g p') (the_enat (llength p'))"
                      proof
                        have "(LCons g p') = lappend (LCons g p) (LCons (the (s e' g')) LNil)" using p'_def
                          by simp
                        have "play_consistent_attacker s (lappend (LCons g p) (LCons (the (s e' g')) LNil)) e"
                        proof (rule play_consistent_attacker_append_one)
                          show "play_consistent_attacker s (LCons g p) e"
                            using P by auto
                          show "lfinite (LCons g p)" using P by auto
                          show "energy_level e (LCons g p) (the_enat (llength (LCons g p)) - 1)  None" using P
                            using A by auto 
                          show "valid_play (lappend (LCons g p) (LCons (the (s e' g')) LNil))" 
                            using valid_play (LCons g p') (LCons g p') = lappend (LCons g p) (LCons (the (s e' g')) LNil) by simp
                          show "llast (LCons g p)  attacker 
    Some (the (s e' g')) =
    s (the (energy_level e (LCons g p) (the_enat (llength (LCons g p)) - 1))) (llast (LCons g p))"
                          proof
                            assume "llast (LCons g p)  attacker"
                            show "Some (the (s e' g')) =
    s (the (energy_level e (LCons g p) (the_enat (llength (LCons g p)) - 1))) (llast (LCons g p))"
                              using llast (LCons g p)  attacker P
                              by (metis One_nat_def s e' g'  None  weight g' (the (s e' g'))  None diff_Suc_1' eSuc_enat lfinite_llength_enat llength_LCons option.collapse option.sel the_enat.simps) 
                          qed
                        qed
                        thus "play_consistent_attacker s (LCons g p') e" using (LCons g p') = lappend (LCons g p) (LCons (the (s e' g')) LNil) by simp
                    
                        show "Some (the (apply_w g' (the (s e' g')) e')) = energy_level e (LCons g p') (the_enat (llength p'))"
                          by (metis eSuc (llength p') = llength (LCons g p') enat (Suc i) = llength p' energy_level e (LCons g p') (the_enat (llength p')) = apply_w g' (the (s e' g')) e' play_consistent_attacker s (LCons g p') e valid_play (LCons g p') S defender_wins_play_def diff_Suc_1 eSuc_enat option.collapse attacker_winning_strategy.elims(2) the_enat.simps)
                      qed
                    qed
                  qed
                qed

                have x_len: "(upd (the (weight g' (the (s e' g')))) e') energies" using y_len
                  by (metis P' energy_level e (LCons g p') (the_enat (llength p')) = apply_w g' (the (s e' g')) e' s e' g'  None  weight g' (the (s e' g'))  None option.distinct(1) upd_well_defined)
                hence "x  reachable_positions_len s g e" using P' reachable_positions_def x_def by auto

                have "(apply_w g' (the (s e' g')) e')  None" using P'
                  by (metis energy_level e (LCons g p') (the_enat (llength p')) = apply_w g' (the (s e' g')) e' option.distinct(1)) 
    
                have "Some (the (apply_w g' (the (s e' g')) e')) = apply_w g' (the (s e' g')) e'  (if g'  attacker then Some (the (s e' g')) = s e' g' else weight g' (the (s e' g'))  None)"
                  using (s e' g')  None  (weight g' (the (s e' g')))None (apply_w g' (the (s e' g')) e')  None by simp
                hence "strategy_order s x y" unfolding strategy_order_def using x_def y = (g', e')
                  by blast
                hence "wb x" using ind x  reachable_positions_len s g e by simp
                hence "winning_budget_len (the (apply_w g' (the (s e' g')) e')) (the (s e' g'))" using wb_def x_def by simp
                then show ?thesis using g'  attacker winning_budget_ind.simps
                  by (meson apply_w g' (the (s e' g')) e'  None s e' g'  None  weight g' (the (s e' g'))  None winning_budget_len.attacker y_len) 
              qed
            next
              case False
              hence "g'  attacker 
            (g''. weight g' g''  None 
          apply_w g' g'' e'  None  winning_budget_len (the (apply_w g' g'' e')) g'')"
              proof
                show "g''. weight g' g''  None 
          apply_w g' g'' e'  None  winning_budget_len (the (apply_w g' g'' e')) g''"
                proof
                  fix g''
                  show "weight g' g''  None 
           apply_w g' g'' e'  None  winning_budget_len (the (apply_w g' g'' e')) g'' "
                  proof
                    assume "weight g' g''  None"
                    show "apply_w g' g'' e'  None  winning_budget_len (the (apply_w g' g'' e')) g''"
                    proof
                      show "apply_w g' g'' e'  None"
                      proof
                        assume "apply_w g' g'' e' = None"
                        define p' where "p'  (LCons g (lappend p (LCons g'' LNil)))"
                        hence "lfinite p'" using P by simp
                        have "i. llength p = enat i" using P
                          by (simp add: lfinite_llength_enat) 
                        from this obtain i where "llength p = enat i" by auto
                        hence "llength (lappend p (LCons g'' LNil)) = enat (Suc i)"
                          by (simp add: llength p = enat i eSuc_enat iadd_Suc_right)
                        hence "llength p' = eSuc (enat(Suc i))" using p'_def
                          by simp 
                        hence "the_enat (llength p') = Suc (Suc i)"
                          by (simp add: eSuc_enat)
                        hence "the_enat (llength p') - 1 = Suc i"
                          by simp 
                        hence "the_enat (llength p') - 1 = the_enat (llength (lappend p (LCons g'' LNil)))"
                          using llength (lappend p (LCons g'' LNil)) = enat (Suc i)
                          by simp

                        have "(lnth p' i) = g'" using p'_def llength p = enat i P
                          by (smt (verit) One_nat_def diff_Suc_1' enat_ord_simps(2) energy_level.elims lessI llast_conv_lnth llength_LCons lnth_0 lnth_LCons' lnth_lappend the_enat.simps)
                        have "(lnth p' (Suc i)) = g''" using p'_def llength p = enat i
                          by (metis llength p' = eSuc (enat (Suc i)) lappend.disc(2) llast_LCons llast_conv_lnth llast_lappend_LCons llength_eq_enat_lfiniteD llist.disc(1) llist.disc(2))
                        have "p' = lappend (LCons g p) (LCons g'' LNil)" using p'_def by simp
                        hence "the (energy_level e p' i) = the (energy_level e (lappend (LCons g p) (LCons g'' LNil)) i)" by simp
                        also have "... = the (energy_level e (LCons g p) i)" using llength p = enat i energy_level_append P
                          by (metis diff_Suc_1 eSuc_enat lessI lfinite_LConsI llength_LCons option.distinct(1) the_enat.simps) 
                        also have "... = e'" using P
                          by (metis llength p = enat i option.sel the_enat.simps) 
                        finally have "the (energy_level e p' i) = e'" . 
                        hence "apply_w (lnth p' i) (lnth p' (Suc i)) (the (energy_level e p' i)) = None" using apply_w g' g'' e'=None (lnth p' i) = g' (lnth p' (Suc i)) = g'' by simp

                        have "energy_level e p' (the_enat (llength p') - 1) = 
                          energy_level e p' (the_enat (llength (lappend p (LCons g'' LNil))))" 
                          using the_enat (llength p') - 1 = the_enat (llength (lappend p (LCons g'' LNil)))
                          by simp 
                        also have "... = energy_level e p' (Suc i)" using llength (lappend p (LCons g'' LNil)) = enat (Suc i) by simp
                        also have "... = (if energy_level e p' i = None  llength p'  enat (Suc i) then None
                                      else apply_w (lnth p' i) (lnth p' (Suc i)) (the (energy_level e p' i)))" using energy_level.simps by simp
                        also have "... = None " using apply_w (lnth p' i) (lnth p' (Suc i)) (the (energy_level e p' i)) = None
                          by simp
                        finally have "energy_level e p' (the_enat (llength p') - 1) = None" .
                        hence "defender_wins_play e p'" unfolding defender_wins_play_def by simp

                        have "valid_play p'"
                          by (metis P p' = lappend (LCons g p) (LCons g'' LNil) weight g' g''  None energy_game.valid_play.intros(2) energy_game.valid_play_append lfinite_LConsI)

                        have "play_consistent_attacker s (lappend (LCons g p) (LCons g'' LNil)) e"
                        proof(rule play_consistent_attacker_append_one)
                          show "play_consistent_attacker s (LCons g p) e" 
                            using P by simp
                          show "lfinite (LCons g p)" using P by simp
                          show "energy_level e (LCons g p) (the_enat (llength (LCons g p)) - 1)  None"
                            using P
                            by (meson S defender_wins_play_def attacker_winning_strategy.elims(2))
                          show "valid_play (lappend (LCons g p) (LCons g'' LNil))"
                            using valid_play p' p' = lappend (LCons g p) (LCons g'' LNil) by simp
                          show "llast (LCons g p)  attacker 
    Some g'' =
    s (the (energy_level e (LCons g p) (the_enat (llength (LCons g p)) - 1))) (llast (LCons g p))"
                            using False P by simp
                        qed
                        hence "play_consistent_attacker s p' e"
                          using p' = lappend (LCons g p) (LCons g'' LNil) by simp
                        hence "¬defender_wins_play e p'" using valid_play p' p'_def S by simp
                        thus "False" using defender_wins_play e p' by simp
                      (* widerspruch weil in reachable und sonst defender_wins_play *)
                      qed

                      define x where "x = (g'', the (apply_w g' g'' e'))"
                      have "wb x" 
                      proof(rule ind)
                        have X: "(p. lfinite p 
             llast (LCons g p) = g'' 
             valid_play (LCons g p)  play_consistent_attacker s (LCons g p) e 
            Some (the (apply_w g' g'' e')) = energy_level e (LCons g p) (the_enat (llength p)))"
                        proof
                          define p' where "p' = lappend p (LCons g'' LNil)"
                          show "lfinite p' 
     llast (LCons g p') = g'' 
     valid_play (LCons g p')  play_consistent_attacker s (LCons g p') e 
    Some (the (apply_w g' g'' e')) = energy_level e (LCons g p') (the_enat (llength p'))"
                          proof
                            show "lfinite p'" using P p'_def by simp
                            show "llast (LCons g p') = g'' 
    valid_play (LCons g p') 
    play_consistent_attacker s (LCons g p') e 
    Some (the (apply_w g' g'' e')) = energy_level e (LCons g p') (the_enat (llength p'))"
                            proof
                              show "llast (LCons g p') = g''" using p'_def
                                by (metis lfinite p' lappend.disc_iff(2) lfinite_lappend llast_LCons llast_lappend_LCons llast_singleton llist.discI(2))
                              show "valid_play (LCons g p') 
    play_consistent_attacker s (LCons g p') e 
    Some (the (apply_w g' g'' e')) = energy_level e (LCons g p') (the_enat (llength p'))"
                              proof
                                show "valid_play (LCons g p')" using p'_def P
                                  using weight g' g''  None lfinite_LCons valid_play.intros(2) valid_play_append by auto
                                show "play_consistent_attacker s (LCons g p') e 
    Some (the (apply_w g' g'' e')) = energy_level e (LCons g p') (the_enat (llength p')) "
                                proof

                                  have "play_consistent_attacker s (lappend (LCons g p) (LCons g'' LNil)) e"
                                  proof(rule play_consistent_attacker_append_one)
                                    show "play_consistent_attacker s (LCons g p) e" 
                                      using P by simp
                                    show "lfinite (LCons g p)" using P by simp
                                    show "energy_level e (LCons g p) (the_enat (llength (LCons g p)) - 1)  None"
                                      using P
                                      by (meson S defender_wins_play_def attacker_winning_strategy.elims(2))
                                    show "valid_play (lappend (LCons g p) (LCons g'' LNil))"
                                      using valid_play (LCons g p') p'_def by simp
                                    show "llast (LCons g p)  attacker 
                                        Some g'' =
                                        s (the (energy_level e (LCons g p) (the_enat (llength (LCons g p)) - 1))) (llast (LCons g p))"
                                      using False P by simp
                                  qed
                                  thus "play_consistent_attacker s (LCons g p') e" using p'_def
                                    by (simp add: lappend_code(2)) 

                                  have "i. Suc i = the_enat (llength p')" using p'_def lfinite p'
                                    by (metis P length_append_singleton length_list_of_conv_the_enat lfinite_LConsI lfinite_LNil list_of_LCons list_of_LNil list_of_lappend)
                                  from this obtain i where "Suc i = the_enat (llength p')" by auto
                                  hence "i = the_enat (llength p)" using p'_def
                                    by (smt (verit) One_nat_def lfinite p' add.commute add_Suc_shift add_right_cancel length_append length_list_of_conv_the_enat lfinite_LNil lfinite_lappend list.size(3) list.size(4) list_of_LCons list_of_LNil list_of_lappend plus_1_eq_Suc)  
                                  hence "Suc i = llength (LCons g p)"
                                    using P eSuc_enat lfinite_llength_enat by fastforce
                                  have "(LCons g p') = lappend (LCons g p) (LCons g'' LNil)" using p'_def by simp
                                  have A: "lfinite (LCons g p)  i < the_enat (llength (LCons g p))   energy_level e (LCons g p) (the_enat (llength (LCons g p)) - 1)  None"
                                  proof
                                    show "lfinite (LCons g p)" using P by simp
                                    show " i < the_enat (llength (LCons g p)) 
    energy_level e (LCons g p) (the_enat (llength (LCons g p)) - 1)  None "
                                    proof
                                      have "(llength p') = llength (LCons g p)" using p'_def
                                        by (metis P lfinite p' length_Cons length_append_singleton length_list_of lfinite_LConsI lfinite_LNil list_of_LCons list_of_LNil list_of_lappend) 
                                      thus "i < the_enat (llength (LCons g p))" using Suc i = the_enat (llength p')
                                        using lessI by force 
                                      show "energy_level e (LCons g p) (the_enat (llength (LCons g p)) - 1)  None" using P
                                        by (meson S energy_game.defender_wins_play_def energy_game.play_consistent_attacker.intros(2) attacker_winning_strategy.simps)
                                    qed
                                  qed
                                  hence "energy_level e (LCons g p') i  None"
                                    using energy_level_append
                                    by (smt (verit) Nat.lessE Suc_leI LCons g p' = lappend (LCons g p) (LCons g'' LNil) diff_Suc_1 energy_level_nth)  
                                  have "enat (Suc i) < llength (LCons g p')" 
                                    using Suc i = the_enat (llength p')
                                    by (metis Suc_ile_eq lfinite p' ldropn_Suc_LCons leI lfinite_conv_llength_enat lnull_ldropn nless_le the_enat.simps) 
                                  hence  el_prems: "energy_level e (LCons g p') i  None  llength (LCons g p') > enat (Suc i)" using energy_level e (LCons g p') i  None by simp

                                  have "(lnth (LCons g p') i) = lnth (LCons g p) i" 
                                    unfolding (LCons g p') = lappend (LCons g p) (LCons g'' LNil) using i = the_enat (llength p) lnth_lappend1
                                    by (metis A enat_ord_simps(2) length_list_of length_list_of_conv_the_enat)
                                  have "lnth (LCons g p) i = llast (LCons g p)" using Suc i = llength (LCons g p)
                                    by (metis enat_ord_simps(2) lappend_LNil2 ldropn_LNil ldropn_Suc_conv_ldropn ldropn_lappend lessI less_not_refl llast_ldropn llast_singleton)
                                  hence "(lnth (LCons g p') i) = g'" using P
                                    by (simp add: lnth (LCons g p') i = lnth (LCons g p) i) 
                                  have "(lnth (LCons g p') (Suc i)) = g''"
                                    using p'_def Suc i = the_enat (llength p')
                                    by (smt (verit) enat (Suc i) < llength (LCons g p') lfinite p' llast (LCons g p') = g'' lappend_snocL1_conv_LCons2 ldropn_LNil ldropn_Suc_LCons ldropn_Suc_conv_ldropn ldropn_lappend2 lfinite_llength_enat llast_ldropn llast_singleton the_enat.simps wlog_linorder_le)

                                  have "energy_level e (LCons g p) i = energy_level e (LCons g p') i" 
                                    using energy_level_append A (LCons g p') = lappend (LCons g p) (LCons g'' LNil)
                                    by presburger
                                  hence "Some e' = (energy_level e (LCons g p') i)" 
                                    using P i = the_enat (llength p)
                                    by argo 

                                  have "energy_level e (LCons g p') (the_enat (llength p')) = energy_level e (LCons g p') (Suc i)" using Suc i = the_enat (llength p') by simp
                                  also have "... = apply_w (lnth (LCons g p') i) (lnth (LCons g p') (Suc i)) (the (energy_level e (LCons g p') i))" 
                                    using energy_level.simps el_prems
                                    by (meson leD) 
                                  also have "... = apply_w g' g'' (the (energy_level e (LCons g p') i))" 
                                    using (lnth (LCons g p') i) = g' (lnth (LCons g p') (Suc i)) = g'' by simp
                                  finally have "energy_level e (LCons g p') (the_enat (llength p')) = (apply_w g' g'' e')" 
                                    using Some e' = (energy_level e (LCons g p') i)
                                    by (metis option.sel) 
                                  thus "Some (the (apply_w g' g'' e')) = energy_level e (LCons g p') (the_enat (llength p'))"
                                    using apply_w g' g'' e'  None by auto
                                qed
                              qed
                            qed
                          qed
                        qed

                        have x_len: "(upd (the (weight g' g'')) e') energies" using y_len
                          using apply_w g' g'' e'  None weight g' g''  None upd_well_defined by auto 

                        thus "x  reachable_positions_len s g e"
                          using X x_def reachable_positions_def
                          by (simp add: mem_Collect_eq) 

                        have "Some (the (apply_w g' g'' e')) = apply_w g' g'' e' 
         (if g'  attacker then Some g'' = s e' g' else weight g' g''  None)"
                        proof
                          show "Some (the (apply_w g' g'' e')) = apply_w g' g'' e'"
                            using apply_w g' g'' e'  None by auto
                          show "(if g'  attacker then Some g'' = s e' g' else weight g' g''  None)"
                            using False
                            by (simp add: weight g' g''  None) 
                        qed
                        thus "strategy_order s x y" using strategy_order_def x_def y = (g', e')
                          by simp
                      qed

                      thus "winning_budget_len (the (apply_w g' g'' e')) g'' " using x_def wb_def 
                        by force 
                    qed
                  qed
                qed
              qed
              thus ?thesis using winning_budget_len.intros y_len by blast
            qed
            thus "wb y" using y = (g', e') wb_def by simp
          qed
        qed
      qed
      thus ?thesis using wb_def by simp
    qed
  qed
qed

end
end