diff -r d9c3cc271e62 -r 7ab36bc29cc2 Nominal/Ex/Classical.thy
--- a/Nominal/Ex/Classical.thy	Tue Jul 05 15:00:41 2011 +0200
+++ b/Nominal/Ex/Classical.thy	Tue Jul 05 15:01:10 2011 +0200
@@ -47,7 +47,6 @@
 thm trm.supp
 thm trm.supp[simplified]
 
-
 nominal_primrec 
   crename :: "trm \<Rightarrow> coname \<Rightarrow> coname \<Rightarrow> trm"  ("_[_\<turnstile>c>_]" [100,100,100] 100) 
 where
@@ -77,6 +76,7 @@
   apply (simp_all add: fresh_star_def)[12]
   apply(metis)+
   -- "compatibility"
+  apply(all_trivials)
   apply(simp_all)
   apply(rule conjI)
   apply(elim conjE)
@@ -216,7 +216,229 @@
   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