Theory Weak_Early_Sim
theory Weak_Early_Sim
imports Weak_Early_Semantics Strong_Early_Sim_Pres
begin
definition weakSimulation :: "pi ⇒ (pi × pi) set ⇒ pi ⇒ bool" ("_ ↝<_> _" [80, 80, 80] 80)
where "P ↝<Rel> Q ≡ (∀a x Q'. 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: weakSimulation_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'. ⟦Q ⟼ a<νx> ≺ Q'; x ♯ P; x ♯ Q; x ≠ a; x ♯ C⟧ ⟹ ∃P'. P ⟹a<νx> ≺ P' ∧ (P', Q') ∈ Rel"
and Free: "⋀α Q'. Q ⟼ α ≺ Q' ⟹ ∃P'. P ⟹⇧^ α ≺ P' ∧ (P', Q') ∈ Rel"
shows "P ↝<Rel> Q"
proof(auto simp add: weakSimulation_def)
fix a x Q'
assume QTrans: "Q ⟼ a<νx> ≺ Q'" and "x ♯ P"
obtain c::name where "c ♯ P" and "c ♯ Q" and "c ≠ a" and "c ♯ Q'" and "c ♯ C" and "c ≠ x"
by(generate_fresh "name") auto
from QTrans ‹c ♯ Q'› have "Q ⟼ a<νc> ≺ ([(x, c)] ∙ Q')" by(simp add: alphaBoundOutput)
then obtain P' where PTrans: "P ⟹a<νc> ≺ P'" and P'RelQ': "(P', [(x, c)] ∙ Q') ∈ Rel"
using ‹c ♯ P› ‹c ♯ Q› ‹c ≠ a› ‹c ♯ C›
by(drule_tac Bound) auto
from PTrans ‹x ♯ P› ‹c ≠ x› have "P ⟹a<νx> ≺ ([(x, c)] ∙ P')"
by(force intro: weakTransitionAlpha simp add: name_swap)
moreover from Eqvt P'RelQ' have "([(x, c)] ∙ P', [(x, c)] ∙ [(x, c)] ∙ Q') ∈ Rel"
by(rule eqvtRelI)
hence "([(x, c)] ∙ P', Q') ∈ Rel" by simp
ultimately show "∃P'. P ⟹a<νx> ≺ P' ∧ (P', Q') ∈ Rel"
by blast
next
fix α Q'
assume "Q ⟼α ≺ Q'"
thus "∃P'. P ⟹⇧^α ≺ P' ∧ (P', Q') ∈ Rel"
by(rule Free)
qed
lemma simCases[case_names Bound Free]:
fixes P :: pi
and Q :: pi
and Rel :: "(pi × pi) set"
and C :: "'a::fs_name"
assumes "⋀Q' a x. ⟦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: weakSimulation_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: weakSimulation_def)+
lemma weakSimTauChain:
fixes P :: pi
and Rel :: "(pi × pi) set"
and Rel' :: "(pi × pi) set"
and Q :: pi
and Q' :: pi
assumes QChain: "Q ⟹⇩τ Q'"
and PRelQ: "(P, Q) ∈ Rel"
and PSimQ: "⋀R S. (R, S) ∈ Rel ⟹ R ↝<Rel> S"
shows "∃P'. P ⟹⇩τ P' ∧ (P', Q') ∈ Rel"
proof -
from QChain show ?thesis
proof(induct rule: tauChainInduct)
case id
moreover have "P ⟹⇩τ P" by simp
ultimately show ?case using PSimQ PRelQ by blast
next
case(ih Q' Q'')
have "∃P'. P ⟹⇩τ P' ∧ (P', Q') ∈ Rel" by fact
then obtain P' where PChain: "P ⟹⇩τ P'" and P'Rel'Q': "(P', Q') ∈ Rel" by blast
from P'Rel'Q' have "P' ↝<Rel> Q'" by(rule PSimQ)
moreover have Q'Trans: "Q' ⟼τ ≺ Q''" by fact
ultimately obtain P'' where P'Trans: "P' ⟹⇧^τ ≺ P''" and P''RelQ'': "(P'', Q'') ∈ Rel"
by(blast dest: simE)
from P'Trans have "P' ⟹⇩τ P''" by simp
with PChain have "P ⟹⇩τ P''" by auto
with P''RelQ'' show ?case by blast
qed
qed
lemma simE2:
fixes P :: pi
and Rel :: "(pi × pi) set"
and Q :: pi
and a :: name
and x :: name
and Q' :: pi
assumes 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'" and "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 obtain P''' where PChain: "P ⟹⇩τ P'''" and P'''RelQ''': "(P''', Q''') ∈ Rel"
by(blast dest: weakSimTauChain)
from PChain ‹x ♯ P› have "x ♯ P'''" by(rule freshChain)
from P'''RelQ''' have "P''' ↝<Rel> Q'''" by(rule Sim)
with Q'''Trans ‹x ♯ P'''› obtain P'' where P'''Trans: "P''' ⟹a<νx> ≺ P''"
and P''RelQ'': "(P'', Q'') ∈ Rel"
by(blast dest: simE)
from Q''Chain P''RelQ'' Sim obtain P' where P''Chain: "P'' ⟹⇩τ P'" and P'RelQ': "(P', Q') ∈ Rel"
by(blast dest: weakSimTauChain)
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'"
thus "∃P'. P ⟹⇧^α ≺ P' ∧ (P', Q') ∈ Rel"
proof(induct rule: transitionCases)
case Step
have "Q ⟹α ≺ Q'" by fact
then obtain Q'' Q''' where QChain: "Q ⟹⇩τ Q''"
and Q''Trans: "Q'' ⟼α ≺ 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 P''RelQ'' have "P'' ↝<Rel> Q''" by(rule Sim)
with Q''Trans obtain P''' where P''Trans: "P'' ⟹⇧^α ≺ P'''"
and P'''RelQ''': "(P''', Q''') ∈ Rel"
by(blast dest: 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 ⟹⇧^α ≺ P'"
by(blast dest: chainTransitionAppend)
with P'RelQ' show ?case by blast
next
case Stay
have "P ⟹⇧^τ ≺ P" by simp
thus ?case using PRelQ 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 Q' a x)
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 eqvts)
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 eqvts)
hence "(perm ∙ P) ⟹a<νx> ≺ (perm ∙ P')" by(simp add: name_per_rev)
moreover 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)
ultimately 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_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: weakSimulation_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 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[where C=Q])
case(Bound a x R')
have RTrans: "R ⟼a<νx> ≺ R'" by fact
from ‹x ♯ Q› QSimR RTrans obtain Q' where QTrans: "Q ⟹a<νx> ≺ Q'"
and Q'Rel'R': "(Q', R') ∈ Rel'"
by(blast dest: simE)
from Sim Eqvt PRelQ QTrans ‹x ♯ P›
obtain P' where PTrans: "P ⟹a<νx> ≺ P'" and P'RelQ': "(P', Q') ∈ Rel"
by(drule_tac simE2) auto
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 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 strongAppend:
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 Trans: "Rel O Rel' ⊆ Rel''"
shows "P ↝<Rel''> R"
proof -
from Eqvt'' show ?thesis
proof(induct rule: simCasesCont[where C=Q])
case(Bound a x R')
have RTrans: "R ⟼a<νx> ≺ R'" by fact
from QSimR RTrans ‹x ♯ Q› obtain Q' where QTrans: "Q ⟼a<νx> ≺ Q'"
and Q'Rel'R': "(Q', R') ∈ Rel'"
by(blast dest: Strong_Early_Sim.elim)
with PSimQ QTrans ‹x ♯ P› obtain P' where PTrans: "P ⟹a<νx> ≺ P'" and P'RelQ': "(P', Q') ∈ Rel"
by(blast dest: simE)
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: Strong_Early_Sim.elim)
from PSimQ QTrans obtain P' where PTrans: "P ⟹⇧^ α ≺ P'" and P'RelQ': "(P', Q') ∈ Rel"
by(blast dest: simE)
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 Q' a x)
have "Q ⟼a<νx> ≺ Q'" by fact
with PSimQ ‹x ♯ P› 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_Semantics.singleActionChain)
with P'RelQ' show ?case by blast
qed
end