Theory Distinction_Implies_Winning_Budgets
section ‹Correctness›
text ‹As in the main theorem of \cite{bisping2023lineartimebranchingtime}, we state in what sense winning energy levels and equivalences coincide as the theorem ‹spectroscopy_game_correctness›:
There exists a formula ‹φ› distinguishing a process ‹p› from a set of processes ‹Q› with
expressiveness price of at most ‹e› if and only if ‹e› is in the winning budget of ‹Attacker_Immediate p Q›.
The proof is split into three lemmas. The forward direction is given by the lemma ‹distinction_implies_winning_budgets› combined with the upwards closure of winning budgets.
To show the other direction one can construct a (strategy) formula with an appropriate price using
the constructive proof of ‹winning_budget_implies_strategy_formula›. From lemma
‹strategy_formulas_distinguish› we then know that this formula actually distinguishes ‹p› from ‹Q›.
›
subsection ‹Distinction Implies Winning Budgets›
theory Distinction_Implies_Winning_Budgets
imports Spectroscopy_Game Expressiveness_Price
begin
context weak_spectroscopy_game
begin
text ‹In this section, we prove that if a formula distinguishes a process @{term ‹p›}
from a set of process @{term ‹Q›}, then the price of this formula is in the attackers-winning
budget. This is the same statement as that of lemma $1$ in the paper \cite[p. 20]{bisping2023lineartimebranchingtime}.
We likewise also prove it in the same manner.
First, we show that the statement holds if @{term ‹Q = {}›}. This is the case, as the
attacker can move, at no cost, from the starting position, @{term ‹Attacker_Immediate p {}›},
to the defender position @{term ‹Defender_Conj p {}›}. In this position the defender is then
unable to make any further moves. Hence, the attacker wins the game with any budget.›
lemma distinction_implies_winning_budgets_empty_Q:
assumes ‹distinguishes_from φ p {}›
shows ‹attacker_wins (expressiveness_price φ) (Attacker_Immediate p {})›
proof-
have is_last_move: ‹spectroscopy_moves (Defender_Conj p {}) p' = None› for p'
by(rule spectroscopy_moves.elims, auto)
moreover have ‹spectroscopy_defender (Defender_Conj p {})› by simp
ultimately have conj_win: ‹attacker_wins (expressiveness_price φ) (Defender_Conj p {})›
by (simp add: attacker_wins.Defense)
from late_inst_conj[of p ‹{}› p ‹{}›] have next_move0:
‹spectroscopy_moves (Attacker_Delayed p {}) (Defender_Conj p {}) = Some Some› by force
from delay[of p ‹{}› p ‹{}›] have next_move1:
‹spectroscopy_moves (Attacker_Immediate p {}) (Attacker_Delayed p {}) = Some Some› by force
moreover have ‹attacker (Attacker_Immediate p {})› by simp
ultimately show ?thesis using attacker_wins.Attack[of ‹Attacker_Immediate p {}› _ ‹expressiveness_price φ›]
using next_move0 next_move1
by (metis conj_win attacker_wins.Attack option.distinct(1) option.sel spectroscopy_defender.simps(4))
qed
text ‹Next, we show the statement for the case that @{term ‹Q ≠ {}›}. Following the proof of
\cite[p. 20]{bisping2023lineartimebranchingtime}, we do this by induction on a more
complex property.›
lemma distinction_implies_winning_budgets:
assumes ‹distinguishes_from φ p Q›
shows ‹attacker_wins (expressiveness_price φ) (Attacker_Immediate p Q)›
proof-
have ‹⋀φ χ ψ.
(∀Q p. Q ≠ {} ⟶ distinguishes_from φ p Q
⟶ attacker_wins (expressiveness_price φ) (Attacker_Immediate p Q))
∧
((∀p Q. Q ≠ {} ⟶ hml_srbb_inner.distinguishes_from χ p Q ⟶ Q ↠S Q
⟶ attacker_wins (expr_pr_inner χ) (Attacker_Delayed p Q))
∧ (∀Ψ_I Ψ p Q. χ = Conj Ψ_I Ψ ⟶
Q ≠ {} ⟶ hml_srbb_inner.distinguishes_from χ p Q
⟶ attacker_wins (expr_pr_inner χ) (Defender_Conj p Q))
∧ (∀Ψ_I Ψ p Q. χ = StableConj Ψ_I Ψ ⟶
Q ≠ {} ⟶ hml_srbb_inner.distinguishes_from χ p Q ⟶ (∀q ∈ Q. ∄q'. q ↦ τ q')
⟶ attacker_wins (expr_pr_inner χ) (Defender_Stable_Conj p Q))
∧ (∀Ψ_I Ψ α φ p Q p' Q_α. χ = BranchConj α φ Ψ_I Ψ ⟶
hml_srbb_inner.distinguishes_from χ p Q ⟶ p ↦a α p' ⟶ p' ⊨SRBB φ ⟶
Q_α = Q - hml_srbb_inner.model_set (Obs α φ)
⟶ attacker_wins (expr_pr_inner χ) (Defender_Branch p α p' (Q - Q_α) Q_α)))
∧
(∀p q. hml_srbb_conj.distinguishes ψ p q
⟶ attacker_wins (expr_pr_conjunct ψ) (Attacker_Clause p q))›
proof -
fix φ χ ψ
show ‹(∀Q p. Q ≠ {} ⟶ distinguishes_from φ p Q
⟶ attacker_wins (expressiveness_price φ) (Attacker_Immediate p Q))
∧
((∀p Q. Q ≠ {} ⟶ hml_srbb_inner.distinguishes_from χ p Q ⟶ Q ↠S Q
⟶ attacker_wins (expr_pr_inner χ) (Attacker_Delayed p Q))
∧ (∀Ψ_I Ψ p Q. χ = Conj Ψ_I Ψ ⟶
Q ≠ {} ⟶ hml_srbb_inner.distinguishes_from χ p Q
⟶ attacker_wins (expr_pr_inner χ) (Defender_Conj p Q))
∧ (∀Ψ_I Ψ p Q. χ = StableConj Ψ_I Ψ ⟶
Q ≠ {} ⟶ hml_srbb_inner.distinguishes_from χ p Q ⟶ (∀q ∈ Q. ∄q'. q ↦ τ q')
⟶ attacker_wins (expr_pr_inner χ) (Defender_Stable_Conj p Q))
∧ (∀Ψ_I Ψ α φ p Q p' Q_α. χ = BranchConj α φ Ψ_I Ψ ⟶
hml_srbb_inner.distinguishes_from χ p Q ⟶ p ↦a α p' ⟶ p' ⊨SRBB φ ⟶
Q_α = Q - hml_srbb_inner.model_set (Obs α φ)
⟶ attacker_wins (expr_pr_inner χ) (Defender_Branch p α p' (Q - Q_α) Q_α)))
∧
(∀p q. hml_srbb_conj.distinguishes ψ p q
⟶ attacker_wins (expr_pr_conjunct ψ) (Attacker_Clause p q))›
proof (induct rule: hml_srbb_hml_srbb_inner_hml_srbb_conjunct.induct[of _ _ _ φ χ ψ])
case TT
then show ?case
proof (clarify)
fix Q p
assume ‹Q ≠ {}›
and ‹distinguishes_from TT p Q›
hence ‹∃q. q ∈ Q›
by blast
then obtain q where ‹q ∈ Q› by auto
from ‹distinguishes_from TT p Q›
and ‹q ∈ Q›
have ‹distinguishes TT p q›
using distinguishes_from_def by auto
with verum_never_distinguishes
show ‹attacker_wins (expressiveness_price TT) (Attacker_Immediate p Q)›
by blast
qed
next
case (Internal χ)
show ?case
proof (clarify)
fix Q p
assume ‹Q ≠ {}›
and ‹distinguishes_from (Internal χ) p Q›
then have ‹∃p'. p ↠ p' ∧ hml_srbb_inner_models p' χ›
and ‹∀q ∈ Q. (∄q'. q ↠ q' ∧ hml_srbb_inner_models q' χ)›
by auto
hence ‹∀q ∈ Q. (∀q'. q ↠ q' ⟶ ¬(hml_srbb_inner_models q' χ))› by auto
then have ‹∀q ∈ Q. (∀q'∈Q'. q ↠ q' ⟶ ¬(hml_srbb_inner_models q' χ))›
for Q' by blast
then have ‹Q ↠S Q' ⟶ (∀q' ∈ Q'. ¬(hml_srbb_inner_models q' χ))›
for Q' using ‹Q ≠ {}› by blast
define Qτ where ‹Qτ ≡ silent_reachable_set Q›
with ‹⋀Q'. Q ↠S Q' ⟶ (∀q' ∈ Q'. ¬(hml_srbb_inner_models q' χ))›
have ‹∀q' ∈ Qτ. ¬(hml_srbb_inner_models q' χ)›
using sreachable_set_is_sreachable by presburger
have ‹Qτ ↠S Qτ› unfolding Qτ_def
by (metis silent_reachable_trans sreachable_set_is_sreachable
silent_reachable.intros(1))
from ‹∃p'. p ↠ p' ∧ (hml_srbb_inner_models p' χ)›
obtain p' where ‹p ↠ p'› and ‹hml_srbb_inner_models p' χ› by auto
from this(1) have ‹p ↠L p'› by(rule silent_reachable_impl_loopless)
have ‹Qτ ≠ {}›
using silent_reachable.intros(1) sreachable_set_is_sreachable Qτ_def ‹Q ≠ {}›
by fastforce
from ‹hml_srbb_inner_models p' χ›
and ‹∀q' ∈ Qτ. ¬(hml_srbb_inner_models q' χ)›
have ‹hml_srbb_inner.distinguishes_from χ p' Qτ› by simp
with ‹Qτ ↠S Qτ› ‹Qτ ≠ {}› Internal
have ‹attacker_wins (expr_pr_inner χ) (Attacker_Delayed p' Qτ)›
by blast
moreover have ‹expr_pr_inner χ = expressiveness_price (Internal χ)› by simp
ultimately have ‹attacker_wins (expressiveness_price (Internal χ))
(Attacker_Delayed p' Qτ)› by simp
hence ‹attacker_wins (expressiveness_price (Internal χ)) (Attacker_Delayed p Qτ)›
proof(induct rule: silent_reachable_loopless.induct[of ‹p› ‹p'›, OF ‹p ↠L p'›])
case (1 p)
thus ?case by simp
next
case (2 p p' p'')
hence ‹attacker_wins (expressiveness_price (Internal χ)) (Attacker_Delayed p' Qτ)›
by simp
moreover have ‹spectroscopy_moves (Attacker_Delayed p Qτ) (Attacker_Delayed p' Qτ)
= Some Some› using spectroscopy_moves.simps(2) ‹p ≠ p'› ‹p ↦τ p'› by auto
moreover have ‹attacker (Attacker_Delayed p Qτ)› by simp
ultimately show ?case using attacker_wins_Ga_with_id_step by auto
qed
have ‹Q ↠S Qτ›
using Qτ_def sreachable_set_is_sreachable by simp
hence ‹spectroscopy_moves (Attacker_Immediate p Q) (Attacker_Delayed p Qτ) = Some Some›
using spectroscopy_moves.simps(1) by simp
with ‹attacker_wins (expressiveness_price (Internal χ)) (Attacker_Delayed p Qτ)›
show ‹attacker_wins (expressiveness_price (Internal χ)) (Attacker_Immediate p Q)›
using attacker_wins_Ga_with_id_step
by (metis option.discI option.sel spectroscopy_defender.simps(1))
qed
next
case (ImmConj I ψs)
show ?case
proof (clarify)
fix Q p
assume ‹Q ≠ {}› and ‹distinguishes_from (ImmConj I ψs) p Q›
from this(2) have ‹∀q∈Q. p ⊨SRBB ImmConj I ψs ∧ ¬ q ⊨SRBB ImmConj I ψs›
unfolding distinguishes_from_def distinguishes_def by blast
hence ‹∀q∈Q. ∃i∈I. hml_srbb_conjunct_models p (ψs i) ∧ ¬hml_srbb_conjunct_models q (ψs i)›
by simp
hence ‹∀q∈Q. ∃i∈I. hml_srbb_conj.distinguishes (ψs i) p q›
using hml_srbb_conj.distinguishes_def by simp
hence ‹∀q∈Q. ∃i∈I. ((ψs i) ∈ range ψs) ∧ hml_srbb_conj.distinguishes (ψs i) p q› by blast
hence ‹∀q∈Q. ∃i∈I. attacker_wins (expr_pr_conjunct (ψs i)) (Attacker_Clause p q)› using ImmConj by blast
hence a_clause_wina: ‹∀q∈Q. ∃i∈I. attacker_wins (expressiveness_price (ImmConj I ψs) - E 0 0 1 0 1 0 0 0) (Attacker_Clause p q)›
using expressiveness_price_ImmConj_geq_parts win_a_upwards_closure by fast
from this ‹Q ≠ {}› have ‹I ≠ {}› by blast
hence subtracts:
‹subtract_fn 0 0 1 0 1 0 0 0 (expressiveness_price (ImmConj I ψs)) = Some (expressiveness_price (ImmConj I ψs) - E 0 0 1 0 1 0 0 0)›
‹subtract_fn 0 0 1 0 0 0 0 0 (expressiveness_price (ImmConj I ψs) - E 0 0 0 0 1 0 0 0) = Some (expressiveness_price (ImmConj I ψs) - E 0 0 1 0 1 0 0 0)›
by (simp add: ‹I ≠ {}›)+
have def_conj: ‹spectroscopy_defender (Defender_Conj p Q)› by simp
have ‹spectroscopy_moves (Defender_Conj p Q) N ≠ None
⟹ N = Attacker_Clause (attacker_state N) (defender_state N)› for N
by (metis spectroscopy_moves.simps(34,35,36,38,64,74) spectroscopy_position.exhaust_sel)
hence move_kind: ‹spectroscopy_moves (Defender_Conj p Q) N ≠ None ⟹ ∃q∈Q. N = Attacker_Clause p q› for N
using conj_answer by metis
hence update: ‹⋀g'. spectroscopy_moves (Defender_Conj p Q) g' ≠ None ⟹
weight (Defender_Conj p Q) g' = subtract_fn 0 0 1 0 0 0 0 0›
by fastforce
hence move_wina: ‹⋀g'. spectroscopy_moves (Defender_Conj p Q) g' ≠ None ⟹
(subtract_fn 0 0 1 0 0 0 0 0) (expressiveness_price (ImmConj I ψs) - E 0 0 0 0 1 0 0 0) = Some (expressiveness_price (ImmConj I ψs) - E 0 0 1 0 1 0 0 0) ∧
attacker_wins (expressiveness_price (ImmConj I ψs) - E 0 0 1 0 1 0 0 0) g'›
using move_kind a_clause_wina subtracts by blast
from attacker_wins_Gd[OF def_conj] update move_wina have def_conj_wina:
‹attacker_wins (expressiveness_price (ImmConj I ψs) - E 0 0 0 0 1 0 0 0) (Defender_Conj p Q)›
by blast
have imm_to_conj: ‹spectroscopy_moves (Attacker_Immediate p Q) (Defender_Conj p Q) ≠ None›
by (simp add: ‹Q ≠ {}›)
have imm_to_conj_wgt: ‹weight (Attacker_Immediate p Q) (Defender_Conj p Q) (expressiveness_price (ImmConj I ψs))
= Some (expressiveness_price (ImmConj I ψs) - E 0 0 0 0 1 0 0 0)›
using ‹Q ≠ {}› leq_components subtracts(1) by force
from Attack[OF _ imm_to_conj imm_to_conj_wgt] def_conj_wina
show ‹attacker_wins (expressiveness_price (ImmConj I ψs)) (Attacker_Immediate p Q)›
by simp
qed
next
case (Obs α φ)
have ‹∀p Q. Q ≠ {} ⟶ hml_srbb_inner.distinguishes_from (hml_srbb_inner.Obs α φ) p Q ⟶ Q ↠S Q
⟶ attacker_wins (expr_pr_inner (hml_srbb_inner.Obs α φ)) (Attacker_Delayed p Q)›
proof(clarify)
fix p Q
assume ‹Q ≠ {}› ‹hml_srbb_inner.distinguishes_from (hml_srbb_inner.Obs α φ) p Q› ‹ ∀p∈Q. ∀q. p ↠ q ⟶ q ∈ Q›
have ‹∃p' Q'. p ↦a α p' ∧ Q ↦aS α Q' ∧ attacker_wins (expressiveness_price φ) (Attacker_Immediate p' Q')›
proof(cases ‹α = τ›)
case True
with ‹hml_srbb_inner.distinguishes_from (hml_srbb_inner.Obs α φ) p Q›
have dist_unfold: ‹((∃p'. p ↦τ p' ∧ p' ⊨SRBB φ) ∨ p ⊨SRBB φ)› by simp
then obtain p' where ‹p' ⊨SRBB φ› ‹p ↦a α p'›
unfolding True by blast
from ‹hml_srbb_inner.distinguishes_from (hml_srbb_inner.Obs α φ) p Q› have
‹∀q∈Q. (¬ q ⊨SRBB φ) ∧ (∄q'. q ↦τ q' ∧ q' ⊨SRBB φ)›
using True by auto
hence ‹∀q∈Q. ¬q ⊨SRBB φ›
using ‹∀p∈Q. ∀q. p ↠ q ⟶ q ∈ Q› by fastforce
hence ‹distinguishes_from φ p' Q›
using ‹p' ⊨SRBB φ› by auto
with Obs have ‹attacker_wins (expressiveness_price φ) (Attacker_Immediate p' Q)›
using ‹Q ≠ {}› by blast
moreover have ‹Q ↦aS α Q›
unfolding True
using ‹∀p∈Q. ∀q. p ↠ q ⟶ q ∈ Q› silent_reachable_append_τ silent_reachable.intros(1) by blast
ultimately show ?thesis using ‹p ↦a α p'› by blast
next
case False
with ‹hml_srbb_inner.distinguishes_from (hml_srbb_inner.Obs α φ) p Q›
obtain p'' where ‹(p ↦α p'') ∧ (p'' ⊨SRBB φ)› by auto
let ?Q' = ‹step_set Q α›
from ‹hml_srbb_inner.distinguishes_from (hml_srbb_inner.Obs α φ) p Q›
have ‹∀q∈?Q'. ¬ q ⊨SRBB φ›
using ‹Q ≠ {}› and step_set_is_step_set
by force
from ‹∀q∈step_set Q α. ¬ q ⊨SRBB φ› ‹p ↦α p'' ∧ p'' ⊨SRBB φ›
have ‹distinguishes_from φ p'' ?Q'› by simp
hence ‹attacker_wins (expressiveness_price φ) (Attacker_Immediate p'' ?Q')›
by (metis Obs distinction_implies_winning_budgets_empty_Q)
moreover have ‹p ↦α p''› using ‹p ↦α p'' ∧ p'' ⊨SRBB φ› by simp
moreover have ‹Q ↦aS α ?Q'› by (simp add: False LTS.step_set_is_step_set)
ultimately show ?thesis by blast
qed
then obtain p' Q' where p'_Q': ‹p ↦a α p'› ‹Q ↦aS α Q'› and
wina: ‹attacker_wins (expressiveness_price φ) (Attacker_Immediate p' Q')› by blast
have attacker: ‹attacker (Attacker_Delayed p Q)› by simp
have ‹spectroscopy_moves (Attacker_Delayed p Q) (Attacker_Immediate p' Q') =
(if (∃a. p ↦a a p' ∧ Q ↦aS a Q') then Some (subtract_fn 1 0 0 0 0 0 0 0) else None)›
for p Q p' Q' by simp
from this[of p Q p' Q'] have
‹spectroscopy_moves (Attacker_Delayed p Q) (Attacker_Immediate p' Q') =
Some (subtract_fn 1 0 0 0 0 0 0 0)› using p'_Q' by auto
with expr_obs_phi[of α φ] show
‹attacker_wins (expr_pr_inner (hml_srbb_inner.Obs α φ)) (Attacker_Delayed p Q)›
using Attack[OF attacker _ _ wina]
by (smt (verit, best) option.sel option.simps(3))
qed
then show ?case by fastforce
next
case (Conj I ψs)
have main_case: ‹∀Ψ_I Ψ p Q. hml_srbb_inner.Conj I ψs = hml_srbb_inner.Conj Ψ_I Ψ ⟶
Q ≠ {} ⟶ hml_srbb_inner.distinguishes_from (hml_srbb_inner.Conj I ψs) p Q
⟶ attacker_wins (expr_pr_inner (hml_srbb_inner.Conj I ψs)) (Defender_Conj p Q)›
proof clarify
fix p Q
assume case_assms:
‹Q ≠ {}›
‹hml_srbb_inner.distinguishes_from (hml_srbb_inner.Conj I ψs) p Q›
hence distinctions: ‹∀q∈Q. ∃i∈I. hml_srbb_conj.distinguishes (ψs i) p q›
by auto
hence inductive_wins: ‹∀q∈Q. ∃i∈I. hml_srbb_conj.distinguishes (ψs i) p q
∧ attacker_wins (expr_pr_conjunct (ψs i)) (Attacker_Clause p q)›
using Conj by blast
define ψqs where
‹ψqs ≡ λq. (SOME ψ. ∃i∈I. ψ = ψs i ∧ hml_srbb_conj.distinguishes ψ p q
∧ attacker_wins (expr_pr_conjunct ψ) (Attacker_Clause p q))›
with inductive_wins someI have ψqs_spec:
‹∀q∈Q. ∃i∈I. ψqs q = ψs i ∧ hml_srbb_conj.distinguishes (ψqs q ) p q
∧ attacker_wins (expr_pr_conjunct (ψqs q)) (Attacker_Clause p q)›
by (smt (verit))
have conjuncts_present: ‹∀q∈Q. expr_pr_conjunct (ψqs q) ∈ expr_pr_conjunct ` (ψqs ` Q)›
using ‹Q ≠ {}› by blast
define e' where ‹e' = E
(Sup (modal_depth ` (expr_pr_conjunct ` (ψqs ` Q))))
(Sup (br_conj_depth ` (expr_pr_conjunct ` (ψqs ` Q))))
(Sup (conj_depth ` (expr_pr_conjunct ` (ψqs ` Q))))
(Sup (st_conj_depth ` (expr_pr_conjunct ` (ψqs ` Q))))
(Sup (imm_conj_depth ` (expr_pr_conjunct ` (ψqs ` Q))))
(Sup (pos_conjuncts ` (expr_pr_conjunct ` (ψqs ` Q))))
(Sup (neg_conjuncts ` (expr_pr_conjunct ` (ψqs ` Q))))
(Sup (neg_depth ` (expr_pr_conjunct ` (ψqs ` Q))))›
from conjuncts_present have ‹∀q∈Q. (expr_pr_conjunct (ψqs q)) ≤ e'›
unfolding e'_def
by (metis SUP_upper energy.sel leq_components)
with ψqs_spec win_a_upwards_closure
have clause_win: ‹∀q∈Q. attacker_wins e' (Attacker_Clause p q)› by blast
define eu' where ‹eu' = E
(Sup (modal_depth ` (expr_pr_conjunct ` (ψs ` I))))
(Sup (br_conj_depth ` (expr_pr_conjunct ` (ψs ` I))))
(Sup (conj_depth ` (expr_pr_conjunct ` (ψs ` I))))
(Sup (st_conj_depth ` (expr_pr_conjunct ` (ψs ` I))))
(Sup (imm_conj_depth ` (expr_pr_conjunct ` (ψs ` I))))
(Sup (pos_conjuncts ` (expr_pr_conjunct ` (ψs ` I))))
(Sup (neg_conjuncts ` (expr_pr_conjunct ` (ψs ` I))))
(Sup (neg_depth ` (expr_pr_conjunct ` (ψs ` I))))›
have subset_form: ‹ψqs ` Q ⊆ ψs ` I›
using ψqs_spec by fastforce
hence ‹e' ≤ eu'› unfolding e'_def eu'_def leq_components
by (simp add: Sup_subset_mono image_mono)
define e where ‹e = E
(modal_depth e')
(br_conj_depth e')
(1 + conj_depth e')
(st_conj_depth e')
(imm_conj_depth e')
(pos_conjuncts e')
(neg_conjuncts e')
(neg_depth e')›
have ‹e' = e - (E 0 0 1 0 0 0 0 0)› unfolding e_def e'_def by simp
hence ‹Some e' = (subtract_fn 0 0 1 0 0 0 0 0) e›
by (auto, smt (verit) add_increasing2 e_def energy.sel energy_leq_cases i0_lb le_numeral_extra(4))
have expr_lower: ‹(E 0 0 1 0 0 0 0 0) ≤ expr_pr_inner (Conj I ψs)›
using case_assms(1) subset_form by auto
have eu'_comp: ‹eu' = (expr_pr_inner (Conj I ψs)) - (E 0 0 1 0 0 0 0 0)›
unfolding eu'_def
by (auto simp add: bot_enat_def image_image)
with expr_lower have eu'_characterization: ‹Some eu' = (subtract_fn 0 0 1 0 0 0 0 0) (expr_pr_inner (Conj I ψs))›
by presburger
have ‹∀g'. spectroscopy_moves (Defender_Conj p Q) g' ≠ None
⟶ (∃q∈Q. (Attacker_Clause p q) = g') ∧ spectroscopy_moves (Defender_Conj p Q) g' = Some (subtract_fn 0 0 1 0 0 0 0 0)›
proof clarify
fix g' upd
assume upd_def: ‹spectroscopy_moves (Defender_Conj p Q) g' = Some upd›
hence ‹⋀px q. g' = Attacker_Clause px q ⟹ p = px ∧ q ∈ Q ∧ upd = (subtract_fn 0 0 1 0 0 0 0 0)›
by (metis (mono_tags, lifting) local.conj_answer option.sel option.simps(3))
with upd_def show ‹(∃q∈Q. Attacker_Clause p q = g') ∧ spectroscopy_moves (Defender_Conj p Q) g' = Some (subtract_fn 0 0 1 0 0 0 0 0)›
by (cases g', auto)
qed
hence ‹∀g'. spectroscopy_moves (Defender_Conj p Q) g' ≠ None
⟶ (∃e'. (the (spectroscopy_moves (Defender_Conj p Q) g')) e = Some e' ∧ attacker_wins e' g')›
unfolding e_def
using clause_win ‹Some e' = (subtract_fn 0 0 1 0 0 0 0 0) e› e_def by force
hence ‹attacker_wins e (Defender_Conj p Q)›
unfolding e_def using attacker_wins.Defense
by auto
moreover have ‹e ≤ expr_pr_inner (Conj I ψs)›
using ‹e' ≤ eu'› eu'_characterization ‹Some e' = (subtract_fn 0 0 1 0 0 0 0 0) e› expr_lower case_assms(1) subset_form
unfolding e_def
by (smt (verit, ccfv_threshold) eu'_comp add_diff_cancel_enat
add_mono_thms_linordered_semiring(1) enat.simps(3) enat_defs(2) energy.sel
expr_pr_inner.simps idiff_0_right inst_conj_depth_inner.simps(2) le_numeral_extra(4)
leq_components minus_energy_def not_one_le_zero)
ultimately show ‹attacker_wins (expr_pr_inner (hml_srbb_inner.Conj I ψs)) (Defender_Conj p Q)›
using win_a_upwards_closure by blast
qed
moreover have
‹∀p Q. Q ≠ {} ⟶ hml_srbb_inner.distinguishes_from (hml_srbb_inner.Conj I ψs) p Q ⟶ Q ↠S Q
⟶ attacker_wins (expr_pr_inner (hml_srbb_inner.Conj I ψs)) (Attacker_Delayed p Q)›
proof clarify
fix p Q
assume
‹Q ≠ {}›
‹hml_srbb_inner.distinguishes_from (hml_srbb_inner.Conj I ψs) p Q›
hence ‹attacker_wins (expr_pr_inner (hml_srbb_inner.Conj I ψs)) (Defender_Conj p Q)›
using main_case by blast
moreover have ‹spectroscopy_moves (Attacker_Delayed p Q) (Defender_Conj p Q) = Some Some›
by auto
ultimately show ‹attacker_wins (expr_pr_inner (hml_srbb_inner.Conj I ψs)) (Attacker_Delayed p Q)›
by (metis attacker_wins_Ga_with_id_step option.discI option.sel spectroscopy_defender.simps(4))
qed
ultimately show ?case by fastforce
next
case (StableConj I ψs)
have main_case: ‹(∀Ψ_I Ψ p Q. StableConj I ψs = StableConj Ψ_I Ψ ⟶
Q ≠ {} ⟶ hml_srbb_inner.distinguishes_from (StableConj I ψs) p Q ⟶ (∀q∈Q. ∄q'. q ↦τ q')
⟶ attacker_wins (expr_pr_inner (StableConj I ψs)) (Defender_Stable_Conj p Q))›
proof clarify
fix p Q
assume case_assms:
‹Q ≠ {}›
‹hml_srbb_inner.distinguishes_from (StableConj I ψs) p Q›
‹∀q∈Q. ∄q'. q ↦τ q'›
hence distinctions: ‹∀q∈Q. ∃i∈I. hml_srbb_conj.distinguishes (ψs i) p q›
by (metis hml_srbb_conj.distinguishes_def hml_srbb_inner.distinguishes_from_def hml_srbb_inner_models.simps(3))
hence inductive_wins: ‹∀q∈Q. ∃i∈I. hml_srbb_conj.distinguishes (ψs i) p q
∧ attacker_wins (expr_pr_conjunct (ψs i)) (Attacker_Clause p q)›
using StableConj by blast
define ψqs where
‹ψqs ≡ λq. (SOME ψ. ∃i∈I. ψ = ψs i ∧ hml_srbb_conj.distinguishes ψ p q
∧ attacker_wins (expr_pr_conjunct ψ) (Attacker_Clause p q))›
with inductive_wins someI have ψqs_spec:
‹∀q∈Q. ∃i∈I. ψqs q = ψs i ∧ hml_srbb_conj.distinguishes (ψqs q ) p q
∧ attacker_wins (expr_pr_conjunct (ψqs q)) (Attacker_Clause p q)›
by (smt (verit))
have conjuncts_present: ‹∀q∈Q. expr_pr_conjunct (ψqs q) ∈ expr_pr_conjunct ` (ψqs ` Q)›
using ‹Q ≠ {}› by blast
define e' where ‹e' = E
(Sup (modal_depth ` (expr_pr_conjunct ` (ψqs ` Q))))
(Sup (br_conj_depth ` (expr_pr_conjunct ` (ψqs ` Q))))
(Sup (conj_depth ` (expr_pr_conjunct ` (ψqs ` Q))))
(Sup (st_conj_depth ` (expr_pr_conjunct ` (ψqs ` Q))))
(Sup (imm_conj_depth ` (expr_pr_conjunct ` (ψqs ` Q))))
(Sup (pos_conjuncts ` (expr_pr_conjunct ` (ψqs ` Q))))
(Sup (neg_conjuncts ` (expr_pr_conjunct ` (ψqs ` Q))))
(Sup (neg_depth ` (expr_pr_conjunct ` (ψqs ` Q))))›
from conjuncts_present have ‹∀q∈Q. (expr_pr_conjunct (ψqs q)) ≤ e'› unfolding e'_def
by (smt (verit, best) SUP_upper energy.sel energy.simps(3) energy_leq_cases image_iff)
with ψqs_spec win_a_upwards_closure
have clause_win: ‹∀q∈Q. attacker_wins e' (Attacker_Clause p q)› by blast
define eu' where ‹eu' = E
(Sup (modal_depth ` (expr_pr_conjunct ` (ψs ` I))))
(Sup (br_conj_depth ` (expr_pr_conjunct ` (ψs ` I))))
(Sup (conj_depth ` (expr_pr_conjunct ` (ψs ` I))))
(Sup (st_conj_depth ` (expr_pr_conjunct ` (ψs ` I))))
(Sup (imm_conj_depth ` (expr_pr_conjunct ` (ψs ` I))))
(Sup (pos_conjuncts ` (expr_pr_conjunct ` (ψs ` I))))
(Sup (neg_conjuncts ` (expr_pr_conjunct ` (ψs ` I))))
(Sup (neg_depth ` (expr_pr_conjunct ` (ψs ` I))))›
have subset_form: ‹ψqs ` Q ⊆ ψs ` I›
using ψqs_spec by fastforce
hence ‹e' ≤ eu'› unfolding e'_def eu'_def
by (simp add: Sup_subset_mono image_mono)
define e where ‹e = E
(modal_depth e')
(br_conj_depth e')
(conj_depth e')
(1 + st_conj_depth e')
(imm_conj_depth e')
(pos_conjuncts e')
(neg_conjuncts e')
(neg_depth e')›
have ‹e' = e - (E 0 0 0 1 0 0 0 0)› unfolding e_def e'_def by auto
hence ‹Some e' = (subtract_fn 0 0 0 1 0 0 0 0) e›
by (metis e_def energy.sel energy_leq_cases i0_lb le_iff_add)
have expr_lower: ‹(E 0 0 0 1 0 0 0 0) ≤ expr_pr_inner (StableConj I ψs)›
using case_assms(1) subset_form by force
have eu'_comp: ‹eu' = (expr_pr_inner (StableConj I ψs)) - (E 0 0 0 1 0 0 0 0)›
unfolding eu'_def using energy.sel
by (auto simp add: bot_enat_def, (metis (no_types, lifting) SUP_cong image_image)+)
with expr_lower have eu'_characterization: ‹Some eu' = (subtract_fn 0 0 0 1 0 0 0 0) (expr_pr_inner (StableConj I ψs))›
by presburger
have ‹∀g'. spectroscopy_moves (Defender_Stable_Conj p Q) g' ≠ None
⟶ (∃q∈Q. (Attacker_Clause p q) = g') ∧ spectroscopy_moves (Defender_Stable_Conj p Q) g' = (subtract 0 0 0 1 0 0 0 0)›
proof clarify
fix g' upd
assume upd_def: ‹spectroscopy_moves (Defender_Stable_Conj p Q) g' = Some upd›
hence ‹⋀px q. g' = Attacker_Clause px q ⟹ p = px ∧ q ∈ Q ∧ upd = (subtract_fn 0 0 0 1 0 0 0 0)›
by (metis (no_types, lifting) local.conj_s_answer option.discI option.inject)
with upd_def case_assms(1) show
‹(∃q∈Q. Attacker_Clause p q = g') ∧ spectroscopy_moves (Defender_Stable_Conj p Q) g' = (subtract 0 0 0 1 0 0 0 0)›
by (cases g', auto)
qed
hence ‹∀g'. spectroscopy_moves (Defender_Stable_Conj p Q) g' ≠ None
⟶ (∃e'. (the (spectroscopy_moves (Defender_Stable_Conj p Q) g')) e = Some e' ∧ attacker_wins e' g')›
unfolding e_def
using clause_win ‹Some e' = (subtract_fn 0 0 0 1 0 0 0 0) e› e_def by force
hence ‹attacker_wins e (Defender_Stable_Conj p Q)›
unfolding e_def
by (auto simp add: attacker_wins.Defense)
moreover have ‹e ≤ expr_pr_inner (StableConj I ψs)›
using ‹e' ≤ eu'› eu'_characterization ‹Some e' = (subtract_fn 0 0 0 1 0 0 0 0) e› expr_lower case_assms(1) subset_form
unfolding e_def eu'_comp minus_energy_def leq_components
by (metis add_diff_assoc_enat add_diff_cancel_enat add_left_mono enat.simps(3) enat_defs(2) energy.sel idiff_0_right)
ultimately show ‹attacker_wins (expr_pr_inner (StableConj I ψs)) (Defender_Stable_Conj p Q)›
using win_a_upwards_closure by blast
qed
moreover have
‹(∀p Q. Q ≠ {} ⟶ hml_srbb_inner.distinguishes_from (StableConj I ψs) p Q ⟶ Q ↠S Q
⟶ attacker_wins (expr_pr_inner (StableConj I ψs)) (Attacker_Delayed p Q))›
proof clarify
fix p Q
assume case_assms:
‹Q ≠ {}›
‹hml_srbb_inner.distinguishes_from (StableConj I ψs) p Q›
‹∀q'∈Q. ∃q∈Q. q ↠ q'›
‹∀q∈Q. ∀q'. q ↠ q' ⟶ q' ∈ Q›
define Q' where ‹Q' = { q ∈ Q. (∄q'. q ↦τ q')}›
with case_assms(2) have Q'_spec: ‹hml_srbb_inner.distinguishes_from (StableConj I ψs) p Q'› ‹∄p''. p ↦τ p''›
unfolding hml_srbb_inner.distinguishes_from_def by auto
hence move: ‹spectroscopy_moves (Attacker_Delayed p Q) (Defender_Stable_Conj p Q') = Some Some›
unfolding Q'_def by auto
show ‹attacker_wins (expr_pr_inner (StableConj I ψs)) (Attacker_Delayed p Q)›
proof (cases ‹Q' = {}›)
case True
hence
‹spectroscopy_moves (Defender_Stable_Conj p Q') (Defender_Conj p {})
= (subtract 0 0 0 1 0 0 0 0)› by auto
moreover have
‹∀g'. spectroscopy_moves (Defender_Stable_Conj p Q') g' ≠ None ⟶ g' = (Defender_Conj p {})›
proof clarify
fix g' u
assume
‹spectroscopy_moves (Defender_Stable_Conj p Q') g' = Some u›
with True show ‹g' = Defender_Conj p {}›
by (induct g', auto, metis option.discI, metis empty_iff option.discI)
qed
ultimately have win_transfer:
‹∀e. E 0 0 0 1 0 0 0 0 ≤ e ∧ attacker_wins (e - E 0 0 0 1 0 0 0 0) (Defender_Conj p {}) ⟶ attacker_wins e (Defender_Stable_Conj p Q')›
using attacker_wins.Defense
by (smt (verit, ccfv_SIG) option.sel spectroscopy_defender.simps(7))
have ‹∀g'. spectroscopy_moves (Defender_Conj p {}) g' = None›
proof
fix g'
show ‹spectroscopy_moves (Defender_Conj p {}) g' = None› by (induct g', auto)
qed
hence ‹∀e. attacker_wins e (Defender_Conj p {})› using attacker_wins_Gd by fastforce
moreover have ‹∀e. (subtract_fn 0 0 0 1 0 0 0 0) e ≠ None ⟶ e ≥ (E 0 0 0 1 0 0 0 0)›
using minus_energy_def by presburger
ultimately have ‹∀e. e ≥ (E 0 0 0 1 0 0 0 0) ⟶ attacker_wins e (Defender_Stable_Conj p Q')›
using win_transfer by presburger
moreover have ‹expr_pr_inner (StableConj I ψs) ≥ (E 0 0 0 1 0 0 0 0)›
by auto
ultimately show ?thesis
by (metis move attacker_wins_Ga_with_id_step option.discI option.sel spectroscopy_defender.simps(4))
next
case False
with move show ?thesis using main_case Q'_spec attacker_wins_Ga_with_id_step unfolding Q'_def
by (metis (mono_tags, lifting) mem_Collect_eq option.distinct(1) option.sel spectroscopy_defender.simps(4))
qed
qed
ultimately show ?case by blast
next
case (BranchConj α φ I ψs)
have main_case:
‹∀p Q p' Q_α.
hml_srbb_inner.distinguishes_from (BranchConj α φ I ψs) p Q ⟶ p ↦a α p' ⟶ p' ⊨SRBB φ ⟶
Q_α = Q - hml_srbb_inner.model_set (Obs α φ)
⟶ attacker_wins (expr_pr_inner (BranchConj α φ I ψs)) (Defender_Branch p α p' (Q - Q_α) Q_α)›
proof ((rule allI)+, (rule impI)+)
fix p Q p' Q_α
assume case_assms:
‹hml_srbb_inner.distinguishes_from (BranchConj α φ I ψs) p Q›
‹p ↦a α p'›
‹p' ⊨SRBB φ›
‹Q_α = Q - hml_srbb_inner.model_set (Obs α φ)›
from case_assms(1) have distinctions:
‹∀q∈(Q ∩ hml_srbb_inner.model_set (Obs α φ)).
∃i∈I. hml_srbb_conj.distinguishes (ψs i) p q›
using srbb_dist_branch_conjunction_implies_dist_conjunct_or_branch
hml_srbb_inner.distinction_unlifting unfolding hml_srbb_inner.distinguishes_def
by (metis Int_Collect)
hence inductive_wins: ‹∀q∈(Q ∩ hml_srbb_inner.model_set (Obs α φ)).
∃i∈I. hml_srbb_conj.distinguishes (ψs i) p q
∧ attacker_wins (expr_pr_conjunct (ψs i)) (Attacker_Clause p q)›
using BranchConj by blast
define ψqs where
‹ψqs ≡ λq. (SOME ψ. ∃i∈I. ψ = ψs i ∧ hml_srbb_conj.distinguishes ψ p q
∧ attacker_wins (expr_pr_conjunct ψ) (Attacker_Clause p q))›
with inductive_wins someI have ψqs_spec:
‹∀q∈(Q ∩ hml_srbb_inner.model_set (Obs α φ)).
∃i∈I. ψqs q = ψs i ∧ hml_srbb_conj.distinguishes (ψqs q ) p q
∧ attacker_wins (expr_pr_conjunct (ψqs q)) (Attacker_Clause p q)›
by (smt (verit))
have conjuncts_present:
‹∀q∈(Q ∩ hml_srbb_inner.model_set (Obs α φ)). expr_pr_conjunct (ψqs q)
∈ expr_pr_conjunct ` (ψqs ` (Q ∩ hml_srbb_inner.model_set (Obs α φ)))›
by blast
define e'0 where ‹e'0 = E
(Sup (modal_depth ` (expr_pr_conjunct ` (ψqs ` (Q ∩ hml_srbb_inner.model_set (Obs α φ))))))
(Sup (br_conj_depth ` (expr_pr_conjunct ` (ψqs ` (Q ∩ hml_srbb_inner.model_set (Obs α φ))))))
(Sup (conj_depth ` (expr_pr_conjunct ` (ψqs ` (Q ∩ hml_srbb_inner.model_set (Obs α φ))))))
(Sup (st_conj_depth ` (expr_pr_conjunct ` (ψqs ` (Q ∩ hml_srbb_inner.model_set (Obs α φ))))))
(Sup (imm_conj_depth ` (expr_pr_conjunct ` (ψqs ` (Q ∩ hml_srbb_inner.model_set (Obs α φ))))))
(Sup (pos_conjuncts ` (expr_pr_conjunct ` (ψqs ` (Q ∩ hml_srbb_inner.model_set (Obs α φ))))))
(Sup (neg_conjuncts ` (expr_pr_conjunct ` (ψqs ` (Q ∩ hml_srbb_inner.model_set (Obs α φ))))))
(Sup (neg_depth ` (expr_pr_conjunct ` (ψqs ` (Q ∩ hml_srbb_inner.model_set (Obs α φ))))))›
from conjuncts_present have branch_answer_bound:
‹∀q∈(Q ∩ hml_srbb_inner.model_set (Obs α φ)). (expr_pr_conjunct (ψqs q)) ≤ e'0›
unfolding e'0_def using SUP_upper energy.sel energy.simps(3) energy_leq_cases image_iff
by (smt (z3))
with ψqs_spec win_a_upwards_closure have
conj_wins: ‹∀q∈(Q ∩ hml_srbb_inner.model_set (Obs α φ)). attacker_wins e'0 (Attacker_Clause p q)› by blast
define eu'0 where ‹eu'0 = E
(Sup (modal_depth ` (expr_pr_conjunct ` (ψs ` I))))
(Sup (br_conj_depth ` (expr_pr_conjunct ` (ψs ` I))))
(Sup (conj_depth ` (expr_pr_conjunct ` (ψs ` I))))
(Sup (st_conj_depth ` (expr_pr_conjunct ` (ψs ` I))))
(Sup (imm_conj_depth ` (expr_pr_conjunct ` (ψs ` I))))
(Sup (pos_conjuncts ` (expr_pr_conjunct ` (ψs ` I))))
(Sup (neg_conjuncts ` (expr_pr_conjunct ` (ψs ` I))))
(Sup (neg_depth ` (expr_pr_conjunct ` (ψs ` I))))›
have subset_form: ‹ψqs ` (Q ∩ hml_srbb_inner.model_set (Obs α φ)) ⊆ ψs ` I›
using ψqs_spec by fastforce
hence ‹e'0 ≤ eu'0› unfolding e'0_def eu'0_def
by (metis (mono_tags, lifting) Sup_subset_mono energy.sel energy_leq_cases image_mono)
have no_q_way: ‹∀q∈Q_α. ∄q'. q ↦ α q' ∧ hml_srbb_models q' φ›
using case_assms(4)
by fastforce
define Q' where ‹Q' ≡ (soft_step_set Q_α α)›
hence ‹distinguishes_from φ p' Q'›
using case_assms(2,3) no_q_way soft_step_set_is_soft_step_set mem_Collect_eq
unfolding case_assms(4)
by fastforce
with BranchConj have win_a_branch:
‹attacker_wins (expressiveness_price φ) (Attacker_Immediate p' Q')›
using distinction_implies_winning_budgets_empty_Q by (cases ‹Q' = {}›) auto
have ‹expr_pr_inner (Obs α φ) ≥ (E 1 0 0 0 0 0 0 0)› by auto
hence ‹(subtract_fn 1 0 0 0 0 0 0 0) (expr_pr_inner (Obs α φ)) = Some (expressiveness_price φ)›
using expr_obs_phi by auto
with win_a_branch have win_a_step:
‹attacker_wins (the ((subtract_fn 1 0 0 0 0 0 0 0) (expr_pr_inner (Obs α φ)))) (Attacker_Immediate p' Q')› by auto
define e' where ‹e' = E
(Sup (modal_depth ` ({expr_pr_inner (Obs α φ)} ∪ (expr_pr_conjunct ` (ψs ` I)))))
(Sup (br_conj_depth ` ({expr_pr_inner (Obs α φ)} ∪ (expr_pr_conjunct ` (ψs ` I)))))
(Sup (conj_depth ` ({expr_pr_inner (Obs α φ)} ∪ (expr_pr_conjunct ` (ψs ` I)))))
(Sup (st_conj_depth ` ({expr_pr_inner (Obs α φ)} ∪ (expr_pr_conjunct ` (ψs ` I)))))
(Sup (imm_conj_depth ` ({expr_pr_inner (Obs α φ)} ∪ (expr_pr_conjunct ` (ψs ` I)))))
(Sup ({1 + modal_depth_srbb φ}
∪ (pos_conjuncts ` ({expr_pr_inner (Obs α φ)} ∪ (expr_pr_conjunct ` (ψs ` I))))))
(Sup (neg_conjuncts ` ({expr_pr_inner (Obs α φ)} ∪ (expr_pr_conjunct ` (ψs ` I)))))
(Sup (neg_depth ` ({expr_pr_inner (Obs α φ)} ∪ (expr_pr_conjunct ` (ψs ` I)))))›
have ‹eu'0 ≤ e'› unfolding e'_def eu'0_def
by (auto, meson sup.cobounded2 sup.coboundedI2)
have ‹spectroscopy_moves (Attacker_Branch p' Q') (Attacker_Immediate p' Q') = Some (subtract_fn 1 0 0 0 0 0 0 0)› by simp
with win_a_step attacker_wins_Ga have obs_later_win: ‹attacker_wins (expr_pr_inner (Obs α φ)) (Attacker_Branch p' Q')›
by force
hence e'_win: ‹attacker_wins e' (Attacker_Branch p' Q')›
unfolding e'_def using win_a_upwards_closure
by auto
have depths: ‹1 + modal_depth_srbb φ = modal_depth (expr_pr_inner (Obs α φ))› by simp
have six_e': ‹pos_conjuncts e' = Sup ({1 + modal_depth_srbb φ} ∪ (pos_conjuncts ` ({expr_pr_inner (Obs α φ)} ∪ (expr_pr_conjunct ` (ψs ` I)))))›
using energy.sel(6) unfolding e'_def by blast
hence six_e'_simp: ‹pos_conjuncts e' = Sup ({1 + modal_depth_srbb φ} ∪ (pos_conjuncts ` (expr_pr_conjunct ` (ψs ` I))))›
by (auto simp add: modal_depth_dominates_pos_conjuncts add_increasing sup.absorb2 sup.coboundedI1)
hence ‹pos_conjuncts e' ≤ modal_depth e'›
unfolding e'_def
by (auto, smt (verit) SUP_mono energy.sel(1) energy.sel(6) image_iff modal_depth_dominates_pos_conjuncts sup.coboundedI2)
hence ‹modal_depth (the (min1_6 e')) = (pos_conjuncts e')›
by simp
with six_e' have min_e'_def: ‹min1_6 e' = Some (E
(Sup ({1 + modal_depth_srbb φ} ∪ pos_conjuncts ` (expr_pr_conjunct ` (ψs ` I))))
(Sup (br_conj_depth ` ({expr_pr_inner (Obs α φ)} ∪ (expr_pr_conjunct ` (ψs ` I)))))
(Sup (conj_depth ` ({expr_pr_inner (Obs α φ)} ∪ (expr_pr_conjunct ` (ψs ` I)))))
(Sup (st_conj_depth ` ({expr_pr_inner (Obs α φ)} ∪ (expr_pr_conjunct ` (ψs ` I)))))
(Sup (imm_conj_depth ` ({expr_pr_inner (Obs α φ)} ∪ (expr_pr_conjunct ` (ψs ` I)))))
(Sup ({1 + modal_depth_srbb φ} ∪ (pos_conjuncts ` ({expr_pr_inner (Obs α φ)} ∪ (expr_pr_conjunct ` (ψs ` I))))))
(Sup (neg_conjuncts ` ({expr_pr_inner (Obs α φ)} ∪ (expr_pr_conjunct ` (ψs ` I)))))
(Sup (neg_depth ` ({expr_pr_inner (Obs α φ)} ∪ (expr_pr_conjunct ` (ψs ` I))))))›
using e'_def min1_6_def six_e'_simp
by (smt (z3) energy.case_eq_if energy.sel min_1_6_simps(1))
hence ‹expr_pr_inner (Obs α φ) ≤ the (min1_6 e')›
by force
hence obs_win: ‹attacker_wins (the (min1_6 e')) (Attacker_Branch p' Q')›
using obs_later_win win_a_upwards_closure by blast
define e where ‹e = E
(modal_depth e')
(1 + br_conj_depth e')
(1 + conj_depth e')
(st_conj_depth e')
(imm_conj_depth e')
(pos_conjuncts e')
(neg_conjuncts e')
(neg_depth e')›
have ‹e' = e - (E 0 1 1 0 0 0 0 0)› unfolding e_def e'_def by auto
hence e'_comp: ‹Some e' = (subtract_fn 0 1 1 0 0 0 0 0) e›
by (metis e_def energy.sel energy_leq_cases i0_lb le_iff_add)
have expr_lower: ‹(E 0 1 1 0 0 0 0 0) ≤ expr_pr_inner (BranchConj α φ I ψs)›
using case_assms subset_form by auto
have e'_minus: ‹e' = expr_pr_inner (BranchConj α φ I ψs) - E 0 1 1 0 0 0 0 0›
unfolding e'_def using energy.sel
by (auto simp add: bot_enat_def sup.left_commute,
(metis (no_types, lifting) SUP_cong image_image)+)
with expr_lower have e'_characterization:
‹Some e' = (subtract_fn 0 1 1 0 0 0 0 0) (expr_pr_inner (BranchConj α φ I ψs))›
by presburger
have moves: ‹∀g'. spectroscopy_moves (Defender_Branch p α p' (Q - Q_α) Q_α) g' ≠ None
⟶ (((Attacker_Branch p' Q' = g')
∧ (spectroscopy_moves (Defender_Branch p α p' (Q - Q_α) Q_α) g' = Some (λe. Option.bind ((subtract_fn 0 1 1 0 0 0 0 0) e) min1_6)))
∨ ((∃q∈(Q - Q_α). Attacker_Clause p q = g'
∧ spectroscopy_moves (Defender_Branch p α p' (Q - Q_α) Q_α) g' = (subtract 0 1 1 0 0 0 0 0))))›
proof clarify
fix g' u
assume no_subtr_move:
‹spectroscopy_moves (Defender_Branch p α p' (Q - Q_α) Q_α) g' = Some u›
‹¬ (∃q∈Q - Q_α. Attacker_Clause p q = g' ∧ spectroscopy_moves (Defender_Branch p α p' (Q - Q_α) Q_α) g' = subtract 0 1 1 0 0 0 0 0)›
hence ‹g' = Attacker_Branch p' Q'›
unfolding Q'_def using soft_step_set_is_soft_step_set no_subtr_move local.br_answer
by (cases g', auto, (metis (no_types, lifting) option.discI)+)
moreover have ‹Attacker_Branch p' Q' = g' ⟶ spectroscopy_moves (Defender_Branch p α p' (Q - Q_α) Q_α) g' = Some (λe. Option.bind ((subtract_fn 0 1 1 0 0 0 0 0) e) min1_6)›
unfolding Q'_def using soft_step_set_is_soft_step_set by auto
ultimately show ‹Attacker_Branch p' Q' = g' ∧ spectroscopy_moves (Defender_Branch p α p' (Q - Q_α) Q_α) g' = Some (λe. Option.bind ((subtract_fn 0 1 1 0 0 0 0 0) e) min1_6)›
by blast
qed
have obs_e: ‹∃e'. (λe. Option.bind ((subtract_fn 0 1 1 0 0 0 0 0) e) min1_6) e = Some e' ∧ attacker_wins e' (Attacker_Branch p' Q')›
using obs_win e'_comp min_e'_def
by (smt (verit, best) bind.bind_lunit min_1_6_some option.collapse)
have ‹∀q∈(Q - Q_α). spectroscopy_moves (Defender_Branch p α p' (Q - Q_α) Q_α) (Attacker_Clause p q) = (subtract 0 1 1 0 0 0 0 0)
⟶ attacker_wins e'0 (Attacker_Clause p q)›
using conj_wins ‹eu'0 ≤ e'› case_assms(4) by blast
with obs_e moves have move_wins: ‹∀g'. spectroscopy_moves (Defender_Branch p α p' (Q - Q_α) Q_α) g' ≠ None
⟶ (∃e'. (the (spectroscopy_moves (Defender_Branch p α p' (Q - Q_α) Q_α) g')) e = Some e' ∧ attacker_wins e' g')›
using ‹eu'0 ≤ e'› e'_comp ‹e'0 ≤ eu'0› win_a_upwards_closure
by (smt (verit, ccfv_SIG) option.sel)
moreover have ‹expr_pr_inner (BranchConj α φ I ψs) = e›
using e'_characterization e'_minus unfolding e_def by force
ultimately show ‹attacker_wins (expr_pr_inner (BranchConj α φ I ψs)) (Defender_Branch p α p' (Q - Q_α) Q_α)›
using attacker_wins.Defense spectroscopy_defender.simps(5)
by metis
qed
moreover have
‹∀p Q. Q ≠ {} ⟶ hml_srbb_inner.distinguishes_from (BranchConj α φ I ψs) p Q
⟶ attacker_wins (expr_pr_inner (BranchConj α φ I ψs)) (Attacker_Delayed p Q)›
proof clarify
fix p Q
assume case_assms:
‹hml_srbb_inner.distinguishes_from (BranchConj α φ I ψs) p Q›
from case_assms(1) obtain p' where p'_spec: ‹p ↦a α p'› ‹p' ⊨SRBB φ›
unfolding hml_srbb_inner.distinguishes_from_def
and distinguishes_def by auto
define Q_α where ‹Q_α = Q - hml_srbb_inner.model_set (Obs α φ)›
have ‹attacker_wins (expr_pr_inner (BranchConj α φ I ψs)) (Defender_Branch p α p' (Q - Q_α) Q_α)›
using main_case case_assms(1) p'_spec Q_α_def by blast
moreover have ‹spectroscopy_moves (Attacker_Delayed p Q) (Defender_Branch p α p' (Q - Q_α) Q_α) = Some Some›
using p'_spec Q_α_def by auto
ultimately show ‹attacker_wins (expr_pr_inner (BranchConj α φ I ψs)) (Attacker_Delayed p Q)›
using attacker_wins_Ga_with_id_step by auto
qed
ultimately show ?case by blast
next
case (Pos χ)
show ?case
proof clarify
fix p q
assume case_assms: ‹hml_srbb_conj.distinguishes (Pos χ) p q›
then obtain p' where p'_spec: ‹p ↠ p'› ‹p' ∈ hml_srbb_inner.model_set χ›
unfolding hml_srbb_conj.distinguishes_def by auto
moreover have q_reach: ‹silent_reachable_set {q} ∩ hml_srbb_inner.model_set χ = {}›
using case_assms sreachable_set_is_sreachable
unfolding hml_srbb_conj.distinguishes_def by force
ultimately have distinction: ‹hml_srbb_inner.distinguishes_from χ p' (silent_reachable_set {q})›
unfolding hml_srbb_inner.distinguishes_from_def by auto
have q_reach_nonempty:
‹silent_reachable_set {q} ≠ {}›
‹silent_reachable_set {q} ↠S silent_reachable_set {q} ›
unfolding silent_reachable_set_def
using silent_reachable.intros(1) silent_reachable_trans by auto
hence ‹attacker_wins (expr_pr_inner χ) (Attacker_Delayed p' (silent_reachable_set {q}))›
using distinction Pos by blast
from p'_spec(1) this have ‹attacker_wins (expr_pr_inner χ) (Attacker_Delayed p (silent_reachable_set {q}))›
by (induct, auto,
metis attacker_wins_Ga_with_id_step local.procrastination option.distinct(1) option.sel spectroscopy_defender.simps(4))
moreover have ‹spectroscopy_moves (Attacker_Clause p q) (Attacker_Delayed p (silent_reachable_set {q})) = Some min1_6›
using q_reach_nonempty sreachable_set_is_sreachable by fastforce
moreover have ‹the (min1_6 (expr_pr_conjunct (Pos χ))) ≥ expr_pr_inner χ›
unfolding min1_6_def by (auto simp add: energy_leq_cases modal_depth_dominates_pos_conjuncts)
ultimately show ‹attacker_wins (expr_pr_conjunct (Pos χ)) (Attacker_Clause p q)›
using attacker_wins_Ga win_a_upwards_closure spectroscopy_defender.simps(3)
by (metis (no_types, lifting) min_1_6_some option.discI option.exhaust_sel option.sel)
qed
next
case (Neg χ)
show ?case
proof clarify
fix p q
assume case_assms: ‹hml_srbb_conj.distinguishes (Neg χ) p q›
then obtain q' where q'_spec: ‹q ↠ q'› ‹q' ∈ hml_srbb_inner.model_set χ›
unfolding hml_srbb_conj.distinguishes_def by auto
moreover have p_reach: ‹silent_reachable_set {p} ∩ hml_srbb_inner.model_set χ = {}›
using case_assms sreachable_set_is_sreachable
unfolding hml_srbb_conj.distinguishes_def by force
ultimately have distinction: ‹hml_srbb_inner.distinguishes_from χ q' (silent_reachable_set {p})›
unfolding hml_srbb_inner.distinguishes_from_def by auto
have ‹p ≠ q› using case_assms unfolding hml_srbb_conj.distinguishes_def by auto
have p_reach_nonempty:
‹silent_reachable_set {p} ≠ {}›
‹silent_reachable_set {p} ↠S silent_reachable_set {p}›
unfolding silent_reachable_set_def
using silent_reachable.intros(1) silent_reachable_trans by auto
hence ‹attacker_wins (expr_pr_inner χ) (Attacker_Delayed q' (silent_reachable_set {p}))›
using distinction Neg by blast
from q'_spec(1) this have ‹attacker_wins (expr_pr_inner χ) (Attacker_Delayed q (silent_reachable_set {p}))›
by (induct, auto,
metis attacker_wins_Ga_with_id_step local.procrastination option.distinct(1) option.sel spectroscopy_defender.simps(4))
moreover have ‹spectroscopy_moves (Attacker_Clause p q) (Attacker_Delayed q (silent_reachable_set {p}))
= Some (λe. Option.bind ((subtract_fn 0 0 0 0 0 0 0 1) e) min1_7)›
using p_reach_nonempty sreachable_set_is_sreachable ‹p ≠ q› by fastforce
moreover have ‹the (min1_7 (expr_pr_conjunct (Neg χ) - E 0 0 0 0 0 0 0 1)) ≥ (expr_pr_inner χ)›
using min1_7_def energy_leq_cases
by (simp add: modal_depth_dominates_neg_conjuncts)
moreover from this have ‹∃e'. Some e' = ((λe. Option.bind ((subtract_fn 0 0 0 0 0 0 0 1) e) min1_7) (expr_pr_conjunct (Neg χ))) ∧ e' ≥ (expr_pr_inner χ)›
unfolding min_1_7_subtr_simp by auto
ultimately show ‹attacker_wins (expr_pr_conjunct (Neg χ)) (Attacker_Clause p q)›
using attacker_wins.Attack win_a_upwards_closure spectroscopy_defender.simps(3)
by (metis (no_types, lifting) option.discI option.sel)
qed
qed
qed
thus ?thesis
by (metis assms distinction_implies_winning_budgets_empty_Q)
qed
end
end