# HG changeset patch
# User urbanc
# Date 1134993495 -3600
# Node ID 9649e24bc10e65f3e3d9b04eb4dc0e13015690f3
# Parent  318d2c2710401193a916c51a5bf15d03ad50050a
added thms to perm_compose (so far only composition
theorems were included where the type of the permutation
was equal)

diff -r 318d2c271040 -r 9649e24bc10e src/HOL/Nominal/nominal_atoms.ML
--- a/src/HOL/Nominal/nominal_atoms.ML	Mon Dec 19 12:09:56 2005 +0100
+++ b/src/HOL/Nominal/nominal_atoms.ML	Mon Dec 19 12:58:15 2005 +0100
@@ -699,14 +699,14 @@
              fun inst_pt thms = Library.flat (map (fn ti => instR ti pts) thms); 
              fun inst_at thms = Library.flat (map (fn ti => instR ti ats) thms);               
              fun inst_fs thms = Library.flat (map (fn ti => instR ti fss) thms);
+             fun inst_cp thms cps = Library.flat (inst_mult thms cps); 
 	     fun inst_pt_at thms = inst_zip ats (inst_pt thms);			
              fun inst_dj thms = Library.flat (map (fn ti => instR ti djs) thms);  
-	     fun inst_pt_pt_at_cp thms = 
-		 Library.flat (inst_mult (inst_zip ats (inst_zip pts (inst_pt thms))) cps);
+	     fun inst_pt_pt_at_cp thms = inst_cp (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 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 = inst_cp i_pt_pt_at cps';
 		 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
@@ -715,7 +715,10 @@
             ||>> PureThy.add_thmss [(("perm_swap", inst_pt_at [pt_swap_bij]),[])]
             ||>> PureThy.add_thmss [(("perm_fresh_fresh", inst_pt_at [pt_fresh_fresh]),[])]
             ||>> PureThy.add_thmss [(("perm_bij", inst_pt_at [pt_bij]),[])]
-            ||>> PureThy.add_thmss [(("perm_compose", inst_pt_at [pt_perm_compose]),[])]
+            ||>> PureThy.add_thmss 
+	      let val thms1 = inst_pt_at [pt_perm_compose];
+		  val thms2 = instR cp1 (Library.flat cps');
+              in [(("perm_compose",thms1 @ thms2),[])] end
             ||>> PureThy.add_thmss [(("perm_app_eq", inst_pt_at [perm_eq_app]),[])]
             ||>> PureThy.add_thmss [(("supp_atm", (inst_at [at_supp]) @ (inst_dj [dj_supp])),[])]
             ||>> PureThy.add_thmss [(("fresh_atm", inst_at [at_fresh]),[])]