388 nominal_primrec 

   389   substn :: "trm \<Rightarrow> name   \<Rightarrow> coname \<Rightarrow> trm \<Rightarrow> trm" ("_{_:=<_>._}" [100,100,100,100] 100) 

   390 where

   391   "(Ax x a){y:=<c>.P} = (if x=y then Cut <c>.P (y).Ax y a else Ax x a)" 

   392 | "\<lbrakk>atom a \<sharp> (c, P); atom x \<sharp> (y, P)\<rbrakk> \<Longrightarrow> (Cut <a>.M (x).N){y:=<c>.P} = 

   393     (if M=Ax y a then Cut <c>.P (x).(N{y:=<c>.P}) else Cut <a>.(M{y:=<c>.P}) (x).(N{y:=<c>.P}))" 

   394 | "atom x\<sharp> (y, P) \<Longrightarrow> (NotR (x).M a){y:=<c>.P} = NotR (x).(M{y:=<c>.P}) a" 

   395 | "\<lbrakk>atom a\<sharp> (c, P); atom x' \<sharp> (M, y, P)\<rbrakk> \<Longrightarrow> (NotL <a>.M x){y:=<c>.P} = 

   396     (if x=y then Cut <c>.P (x').NotL <a>.(M{y:=<c>.P}) x' else NotL <a>.(M{y:=<c>.P}) x)"

   397 | "\<lbrakk>atom a \<sharp> (c, P); atom b \<sharp> (c, P)\<rbrakk> \<Longrightarrow> 

   398     (AndR <a>.M <b>.N d){y:=<c>.P} = AndR <a>.(M{y:=<c>.P}) <b>.(N{y:=<c>.P}) d" 

   399 | "atom x \<sharp> (y, P) \<Longrightarrow> (AndL1 (x).M z){y:=<c>.P} = 

   400     (if z=y then Cut <c>.P (z').AndL1 (x).(M{y:=<c>.P}) z' else AndL1 (x).(M{y:=<c>.P}) z)"

   401 | "atom x \<sharp> (y, P) \<Longrightarrow> (AndL2 (x).M z){y:=<c>.P} = 

   402     (if z=y then Cut <c>.P (z').AndL2 (x).(M{y:=<c>.P}) z' else AndL2 (x).(M{y:=<c>.P}) z)"

   403 | "atom a \<sharp> (c, P) \<Longrightarrow> (OrR1 <a>.M b){y:=<c>.P} = OrR1 <a>.(M{y:=<c>.P}) b"

   404 | "atom a \<sharp> (c, P) \<Longrightarrow> (OrR2 <a>.M b){y:=<c>.P} = OrR2 <a>.(M{y:=<c>.P}) b"

   405 | "\<lbrakk>atom x \<sharp> (y, P); atom u \<sharp> (y, P)\<rbrakk> \<Longrightarrow> (OrL (x).M (u).N z){y:=<c>.P} = 

   406      (if z=y then Cut <c>.P (z').OrL (x).(M{y:=<c>.P}) (u).(N{y:=<c>.P}) z' 

   407       else OrL (x).(M{y:=<c>.P}) (u).(N{y:=<c>.P}) z)"

   408 | "\<lbrakk>atom a \<sharp> (c, P); atom x \<sharp> (y, P)\<rbrakk> \<Longrightarrow> (ImpR (x).<a>.M b){y:=<c>.P} = ImpR (x).<a>.(M{y:=<c>.P}) b"

   409 | "\<lbrakk>atom a \<sharp> (c, P); atom x \<sharp> (y, P)\<rbrakk> \<Longrightarrow> (ImpL <a>.M (x).N z){y:=<c>.P} = 

   410      (if y=z then Cut <c>.P (z').ImpL <a>.(M{y:=<c>.P}) (x).(N{y:=<c>.P}) z' 

   411       else ImpL <a>.(M{y:=<c>.P}) (x).(N{y:=<c>.P}) z)"

   412   apply(simp only: eqvt_def)

   413   apply(simp only: substn_graph_def)

   414   apply (rule, perm_simp, rule)

   415   apply(rule TrueI)

   416   -- "covered all cases"

   417   apply(case_tac x)

   418   apply(rule_tac y="a" and c="(b, c, d)" in trm.strong_exhaust)

   419   apply (simp_all add: fresh_star_def fresh_Pair)[12]

   420   apply(metis)+

   421   apply(subgoal_tac "\<exists>x'::name. atom x' \<sharp> (trm, b, d)")

   422   apply(auto simp add: fresh_Pair)[1]

   423   apply(metis)+

   424   apply(subgoal_tac "\<exists>x'::name. atom x' \<sharp> (trm, b, d)")

   425   apply(auto simp add: fresh_Pair)[1]

   426   apply(rule obtain_fresh)

   427   apply(auto)[1]

   428   apply(metis)+

   429   -- "compatibility"

   430   apply(all_trivials)

   431   apply(simp)

   432   oops

   433