# HG changeset patch
# User huffman
# Date 1267681362 28800
# Node ID 44eeda8cb70821ea0b8b667f3daaa740a61d061f
# Parent  20995afa8fa16be3d6f3261f2201d6320543fb0d
generate lemma take_below, declare chain_take [simp]

diff -r 20995afa8fa1 -r 44eeda8cb708 src/HOLCF/FOCUS/Fstreams.thy
--- a/src/HOLCF/FOCUS/Fstreams.thy	Wed Mar 03 20:20:41 2010 -0800
+++ b/src/HOLCF/FOCUS/Fstreams.thy	Wed Mar 03 21:42:42 2010 -0800
@@ -240,7 +240,6 @@
      ==> (EX j t. Y j = <a> ooo t) & (EX X. chain X & (ALL i. EX j. <a> ooo X i << Y j) & (LUB i. X i) = s)"
 apply (auto simp add: fstreams_lub_lemma1)
 apply (rule_tac x="%n. stream_take n$s" in exI, auto)
-apply (simp add: chain_stream_take)
 apply (induct_tac i, auto)
 apply (drule fstreams_lub_lemma1, auto)
 apply (rule_tac x="j" in exI, auto)
@@ -293,7 +292,6 @@
       ==> (EX j t. Y j = (a, <m> ooo t)) & (EX X. chain X & (ALL i. EX j. (a, <m> ooo X i) << Y j) & (LUB i. X i) = ms)"
 apply (auto simp add: fstreams_lub_lemma2)
 apply (rule_tac x="%n. stream_take n$ms" in exI, auto)
-apply (simp add: chain_stream_take)
 apply (induct_tac i, auto)
 apply (drule fstreams_lub_lemma2, auto)
 apply (rule_tac x="j" in exI, auto)
diff -r 20995afa8fa1 -r 44eeda8cb708 src/HOLCF/Tools/Domain/domain_take_proofs.ML
--- a/src/HOLCF/Tools/Domain/domain_take_proofs.ML	Wed Mar 03 20:20:41 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_take_proofs.ML	Wed Mar 03 21:42:42 2010 -0800
@@ -262,9 +262,13 @@
         val goal = mk_trp (mk_chain take_const);
         val rules = take_defs @ @{thms chain_iterate ch2ch_fst ch2ch_snd};
         val tac = simp_tac (HOL_basic_ss addsimps rules) 1;
-        val chain_take_thm = Goal.prove_global thy [] [] goal (K tac);
+        val thm = Goal.prove_global thy [] [] goal (K tac);
       in
-        add_qualified_thm "chain_take" (dname, chain_take_thm) thy
+        thy
+          |> Sign.add_path dname
+          |> yield_singleton PureThy.add_thms
+              ((Binding.name "chain_take", thm), [Simplifier.simp_add])
+          ||> Sign.parent_path
       end;
     val (chain_take_thms, thy) =
       fold_map prove_chain_take (take_consts ~~ dnames) thy;
@@ -342,17 +346,17 @@
           (conjuncts dnames deflation_take_thm)) thy;
 
     (* prove strictness of take functions *)
-    fun prove_take_strict (take_const, dname) thy =
+    fun prove_take_strict (deflation_take, dname) thy =
       let
-        val goal = mk_trp (mk_strict (take_const $ Free ("n", natT)));
-        val tac = rtac @{thm deflation_strict} 1
-                  THEN resolve_tac deflation_take_thms 1;
-        val take_strict_thm = Goal.prove_global thy [] [] goal (K tac);
+        val take_strict_thm =
+            Drule.export_without_context
+            (@{thm deflation_strict} OF [deflation_take]);
       in
         add_qualified_thm "take_strict" (dname, take_strict_thm) thy
       end;
     val (take_strict_thms, thy) =
-      fold_map prove_take_strict (take_consts ~~ dnames) thy;
+      fold_map prove_take_strict
+        (deflation_take_thms ~~ dnames) thy;
 
     (* prove take/take rules *)
     fun prove_take_take ((chain_take, deflation_take), dname) thy =
@@ -367,6 +371,19 @@
       fold_map prove_take_take
         (chain_take_thms ~~ deflation_take_thms ~~ dnames) thy;
 
+    (* prove take_below rules *)
+    fun prove_take_below (deflation_take, dname) thy =
+      let
+        val take_below_thm =
+            Drule.export_without_context
+            (@{thm deflation.below} OF [deflation_take]);
+      in
+        add_qualified_thm "take_below" (dname, take_below_thm) thy
+      end;
+    val (take_below_thms, thy) =
+      fold_map prove_take_below
+        (deflation_take_thms ~~ dnames) thy;
+
     (* define finiteness predicates *)
     fun define_finite_const ((tbind, take_const), (lhsT, rhsT)) thy =
       let