diff -r 014e7696ac6b -r 49e2d9744ae1 src/HOL/Nominal/Examples/Class.thy
--- a/src/HOL/Nominal/Examples/Class.thy	Tue Mar 06 08:09:43 2007 +0100
+++ b/src/HOL/Nominal/Examples/Class.thy	Tue Mar 06 15:28:22 2007 +0100
@@ -1,26 +1,37 @@
 (* $Id$ *)
 
 theory Class 
-imports "Nominal" 
+imports "../Nominal" 
 begin
 
 section {* Term-Calculus from Urban's PhD *}
 
 atom_decl name coname
 
+text {* types *}
+
+nominal_datatype ty =
+    PROP "string"
+  | NOT  "ty"
+  | AND  "ty" "ty"   ("_ AND _" [100,100] 100)
+  | OR   "ty" "ty"   ("_ OR _" [100,100] 100)
+  | IMP  "ty" "ty"   ("_ IMPL _" [100,100] 100)
+
+text {* terms *}
+
 nominal_datatype trm = 
     Ax   "name" "coname"
-  | Cut  "\<guillemotleft>coname\<guillemotright>trm" "\<guillemotleft>name\<guillemotright>trm"            ("Cut <_>._ [_]._" [100,100,100,100] 100)
-  | NotR "\<guillemotleft>name\<guillemotright>trm" "coname"                 ("NotR [_]._ _" [100,100,100] 100)
+  | Cut  "\<guillemotleft>coname\<guillemotright>trm" "\<guillemotleft>name\<guillemotright>trm"            ("Cut <_>._ (_)._" [100,100,100,100] 100)
+  | NotR "\<guillemotleft>name\<guillemotright>trm" "coname"                 ("NotR (_)._ _" [100,100,100] 100)
   | NotL "\<guillemotleft>coname\<guillemotright>trm" "name"                 ("NotL <_>._ _" [100,100,100] 100)
   | AndR "\<guillemotleft>coname\<guillemotright>trm" "\<guillemotleft>coname\<guillemotright>trm" "coname" ("AndR <_>._ <_>._ _" [100,100,100,100,100] 100)
-  | AndL1 "\<guillemotleft>name\<guillemotright>trm" "name"                  ("AndL1 [_]._ _" [100,100,100] 100)
-  | AndL2 "\<guillemotleft>name\<guillemotright>trm" "name"                  ("AndL2 [_]._ _" [100,100,100] 100)
+  | AndL1 "\<guillemotleft>name\<guillemotright>trm" "name"                  ("AndL1 (_)._ _" [100,100,100] 100)
+  | AndL2 "\<guillemotleft>name\<guillemotright>trm" "name"                  ("AndL2 (_)._ _" [100,100,100] 100)
   | OrR1 "\<guillemotleft>coname\<guillemotright>trm" "coname"               ("OrR1 <_>._ _" [100,100,100] 100)
   | OrR2 "\<guillemotleft>coname\<guillemotright>trm" "coname"               ("OrR2 <_>._ _" [100,100,100] 100)
-  | OrL "\<guillemotleft>name\<guillemotright>trm" "\<guillemotleft>name\<guillemotright>trm" "name"        ("OrL [_]._ [_]._ _" [100,100,100,100,100] 100)
-  | ImpR "\<guillemotleft>name\<guillemotright>(\<guillemotleft>coname\<guillemotright>trm)" "coname"       ("ImpR [_].<_>._ _" [100,100,100,100] 100)
-  | ImpL "\<guillemotleft>coname\<guillemotright>trm" "\<guillemotleft>name\<guillemotright>trm" "name"     ("ImpL <_>._ [_]._ _" [100,100,100,100,100] 100)
+  | OrL "\<guillemotleft>name\<guillemotright>trm" "\<guillemotleft>name\<guillemotright>trm" "name"        ("OrL (_)._ (_)._ _" [100,100,100,100,100] 100)
+  | ImpR "\<guillemotleft>name\<guillemotright>(\<guillemotleft>coname\<guillemotright>trm)" "coname"       ("ImpR (_).<_>._ _" [100,100,100,100] 100)
+  | ImpL "\<guillemotleft>coname\<guillemotright>trm" "\<guillemotleft>name\<guillemotright>trm" "name"     ("ImpL <_>._ (_)._ _" [100,100,100,100,100] 100)
 
 text {* Induction principles *}
 
@@ -30,24 +41,12 @@
 
 text {* named terms *}
 
-nominal_datatype ntrm = Na "\<guillemotleft>name\<guillemotright>trm" ("([_]:_)" [100,100] 100)
+nominal_datatype ntrm = Na "\<guillemotleft>name\<guillemotright>trm" ("((_):_)" [100,100] 100)
 
 text {* conamed terms *}
 
 nominal_datatype ctrm = Co "\<guillemotleft>coname\<guillemotright>trm" ("(<_>:_)" [100,100] 100)
 
-lemma eq_eqvt_name[eqvt]:
-  fixes pi::"name prm"
-  and   x::"'a::pt_name"
-  shows "pi\<bullet>(x=y) = ((pi\<bullet>x)=(pi\<bullet>y))"
-  by (simp add: perm_bool perm_bij)
-
-lemma eq_eqvt_coname[eqvt]:
-  fixes pi::"coname prm"
-  and   x::"'a::pt_coname"
-  shows "pi\<bullet>(x=y) = ((pi\<bullet>x)=(pi\<bullet>y))"
-  by (simp add: perm_bool perm_bij)
-
 text {* renaming functions *}
 
 consts
@@ -56,49 +55,232 @@
 
 nominal_primrec (freshness_context: "(d::coname,e::coname)") 
   "(Ax x a)[d\<turnstile>c>e] = (if a=d then Ax x e else Ax x a)" 
-  "\<lbrakk>a\<sharp>(d,e,N);x\<sharp>M\<rbrakk> \<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)" 
+  "\<lbrakk>a\<sharp>(d,e,N);x\<sharp>M\<rbrakk> \<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)" 
   "a\<sharp>(d,e) \<Longrightarrow> (NotL <a>.M x)[d\<turnstile>c>e] = (NotL <a>.(M[d\<turnstile>c>e]) x)" 
   "\<lbrakk>a\<sharp>(d,e,N,c);b\<sharp>(d,e,M,c);b\<noteq>a\<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)" 
-  "x\<sharp>y \<Longrightarrow> (AndL1 [x].M y)[d\<turnstile>c>e] = AndL1 [x].(M[d\<turnstile>c>e]) y"
-  "x\<sharp>y \<Longrightarrow> (AndL2 [x].M y)[d\<turnstile>c>e] = AndL2 [x].(M[d\<turnstile>c>e]) y"
+  "x\<sharp>y \<Longrightarrow> (AndL1 (x).M y)[d\<turnstile>c>e] = AndL1 (x).(M[d\<turnstile>c>e]) y"
+  "x\<sharp>y \<Longrightarrow> (AndL2 (x).M y)[d\<turnstile>c>e] = AndL2 (x).(M[d\<turnstile>c>e]) y"
   "a\<sharp>(d,e,b) \<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)"
   "a\<sharp>(d,e,b) \<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)"
-  "\<lbrakk>x\<sharp>(N,z);y\<sharp>(M,z);y\<noteq>x\<rbrakk> \<Longrightarrow> (OrL [x].M [y].N z)[d\<turnstile>c>e] = OrL [x].(M[d\<turnstile>c>e]) [y].(N[d\<turnstile>c>e]) z"
-  "a\<sharp>(d,e,b) \<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)"
-  "\<lbrakk>a\<sharp>(d,e,N);x\<sharp>(M,y)\<rbrakk> \<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(finite_guess add: eqvt perm_if fs_coname1 fs_name1 | 
-      perm_simp add: abs_fresh abs_supp fs_name1 fs_coname1)+
-apply(fresh_guess add: eqvt perm_if fs_coname1 fs_name1 | perm_simp add: fresh_atm)+
+  "\<lbrakk>x\<sharp>(N,z);y\<sharp>(M,z);y\<noteq>x\<rbrakk> \<Longrightarrow> (OrL (x).M (y).N z)[d\<turnstile>c>e] = OrL (x).(M[d\<turnstile>c>e]) (y).(N[d\<turnstile>c>e]) z"
+  "a\<sharp>(d,e,b) \<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)"
+  "\<lbrakk>a\<sharp>(d,e,N);x\<sharp>(M,y)\<rbrakk> \<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(finite_guess)+
+apply(rule TrueI)+
+apply(simp add: abs_fresh abs_supp fin_supp)+
+apply(fresh_guess)+
 done
 
 nominal_primrec (freshness_context: "(u::name,v::name)") 
   "(Ax x a)[u\<turnstile>n>v] = (if x=u then Ax v a else Ax x a)" 
