Theory Strategy_Formulas
subsection ‹Strategy Formulas›
theory Strategy_Formulas
imports Spectroscopy_Game Expressiveness_Price
begin
text‹In this section, we introduce strategy formulas as a tool of proving the corresponding lemma, \\
‹spectroscopy_game_correctness›, in section \ref{th1}.
We first define strategy formulas, creating a bridge between HML formulas, the
spectroscopy game and winning budgets. We then show that for some energy ‹e› in a winning budget there
exists a strategy formula with expressiveness price ‹≤ e›. Afterwards, we prove that this formula
actually distinguishes the corresponding processes.›
context weak_spectroscopy_game
begin
text ‹\label{stratFormula}›
text ‹We define strategy formulas inductively. For example for ‹⟨α⟩φ› to be a strategy formula for some attacker
delayed position ‹g› with energy ‹e› the following must hold: ‹φ› is a strategy formula at the from ‹ g› through an observation move
reached attacker (immediate) position with the energy ‹ e › updated according to the move. Then the function
‹strategy_formula_inner g e ⟨α⟩φ› returns true. Similarly, every derivation rule for strategy formulas corresponds to
possible moves in the spectroscopy game. To account for the three different data types a HML$_{\text{SRBB}}$
formula can have in our formalization, we define three functions at the same time:›
inductive
strategy_formula :: ‹('s, 'a) spectroscopy_position ⇒ energy ⇒ ('a, 's)hml_srbb ⇒ bool›
and strategy_formula_inner
:: ‹('s, 'a) spectroscopy_position ⇒ energy ⇒ ('a, 's)hml_srbb_inner ⇒ bool›
and strategy_formula_conjunct
:: ‹('s, 'a) spectroscopy_position ⇒ energy ⇒ ('a, 's)hml_srbb_conjunct ⇒ bool›
where
delay:
‹strategy_formula (Attacker_Immediate p Q) e (Internal χ)›
if ‹((∃Q'. (spectroscopy_moves (Attacker_Immediate p Q) (Attacker_Delayed p Q')
= (Some Some)) ∧ (attacker_wins e (Attacker_Delayed p Q'))
∧ strategy_formula_inner (Attacker_Delayed p Q') e χ))› |
procrastination:
‹strategy_formula_inner (Attacker_Delayed p Q) e χ›
if ‹(∃p'. spectroscopy_moves (Attacker_Delayed p Q) (Attacker_Delayed p' Q)
= (Some Some) ∧ attacker_wins e (Attacker_Delayed p' Q)
∧ strategy_formula_inner (Attacker_Delayed p' Q) e χ)› |
observation:
‹strategy_formula_inner (Attacker_Delayed p Q) e (Obs α φ)›
if ‹∃p' Q'. spectroscopy_moves (Attacker_Delayed p Q) (Attacker_Immediate p' Q')
= (subtract 1 0 0 0 0 0 0 0)
∧ attacker_wins (e - (E 1 0 0 0 0 0 0 0)) (Attacker_Immediate p' Q')
∧ strategy_formula (Attacker_Immediate p' Q') (e - (E 1 0 0 0 0 0 0 0)) φ
∧ p ↦aα p' ∧ Q ↦aS α Q'› |
early_conj:
‹strategy_formula (Attacker_Immediate p Q) e φ›
if ‹∃p'. spectroscopy_moves (Attacker_Immediate p Q) (Defender_Conj p' Q')
= (subtract 0 0 0 0 1 0 0 0)
∧ attacker_wins (e - (E 0 0 0 0 1 0 0 0)) (Defender_Conj p' Q')
∧ strategy_formula (Defender_Conj p' Q') (e - (E 0 0 0 0 1 0 0 0)) φ› |
late_conj:
‹strategy_formula_inner (Attacker_Delayed p Q) e χ›
if ‹(spectroscopy_moves (Attacker_Delayed p Q) (Defender_Conj p Q)
= (Some Some) ∧ (attacker_wins e (Defender_Conj p Q))
∧ strategy_formula_inner (Defender_Conj p Q) e χ)› |
conj:
‹strategy_formula_inner (Defender_Conj p Q) e (Conj Q Φ)›
if ‹∀q ∈ Q. spectroscopy_moves (Defender_Conj p Q) (Attacker_Clause p q)
= (subtract 0 0 1 0 0 0 0 0)
∧ (attacker_wins (e - (E 0 0 1 0 0 0 0 0)) (Attacker_Clause p q))
∧ strategy_formula_conjunct (Attacker_Clause p q) (e - (E 0 0 1 0 0 0 0 0)) (Φ q)› |
imm_conj:
‹strategy_formula (Defender_Conj p Q) e (ImmConj Q Φ)›
if ‹∀q ∈ Q. spectroscopy_moves (Defender_Conj p Q) (Attacker_Clause p q)
= (subtract 0 0 1 0 0 0 0 0)
∧ (attacker_wins (e - (E 0 0 1 0 0 0 0 0)) (Attacker_Clause p q))
∧ strategy_formula_conjunct (Attacker_Clause p q) (e - (E 0 0 1 0 0 0 0 0)) (Φ q)› |
pos:
‹strategy_formula_conjunct (Attacker_Clause p q) e (Pos χ)›
if ‹(∃Q'. spectroscopy_moves (Attacker_Clause p q) (Attacker_Delayed p Q')
= Some min1_6 ∧ attacker_wins (the (min1_6 e)) (Attacker_Delayed p Q')
∧ strategy_formula_inner (Attacker_Delayed p Q') (the (min1_6 e)) χ)› |
neg:
‹strategy_formula_conjunct (Attacker_Clause p q) e (Neg χ)›
if ‹∃P'. (spectroscopy_moves (Attacker_Clause p q) (Attacker_Delayed q P')
= Some (λe. Option.bind ((subtract_fn 0 0 0 0 0 0 0 1) e) min1_7)
∧ attacker_wins (the (min1_7 (e - (E 0 0 0 0 0 0 0 1)))) (Attacker_Delayed q P'))
∧ strategy_formula_inner (Attacker_Delayed q P') (the (min1_7 (e - (E 0 0 0 0 0 0 0 1)))) χ› |
stable:
‹strategy_formula_inner (Attacker_Delayed p Q) e χ›
if ‹(∃Q'. spectroscopy_moves (Attacker_Delayed p Q) (Defender_Stable_Conj p Q')
= (Some Some) ∧ attacker_wins e (Defender_Stable_Conj p Q')
∧ strategy_formula_inner (Defender_Stable_Conj p Q') e χ)› |
stable_conj:
‹strategy_formula_inner (Defender_Stable_Conj p Q) e (StableConj Q Φ)›
if ‹∀q ∈ Q. spectroscopy_moves (Defender_Stable_Conj p Q) (Attacker_Clause p q)
= (subtract 0 0 0 1 0 0 0 0)
∧ attacker_wins (e - (E 0 0 0 1 0 0 0 0)) (Attacker_Clause p q)
∧ strategy_formula_conjunct (Attacker_Clause p q) (e - (E 0 0 0 1 0 0 0 0)) (Φ q)› |
branch:
‹strategy_formula_inner (Attacker_Delayed p Q) e χ›
if ‹∃p' Q' α Qα. spectroscopy_moves (Attacker_Delayed p Q) (Defender_Branch p α p' Q' Qα)
= (Some Some) ∧ attacker_wins e (Defender_Branch p α p' Q' Qα)
∧ strategy_formula_inner (Defender_Branch p α p' Q' Qα) e χ› |
branch_conj:
‹strategy_formula_inner (Defender_Branch p α p' Q Qα) e (BranchConj α φ Q Φ)›
if ‹∃Q'. spectroscopy_moves (Defender_Branch p α p' Q Qα) (Attacker_Branch p' Q')
= Some (λe. Option.bind ((subtract_fn 0 1 1 0 0 0 0 0) e) min1_6)
∧ spectroscopy_moves (Attacker_Branch p' Q') (Attacker_Immediate p' Q')
= subtract 1 0 0 0 0 0 0 0
∧ (attacker_wins (the (min1_6 (e - E 0 1 1 0 0 0 0 0)) - (E 1 0 0 0 0 0 0 0))
(Attacker_Immediate p' Q'))
∧ strategy_formula (Attacker_Immediate p' Q') (the (min1_6 (e - E 0 1 1 0 0 0 0 0)) - (E 1 0 0 0 0 0 0 0)) φ›
‹∀q ∈ Q. spectroscopy_moves (Defender_Branch p α p' Q Qα) (Attacker_Clause p q)
= (subtract 0 1 1 0 0 0 0 0)
∧ attacker_wins (e - (E 0 1 1 0 0 0 0 0)) (Attacker_Clause p q)
∧ strategy_formula_conjunct (Attacker_Clause p q) (e - (E 0 1 1 0 0 0 0 0)) (Φ q)›
text ‹To prove ‹spectroscopy_game_correctness› we need the following implication:
If ‹e› is in the winning budget of ‹Attacker_Immediate p Q›, there is a strategy formula ‹φ› for
‹Attacker_Immediate p Q› with energy ‹e› with expressiveness price ‹≤ e›.
\\
\\
We prove a more detailed result for all possible game positions ‹g› by induction over the structure of winning budgets (Cases $1-3$:\label{deviation:lemma2}
\begin{enumerate}
\item We first show that the statement holds if ‹g› has no outgoing edges. This can only be the case for defender positions.
\item If ‹g› is an attacker position, by ‹e› being in the winning budget of ‹g›, we know there exists a successor of ‹g› that the attacker can move to.
If by induction the property holds true for that successor, we show that it then holds for ‹g› as well.
\item If a defender position ‹g› has outgoing edges and the statement holds true for all successors, we show that the statement holds true for ‹g› as well.
\end{enumerate}
›
lemma winning_budget_implies_strategy_formula:
fixes g e
assumes ‹attacker_wins e g›
shows
‹case g of
Attacker_Immediate p Q ⇒ ∃φ. strategy_formula g e φ ∧ expressiveness_price φ ≤ e
| Attacker_Delayed p Q ⇒ ∃χ. strategy_formula_inner g e χ ∧ expr_pr_inner χ ≤ e
| Attacker_Clause p q ⇒ ∃ψ. strategy_formula_conjunct g e ψ ∧ expr_pr_conjunct ψ ≤ e
| Defender_Conj p Q ⇒ ∃χ. strategy_formula_inner g e χ ∧ expr_pr_inner χ ≤ e
| Defender_Stable_Conj p Q ⇒ ∃χ. strategy_formula_inner g e χ ∧ expr_pr_inner χ ≤ e
| Defender_Branch p α p' Q Qa ⇒ ∃χ. strategy_formula_inner g e χ ∧ expr_pr_inner χ ≤ e
| Attacker_Branch p Q ⇒
∃φ. strategy_formula (Attacker_Immediate p Q) (e - E 1 0 0 0 0 0 0 0) φ
∧ expressiveness_price φ ≤ e - E 1 0 0 0 0 0 0 0›
using assms
proof(induction rule: attacker_wins.induct)
case (Attack g g' e e')
then show ?case
proof (induct g)
case (Attacker_Immediate p Q)
hence move: ‹
(∃p Q. g' = Defender_Conj p Q) ⟶
(∃φ. strategy_formula_inner g' (the (weight g g' e)) φ ∧ expr_pr_inner φ ≤ updated g g' e) ∧
(∃p Q. g' = Attacker_Delayed p Q) ⟶
(∃φ. strategy_formula_inner g' (the (weight g g' e)) φ ∧ expr_pr_inner φ ≤ updated g g' e)›
using attacker_wins.cases
by simp
from move Attacker_Immediate have move_cases: ‹(∃p' Q'. g' = (Attacker_Delayed p' Q')) ∨ (∃ p' Q'. g' = (Defender_Conj p' Q'))›
using spectroscopy_moves.simps
by (smt (verit, del_insts) spectroscopy_defender.elims(2,3))
show ?case using move_cases
proof(rule disjE)
assume ‹∃p' Q'. g' = Attacker_Delayed p' Q'›
then obtain p' Q' where g'_att_del: ‹g' = Attacker_Delayed p' Q'› by blast
have e_comp: ‹(the (spectroscopy_moves (Attacker_Immediate p Q) (Attacker_Delayed p' Q')) e) = (Some e)›
by (smt (verit, ccfv_threshold) Spectroscopy_Game.LTS_Tau.delay g'_att_del Attacker_Immediate move option.exhaust_sel option.inject)
have ‹p' = p›
by (metis g'_att_del Attacker_Immediate(2) spectroscopy_moves.simps(1))
moreover have ‹(attacker_wins e (Attacker_Delayed p Q'))›
using ‹g' = Attacker_Delayed p' Q'› ‹p' = p› Attacker_Immediate win_a_upwards_closure e_comp
by simp
ultimately have ‹(∃χ. strategy_formula_inner g' (the (weight (Attacker_Immediate p Q) g' e)) χ ∧
expr_pr_inner χ ≤ updated (Attacker_Immediate p Q) g' e)›
using g'_att_del Attacker_Immediate by fastforce
then obtain χ where ‹(strategy_formula_inner (Attacker_Delayed p Q') e χ ∧ expr_pr_inner χ ≤ e)›
using ‹p' = p› ‹weight (Attacker_Immediate p Q) (Attacker_Delayed p' Q') e = Some e› g'_att_del by auto
hence ‹((∃Q'. (spectroscopy_moves (Attacker_Immediate p Q) (Attacker_Delayed p Q')
= (Some Some)) ∧ (attacker_wins e (Attacker_Delayed p Q'))
∧ strategy_formula_inner (Attacker_Delayed p Q') e χ))›
using g'_att_del
by (smt (verit) Spectroscopy_Game.LTS_Tau.delay ‹attacker_wins e (Attacker_Delayed p Q')› Attacker_Immediate)
hence ‹strategy_formula (Attacker_Immediate p Q) e (Internal χ)›
using strategy_formula_strategy_formula_inner_strategy_formula_conjunct.delay by blast
moreover have ‹expressiveness_price (Internal χ) ≤ e›
using ‹(strategy_formula_inner (Attacker_Delayed p Q') e χ ∧ expr_pr_inner χ ≤ e)›
by auto
ultimately show ?case by auto
next
assume ‹∃p' Q'. g' = Defender_Conj p' Q'›
then obtain p' Q' where g'_def_conj: ‹g' = Defender_Conj p' Q'› by blast
hence M: ‹spectroscopy_moves (Attacker_Immediate p Q) (Defender_Conj p' Q') = (subtract 0 0 0 0 1 0 0 0)›
using local.f_or_early_conj Attacker_Immediate by presburger
hence Qp': ‹Q≠{}› ‹Q = Q'› ‹p = p'›
using Attack.hyps(2) Attacker_Immediate g'_def_conj local.f_or_early_conj by metis+
from M have ‹updated (Attacker_Immediate p Q) (Defender_Conj p' Q') e
= e - (E 0 0 0 0 1 0 0 0)›
using Attack.hyps(3) g'_def_conj Attacker_Immediate
by (smt (verit) option.distinct(1) option.sel)
hence ‹(attacker_wins (e - (E 0 0 0 0 1 0 0 0)) (Defender_Conj p Q'))›
using g'_def_conj Qp' Attacker_Immediate win_a_upwards_closure by force
with g'_def_conj have IH_case: ‹∃χ. strategy_formula_inner g' (updated (Attacker_Immediate p Q) g' e) χ ∧
expr_pr_inner χ ≤ updated (Attacker_Immediate p Q) g' e›
using Attacker_Immediate by auto
hence ‹(∃χ. strategy_formula_inner (Defender_Conj p Q) (e - (E 0 0 0 0 1 0 0 0)) χ ∧ expr_pr_inner χ ≤ (e - (E 0 0 0 0 1 0 0 0)))›
using ‹attacker_wins (e - (E 0 0 0 0 1 0 0 0)) (Defender_Conj p Q')› IH_case Qp'
‹the (weight (Attacker_Immediate p Q) (Defender_Conj p' Q') e) = e - E 0 0 0 0 1 0 0 0› g'_def_conj by auto
then obtain χ where S: ‹(strategy_formula_inner (Defender_Conj p Q) (e - (E 0 0 0 0 1 0 0 0)) χ ∧ expr_pr_inner χ ≤ (e - (E 0 0 0 0 1 0 0 0)))›
by blast
hence ‹∃ψ. χ = Conj Q ψ›
using strategy_formula_strategy_formula_inner_strategy_formula_conjunct.conj Qp' g'_def_conj Attacker_Immediate unfolding Qp'
by (smt (verit) spectroscopy_moves.simps(60,70) spectroscopy_position.distinct(33) spectroscopy_position.inject(6) strategy_formula_inner.simps)
then obtain ψ where ‹χ = Conj Q ψ› by auto
hence ‹strategy_formula (Defender_Conj p Q) (e - (E 0 0 0 0 1 0 0 0)) (ImmConj Q ψ)›
using S strategy_formula_strategy_formula_inner_strategy_formula_conjunct.conj strategy_formula_strategy_formula_inner_strategy_formula_conjunct.imm_conj
by (smt (verit) Qp' g'_def_conj hml_srbb_inner.inject(2) Attacker_Immediate spectroscopy_defender.simps(4,6) spectroscopy_moves.simps(60) spectroscopy_moves.simps(70) strategy_formula_inner.cases)
hence SI: ‹strategy_formula (Attacker_Immediate p Q) e (ImmConj Q ψ)›
using strategy_formula_strategy_formula_inner_strategy_formula_conjunct.delay early_conj Qp'
by (metis (no_types, lifting) ‹attacker_wins (e - E 0 0 0 0 1 0 0 0) (Defender_Conj p Q')› local.f_or_early_conj)
have ‹expr_pr_inner (Conj Q ψ) ≤ (e - (E 0 0 0 0 1 0 0 0))› using S ‹χ = Conj Q ψ› by simp
hence ‹expressiveness_price (ImmConj Q ψ) ≤ e› using expr_imm_conj Qp'
by (smt (verit) M g'_def_conj Attacker_Immediate option.sel option.simps(3))
thus ?thesis using SI by auto
qed
next
case (Attacker_Branch p Q)
hence g'_def: ‹g' = Attacker_Immediate p Q› using br_acct
by (metis (no_types, lifting) spectroscopy_defender.elims(2,3) spectroscopy_moves.simps(17,51,57,61,66,71))
hence move: ‹spectroscopy_moves (Attacker_Branch p Q) g' = subtract 1 0 0 0 0 0 0 0› by simp
then obtain φ where
‹strategy_formula g' (updated (Attacker_Branch p Q) g' e) φ ∧
expressiveness_price φ ≤ updated (Attacker_Branch p Q) g' e›
using Attacker_Branch g'_def by auto
hence ‹(strategy_formula (Attacker_Immediate p Q) (e - E 1 0 0 0 0 0 0 0) φ)
∧ expressiveness_price φ ≤ e - E 1 0 0 0 0 0 0 0›
using move Attacker_Branch unfolding g'_def
by (smt (verit, del_insts) option.distinct(1) option.sel)
then show ?case by auto
next
case (Attacker_Clause p q)
hence ‹(∃p' Q'. g' = (Attacker_Delayed p' Q'))›
using Attack.hyps spectroscopy_moves.simps
by (smt (verit, del_insts) spectroscopy_defender.elims(1))
then obtain p' Q' where
g'_att_del: ‹g' = Attacker_Delayed p' Q'› by blast
show ?case
proof(cases ‹p = p'›)
case True
hence ‹{q} ↠S Q'›
using g'_att_del local.pos_neg_clause Attacker_Clause by presburger
hence post_win:
‹(the (spectroscopy_moves (Attacker_Clause p q) g') e) = min1_6 e›
‹(attacker_wins (the (min1_6 e)) (Attacker_Delayed p Q'))›
using ‹{q} ↠S Q'› Attacker_Clause win_a_upwards_closure unfolding True g'_att_del
by auto
then obtain χ where χ_spec:
‹strategy_formula_inner (Attacker_Delayed p Q') (the (min1_6 e)) χ›
‹expr_pr_inner χ ≤ the (min1_6 e)›
using Attacker_Clause Attack True post_win unfolding g'_att_del
by (smt (verit) option.sel spectroscopy_position.simps(53))
hence
‹spectroscopy_moves (Attacker_Clause p q) (Attacker_Delayed p Q') = Some min1_6›
‹attacker_wins (the (min1_6 e)) (Attacker_Delayed p Q')›
‹strategy_formula_inner (Attacker_Delayed p Q') (the (min1_6 e)) χ›
using ‹{q} ↠S Q'› local.pos_neg_clause post_win by auto
hence ‹strategy_formula_conjunct (Attacker_Clause p q) e (Pos χ)›
using strategy_formula_strategy_formula_inner_strategy_formula_conjunct.delay pos
by blast
thus ?thesis
using χ_spec expr_pos by fastforce
next
case False
hence Qp': ‹{p} ↠S Q'› ‹p' = q›
using local.pos_neg_clause Attacker_Clause unfolding g'_att_del
by presburger+
hence move: ‹spectroscopy_moves (Attacker_Clause p q) (Attacker_Delayed p' Q')
= Some (λe. Option.bind ((subtract_fn 0 0 0 0 0 0 0 1) e) min1_7)›
using False by auto
hence win: ‹attacker_wins (the (min1_7 (e - E 0 0 0 0 0 0 0 1))) (Attacker_Delayed p' Q')›
using Attacker_Clause unfolding g'_att_del
by (smt (verit) bind.bind_lunit bind.bind_lzero option.distinct(1) option.sel)
hence ‹(∃φ. strategy_formula_inner (Attacker_Delayed p' Q') (the (min1_7 (e - E 0 0 0 0 0 0 0 1))) φ
∧ expr_pr_inner φ ≤ the (min1_7 (e - E 0 0 0 0 0 0 0 1)))›
using Attack Attacker_Clause move unfolding g'_att_del
by (smt (verit, del_insts) bind.bind_lunit bind_eq_None_conv option.discI option.sel spectroscopy_position.simps(53))
then obtain χ where χ_spec:
‹strategy_formula_inner (Attacker_Delayed p' Q') (the (min1_7 (e - E 0 0 0 0 0 0 0 1))) χ›
‹expr_pr_inner χ ≤ the (min1_7 (e - E 0 0 0 0 0 0 0 1))›
by blast
hence ‹strategy_formula_conjunct (Attacker_Clause p q) e (Neg χ)›
using strategy_formula_strategy_formula_inner_strategy_formula_conjunct.delay
neg Qp' win move by blast
thus ?thesis
using χ_spec Attacker_Clause expr_neg move
unfolding g'_att_del
by (smt (verit, best) bind.bind_lunit bind_eq_None_conv option.distinct(1) option.sel spectroscopy_position.simps(52))
qed
next
case (Attacker_Delayed p Q)
then consider
(Att_Del) ‹(∃p Q. g' = Attacker_Delayed p Q)› | (Att_Imm) ‹(∃p' Q'. g' = (Attacker_Immediate p' Q'))› |
(Def_Conj) ‹(∃p Q. g' = (Defender_Conj p Q))› | (Def_St_Conj) ‹(∃p Q. g' = (Defender_Stable_Conj p Q))› |
(Def_Branch) ‹(∃p' α p'' Q' Qα. g' = (Defender_Branch p' α p'' Q' Qα))›
by (smt (verit, ccfv_threshold) spectroscopy_defender.elims(1) spectroscopy_moves.simps(27,28))
then show ?case
proof (cases)
case Att_Del
then obtain p' Q' where
g'_att_del: ‹g' = Attacker_Delayed p' Q'› by blast
have Qp': ‹Q' = Q› ‹p ≠ p'› ‹p ↦ τ p'›
using Attacker_Delayed g'_att_del Spectroscopy_Game.LTS_Tau.procrastination
by metis+
hence e_comp: ‹(the (spectroscopy_moves (Attacker_Delayed p Q) g') e) = Some e›
using g'_att_del
by simp
hence att_win: ‹(attacker_wins e (Attacker_Delayed p' Q'))›
using g'_att_del Qp' Attacker_Delayed attacker_wins.Defense e_comp
by (metis option.sel)
have ‹(updated (Attacker_Delayed p Q) g' e) = e›
using g'_att_del Attacker_Delayed e_comp by fastforce
then obtain χ where ‹(strategy_formula_inner (Attacker_Delayed p' Q') e χ ∧ expr_pr_inner χ ≤ e)›
using Attacker_Delayed g'_att_del by auto
hence ‹∃p'. spectroscopy_moves (Attacker_Delayed p Q) (Attacker_Delayed p' Q) = (Some Some)
∧ attacker_wins e (Attacker_Delayed p' Q)
∧ strategy_formula_inner (Attacker_Delayed p' Q) e χ›
using e_comp g'_att_del Qp' local.procrastination Attack.hyps att_win
Spectroscopy_Game.LTS_Tau.procrastination
by metis
hence ‹strategy_formula_inner (Attacker_Delayed p Q) e χ›
using strategy_formula_strategy_formula_inner_strategy_formula_conjunct.procrastination by blast
moreover have ‹expr_pr_inner χ ≤ e›
using ‹strategy_formula_inner (Attacker_Delayed p' Q') e χ ∧ expr_pr_inner χ ≤ e› by blast
ultimately show ?thesis by auto
next
case Att_Imm
then obtain p' Q' where
g'_att_imm: ‹g' = Attacker_Immediate p' Q'› by blast
hence move: ‹spectroscopy_moves (Attacker_Delayed p Q) (Attacker_Immediate p' Q') ≠ None›
using Attacker_Delayed by blast
hence ‹∃a. p ↦a a p' ∧ Q ↦aS a Q'› unfolding spectroscopy_moves.simps(3) by presburger
then obtain α where α_prop: ‹p ↦a α p'› ‹Q ↦aS α Q'› by blast
moreover then have weight:
‹spectroscopy_moves (Attacker_Delayed p Q) (Attacker_Immediate p' Q') = subtract 1 0 0 0 0 0 0 0›
by (simp, metis)
moreover then have update: ‹updated (Attacker_Delayed p Q) g' e = e - (E 1 0 0 0 0 0 0 0)›
using g'_att_imm Attacker_Delayed
by (smt (verit, del_insts) option.distinct(1) option.sel)
moreover then obtain χ where χ_prop:
‹strategy_formula (Attacker_Immediate p' Q') (e - E 1 0 0 0 0 0 0 0) χ›
‹expressiveness_price χ ≤ e - E 1 0 0 0 0 0 0 0›
using Attacker_Delayed g'_att_imm
by auto
moreover have ‹attacker_wins (e - (E 1 0 0 0 0 0 0 0)) (Attacker_Immediate p' Q')›
using attacker_wins.Attack Attack.hyps(4) Attacker_Delayed.prems(3) calculation(4) g'_att_imm
by force
ultimately have ‹strategy_formula_inner (Attacker_Delayed p Q) e (Obs α χ)›
using local.observation[of p Q e χ α] by blast
moreover have ‹expr_pr_inner (Obs α χ) ≤ e›
using expr_obs χ_prop Attacker_Delayed g'_att_imm weight update
by (smt (verit) option.sel)
ultimately show ?thesis by auto
next
case Def_Conj
then obtain p' Q' where
g'_def_conj: ‹g' = Defender_Conj p' Q'› by blast
hence ‹p = p'› ‹Q = Q'›
using local.late_inst_conj Attacker_Delayed by presburger+
hence ‹the (spectroscopy_moves (Attacker_Delayed p Q) (Defender_Conj p' Q')) e = Some e›
by fastforce
hence ‹attacker_wins e (Defender_Conj p' Q')› ‹updated g g' e = e›
using Attacker_Delayed Attack unfolding g'_def_conj by simp+
then obtain χ where
χ_prop: ‹(strategy_formula_inner (Defender_Conj p' Q') e χ ∧ expr_pr_inner χ ≤ e)›
using Attack g'_def_conj by auto
hence
‹spectroscopy_moves (Attacker_Delayed p Q) (Defender_Conj p' Q') = Some Some
∧ attacker_wins e (Defender_Conj p' Q')
∧ strategy_formula_inner (Defender_Conj p' Q') e χ›
by (simp add: ‹Q = Q'› ‹attacker_wins e (Defender_Conj p' Q')› ‹p = p'›)
then show ?thesis
using χ_prop ‹Q = Q'› ‹attacker_wins e (Defender_Conj p' Q')› ‹p = p'› late_conj
by fastforce
next
case Def_St_Conj
then obtain p' Q' where g'_def: ‹g' = Defender_Stable_Conj p' Q'› by blast
hence pQ': ‹p = p'› ‹Q' = { q ∈ Q. (∄q'. q ↦τ q')}› ‹∄p''. p ↦τ p''›
using local.late_stbl_conj Attacker_Delayed
by meson+
hence ‹(the (spectroscopy_moves (Attacker_Delayed p Q) (Defender_Stable_Conj p' Q')) e) = Some e›
by auto
hence ‹attacker_wins e (Defender_Stable_Conj p' Q')› ‹updated g g' e = e›
using Attacker_Delayed Attack unfolding g'_def by force+
then obtain χ where χ_prop:
‹strategy_formula_inner (Defender_Stable_Conj p' Q') e χ› ‹expr_pr_inner χ ≤ e›
using Attack g'_def by auto
have ‹spectroscopy_moves (Attacker_Delayed p Q) (Defender_Stable_Conj p' Q') = Some Some
∧ attacker_wins e (Defender_Stable_Conj p' Q')
∧ strategy_formula_inner (Defender_Stable_Conj p' Q') e χ›
using Attack χ_prop ‹attacker_wins e (Defender_Stable_Conj p' Q')› local.late_stbl_conj pQ'
unfolding g'_def
by force
thus ?thesis using local.stable[of p Q e χ] pQ' χ_prop by fastforce
next
case Def_Branch
then obtain p' α p'' Q' Qα where
g'_def_br: ‹g' = Defender_Branch p' α p'' Q' Qα› by blast
hence pQ': ‹p = p'› ‹Q' = Q - Qα› ‹p ↦a α p''› ‹Qα ⊆ Q›
using local.br_conj Attacker_Delayed by metis+
hence ‹the (spectroscopy_moves (Attacker_Delayed p Q) (Defender_Branch p' α p'' Q' Qα)) e = Some e›
by auto
hence post: ‹attacker_wins e (Defender_Branch p' α p'' Q' Qα)› ‹updated g g' e = e›
using Attack option.inject Attacker_Delayed unfolding g'_def_br by auto
then obtain χ where χ_prop:
‹strategy_formula_inner (Defender_Branch p' α p'' Q' Qα) e χ› ‹expr_pr_inner χ ≤ e›
using g'_def_br Attack Attacker_Delayed
by auto
hence ‹spectroscopy_moves (Attacker_Delayed p Q) (Defender_Branch p α p'' Q' Qα) = Some Some
∧ attacker_wins e (Defender_Branch p α p'' Q' Qα)
∧ strategy_formula_inner (Defender_Branch p α p'' Q' Qα) e χ›
using g'_def_br local.branch Attack post pQ' by simp
hence ‹strategy_formula_inner (Attacker_Delayed p Q) e χ›
using Attack Attacker_Delayed local.br_conj branch
unfolding g'_def_br by fastforce
thus ?thesis using χ_prop
by fastforce
qed
next
case (Defender_Branch)
thus ?case by force
next
case (Defender_Conj)
thus ?case by force
next
case (Defender_Stable_Conj)
thus ?case by force
qed
next
case (Defense g e)
thus ?case
proof (induct g)
case (Attacker_Immediate)
thus ?case by force
next
case (Attacker_Branch)
thus ?case by force
next
case (Attacker_Clause)
thus ?case by force
next
case (Attacker_Delayed)
thus ?case by force
next
case (Defender_Branch p α p' Q Qa)
hence conjs:
‹∀q∈ Q. spectroscopy_moves (Defender_Branch p α p' Q Qa) (Attacker_Clause p q) = (subtract 0 1 1 0 0 0 0 0)›
by simp
obtain e' where e'_spec:
‹∀q∈Q. weight (Defender_Branch p α p' Q Qa) (Attacker_Clause p q) e = Some e'
∧ attacker_wins e' (Attacker_Clause p q)
∧ (∃ψ. strategy_formula_conjunct (Attacker_Clause p q) e' ψ ∧ expr_pr_conjunct ψ ≤ e')›
using conjs Defender_Branch option.distinct(1) option.sel
by (smt (z3) spectroscopy_position.simps(52))
hence e'_def: ‹Q ≠ {} ⟹ e' = e - E 0 1 1 0 0 0 0 0› using conjs
by (smt (verit) all_not_in_conv option.distinct(1) option.sel)
then obtain Φ where Φ_spec:
‹∀q ∈ Q. strategy_formula_conjunct (Attacker_Clause p q) e' (Φ q) ∧ expr_pr_conjunct (Φ q) ≤ e'›
using e'_spec by metis
have obs: ‹spectroscopy_moves (Defender_Branch p α p' Q Qa) (Attacker_Branch p' (soft_step_set Qa α)) =
Some (λe. Option.bind ((subtract_fn 0 1 1 0 0 0 0 0) e) min1_6)›
by (simp add: soft_step_set_is_soft_step_set)
have ‹∀p Q. (Attacker_Branch p' (soft_step_set Qa α)) = (Attacker_Branch p Q) ⟶ p = p' ∧ Q = soft_step_set Qa α› by blast
with option.discI[OF obs] obtain e'' where
‹∃φ. strategy_formula (Attacker_Immediate p' (soft_step_set Qa α)) (e'' - E 1 0 0 0 0 0 0 0) φ
∧ expressiveness_price φ ≤ e'' - E 1 0 0 0 0 0 0 0›
using Defense.IH option.distinct(1) option.sel
by (smt (verit, best) Defender_Branch.prems(2) spectroscopy_position.simps(51))
then obtain φ where
‹strategy_formula (Attacker_Immediate p' (soft_step_set Qa α))
(updated (Defender_Branch p α p' Q Qa) (Attacker_Branch p' (soft_step_set Qa α)) e - E 1 0 0 0 0 0 0 0) φ›
‹expressiveness_price φ ≤ updated (Defender_Branch p α p' Q Qa) (Attacker_Branch p' (soft_step_set Qa α)) e - E 1 0 0 0 0 0 0 0›
using Defender_Branch.prems(2) option.discI[OF obs]
by (smt (verit, best) option.sel spectroscopy_position.simps(51))
hence obs_strat:
‹strategy_formula (Attacker_Immediate p' (soft_step_set Qa α)) (the (min1_6 (e - E 0 1 1 0 0 0 0 0)) - (E 1 0 0 0 0 0 0 0)) φ›
‹expressiveness_price φ ≤ (the (min1_6 (e - E 0 1 1 0 0 0 0 0)) - (E 1 0 0 0 0 0 0 0))›
by (smt (verit, best) Defender_Branch.prems(2) bind.bind_lunit bind.bind_lzero obs option.distinct(1) option.sel)+
have ‹spectroscopy_moves (Attacker_Branch p' (soft_step_set Qa α)) (Attacker_Immediate p' (soft_step_set Qa α))
= (subtract 1 0 0 0 0 0 0 0)› by simp
obtain e'' where win_branch:
‹Some e'' = min1_6 (e - E 0 1 1 0 0 0 0 0)›
‹attacker_wins e'' (Attacker_Branch p' (soft_step_set Qa α))›
using Defender_Branch
by (smt (verit, ccfv_threshold) bind.bind_lunit bind_eq_None_conv obs option.discI option.sel)
then obtain g'' where g''_spec:
‹spectroscopy_moves (Attacker_Branch p' (soft_step_set Qa α)) g'' ≠ None›
‹attacker_wins (updated (Attacker_Branch p' (soft_step_set Qa α)) g'' (the (min1_6 (e - E 0 1 1 0 0 0 0 0)))) g''›
using attacker_wins_GaE
by (metis option.sel spectroscopy_defender.simps(2))
hence move_immediate:
‹g'' = (Attacker_Immediate p' (soft_step_set Qa α))
∧ spectroscopy_moves (Attacker_Branch p' (soft_step_set Qa α)) (Attacker_Immediate p' (soft_step_set Qa α)) = subtract 1 0 0 0 0 0 0 0›
using br_acct
by (metis (no_types, lifting) spectroscopy_defender.elims(2,3) spectroscopy_moves.simps(17,51,57,61,66,71))
then obtain e''' where win_immediate:
‹Some e''' = subtract_fn 1 0 0 0 0 0 0 0 e''›
‹attacker_wins e''' (Attacker_Immediate p' (soft_step_set Qa α))›
using g''_spec win_branch attacker_wins.simps local.br_acct
by (smt (verit) option.distinct(1) option.sel spectroscopy_defender.elims(1) spectroscopy_moves.simps(17,19,20,51,57,61))
hence strat: ‹strategy_formula_inner (Defender_Branch p α p' Q Qa) e (BranchConj α φ Q Φ)›
using branch_conj obs move_immediate obs_strat Φ_spec conjs e'_def e'_spec
by (smt (verit, best) option.distinct(1) option.sel win_branch(1))
have ‹E 1 0 0 0 0 0 0 0 ≤ e''› using win_branch g''_spec
by (metis option.distinct(1) win_immediate(1))
hence above_one: ‹0 < min (modal_depth e) (pos_conjuncts e)›
using win_immediate win_branch
by (metis energy.sel(1) energy.sel(6) gr_zeroI idiff_0_right leq_components
min_1_6_simps(1) minus_energy_def not_one_le_zero option.sel)
have ‹∀q ∈ Q. expr_pr_conjunct (Φ q) ≤ (e - (E 0 1 1 0 0 0 0 0))›
using Φ_spec e'_def by blast
moreover have ‹expressiveness_price φ ≤ the (min1_6 (e - E 0 1 1 0 0 0 0 0)) - E 1 0 0 0 0 0 0 0›
using obs_strat(2) by blast
moreover hence ‹modal_depth_srbb φ ≤ min (modal_depth e) (pos_conjuncts e) - 1›
by simp
hence ‹1 + modal_depth_srbb φ ≤ min (modal_depth e) (pos_conjuncts e)›
by (metis above_one add.right_neutral add_diff_cancel_enat add_mono_thms_linordered_semiring(1) enat.simps(3) enat_defs(2) ileI1 le_iff_add plus_1_eSuc(1))
moreover hence ‹1 + modal_depth_srbb φ ≤ pos_conjuncts e› by simp
ultimately have ‹expr_pr_inner (BranchConj α φ Q Φ) ≤ e›
using expr_br_conj[of e e' e'' e''' φ Q Φ α] e'_def obs Defender_Branch(2) win_branch(1) win_immediate(1)
by (smt (verit, best) bind_eq_None_conv expr_br_conj option.distinct(1) option.sel option.simps(3))
then show ?case using strat by force
next
case (Defender_Conj p Q)
hence moves:
‹∀g'. spectroscopy_moves (Defender_Conj p Q) g' ≠ None ⟶ (∃e'. weight (Defender_Conj p Q) g' e = Some e' ∧ attacker_wins e' g')
∧ (∃q. g' = (Attacker_Clause p q))›
using local.conj_answer
by (metis (no_types, lifting) spectroscopy_defender.elims(2,3) spectroscopy_moves.simps(34,35,36,37,38,39))
show ?case
proof (cases ‹Q = {}›)
case True
then obtain Φ where ‹∀q ∈ Q.
spectroscopy_moves (Defender_Conj p Q) (Attacker_Clause p q) = (subtract 0 0 1 0 0 0 0 0)
∧ (attacker_wins (e - (E 0 0 1 0 0 0 0 0)) (Attacker_Clause p q))
∧ strategy_formula_conjunct (Attacker_Clause p q) (e - (E 0 0 1 0 0 0 0 0)) (Φ q)›
by (auto simp add: emptyE)
hence Strat: ‹strategy_formula_inner (Defender_Conj p Q) e (Conj {} Φ)›
using ‹Q = {}› conj by blast
hence
‹modal_depth_srbb_inner (Conj Q Φ) = Sup ((modal_depth_srbb_conjunct ∘ Φ) ` Q)›
‹branch_conj_depth_inner (Conj Q Φ) = Sup ((branch_conj_depth_conjunct ∘ Φ) ` Q)›
‹inst_conj_depth_inner (Conj Q Φ) = 0›
‹st_conj_depth_inner (Conj Q Φ) = Sup ((st_conj_depth_conjunct ∘ Φ) ` Q)›
‹imm_conj_depth_inner (Conj Q Φ) = Sup ((imm_conj_depth_conjunct ∘ Φ) ` Q)›
‹max_pos_conj_depth_inner (Conj Q Φ) = Sup ((max_pos_conj_depth_conjunct ∘ Φ) ` Q)›
‹max_neg_conj_depth_inner (Conj Q Φ) = Sup ((max_neg_conj_depth_conjunct ∘ Φ) ` Q)›
‹neg_depth_inner (Conj Q Φ) = Sup ((neg_depth_conjunct ∘ Φ) ` Q)›
using modal_depth_srbb_inner.simps(3) branch_conj_depth_inner.simps st_conj_depth_inner.simps
inst_conj_depth_inner.simps imm_conj_depth_inner.simps max_pos_conj_depth_inner.simps
max_neg_conj_depth_inner.simps neg_depth_inner.simps ‹Q = {}›
by auto+
hence
‹modal_depth_srbb_inner (Conj Q Φ) = 0›
‹branch_conj_depth_inner (Conj Q Φ) = 0›
‹inst_conj_depth_inner (Conj Q Φ) = 0›
‹st_conj_depth_inner (Conj Q Φ) = 0›
‹imm_conj_depth_inner (Conj Q Φ) = 0›
‹max_pos_conj_depth_inner (Conj Q Φ) = 0›
‹max_neg_conj_depth_inner (Conj Q Φ) = 0›
‹neg_depth_inner (Conj Q Φ) = 0›
using ‹Q = {}› by (simp add: bot_enat_def)+
hence ‹expr_pr_inner (Conj Q Φ) = (E 0 0 0 0 0 0 0 0)›
using ‹Q = {}› by force
hence price: ‹expr_pr_inner (Conj Q Φ) ≤ e›
by auto
with Strat price True show ?thesis by auto
next
case False
hence fa_q: ‹∀q ∈ Q. ∃e'.
Some e' = subtract_fn 0 0 1 0 0 0 0 0 e
∧ spectroscopy_moves (Defender_Conj p Q) (Attacker_Clause p q) = (subtract 0 0 1 0 0 0 0 0)
∧ attacker_wins e' (Attacker_Clause p q)›
using moves local.conj_answer option.distinct(1)
by (smt (z3) option.sel)
have q_ex_e': ‹∀q ∈ Q. ∃e'.
spectroscopy_moves (Defender_Conj p Q) (Attacker_Clause p q) = subtract 0 0 1 0 0 0 0 0
∧ Some e' = subtract_fn 0 0 1 0 0 0 0 0 e
∧ attacker_wins e' (Attacker_Clause p q)
∧ (∃φ. strategy_formula_conjunct (Attacker_Clause p q) e' φ ∧ expr_pr_conjunct φ ≤ e')›
proof safe
fix q
assume ‹q ∈ Q›
then obtain e' where e'_spec:
‹Some e' = subtract_fn 0 0 1 0 0 0 0 0 e›
‹spectroscopy_moves (Defender_Conj p Q) (Attacker_Clause p q) = (subtract 0 0 1 0 0 0 0 0)›
‹attacker_wins e' (Attacker_Clause p q)›
using fa_q by blast
hence ‹weight (Defender_Conj p Q) (Attacker_Clause p q) e = Some e'›
by simp
then have ‹∃ψ. strategy_formula_conjunct (Attacker_Clause p q) e' ψ ∧ expr_pr_conjunct ψ ≤ e'›
using Defender_Conj e'_spec
by (smt (verit, best) option.distinct(1) option.sel spectroscopy_position.simps(52))
thus ‹∃e'. spectroscopy_moves (Defender_Conj p Q) (Attacker_Clause p q) = (subtract 0 0 1 0 0 0 0 0) ∧
Some e' = subtract_fn 0 0 1 0 0 0 0 0 e ∧
attacker_wins e' (Attacker_Clause p q) ∧ (∃φ. strategy_formula_conjunct (Attacker_Clause p q) e' φ ∧ expr_pr_conjunct φ ≤ e')›
using e'_spec by blast
qed
hence ‹∃Φ. ∀q ∈ Q.
attacker_wins (e - E 0 0 1 0 0 0 0 0) (Attacker_Clause p q)
∧ (strategy_formula_conjunct (Attacker_Clause p q) (e - E 0 0 1 0 0 0 0 0) (Φ q)
∧ expr_pr_conjunct (Φ q) ≤ (e - E 0 0 1 0 0 0 0 0))›
by (metis (no_types, opaque_lifting) option.distinct(1) option.inject)
then obtain Φ where IH:
‹∀q ∈ Q. attacker_wins (e - E 0 0 1 0 0 0 0 0) (Attacker_Clause p q)
∧ (strategy_formula_conjunct (Attacker_Clause p q) (e - E 0 0 1 0 0 0 0 0) (Φ q)
∧ expr_pr_conjunct (Φ q) ≤ (e - E 0 0 1 0 0 0 0 0))› by auto
hence ‹strategy_formula_inner (Defender_Conj p Q) e (Conj Q Φ)›
by (simp add: conj)
moreover have ‹expr_pr_inner (Conj Q Φ) ≤ e›
using IH expr_conj ‹Q ≠ {}› q_ex_e'
by (metis (no_types, lifting) equals0I option.distinct(1))
ultimately show ?thesis by auto
qed
next
case (Defender_Stable_Conj p Q)
hence cases:
‹∀g'. spectroscopy_moves (Defender_Stable_Conj p Q) g' ≠ None ⟶
(∃e'. weight (Defender_Stable_Conj p Q) g' e = Some e' ∧ attacker_wins e' g')
∧ ((∃p' q. g' = (Attacker_Clause p' q)) ∨ (∃p' Q'. g' = (Defender_Conj p' Q')))›
by (metis (no_types, opaque_lifting)
spectroscopy_defender.elims(2,3) spectroscopy_moves.simps(40,42,43,44,55))
show ?case
proof(cases ‹Q = {}›)
case True
then obtain e' where e'_spec:
‹weight (Defender_Stable_Conj p Q) (Defender_Conj p Q) e = Some e'›
‹e' = e - (E 0 0 0 1 0 0 0 0)›
‹attacker_wins e' (Defender_Conj p Q)›
using cases local.empty_stbl_conj_answer
by (smt (verit, best) option.discI option.sel)
then obtain Φ where Φ_prop: ‹strategy_formula_inner (Defender_Conj p Q) e' (Conj Q Φ)›
using conj True by blast
hence strategy: ‹strategy_formula_inner (Defender_Stable_Conj p Q) e (StableConj Q Φ)›
by (simp add: True stable_conj)
have ‹E 0 0 0 1 0 0 0 0 ≤ e› using e'_spec
using option.sel True by fastforce
moreover have ‹expr_pr_inner (StableConj Q Φ) = E 0 0 0 1 0 0 0 0›
using True by (simp add: bot_enat_def)
ultimately have ‹expr_pr_inner (StableConj Q Φ) ≤ e› by simp
with strategy show ?thesis by auto
next
case False
then obtain e' where e'_spec:
‹e' = e - (E 0 0 0 1 0 0 0 0)›
‹∀q ∈ Q. weight (Defender_Stable_Conj p Q) (Attacker_Clause p q) e = Some e'
∧ attacker_wins e' (Attacker_Clause p q)›
using cases local.conj_s_answer
by (smt (verit, del_insts) option.distinct(1) option.sel)
hence IH: ‹∀q ∈ Q. ∃ψ.
strategy_formula_conjunct (Attacker_Clause p q) e' ψ ∧
expr_pr_conjunct ψ ≤ e'›
using Defender_Stable_Conj local.conj_s_answer
by (smt (verit, best) option.distinct(1) option.inject spectroscopy_position.simps(52))
hence ‹∃Φ. ∀q ∈ Q.
strategy_formula_conjunct (Attacker_Clause p q) e' (Φ q) ∧
expr_pr_conjunct (Φ q) ≤ e'›
by meson
then obtain Φ where Φ_prop: ‹∀q ∈ Q.
strategy_formula_conjunct (Attacker_Clause p q) e' (Φ q)
∧ expr_pr_conjunct (Φ q) ≤ e'›
by blast
have ‹E 0 0 0 1 0 0 0 0 ≤ e›
using e'_spec False by fastforce
hence ‹expr_pr_inner (StableConj Q Φ) ≤ e›
using expr_st_conj e'_spec Φ_prop False by metis
moreover have ‹strategy_formula_inner (Defender_Stable_Conj p Q) e (StableConj Q Φ)›
using Φ_prop e'_spec stable_conj
unfolding e'_spec by fastforce
ultimately show ?thesis by auto
qed
qed
qed
text ‹To prove ‹spectroscopy_game_correctness› we need the following implication:
If ‹φ› is a strategy formula for ‹Attacker_Immediate p Q› with energy ‹e›, then ‹φ› distinguishes
‹p› from ‹Q›.
\\
\\
We prove a more detailed result for all possible game positions ‹g› by induction. Note that the
case of ‹g› being an attacker branching position is not explicitly needed as part of the induction
hypothesis but is proven as a part of case ‹branch_conj›. The induction relies on the inductive
structure of strategy formulas.
\\
Since our formalization differentiates immediate conjunctions and conjunctions, two ‹Defender_Conj›
cases are necessary. Specifically, the strategy construction rule ‹early_conj› uses immediate
conjunctions, while ‹late_conj› uses conjunctions. \label{deviation:lemma3}
›
lemma strategy_formulas_distinguish:
shows ‹(strategy_formula g e φ ⟶
(case g of
Attacker_Immediate p Q ⇒ distinguishes_from φ p Q
| Defender_Conj p Q ⇒ distinguishes_from φ p Q
| _ ⇒ True))
∧
(strategy_formula_inner g e χ ⟶
(case g of
Attacker_Delayed p Q ⇒ (Q ↠S Q) ⟶ distinguishes_from (Internal χ) p Q
| Defender_Conj p Q ⇒ hml_srbb_inner.distinguishes_from χ p Q
| Defender_Stable_Conj p Q ⇒ (∀q. ¬ p ↦ τ q)
⟶ hml_srbb_inner.distinguishes_from χ p Q
| Defender_Branch p α p' Q Qa ⇒(p ↦a α p')
⟶ hml_srbb_inner.distinguishes_from χ p (Q∪Qa)
| _ ⇒ True))
∧
(strategy_formula_conjunct g e ψ ⟶
(case g of
Attacker_Clause p q ⇒ hml_srbb_conj.distinguishes ψ p q
| _ ⇒ True))›
proof(induction rule: strategy_formula_strategy_formula_inner_strategy_formula_conjunct.induct)
case (delay p Q e χ)
then show ?case
by (smt (verit) distinguishes_from_def option.discI silent_reachable.intros(1) silent_reachable_trans spectroscopy_moves.simps(1) spectroscopy_position.simps(50) spectroscopy_position.simps(53))
next
case (procrastination p Q e χ)
from this obtain p' where IH: ‹spectroscopy_moves (Attacker_Delayed p Q) (Attacker_Delayed p' Q) = Some Some ∧
attacker_wins e (Attacker_Delayed p' Q) ∧
strategy_formula_inner (Attacker_Delayed p' Q) e χ ∧
(case Attacker_Delayed p' Q of Attacker_Delayed p Q ⇒ Q ↠S Q ⟶ distinguishes_from (hml_srbb.Internal χ) p Q
| Defender_Branch p α p' Q Qa ⇒ p ↦α p' ∧ Qa ≠ {} ⟶ hml_srbb_inner.distinguishes_from χ p (Q ∪ Qa)
| Defender_Conj p Q ⇒ hml_srbb_inner.distinguishes_from χ p Q
| Defender_Stable_Conj p Q ⇒ (∀q. ¬ p ↦τ q) ⟶ hml_srbb_inner.distinguishes_from χ p Q | _ ⇒ True)› by fastforce
hence D: ‹Q ↠S Q ⟶ distinguishes_from (hml_srbb.Internal χ) p' Q›
using spectroscopy_position.simps(53) by fastforce
from IH have ‹p ↠p'›
by (metis option.discI silent_reachable.intros(1) silent_reachable_append_τ spectroscopy_moves.simps(2))
hence ‹Q ↠S Q ⟶ distinguishes_from (hml_srbb.Internal χ) p Q› using D
by (smt (verit) LTS_Tau.silent_reachable_trans distinguishes_from_def hml_srbb_models.simps(2))
then show ?case by simp
next
case (observation p Q e φ α)
then obtain p' Q' where IH: ‹spectroscopy_moves (Attacker_Delayed p Q) (Attacker_Immediate p' Q') = subtract 1 0 0 0 0 0 0 0 ∧
attacker_wins (e - E 1 0 0 0 0 0 0 0) (Attacker_Immediate p' Q') ∧
(strategy_formula (Attacker_Immediate p' Q') (e - E 1 0 0 0 0 0 0 0) φ ∧
(case Attacker_Immediate p' Q' of Attacker_Immediate p Q ⇒ distinguishes_from φ p Q
| Defender_Conj p Q ⇒ distinguishes_from φ p Q | _ ⇒ True)) ∧
p ↦a α p' ∧ Q ↦aS α Q'› by auto
hence D: ‹distinguishes_from φ p' Q'› by auto
hence ‹p' ⊨SRBB φ› by auto
have observation: ‹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 p' Q Q' by simp
from IH have ‹spectroscopy_moves (Attacker_Delayed p Q) (Attacker_Immediate p' Q')
= subtract 1 0 0 0 0 0 0 0› by simp
also have ‹... ≠ None› by blast
finally have ‹(∃a. p ↦a a p' ∧ Q ↦aS a Q')› unfolding observation by metis
from IH have ‹p ↦a α p'› and ‹Q ↦aS α Q'› by auto
hence P: ‹p ⊨SRBB (Internal (Obs α φ))› using ‹p' ⊨SRBB φ›
using silent_reachable.intros(1) by auto
have ‹Q ↠S Q ⟶ (∀q∈Q. ¬(q ⊨SRBB (Internal (Obs α φ))))›
proof (rule+)
fix q
assume
‹Q ↠S Q›
‹q ∈ Q›
‹q ⊨SRBB Internal (Obs α φ)›
hence ‹∃q'. q ↠ q' ∧ hml_srbb_inner_models q' (Obs α φ)› by simp
then obtain q' where X: ‹q ↠ q' ∧ hml_srbb_inner_models q' (Obs α φ)› by auto
hence ‹hml_srbb_inner_models q' (Obs α φ)› by simp
from X have ‹q'∈Q› using ‹Q ↠S Q› ‹q ∈ Q› by blast
hence ‹∃q''∈Q'. q' ↦a α q'' ∧ q'' ⊨SRBB φ›
using ‹Q ↦aS α Q'› ‹hml_srbb_inner_models q' (Obs α φ)› by auto
then obtain q'' where ‹q''∈Q'∧ q' ↦a α q'' ∧ q'' ⊨SRBB φ› by auto
thus ‹False› using D by auto
qed
hence ‹Q ↠S Q ⟶ distinguishes_from (hml_srbb.Internal (hml_srbb_inner.Obs α φ)) p Q›
using P by fastforce
then show ?case by simp
next
case (early_conj Q p Q' e φ)
then show ?case
by (simp, metis not_None_eq)
next
case (late_conj p Q e χ)
then show ?case
using silent_reachable.intros(1)
by auto
next
case (conj Q p e Φ)
then show ?case by auto
next
case (imm_conj Q p e Φ)
then show ?case by auto
next
case (pos p q e χ)
then show ?case using silent_reachable.refl
by (simp) (metis option.discI silent_reachable_trans)
next
case (neg p q e χ)
then obtain P' where IH:
‹spectroscopy_moves (Attacker_Clause p q) (Attacker_Delayed q P') = Some (λe. Option.bind (subtract_fn 0 0 0 0 0 0 0 1 e) min1_7)›
‹attacker_wins (the (min1_7 (e - E 0 0 0 0 0 0 0 1))) (Attacker_Delayed q P') ∧
strategy_formula_inner (Attacker_Delayed q P') (the (min1_7 (e - E 0 0 0 0 0 0 0 1))) χ ∧
(case Attacker_Delayed q P' of Attacker_Delayed p Q ⇒ Q ↠S Q ⟶ distinguishes_from (hml_srbb.Internal χ) p Q
| Defender_Branch p α p' Q Qa ⇒ p ↦α p' ∧ Qa ≠ {} ⟶ hml_srbb_inner.distinguishes_from χ p (Q ∪ Qa)
| Defender_Conj p Q ⇒ hml_srbb_inner.distinguishes_from χ p Q
| Defender_Stable_Conj p Q ⇒ (∀q. ¬ p ↦τ q) ⟶ hml_srbb_inner.distinguishes_from χ p Q | _ ⇒ True)› by fastforce
hence D: ‹P' ↠S P' ⟶ distinguishes_from (hml_srbb.Internal χ) q P'› by simp
have ‹{p} ↠S P'› using IH(1) spectroscopy_moves.simps
by (metis (no_types, lifting) not_Some_eq)
have ‹P' ↠S P' ⟶ p ∈ P'› using ‹{p} ↠S P'› by (simp add: silent_reachable.intros(1))
hence ‹hml_srbb_conj.distinguishes (hml_srbb_conjunct.Neg χ) p q› using D ‹{p} ↠S P'›
unfolding hml_srbb_conj.distinguishes_def distinguishes_from_def
by (smt (verit) LTS_Tau.silent_reachable_trans hml_srbb_conjunct_models.simps(2) hml_srbb_models.simps(2) silent_reachable.refl)
then show ?case by simp
next
case (stable p Q e χ)
then obtain Q' where IH: ‹spectroscopy_moves (Attacker_Delayed p Q) (Defender_Stable_Conj p Q') = Some Some›
‹attacker_wins e (Defender_Stable_Conj p Q') ∧
strategy_formula_inner (Defender_Stable_Conj p Q') e χ ∧
(case Defender_Stable_Conj p Q' of Attacker_Delayed p Q ⇒ Q ↠S Q ⟶ distinguishes_from (hml_srbb.Internal χ) p Q
| Defender_Branch p α p' Q Qa ⇒ p ↦α p' ∧ Qa ≠ {} ⟶ hml_srbb_inner.distinguishes_from χ p (Q ∪ Qa)
| Defender_Conj p Q ⇒ hml_srbb_inner.distinguishes_from χ p Q
| Defender_Stable_Conj p Q ⇒ (∀q. ¬ p ↦τ q) ⟶ hml_srbb_inner.distinguishes_from χ p Q | _ ⇒ True)› by auto
hence ‹(∄p''. p ↦τ p'')›
by (metis local.late_stbl_conj option.distinct(1))
from IH have ‹(∀q. ¬ p ↦τ q) ⟶ hml_srbb_inner.distinguishes_from χ p Q'› by simp
hence ‹hml_srbb_inner.distinguishes_from χ p Q'› using ‹∄p''. p ↦τ p''› by auto
hence ‹hml_srbb_inner_models p χ› by simp
hence ‹p ⊨SRBB (hml_srbb.Internal χ)›
using LTS_Tau.refl by force
have ‹Q ↠S Q ⟶ distinguishes_from (hml_srbb.Internal χ) p Q›
proof
assume ‹Q ↠S Q›
have ‹(∀q ∈ Q. ¬(q ⊨SRBB (hml_srbb.Internal χ)))›
proof (clarify)
fix q
assume ‹q ∈ Q› ‹(q ⊨SRBB (hml_srbb.Internal χ))›
hence ‹∃q'. q ↠ q' ∧ hml_srbb_inner_models q' χ› by simp
then obtain q' where X: ‹q ↠ q' ∧ hml_srbb_inner_models q' χ› by auto
hence ‹q' ∈ Q› using ‹Q ↠S Q› ‹q ∈ Q› by blast
then show ‹False›
proof (cases ‹q' ∈ Q'›)
case True
thus ‹False› using X ‹hml_srbb_inner.distinguishes_from χ p Q'›
by simp
next
case False
from IH have ‹strategy_formula_inner (Defender_Stable_Conj p Q') e χ› by simp
hence ‹∃Φ. χ=(StableConj Q' Φ)› using strategy_formula_inner.simps
by (smt (verit) spectroscopy_position.distinct(35) spectroscopy_position.distinct(39) spectroscopy_position.distinct(41) spectroscopy_position.inject(7))
then obtain Φ where P: ‹χ=(StableConj Q' Φ)› by auto
from IH(1) have ‹Q' = { q ∈ Q. (∄q'. q ↦τ q')}›
by (metis (full_types) local.late_stbl_conj option.distinct(1))
hence ‹∃q''. q' ↦τ q''› using False ‹q' ∈ Q› by simp
from X have ‹hml_srbb_inner_models q' (StableConj Q' Φ)› using P by auto
then show ?thesis using ‹∃q''. q' ↦τ q''› by simp
qed
qed
thus ‹distinguishes_from (hml_srbb.Internal χ) p Q›
using ‹p ⊨SRBB (hml_srbb.Internal χ)› by simp
qed
then show ?case by simp
next
case (stable_conj Q p e Φ)
hence IH: ‹∀q∈ Q. hml_srbb_conj.distinguishes (Φ q) p q› by simp
hence Q: ‹∀q ∈ Q. hml_srbb_conjunct_models p (Φ q)› by simp
hence ‹(∀q. ¬ p ↦τ q) ⟶ hml_srbb_inner.distinguishes_from (StableConj Q Φ) p Q›
using IH by auto
then show ?case by simp
next
case (branch p Q e χ)
then obtain p' Q' α Qα where IH:
‹spectroscopy_moves (Attacker_Delayed p Q) (Defender_Branch p α p' Q' Qα) = Some Some›
‹attacker_wins e (Defender_Branch p α p' Q' Qα) ∧
strategy_formula_inner (Defender_Branch p α p' Q' Qα) e χ ∧
(case Defender_Branch p α p' Q' Qα of Attacker_Delayed p Q ⇒ Q ↠S Q ⟶ distinguishes_from (Internal χ) p Q
| Defender_Branch p α p' Q Qa ⇒ p ↦a α p' ⟶ hml_srbb_inner.distinguishes_from χ p (Q ∪ Qa)
| Defender_Conj p Q ⇒ hml_srbb_inner.distinguishes_from χ p Q
| Defender_Stable_Conj p Q ⇒ (∀q. ¬ p ↦τ q) ⟶ hml_srbb_inner.distinguishes_from χ p Q | _ ⇒ True)› by blast
from IH(1) have ‹p ↦a α p'›
by (metis local.br_conj option.distinct(1))
from IH have ‹p ↦a α p' ⟶ hml_srbb_inner.distinguishes_from χ p (Q' ∪ Qα)› by simp
hence D: ‹hml_srbb_inner.distinguishes_from χ p (Q' ∪ Qα)› using ‹p ↦a α p'› by auto
from IH have ‹Q' = Q - Qα ∧ p ↦a α p' ∧ Qα ⊆ Q›
by (metis (no_types, lifting) br_conj option.discI)
hence ‹Q=(Q' ∪ Qα)› by auto
then show ?case
using D silent_reachable.refl by auto
next
case (branch_conj p α p' Q1 Qα e ψ Φ)
hence A1: ‹∀q∈Q1. hml_srbb_conjunct_models p (Φ q)› by simp
from branch_conj obtain Q' where IH:
‹spectroscopy_moves (Defender_Branch p α p' Q1 Qα) (Attacker_Branch p' Q')
= Some (λe. Option.bind (subtract_fn 0 1 1 0 0 0 0 0 e) min1_6)›
‹spectroscopy_moves (Attacker_Branch p' Q') (Attacker_Immediate p' Q') = subtract 1 0 0 0 0 0 0 0 ∧
attacker_wins (the (min1_6 (e - E 0 1 1 0 0 0 0 0)) - E 1 0 0 0 0 0 0 0) (Attacker_Immediate p' Q') ∧
strategy_formula (Attacker_Immediate p' Q') (the (min1_6 (e - E 0 1 1 0 0 0 0 0)) - E 1 0 0 0 0 0 0 0) ψ ∧
(case Attacker_Immediate p' Q' of Attacker_Immediate p Q ⇒ distinguishes_from ψ p Q
| Defender_Conj p Q ⇒ distinguishes_from ψ p Q | _ ⇒ True)› by auto
hence ‹distinguishes_from ψ p' Q'› by simp
hence X: ‹p' ⊨SRBB ψ› by simp
have Y: ‹∀q ∈ Q'. ¬(q ⊨SRBB ψ)› using ‹distinguishes_from ψ p' Q'› by simp
have ‹(p ↦a α p') ⟶ hml_srbb_inner.distinguishes_from (BranchConj α ψ Q1 Φ) p (Q1 ∪ Qα)›
proof
assume ‹p ↦a α p'›
hence ‹p ↦a α p'› by simp
with IH(1) have ‹Qα ↦aS α Q'›
by (simp, metis option.discI)
hence A2: ‹hml_srbb_inner_models p (Obs α ψ)› using X ‹p ↦a α p'› by auto
have A3: ‹∀q ∈ (Q1 ∪ Qα). hml_srbb_inner.distinguishes (BranchConj α ψ Q1 Φ) p q›
proof (safe)
fix q
assume ‹q ∈ Q1›
hence ‹hml_srbb_conj.distinguishes (Φ q) p q› using branch_conj(2) by simp
thus ‹hml_srbb_inner.distinguishes (BranchConj α ψ Q1 Φ) p q›
using A1 A2 srbb_dist_conjunct_or_branch_implies_dist_branch_conjunction ‹q ∈ Q1› by blast
next
fix q
assume ‹q ∈ Qα›
hence ‹¬(hml_srbb_inner_models q (Obs α ψ))›
using Y ‹Qα ↦aS α Q'› by auto
hence ‹hml_srbb_inner.distinguishes (Obs α ψ) p q›
using A2 by auto
thus ‹hml_srbb_inner.distinguishes (BranchConj α ψ Q1 Φ) p q›
using A1 A2 srbb_dist_conjunct_or_branch_implies_dist_branch_conjunction by blast
qed
have A4: ‹hml_srbb_inner_models p (BranchConj α ψ Q1 Φ)›
using A3 A2 by fastforce
with A3 show ‹hml_srbb_inner.distinguishes_from (BranchConj α ψ Q1 Φ) p (Q1 ∪ Qα)›
by simp
qed
then show ?case by simp
qed
end
end