--- a/Nominal/Ex/Ex1rec.thy	Sun May 09 11:43:24 2010 +0100
+++ b/Nominal/Ex/Ex1rec.thy	Sun May 09 12:26:10 2010 +0100
@@ -29,10 +29,11 @@
 ML {* Sign.of_sort @{theory} (@{typ lam}, @{sort fs}) *}
 thm lam_bp.fv[simplified lam_bp.supp(1-2)]
 
-(*declare permute_lam_raw_permute_bp_raw.simps[eqvt]
+declare permute_lam_raw_permute_bp_raw.simps[eqvt]
 declare alpha_gen_eqvt[eqvt]
+
 equivariance alpha_lam_raw
-*)
+
 
 end
 

--- a/Nominal/Ex/Ex2.thy	Sun May 09 11:43:24 2010 +0100
+++ b/Nominal/Ex/Ex2.thy	Sun May 09 12:26:10 2010 +0100
@@ -27,6 +27,12 @@
 thm trm_pat.distinct
 thm trm_pat.fv[simplified trm_pat.supp(1-2)]
 
+declare permute_trm_raw_permute_pat_raw.simps[eqvt]
+declare alpha_gen_eqvt[eqvt]
+
+equivariance alpha_trm_raw
+
+
 end
 
 

--- a/Nominal/Ex/Ex3.thy	Sun May 09 11:43:24 2010 +0100
+++ b/Nominal/Ex/Ex3.thy	Sun May 09 12:26:10 2010 +0100
@@ -30,6 +30,13 @@
 thm trm_pat.distinct
 thm trm_pat.fv[simplified trm_pat.supp(1-2)]
 
+
+declare permute_trm_raw_permute_pat_raw.simps[eqvt]
+declare alpha_gen_eqvt[eqvt]
+
+equivariance alpha_trm_raw
+
+
 end
 
 

--- a/Nominal/Ex/ExLF.thy	Sun May 09 11:43:24 2010 +0100
+++ b/Nominal/Ex/ExLF.thy	Sun May 09 12:26:10 2010 +0100
@@ -20,6 +20,14 @@
 
 thm kind_ty_trm.supp
 
+declare permute_kind_raw_permute_ty_raw_permute_trm_raw.simps[eqvt]
+declare alpha_gen_eqvt[eqvt]
+
+equivariance alpha_trm_raw
+
+
+
+
 end
 
 

--- a/Nominal/Ex/ExLeroy.thy	Sun May 09 11:43:24 2010 +0100
+++ b/Nominal/Ex/ExLeroy.thy	Sun May 09 12:26:10 2010 +0100
@@ -16,10 +16,10 @@
   Empty
 | Seq c::defn d::"body"     bind_set "cbinders c" in d
 and defn =
-  Type "name" "tyty"
+  Type "name" "ty"
 | Dty "name"
 | DStru "name" "mexp"
-| Val "name" "trmtrm"
+| Val "name" "trm"
 and sexp =
   Sig sbody
 | SFunc "name" "sexp" "sexp"
@@ -28,22 +28,22 @@
 | SSeq C::spec D::sbody    bind_set "Cbinders C" in D
 and spec =
   Type1 "name"
-| Type2 "name" "tyty"
+| Type2 "name" "ty"
 | SStru "name" "sexp"
-| SVal "name" "tyty"
-and tyty =
+| SVal "name" "ty"
+and ty =
   Tyref1 "name"
-| Tyref2 "path" "tyty"
-| Fun "tyty" "tyty"
+| Tyref2 "path" "ty"
+| Fun "ty" "ty"
 and path =
   Sref1 "name"
 | Sref2 "path" "name"
-and trmtrm =
+and trm =
   Tref1 "name"
 | Tref2 "path" "name"
-| Lam' v::"name" "tyty" M::"trmtrm"  bind_set v in M
-| App' "trmtrm" "trmtrm"
-| Let' "body" "trmtrm"
+| Lam' v::"name" "ty" M::"trm"  bind_set v in M
+| App' "trm" "trm"
+| Let' "body" "trm"
 binder
     cbinders :: "defn \<Rightarrow> atom set"
 and Cbinders :: "spec \<Rightarrow> atom set"
@@ -57,15 +57,21 @@
 | "Cbinders (SStru x S) = {atom x}"
 | "Cbinders (SVal v T) = {atom v}"
 
-thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.fv
-thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.eq_iff
-thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.bn
-thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.perm
-thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.induct
-thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.inducts
-thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.distinct
-thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.supp(1-3,5-7,9-10)
-thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.fv[simplified mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.supp(1-3,5-7,9-10)]
+thm mexp_body_defn_sexp_sbody_spec_ty_path_trm.fv
+thm mexp_body_defn_sexp_sbody_spec_ty_path_trm.eq_iff
+thm mexp_body_defn_sexp_sbody_spec_ty_path_trm.bn
+thm mexp_body_defn_sexp_sbody_spec_ty_path_trm.perm
+thm mexp_body_defn_sexp_sbody_spec_ty_path_trm.induct
+thm mexp_body_defn_sexp_sbody_spec_ty_path_trm.inducts
+thm mexp_body_defn_sexp_sbody_spec_ty_path_trm.distinct
+thm mexp_body_defn_sexp_sbody_spec_ty_path_trm.supp(1-3,5-7,9-10)
+thm mexp_body_defn_sexp_sbody_spec_ty_path_trm.fv[simplified mexp_body_defn_sexp_sbody_spec_ty_path_trm.supp(1-3,5-7,9-10)]
+
+declare permute_mexp_raw_permute_body_raw_permute_defn_raw_permute_sexp_raw_permute_sbody_raw_permute_spec_raw_permute_ty_raw_permute_path_raw_permute_trm_raw.simps[eqvt]
+declare alpha_gen_eqvt[eqvt]
+
+equivariance alpha_trm_raw
+
 
 end
 

--- a/Nominal/Ex/ExLet.thy	Sun May 09 11:43:24 2010 +0100
+++ b/Nominal/Ex/ExLet.thy	Sun May 09 12:26:10 2010 +0100
@@ -35,6 +35,13 @@
 thm trm_lts.fv[simplified trm_lts.supp(1-2)]
 
 
+declare permute_trm_raw_permute_lts_raw.simps[eqvt]
+declare alpha_gen_eqvt[eqvt]
+
+equivariance alpha_trm_raw
+
+
+
 primrec
   permute_bn_raw
 where
@@ -95,14 +102,14 @@
   apply (rule_tac x="q" in exI)
   apply (simp add: alphas)
   apply (simp add: perm_bn[symmetric])
-  apply (simp add: eqvts[symmetric])
-  apply (simp add: supp_abs)
+  apply(rule conjI)
+  apply(drule supp_perm_eq)
+  apply(simp add: abs_eq_iff)
+  apply(simp add: alphas_abs alphas)
+  apply(drule conjunct1)
   apply (simp add: trm_lts.supp)
-  apply (rule supp_perm_eq[symmetric])
-  apply (subst supp_finite_atom_set)
-  apply (rule finite_Diff)
-  apply (simp add: finite_supp)
-  apply (assumption)
+  apply(simp add: supp_abs)
+  apply (simp add: trm_lts.supp)
   done
 
 

--- a/Nominal/Ex/ExLetMult.thy	Sun May 09 11:43:24 2010 +0100
+++ b/Nominal/Ex/ExLetMult.thy	Sun May 09 12:26:10 2010 +0100
@@ -22,6 +22,12 @@
 thm trm_lts.induct
 thm trm_lts.fv[simplified trm_lts.supp]
 
+declare permute_trm_raw_permute_lts_raw.simps[eqvt]
+declare alpha_gen_eqvt[eqvt]
+
+equivariance alpha_trm_raw
+
+
 end
 
 

--- a/Nominal/Ex/ExLetRec.thy	Sun May 09 11:43:24 2010 +0100
+++ b/Nominal/Ex/ExLetRec.thy	Sun May 09 12:26:10 2010 +0100
@@ -30,6 +30,11 @@
 thm trm_lts.supp
 thm trm_lts.fv[simplified trm_lts.supp]
 
+declare permute_trm_raw_permute_lts_raw.simps[eqvt]
+declare alpha_gen_eqvt[eqvt]
+
+equivariance alpha_trm_raw
+
 (* why is this not in HOL simpset? *)
 lemma set_sub: "{a, b} - {b} = {a} - {b}"
 by auto

--- a/Nominal/Ex/ExNotRsp.thy	Sun May 09 11:43:24 2010 +0100
+++ b/Nominal/Ex/ExNotRsp.thy	Sun May 09 12:26:10 2010 +0100
@@ -1,46 +1,52 @@
 theory ExNotRsp
-imports "../Parser"
+imports "../NewParser"
 begin
 
 atom_decl name
 
