--- 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