# HG changeset patch
# User berghofe
# Date 1229183973 -3600
# Node ID 933145f5a9ba960c869ad9b77490dd996c165dfc
# Parent  bebd671c6055c496e87e653e192e549d3761d7d7# Parent  6b23a58cc67c80442daeb7f36f116172dd15f8d6
merged

diff -r bebd671c6055 -r 933145f5a9ba src/HOL/Nominal/Examples/Class.thy
--- a/src/HOL/Nominal/Examples/Class.thy	Sat Dec 13 16:29:33 2008 +0100
+++ b/src/HOL/Nominal/Examples/Class.thy	Sat Dec 13 16:59:33 2008 +0100
@@ -1,5 +1,3 @@
-(* $Id$ *)
-
 theory Class
 imports "../Nominal" 
 begin
@@ -17,16 +15,22 @@
   | OR   "ty" "ty"   ("_ OR _" [100,100] 100)
   | IMP  "ty" "ty"   ("_ IMP _" [100,100] 100)
 
-instance ty :: size ..
-
-nominal_primrec
+instantiation ty :: size
+begin
+
+nominal_primrec size_ty
+where
   "size (PR s)     = (1::nat)"
-  "size (NOT T)     = 1 + size T"
-  "size (T1 AND T2) = 1 + size T1 + size T2"
-  "size (T1 OR T2)  = 1 + size T1 + size T2"
-  "size (T1 IMP T2) = 1 + size T1 + size T2"
+| "size (NOT T)     = 1 + size T"
+| "size (T1 AND T2) = 1 + size T1 + size T2"
+| "size (T1 OR T2)  = 1 + size T1 + size T2"
+| "size (T1 IMP T2) = 1 + size T1 + size T2"
 by (rule TrueI)+
 
+instance ..
+
+end
+
 lemma ty_cases:
   fixes T::ty
   shows "(\<exists>s. T=PR s) \<or> (\<exists>T'. T=NOT T') \<or> (\<exists>S U. T=S OR U) \<or> (\<exists>S U. T=S AND U) \<or> (\<exists>S U. T=S IMP U)"
@@ -66,25 +70,23 @@
 
 text {* renaming functions *}
 
-consts
-  nrename :: "trm \<Rightarrow> name \<Rightarrow> name \<Rightarrow> trm"      ("_[_\<turnstile>n>_]" [100,100,100] 100) 
+nominal_primrec (freshness_context: "(d::coname,e::coname)") 
   crename :: "trm \<Rightarrow> coname \<Rightarrow> coname \<Rightarrow> trm"  ("_[_\<turnstile>c>_]" [100,100,100] 100) 
-
-nominal_primrec (freshness_context: "(d::coname,e::coname)") 
+where
   "(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)" 
-  "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] = 
+| "\<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"
-  "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] = 
+| "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"
+| "\<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)+
@@ -92,19 +94,21 @@
 done
 
 nominal_primrec (freshness_context: "(u::name,v::name)") 
+  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)" 
-  "\<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)"
-  "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] = 
+| "\<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)"
+| "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] = 
+| "\<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)+
@@ -766,32 +770,30 @@
 apply(simp add: fin_supp)
 done
 
-consts
+nominal_primrec (freshness_context: "(y::name,c::coname,P::trm)")
   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)")
+where
   "(Ax x a){y:=<c>.P} = (if x=y then Cut <c>.P (y).Ax y a else Ax x a)" 
-  "\<lbrakk>a\<sharp>(c,P,N);x\<sharp>(y,P,M)\<rbrakk> \<Longrightarrow> (Cut <a>.M (x).N){y:=<c>.P} = 
+| "\<lbrakk>a\<sharp>(c,P,N);x\<sharp>(y,P,M)\<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}))" 
-  "x\<sharp>(y,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} = 
+| "x\<sharp>(y,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 fresh_fun (\<lambda>x'. 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> 
+| "\<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,P,z) \<Longrightarrow> (AndL1 (x).M z){y:=<c>.P} = 
+| "x\<sharp>(y,P,z) \<Longrightarrow> (AndL1 (x).M z){y:=<c>.P} = 
   (if z=y then fresh_fun (\<lambda>z'. Cut <c>.P (z').AndL1 (x).(M{y:=<c>.P}) z') 
    else AndL1 (x).(M{y:=<c>.P}) z)"
