--- a/Nominal/Ex/Lambda.thy	Thu Apr 28 11:44:36 2011 +0800
+++ b/Nominal/Ex/Lambda.thy	Thu Apr 28 11:51:01 2011 +0800
@@ -16,10 +16,40 @@
   Var: "triv (Var x) n"
 
 equivariance triv
-nominal_inductive triv avoids Var : "{}::name set"
-apply(auto simp add: fresh_star_def)
-done 
+nominal_inductive triv avoids Var: "{}::name set"
+apply(auto simp add: fresh_star_def) 
+done
+
+inductive 
+  triv2 :: "lam \<Rightarrow> nat \<Rightarrow> bool" 
+where
+  Var1: "triv2 (Var x) 0"
+| Var2: "triv2 (Var x) (n + n)"
+| Var3: "triv2 (Var x) n"
+
+equivariance triv2
+nominal_inductive triv2 .
 
+lemma Abs1_eq_fdest:
+  fixes x y :: "'a :: at_base"
+    and S T :: "'b :: fs"
+  assumes "(Abs_lst [atom x] T) = (Abs_lst [atom y] S)"
+  and "x \<noteq> y \<Longrightarrow> atom y \<sharp> T \<Longrightarrow> atom x \<sharp> f x T"
+  and "x \<noteq> y \<Longrightarrow> atom y \<sharp> T \<Longrightarrow> atom y \<sharp> f x T"
+  and "x \<noteq> y \<Longrightarrow> atom y \<sharp> T \<Longrightarrow> (atom x \<rightleftharpoons> atom y) \<bullet> T = S \<Longrightarrow> (atom x \<rightleftharpoons> atom y) \<bullet> (f x T) = f y S"
+  and "sort_of (atom x) = sort_of (atom y)"
+  shows "f x T = f y S"
+using assms apply -
+apply (subst (asm) Abs1_eq_iff')
+apply simp_all
+apply (elim conjE disjE)
+apply simp
+apply(rule trans)
+apply (rule_tac p="(atom x \<rightleftharpoons> atom y)" in supp_perm_eq[symmetric])
+apply(rule fresh_star_supp_conv)
+apply(simp add: supp_swap fresh_star_def)
+apply(simp add: swap_commute)
+done
 
 text {* height function *}
 
@@ -32,11 +62,8 @@
 defer
 apply(rule_tac y="x" in lam.exhaust)
 apply(auto simp add: lam.distinct lam.eq_iff)
-apply(simp add: Abs_eq_iff alphas)
-apply(clarify)
-apply(subst (4) supp_perm_eq[where p="p", symmetric])
-apply(simp add: pure_supp fresh_star_def)
-apply(simp add: eqvt_at_def)
+apply (erule Abs1_eq_fdest)
+apply(simp_all add: fresh_def pure_supp eqvt_at_def)
 apply(subgoal_tac "\<And>p x r. height_graph x r \<Longrightarrow> height_graph (p \<bullet> x) (p \<bullet> r)") 
 unfolding eqvt_def
 apply(rule allI)
@@ -82,23 +109,12 @@
 defer
 apply(rule_tac y="x" in lam.exhaust)
 apply(simp_all)[3]
-apply(simp_all only: lam.distinct)
-apply(simp add: lam.eq_iff)
-apply(simp add: lam.eq_iff)
-apply(simp add: lam.eq_iff)
-apply(simp add: Abs_eq_iff)
-apply(erule exE)
-apply(simp add: alphas)
-apply(simp add: atom_eqvt)
-apply(clarify)
-apply(rule trans)
-apply(rule_tac p="p" in supp_perm_eq[symmetric])
-apply(simp (no_asm) add: supp_removeAll)
+apply(simp_all add: lam.distinct lam.eq_iff)
+apply (erule Abs1_eq_fdest)
+apply(simp add: supp_removeAll fresh_def)
 apply(drule supp_eqvt_at)
 apply(simp add: finite_supp)
-apply(auto simp add: fresh_star_def)[1]
-unfolding eqvt_at_def
-apply(simp only: removeAll_eqvt atom_eqvt)
+apply(auto simp add: fresh_def supp_removeAll eqvts eqvt_at_def)
 apply(subgoal_tac "\<And>p x r. frees_lst_graph x r \<Longrightarrow> frees_lst_graph (p \<bullet> x) (p \<bullet> r)") 
 unfolding eqvt_def
 apply(rule allI)
@@ -151,36 +167,15 @@
 apply(auto simp add: lam.distinct lam.eq_iff)
 apply(rule_tac y="a" and c="(aa, b)" in lam.strong_exhaust)
 apply(blast)+
-apply(simp add: fresh_star_def)
-apply(subgoal_tac "atom xa \<sharp> [[atom x]]lst. t")
-apply(subst (asm) Abs_eq_iff2)
-apply(simp add: alphas atom_eqvt)
-apply(clarify)
-apply(rule trans)
-apply(rule_tac p="p" in supp_perm_eq[symmetric])
-apply(rule fresh_star_supp_conv)
-apply(drule fresh_star_perm_set_conv)
-apply(simp add: finite_supp)
-apply(subgoal_tac "{atom (p \<bullet> x), atom x} \<sharp>* ([[atom x]]lst. subst_sumC (t, ya, sa))")
-apply(auto simp add: fresh_star_def)[1]
-apply(simp (no_asm) add: fresh_star_def)
-apply(rule conjI)
-apply(simp (no_asm) add: Abs_fresh_iff)
-apply(clarify)
-apply(drule_tac a="atom (p \<bullet> x)" in fresh_eqvt_at)
-apply(simp add: finite_supp)
-apply(simp (no_asm_use) add: fresh_Pair)
-apply(simp add: Abs_fresh_iff)
-apply(simp)
-apply(simp add: Abs_fresh_iff)
-apply(subgoal_tac "p \<bullet> ya = ya")
-apply(subgoal_tac "p \<bullet> sa = sa")
-apply(simp add: atom_eqvt eqvt_at_def)
-apply(rule perm_supp_eq)
-apply(auto simp add: fresh_star_def fresh_Pair)[1]
-apply(rule perm_supp_eq)
-apply(auto simp add: fresh_star_def fresh_Pair)[1]
-apply(simp add: Abs_fresh_iff)
+apply(simp_all add: fresh_star_def fresh_Pair_elim)
+apply (erule Abs1_eq_fdest)
+apply(simp_all add: Abs_fresh_iff)
+apply(drule_tac a="atom (xa)" in fresh_eqvt_at)
+apply(simp_all add: finite_supp fresh_Pair)
+apply(subgoal_tac "(atom x \<rightleftharpoons> atom xa) \<bullet> sa = sa")
+apply(subgoal_tac "(atom x \<rightleftharpoons> atom xa) \<bullet> ya = ya")
+apply(simp add: eqvt_at_def)
+apply(rule perm_supp_eq,simp add: fresh_star_def fresh_Pair supp_swap)+
 apply(subgoal_tac "\<And>p x r. subst_graph x r \<Longrightarrow> subst_graph (p \<bullet> x) (p \<bullet> r)") 
 unfolding eqvt_def
 apply(rule allI)
@@ -256,6 +251,28 @@
 apply (auto simp add: lam.fresh fresh_at_base)
 done
 
+lemma height_ge_one:
+  shows "1 \<le> (height e)"
+by (induct e rule: lam.induct) (simp_all)
+
+theorem height_subst:
+  shows "height (e[x::=e']) \<le> ((height e) - 1) + (height e')"
+proof (nominal_induct e avoiding: x e' rule: lam.strong_induct)
+  case (Var y)
+  have "1 \<le> height e'" by (rule height_ge_one)
+  then show "height (Var y[x::=e']) \<le> height (Var y) - 1 + height e'" by simp
+next
+  case (Lam y e1)
+  hence ih: "height (e1[x::=e']) \<le> ((height e1) - 1) + (height e')" by simp
+  moreover
+  have vc: "atom y\<sharp>x" "atom y\<sharp>e'" by fact+ (* usual variable convention *)
+  ultimately show "height ((Lam [y]. e1)[x::=e']) \<le> height (Lam [y]. e1) - 1 + height e'" by simp
+next
+  case (App e1 e2)
+  hence ih1: "height (e1[x::=e']) \<le> ((height e1) - 1) + (height e')"
+    and ih2: "height (e2[x::=e']) \<le> ((height e2) - 1) + (height e')" by simp_all
+  then show "height ((App e1 e2)[x::=e']) \<le> height (App e1 e2) - 1 + height e'"  by simp
+qed
 
 subsection {* single-step beta-reduction *}
 
@@ -332,9 +349,7 @@
 
 lemma [eqvt]:
   shows "(p \<bullet> lookup xs n x) = lookup (p \<bullet> xs) (p \<bullet> n) (p \<bullet> x)"
-  apply(induct xs arbitrary: n)
-  apply(simp_all add: permute_pure)
-  done
+  by (induct xs arbitrary: n) (simp_all add: permute_pure)
 
 nominal_primrec
   trans :: "lam \<Rightarrow> name list \<Rightarrow> ln"
@@ -349,50 +364,18 @@
 apply(simp_all add: fresh_star_def)[3]
 apply(blast)
 apply(blast)
-apply(simp_all add: lam.distinct)
-apply(simp add: lam.eq_iff)
-apply(simp add: lam.eq_iff)
-apply(simp add: lam.eq_iff)
-apply(erule conjE)
-apply(subgoal_tac "atom xa \<sharp> [[atom x]]lst. t")
+apply(simp_all add: lam.distinct lam.eq_iff)
+apply(elim conjE)
+apply clarify
+apply (erule Abs1_eq_fdest)
+apply (simp_all add: ln.fresh)
 prefer 2
-apply(simp add: Abs_fresh_iff)
-apply(subst (asm) Abs_eq_iff2)
-apply(auto)
-apply(simp add: alphas)
-apply(simp add: atom_eqvt)
-apply(clarify)
-apply(rule trans)
-apply(rule_tac p="p" in supp_perm_eq[symmetric])
+apply(drule supp_eqvt_at)
+apply (auto simp add: finite_supp supp_Pair fresh_def supp_Cons supp_at_base)[2]
 prefer 2
-apply (subgoal_tac "p \<bullet> xsa = xsa")
+apply (subgoal_tac "(atom x \<rightleftharpoons> atom xa) \<bullet> xsa = xsa")
 apply (simp add: eqvt_at_def)
-apply (rule supp_perm_eq)
-apply (rule fresh_star_supp_conv)
-apply (subgoal_tac "{atom (p \<bullet> x), atom x} \<sharp>* xsa")
-apply (simp add: fresh_star_def fresh_def)
-apply blast
-apply (simp add: fresh_star_def fresh_def)
-apply (simp add:  ln.supp)
-apply(rule fresh_star_supp_conv)
-apply (subst (asm) supp_perm_pair)
-apply (elim disjE)
-apply (simp add: fresh_star_def supp_zero_perm)
-apply (simp add: flip_def[symmetric])
-apply(subgoal_tac "supp (x \<leftrightarrow> p \<bullet> x) \<sharp>* trans_sumC (t, x # xsa)")
-apply simp
-apply (subst flip_def)
-apply (simp add: supp_swap)
-apply (simp add: fresh_star_def)
-apply (rule)
-apply rule
-prefer 2
-apply(drule_tac a="atom (p \<bullet> x)" in fresh_eqvt_at)
-apply(simp add: finite_supp)
-apply(simp (no_asm_use) add: fresh_Pair)
-apply(simp add: Abs_fresh_iff fresh_Cons)[1]
-apply (metis Rep_name_inverse atom_name_def fresh_at_base)
-apply assumption
+apply (metis atom_name_def swap_fresh_fresh)
 oops
 
 (* lemma helpr: "atom x \<sharp> ta \<Longrightarrow> Lam [xa]. ta = Lam [x]. ((xa \<leftrightarrow> x) \<bullet> ta)"

--- a/Nominal/Nominal2.thy	Thu Apr 28 11:44:36 2011 +0800
+++ b/Nominal/Nominal2.thy	Thu Apr 28 11:51:01 2011 +0800
@@ -323,19 +323,19 @@
 
   val _ = trace_msg (K "Defining the quotient constants...")
   val qconstrs_descrs =
-    (map2 o map2) (fn (b, _, mx) => fn t => (Name.of_binding b, t, mx)) (get_cnstrs dts) raw_constrs
+    (map2 o map2) (fn (b, _, mx) => fn t => (Variable.name b, t, mx)) (get_cnstrs dts) raw_constrs
 
   val qbns_descr =
-    map2 (fn (b, _, mx) => fn t => (Name.of_binding b, t, mx)) bn_funs raw_bns
+    map2 (fn (b, _, mx) => fn t => (Variable.name b, t, mx)) bn_funs raw_bns
 
   val qfvs_descr = 
     map2 (fn n => fn t => ("fv_" ^ n, t, NoSyn)) qty_names raw_fvs
 
   val qfv_bns_descr = 
-    map2 (fn (b, _, _) => fn t => ("fv_" ^ Name.of_binding b, t, NoSyn)) bn_funs raw_fv_bns
+    map2 (fn (b, _, _) => fn t => ("fv_" ^ Variable.name b, t, NoSyn)) bn_funs raw_fv_bns
 
   val qalpha_bns_descr = 
-    map2 (fn (b, _, _) => fn t => ("alpha_" ^ Name.of_binding b, t, NoSyn)) bn_funs  alpha_bn_trms
+    map2 (fn (b, _, _) => fn t => ("alpha_" ^ Variable.name b, t, NoSyn)) bn_funs  alpha_bn_trms
 
   val qperm_descr =
     map2 (fn n => fn t => ("permute_" ^ n, Type.legacy_freeze t, NoSyn)) qty_names raw_perm_funs
@@ -344,7 +344,7 @@
     map2 (fn n => fn t => ("size_" ^ n, t, NoSyn)) qty_names raw_size_trms
 
   val qperm_bn_descr = 
-    map2 (fn (b, _, _) => fn t => ("permute_" ^ Name.of_binding b, t, NoSyn)) bn_funs raw_perm_bns
+    map2 (fn (b, _, _) => fn t => ("permute_" ^ Variable.name b, t, NoSyn)) bn_funs raw_perm_bns
      
   val ((((((qconstrs_infos, qbns_info), qfvs_info), qfv_bns_info), qalpha_bns_info), qperm_bns_info), 
     lthy8) = 
@@ -646,7 +646,7 @@
 
   val (((dts, (bn_funs, bn_eqs)), bclauses), tmp_thy') = 
     tmp_thy
-    |> Sign.add_types pre_typs
+    |> Sign.add_types_global pre_typs
     |> prepare_dts dt_strs 
     ||>> prepare_bn_funs bn_fun_strs bn_eq_strs 
     ||>> prepare_bclauses dt_strs 

--- a/Nominal/nominal_inductive.ML	Thu Apr 28 11:44:36 2011 +0800
+++ b/Nominal/nominal_inductive.ML	Thu Apr 28 11:51:01 2011 +0800
@@ -139,10 +139,10 @@
 in
 (* by default eqvt_strict_config contains unwanted @{thm permute_pure} *) 
 
-val eqvt_sconfig = (delposts eqvt_strict_config) addpres @{thms permute_minus_cancel}
+val eqvt_sconfig = eqvt_strict_config addpres @{thms permute_minus_cancel}
 
 fun eqvt_stac ctxt = eqvt_tac ctxt eqvt_sconfig
-fun eqvt_srule ctxt = eqvt_rule ctxt eqvt_sconfig  
+fun eqvt_srule ctxt = eqvt_rule ctxt eqvt_sconfig
 
 end
 
@@ -175,7 +175,9 @@
       val prm_tys = map (fastype_of o term_of) prms
       val cperms = map (cterm_of thy o perm_const) prm_tys
       val p_prms = map2 (fn ct1 => fn ct2 => Thm.mk_binop ct1 p ct2) cperms prms 
-      val prem' = cterm_instantiate (intr_cvars ~~ p_prms) prem
+      val prem' = prem
+        |> cterm_instantiate (intr_cvars ~~ p_prms) 
+        |> eqvt_srule ctxt
 
       (* for inductive-premises*)
       fun tac1 prm = helper_tac true prm p context 
@@ -189,7 +191,9 @@
       fun select prm (t, i) =
         (if member same_name Ps (real_head_of t) then tac1 prm else tac2 prm) i
     in
-      EVERY1 [eqvt_stac ctxt, rtac prem', RANGE (map (SUBGOAL o select) prems) ]
+      EVERY1 [ eqvt_stac context, 
+               rtac prem', 
+               RANGE (map (SUBGOAL o select) prems) ]
     end) ctxt
 
 fun fresh_thm ctxt user_thm p c concl_args avoid_trm =
@@ -244,7 +248,9 @@
 
       val cperms = map (cterm_of thy o perm_const) prm_tys
       val qp_prms = map2 (fn ct1 => fn ct2 => Thm.mk_binop ct1 (mk_cplus q p) ct2) cperms prms 
-      val prem' = cterm_instantiate (intr_cvars ~~ qp_prms) prem
+      val prem' = prem
+        |> cterm_instantiate (intr_cvars ~~ qp_prms)
+        |> eqvt_srule ctxt
 
       val fprop' = eqvt_srule ctxt' fprop 
       val tac_fresh = simp_tac (HOL_basic_ss addsimps [fprop'])
@@ -277,7 +283,8 @@
     val tac1 = non_binder_tac prem intr_cvars Ps ctxt
     val tac2 = binder_tac prem intr_cvars param_trms Ps user_thm avoid_trm concl_args ctxt
   in 
-    EVERY' [ rtac @{thm allI}, rtac @{thm allI}, if null avoid then tac1 else tac2 ]
+    EVERY' [ rtac @{thm allI}, rtac @{thm allI}, 
+             if null avoid then tac1 else tac2 ]
   end
 
 fun prove_sinduct_tac raw_induct user_thms Ps avoids avoid_trms intr_cvars param_trms concl_args