(* Title: The pi-calculus Author/Maintainer: Jesper Bengtson (jebe.dk), 2012 *) theory Strong_Late_Axiomatisation imports Strong_Late_Expansion_Law begin lemma inputSuppPres: fixes P :: pi and Q :: pi and x :: name and Rel :: "(pi × pi) set" assumes PRelQ: "⋀y. y ∈ supp(P, Q, x) ⟹ (P[x::=y], Q[x::=y]) ∈ Rel" and Eqvt: "eqvt Rel" shows "a<x>.P ↝[Rel] a<x>.Q" proof - from Eqvt show ?thesis proof(induct rule: simCasesCont[where C="(x, a, Q, P)"]) case(Bound b y Q') have "x ∈ supp(P, Q, x)" by(simp add: supp_prod supp_atm) with PRelQ have "(P, Q) ∈ Rel" by fastforce have QTrans: "a<x>.Q ⟼ b«y» ≺ Q'" by fact have "y ♯ (x, a, Q, P)" by fact hence "y ≠ a" and yineqx: "y ≠ x" and "y ♯ Q" and "y ♯ P" by(simp add: fresh_prod)+ with QTrans show ?case proof(induct rule: inputCases) have "a<y>.([(x, y)] ∙ P) ⟼a<y> ≺ ([(x, y)] ∙ P)" by(rule Input) hence "a<x>.P ⟼a<y> ≺ ([(x, y)] ∙ P)" using ‹y ♯ P› by(simp add: alphaInput) moreover have "derivative ([(x, y)] ∙ P) ([(x, y)] ∙ Q) (InputS a) y Rel" proof(auto simp add: derivative_def) fix u have "x ∈ supp(P, Q, x)" by(simp add: supp_prod supp_atm) have "(P[x::=u], Q[x::=u]) ∈ Rel" proof(cases "u ∈ supp(P, Q, x)") case True with PRelQ show ?thesis by auto next case False hence "u ♯ P" and "u ♯ Q" by(auto simp add: fresh_def supp_prod) moreover from ‹eqvt Rel› ‹(P, Q) ∈ Rel› have "([(x, u)] ∙ P, [(x, u)] ∙ Q) ∈ Rel" by(rule eqvtRelI) ultimately show ?thesis by(simp only: injPermSubst) qed with ‹y ♯ P› ‹y ♯ Q› show "(([(x, y)] ∙ P)[y::=u], ([(x, y)] ∙ Q)[y::=u]) ∈ Rel" by(simp add: renaming) qed ultimately show "∃P'. a<x>.P ⟼ a<y> ≺ P' ∧ derivative P' ([(x, y)] ∙ Q) (InputS a) y Rel" by blast qed next case(Free α Q') have "a<x>.Q ⟼ α ≺ Q'" by fact hence False by auto thus ?case by blast qed qed lemma inputSuppPresBisim: fixes P :: pi and Q :: pi and x :: name assumes PSimQ: "⋀y. y ∈ supp(P, Q, x) ⟹ P[x::=y] ∼ Q[x::=y]" shows "a<x>.P ∼ a<x>.Q" proof - let ?X = "{(a<x>.P, a<x>.Q) | a x P Q. ∀y ∈ supp(P, Q, x). P[x::=y] ∼ Q[x::=y]}" have "eqvt ?X" apply(auto simp add: eqvt_def) apply(rule_tac x="perma ∙ aa" in exI) apply(rule_tac x="perma ∙ x" in exI) apply(rule_tac x="perma ∙ P" in exI) apply auto apply(rule_tac x="perma ∙ Q" in exI) apply auto apply(drule_tac pi="rev perma" in pt_set_bij2[OF pt_name_inst, OF at_name_inst]) apply(simp add: eqvts pt_rev_pi[OF pt_name_inst, OF at_name_inst]) apply(erule_tac x="rev perma ∙ y" in ballE) apply auto apply(drule_tac p=perma in bisimClosed) by(simp add: eqvts pt_pi_rev[OF pt_name_inst, OF at_name_inst]) from assms have "(a<x>.P, a<x>.Q) ∈ ?X" by fastforce thus ?thesis proof(coinduct rule: bisimCoinduct) case(cSim P Q) thus ?case using ‹eqvt ?X› by(fastforce intro: inputSuppPres) next case(cSym P Q) thus ?case by(fastforce simp add: supp_prod dest: symmetric) qed qed inductive equiv :: "pi ⇒ pi ⇒ bool" (infixr ‹≡⇩_{e}› 80) where Refl: "P ≡⇩_{e}P" | Sym: "P ≡⇩_{e}Q ⟹ Q ≡⇩_{e}P" | Trans: "⟦P ≡⇩_{e}Q; Q ≡⇩_{e}R⟧ ⟹ P ≡⇩_{e}R" | Match: "[a⌢a]P ≡⇩_{e}P" | Match': "a ≠ b ⟹ [a⌢b]P ≡⇩_{e}𝟬" | Mismatch: "a ≠ b ⟹ [a≠b]P ≡⇩_{e}P" | Mismatch': "[a≠a]P ≡⇩_{e}𝟬" | SumSym: "P ⊕ Q ≡⇩_{e}Q ⊕ P" | SumAssoc: "(P ⊕ Q) ⊕ R ≡⇩_{e}P ⊕ (Q ⊕ R)" | SumZero: "P ⊕ 𝟬 ≡⇩_{e}P" | SumIdemp: "P ⊕ P ≡⇩_{e}P" | SumRes: "<νx>(P ⊕ Q) ≡⇩_{e}(<νx>P) ⊕ (<νx>Q)" | ResNil: "<νx>𝟬 ≡⇩_{e}𝟬" | ResInput: "⟦x ≠ a; x ≠ y⟧ ⟹ <νx>a<y>.P ≡⇩_{e}a<y>.(<νx>P)" | ResInput': "<νx>x<y>.P ≡⇩_{e}𝟬" | ResOutput: "⟦x ≠ a; x ≠ b⟧ ⟹ <νx>a{b}.P ≡⇩_{e}a{b}.(<νx>P)" | ResOutput': "<νx>x{b}.P ≡⇩_{e}𝟬" | ResTau: "<νx>τ.(P) ≡⇩_{e}τ.(<νx>P)" | ResComm: "<νx><νy>P ≡⇩_{e}<νy><νx>P" | ResFresh: "x ♯ P ⟹ <νx>P ≡⇩_{e}P" | Expand: "⟦(R, expandSet P Q) ∈ sumComposeSet; hnf P; hnf Q⟧ ⟹ P ∥ Q ≡⇩_{e}R" | SumPres: "P ≡⇩_{e}Q ⟹ P ⊕ R ≡⇩_{e}Q ⊕ R" | ParPres: "⟦P ≡⇩_{e}P'; Q ≡⇩_{e}Q'⟧ ⟹ P ∥ Q ≡⇩_{e}P' ∥ Q'" | ResPres: "P ≡⇩_{e}Q ⟹ <νx>P ≡⇩_{e}<νx>Q" | TauPres: "P ≡⇩_{e}Q ⟹ τ.(P) ≡⇩_{e}τ.(Q)" | OutputPres: "P ≡⇩_{e}Q ⟹ a{b}.P ≡⇩_{e}a{b}.Q" | InputPres: "⟦∀y ∈ supp(P, Q, x). P[x::=y] ≡⇩_{e}Q[x::=y]⟧ ⟹ a<x>.P ≡⇩_{e}a<x>.Q" lemma SumIdemp': fixes P :: pi and P' :: pi assumes "P ≡⇩_{e}P'" shows "P ⊕ P' ≡⇩_{e}P" proof - have "P ≡⇩_{e}P ⊕ P" by(blast intro: Sym SumIdemp) moreover from assms have "P ⊕ P ≡⇩_{e}P' ⊕ P" by(rule SumPres) moreover have "P' ⊕ P ≡⇩_{e}P ⊕ P'" by(rule SumSym) ultimately have "P ≡⇩_{e}P ⊕ P'" by(blast intro: Trans) thus ?thesis by(rule Sym) qed lemma SumPres': fixes P :: pi and P' :: pi and Q :: pi and Q' :: pi assumes PeqP': "P ≡⇩_{e}P'" and QeqQ': "Q ≡⇩_{e}Q'" shows "P ⊕ Q ≡⇩_{e}P' ⊕ Q'" proof - from PeqP' have "P ⊕ Q ≡⇩_{e}P' ⊕ Q" by(rule SumPres) moreover have "P' ⊕ Q ≡⇩_{e}Q ⊕ P'" by(rule SumSym) moreover from QeqQ' have "Q ⊕ P' ≡⇩_{e}Q' ⊕ P'" by(rule SumPres) moreover have "Q' ⊕ P' ≡⇩_{e}P' ⊕ Q'" by(rule SumSym) ultimately show ?thesis by(blast intro: Trans) qed (* lemma ParComm: fixes P :: pi and Q :: pi and R :: pi assumes "(R, expandSet P Q) ∈ sumComposeSet" obtains R' where "(R, expandSet Q P) ∈ sumComposeSet" and "R ≡⇩_{e}R'" using assms apply(induct S=="expandSet P Q" rule: sumComposeSet.induct) apply auto apply(simp add: expandSet_def) apply fastforce apply auto apply(clarify) *) lemma sound: fixes P :: pi and Q :: pi assumes "P ≡⇩_{e}Q" shows "P ∼ Q" using assms proof(induct) case(Refl P) show ?case by(rule reflexive) next case(Sym P Q) have "P ∼ Q" by fact thus ?case by(rule symmetric) next case(Trans P Q R) have "P ∼ Q" and "Q ∼ R" by fact+ thus ?case by(rule transitive) next case(Match a P) show ?case by(rule matchId) next case(Match' a b P) have "a ≠ b" by fact thus ?case by(rule matchNil) next case(Mismatch a b P) have "a ≠ b" by fact thus ?case by(rule mismatchId) next case(Mismatch' a P) show ?case by(rule mismatchNil) next case(SumSym P Q) show ?case by(rule sumSym) next case(SumAssoc P Q R) show ?case by(rule sumAssoc) next case(SumZero P) show ?case by(rule sumZero) next case(SumIdemp P) show ?case by(rule sumIdemp) next case(SumRes x P Q) show ?case by(rule sumRes) next case(ResNil x) show ?case by(rule nilRes) next case(ResInput x a y P) have "x ≠ a" and "x ≠ y" by fact+ thus ?case by(rule resInput) next case(ResInput' x y P) show ?case by(rule resNil) next case(ResOutput x a b P) have "x ≠ a" and "x ≠ b" by fact+ thus ?case by(rule resOutput) next case(ResOutput' x b P) show ?case by(rule resNil) next case(ResTau x P) show ?case by(rule resTau) next case(ResComm x P) show ?case by(rule resComm) next case(ResFresh x P) have "x ♯ P" by fact thus ?case by(rule scopeFresh) next case(Expand R P Q) have "(R, expandSet P Q) ∈ sumComposeSet" and "hnf P" and "hnf Q" by fact+ thus ?case by(rule expandSC) next case(SumPres P Q R) from ‹P ∼ Q› show ?case by(rule sumPres) next case(ParPres P P' Q Q') have "P ∼ P'" and "Q ∼ Q'" by fact+ thus ?case by(metis transitive symmetric parPres parSym) next case(ResPres P Q x) from ‹P ∼ Q› show ?case by(rule resPres) next case(TauPres P Q) from ‹P ∼ Q› show ?case by(rule tauPres) next case(OutputPres P Q a b) from ‹P ∼ Q› show ?case by(rule outputPres) next case(InputPres P Q x a) have "∀y ∈ supp(P, Q, x). P[x::=y] ≡⇩_{e}Q[x::=y] ∧ P[x::=y] ∼ Q[x::=y]" by fact hence "∀y ∈ supp(P, Q, x). P[x::=y] ∼ Q[x::=y]" by blast thus ?case by(rule_tac inputSuppPresBisim) auto qed lemma zeroDest[dest]: fixes a :: name and b :: name and x :: name and P :: pi shows "(a{b}.P) ≡⇩_{e}𝟬 ⟹ False" and "(a<x>.P) ≡⇩_{e}𝟬 ⟹ False" and "(τ.(P)) ≡⇩_{e}𝟬 ⟹ False" and "𝟬 ≡⇩_{e}a{b}.P ⟹ False" and "𝟬 ≡⇩_{e}a<x>.P ⟹ False" and "𝟬 ≡⇩_{e}τ.(P) ⟹ False" by(auto dest: sound) lemma eq_eqvt: fixes pi::"name prm" and x::"'a::pt_name" shows "pi∙(x=y) = ((pi∙x)=(pi∙y))" by(simp add: perm_bool perm_bij) nominal_primrec "depth" :: "pi ⇒ nat" where "depth 𝟬 = 0" | "depth (τ.(P)) = 1 + (depth P)" | "a ♯ x ⟹ depth (a<x>.P) = 1 + (depth P)" | "depth (a{b}.P) = 1 + (depth P)" | "depth ([a⌢b]P) = (depth P)" | "depth ([a≠b]P) = (depth P)" | "depth (P ⊕ Q) = max (depth P) (depth Q)" | "depth (P ∥ Q) = ((depth P) + (depth Q))" | "depth (<νx>P) = (depth P)" | "depth (!P) = (depth P)" apply(auto simp add: fresh_nat) apply(finite_guess)+ by(fresh_guess)+ lemma depthEqvt[simp]: fixes P :: pi and p :: "name prm" shows "depth(p ∙ P) = depth P" by(nominal_induct P rule: pi.strong_induct, auto simp add: name_bij) lemma depthInput[simp]: fixes a :: name and x :: name and P :: pi shows "depth (a<x>.P) = 1 + (depth P)" proof - obtain y where yineqa: "y ≠ a" and yFreshP: "y ♯ P" by(force intro: name_exists_fresh[of "(a, P)"] simp add: fresh_prod) from yFreshP have "a<x>.P = a<y>.([(x, y)] ∙ P)" by(simp add: alphaInput) with yineqa show ?thesis by simp qed nominal_primrec "valid" :: "pi ⇒ bool" where "valid 𝟬 = True" | "valid (τ.(P)) = valid P" | "x ♯ a ⟹ valid (a<x>.P) = valid P" | "valid (a{b}.P) = valid P" | "valid ([a⌢b]P) = valid P" | "valid ([a≠b]P) = valid P" | "valid (P ⊕ Q) = ((valid P) ∧ (valid Q))" | "valid (P ∥ Q) = ((valid P) ∧ (valid Q))" | "valid (<νx>P) = valid P" | "valid (!P) = False" apply(auto simp add: fresh_bool) apply(finite_guess)+ by(fresh_guess)+ lemma validEqvt[simp]: fixes P :: pi and p :: "name prm" shows "valid(p ∙ P) = valid P" by(nominal_induct P rule: pi.strong_induct, auto simp add: name_bij) lemma validInput[simp]: fixes a :: name and x :: name and P :: pi shows "valid (a<x>.P) = valid P" proof - obtain y where yineqa: "y ≠ a" and yFreshP: "y ♯ P" by(force intro: name_exists_fresh[of "(a, P)"] simp add: fresh_prod) from yFreshP have "a<x>.P = a<y>.([(x, y)] ∙ P)" by(simp add: alphaInput) with yineqa show ?thesis by simp qed lemma depthMin[intro]: fixes P shows "0 ≤ depth P" by(induct P rule: pi.induct, auto) lemma hnfTransition: fixes P :: pi assumes "hnf P" and "P ≠ 𝟬" shows "∃Rs. P ⟼ Rs" using assms by(induct rule: pi.induct, auto intro: Output Tau Input Sum1 Open) definition "uhnf" :: "pi ⇒ bool" where "uhnf P ≡ hnf P ∧ (∀R ∈ summands P. ∀R' ∈ summands P. R ≠ R' ⟶ ¬(R ≡⇩_{e}R'))" lemma summandsIdemp: fixes P :: pi and Q :: pi assumes "Q ∈ summands P" and "Q ≡⇩_{e}Q'" shows "P ⊕ Q' ≡⇩_{e}P" using assms proof(nominal_induct P arbitrary: Q rule: pi.strong_inducts) case(PiNil Q) have "Q ∈ summands 𝟬" by fact hence False by simp thus ?case by simp next case(Output a b P Q) have "Q ≡⇩_{e}Q'" by fact hence "a{b}.P ⊕ Q' ≡⇩_{e}a{b}.P ⊕ Q" by(blast intro: SumPres' Refl Sym) moreover have "Q = a{b}.P" proof - have "Q ∈ summands (a{b}.P)" by fact thus ?thesis by simp qed ultimately show ?case by(blast intro: SumIdemp Trans) next case(Tau P Q) have "Q ≡⇩_{e}Q'" by fact hence "τ.(P) ⊕ Q' ≡⇩_{e}τ.(P) ⊕ Q" by(blast intro: SumPres' Refl Sym) moreover have "Q = τ.(P)" proof - have "Q ∈ summands (τ.(P))" by fact thus ?thesis by simp qed ultimately show ?case by(blast intro: SumIdemp Trans) next case(Input a x P Q) have "Q ≡⇩_{e}Q'" by fact hence "a<x>.P ⊕ Q' ≡⇩_{e}a<x>.P ⊕ Q" by(blast intro: SumPres' Refl Sym) moreover have "Q = a<x>.P" proof - have "Q ∈ summands (a<x>.P)" by fact thus ?thesis by simp qed ultimately show ?case by(blast intro: SumIdemp Trans) next case(Match a b P Q) have "Q ∈ summands ([a⌢b]P)" by fact hence False by simp thus ?case by simp next case(Mismatch a b P Q) have "Q ∈ summands ([a≠b]P)" by fact hence False by simp thus ?case by simp next case(Sum P Q R) have IHP: "⋀P'. ⟦P' ∈ summands P; P' ≡⇩_{e}Q'⟧ ⟹ P ⊕ Q' ≡⇩_{e}P" by fact have IHQ: "⋀Q''. ⟦Q'' ∈ summands Q; Q'' ≡⇩_{e}Q'⟧ ⟹ Q ⊕ Q' ≡⇩_{e}Q" by fact have ReqQ': "R ≡⇩_{e}Q'" by fact have "R ∈ summands(P ⊕ Q)" by fact hence "R ∈ summands P ∨ R ∈ summands Q" by simp thus ?case proof(rule disjE) assume "R ∈ summands P" hence PQ'eqP: "P ⊕ Q' ≡⇩_{e}P" using ReqQ' by(rule IHP) have "(P ⊕ Q) ⊕ Q' ≡⇩_{e}P ⊕ (Q ⊕ Q')" by(rule SumAssoc) moreover have "P ⊕ (Q ⊕ Q') ≡⇩_{e}P ⊕ (Q' ⊕ Q)" by(blast intro: Refl SumSym SumPres') moreover have "P ⊕ (Q' ⊕ Q) ≡⇩_{e}(P ⊕ Q') ⊕ Q" by(blast intro: SumAssoc Sym) moreover from PQ'eqP have "(P ⊕ Q') ⊕ Q ≡⇩_{e}P ⊕ Q" by(blast intro: SumPres' Refl) ultimately show ?case by(blast intro: Trans) next assume "R ∈ summands Q" hence QQ'eqQ: "Q ⊕ Q' ≡⇩_{e}Q" using ReqQ' by(rule IHQ) have "(P ⊕ Q) ⊕ Q' ≡⇩_{e}P ⊕ (Q ⊕ Q')" by(rule SumAssoc) moreover from QQ'eqQ have "P ⊕ (Q ⊕ Q') ≡⇩_{e}P ⊕ Q" by(blast intro: Refl SumPres') ultimately show ?case by(rule Trans) qed next case(Par P Q R) have "R ∈ summands (P ∥ Q)" by fact hence False by simp thus ?case by simp next case(Res x P Q) have "Q ≡⇩_{e}Q'" by fact hence "(<νx>P) ⊕ Q' ≡⇩_{e}(<νx>P) ⊕ Q" by(blast intro: SumPres' Refl Sym) moreover have "Q = <νx>P" proof - have "Q ∈ summands (<νx>P)" by fact thus ?thesis by(auto simp add: if_split) qed ultimately show ?case by(blast intro: SumIdemp Trans) next case(Bang P Q) have "Q ∈ summands(!P)" by fact hence False by simp thus ?case by simp qed lemma uhnfSum: fixes P :: pi and Q :: pi assumes Phnf: "uhnf P" and Qhnf: "uhnf Q" and validP: "valid P" and validQ: "valid Q" shows "∃R. uhnf R ∧ valid R ∧ P ⊕ Q ≡⇩_{e}R ∧ (depth R) ≤ (depth (P ⊕ Q))" using assms proof(nominal_induct P arbitrary: Q rule: pi.strong_inducts) case(PiNil Q) have "uhnf Q" by fact moreover have "valid Q" by fact moreover have "𝟬 ⊕ Q ≡⇩_{e}Q" by(blast intro: SumZero SumSym Trans) moreover have "depth Q ≤ depth(𝟬 ⊕ Q)" by auto ultimately show ?case by blast next case(Output a b P Q) show ?case proof(case_tac "Q = 𝟬") assume "Q = 𝟬" moreover have "uhnf (a{b}.P)" by(simp add: uhnf_def) moreover have "valid (a{b}.P)" by fact moreover have "a{b}.P ⊕ 𝟬 ≡⇩_{e}a{b}.P" by(rule SumZero) moreover have "depth(a{b}.P) ≤ depth(a{b}.P ⊕ 𝟬)" by simp ultimately show ?case by blast next assume QineqNil: "Q ≠ 𝟬" have Qhnf: "uhnf Q" by fact have validQ: "valid Q" by fact have validP: "valid(a{b}.P)" by fact show ?case proof(case_tac "∃Q' ∈ summands Q. Q' ≡⇩_{e}a{b}.P") assume "∃Q' ∈ summands Q. Q' ≡⇩_{e}a{b}.P" then obtain Q' where "Q' ∈ summands Q" and "Q' ≡⇩_{e}a{b}.P" by blast hence "Q ⊕ a{b}.P ≡⇩_{e}Q" by(rule summandsIdemp) moreover have "depth Q ≤ depth(Q ⊕ a{b}.P)" by simp ultimately show ?case using Qhnf validQ by(force intro: SumSym Trans) next assume "¬(∃Q' ∈ summands Q. Q' ≡⇩_{e}a{b}.P)" hence "∀Q' ∈ summands Q. ¬(Q' ≡⇩_{e}a{b}.P)" by simp with Qhnf QineqNil have "uhnf (a{b}.P ⊕ Q)" by(force dest: Sym simp add: uhnf_def) moreover from validQ validP have "valid(a{b}.P ⊕ Q)" by simp moreover have "a{b}.P ⊕ Q ≡⇩_{e}a{b}.P ⊕ Q" by(rule Refl) moreover have "depth(a{b}.P ⊕ Q) ≤ depth(a{b}.P ⊕ Q)" by simp ultimately show ?case by blast qed qed next case(Tau P Q) show ?case proof(case_tac "Q = 𝟬") assume "Q = 𝟬" moreover have "uhnf (τ.(P))" by(simp add: uhnf_def) moreover have "valid (τ.(P))" by fact moreover have "τ.(P) ⊕ 𝟬 ≡⇩_{e}τ.(P)" by(rule SumZero) moreover have "depth(τ.(P)) ≤ depth(τ.(P) ⊕ 𝟬)" by simp ultimately show ?case by blast next assume QineqNil: "Q ≠ 𝟬" have Qhnf: "uhnf Q" by fact have validP: "valid(τ.(P))" and validQ: "valid Q" by fact+ show ?case proof(case_tac "∃Q' ∈ summands Q. Q' ≡⇩_{e}τ.(P)") assume "∃Q' ∈ summands Q. Q' ≡⇩_{e}τ.(P)" then obtain Q' where "Q' ∈ summands Q" and "Q' ≡⇩_{e}τ.(P)" by blast hence "Q ⊕ τ.(P) ≡⇩_{e}Q" by(rule summandsIdemp) moreover have "depth Q ≤ depth(Q ⊕ τ.(P))" by simp ultimately show ?case using Qhnf validQ by(force intro: SumSym Trans) next assume "¬(∃Q' ∈ summands Q. Q' ≡⇩_{e}τ.(P))" hence "∀Q' ∈ summands Q. ¬(Q' ≡⇩_{e}τ.(P))" by simp with Qhnf QineqNil have "uhnf (τ.(P) ⊕ Q)" by(force dest: Sym simp add: uhnf_def) moreover from validP validQ have "valid(τ.(P) ⊕ Q)" by simp moreover have "τ.(P) ⊕ Q ≡⇩_{e}τ.(P) ⊕ Q" by(rule Refl) moreover have "depth(τ.(P) ⊕ Q) ≤ depth(τ.(P) ⊕ Q)" by simp ultimately show ?case by blast qed qed next case(Input a x P Q) show ?case proof(case_tac "Q = 𝟬") assume "Q = 𝟬" moreover have "uhnf (a<x>.P)" by(simp add: uhnf_def) moreover have "valid (a<x>.P)" by fact moreover have "a<x>.P ⊕ 𝟬 ≡⇩_{e}a<x>.P" by(rule SumZero) moreover have "depth(a<x>.P) ≤ depth(a<x>.P ⊕ 𝟬)" by simp ultimately show ?case by blast next assume QineqNil: "Q ≠ 𝟬" have validP: "valid(a<x>.P)" and validQ: "valid Q" by fact+ have Qhnf: "uhnf Q" by fact show ?case proof(case_tac "∃Q' ∈ summands Q. Q' ≡⇩_{e}a<x>.P") assume "∃Q' ∈ summands Q. Q' ≡⇩_{e}a<x>.P" then obtain Q' where "Q' ∈ summands Q" and "Q' ≡⇩_{e}a<x>.P" by blast hence "Q ⊕ a<x>.P ≡⇩_{e}Q" by(rule summandsIdemp) moreover have "depth Q ≤ depth(Q ⊕ a<x>.P)" by simp ultimately show ?case using Qhnf validQ by(force intro: SumSym Trans) next assume "¬(∃Q' ∈ summands Q. Q' ≡⇩_{e}a<x>.P)" hence "∀Q' ∈ summands Q. ¬(Q' ≡⇩_{e}a<x>.P)" by simp with Qhnf QineqNil have "uhnf (a<x>.P ⊕ Q)" by(force dest: Sym simp add: uhnf_def) moreover from validP validQ have "valid(a<x>.P ⊕ Q)" by simp moreover have "a<x>.P ⊕ Q ≡⇩_{e}a<x>.P ⊕ Q" by(rule Refl) moreover have "depth(a<x>.P ⊕ Q) ≤ depth(a<x>.P ⊕ Q)" by simp ultimately show ?case by blast qed qed next case(Match a b P Q) have "uhnf ([a⌢b]P)" by fact hence False by(simp add: uhnf_def) thus ?case by simp next case(Mismatch a b P Q) have "uhnf ([a≠b]P)" by fact hence False by(simp add: uhnf_def) thus ?case by simp next case(Sum P Q R) have Rhnf: "uhnf R" by fact have validR: "valid R" by fact have PQhnf: "uhnf (P ⊕ Q)" by fact have validPQ: "valid(P ⊕ Q)" by fact have "∃T. uhnf T ∧ valid T ∧ Q ⊕ R ≡⇩_{e}T ∧ depth T ≤ depth (Q ⊕ R)" proof - from PQhnf have "uhnf Q" by(simp add: uhnf_def) moreover from validPQ have "valid Q" by simp+ moreover have "⋀R. ⟦uhnf Q; uhnf R; valid Q; valid R⟧ ⟹ ∃T. uhnf T ∧ valid T ∧ Q ⊕ R ≡⇩_{e}T ∧ depth T ≤ depth(Q ⊕ R)" by fact ultimately show ?thesis using Rhnf validR by blast qed then obtain T where Thnf: "uhnf T" and QReqT: "Q ⊕ R ≡⇩_{e}T" and validT: "valid T" and Tdepth: "depth T ≤ depth(Q ⊕ R)" by blast have "∃S. uhnf S ∧ valid S ∧ P ⊕ T ≡⇩_{e}S ∧ depth S ≤ depth(P ⊕ T)" proof - from PQhnf have "uhnf P" by(simp add: uhnf_def) moreover from validPQ have "valid P" by simp moreover have "⋀T. ⟦uhnf P; uhnf T; valid P; valid T⟧ ⟹ ∃S. uhnf S ∧ valid S ∧ P ⊕ T ≡⇩_{e}S ∧ depth S ≤ depth(P ⊕ T)" by fact ultimately show ?thesis using Thnf validT by blast qed then obtain S where Shnf: "uhnf S" and PTeqS: "P ⊕ T ≡⇩_{e}S" and validS: "valid S" and Sdepth: "depth S ≤ depth(P ⊕ T)" by blast have "(P ⊕ Q) ⊕ R ≡⇩_{e}S" proof - have "(P ⊕ Q) ⊕ R ≡⇩_{e}P ⊕ (Q ⊕ R)" by(rule SumAssoc) moreover from QReqT have "P ⊕ (Q ⊕ R) ≡⇩_{e}P ⊕ T" by(blast intro: Refl SumPres') ultimately show ?thesis using PTeqS by(blast intro: Trans) qed moreover from Tdepth Sdepth have "depth S ≤ depth((P ⊕ Q) ⊕ R)" by auto ultimately show ?case using Shnf validS by blast next case(Par P Q R) have "uhnf (P ∥ Q)" by fact hence False by(simp add: uhnf_def) thus ?case by simp next case(Res x P Q) show ?case proof(case_tac "Q = 𝟬") assume "Q = 𝟬" moreover have "uhnf (<νx>P)" by fact moreover have "valid (<νx>P)" by fact moreover have "<νx>P ⊕ 𝟬 ≡⇩_{e}<νx>P" by(rule SumZero) moreover have "depth(<νx>P) ≤ depth((<νx>P) ⊕ 𝟬)" by simp ultimately show ?case by blast next assume QineqNil: "Q ≠ 𝟬" have Qhnf: "uhnf Q" by fact have validP: "valid(<νx>P)" and validQ: "valid Q" by fact+ show ?case proof(case_tac "∃Q' ∈ summands Q. Q' ≡⇩_{e}<νx>P") assume "∃Q' ∈ summands Q. Q' ≡⇩_{e}<νx>P" then obtain Q' where "Q' ∈ summands Q" and "Q' ≡⇩_{e}<νx>P" by blast hence "Q ⊕ <νx>P ≡⇩_{e}Q" by(rule summandsIdemp) moreover have "depth Q ≤ depth(Q ⊕ <νx>P)" by simp ultimately show ?case using Qhnf validQ by(force intro: SumSym Trans) next assume "¬(∃Q' ∈ summands Q. Q' ≡⇩_{e}<νx>P)" hence "∀Q' ∈ summands Q. ¬(Q' ≡⇩_{e}<νx>P)" by simp moreover have "uhnf (<νx>P)" by fact ultimately have "uhnf (<νx>P ⊕ Q)" using Qhnf QineqNil by(force dest: Sym simp add: uhnf_def) moreover from validP validQ have "valid(<νx>P ⊕ Q)" by simp moreover have "(<νx>P) ⊕ Q ≡⇩_{e}(<νx>P) ⊕ Q" by(rule Refl) moreover have "depth((<νx>P) ⊕ Q) ≤ depth((<νx>P) ⊕ Q)" by simp ultimately show ?case by blast qed qed next case(Bang P Q) have "uhnf (!P)" by fact hence False by(simp add: uhnf_def) thus ?case by simp qed lemma uhnfRes: fixes x :: name and P :: pi assumes Phnf: "uhnf P" and validP: "valid P" shows "∃P'. uhnf P' ∧ valid P' ∧ <νx>P ≡⇩_{e}P' ∧ depth P' ≤ depth(<νx>P)" using assms proof(nominal_induct P avoiding: x rule: pi.strong_inducts) case(PiNil x) have "uhnf 𝟬" by(simp add: uhnf_def) moreover have "valid 𝟬" by simp moreover have "<νx>𝟬 ≡⇩_{e}𝟬" by(rule ResNil) moreover have "depth 𝟬 ≤ depth(<νx>𝟬)" by simp ultimately show ?case by blast next case(Output a b P) have "valid(a{b}.P)" by fact hence validP: "valid P" by simp show ?case proof(case_tac "x=a") assume "x = a" moreover have "uhnf 𝟬" by(simp add: uhnf_def) moreover have "valid 𝟬" by simp moreover have "𝟬 ≡⇩_{e}<νx>x{b}.P" by(blast intro: ResOutput' Sym) moreover have "depth 𝟬 ≤ depth(<νx>x{b}.P)" by simp ultimately show ?case by(blast intro: Sym) next assume xineqa: "x ≠ a" show ?case proof(case_tac "x=b") assume "x=b" moreover from xineqa have "uhnf(<νx>a{x}.P)" by(force simp add: uhnf_def) moreover from validP have "valid(<νx>a{x}.P)" by simp moreover have "<νx>a{x}.P ≡⇩_{e}<νx>a{x}.P" by(rule Refl) moreover have "depth(<νx>a{x}.P) ≤ depth(<νx>a{x}.P)" by simp ultimately show ?case by blast next assume xineqb: "x ≠ b" have "uhnf(a{b}.(<νx>P))" by(simp add: uhnf_def) moreover from validP have "valid(a{b}.(<νx>P))" by simp moreover from xineqa xineqb have "a{b}.(<νx>P) ≡⇩_{e}<νx>a{b}.P" by(blast intro: ResOutput Sym) moreover have "depth(a{b}.(<νx>P)) ≤ depth(<νx>a{b}.P)" by simp ultimately show ?case by(blast intro: Sym) qed qed next case(Tau P) have "valid(τ.(P))" by fact hence validP: "valid P" by simp have "uhnf(τ.(<νx>P))" by(simp add: uhnf_def) moreover from validP have "valid(τ.(<νx>P))" by simp moreover have "τ.(<νx>P) ≡⇩_{e}<νx>τ.(P)" by(blast intro: ResTau Sym) moreover have "depth(τ.(<νx>P)) ≤ depth(<νx>τ.(P))" by simp ultimately show ?case by(blast intro: Sym) next case(Input a y P x) have "valid(a<y>.P)" by fact hence validP: "valid P" by simp have "y ♯ x" by fact hence yineqx: "y ≠ x" by simp show ?case proof(case_tac "x=a") assume "x = a" moreover have "uhnf 𝟬" by(simp add: uhnf_def) moreover have "valid 𝟬" by simp moreover have "𝟬 ≡⇩_{e}<νx>x<y>.P" by(blast intro: ResInput' Sym) moreover have "depth 𝟬 ≤ depth(<νx>x<y>.P)" by simp ultimately show ?case by(blast intro: Sym) next assume xineqa: "x ≠ a" have "uhnf(a<y>.(<νx>P))" by(simp add: uhnf_def) moreover from validP have "valid(a<y>.(<νx>P))" by simp moreover from xineqa yineqx have "a<y>.(<νx>P) ≡⇩_{e}<νx>a<y>.P" by(blast intro: ResInput Sym) moreover have "depth(a<y>.(<νx>P)) ≤ depth(<νx>a<y>.P)" by simp ultimately show ?case by(blast intro: Sym) qed next case(Match a b P x) have "uhnf([a⌢b]P)" by fact hence False by(simp add: uhnf_def) thus ?case by simp next case(Mismatch a b P x) have "uhnf([a≠b]P)" by fact hence False by(simp add: uhnf_def) thus ?case by simp next case(Sum P Q x) have "valid(P ⊕ Q)" by fact hence validP: "valid P" and validQ: "valid Q" by simp+ have "uhnf(P ⊕ Q)" by fact hence Phnf: "uhnf P" and Qhnf: "uhnf Q" by(auto simp add: uhnf_def) have "∃P'. uhnf P' ∧ valid P' ∧ P' ≡⇩_{e}<νx>P ∧ (depth P') ≤ (depth(<νx>P))" proof - have "⟦uhnf P; valid P⟧ ⟹ ∃P'. uhnf P' ∧ valid P' ∧ <νx>P ≡⇩_{e}P' ∧ (depth P') ≤ (depth (<νx>P))" by fact with validP Phnf show ?thesis by(blast intro: Sym) qed then obtain P' where P'hnf: "uhnf P'" and P'eqP: "P' ≡⇩_{e}<νx>P" and validP': "valid P'" and P'depth: "(depth P') ≤ (depth(<νx>P))" by blast have "∃Q'. uhnf Q' ∧ valid Q' ∧ Q' ≡⇩_{e}<νx>Q ∧ (depth Q') ≤ (depth(<νx>Q))" proof - have "⟦uhnf Q; valid Q⟧ ⟹ ∃Q'. uhnf Q' ∧ valid Q' ∧ <νx>Q ≡⇩_{e}Q' ∧ (depth Q') ≤ (depth(<νx>Q))" by fact with validQ Qhnf show ?thesis by(blast intro: Sym) qed then obtain Q' where Q'hnf: "uhnf Q'" and Q'eqQ: "Q' ≡⇩_{e}<νx>Q" and validQ': "valid Q'" and Q'depth: "(depth Q') ≤ (depth(<νx>Q))" by blast from P'hnf Q'hnf validP' validQ' obtain R where Rhnf: "uhnf R" and validR: "valid R" and P'Q'eqR: "P' ⊕ Q' ≡⇩_{e}R" and Rdepth: "depth R ≤ depth(P' ⊕ Q')" apply(drule_tac uhnfSum) apply assumption+ by blast from P'eqP Q'eqQ P'Q'eqR have "<νx>(P ⊕ Q) ≡⇩_{e}R" by(blast intro: Sym SumPres' SumRes Trans) moreover from Rdepth P'depth Q'depth have "depth R ≤ depth(<νx>(P ⊕ Q))" by auto ultimately show ?case using validR Rhnf by(blast intro: Sym) next case(Par P Q) have "uhnf(P ∥ Q)" by fact hence False by(simp add: uhnf_def) thus ?case by simp next case(Res y P x) have "valid(<νy>P)" by fact hence validP: "valid P" by simp have "uhnf(<νy>P)" by fact then obtain a P' where aineqy: "a ≠ y" and PeqP': "P = a{y}.P'" by(force simp add: uhnf_def) show ?case proof(case_tac "x=y") assume "x=y" moreover from aineqy have "uhnf(<νy>a{y}.P')" by(force simp add: uhnf_def) moreover from validP PeqP' have "valid(<νy>a{y}.P')" by simp moreover have "<νy><νy>a{y}.P' ≡⇩_{e}<νy>a{y}.P'" proof - have "y ♯ <νy>a{y}.P'" by(simp add: name_fresh_abs) hence "<νy><νy>a{y}.P' ≡⇩_{e}<νy>a{y}.P'" by(rule ResFresh) thus ?thesis by(blast intro: Trans) qed moreover have "depth(<νy>a{y}.P') ≤ depth(<νy><νy>a{y}.P')" by simp ultimately show ?case using PeqP' by blast next assume xineqy: "x≠y" show ?case proof(case_tac "x=a") assume "x=a" moreover have "uhnf 𝟬" by(simp add: uhnf_def) moreover have "valid 𝟬" by simp moreover have "<νa><νy>a{y}.P' ≡⇩_{e}𝟬" proof - have "<νa><νy>a{y}.P' ≡⇩_{e}<νy><νa>a{y}.P'" by(rule ResComm) moreover have "<νy><νa>a{y}.P' ≡⇩_{e}𝟬" by(blast intro: ResOutput' ResNil ResPres Trans) ultimately show ?thesis by(blast intro: Trans) qed moreover have "depth 𝟬 ≤ depth(<νa><νy>a{y}.P')" by simp ultimately show ?case using PeqP' by blast next assume xineqa: "x ≠ a" from aineqy have "uhnf(<νy>a{y}.(<νx>P'))" by(force simp add: uhnf_def) moreover from validP PeqP' have "valid(<νy>a{y}.(<νx>P'))" by simp moreover have "<νx><νy>a{y}.P' ≡⇩_{e}<νy>a{y}.(<νx>P')" proof - have "<νx><νy>a{y}.P' ≡⇩_{e}<νy><νx>a{y}.P'" by(rule ResComm) moreover from xineqa xineqy have "<νy><νx>a{y}.P' ≡⇩_{e}<νy>a{y}.(<νx>P')" by(blast intro: ResOutput ResPres Trans) ultimately show ?thesis by(blast intro: Trans) qed moreover have "depth(<νy>a{y}.(<νx>P')) ≤ depth(<νx><νy>a{y}.P')" by simp ultimately show ?case using PeqP' by blast qed qed next case(Bang P x) have "valid(!P)" by fact hence False by simp thus ?case by simp qed lemma expandHnf: fixes P :: pi and S :: "pi set" assumes "(P, S) ∈ sumComposeSet" and "∀P ∈ S. uhnf P ∧ valid P" shows "∃P'. uhnf P' ∧ valid P' ∧ P ≡⇩_{e}P' ∧ depth P' ≤ depth P" using assms proof(induct rule: sumComposeSet.induct) case empty have "uhnf 𝟬" by(simp add: uhnf_def) moreover have "valid 𝟬" by simp moreover have "𝟬 ≡⇩_{e}𝟬" by(rule Refl) moreover have "depth 𝟬 ≤ depth 𝟬" by simp ultimately show ?case by blast next case(insert Q S P) have Shnf: "∀P ∈ S. uhnf P ∧ valid P" by fact hence "∀P ∈ (S - {(Q)}). uhnf P ∧ valid P" by simp moreover have "∀P ∈ (S - {(Q)}). uhnf P ∧ valid P ⟹ ∃P'. uhnf P' ∧ valid P' ∧ P ≡⇩_{e}P' ∧ depth P' ≤ depth P" by fact ultimately obtain P' where P'hnf: "uhnf P'" and validP': "valid P'" and PeqP': "P ≡⇩_{e}P'" and PP'depth: "depth P' ≤ depth P" by blast have "Q ∈ S" by fact with Shnf have "uhnf Q" and "valid Q" by simp+ with P'hnf validP' obtain R where Rhnf: "uhnf R" and validR: "valid R" and P'QeqR: "P' ⊕ Q ≡⇩_{e}R" and P'QRdepth: "depth R ≤ depth (P' ⊕ Q)" by(auto dest: uhnfSum) from PeqP' P'QeqR have "P ⊕ Q ≡⇩_{e}R" by(blast intro: SumPres Trans) moreover from PP'depth P'QRdepth have "depth R ≤ depth(P ⊕ Q)" by simp ultimately show ?case using Rhnf validR by blast qed lemma hnfSummandsRemove: fixes P :: pi and Q :: pi assumes "P ∈ summands Q" and "uhnf Q" shows "(summands Q) - {P' | P'. P' ∈ summands Q ∧ P' ≡⇩_{e}P} = (summands Q) - {P}" using assms by(auto intro: Refl simp add: uhnf_def) lemma pullSummand: fixes P :: pi and Q :: pi assumes PsummQ: "P ∈ summands Q" and Qhnf: "uhnf Q" shows "∃Q'. P ⊕ Q' ≡⇩_{e}Q ∧ (summands Q') = ((summands Q) - {x. ∃P'. x = P' ∧ P' ∈ (summands Q) ∧ P' ≡⇩_{e}P}) ∧ uhnf Q'" proof - have SumGoal: "⋀P Q R. ⟦P ∈ summands Q; uhnf(Q ⊕ R); ⋀P. ⟦P ∈ summands Q⟧ ⟹ ∃Q'. P ⊕ Q' ≡⇩_{e}Q ∧ (summands Q') = ((summands Q) - {P' |P'. P' ∈ summands Q ∧ P' ≡⇩_{e}P}) ∧ uhnf Q'; ⋀P. ⟦P ∈ summands R⟧ ⟹ ∃R'. P ⊕ R' ≡⇩_{e}R ∧ (summands R') = ((summands R) - {P' |P'. P' ∈ summands R ∧ P' ≡⇩_{e}P}) ∧ uhnf R'⟧ ⟹ ∃Q'. P ⊕ Q' ≡⇩_{e}Q ⊕ R ∧ summands Q' = summands (pi.Sum Q R) - {P' |P'. P' ∈ summands (Q ⊕ R) ∧ P' ≡⇩_{e}P} ∧ uhnf Q'" proof - fix P Q R assume IHR: "⋀P. P ∈ summands R ⟹ ∃R'. P ⊕ R' ≡⇩_{e}R ∧ (summands R') = ((summands R) - {P' |P'. P' ∈ summands R ∧ P' ≡⇩_{e}P}) ∧ uhnf R'" assume PsummQ: "P ∈ summands Q" moreover assume "⋀P. P ∈ summands Q ⟹ ∃Q'. P ⊕ Q' ≡⇩_{e}Q ∧ (summands Q') = ((summands Q) - {P' |P'. P' ∈ summands Q ∧ P' ≡⇩_{e}P}) ∧ uhnf Q'" ultimately obtain Q' where PQ'eqQ: "P ⊕ Q' ≡⇩_{e}Q" and Q'summQ: "(summands Q') = ((summands Q) - {P' |P'. P' ∈ summands Q ∧ P' ≡⇩_{e}P})" and Q'hnf: "uhnf Q'" by blast assume QRhnf: "uhnf(Q ⊕ R)" show "∃Q'. P ⊕ Q' ≡⇩_{e}Q ⊕ R ∧ summands Q' = summands (pi.Sum Q R) - {P' |P'. P' ∈ summands (Q ⊕ R) ∧ P' ≡⇩_{e}P} ∧ uhnf Q'" proof(cases "∃P' ∈ summands R. P' ≡⇩_{e}P") assume "∃P' ∈ summands R. P' ≡⇩_{e}P" then obtain P' where P'summR: "P' ∈ summands R" and P'eqP: "P' ≡⇩_{e}P" by blast with IHR obtain R' where PR'eqR: "P' ⊕ R' ≡⇩_{e}R" and R'summR: "(summands R') = ((summands R) - {P'' |P''. P'' ∈ summands R ∧ P'' ≡⇩_{e}P'})" and R'hnf: "uhnf R'" by blast have L1: "P ⊕ (Q' ⊕ R') ≡⇩_{e}Q ⊕ R" proof - from P'eqP have "P ⊕ (Q' ⊕ R') ≡⇩_{e}(P ⊕ P') ⊕ (Q' ⊕ R')" by(blast intro: SumIdemp' SumPres Sym) moreover have "(P ⊕ P') ⊕ (Q' ⊕ R') ≡⇩_{e}P ⊕ (P' ⊕ (Q' ⊕ R'))" by(rule SumAssoc) moreover have "P ⊕ (P' ⊕ (Q' ⊕ R')) ≡⇩_{e}P ⊕ (P' ⊕ (R' ⊕ Q'))" by(blast intro: Refl SumPres' SumSym) moreover have "P ⊕ (P' ⊕ (R' ⊕ Q')) ≡⇩_{e}P ⊕ (P' ⊕ R') ⊕ Q'" by(blast intro: Refl SumPres' Sym SumAssoc) moreover have "P ⊕ (P' ⊕ R') ⊕ Q' ≡⇩_{e}(P ⊕ Q') ⊕ (P' ⊕ R')" proof - have "P ⊕ (P' ⊕ R') ⊕ Q' ≡⇩_{e}P ⊕ Q' ⊕ (P' ⊕ R')" by(blast intro: Refl SumPres' SumSym) thus ?thesis by(blast intro: Sym SumAssoc Trans) qed moreover from PQ'eqQ PR'eqR have "(P ⊕ Q') ⊕ (P' ⊕ R') ≡⇩_{e}Q ⊕ R" by(rule SumPres') ultimately show ?thesis by(blast intro!: Trans) qed show ?thesis proof(cases "Q' = 𝟬") assume Q'eqNil: "Q' = 𝟬" have "P ⊕ R' ≡⇩_{e}Q ⊕ R" proof - have "P ⊕ R' ≡⇩_{e}P ⊕ (R' ⊕ 𝟬)" by(blast intro: SumZero Refl Trans SumPres' Sym) moreover have "P ⊕ (R' ⊕ 𝟬) ≡⇩_{e}P ⊕ (𝟬 ⊕ R')" by(blast intro: SumSym Trans SumPres' Refl) ultimately show ?thesis using L1 Q'eqNil by(blast intro: Trans) qed moreover from R'summR Q'summQ P'eqP Q'eqNil have "summands (R') = (summands (Q ⊕ R) - {P' |P'. P' ∈ summands(Q ⊕ R) ∧ P' ≡⇩_{e}P})" by(auto intro: Sym Trans) ultimately show ?thesis using R'hnf by blast next assume Q'ineqNil: "Q' ≠ 𝟬" show ?thesis proof(case_tac "R' = 𝟬") assume R'eqNil: "R' = 𝟬" have "P ⊕ Q' ≡⇩_{e}Q ⊕ R" proof - have "P ⊕ Q' ≡⇩_{e}P ⊕ (Q' ⊕ 𝟬)" by(blast intro: SumZero Refl Trans SumPres' Sym) with L1 R'eqNil show ?thesis by(blast intro: Trans) qed moreover from R'summR Q'summQ P'eqP R'eqNil have "summands (Q') = (summands (Q ⊕ R) - {P' |P'. P' ∈ summands(Q ⊕ R) ∧ P' ≡⇩_{e}P})" by(auto intro: Sym Trans) ultimately show ?thesis using Q'hnf by blast next assume R'ineqNil: "R' ≠ 𝟬" from R'summR Q'summQ P'eqP have "summands (Q' ⊕ R') = (summands (Q ⊕ R) - {P' |P'. P' ∈ summands(Q ⊕ R) ∧ P' ≡⇩_{e}P})" by(auto intro: Sym Trans) moreover from QRhnf Q'hnf R'hnf R'summR Q'summQ Q'ineqNil R'ineqNil have "uhnf(Q' ⊕ R')" by(auto simp add: uhnf_def) ultimately show ?thesis using L1 by blast qed qed next assume "¬(∃P' ∈ summands R. P' ≡⇩_{e}P)" hence Case: "∀P' ∈ summands R. ¬(P' ≡⇩_{e}P)" by simp show ?thesis proof(case_tac "Q' = 𝟬") assume Q'eqNil: "Q' = 𝟬" have "P ⊕ R ≡⇩_{e}Q ⊕ R" proof - have "P ⊕ R ≡⇩_{e}(P ⊕ 𝟬) ⊕ R" by(blast intro: SumZero Sym Trans SumPres) moreover from PQ'eqQ have "P ⊕ (Q' ⊕ R) ≡⇩_{e}Q ⊕ R" by(blast intro: SumAssoc Trans Sym SumPres) ultimately show ?thesis using Q'eqNil by(blast intro: SumAssoc Trans) qed moreover from Q'summQ Q'eqNil Case have "summands (R) = (summands (Q ⊕ R) - {P' |P'. P' ∈ summands(Q ⊕ R) ∧ P' ≡⇩_{e}P})" by auto moreover from QRhnf have "uhnf R" by(simp add: uhnf_def) ultimately show ?thesis by blast next assume Q'ineqNil: "Q' ≠ 𝟬" from PQ'eqQ have "P ⊕ (Q' ⊕ R) ≡⇩_{e}Q ⊕ R" by(blast intro: SumAssoc Trans Sym SumPres) moreover from Q'summQ Case have "summands (Q' ⊕ R) = (summands (Q ⊕ R) - {P' |P'. P' ∈ summands(Q ⊕ R) ∧ P' ≡⇩_{e}P})" by auto moreover from QRhnf Q'hnf Q'summQ Q'ineqNil have "uhnf (Q' ⊕ R)" by(auto simp add: uhnf_def) ultimately show ?thesis by blast qed qed qed from assms show ?thesis proof(nominal_induct Q arbitrary: P rule: pi.strong_inducts) case PiNil have "P ∈ summands 𝟬" by fact hence False by auto thus ?case by simp next case(Output a b Q) have "P ∈ summands (a{b}.Q)" by fact hence PeqQ: "P = a{b}.Q" by simp have "P ⊕ 𝟬 ≡⇩_{e}a{b}.Q" proof - have "P ⊕ 𝟬 ≡⇩_{e}P" by(rule SumZero) with PeqQ show ?thesis by simp qed moreover have "(summands 𝟬) = (summands (a{b}.Q)) - {P' | P'. P' ∈ summands (a{b}.Q) ∧ P' ≡⇩_{e}P}" proof - have "a{b}.Q ≡⇩_{e}a{b}.Q" by(rule Refl) with PeqQ show ?thesis by simp qed moreover have "uhnf 𝟬" by(simp add: uhnf_def) ultimately show ?case by blast next case(Tau Q) have "P ∈ summands (τ.(Q))" by fact hence PeqQ: "P = τ.(Q)" by simp have "P ⊕ 𝟬 ≡⇩_{e}τ.(Q)" proof - have "P ⊕ 𝟬 ≡⇩_{e}P" by(rule SumZero) with PeqQ show ?thesis by simp qed moreover have "(summands 𝟬) = (summands (τ.(Q))) - {P' | P'. P' ∈ summands (τ.(Q)) ∧ P' ≡⇩_{e}P}" proof - have "τ.(Q) ≡⇩_{e}τ.(Q)" by(rule Refl) with PeqQ show ?thesis by simp qed moreover have "uhnf 𝟬" by(simp add: uhnf_def) ultimately show ?case by blast next case(Input a x Q) have "P ∈ summands (a<x>.Q)" by fact hence PeqQ: "P = a<x>.Q" by simp have "P ⊕ 𝟬 ≡⇩_{e}a<x>.Q" proof - have "P ⊕ 𝟬 ≡⇩_{e}P" by(rule SumZero) with PeqQ show ?thesis by simp qed moreover have "(summands 𝟬) = (summands (a<x>.Q)) - {P' | P'. P' ∈ summands (a<x>.Q) ∧ P' ≡⇩_{e}P}" proof - have "a<x>.Q ≡⇩_{e}a<x>.Q" by(rule Refl) with PeqQ show ?thesis by simp qed moreover have "uhnf 𝟬" by(simp add: uhnf_def) ultimately show ?case by blast next case(Match a b Q) have "P ∈ summands ([a⌢b]Q)" by fact hence False by simp thus ?case by simp next case(Mismatch a b Q) have "P ∈ summands ([a≠b]Q)" by fact hence False by simp thus ?case by simp next case(Sum Q R) have QRhnf: "uhnf (Q ⊕ R)" by fact hence Qhnf: "uhnf Q" and Rhnf: "uhnf R" by(simp add: uhnf_def)+ have "⋀P. ⟦P ∈ summands Q; uhnf Q⟧ ⟹ ∃Q'. P ⊕ Q' ≡⇩_{e}Q ∧ (summands Q') = ((summands Q) - {P' |P'. P' ∈ summands Q ∧ P' ≡⇩_{e}P}) ∧ uhnf Q'" by fact with Qhnf have IHQ: "⋀P. P ∈ summands Q ⟹ ∃Q'. P ⊕ Q' ≡⇩_{e}Q ∧ (summands Q') = ((summands Q) - {P' |P'. P' ∈ summands Q ∧ P' ≡⇩_{e}P}) ∧ uhnf Q'" by simp have "⋀P. ⟦P ∈ summands R; uhnf R⟧ ⟹ ∃R'. P ⊕ R' ≡⇩_{e}R ∧ (summands R') = ((summands R) - {P' |P'. P' ∈ summands R ∧ P' ≡⇩_{e}P}) ∧ uhnf R'" by fact with Rhnf have IHR: "⋀P. P ∈ summands R ⟹ ∃R'. P ⊕ R' ≡⇩_{e}R ∧ (summands R') = ((summands R) - {P' |P'. P' ∈ summands R ∧ P' ≡⇩_{e}P}) ∧ uhnf R'" by simp have "P ∈ summands (Q ⊕ R)" by fact hence "P ∈ summands Q ∨ P ∈ summands R" by simp thus ?case proof(rule disjE) assume "P ∈ summands Q" thus ?case using QRhnf IHQ IHR by(rule SumGoal) next assume "P ∈ summands R" moreover from QRhnf have "uhnf (R ⊕ Q)" by(auto simp add: uhnf_def) ultimately have "∃Q'. (pi.Sum P Q') ≡⇩_{e}(pi.Sum R Q) ∧ summands Q' = summands (pi.Sum R Q) - {P' |P'. P' ∈ summands (pi.Sum R Q) ∧ P' ≡⇩_{e}P} ∧ uhnf Q'" using IHR IHQ by(rule SumGoal) thus ?case by(force intro: SumSym Trans) qed next case(Par Q R P) have "P ∈ summands (Q ∥ R)" by fact hence False by simp thus ?case by simp next case(Res x Q P) have "P ∈ summands (<νx>Q)" by fact hence PeqQ: "P = <νx>Q" by(simp add: if_split) have "P ⊕ 𝟬 ≡⇩_{e}<νx>Q" proof - have "P ⊕ 𝟬 ≡⇩_{e}P" by(rule SumZero) with PeqQ show ?thesis by simp qed moreover have "(summands 𝟬) = (summands (<νx>Q)) - {P' | P'. P' ∈ summands (<νx>Q) ∧ P' ≡⇩_{e}P}" proof - have "<νx>Q ≡⇩_{e}<νx>Q" by(rule Refl) with PeqQ show ?thesis by simp qed moreover have "uhnf 𝟬" by(simp add: uhnf_def) ultimately show ?case by blast next case(Bang Q P) have "P ∈ summands (!Q)" by fact hence False by simp thus ?case by simp qed qed lemma nSym: fixes P :: pi and Q :: pi assumes "¬(P ≡⇩_{e}Q)" shows "¬(Q ≡⇩_{e}P)" using assms by(blast dest: Sym) lemma summandsZero: fixes P :: pi assumes "summands P = {}" and "hnf P" shows "P = 𝟬" using assms by(nominal_induct P rule: pi.strong_inducts, auto intro: Refl SumIdemp SumPres' Trans) lemma summandsZero': fixes P :: pi assumes summP: "summands P = {}" and Puhnf: "uhnf P" shows "P = 𝟬" proof - from Puhnf have "hnf P" by(simp add: uhnf_def) with summP show ?thesis by(rule summandsZero) qed lemma summandEquiv: fixes P :: pi and Q :: pi assumes Phnf: "uhnf P" and Qhnf: "uhnf Q" and PinQ: "∀P' ∈ summands P. ∃Q' ∈ summands Q. P' ≡⇩_{e}Q'" and QinP: "∀Q' ∈ summands Q. ∃P' ∈ summands P. Q' ≡⇩_{e}P'" shows "P ≡⇩_{e}Q" proof - from finiteSummands assms show ?thesis proof(induct F=="summands P" arbitrary: P Q rule: finite_induct) case(empty P Q) have PEmpty: "{} = summands P" by fact moreover have "∀Q'∈summands Q. ∃P'∈summands P. Q' ≡⇩_{e}P'" by fact ultimately have QEmpty: "summands Q = {}" by simp have "P = 𝟬" proof - have "uhnf P" by fact with PEmpty show ?thesis by(blast intro: summandsZero') qed moreover have "Q = 𝟬" proof - have "uhnf Q" by fact with QEmpty show ?thesis by(blast intro: summandsZero') qed ultimately show ?case by(blast intro: Refl) next case(insert P' F P Q) have Phnf: "uhnf P" by fact have Qhnf: "uhnf Q" by fact have IH: "⋀P Q. ⟦F = summands P; uhnf P; uhnf Q; ∀P' ∈ summands P. ∃Q' ∈ summands Q. P' ≡⇩_{e}Q'; ∀Q' ∈ summands Q. ∃P' ∈ summands P. Q' ≡⇩_{e}P'⟧ ⟹ P ≡⇩_{e}Q" by fact have PeqQ: "∀P' ∈ summands P. ∃Q' ∈ summands Q. P' ≡⇩_{e}Q'" by fact have QeqP: "∀Q' ∈ summands Q. ∃P' ∈ summands P. Q' ≡⇩_{e}P'" by fact have PSumm: "insert P' F = summands P" by fact hence P'SummP: "P' ∈ summands P" by auto with Phnf obtain P'' where P'P''eqP: "P' ⊕ P'' ≡⇩_{e}P" and P''Summ: "summands P'' = summands P - {P'' |P''. P'' ∈ summands P ∧ P'' ≡⇩_{e}P'}" and P''hnf: "uhnf P''" by(blast dest: pullSummand) from PeqQ P'SummP obtain Q' where Q'SummQ: "Q' ∈ summands Q" and P'eqQ': "P' ≡⇩_{e}Q'" by blast from Q'SummQ Qhnf obtain Q'' where Q'Q''eqQ: "Q' ⊕ Q'' ≡⇩_{e}Q" and Q''Summ: "summands Q'' = summands Q - {Q'' |Q''. Q'' ∈ summands Q ∧ Q'' ≡⇩_{e}Q'}" and Q''hnf: "uhnf Q''" by(blast dest: pullSummand) have FeqP'': "F = summands P''" proof - have "P' ∉ F" by fact with P''Summ PSumm hnfSummandsRemove[OF P'SummP Phnf] show ?thesis by blast qed moreover have "∀P' ∈ summands P''. ∃Q' ∈ summands Q''. P' ≡⇩_{e}Q'" proof(rule ballI) fix P''' assume P'''Summ: "P''' ∈ summands P''" with P''Summ have "P''' ∈ summands P" by simp with PeqQ obtain Q''' where Q'''Summ: "Q''' ∈ summands Q" and P'''eqQ''': "P''' ≡⇩_{e}Q'''" by blast have "Q''' ∈ summands Q''" proof - from P'''Summ P''Summ have "¬(P''' ≡⇩_{e}P')" by simp with P'eqQ' P'''eqQ''' have "¬(Q''' ≡⇩_{e}Q')" by(blast intro: Trans Sym) with Q''Summ Q'''Summ show ?thesis by simp qed with P'''eqQ''' show "∃Q'∈summands Q''. P''' ≡⇩_{e}Q'" by blast qed moreover have "∀Q' ∈ summands Q''. ∃P' ∈ summands P''. Q' ≡⇩_{e}P'" proof(rule ballI) fix Q''' assume Q'''Summ: "Q''' ∈ summands Q''" with Q''Summ have "Q''' ∈ summands Q" by simp with QeqP obtain P''' where P'''Summ: "P''' ∈ summands P" and Q'''eqP''': "Q''' ≡⇩_{e}P'''" by blast have "P''' ∈ summands P''" proof - from Q'''Summ Q''Summ have "¬(Q''' ≡⇩_{e}Q')" by simp with P'eqQ' Q'''eqP''' have "¬(P''' ≡⇩_{e}P')" by(blast intro: Trans) with P''Summ P'''Summ show ?thesis by simp qed with Q'''eqP''' show "∃P'∈summands P''. Q''' ≡⇩_{e}P'" by blast qed ultimately have P''eqQ'': "P'' ≡⇩_{e}Q''" using P''hnf Q''hnf by(rule_tac IH) from P'P''eqP have "P ≡⇩_{e}P' ⊕ P''" by(rule Sym) moreover from P'eqQ' P''eqQ'' have "P' ⊕ P'' ≡⇩_{e}Q' ⊕ Q''" by(rule SumPres') ultimately show ?case using Q'Q''eqQ by(blast intro: Trans) qed qed lemma validSubst[simp]: fixes P :: pi and a :: name and b :: name and p :: pi shows "valid(P[a::=b]) = valid P"