Theory Weak_Early_Step_Sim
theory Weak_Early_Step_Sim
imports Weak_Early_Sim Strong_Early_Sim
begin
definition weakStepSimulation :: "pi ⇒ (pi × pi) set ⇒ pi ⇒ bool" (‹_ ↝«_» _› [80, 80, 80] 80) where
"P ↝«Rel» Q ≡ (∀Q' a x. Q ⟼a<νx> ≺ Q' ⟶ x ♯ P ⟶ (∃P' . P ⟹a<νx> ≺ P' ∧ (P', Q') ∈ Rel)) ∧
(∀Q' α. Q ⟼α ≺ Q' ⟶ (∃P'. P ⟹α ≺ P' ∧ (P', Q') ∈ Rel))"
lemma monotonic:
fixes A :: "(pi × pi) set"
and B :: "(pi × pi) set"
and P :: pi
and P' :: pi
assumes "P ↝«A» P'"
and "A ⊆ B"
shows "P ↝«B» P'"
using assms
by(simp add: weakStepSimulation_def) blast
lemma simCasesCont[consumes 1, case_names Bound Free]:
fixes P :: pi
and Q :: pi
and Rel :: "(pi × pi) set"
and C :: "'a::fs_name"
assumes Eqvt: "eqvt Rel"
and Bound: "⋀a x Q'. ⟦x ♯ C; Q ⟼ a<νx> ≺ Q'⟧ ⟹ ∃P'. P ⟹ a<νx> ≺ P' ∧ (P', Q') ∈ Rel"
and Free: "⋀α Q'. Q ⟼ α ≺ Q' ⟹ ∃P'. P ⟹ α ≺ P' ∧ (P', Q') ∈ Rel"
shows "P ↝«Rel» Q"
proof -
from Free show ?thesis
proof(auto simp add: weakStepSimulation_def)
fix Q' a x
assume xFreshP: "(x::name) ♯ P"
assume Trans: "Q ⟼ a<νx> ≺ Q'"
have "∃c::name. c ♯ (P, Q', x, C)" by(blast intro: name_exists_fresh)
then obtain c::name where cFreshP: "c ♯ P" and cFreshQ': "c ♯ Q'" and cFreshC: "c ♯ C"
and cineqx: "c ≠ x"
by(force simp add: fresh_prod)
from Trans cFreshQ' have "Q ⟼ a<νc> ≺ ([(x, c)] ∙ Q')" by(simp add: alphaBoundOutput)
with cFreshC have "∃P'. P ⟹ a<νc> ≺ P' ∧ (P', [(x, c)] ∙ Q') ∈ Rel"
by(rule Bound)
then obtain P' where PTrans: "P ⟹ a<νc> ≺ P'" and P'RelQ': "(P', [(x, c)] ∙ Q') ∈ Rel"
by blast
from PTrans ‹x ♯ P› ‹c ≠ x› have "P ⟹a<νx> ≺ ([(x, c)] ∙ P')"
by(simp add: weakTransitionAlpha name_swap)
moreover from Eqvt P'RelQ' have "([(x, c)] ∙ P', [(x, c)] ∙ [(x, c)] ∙ Q') ∈ Rel"
by(rule eqvtRelI)
with ‹c ≠ x› have "([(x, c)] ∙ P', Q') ∈ Rel"
by simp
ultimately show "∃P'. P ⟹a<νx> ≺ P' ∧ (P', Q') ∈ Rel" by blast
qed
qed
lemma simCases[consumes 0, case_names Bound Free]:
fixes P :: pi
and Q :: pi
and Rel :: "(pi × pi) set"
and C :: "'a::fs_name"
assumes "⋀a x Q'. ⟦Q ⟼ a<νx> ≺ Q'; x ♯ P⟧ ⟹ ∃P'. P ⟹ a<νx> ≺ P' ∧ (P', Q') ∈ Rel"
and "⋀α Q'. Q ⟼ α ≺ Q' ⟹ ∃P'. P ⟹ α ≺ P' ∧ (P', Q') ∈ Rel"
shows "P ↝«Rel» Q"
using assms
by(auto simp add: weakStepSimulation_def)
lemma simE:
fixes P :: pi
and Rel :: "(pi × pi) set"
and Q :: pi
and a :: name
and x :: name
and Q' :: pi
assumes "P ↝«Rel» Q"
shows "Q ⟼a<νx> ≺ Q' ⟹ x ♯ P ⟹ ∃P'. P ⟹a<νx> ≺ P' ∧ (P', Q') ∈ Rel"
and "Q ⟼α ≺ Q' ⟹ ∃P'. P ⟹α ≺ P' ∧ (P', Q') ∈ Rel"
using assms by(simp add: weakStepSimulation_def)+
lemma simE2:
fixes P :: pi
and Rel :: "(pi × pi) set"
and Q :: pi
and a :: name
and x :: name
and Q' :: pi
assumes PSimQ: "P ↝«Rel» Q"
and Sim: "⋀R S. (R, S) ∈ Rel ⟹ R ↝<Rel> S"
and Eqvt: "eqvt Rel"
and PRelQ: "(P, Q) ∈ Rel"
shows "Q ⟹a<νx> ≺ Q' ⟹ x ♯ P ⟹ ∃P'. P ⟹a<νx> ≺ P' ∧ (P', Q') ∈ Rel"
and "Q ⟹α ≺ Q' ⟹ ∃P'. P ⟹α ≺ P' ∧ (P', Q') ∈ Rel"
proof -
assume QTrans: "Q ⟹a<νx> ≺ Q'"
assume "x ♯ P"
from QTrans obtain Q'' Q''' where QChain: "Q ⟹⇩τ Q''"
and Q''Trans: "Q'' ⟼a<νx> ≺ Q'''"
and Q'''Chain: "Q''' ⟹⇩τ Q'"
by(blast dest: transitionE)
from QChain PRelQ Sim have "∃P''. P ⟹⇩τ P'' ∧ (P'', Q'') ∈ Rel"
by(rule weakSimTauChain)
then obtain P'' where PChain: "P ⟹⇩τ P''" and P''RelQ'': "(P'', Q'') ∈ Rel" by blast
from PChain ‹x ♯ P› have xFreshP'': "x ♯ P''" by(rule freshChain)
from P''RelQ'' have "P'' ↝<Rel> Q''" by(rule Sim)
with Q''Trans xFreshP'' obtain P''' where P''Trans: "P'' ⟹a<νx> ≺ P'''"
and P'''RelQ''': "(P''', Q''') ∈ Rel"
by(blast dest: Weak_Early_Sim.simE)
have "∃P'. P''' ⟹⇩τ P' ∧ (P', Q') ∈ Rel" using Q'''Chain P'''RelQ''' Sim
by(rule weakSimTauChain)
then obtain P' where P'''Chain: "P''' ⟹⇩τ P'" and P'RelQ': "(P', Q') ∈ Rel" by blast
from PChain P''Trans P'''Chain have "P ⟹a<νx> ≺ P'"
by(blast dest: Weak_Early_Step_Semantics.chainTransitionAppend)
with P'RelQ' show "∃P'. P ⟹ a<νx> ≺ P' ∧ (P', Q') ∈ Rel"
by blast
next
assume "Q ⟹α ≺ Q'"
then obtain Q'' Q''' where QChain: "Q ⟹⇩τ Q''"
and Q''Trans: "Q'' ⟼α ≺ Q'''"
and Q'''Chain: "Q''' ⟹⇩τ Q'"
by(blast dest: transitionE)
from QChain Q''Trans Q'''Chain show "∃P'. P ⟹α ≺ P' ∧ (P', Q') ∈ Rel"
proof(induct arbitrary: α Q''' Q' rule: tauChainInduct)
case id
from PSimQ ‹Q ⟼α ≺ Q'''› have "∃P'. P ⟹α ≺ P' ∧ (P', Q''') ∈ Rel"
by(blast dest: simE)
then obtain P''' where PTrans: "P ⟹α ≺ P'''" and P'RelQ''': "(P''', Q''') ∈ Rel"
by blast
have "∃P'. P''' ⟹⇩τ P' ∧ (P', Q') ∈ Rel" using ‹Q''' ⟹⇩τ Q'› P'RelQ''' Sim
by(rule Weak_Early_Sim.weakSimTauChain)
then obtain P' where P'''Chain: "P''' ⟹⇩τ P'" and P'RelQ': "(P', Q') ∈ Rel" by blast
from P'''Chain PTrans have "P ⟹α ≺ P'"
by(blast dest: Weak_Early_Step_Semantics.chainTransitionAppend)
with P'RelQ' show ?case by blast
next
case(ih Q'''' Q'' α Q''' Q')
have "Q'' ⟹⇩τ Q''" by simp
with ‹Q'''' ⟼τ ≺ Q''› obtain P'' where PChain: "P ⟹τ ≺ P''" and P''RelQ'': "(P'', Q'') ∈ Rel"
by(drule_tac ih) auto
from P''RelQ'' have "P'' ↝<Rel> Q''" by(rule Sim)
hence "∃P'''. P'' ⟹⇧^α ≺ P''' ∧ (P''', Q''') ∈ Rel" using ‹Q'' ⟼α ≺ Q'''›
by(rule Weak_Early_Sim.simE)
then obtain P''' where P''Trans: "P'' ⟹⇧^α ≺ P'''"
and P'''RelQ''': "(P''', Q''') ∈ Rel"
by blast
from ‹Q''' ⟹⇩τ Q'› P'''RelQ''' Sim have "∃P'. P''' ⟹⇩τ P' ∧ (P', Q') ∈ Rel"
by(rule Weak_Early_Sim.weakSimTauChain)
then obtain P' where P'''Chain: "P''' ⟹⇩τ P'"
and P'RelQ': "(P', Q') ∈ Rel"
by blast
from PChain P''Trans have "P ⟹α ≺ P'''"
apply(auto simp add: freeTransition_def weakFreeTransition_def)
apply(drule tauActTauChain, auto)
by(rule_tac x=P'''aa in exI) auto
hence "P ⟹α ≺ P'" using P'''Chain
by(rule Weak_Early_Step_Semantics.chainTransitionAppend)
with P'RelQ' show ?case by blast
qed
qed
lemma eqvtI:
fixes P :: pi
and Q :: pi
and Rel :: "(pi × pi) set"
and perm :: "name prm"
assumes PSimQ: "P ↝«Rel» Q"
and RelRel': "Rel ⊆ Rel'"
and EqvtRel': "eqvt Rel'"
shows "(perm ∙ P) ↝«Rel'» (perm ∙ Q)"
proof(induct rule: simCases)
case(Bound a x Q')
have xFreshP: "x ♯ perm ∙ P" by fact
have QTrans: "(perm ∙ Q) ⟼ a<νx> ≺ Q'" by fact
hence "(rev perm ∙ (perm ∙ Q)) ⟼ rev perm ∙ (a<νx> ≺ Q')" by(rule eqvt)
hence "Q ⟼ (rev perm ∙ a)<ν(rev perm ∙ x)> ≺ (rev perm ∙ Q')"
by(simp add: name_rev_per)
moreover from xFreshP have "(rev perm ∙ x) ♯ P" by(simp add: name_fresh_left)
ultimately obtain P' where PTrans: "P ⟹ (rev perm ∙ a)<ν(rev perm ∙ x)> ≺ P'"
and P'RelQ': "(P', rev perm ∙ Q') ∈ Rel" using PSimQ
by(blast dest: simE)
from PTrans have "(perm ∙ P) ⟹(perm ∙ rev perm ∙ a)<ν(perm ∙ rev perm ∙ x)> ≺ perm ∙ P'"
by(rule Weak_Early_Step_Semantics.eqvtI)
hence L1: "(perm ∙ P) ⟹ a<νx> ≺ (perm ∙ P')" by(simp add: name_per_rev)
from P'RelQ' RelRel' have "(P', rev perm ∙ Q') ∈ Rel'" by blast
with EqvtRel' have "(perm ∙ P', perm ∙ (rev perm ∙ Q')) ∈ Rel'"
by(rule eqvtRelI)
hence "(perm ∙ P', Q') ∈ Rel'" by(simp add: name_per_rev)
with L1 show ?case by blast
next
case(Free α Q')
have QTrans: "(perm ∙ Q) ⟼ α ≺ Q'" by fact
hence "(rev perm ∙ (perm ∙ Q)) ⟼ rev perm ∙ (α ≺ Q')" by(rule eqvts)
hence "Q ⟼ (rev perm ∙ α) ≺ (rev perm ∙ Q')" by(simp add: name_rev_per)
with PSimQ obtain P' where PTrans: "P ⟹ (rev perm ∙ α) ≺ P'"
and PRel: "(P', (rev perm ∙ Q')) ∈ Rel"
by(blast dest: simE)
from PTrans have "(perm ∙ P) ⟹(perm ∙ rev perm ∙ α) ≺ perm ∙ P'"
by(rule Weak_Early_Step_Semantics.eqvtI)
hence L1: "(perm ∙ P) ⟹ α ≺ (perm ∙ P')" by(simp add: name_per_rev)
from PRel EqvtRel' RelRel' have "((perm ∙ P'), (perm ∙ (rev perm ∙ Q'))) ∈ Rel'"
by(force intro: eqvtRelI)
hence "((perm ∙ P'), Q') ∈ Rel'" by(simp add: name_per_rev)
with L1 show ?case by blast
qed
lemma reflexive:
fixes P :: pi
and Rel :: "(pi × pi) set"
assumes "Id ⊆ Rel"
shows "P ↝«Rel» P"
using assms
by(auto intro: Weak_Early_Step_Semantics.singleActionChain
simp add: weakStepSimulation_def weakFreeTransition_def)
lemma transitive:
fixes P :: pi
and Q :: pi
and R :: pi
and Rel :: "(pi × pi) set"
and Rel' :: "(pi × pi) set"
and Rel'' :: "(pi × pi) set"
assumes PSimQ: "P ↝«Rel» Q"
and QSimR: "Q ↝«Rel'» R"
and Eqvt: "eqvt Rel"
and Eqvt'': "eqvt Rel''"
and Trans: "Rel O Rel' ⊆ Rel''"
and Sim: "⋀S T. (S, T) ∈ Rel ⟹ S ↝<Rel> T"
and PRelQ: "(P, Q) ∈ Rel"
shows "P ↝«Rel''» R"
proof -
from Eqvt'' show ?thesis
proof(induct rule: simCasesCont[of _ "(P, Q)"])
case(Bound a x R')
have "x ♯ (P, Q)" by fact
hence xFreshP: "x ♯ P" and xFreshQ: "x ♯ Q" by(simp add: fresh_prod)+
have RTrans: "R ⟼a<νx> ≺ R'" by fact
from xFreshQ QSimR RTrans obtain Q' where QTrans: "Q ⟹ a<νx> ≺ Q'"
and Q'Rel'R': "(Q', R') ∈ Rel'"
by(blast dest: simE)
with PSimQ Sim Eqvt PRelQ QTrans xFreshP have "∃P'. P ⟹ a<νx> ≺ P' ∧ (P', Q') ∈ Rel"
by(blast intro: simE2)
then obtain P' where PTrans: "P ⟹ a<νx> ≺ P'" and P'RelQ': "(P', Q') ∈ Rel" by blast
moreover from P'RelQ' Q'Rel'R' Trans have "(P', R') ∈ Rel''" by blast
ultimately show ?case by blast
next
case(Free α R')
have RTrans: "R ⟼ α ≺ R'" by fact
with QSimR obtain Q' where QTrans: "Q ⟹ α ≺ Q'" and Q'RelR': "(Q', R') ∈ Rel'"
by(blast dest: simE)
from PSimQ Sim Eqvt PRelQ QTrans have "∃P'. P ⟹ α ≺ P' ∧ (P', Q') ∈ Rel"
by(blast intro: simE2)
then obtain P' where PTrans: "P ⟹ α ≺ P'" and P'RelQ': "(P', Q') ∈ Rel" by blast
from P'RelQ' Q'RelR' Trans have "(P', R') ∈ Rel''" by blast
with PTrans show ?case by blast
qed
qed
lemma strongSimWeakSim:
fixes P :: pi
and Q :: pi
and Rel :: "(pi × pi) set"
assumes PSimQ: "P ↝[Rel] Q"
shows "P ↝«Rel» Q"
proof(induct rule: simCases)
case(Bound a x Q')
have "Q ⟼a<νx> ≺ Q'" and "x ♯ P" by fact+
with PSimQ obtain P' where PTrans: "P ⟼a<νx> ≺ P'" and P'RelQ': "(P', Q') ∈ Rel"
by(blast dest: Strong_Early_Sim.elim)
from PTrans have "P ⟹a<νx> ≺ P'"
by(force intro: Weak_Early_Step_Semantics.singleActionChain simp add: weakFreeTransition_def)
with P'RelQ' show ?case by blast
next
case(Free α Q')
have "Q ⟼α ≺ Q'" by fact
with PSimQ obtain P' where PTrans: "P ⟼α ≺ P'" and P'RelQ': "(P', Q') ∈ Rel"
by(blast dest: Strong_Early_Sim.elim)
from PTrans have "P ⟹α ≺ P'" by(rule Weak_Early_Step_Semantics.singleActionChain)
with P'RelQ' show ?case by blast
qed
lemma weakSimWeakEqSim:
fixes P :: pi
and Q :: pi
and Rel :: "(pi × pi) set"
assumes "P ↝«Rel» Q"
shows "P ↝<Rel> Q"
using assms
by(force simp add: weakStepSimulation_def Weak_Early_Sim.weakSimulation_def weakFreeTransition_def)
end