# HG changeset patch
# User huffman
# Date 1265656452 28800
# Node ID d0cc1650b378cd37e8382bb574667043629ceeee
# Parent  03d023236fcdf35e1c7865a479bd913d532c14ce
handle case where copy_stricts cannot be proven; rewrite proof script for take_apps

diff -r 03d023236fcd -r d0cc1650b378 src/HOLCF/Tools/Domain/domain_theorems.ML
--- a/src/HOLCF/Tools/Domain/domain_theorems.ML	Sun Feb 07 10:31:11 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_theorems.ML	Mon Feb 08 11:14:12 2010 -0800
@@ -593,7 +593,12 @@
     val goal = mk_trp (strict (dc_copy `% "f"));
     val rules = [abs_strict, rep_strict] @ @{thms domain_map_stricts};
     val tacs = [asm_simp_tac (HOLCF_ss addsimps rules) 1];
-  in pg [ax_copy_def] goal (K tacs) end;
+  in
+    SOME (pg [ax_copy_def] goal (K tacs))
+    handle
+      THM (s, _, _) => (trace s; NONE)
+    | ERROR s => (trace s; NONE)
+  end;
 
 local
   fun copy_app (con, args) =
@@ -621,18 +626,23 @@
   fun one_strict (con, args) = 
     let
       val goal = mk_trp (dc_copy`UU`(con_app con args) === UU);
-      val rews = copy_strict :: copy_apps @ con_rews;
+      val rews = the_list copy_strict @ copy_apps @ con_rews;
       fun tacs ctxt = map (case_UU_tac ctxt rews 1) (nonlazy args) @
         [asm_simp_tac (HOLCF_ss addsimps rews) 1];
-    in pg [] goal tacs end;
+    in
+      SOME (pg [] goal tacs)
+      handle
+        THM (s, _, _) => (trace s; NONE)
+      | ERROR s => (trace s; NONE)
+    end;
 
   fun has_nonlazy_rec (_, args) = exists is_nonlazy_rec args;
 in
   val _ = trace " Proving copy_stricts...";
-  val copy_stricts = map one_strict (filter has_nonlazy_rec cons);
+  val copy_stricts = map_filter one_strict (filter has_nonlazy_rec cons);
 end;
 
-val copy_rews = copy_strict :: copy_apps @ copy_stricts;
+val copy_rews = the_list copy_strict @ copy_apps @ copy_stricts;
 
 in
   thy
@@ -721,47 +731,34 @@
         rtac @{thm iterate_below_fix} 1];
     in pg axs_take_def goal (K tacs) end;
   val take_stricts = map one_take_strict eqs;
-  val take_stricts' = map (rewrite_rule copy_take_defs) take_stricts;
   fun take_0 n dn =
     let
-      val goal = mk_trp ((dc_take dn $ %%: @{const_name Algebras.zero}) `% x_name n === UU);
+      val goal = mk_trp ((dc_take dn $ @{term "0::nat"}) `% x_name n === UU);
     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;
+  fun c_UU_tac ctxt = case_UU_tac ctxt (take_stricts @ con_rews) 1;
   val _ = trace " Proving take_apps...";
-  val take_apps =
+  fun one_take_app dn (con, args) =
     let
-      fun mk_eqn dn (con, args) =
-        let
-          fun mk_take n = dc_take (List.nth (dnames, n)) $ %:"n";
-          fun one_rhs arg =
-              if Datatype_Aux.is_rec_type (dtyp_of arg)
-              then Domain_Axioms.copy_of_dtyp map_tab
-                     mk_take (dtyp_of arg) ` (%# arg)
-              else (%# arg);
-          val lhs = (dc_take dn $ (%%:"Suc" $ %:"n"))`(con_app con args);
-          val rhs = con_app2 con one_rhs args;
-        in Library.foldr mk_all (map vname args, lhs === rhs) end;
-      fun mk_eqns ((dn, _), cons) = map (mk_eqn dn) cons;
-      val goal = mk_trp (foldr1 mk_conj (maps mk_eqns eqs));
-      val simps = filter (has_fewer_prems 1) copy_rews;
-      fun con_tac ctxt (con, args) =
-        if nonlazy_rec args = []
-        then all_tac
-        else EVERY (map (c_UU_tac ctxt) (nonlazy_rec args)) THEN
-          asm_full_simp_tac (HOLCF_ss addsimps copy_rews) 1;
-      fun eq_tacs ctxt ((dn, _), cons) = map (con_tac ctxt) cons;
+      fun mk_take n = dc_take (List.nth (dnames, n)) $ %:"n";
+      fun one_rhs arg =
+          if Datatype_Aux.is_rec_type (dtyp_of arg)
+          then Domain_Axioms.copy_of_dtyp map_tab
+                 mk_take (dtyp_of arg) ` (%# arg)
+          else (%# arg);
+      val lhs = (dc_take dn $ (%%:"Suc" $ %:"n"))`(con_app con args);
+      val rhs = con_app2 con one_rhs args;
+      val goal = mk_trp (lhs === rhs);
       fun tacs ctxt =
-        simp_tac iterate_Cprod_ss 1 ::
-        InductTacs.induct_tac ctxt [[SOME "n"]] 1 ::
-        simp_tac (iterate_Cprod_ss addsimps copy_con_rews) 1 ::
-        asm_full_simp_tac (HOLCF_ss addsimps simps) 1 ::
-        TRY (safe_tac HOL_cs) ::
-        maps (eq_tacs ctxt) eqs;
-    in pg copy_take_defs goal tacs end;
+        map (c_UU_tac ctxt) (nonlazy_rec args) @ [
+        rewrite_goals_tac copy_take_defs,
+        asm_simp_tac (HOLCF_ss addsimps copy_con_rews) 1];
+    in pg [] goal tacs end;
+  fun one_take_apps ((dn, _), cons) = map (one_take_app dn) cons;
+  val take_apps = maps one_take_apps eqs;
 in
   val take_rews = map Drule.standard
-    (take_stricts @ take_0s @ atomize global_ctxt take_apps);
+    (take_stricts @ take_0s @ take_apps);
 end; (* local *)
 
 local