(* Theory be Kirstin Peters *)+
−
+
−
theory Pi+
−
  imports "../Nominal2"+
−
begin+
−
+
−
atom_decl name+
−
+
−
subsection {* Capture-Avoiding Substitution of Names *}+
−
+
−
definition+
−
  subst_name :: "name \<Rightarrow> name \<Rightarrow> name \<Rightarrow> name" ("_[_:::=_]" [110, 110, 110] 110)+
−
where+
−
  "a[b:::=c] \<equiv> if (a = b) then c else a"+
−
+
−
declare subst_name_def[simp]+
−
+
−
lemma subst_name_mix_eqvt[eqvt]:+
−
  fixes p :: perm+
−
  and   a :: name+
−
  and   b :: name+
−
  and   c :: name+
−
+
−
  shows "p \<bullet> (a[b:::=c]) = (p \<bullet> a)[(p \<bullet> b):::=(p \<bullet> c)]"+
−
proof -+
−
  show ?thesis+
−
    by(auto)+
−
qed+
−
+
−
nominal_primrec+
−
  subst_name_list :: "name \<Rightarrow> (name \<times> name) list \<Rightarrow> name"+
−
where+
−
  "subst_name_list a [] = a"+
−
| "subst_name_list a ((b, c)#xs) = (if (a = b) then c else (subst_name_list a xs))"+
−
  apply(auto)+
−
  apply(subgoal_tac "\<And>p x r. subst_name_list_graph x r \<Longrightarrow> subst_name_list_graph (p \<bullet> x) (p \<bullet> r)")+
−
  unfolding eqvt_def+
−
  apply(rule allI)+
−
  apply(simp add: permute_fun_def)+
−
  apply(rule ext)+
−
  apply(rule ext)+
−
  apply(simp add: permute_bool_def)+
−
  apply(rule iffI)+
−
  apply(drule_tac x="p" in meta_spec)+
−
  apply(drule_tac x="- p \<bullet> x" in meta_spec)+
−
  apply(drule_tac x="- p \<bullet> xa" in meta_spec)+
−
  apply(simp)+
−
  apply(drule_tac x="-p" in meta_spec)+
−
  apply(drule_tac x="x" in meta_spec)+
−
  apply(drule_tac x="xa" in meta_spec)+
−
  apply(simp)+
−
  apply(erule subst_name_list_graph.induct)+
−
  apply(perm_simp)+
−
  apply(rule subst_name_list_graph.intros)+
−
  apply(perm_simp)+
−
  apply(rule subst_name_list_graph.intros)+
−
  apply(simp)+
−
  apply(rule_tac y="b" in list.exhaust)+
−
  by(auto)+
−
+
−
termination (eqvt)+
−
  by (lexicographic_order)+
−
+
−
+
−
section {* The Synchronous Pi-Calculus *}+
−
+
−
subsection {* Syntax: Synchronous, Monadic Pi-Calculus with n-ary, Mixed Choice *}+
−
+
−
nominal_datatype+
−
      guardedTerm_mix = Output name name piMix                     ("_!<_>\<onesuperior>._" [120, 120, 110] 110)+
−
                      | Input name b::name P::piMix  binds b in P  ("_?<_>\<onesuperior>._" [120, 120, 110] 110)+
−
                      | Tau piMix                                  ("<\<tau>\<onesuperior>>._" [110] 110)+
−
  and sumList_mix     = SumNil                                     ("\<zero>\<onesuperior>")+
−
                      | AddSummand guardedTerm_mix sumList_mix     (infixr "\<oplus>\<onesuperior>" 65)+
−
  and piMix           = Res a::name P::piMix         binds a in P  ("<\<nu>_>\<onesuperior>_" [100, 100] 100)+
−
                      | Par piMix piMix                            (infixr "\<parallel>\<onesuperior>" 85)+
−
                      | Match name name piMix                      ("[_\<frown>\<onesuperior>_]_" [120, 120, 110] 110)+
−
                      | Sum sumList_mix                            ("\<oplus>\<onesuperior>{_}" 90)+
−
                      | Rep name b::name P::piMix    binds b in P  ("\<infinity>_?<_>\<onesuperior>._" [120, 120, 110] 110)+
−
                      | Succ                                       ("succ\<onesuperior>")+
