merged
authorberghofe
Sat Dec 13 17:13:09 2008 +0100 (2008-12-13)
changeset 2910166fe138979f4
parent 29096 1b8e021e8c1f
parent 29100 933145f5a9ba
child 29102 2e1011dcd577
merged
     1.1 --- a/src/HOL/Nominal/Examples/CK_Machine.thy	Sat Dec 13 15:35:29 2008 +0100
     1.2 +++ b/src/HOL/Nominal/Examples/CK_Machine.thy	Sat Dec 13 17:13:09 2008 +0100
     1.3 @@ -1,5 +1,3 @@
     1.4 -(* $Id$ *)
     1.5 -
     1.6  theory CK_Machine 
     1.7    imports "../Nominal" 
     1.8  begin
     1.9 @@ -41,21 +39,21 @@
    1.10  
    1.11  section {* Capture-Avoiding Substitution *}
    1.12  
    1.13 -consts subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam"  ("_[_::=_]" [100,100,100] 100)
    1.14 -
    1.15  nominal_primrec
    1.16 +  subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam"  ("_[_::=_]" [100,100,100] 100)
    1.17 +where
    1.18    "(VAR x)[y::=s] = (if x=y then s else (VAR x))"
    1.19 -  "(APP t\<^isub>1 t\<^isub>2)[y::=s] = APP (t\<^isub>1[y::=s]) (t\<^isub>2[y::=s])"
    1.20 -  "x\<sharp>(y,s) \<Longrightarrow> (LAM [x].t)[y::=s] = LAM [x].(t[y::=s])"
    1.21 -  "(NUM n)[y::=s] = NUM n"
    1.22 -  "(t\<^isub>1 -- t\<^isub>2)[y::=s] = (t\<^isub>1[y::=s]) -- (t\<^isub>2[y::=s])"
    1.23 -  "(t\<^isub>1 ++ t\<^isub>2)[y::=s] = (t\<^isub>1[y::=s]) ++ (t\<^isub>2[y::=s])"
    1.24 -  "x\<sharp>(y,s) \<Longrightarrow> (FIX [x].t)[y::=s] = FIX [x].(t[y::=s])"
    1.25 -  "TRUE[y::=s] = TRUE"
    1.26 -  "FALSE[y::=s] = FALSE"
    1.27 -  "(IF t1 t2 t3)[y::=s] = IF (t1[y::=s]) (t2[y::=s]) (t3[y::=s])"
    1.28 -  "(ZET t)[y::=s] = ZET (t[y::=s])"
    1.29 -  "(EQI t1 t2)[y::=s] = EQI (t1[y::=s]) (t2[y::=s])"
    1.30 +| "(APP t\<^isub>1 t\<^isub>2)[y::=s] = APP (t\<^isub>1[y::=s]) (t\<^isub>2[y::=s])"
    1.31 +| "x\<sharp>(y,s) \<Longrightarrow> (LAM [x].t)[y::=s] = LAM [x].(t[y::=s])"
    1.32 +| "(NUM n)[y::=s] = NUM n"
    1.33 +| "(t\<^isub>1 -- t\<^isub>2)[y::=s] = (t\<^isub>1[y::=s]) -- (t\<^isub>2[y::=s])"
    1.34 +| "(t\<^isub>1 ++ t\<^isub>2)[y::=s] = (t\<^isub>1[y::=s]) ++ (t\<^isub>2[y::=s])"
    1.35 +| "x\<sharp>(y,s) \<Longrightarrow> (FIX [x].t)[y::=s] = FIX [x].(t[y::=s])"
    1.36 +| "TRUE[y::=s] = TRUE"
    1.37 +| "FALSE[y::=s] = FALSE"
    1.38 +| "(IF t1 t2 t3)[y::=s] = IF (t1[y::=s]) (t2[y::=s]) (t3[y::=s])"
    1.39 +| "(ZET t)[y::=s] = ZET (t[y::=s])"
    1.40 +| "(EQI t1 t2)[y::=s] = EQI (t1[y::=s]) (t2[y::=s])"
    1.41  apply(finite_guess)+
    1.42  apply(rule TrueI)+
    1.43  apply(simp add: abs_fresh)+
     2.1 --- a/src/HOL/Nominal/Examples/CR_Takahashi.thy	Sat Dec 13 15:35:29 2008 +0100
     2.2 +++ b/src/HOL/Nominal/Examples/CR_Takahashi.thy	Sat Dec 13 17:13:09 2008 +0100
     2.3 @@ -1,5 +1,3 @@
     2.4 -(* $Id$ *)
     2.5 -
     2.6  (* Authors: Christian Urban and Mathilde Arnaud                   *)
     2.7  (*                                                                *)
     2.8  (* A formalisation of the Church-Rosser proof by Masako Takahashi.*)
     2.9 @@ -20,12 +18,12 @@
    2.10    | App "lam" "lam"
    2.11    | Lam "\<guillemotleft>name\<guillemotright>lam" ("Lam [_]._" [100,100] 100)
    2.12  
    2.13 -consts subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam"  ("_[_::=_]" [100,100,100] 100)
    2.14 -
    2.15  nominal_primrec
    2.16 +  subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam"  ("_[_::=_]" [100,100,100] 100)
    2.17 +where
    2.18    "(Var x)[y::=s] = (if x=y then s else (Var x))"
    2.19 -  "(App t\<^isub>1 t\<^isub>2)[y::=s] = App (t\<^isub>1[y::=s]) (t\<^isub>2[y::=s])"
    2.20 -  "x\<sharp>(y,s) \<Longrightarrow> (Lam [x].t)[y::=s] = Lam [x].(t[y::=s])"
    2.21 +| "(App t\<^isub>1 t\<^isub>2)[y::=s] = App (t\<^isub>1[y::=s]) (t\<^isub>2[y::=s])"
    2.22 +| "x\<sharp>(y,s) \<Longrightarrow> (Lam [x].t)[y::=s] = Lam [x].(t[y::=s])"
    2.23  apply(finite_guess)+
    2.24  apply(rule TrueI)+
    2.25  apply(simp add: abs_fresh)
     3.1 --- a/src/HOL/Nominal/Examples/Class.thy	Sat Dec 13 15:35:29 2008 +0100
     3.2 +++ b/src/HOL/Nominal/Examples/Class.thy	Sat Dec 13 17:13:09 2008 +0100
     3.3 @@ -1,5 +1,3 @@
     3.4 -(* $Id$ *)
     3.5 -
     3.6  theory Class
     3.7  imports "../Nominal" 
     3.8  begin
     3.9 @@ -17,16 +15,22 @@
    3.10    | OR   "ty" "ty"   ("_ OR _" [100,100] 100)
    3.11    | IMP  "ty" "ty"   ("_ IMP _" [100,100] 100)
    3.12  
    3.13 -instance ty :: size ..
    3.14 -
    3.15 -nominal_primrec
    3.16 +instantiation ty :: size
    3.17 +begin
    3.18 +
    3.19 +nominal_primrec size_ty
    3.20 +where
    3.21    "size (PR s)     = (1::nat)"
    3.22 -  "size (NOT T)     = 1 + size T"
    3.23 -  "size (T1 AND T2) = 1 + size T1 + size T2"
    3.24 -  "size (T1 OR T2)  = 1 + size T1 + size T2"
    3.25 -  "size (T1 IMP T2) = 1 + size T1 + size T2"
    3.26 +| "size (NOT T)     = 1 + size T"
    3.27 +| "size (T1 AND T2) = 1 + size T1 + size T2"
    3.28 +| "size (T1 OR T2)  = 1 + size T1 + size T2"
    3.29 +| "size (T1 IMP T2) = 1 + size T1 + size T2"
    3.30  by (rule TrueI)+
    3.31  
    3.32 +instance ..
    3.33 +
    3.34 +end
    3.35 +
    3.36  lemma ty_cases:
    3.37    fixes T::ty
    3.38    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)"
    3.39 @@ -66,25 +70,23 @@
    3.40  
    3.41  text {* renaming functions *}
    3.42  
    3.43 -consts
    3.44 -  nrename :: "trm \<Rightarrow> name \<Rightarrow> name \<Rightarrow> trm"      ("_[_\<turnstile>n>_]" [100,100,100] 100) 
    3.45 +nominal_primrec (freshness_context: "(d::coname,e::coname)") 
    3.46    crename :: "trm \<Rightarrow> coname \<Rightarrow> coname \<Rightarrow> trm"  ("_[_\<turnstile>c>_]" [100,100,100] 100) 
    3.47 -
    3.48 -nominal_primrec (freshness_context: "(d::coname,e::coname)") 
    3.49 +where
    3.50    "(Ax x a)[d\<turnstile>c>e] = (if a=d then Ax x e else Ax x a)" 
    3.51 -  "\<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])" 
    3.52 -  "(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)" 
    3.53 -  "a\<sharp>(d,e) \<Longrightarrow> (NotL <a>.M x)[d\<turnstile>c>e] = (NotL <a>.(M[d\<turnstile>c>e]) x)" 
    3.54 -  "\<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] = 
    3.55 +| "\<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])" 
    3.56 +| "(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)" 
    3.57 +| "a\<sharp>(d,e) \<Longrightarrow> (NotL <a>.M x)[d\<turnstile>c>e] = (NotL <a>.(M[d\<turnstile>c>e]) x)" 
    3.58 +| "\<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] = 
    3.59            (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)" 
    3.60 -  "x\<sharp>y \<Longrightarrow> (AndL1 (x).M y)[d\<turnstile>c>e] = AndL1 (x).(M[d\<turnstile>c>e]) y"
    3.61 -  "x\<sharp>y \<Longrightarrow> (AndL2 (x).M y)[d\<turnstile>c>e] = AndL2 (x).(M[d\<turnstile>c>e]) y"
    3.62 -  "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)"
    3.63 -  "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)"
    3.64 -  "\<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"
    3.65 -  "a\<sharp>(d,e,b) \<Longrightarrow> (ImpR (x).<a>.M b)[d\<turnstile>c>e] = 
    3.66 +| "x\<sharp>y \<Longrightarrow> (AndL1 (x).M y)[d\<turnstile>c>e] = AndL1 (x).(M[d\<turnstile>c>e]) y"
    3.67 +| "x\<sharp>y \<Longrightarrow> (AndL2 (x).M y)[d\<turnstile>c>e] = AndL2 (x).(M[d\<turnstile>c>e]) y"
    3.68 +| "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)"
    3.69 +| "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)"
    3.70 +| "\<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"
    3.71 +| "a\<sharp>(d,e,b) \<Longrightarrow> (ImpR (x).<a>.M b)[d\<turnstile>c>e] = 
    3.72         (if b=d then ImpR (x).<a>.(M[d\<turnstile>c>e]) e else ImpR (x).<a>.(M[d\<turnstile>c>e]) b)"
    3.73 -  "\<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"
    3.74 +| "\<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"
    3.75  apply(finite_guess)+
    3.76  apply(rule TrueI)+
    3.77  apply(simp add: abs_fresh abs_supp fin_supp)+
    3.78 @@ -92,19 +94,21 @@
    3.79  done
    3.80  
    3.81  nominal_primrec (freshness_context: "(u::name,v::name)") 
    3.82 +  nrename :: "trm \<Rightarrow> name \<Rightarrow> name \<Rightarrow> trm"      ("_[_\<turnstile>n>_]" [100,100,100] 100) 
    3.83 +where
    3.84    "(Ax x a)[u\<turnstile>n>v] = (if x=u then Ax v a else Ax x a)" 
    3.85 -  "\<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])" 
    3.86 -  "x\<sharp>(u,v) \<Longrightarrow> (NotR (x).M a)[u\<turnstile>n>v] = NotR (x).(M[u\<turnstile>n>v]) a" 
    3.87 -  "(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)" 
    3.88 -  "\<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" 
    3.89 -  "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)"
    3.90 -  "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)"
    3.91 -  "a\<sharp>b \<Longrightarrow> (OrR1 <a>.M b)[u\<turnstile>n>v] = OrR1 <a>.(M[u\<turnstile>n>v]) b"
    3.92 -  "a\<sharp>b \<Longrightarrow> (OrR2 <a>.M b)[u\<turnstile>n>v] = OrR2 <a>.(M[u\<turnstile>n>v]) b"
    3.93 -  "\<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] = 
    3.94 +| "\<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])" 
    3.95 +| "x\<sharp>(u,v) \<Longrightarrow> (NotR (x).M a)[u\<turnstile>n>v] = NotR (x).(M[u\<turnstile>n>v]) a" 
    3.96 +| "(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)" 
    3.97 +| "\<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" 
    3.98 +| "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)"
    3.99 +| "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)"
   3.100 +| "a\<sharp>b \<Longrightarrow> (OrR1 <a>.M b)[u\<turnstile>n>v] = OrR1 <a>.(M[u\<turnstile>n>v]) b"
   3.101 +| "a\<sharp>b \<Longrightarrow> (OrR2 <a>.M b)[u\<turnstile>n>v] = OrR2 <a>.(M[u\<turnstile>n>v]) b"
   3.102 +| "\<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] = 
   3.103          (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)"
   3.104 -  "\<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"
   3.105 -  "\<lbrakk>a\<sharp>N;x\<sharp>(u,v,M,y)\<rbrakk> \<Longrightarrow> (ImpL <a>.M (x).N y)[u\<turnstile>n>v] = 
   3.106 +| "\<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"
   3.107 +| "\<lbrakk>a\<sharp>N;x\<sharp>(u,v,M,y)\<rbrakk> \<Longrightarrow> (ImpL <a>.M (x).N y)[u\<turnstile>n>v] = 
   3.108          (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)"
   3.109  apply(finite_guess)+
   3.110  apply(rule TrueI)+
   3.111 @@ -766,32 +770,30 @@
   3.112  apply(simp add: fin_supp)
   3.113  done
   3.114  
   3.115 -consts
   3.116 +nominal_primrec (freshness_context: "(y::name,c::coname,P::trm)")
   3.117    substn :: "trm \<Rightarrow> name   \<Rightarrow> coname \<Rightarrow> trm \<Rightarrow> trm" ("_{_:=<_>._}" [100,100,100,100] 100) 
   3.118 -  substc :: "trm \<Rightarrow> coname \<Rightarrow> name   \<Rightarrow> trm \<Rightarrow> trm" ("_{_:=(_)._}" [100,100,100,100] 100)
   3.119 -
   3.120 -nominal_primrec (freshness_context: "(y::name,c::coname,P::trm)")
   3.121 +where
   3.122    "(Ax x a){y:=<c>.P} = (if x=y then Cut <c>.P (y).Ax y a else Ax x a)" 
   3.123 -  "\<lbrakk>a\<sharp>(c,P,N);x\<sharp>(y,P,M)\<rbrakk> \<Longrightarrow> (Cut <a>.M (x).N){y:=<c>.P} = 
   3.124 +| "\<lbrakk>a\<sharp>(c,P,N);x\<sharp>(y,P,M)\<rbrakk> \<Longrightarrow> (Cut <a>.M (x).N){y:=<c>.P} = 
   3.125    (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}))" 
   3.126 -  "x\<sharp>(y,P) \<Longrightarrow> (NotR (x).M a){y:=<c>.P} = NotR (x).(M{y:=<c>.P}) a" 
   3.127 -  "a\<sharp>(c,P) \<Longrightarrow> (NotL <a>.M x){y:=<c>.P} = 
   3.128 +| "x\<sharp>(y,P) \<Longrightarrow> (NotR (x).M a){y:=<c>.P} = NotR (x).(M{y:=<c>.P}) a" 
   3.129 +| "a\<sharp>(c,P) \<Longrightarrow> (NotL <a>.M x){y:=<c>.P} = 
   3.130    (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)"
   3.131 -  "\<lbrakk>a\<sharp>(c,P,N,d);b\<sharp>(c,P,M,d);b\<noteq>a\<rbrakk> \<Longrightarrow> 
   3.132 +| "\<lbrakk>a\<sharp>(c,P,N,d);b\<sharp>(c,P,M,d);b\<noteq>a\<rbrakk> \<Longrightarrow> 
   3.133    (AndR <a>.M <b>.N d){y:=<c>.P} = AndR <a>.(M{y:=<c>.P}) <b>.(N{y:=<c>.P}) d" 
   3.134 -  "x\<sharp>(y,P,z) \<Longrightarrow> (AndL1 (x).M z){y:=<c>.P} = 
   3.135 +| "x\<sharp>(y,P,z) \<Longrightarrow> (AndL1 (x).M z){y:=<c>.P} = 
   3.136    (if z=y then fresh_fun (\<lambda>z'. Cut <c>.P (z').AndL1 (x).(M{y:=<c>.P}) z') 
   3.137     else AndL1 (x).(M{y:=<c>.P}) z)"
   3.138 -  "x\<sharp>(y,P,z) \<Longrightarrow> (AndL2 (x).M z){y:=<c>.P} = 
   3.139 +| "x\<sharp>(y,P,z) \<Longrightarrow> (AndL2 (x).M z){y:=<c>.P} = 
   3.140    (if z=y then fresh_fun (\<lambda>z'. Cut <c>.P (z').AndL2 (x).(M{y:=<c>.P}) z') 
   3.141     else AndL2 (x).(M{y:=<c>.P}) z)"
   3.142 -  "a\<sharp>(c,P,b) \<Longrightarrow> (OrR1 <a>.M b){y:=<c>.P} = OrR1 <a>.(M{y:=<c>.P}) b"
   3.143 -  "a\<sharp>(c,P,b) \<Longrightarrow> (OrR2 <a>.M b){y:=<c>.P} = OrR2 <a>.(M{y:=<c>.P}) b"
   3.144 -  "\<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} = 
   3.145 +| "a\<sharp>(c,P,b) \<Longrightarrow> (OrR1 <a>.M b){y:=<c>.P} = OrR1 <a>.(M{y:=<c>.P}) b"
   3.146 +| "a\<sharp>(c,P,b) \<Longrightarrow> (OrR2 <a>.M b){y:=<c>.P} = OrR2 <a>.(M{y:=<c>.P}) b"
   3.147 +| "\<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} = 
   3.148    (if z=y then fresh_fun (\<lambda>z'. Cut <c>.P (z').OrL (x).(M{y:=<c>.P}) (u).(N{y:=<c>.P}) z') 
   3.149     else OrL (x).(M{y:=<c>.P}) (u).(N{y:=<c>.P}) z)"
   3.150 -  "\<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"
   3.151 -  "\<lbrakk>a\<sharp>(N,c,P);x\<sharp>(y,P,M,z)\<rbrakk> \<Longrightarrow> (ImpL <a>.M (x).N z){y:=<c>.P} = 
   3.152 +| "\<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"
   3.153 +| "\<lbrakk>a\<sharp>(N,c,P);x\<sharp>(y,P,M,z)\<rbrakk> \<Longrightarrow> (ImpL <a>.M (x).N z){y:=<c>.P} = 
   3.154    (if y=z then fresh_fun (\<lambda>z'. Cut <c>.P (z').ImpL <a>.(M{y:=<c>.P}) (x).(N{y:=<c>.P}) z') 
   3.155     else ImpL <a>.(M{y:=<c>.P}) (x).(N{y:=<c>.P}) z)"
   3.156  apply(finite_guess)+
   3.157 @@ -842,27 +844,29 @@
   3.158  done
   3.159  
   3.160  nominal_primrec (freshness_context: "(d::name,z::coname,P::trm)")
   3.161 +  substc :: "trm \<Rightarrow> coname \<Rightarrow> name   \<Rightarrow> trm \<Rightarrow> trm" ("_{_:=(_)._}" [100,100,100,100] 100)
   3.162 +where
   3.163    "(Ax x a){d:=(z).P} = (if d=a then Cut <a>.(Ax x a) (z).P else Ax x a)" 
   3.164 -  "\<lbrakk>a\<sharp>(d,P,N);x\<sharp>(z,P,M)\<rbrakk> \<Longrightarrow> (Cut <a>.M (x).N){d:=(z).P} = 
   3.165 +| "\<lbrakk>a\<sharp>(d,P,N);x\<sharp>(z,P,M)\<rbrakk> \<Longrightarrow> (Cut <a>.M (x).N){d:=(z).P} = 
   3.166    (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}))" 
   3.167 -  "x\<sharp>(z,P) \<Longrightarrow> (NotR (x).M a){d:=(z).P} = 
   3.168 +| "x\<sharp>(z,P) \<Longrightarrow> (NotR (x).M a){d:=(z).P} = 
   3.169    (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)" 
   3.170 -  "a\<sharp>(d,P) \<Longrightarrow> (NotL <a>.M x){d:=(z).P} = NotL <a>.(M{d:=(z).P}) x" 
   3.171 -  "\<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} = 
   3.172 +| "a\<sharp>(d,P) \<Longrightarrow> (NotL <a>.M x){d:=(z).P} = NotL <a>.(M{d:=(z).P}) x" 
   3.173 +| "\<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} = 
   3.174    (if d=c then fresh_fun (\<lambda>a'. Cut <a'>.(AndR <a>.(M{d:=(z).P}) <b>.(N{d:=(z).P}) a') (z).P)
   3.175     else AndR <a>.(M{d:=(z).P}) <b>.(N{d:=(z).P}) c)" 
   3.176 -  "x\<sharp>(y,z,P) \<Longrightarrow> (AndL1 (x).M y){d:=(z).P} = AndL1 (x).(M{d:=(z).P}) y"
   3.177 -  "x\<sharp>(y,P,z) \<Longrightarrow> (AndL2 (x).M y){d:=(z).P} = AndL2 (x).(M{d:=(z).P}) y"
   3.178 -  "a\<sharp>(d,P,b) \<Longrightarrow> (OrR1 <a>.M b){d:=(z).P} = 
   3.179 +| "x\<sharp>(y,z,P) \<Longrightarrow> (AndL1 (x).M y){d:=(z).P} = AndL1 (x).(M{d:=(z).P}) y"
   3.180 +| "x\<sharp>(y,P,z) \<Longrightarrow> (AndL2 (x).M y){d:=(z).P} = AndL2 (x).(M{d:=(z).P}) y"
   3.181 +| "a\<sharp>(d,P,b) \<Longrightarrow> (OrR1 <a>.M b){d:=(z).P} = 
   3.182    (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)"
   3.183 -  "a\<sharp>(d,P,b) \<Longrightarrow> (OrR2 <a>.M b){d:=(z).P} = 
   3.184 +| "a\<sharp>(d,P,b) \<Longrightarrow> (OrR2 <a>.M b){d:=(z).P} = 
   3.185    (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)"
   3.186 -  "\<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} = 
   3.187 +| "\<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} = 
   3.188    OrL (x).(M{d:=(z).P}) (y).(N{d:=(z).P}) u" 
   3.189 -  "\<lbrakk>a\<sharp>(b,d,P); x\<sharp>(z,P)\<rbrakk> \<Longrightarrow> (ImpR (x).<a>.M b){d:=(z).P} = 
   3.190 +| "\<lbrakk>a\<sharp>(b,d,P); x\<sharp>(z,P)\<rbrakk> \<Longrightarrow> (ImpR (x).<a>.M b){d:=(z).P} = 
   3.191    (if d=b then fresh_fun (\<lambda>a'. Cut <a'>.ImpR (x).<a>.(M{d:=(z).P}) a' (z).P) 
   3.192     else ImpR (x).<a>.(M{d:=(z).P}) b)"
   3.193 -  "\<lbrakk>a\<sharp>(N,d,P);x\<sharp>(y,z,P,M)\<rbrakk> \<Longrightarrow> (ImpL <a>.M (x).N y){d:=(z).P} = 
   3.194 +| "\<lbrakk>a\<sharp>(N,d,P);x\<sharp>(y,z,P,M)\<rbrakk> \<Longrightarrow> (ImpL <a>.M (x).N y){d:=(z).P} = 
   3.195    ImpL <a>.(M{d:=(z).P}) (x).(N{d:=(z).P}) y"
   3.196  apply(finite_guess)+
   3.197  apply(rule TrueI)+
   3.198 @@ -10305,11 +10309,10 @@
   3.199  lemma BINDINGc_decreasing:
   3.200    shows "X\<subseteq>Y \<Longrightarrow> BINDINGc B Y \<subseteq> BINDINGc B X"
   3.201  by (simp add: BINDINGc_def) (blast) 
   3.202 -
   3.203 -consts
   3.204 -  NOTRIGHT::"ty \<Rightarrow> ntrm set \<Rightarrow> ctrm set"
   3.205    
   3.206  nominal_primrec
   3.207 +  NOTRIGHT :: "ty \<Rightarrow> ntrm set \<Rightarrow> ctrm set"
   3.208 +where
   3.209   "NOTRIGHT (NOT B) X = { <a>:NotR (x).M a | a x M. fic (NotR (x).M a) a \<and> (x):M \<in> X }"
   3.210  apply(rule TrueI)+
   3.211  done
   3.212 @@ -10365,11 +10368,10 @@
   3.213  apply(drule pt_bij1[OF pt_coname_inst, OF at_coname_inst])
   3.214  apply(simp add: swap_simps)
   3.215  done
   3.216 -
   3.217 -consts
   3.218 -  NOTLEFT::"ty \<Rightarrow> ctrm set \<Rightarrow> ntrm set"
   3.219    
   3.220  nominal_primrec
   3.221 +  NOTLEFT :: "ty \<Rightarrow> ctrm set \<Rightarrow> ntrm set"
   3.222 +where
   3.223   "NOTLEFT (NOT B) X = { (x):NotL <a>.M x | a x M. fin (NotL <a>.M x) x \<and> <a>:M \<in> X }"
   3.224  apply(rule TrueI)+
   3.225  done
   3.226 @@ -10425,11 +10427,10 @@
   3.227  apply(drule pt_bij1[OF pt_coname_inst, OF at_coname_inst])
   3.228  apply(simp add: swap_simps)
   3.229  done
   3.230 -
   3.231 -consts
   3.232 -  ANDRIGHT::"ty \<Rightarrow> ctrm set \<Rightarrow> ctrm set \<Rightarrow> ctrm set"
   3.233    
   3.234  nominal_primrec
   3.235 +  ANDRIGHT :: "ty \<Rightarrow> ctrm set \<Rightarrow> ctrm set \<Rightarrow> ctrm set"
   3.236 +where
   3.237   "ANDRIGHT (B AND C) X Y = 
   3.238              { <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 }"
   3.239  apply(rule TrueI)+
   3.240 @@ -10505,10 +10506,9 @@
   3.241  apply(simp)
   3.242  done
   3.243  
   3.244 -consts
   3.245 -  ANDLEFT1::"ty \<Rightarrow> ntrm set \<Rightarrow> ntrm set"
   3.246 -
   3.247  nominal_primrec
   3.248 +  ANDLEFT1 :: "ty \<Rightarrow> ntrm set \<Rightarrow> ntrm set"
   3.249 +where
   3.250   "ANDLEFT1 (B AND C) X = { (y):AndL1 (x).M y | x y M. fin (AndL1 (x).M y) y \<and> (x):M \<in> X }"
   3.251  apply(rule TrueI)+
   3.252  done
   3.253 @@ -10565,10 +10565,9 @@
   3.254  apply(simp add: swap_simps)
   3.255  done
   3.256  
   3.257 -consts
   3.258 -  ANDLEFT2::"ty \<Rightarrow> ntrm set \<Rightarrow> ntrm set"
   3.259 -
   3.260  nominal_primrec
   3.261 +  ANDLEFT2 :: "ty \<Rightarrow> ntrm set \<Rightarrow> ntrm set"
   3.262 +where
   3.263   "ANDLEFT2 (B AND C) X = { (y):AndL2 (x).M y | x y M. fin (AndL2 (x).M y) y \<and> (x):M \<in> X }"
   3.264  apply(rule TrueI)+
   3.265  done
   3.266 @@ -10625,10 +10624,9 @@
   3.267  apply(simp add: swap_simps)
   3.268  done
   3.269  
   3.270 -consts
   3.271 -  ORLEFT::"ty \<Rightarrow> ntrm set \<Rightarrow> ntrm set \<Rightarrow> ntrm set"
   3.272 -  
   3.273  nominal_primrec
   3.274 +  ORLEFT :: "ty \<Rightarrow> ntrm set \<Rightarrow> ntrm set \<Rightarrow> ntrm set"
   3.275 +where
   3.276   "ORLEFT (B OR C) X Y = 
   3.277              { (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 }"
   3.278  apply(rule TrueI)+
   3.279 @@ -10704,10 +10702,9 @@
   3.280  apply(simp add: swap_simps)
   3.281  done
   3.282  
   3.283 -consts
   3.284 -  ORRIGHT1::"ty \<Rightarrow> ctrm set \<Rightarrow> ctrm set"
   3.285 -
   3.286  nominal_primrec
   3.287 +  ORRIGHT1 :: "ty \<Rightarrow> ctrm set \<Rightarrow> ctrm set"
   3.288 +where
   3.289   "ORRIGHT1 (B OR C) X = { <b>:OrR1 <a>.M b | a b M. fic (OrR1 <a>.M b) b \<and> <a>:M \<in> X }"
   3.290  apply(rule TrueI)+
   3.291  done
   3.292 @@ -10764,10 +10761,9 @@
   3.293  apply(simp)
   3.294  done
   3.295  
   3.296 -consts
   3.297 -  ORRIGHT2::"ty \<Rightarrow> ctrm set \<Rightarrow> ctrm set"
   3.298 -
   3.299  nominal_primrec
   3.300 +  ORRIGHT2 :: "ty \<Rightarrow> ctrm set \<Rightarrow> ctrm set"
   3.301 +where
   3.302   "ORRIGHT2 (B OR C) X = { <b>:OrR2 <a>.M b | a b M. fic (OrR2 <a>.M b) b \<and> <a>:M \<in> X }"
   3.303  apply(rule TrueI)+
   3.304  done
   3.305 @@ -10824,10 +10820,9 @@
   3.306  apply(simp)
   3.307  done
   3.308  
   3.309 -consts
   3.310 -  IMPRIGHT::"ty \<Rightarrow> ntrm set \<Rightarrow> ctrm set \<Rightarrow> ntrm set \<Rightarrow> ctrm set \<Rightarrow> ctrm set"
   3.311 -
   3.312  nominal_primrec
   3.313 +  IMPRIGHT :: "ty \<Rightarrow> ntrm set \<Rightarrow> ctrm set \<Rightarrow> ntrm set \<Rightarrow> ctrm set \<Rightarrow> ctrm set"
   3.314 +where
   3.315   "IMPRIGHT (B IMP C) X Y Z U= 
   3.316          { <b>:ImpR (x).<a>.M b | x a b M. fic (ImpR (x).<a>.M b) b 
   3.317                                          \<and> (\<forall>z P. x\<sharp>(z,P) \<and> (z):P \<in> Z \<longrightarrow> (x):(M{a:=(z).P}) \<in> X)
   3.318 @@ -10954,10 +10949,9 @@
   3.319  apply(perm_simp add: nsubst_eqvt fresh_right)
   3.320  done
   3.321  
   3.322 -consts
   3.323 -  IMPLEFT::"ty \<Rightarrow> ctrm set \<Rightarrow> ntrm set \<Rightarrow> ntrm set"
   3.324 -
   3.325  nominal_primrec
   3.326 +  IMPLEFT :: "ty \<Rightarrow> ctrm set \<Rightarrow> ntrm set \<Rightarrow> ntrm set"
   3.327 +where
   3.328   "IMPLEFT (B IMP C) X Y = 
   3.329          { (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 }"
   3.330  apply(rule TrueI)+
   3.331 @@ -17800,23 +17794,21 @@
   3.332  apply(auto)
   3.333  done 
   3.334  
   3.335 -consts
   3.336 +nominal_primrec (freshness_context: "\<theta>n::(name\<times>coname\<times>trm)")
   3.337    stn :: "trm\<Rightarrow>(name\<times>coname\<times>trm) list\<Rightarrow>trm" 
   3.338 -  stc :: "trm\<Rightarrow>(coname\<times>name\<times>trm) list\<Rightarrow>trm" 
   3.339 -
   3.340 -nominal_primrec (freshness_context: "\<theta>n::(name\<times>coname\<times>trm)")
   3.341 +where
   3.342    "stn (Ax x a) \<theta>n = lookupc x a \<theta>n"
   3.343 -  "\<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)" 
   3.344 -  "x\<sharp>\<theta>n \<Longrightarrow> stn (NotR (x).M a) \<theta>n = (NotR (x).M a)"
   3.345 -  "a\<sharp>\<theta>n \<Longrightarrow>stn (NotL <a>.M x) \<theta>n = (NotL <a>.M x)"
   3.346 -  "\<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)"
   3.347 -  "x\<sharp>(z,\<theta>n) \<Longrightarrow> stn (AndL1 (x).M z) \<theta>n = (AndL1 (x).M z)"
   3.348 -  "x\<sharp>(z,\<theta>n) \<Longrightarrow> stn (AndL2 (x).M z) \<theta>n = (AndL2 (x).M z)"
   3.349 -  "a\<sharp>(b,\<theta>n) \<Longrightarrow> stn (OrR1 <a>.M b) \<theta>n = (OrR1 <a>.M b)"
   3.350 -  "a\<sharp>(b,\<theta>n) \<Longrightarrow> stn (OrR2 <a>.M b) \<theta>n = (OrR2 <a>.M b)"
   3.351 -  "\<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)"
   3.352 -  "\<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)"
   3.353 -  "\<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)"
   3.354 +| "\<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)" 
   3.355 +| "x\<sharp>\<theta>n \<Longrightarrow> stn (NotR (x).M a) \<theta>n = (NotR (x).M a)"
   3.356 +| "a\<sharp>\<theta>n \<Longrightarrow>stn (NotL <a>.M x) \<theta>n = (NotL <a>.M x)"
   3.357 +| "\<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)"
   3.358 +| "x\<sharp>(z,\<theta>n) \<Longrightarrow> stn (AndL1 (x).M z) \<theta>n = (AndL1 (x).M z)"
   3.359 +| "x\<sharp>(z,\<theta>n) \<Longrightarrow> stn (AndL2 (x).M z) \<theta>n = (AndL2 (x).M z)"
   3.360 +| "a\<sharp>(b,\<theta>n) \<Longrightarrow> stn (OrR1 <a>.M b) \<theta>n = (OrR1 <a>.M b)"
   3.361 +| "a\<sharp>(b,\<theta>n) \<Longrightarrow> stn (OrR2 <a>.M b) \<theta>n = (OrR2 <a>.M b)"
   3.362 +| "\<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)"
   3.363 +| "\<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)"
   3.364 +| "\<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)"
   3.365  apply(finite_guess)+
   3.366  apply(rule TrueI)+
   3.367  apply(simp add: abs_fresh abs_supp fin_supp)+
   3.368 @@ -17824,18 +17816,20 @@
   3.369  done
   3.370  
   3.371  nominal_primrec (freshness_context: "\<theta>c::(coname\<times>name\<times>trm)")
   3.372 +  stc :: "trm\<Rightarrow>(coname\<times>name\<times>trm) list\<Rightarrow>trm" 
   3.373 +where
   3.374    "stc (Ax x a) \<theta>c = lookupd x a \<theta>c"
   3.375 -  "\<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)" 
   3.376 -  "x\<sharp>\<theta>c \<Longrightarrow> stc (NotR (x).M a) \<theta>c = (NotR (x).M a)"
   3.377 -  "a\<sharp>\<theta>c \<Longrightarrow> stc (NotL <a>.M x) \<theta>c = (NotL <a>.M x)"
   3.378 -  "\<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)"
   3.379 -  "x\<sharp>(z,\<theta>c) \<Longrightarrow> stc (AndL1 (x).M z) \<theta>c = (AndL1 (x).M z)"
   3.380 -  "x\<sharp>(z,\<theta>c) \<Longrightarrow> stc (AndL2 (x).M z) \<theta>c = (AndL2 (x).M z)"
   3.381 -  "a\<sharp>(b,\<theta>c) \<Longrightarrow> stc (OrR1 <a>.M b) \<theta>c = (OrR1 <a>.M b)"
   3.382 -  "a\<sharp>(b,\<theta>c) \<Longrightarrow> stc (OrR2 <a>.M b) \<theta>c = (OrR2 <a>.M b)"
   3.383 -  "\<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)"
   3.384 -  "\<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)"
   3.385 -  "\<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)"
   3.386 +| "\<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)" 
   3.387 +| "x\<sharp>\<theta>c \<Longrightarrow> stc (NotR (x).M a) \<theta>c = (NotR (x).M a)"
   3.388 +| "a\<sharp>\<theta>c \<Longrightarrow> stc (NotL <a>.M x) \<theta>c = (NotL <a>.M x)"
   3.389 +| "\<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)"
   3.390 +| "x\<sharp>(z,\<theta>c) \<Longrightarrow> stc (AndL1 (x).M z) \<theta>c = (AndL1 (x).M z)"
   3.391 +| "x\<sharp>(z,\<theta>c) \<Longrightarrow> stc (AndL2 (x).M z) \<theta>c = (AndL2 (x).M z)"
   3.392 +| "a\<sharp>(b,\<theta>c) \<Longrightarrow> stc (OrR1 <a>.M b) \<theta>c = (OrR1 <a>.M b)"
   3.393 +| "a\<sharp>(b,\<theta>c) \<Longrightarrow> stc (OrR2 <a>.M b) \<theta>c = (OrR2 <a>.M b)"
   3.394 +| "\<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)"
   3.395 +| "\<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)"
   3.396 +| "\<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)"
   3.397  apply(finite_guess)+
   3.398  apply(rule TrueI)+
   3.399  apply(simp add: abs_fresh abs_supp fin_supp)+
   3.400 @@ -17926,51 +17920,50 @@
   3.401  apply(perm_simp)
   3.402  done
   3.403  
   3.404 -consts
   3.405 +nominal_primrec (freshness_context: "(\<theta>n::(name\<times>coname\<times>trm) list,\<theta>c::(coname\<times>name\<times>trm) list)")
   3.406    psubst :: "(name\<times>coname\<times>trm) list\<Rightarrow>(coname\<times>name\<times>trm) list\<Rightarrow>trm\<Rightarrow>trm" ("_,_<_>" [100,100,100] 100) 
   3.407 -
   3.408 -nominal_primrec (freshness_context: "(\<theta>n::(name\<times>coname\<times>trm) list,\<theta>c::(coname\<times>name\<times>trm) list)")
   3.409 +where
   3.410    "\<theta>n,\<theta>c<Ax x a> = lookup x a \<theta>n \<theta>c" 
   3.411 -  "\<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> = 
   3.412 +| "\<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> = 
   3.413     Cut <a>.(if \<exists>x. M=Ax x a then stn M \<theta>n else \<theta>n,\<theta>c<M>) 
   3.414         (x).(if \<exists>a. N=Ax x a then stc N \<theta>c else \<theta>n,\<theta>c<N>)" 
   3.415 -  "x\<sharp>(\<theta>n,\<theta>c) \<Longrightarrow> \<theta>n,\<theta>c<NotR (x).M a> = 
   3.416 +| "x\<sharp>(\<theta>n,\<theta>c) \<Longrightarrow> \<theta>n,\<theta>c<NotR (x).M a> = 
   3.417    (case (findc \<theta>c a) of 
   3.418         Some (u,P) \<Rightarrow> fresh_fun (\<lambda>a'. Cut <a'>.NotR (x).(\<theta>n,\<theta>c<M>) a' (u).P) 
   3.419       | None \<Rightarrow> NotR (x).(\<theta>n,\<theta>c<M>) a)"
   3.420 -  "a\<sharp>(\<theta>n,\<theta>c) \<Longrightarrow> \<theta>n,\<theta>c<NotL <a>.M x> = 
   3.421 +| "a\<sharp>(\<theta>n,\<theta>c) \<Longrightarrow> \<theta>n,\<theta>c<NotL <a>.M x> = 
   3.422    (case (findn \<theta>n x) of 
   3.423         Some (c,P) \<Rightarrow> fresh_fun (\<lambda>x'. Cut <c>.P (x').(NotL <a>.(\<theta>n,\<theta>c<M>) x')) 
   3.424       | None \<Rightarrow> NotL <a>.(\<theta>n,\<theta>c<M>) x)"
   3.425 -  "\<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>) = 
   3.426 +| "\<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>) = 
   3.427    (case (findc \<theta>c c) of 
   3.428         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)
   3.429       | None \<Rightarrow> AndR <a>.(\<theta>n,\<theta>c<M>) <b>.(\<theta>n,\<theta>c<N>) c)"
   3.430 -  "x\<sharp>(z,\<theta>n,\<theta>c) \<Longrightarrow> (\<theta>n,\<theta>c<AndL1 (x).M z>) = 
   3.431 +| "x\<sharp>(z,\<theta>n,\<theta>c) \<Longrightarrow> (\<theta>n,\<theta>c<AndL1 (x).M z>) = 
   3.432    (case (findn \<theta>n z) of 
   3.433         Some (c,P) \<Rightarrow> fresh_fun (\<lambda>z'. Cut <c>.P (z').AndL1 (x).(\<theta>n,\<theta>c<M>) z') 
   3.434       | None \<Rightarrow> AndL1 (x).(\<theta>n,\<theta>c<M>) z)"
   3.435 -  "x\<sharp>(z,\<theta>n,\<theta>c) \<Longrightarrow> (\<theta>n,\<theta>c<AndL2 (x).M z>) = 
   3.436 +| "x\<sharp>(z,\<theta>n,\<theta>c) \<Longrightarrow> (\<theta>n,\<theta>c<AndL2 (x).M z>) = 
   3.437    (case (findn \<theta>n z) of 
   3.438         Some (c,P) \<Rightarrow> fresh_fun (\<lambda>z'. Cut <c>.P (z').AndL2 (x).(\<theta>n,\<theta>c<M>) z') 
   3.439       | None \<Rightarrow> AndL2 (x).(\<theta>n,\<theta>c<M>) z)"
   3.440 -  "\<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>) =
   3.441 +| "\<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>) =
   3.442    (case (findn \<theta>n z) of  
   3.443         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') 
   3.444       | None \<Rightarrow> OrL (x).(\<theta>n,\<theta>c<M>) (u).(\<theta>n,\<theta>c<N>) z)"
   3.445 -  "a\<sharp>(b,\<theta>n,\<theta>c) \<Longrightarrow> (\<theta>n,\<theta>c<OrR1 <a>.M b>) = 
   3.446 +| "a\<sharp>(b,\<theta>n,\<theta>c) \<Longrightarrow> (\<theta>n,\<theta>c<OrR1 <a>.M b>) = 
   3.447    (case (findc \<theta>c b) of
   3.448         Some (x,P) \<Rightarrow> fresh_fun (\<lambda>a'. Cut <a'>.OrR1 <a>.(\<theta>n,\<theta>c<M>) a' (x).P) 
   3.449       | None \<Rightarrow> OrR1 <a>.(\<theta>n,\<theta>c<M>) b)"
   3.450 -  "a\<sharp>(b,\<theta>n,\<theta>c) \<Longrightarrow> (\<theta>n,\<theta>c<OrR2 <a>.M b>) = 
   3.451 +| "a\<sharp>(b,\<theta>n,\<theta>c) \<Longrightarrow> (\<theta>n,\<theta>c<OrR2 <a>.M b>) = 
   3.452    (case (findc \<theta>c b) of
   3.453         Some (x,P) \<Rightarrow> fresh_fun (\<lambda>a'. Cut <a'>.OrR2 <a>.(\<theta>n,\<theta>c<M>) a' (x).P) 
   3.454       | None \<Rightarrow> OrR2 <a>.(\<theta>n,\<theta>c<M>) b)"
   3.455 -  "\<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>) = 
   3.456 +| "\<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>) = 
   3.457    (case (findc \<theta>c b) of
   3.458         Some (z,P) \<Rightarrow> fresh_fun (\<lambda>a'. Cut <a'>.ImpR (x).<a>.(\<theta>n,\<theta>c<M>) a' (z).P)
   3.459       | None \<Rightarrow> ImpR (x).<a>.(\<theta>n,\<theta>c<M>) b)"
   3.460 -  "\<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>) = 
   3.461 +| "\<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>) = 
   3.462    (case (findn \<theta>n z) of
   3.463         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') 
   3.464       | None \<Rightarrow> ImpL <a>.(\<theta>n,\<theta>c<M>) (x).(\<theta>n,\<theta>c<N>) z)"
     4.1 --- a/src/HOL/Nominal/Examples/Compile.thy	Sat Dec 13 15:35:29 2008 +0100
     4.2 +++ b/src/HOL/Nominal/Examples/Compile.thy	Sat Dec 13 17:13:09 2008 +0100
     4.3 @@ -1,5 +1,3 @@
     4.4 -(* $Id$ *)
     4.5 -
     4.6  (* The definitions for a challenge suggested by Adam Chlipala *)
     4.7  
     4.8  theory Compile
     4.9 @@ -92,20 +90,24 @@
    4.10  
    4.11  text {* capture-avoiding substitution *}
    4.12  
    4.13 -consts
    4.14 -  subst :: "'a \<Rightarrow> name \<Rightarrow> 'a \<Rightarrow> 'a"  ("_[_::=_]" [100,100,100] 100)
    4.15 +class subst =
    4.16 +  fixes subst :: "'a \<Rightarrow> name \<Rightarrow> 'a \<Rightarrow> 'a"  ("_[_::=_]" [100,100,100] 100)
    4.17  
    4.18 -nominal_primrec
    4.19 +instantiation trm :: subst
    4.20 +begin
    4.21 +
    4.22 +nominal_primrec subst_trm
    4.23 +where
    4.24    "(Var x)[y::=t'] = (if x=y then t' else (Var x))"
    4.25 -  "(App t1 t2)[y::=t'] = App (t1[y::=t']) (t2[y::=t'])"
    4.26 -  "\<lbrakk>x\<sharp>y; x\<sharp>t'\<rbrakk> \<Longrightarrow> (Lam [x].t)[y::=t'] = Lam [x].(t[y::=t'])"
    4.27 -  "(Const n)[y::=t'] = Const n"
    4.28 -  "(Pr e1 e2)[y::=t'] = Pr (e1[y::=t']) (e2[y::=t'])"
    4.29 -  "(Fst e)[y::=t'] = Fst (e[y::=t'])"
    4.30 -  "(Snd e)[y::=t'] = Snd (e[y::=t'])"
    4.31 -  "(InL e)[y::=t'] = InL (e[y::=t'])"
    4.32 -  "(InR e)[y::=t'] = InR (e[y::=t'])"
    4.33 -  "\<lbrakk>z\<noteq>x; x\<sharp>y; x\<sharp>e; x\<sharp>e2; z\<sharp>y; z\<sharp>e; z\<sharp>e1; x\<sharp>t'; z\<sharp>t'\<rbrakk> \<Longrightarrow>
    4.34 +| "(App t1 t2)[y::=t'] = App (t1[y::=t']) (t2[y::=t'])"
    4.35 +| "\<lbrakk>x\<sharp>y; x\<sharp>t'\<rbrakk> \<Longrightarrow> (Lam [x].t)[y::=t'] = Lam [x].(t[y::=t'])"
    4.36 +| "(Const n)[y::=t'] = Const n"
    4.37 +| "(Pr e1 e2)[y::=t'] = Pr (e1[y::=t']) (e2[y::=t'])"
    4.38 +| "(Fst e)[y::=t'] = Fst (e[y::=t'])"
    4.39 +| "(Snd e)[y::=t'] = Snd (e[y::=t'])"
    4.40 +| "(InL e)[y::=t'] = InL (e[y::=t'])"
    4.41 +| "(InR e)[y::=t'] = InR (e[y::=t'])"
    4.42 +| "\<lbrakk>z\<noteq>x; x\<sharp>y; x\<sharp>e; x\<sharp>e2; z\<sharp>y; z\<sharp>e; z\<sharp>e1; x\<sharp>t'; z\<sharp>t'\<rbrakk> \<Longrightarrow>
    4.43       (Case e of inl x \<rightarrow> e1 | inr z \<rightarrow> e2)[y::=t'] =
    4.44         (Case (e[y::=t']) of inl x \<rightarrow> (e1[y::=t']) | inr z \<rightarrow> (e2[y::=t']))"
    4.45    apply(finite_guess)+
    4.46 @@ -114,23 +116,35 @@
    4.47    apply(fresh_guess)+
    4.48    done
    4.49  
    4.50 -nominal_primrec (Isubst)
    4.51 +instance ..
    4.52 +
    4.53 +end
    4.54 +
    4.55 +instantiation trmI :: subst
    4.56 +begin
    4.57 +
    4.58 +nominal_primrec subst_trmI
    4.59 +where
    4.60    "(IVar x)[y::=t'] = (if x=y then t' else (IVar x))"
    4.61 -  "(IApp t1 t2)[y::=t'] = IApp (t1[y::=t']) (t2[y::=t'])"
    4.62 -  "\<lbrakk>x\<sharp>y; x\<sharp>t'\<rbrakk> \<Longrightarrow> (ILam [x].t)[y::=t'] = ILam [x].(t[y::=t'])"
    4.63 -  "(INat n)[y::=t'] = INat n"
    4.64 -  "(IUnit)[y::=t'] = IUnit"
    4.65 -  "(ISucc e)[y::=t'] = ISucc (e[y::=t'])"
    4.66 -  "(IAss e1 e2)[y::=t'] = IAss (e1[y::=t']) (e2[y::=t'])"
    4.67 -  "(IRef e)[y::=t'] = IRef (e[y::=t'])"
    4.68 -  "(ISeq e1 e2)[y::=t'] = ISeq (e1[y::=t']) (e2[y::=t'])"
    4.69 -  "(Iif e e1 e2)[y::=t'] = Iif (e[y::=t']) (e1[y::=t']) (e2[y::=t'])"
    4.70 +| "(IApp t1 t2)[y::=t'] = IApp (t1[y::=t']) (t2[y::=t'])"
    4.71 +| "\<lbrakk>x\<sharp>y; x\<sharp>t'\<rbrakk> \<Longrightarrow> (ILam [x].t)[y::=t'] = ILam [x].(t[y::=t'])"
    4.72 +| "(INat n)[y::=t'] = INat n"
    4.73 +| "(IUnit)[y::=t'] = IUnit"
    4.74 +| "(ISucc e)[y::=t'] = ISucc (e[y::=t'])"
    4.75 +| "(IAss e1 e2)[y::=t'] = IAss (e1[y::=t']) (e2[y::=t'])"
    4.76 +| "(IRef e)[y::=t'] = IRef (e[y::=t'])"
    4.77 +| "(ISeq e1 e2)[y::=t'] = ISeq (e1[y::=t']) (e2[y::=t'])"
    4.78 +| "(Iif e e1 e2)[y::=t'] = Iif (e[y::=t']) (e1[y::=t']) (e2[y::=t'])"
    4.79    apply(finite_guess)+
    4.80    apply(rule TrueI)+
    4.81    apply(simp add: abs_fresh)+
    4.82    apply(fresh_guess)+
    4.83    done
    4.84  
    4.85 +instance ..
    4.86 +
    4.87 +end
    4.88 +
    4.89  lemma Isubst_eqvt[eqvt]:
    4.90    fixes pi::"name prm"
    4.91    and   t1::"trmI"
    4.92 @@ -138,7 +152,7 @@
    4.93    and   x::"name"
    4.94    shows "pi\<bullet>(t1[x::=t2]) = ((pi\<bullet>t1)[(pi\<bullet>x)::=(pi\<bullet>t2)])"
    4.95    apply (nominal_induct t1 avoiding: x t2 rule: trmI.strong_induct)
    4.96 -  apply (simp_all add: Isubst.simps eqvts fresh_bij)
    4.97 +  apply (simp_all add: subst_trmI.simps eqvts fresh_bij)
    4.98    done
    4.99  
   4.100  lemma Isubst_supp:
   4.101 @@ -147,7 +161,7 @@
   4.102    and   x::"name"
   4.103    shows "((supp (t1[x::=t2]))::name set) \<subseteq> (supp t2)\<union>((supp t1)-{x})"
   4.104    apply (nominal_induct t1 avoiding: x t2 rule: trmI.strong_induct)
   4.105 -  apply (auto simp add: Isubst.simps trmI.supp supp_atm abs_supp supp_nat)
   4.106 +  apply (auto simp add: subst_trmI.simps trmI.supp supp_atm abs_supp supp_nat)
   4.107    apply blast+
   4.108    done
   4.109  
   4.110 @@ -198,29 +212,29 @@
   4.111  
   4.112  text {* Translation functions *}
   4.113  
   4.114 -consts trans :: "trm \<Rightarrow> trmI" 
   4.115 -
   4.116  nominal_primrec
   4.117 +  trans :: "trm \<Rightarrow> trmI"
   4.118 +where
   4.119    "trans (Var x) = (IVar x)"
   4.120 -  "trans (App e1 e2) = IApp (trans e1) (trans e2)"
   4.121 -  "trans (Lam [x].e) = ILam [x].(trans e)"
   4.122 -  "trans (Const n) = INat n"
   4.123 -  "trans (Pr e1 e2) = 
   4.124 +| "trans (App e1 e2) = IApp (trans e1) (trans e2)"
   4.125 +| "trans (Lam [x].e) = ILam [x].(trans e)"
   4.126 +| "trans (Const n) = INat n"
   4.127 +| "trans (Pr e1 e2) = 
   4.128         (let limit = IRef(INat 0) in 
   4.129          let v1 = (trans e1) in 
   4.130          let v2 = (trans e2) in 
   4.131          (((ISucc limit)\<mapsto>v1);;(ISucc(ISucc limit)\<mapsto>v2));;(INat 0 \<mapsto> ISucc(ISucc(limit))))"
   4.132 -  "trans (Fst e) = IRef (ISucc (trans e))"
   4.133 -  "trans (Snd e) = IRef (ISucc (ISucc (trans e)))"
   4.134 -  "trans (InL e) = 
   4.135 +| "trans (Fst e) = IRef (ISucc (trans e))"
   4.136 +| "trans (Snd e) = IRef (ISucc (ISucc (trans e)))"
   4.137 +| "trans (InL e) = 
   4.138          (let limit = IRef(INat 0) in 
   4.139           let v = (trans e) in 
   4.140           (((ISucc limit)\<mapsto>INat(0));;(ISucc(ISucc limit)\<mapsto>v));;(INat 0 \<mapsto> ISucc(ISucc(limit))))"
   4.141 -  "trans (InR e) = 
   4.142 +| "trans (InR e) = 
   4.143          (let limit = IRef(INat 0) in 
   4.144           let v = (trans e) in 
   4.145           (((ISucc limit)\<mapsto>INat(1));;(ISucc(ISucc limit)\<mapsto>v));;(INat 0 \<mapsto> ISucc(ISucc(limit))))"
   4.146 -  "\<lbrakk>x2\<noteq>x1; x1\<sharp>e; x1\<sharp>e2; x2\<sharp>e; x2\<sharp>e1\<rbrakk> \<Longrightarrow> 
   4.147 +| "\<lbrakk>x2\<noteq>x1; x1\<sharp>e; x1\<sharp>e2; x2\<sharp>e; x2\<sharp>e1\<rbrakk> \<Longrightarrow> 
   4.148     trans (Case e of inl x1 \<rightarrow> e1 | inr x2 \<rightarrow> e2) =
   4.149         (let v = (trans e) in
   4.150          let v1 = (trans e1) in
   4.151 @@ -232,11 +246,11 @@
   4.152    apply(fresh_guess add: Let_def)+
   4.153    done
   4.154  
   4.155 -consts trans_type :: "ty \<Rightarrow> tyI"
   4.156 -
   4.157  nominal_primrec
   4.158 +  trans_type :: "ty \<Rightarrow> tyI"
   4.159 +where
   4.160    "trans_type (Data \<sigma>) = DataI(NatI)"
   4.161 -  "trans_type (\<tau>1\<rightarrow>\<tau>2) = (trans_type \<tau>1)\<rightarrow>(trans_type \<tau>2)"
   4.162 +| "trans_type (\<tau>1\<rightarrow>\<tau>2) = (trans_type \<tau>1)\<rightarrow>(trans_type \<tau>2)"
   4.163    by (rule TrueI)+
   4.164  
   4.165  end
   4.166 \ No newline at end of file
     5.1 --- a/src/HOL/Nominal/Examples/Contexts.thy	Sat Dec 13 15:35:29 2008 +0100
     5.2 +++ b/src/HOL/Nominal/Examples/Contexts.thy	Sat Dec 13 17:13:09 2008 +0100
     5.3 @@ -1,5 +1,3 @@
     5.4 -(* $Id$ *)
     5.5 -
     5.6  theory Contexts
     5.7  imports "../Nominal"
     5.8  begin
     5.9 @@ -42,12 +40,12 @@
    5.10  
    5.11  text {* Capture-Avoiding Substitution *}
    5.12  
    5.13 -consts subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam"  ("_[_::=_]" [100,100,100] 100)
    5.14 -
    5.15  nominal_primrec
    5.16 +  subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam"  ("_[_::=_]" [100,100,100] 100)
    5.17 +where
    5.18    "(Var x)[y::=s] = (if x=y then s else (Var x))"
    5.19 -  "(App t\<^isub>1 t\<^isub>2)[y::=s] = App (t\<^isub>1[y::=s]) (t\<^isub>2[y::=s])"
    5.20 -  "x\<sharp>(y,s) \<Longrightarrow> (Lam [x].t)[y::=s] = Lam [x].(t[y::=s])"
    5.21 +| "(App t\<^isub>1 t\<^isub>2)[y::=s] = App (t\<^isub>1[y::=s]) (t\<^isub>2[y::=s])"
    5.22 +| "x\<sharp>(y,s) \<Longrightarrow> (Lam [x].t)[y::=s] = Lam [x].(t[y::=s])"
    5.23  apply(finite_guess)+
    5.24  apply(rule TrueI)+
    5.25  apply(simp add: abs_fresh)
    5.26 @@ -59,14 +57,13 @@
    5.27    This operation is possibly capturing.
    5.28  *}
    5.29  
    5.30 -consts 
    5.31 +nominal_primrec
    5.32    filling :: "ctx \<Rightarrow> lam \<Rightarrow> lam" ("_\<lbrakk>_\<rbrakk>" [100,100] 100)
    5.33 -
    5.34 -nominal_primrec
    5.35 +where
    5.36    "\<box>\<lbrakk>t\<rbrakk> = t"
    5.37 -  "(CAppL E t')\<lbrakk>t\<rbrakk> = App (E\<lbrakk>t\<rbrakk>) t'"
    5.38 -  "(CAppR t' E)\<lbrakk>t\<rbrakk> = App t' (E\<lbrakk>t\<rbrakk>)"
    5.39 -  "(CLam [x].E)\<lbrakk>t\<rbrakk> = Lam [x].(E\<lbrakk>t\<rbrakk>)" 
    5.40 +| "(CAppL E t')\<lbrakk>t\<rbrakk> = App (E\<lbrakk>t\<rbrakk>) t'"
    5.41 +| "(CAppR t' E)\<lbrakk>t\<rbrakk> = App t' (E\<lbrakk>t\<rbrakk>)"
    5.42 +| "(CLam [x].E)\<lbrakk>t\<rbrakk> = Lam [x].(E\<lbrakk>t\<rbrakk>)" 
    5.43  by (rule TrueI)+
    5.44  
    5.45  text {* 
    5.46 @@ -81,14 +78,13 @@
    5.47  
    5.48  text {* The composition of two contexts. *}
    5.49  
    5.50 -consts 
    5.51 +nominal_primrec
    5.52   ctx_compose :: "ctx \<Rightarrow> ctx \<Rightarrow> ctx" ("_ \<circ> _" [100,100] 100)
    5.53 -
    5.54 -nominal_primrec
    5.55 +where
    5.56    "\<box> \<circ> E' = E'"
    5.57 -  "(CAppL E t') \<circ> E' = CAppL (E \<circ> E') t'"
    5.58 -  "(CAppR t' E) \<circ> E' = CAppR t' (E \<circ> E')"
    5.59 -  "(CLam [x].E) \<circ> E' = CLam [x].(E \<circ> E')"
    5.60 +| "(CAppL E t') \<circ> E' = CAppL (E \<circ> E') t'"
    5.61 +| "(CAppR t' E) \<circ> E' = CAppR t' (E \<circ> E')"
    5.62 +| "(CLam [x].E) \<circ> E' = CLam [x].(E \<circ> E')"
    5.63  by (rule TrueI)+
    5.64    
    5.65  lemma ctx_compose:
     6.1 --- a/src/HOL/Nominal/Examples/Crary.thy	Sat Dec 13 15:35:29 2008 +0100
     6.2 +++ b/src/HOL/Nominal/Examples/Crary.thy	Sat Dec 13 17:13:09 2008 +0100
     6.3 @@ -1,4 +1,3 @@
     6.4 -(* "$Id$" *)
     6.5  (*                                                    *)
     6.6  (* Formalisation of the chapter on Logical Relations  *)
     6.7  (* and a Case Study in Equivalence Checking           *)
     6.8 @@ -47,14 +46,20 @@
     6.9    shows "(\<exists> T\<^isub>1 T\<^isub>2. T=T\<^isub>1\<rightarrow>T\<^isub>2) \<or> T=TUnit \<or> T=TBase"
    6.10  by (induct T rule:ty.induct) (auto)
    6.11  
    6.12 -instance ty :: size ..
    6.13 +instantiation ty :: size
    6.14 +begin
    6.15  
    6.16 -nominal_primrec
    6.17 +nominal_primrec size_ty
    6.18 +where
    6.19    "size (TBase) = 1"
    6.20 -  "size (TUnit) = 1"
    6.21 -  "size (T\<^isub>1\<rightarrow>T\<^isub>2) = size T\<^isub>1 + size T\<^isub>2"
    6.22 +| "size (TUnit) = 1"
    6.23 +| "size (T\<^isub>1\<rightarrow>T\<^isub>2) = size T\<^isub>1 + size T\<^isub>2"
    6.24  by (rule TrueI)+
    6.25  
    6.26 +instance ..
    6.27 +
    6.28 +end
    6.29 +
    6.30  lemma ty_size_greater_zero[simp]:
    6.31    fixes T::"ty"
    6.32    shows "size T > 0"
    6.33 @@ -87,16 +92,15 @@
    6.34  using a
    6.35  by (induct rule: lookup.induct)
    6.36     (auto simp add: fresh_list_cons fresh_prod fresh_atm)
    6.37 -
    6.38 -consts
    6.39 -  psubst :: "Subst \<Rightarrow> trm \<Rightarrow> trm"  ("_<_>" [100,100] 130)
    6.40   
    6.41  nominal_primrec
    6.42 +  psubst :: "Subst \<Rightarrow> trm \<Rightarrow> trm"  ("_<_>" [100,100] 130)
    6.43 +where
    6.44    "\<theta><(Var x)> = (lookup \<theta> x)"
    6.45 -  "\<theta><(App t\<^isub>1 t\<^isub>2)> = App \<theta><t\<^isub>1> \<theta><t\<^isub>2>"
    6.46 -  "x\<sharp>\<theta> \<Longrightarrow> \<theta><(Lam [x].t)> = Lam [x].(\<theta><t>)"
    6.47 -  "\<theta><(Const n)> = Const n"
    6.48 -  "\<theta><(Unit)> = Unit"
    6.49 +| "\<theta><(App t\<^isub>1 t\<^isub>2)> = App \<theta><t\<^isub>1> \<theta><t\<^isub>2>"
    6.50 +| "x\<sharp>\<theta> \<Longrightarrow> \<theta><(Lam [x].t)> = Lam [x].(\<theta><t>)"
    6.51 +| "\<theta><(Const n)> = Const n"
    6.52 +| "\<theta><(Unit)> = Unit"
    6.53  apply(finite_guess)+
    6.54  apply(rule TrueI)+
    6.55  apply(simp add: abs_fresh)+
     7.1 --- a/src/HOL/Nominal/Examples/Fsub.thy	Sat Dec 13 15:35:29 2008 +0100
     7.2 +++ b/src/HOL/Nominal/Examples/Fsub.thy	Sat Dec 13 17:13:09 2008 +0100
     7.3 @@ -1,5 +1,3 @@
     7.4 -(* $Id$ *)
     7.5 -
     7.6  (*<*)
     7.7  theory Fsub
     7.8  imports "../Nominal" 
     7.9 @@ -229,32 +227,26 @@
    7.10  
    7.11  section {* Size and Capture-Avoiding Substitution for Types *}
    7.12  
    7.13 -consts size_ty :: "ty \<Rightarrow> nat"
    7.14 -
    7.15  nominal_primrec
    7.16 +  size_ty :: "ty \<Rightarrow> nat"
    7.17 +where
    7.18    "size_ty (Tvar X) = 1"
    7.19 -  "size_ty (Top) = 1"
    7.20 -  "size_ty (T1 \<rightarrow> T2) = (size_ty T1) + (size_ty T2) + 1"
    7.21 -  "X\<sharp>T1 \<Longrightarrow> size_ty (\<forall>[X<:T1].T2) = (size_ty T1) + (size_ty T2) + 1"
    7.22 +| "size_ty (Top) = 1"
    7.23 +| "size_ty (T1 \<rightarrow> T2) = (size_ty T1) + (size_ty T2) + 1"
    7.24 +| "X\<sharp>T1 \<Longrightarrow> size_ty (\<forall>[X<:T1].T2) = (size_ty T1) + (size_ty T2) + 1"
    7.25    apply (finite_guess)+
    7.26    apply (rule TrueI)+
    7.27    apply (simp add: fresh_nat)
    7.28    apply (fresh_guess)+
    7.29    done
    7.30  
    7.31 -consts subst_ty :: "tyvrs \<Rightarrow> ty \<Rightarrow> ty \<Rightarrow> ty"
    7.32 -
    7.33 -syntax 
    7.34 - subst_ty_syn :: "ty \<Rightarrow> tyvrs \<Rightarrow> ty \<Rightarrow> ty" ("_[_:=_]\<^isub>t\<^isub>y" [100,100,100] 100)
    7.35 -
    7.36 -translations 
    7.37 -  "T1[Y:=T2]\<^isub>t\<^isub>y" \<rightleftharpoons> "subst_ty Y T2 T1"
    7.38 -
    7.39  nominal_primrec
    7.40 +  subst_ty :: "ty \<Rightarrow> tyvrs \<Rightarrow> ty \<Rightarrow> ty" ("_[_:=_]\<^isub>t\<^isub>y" [100,100,100] 100)
    7.41 +where
    7.42    "(Tvar X)[Y:=T]\<^isub>t\<^isub>y= (if X=Y then T else (Tvar X))"
    7.43 -  "(Top)[Y:=T]\<^isub>t\<^isub>y = Top"
    7.44 -  "(T\<^isub>1 \<rightarrow> T\<^isub>2)[Y:=T]\<^isub>t\<^isub>y = (T\<^isub>1[Y:=T]\<^isub>t\<^isub>y) \<rightarrow> (T\<^isub>2[Y:=T]\<^isub>t\<^isub>y)"
    7.45 -  "\<lbrakk>X\<sharp>(Y,T); X\<sharp>T\<^isub>1\<rbrakk> \<Longrightarrow> (\<forall>[X<:T\<^isub>1].T\<^isub>2)[Y:=T]\<^isub>t\<^isub>y = (\<forall>[X<:(T\<^isub>1[Y:=T]\<^isub>t\<^isub>y)].(T\<^isub>2[Y:=T]\<^isub>t\<^isub>y))"
    7.46 +| "(Top)[Y:=T]\<^isub>t\<^isub>y = Top"
    7.47 +| "(T\<^isub>1 \<rightarrow> T\<^isub>2)[Y:=T]\<^isub>t\<^isub>y = (T\<^isub>1[Y:=T]\<^isub>t\<^isub>y) \<rightarrow> (T\<^isub>2[Y:=T]\<^isub>t\<^isub>y)"
    7.48 +| "\<lbrakk>X\<sharp>(Y,T); X\<sharp>T\<^isub>1\<rbrakk> \<Longrightarrow> (\<forall>[X<:T\<^isub>1].T\<^isub>2)[Y:=T]\<^isub>t\<^isub>y = (\<forall>[X<:(T\<^isub>1[Y:=T]\<^isub>t\<^isub>y)].(T\<^isub>2[Y:=T]\<^isub>t\<^isub>y))"
    7.49    apply (finite_guess)+
    7.50    apply (rule TrueI)+
    7.51    apply (simp add: abs_fresh)
     8.1 --- a/src/HOL/Nominal/Examples/Height.thy	Sat Dec 13 15:35:29 2008 +0100
     8.2 +++ b/src/HOL/Nominal/Examples/Height.thy	Sat Dec 13 17:13:09 2008 +0100
     8.3 @@ -1,5 +1,3 @@
     8.4 -(* $Id$ *)
     8.5 -
     8.6  theory Height
     8.7    imports "../Nominal"
     8.8  begin
     8.9 @@ -17,13 +15,13 @@
    8.10    | Lam "\<guillemotleft>name\<guillemotright>lam" ("Lam [_]._" [100,100] 100)
    8.11  
    8.12  text {* Definition of the height-function on lambda-terms. *} 
    8.13 -consts 
    8.14 -  height :: "lam \<Rightarrow> int"
    8.15  
    8.16  nominal_primrec
    8.17 +  height :: "lam \<Rightarrow> int"
    8.18 +where
    8.19    "height (Var x) = 1"
    8.20 -  "height (App t1 t2) = (max (height t1) (height t2)) + 1"
    8.21 -  "height (Lam [a].t) = (height t) + 1"
    8.22 +| "height (App t1 t2) = (max (height t1) (height t2)) + 1"
    8.23 +| "height (Lam [a].t) = (height t) + 1"
    8.24    apply(finite_guess add: perm_int_def)+
    8.25    apply(rule TrueI)+
    8.26    apply(simp add: fresh_int)
    8.27 @@ -32,13 +30,12 @@
    8.28  
    8.29  text {* Definition of capture-avoiding substitution. *}
    8.30  
    8.31 -consts
    8.32 +nominal_primrec
    8.33    subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam"  ("_[_::=_]" [100,100,100] 100)
    8.34 -
    8.35 -nominal_primrec
    8.36 +where
    8.37    "(Var x)[y::=t'] = (if x=y then t' else (Var x))"
    8.38 -  "(App t1 t2)[y::=t'] = App (t1[y::=t']) (t2[y::=t'])"
    8.39 -  "\<lbrakk>x\<sharp>y; x\<sharp>t'\<rbrakk> \<Longrightarrow> (Lam [x].t)[y::=t'] = Lam [x].(t[y::=t'])"
    8.40 +| "(App t1 t2)[y::=t'] = App (t1[y::=t']) (t2[y::=t'])"
    8.41 +| "\<lbrakk>x\<sharp>y; x\<sharp>t'\<rbrakk> \<Longrightarrow> (Lam [x].t)[y::=t'] = Lam [x].(t[y::=t'])"
    8.42  apply(finite_guess)+
    8.43  apply(rule TrueI)+
    8.44  apply(simp add: abs_fresh)
     9.1 --- a/src/HOL/Nominal/Examples/Lam_Funs.thy	Sat Dec 13 15:35:29 2008 +0100
     9.2 +++ b/src/HOL/Nominal/Examples/Lam_Funs.thy	Sat Dec 13 17:13:09 2008 +0100
     9.3 @@ -1,5 +1,3 @@
     9.4 -(* $Id$ *)
     9.5 -
     9.6  theory Lam_Funs
     9.7    imports "../Nominal"
     9.8  begin
     9.9 @@ -18,13 +16,12 @@
    9.10  
    9.11  text {* The depth of a lambda-term. *}
    9.12  
    9.13 -consts 
    9.14 +nominal_primrec
    9.15    depth :: "lam \<Rightarrow> nat"
    9.16 -
    9.17 -nominal_primrec
    9.18 +where
    9.19    "depth (Var x) = 1"
    9.20 -  "depth (App t1 t2) = (max (depth t1) (depth t2)) + 1"
    9.21 -  "depth (Lam [a].t) = (depth t) + 1"
    9.22 +| "depth (App t1 t2) = (max (depth t1) (depth t2)) + 1"
    9.23 +| "depth (Lam [a].t) = (depth t) + 1"
    9.24    apply(finite_guess)+
    9.25    apply(rule TrueI)+
    9.26    apply(simp add: fresh_nat)
    9.27 @@ -38,13 +35,12 @@
    9.28    the invariant that frees always returns a finite set of names. 
    9.29  *}
    9.30  
    9.31 -consts 
    9.32 +nominal_primrec (invariant: "\<lambda>s::name set. finite s")
    9.33    frees :: "lam \<Rightarrow> name set"
    9.34 -
    9.35 -nominal_primrec (invariant: "\<lambda>s::name set. finite s")
    9.36 +where
    9.37    "frees (Var a) = {a}"
    9.38 -  "frees (App t1 t2) = (frees t1) \<union> (frees t2)"
    9.39 -  "frees (Lam [a].t) = (frees t) - {a}"
    9.40 +| "frees (App t1 t2) = (frees t1) \<union> (frees t2)"
    9.41 +| "frees (Lam [a].t) = (frees t) - {a}"
    9.42  apply(finite_guess)+
    9.43  apply(simp)+ 
    9.44  apply(simp add: fresh_def)
    9.45 @@ -78,14 +74,13 @@
    9.46    and   X::"name"
    9.47    shows "pi\<bullet>(lookup \<theta> X) = lookup (pi\<bullet>\<theta>) (pi\<bullet>X)"
    9.48  by (induct \<theta>) (auto simp add: eqvts)
    9.49 -
    9.50 -consts
    9.51 -  psubst :: "(name\<times>lam) list \<Rightarrow> lam \<Rightarrow> lam"  ("_<_>" [95,95] 105)
    9.52   
    9.53  nominal_primrec
    9.54 +  psubst :: "(name\<times>lam) list \<Rightarrow> lam \<Rightarrow> lam"  ("_<_>" [95,95] 105)
    9.55 +where
    9.56    "\<theta><(Var x)> = (lookup \<theta> x)"
    9.57 -  "\<theta><(App e\<^isub>1 e\<^isub>2)> = App (\<theta><e\<^isub>1>) (\<theta><e\<^isub>2>)"
    9.58 -  "x\<sharp>\<theta> \<Longrightarrow> \<theta><(Lam [x].e)> = Lam [x].(\<theta><e>)"
    9.59 +| "\<theta><(App e\<^isub>1 e\<^isub>2)> = App (\<theta><e\<^isub>1>) (\<theta><e\<^isub>2>)"
    9.60 +| "x\<sharp>\<theta> \<Longrightarrow> \<theta><(Lam [x].e)> = Lam [x].(\<theta><e>)"
    9.61  apply(finite_guess)+
    9.62  apply(rule TrueI)+
    9.63  apply(simp add: abs_fresh)+
    9.64 @@ -130,26 +125,24 @@
    9.65  
    9.66  text {* Filling a lambda-term into a context. *}
    9.67  
    9.68 -consts 
    9.69 +nominal_primrec
    9.70    filling :: "clam \<Rightarrow> lam \<Rightarrow> lam" ("_\<lbrakk>_\<rbrakk>" [100,100] 100)
    9.71 -
    9.72 -nominal_primrec
    9.73 +where
    9.74    "\<box>\<lbrakk>t\<rbrakk> = t"
    9.75 -  "(CAppL E t')\<lbrakk>t\<rbrakk> = App (E\<lbrakk>t\<rbrakk>) t'"
    9.76 -  "(CAppR t' E)\<lbrakk>t\<rbrakk> = App t' (E\<lbrakk>t\<rbrakk>)"
    9.77 -  "(CLam [x].E)\<lbrakk>t\<rbrakk> = Lam [x].(E\<lbrakk>t\<rbrakk>)" 
    9.78 +| "(CAppL E t')\<lbrakk>t\<rbrakk> = App (E\<lbrakk>t\<rbrakk>) t'"
    9.79 +| "(CAppR t' E)\<lbrakk>t\<rbrakk> = App t' (E\<lbrakk>t\<rbrakk>)"
    9.80 +| "(CLam [x].E)\<lbrakk>t\<rbrakk> = Lam [x].(E\<lbrakk>t\<rbrakk>)" 
    9.81  by (rule TrueI)+
    9.82  
    9.83  text {* Composition od two contexts *}
    9.84  
    9.85 -consts 
    9.86 +nominal_primrec
    9.87   clam_compose :: "clam \<Rightarrow> clam \<Rightarrow> clam" ("_ \<circ> _" [100,100] 100)
    9.88 -
    9.89 -nominal_primrec
    9.90 +where
    9.91    "\<box> \<circ> E' = E'"
    9.92 -  "(CAppL E t') \<circ> E' = CAppL (E \<circ> E') t'"
    9.93 -  "(CAppR t' E) \<circ> E' = CAppR t' (E \<circ> E')"
    9.94 -  "(CLam [x].E) \<circ> E' = CLam [x].(E \<circ> E')"
    9.95 +| "(CAppL E t') \<circ> E' = CAppL (E \<circ> E') t'"
    9.96 +| "(CAppR t' E) \<circ> E' = CAppR t' (E \<circ> E')"
    9.97 +| "(CLam [x].E) \<circ> E' = CLam [x].(E \<circ> E')"
    9.98  by (rule TrueI)+
    9.99    
   9.100  lemma clam_compose:
    10.1 --- a/src/HOL/Nominal/Examples/LocalWeakening.thy	Sat Dec 13 15:35:29 2008 +0100
    10.2 +++ b/src/HOL/Nominal/Examples/LocalWeakening.thy	Sat Dec 13 17:13:09 2008 +0100
    10.3 @@ -1,5 +1,3 @@
    10.4 -(* $Id$ *)
    10.5 -
    10.6  (* Formalisation of weakening using locally nameless    *)
    10.7  (* terms; the nominal infrastructure can also derive    *)
    10.8  (* strong induction principles for such representations *)
    10.9 @@ -29,13 +27,13 @@
   10.10  by (induct t rule: llam.induct)
   10.11     (auto simp add: llam.inject)
   10.12  
   10.13 -consts llam_size :: "llam \<Rightarrow> nat"
   10.14 -
   10.15  nominal_primrec
   10.16 - "llam_size (lPar a) = 1"
   10.17 - "llam_size (lVar n) = 1"
   10.18 - "llam_size (lApp t1 t2) = 1 + (llam_size t1) + (llam_size t2)"
   10.19 - "llam_size (lLam t) = 1 + (llam_size t)"
   10.20 +  llam_size :: "llam \<Rightarrow> nat"
   10.21 +where
   10.22 +  "llam_size (lPar a) = 1"
   10.23 +| "llam_size (lVar n) = 1"
   10.24 +| "llam_size (lApp t1 t2) = 1 + (llam_size t1) + (llam_size t2)"
   10.25 +| "llam_size (lLam t) = 1 + (llam_size t)"
   10.26  by (rule TrueI)+
   10.27  
   10.28  function  
    11.1 --- a/src/HOL/Nominal/Examples/SN.thy	Sat Dec 13 15:35:29 2008 +0100
    11.2 +++ b/src/HOL/Nominal/Examples/SN.thy	Sat Dec 13 17:13:09 2008 +0100
    11.3 @@ -1,5 +1,3 @@
    11.4 -(* $Id$ *)
    11.5 -
    11.6  theory SN
    11.7    imports Lam_Funs
    11.8  begin
    11.9 @@ -228,12 +226,11 @@
   11.10  
   11.11  section {* Candidates *}
   11.12  
   11.13 -consts
   11.14 +nominal_primrec
   11.15    RED :: "ty \<Rightarrow> lam set"
   11.16 -
   11.17 -nominal_primrec
   11.18 +where
   11.19    "RED (TVar X) = {t. SN(t)}"
   11.20 -  "RED (\<tau>\<rightarrow>\<sigma>) =   {t. \<forall>u. (u\<in>RED \<tau> \<longrightarrow> (App t u)\<in>RED \<sigma>)}"
   11.21 +| "RED (\<tau>\<rightarrow>\<sigma>) =   {t. \<forall>u. (u\<in>RED \<tau> \<longrightarrow> (App t u)\<in>RED \<sigma>)}"
   11.22  by (rule TrueI)+
   11.23  
   11.24  text {* neutral terms *}
   11.25 @@ -248,13 +245,12 @@
   11.26  where
   11.27    fst[intro!]:  "(App t s) \<guillemotright> t"
   11.28  
   11.29 -consts
   11.30 +nominal_primrec
   11.31    fst_app_aux::"lam\<Rightarrow>lam option"
   11.32 -
   11.33 -nominal_primrec
   11.34 +where
   11.35    "fst_app_aux (Var a)     = None"
   11.36 -  "fst_app_aux (App t1 t2) = Some t1"
   11.37 -  "fst_app_aux (Lam [x].t) = None"
   11.38 +| "fst_app_aux (App t1 t2) = Some t1"
   11.39 +| "fst_app_aux (Lam [x].t) = None"
   11.40  apply(finite_guess)+
   11.41  apply(rule TrueI)+
   11.42  apply(simp add: fresh_none)
    12.1 --- a/src/HOL/Nominal/Examples/SOS.thy	Sat Dec 13 15:35:29 2008 +0100
    12.2 +++ b/src/HOL/Nominal/Examples/SOS.thy	Sat Dec 13 17:13:09 2008 +0100
    12.3 @@ -1,4 +1,3 @@
    12.4 -(* "$Id$" *)
    12.5  (*                                                        *)
    12.6  (* Formalisation of some typical SOS-proofs.              *)
    12.7  (*                                                        *) 
    12.8 @@ -62,13 +61,12 @@
    12.9  
   12.10  (* parallel substitution *)
   12.11  
   12.12 -consts
   12.13 +nominal_primrec
   12.14    psubst :: "(name\<times>trm) list \<Rightarrow> trm \<Rightarrow> trm"  ("_<_>" [95,95] 105)
   12.15 - 
   12.16 -nominal_primrec
   12.17 +where
   12.18    "\<theta><(Var x)> = (lookup \<theta> x)"
   12.19 -  "\<theta><(App e\<^isub>1 e\<^isub>2)> = App (\<theta><e\<^isub>1>) (\<theta><e\<^isub>2>)"
   12.20 -  "x\<sharp>\<theta> \<Longrightarrow> \<theta><(Lam [x].e)> = Lam [x].(\<theta><e>)"
   12.21 +| "\<theta><(App e\<^isub>1 e\<^isub>2)> = App (\<theta><e\<^isub>1>) (\<theta><e\<^isub>2>)"
   12.22 +| "x\<sharp>\<theta> \<Longrightarrow> \<theta><(Lam [x].e)> = Lam [x].(\<theta><e>)"
   12.23  apply(finite_guess)+
   12.24  apply(rule TrueI)+
   12.25  apply(simp add: abs_fresh)+
   12.26 @@ -349,12 +347,12 @@
   12.27  using h by (induct) (auto)
   12.28  
   12.29  (* Valuation *)
   12.30 -consts
   12.31 -  V :: "ty \<Rightarrow> trm set" 
   12.32  
   12.33  nominal_primrec
   12.34 +  V :: "ty \<Rightarrow> trm set" 
   12.35 +where
   12.36    "V (TVar x) = {e. val e}"
   12.37 -  "V (T\<^isub>1 \<rightarrow> T\<^isub>2) = {Lam [x].e | x e. \<forall> v \<in> (V T\<^isub>1). \<exists> v'. e[x::=v] \<Down> v' \<and> v' \<in> V T\<^isub>2}"
   12.38 +| "V (T\<^isub>1 \<rightarrow> T\<^isub>2) = {Lam [x].e | x e. \<forall> v \<in> (V T\<^isub>1). \<exists> v'. e[x::=v] \<Down> v' \<and> v' \<in> V T\<^isub>2}"
   12.39    by (rule TrueI)+ 
   12.40  
   12.41  lemma V_eqvt:
    13.1 --- a/src/HOL/Nominal/Examples/Standardization.thy	Sat Dec 13 15:35:29 2008 +0100
    13.2 +++ b/src/HOL/Nominal/Examples/Standardization.thy	Sat Dec 13 17:13:09 2008 +0100
    13.3 @@ -1,5 +1,4 @@
    13.4  (*  Title:      HOL/Nominal/Examples/Standardization.thy
    13.5 -    ID:         $Id$
    13.6      Author:     Stefan Berghofer and Tobias Nipkow
    13.7      Copyright   2005, 2008 TU Muenchen
    13.8  *)
    13.9 @@ -24,24 +23,30 @@
   13.10  | App "lam" "lam" (infixl "\<degree>" 200)
   13.11  | Lam "\<guillemotleft>name\<guillemotright>lam" ("Lam [_]._" [0, 10] 10)
   13.12  
   13.13 -instance lam :: size ..
   13.14 +instantiation lam :: size
   13.15 +begin
   13.16  
   13.17 -nominal_primrec
   13.18 +nominal_primrec size_lam
   13.19 +where
   13.20    "size (Var n) = 0"
   13.21 -  "size (t \<degree> u) = size t + size u + 1"
   13.22 -  "size (Lam [x].t) = size t + 1"
   13.23 +| "size (t \<degree> u) = size t + size u + 1"
   13.24 +| "size (Lam [x].t) = size t + 1"
   13.25    apply finite_guess+
   13.26    apply (rule TrueI)+
   13.27    apply (simp add: fresh_nat)
   13.28    apply fresh_guess+
   13.29    done
   13.30  
   13.31 -consts subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam"  ("_[_::=_]" [300, 0, 0] 300)
   13.32 +instance ..
   13.33 +
   13.34 +end
   13.35  
   13.36  nominal_primrec
   13.37 +  subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam"  ("_[_::=_]" [300, 0, 0] 300)
   13.38 +where
   13.39    subst_Var: "(Var x)[y::=s] = (if x=y then s else (Var x))"
   13.40 -  subst_App: "(t\<^isub>1 \<degree> t\<^isub>2)[y::=s] = t\<^isub>1[y::=s] \<degree> t\<^isub>2[y::=s]"
   13.41 -  subst_Lam: "x \<sharp> (y, s) \<Longrightarrow> (Lam [x].t)[y::=s] = (Lam [x].(t[y::=s]))"
   13.42 +| subst_App: "(t\<^isub>1 \<degree> t\<^isub>2)[y::=s] = t\<^isub>1[y::=s] \<degree> t\<^isub>2[y::=s]"
   13.43 +| subst_Lam: "x \<sharp> (y, s) \<Longrightarrow> (Lam [x].t)[y::=s] = (Lam [x].(t[y::=s]))"
   13.44    apply(finite_guess)+
   13.45    apply(rule TrueI)+
   13.46    apply(simp add: abs_fresh)
    14.1 --- a/src/HOL/Nominal/Examples/Type_Preservation.thy	Sat Dec 13 15:35:29 2008 +0100
    14.2 +++ b/src/HOL/Nominal/Examples/Type_Preservation.thy	Sat Dec 13 17:13:09 2008 +0100
    14.3 @@ -1,5 +1,3 @@
    14.4 -(* $Id$ *)
    14.5 -
    14.6  theory Type_Preservation
    14.7    imports Nominal
    14.8  begin
    14.9 @@ -21,13 +19,12 @@
   14.10  
   14.11  text {* Capture-Avoiding Substitution *}
   14.12  
   14.13 -consts 
   14.14 +nominal_primrec
   14.15    subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam"  ("_[_::=_]")
   14.16 -
   14.17 -nominal_primrec
   14.18 +where
   14.19    "(Var x)[y::=s] = (if x=y then s else (Var x))"
   14.20 -  "(App t\<^isub>1 t\<^isub>2)[y::=s] = App (t\<^isub>1[y::=s]) (t\<^isub>2[y::=s])"
   14.21 -  "x\<sharp>(y,s) \<Longrightarrow> (Lam [x].t)[y::=s] = Lam [x].(t[y::=s])"
   14.22 +| "(App t\<^isub>1 t\<^isub>2)[y::=s] = App (t\<^isub>1[y::=s]) (t\<^isub>2[y::=s])"
   14.23 +| "x\<sharp>(y,s) \<Longrightarrow> (Lam [x].t)[y::=s] = Lam [x].(t[y::=s])"
   14.24  apply(finite_guess)+
   14.25  apply(rule TrueI)+
   14.26  apply(simp add: abs_fresh)
    15.1 --- a/src/HOL/Nominal/Examples/W.thy	Sat Dec 13 15:35:29 2008 +0100
    15.2 +++ b/src/HOL/Nominal/Examples/W.thy	Sat Dec 13 17:13:09 2008 +0100
    15.3 @@ -1,5 +1,3 @@
    15.4 -(* "$Id$" *)
    15.5 -
    15.6  theory W
    15.7  imports Nominal
    15.8  begin
    15.9 @@ -50,26 +48,68 @@
   15.10    Ctxt  = "(var\<times>tyS) list" 
   15.11  
   15.12  text {* free type variables *}
   15.13 -consts
   15.14 -  ftv    :: "'a \<Rightarrow> tvar list"
   15.15 +
   15.16 +class ftv = type +
   15.17 +  fixes ftv :: "'a \<Rightarrow> tvar list"
   15.18 +
   15.19 +instantiation * :: (ftv, ftv) ftv
   15.20 +begin
   15.21 +
   15.22 +primrec ftv_prod
   15.23 +where
   15.24 + "ftv (x::'a::ftv, y::'b::ftv) = (ftv x)@(ftv y)"
   15.25 +
   15.26 +instance ..
   15.27 +
   15.28 +end
   15.29  
   15.30 -primrec (ftv_of_prod)
   15.31 - "ftv (x,y) = (ftv x)@(ftv y)"
   15.32 +instantiation tvar :: ftv
   15.33 +begin
   15.34 +
   15.35 +definition
   15.36 +  ftv_of_tvar[simp]:  "ftv X \<equiv> [(X::tvar)]"
   15.37  
   15.38 -defs (overloaded)
   15.39 -  ftv_of_tvar[simp]:  "ftv X \<equiv> [(X::tvar)]"
   15.40 +instance ..
   15.41 +
   15.42 +end
   15.43 +
   15.44 +instantiation var :: ftv
   15.45 +begin
   15.46 +
   15.47 +definition
   15.48    ftv_of_var[simp]:   "ftv (x::var) \<equiv> []" 
   15.49  
   15.50 -primrec (ftv_of_list)
   15.51 +instance ..
   15.52 +
   15.53 +end
   15.54 +
   15.55 +instantiation list :: (ftv) ftv
   15.56 +begin
   15.57 +
   15.58 +primrec ftv_list
   15.59 +where
   15.60    "ftv [] = []"
   15.61 -  "ftv (x#xs) = (ftv x)@(ftv xs)"
   15.62 +| "ftv (x#xs) = (ftv x)@(ftv xs)"
   15.63 +
   15.64 +instance ..
   15.65 +
   15.66 +end
   15.67  
   15.68  (* free type-variables of types *)
   15.69 -nominal_primrec (ftv_ty)
   15.70 +
   15.71 +instantiation ty :: ftv
   15.72 +begin
   15.73 +
   15.74 +nominal_primrec ftv_ty
   15.75 +where
   15.76    "ftv (TVar X) = [X]"
   15.77 -  "ftv (T\<^isub>1\<rightarrow>T\<^isub>2) = (ftv T\<^isub>1)@(ftv T\<^isub>2)"
   15.78 +| "ftv (T\<^isub>1\<rightarrow>T\<^isub>2) = (ftv T\<^isub>1)@(ftv T\<^isub>2)"
   15.79  by (rule TrueI)+
   15.80  
   15.81 +instance ..
   15.82 +
   15.83 +end
   15.84 +
   15.85  lemma ftv_ty_eqvt[eqvt]:
   15.86    fixes pi::"tvar prm"
   15.87    and   T::"ty"
   15.88 @@ -77,9 +117,13 @@
   15.89  by (nominal_induct T rule: ty.strong_induct)
   15.90     (perm_simp add: append_eqvt)+
   15.91  
   15.92 -nominal_primrec (ftv_tyS)
   15.93 +instantiation tyS :: ftv
   15.94 +begin
   15.95 +
   15.96 +nominal_primrec ftv_tyS
   15.97 +where
   15.98    "ftv (Ty T)    = ftv T"
   15.99 -  "ftv (\<forall>[X].S) = (ftv S) - [X]"
  15.100 +| "ftv (\<forall>[X].S) = (ftv S) - [X]"
  15.101  apply(finite_guess add: ftv_ty_eqvt fs_tvar1)+
  15.102  apply(rule TrueI)+
  15.103  apply(rule difference_fresh)
  15.104 @@ -87,6 +131,10 @@
  15.105  apply(fresh_guess add: ftv_ty_eqvt fs_tvar1)+
  15.106  done
  15.107  
  15.108 +instance ..
  15.109 +
  15.110 +end
  15.111 +
  15.112  lemma ftv_tyS_eqvt[eqvt]:
  15.113    fixes pi::"tvar prm"
  15.114    and   S::"tyS"
  15.115 @@ -140,11 +188,11 @@
  15.116  
  15.117  types Subst = "(tvar\<times>ty) list"
  15.118  
  15.119 -consts
  15.120 - psubst :: "Subst \<Rightarrow> 'a \<Rightarrow> 'a"       ("_<_>" [100,60] 120)
  15.121 +class psubst =
  15.122 +  fixes psubst :: "Subst \<Rightarrow> 'a \<Rightarrow> 'a"       ("_<_>" [100,60] 120)
  15.123  
  15.124  abbreviation 
  15.125 -  subst :: "'a \<Rightarrow> tvar \<Rightarrow> ty \<Rightarrow> 'a"  ("_[_::=_]" [100,100,100] 100)
  15.126 +  subst :: "'a::psubst \<Rightarrow> tvar \<Rightarrow> ty \<Rightarrow> 'a"  ("_[_::=_]" [100,100,100] 100)
  15.127  where
  15.128    "smth[X::=T] \<equiv> ([(X,T)])<smth>" 
  15.129  
  15.130 @@ -159,11 +207,19 @@
  15.131    shows "pi\<bullet>(lookup \<theta> X) = lookup (pi\<bullet>\<theta>) (pi\<bullet>X)"
  15.132  by (induct \<theta>) (auto simp add: eqvts)
  15.133  
  15.134 -nominal_primrec (psubst_ty)
  15.135 +instantiation ty :: psubst
  15.136 +begin
  15.137 +
  15.138 +nominal_primrec psubst_ty
  15.139 +where
  15.140    "\<theta><TVar X>   = lookup \<theta> X"
  15.141 -  "\<theta><T\<^isub>1 \<rightarrow> T\<^isub>2> = (\<theta><T\<^isub>1>) \<rightarrow> (\<theta><T\<^isub>2>)"
  15.142 +| "\<theta><T\<^isub>1 \<rightarrow> T\<^isub>2> = (\<theta><T\<^isub>1>) \<rightarrow> (\<theta><T\<^isub>2>)"
  15.143  by (rule TrueI)+
  15.144  
  15.145 +instance ..
  15.146 +
  15.147 +end
  15.148 +
  15.149  lemma psubst_ty_eqvt[eqvt]:
  15.150    fixes pi1::"tvar prm"
  15.151    and   \<theta>::"Subst"
    16.1 --- a/src/HOL/Nominal/nominal_primrec.ML	Sat Dec 13 15:35:29 2008 +0100
    16.2 +++ b/src/HOL/Nominal/nominal_primrec.ML	Sat Dec 13 17:13:09 2008 +0100
    16.3 @@ -1,5 +1,4 @@
    16.4  (*  Title:      HOL/Nominal/nominal_primrec.ML
    16.5 -    ID:         $Id$
    16.6      Author:     Stefan Berghofer, TU Muenchen and Norbert Voelker, FernUni Hagen
    16.7  
    16.8  Package for defining functions on nominal datatypes by primitive recursion.
    16.9 @@ -8,14 +7,10 @@
   16.10  
   16.11  signature NOMINAL_PRIMREC =
   16.12  sig
   16.13 -  val add_primrec: string -> string list option -> string option ->
   16.14 -    ((Binding.T * string) * Attrib.src list) list -> theory -> Proof.state
   16.15 -  val add_primrec_unchecked: string -> string list option -> string option ->
   16.16 -    ((Binding.T * string) * Attrib.src list) list -> theory -> Proof.state
   16.17 -  val add_primrec_i: string -> term list option -> term option ->
   16.18 -    ((Binding.T * term) * attribute list) list -> theory -> Proof.state
   16.19 -  val add_primrec_unchecked_i: string -> term list option -> term option ->
   16.20 -    ((Binding.T * term) * attribute list) list -> theory -> Proof.state
   16.21 +  val add_primrec: term list option -> term option ->
   16.22 +    (Binding.T * typ option * mixfix) list ->
   16.23 +    (Binding.T * typ option * mixfix) list ->
   16.24 +    (Attrib.binding * term) list -> local_theory -> Proof.state
   16.25  end;
   16.26  
   16.27  structure NominalPrimrec : NOMINAL_PRIMREC =
   16.28 @@ -26,23 +21,31 @@
   16.29  exception RecError of string;
   16.30  
   16.31  fun primrec_err s = error ("Nominal primrec definition error:\n" ^ s);
   16.32 -fun primrec_eq_err thy s eq =
   16.33 -  primrec_err (s ^ "\nin\n" ^ quote (Syntax.string_of_term_global thy eq));
   16.34 +fun primrec_eq_err lthy s eq =
   16.35 +  primrec_err (s ^ "\nin\n" ^ quote (Syntax.string_of_term lthy eq));
   16.36  
   16.37  
   16.38  (* preprocessing of equations *)
   16.39  
   16.40 -fun process_eqn thy eq rec_fns = 
   16.41 +fun unquantify t =
   16.42    let
   16.43 +    val (vs, Ts) = split_list (strip_qnt_vars "all" t);
   16.44 +    val body = strip_qnt_body "all" t;
   16.45 +    val (vs', _) = Name.variants vs (Name.make_context (fold_aterms
   16.46 +      (fn Free (v, _) => insert (op =) v | _ => I) body []))
   16.47 +  in (curry subst_bounds (map2 (curry Free) vs' Ts |> rev) body) end;
   16.48 +
   16.49 +fun process_eqn lthy is_fixed spec rec_fns = 
   16.50 +  let
   16.51 +    val eq = unquantify spec;
   16.52      val (lhs, rhs) = 
   16.53 -      if null (term_vars eq) then
   16.54 -        HOLogic.dest_eq (HOLogic.dest_Trueprop (Logic.strip_imp_concl eq))
   16.55 -        handle TERM _ => raise RecError "not a proper equation"
   16.56 -      else raise RecError "illegal schematic variable(s)";
   16.57 +      HOLogic.dest_eq (HOLogic.dest_Trueprop (Logic.strip_imp_concl eq))
   16.58 +      handle TERM _ => raise RecError "not a proper equation";
   16.59  
   16.60      val (recfun, args) = strip_comb lhs;
   16.61 -    val fnameT = dest_Const recfun handle TERM _ => 
   16.62 -      raise RecError "function is not declared as constant in theory";
   16.63 +    val fname = case recfun of Free (v, _) => if is_fixed v then v
   16.64 +          else raise RecError "illegal head of function equation"
   16.65 +      | _ => raise RecError "illegal head of function equation";
   16.66  
   16.67      val (ls', rest)  = take_prefix is_Free args;
   16.68      val (middle, rs') = take_suffix is_Free rest;
   16.69 @@ -68,26 +71,28 @@
   16.70      else
   16.71       (check_vars "repeated variable names in pattern: " (duplicates (op =) lfrees);
   16.72        check_vars "extra variables on rhs: "
   16.73 -        (map dest_Free (term_frees rhs) \\ lfrees);
   16.74 -      case AList.lookup (op =) rec_fns fnameT of
   16.75 +        (map dest_Free (term_frees rhs) |> subtract (op =) lfrees
   16.76 +          |> filter_out (is_fixed o fst));
   16.77 +      case AList.lookup (op =) rec_fns fname of
   16.78          NONE =>
   16.79 -          (fnameT, (tname, rpos, [(cname, (ls, cargs, rs, rhs, eq))]))::rec_fns
   16.80 +          (fname, (tname, rpos, [(cname, (ls, cargs, rs, rhs, eq))]))::rec_fns
   16.81        | SOME (_, rpos', eqns) =>
   16.82            if AList.defined (op =) eqns cname then
   16.83              raise RecError "constructor already occurred as pattern"
   16.84            else if rpos <> rpos' then
   16.85              raise RecError "position of recursive argument inconsistent"
   16.86            else
   16.87 -            AList.update (op =) (fnameT, (tname, rpos, (cname, (ls, cargs, rs, rhs, eq))::eqns))
   16.88 +            AList.update (op =)
   16.89 +              (fname, (tname, rpos, (cname, (ls, cargs, rs, rhs, eq))::eqns))
   16.90                rec_fns)
   16.91    end
   16.92 -  handle RecError s => primrec_eq_err thy s eq;
   16.93 +  handle RecError s => primrec_eq_err lthy s spec;
   16.94  
   16.95  val param_err = "Parameters must be the same for all recursive functions";
   16.96  
   16.97 -fun process_fun thy descr rec_eqns (i, fnameT as (fname, _)) (fnameTs, fnss) =
   16.98 +fun process_fun lthy descr eqns (i, fname) (fnames, fnss) =
   16.99    let
  16.100 -    val (_, (tname, _, constrs)) = List.nth (descr, i);
  16.101 +    val (_, (tname, _, constrs)) = nth descr i;
  16.102  
  16.103      (* substitute "fname ls x rs" by "y" for (x, (_, y)) in subs *)
  16.104  
  16.105 @@ -100,16 +105,17 @@
  16.106            let
  16.107              val (f, ts) = strip_comb t;
  16.108            in
  16.109 -            if is_Const f andalso dest_Const f mem map fst rec_eqns then
  16.110 +            if is_Free f
  16.111 +              andalso member (fn ((v, _), (w, _)) => v = w) eqns (dest_Free f) then
  16.112                let
  16.113 -                val fnameT' as (fname', _) = dest_Const f;
  16.114 -                val (_, rpos, eqns) = the (AList.lookup (op =) rec_eqns fnameT');
  16.115 -                val ls = Library.take (rpos, ts);
  16.116 -                val rest = Library.drop (rpos, ts);
  16.117 -                val (x', rs) = (hd rest, tl rest)
  16.118 -                  handle Empty => raise RecError ("not enough arguments\
  16.119 -                   \ in recursive application\nof function " ^ quote fname' ^ " on rhs");
  16.120 -                val rs' = (case eqns of
  16.121 +                val (fname', _) = dest_Free f;
  16.122 +                val (_, rpos, eqns') = the (AList.lookup (op =) eqns fname');
  16.123 +                val (ls, rs'') = chop rpos ts
  16.124 +                val (x', rs) = case rs'' of
  16.125 +                    x' :: rs => (x', rs)
  16.126 +                  | [] => raise RecError ("not enough arguments in recursive application\n"
  16.127 +                      ^ "of function " ^ quote fname' ^ " on rhs");
  16.128 +                val rs' = (case eqns' of
  16.129                      (_, (ls', _, rs', _, _)) :: _ =>
  16.130                        let val (rs1, rs2) = chop (length rs') rs
  16.131                        in
  16.132 @@ -126,7 +132,7 @@
  16.133                  | SOME (i', y) =>
  16.134                      fs
  16.135                      |> fold_map (subst subs) (xs @ rs')
  16.136 -                    ||> process_fun thy descr rec_eqns (i', fnameT')
  16.137 +                    ||> process_fun lthy descr eqns (i', fname')
  16.138                      |-> (fn ts' => pair (list_comb (y, ts')))
  16.139                end
  16.140              else
  16.141 @@ -138,41 +144,39 @@
  16.142  
  16.143      (* translate rec equations into function arguments suitable for rec comb *)
  16.144  
  16.145 -    fun trans eqns (cname, cargs) (fnameTs', fnss', fns) =
  16.146 +    fun trans eqns (cname, cargs) (fnames', fnss', fns) =
  16.147        (case AList.lookup (op =) eqns cname of
  16.148            NONE => (warning ("No equation for constructor " ^ quote cname ^
  16.149              "\nin definition of function " ^ quote fname);
  16.150 -              (fnameTs', fnss', (Const (@{const_name undefined}, dummyT))::fns))
  16.151 +              (fnames', fnss', (Const (@{const_name undefined}, dummyT))::fns))
  16.152          | SOME (ls, cargs', rs, rhs, eq) =>
  16.153              let
  16.154                val recs = filter (is_rec_type o snd) (cargs' ~~ cargs);
  16.155                val rargs = map fst recs;
  16.156 -              val subs = map (rpair dummyT o fst) 
  16.157 +              val subs = map (rpair dummyT o fst)
  16.158                  (rev (rename_wrt_term rhs rargs));
  16.159 -              val (rhs', (fnameTs'', fnss'')) = 
  16.160 -                  (subst (map (fn ((x, y), z) =>
  16.161 -                               (Free x, (body_index y, Free z)))
  16.162 -                          (recs ~~ subs)) rhs (fnameTs', fnss'))
  16.163 -                  handle RecError s => primrec_eq_err thy s eq
  16.164 -            in (fnameTs'', fnss'', 
  16.165 +              val (rhs', (fnames'', fnss'')) = subst (map2 (fn (x, y) => fn z =>
  16.166 +                (Free x, (body_index y, Free z))) recs subs) rhs (fnames', fnss')
  16.167 +                  handle RecError s => primrec_eq_err lthy s eq
  16.168 +            in (fnames'', fnss'', 
  16.169                  (list_abs_free (cargs' @ subs, rhs'))::fns)
  16.170              end)
  16.171  
  16.172 -  in (case AList.lookup (op =) fnameTs i of
  16.173 +  in (case AList.lookup (op =) fnames i of
  16.174        NONE =>
  16.175 -        if exists (equal fnameT o snd) fnameTs then
  16.176 +        if exists (fn (_, v) => fname = v) fnames then
  16.177            raise RecError ("inconsistent functions for datatype " ^ quote tname)
  16.178          else
  16.179            let
  16.180 -            val SOME (_, _, eqns as (_, (ls, _, rs, _, _)) :: _) =
  16.181 -              AList.lookup (op =) rec_eqns fnameT;
  16.182 -            val (fnameTs', fnss', fns) = fold_rev (trans eqns) constrs
  16.183 -              ((i, fnameT)::fnameTs, fnss, []) 
  16.184 +            val SOME (_, _, eqns' as (_, (ls, _, rs, _, _)) :: _) =
  16.185 +              AList.lookup (op =) eqns fname;
  16.186 +            val (fnames', fnss', fns) = fold_rev (trans eqns') constrs
  16.187 +              ((i, fname)::fnames, fnss, []) 
  16.188            in
  16.189 -            (fnameTs', (i, (fname, ls, rs, fns))::fnss')
  16.190 +            (fnames', (i, (fname, ls, rs, fns))::fnss')
  16.191            end
  16.192 -    | SOME fnameT' =>
  16.193 -        if fnameT = fnameT' then (fnameTs, fnss)
  16.194 +    | SOME fname' =>
  16.195 +        if fname = fname' then (fnames, fnss)
  16.196          else raise RecError ("inconsistent functions for datatype " ^ quote tname))
  16.197    end;
  16.198  
  16.199 @@ -195,18 +199,21 @@
  16.200  
  16.201  (* make definition *)
  16.202  
  16.203 -fun make_def thy fs (fname, ls, rs, rec_name, tname) =
  16.204 +fun make_def ctxt fixes fs (fname, ls, rs, rec_name, tname) =
  16.205    let
  16.206      val used = map fst (fold Term.add_frees fs []);
  16.207      val x = (Name.variant used "x", dummyT);
  16.208      val frees = ls @ x :: rs;
  16.209 -    val rhs = list_abs_free (frees,
  16.210 +    val raw_rhs = list_abs_free (frees,
  16.211        list_comb (Const (rec_name, dummyT), fs @ [Free x]))
  16.212 -    val def_name = Sign.base_name fname ^ "_" ^ Sign.base_name tname ^ "_def";
  16.213 -    val def_prop as _ $ _ $ t =
  16.214 -      singleton (Syntax.check_terms (ProofContext.init thy))
  16.215 -        (Logic.mk_equals (Const (fname, dummyT), rhs));
  16.216 -  in ((def_name, def_prop), subst_bounds (rev (map Free frees), strip_abs_body t)) end;
  16.217 +    val def_name = Thm.def_name (Sign.base_name fname);
  16.218 +    val rhs = singleton (Syntax.check_terms ctxt) raw_rhs;
  16.219 +    val SOME var = get_first (fn ((b, _), mx) =>
  16.220 +      if Binding.base_name b = fname then SOME (b, mx) else NONE) fixes;
  16.221 +  in
  16.222 +    ((var, ((Binding.name def_name, []), rhs)),
  16.223 +     subst_bounds (rev (map Free frees), strip_abs_body rhs))
  16.224 +  end;
  16.225  
  16.226  
  16.227  (* find datatypes which contain all datatypes in tnames' *)
  16.228 @@ -227,27 +234,36 @@
  16.229  
  16.230  local
  16.231  
  16.232 -fun gen_primrec_i note def alt_name invs fctxt eqns_atts thy =
  16.233 +fun prepare_spec prep_spec ctxt raw_fixes raw_spec =
  16.234 +  let
  16.235 +    val ((fixes, spec), _) = prep_spec
  16.236 +      raw_fixes (map (single o apsnd single) raw_spec) ctxt
  16.237 +  in (fixes, map (apsnd the_single) spec) end;
  16.238 +
  16.239 +fun gen_primrec set_group prep_spec prep_term invs fctxt raw_fixes raw_params raw_spec lthy =
  16.240    let
  16.241 -    val (raw_eqns, atts) = split_list eqns_atts;
  16.242 -    val eqns = map (apfst Binding.base_name) raw_eqns;
  16.243 -    val dt_info = NominalPackage.get_nominal_datatypes thy;
  16.244 -    val rec_eqns = fold_rev (process_eqn thy o snd) eqns [];
  16.245 +    val (fixes', spec) = prepare_spec prep_spec lthy (raw_fixes @ raw_params) raw_spec;
  16.246 +    val fixes = List.take (fixes', length raw_fixes);
  16.247 +    val (names_atts, spec') = split_list spec;
  16.248 +    val eqns' = map unquantify spec'
  16.249 +    val eqns = fold_rev (process_eqn lthy (fn v => Variable.is_fixed lthy v
  16.250 +      orelse exists (fn ((w, _), _) => v = Binding.base_name w) fixes)) spec' [];
  16.251 +    val dt_info = NominalPackage.get_nominal_datatypes (ProofContext.theory_of lthy);
  16.252      val lsrs :: lsrss = maps (fn (_, (_, _, eqns)) =>
  16.253 -      map (fn (_, (ls, _, rs, _, _)) => ls @ rs) eqns) rec_eqns
  16.254 +      map (fn (_, (ls, _, rs, _, _)) => ls @ rs) eqns) eqns
  16.255      val _ =
  16.256        (if forall (curry eq_set lsrs) lsrss andalso forall
  16.257           (fn (_, (_, _, (_, (ls, _, rs, _, _)) :: eqns)) =>
  16.258                 forall (fn (_, (ls', _, rs', _, _)) =>
  16.259                   ls = ls' andalso rs = rs') eqns
  16.260 -           | _ => true) rec_eqns
  16.261 +           | _ => true) eqns
  16.262         then () else primrec_err param_err);
  16.263 -    val tnames = distinct (op =) (map (#1 o snd) rec_eqns);
  16.264 +    val tnames = distinct (op =) (map (#1 o snd) eqns);
  16.265      val dts = find_dts dt_info tnames tnames;
  16.266      val main_fns = 
  16.267        map (fn (tname, {index, ...}) =>
  16.268          (index, 
  16.269 -          (fst o the o find_first (fn f => (#1 o snd) f = tname)) rec_eqns))
  16.270 +          (fst o the o find_first (fn (_, x) => #1 x = tname)) eqns))
  16.271        dts;
  16.272      val {descr, rec_names, rec_rewrites, ...} = 
  16.273        if null dts then
  16.274 @@ -256,32 +272,32 @@
  16.275      val descr = map (fn (i, (tname, args, constrs)) => (i, (tname, args,
  16.276        map (fn (cname, cargs) => (cname, fold (fn (dTs, dT) => fn dTs' =>
  16.277          dTs' @ dTs @ [dT]) cargs [])) constrs))) descr;
  16.278 -    val (fnameTs, fnss) =
  16.279 -      fold_rev (process_fun thy descr rec_eqns) main_fns ([], []);
  16.280 +    val (fnames, fnss) = fold_rev (process_fun lthy descr eqns) main_fns ([], []);
  16.281      val (fs, defs) = fold_rev (get_fns fnss) (descr ~~ rec_names) ([], []);
  16.282 -    val defs' = map (make_def thy fs) defs;
  16.283 -    val nameTs1 = map snd fnameTs;
  16.284 -    val nameTs2 = map fst rec_eqns;
  16.285 -    val _ = if gen_eq_set (op =) (nameTs1, nameTs2) then ()
  16.286 -            else primrec_err ("functions " ^ commas_quote (map fst nameTs2) ^
  16.287 -              "\nare not mutually recursive");
  16.288 -    val primrec_name =
  16.289 -      if alt_name = "" then (space_implode "_" (map (Sign.base_name o #1) defs)) else alt_name;
  16.290 -    val (defs_thms', thy') =
  16.291 -      thy
  16.292 -      |> Sign.add_path primrec_name
  16.293 -      |> fold_map def (map (fn ((name, t), _) => ((name, []), t)) defs');
  16.294 -    val cert = cterm_of thy';
  16.295 +    val defs' = map (make_def lthy fixes fs) defs;
  16.296 +    val names1 = map snd fnames;
  16.297 +    val names2 = map fst eqns;
  16.298 +    val _ = if gen_eq_set (op =) (names1, names2) then ()
  16.299 +      else primrec_err ("functions " ^ commas_quote names2 ^
  16.300 +        "\nare not mutually recursive");
  16.301 +    val (defs_thms, lthy') = lthy |>
  16.302 +      set_group ? LocalTheory.set_group (serial_string ()) |>
  16.303 +      fold_map (apfst (snd o snd) oo
  16.304 +        LocalTheory.define Thm.definitionK o fst) defs';
  16.305 +    val qualify = Binding.qualify
  16.306 +      (space_implode "_" (map (Sign.base_name o #1) defs));
  16.307 +    val names_atts' = map (apfst qualify) names_atts;
  16.308 +    val cert = cterm_of (ProofContext.theory_of lthy');
  16.309  
  16.310      fun mk_idx eq =
  16.311        let
  16.312 -        val Const c = head_of (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop
  16.313 +        val Free (name, _) = head_of (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop
  16.314            (Logic.strip_imp_concl eq))));
  16.315 -        val SOME i = AList.lookup op = (map swap fnameTs) c;
  16.316 +        val SOME i = AList.lookup op = (map swap fnames) name;
  16.317          val SOME (_, _, constrs) = AList.lookup op = descr i;
  16.318 -        val SOME (_, _, eqns) = AList.lookup op = rec_eqns c;
  16.319 +        val SOME (_, _, eqns'') = AList.lookup op = eqns name;
  16.320          val SOME (cname, (_, cargs, _, _, _)) = find_first
  16.321 -          (fn (_, (_, _, _, _, eq')) => eq = eq') eqns
  16.322 +          (fn (_, (_, _, _, _, eq')) => eq = eq') eqns''
  16.323        in (i, find_index (fn (cname', _) => cname = cname') constrs, cargs) end;
  16.324  
  16.325      val rec_rewritess =
  16.326 @@ -296,19 +312,15 @@
  16.327        curry (List.take o swap) (length fvars) |> map cert;
  16.328      val invs' = (case invs of
  16.329          NONE => map (fn (i, _) =>
  16.330 -          let
  16.331 -            val SOME (_, T) = AList.lookup op = fnameTs i
  16.332 -            val (Ts, U) = strip_type T
  16.333 -          in
  16.334 -            Abs ("x", List.drop (Ts, length lsrs + 1) ---> U, HOLogic.true_const)
  16.335 -          end) descr
  16.336 -      | SOME invs' => invs');
  16.337 +          Abs ("x", fastype_of (snd (nth defs' i)), HOLogic.true_const)) descr
  16.338 +      | SOME invs' => map (prep_term lthy') invs');
  16.339      val inst = (map cert fvars ~~ cfs) @
  16.340        (map (cert o Var) pvars ~~ map cert invs') @
  16.341        (case ctxtvars of
  16.342 -         [ctxtvar] => [(cert (Var ctxtvar), cert (the_default HOLogic.unit fctxt))]
  16.343 +         [ctxtvar] => [(cert (Var ctxtvar),
  16.344 +           cert (the_default HOLogic.unit (Option.map (prep_term lthy') fctxt)))]
  16.345         | _ => []);
  16.346 -    val rec_rewrites' = map (fn (_, eq) =>
  16.347 +    val rec_rewrites' = map (fn eq =>
  16.348        let
  16.349          val (i, j, cargs) = mk_idx eq
  16.350          val th = nth (nth rec_rewritess i) j;
  16.351 @@ -317,8 +329,8 @@
  16.352            strip_comb |> snd
  16.353        in (cargs, Logic.strip_imp_prems eq,
  16.354          Drule.cterm_instantiate (inst @
  16.355 -          (map (cterm_of thy') cargs' ~~ map (cterm_of thy' o Free) cargs)) th)
  16.356 -      end) eqns;
  16.357 +          (map cert cargs' ~~ map (cert o Free) cargs)) th)
  16.358 +      end) eqns';
  16.359  
  16.360      val prems = foldr1 (common_prefix op aconv) (map (prems_of o #3) rec_rewrites');
  16.361      val cprems = map cert prems;
  16.362 @@ -346,64 +358,37 @@
  16.363      val rule = implies_intr_list rule_prems
  16.364        (Conjunction.intr_balanced (map mk_eqn (rec_rewrites' ~~ asmss)));
  16.365  
  16.366 -    val goals = map (fn ((cargs, _, _), (_, eqn)) =>
  16.367 -      (list_all_free (cargs, eqn), [])) (rec_rewrites' ~~ eqns);
  16.368 +    val goals = map (fn ((cargs, _, _), eqn) =>
  16.369 +      (list_all_free (cargs, eqn), [])) (rec_rewrites' ~~ eqns');
  16.370  
  16.371    in
  16.372 -    thy' |>
  16.373 -    ProofContext.init |>
  16.374 +    lthy' |>
  16.375 +    Variable.add_fixes (map fst lsrs) |> snd |>
  16.376      Proof.theorem_i NONE
  16.377 -      (fn thss => ProofContext.theory (fn thy =>
  16.378 +      (fn thss => fn goal_ctxt =>
  16.379           let
  16.380 -           val simps = map standard (flat thss);
  16.381 -           val (simps', thy') =
  16.382 -             fold_map note ((map fst eqns ~~ atts) ~~ map single simps) thy;
  16.383 -           val simps'' = maps snd simps'
  16.384 +           val simps = ProofContext.export goal_ctxt lthy' (flat thss);
  16.385 +           val (simps', lthy'') = fold_map (LocalTheory.note Thm.theoremK)
  16.386 +             (names_atts' ~~ map single simps) lthy'
  16.387           in
  16.388 -           thy'
  16.389 -           |> note (("simps", [Simplifier.simp_add]), simps'')
  16.390 +           lthy''
  16.391 +           |> LocalTheory.note Thm.theoremK ((qualify (Binding.name "simps"),
  16.392 +             [Attrib.internal (K Simplifier.simp_add)]), maps snd simps')
  16.393             |> snd
  16.394 -           |> Sign.parent_path
  16.395 -         end))
  16.396 +         end)
  16.397        [goals] |>
  16.398      Proof.apply (Method.Basic (fn _ => Method.RAW_METHOD (fn _ =>
  16.399 -      rewrite_goals_tac (map snd defs_thms') THEN
  16.400 +      rewrite_goals_tac defs_thms THEN
  16.401        compose_tac (false, rule, length rule_prems) 1), Position.none)) |>
  16.402      Seq.hd
  16.403    end;
  16.404  
  16.405 -fun gen_primrec note def alt_name invs fctxt eqns thy =
  16.406 -  let
  16.407 -    val ((names, strings), srcss) = apfst split_list (split_list eqns);
  16.408 -    val atts = map (map (Attrib.attribute thy)) srcss;
  16.409 -    val eqn_ts = map (fn s => Syntax.read_prop_global thy s
  16.410 -      handle ERROR msg => cat_error msg ("The error(s) above occurred for " ^ s)) strings;
  16.411 -    val rec_ts = map (fn eq => head_of (fst (HOLogic.dest_eq
  16.412 -      (HOLogic.dest_Trueprop (Logic.strip_imp_concl eq))))
  16.413 -      handle TERM _ => primrec_eq_err thy "not a proper equation" eq) eqn_ts;
  16.414 -    val (_, eqn_ts') = OldPrimrecPackage.unify_consts thy rec_ts eqn_ts
  16.415 -  in
  16.416 -    gen_primrec_i note def alt_name
  16.417 -      (Option.map (map (Syntax.read_term_global thy)) invs)
  16.418 -      (Option.map (Syntax.read_term_global thy) fctxt)
  16.419 -      (names ~~ eqn_ts' ~~ atts) thy
  16.420 -  end;
  16.421 -
  16.422 -fun thy_note ((name, atts), thms) =
  16.423 -  PureThy.add_thmss [((name, thms), atts)] #-> (fn [thms] => pair (name, thms));
  16.424 -fun thy_def false ((name, atts), t) =
  16.425 -      PureThy.add_defs false [((name, t), atts)] #-> (fn [thm] => pair (name, thm))
  16.426 -  | thy_def true ((name, atts), t) =
  16.427 -      PureThy.add_defs_unchecked false [((name, t), atts)] #-> (fn [thm] => pair (name, thm));
  16.428 -
  16.429  in
  16.430  
  16.431 -val add_primrec = gen_primrec thy_note (thy_def false);
  16.432 -val add_primrec_unchecked = gen_primrec thy_note (thy_def true);
  16.433 -val add_primrec_i = gen_primrec_i thy_note (thy_def false);
  16.434 -val add_primrec_unchecked_i = gen_primrec_i thy_note (thy_def true);
  16.435 +val add_primrec = gen_primrec false Specification.check_specification (K I);
  16.436 +val add_primrec_cmd = gen_primrec true Specification.read_specification Syntax.read_term;
  16.437  
  16.438 -end; (*local*)
  16.439 +end;
  16.440  
  16.441  
  16.442  (* outer syntax *)
  16.443 @@ -419,25 +404,26 @@
  16.444  val parser2 = (invariant -- P.$$$ ":") |--
  16.445      (Scan.repeat1 (unless_flag P.term) >> SOME) -- Scan.optional parser1 NONE ||
  16.446    (parser1 >> pair NONE);
  16.447 -val parser3 =
  16.448 -  unless_flag P.name -- Scan.optional parser2 (NONE, NONE) ||
  16.449 -  (parser2 >> pair "");
  16.450 -val parser4 =
  16.451 -  (P.$$$ "unchecked" >> K true) -- Scan.optional parser3 ("", (NONE, NONE)) ||
  16.452 -  (parser3 >> pair false);
  16.453  val options =
  16.454    Scan.optional (P.$$$ "(" |-- P.!!!
  16.455 -    (parser4 --| P.$$$ ")")) (false, ("", (NONE, NONE)));
  16.456 +    (parser2 --| P.$$$ ")")) (NONE, NONE);
  16.457 +
  16.458 +fun pipe_error t = P.!!! (Scan.fail_with (K
  16.459 +  (cat_lines ["Equations must be separated by " ^ quote "|", quote t])));
  16.460  
  16.461 -val primrec_decl =
  16.462 -  options -- Scan.repeat1 (SpecParse.opt_thm_name ":" -- P.prop);
  16.463 +val statement = SpecParse.opt_thm_name ":" -- P.prop --| Scan.ahead
  16.464 +  ((P.term :-- pipe_error) || Scan.succeed ("",""));
  16.465 +
  16.466 +val statements = P.enum1 "|" statement;
  16.467 +
  16.468 +val primrec_decl = P.opt_target -- options --
  16.469 +  P.fixes -- P.for_fixes --| P.$$$ "where" -- statements;
  16.470  
  16.471  val _ =
  16.472    OuterSyntax.command "nominal_primrec" "define primitive recursive functions on nominal datatypes" K.thy_goal
  16.473 -    (primrec_decl >> (fn ((unchecked, (alt_name, (invs, fctxt))), eqns) =>
  16.474 -      Toplevel.print o Toplevel.theory_to_proof
  16.475 -        ((if unchecked then add_primrec_unchecked else add_primrec) alt_name invs fctxt
  16.476 -          (map P.triple_swap eqns))));
  16.477 +    (primrec_decl >> (fn ((((opt_target, (invs, fctxt)), raw_fixes), raw_params), raw_spec) =>
  16.478 +      Toplevel.print o Toplevel.local_theory_to_proof opt_target
  16.479 +        (add_primrec_cmd invs fctxt raw_fixes raw_params raw_spec)));
  16.480  
  16.481  end;
  16.482