-  "x\<sharp>(y,P,z) \<Longrightarrow> (AndL2 (x).M z){y:=<c>.P} = 
+| "x\<sharp>(y,P,z) \<Longrightarrow> (AndL2 (x).M z){y:=<c>.P} = 
   (if z=y then fresh_fun (\<lambda>z'. 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,P,z);u\<sharp>(y,M,P,z);x\<noteq>u\<rbrakk> \<Longrightarrow> (OrL (x).M (u).N z){y:=<c>.P} = 
+| "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,P,z);u\<sharp>(y,M,P,z);x\<noteq>u\<rbrakk> \<Longrightarrow> (OrL (x).M (u).N z){y:=<c>.P} = 
   (if z=y then fresh_fun (\<lambda>z'. 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,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,P,M,z)\<rbrakk> \<Longrightarrow> (ImpL <a>.M (x).N z){y:=<c>.P} = 
+| "\<lbrakk>a\<sharp>(b,c,P); x\<sharp>(y,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,P,M,z)\<rbrakk> \<Longrightarrow> (ImpL <a>.M (x).N z){y:=<c>.P} = 
   (if y=z then fresh_fun (\<lambda>z'. 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)+
@@ -842,27 +844,29 @@
 done
 
 nominal_primrec (freshness_context: "(d::name,z::coname,P::trm)")
+  substc :: "trm \<Rightarrow> coname \<Rightarrow> name   \<Rightarrow> trm \<Rightarrow> trm" ("_{_:=(_)._}" [100,100,100,100] 100)
+where
   "(Ax x a){d:=(z).P} = (if d=a then Cut <a>.(Ax x a) (z).P else Ax x a)" 
-  "\<lbrakk>a\<sharp>(d,P,N);x\<sharp>(z,P,M)\<rbrakk> \<Longrightarrow> (Cut <a>.M (x).N){d:=(z).P} = 
+| "\<lbrakk>a\<sharp>(d,P,N);x\<sharp>(z,P,M)\<rbrakk> \<Longrightarrow> (Cut <a>.M (x).N){d:=(z).P} = 
   (if N=Ax x d then Cut <a>.(M{d:=(z).P}) (z).P else Cut <a>.(M{d:=(z).P}) (x).(N{d:=(z).P}))" 
-  "x\<sharp>(z,P) \<Longrightarrow> (NotR (x).M a){d:=(z).P} = 
+| "x\<sharp>(z,P) \<Longrightarrow> (NotR (x).M a){d:=(z).P} = 
   (if d=a then fresh_fun (\<lambda>a'. Cut <a'>.NotR (x).(M{d:=(z).P}) a' (z).P) else NotR (x).(M{d:=(z).P}) a)" 
-  "a\<sharp>(d,P) \<Longrightarrow> (NotL <a>.M x){d:=(z).P} = NotL <a>.(M{d:=(z).P}) x" 
-  "\<lbrakk>a\<sharp>(P,c,N,d);b\<sharp>(P,c,M,d);b\<noteq>a\<rbrakk> \<Longrightarrow> (AndR <a>.M <b>.N c){d:=(z).P} = 
+| "a\<sharp>(d,P) \<Longrightarrow> (NotL <a>.M x){d:=(z).P} = NotL <a>.(M{d:=(z).P}) x" 
+| "\<lbrakk>a\<sharp>(P,c,N,d);b\<sharp>(P,c,M,d);b\<noteq>a\<rbrakk> \<Longrightarrow> (AndR <a>.M <b>.N c){d:=(z).P} = 
   (if d=c then fresh_fun (\<lambda>a'. Cut <a'>.(AndR <a>.(M{d:=(z).P}) <b>.(N{d:=(z).P}) a') (z).P)
    else AndR <a>.(M{d:=(z).P}) <b>.(N{d:=(z).P}) c)" 
-  "x\<sharp>(y,z,P) \<Longrightarrow> (AndL1 (x).M y){d:=(z).P} = AndL1 (x).(M{d:=(z).P}) y"
-  "x\<sharp>(y,P,z) \<Longrightarrow> (AndL2 (x).M y){d:=(z).P} = AndL2 (x).(M{d:=(z).P}) y"
-  "a\<sharp>(d,P,b) \<Longrightarrow> (OrR1 <a>.M b){d:=(z).P} = 
+| "x\<sharp>(y,z,P) \<Longrightarrow> (AndL1 (x).M y){d:=(z).P} = AndL1 (x).(M{d:=(z).P}) y"
+| "x\<sharp>(y,P,z) \<Longrightarrow> (AndL2 (x).M y){d:=(z).P} = AndL2 (x).(M{d:=(z).P}) y"
+| "a\<sharp>(d,P,b) \<Longrightarrow> (OrR1 <a>.M b){d:=(z).P} = 
   (if d=b then fresh_fun (\<lambda>a'. Cut <a'>.OrR1 <a>.(M{d:=(z).P}) a' (z).P) else OrR1 <a>.(M{d:=(z).P}) b)"
-  "a\<sharp>(d,P,b) \<Longrightarrow> (OrR2 <a>.M b){d:=(z).P} = 
+| "a\<sharp>(d,P,b) \<Longrightarrow> (OrR2 <a>.M b){d:=(z).P} = 
   (if d=b then fresh_fun (\<lambda>a'. Cut <a'>.OrR2 <a>.(M{d:=(z).P}) a' (z).P) else OrR2 <a>.(M{d:=(z).P}) b)"
-  "\<lbrakk>x\<sharp>(N,z,P,u);y\<sharp>(M,z,P,u);x\<noteq>y\<rbrakk> \<Longrightarrow> (OrL (x).M (y).N u){d:=(z).P} = 
+| "\<lbrakk>x\<sharp>(N,z,P,u);y\<sharp>(M,z,P,u);x\<noteq>y\<rbrakk> \<Longrightarrow> (OrL (x).M (y).N u){d:=(z).P} = 
   OrL (x).(M{d:=(z).P}) (y).(N{d:=(z).P}) u" 
-  "\<lbrakk>a\<sharp>(b,d,P); x\<sharp>(z,P)\<rbrakk> \<Longrightarrow> (ImpR (x).<a>.M b){d:=(z).P} = 
+| "\<lbrakk>a\<sharp>(b,d,P); x\<sharp>(z,P)\<rbrakk> \<Longrightarrow> (ImpR (x).<a>.M b){d:=(z).P} = 
   (if d=b then fresh_fun (\<lambda>a'. Cut <a'>.ImpR (x).<a>.(M{d:=(z).P}) a' (z).P) 
    else ImpR (x).<a>.(M{d:=(z).P}) b)"
-  "\<lbrakk>a\<sharp>(N,d,P);x\<sharp>(y,z,P,M)\<rbrakk> \<Longrightarrow> (ImpL <a>.M (x).N y){d:=(z).P} = 
+| "\<lbrakk>a\<sharp>(N,d,P);x\<sharp>(y,z,P,M)\<rbrakk> \<Longrightarrow> (ImpL <a>.M (x).N y){d:=(z).P} = 
   ImpL <a>.(M{d:=(z).P}) (x).(N{d:=(z).P}) y"
 apply(finite_guess)+
 apply(rule TrueI)+
@@ -10305,11 +10309,10 @@
 lemma BINDINGc_decreasing:
   shows "X\<subseteq>Y \<Longrightarrow> BINDINGc B Y \<subseteq> BINDINGc B X"
 by (simp add: BINDINGc_def) (blast) 
-
-consts
-  NOTRIGHT::"ty \<Rightarrow> ntrm set \<Rightarrow> ctrm set"
   
 nominal_primrec
+  NOTRIGHT :: "ty \<Rightarrow> ntrm set \<Rightarrow> ctrm set"
+where
  "NOTRIGHT (NOT B) X = { <a>:NotR (x).M a | a x M. fic (NotR (x).M a) a \<and> (x):M \<in> X }"
 apply(rule TrueI)+
 done
@@ -10365,11 +10368,10 @@
 apply(drule pt_bij1[OF pt_coname_inst, OF at_coname_inst])
 apply(simp add: swap_simps)
 done
-
-consts
-  NOTLEFT::"ty \<Rightarrow> ctrm set \<Rightarrow> ntrm set"
   
 nominal_primrec
+  NOTLEFT :: "ty \<Rightarrow> ctrm set \<Rightarrow> ntrm set"
+where
  "NOTLEFT (NOT B) X = { (x):NotL <a>.M x | a x M. fin (NotL <a>.M x) x \<and> <a>:M \<in> X }"
 apply(rule TrueI)+
 done
@@ -10425,11 +10427,10 @@
 apply(drule pt_bij1[OF pt_coname_inst, OF at_coname_inst])
 apply(simp add: swap_simps)
 done
-
-consts
-  ANDRIGHT::"ty \<Rightarrow> ctrm set \<Rightarrow> ctrm set \<Rightarrow> ctrm set"
   
 nominal_primrec
+  ANDRIGHT :: "ty \<Rightarrow> ctrm set \<Rightarrow> ctrm set \<Rightarrow> ctrm set"
+where
  "ANDRIGHT (B AND C) X Y = 
             { <c>:AndR <a>.M <b>.N c | c a b M N. fic (AndR <a>.M <b>.N c) c \<and> <a>:M \<in> X \<and> <b>:N \<in> Y }"
 apply(rule TrueI)+
@@ -10505,10 +10506,9 @@
 apply(simp)
 done
 
-consts
-  ANDLEFT1::"ty \<Rightarrow> ntrm set \<Rightarrow> ntrm set"
-
 nominal_primrec
+  ANDLEFT1 :: "ty \<Rightarrow> ntrm set \<Rightarrow> ntrm set"
+where
  "ANDLEFT1 (B AND C) X = { (y):AndL1 (x).M y | x y M. fin (AndL1 (x).M y) y \<and> (x):M \<in> X }"
 apply(rule TrueI)+
 done
@@ -10565,10 +10565,9 @@
 apply(simp add: swap_simps)
 done
 
-consts
-  ANDLEFT2::"ty \<Rightarrow> ntrm set \<Rightarrow> ntrm set"
-
 nominal_primrec
+  ANDLEFT2 :: "ty \<Rightarrow> ntrm set \<Rightarrow> ntrm set"
+where
  "ANDLEFT2 (B AND C) X = { (y):AndL2 (x).M y | x y M. fin (AndL2 (x).M y) y \<and> (x):M \<in> X }"
 apply(rule TrueI)+
 done
@@ -10625,10 +10624,9 @@
 apply(simp add: swap_simps)
 done
 
-consts
-  ORLEFT::"ty \<Rightarrow> ntrm set \<Rightarrow> ntrm set \<Rightarrow> ntrm set"
-  
 nominal_primrec
+  ORLEFT :: "ty \<Rightarrow> ntrm set \<Rightarrow> ntrm set \<Rightarrow> ntrm set"
+where
  "ORLEFT (B OR C) X Y = 
             { (z):OrL (x).M (y).N z | x y z M N. fin (OrL (x).M (y).N z) z \<and> (x):M \<in> X \<and> (y):N \<in> Y }"
 apply(rule TrueI)+
@@ -10704,10 +10702,9 @@
 apply(simp add: swap_simps)
 done
 
-consts
-  ORRIGHT1::"ty \<Rightarrow> ctrm set \<Rightarrow> ctrm set"
-
 nominal_primrec
+  ORRIGHT1 :: "ty \<Rightarrow> ctrm set \<Rightarrow> ctrm set"
+where
  "ORRIGHT1 (B OR C) X = { <b>:OrR1 <a>.M b | a b M. fic (OrR1 <a>.M b) b \<and> <a>:M \<in> X }"
 apply(rule TrueI)+
 done
@@ -10764,10 +10761,9 @@
 apply(simp)
 done
 
-consts
-  ORRIGHT2::"ty \<Rightarrow> ctrm set \<Rightarrow> ctrm set"
-
 nominal_primrec
+  ORRIGHT2 :: "ty \<Rightarrow> ctrm set \<Rightarrow> ctrm set"
+where
  "ORRIGHT2 (B OR C) X = { <b>:OrR2 <a>.M b | a b M. fic (OrR2 <a>.M b) b \<and> <a>:M \<in> X }"
 apply(rule TrueI)+
 done
@@ -10824,10 +10820,9 @@
 apply(simp)
 done
 
-consts
-  IMPRIGHT::"ty \<Rightarrow> ntrm set \<Rightarrow> ctrm set \<Rightarrow> ntrm set \<Rightarrow> ctrm set \<Rightarrow> ctrm set"
-
 nominal_primrec
+  IMPRIGHT :: "ty \<Rightarrow> ntrm set \<Rightarrow> ctrm set \<Rightarrow> ntrm set \<Rightarrow> ctrm set \<Rightarrow> ctrm set"
+where
  "IMPRIGHT (B IMP C) X Y Z U= 
         { <b>:ImpR (x).<a>.M b | x a b M. fic (ImpR (x).<a>.M b) b 
                                         \<and> (\<forall>z P. x\<sharp>(z,P) \<and> (z):P \<in> Z \<longrightarrow> (x):(M{a:=(z).P}) \<in> X)
@@ -10954,10 +10949,9 @@
 apply(perm_simp add: nsubst_eqvt fresh_right)
 done
 
-consts
-  IMPLEFT::"ty \<Rightarrow> ctrm set \<Rightarrow> ntrm set \<Rightarrow> ntrm set"
-
 nominal_primrec
+  IMPLEFT :: "ty \<Rightarrow> ctrm set \<Rightarrow> ntrm set \<Rightarrow> ntrm set"
+where
  "IMPLEFT (B IMP C) X Y = 
         { (y):ImpL <a>.M (x).N y | x a y M N. fin (ImpL <a>.M (x).N y) y \<and> <a>:M \<in> X \<and> (x):N \<in> Y }"
 apply(rule TrueI)+
@@ -17800,23 +17794,21 @@
 apply(auto)
 done 
 
-consts
+nominal_primrec (freshness_context: "\<theta>n::(name\<times>coname\<times>trm)")
   stn :: "trm\<Rightarrow>(name\<times>coname\<times>trm) list\<Rightarrow>trm" 
-  stc :: "trm\<Rightarrow>(coname\<times>name\<times>trm) list\<Rightarrow>trm" 
-
-nominal_primrec (freshness_context: "\<theta>n::(name\<times>coname\<times>trm)")
+where
   "stn (Ax x a) \<theta>n = lookupc x a \<theta>n"
-  "\<lbrakk>a\<sharp>(N,\<theta>n);x\<sharp>(M,\<theta>n)\<rbrakk> \<Longrightarrow> stn (Cut <a>.M (x).N) \<theta>n = (Cut <a>.M (x).N)" 
-  "x\<sharp>\<theta>n \<Longrightarrow> stn (NotR (x).M a) \<theta>n = (NotR (x).M a)"
-  "a\<sharp>\<theta>n \<Longrightarrow>stn (NotL <a>.M x) \<theta>n = (NotL <a>.M x)"
-  "\<lbrakk>a\<sharp>(N,d,b,\<theta>n);b\<sharp>(M,d,a,\<theta>n)\<rbrakk> \<Longrightarrow> stn (AndR <a>.M <b>.N d) \<theta>n = (AndR <a>.M <b>.N d)"
-  "x\<sharp>(z,\<theta>n) \<Longrightarrow> stn (AndL1 (x).M z) \<theta>n = (AndL1 (x).M z)"
-  "x\<sharp>(z,\<theta>n) \<Longrightarrow> stn (AndL2 (x).M z) \<theta>n = (AndL2 (x).M z)"
-  "a\<sharp>(b,\<theta>n) \<Longrightarrow> stn (OrR1 <a>.M b) \<theta>n = (OrR1 <a>.M b)"
-  "a\<sharp>(b,\<theta>n) \<Longrightarrow> stn (OrR2 <a>.M b) \<theta>n = (OrR2 <a>.M b)"
-  "\<lbrakk>x\<sharp>(N,z,u,\<theta>n);u\<sharp>(M,z,x,\<theta>n)\<rbrakk> \<Longrightarrow> stn (OrL (x).M (u).N z) \<theta>n = (OrL (x).M (u).N z)"
-  "\<lbrakk>a\<sharp>(b,\<theta>n);x\<sharp>\<theta>n\<rbrakk> \<Longrightarrow> stn (ImpR (x).<a>.M b) \<theta>n = (ImpR (x).<a>.M b)"
-  "\<lbrakk>a\<sharp>(N,\<theta>n);x\<sharp>(M,z,\<theta>n)\<rbrakk> \<Longrightarrow> stn (ImpL <a>.M (x).N z) \<theta>n = (ImpL <a>.M (x).N z)"
+| "\<lbrakk>a\<sharp>(N,\<theta>n);x\<sharp>(M,\<theta>n)\<rbrakk> \<Longrightarrow> stn (Cut <a>.M (x).N) \<theta>n = (Cut <a>.M (x).N)" 
+| "x\<sharp>\<theta>n \<Longrightarrow> stn (NotR (x).M a) \<theta>n = (NotR (x).M a)"
+| "a\<sharp>\<theta>n \<Longrightarrow>stn (NotL <a>.M x) \<theta>n = (NotL <a>.M x)"
+| "\<lbrakk>a\<sharp>(N,d,b,\<theta>n);b\<sharp>(M,d,a,\<theta>n)\<rbrakk> \<Longrightarrow> stn (AndR <a>.M <b>.N d) \<theta>n = (AndR <a>.M <b>.N d)"
+| "x\<sharp>(z,\<theta>n) \<Longrightarrow> stn (AndL1 (x).M z) \<theta>n = (AndL1 (x).M z)"
+| "x\<sharp>(z,\<theta>n) \<Longrightarrow> stn (AndL2 (x).M z) \<theta>n = (AndL2 (x).M z)"
+| "a\<sharp>(b,\<theta>n) \<Longrightarrow> stn (OrR1 <a>.M b) \<theta>n = (OrR1 <a>.M b)"
+| "a\<sharp>(b,\<theta>n) \<Longrightarrow> stn (OrR2 <a>.M b) \<theta>n = (OrR2 <a>.M b)"
+| "\<lbrakk>x\<sharp>(N,z,u,\<theta>n);u\<sharp>(M,z,x,\<theta>n)\<rbrakk> \<Longrightarrow> stn (OrL (x).M (u).N z) \<theta>n = (OrL (x).M (u).N z)"
+| "\<lbrakk>a\<sharp>(b,\<theta>n);x\<sharp>\<theta>n\<rbrakk> \<Longrightarrow> stn (ImpR (x).<a>.M b) \<theta>n = (ImpR (x).<a>.M b)"
+| "\<lbrakk>a\<sharp>(N,\<theta>n);x\<sharp>(M,z,\<theta>n)\<rbrakk> \<Longrightarrow> stn (ImpL <a>.M (x).N z) \<theta>n = (ImpL <a>.M (x).N z)"
 apply(finite_guess)+
 apply(rule TrueI)+
 apply(simp add: abs_fresh abs_supp fin_supp)+
@@ -17824,18 +17816,20 @@
 done
 
 nominal_primrec (freshness_context: "\<theta>c::(coname\<times>name\<times>trm)")
+  stc :: "trm\<Rightarrow>(coname\<times>name\<times>trm) list\<Rightarrow>trm" 
+where
   "stc (Ax x a) \<theta>c = lookupd x a \<theta>c"
-  "\<lbrakk>a\<sharp>(N,\<theta>c);x\<sharp>(M,\<theta>c)\<rbrakk> \<Longrightarrow> stc (Cut <a>.M (x).N) \<theta>c = (Cut <a>.M (x).N)" 
-  "x\<sharp>\<theta>c \<Longrightarrow> stc (NotR (x).M a) \<theta>c = (NotR (x).M a)"
-  "a\<sharp>\<theta>c \<Longrightarrow> stc (NotL <a>.M x) \<theta>c = (NotL <a>.M x)"
-  "\<lbrakk>a\<sharp>(N,d,b,\<theta>c);b\<sharp>(M,d,a,\<theta>c)\<rbrakk> \<Longrightarrow> stc (AndR <a>.M <b>.N d) \<theta>c = (AndR <a>.M <b>.N d)"
-  "x\<sharp>(z,\<theta>c) \<Longrightarrow> stc (AndL1 (x).M z) \<theta>c = (AndL1 (x).M z)"
-  "x\<sharp>(z,\<theta>c) \<Longrightarrow> stc (AndL2 (x).M z) \<theta>c = (AndL2 (x).M z)"
-  "a\<sharp>(b,\<theta>c) \<Longrightarrow> stc (OrR1 <a>.M b) \<theta>c = (OrR1 <a>.M b)"
-  "a\<sharp>(b,\<theta>c) \<Longrightarrow> stc (OrR2 <a>.M b) \<theta>c = (OrR2 <a>.M b)"
-  "\<lbrakk>x\<sharp>(N,z,u,\<theta>c);u\<sharp>(M,z,x,\<theta>c)\<rbrakk> \<Longrightarrow> stc (OrL (x).M (u).N z) \<theta>c = (OrL (x).M (u).N z)"
-  "\<lbrakk>a\<sharp>(b,\<theta>c);x\<sharp>\<theta>c\<rbrakk> \<Longrightarrow> stc (ImpR (x).<a>.M b) \<theta>c = (ImpR (x).<a>.M b)"
-  "\<lbrakk>a\<sharp>(N,\<theta>c);x\<sharp>(M,z,\<theta>c)\<rbrakk> \<Longrightarrow> stc (ImpL <a>.M (x).N z) \<theta>c = (ImpL <a>.M (x).N z)"
+| "\<lbrakk>a\<sharp>(N,\<theta>c);x\<sharp>(M,\<theta>c)\<rbrakk> \<Longrightarrow> stc (Cut <a>.M (x).N) \<theta>c = (Cut <a>.M (x).N)" 
+| "x\<sharp>\<theta>c \<Longrightarrow> stc (NotR (x).M a) \<theta>c = (NotR (x).M a)"
+| "a\<sharp>\<theta>c \<Longrightarrow> stc (NotL <a>.M x) \<theta>c = (NotL <a>.M x)"
+| "\<lbrakk>a\<sharp>(N,d,b,\<theta>c);b\<sharp>(M,d,a,\<theta>c)\<rbrakk> \<Longrightarrow> stc (AndR <a>.M <b>.N d) \<theta>c = (AndR <a>.M <b>.N d)"
+| "x\<sharp>(z,\<theta>c) \<Longrightarrow> stc (AndL1 (x).M z) \<theta>c = (AndL1 (x).M z)"
+| "x\<sharp>(z,\<theta>c) \<Longrightarrow> stc (AndL2 (x).M z) \<theta>c = (AndL2 (x).M z)"
+| "a\<sharp>(b,\<theta>c) \<Longrightarrow> stc (OrR1 <a>.M b) \<theta>c = (OrR1 <a>.M b)"
+| "a\<sharp>(b,\<theta>c) \<Longrightarrow> stc (OrR2 <a>.M b) \<theta>c = (OrR2 <a>.M b)"
+| "\<lbrakk>x\<sharp>(N,z,u,\<theta>c);u\<sharp>(M,z,x,\<theta>c)\<rbrakk> \<Longrightarrow> stc (OrL (x).M (u).N z) \<theta>c = (OrL (x).M (u).N z)"
+| "\<lbrakk>a\<sharp>(b,\<theta>c);x\<sharp>\<theta>c\<rbrakk> \<Longrightarrow> stc (ImpR (x).<a>.M b) \<theta>c = (ImpR (x).<a>.M b)"
+| "\<lbrakk>a\<sharp>(N,\<theta>c);x\<sharp>(M,z,\<theta>c)\<rbrakk> \<Longrightarrow> stc (ImpL <a>.M (x).N z) \<theta>c = (ImpL <a>.M (x).N z)"
 apply(finite_guess)+
 apply(rule TrueI)+
 apply(simp add: abs_fresh abs_supp fin_supp)+
@@ -17926,51 +17920,50 @@
 apply(perm_simp)
 done
 
-consts
+nominal_primrec (freshness_context: "(\<theta>n::(name\<times>coname\<times>trm) list,\<theta>c::(coname\<times>name\<times>trm) list)")
   psubst :: "(name\<times>coname\<times>trm) list\<Rightarrow>(coname\<times>name\<times>trm) list\<Rightarrow>trm\<Rightarrow>trm" ("_,_<_>" [100,100,100] 100) 
-
-nominal_primrec (freshness_context: "(\<theta>n::(name\<times>coname\<times>trm) list,\<theta>c::(coname\<times>name\<times>trm) list)")
+where
   "\<theta>n,\<theta>c<Ax x a> = lookup x a \<theta>n \<theta>c" 
-  "\<lbrakk>a\<sharp>(N,\<theta>n,\<theta>c);x\<sharp>(M,\<theta>n,\<theta>c)\<rbrakk> \<Longrightarrow> \<theta>n,\<theta>c<Cut <a>.M (x).N> = 
+| "\<lbrakk>a\<sharp>(N,\<theta>n,\<theta>c);x\<sharp>(M,\<theta>n,\<theta>c)\<rbrakk> \<Longrightarrow> \<theta>n,\<theta>c<Cut <a>.M (x).N> = 
    Cut <a>.(if \<exists>x. M=Ax x a then stn M \<theta>n else \<theta>n,\<theta>c<M>) 
        (x).(if \<exists>a. N=Ax x a then stc N \<theta>c else \<theta>n,\<theta>c<N>)" 
-  "x\<sharp>(\<theta>n,\<theta>c) \<Longrightarrow> \<theta>n,\<theta>c<NotR (x).M a> = 
+| "x\<sharp>(\<theta>n,\<theta>c) \<Longrightarrow> \<theta>n,\<theta>c<NotR (x).M a> = 
   (case (findc \<theta>c a) of 
        Some (u,P) \<Rightarrow> fresh_fun (\<lambda>a'. Cut <a'>.NotR (x).(\<theta>n,\<theta>c<M>) a' (u).P) 
      | None \<Rightarrow> NotR (x).(\<theta>n,\<theta>c<M>) a)"
-  "a\<sharp>(\<theta>n,\<theta>c) \<Longrightarrow> \<theta>n,\<theta>c<NotL <a>.M x> = 
+| "a\<sharp>(\<theta>n,\<theta>c) \<Longrightarrow> \<theta>n,\<theta>c<NotL <a>.M x> = 
   (case (findn \<theta>n x) of 
        Some (c,P) \<Rightarrow> fresh_fun (\<lambda>x'. Cut <c>.P (x').(NotL <a>.(\<theta>n,\<theta>c<M>) x')) 
      | None \<Rightarrow> NotL <a>.(\<theta>n,\<theta>c<M>) x)"
-  "\<lbrakk>a\<sharp>(N,c,\<theta>n,\<theta>c);b\<sharp>(M,c,\<theta>n,\<theta>c);b\<noteq>a\<rbrakk> \<Longrightarrow> (\<theta>n,\<theta>c<AndR <a>.M <b>.N c>) = 
+| "\<lbrakk>a\<sharp>(N,c,\<theta>n,\<theta>c);b\<sharp>(M,c,\<theta>n,\<theta>c);b\<noteq>a\<rbrakk> \<Longrightarrow> (\<theta>n,\<theta>c<AndR <a>.M <b>.N c>) = 
   (case (findc \<theta>c c) of 
        Some (x,P) \<Rightarrow> fresh_fun (\<lambda>a'. Cut <a'>.(AndR <a>.(\<theta>n,\<theta>c<M>) <b>.(\<theta>n,\<theta>c<N>) a') (x).P)
      | None \<Rightarrow> AndR <a>.(\<theta>n,\<theta>c<M>) <b>.(\<theta>n,\<theta>c<N>) c)"
-  "x\<sharp>(z,\<theta>n,\<theta>c) \<Longrightarrow> (\<theta>n,\<theta>c<AndL1 (x).M z>) = 
+| "x\<sharp>(z,\<theta>n,\<theta>c) \<Longrightarrow> (\<theta>n,\<theta>c<AndL1 (x).M z>) = 
   (case (findn \<theta>n z) of 
        Some (c,P) \<Rightarrow> fresh_fun (\<lambda>z'. Cut <c>.P (z').AndL1 (x).(\<theta>n,\<theta>c<M>) z') 
      | None \<Rightarrow> AndL1 (x).(\<theta>n,\<theta>c<M>) z)"
-  "x\<sharp>(z,\<theta>n,\<theta>c) \<Longrightarrow> (\<theta>n,\<theta>c<AndL2 (x).M z>) = 
+| "x\<sharp>(z,\<theta>n,\<theta>c) \<Longrightarrow> (\<theta>n,\<theta>c<AndL2 (x).M z>) = 
   (case (findn \<theta>n z) of 
        Some (c,P) \<Rightarrow> fresh_fun (\<lambda>z'. Cut <c>.P (z').AndL2 (x).(\<theta>n,\<theta>c<M>) z') 
      | None \<Rightarrow> AndL2 (x).(\<theta>n,\<theta>c<M>) z)"
-  "\<lbrakk>x\<sharp>(N,z,\<theta>n,\<theta>c);u\<sharp>(M,z,\<theta>n,\<theta>c);x\<noteq>u\<rbrakk> \<Longrightarrow> (\<theta>n,\<theta>c<OrL (x).M (u).N z>) =
+| "\<lbrakk>x\<sharp>(N,z,\<theta>n,\<theta>c);u\<sharp>(M,z,\<theta>n,\<theta>c);x\<noteq>u\<rbrakk> \<Longrightarrow> (\<theta>n,\<theta>c<OrL (x).M (u).N z>) =
   (case (findn \<theta>n z) of  
        Some (c,P) \<Rightarrow> fresh_fun (\<lambda>z'. Cut <c>.P (z').OrL (x).(\<theta>n,\<theta>c<M>) (u).(\<theta>n,\<theta>c<N>) z') 
      | None \<Rightarrow> OrL (x).(\<theta>n,\<theta>c<M>) (u).(\<theta>n,\<theta>c<N>) z)"
-  "a\<sharp>(b,\<theta>n,\<theta>c) \<Longrightarrow> (\<theta>n,\<theta>c<OrR1 <a>.M b>) = 
+| "a\<sharp>(b,\<theta>n,\<theta>c) \<Longrightarrow> (\<theta>n,\<theta>c<OrR1 <a>.M b>) = 
   (case (findc \<theta>c b) of
        Some (x,P) \<Rightarrow> fresh_fun (\<lambda>a'. Cut <a'>.OrR1 <a>.(\<theta>n,\<theta>c<M>) a' (x).P) 
      | None \<Rightarrow> OrR1 <a>.(\<theta>n,\<theta>c<M>) b)"
-  "a\<sharp>(b,\<theta>n,\<theta>c) \<Longrightarrow> (\<theta>n,\<theta>c<OrR2 <a>.M b>) = 
+| "a\<sharp>(b,\<theta>n,\<theta>c) \<Longrightarrow> (\<theta>n,\<theta>c<OrR2 <a>.M b>) = 
   (case (findc \<theta>c b) of
        Some (x,P) \<Rightarrow> fresh_fun (\<lambda>a'. Cut <a'>.OrR2 <a>.(\<theta>n,\<theta>c<M>) a' (x).P) 
      | None \<Rightarrow> OrR2 <a>.(\<theta>n,\<theta>c<M>) b)"
-  "\<lbrakk>a\<sharp>(b,\<theta>n,\<theta>c); x\<sharp>(\<theta>n,\<theta>c)\<rbrakk> \<Longrightarrow> (\<theta>n,\<theta>c<ImpR (x).<a>.M b>) = 
+| "\<lbrakk>a\<sharp>(b,\<theta>n,\<theta>c); x\<sharp>(\<theta>n,\<theta>c)\<rbrakk> \<Longrightarrow> (\<theta>n,\<theta>c<ImpR (x).<a>.M b>) = 
   (case (findc \<theta>c b) of
        Some (z,P) \<Rightarrow> fresh_fun (\<lambda>a'. Cut <a'>.ImpR (x).<a>.(\<theta>n,\<theta>c<M>) a' (z).P)
      | None \<Rightarrow> ImpR (x).<a>.(\<theta>n,\<theta>c<M>) b)"
-  "\<lbrakk>a\<sharp>(N,\<theta>n,\<theta>c); x\<sharp>(z,M,\<theta>n,\<theta>c)\<rbrakk> \<Longrightarrow> (\<theta>n,\<theta>c<ImpL <a>.M (x).N z>) = 
+| "\<lbrakk>a\<sharp>(N,\<theta>n,\<theta>c); x\<sharp>(z,M,\<theta>n,\<theta>c)\<rbrakk> \<Longrightarrow> (\<theta>n,\<theta>c<ImpL <a>.M (x).N z>) = 
   (case (findn \<theta>n z) of
        Some (c,P) \<Rightarrow> fresh_fun (\<lambda>z'. Cut <c>.P (z').ImpL <a>.(\<theta>n,\<theta>c<M>) (x).(\<theta>n,\<theta>c<N>) z') 
      | None \<Rightarrow> ImpL <a>.(\<theta>n,\<theta>c<M>) (x).(\<theta>n,\<theta>c<N>) z)"
diff -r bebd671c6055 -r 933145f5a9ba src/HOL/Nominal/Examples/W.thy
--- a/src/HOL/Nominal/Examples/W.thy	Sat Dec 13 16:29:33 2008 +0100
+++ b/src/HOL/Nominal/Examples/W.thy	Sat Dec 13 16:59:33 2008 +0100
@@ -1,5 +1,3 @@
-(* "$Id$" *)
-
 theory W
 imports Nominal
 begin
@@ -50,26 +48,68 @@
   Ctxt  = "(var\<times>tyS) list" 
 
 text {* free type variables *}
-consts
-  ftv    :: "'a \<Rightarrow> tvar list"
+
+class ftv = type +
+  fixes ftv :: "'a \<Rightarrow> tvar list"
+
+instantiation * :: (ftv, ftv) ftv
+begin
+
+primrec ftv_prod
+where
+ "ftv (x::'a::ftv, y::'b::ftv) = (ftv x)@(ftv y)"
+
+instance ..
+
+end
 
-primrec (ftv_of_prod)
- "ftv (x,y) = (ftv x)@(ftv y)"
+instantiation tvar :: ftv
+begin
+
+definition
+  ftv_of_tvar[simp]:  "ftv X \<equiv> [(X::tvar)]"
 
-defs (overloaded)
-  ftv_of_tvar[simp]:  "ftv X \<equiv> [(X::tvar)]"
+instance ..
+
+end
+
+instantiation var :: ftv
+begin
+
+definition
   ftv_of_var[simp]:   "ftv (x::var) \<equiv> []" 
 
-primrec (ftv_of_list)
+instance ..
+
+end
+
+instantiation list :: (ftv) ftv
+begin
+
+primrec ftv_list
+where
   "ftv [] = []"
-  "ftv (x#xs) = (ftv x)@(ftv xs)"
+| "ftv (x#xs) = (ftv x)@(ftv xs)"
+
+instance ..
+
+end
 
 (* free type-variables of types *)
-nominal_primrec (ftv_ty)
+
+instantiation ty :: ftv
+begin
+
+nominal_primrec ftv_ty
+where
   "ftv (TVar X) = [X]"
-  "ftv (T\<^isub>1\<rightarrow>T\<^isub>2) = (ftv T\<^isub>1)@(ftv T\<^isub>2)"
+| "ftv (T\<^isub>1\<rightarrow>T\<^isub>2) = (ftv T\<^isub>1)@(ftv T\<^isub>2)"
 by (rule TrueI)+
 
+instance ..
+
+end
+
 lemma ftv_ty_eqvt[eqvt]:
   fixes pi::"tvar prm"
   and   T::"ty"
@@ -77,9 +117,13 @@
 by (nominal_induct T rule: ty.strong_induct)
    (perm_simp add: append_eqvt)+
 
-nominal_primrec (ftv_tyS)
+instantiation tyS :: ftv
+begin
+
+nominal_primrec ftv_tyS
+where
   "ftv (Ty T)    = ftv T"
-  "ftv (\<forall>[X].S) = (ftv S) - [X]"
+| "ftv (\<forall>[X].S) = (ftv S) - [X]"
 apply(finite_guess add: ftv_ty_eqvt fs_tvar1)+
 apply(rule TrueI)+
 apply(rule difference_fresh)
@@ -87,6 +131,10 @@
 apply(fresh_guess add: ftv_ty_eqvt fs_tvar1)+
 done
 
+instance ..
+
+end
+
 lemma ftv_tyS_eqvt[eqvt]:
   fixes pi::"tvar prm"
   and   S::"tyS"
@@ -140,11 +188,11 @@
 
 types Subst = "(tvar\<times>ty) list"
 
-consts
- psubst :: "Subst \<Rightarrow> 'a \<Rightarrow> 'a"       ("_<_>" [100,60] 120)
+class psubst =
+  fixes psubst :: "Subst \<Rightarrow> 'a \<Rightarrow> 'a"       ("_<_>" [100,60] 120)
 
 abbreviation 
-  subst :: "'a \<Rightarrow> tvar \<Rightarrow> ty \<Rightarrow> 'a"  ("_[_::=_]" [100,100,100] 100)
+  subst :: "'a::psubst \<Rightarrow> tvar \<Rightarrow> ty \<Rightarrow> 'a"  ("_[_::=_]" [100,100,100] 100)
 where
   "smth[X::=T] \<equiv> ([(X,T)])<smth>" 
 
@@ -159,11 +207,19 @@
   shows "pi\<bullet>(lookup \<theta> X) = lookup (pi\<bullet>\<theta>) (pi\<bullet>X)"
 by (induct \<theta>) (auto simp add: eqvts)
 
-nominal_primrec (psubst_ty)
+instantiation ty :: psubst
+begin
+
+nominal_primrec psubst_ty
+where
   "\<theta><TVar X>   = lookup \<theta> X"
-  "\<theta><T\<^isub>1 \<rightarrow> T\<^isub>2> = (\<theta><T\<^isub>1>) \<rightarrow> (\<theta><T\<^isub>2>)"
+| "\<theta><T\<^isub>1 \<rightarrow> T\<^isub>2> = (\<theta><T\<^isub>1>) \<rightarrow> (\<theta><T\<^isub>2>)"
 by (rule TrueI)+
 
+instance ..
+
+end
+
 lemma psubst_ty_eqvt[eqvt]:
   fixes pi1::"tvar prm"
   and   \<theta>::"Subst"