(* Title: The pi-calculus Author/Maintainer: Jesper Bengtson (jebe.dk), 2012 *) theory Early_Tau_Chain imports Early_Semantics begin abbreviation tauChain :: "pi ⇒ pi ⇒ bool" (‹_ ⟹⇩_{τ}_› [80, 80] 80) where "P ⟹⇩_{τ}P' ≡ (P, P') ∈ {(P, P') | P P'. P ⟼τ ≺ P'}^*" lemma tauActTauChain: fixes P :: pi and P' :: pi assumes "P ⟼τ ≺ P'" shows "P ⟹⇩_{τ}P'" using assms by auto lemma tauChainAddTau[intro]: fixes P :: pi and P' :: pi and P'' :: pi shows "P ⟹⇩_{τ}P' ⟹ P' ⟼τ ≺ P'' ⟹ P ⟹⇩_{τ}P''" and "P ⟼τ ≺ P' ⟹ P' ⟹⇩_{τ}P'' ⟹ P ⟹⇩_{τ}P''" by(auto dest: tauActTauChain) lemma tauChainInduct[consumes 1, case_names id ih]: fixes P :: pi and P' :: pi assumes "P ⟹⇩_{τ}P'" and "F P" and "⋀P'' P'''. ⟦P ⟹⇩_{τ}P''; P'' ⟼τ ≺ P'''; F P''⟧ ⟹ F P'''" shows "F P'" using assms by(drule_tac rtrancl_induct) auto lemma eqvtChainI: fixes P :: pi and P' :: pi and perm :: "name prm" assumes "P ⟹⇩_{τ}P'" shows "(perm ∙ P) ⟹⇩_{τ}(perm ∙ P')" using assms proof(induct rule: tauChainInduct) case id thus ?case by simp next case(ih P'' P''') have "P ⟹⇩_{τ}P''" and "P'' ⟼ τ ≺ P'''" by fact+ hence "(perm ∙ P'') ⟼τ ≺ (perm ∙ P''')" by(drule_tac TransitionsEarly.eqvt) auto moreover have "(perm ∙ P) ⟹⇩_{τ}(perm ∙ P'')" by fact ultimately show ?case by(force dest: tauActTauChain) qed lemma eqvtChainE: fixes perm :: "name prm" and P :: pi and P' :: pi assumes Trans: "(perm ∙ P) ⟹⇩_{τ}(perm ∙ P')" shows "P ⟹⇩_{τ}P'" proof - have "rev perm ∙ (perm ∙ P) = P" by(simp add: pt_rev_pi[OF pt_name_inst, OF at_name_inst]) moreover have "rev perm ∙ (perm ∙ P') = P'" by(simp add: pt_rev_pi[OF pt_name_inst, OF at_name_inst]) ultimately show ?thesis using assms by(drule_tac perm="rev perm" in eqvtChainI, simp) qed lemma eqvtChainEq: fixes P :: pi and P' :: pi and perm :: "name prm" shows "P ⟹⇩_{τ}P' = (perm ∙ P) ⟹⇩_{τ}(perm ∙ P')" by(blast intro: eqvtChainE eqvtChainI) lemma freshChain: fixes P :: pi and P' :: pi and x :: name assumes "P ⟹⇩_{τ}P'" and "x ♯ P" shows "x ♯ P'" using assms proof(induct rule: tauChainInduct) case id thus ?case by simp next case(ih P' P'') have "x ♯ P" and "x ♯ P ⟹ x ♯ P'" by fact+ hence "x ♯ P'" by simp moreover have "P' ⟼ τ ≺ P''" by fact ultimately show ?case by(force intro: freshTransition) qed lemma matchChain: fixes b :: name and P :: pi and P' :: pi assumes "P ⟹⇩_{τ}P'" and "P ≠ P'" shows "[b⌢b]P ⟹⇩_{τ}P'" using assms proof(induct rule: tauChainInduct) case id thus ?case by simp next case(ih P'' P''') have P''TransP''': "P'' ⟼τ ≺ P'''" by fact show "[b⌢b]P ⟹⇩_{τ}P'''" proof(cases "P = P''") assume "P=P''" moreover with P''TransP''' have "[b⌢b]P ⟼τ ≺ P'''" by(force intro: Match) thus "[b⌢b]P ⟹⇩_{τ}P'''" by(rule tauActTauChain) next assume "P ≠ P''" moreover have "P ≠ P'' ⟹ [b⌢b]P ⟹⇩_{τ}P''" by fact ultimately show "[b⌢b]P ⟹⇩_{τ}P'''" using P''TransP''' by(blast) qed qed lemma mismatchChain: fixes a :: name and b :: name and P :: pi and P' :: pi assumes PChain: "P ⟹⇩_{τ}P'" and aineqb: "a ≠ b" and PineqP': "P ≠ P'" shows "[a≠b]P ⟹⇩_{τ}P'" proof - from PChain PineqP' show ?thesis proof(induct rule: tauChainInduct) case id thus ?case by simp next case(ih P'' P''') have P''TransP''': "P'' ⟼τ ≺ P'''" by fact show "[a≠b]P ⟹⇩_{τ}P'''" proof(cases "P = P''") assume "P=P''" moreover with aineqb P''TransP''' have "[a≠b]P ⟼τ ≺ P'''" by(force intro: Mismatch) thus "[a≠b]P ⟹⇩_{τ}P'''" by(rule tauActTauChain) next assume "P ≠ P''" moreover have "P ≠ P'' ⟹ [a≠b]P ⟹⇩_{τ}P''" by fact ultimately show "[a≠b]P ⟹⇩_{τ}P'''" using P''TransP''' by(blast) qed qed qed lemma sum1Chain: fixes P :: pi and P' :: pi and Q :: pi assumes "P ⟹⇩_{τ}P'" and "P ≠ P'" shows "P ⊕ Q ⟹⇩_{τ}P'" using assms proof(induct rule: tauChainInduct) case id thus ?case by simp next case(ih P'' P''') have P''TransP''': "P'' ⟼τ ≺ P'''" by fact show "P ⊕ Q ⟹⇩_{τ}P'''" proof(cases "P = P''") assume "P=P''" moreover with P''TransP''' have "P ⊕ Q ⟼τ ≺ P'''" by(force intro: Sum1) thus "P ⊕ Q ⟹⇩_{τ}P'''" by(force intro: tauActTauChain) next assume "P ≠ P''" moreover have "P ≠ P'' ⟹ P ⊕ Q ⟹⇩_{τ}P''" by fact ultimately show "P ⊕ Q ⟹⇩_{τ}P'''" using P''TransP''' by(force dest: tauActTauChain) qed qed lemma sum2Chain: fixes P :: pi and Q :: pi and Q' :: pi assumes "Q ⟹⇩_{τ}Q'" and "Q ≠ Q'" shows "P ⊕ Q ⟹⇩_{τ}Q'" using assms proof(induct rule: tauChainInduct) case id thus ?case by simp next case(ih Q'' Q''') have Q''TransQ''': "Q'' ⟼τ ≺ Q'''" by fact show "P ⊕ Q ⟹⇩_{τ}Q'''" proof(cases "Q = Q''") assume "Q=Q''" moreover with Q''TransQ''' have "P ⊕ Q ⟼τ ≺ Q'''" by(force intro: Sum2) thus "P ⊕ Q ⟹⇩_{τ}Q'''" by(force intro: tauActTauChain) next assume "Q ≠ Q''" moreover have "Q ≠ Q'' ⟹ P ⊕ Q ⟹⇩_{τ}Q''" by fact ultimately show "P ⊕ Q ⟹⇩_{τ}Q'''" using Q''TransQ''' by blast qed qed lemma Par1Chain: fixes P :: pi and P' :: pi and Q :: pi assumes "P ⟹⇩_{τ}P'" shows "P ∥ Q ⟹⇩_{τ}P' ∥ Q" using assms proof(induct rule: tauChainInduct) case id thus ?case by simp next case(ih P'' P') have P''TransP': "P'' ⟼τ ≺ P'" by fact have IH: "P ∥ Q ⟹⇩_{τ}P'' ∥ Q" by fact have "P'' ∥ Q ⟼τ ≺ P' ∥ Q" using P''TransP' by(force intro: Par1F) thus "P ∥ Q ⟹⇩_{τ}P' ∥ Q" using IH by(force dest: tauActTauChain) qed lemma Par2Chain: fixes P :: pi and Q :: pi and Q' :: pi assumes "Q ⟹⇩_{τ}Q'" shows "P ∥ Q ⟹⇩_{τ}P ∥ Q'" using assms proof(induct rule: tauChainInduct) case id thus ?case by simp next case(ih Q'' Q') have Q''TransQ': "Q'' ⟼τ ≺ Q'" by fact have IH: "P ∥ Q ⟹⇩_{τ}P ∥ Q''" by fact have "P ∥ Q'' ⟼τ ≺ P ∥ Q'" using Q''TransQ' by(force intro: Par2F) thus "P ∥ Q ⟹⇩_{τ}P ∥ Q'" using IH by(force dest: tauActTauChain) qed lemma chainPar: fixes P :: pi and P' :: pi and Q :: pi and Q' :: pi assumes "P ⟹⇩_{τ}P'" and "Q ⟹⇩_{τ}Q'" shows "P ∥ Q ⟹⇩_{τ}P' ∥ Q'" proof - from ‹P ⟹⇩_{τ}P'› have "P ∥ Q ⟹⇩_{τ}P' ∥ Q" by(rule Par1Chain) moreover from ‹Q ⟹⇩_{τ}Q'› have "P' ∥ Q ⟹⇩_{τ}P' ∥ Q'" by(rule Par2Chain) ultimately show ?thesis by auto qed lemma ResChain: fixes P :: pi and P' :: pi and a :: name assumes "P ⟹⇩_{τ}P'" shows "<νa>P ⟹⇩_{τ}<νa>P'" using assms proof(induct rule: tauChainInduct) case id thus ?case by simp next case(ih P'' P''') have "P'' ⟼τ ≺ P'''" by fact hence "<νa>P'' ⟼τ ≺ <νa>P'''" by(force intro: ResF) moreover have "<νa>P ⟹⇩_{τ}<νa>P''" by fact ultimately show ?case by(force dest: tauActTauChain) qed lemma substChain: fixes P :: pi and x :: name and b :: name and P' :: pi assumes PTrans: "P[x::=b] ⟹⇩_{τ}P'" shows "P[x::=b] ⟹⇩_{τ}P'[x::=b]" proof(cases "x=b") assume "x = b" with PTrans show ?thesis by simp next assume "x ≠ b" hence "x ♯ P[x::=b]" by(simp add: fresh_fact2) with PTrans have "x ♯ P'" by(force intro: freshChain) hence "P' = P'[x::=b]" by(simp add: forget) with PTrans show ?thesis by simp qed lemma bangChain: fixes P :: pi and P' :: pi assumes PTrans: "P ∥ !P ⟹⇩_{τ}P'" and P'ineq: "P' ≠ P ∥ !P" shows "!P ⟹⇩_{τ}P'" using assms proof(induct rule: tauChainInduct) case id thus ?case by simp next case(ih P' P'') show ?case proof(cases "P' = P ∥ !P") case True from ‹P' ⟼τ ≺ P''› ‹P' = P ∥ !P› have "!P ⟼τ ≺ P''" by(blast intro: Bang) thus ?thesis by auto next case False from ‹P' ≠ P ∥ !P› have "!P ⟹⇩_{τ}P'" by(rule ih) with ‹P' ⟼τ ≺ P''› show ?thesis by(auto dest: tauActTauChain) qed qed end