# HG changeset patch
# User huffman
# Date 1231344836 28800
# Node ID 9610f3870d64ef33b393e4471544e2aea082835a
# Parent  94fd5dd918f523f29a55bef1f9c35606b08101ce
add tracing for domain package proofs

diff -r 94fd5dd918f5 -r 9610f3870d64 src/HOLCF/Tools/domain/domain_theorems.ML
--- a/src/HOLCF/Tools/domain/domain_theorems.ML	Tue Jan 06 11:49:23 2009 -0800
+++ b/src/HOLCF/Tools/domain/domain_theorems.ML	Wed Jan 07 08:13:56 2009 -0800
@@ -10,6 +10,12 @@
 
 structure Domain_Theorems = struct
 
+val quiet_mode = ref false;
+val trace_domain = ref false;
+
+fun message s = if !quiet_mode then () else writeln s;
+fun trace s = if !trace_domain then tracing s else ();
+
 local
 
 val adm_impl_admw = @{thm adm_impl_admw};
@@ -115,7 +121,7 @@
 fun theorems (((dname, _), cons) : eq, eqs : eq list) thy =
 let
 
-val dummy = writeln ("Proving isomorphism properties of domain "^dname^" ...");
+val _ = message ("Proving isomorphism properties of domain "^dname^" ...");
 val pg = pg' thy;
 
 (* ----- getting the axioms and definitions --------------------------------- *)
@@ -158,6 +164,8 @@
 
 (* ----- generating beta reduction rules from definitions-------------------- *)
 
+val _ = trace " Proving beta reduction rules...";
+
 local
   fun arglist (Const _ $ Abs (s, _, t)) =
     let
@@ -179,7 +187,9 @@
     in pg (def::betas) appl (K [rtac reflexive_thm 1]) end;
 end;
 
+val _ = trace "Proving when_appl...";
 val when_appl = appl_of_def ax_when_def;
+val _ = trace "Proving con_appls...";
 val con_appls = map appl_of_def axs_con_def;
 
 local
@@ -229,7 +239,9 @@
     rewrite_goals_tac [mk_meta_eq iso_swap],
     rtac thm3 1];
 in
+  val _ = trace " Proving exhaust...";
   val exhaust = pg con_appls (mk_trp exh) (K tacs);
+  val _ = trace " Proving casedist...";
   val casedist =
     standard (rewrite_rule exh_casedists (exhaust RS exh_casedist0));
 end;
@@ -239,6 +251,7 @@
   fun bound_fun i _ = Bound (length cons - i);
   val when_app = list_ccomb (%%:(dname^"_when"), mapn bound_fun 1 cons);
 in
+  val _ = trace " Proving when_strict...";
   val when_strict =
     let
       val axs = [when_appl, mk_meta_eq rep_strict];
@@ -246,6 +259,7 @@
       val tacs = [resolve_tac [sscase1, ssplit1, strictify1] 1];
     in pg axs goal (K tacs) end;
 
+  val _ = trace " Proving when_apps...";
   val when_apps =
     let
       fun one_when n (con,args) =
@@ -276,6 +290,7 @@
       val tacs = [asm_simp_tac (HOLCF_ss addsimps when_rews) 1];
     in pg axs_dis_def goal (K tacs) end;
 
+  val _ = trace " Proving dis_apps...";
   val dis_apps = maps (fn (c,_) => map (dis_app c) cons) cons;
 
   fun dis_defin (con, args) =
@@ -288,7 +303,9 @@
           (asm_simp_tac (HOLCF_ss addsimps dis_apps) 1))];
     in pg [] goal (K tacs) end;
 
+  val _ = trace " Proving dis_stricts...";
   val dis_stricts = map dis_strict cons;
+  val _ = trace " Proving dis_defins...";
   val dis_defins = map dis_defin cons;
 in
   val dis_rews = dis_stricts @ dis_defins @ dis_apps;
@@ -301,6 +318,7 @@
       val tacs = [rtac when_strict 1];
     in pg axs_mat_def goal (K tacs) end;
 
+  val _ = trace " Proving mat_stricts...";
   val mat_stricts = map mat_strict cons;
 
   fun one_mat c (con, args) =
@@ -314,6 +332,7 @@
       val tacs = [asm_simp_tac (HOLCF_ss addsimps when_rews) 1];
     in pg axs_mat_def goal (K tacs) end;
 
+  val _ = trace " Proving mat_apps...";
   val mat_apps =
     maps (fn (c,_) => map (one_mat c) cons) cons;
 in
@@ -346,7 +365,9 @@
       val tacs = [asm_simp_tac (HOLCF_ss addsimps when_rews) 1];
     in pg axs goal (K tacs) end;
 
+  val _ = trace " Proving pat_stricts...";
   val pat_stricts = map pat_strict cons;
+  val _ = trace " Proving pat_apps...";
   val pat_apps = maps (fn c => map (pat_app c) cons) cons;
 in
   val pat_rews = pat_stricts @ pat_apps;
@@ -374,7 +395,9 @@
         asm_simp_tac (HOLCF_ss addsimps dis_rews) 1];
     in pg [] goal tacs end;
 in
+  val _ = trace " Proving con_stricts...";
   val con_stricts = maps con_strict cons;
+  val _ = trace " Proving pat_defins...";
   val con_defins = map con_defin cons;
   val con_rews = con_stricts @ con_defins;
 end;
@@ -391,6 +414,7 @@
         REPEAT (resolve_tac rules 1 ORELSE atac 1)];
     in pg con_appls goal (K tacs) end;
 in
+  val _ = trace " Proving con_compacts...";
   val con_compacts = map con_compact cons;
 end;
 
