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 ⟹ e∈energies
⟹ 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 ⟹ e∈energies
⟹ 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 ⟹e∈energies ⟹ 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 ⟹ e∈energies ⟹ 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 ⟹ e∈energies
⟹ 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 "e∈energies ⟹ order e (the (application (the (weight p p')) (the (inverse_application (the (weight p p')) e))))"
proof-
assume "e∈energies"
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 ‹e∈energies› ‹weight p p' ≠ None› e'_def inv_well_defined u_def by presburger
show "e∈energies" using ‹e∈energies›.
show "e'∈energies" unfolding e'_def
using ‹e∈energies› ‹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 ⟹ e∈energies
⟹ 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 "e∈energies ⟹ 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 "e∈energies" 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 ‹e∈energies› using ‹e∈energies› .
show ‹e'∈energies› unfolding e'_def using ‹e∈energies›
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 ⟹e∈energies ⟹ 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 "e∈energies" 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 ‹e∈energies› ‹weight p p' ≠ None› upd_well_defined
using ‹apply_w p p' e ≠ None› by blast
show "e'∈energies"
using ‹e∈energies› ‹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› ‹e∈energies› ‹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 ⟹ e∈energies ⟹ 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 "e∈energies ⟹ 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 "e∈energies" 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 "e∈energies" using ‹e∈energies›.
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 ‹e∈energies› 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 "∀e∈energies. ∀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 "∀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 = {e∈A . ∀e'∈A. e≠e' ⟶ ¬ (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 "e∈energies ∧ 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 "e∈energies ∧ 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
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
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
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