−
+
−
lemmas piMix_strong_induct  = guardedTerm_mix_sumList_mix_piMix.strong_induct+
−
lemmas piMix_fresh          = guardedTerm_mix_sumList_mix_piMix.fresh+
−
lemmas piMix_eq_iff         = guardedTerm_mix_sumList_mix_piMix.eq_iff+
−
lemmas piMix_distinct       = guardedTerm_mix_sumList_mix_piMix.distinct+
−
lemmas piMix_size           = guardedTerm_mix_sumList_mix_piMix.size+
−
+
−
subsection {* Alpha-Conversion Lemmata *}+
−
+
−
lemma alphaRes_mix:+
−
  fixes a :: name+
−
  and   P :: piMix+
−
  and   z :: name+
−
+
−
  assumes "atom z \<sharp> P"+
−
+
−
  shows "<\<nu>a>\<onesuperior>P = <\<nu>z>\<onesuperior>((atom a \<rightleftharpoons> atom z) \<bullet> P)"+
−
proof(cases "a = z")+
−
  assume "a = z"+
−
  thus ?thesis+
−
    by(simp)+
−
next+
−
  assume "a \<noteq> z"+
−
  thus ?thesis+
−
    using assms+
−
    by(simp add: piMix_eq_iff Abs1_eq_iff fresh_permute_left)+
−
qed+
−
+
−
lemma alphaInput_mix:+
−
  fixes a :: name+
−
  and   b :: name+
−
  and   P :: piMix+
−
  and   z :: name+
−
+
−
  assumes "atom z \<sharp> P"+
−
+
−
  shows "a?<b>\<onesuperior>.P = a?<z>\<onesuperior>.((atom b \<rightleftharpoons> atom z) \<bullet> P)"+
−
proof(cases "b = z")+
−
  assume "b = z"+
−
  thus ?thesis+
−
    by(simp)+
−
next+
−
  assume "b \<noteq> z"+
−
  thus ?thesis+
−
    using assms+
−
    by(simp add: piMix_eq_iff Abs1_eq_iff fresh_permute_left)+
−
qed+
−
+
−
lemma alphaRep_mix:+
−
  fixes a :: name+
−
  and   b :: name+
−
  and   P :: piMix+
−
  and   z :: name+
−
+
−
  assumes "atom z \<sharp> P"+
−
+
−
  shows "\<infinity>a?<b>\<onesuperior>.P = \<infinity>a?<z>\<onesuperior>.((atom b \<rightleftharpoons> atom z) \<bullet> P)"+
−
proof(cases "b = z")+
−
  assume "b = z"+
−
  thus ?thesis+
−
    by(simp)+
−
next+
−
  assume "b \<noteq> z"+
−
  thus ?thesis+
−
    using assms+
−
    by(simp add: piMix_eq_iff Abs1_eq_iff fresh_permute_left)+
−
qed+
−
+
−
subsection {* Capture-Avoiding Substitution of Names *}+
−
+
−
lemma testl:+
−
  assumes a: "\<exists>y. f = Inl y"+
−
  shows "(p \<bullet> (Sum_Type.Projl f)) = Sum_Type.Projl (p \<bullet> f)"+
−
using a by auto+
−
+
−
lemma testrr:+
−
  assumes a: "\<exists>y. f = Inr (Inr y)"+
−
  shows "(p \<bullet> (Sum_Type.Projr (Sum_Type.Projr f))) = Sum_Type.Projr (Sum_Type.Projr (p \<bullet> f))"+
−
using a by auto+
−
+
−
lemma testlr:+
−
  assumes a: "\<exists>y. f = Inr (Inl y)"+
−
  shows "(p \<bullet> (Sum_Type.Projl (Sum_Type.Projr f))) = Sum_Type.Projl (Sum_Type.Projr (p \<bullet> f))"+
−
using a by auto+
−
+
−
nominal_primrec (default "sum_case (\<lambda>x. Inl undefined) (sum_case (\<lambda>x. Inr (Inl undefined)) (\<lambda>x. Inr (Inr undefined)))")+
−
  subsGuard_mix :: "guardedTerm_mix \<Rightarrow> name \<Rightarrow> name \<Rightarrow> guardedTerm_mix"  ("_[_::=\<onesuperior>\<onesuperior>_]" [100, 100, 100] 100) and+
−
  subsList_mix  :: "sumList_mix \<Rightarrow> name \<Rightarrow> name \<Rightarrow> sumList_mix"          ("_[_::=\<onesuperior>\<twosuperior>_]" [100, 100, 100] 100) and+
−
  subs_mix      :: "piMix \<Rightarrow> name \<Rightarrow> name \<Rightarrow> piMix"                      ("_[_::=\<onesuperior>_]" [100, 100, 100] 100)+
