--- a/Nominal/Ex/Datatypes.thy	Mon May 09 04:46:43 2011 +0100
+++ b/Nominal/Ex/Datatypes.thy	Mon May 09 04:49:58 2011 +0100
@@ -67,7 +67,29 @@
 thm baz.fv_bn_eqvt
 thm baz.size_eqvt
 thm baz.supp
+
+(*
+  a nominal datatype with a set argument of
+  pure type
+*)
   
+nominal_datatype set_ty = 
+  Set_ty "nat set"
+| Fun "nat \<Rightarrow> nat"
+| Var "name"
+| Lam x::"name" t::"set_ty" bind x in t
+
+thm set_ty.distinct
+thm set_ty.induct
+thm set_ty.exhaust
+thm set_ty.strong_exhaust
+thm set_ty.fv_defs
+thm set_ty.bn_defs
+thm set_ty.perm_simps
+thm set_ty.eq_iff
+thm set_ty.fv_bn_eqvt
+thm set_ty.size_eqvt
+thm set_ty.supp
 
 end
 

--- a/Nominal/Ex/LF.thy	Mon May 09 04:46:43 2011 +0100
+++ b/Nominal/Ex/LF.thy	Mon May 09 04:49:58 2011 +0100
@@ -17,7 +17,22 @@
       Const "ident"
     | Var "name"
     | App "trm" "trm"
-    | Lam "ty" n::"name" t::"trm"  bind n in t
+    | Lam' "ty" n::"name" t::"trm"  bind n in t
+
+abbreviation
+  KPi_syn::"name \<Rightarrow> ty \<Rightarrow> kind \<Rightarrow> kind" ("\<Pi>[_:_]._" [100,100,100] 100)
+where 
+  "\<Pi>[x:A].K \<equiv> KPi A x K"
+
+abbreviation
+  TPi_syn::"name \<Rightarrow> ty \<Rightarrow> ty \<Rightarrow> ty" ("\<Pi>[_:_]._" [100,100,100] 100)
+where 
+  "\<Pi>[x:A1].A2 \<equiv> TPi A1 x A2"
+
+abbreviation
+  Lam_syn::"name \<Rightarrow> ty \<Rightarrow> trm \<Rightarrow> trm" ("Lam [_:_]._" [100,100,100] 100)
+where 
+  "Lam [x:A].M \<equiv> Lam' A x M"
 
 thm lf.distinct
 thm lf.induct
@@ -36,7 +51,110 @@
 thm lf.fresh
 thm lf.fresh[simplified]
 
+nominal_datatype sig_ass =
+    TC_ass "ident" "kind"
+  | C_ass "ident" "ty"
 
