Theory Distinction_Implies_Winning_Budgets
section ‹Correctness›
text ‹
Energy levels where the defender wins in the spectroscopy game and equivalences coincide in the following sense:
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 attacker's winning budget of ‹Attacker_Immediate p Q›.
The proof is split into two directions, closely following the structure of \<^cite>‹bj2023silentStepSpectroscopyArxiv›.
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›.
›
subsection ‹Distinction Implies Winning Budgets›
theory Distinction_Implies_Winning_Budgets
imports Spectroscopy_Game Expressiveness_Price
begin
context lts_tau
begin
text ‹
We prove that if a formula distinguishes process ‹p› from a set of process ‹Q›, then the price of this formula is in attacker's winning budgets.
›
lemma distinction_implies_winning_budgets_empty_Q:
assumes
‹distinguishes_from φ p {}›
shows
‹spectro_att_wins (expressiveness_price φ) (Attacker_Immediate p {})›
using assms
proof -
have ‹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: ‹spectro_att_wins (expressiveness_price φ) (Defender_Conj p {})›
by (simp add: weak_spectroscopy_game.attacker_wins.Defense)
from late_inst_conj[of p ‹{}› p ‹{}›] have next_move0:
‹spectroscopy_moves (Attacker_Delayed p {}) (Defender_Conj p {}) = id_up› by force
from delay[of p ‹{}› p ‹{}›] have next_move1:
‹spectroscopy_moves (Attacker_Immediate p {}) (Attacker_Delayed p {}) = id_up› by force
moreover have ‹weak_spectroscopy_game.attacker (Attacker_Immediate p {})› by simp
ultimately show ?thesis
using weak_spectroscopy_game.attacker_wins.Attack next_move0 next_move1
by (metis conj_win option.distinct(1) option.sel spectroscopy_defender.simps(4))
qed
lemma distinction_implies_winning_budgets:
assumes
‹distinguishes_from φ p Q›
shows
‹spectro_att_wins (expressiveness_price φ) (Attacker_Immediate p Q)›
proof -
have
‹ (∀Q p. Q ≠ {} ⟶ distinguishes_from φ p Q
⟶ spectro_att_wins (expressiveness_price φ)(Attacker_Immediate p Q))
∧
((∀p Q. Q ≠ {} ⟶ hml_srbb_inner.distinguishes_from χ p Q ⟶ Q ↠S Q
⟶ spectro_att_wins (expr_pr_inner χ) (Attacker_Delayed p Q))
∧ (∀Ψ_I Ψ p Q. χ = Conj Ψ_I Ψ ⟶
Q ≠ {} ⟶ hml_srbb_inner.distinguishes_from χ p Q
⟶ spectro_att_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')
⟶ spectro_att_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 α φ)
⟶ spectro_att_wins (expr_pr_inner χ) (Defender_Branch p α p' (Q - Q_α) Q_α)))
∧
(∀p q. hml_srbb_conj.distinguishes ψ p q
⟶ spectro_att_wins (expr_pr_conjunct ψ) (Attacker_Conjunct p q))›
for φ χ ψ
proof -
fix φ χ ψ
show ‹(∀Q p. Q ≠ {} ⟶ distinguishes_from φ p Q
⟶ spectro_att_wins (expressiveness_price φ) (Attacker_Immediate p Q))
∧
((∀p Q. Q ≠ {} ⟶ hml_srbb_inner.distinguishes_from χ p Q ⟶ Q ↠S Q
⟶ spectro_att_wins (expr_pr_inner χ) (Attacker_Delayed p Q))
∧ (∀Ψ_I Ψ p Q. χ = Conj Ψ_I Ψ ⟶
Q ≠ {} ⟶ hml_srbb_inner.distinguishes_from χ p Q
⟶ spectro_att_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')
⟶ spectro_att_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 α φ)
⟶ spectro_att_wins (expr_pr_inner χ) (Defender_Branch p α p' (Q - Q_α) Q_α)))
∧
(∀p q. hml_srbb_conj.distinguishes ψ p q
⟶ spectro_att_wins (expr_pr_conjunct ψ) (Attacker_Conjunct 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 ≠ {}› ‹distinguishes_from TT p Q›
hence ‹∃q. q ∈ Q›
by blast
then obtain q where ‹q ∈ Q› by auto
hence ‹distinguishes TT p q›
using ‹distinguishes_from TT p Q› distinguishes_from_def by auto
with verum_never_distinguishes
show ‹spectro_att_wins (expressiveness_price TT) (Attacker_Immediate p Q)›
by blast
qed
next
case (Internal χ)
show ?case
proof (clarify)
fix Q p
assume ‹Q ≠ {}› ‹distinguishes_from (Internal χ) p Q›
then have
‹∃p'. p ↠ p' ∧ hml_srbb_inner_models p' χ›
‹∀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'› ‹hml_srbb_inner_models p' χ› by auto
from this(1) have ‹p ↠L p'› using silent_reachable_impl_loopless by blast
have ‹Qτ ≠ {}›
using silent_reachable.intros(1) sreachable_set_is_sreachable Qτ_def ‹Q ≠ {}›
by fastforce
from ‹hml_srbb_inner_models p' χ› ‹∀q' ∈ Qτ. ¬(hml_srbb_inner_models q' χ)›
have ‹hml_srbb_inner.distinguishes_from χ p' Qτ› by simp
with ‹Qτ ↠S Qτ› ‹Qτ ≠ {}› Internal
have ‹spectro_att_wins (expr_pr_inner χ) (Attacker_Delayed p' Qτ)›
by blast
moreover have ‹expr_pr_inner χ = expressiveness_price (Internal χ)› by simp
ultimately have ‹spectro_att_wins (expressiveness_price (Internal χ))
(Attacker_Delayed p' Qτ)› by simp
hence ‹spectro_att_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 ‹spectro_att_wins (expressiveness_price (Internal χ))
(Attacker_Delayed p' Qτ)›
by simp
moreover have ‹spectroscopy_moves (Attacker_Delayed p Qτ) (Attacker_Delayed p' Qτ)
= id_up› using spectroscopy_moves.simps(2) ‹p ≠ p'› ‹p ↦τ p'› by auto
moreover have ‹weak_spectroscopy_game.attacker (Attacker_Delayed p Qτ)› by simp
ultimately show ?case
using weak_spectroscopy_game.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τ) = id_up›
using spectroscopy_moves.simps(1) by simp
with ‹spectro_att_wins (expressiveness_price (Internal χ)) (Attacker_Delayed p Qτ)›
show ‹spectro_att_wins (expressiveness_price (Internal χ)) (Attacker_Immediate p Q)›
using weak_spectroscopy_game.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.
spectro_att_wins (expr_pr_conjunct (ψs i)) (Attacker_Conjunct p q)›
using ImmConj by blast
hence a_clause_wina:
‹∀q∈Q. ∃i∈I.
spectro_att_wins (expressiveness_price (ImmConj I ψs) - E 0 0 1 0 1 0 0 0)
(Attacker_Conjunct p q)›
using expressiveness_price_ImmConj_geq_parts
weak_spectroscopy_game.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_Conjunct (attacker_state N) (defender_state N)› for N
by (metis spectroscopy_moves.simps(29,30,33,34,58,62)
spectroscopy_position.exhaust_sel)
hence move_kind: ‹spectroscopy_moves (Defender_Conj p Q) N ≠ None
⟹ ∃q∈Q. N = Attacker_Conjunct p q› for N
using conj_answer by metis
hence update: ‹⋀g'. spectroscopy_moves (Defender_Conj p Q) g' ≠ None ⟹
weak_spectroscopy_game.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)
∧ spectro_att_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 weak_spectroscopy_game.attacker_wins.Defense[OF def_conj] update move_wina have
def_conj_wina:
‹spectro_att_wins (expressiveness_price (ImmConj I ψs) - E 0 0 0 0 1 0 0 0)
(Defender_Conj p Q)›
by (metis (lifting))
have imm_to_conj:
‹spectroscopy_moves (Attacker_Immediate p Q) (Defender_Conj p Q) ≠ None›
by (simp add: ‹Q ≠ {}›)
have imm_to_conj_wgt:
‹weak_spectroscopy_game.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 weak_spectroscopy_game.Attack[OF _ imm_to_conj imm_to_conj_wgt] def_conj_wina
show
‹spectro_att_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 ⟶ spectro_att_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'
∧ spectro_att_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 ‹spectro_att_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 ‹spectro_att_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: ‹spectro_att_wins (expressiveness_price φ) (Attacker_Immediate p' Q')› by blast
have attacker: ‹weak_spectroscopy_game.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 subtract 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') =
subtract 1 0 0 0 0 0 0 0› using p'_Q' by auto
with expr_obs_phi[of α φ] show
‹spectro_att_wins (expr_pr_inner (hml_srbb_inner.Obs α φ)) (Attacker_Delayed p Q)›
using weak_spectroscopy_game.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
⟶ spectro_att_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
∧ spectro_att_wins (expr_pr_conjunct (ψs i)) (Attacker_Conjunct p q)›
using Conj by blast
define ψqs where
‹ψqs ≡ λq. (SOME ψ. ∃i∈I. ψ = ψs i ∧ hml_srbb_conj.distinguishes ψ p q
∧ spectro_att_wins (expr_pr_conjunct ψ) (Attacker_Conjunct 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
∧ spectro_att_wins (expr_pr_conjunct (ψqs q)) (Attacker_Conjunct 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 weak_spectroscopy_game.win_a_upwards_closure
have clause_win: ‹∀q∈Q. spectro_att_wins e' (Attacker_Conjunct 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_Conjunct 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_Conjunct 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_Conjunct 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'
∧ spectro_att_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 ‹spectro_att_wins e (Defender_Conj p Q)›
unfolding e_def using weak_spectroscopy_game.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 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
‹spectro_att_wins (expr_pr_inner (hml_srbb_inner.Conj I ψs)) (Defender_Conj p Q)›
using weak_spectroscopy_game.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 ⟶ spectro_att_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
‹spectro_att_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) = id_up›
by auto
ultimately show
‹spectro_att_wins (expr_pr_inner (hml_srbb_inner.Conj I ψs))
(Attacker_Delayed p Q)›
by (metis weak_spectroscopy_game.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')
⟶ spectro_att_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
∧ spectro_att_wins (expr_pr_conjunct (ψs i)) (Attacker_Conjunct p q)›
using StableConj by blast
define ψqs where
‹ψqs ≡ λq. (SOME ψ. ∃i∈I. ψ = ψs i ∧ hml_srbb_conj.distinguishes ψ p q
∧ spectro_att_wins (expr_pr_conjunct ψ) (Attacker_Conjunct 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
∧ spectro_att_wins (expr_pr_conjunct (ψqs q)) (Attacker_Conjunct 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 weak_spectroscopy_game.win_a_upwards_closure
have clause_win: ‹∀q∈Q. spectro_att_wins e' (Attacker_Conjunct 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_Conjunct 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_Conjunct 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_Conjunct 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'
∧ spectro_att_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 ‹spectro_att_wins e (Defender_Stable_Conj p Q)›
unfolding e_def
by (auto simp add: weak_spectroscopy_game.attacker_wins.Defense)
moreover have ‹e ≤ expr_pr_inner (StableConj I ψs)›
using ‹e' ≤ eu'› eu'_characterization 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
‹spectro_att_wins (expr_pr_inner (StableConj I ψs)) (Defender_Stable_Conj p Q)›
using weak_spectroscopy_game.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
⟶ spectro_att_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') = id_up›
unfolding Q'_def by auto
show ‹spectro_att_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
∧ spectro_att_wins (e - E 0 0 0 1 0 0 0 0) (Defender_Conj p {})
⟶ spectro_att_wins e (Defender_Stable_Conj p Q')›
using weak_spectroscopy_game.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. spectro_att_wins e (Defender_Conj p {})›
using weak_spectroscopy_game.attacker_wins.Defense 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)
⟶ spectro_att_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 weak_spectroscopy_game.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 weak_spectroscopy_game.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 α φ)
⟶ spectro_att_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
∧ spectro_att_wins (expr_pr_conjunct (ψs i)) (Attacker_Conjunct p q)›
using BranchConj by blast
define ψqs where
‹ψqs ≡ λq. (SOME ψ. ∃i∈I. ψ = ψs i ∧ hml_srbb_conj.distinguishes ψ p q
∧ spectro_att_wins (expr_pr_conjunct ψ) (Attacker_Conjunct 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
∧ spectro_att_wins (expr_pr_conjunct (ψqs q)) (Attacker_Conjunct 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›
using e'0_def SUP_upper energy.sel energy.simps(3) energy_leq_cases image_iff
by (smt (z3))
with ψqs_spec weak_spectroscopy_game.win_a_upwards_closure have
conj_wins: ‹∀q∈(Q ∩ hml_srbb_inner.model_set (Obs α φ)).
spectro_att_wins e'0 (Attacker_Conjunct 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:
‹spectro_att_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:
‹spectro_att_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 weak_spectroscopy_game.attacker_wins.Attack have obs_later_win:
‹spectro_att_wins (expr_pr_inner (Obs α φ)) (Attacker_Branch p' Q')›
by force
hence e'_win: ‹spectro_att_wins e' (Attacker_Branch p' Q')›
unfolding e'_def using weak_spectroscopy_game.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: ‹spectro_att_wins (the (min1_6 e')) (Attacker_Branch p' Q')›
using obs_later_win weak_spectroscopy_game.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_Conjunct 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_Conjunct 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'
∧ spectro_att_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_Conjunct p q)
= (subtract 0 1 1 0 0 0 0 0)
⟶ spectro_att_wins e'0 (Attacker_Conjunct 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' ∧ spectro_att_wins e' g')›
using ‹eu'0 ≤ e'› e'_comp ‹e'0 ≤ eu'0› weak_spectroscopy_game.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 ‹spectro_att_wins (expr_pr_inner (BranchConj α φ I ψs))
(Defender_Branch p α p' (Q - Q_α) Q_α)›
using weak_spectroscopy_game.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
⟶ spectro_att_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 ‹spectro_att_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_α) = id_up›
using p'_spec Q_α_def by auto
ultimately show
‹spectro_att_wins (expr_pr_inner (BranchConj α φ I ψs)) (Attacker_Delayed p Q)›
using weak_spectroscopy_game.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 ‹spectro_att_wins (expr_pr_inner χ)
(Attacker_Delayed p' (silent_reachable_set {q}))›
using distinction Pos by blast
from p'_spec(1) this have
‹spectro_att_wins (expr_pr_inner χ) (Attacker_Delayed p (silent_reachable_set {q}))›
by (induct, auto,
metis weak_spectroscopy_game.attacker_wins_Ga_with_id_step procrastination
option.distinct(1) option.sel spectroscopy_defender.simps(4))
moreover have ‹spectroscopy_moves (Attacker_Conjunct 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 ‹spectro_att_wins (expr_pr_conjunct (Pos χ)) (Attacker_Conjunct p q)›
using weak_spectroscopy_game.attacker_wins.simps
weak_spectroscopy_game.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 ‹spectro_att_wins (expr_pr_inner χ)
(Attacker_Delayed q' (silent_reachable_set {p}))›
using distinction Neg by blast
from q'_spec(1) this have
‹spectro_att_wins (expr_pr_inner χ) (Attacker_Delayed q (silent_reachable_set {p}))›
by (induct, auto,
metis weak_spectroscopy_game.attacker_wins_Ga_with_id_step procrastination
option.distinct(1) option.sel spectroscopy_defender.simps(4))
moreover have ‹spectroscopy_moves (Attacker_Conjunct 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 ‹spectro_att_wins (expr_pr_conjunct (Neg χ)) (Attacker_Conjunct p q)›
using weak_spectroscopy_game.attacker_wins.Attack
weak_spectroscopy_game.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