−
where+
−
  "(a!<b>\<onesuperior>.P)[x::=\<onesuperior>\<onesuperior>y] = (a[x:::=y])!<(b[x:::=y])>\<onesuperior>.(P[x::=\<onesuperior>y])"+
−
| "\<lbrakk>atom b \<sharp> (x, y)\<rbrakk> \<Longrightarrow> (a?<b>\<onesuperior>.P)[x::=\<onesuperior>\<onesuperior>y] = (a[x:::=y])?<b>\<onesuperior>.(P[x::=\<onesuperior>y])"+
−
| "(<\<tau>\<onesuperior>>.P)[x::=\<onesuperior>\<onesuperior>y] = <\<tau>\<onesuperior>>.(P[x::=\<onesuperior>y])"+
−
| "(\<zero>\<onesuperior>)[x::=\<onesuperior>\<twosuperior>y] = \<zero>\<onesuperior>"+
−
| "(g \<oplus>\<onesuperior> xg)[x::=\<onesuperior>\<twosuperior>y] = (g[x::=\<onesuperior>\<onesuperior>y]) \<oplus>\<onesuperior> (xg[x::=\<onesuperior>\<twosuperior>y])"+
−
| "\<lbrakk>atom a \<sharp> (x, y)\<rbrakk> \<Longrightarrow> (<\<nu>a>\<onesuperior>P)[x::=\<onesuperior>y] = <\<nu>a>\<onesuperior>(P[x::=\<onesuperior>y])"+
−
| "(P \<parallel>\<onesuperior> Q)[x::=\<onesuperior>y] = (P[x::=\<onesuperior>y]) \<parallel>\<onesuperior> (Q[x::=\<onesuperior>y])"+
−
| "([a\<frown>\<onesuperior>b]P)[x::=\<onesuperior>y] = ([(a[x:::=y])\<frown>\<onesuperior>(b[x:::=y])](P[x::=\<onesuperior>y]))"+
−
| "(\<oplus>\<onesuperior>{xg})[x::=\<onesuperior>y] = \<oplus>\<onesuperior>{(xg[x::=\<onesuperior>\<twosuperior>y])}"+
−
| "\<lbrakk>atom b \<sharp> (x, y)\<rbrakk> \<Longrightarrow> (\<infinity>a?<b>\<onesuperior>.P)[x::=\<onesuperior>y] = \<infinity>(a[x:::=y])?<b>\<onesuperior>.(P[x::=\<onesuperior>y])"+
−
| "(succ\<onesuperior>)[x::=\<onesuperior>y] = succ\<onesuperior>"+
−
  apply(auto simp add: piMix_distinct piMix_eq_iff)+
−
  apply(subgoal_tac "\<And>p x r. subsGuard_mix_subsList_mix_subs_mix_graph x r \<Longrightarrow> subsGuard_mix_subsList_mix_subs_mix_graph (p \<bullet> x) (p \<bullet> r)")+
−
  unfolding eqvt_def+
−
  apply(rule allI)+
−
  apply(simp add: permute_fun_def)+
−
  apply(rule ext)+
−
  apply(rule ext)+
−
  apply(simp add: permute_bool_def)+
−
  apply(rule iffI)+
−
  apply(drule_tac x="p" in meta_spec)+
−
  apply(drule_tac x="- p \<bullet> x" in meta_spec)+
−
  apply(drule_tac x="- p \<bullet> xa" in meta_spec)+
−
  apply(simp)+
−
  apply(drule_tac x="-p" in meta_spec)+
−
  apply(drule_tac x="x" in meta_spec)+
−
  apply(drule_tac x="xa" in meta_spec)+
−
  apply(simp)+
−
  --"Equivariance"+
−
  apply(erule subsGuard_mix_subsList_mix_subs_mix_graph.induct)+
−
  apply(simp (no_asm_use) only: eqvts)+
−
  apply(subst testrr)+
−
  apply(erule subsGuard_mix_subsList_mix_subs_mix_graph.cases)+
−
  apply(blast)++
−
  apply(rule subsGuard_mix_subsList_mix_subs_mix_graph.intros)+
−
  apply(simp)+
−
  apply(simp (no_asm_use) only: eqvts)+
−
  apply(subst testrr)+
−
  apply(erule subsGuard_mix_subsList_mix_subs_mix_graph.cases)+
−
  apply(blast)++
