# HG changeset patch
# User huffman
# Date 1214168912 -7200
# Node ID 7f4ee574f29cda504231e6909e8d66eb006056a0
# Parent  9e74019041d4ea4145d9e619d29cca6f9ad9b4d3
cleaned up some proofs;
removed unused stuff about totally-ordered sets;
import Main

diff -r 9e74019041d4 -r 7f4ee574f29c src/HOLCF/Porder.thy
--- a/src/HOLCF/Porder.thy	Sun Jun 22 23:02:40 2008 +0200
+++ b/src/HOLCF/Porder.thy	Sun Jun 22 23:08:32 2008 +0200
@@ -6,7 +6,7 @@
 header {* Partial orders *}
 
 theory Porder
-imports Datatype Finite_Set
+imports Main
 begin
 
 subsection {* Type class for partial orders *}
@@ -178,25 +178,14 @@
 
 text {* chains are monotone functions *}
 
-lemma chain_mono:
-  assumes Y: "chain Y"
-  shows "i \<le> j \<Longrightarrow> Y i \<sqsubseteq> Y j"
-apply (induct j)
-apply simp
-apply (erule le_SucE)
-apply (rule trans_less [OF _ chainE [OF Y]])
-apply simp
-apply simp
-done
+lemma chain_mono_less: "\<lbrakk>chain Y; i < j\<rbrakk> \<Longrightarrow> Y i \<sqsubseteq> Y j"
+by (erule less_Suc_induct, erule chainE, erule trans_less)
 
-lemma chain_mono_less: "\<lbrakk>chain Y; i < j\<rbrakk> \<Longrightarrow> Y i \<sqsubseteq> Y j"
-by (erule chain_mono, simp)
+lemma chain_mono: "\<lbrakk>chain Y; i \<le> j\<rbrakk> \<Longrightarrow> Y i \<sqsubseteq> Y j"
+by (cases "i = j", simp, simp add: chain_mono_less)
 
 lemma chain_shift: "chain Y \<Longrightarrow> chain (\<lambda>i. Y (i + j))"
-apply (rule chainI)
-apply simp
-apply (erule chainE)
-done
+by (rule chainI, simp, erule chainE)
 
 text {* technical lemmas about (least) upper bounds of chains *}
 
@@ -230,37 +219,6 @@
 lemma thelub_const [simp]: "(\<Squnion>i. c) = c"
 by (rule lub_const [THEN thelubI])
 
-subsection {* Totally ordered sets *}
-
-definition
-  -- {* Arbitrary chains are total orders *}
-  tord :: "'a::po set \<Rightarrow> bool" where
-  "tord S = (\<forall>x y. x \<in> S \<and> y \<in> S \<longrightarrow> (x \<sqsubseteq> y \<or> y \<sqsubseteq> x))"
-
-text {* The range of a chain is a totally ordered *}
-
-lemma chain_tord: "chain Y \<Longrightarrow> tord (range Y)"
-unfolding tord_def
-apply (clarify, rename_tac i j)
-apply (rule_tac x=i and y=j in linorder_le_cases)
-apply (fast intro: chain_mono)+
-done
-
-lemma finite_tord_has_max:
-  "\<lbrakk>finite S; S \<noteq> {}; tord S\<rbrakk> \<Longrightarrow> \<exists>y\<in>S. \<forall>x\<in>S. x \<sqsubseteq> y"
- apply (induct S rule: finite_ne_induct)
-  apply simp
- apply (drule meta_mp, simp add: tord_def)
- apply (erule bexE, rename_tac z)
- apply (subgoal_tac "x \<sqsubseteq> z \<or> z \<sqsubseteq> x")
-  apply (erule disjE)
-   apply (rule_tac x="z" in bexI, simp, simp)
-  apply (rule_tac x="x" in bexI)
-   apply (clarsimp elim!: rev_trans_less)
-  apply simp
- apply (simp add: tord_def)
-done
-
 subsection {* Finite chains *}
 
 definition
@@ -280,6 +238,14 @@
 lemma max_in_chainD: "\<lbrakk>max_in_chain i Y; i \<le> j\<rbrakk> \<Longrightarrow> Y i = Y j"
 unfolding max_in_chain_def by fast
 
+lemma finite_chainI:
+  "\<lbrakk>chain C; max_in_chain i C\<rbrakk> \<Longrightarrow> finite_chain C"
+unfolding finite_chain_def by fast
+
+lemma finite_chainE:
+  "\<lbrakk>finite_chain C; \<And>i. \<lbrakk>chain C; max_in_chain i C\<rbrakk> \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R"
+unfolding finite_chain_def by fast
+
 lemma lub_finch1: "\<lbrakk>chain C; max_in_chain i C\<rbrakk> \<Longrightarrow> range C <<| C i"
 apply (rule is_lubI)
 apply (rule ub_rangeI, rename_tac j)
@@ -290,35 +256,59 @@
 done
 
 lemma lub_finch2:
-        "finite_chain C \<Longrightarrow> range C <<| C (LEAST i. max_in_chain i C)"
-apply (unfold finite_chain_def)
-apply (erule conjE)
-apply (erule LeastI2_ex)
+  "finite_chain C \<Longrightarrow> range C <<| C (LEAST i. max_in_chain i C)"
+apply (erule finite_chainE)
+apply (erule LeastI2 [where Q="\<lambda>i. range C <<| C i"])
 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 (erule finite_chainE)
+ apply (rule_tac B="Y ` {..i}" in finite_subset)
   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
+ apply simp
 done
 
+lemma finite_range_has_max:
+  fixes f :: "nat \<Rightarrow> 'a" and r :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
+  assumes mono: "\<And>i j. i \<le> j \<Longrightarrow> r (f i) (f j)"
+  assumes finite_range: "finite (range f)"
+  shows "\<exists>k. \<forall>i. r (f i) (f k)"
+proof (intro exI allI)
+  fix i :: nat
+  let ?j = "LEAST k. f k = f i"
+  let ?k = "Max ((\<lambda>x. LEAST k. f k = x) ` range f)"
+  have "?j \<le> ?k"
+  proof (rule Max_ge)
+    show "finite ((\<lambda>x. LEAST k. f k = x) ` range f)"
+      using finite_range by (rule finite_imageI)
+    show "?j \<in> (\<lambda>x. LEAST k. f k = x) ` range f"
+      by (intro imageI rangeI)
+  qed
+  hence "r (f ?j) (f ?k)"
+    by (rule mono)
+  also have "f ?j = f i"
+    by (rule LeastI, rule refl)
+  finally show "r (f i) (f ?k)" .
+qed
+
 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_mono)
- apply (erule finite_tord_has_max, simp)
- apply (erule chain_tord)
+ apply (subgoal_tac "\<exists>k. \<forall>i. Y i \<sqsubseteq> Y k")
+  apply (erule exE)
+  apply (rule finite_chainI, assumption)
+  apply (rule max_in_chainI)
+  apply (rule antisym_less)
+   apply (erule (1) chain_mono)
+  apply (erule spec)
+ apply (rule finite_range_has_max)
+  apply (erule (1) chain_mono)
+ apply assumption
 done
 
 lemma bin_chain: "x \<sqsubseteq> y \<Longrightarrow> chain (\<lambda>i. if i=0 then x else y)"