@@ -402,6 +426,7 @@
   fun sel_strict (_, args) =
     List.mapPartial (Option.map one_sel o sel_of) args;
 in
+  val _ = trace " Proving sel_stricts...";
   val sel_stricts = maps sel_strict cons;
 end;
 
@@ -439,6 +464,7 @@
   fun one_con (c, args) =
     flat (map_filter I (mapn (one_sel' c) 0 args));
 in
+  val _ = trace " Proving sel_apps...";
   val sel_apps = maps one_con cons;
 end;
 
@@ -453,6 +479,7 @@
           (asm_simp_tac (HOLCF_ss addsimps sel_apps) 1))];
     in pg [] goal (K tacs) end;
 in
+  val _ = trace " Proving sel_defins...";
   val sel_defins =
     if length cons = 1
     then List.mapPartial (fn arg => Option.map sel_defin (sel_of arg))
@@ -463,6 +490,7 @@
 val sel_rews = sel_stricts @ sel_defins @ sel_apps;
 val rev_contrapos = @{thm rev_contrapos};
 
+val _ = trace " Proving dist_les...";
 val distincts_le =
   let
     fun dist (con1, args1) (con2, args2) =
@@ -487,6 +515,8 @@
       | distincts (c::cs) = (map (distinct c) cs) :: distincts cs;
   in distincts cons end;
 val dist_les = flat (flat distincts_le);
+
+val _ = trace " Proving dist_eqs...";
 val dist_eqs =
   let
     fun distinct (_,args1) ((_,args2), leqs) =
@@ -517,6 +547,7 @@
     in pg con_appls prop end;
   val cons' = List.filter (fn (_,args) => args<>[]) cons;
 in
+  val _ = trace " Proving inverts...";
   val inverts =
     let
       val abs_less = ax_abs_iso RS (allI RS injection_less);
@@ -524,6 +555,7 @@
         [asm_full_simp_tac (HOLCF_ss addsimps [abs_less, spair_less]) 1];
     in map (fn (con, args) => pgterm (op <<) con args (K tacs)) cons' end;
 
+  val _ = trace " Proving injects...";
   val injects =
     let
       val abs_eq = ax_abs_iso RS (allI RS injection_eq);
@@ -551,6 +583,7 @@
       val tacs2 = [asm_simp_tac (HOLCF_ss addsimps when_apps) 1];
     in pg [ax_copy_def] goal (fn ctxt => (tacs1 ctxt @ tacs2)) end;
 in
+  val _ = trace " Proving copy_apps...";
   val copy_apps = map copy_app cons;
 end;
 
@@ -565,6 +598,7 @@
 
   fun has_nonlazy_rec (_, args) = exists is_nonlazy_rec args;
 in
+  val _ = trace " Proving copy_stricts...";
   val copy_stricts = map one_strict (List.filter has_nonlazy_rec cons);
 end;
 
@@ -603,7 +637,7 @@
 val conss  = map  snd        eqs;
 val comp_dname = Sign.full_bname thy comp_dnam;
 
-val d = writeln("Proving induction properties of domain "^comp_dname^" ...");
+val _ = message ("Proving induction properties of domain "^comp_dname^" ...");
 val pg = pg' thy;
 
 (* ----- getting the composite axiom and definitions ------------------------ *)
@@ -639,6 +673,7 @@
   val copy_con_rews  = copy_rews @ con_rews;
   val copy_take_defs =
     (if n_eqs = 1 then [] else [ax_copy2_def]) @ axs_take_def;
+  val _ = trace " Proving take_stricts...";
   val take_stricts =
     let
       fun one_eq ((dn, args), _) = strict (dc_take dn $ %:"n");
@@ -656,6 +691,7 @@
     in pg axs_take_def goal (K [simp_tac iterate_Cprod_ss 1]) end;
   val take_0s = mapn take_0 1 dnames;
   fun c_UU_tac ctxt = case_UU_tac ctxt (take_stricts'::copy_con_rews) 1;
+  val _ = trace " Proving take_apps...";
   val take_apps =
     let
       fun mk_eqn dn (con, args) =
@@ -737,6 +773,7 @@
     val is_finite = forall (not o lazy_rec_to [] false) n__eqs;
   end;
 in (* local *)
+  val _ = trace " Proving finite_ind...";
   val finite_ind =
     let
       fun concf n dn = %:(P_name n) $ (dc_take dn $ %:"n" `%(x_name n));
@@ -768,6 +805,7 @@
         end;
     in pg'' thy [] goal tacf end;
 
+  val _ = trace " Proving take_lemmas...";
   val take_lemmas =
     let
       fun take_lemma n (dn, ax_reach) =
@@ -793,6 +831,7 @@
 
 (* ----- theorems concerning finiteness and induction ----------------------- *)
 
+  val _ = trace " Proving finites, ind...";
   val (finites, ind) =
     if is_finite
     then (* finite case *)
@@ -914,6 +953,7 @@
   fun bnd_arg n i = Bound(2*(n_eqs - n)-i-1);
   val take_ss = HOL_ss addsimps take_rews;
   val sproj = prj (fn s => K("fst("^s^")")) (fn s => K("snd("^s^")"));
+  val _ = trace " Proving coind_lemma...";
   val coind_lemma =
     let
       fun mk_prj n _ = proj (%:"R") eqs n $ bnd_arg n 0 $ bnd_arg n 1;
@@ -940,6 +980,7 @@
         flat (mapn (x_tacs ctxt) 0 xs);
     in pg [ax_bisim_def] goal tacs end;
 in
+  val _ = trace " Proving coind...";
   val coind = 
     let
       fun mk_prj n x = mk_trp (proj (%:"R") eqs n $ %:x $ %:(x^"'"));