-(* example 6 from Terms.thy *)
-
-nominal_datatype trm6 =
-  Vr6 "name"
-| Lm6 x::"name" t::"trm6"         bind x in t
-| Lt6 left::"trm6" right::"trm6"  bind "bv6 left" in right
+(* this example binds bound names and
+   so is not respectful *)
+(*
+nominal_datatype trm =
+  Vr "name"
+| Lm x::"name" t::"trm"         bind x in t
+| Lt left::"trm" right::"trm"   bind "bv left" in right
 binder
-  bv6
+  bv
 where
-  "bv6 (Vr6 n) = {}"
-| "bv6 (Lm6 n t) = {atom n} \<union> bv6 t"
-| "bv6 (Lt6 l r) = bv6 l \<union> bv6 r"
-
-(* example 7 from Terms.thy *)
-nominal_datatype trm7 =
-  Vr7 "name"
-| Lm7 l::"name" r::"trm7"   bind l in r
-| Lt7 l::"trm7" r::"trm7"   bind "bv7 l" in r
-binder
-  bv7
-where
-  "bv7 (Vr7 n) = {atom n}"
-| "bv7 (Lm7 n t) = bv7 t - {atom n}"
-| "bv7 (Lt7 l r) = bv7 l \<union> bv7 r"
+  "bv (Vr n) = {}"
+| "bv (Lm n t) = {atom n} \<union> bv t"
+| "bv (Lt l r) = bv l \<union> bv r"
 *)
 
-(* example 9 from Terms.thy *)
-nominal_datatype lam9 =
-  Var9 "name"
-| Lam9 n::"name" l::"lam9" bind n in l
-and bla9 =
-  Bla9 f::"lam9" s::"lam9" bind "bv9 f" in s
+(* this example uses "-" in the binding function; 
+   at the moment this is unsupported *)
+(*
+nominal_datatype trm' =
+  Vr' "name"
+| Lm' l::"name" r::"trm'"   bind l in r
+| Lt' l::"trm'" r::"trm'"   bind "bv' l" in r
 binder
-  bv9
+  bv'
 where
-  "bv9 (Var9 x) = {}"
-| "bv9 (Lam9 x b) = {atom x}"
+  "bv' (Vr' n) = {atom n}"
+| "bv' (Lm' n t) = bv' t - {atom n}"
+| "bv' (Lt' l r) = bv' l \<union> bv' r"
+*)
+
+(* this example again binds bound names  *)
+(*
+nominal_datatype trm'' =
+  Va'' "name"
+| Lm'' n::"name" l::"trm''" bind n in l
+and bla'' =
+  Bla'' f::"trm''" s::"trm''" bind "bv'' f" in s
+binder
+  bv''
+where
+  "bv'' (Vm'' x) = {}"
+| "bv'' (Lm'' x b) = {atom x}"
+*)
 
 end
 

--- a/Nominal/Ex/ExPS3.thy	Sun May 09 11:43:24 2010 +0100
+++ b/Nominal/Ex/ExPS3.thy	Sun May 09 12:26:10 2010 +0100
@@ -11,29 +11,35 @@
 ML {* val _ = cheat_alpha_bn_rsp := true *}
 
 nominal_datatype exp =
-  VarP "name"
-| AppP "exp" "exp"
-| LamP x::"name" e::"exp" bind_set x in e
-| LetP x::"name" p::"pat3" e1::"exp" e2::"exp" bind_set x in e2, bind_set "bp p" in e1
-and pat3 =
+  Var "name"
+| App "exp" "exp"
+| Lam x::"name" e::"exp" bind_set x in e
+| Let x::"name" p::"pat" e1::"exp" e2::"exp" bind_set x in e2, bind_set "bp p" in e1
+and pat =
   PVar "name"
 | PUnit
-| PPair "pat3" "pat3"
+| PPair "pat" "pat"
 binder
-  bp :: "pat3 \<Rightarrow> atom set"
+  bp :: "pat \<Rightarrow> atom set"
 where
   "bp (PVar x) = {atom x}"
 | "bp (PUnit) = {}"
 | "bp (PPair p1 p2) = bp p1 \<union> bp p2"
 
-thm exp_pat3.fv
-thm exp_pat3.eq_iff
-thm exp_pat3.bn
-thm exp_pat3.perm
-thm exp_pat3.induct
-thm exp_pat3.distinct
-thm exp_pat3.fv
-thm exp_pat3.supp(1-2)
+thm exp_pat.fv
+thm exp_pat.eq_iff
+thm exp_pat.bn
+thm exp_pat.perm
+thm exp_pat.induct
+thm exp_pat.distinct
+thm exp_pat.fv
+thm exp_pat.supp(1-2)
+
+declare permute_exp_raw_permute_pat_raw.simps[eqvt]
+declare alpha_gen_eqvt[eqvt]
+
+equivariance alpha_exp_raw
+
 
 end
 

