# 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 = ooo t) & (EX X. chain X & (ALL i. EX j. 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, ooo t)) & (EX X. chain X & (ALL i. EX j. (a, 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