-  "\<lbrakk>a\<sharp>N;x\<sharp>(u,v,M)\<rbrakk> \<Longrightarrow> (Cut <a>.M [x].N)[u\<turnstile>n>v] = Cut <a>.(M[u\<turnstile>n>v]) [x].(N[u\<turnstile>n>v])" 
-  "x\<sharp>(u,v) \<Longrightarrow> (NotR [x].M a)[u\<turnstile>n>v] = NotR [x].(M[u\<turnstile>n>v]) a" 
+  "\<lbrakk>a\<sharp>N;x\<sharp>(u,v,M)\<rbrakk> \<Longrightarrow> (Cut <a>.M (x).N)[u\<turnstile>n>v] = Cut <a>.(M[u\<turnstile>n>v]) (x).(N[u\<turnstile>n>v])" 
+  "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)" 
   "\<lbrakk>a\<sharp>(N,c);b\<sharp>(M,c);b\<noteq>a\<rbrakk> \<Longrightarrow> (AndR <a>.M <b>.N c)[u\<turnstile>n>v] = AndR <a>.(M[u\<turnstile>n>v]) <b>.(N[u\<turnstile>n>v]) c" 
-  "x\<sharp>(u,v,y) \<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)"
-  "x\<sharp>(u,v,y) \<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)"
+  "x\<sharp>(u,v,y) \<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)"
+  "x\<sharp>(u,v,y) \<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)"
   "a\<sharp>b \<Longrightarrow> (OrR1 <a>.M b)[u\<turnstile>n>v] = OrR1 <a>.(M[u\<turnstile>n>v]) b"
   "a\<sharp>b \<Longrightarrow> (OrR2 <a>.M b)[u\<turnstile>n>v] = OrR2 <a>.(M[u\<turnstile>n>v]) b"
