new lemmas max_in_chainI, max_in_chainD
authorhuffman
Thu Jan 10 05:11:09 2008 +0100 (2008-01-10)
changeset 25878bfd53f791c10
parent 25877 6a549c03b28b
child 25879 98b93782c3b1
new lemmas max_in_chainI, max_in_chainD
src/HOLCF/Porder.thy
     1.1 --- a/src/HOLCF/Porder.thy	Wed Jan 09 20:25:18 2008 +0100
     1.2 +++ b/src/HOLCF/Porder.thy	Thu Jan 10 05:11:09 2008 +0100
     1.3 @@ -273,12 +273,17 @@
     1.4  
     1.5  text {* results about finite chains *}
     1.6  
     1.7 +lemma max_in_chainI: "(\<And>j. i \<le> j \<Longrightarrow> Y i = Y j) \<Longrightarrow> max_in_chain i Y"
     1.8 +unfolding max_in_chain_def by fast
     1.9 +
    1.10 +lemma max_in_chainD: "\<lbrakk>max_in_chain i Y; i \<le> j\<rbrakk> \<Longrightarrow> Y i = Y j"
    1.11 +unfolding max_in_chain_def by fast
    1.12 +
    1.13  lemma lub_finch1: "\<lbrakk>chain C; max_in_chain i C\<rbrakk> \<Longrightarrow> range C <<| C i"
    1.14 -apply (unfold max_in_chain_def)
    1.15  apply (rule is_lubI)
    1.16  apply (rule ub_rangeI, rename_tac j)
    1.17  apply (rule_tac x=i and y=j in linorder_le_cases)
    1.18 -apply simp
    1.19 +apply (drule (1) max_in_chainD, simp)
    1.20  apply (erule (1) chain_mono3)
    1.21  apply (erule ub_rangeD)
    1.22  done