# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1303138665 -3600
# Node ID 810e7303c70defe494672fec1e3d882e69491bfc
# Parent  639979b7fa6e00a6eeeedf9118a5b592829fbe71# Parent  94f6f70e30675590b9acd5d3ef53b8cf33b56853
merged

diff -r 94f6f70e3067 -r 810e7303c70d Nominal/Ex/Lambda.thy
--- a/Nominal/Ex/Lambda.thy	Fri Apr 15 15:20:56 2011 +0900
+++ b/Nominal/Ex/Lambda.thy	Mon Apr 18 15:57:45 2011 +0100
@@ -16,9 +16,19 @@
   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"
diff -r 94f6f70e3067 -r 810e7303c70d Nominal/Nominal2.thy
--- a/Nominal/Nominal2.thy	Fri Apr 15 15:20:56 2011 +0900
+++ b/Nominal/Nominal2.thy	Mon Apr 18 15:57:45 2011 +0100
@@ -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) = 
diff -r 94f6f70e3067 -r 810e7303c70d Nominal/nominal_inductive.ML
--- a/Nominal/nominal_inductive.ML	Fri Apr 15 15:20:56 2011 +0900
+++ b/Nominal/nominal_inductive.ML	Mon Apr 18 15:57:45 2011 +0100
@@ -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