-  "\<lbrakk>x\<sharp>(u,v,N,z);y\<sharp>(u,v,M,z);y\<noteq>x\<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)"
-  "\<lbrakk>a\<sharp>b; x\<sharp>(u,v)\<rbrakk> \<Longrightarrow> (ImpR [x].<a>.M b)[u\<turnstile>n>v] = ImpR [x].<a>.(M[u\<turnstile>n>v]) b"
-  "\<lbrakk>a\<sharp>N;x\<sharp>(u,v,M,y)\<rbrakk> \<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(finite_guess add: eqvt perm_if fs_coname1 fs_name1 | 
-      perm_simp add: abs_fresh abs_supp fresh_prod fs_name1 fs_coname1)+
-apply(fresh_guess add: eqvt perm_if fs_coname1 fs_name1 | perm_simp add: fresh_atm)+
+  "\<lbrakk>x\<sharp>(u,v,N,z);y\<sharp>(u,v,M,z);y\<noteq>x\<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)"
+  "\<lbrakk>a\<sharp>b; x\<sharp>(u,v)\<rbrakk> \<Longrightarrow> (ImpR (x).<a>.M b)[u\<turnstile>n>v] = ImpR (x).<a>.(M[u\<turnstile>n>v]) b"
+  "\<lbrakk>a\<sharp>N;x\<sharp>(u,v,M,y)\<rbrakk> \<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(finite_guess)+
+apply(rule TrueI)+
+apply(simp add: abs_fresh abs_supp fs_name1 fs_coname1)+
+apply(fresh_guess)+
+done
+
+lemmas eq_bij = pt_bij[OF pt_name_inst, OF at_name_inst] pt_bij[OF pt_coname_inst, OF at_coname_inst]
+
+
+lemma crename_name_eqvt[eqvt]:
+  fixes pi::"name prm"
+  shows "pi\<bullet>(M[d\<turnstile>c>e]) = (pi\<bullet>M)[(pi\<bullet>d)\<turnstile>c>(pi\<bullet>e)]"
+apply(nominal_induct M avoiding: d e rule: trm.induct)
+apply(auto simp add: fresh_bij eq_bij)
+done
+
+
+lemma crename_coname_eqvt[eqvt]:
+  fixes pi::"coname prm"
+  shows "pi\<bullet>(M[d\<turnstile>c>e]) = (pi\<bullet>M)[(pi\<bullet>d)\<turnstile>c>(pi\<bullet>e)]"
+apply(nominal_induct M avoiding: d e rule: trm.induct)
+apply(auto simp add: fresh_bij eq_bij)
+done
+
+lemma nrename_name_eqvt[eqvt]:
+  fixes pi::"name prm"
+  shows "pi\<bullet>(M[x\<turnstile>n>y]) = (pi\<bullet>M)[(pi\<bullet>x)\<turnstile>n>(pi\<bullet>y)]"
+apply(nominal_induct M avoiding: x y rule: trm.induct)
+apply(auto simp add: fresh_bij eq_bij)
+done
+
+lemma nrename_coname_eqvt[eqvt]:
+  fixes pi::"coname prm"
+  shows "pi\<bullet>(M[x\<turnstile>n>y]) = (pi\<bullet>M)[(pi\<bullet>x)\<turnstile>n>(pi\<bullet>y)]"
+apply(nominal_induct M avoiding: x y rule: trm.induct)
+apply(auto simp add: fresh_bij eq_bij)
+done
+
+text {* substitution functions *}
+
+consts
+  substn :: "trm \<Rightarrow> name   \<Rightarrow> coname \<Rightarrow> trm \<Rightarrow> trm" ("_[_:=<_>._]" [100,100,100,100] 100) 
+  substc :: "trm \<Rightarrow> coname \<Rightarrow> name   \<Rightarrow> trm \<Rightarrow> trm" ("_[_:=(_)._]" [100,100,100,100] 100)
+
+nominal_primrec (freshness_context: "(y::name,c::coname,P::trm)")
+  "(Ax x a)[y:=<c>.P] = (if x=y then P[c\<turnstile>c>a] else Ax x a)" 
+  "\<lbrakk>a\<sharp>(c,P,N);x\<sharp>(y,c,P,M)\<rbrakk> \<Longrightarrow> 
+   (Cut <a>.M (x).N)[y:=<c>.P] = Cut <a>.(M[y:=<c>.P]) (x).(N[y:=<c>.P])" 
+  "x\<sharp>(y,c,P) \<Longrightarrow> 
+   (NotR (x).M a)[y:=<c>.P] = NotR (x).(M[y:=<c>.P]) a" 
+  "a\<sharp>(c,P)\<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>a\<sharp>(c,P,N,d);b\<sharp>(c,P,M,d);b\<noteq>a\<rbrakk> \<Longrightarrow> 
+   (AndR <a>.M <b>.N d)[y:=<c>.P] = AndR <a>.(M[y:=<c>.P]) <b>.(N[y:=<c>.P]) d" 
+  "x\<sharp>(y,c,P,z) \<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)"
+  "x\<sharp>(y,c,P,z) \<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)"
+  "a\<sharp>(c,P,b) \<Longrightarrow> 
+   (OrR1 <a>.M b)[y:=<c>.P] = OrR1 <a>.(M[y:=<c>.P]) b"
+  "a\<sharp>(c,P,b) \<Longrightarrow> 
+   (OrR2 <a>.M b)[y:=<c>.P] = OrR2 <a>.(M[y:=<c>.P]) b"
+  "\<lbrakk>x\<sharp>(y,N,c,P,z);u\<sharp>(y,M,c,P,z);x\<noteq>u\<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>a\<sharp>(b,c,P); x\<sharp>(y,c,P)\<rbrakk> \<Longrightarrow> 
+   (ImpR (x).<a>.M b)[y:=<c>.P] = ImpR (x).<a>.(M[y:=<c>.P]) b"
+  "\<lbrakk>a\<sharp>(N,c,P);x\<sharp>(y,c,P,M,z)\<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(finite_guess)+
+apply(rule TrueI)+
+apply(simp add: abs_fresh abs_supp fs_name1 fs_coname1)+
+apply(fresh_guess)+
 done
 