+types Sig = "sig_ass list"
+types Ctx = "(name \<times> ty) list"
+types Subst = "(name \<times> trm) list"
+
+inductive
+    sig_valid  :: "Sig \<Rightarrow> bool" ("\<turnstile> _ sig" [60] 60)
+and ctx_valid  :: "Sig \<Rightarrow> Ctx \<Rightarrow> bool" ("_ \<turnstile> _ ctx" [60,60] 60)
+and trm_valid  :: "Sig \<Rightarrow> Ctx \<Rightarrow> trm \<Rightarrow> ty \<Rightarrow> bool" ("_,_ \<turnstile> _ : _" [60,60,60,60] 60)
+and ty_valid   :: "Sig \<Rightarrow> Ctx \<Rightarrow> ty \<Rightarrow> kind \<Rightarrow> bool" ("_,_ \<turnstile> _ : _" [60,60,60,60] 60)
+and kind_valid :: "Sig \<Rightarrow> Ctx \<Rightarrow> kind \<Rightarrow> bool" ("_,_ \<turnstile> _ : Kind" [60,60,60] 60)
+and trm_equiv  :: "Sig \<Rightarrow> Ctx \<Rightarrow> trm \<Rightarrow> trm \<Rightarrow> ty \<Rightarrow> bool" ("_,_ \<turnstile> _ = _ : _" [60,60,60,60,60] 60)
+and ty_equiv   :: "Sig \<Rightarrow> Ctx \<Rightarrow> ty \<Rightarrow> ty \<Rightarrow> kind \<Rightarrow> bool" ("_,_ \<turnstile> _ = _ : _" [60,60,60,60,60] 60)
+and kind_equiv :: "Sig \<Rightarrow> Ctx \<Rightarrow> kind \<Rightarrow> kind \<Rightarrow> bool" ("_,_ \<turnstile> _ = _ : Kind" [60,60,60,60] 60)
+where
+(* Signatures *)
+  s1: "\<turnstile> [] sig"
+| s2: "\<lbrakk>\<turnstile> \<Sigma> sig; \<Sigma>,[] \<turnstile> K : Kind; atom a\<sharp>\<Sigma>\<rbrakk> \<Longrightarrow> \<turnstile> (TC_ass a K)#\<Sigma> sig"
+| s3: "\<lbrakk>\<turnstile> \<Sigma> sig; \<Sigma>,[] \<turnstile> A : Type; atom c\<sharp>\<Sigma>\<rbrakk> \<Longrightarrow> \<turnstile> (C_ass c A)#\<Sigma> sig"
+
+(* Contexts *)
+| c1: "\<turnstile> \<Sigma> sig \<Longrightarrow> \<Sigma> \<turnstile> [] ctx"
+| c2: "\<lbrakk>\<Sigma> \<turnstile> \<Gamma>  ctx; \<Sigma>,\<Gamma> \<turnstile> A : Type; atom x\<sharp>\<Gamma>\<rbrakk> \<Longrightarrow> \<Sigma> \<turnstile> (x,A)#\<Gamma> ctx"
+
+(* Typing Terms *)
+| t1: "\<lbrakk>\<Sigma> \<turnstile> \<Gamma>  ctx; (x,A) \<in> set \<Gamma>\<rbrakk> \<Longrightarrow> \<Sigma>,\<Gamma> \<turnstile> (Var x) : A"
+| t2: "\<lbrakk>\<Sigma> \<turnstile> \<Gamma>  ctx; C_ass c A \<in> set \<Sigma>\<rbrakk> \<Longrightarrow> \<Sigma>,\<Gamma> \<turnstile> (Const c) : A"
+| t3: "\<lbrakk>\<Sigma>,\<Gamma> \<turnstile> M1 : \<Pi>[x:A2].A1; \<Sigma>,\<Gamma> \<turnstile> M2 : A2; atom x\<sharp>\<Gamma>\<rbrakk> \<Longrightarrow> \<Sigma>,\<Gamma> \<turnstile> (App M1 M2) : A1"
+| t4: "\<lbrakk>\<Sigma>,\<Gamma> \<turnstile> A1 : Type; \<Sigma>,(x,A1)#\<Gamma> \<turnstile> M2 : A2; atom x\<sharp>(\<Gamma>,A1)\<rbrakk> \<Longrightarrow> \<Sigma>,\<Gamma> \<turnstile> (Lam [x:A1].M2) : \<Pi>[x:A1].A2"
+| t5: "\<lbrakk>\<Sigma>,\<Gamma> \<turnstile> M : A; \<Sigma>,\<Gamma> \<turnstile> A = B : Type\<rbrakk> \<Longrightarrow> \<Sigma>,\<Gamma> \<turnstile> M : B "
+
+(* Typing Types *)
+| f1: "\<lbrakk>\<Sigma> \<turnstile> \<Gamma>  ctx; TC_ass a K \<in> set \<Sigma>\<rbrakk> \<Longrightarrow> \<Sigma>,\<Gamma> \<turnstile> (TConst a) : K"
+| f2: "\<lbrakk>\<Sigma>,\<Gamma> \<turnstile> A : \<Pi>[x:B].K; \<Sigma>,\<Gamma> \<turnstile> M : B; atom x\<sharp>\<Gamma>\<rbrakk> \<Longrightarrow> \<Sigma>,\<Gamma> \<turnstile> (TApp A M) : K"
+| f3: "\<lbrakk>\<Sigma>,\<Gamma> \<turnstile> A1 : Type; \<Sigma>,(x,A1)#\<Gamma> \<turnstile> A2 : Type; atom x\<sharp>(\<Gamma>,A1)\<rbrakk> \<Longrightarrow> \<Sigma>,\<Gamma> \<turnstile> (\<Pi>[x:A1].A2) : Type"
+| f4: "\<lbrakk>\<Sigma>,\<Gamma> \<turnstile> A : K; \<Sigma>,\<Gamma> \<turnstile> K = L : Kind\<rbrakk> \<Longrightarrow> \<Sigma>,\<Gamma> \<turnstile> A : L"
+
+(* Typing Kinds *)
+| k1: "\<Sigma> \<turnstile> \<Gamma> ctx \<Longrightarrow> \<Sigma>,\<Gamma> \<turnstile> Type : Kind"
+| k2: "\<lbrakk>\<Sigma>,\<Gamma> \<turnstile> A : Type; \<Sigma>,(x,A)#\<Gamma> \<turnstile> K : Kind; atom x\<sharp>(\<Gamma>,A)\<rbrakk> \<Longrightarrow> \<Sigma>,\<Gamma> \<turnstile> (\<Pi>[x:A].K) : Kind"
+
+(* Simultaneous Congruence for Terms *)
+| q1: "\<lbrakk>\<Sigma> \<turnstile> \<Gamma>  ctx; (x,A) \<in> set \<Gamma>\<rbrakk> \<Longrightarrow> \<Sigma>,\<Gamma> \<turnstile> (Var x) = (Var x) : A"
+| q2: "\<lbrakk>\<Sigma> \<turnstile> \<Gamma>  ctx; C_ass c A \<in> set \<Sigma>\<rbrakk> \<Longrightarrow> \<Sigma>,\<Gamma> \<turnstile> (Const c) = (Const c): A"
+| q3: "\<lbrakk>\<Sigma>,\<Gamma> \<turnstile> M1 = N1 : \<Pi>[x:A2].A1; \<Sigma>,\<Gamma> \<turnstile> M2 = N2 : A2; atom x\<sharp>\<Gamma>\<rbrakk> 
+       \<Longrightarrow> \<Sigma>,\<Gamma> \<turnstile> (App M1 M2) = (App N1 N2) : A1"
+| q4: "\<lbrakk>\<Sigma>,\<Gamma> \<turnstile> A1' = A1 : Type; \<Sigma>,\<Gamma> \<turnstile> A1'' = A1 : Type; \<Sigma>,\<Gamma> \<turnstile> A1 : Type;
+        \<Sigma>,(x,A1)#\<Gamma> \<turnstile> M2 = N2 : A2; atom x\<sharp>\<Gamma>\<rbrakk> \<Longrightarrow> \<Sigma>,\<Gamma> \<turnstile> (Lam [x:A1'].M2) = (Lam [x:A1''].N2) : \<Pi>[x:A1].A2"
+
+(* Extensionality *)
+| ex: "\<lbrakk>\<Sigma>,\<Gamma> \<turnstile> M : \<Pi>[x:A1].A2; \<Sigma>,\<Gamma> \<turnstile> N : \<Pi>[x:A1].A2; \<Sigma>,\<Gamma> \<turnstile> A1 : Type;
+        \<Sigma>,(x,A1)#\<Gamma> \<turnstile> App M (Var x) = App N (Var x) : A2; atom x\<sharp>\<Gamma>\<rbrakk> \<Longrightarrow> \<Sigma>,\<Gamma> \<turnstile> M = N : \<Pi>[x:A1].A2"
+
+(* Parallel Conversion *)
+| pc: "\<lbrakk>\<Sigma>,\<Gamma> \<turnstile> A1 : Type; \<Sigma>,(x,A1)#\<Gamma> \<turnstile> M2 = N2 : A2; \<Sigma>,\<Gamma> \<turnstile> M1 = N1 : A1; atom x\<sharp>\<Gamma>\<rbrakk> 
+       \<Longrightarrow> \<Sigma>,\<Gamma> \<turnstile> App (Lam [x:A1].M2) M1 = N2 : A2"
+
+(* Equivalence *)
+| e1: "\<Sigma>,\<Gamma> \<turnstile> M = N : A \<Longrightarrow> \<Sigma>,\<Gamma> \<turnstile> N = M : (A::ty)"
+| e2: "\<lbrakk>\<Sigma>,\<Gamma> \<turnstile> M = N : A; \<Sigma>,\<Gamma> \<turnstile> N = P : A\<rbrakk> \<Longrightarrow> \<Sigma>,\<Gamma> \<turnstile> M = P : (A::ty)"
+(*| e3: "\<Sigma>,\<Gamma> \<turnstile> M : A \<Longrightarrow> \<Sigma>,\<Gamma> \<turnstile> M = M : (A::ty)"*)
+
+(* Type conversion *)
+| tc: "\<lbrakk>\<Sigma>,\<Gamma> \<turnstile> M = N : A; \<Sigma>,\<Gamma> \<turnstile> A = B : Type\<rbrakk> \<Longrightarrow> \<Sigma>,\<Gamma> \<turnstile> M = N : B"
+
+(* Types Conruence *)
+| ft1: "\<lbrakk>\<Sigma> \<turnstile> \<Gamma>  ctx; TC_ass a K \<in> set \<Sigma>\<rbrakk> \<Longrightarrow> \<Sigma>,\<Gamma> \<turnstile> (TConst a) = (TConst a) : K"
+| ft2: "\<lbrakk>\<Sigma>,\<Gamma> \<turnstile> A = B : \<Pi>[x:C].K; \<Sigma>,\<Gamma> \<turnstile> M = N : C; atom x\<sharp>\<Gamma>\<rbrakk> \<Longrightarrow> \<Sigma>,\<Gamma> \<turnstile> (TApp A M) = (TApp B N) : K"
+| ft3: "\<lbrakk>\<Sigma>,\<Gamma> \<turnstile> A1 = B1 : Type; \<Sigma>,\<Gamma> \<turnstile> A1 : Type; \<Sigma>,(x,A1)#\<Gamma> \<turnstile> A2 = B2 : Type; atom x\<sharp>\<Gamma>\<rbrakk> 
+       \<Longrightarrow> \<Sigma>,\<Gamma> \<turnstile> \<Pi>[x:A1].A2 = \<Pi>[x:B1].B2 : Type"
+
+(* Types Equivalence *)
+| fe1: "\<Sigma>,\<Gamma> \<turnstile> A = (B::ty) : (K::kind) \<Longrightarrow> \<Sigma>,\<Gamma> \<turnstile> B = A : K"
+| fe2: "\<lbrakk>\<Sigma>,\<Gamma> \<turnstile> A = B : K; \<Sigma>,\<Gamma> \<turnstile> B = C : K\<rbrakk> \<Longrightarrow> \<Sigma>,\<Gamma> \<turnstile> A = C : (K::kind)"
+(*| fe3: "\<Sigma>,\<Gamma> \<turnstile> A : K \<Longrightarrow> \<Sigma>,\<Gamma> \<turnstile> A = A : (K::kind)"*)
+
+(* Kind Conversion *)
+| kc: "\<lbrakk>\<Sigma>,\<Gamma> \<turnstile> A = B : K; \<Sigma>,\<Gamma> \<turnstile> K = L : Kind\<rbrakk> \<Longrightarrow> \<Sigma>,\<Gamma> \<turnstile> A = B : (L::kind)"
+
+(* Kind Congruence *)
+| kc1: "\<Sigma> \<turnstile> \<Gamma> ctx \<Longrightarrow> \<Sigma>,\<Gamma> \<turnstile> Type = Type : Kind"
+| kc2: "\<lbrakk>\<Sigma>,\<Gamma> \<turnstile> A = B : Type; \<Sigma>,\<Gamma> \<turnstile> A : Type; \<Sigma>,(x,A)#\<Gamma> \<turnstile> K = L : Kind; atom x\<sharp>\<Gamma>\<rbrakk> 
+        \<Longrightarrow> \<Sigma>,\<Gamma> \<turnstile> \<Pi>[x:A].K = \<Pi>[x:B].L : Kind"
+
+(* Kind Equivalence *)
+| ke1: "\<Sigma>,\<Gamma> \<turnstile> K = L : Kind \<Longrightarrow> \<Sigma>,\<Gamma> \<turnstile> L = K : Kind"
+| ke2: "\<lbrakk>\<Sigma>,\<Gamma> \<turnstile> K = L : Kind; \<Sigma>,\<Gamma> \<turnstile> L = L' : Kind\<rbrakk> \<Longrightarrow> \<Sigma>,\<Gamma> \<turnstile> K = L' : Kind"
+(*| ke3: "\<Sigma>,\<Gamma> \<turnstile> K : Kind \<Longrightarrow> \<Sigma>,\<Gamma> \<turnstile> K = K : Kind"*)
+
+(* type extensionality - needed in order to get the soundness theorem through*)
+| tex: "\<lbrakk>\<Sigma>,\<Gamma> \<turnstile> A : \<Pi>[x:C].K; \<Sigma>,\<Gamma> \<turnstile> B : \<Pi>[x:C].K; \<Sigma>,\<Gamma> \<turnstile> C : Type; 
+         \<Sigma>,(x,C)#\<Gamma> \<turnstile> TApp A (Var x) = TApp B (Var x) : K; atom x\<sharp>\<Gamma>\<rbrakk> \<Longrightarrow> \<Sigma>,\<Gamma> \<turnstile> A = B : \<Pi>[x:C].K"
+
+thm sig_valid_ctx_valid_trm_valid_ty_valid_kind_valid_trm_equiv_ty_equiv_kind_equiv_def
+thm sig_valid_def
+thm trm_valid_def
+thm ty_valid_def
+thm kind_valid_def
+thm trm_equiv_def
+thm kind_equiv_def
+thm ty_equiv_def
 
 end
 

