added container-lemma fresh_eqvt
authorurbanc
Fri Dec 16 18:22:58 2005 +0100 (2005-12-16)
changeset 18426d2303e8654a2
parent 18425 bcf13dbaa339
child 18427 b7ee916ae3ec
added container-lemma fresh_eqvt


(definition: container-lemma contains all instantiations
of a lemma from the general theory)
src/HOL/Nominal/nominal_atoms.ML
     1.1 --- a/src/HOL/Nominal/nominal_atoms.ML	Fri Dec 16 18:20:59 2005 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_atoms.ML	Fri Dec 16 18:22:58 2005 +0100
     1.3 @@ -817,6 +817,8 @@
     1.4         val dj_supp           = thm "nominal.dj_supp";
     1.5         val fresh_left_ineq   = thm "nominal.pt_fresh_left_ineq";
     1.6         val fresh_left        = thm "nominal.pt_fresh_left";
     1.7 +       val fresh_bij_ineq    = thm "nominal.pt_fresh_bij_ineq";
     1.8 +       val fresh_bij         = thm "nominal.pt_fresh_bij";
     1.9  
    1.10         (* Now we collect and instantiate some lemmas w.r.t. all atom      *)
    1.11         (* types; this allows for example to use abs_perm (which is a      *)
    1.12 @@ -908,6 +910,10 @@
    1.13  	      let val thms1 = inst_pt_at [fresh_left]
    1.14  		  and thms2 = inst_pt_pt_at_cp [fresh_left_ineq]
    1.15  	      in [(("fresh_left", thms1 @ thms2),[])] end
    1.16 +            ||>> PureThy.add_thmss
    1.17 +	      let val thms1 = inst_pt_at [fresh_bij]
    1.18 +		  and thms2 = inst_pt_pt_at_cp [fresh_bij_ineq]
    1.19 +	      in [(("fresh_eqvt", thms1 @ thms2),[])] end
    1.20  	   end;
    1.21  
    1.22      in NominalData.put (fold Symtab.update (map (rpair ()) full_ak_names)