# HG changeset patch
# User huffman
# Date 1213908239 -7200
# Node ID 274b806912598c346ee0958882988156b1ed462c
# Parent  3b0d7a417a8b181fcd4dcd8316d6d0be2832a521
add lemmas take_chain_less and take_chain_le

diff -r 3b0d7a417a8b -r 274b80691259 src/HOLCF/CompactBasis.thy
--- a/src/HOLCF/CompactBasis.thy	Thu Jun 19 22:27:10 2008 +0200
+++ b/src/HOLCF/CompactBasis.thy	Thu Jun 19 22:43:59 2008 +0200
@@ -136,6 +136,15 @@
   assumes take_chain: "take n a \<preceq> take (Suc n) a"
   assumes finite_range_take: "finite (range (take n))"
   assumes take_covers: "\<exists>n. take n a = a"
+begin
+
+lemma take_chain_less: "m < n \<Longrightarrow> take m a \<preceq> take n a"
+by (erule less_Suc_induct, rule take_chain, erule (1) r_trans)
+
+lemma take_chain_le: "m \<le> n \<Longrightarrow> take m a \<preceq> take n a"
+by (cases "m = n", simp add: r_refl, simp add: take_chain_less)
+
+end
 
 locale ideal_completion = basis_take +
   fixes principal :: "'a::type \<Rightarrow> 'b::cpo"