Theory Strategy_Formulas
subsection ‹Strategy Formulas›
theory Strategy_Formulas
imports Spectroscopy_Game Expressiveness_Price
begin
text ‹
Strategy formulas express attacker strategies in HML. They bridge between HML formulas, the spectroscopy game and winning budgets. We show that, if some energy ‹e› suffices for the attacker to win, there exists a strategy formula with expressiveness price ‹≤ e›. We also prove that this formula actually distinguishes the processes of the attacker position.
›
context lts_tau
begin
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') = id_up
∧ spectro_att_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) = id_up
∧ spectro_att_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)
∧ spectro_att_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)
∧ spectro_att_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)
= id_up ∧ (spectro_att_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_Conjunct p q)
= (subtract 0 0 1 0 0 0 0 0)
∧ (spectro_att_wins (e - (E 0 0 1 0 0 0 0 0)) (Attacker_Conjunct p q))
∧ strategy_formula_conjunct (Attacker_Conjunct 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_Conjunct p q)
= (subtract 0 0 1 0 0 0 0 0)
∧ (spectro_att_wins (e - (E 0 0 1 0 0 0 0 0)) (Attacker_Conjunct p q))
∧ strategy_formula_conjunct (Attacker_Conjunct p q) (e - E 0 0 1 0 0 0 0 0) (Φ q)›
|
pos: ‹strategy_formula_conjunct (Attacker_Conjunct p q) e (Pos χ)›
if ‹(∃Q'. spectroscopy_moves (Attacker_Conjunct p q) (Attacker_Delayed p Q')
= Some min1_6 ∧ spectro_att_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_Conjunct p q) e (Neg χ)›
if ‹∃P'. (spectroscopy_moves (Attacker_Conjunct p q) (Attacker_Delayed q P')
= Some (λe. Option.bind ((subtract_fn 0 0 0 0 0 0 0 1) e) min1_7)
∧ spectro_att_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')
= id_up ∧ spectro_att_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_Conjunct p q)
= (subtract 0 0 0 1 0 0 0 0)
∧ spectro_att_wins (e - (E 0 0 0 1 0 0 0 0)) (Attacker_Conjunct p q)
∧ strategy_formula_conjunct (Attacker_Conjunct 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α) = id_up
∧ spectro_att_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
∧ (spectro_att_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_Conjunct p q)
= (subtract 0 1 1 0 0 0 0 0)
∧ spectro_att_wins (e - (E 0 1 1 0 0 0 0 0)) (Attacker_Conjunct p q)
∧ strategy_formula_conjunct (Attacker_Conjunct p q) (e - E 0 1 1 0 0 0 0 0) (Φ q)›
lemma winning_budget_implies_strategy_formula:
assumes
‹spectro_att_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_Conjunct 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: weak_spectroscopy_game.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 (weak_spectroscopy_game.weight g g' e)) φ
∧ expr_pr_inner φ ≤ weak_spectroscopy_game.updated g g' e) ∧
(∃p Q. g' = Attacker_Delayed p Q) ⟶
(∃φ. strategy_formula_inner g' (the (weak_spectroscopy_game.weight g g' e)) φ
∧ expr_pr_inner φ ≤ weak_spectroscopy_game.updated g g' e)›
using weak_spectroscopy_game.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 ‹(spectro_att_wins e (Attacker_Delayed p Q'))›
using ‹g' = Attacker_Delayed p' Q'› ‹p' = p› Attacker_Immediate
weak_spectroscopy_game.win_a_upwards_closure e_comp
by simp
ultimately have ‹(∃χ.
strategy_formula_inner g'
(the (weak_spectroscopy_game.weight (Attacker_Immediate p Q) g' e)) χ ∧
expr_pr_inner χ ≤ weak_spectroscopy_game.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› e_comp g'_att_del by auto
hence ‹∃Q'. spectroscopy_moves (Attacker_Immediate p Q) (Attacker_Delayed p Q') = id_up
∧ (spectro_att_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
‹spectro_att_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 M':
‹weak_spectroscopy_game.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 M'': ‹(spectro_att_wins (e - (E 0 0 0 0 1 0 0 0)) (Defender_Conj p Q'))›
using g'_def_conj Qp' Attacker_Immediate weak_spectroscopy_game.win_a_upwards_closure
by force
with g'_def_conj have IH_case: ‹∃χ.
strategy_formula_inner g'
(weak_spectroscopy_game.updated (Attacker_Immediate p Q) g' e) χ
∧ expr_pr_inner χ ≤ weak_spectroscopy_game.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 ‹spectro_att_wins (e - (E 0 0 0 0 1 0 0 0)) (Defender_Conj p Q')› IH_case
Qp' M' 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
g'_def_conj Attacker_Immediate
unfolding Qp'
by (smt (verit) spectroscopy_moves.simps(64,70) spectroscopy_position.distinct(17)
spectroscopy_position.inject(5) strategy_formula_inner.cases)
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
Qp' Attacker_Immediate unfolding g'_def_conj
by (smt (verit) lts_tau.spectroscopy_moves.simps(70) hml_srbb_inner.inject(2)
spectroscopy_position.distinct(17,37) strategy_formula_inner.cases)
hence SI: ‹strategy_formula (Attacker_Immediate p Q) e (ImmConj Q ψ)›
using delay early_conj Qp'
by (metis (no_types, lifting) M'' 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 (induct g', auto) (metis option.discI)+
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' (weak_spectroscopy_game.updated (Attacker_Branch p Q) g' e) φ ∧
expressiveness_price φ ≤ weak_spectroscopy_game.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_Conjunct 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_Conjunct by presburger
hence post_win:
‹(the (spectroscopy_moves (Attacker_Conjunct p q) g') e) = min1_6 e›
‹(spectro_att_wins (the (min1_6 e)) (Attacker_Delayed p Q'))›
using ‹{q} ↠S Q'› Attacker_Conjunct weak_spectroscopy_game.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_Conjunct Attack True post_win unfolding g'_att_del
by (smt (verit) option.sel spectroscopy_position.simps(51))
hence
‹spectroscopy_moves (Attacker_Conjunct p q) (Attacker_Delayed p Q') = Some min1_6›
‹spectro_att_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_Conjunct 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_Conjunct unfolding g'_att_del
by presburger+
hence move: ‹spectroscopy_moves (Attacker_Conjunct 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:
‹spectro_att_wins (the (min1_7 (e - E 0 0 0 0 0 0 0 1))) (Attacker_Delayed p' Q')›
using Attacker_Conjunct 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_Conjunct move unfolding g'_att_del
by (smt (verit, del_insts) bind.bind_lunit bind_eq_None_conv option.discI
option.sel spectroscopy_position.simps(51))
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_Conjunct 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_Conjunct 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 (cases g', auto)
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: ‹(spectro_att_wins e (Attacker_Delayed p' Q'))›
using g'_att_del Qp' Attacker_Delayed weak_spectroscopy_game.attacker_wins.Defense e_comp
by (metis option.sel)
have ‹(weak_spectroscopy_game.updated (Attacker_Delayed p Q) g' e) = e›
using g'_att_del Attacker_Delayed e_comp by fastforce
then obtain χ where χ_spec:
‹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) = id_up
∧ spectro_att_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 procrastination by blast
moreover have ‹expr_pr_inner χ ≤ e›
using χ_spec 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:
‹weak_spectroscopy_game.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 ‹spectro_att_wins (e - (E 1 0 0 0 0 0 0 0)) (Attacker_Immediate p' Q')›
using weak_spectroscopy_game.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
‹spectro_att_wins e (Defender_Conj p' Q')›
‹weak_spectroscopy_game.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') = id_up
∧ spectro_att_wins e (Defender_Conj p' Q')
∧ strategy_formula_inner (Defender_Conj p' Q') e χ›
by (simp add: ‹Q = Q'› ‹spectro_att_wins e (Defender_Conj p' Q')› ‹p = p'›)
then show ?thesis
using χ_prop ‹Q = Q'› ‹spectro_att_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 ‹spectro_att_wins e (Defender_Stable_Conj p' Q')›
‹weak_spectroscopy_game.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') = id_up
∧ spectro_att_wins e (Defender_Stable_Conj p' Q')
∧ strategy_formula_inner (Defender_Stable_Conj p' Q') e χ›
using Attack χ_prop ‹spectro_att_wins e (Defender_Stable_Conj p' Q')› late_stbl_conj
pQ' 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 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:
‹spectro_att_wins e (Defender_Branch p' α p'' Q' Qα)›
‹weak_spectroscopy_game.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α) = id_up
∧ spectro_att_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
qed force+
next
case (Defense g e)
thus ?case
proof (induct g)
case (Defender_Branch p α p' Q Qa)
hence conjs:
‹∀q∈ Q. spectroscopy_moves (Defender_Branch p α p' Q Qa) (Attacker_Conjunct p q)
= subtract 0 1 1 0 0 0 0 0›
by simp
obtain e' where e'_spec:
‹∀q∈Q. weak_spectroscopy_game.weight (Defender_Branch p α p' Q Qa)
(Attacker_Conjunct p q) e = Some e'
∧ spectro_att_wins e' (Attacker_Conjunct p q)
∧ (∃ψ. strategy_formula_conjunct (Attacker_Conjunct 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_Conjunct 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(53))
then obtain φ where
‹strategy_formula (Attacker_Immediate p' (soft_step_set Qa α))
(weak_spectroscopy_game.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 φ
≤ weak_spectroscopy_game.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(53))
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)›
‹spectro_att_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›
‹spectro_att_wins (weak_spectroscopy_game.updated
(Attacker_Branch p' (soft_step_set Qa α)) g'' (the (min1_6 (e - E 0 1 1 0 0 0 0 0))))
g''›
using weak_spectroscopy_game.attacker_wins.cases
by (metis spectroscopy_defender.simps(2) option.sel)
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 (cases g'', auto) (metis option.discI)+
then obtain e''' where win_immediate:
‹Some e''' = subtract_fn 1 0 0 0 0 0 0 0 e''›
‹spectro_att_wins e''' (Attacker_Immediate p' (soft_step_set Qa α))›
using g''_spec win_branch option.distinct(1) option.sel spectroscopy_defender.elims(1)
spectroscopy_defender.simps(2)
weak_spectroscopy_game.attacker_wins.cases[OF win_branch(2)]
by (smt (verit, del_insts) local.br_acct spectroscopy_moves.simps(23,53,57,61,66,72))
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 e'_def obs Defender_Branch(2) win_branch(1) win_immediate(1)
by (smt (verit, best) bind_eq_None_conv 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'. weak_spectroscopy_game.weight (Defender_Conj p Q) g' e = Some e'
∧ spectro_att_wins e' g')
∧ (∃q. g' = (Attacker_Conjunct p q))›
using local.conj_answer
lts_tau.spectroscopy_defender.elims spectroscopy_moves.simps(30,33,34,47,58,62)
by (smt (verit, best))
show ?case
proof (cases ‹Q = {}›)
case True
then obtain Φ where ‹∀q ∈ Q.
spectroscopy_moves (Defender_Conj p Q) (Attacker_Conjunct p q)
= subtract 0 0 1 0 0 0 0 0
∧ spectro_att_wins (e - (E 0 0 1 0 0 0 0 0)) (Attacker_Conjunct p q)
∧ strategy_formula_conjunct (Attacker_Conjunct 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 ‹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_Conjunct p q)
= subtract 0 0 1 0 0 0 0 0
∧ spectro_att_wins e' (Attacker_Conjunct 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_Conjunct p q)
= subtract 0 0 1 0 0 0 0 0
∧ Some e' = subtract_fn 0 0 1 0 0 0 0 0 e
∧ spectro_att_wins e' (Attacker_Conjunct p q)
∧ (∃φ. strategy_formula_conjunct (Attacker_Conjunct 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_Conjunct p q)
= subtract 0 0 1 0 0 0 0 0›
‹spectro_att_wins e' (Attacker_Conjunct p q)›
using fa_q by blast
hence ‹weak_spectroscopy_game.weight (Defender_Conj p Q) (Attacker_Conjunct p q) e
= Some e'›
by simp
then have ‹∃ψ. strategy_formula_conjunct (Attacker_Conjunct 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_Conjunct p q)
= subtract 0 0 1 0 0 0 0 0
∧ Some e' = subtract_fn 0 0 1 0 0 0 0 0 e
∧ spectro_att_wins e' (Attacker_Conjunct p q)
∧ (∃φ. strategy_formula_conjunct (Attacker_Conjunct p q) e' φ
∧ expr_pr_conjunct φ ≤ e')›
using e'_spec by blast
qed
hence ‹∃Φ. ∀q ∈ Q.
spectro_att_wins (e - E 0 0 1 0 0 0 0 0) (Attacker_Conjunct p q)
∧ (strategy_formula_conjunct (Attacker_Conjunct 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. spectro_att_wins (e - E 0 0 1 0 0 0 0 0) (Attacker_Conjunct p q)
∧ (strategy_formula_conjunct (Attacker_Conjunct 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'. weak_spectroscopy_game.weight (Defender_Stable_Conj p Q) g' e = Some e'
∧ spectro_att_wins e' g')
∧ ((∃p' q. g' = Attacker_Conjunct p' q) ∨ (∃p' Q'. g' = Defender_Conj p' Q'))›
by (metis (no_types, opaque_lifting)
spectroscopy_defender.elims(2,3) spectroscopy_moves.simps(35,36,37,38,74))
show ?case
proof(cases ‹Q = {}›)
case True
then obtain e' where e'_spec:
‹weak_spectroscopy_game.weight (Defender_Stable_Conj p Q) (Defender_Conj p Q) e
= Some e'›
‹e' = e - (E 0 0 0 1 0 0 0 0)›
‹spectro_att_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. weak_spectroscopy_game.weight (Defender_Stable_Conj p Q)
(Attacker_Conjunct p q) e = Some e'
∧ spectro_att_wins e' (Attacker_Conjunct 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_Conjunct 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_Conjunct p q) e' (Φ q) ∧
expr_pr_conjunct (Φ q) ≤ e'›
by meson
then obtain Φ where Φ_prop: ‹∀q ∈ Q.
strategy_formula_conjunct (Attacker_Conjunct 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 force+
qed
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_Conjunct 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)
next
case (procrastination p Q e χ)
from this obtain p' where IH:
‹spectroscopy_moves (Attacker_Delayed p Q) (Attacker_Delayed p' Q) = id_up ∧
spectro_att_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) 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 ∧
spectro_att_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 α φ))))›
by (simp, meson D ‹Q ↦aS α Q'› distinguishes_from_def)
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_Conjunct p q) (Attacker_Delayed q P')
= Some (λe. Option.bind (subtract_fn 0 0 0 0 0 0 0 1 e) min1_7)›
‹spectro_att_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') = id_up›
‹spectro_att_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_defender.simps(4,7)
spectroscopy_position.distinct(37,41) spectroscopy_position.inject(6))
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α) = id_up›
‹spectro_att_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 ∧
spectro_att_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 ‹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