1.1 --- a/src/HOLCF/Tools/Domain/domain_theorems.ML	Thu Jan 28 11:48:49 2010 +0100
     1.2 +++ b/src/HOLCF/Tools/Domain/domain_theorems.ML	Sun Feb 07 10:31:11 2010 -0800
     1.3 @@ -706,23 +706,28 @@
     1.4    val copy_take_defs =
     1.5      (if n_eqs = 1 then [] else [ax_copy2_def]) @ axs_take_def;
     1.6    val _ = trace " Proving take_stricts...";
     1.7 -  val take_stricts =
     1.8 +  fun one_take_strict ((dn, args), _) =
     1.9      let
    1.10 -      fun one_eq ((dn, args), _) = strict (dc_take dn $ %:"n");
    1.11 -      val goal = mk_trp (foldr1 mk_conj (map one_eq eqs));
    1.12 -      fun tacs ctxt = [
    1.13 -        InductTacs.induct_tac ctxt [[SOME "n"]] 1,
    1.14 -        simp_tac iterate_Cprod_ss 1,
    1.15 -        asm_simp_tac (iterate_Cprod_ss addsimps copy_rews) 1];
    1.16 -    in pg copy_take_defs goal tacs end;
    1.17 -
    1.18 -  val take_stricts' = rewrite_rule copy_take_defs take_stricts;
    1.19 +      val goal = mk_trp (strict (dc_take dn $ %:"n"));
    1.20 +      val rules = [
    1.21 +        @{thm monofun_fst [THEN monofunE]},
    1.22 +        @{thm monofun_snd [THEN monofunE]}];
    1.23 +      val tacs = [
    1.24 +        rtac @{thm UU_I} 1,
    1.25 +        rtac @{thm below_eq_trans} 1,
    1.26 +        resolve_tac axs_reach 2,
    1.27 +        rtac @{thm monofun_cfun_fun} 1,
    1.28 +        REPEAT (resolve_tac rules 1),
    1.29 +        rtac @{thm iterate_below_fix} 1];
    1.30 +    in pg axs_take_def goal (K tacs) end;
    1.31 +  val take_stricts = map one_take_strict eqs;
    1.32 +  val take_stricts' = map (rewrite_rule copy_take_defs) take_stricts;
    1.33    fun take_0 n dn =
    1.34      let
    1.35        val goal = mk_trp ((dc_take dn $ %%: @{const_name Algebras.zero}) `% x_name n === UU);
    1.36      in pg axs_take_def goal (K [simp_tac iterate_Cprod_ss 1]) end;
    1.37    val take_0s = mapn take_0 1 dnames;
    1.38 -  fun c_UU_tac ctxt = case_UU_tac ctxt (take_stricts'::copy_con_rews) 1;
    1.39 +  fun c_UU_tac ctxt = case_UU_tac ctxt (take_stricts' @ copy_con_rews) 1;
    1.40    val _ = trace " Proving take_apps...";
    1.41    val take_apps =
    1.42      let
    1.43 @@ -756,7 +761,7 @@
    1.44      in pg copy_take_defs goal tacs end;
    1.45  in
    1.46    val take_rews = map Drule.standard
    1.47 -    (atomize global_ctxt take_stricts @ take_0s @ atomize global_ctxt take_apps);
    1.48 +    (take_stricts @ take_0s @ atomize global_ctxt take_apps);
    1.49  end; (* local *)
    1.50  
    1.51  local