-text {* We should now define the two forms of substitition :o( *}
+text {* typing contexts *}
+
+types 
+  ctxtn = "(name\<times>ty) list"
+  ctxtc = "(coname\<times>ty) list"
+
+inductive2
+  validc :: "ctxtc \<Rightarrow> bool"
+where
+  vc1[intro]: "validc []"
+| vc2[intro]: "\<lbrakk>a\<sharp>\<Delta>; validc \<Delta>\<rbrakk> \<Longrightarrow> validc ((a,T)#\<Delta>)"  
+
+inductive2
+  validn :: "ctxtn \<Rightarrow> bool"
+where
+  vn1[intro]: "validn []"
+| vn2[intro]: "\<lbrakk>x\<sharp>\<Gamma>; validn \<Gamma>\<rbrakk> \<Longrightarrow> validn ((x,T)#\<Gamma>)"
+
+text {* typing relation *}
+
+inductive2
+   typing :: "ctxtn \<Rightarrow> trm \<Rightarrow> ctxtc \<Rightarrow> bool" ("_ \<turnstile> _ \<turnstile> _" [100,100,100] 100)
+where
+  "\<lbrakk>validn \<Gamma>;validc \<Delta>; (x,B)\<in>set \<Gamma>; (a,B)\<in>set \<Delta>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Ax x a \<turnstile> \<Delta>"
+| "\<lbrakk>x\<sharp>\<Gamma>; ((x,B)#\<Gamma>) \<turnstile> M \<turnstile> \<Delta>\<rbrakk> \<Longrightarrow>  \<Gamma> \<turnstile> NotR (x).M a \<turnstile> ((a,NOT B)#\<Delta>)"
+| "\<lbrakk>a\<sharp>\<Delta>; \<Gamma> \<turnstile> M \<turnstile> ((a,B)#\<Delta>)\<rbrakk> \<Longrightarrow>  ((x,NOT B)#\<Gamma>) \<turnstile> NotL <a>.M x \<turnstile> \<Delta>"
+| "\<lbrakk>x\<sharp>\<Gamma>; ((x,B1)#\<Gamma>) \<turnstile> M \<turnstile> \<Delta>\<rbrakk> \<Longrightarrow>  ((y,B1 AND B2)#\<Gamma>) \<turnstile> AndL1 (x).M y \<turnstile> \<Delta>"
+| "\<lbrakk>x\<sharp>\<Gamma>; ((x,B2)#\<Gamma>) \<turnstile> M \<turnstile> \<Delta>\<rbrakk> \<Longrightarrow>  ((y,B1 AND B2)#\<Gamma>) \<turnstile> AndL2 (x).M y \<turnstile> \<Delta>"
+| "\<lbrakk>a\<sharp>\<Delta>;b\<sharp>\<Delta>; \<Gamma> \<turnstile> M \<turnstile> ((a,B)#\<Delta>); \<Gamma> \<turnstile> N \<turnstile> ((b,C)#\<Delta>)\<rbrakk> \<Longrightarrow>  \<Gamma> \<turnstile> AndR <a>.M <b>.N c \<turnstile> ((c,B AND C)#\<Delta>)"
+| "\<lbrakk>x\<sharp>\<Gamma>;y\<sharp>\<Gamma>; ((x,B)#\<Gamma>) \<turnstile> M \<turnstile> \<Delta>; ((y,C)#\<Gamma>) \<turnstile> N \<turnstile> \<Delta>\<rbrakk> \<Longrightarrow>  ((z,B OR C)#\<Gamma>) \<turnstile> OrL (x).M (y).N z \<turnstile> \<Delta>"
+| "\<lbrakk>a\<sharp>\<Delta>; \<Gamma> \<turnstile> M \<turnstile> ((a,B1)#\<Delta>)\<rbrakk> \<Longrightarrow>  \<Gamma> \<turnstile> OrR1 <a>.M b \<turnstile> ((b,B1 OR B2)#\<Delta>)"
+| "\<lbrakk>a\<sharp>\<Delta>; \<Gamma> \<turnstile> M \<turnstile> ((a,B2)#\<Delta>)\<rbrakk> \<Longrightarrow>  \<Gamma> \<turnstile> OrR2 <a>.M b \<turnstile> ((b,B1 OR B2)#\<Delta>)"
+| "\<lbrakk>a\<sharp>\<Delta>;x\<sharp>\<Gamma>; \<Gamma> \<turnstile> M \<turnstile> ((a,B)#\<Delta>); ((x,C)#\<Gamma>) \<turnstile> N \<turnstile> \<Delta>\<rbrakk> \<Longrightarrow>  ((y,B IMPL C)#\<Gamma>) \<turnstile> ImpL <a>.M (x).N y \<turnstile> \<Delta>"
+| "\<lbrakk>a\<sharp>\<Delta>;x\<sharp>\<Gamma>; ((x,B)#\<Gamma>) \<turnstile> M \<turnstile> ((a,C)#\<Delta>)\<rbrakk> \<Longrightarrow>  \<Gamma> \<turnstile> ImpR (x).<a>.M b \<turnstile> ((b,B IMPL C)#\<Delta>)"
+| "\<lbrakk>a\<sharp>\<Delta>1;x\<sharp>\<Gamma>2; validn(\<Gamma>1@\<Gamma>2); validc (\<Delta>1@\<Delta>2); \<Gamma>1 \<turnstile> M \<turnstile> ((a,B)#\<Delta>1); ((x,B)#\<Gamma>2) \<turnstile> N \<turnstile> \<Delta>2\<rbrakk> 
+   \<Longrightarrow>  (\<Gamma>1@\<Gamma>2) \<turnstile> Cut <a>.M (x).N \<turnstile> (\<Delta>1@\<Delta>2)"
+
+text {* relations about freshly introducing a name or coname *} 
+
+inductive2
+  fin :: "trm \<times> name \<Rightarrow> bool"
+where
+  "fin (Ax x a,x)"
+| "x\<sharp>M \<Longrightarrow> fin (NotL <a>.M x,x)"
+| "y\<sharp>[x].M \<Longrightarrow> fin (AndL1 (x).M y,y)"
+| "y\<sharp>[x].M \<Longrightarrow> fin (AndL2 (x).M y,y)"
+| "\<lbrakk>z\<sharp>[x].M;z\<sharp>[y].N\<rbrakk> \<Longrightarrow> fin (OrL (x).M (y).N z,z)"
+| "\<lbrakk>y\<sharp>M;y\<sharp>[x].N\<rbrakk> \<Longrightarrow> fin (ImpL <a>.M (x).N y,y)"
 
-consts
-  substn :: "trm \<Rightarrow> name   \<Rightarrow> ctrm \<Rightarrow> trm" ("_[_::n=_]" [100,100,100] 100) 
-  substc :: "trm \<Rightarrow> coname \<Rightarrow> ntrm \<Rightarrow> trm" ("_[_::c=_]" [100,100,100] 100)
+inductive2
+  fic :: "trm \<times> coname \<Rightarrow> bool"
+where
+  "fic (Ax x a,a)"
+| "a\<sharp>M \<Longrightarrow> fic (NotR (x).M a,a)"
+| "\<lbrakk>c\<sharp>[a].M;c\<sharp>[b].N\<rbrakk> \<Longrightarrow> fic (AndR <a>.M <b>.N c,c)"
+| "b\<sharp>[a].M \<Longrightarrow> fic (OrR1 <a>.M b,b)"
+| "b\<sharp>[a].M \<Longrightarrow> fic (OrR2 <a>.M b,b)"
+| "\<lbrakk>b\<sharp>[a].M\<rbrakk> \<Longrightarrow> fic (ImpR (x).<a>.M b,b)"
+
+text {* cut-reductions *}
+
+inductive2
+  red :: "trm \<Rightarrow> trm \<Rightarrow> bool" ("_ \<longrightarrow>\<^isub>c _" [100,100] 100)
+where
+  "fic (M,a) \<Longrightarrow> Cut <a>.M (x).(Ax x b) \<longrightarrow>\<^isub>c M[a\<turnstile>c>b]"
+| "fin (M,x) \<Longrightarrow> Cut <a>.(Ax y a) (x).M \<longrightarrow>\<^isub>c M[x\<turnstile>n>y]"
+| "\<lbrakk>fic (NotR (x).M a,a); fin (NotL <b>.N y,y)\<rbrakk> \<Longrightarrow>
+   Cut <a>.(NotR (x).M a) (y).(NotL <b>.N y) \<longrightarrow>\<^isub>c Cut <b>.N (x).M" 
+| "\<lbrakk>fic (AndR <a1>.M1 <a2>.M2 b,b); fin (AndL1 (x).N y,y)\<rbrakk> \<Longrightarrow>
+   Cut <b>.(AndR <a1>.M1 <a2>.M2 b) (y).(AndL1 (x).N y) \<longrightarrow>\<^isub>c Cut <a1>.M1 (x).N"
+| "\<lbrakk>fic (AndR <a1>.M1 <a2>.M2 b,b); fin (AndL2 (x).N y,y)\<rbrakk> \<Longrightarrow>
+   Cut <b>.(AndR <a1>.M1 <a2>.M2 b) (y).(AndL2 (x).N y) \<longrightarrow>\<^isub>c Cut <a2>.M2 (x).N"
+| "\<lbrakk>fic (AndR <a1>.M1 <a2>.M2 b,b); fin (AndL1 (x).N y,y)\<rbrakk> \<Longrightarrow>
+   Cut <b>.(AndR <a1>.M1 <a2>.M2 b) (y).(AndL1 (x).N y) \<longrightarrow>\<^isub>c Cut <a1>.M1 (x).N"
+| "\<lbrakk>fic (OrR1 <a>.M b,b); fin (OrL (x1).N1 (x2).N2 y,y)\<rbrakk> \<Longrightarrow>
+   Cut <b>.(OrR1 <a>.M b) (y).(OrL (x1).N1 (x2).N2 y) \<longrightarrow>\<^isub>c Cut <a>.M (x1).N1"
+| "\<lbrakk>fic (OrR2 <a>.M b,b); fin (OrL (x1).N1 (x2).N2 y,y)\<rbrakk> \<Longrightarrow>
+   Cut <b>.(OrR2 <a>.M b) (y).(OrL (x1).N1 (x2).N2 y) \<longrightarrow>\<^isub>c Cut <a>.M (x2).N2"
+| "\<lbrakk>fin (ImpL <c>.N (y).P z,z); fic (ImpR (x).<a>.M b,b)\<rbrakk> \<Longrightarrow>
+   Cut <b>.(ImpR (x).<a>.M b) (z).(ImpL <c>.N (y).P z) \<longrightarrow>\<^isub>c Cut <a>.(Cut <c>.N (x).M) (y).P"
+| "\<lbrakk>fin (ImpL <c>.N (y).P z,z); fic (ImpR (x).<a>.M b,b)\<rbrakk> \<Longrightarrow>
+   Cut <b>.(ImpR (x).<a>.M b) (z).(ImpL <c>.N (y).P z) \<longrightarrow>\<^isub>c Cut <a>.N (x).(Cut <a>.M (y).P)"
+| "\<not>fic (M,a) \<Longrightarrow> Cut <a>.M (x).N \<longrightarrow>\<^isub>c M[a:=(x).N]"
+| "\<not>fin (N,x) \<Longrightarrow> Cut <a>.M (x).N \<longrightarrow>\<^isub>c N[x:=<a>.M]"
+
+text {* PROOFS *}
+
+lemma validn_eqvt[eqvt]:
+  fixes   pi1:: "name prm"
+  and     pi2:: "coname prm"
+  assumes a: "validn \<Gamma>"
+  shows   "validn (pi1\<bullet>\<Gamma>)" and "validn (pi2\<bullet>\<Gamma>)"
+using a by (induct) (auto simp add: fresh_bij)
+
+lemma validc_eqvt[eqvt]:
+  fixes   pi1:: "name prm"
+  and     pi2:: "coname prm"
+  assumes a: "validc \<Delta>"
+  shows   "validc (pi1\<bullet>\<Delta>)" and "validc (pi2\<bullet>\<Delta>)"
+using a by (induct) (auto simp add: fresh_bij)
+
+text {* Weakening Lemma *}
+
+abbreviation
+  "subn" :: "ctxtn \<Rightarrow> ctxtn \<Rightarrow> bool" (" _ \<lless>n _ " [80,80] 80) 
+where
+  "\<Gamma>1 \<lless>n \<Gamma>2 \<equiv> \<forall>x B. (x,B)\<in>set \<Gamma>1 \<longrightarrow> (x,B)\<in>set \<Gamma>2"
+
+abbreviation
+  "subc" :: "ctxtc \<Rightarrow> ctxtc \<Rightarrow> bool" (" _ \<lless>c _ " [80,80] 80) 
+where
+  "\<Delta>1 \<lless>c \<Delta>2 \<equiv> \<forall>a B. (a,B)\<in>set \<Delta>1 \<longrightarrow> (a,B)\<in>set \<Delta>2"
+
 
 end