Theory Strong_Early_Sim
theory Strong_Early_Sim
imports Early_Semantics Rel
begin
definition "strongSimEarly" :: "pi ⇒ (pi × pi) set ⇒ pi ⇒ bool" (‹_ ↝[_] _› [80, 80, 80] 80) where
"P ↝[Rel] Q ≡ (∀a y Q'. Q ⟼a<νy> ≺ Q' ⟶ y ♯ P ⟶ (∃P'. P ⟼a<νy> ≺ 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(fastforce simp add: strongSimEarly_def)
lemma freshUnit[simp]:
fixes y :: name
shows "y ♯ ()"
by(auto simp add: fresh_def supp_unit)
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 y Q'. ⟦Q ⟼ a<νy> ≺ Q'; y ♯ P; y ♯ Q; y ♯ C⟧ ⟹ ∃P'. P ⟼ a<νy> ≺ 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: strongSimEarly_def)
fix Q' a y
assume yFreshP: "(y::name) ♯ P"
assume Trans: "Q ⟼ a<νy> ≺ Q'"
have "∃c::name. c ♯ (P, Q', y, Q, C)" by(blast intro: name_exists_fresh)
then obtain c::name where cFreshP: "c ♯ P" and cFreshQ': "c ♯ Q'" and cFreshC: "c ♯ C"
and cineqy: "c ≠ y" and "c ♯ Q"
by(force simp add: fresh_prod name_fresh)
from Trans cFreshQ' have "Q ⟼ a<νc> ≺ ([(y, c)] ∙ Q')" by(simp add: alphaBoundOutput)
hence "∃P'. P ⟼ a<νc> ≺ P' ∧ (P', [(y, c)] ∙ Q') ∈ Rel" using ‹c ♯ P› ‹c ♯ Q› ‹c ♯ C›
by(rule Bound)
then obtain P' where PTrans: "P ⟼ a<νc> ≺ P'" and P'RelQ': "(P', [(y, c)] ∙ Q') ∈ Rel"
by blast
from PTrans yFreshP cineqy have yFreshP': "y ♯ P'" by(force intro: freshTransition)
with PTrans have "P ⟼ a<νy> ≺ ([(y, c)] ∙ P')" by(simp add: alphaBoundOutput name_swap)
moreover have "([(y, c)] ∙ P', Q') ∈ Rel" (is "?goal")
proof -
from Eqvt P'RelQ' have "([(y, c)] ∙ P', [(y, c)] ∙ [(y, c)] ∙ Q') ∈ Rel"
by(rule eqvtRelI)
with cineqy show ?goal by(simp add: name_calc)
qed
ultimately show "∃P'. P ⟼a<νy> ≺ 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 Bound: "⋀a y Q'. ⟦Q ⟼ a<νy> ≺ Q'; y ♯ P⟧ ⟹ ∃P'. P ⟼ a<νy> ≺ P' ∧ (P', Q') ∈ Rel"
and Free: "⋀α Q'. Q ⟼ α ≺ Q' ⟹ ∃P'. P ⟼ α ≺ P' ∧ (P', Q') ∈ Rel"
shows "P ↝[Rel] Q"
using assms
by(auto simp add: strongSimEarly_def)
lemma elim:
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: strongSimEarly_def)+
lemma eqvtI:
fixes P :: pi
and Q :: pi
and Rel :: "(pi × pi) set"
and perm :: "name prm"
assumes Sim: "P ↝[Rel] Q"
and RelRel': "Rel ⊆ Rel'"
and EqvtRel': "eqvt Rel'"
shows "(perm ∙ P) ↝[Rel'] (perm ∙ Q)"
proof(induct rule: simCases)
case(Bound a y Q')
have Trans: "(perm ∙ Q) ⟼ a<νy> ≺ Q'" by fact
have yFreshP: "y ♯ perm ∙ P" by fact
from Trans have "(rev perm ∙ (perm ∙ Q)) ⟼ rev perm ∙ (a<νy> ≺ Q')"
by(rule TransitionsEarly.eqvt)
hence "Q ⟼ (rev perm ∙ a)<ν(rev perm ∙ y)> ≺ (rev perm ∙ Q')"
by(simp add: name_rev_per)
moreover from yFreshP have "(rev perm ∙ y) ♯ P" by(simp add: name_fresh_left)
ultimately have "∃P'. P ⟼ (rev perm ∙ a)<ν(rev perm ∙ y)> ≺ P' ∧ (P', rev perm ∙ Q') ∈ Rel" using Sim
by(force intro: elim)
then obtain P' where PTrans: "P ⟼ (rev perm ∙ a)<ν(rev perm ∙ y)> ≺ P'" and P'RelQ': "(P', rev perm ∙ Q') ∈ Rel"
by blast
from PTrans have "(perm ∙ P) ⟼ perm ∙ ((rev perm ∙ a)<ν(rev perm ∙ y)> ≺ P')" by(rule TransitionsEarly.eqvt)
hence L1: "(perm ∙ P) ⟼ a<νy> ≺ (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 Trans: "(perm ∙ Q) ⟼ α ≺ Q'" by fact
from Trans have "(rev perm ∙ (perm ∙ Q)) ⟼ rev perm ∙ (α ≺ Q')"
by(rule TransitionsEarly.eqvt)
hence "Q ⟼ (rev perm ∙ α) ≺ (rev perm ∙ Q')"
by(simp add: name_rev_per)
with Sim have "∃P'. P ⟼ (rev perm ∙ α) ≺ P' ∧ (P', (rev perm ∙ Q')) ∈ Rel"
by(force intro: elim)
then obtain P' where PTrans: "P ⟼ (rev perm ∙ α) ≺ P'" and PRel: "(P', (rev perm ∙ Q')) ∈ Rel" by blast
from PTrans have "(perm ∙ P) ⟼ perm ∙ ((rev perm ∙ α)≺ P')" by(rule TransitionsEarly.eqvt)
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 simp add: strongSimEarly_def)
lemmas fresh_prod[simp]
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 Trans: "Rel O Rel' ⊆ Rel''"
shows "P ↝[Rel''] R"
proof -
from Eqvt' show ?thesis
proof(induct rule: simCasesCont[where C=Q])
case(Bound a y R')
have RTrans: "R ⟼ a<νy> ≺ R'" by fact
from QSimR RTrans ‹y ♯ Q› have "∃Q'. Q ⟼ a<νy> ≺ Q' ∧ (Q', R') ∈ Rel'"
by(rule elim)
then obtain Q' where QTrans: "Q ⟼ a<νy> ≺ Q'" and Q'Rel'R': "(Q', R') ∈ Rel'" by blast
from PSimQ QTrans ‹y ♯ P› have "∃P'. P ⟼ a<νy> ≺ P' ∧ (P', Q') ∈ Rel"
by(rule elim)
then obtain P' where PTrans: "P ⟼ a<νy> ≺ 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 have "∃Q'. Q ⟼ α ≺ Q' ∧ (Q', R') ∈ Rel'" by(rule elim)
then obtain Q' where QTrans: "Q ⟼ α ≺ Q'" and Q'RelR': "(Q', R') ∈ Rel'" by blast
from PSimQ QTrans have "∃P'. P ⟼ α ≺ P' ∧ (P', Q') ∈ Rel" by(rule elim)
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 "∃P'. P ⟼ α ≺ P' ∧ (P', R') ∈ Rel''" by blast
qed
qed
end