−
  apply(rule subsGuard_mix_subsList_mix_subs_mix_graph.intros)+
−
  apply(simp only: atom_eqvt[symmetric] Pair_eqvt[symmetric] fresh_eqvt[symmetric] permute_bool_def)+
−
  apply(simp)+
−
  apply(simp (no_asm_use) only: eqvts)+
−
  apply(subst testrr)+
−
  apply(erule subsGuard_mix_subsList_mix_subs_mix_graph.cases)+
−
  apply(blast)++
−
  apply(rule subsGuard_mix_subsList_mix_subs_mix_graph.intros)+
−
  apply(simp)+
−
  apply(simp (no_asm_use) only: eqvts)+
−
  apply(rule subsGuard_mix_subsList_mix_subs_mix_graph.intros)+
−
  apply(simp (no_asm_use) only: eqvts)  +
−
  apply(subst testl)+
−
  apply(erule subsGuard_mix_subsList_mix_subs_mix_graph.cases)+
−
  apply(blast)++
−
  apply(subst testlr)+
−
  apply(rotate_tac 2)+
−
  apply(erule subsGuard_mix_subsList_mix_subs_mix_graph.cases)+
−
  apply(blast)++
−
  apply(perm_simp)+
−
  apply(rule subsGuard_mix_subsList_mix_subs_mix_graph.intros)+
−
  apply(blast)+
−
  apply(blast)+
−
  apply(simp (no_asm_use) only: eqvts)+
−
  apply(subst testrr)+
−
  apply(erule subsGuard_mix_subsList_mix_subs_mix_graph.cases)+
−
  apply(blast)++
−
  apply(rule subsGuard_mix_subsList_mix_subs_mix_graph.intros)+
−
  apply(simp only: atom_eqvt[symmetric] Pair_eqvt[symmetric] fresh_eqvt[symmetric] permute_bool_def)+
−
  apply(simp)+
−
  apply(simp (no_asm_use) only: eqvts)+
−
  apply(subst testrr)+
−
  apply(erule subsGuard_mix_subsList_mix_subs_mix_graph.cases)+
−
  apply(blast)++
−
  apply(subst testrr)+
−
  apply(rotate_tac 2)+
−
  apply(erule subsGuard_mix_subsList_mix_subs_mix_graph.cases)+
−
  apply(blast)++
−
  apply(perm_simp)+
−
  apply(rule subsGuard_mix_subsList_mix_subs_mix_graph.intros)+
−
  apply(blast)+
−
  apply(blast)+
−
  apply(simp (no_asm_use) only: eqvts)+
−
  apply(subst testrr)+
−
  apply(erule subsGuard_mix_subsList_mix_subs_mix_graph.cases)+
−
  apply(blast)++
−
  apply(rule subsGuard_mix_subsList_mix_subs_mix_graph.intros)+
−
  apply(blast)+
−
  apply(simp (no_asm_use) only: eqvts)+
−
  apply(subst testlr)+
−
  apply(erule subsGuard_mix_subsList_mix_subs_mix_graph.cases)+
−
  apply(blast)++
−
  apply(rule subsGuard_mix_subsList_mix_subs_mix_graph.intros)+
−
  apply(blast)+
−
  apply(simp (no_asm_use) only: eqvts)+
−
  apply(subst testrr)+
−
  apply(erule subsGuard_mix_subsList_mix_subs_mix_graph.cases)+
−
  apply(blast)++
−
  apply(rule subsGuard_mix_subsList_mix_subs_mix_graph.intros)+
−
  apply(simp only: atom_eqvt[symmetric] Pair_eqvt[symmetric] fresh_eqvt[symmetric] permute_bool_def)+
−
  apply(blast)+
−
  apply(perm_simp)+
−
  apply(rule subsGuard_mix_subsList_mix_subs_mix_graph.intros)+
−
  --"Covered all cases"+
−
  apply(case_tac x)+
−
  apply(simp)+
−
  apply(case_tac a)+
−
  apply(simp)+
−
  apply (rule_tac y="aa" and c="(b, c)" in guardedTerm_mix_sumList_mix_piMix.strong_exhaust(1))+
−
  apply(blast)+
−
  apply(auto simp add: fresh_star_def)[1]+
−
  apply(blast)+
−
  apply(simp)+
−
  apply(blast)+
−
  apply(simp)+
−
  apply(case_tac b)+
−
  apply(simp)+
−
  apply(case_tac a)+
−
  apply(simp)+
