# HG changeset patch
# User huffman
# Date 1129078938 -7200
# Node ID 11bcd77cfa222643d2b6b8d3085adb91134be961
# Parent  060dd0213f94ffdc1d4d4b783e92467ef2fbcab7
domain package generates compactness lemmas for new constructors

diff -r 060dd0213f94 -r 11bcd77cfa22 src/HOLCF/domain/library.ML
--- a/src/HOLCF/domain/library.ML	Wed Oct 12 03:01:30 2005 +0200
+++ b/src/HOLCF/domain/library.ML	Wed Oct 12 03:02:18 2005 +0200
@@ -104,6 +104,7 @@
 val lessN      = "Porder.<<"
 val UU_N       = "Pcpo.UU";
 val admN       = "Adm.adm";
+val compactN   = "Adm.compact";
 val Rep_CFunN  = "Cfun.Rep_CFun";
 val Abs_CFunN  = "Cfun.Abs_CFun";
 val ID_N       = "Cfun.ID";
diff -r 060dd0213f94 -r 11bcd77cfa22 src/HOLCF/domain/theorems.ML
--- a/src/HOLCF/domain/theorems.ML	Wed Oct 12 03:01:30 2005 +0200
+++ b/src/HOLCF/domain/theorems.ML	Wed Oct 12 03:02:18 2005 +0200
@@ -217,6 +217,14 @@
                           asm_simp_tac (HOLCF_ss addsimps dis_rews) 1] )) cons;
 val con_rews = con_stricts @ con_defins;
 
+val con_compacts =
+  let
+    val rules = [compact_sinl, compact_sinr, compact_spair, compact_up, compact_ONE];
+    fun one_compact (con,args) = pg con_appls
+      (lift (fn x => %%:compactN $ %:(vname x)) (args, mk_trp(%%:compactN $ (con_app con args))))
+      [rtac (iso_locale RS iso_compact_abs) 1, REPEAT (resolve_tac rules 1 ORELSE atac 1)];
+  in map one_compact cons end;
+
 val sel_stricts = let fun one_sel sel = pg axs_sel_def (mk_trp(strict(%%:sel))) [
                                 simp_tac (HOLCF_ss addsimps when_rews) 1];
 in List.concat(map (fn (_,args) => List.mapPartial (fn arg => Option.map one_sel (sel_of arg)) args) cons) end;
@@ -330,6 +338,7 @@
 		("exhaust"  , [exhaust] ),
 		("casedist" , [casedist]),
 		("when_rews", when_rews ),
+		("compacts", con_compacts),
 		("con_rews", con_rews),
 		("sel_rews", sel_rews),
 		("dis_rews", dis_rews),