added facts to lemma swap_simps and tuned lemma calc_atms
authorurbanc
Mon Jun 30 14:06:44 2008 +0200 (2008-06-30 ago)
changeset 273991fb3d1219c12
parent 27398 768da1da59d6
child 27400 42ee5e7c3b50
added facts to lemma swap_simps and tuned lemma calc_atms
src/HOL/Nominal/nominal_atoms.ML
     1.1 --- a/src/HOL/Nominal/nominal_atoms.ML	Mon Jun 30 13:41:33 2008 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_atoms.ML	Mon Jun 30 14:06:44 2008 +0200
     1.3 @@ -837,7 +837,10 @@
     1.4              ||>> PureThy.add_thmss [(("alpha_fresh", inst_pt_at [abs_fun_fresh]),[])]
     1.5              ||>> PureThy.add_thmss [(("alpha_fresh'", inst_pt_at [abs_fun_fresh']),[])]
     1.6              ||>> PureThy.add_thmss [(("perm_swap", inst_pt_at [pt_swap_bij] @ inst_pt_at [pt_swap_bij']),[])]
     1.7 -            ||>> PureThy.add_thmss [(("swap_simps", inst_at at_swap_simps),[])]  
     1.8 +            ||>> PureThy.add_thmss 
     1.9 +	      let val thms1 = inst_at at_swap_simps
    1.10 +                  and thms2 = inst_dj [dj_perm_forget]
    1.11 +              in [(("swap_simps", thms1 @ thms2),[])] end 
    1.12              ||>> PureThy.add_thmss 
    1.13                let val thms1 = inst_pt_at [pt_pi_rev];
    1.14                    val thms2 = inst_pt_at [pt_rev_pi];
    1.15 @@ -866,10 +869,9 @@
    1.16                    val thms2 = inst_dj [at_fresh_ineq]
    1.17                in [(("fresh_atm", thms1 @ thms2),[])] end
    1.18              ||>> PureThy.add_thmss
    1.19 -              let val thms1 = filter
    1.20 -                (fn th => case prop_of th of _ $ _ $ Var _ => true | _ => false)
    1.21 -                (List.concat (List.concat perm_defs))
    1.22 -              in [(("calc_atm", (inst_at at_calc) @ thms1),[])] end
    1.23 +              let val thms1 = inst_at at_calc
    1.24 +                  and thms2 = inst_dj [dj_perm_forget]
    1.25 +              in [(("calc_atm", thms1 @ thms2),[])] end
    1.26              ||>> PureThy.add_thmss
    1.27                let val thms1 = inst_pt_at [abs_fun_pi]
    1.28                    and thms2 = inst_pt_pt_at_cp [abs_fun_pi_ineq]