# HG changeset patch
# User urbanc
# Date 1134493881 -3600
# Node ID b3e7da94b51fd5288df0c363dc300b0708d92b1f
# Parent  87217764cec2976980e1239781719a482be1d1b4
added a fresh_left lemma that contains all instantiation
for the various atom-types.

diff -r 87217764cec2 -r b3e7da94b51f src/HOL/Nominal/nominal_atoms.ML
--- a/src/HOL/Nominal/nominal_atoms.ML	Tue Dec 13 16:30:50 2005 +0100
+++ b/src/HOL/Nominal/nominal_atoms.ML	Tue Dec 13 18:11:21 2005 +0100
@@ -815,6 +815,8 @@
        val at_calc           = thms "nominal.at_calc";
        val at_supp           = thm "nominal.at_supp";
        val dj_supp           = thm "nominal.dj_supp";
+       val fresh_left_ineq   = thm "nominal.pt_fresh_left_ineq";
+       val fresh_left        = thm "nominal.pt_fresh_left";
 
        (* Now we collect and instantiate some lemmas w.r.t. all atom      *)
        (* types; this allows for example to use abs_perm (which is a      *)
@@ -869,11 +871,11 @@
 	     fun inst_pt_pt_at_cp thms = 
 		 Library.flat (inst_mult (inst_zip ats (inst_zip pts (inst_pt thms))) cps);
              fun inst_pt_at_fs thms = inst_zip (inst_fs [fs1]) (inst_zip ats (inst_pt thms));
-	     fun inst_pt_pt_at_cp_dj thms = 
+	     fun inst_pt_pt_at_cp thms = 
 		 let val i_pt_pt_at = inst_zip ats (inst_zip pts (inst_pt thms));
                      val i_pt_pt_at_cp = Library.flat (inst_mult i_pt_pt_at cps');
-                     val i_pt_pt_at_cp_dj = inst_zip djs i_pt_pt_at_cp;
-		 in i_pt_pt_at_cp_dj end;
+		 in i_pt_pt_at_cp end;
+             fun inst_pt_pt_at_cp_dj thms = inst_zip djs (inst_pt_pt_at_cp thms);
            in
             thy32 
 	    |>   PureThy.add_thmss [(("alpha", inst_pt_at [abs_fun_eq]),[])]
@@ -902,6 +904,10 @@
 		  and thms2 = inst_pt_at_fs [abs_fun_supp]
 		  and thms3 = inst_pt_pt_at_cp_dj [abs_fun_supp_ineq]
 	      in [(("abs_supp", thms1 @ thms2 @ thms3),[])] end
+            ||>> PureThy.add_thmss
+	      let val thms1 = inst_pt_at [fresh_left]
+		  and thms2 = inst_pt_pt_at_cp [fresh_left_ineq]
+	      in [(("fresh_left", thms1 @ thms2),[])] end
 	   end;
 
     in NominalData.put (fold Symtab.update (map (rpair ()) full_ak_names)