1.1 --- a/src/HOLCF/Tools/Domain/domain_theorems.ML	Sun Feb 07 10:31:11 2010 -0800
     1.2 +++ b/src/HOLCF/Tools/Domain/domain_theorems.ML	Mon Feb 08 11:14:12 2010 -0800
     1.3 @@ -593,7 +593,12 @@
     1.4      val goal = mk_trp (strict (dc_copy `% "f"));
     1.5      val rules = [abs_strict, rep_strict] @ @{thms domain_map_stricts};
     1.6      val tacs = [asm_simp_tac (HOLCF_ss addsimps rules) 1];
     1.7 -  in pg [ax_copy_def] goal (K tacs) end;
     1.8 +  in
     1.9 +    SOME (pg [ax_copy_def] goal (K tacs))
    1.10 +    handle
    1.11 +      THM (s, _, _) => (trace s; NONE)
    1.12 +    | ERROR s => (trace s; NONE)
    1.13 +  end;
    1.14  
    1.15  local
    1.16    fun copy_app (con, args) =
    1.17 @@ -621,18 +626,23 @@
    1.18    fun one_strict (con, args) = 
    1.19      let
    1.20        val goal = mk_trp (dc_copy`UU`(con_app con args) === UU);
    1.21 -      val rews = copy_strict :: copy_apps @ con_rews;
    1.22 +      val rews = the_list copy_strict @ copy_apps @ con_rews;
    1.23        fun tacs ctxt = map (case_UU_tac ctxt rews 1) (nonlazy args) @
    1.24          [asm_simp_tac (HOLCF_ss addsimps rews) 1];
    1.25 -    in pg [] goal tacs end;
    1.26 +    in
    1.27 +      SOME (pg [] goal tacs)
    1.28 +      handle
    1.29 +        THM (s, _, _) => (trace s; NONE)
    1.30 +      | ERROR s => (trace s; NONE)
    1.31 +    end;
    1.32  
    1.33    fun has_nonlazy_rec (_, args) = exists is_nonlazy_rec args;
    1.34  in
    1.35    val _ = trace " Proving copy_stricts...";
    1.36 -  val copy_stricts = map one_strict (filter has_nonlazy_rec cons);
    1.37 +  val copy_stricts = map_filter one_strict (filter has_nonlazy_rec cons);
    1.38  end;
    1.39  
    1.40 -val copy_rews = copy_strict :: copy_apps @ copy_stricts;
    1.41 +val copy_rews = the_list copy_strict @ copy_apps @ copy_stricts;
    1.42  
    1.43  in
    1.44    thy
    1.45 @@ -721,47 +731,34 @@
    1.46          rtac @{thm iterate_below_fix} 1];
    1.47      in pg axs_take_def goal (K tacs) end;
    1.48    val take_stricts = map one_take_strict eqs;
    1.49 -  val take_stricts' = map (rewrite_rule copy_take_defs) take_stricts;
    1.50    fun take_0 n dn =
    1.51      let
    1.52 -      val goal = mk_trp ((dc_take dn $ %%: @{const_name Algebras.zero}) `% x_name n === UU);
    1.53 +      val goal = mk_trp ((dc_take dn $ @{term "0::nat"}) `% x_name n === UU);
    1.54      in pg axs_take_def goal (K [simp_tac iterate_Cprod_ss 1]) end;
    1.55    val take_0s = mapn take_0 1 dnames;
    1.56 -  fun c_UU_tac ctxt = case_UU_tac ctxt (take_stricts' @ copy_con_rews) 1;
    1.57 +  fun c_UU_tac ctxt = case_UU_tac ctxt (take_stricts @ con_rews) 1;
    1.58    val _ = trace " Proving take_apps...";
    1.59 -  val take_apps =
    1.60 +  fun one_take_app dn (con, args) =
    1.61      let
    1.62 -      fun mk_eqn dn (con, args) =
    1.63 -        let
    1.64 -          fun mk_take n = dc_take (List.nth (dnames, n)) $ %:"n";
    1.65 -          fun one_rhs arg =
    1.66 -              if Datatype_Aux.is_rec_type (dtyp_of arg)
    1.67 -              then Domain_Axioms.copy_of_dtyp map_tab
    1.68 -                     mk_take (dtyp_of arg) ` (%# arg)
    1.69 -              else (%# arg);
    1.70 -          val lhs = (dc_take dn $ (%%:"Suc" $ %:"n"))`(con_app con args);
    1.71 -          val rhs = con_app2 con one_rhs args;
    1.72 -        in Library.foldr mk_all (map vname args, lhs === rhs) end;
    1.73 -      fun mk_eqns ((dn, _), cons) = map (mk_eqn dn) cons;
    1.74 -      val goal = mk_trp (foldr1 mk_conj (maps mk_eqns eqs));
    1.75 -      val simps = filter (has_fewer_prems 1) copy_rews;
    1.76 -      fun con_tac ctxt (con, args) =
    1.77 -        if nonlazy_rec args = []
    1.78 -        then all_tac
    1.79 -        else EVERY (map (c_UU_tac ctxt) (nonlazy_rec args)) THEN
    1.80 -          asm_full_simp_tac (HOLCF_ss addsimps copy_rews) 1;
    1.81 -      fun eq_tacs ctxt ((dn, _), cons) = map (con_tac ctxt) cons;
    1.82 +      fun mk_take n = dc_take (List.nth (dnames, n)) $ %:"n";
    1.83 +      fun one_rhs arg =
    1.84 +          if Datatype_Aux.is_rec_type (dtyp_of arg)
    1.85 +          then Domain_Axioms.copy_of_dtyp map_tab
    1.86 +                 mk_take (dtyp_of arg) ` (%# arg)
    1.87 +          else (%# arg);
    1.88 +      val lhs = (dc_take dn $ (%%:"Suc" $ %:"n"))`(con_app con args);
    1.89 +      val rhs = con_app2 con one_rhs args;
    1.90 +      val goal = mk_trp (lhs === rhs);
    1.91        fun tacs ctxt =
    1.92 -        simp_tac iterate_Cprod_ss 1 ::
    1.93 -        InductTacs.induct_tac ctxt [[SOME "n"]] 1 ::
    1.94 -        simp_tac (iterate_Cprod_ss addsimps copy_con_rews) 1 ::
    1.95 -        asm_full_simp_tac (HOLCF_ss addsimps simps) 1 ::
    1.96 -        TRY (safe_tac HOL_cs) ::
    1.97 -        maps (eq_tacs ctxt) eqs;
    1.98 -    in pg copy_take_defs goal tacs end;
    1.99 +        map (c_UU_tac ctxt) (nonlazy_rec args) @ [
   1.100 +        rewrite_goals_tac copy_take_defs,
   1.101 +        asm_simp_tac (HOLCF_ss addsimps copy_con_rews) 1];
   1.102 +    in pg [] goal tacs end;
   1.103 +  fun one_take_apps ((dn, _), cons) = map (one_take_app dn) cons;
   1.104 +  val take_apps = maps one_take_apps eqs;
   1.105  in
   1.106    val take_rews = map Drule.standard
   1.107 -    (take_stricts @ take_0s @ atomize global_ctxt take_apps);
   1.108 +    (take_stricts @ take_0s @ take_apps);
   1.109  end; (* local *)
   1.110  
   1.111  local