merged

--- a/src/HOL/Library/Infinite_Set.thy	Mon Feb 08 21:28:27 2010 +0100
+++ b/src/HOL/Library/Infinite_Set.thy	Mon Feb 08 15:54:01 2010 -0800
@@ -192,10 +192,11 @@
     by (auto simp add: infinite_nat_iff_unbounded)
 qed
 
-lemma nat_infinite [simp]: "infinite (UNIV :: nat set)"
+(* duplicates Finite_Set.infinite_UNIV_nat *)
+lemma nat_infinite: "infinite (UNIV :: nat set)"
   by (auto simp add: infinite_nat_iff_unbounded)
 
-lemma nat_not_finite [elim]: "finite (UNIV::nat set) \<Longrightarrow> R"
+lemma nat_not_finite: "finite (UNIV::nat set) \<Longrightarrow> R"
   by simp
 
 text {*

--- a/src/HOLCF/Fix.thy	Mon Feb 08 21:28:27 2010 +0100
+++ b/src/HOLCF/Fix.thy	Mon Feb 08 15:54:01 2010 -0800
@@ -73,6 +73,10 @@
 apply simp
 done
 
+lemma iterate_below_fix: "iterate n\<cdot>f\<cdot>\<bottom> \<sqsubseteq> fix\<cdot>f"
+  unfolding fix_def2
+  using chain_iterate by (rule is_ub_thelub)
+
 text {*
   Kleene's fixed point theorems for continuous functions in pointed
   omega cpo's

--- a/src/HOLCF/Tools/Domain/domain_theorems.ML	Mon Feb 08 21:28:27 2010 +0100
+++ b/src/HOLCF/Tools/Domain/domain_theorems.ML	Mon Feb 08 15:54:01 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) =
@@ -605,6 +610,9 @@
                  (proj (%:"f") eqs) (dtyp_of arg) ` (%# arg)
           else (%# arg);
       val rhs = con_app2 con one_rhs args;
+      fun is_rec arg = Datatype_Aux.is_rec_type (dtyp_of arg);
+      fun is_nonlazy_rec arg = is_rec arg andalso not (is_lazy arg);
+      fun nonlazy_rec args = map vname (filter is_nonlazy_rec args);
       val goal = lift_defined %: (nonlazy_rec args, mk_trp (lhs === rhs));
       val args' = filter_out (fn a => is_rec a orelse is_lazy a) args;
       val stricts = abs_strict :: rep_strict :: @{thms domain_map_stricts};
@@ -621,18 +629,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
@@ -706,57 +719,48 @@
   val copy_take_defs =
     (if n_eqs = 1 then [] else [ax_copy2_def]) @ axs_take_def;
   val _ = trace " Proving take_stricts...";
-  val take_stricts =
+  fun one_take_strict ((dn, args), _) =
     let
-      fun one_eq ((dn, args), _) = strict (dc_take dn $ %:"n");
-      val goal = mk_trp (foldr1 mk_conj (map one_eq eqs));
-      fun tacs ctxt = [
-        InductTacs.induct_tac ctxt [[SOME "n"]] 1,
-        simp_tac iterate_Cprod_ss 1,
-        asm_simp_tac (iterate_Cprod_ss addsimps copy_rews) 1];
-    in pg copy_take_defs goal tacs end;
-
-  val take_stricts' = rewrite_rule copy_take_defs take_stricts;
+      val goal = mk_trp (strict (dc_take dn $ %:"n"));
+      val rules = [
+        @{thm monofun_fst [THEN monofunE]},
+        @{thm monofun_snd [THEN monofunE]}];
+      val tacs = [
+        rtac @{thm UU_I} 1,
+        rtac @{thm below_eq_trans} 1,
+        resolve_tac axs_reach 2,
+        rtac @{thm monofun_cfun_fun} 1,
+        REPEAT (resolve_tac rules 1),
+        rtac @{thm iterate_below_fix} 1];
+    in pg axs_take_def goal (K tacs) end;
+  val take_stricts = map one_take_strict eqs;
   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;
   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 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;
+      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;
+      fun is_rec arg = Datatype_Aux.is_rec_type (dtyp_of arg);
+      fun is_nonlazy_rec arg = is_rec arg andalso not (is_lazy arg);
+      fun nonlazy_rec args = map vname (filter is_nonlazy_rec args);
+      val goal = lift_defined %: (nonlazy_rec args, mk_trp (lhs === rhs));
+      val tacs = [asm_simp_tac (HOLCF_ss addsimps copy_con_rews) 1];
+    in pg copy_take_defs goal (K 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.export_without_context
-    (atomize global_ctxt take_stricts @ take_0s @ atomize global_ctxt take_apps);
+    (take_stricts @ take_0s @ take_apps);
 end; (* local *)
 
 local