added simplification rules to the fresh_guess tactic
authorurbanc
Tue Jul 04 17:26:02 2006 +0200 (2006-07-04)
changeset 19993e0a5783d708f
parent 19992 bb383dcec3d8
child 19994 669a1a609544
added simplification rules to the fresh_guess tactic
src/HOL/Nominal/nominal_atoms.ML
src/HOL/Nominal/nominal_permeq.ML
     1.1 --- a/src/HOL/Nominal/nominal_atoms.ML	Tue Jul 04 15:57:19 2006 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_atoms.ML	Tue Jul 04 17:26:02 2006 +0200
     1.3 @@ -773,9 +773,7 @@
     1.4  	      in [(("fresh_atm", thms1 @ thms2),[])] end
     1.5              ||>> PureThy.add_thmss
     1.6  	      let val thms1 = List.concat (List.concat perm_defs)
     1.7 -                  val thms2 = List.concat prm_eqs
     1.8 -                  val thms3 = List.concat swap_eqs
     1.9 -              in [(("calc_atm", (inst_at at_calc) @ thms1 @ thms2 @ thms3 ),[])] end
    1.10 +              in [(("calc_atm", (inst_at at_calc) @ thms1),[])] end
    1.11              ||>> PureThy.add_thmss
    1.12  	      let val thms1 = inst_pt_at [abs_fun_pi]
    1.13  		  and thms2 = inst_pt_pt_at_cp [abs_fun_pi_ineq]
     2.1 --- a/src/HOL/Nominal/nominal_permeq.ML	Tue Jul 04 15:57:19 2006 +0200
     2.2 +++ b/src/HOL/Nominal/nominal_permeq.ML	Tue Jul 04 17:26:02 2006 +0200
     2.3 @@ -271,6 +271,9 @@
     2.4      handle Subscript => Seq.empty
     2.5  
     2.6  val supports_fresh_rule = thm "supports_fresh";
     2.7 +val fresh_def           = thm "Nominal.fresh_def";
     2.8 +val fresh_prod          = thm "Nominal.fresh_prod";
     2.9 +val fresh_unit          = thm "Nominal.fresh_unit";
    2.10  
    2.11  fun fresh_guess_tac tactical ss i st =
    2.12      let 
    2.13 @@ -293,15 +296,15 @@
    2.14                Logic.strip_assums_concl (hd (prems_of supports_fresh_rule'));
    2.15              val supports_fresh_rule'' = Drule.cterm_instantiate
    2.16                [(cert (head_of S), cert s')] supports_fresh_rule'
    2.17 -            val fresh_def   = thm "Nominal.fresh_def";
    2.18 -	    val fresh_prod  = thm "Nominal.fresh_prod";
    2.19 -            val fresh_unit  = thm "Nominal.fresh_unit";
    2.20 -	    val simps       = [symmetric fresh_def,fresh_prod,fresh_unit]
    2.21 +	    val ss1 = ss addsimps [symmetric fresh_def,fresh_prod,fresh_unit]
    2.22 +            val ss2 = ss addsimps [supp_prod,supp_unit,finite_Un,Finites.emptyI]
    2.23 +            (* FIXME sometimes these rewrite rules are already in the ss, *)
    2.24 +            (* which produces a warning                                   *)
    2.25            in
    2.26              (tactical ("guessing of the right set that supports the goal",
    2.27                        EVERY [compose_tac (false, supports_fresh_rule'', 3) i,
    2.28 -                             asm_full_simp_tac (ss addsimps simps) (i+2),
    2.29 -                             asm_full_simp_tac ss (i+1), 
    2.30 +                             asm_full_simp_tac ss1 (i+2),
    2.31 +                             asm_full_simp_tac ss2 (i+1), 
    2.32                               supports_tac tactical ss i])) st
    2.33            end
    2.34          | _ => Seq.empty