--- a/Nominal/Ex/ExPS6.thy	Sun May 09 11:43:24 2010 +0100
+++ b/Nominal/Ex/ExPS6.thy	Sun May 09 12:26:10 2010 +0100
@@ -1,37 +1,42 @@
 theory ExPS6
-imports "../Parser"
+imports "../NewParser"
 begin
 
 (* example 6 from Peter Sewell's bestiary *)
 
 atom_decl name
 
-(* The binding structure is too complicated, so equivalence the
-   way we define it is not true *)
+(* Is this binding structure supported - I think not 
+   because e1 occurs twice as body *)
 
-ML {* val _ = recursive := false  *}
-nominal_datatype exp6 =
-  EVar name
-| EPair exp6 exp6
-| ELetRec x::name p::pat6 e1::exp6 e2::exp6 bind x in e1, bind x in e2, bind "bp6 p" in e1
-and pat6 =
-  PVar' name
-| PUnit'
-| PPair' pat6 pat6
+nominal_datatype exp =
+  Var name
+| Pair exp exp
+| LetRec x::name p::pat e1::exp e2::exp  bind x in e1 e2, bind "bp p" in e1
+and pat =
+  PVar name
+| PUnit
+| PPair pat pat
 binder
-  bp6 :: "pat6 \<Rightarrow> atom set"
+  bp :: "pat \<Rightarrow> atom list"
 where
-  "bp6 (PVar' x) = {atom x}"
-| "bp6 (PUnit') = {}"
-| "bp6 (PPair' p1 p2) = bp6 p1 \<union> bp6 p2"
+  "bp (PVar x) = [atom x]"
+| "bp (PUnit) = []"
+| "bp (PPair p1 p2) = bp p1 @ bp p2"
 
-thm exp6_pat6.fv
-thm exp6_pat6.eq_iff
-thm exp6_pat6.bn
-thm exp6_pat6.perm
-thm exp6_pat6.induct
-thm exp6_pat6.distinct
-thm exp6_pat6.supp
+thm exp_pat.fv
+thm exp_pat.eq_iff
+thm exp_pat.bn
+thm exp_pat.perm
+thm exp_pat.induct
+thm exp_pat.distinct
+thm exp_pat.supp
+
+declare permute_exp_raw_permute_pat_raw.simps[eqvt]
+declare alpha_gen_eqvt[eqvt]
+
+equivariance alpha_exp_raw
+
 
 end
 

--- a/Nominal/Ex/ExPS7.thy	Sun May 09 11:43:24 2010 +0100
+++ b/Nominal/Ex/ExPS7.thy	Sun May 09 12:26:10 2010 +0100
@@ -1,3 +1,4 @@
+
 theory ExPS7
 imports "../NewParser"
 begin
@@ -6,25 +7,31 @@
 
 atom_decl name
 
-nominal_datatype exp7 =
-  EVar name
-| EUnit
-| EPair exp7 exp7
-| ELetRec l::"lrbs" e::"exp7" bind_set "b7s l" in l e
+nominal_datatype exp =
+  Var name
+| Unit
+| Pair exp exp
+| LetRec l::"lrbs" e::"exp"  bind_set "bs l" in l e
 and lrb =
-  Assign name exp7
+  Assign name exp
 and lrbs =
   Single lrb
 | More lrb lrbs
 binder
-  b7 :: "lrb \<Rightarrow> atom set" and
-  b7s :: "lrbs \<Rightarrow> atom set"
+  b :: "lrb \<Rightarrow> atom set" and
+  bs :: "lrbs \<Rightarrow> atom set"
 where
-  "b7 (Assign x e) = {atom x}"
-| "b7s (Single a) = b7 a"
-| "b7s (More a as) = (b7 a) \<union> (b7s as)"
-thm exp7_lrb_lrbs.eq_iff
-thm exp7_lrb_lrbs.supp
+  "b (Assign x e) = {atom x}"
+| "bs (Single a) = b a"
+| "bs (More a as) = (b a) \<union> (bs as)"
+
+thm exp_lrb_lrbs.eq_iff
+thm exp_lrb_lrbs.supp
+
+declare permute_exp_raw_permute_lrb_raw_permute_lrbs_raw.simps[eqvt]
+declare alpha_gen_eqvt[eqvt]
+
+equivariance alpha_exp_raw
 
 end
 

--- a/Nominal/Ex/ExPS8.thy	Sun May 09 11:43:24 2010 +0100
+++ b/Nominal/Ex/ExPS8.thy	Sun May 09 12:26:10 2010 +0100
@@ -48,6 +48,11 @@
 thm exp_fnclause_fnclauses_lrb_lrbs_pat.fv
 thm exp_fnclause_fnclauses_lrb_lrbs_pat.eq_iff
 
+
+declare permute_exp_raw_permute_fnclause_raw_permute_fnclauses_raw_permute_lrb_raw_permute_lrbs_raw_permute_pat_raw.simps[eqvt]
+declare alpha_gen_eqvt[eqvt]
+
+equivariance alpha_exp_raw
 end
 
 

--- a/Nominal/Ex/Lambda.thy	Sun May 09 11:43:24 2010 +0100
+++ b/Nominal/Ex/Lambda.thy	Sun May 09 12:26:10 2010 +0100
@@ -15,6 +15,10 @@
 
 declare lam.perm[eqvt]
 
+declare permute_lam_raw.simps[eqvt]
+declare alpha_gen_eqvt[eqvt]
+equivariance alpha_lam_raw
+
 section {* Strong Induction Principles*}
 
 (*

--- a/Nominal/Ex/Term8.thy	Sun May 09 11:43:24 2010 +0100
+++ b/Nominal/Ex/Term8.thy	Sun May 09 12:26:10 2010 +0100
@@ -2,22 +2,27 @@
 imports "../NewParser"
 begin
 
-(* example 8 from Terms.thy *)
+(* example 8 *)
 
 atom_decl name
 
+(* this should work but gives an error at the moment:
+   seems like in the symmetry proof
+*)
+
 nominal_datatype foo =
   Foo0 "name"
 | Foo1 b::"bar" f::"foo" bind_set "bv b" in f
 and bar =
   Bar0 "name"
-| Bar1 "name" s::"name" b::"bar" bind_set s in b
+| Bar1 "name" s::"name" b::"bar" bind s in b
 binder
   bv
 where
   "bv (Bar0 x) = {}"
 | "bv (Bar1 v x b) = {atom v}"
 
+
 end
 
 

--- a/Nominal/Ex/TestMorePerm.thy	Sun May 09 11:43:24 2010 +0100
+++ b/Nominal/Ex/TestMorePerm.thy	Sun May 09 12:26:10 2010 +0100
@@ -1,35 +1,35 @@
 theory TestMorePerm
-imports "../Parser"
+imports "../NewParser"
 begin
 
 text {* 
   "Weirdo" example from Peter Sewell's bestiary. 
 
-  In case of deep binders, it is not coverd by our 
-  approach of defining alpha-equivalence with a 
-  single permutation.
-
-  Check whether it works with shallow binders as
-  defined below.
+  This example is not covered by our binding 
+  specification.
 
 *}
 ML {* val _ = cheat_equivp := true *}
 
 atom_decl name
 
-nominal_datatype foo =
+nominal_datatype weird =
   Foo_var "name"
-| Foo_pair "foo" "foo" 
-| Foo x::"name" y::"name" p1::"foo" p2::"foo" p3::"foo"
-    bind x in p1, bind x in p2, 
-    bind y in p2, bind y in p3
+| Foo_pair "weird" "weird" 
+| Foo x::"name" y::"name" p1::"weird" p2::"weird" p3::"weird"
+    bind x in p1 p2, 
+    bind y in p2 p3
 
-thm alpha_foo_raw.intros[no_vars]
+thm alpha_weird_raw.intros[no_vars]
 
 thm permute_weird_raw.simps[no_vars]
 thm alpha_weird_raw.intros[no_vars]
 thm fv_weird_raw.simps[no_vars]
 
+declare permute_weird_raw.simps[eqvt]
+declare alpha_gen_eqvt[eqvt]
+equivariance alpha_weird_raw
+
 
 end
 

--- a/Nominal/Ex/TypeSchemes.thy	Sun May 09 11:43:24 2010 +0100
+++ b/Nominal/Ex/TypeSchemes.thy	Sun May 09 12:26:10 2010 +0100
@@ -14,6 +14,11 @@
 
 lemmas ty_tys_supp = ty_tys.fv[simplified ty_tys.supp]
 
+declare permute_ty_raw_permute_tys_raw.simps[eqvt]
+declare alpha_gen_eqvt[eqvt]
+equivariance alpha_ty_raw
+
+
 (* below we define manually the function for size *)
 
 lemma size_eqvt_raw: