theory Classical
imports "../Nominal2"
begin


(* example from Urban's PhD *)

atom_decl name
atom_decl coname

nominal_datatype trm =
  Ax "name" "coname"
| Cut c::"coname" t1::"trm" n::"name" t2::"trm"             binds n in t1, binds c in t2  
     ("Cut <_>._ '(_')._" [100,100,100,100] 100)
| NotR n::"name" t::"trm" "coname"                            binds n in t
     ("NotR '(_')._ _" [100,100,100] 100)
| NotL c::"coname" t::"trm" "name"                            binds c in t   
     ("NotL <_>._ _" [100,100,100] 100)
| AndR c1::"coname" t1::"trm" c2::"coname" t2::"trm" "coname" binds c1 in t1, binds c2 in t2
     ("AndR <_>._ <_>._ _" [100,100,100,100,100] 100)
| AndL1 n::"name" t::"trm" "name"                             binds n in t
     ("AndL1 '(_')._ _" [100,100,100] 100)
| AndL2 n::"name" t::"trm" "name"                             binds n in t
     ("AndL2 '(_')._ _" [100,100,100] 100)
| OrR1 c::"coname" t::"trm" "coname"                          binds c in t             
     ("OrR1 <_>._ _" [100,100,100] 100)
| OrR2 c::"coname" t::"trm" "coname"                          binds c in t     
     ("OrR2 <_>._ _" [100,100,100] 100)
| OrL n1::"name" t1::"trm" n2::"name" t2::"trm" "name"        binds n1 in t1, binds n2 in t2       
     ("OrL '(_')._ '(_')._ _" [100,100,100,100,100] 100)
| ImpL c::"coname" t1::"trm" n::"name" t2::"trm" "name"       binds c in t1, binds n in t2
     ("ImpL <_>._ '(_')._ _" [100,100,100,100,100] 100)
| ImpR n::"name" c::"coname" t::"trm" "coname"                binds n c in t
     ("ImpR '(_').<_>._ _" [100,100,100,100] 100)

thm trm.distinct
thm trm.induct
thm trm.exhaust
thm trm.strong_exhaust
thm trm.strong_exhaust[simplified]
thm trm.fv_defs
thm trm.bn_defs
thm trm.perm_simps
thm trm.eq_iff
thm trm.fv_bn_eqvt
thm trm.size_eqvt
thm trm.supp
thm trm.supp[simplified]

nominal_primrec 
  crename :: "trm \<Rightarrow> coname \<Rightarrow> coname \<Rightarrow> trm"  ("_[_\<turnstile>c>_]" [100,100,100] 100) 
where
  "(Ax x a)[d\<turnstile>c>e] = (if a=d then Ax x e else Ax x a)" 
| "atom a \<sharp> (d, e) \<Longrightarrow> (Cut <a>.M (x).N)[d\<turnstile>c>e] = Cut <a>.(M[d\<turnstile>c>e]) (x).(N[d\<turnstile>c>e])" 
| "(NotR (x).M a)[d\<turnstile>c>e] = (if a=d then NotR (x).(M[d\<turnstile>c>e]) e else NotR (x).(M[d\<turnstile>c>e]) a)" 
| "atom a \<sharp> (d, e) \<Longrightarrow> (NotL <a>.M x)[d\<turnstile>c>e] = (NotL <a>.(M[d\<turnstile>c>e]) x)" 
| "\<lbrakk>atom a \<sharp> (d, e); atom b \<sharp> (d, e)\<rbrakk> \<Longrightarrow> (AndR <a>.M <b>.N c)[d\<turnstile>c>e] = 
          (if c=d then AndR <a>.(M[d\<turnstile>c>e]) <b>.(N[d \<turnstile>c>e]) e else AndR <a>.(M[d\<turnstile>c>e]) <b>.(N[d\<turnstile>c>e]) c)" 
| "(AndL1 (x).M y)[d\<turnstile>c>e] = AndL1 (x).(M[d\<turnstile>c>e]) y"
| "(AndL2 (x).M y)[d\<turnstile>c>e] = AndL2 (x).(M[d\<turnstile>c>e]) y"
| "atom a \<sharp> (d, e) \<Longrightarrow> (OrR1 <a>.M b)[d\<turnstile>c>e] = 
          (if b=d then OrR1 <a>.(M[d\<turnstile>c>e]) e else OrR1 <a>.(M[d\<turnstile>c>e]) b)"
| "atom a \<sharp> (d, e) \<Longrightarrow> (OrR2 <a>.M b)[d\<turnstile>c>e] = 
          (if b=d then OrR2 <a>.(M[d\<turnstile>c>e]) e else OrR2 <a>.(M[d\<turnstile>c>e]) b)"
| "(OrL (x).M (y).N z)[d\<turnstile>c>e] = OrL (x).(M[d\<turnstile>c>e]) (y).(N[d\<turnstile>c>e]) z"
| "atom a \<sharp> (d, e) \<Longrightarrow> (ImpR (x).<a>.M b)[d\<turnstile>c>e] = 
          (if b=d then ImpR (x).<a>.(M[d\<turnstile>c>e]) e else ImpR (x).<a>.(M[d\<turnstile>c>e]) b)"
| "atom a \<sharp> (d, e) \<Longrightarrow> (ImpL <a>.M (x).N y)[d\<turnstile>c>e] = ImpL <a>.(M[d\<turnstile>c>e]) (x).(N[d\<turnstile>c>e]) y"
  apply(simp only: eqvt_def)
  apply(simp only: crename_graph_def)
  apply (rule, perm_simp, rule)
  apply(rule TrueI)
  -- "covered all cases"
  apply(case_tac x)
  apply(rule_tac y="a" and c="(b, c)" in trm.strong_exhaust)
  apply (simp_all add: fresh_star_def)[12]
  apply(metis)+
  -- "compatibility"
  apply(all_trivials)
  apply(simp_all)
  apply(rule conjI)
  apply(elim conjE)
  apply(erule_tac c="(da,ea)" in Abs_lst1_fcb2)
  apply(simp add: Abs_fresh_iff)
  apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
  apply(elim conjE)
  apply(erule_tac c="(da,ea)" in Abs_lst1_fcb2)
  apply(simp add: Abs_fresh_iff)
  apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
  apply(elim conjE)
  apply(subgoal_tac "eqvt_at crename_sumC (M, da, ea)")
  apply(subgoal_tac "eqvt_at crename_sumC (Ma, da, ea)")
  apply(erule Abs_lst1_fcb2)
  apply(simp add: Abs_fresh_iff)
  apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
  apply(blast)
  apply(blast)
  apply(elim conjE)
  apply(erule_tac c="(da,ea)" in Abs_lst1_fcb2)
  apply(simp add: Abs_fresh_iff)
  apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
  apply(rule conjI)
  apply(elim conjE)
  apply(subgoal_tac "eqvt_at crename_sumC (M, da, ea)")
  apply(subgoal_tac "eqvt_at crename_sumC (Ma, da, ea)")
  apply(erule Abs_lst1_fcb2)
  apply(simp add: Abs_fresh_iff)
  apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
  apply(blast)
  apply(blast)
  apply(erule conjE)+
  apply(subgoal_tac "eqvt_at crename_sumC (N, da, ea)")
  apply(subgoal_tac "eqvt_at crename_sumC (Na, da, ea)")
  apply(erule Abs_lst1_fcb2)
  apply(simp add: Abs_fresh_iff)
  apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
  apply(blast)
  apply(blast)
  apply(elim conjE)
  apply(erule_tac c="(da,ea)" in Abs_lst1_fcb2)
  apply(simp add: Abs_fresh_iff)
  apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
  apply(elim conjE)
  apply(erule_tac c="(da,ea)" in Abs_lst1_fcb2)
  apply(simp add: Abs_fresh_iff)
  apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
  apply(elim conjE)
  apply(subgoal_tac "eqvt_at crename_sumC (M, da, ea)")
  apply(subgoal_tac "eqvt_at crename_sumC (Ma, da, ea)")
  apply(erule Abs_lst1_fcb2)
  apply(simp add: Abs_fresh_iff)
  apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
  apply(blast)
  apply(blast)
  apply(erule conjE)+
  apply(subgoal_tac "eqvt_at crename_sumC (M, da, ea)")
  apply(subgoal_tac "eqvt_at crename_sumC (Ma, da, ea)")
  apply(erule Abs_lst1_fcb2)
  apply(simp add: Abs_fresh_iff)
  apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
  apply(blast)
  apply(blast)
  apply(rule conjI)
  apply(erule conjE)+
  apply(subgoal_tac "eqvt_at crename_sumC (M, da, ea)")
  apply(subgoal_tac "eqvt_at crename_sumC (Ma, da, ea)")
  apply(erule Abs_lst1_fcb2)
  apply(simp add: Abs_fresh_iff)
  apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
  apply(blast)
  apply(blast)
  apply(erule conjE)+
  apply(subgoal_tac "eqvt_at crename_sumC (N, da, ea)")
  apply(subgoal_tac "eqvt_at crename_sumC (Na, da, ea)")
  apply(erule Abs_lst1_fcb2)
  apply(simp add: Abs_fresh_iff)
  apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
  apply(blast)
  apply(blast)
  defer
  apply(erule conjE)+
  apply(rule conjI)
  apply(subgoal_tac "eqvt_at crename_sumC (M, da, ea)")
  apply(subgoal_tac "eqvt_at crename_sumC (Ma, da, ea)")
  apply(erule Abs_lst1_fcb2)
  apply(simp add: Abs_fresh_iff)
  apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
  apply(blast)
  apply(blast)  
  apply(subgoal_tac "eqvt_at crename_sumC (N, da, ea)")
  apply(subgoal_tac "eqvt_at crename_sumC (Na, da, ea)")
  apply(erule Abs_lst1_fcb2)
  apply(simp add: Abs_fresh_iff)
  apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
  apply(blast)
  apply(blast)
  apply(subgoal_tac "eqvt_at crename_sumC (M, da, ea)")
  apply(subgoal_tac "eqvt_at crename_sumC (Ma, da, ea)")
  apply(erule conjE)+
  apply(erule Abs_lst_fcb2)
  apply(simp add: Abs_fresh_star)
  apply(simp add: Abs_fresh_star)
  apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
  apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
  apply(blast)
  apply(blast)
  done

termination 
  by lexicographic_order

nominal_primrec 
  nrename :: "trm \<Rightarrow> name \<Rightarrow> name \<Rightarrow> trm"      ("_[_\<turnstile>n>_]" [100,100,100] 100) 
where
  "(Ax x a)[u\<turnstile>n>v] = (if x=u then Ax v a else Ax x a)" 
| "atom x \<sharp> (u, v) \<Longrightarrow> (Cut <a>.M (x).N)[u\<turnstile>n>v] = Cut <a>.(M[u\<turnstile>n>v]) (x).(N[u\<turnstile>n>v])" 
| "atom x \<sharp> (u, v) \<Longrightarrow> (NotR (x).M a)[u\<turnstile>n>v] = NotR (x).(M[u\<turnstile>n>v]) a" 
| "(NotL <a>.M x)[u\<turnstile>n>v] = (if x=u then NotL <a>.(M[u\<turnstile>n>v]) v else NotL <a>.(M[u\<turnstile>n>v]) x)" 
| "(AndR <a>.M <b>.N c)[u\<turnstile>n>v] = AndR <a>.(M[u\<turnstile>n>v]) <b>.(N[u\<turnstile>n>v]) c" 
| "atom x \<sharp> (u, v) \<Longrightarrow> (AndL1 (x).M y)[u\<turnstile>n>v] = 
          (if y=u then AndL1 (x).(M[u\<turnstile>n>v]) v else AndL1 (x).(M[u\<turnstile>n>v]) y)"
| "atom x \<sharp> (u, v) \<Longrightarrow> (AndL2 (x).M y)[u\<turnstile>n>v] = 
          (if y=u then AndL2 (x).(M[u\<turnstile>n>v]) v else AndL2 (x).(M[u\<turnstile>n>v]) y)"
| "(OrR1 <a>.M b)[u\<turnstile>n>v] = OrR1 <a>.(M[u\<turnstile>n>v]) b"
| "(OrR2 <a>.M b)[u\<turnstile>n>v] = OrR2 <a>.(M[u\<turnstile>n>v]) b"
| "\<lbrakk>atom x \<sharp> (u, v); atom y \<sharp> (u, v)\<rbrakk> \<Longrightarrow> (OrL (x).M (y).N z)[u\<turnstile>n>v] = 
        (if z=u then OrL (x).(M[u\<turnstile>n>v]) (y).(N[u\<turnstile>n>v]) v else OrL (x).(M[u\<turnstile>n>v]) (y).(N[u\<turnstile>n>v]) z)"
| "atom x \<sharp> (u, v) \<Longrightarrow> (ImpR (x).<a>.M b)[u\<turnstile>n>v] = ImpR (x).<a>.(M[u\<turnstile>n>v]) b"
| "atom x \<sharp> (u, v) \<Longrightarrow> (ImpL <a>.M (x).N y)[u\<turnstile>n>v] = 
        (if y=u then ImpL <a>.(M[u\<turnstile>n>v]) (x).(N[u\<turnstile>n>v]) v else ImpL <a>.(M[u\<turnstile>n>v]) (x).(N[u\<turnstile>n>v]) y)"
  apply(simp only: eqvt_def)
  apply(simp only: nrename_graph_def)
  apply (rule, perm_simp, rule)
  apply(rule TrueI)
  -- "covered all cases"
  apply(case_tac x)
  apply(rule_tac y="a" and c="(b, c)" in trm.strong_exhaust)
  apply (simp_all add: fresh_star_def)[12]
  apply(metis)+
  -- "compatibility"
  apply(simp_all)
  apply(rule conjI)
  apply(elim conjE)
  apply(erule_tac c="(ua,va)" in Abs_lst1_fcb2)
  apply(simp add: Abs_fresh_iff)
  apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
  apply(elim conjE)
  apply(erule_tac c="(ua,va)" in Abs_lst1_fcb2)
  apply(simp add: Abs_fresh_iff)
  apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
  apply(elim conjE)
  apply(erule_tac c="(ua,va)" in Abs_lst1_fcb2)
  apply(simp add: Abs_fresh_iff)
  apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
  apply(elim conjE)
  apply(subgoal_tac "eqvt_at nrename_sumC (M, ua, va)")
  apply(subgoal_tac "eqvt_at nrename_sumC (Ma, ua, va)")
  apply(erule Abs_lst1_fcb2)
  apply(simp add: Abs_fresh_iff)
  apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
  apply(blast)
  apply(blast)
  apply(elim conjE)
  apply(rule conjI)
  apply(subgoal_tac "eqvt_at nrename_sumC (M, ua, va)")
  apply(subgoal_tac "eqvt_at nrename_sumC (Ma, ua, va)")
  apply(erule Abs_lst1_fcb2)
  apply(simp add: Abs_fresh_iff)
  apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
  apply(blast)
  apply(blast)
  apply(subgoal_tac "eqvt_at nrename_sumC (N, ua, va)")
  apply(subgoal_tac "eqvt_at nrename_sumC (Na, ua, va)")
  apply(erule Abs_lst1_fcb2)
  apply(simp add: Abs_fresh_iff)
  apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
  apply(blast)
  apply(blast)
  apply(elim conjE)
  apply(subgoal_tac "eqvt_at nrename_sumC (M, ua, va)")
  apply(subgoal_tac "eqvt_at nrename_sumC (Ma, ua, va)")
  apply(erule Abs_lst1_fcb2)
  apply(simp add: Abs_fresh_iff)
  apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
  apply(blast)
  apply(blast)
  apply(elim conjE)+
  apply(subgoal_tac "eqvt_at nrename_sumC (M, ua, va)")
  apply(subgoal_tac "eqvt_at nrename_sumC (Ma, ua, va)")
  apply(erule Abs_lst1_fcb2)
  apply(simp add: Abs_fresh_iff)
  apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
  apply(blast)
  apply(blast)
  apply(elim conjE)+
  apply(erule_tac c="(ua,va)" in Abs_lst1_fcb2)
  apply(simp add: Abs_fresh_iff)
  apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
  apply(elim conjE)
  apply(erule_tac c="(ua,va)" in Abs_lst1_fcb2)
  apply(simp add: Abs_fresh_iff)
  apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
  apply(elim conjE)
  apply(rule conjI)
  apply(subgoal_tac "eqvt_at nrename_sumC (M, ua, va)")
  apply(subgoal_tac "eqvt_at nrename_sumC (Ma, ua, va)")
  apply(erule Abs_lst1_fcb2)
  apply(simp add: Abs_fresh_iff)
  apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
  apply(blast)
  apply(blast)
  apply(subgoal_tac "eqvt_at nrename_sumC (N, ua, va)")
  apply(subgoal_tac "eqvt_at nrename_sumC (Na, ua, va)")
  apply(erule Abs_lst1_fcb2)
  apply(simp add: Abs_fresh_iff)
  apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
  apply(blast)
  apply(blast)
  apply(erule conjE)+
  apply(erule Abs_lst_fcb2)
  apply(simp add: Abs_fresh_star)
  apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
  apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
  apply(erule conjE)+
  apply(rule conjI)
  apply(subgoal_tac "eqvt_at nrename_sumC (M, ua, va)")
  apply(subgoal_tac "eqvt_at nrename_sumC (Ma, ua, va)")
  apply(erule Abs_lst1_fcb2)
  apply(simp add: Abs_fresh_iff)
  apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
  apply(blast)
  apply(blast)
  apply(subgoal_tac "eqvt_at nrename_sumC (N, ua, va)")
  apply(subgoal_tac "eqvt_at nrename_sumC (Na, ua, va)")
  apply(erule Abs_lst1_fcb2)
  apply(simp add: Abs_fresh_iff)
  apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
  apply(blast)
  apply(blast)
  done

termination 
  by lexicographic_order

lemma crename_name_eqvt[eqvt]:
  shows "p \<bullet> (M[d\<turnstile>c>e]) = (p \<bullet> M)[(p \<bullet> d)\<turnstile>c>(p \<bullet> e)]"
apply(nominal_induct M avoiding: d e rule: trm.strong_induct)
apply(auto)
done

lemma nrename_name_eqvt[eqvt]:
  shows "p \<bullet> (M[x\<turnstile>n>y]) = (p \<bullet> M)[(p \<bullet> x)\<turnstile>n>(p \<bullet> y)]"
apply(nominal_induct M avoiding: x y rule: trm.strong_induct)
apply(auto)
done

nominal_primrec 
  substn :: "trm \<Rightarrow> name   \<Rightarrow> coname \<Rightarrow> trm \<Rightarrow> trm" ("_{_:=<_>._}" [100,100,100,100] 100) 
where
  "(Ax x a){y:=<c>.P} = (if x=y then Cut <c>.P (y).Ax y a else Ax x a)" 
| "\<lbrakk>atom a \<sharp> (c, P); atom x \<sharp> (y, P)\<rbrakk> \<Longrightarrow> (Cut <a>.M (x).N){y:=<c>.P} = 
    (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}))" 
| "atom x\<sharp> (y, P) \<Longrightarrow> (NotR (x).M a){y:=<c>.P} = NotR (x).(M{y:=<c>.P}) a" 
| "\<lbrakk>atom a\<sharp> (c, P); atom x' \<sharp> (M, y, P)\<rbrakk> \<Longrightarrow> (NotL <a>.M x){y:=<c>.P} = 
    (if x=y then Cut <c>.P (x').NotL <a>.(M{y:=<c>.P}) x' else NotL <a>.(M{y:=<c>.P}) x)"
| "\<lbrakk>atom a \<sharp> (c, P); atom b \<sharp> (c, P)\<rbrakk> \<Longrightarrow> 
    (AndR <a>.M <b>.N d){y:=<c>.P} = AndR <a>.(M{y:=<c>.P}) <b>.(N{y:=<c>.P}) d" 
| "atom x \<sharp> (y, P) \<Longrightarrow> (AndL1 (x).M z){y:=<c>.P} = 
    (if z=y then Cut <c>.P (z').AndL1 (x).(M{y:=<c>.P}) z' else AndL1 (x).(M{y:=<c>.P}) z)"
| "atom x \<sharp> (y, P) \<Longrightarrow> (AndL2 (x).M z){y:=<c>.P} = 
    (if z=y then Cut <c>.P (z').AndL2 (x).(M{y:=<c>.P}) z' else AndL2 (x).(M{y:=<c>.P}) z)"
| "atom a \<sharp> (c, P) \<Longrightarrow> (OrR1 <a>.M b){y:=<c>.P} = OrR1 <a>.(M{y:=<c>.P}) b"
| "atom a \<sharp> (c, P) \<Longrightarrow> (OrR2 <a>.M b){y:=<c>.P} = OrR2 <a>.(M{y:=<c>.P}) b"
| "\<lbrakk>atom x \<sharp> (y, P); atom u \<sharp> (y, P)\<rbrakk> \<Longrightarrow> (OrL (x).M (u).N z){y:=<c>.P} = 
     (if z=y then Cut <c>.P (z').OrL (x).(M{y:=<c>.P}) (u).(N{y:=<c>.P}) z' 
      else OrL (x).(M{y:=<c>.P}) (u).(N{y:=<c>.P}) z)"
| "\<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"
| "\<lbrakk>atom a \<sharp> (c, P); atom x \<sharp> (y, P)\<rbrakk> \<Longrightarrow> (ImpL <a>.M (x).N z){y:=<c>.P} = 
     (if y=z then Cut <c>.P (z').ImpL <a>.(M{y:=<c>.P}) (x).(N{y:=<c>.P}) z' 
      else ImpL <a>.(M{y:=<c>.P}) (x).(N{y:=<c>.P}) z)"
  apply(simp only: eqvt_def)
  apply(simp only: substn_graph_def)
  apply (rule, perm_simp, rule)
  apply(rule TrueI)
  -- "covered all cases"
  apply(case_tac x)
  apply(rule_tac y="a" and c="(b, c, d)" in trm.strong_exhaust)
  apply (simp_all add: fresh_star_def fresh_Pair)[12]
  apply(metis)+
  apply(subgoal_tac "\<exists>x'::name. atom x' \<sharp> (trm, b, d)")
  apply(auto simp add: fresh_Pair)[1]
  apply(metis)+
  apply(subgoal_tac "\<exists>x'::name. atom x' \<sharp> (trm, b, d)")
  apply(auto simp add: fresh_Pair)[1]
  apply(rule obtain_fresh)
  apply(auto)[1]
  apply(metis)+
  -- "compatibility"
  apply(all_trivials)
  apply(simp)
  oops

end