# HG changeset patch
# User urbanc
# Date 1152026762 -7200
# Node ID e0a5783d708fd322a0bcecb5236d2097a3c68ba3
# Parent  bb383dcec3d8f134f2f113c3258de45aad8c685d
added simplification rules to the fresh_guess tactic

diff -r bb383dcec3d8 -r e0a5783d708f src/HOL/Nominal/nominal_atoms.ML
--- a/src/HOL/Nominal/nominal_atoms.ML	Tue Jul 04 15:57:19 2006 +0200
+++ b/src/HOL/Nominal/nominal_atoms.ML	Tue Jul 04 17:26:02 2006 +0200
@@ -773,9 +773,7 @@
 	      in [(("fresh_atm", thms1 @ thms2),[])] end
             ||>> PureThy.add_thmss
 	      let val thms1 = List.concat (List.concat perm_defs)
-                  val thms2 = List.concat prm_eqs
-                  val thms3 = List.concat swap_eqs
-              in [(("calc_atm", (inst_at at_calc) @ thms1 @ thms2 @ thms3 ),[])] end
+              in [(("calc_atm", (inst_at at_calc) @ thms1),[])] end
             ||>> PureThy.add_thmss
 	      let val thms1 = inst_pt_at [abs_fun_pi]
 		  and thms2 = inst_pt_pt_at_cp [abs_fun_pi_ineq]
diff -r bb383dcec3d8 -r e0a5783d708f src/HOL/Nominal/nominal_permeq.ML
--- a/src/HOL/Nominal/nominal_permeq.ML	Tue Jul 04 15:57:19 2006 +0200
+++ b/src/HOL/Nominal/nominal_permeq.ML	Tue Jul 04 17:26:02 2006 +0200
@@ -271,6 +271,9 @@
     handle Subscript => Seq.empty
 
 val supports_fresh_rule = thm "supports_fresh";
+val fresh_def           = thm "Nominal.fresh_def";
+val fresh_prod          = thm "Nominal.fresh_prod";
+val fresh_unit          = thm "Nominal.fresh_unit";
 
 fun fresh_guess_tac tactical ss i st =
     let 
@@ -293,15 +296,15 @@
               Logic.strip_assums_concl (hd (prems_of supports_fresh_rule'));
             val supports_fresh_rule'' = Drule.cterm_instantiate
               [(cert (head_of S), cert s')] supports_fresh_rule'
-            val fresh_def   = thm "Nominal.fresh_def";
-	    val fresh_prod  = thm "Nominal.fresh_prod";
-            val fresh_unit  = thm "Nominal.fresh_unit";
-	    val simps       = [symmetric fresh_def,fresh_prod,fresh_unit]
+	    val ss1 = ss addsimps [symmetric fresh_def,fresh_prod,fresh_unit]
+            val ss2 = ss addsimps [supp_prod,supp_unit,finite_Un,Finites.emptyI]
+            (* FIXME sometimes these rewrite rules are already in the ss, *)
+            (* which produces a warning                                   *)
           in
             (tactical ("guessing of the right set that supports the goal",
                       EVERY [compose_tac (false, supports_fresh_rule'', 3) i,
-                             asm_full_simp_tac (ss addsimps simps) (i+2),
-                             asm_full_simp_tac ss (i+1), 
+                             asm_full_simp_tac ss1 (i+2),
+                             asm_full_simp_tac ss2 (i+1), 
                              supports_tac tactical ss i])) st
           end
         | _ => Seq.empty