−
  apply (rule_tac ya="aa" in guardedTerm_mix_sumList_mix_piMix.strong_exhaust(2))+
−
  apply(blast)+
−
  apply(blast)+
−
  apply(simp)+
−
  apply(case_tac ba)+
−
  apply(simp)+
−
  apply (rule_tac yb="a" and c="(bb,c)" in guardedTerm_mix_sumList_mix_piMix.strong_exhaust(3))+
−
  apply(auto simp add: fresh_star_def)[1]+
−
  apply(blast)+
−
  apply(blast)+
−
  apply(blast)+
−
  apply(auto simp add: fresh_star_def)[1]+
−
  apply(blast)+
−
  apply(simp)+
−
  apply(blast)+
−
  --"compatibility"+
−
  apply (simp add: meta_eq_to_obj_eq[OF subs_mix_def, symmetric, unfolded fun_eq_iff])+
−
  apply (subgoal_tac "eqvt_at (\<lambda>(a, b, c). subs_mix a b c) (P, xa, ya)")+
−
  apply (thin_tac "eqvt_at subsGuard_mix_subsList_mix_subs_mix_sumC (Inr (Inr (P, xa, ya)))")+
−
  apply (thin_tac "eqvt_at subsGuard_mix_subsList_mix_subs_mix_sumC (Inr (Inr (Pa, xa, ya)))")+
−
  prefer 2+
−
  apply (simp add: eqvt_at_def subs_mix_def)+
−
  apply rule+
−
  apply (subst testrr)+
−
  apply (simp add: subsGuard_mix_subsList_mix_subs_mix_sumC_def)+
−
  apply (simp add: THE_default_def)+
−
apply (case_tac "Ex1 (subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (P, xa, ya))))")+
−
apply simp_all[2]+
−
apply auto[1]+
−
apply (erule_tac x="x" in allE)+
−
apply simp+
−
apply (thin_tac "\<forall>p\<Colon>perm.+
−
           p \<bullet> The (subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (P, xa, ya)))) =+
−
           (if \<exists>!x\<Colon>guardedTerm_mix + sumList_mix + piMix.+
−
                  subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (p \<bullet> P, p \<bullet> xa, p \<bullet> ya))) x+
−
            then THE x\<Colon>guardedTerm_mix + sumList_mix + piMix.+
−
                    subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (p \<bullet> P, p \<bullet> xa, p \<bullet> ya))) x+
−
            else Inr (Inr undefined))")+
−
apply (thin_tac "\<forall>p\<Colon>perm.+
−
           p \<bullet> (if \<exists>!x\<Colon>guardedTerm_mix + sumList_mix + piMix.+
−
                      subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (Pa, xa, ya))) x+
−
                then THE x\<Colon>guardedTerm_mix + sumList_mix + piMix.+
−
                        subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (Pa, xa, ya))) x+
−
                else Inr (Inr undefined)) =+
−
           (if \<exists>!x\<Colon>guardedTerm_mix + sumList_mix + piMix.+
−
                  subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (p \<bullet> Pa, p \<bullet> xa, p \<bullet> ya))) x+
−
            then THE x\<Colon>guardedTerm_mix + sumList_mix + piMix.+
−
                    subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (p \<bullet> Pa, p \<bullet> xa, p \<bullet> ya))) x+
−
            else Inr (Inr undefined))")+
−
apply (thin_tac "atom b \<sharp> (xa, ya)")+
−
apply (thin_tac "atom ba \<sharp> (xa, ya)")+
−
apply (thin_tac "[[atom b]]lst. P = [[atom ba]]lst. Pa")+
−
apply(cases rule: subsGuard_mix_subsList_mix_subs_mix_graph.cases)+
−
apply assumption+
−
apply (metis Inr_not_Inl)+
−
apply (metis Inr_not_Inl)+
−
apply (metis Inr_not_Inl)+
−
apply (metis Inr_inject Inr_not_Inl)+
−
apply (metis Inr_inject Inr_not_Inl)+
−
apply (rule_tac x="<\<nu>a>\<onesuperior>Sum_Type.Projr+
−
                            (Sum_Type.Projr+
−
                              (subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inr (Pb, xb, y)))))" in exI)+
−
apply clarify+
−
apply (rule the1_equality)+
−
apply blast apply assumption+
−
apply (rule_tac x="Sum_Type.Projr+
−
                       (Sum_Type.Projr (subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inr (Pb, xb, y))))) \<parallel>\<onesuperior>+