--- a/Nominal/Ex/Lambda.thy	Mon May 09 04:46:43 2011 +0100
+++ b/Nominal/Ex/Lambda.thy	Mon May 09 04:49:58 2011 +0100
@@ -2,6 +2,23 @@
 imports "../Nominal2" 
 begin
 
+inductive
+  even :: "nat \<Rightarrow> bool" and
+  odd  :: "nat \<Rightarrow> bool"
+where
+  "even 0"
+| "odd n \<Longrightarrow> even (Suc n)"
+| "even n \<Longrightarrow> odd (Suc n)"
+
+thm even_odd_def
+
+lemma
+  shows "p \<bullet> (even n) = even (p \<bullet> n)"
+unfolding even_def
+unfolding even_odd_def
+apply(perm_simp)
+apply(rule refl)
+done
 
 atom_decl name
 
@@ -10,10 +27,26 @@
 | App "lam" "lam"
 | Lam x::"name" l::"lam"  bind x in l ("Lam [_]. _" [100, 100] 100)
 
+
 inductive 
   triv :: "lam \<Rightarrow> nat \<Rightarrow> bool"
 where
   Var: "triv (Var x) n"
+| App: "\<lbrakk>triv t1 n; triv t2 n\<rbrakk> \<Longrightarrow> triv (App t1 t2) n"
+
+lemma 
+  "p \<bullet> (triv t x) = triv (p \<bullet> t) (p \<bullet> x)"
+unfolding triv_def
+apply(perm_simp)
+apply(rule refl)
+oops
+(*apply(perm_simp)*)
+
+ML {*
+  Inductive.the_inductive @{context} "Lambda.triv"
+*}
+
+thm triv_def
 
 equivariance triv
 nominal_inductive triv avoids Var: "{}::name set"

