(* Title: The pi-calculus Author/Maintainer: Jesper Bengtson (jebe.dk), 2012 *) 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 (*****************Reflexivity and transitivity*********************) 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 (* by(blast dest: simE2)*) 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