−
                      Sum_Type.Projr+
−
                       (Sum_Type.Projr (subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inr (Q, xb, y)))))" in exI)+
−
apply clarify+
−
apply (rule the1_equality)+
−
apply blast apply assumption+
−
apply (rule_tac x="[(a[xb:::=y])\<frown>\<onesuperior>(bb[xb:::=y])]Sum_Type.Projr+
−
                                                    (Sum_Type.Projr+
−
(subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inr (Pb, xb, y)))))" in exI)+
−
apply clarify+
−
apply (rule the1_equality)+
−
apply blast apply assumption+
−
apply (rule_tac x="\<oplus>\<onesuperior>{Sum_Type.Projl+
−
                          (Sum_Type.Projr+
−
                            (subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inl (xg, xb, y)))))}" in exI)+
−
apply clarify+
−
apply (rule the1_equality)+
−
apply blast apply assumption+
−
apply (rule_tac x="\<infinity>(a[xb:::=y])?<bb>\<onesuperior>.Sum_Type.Projr+
−
                                           (Sum_Type.Projr+
−
                                             (subsGuard_mix_subsList_mix_subs_mix_sum+
−
                                               (Inr (Inr (Pb, xb, y)))))" in exI)+
−
apply clarify+
−
apply (rule the1_equality)+
−
apply blast apply assumption+
−
apply (rule_tac x="succ\<onesuperior>" in exI)+
−
apply clarify+
−
apply (rule the1_equality)+
−
apply blast apply assumption+
−
apply simp+
−
(* Here the only real goal compatibility is left *)+
−
  apply (erule Abs_lst1_fcb)+
−
  apply (simp_all add: Abs_fresh_iff fresh_fun_eqvt_app)+
−
  apply (subgoal_tac "atom ba \<sharp> (\<lambda>(a, x, y). subs_mix a x y) (P, xa, ya)")+
−
  apply simp+
−
  apply (erule fresh_eqvt_at)+
−
  apply (simp_all add: fresh_Pair finite_supp eqvts eqvt_at_def fresh_Pair swap_fresh_fresh)+
−
  done+
−
+
−
termination (eqvt)+
−
  by (lexicographic_order)+
−
+
−
lemma forget_mix:+
−
  fixes g  :: guardedTerm_mix+
−
  and   xg :: sumList_mix+
−
  and   P  :: piMix+
−
  and   x  :: name+
−
  and   y  :: name+
−
+
−
  shows "atom x \<sharp> g \<longrightarrow> g[x::=\<onesuperior>\<onesuperior>y] = g"+
−
  and   "atom x \<sharp> xg \<longrightarrow> xg[x::=\<onesuperior>\<twosuperior>y] = xg"+
−
  and   "atom x \<sharp> P \<longrightarrow> P[x::=\<onesuperior>y] = P"+
−
proof -+
−
  show  "atom x \<sharp> g \<longrightarrow> g[x::=\<onesuperior>\<onesuperior>y] = g"+
−
  and   "atom x \<sharp> xg \<longrightarrow> xg[x::=\<onesuperior>\<twosuperior>y] = xg"+
−
  and   "atom x \<sharp> P \<longrightarrow> P[x::=\<onesuperior>y] = P"+
−
    using assms+
−
    apply(nominal_induct g and xg and P avoiding: x y rule: piMix_strong_induct)+
−
    by(auto simp add: piMix_eq_iff piMix_fresh fresh_at_base)+
−
qed+
−
+
−
lemma fresh_fact_mix:+
−
  fixes g  :: guardedTerm_mix+
−
  and   xg :: sumList_mix+
−
  and   P  :: piMix+
−
  and   x  :: name+
−
  and   y  :: name+
−
  and   z  :: name+
−
+
−
  assumes "atom z \<sharp> y"+
−
+
−
  shows "(z = x \<or> atom z \<sharp> g) \<longrightarrow> atom z \<sharp> g[x::=\<onesuperior>\<onesuperior>y]"+
−
  and   "(z = x \<or> atom z \<sharp> xg) \<longrightarrow> atom z \<sharp> xg[x::=\<onesuperior>\<twosuperior>y]"+
−
  and   "(z = x \<or> atom z \<sharp> P) \<longrightarrow> atom z \<sharp> P[x::=\<onesuperior>y]"+
−
proof -+
−
  show  "(z = x \<or> atom z \<sharp> g) \<longrightarrow> atom z \<sharp> g[x::=\<onesuperior>\<onesuperior>y]"+
−
  and   "(z = x \<or> atom z \<sharp> xg) \<longrightarrow> atom z \<sharp> xg[x::=\<onesuperior>\<twosuperior>y]"+
−
  and   "(z = x \<or> atom z \<sharp> P) \<longrightarrow> atom z \<sharp> P[x::=\<onesuperior>y]"+
−
    using assms+
−
    apply(nominal_induct g and xg and P avoiding: x y z rule: piMix_strong_induct)+
−
    by(auto simp add: piMix_fresh fresh_at_base)+
−
qed+
−
+
−
lemma substitution_lemma_mix:+
−
  fixes g  :: guardedTerm_mix+
−
  and   xg :: sumList_mix+
−
  and   P  :: piMix+
−
  and   s  :: name+
−
  and   u  :: name+
−
  and   x  :: name+
−
  and   y  :: name+
−
+
−
  assumes "x \<noteq> y"+
−
  and     "atom x \<sharp> u"+
−
+
−
  shows "g[x::=\<onesuperior>\<onesuperior>s][y::=\<onesuperior>\<onesuperior>u] = g[y::=\<onesuperior>\<onesuperior>u][x::=\<onesuperior>\<onesuperior>s[y:::=u]]"+
−
  and   "xg[x::=\<onesuperior>\<twosuperior>s][y::=\<onesuperior>\<twosuperior>u] = xg[y::=\<onesuperior>\<twosuperior>u][x::=\<onesuperior>\<twosuperior>s[y:::=u]]"+
−
  and   "P[x::=\<onesuperior>s][y::=\<onesuperior>u] = P[y::=\<onesuperior>u][x::=\<onesuperior>s[y:::=u]]"+
−
proof -+
−
  show  "g[x::=\<onesuperior>\<onesuperior>s][y::=\<onesuperior>\<onesuperior>u] = g[y::=\<onesuperior>\<onesuperior>u][x::=\<onesuperior>\<onesuperior>s[y:::=u]]"+
−
  and   "xg[x::=\<onesuperior>\<twosuperior>s][y::=\<onesuperior>\<twosuperior>u] = xg[y::=\<onesuperior>\<twosuperior>u][x::=\<onesuperior>\<twosuperior>s[y:::=u]]"+
−
  and   "P[x::=\<onesuperior>s][y::=\<onesuperior>u] = P[y::=\<onesuperior>u][x::=\<onesuperior>s[y:::=u]]"+
−
    using assms+
−
    apply(nominal_induct g and xg and P avoiding: x y s u rule: piMix_strong_induct)+
−
    apply(simp_all add: fresh_fact_mix forget_mix)+
−
    by(auto simp add: fresh_at_base)+
−
qed+
−
+
−
lemma perm_eq_subst_mix:+
−
  fixes g  :: guardedTerm_mix+
−
  and   xg :: sumList_mix+
−
  and   P  :: piMix+
−
  and   x  :: name+
−
  and   y  :: name+
−
+
−
  shows "atom y \<sharp> g \<longrightarrow> (atom x \<rightleftharpoons> atom y) \<bullet> g = g[x::=\<onesuperior>\<onesuperior>y]"+
−
  and   "atom y \<sharp> xg \<longrightarrow> (atom x \<rightleftharpoons> atom y) \<bullet> xg = xg[x::=\<onesuperior>\<twosuperior>y]"+
−
  and   "atom y \<sharp> P \<longrightarrow> (atom x \<rightleftharpoons> atom y) \<bullet> P = P[x::=\<onesuperior>y]"+
−
proof -+
−
  show  "atom y \<sharp> g \<longrightarrow> (atom x \<rightleftharpoons> atom y) \<bullet> g = g[x::=\<onesuperior>\<onesuperior>y]"+
−
  and   "atom y \<sharp> xg \<longrightarrow> (atom x \<rightleftharpoons> atom y) \<bullet> xg = xg[x::=\<onesuperior>\<twosuperior>y]"+
−
  and   "atom y \<sharp> P \<longrightarrow> (atom x \<rightleftharpoons> atom y) \<bullet> P = P[x::=\<onesuperior>y]"+
−
    apply(nominal_induct g and xg and P avoiding: x y rule: piMix_strong_induct)+
−
    by(auto simp add: piMix_fresh fresh_at_base)+
−
qed+
−
+
−
lemma subst_id_mix:+
−
  fixes g  :: guardedTerm_mix+
−
  and   xg :: sumList_mix+
−
  and   P  :: piMix+
−
  and   x  :: name+
−
+
−
  shows "g[x::=\<onesuperior>\<onesuperior>x] = g" and "xg[x::=\<onesuperior>\<twosuperior>x] = xg" and "P[x::=\<onesuperior>x] = P"+
−
proof -+
−
  show  "g[x::=\<onesuperior>\<onesuperior>x] = g" and "xg[x::=\<onesuperior>\<twosuperior>x] = xg" and "P[x::=\<onesuperior>x] = P"+
−
    apply(nominal_induct g and xg and P avoiding: x rule: piMix_strong_induct)+
−
    by(auto)+
−
qed+
−
+
−
lemma alphaRes_subst_mix:+
−
  fixes a :: name+
−
  and   P :: piMix+
−
  and   z :: name+
−
+
−
  assumes "atom z \<sharp> P"+
−
+
−
  shows "<\<nu>a>\<onesuperior>P = <\<nu>z>\<onesuperior>(P[a::=\<onesuperior>z])"+
−
proof(cases "a = z")+
−
  assume "a = z"+
−
  thus ?thesis+
−
    by(simp add: subst_id_mix)+
−
next+
−
  assume "a \<noteq> z"+
−
  thus ?thesis+
−
    using assms+
−
    by(simp add: alphaRes_mix perm_eq_subst_mix)+
−
qed+
−
+
−
lemma alphaInput_subst_mix:+
−
  fixes a :: name+
−
  and   b :: name+
−
  and   P :: piMix+
−
  and   z :: name+
−
+
−
  assumes "atom z \<sharp> P"+
−
+
−
  shows "a?<b>\<onesuperior>.P = a?<z>\<onesuperior>.(P[b::=\<onesuperior>z])"+
−
proof(cases "b = z")+
−
  assume "b = z"+
−
  thus ?thesis+
−
    by(simp add: subst_id_mix)+
−
next+
−
  assume "b \<noteq> z"+
−
  thus ?thesis+
−
    using assms+
−
    by(simp add: alphaInput_mix perm_eq_subst_mix)+
−
qed+
−
+
−
lemma alphaRep_subst_mix:+
−
  fixes a :: name+
−
  and   b :: name+
−
  and   P :: piMix+
−
  and   z :: name+
−
+
−
  assumes "atom z \<sharp> P"+
−
+
−
  shows "\<infinity>a?<b>\<onesuperior>.P = \<infinity>a?<z>\<onesuperior>.(P[b::=\<onesuperior>z])"+
−
proof(cases "b = z")+
−
  assume "b = z"+
−
  thus ?thesis+
−
    by(simp add: subst_id_mix)+
−
next+
−
  assume "b \<noteq> z"+
−
  thus ?thesis+
−
    using assms+
−
    by(simp add: alphaRep_mix perm_eq_subst_mix)+
−
qed+
−
+
−
inductive+
−
  fresh_list_guard_mix :: "name list \<Rightarrow> guardedTerm_mix \<Rightarrow> bool"+
−
where+
−
  "fresh_list_guard_mix [] g"+
−
| "\<lbrakk>atom n \<sharp> g; fresh_list_guard_mix xn g\<rbrakk> \<Longrightarrow> fresh_list_guard_mix (n#xn) g"+
−
+
−
equivariance fresh_list_guard_mix+
−
nominal_inductive fresh_list_guard_mix+
−
  done+
−
+
−
inductive+
−
  fresh_list_sumList_mix :: "name list \<Rightarrow> sumList_mix \<Rightarrow> bool"+
−
where+
−
  "fresh_list_sumList_mix [] xg"+
−
| "\<lbrakk>atom n \<sharp> xg; fresh_list_sumList_mix xn xg\<rbrakk> \<Longrightarrow> fresh_list_sumList_mix (n#xn) xg"+
−
+
−
equivariance fresh_list_sumList_mix+
−
nominal_inductive fresh_list_sumList_mix+
−
  done+
−
+
−
inductive+
−
  fresh_list_mix :: "name list \<Rightarrow> piMix \<Rightarrow> bool"+
−
where+
−
  "fresh_list_mix [] P"+
−
| "\<lbrakk>atom n \<sharp> P; fresh_list_mix xn P\<rbrakk> \<Longrightarrow> fresh_list_mix (n#xn) P"+
−
+
−
equivariance fresh_list_mix+
−
nominal_inductive fresh_list_mix+
−
  done+
−
+
−
end+
−