1.1 --- a/src/HOLCF/Porder.thy	Sun Jun 22 23:02:40 2008 +0200
     1.2 +++ b/src/HOLCF/Porder.thy	Sun Jun 22 23:08:32 2008 +0200
     1.3 @@ -6,7 +6,7 @@
     1.4  header {* Partial orders *}
     1.5  
     1.6  theory Porder
     1.7 -imports Datatype Finite_Set
     1.8 +imports Main
     1.9  begin
    1.10  
    1.11  subsection {* Type class for partial orders *}
    1.12 @@ -178,25 +178,14 @@
    1.13  
    1.14  text {* chains are monotone functions *}
    1.15  
    1.16 -lemma chain_mono:
    1.17 -  assumes Y: "chain Y"
    1.18 -  shows "i \<le> j \<Longrightarrow> Y i \<sqsubseteq> Y j"
    1.19 -apply (induct j)
    1.20 -apply simp
    1.21 -apply (erule le_SucE)
    1.22 -apply (rule trans_less [OF _ chainE [OF Y]])
    1.23 -apply simp
    1.24 -apply simp
    1.25 -done
    1.26 +lemma chain_mono_less: "\<lbrakk>chain Y; i < j\<rbrakk> \<Longrightarrow> Y i \<sqsubseteq> Y j"
    1.27 +by (erule less_Suc_induct, erule chainE, erule trans_less)
    1.28  
    1.29 -lemma chain_mono_less: "\<lbrakk>chain Y; i < j\<rbrakk> \<Longrightarrow> Y i \<sqsubseteq> Y j"
    1.30 -by (erule chain_mono, simp)
    1.31 +lemma chain_mono: "\<lbrakk>chain Y; i \<le> j\<rbrakk> \<Longrightarrow> Y i \<sqsubseteq> Y j"
    1.32 +by (cases "i = j", simp, simp add: chain_mono_less)
    1.33  
    1.34  lemma chain_shift: "chain Y \<Longrightarrow> chain (\<lambda>i. Y (i + j))"
    1.35 -apply (rule chainI)
    1.36 -apply simp
    1.37 -apply (erule chainE)
    1.38 -done
    1.39 +by (rule chainI, simp, erule chainE)
    1.40  
    1.41  text {* technical lemmas about (least) upper bounds of chains *}
    1.42  
    1.43 @@ -230,37 +219,6 @@
    1.44  lemma thelub_const [simp]: "(\<Squnion>i. c) = c"
    1.45  by (rule lub_const [THEN thelubI])
    1.46  
    1.47 -subsection {* Totally ordered sets *}
    1.48 -
    1.49 -definition
    1.50 -  -- {* Arbitrary chains are total orders *}
    1.51 -  tord :: "'a::po set \<Rightarrow> bool" where
    1.52 -  "tord S = (\<forall>x y. x \<in> S \<and> y \<in> S \<longrightarrow> (x \<sqsubseteq> y \<or> y \<sqsubseteq> x))"
    1.53 -
    1.54 -text {* The range of a chain is a totally ordered *}
    1.55 -
    1.56 -lemma chain_tord: "chain Y \<Longrightarrow> tord (range Y)"
    1.57 -unfolding tord_def
    1.58 -apply (clarify, rename_tac i j)
    1.59 -apply (rule_tac x=i and y=j in linorder_le_cases)
    1.60 -apply (fast intro: chain_mono)+
    1.61 -done
    1.62 -
    1.63 -lemma finite_tord_has_max:
    1.64 -  "\<lbrakk>finite S; S \<noteq> {}; tord S\<rbrakk> \<Longrightarrow> \<exists>y\<in>S. \<forall>x\<in>S. x \<sqsubseteq> y"
    1.65 - apply (induct S rule: finite_ne_induct)
    1.66 -  apply simp
    1.67 - apply (drule meta_mp, simp add: tord_def)
    1.68 - apply (erule bexE, rename_tac z)
    1.69 - apply (subgoal_tac "x \<sqsubseteq> z \<or> z \<sqsubseteq> x")
    1.70 -  apply (erule disjE)
    1.71 -   apply (rule_tac x="z" in bexI, simp, simp)
    1.72 -  apply (rule_tac x="x" in bexI)
    1.73 -   apply (clarsimp elim!: rev_trans_less)
    1.74 -  apply simp
    1.75 - apply (simp add: tord_def)
    1.76 -done
    1.77 -
    1.78  subsection {* Finite chains *}
    1.79  
    1.80  definition
    1.81 @@ -280,6 +238,14 @@
    1.82  lemma max_in_chainD: "\<lbrakk>max_in_chain i Y; i \<le> j\<rbrakk> \<Longrightarrow> Y i = Y j"
    1.83  unfolding max_in_chain_def by fast
    1.84  
    1.85 +lemma finite_chainI:
    1.86 +  "\<lbrakk>chain C; max_in_chain i C\<rbrakk> \<Longrightarrow> finite_chain C"
    1.87 +unfolding finite_chain_def by fast
    1.88 +
    1.89 +lemma finite_chainE:
    1.90 +  "\<lbrakk>finite_chain C; \<And>i. \<lbrakk>chain C; max_in_chain i C\<rbrakk> \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R"
    1.91 +unfolding finite_chain_def by fast
    1.92 +
    1.93  lemma lub_finch1: "\<lbrakk>chain C; max_in_chain i C\<rbrakk> \<Longrightarrow> range C <<| C i"
    1.94  apply (rule is_lubI)
    1.95  apply (rule ub_rangeI, rename_tac j)
    1.96 @@ -290,35 +256,59 @@
    1.97  done
    1.98  
    1.99  lemma lub_finch2:
   1.100 -        "finite_chain C \<Longrightarrow> range C <<| C (LEAST i. max_in_chain i C)"
   1.101 -apply (unfold finite_chain_def)
   1.102 -apply (erule conjE)
   1.103 -apply (erule LeastI2_ex)
   1.104 +  "finite_chain C \<Longrightarrow> range C <<| C (LEAST i. max_in_chain i C)"
   1.105 +apply (erule finite_chainE)
   1.106 +apply (erule LeastI2 [where Q="\<lambda>i. range C <<| C i"])
   1.107  apply (erule (1) lub_finch1)
   1.108  done
   1.109  
   1.110  lemma finch_imp_finite_range: "finite_chain Y \<Longrightarrow> finite (range Y)"
   1.111 - apply (unfold finite_chain_def, clarify)
   1.112 - apply (rule_tac f="Y" and n="Suc i" in nat_seg_image_imp_finite)
   1.113 - apply (rule equalityI)
   1.114 + apply (erule finite_chainE)
   1.115 + apply (rule_tac B="Y ` {..i}" in finite_subset)
   1.116    apply (rule subsetI)
   1.117    apply (erule rangeE, rename_tac j)
   1.118    apply (rule_tac x=i and y=j in linorder_le_cases)
   1.119     apply (subgoal_tac "Y j = Y i", simp)
   1.120     apply (simp add: max_in_chain_def)
   1.121    apply simp
   1.122 - apply fast
   1.123 + apply simp
   1.124  done
   1.125  
   1.126 +lemma finite_range_has_max:
   1.127 +  fixes f :: "nat \<Rightarrow> 'a" and r :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
   1.128 +  assumes mono: "\<And>i j. i \<le> j \<Longrightarrow> r (f i) (f j)"
   1.129 +  assumes finite_range: "finite (range f)"
   1.130 +  shows "\<exists>k. \<forall>i. r (f i) (f k)"
   1.131 +proof (intro exI allI)
   1.132 +  fix i :: nat
   1.133 +  let ?j = "LEAST k. f k = f i"
   1.134 +  let ?k = "Max ((\<lambda>x. LEAST k. f k = x) ` range f)"
   1.135 +  have "?j \<le> ?k"
   1.136 +  proof (rule Max_ge)
   1.137 +    show "finite ((\<lambda>x. LEAST k. f k = x) ` range f)"
   1.138 +      using finite_range by (rule finite_imageI)
   1.139 +    show "?j \<in> (\<lambda>x. LEAST k. f k = x) ` range f"
   1.140 +      by (intro imageI rangeI)
   1.141 +  qed
   1.142 +  hence "r (f ?j) (f ?k)"
   1.143 +    by (rule mono)
   1.144 +  also have "f ?j = f i"
   1.145 +    by (rule LeastI, rule refl)
   1.146 +  finally show "r (f i) (f ?k)" .
   1.147 +qed
   1.148 +
   1.149  lemma finite_range_imp_finch:
   1.150    "\<lbrakk>chain Y; finite (range Y)\<rbrakk> \<Longrightarrow> finite_chain Y"
   1.151 - apply (subgoal_tac "\<exists>y\<in>range Y. \<forall>x\<in>range Y. x \<sqsubseteq> y")
   1.152 -  apply (clarsimp, rename_tac i)
   1.153 -  apply (subgoal_tac "max_in_chain i Y")
   1.154 -   apply (simp add: finite_chain_def exI)
   1.155 -  apply (simp add: max_in_chain_def po_eq_conv chain_mono)
   1.156 - apply (erule finite_tord_has_max, simp)
   1.157 - apply (erule chain_tord)
   1.158 + apply (subgoal_tac "\<exists>k. \<forall>i. Y i \<sqsubseteq> Y k")
   1.159 +  apply (erule exE)
   1.160 +  apply (rule finite_chainI, assumption)
   1.161 +  apply (rule max_in_chainI)
   1.162 +  apply (rule antisym_less)
   1.163 +   apply (erule (1) chain_mono)
   1.164 +  apply (erule spec)
   1.165 + apply (rule finite_range_has_max)
   1.166 +  apply (erule (1) chain_mono)
   1.167 + apply assumption
   1.168  done
   1.169  
   1.170  lemma bin_chain: "x \<sqsubseteq> y \<Longrightarrow> chain (\<lambda>i. if i=0 then x else y)"