# HG changeset patch
# User huffman
# Date 1147400402 -7200
# Node ID 475140eb82f2badd2137c3d271492f1e08a7fdf4
# Parent  ccd6de95f4a60274c6c699939895fe26e604659e
add new finite chain theorems

diff -r ccd6de95f4a6 -r 475140eb82f2 src/HOLCF/Porder.thy
--- a/src/HOLCF/Porder.thy	Fri May 12 01:01:08 2006 +0200
+++ b/src/HOLCF/Porder.thy	Fri May 12 04:20:02 2006 +0200
@@ -6,7 +6,7 @@
 header {* Partial orders *}
 
 theory Porder
-imports Datatype
+imports Finite_Set
 begin
 
 subsection {* Type class for partial orders *}
@@ -212,6 +212,47 @@
 apply (erule (1) lub_finch1)
 done
 
+lemma finch_imp_finite_range: "finite_chain Y \<Longrightarrow> finite (range Y)"
+ apply (unfold finite_chain_def, clarify)
+ apply (rule_tac f="Y" and n="Suc i" in nat_seg_image_imp_finite)
+ apply (rule equalityI)
+  apply (rule subsetI)
+  apply (erule rangeE, rename_tac j)
+  apply (rule_tac x=i and y=j in linorder_le_cases)
+   apply (subgoal_tac "Y j = Y i", simp)
+   apply (simp add: max_in_chain_def)
+  apply simp
+ apply fast
+done
+
+lemma finite_tord_has_max [rule_format]:
+  "finite S \<Longrightarrow> S \<noteq> {} \<longrightarrow> tord S \<longrightarrow> (\<exists>y\<in>S. \<forall>x\<in>S. x \<sqsubseteq> y)"
+ apply (erule finite_induct, simp)
+ apply (rename_tac a S, clarify)
+ apply (case_tac "S = {}", simp)
+ apply (drule (1) mp)
+ apply (drule mp, simp add: tord_def)
+ apply (erule bexE, rename_tac z)
+ apply (subgoal_tac "a \<sqsubseteq> z \<or> z \<sqsubseteq> a")
+  apply (erule disjE)
+   apply (rule_tac x="z" in bexI, simp, simp)
+  apply (rule_tac x="a" in bexI)
+   apply (clarsimp elim!: rev_trans_less)
+  apply simp
+ apply (simp add: tord_def)
+done
+
+lemma finite_range_imp_finch:
+  "\<lbrakk>chain Y; finite (range Y)\<rbrakk> \<Longrightarrow> finite_chain Y"
+ apply (subgoal_tac "\<exists>y\<in>range Y. \<forall>x\<in>range Y. x \<sqsubseteq> y")
+  apply (clarsimp, rename_tac i)
+  apply (subgoal_tac "max_in_chain i Y")
+   apply (simp add: finite_chain_def exI)
+  apply (simp add: max_in_chain_def po_eq_conv chain_mono3)
+ apply (erule finite_tord_has_max, simp)
+ apply (erule chain_tord)
+done
+
 lemma bin_chain: "x \<sqsubseteq> y \<Longrightarrow> chain (\<lambda>i. if i=0 then x else y)"
 by (rule chainI, simp)