Theory Weak_HML_Contrasimulation
section ‹Weak HML and the Contrasimulation Set Game›
theory Weak_HML_Contrasimulation
imports
Contrasim_Set_Game
HM_Logic_Infinitary
begin
subsection ‹ Distinguishing Formulas at Winning Attacker Positions›
locale c_game_with_attacker_strategy =
c_set_game trans τ
for
trans :: ‹'s ⇒ 'a ⇒ 's ⇒ bool› and
τ :: ‹'a› +
fixes
strat :: ‹('s, 'a) c_set_game_node posstrategy› and
attacker_winning_region :: ‹('s, 'a) c_set_game_node set› and
attacker_order
defines
‹attacker_order ≡ {(g', g). c_set_game_moves g g' ∧
g ∈ attacker_winning_region ∧ g' ∈ attacker_winning_region ∧
(player1_position g ⟶ g' = strat g)}⇧+›
assumes
finite_win:
‹wf attacker_order› and
strat_stays_winning:
‹g ∈ attacker_winning_region ⟹ player1_position g ⟹
strat g ∈ attacker_winning_region ∧ c_set_game_moves g (strat g)› and
defender_keeps_losing:
‹g ∈ attacker_winning_region ⟹ c_set_game_defender_node g ⟹ c_set_game_moves g g'
⟹ g' ∈ attacker_winning_region›
begin
text ‹This construction of attacker formulas from a game only works if ‹strat› is a well-founded
attacker strategy. (If it's winning and sound, the constructed formula should be distinguishing.)›
function attack_formula :: ‹('s, 'a) c_set_game_node ⇒ ('a,'s) HML_formula› where
‹attack_formula (AttackerNode p Q) =
(if (AttackerNode p Q) ∈ attacker_winning_region
then attack_formula (strat (AttackerNode p Q))
else HML_true)›
| ‹attack_formula (DefenderSimNode a p Q) =
(if (DefenderSimNode a p Q) ∈ attacker_winning_region
then ⟨τ⟩⟨a⟩(attack_formula (AttackerNode p (dsuccs a Q)))
else HML_true)›
| ‹attack_formula (DefenderSwapNode p Q) =
(if Q = {} ∨ DefenderSwapNode p Q ∉ attacker_winning_region
then HML_true
else (HML_weaknor (weak_tau_succs Q)
(λq. if q ∈ (weak_tau_succs Q)
then (attack_formula (AttackerNode q {p}))
else HML_true )))›
using c_set_game_defender_node.cases
by (auto, blast)
termination attack_formula
using finite_win
proof (standard, safe)
fix p Q
assume ‹AttackerNode p Q ∈ attacker_winning_region›
thus ‹(strat (AttackerNode p Q), AttackerNode p Q) ∈ attacker_order›
unfolding attacker_order_def
using strat_stays_winning
by auto
next
fix a p Q
assume attacker_wins: ‹DefenderSimNode a p Q ∈ attacker_winning_region›
hence ‹AttackerNode p (dsuccs a Q) ∈ attacker_winning_region›
using defender_keeps_losing simulation_answer by force
with attacker_wins show
‹(AttackerNode p (dsuccs a Q), DefenderSimNode a p Q) ∈ attacker_order›
unfolding attacker_order_def
by (simp add: r_into_trancl')
next
fix p Q q' q
assume case_assms:
‹q' ∈ weak_tau_succs Q›
‹(AttackerNode q' {p}, DefenderSwapNode p Q) ∉ attacker_order›
‹DefenderSwapNode p Q ∈ attacker_winning_region›
‹q ∈ Q›
hence ‹AttackerNode q' {p} ∉ attacker_winning_region›
unfolding attacker_order_def by auto
moreover from case_assms have ‹AttackerNode q' {p} ∈ attacker_winning_region›
using swap_answer defender_keeps_losing by force
ultimately show ‹q ∈ {}› by blast
qed
lemma attacker_defender_switch:
assumes
‹(AttackerNode p Q) ∈ attacker_winning_region›
shows
‹(∃a p'. (strat (AttackerNode p Q)) = (DefenderSimNode a p' Q) ∧ p =⊳a p' ∧ ¬tau a)
∨(∃p'. (strat (AttackerNode p Q)) = (DefenderSwapNode p' Q) ∧ p ⟼* tau p' )›
using strat_stays_winning[OF assms] by (cases ‹strat (AttackerNode p Q)›, auto)
lemma attack_options:
assumes
‹(AttackerNode p Q) ∈ attacker_winning_region›
shows
‹(∃a p'. p =⊳a p' ∧ ¬tau a ∧ strat (AttackerNode p Q) = (DefenderSimNode a p' Q) ∧
attack_formula (AttackerNode p Q)
= ⟨τ⟩⟨a⟩(attack_formula (AttackerNode p' (dsuccs a Q))))
∨ (∃p'. p ⟼* tau p' ∧ strat (AttackerNode p Q) = (DefenderSwapNode p' Q) ∧
attack_formula (AttackerNode p Q) =
(HML_weaknor (weak_tau_succs Q) (λq.
if q ∈ (weak_tau_succs Q)
then (attack_formula (AttackerNode q {p'}))
else HML_true )))
∨ (Q = {} ∧ attack_formula (AttackerNode p Q) = HML_true)›
proof -
from assms have
‹attack_formula (AttackerNode p Q) = attack_formula (strat (AttackerNode p Q))›
by simp
moreover from attacker_defender_switch assms have
‹(∃a p'. (strat (AttackerNode p Q)) = (DefenderSimNode a p' Q) ∧ p =⊳a p' ∧ ¬tau a)
∨ (∃p'. (strat (AttackerNode p Q)) = (DefenderSwapNode p' Q) ∧ p ⟼* tau p')›
by blast
ultimately have
‹ (∃a p'. (strat (AttackerNode p Q)) = (DefenderSimNode a p' Q) ∧
(attack_formula (AttackerNode p Q))
= attack_formula (DefenderSimNode a p' Q) ∧ p =⊳a p' ∧ ¬tau a)
∨ (∃p'. (strat (AttackerNode p Q)) = (DefenderSwapNode p' Q) ∧
(attack_formula (AttackerNode p Q))
= attack_formula (DefenderSwapNode p' Q) ∧ p ⟼* tau p')›
by metis
moreover from assms have ‹strat (AttackerNode p Q) ∈ attacker_winning_region›
by (simp add: strat_stays_winning)
ultimately show ?thesis using assms empty_iff
by fastforce
qed
lemma distinction_soundness:
fixes p Q p0 Q0
defines
‹pQ == AttackerNode p Q›
defines
‹φ == attack_formula pQ›
assumes
‹pQ ∈ attacker_winning_region›
shows
‹p ⊨ φ ∧ (∀q∈Q. ¬ q ⊨ φ)›
using finite_win assms
proof (induct arbitrary: p Q φ)
case (less p Q)
from attack_options[OF this(2)] show ?case
proof
assume ‹∃a p'. p =⊳ a p' ∧ ¬ tau a ∧
strat (AttackerNode p Q) = DefenderSimNode a p' Q ∧
attack_formula (AttackerNode p Q) = ⟨τ⟩⟨a⟩attack_formula (AttackerNode p' (dsuccs a Q))›
then obtain a p' where case_assms:
‹p =⊳ a p' ∧ ¬ tau a›
‹strat (AttackerNode p Q) = DefenderSimNode a p' Q›
‹attack_formula (AttackerNode p Q)
= ⟨τ⟩⟨a⟩attack_formula (AttackerNode p' (dsuccs a Q))› by blast
hence moves:
‹c_set_game_moves (AttackerNode p Q) (DefenderSimNode a p' Q)›
‹c_set_game_moves (DefenderSimNode a p' Q) (AttackerNode p' (dsuccs a Q))› by auto
with case_assms less(2) defender_keeps_losing strat_stays_winning have all_winning:
‹(AttackerNode p' (dsuccs a Q)) ∈ attacker_winning_region›
‹(DefenderSimNode a p' Q) ∈ attacker_winning_region›
by (metis c_set_game_defender_node.simps(2), force)
with case_assms moves less(2) have
‹(AttackerNode p' (dsuccs a Q), DefenderSimNode a p' Q) ∈ attacker_order›
‹(DefenderSimNode a p' Q, AttackerNode p Q) ∈ attacker_order›
unfolding attacker_order_def by (simp add: r_into_trancl')+
hence ‹(AttackerNode p' (dsuccs a Q), AttackerNode p Q) ∈ attacker_order›
unfolding attacker_order_def by auto
with less.hyps all_winning(1) have
‹p' ⊨ attack_formula (AttackerNode p' (dsuccs a Q)) ∧
(∀q∈(dsuccs a Q). ¬ q ⊨ attack_formula (AttackerNode p' (dsuccs a Q)))›
by blast
with case_assms have
‹p ⊨ ⟨τ⟩⟨a⟩attack_formula (AttackerNode p' (dsuccs a Q))›
‹∀q∈Q. ¬q ⊨ ⟨τ⟩⟨a⟩attack_formula (AttackerNode p' (dsuccs a Q))›
unfolding dsuccs_def by (auto, blast+)
thus ?case unfolding case_assms by blast
next
assume ‹(∃p'. p ⟼* tau p' ∧ strat (AttackerNode p Q) = DefenderSwapNode p' Q ∧
attack_formula (AttackerNode p Q)
= HML_weaknor (weak_tau_succs Q) (λq.
if q ∈ (weak_tau_succs Q)
then attack_formula (AttackerNode q {p'})
else HML_true)) ∨
Q = {} ∧ attack_formula (AttackerNode p Q) = HML_true›
thus ?case
proof
assume ‹∃p'. p ⟼* tau p' ∧ strat (AttackerNode p Q) = DefenderSwapNode p' Q ∧
attack_formula (AttackerNode p Q)
= HML_weaknor (weak_tau_succs Q) (λq.
if q ∈ (weak_tau_succs Q)
then attack_formula (AttackerNode q {p'})
else HML_true)›
then obtain p' where case_assms:
‹p ⟼* tau p'›
‹strat (AttackerNode p Q) = DefenderSwapNode p' Q›
‹attack_formula (AttackerNode p Q)
= HML_weaknor (weak_tau_succs Q) (λq.
if q ∈ (weak_tau_succs Q)
then attack_formula (AttackerNode q {p'})
else HML_true)›
by blast
from case_assms have moves:
‹c_set_game_moves (AttackerNode p Q) (DefenderSwapNode p' Q)›
‹∀q'∈(weak_tau_succs Q).
c_set_game_moves (DefenderSwapNode p' Q) (AttackerNode q' {p'})›
by auto
with case_assms less(2) defender_keeps_losing strat_stays_winning
have all_winning:
‹(DefenderSwapNode p' Q) ∈ attacker_winning_region›
‹∀q'∈(weak_tau_succs Q). (AttackerNode q' {p'}) ∈ attacker_winning_region›
by (metis, metis c_set_game_defender_node.simps(1,3))
with case_assms moves less(2) have
‹∀q'∈ weak_tau_succs Q. (AttackerNode q' {p'}, DefenderSwapNode p' Q) ∈ attacker_order›
‹(DefenderSwapNode p' Q, AttackerNode p Q) ∈ attacker_order›
unfolding attacker_order_def by (simp add: r_into_trancl')+
hence ‹∀q'∈ weak_tau_succs Q. (AttackerNode q' {p'}, AttackerNode p Q) ∈ attacker_order›
unfolding attacker_order_def by auto
with less.hyps all_winning have
‹∀q'∈ weak_tau_succs Q.
q' ⊨ attack_formula (AttackerNode q' {p'}) ∧
¬ p' ⊨ attack_formula (AttackerNode q' {p'})›
by blast
with case_assms have
‹p' ⊨ HML_conj (weak_tau_succs Q)
(λq'. HML_neg (attack_formula (AttackerNode q' {p'})))›
‹∀q'∈ weak_tau_succs Q.
¬ q' ⊨ HML_conj (weak_tau_succs Q)
(λqq'. HML_neg (attack_formula (AttackerNode qq' {p'})))›
by (simp, fastforce)
with case_assms have
‹p ⊨ HML_weaknor (weak_tau_succs Q)
(λq. if q ∈ (weak_tau_succs Q)
then attack_formula (AttackerNode q {p'})
else HML_true)›
‹∀q∈Q. ¬q ⊨ HML_weaknor (weak_tau_succs Q)
(λq. if q ∈ (weak_tau_succs Q)
then attack_formula (AttackerNode q {p'})
else HML_true)›
unfolding weak_tau_succs_def HML_weaknor_def
using conj_only_depends_on_indexset by (auto, force, fastforce)
thus ?case unfolding case_assms by blast
next
assume ‹Q = {} ∧ attack_formula (AttackerNode p Q) = HML_true›
thus ?case by auto
qed
qed
qed
lemma distinction_in_language:
fixes p Q
defines
‹pQ == AttackerNode p Q›
defines
‹φ == attack_formula pQ›
assumes
‹pQ ∈ attacker_winning_region›
shows
‹φ ∈ HML_weak_formulas›
using assms(2,3) unfolding assms(1)
proof (induct arbitrary: φ rule: attack_formula.induct)
case (1 p Q)
then show ?case using strat_stays_winning by auto
next
case (2 a p Q)
then show ?case
by (simp add: HML_weak_formulas.Base HML_weak_formulas.Obs)
next
case (3 p Q)
hence ‹∀q' ∈ weak_tau_succs Q. attack_formula (AttackerNode q' {p}) ∈ HML_weak_formulas›
using weak_tau_succs_def HML_weak_formulas.Base by fastforce
then show ?case
using HML_weak_formulas.Base ‹DefenderSwapNode p Q ∈ attacker_winning_region›
by (auto simp add: HML_weak_formulas.Conj)
qed
end
subsection ‹Attacker Wins on Pairs with Distinguishing Formulas›
locale c_game_with_attacker_formula =
c_set_game trans τ
for
trans :: ‹'s ⇒ 'a ⇒ 's ⇒ bool› and
τ :: ‹'a›
begin
inductive_set attacker_winning_region :: ‹('s, 'a) c_set_game_node set› where
Base: ‹DefenderSwapNode _ {} ∈ attacker_winning_region› |
Atk: ‹(c_set_game_moves (AttackerNode p Q) g' ∧ g' ∈ attacker_winning_region)
⟹ (AttackerNode p Q) ∈ attacker_winning_region› |
Def: ‹c_set_game_defender_node g ⟹
(⋀g'. c_set_game_moves g g' ⟹ g' ∈ attacker_winning_region)
⟹ g ∈ attacker_winning_region›
lemma attacker_wins_if_defender_set_empty:
assumes
‹Q = {}›
shows
‹AttackerNode p Q ∈ attacker_winning_region›
proof -
have atk_move: ‹c_set_game_moves (AttackerNode p Q) (DefenderSwapNode p Q)›
by (simp add: steps.refl)
have ‹DefenderSwapNode p Q ∈ attacker_winning_region›
using assms attacker_winning_region.Base by simp
thus ?thesis using atk_move attacker_winning_region.Atk by blast
qed
lemma attacker_wr_propagation:
assumes
‹AttackerNode p' (dsuccs a Q) ∈ attacker_winning_region›
‹p =⊳a p'›
‹¬tau a›
shows
‹AttackerNode p Q ∈ attacker_winning_region›
proof -
have AtkToSim: ‹c_set_game_moves (AttackerNode p Q) (DefenderSimNode a p' Q)›
using assms(2, 3) by simp
have ‹∀g. c_set_game_moves
(DefenderSimNode a p' Q) g
⟶ (g = AttackerNode p' (dsuccs a Q))›
by (simp add: csg_move_defsimnode_to_atknode)
hence ‹(DefenderSimNode a p' Q) ∈ attacker_winning_region›
using assms(1) attacker_winning_region.Def
by (metis c_set_game_defender_node.simps(2))
thus ?thesis using AtkToSim attacker_winning_region.Atk by blast
qed
lemma distinction_completeness:
assumes
‹φ ∈ HML_weak_formulas›
‹distinguishes_from_set φ p Q›
shows
‹(AttackerNode p Q) ∈ attacker_winning_region›
proof (cases ‹Q = {}›)
case True
then show ?thesis using attacker_wins_if_defender_set_empty by auto
next
case False
then show ?thesis using assms
proof (induct arbitrary: p Q rule: HML_weak_formulas.induct[OF assms(1)])
case Base: 1
have ‹∀q. q ⊨ HML_true› by simp
hence ‹False›
using Base.prems(1, 3) by simp
then show ?case by auto
next
case Obs: (2 φ a)
then obtain p' where p'_def: ‹p =⊳a p' ∧ p' ⊨ φ ›
using tau_a_obs_implies_delay_step[of p a φ] by auto
have ‹∀q. q ∈ Q ⟶ ¬ q ⊨ ⟨τ⟩⟨a⟩φ› using Obs by auto
hence ‹∀q. q ∈ Q ⟶ (∀q'. ¬q =⊳a q' ∨ ¬q' ⊨ φ)›
using delay_step_implies_tau_a_obs by blast
hence ‹∀q'. q' ∈ dsuccs a Q ⟶ ¬ q' ⊨ φ›
unfolding dsuccs_def by blast
hence phi_distinguishing: ‹distinguishes_from_set φ p' (dsuccs a Q)›
using p'_def by simp
thus ?case
proof (cases ‹dsuccs a Q = {}›)
case dsuccs_empty: True
then show ?thesis
proof (cases ‹tau a›)
case True
hence ‹{q1. ∃q∈ Q. q ⟼* tau q1} = {}› using dsuccs_def dsuccs_empty by auto
hence ‹Q = {}› using steps.refl by blast
then show ?thesis using attacker_wins_if_defender_set_empty by auto
next
case False
hence ‹AttackerNode p' (dsuccs a Q) ∈ attacker_winning_region›
using attacker_wins_if_defender_set_empty dsuccs_empty by auto
thus ?thesis using attacker_wr_propagation False p'_def by blast
qed
next
case False
hence wr_pred_atk_node:
‹AttackerNode p' (dsuccs a Q) ∈ attacker_winning_region›
using Obs.hyps phi_distinguishing
by auto
thus ?thesis
proof(cases ‹tau a›)
case True
hence ‹∀p. (p ⊨ ⟨τ⟩⟨a⟩φ) = (p ⊨ φ)›
using delay_step_implies_tau_a_obs p'_def satisfies.simps(4) tau_tau
Obs.hyps(1) weak_backwards_truth
by (meson lts.refl)
hence ‹distinguishes_from_set φ p Q› using Obs.prems by auto
thus ?thesis using Obs.hyps Obs.prems by blast
next
case False
then show ?thesis
using wr_pred_atk_node attacker_wr_propagation p'_def
by blast
qed
qed
next
case Conj: (3 I F)
then obtain p' where ‹p ⇒^τ p'› and p_sat: ‹p' ⊨ HML_conj I (λf. HML_neg (F f))›
unfolding HML_weaknor_def by auto
have ‹⋀q . q ∈ Q ⟹ ¬q ⊨ HML_poss τ (HML_conj I (λf. HML_neg (F f)))›
by (metis Conj.prems(3) HML_weaknor_def distinguishes_from_set.elims(2))
hence ‹⋀q q'. q ∈ Q ⟹ ¬q ⇒^τ q' ∨ ¬q' ⊨ HML_conj I (λf. HML_neg (F f))›
using satisfies.simps(4) tau_tau by blast
hence ‹⋀q'. ¬q' ∈ (weak_tau_succs Q) ∨ ¬q' ⊨ HML_conj I (λf. HML_neg (F f))›
using weak_tau_succs_def by auto
hence Ex: ‹⋀q'. q' ∈ (weak_tau_succs Q) ⟹ (∃i. i ∈ I ∧ q' ⊨ (F i))›
by auto
have atk_move: ‹c_set_game_moves (AttackerNode p Q) (DefenderSwapNode p' Q)›
using ‹p ⇒^τ p'› by auto
have Ex_i:
‹∀q1 P1. c_set_game_moves (DefenderSwapNode p' Q) (AttackerNode q1 P1) ⟶
(∃i. i ∈ I ∧ q1 ⊨ (F i)) ∧ P1 = {p'}›
using Ex by auto
hence ‹∀q1 P1.
c_set_game_moves (DefenderSwapNode p' Q) (AttackerNode q1 P1)
⟶ (∃i. i ∈ I ∧ q1 ⊨ (F i) ∧ (∀p'. p' ∈ P1 ⟶ ¬ p' ⊨ (F i)))›
using p_sat by auto
hence ‹∀q1 P1.
c_set_game_moves (DefenderSwapNode p' Q) (AttackerNode q1 P1)
⟶ (∃i. i ∈ I ∧ distinguishes_from_set (F i) q1 P1)›
unfolding distinguishes_from_set.simps using p_sat by blast
hence all_atk_succs_in_wr:
‹∀q1 P1. c_set_game_moves (DefenderSwapNode p' Q) (AttackerNode q1 P1)
⟶ (AttackerNode q1 P1 ∈ attacker_winning_region)›
using Conj.hyps Ex_i by blast
hence ‹∀g. c_set_game_moves (DefenderSwapNode p' Q) g
⟶ (∃ q1 P1. g = (AttackerNode q1 P1))›
using csg_move_defswapnode_to_atknode by blast
hence ‹∀g. c_set_game_moves (DefenderSwapNode p' Q) g
⟶ g ∈ attacker_winning_region›
using all_atk_succs_in_wr by auto
hence ‹DefenderSwapNode p' Q ∈ attacker_winning_region›
using attacker_winning_region.Def
by (meson c_set_game_defender_node.simps(3))
then show ?case using atk_move attacker_winning_region.Atk by blast
qed
qed
end
end