--- a/Nominal/Nominal2_Base.thy	Mon May 09 04:46:43 2011 +0100
+++ b/Nominal/Nominal2_Base.thy	Mon May 09 04:49:58 2011 +0100
@@ -789,7 +789,6 @@
   unfolding permute_perm_def
   by (simp add: diff_minus minus_add add_assoc)
 
-
 subsubsection {* Equivariance of Logical Operators *}
 
 lemma eq_eqvt [eqvt]:
@@ -950,6 +949,12 @@
   unfolding Union_eq 
   by (perm_simp) (rule refl)
 
+lemma Inter_eqvt [eqvt]:
+  shows "p \<bullet> (\<Inter> S) = \<Inter> (p \<bullet> S)"
+  unfolding Inter_eq 
+  by (perm_simp) (rule refl)
+
+
 (* FIXME: eqvt attribute *)
 lemma Sigma_eqvt:
   shows "(p \<bullet> (X \<times> Y)) = (p \<bullet> X) \<times> (p \<bullet> Y)"
@@ -957,9 +962,78 @@
 unfolding UNION_eq_Union_image
 by (perm_simp) (rule refl)
 
+text {* 
+  In order to prove that lfp is equivariant we need two
+  auxiliary classes which specify that (op <=) and
+  Inf are equivariant. Instances for bool and fun are 
+  given.
+*}
+
+class le_eqvt =  order + 
+  assumes le_eqvt [eqvt]: "p \<bullet> (x \<le> y) = ((p \<bullet> x) \<le> (p \<bullet> (y::('a::{pt, order}))))"
+
+class inf_eqvt = complete_lattice +
+  assumes inf_eqvt [eqvt]: "p \<bullet> (Inf X) = Inf (p \<bullet> (X::('a::{pt, Inf}) set))"
+
+instantiation bool :: le_eqvt
+begin
+
+instance 
+apply(default)
+unfolding le_bool_def
+apply(perm_simp)
+apply(rule refl)
+done
+
+end
+
+instantiation "fun" :: (pt, le_eqvt) le_eqvt
+begin
+
+instance 
+apply(default)
+unfolding le_fun_def
+apply(perm_simp)
+apply(rule refl)
+done 
+
+end
+
+instantiation bool :: inf_eqvt
+begin
+
+instance 
+apply(default)
+unfolding Inf_bool_def
+apply(perm_simp)
+apply(rule refl)
+done
+
+end
+
+instantiation "fun" :: (pt, inf_eqvt) inf_eqvt
+begin
+
+instance 
+apply(default)
+unfolding Inf_fun_def
+apply(perm_simp)
+apply(rule refl)
+done 
+
+end
+
+lemma lfp_eqvt [eqvt]:
+  fixes F::"('a \<Rightarrow> 'b) \<Rightarrow> ('a::pt \<Rightarrow> 'b::{inf_eqvt, le_eqvt})"
+  shows "p \<bullet> (lfp F) = lfp (p \<bullet> F)"
+unfolding lfp_def
+by (perm_simp) (rule refl)
+
 lemma finite_eqvt [eqvt]:
   shows "p \<bullet> finite A = finite (p \<bullet> A)"
-  unfolding permute_finite permute_bool_def ..
+unfolding finite_def
+by (perm_simp) (rule refl)
+
 
 subsubsection {* Equivariance for product operations *}
 

--- a/Nominal/nominal_eqvt.ML	Mon May 09 04:46:43 2011 +0100
+++ b/Nominal/nominal_eqvt.ML	Mon May 09 04:49:58 2011 +0100
@@ -8,9 +8,6 @@
 
 signature NOMINAL_EQVT =
 sig
-  val eqvt_rel_tac: Proof.context -> string list -> term -> thm -> thm list -> int -> tactic
-  val eqvt_rel_single_case_tac: Proof.context -> string list -> term -> thm -> int -> tactic
-  
   val raw_equivariance: bool -> term list -> thm -> thm list -> Proof.context -> thm list * local_theory
   val equivariance: string -> Proof.context -> (thm list * local_theory)
   val equivariance_cmd: string -> Proof.context -> local_theory