# HG changeset patch
# User huffman
# Date 1198001731 -3600
# Node ID 7025a263aa490cd282c0819e4eee14fb9580d1ba
# Parent  cbb59ba6bf0c1f2cc70cd76d7e081c1eabfb6eac
rearrange into subsections

diff -r cbb59ba6bf0c -r 7025a263aa49 src/HOLCF/Porder.thy
--- a/src/HOLCF/Porder.thy	Tue Dec 18 18:39:00 2007 +0100
+++ b/src/HOLCF/Porder.thy	Tue Dec 18 19:15:31 2007 +0100
@@ -56,9 +56,7 @@
   sq_ord_less_eq_trans
   sq_ord_eq_less_trans
 
-subsection {* Chains and least upper bounds *}
-
-text {* class definitions *}
+subsection {* Least upper bounds *}
 
 definition
   is_ub :: "['a set, 'a::po] \<Rightarrow> bool"  (infixl "<|" 55)  where
@@ -69,25 +67,6 @@
   "(S <<| x) = (S <| x \<and> (\<forall>u. S <| u \<longrightarrow> x \<sqsubseteq> u))"
 
 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))"
-
-definition
-  -- {* Here we use countable chains and I prefer to code them as functions! *}
-  chain :: "(nat \<Rightarrow> 'a::po) \<Rightarrow> bool" where
-  "chain F = (\<forall>i. F i \<sqsubseteq> F (Suc i))"
-
-definition
-  -- {* finite chains, needed for monotony of continuous functions *}
-  max_in_chain :: "[nat, nat \<Rightarrow> 'a::po] \<Rightarrow> bool" where
-  "max_in_chain i C = (\<forall>j. i \<le> j \<longrightarrow> C i = C j)"
-
-definition
-  finite_chain :: "(nat \<Rightarrow> 'a::po) \<Rightarrow> bool" where
-  "finite_chain C = (chain C \<and> (\<exists>i. max_in_chain i C))"
-
-definition
   lub :: "'a set \<Rightarrow> 'a::po" where
   "lub S = (THE x. S <<| x)"
 
@@ -106,28 +85,6 @@
 apply (blast intro: antisym_less)
 done
 
-text {* chains are monotone functions *}
-
-lemma chain_mono [rule_format]: "chain F \<Longrightarrow> x < y \<longrightarrow> F x \<sqsubseteq> F y"
-apply (unfold chain_def)
-apply (induct_tac y)
-apply simp
-apply (blast elim: less_SucE intro: trans_less)
-done
-
-lemma chain_mono3: "\<lbrakk>chain F; x \<le> y\<rbrakk> \<Longrightarrow> F x \<sqsubseteq> F y"
-apply (drule le_imp_less_or_eq)
-apply (blast intro: chain_mono)
-done
-
-text {* The range of a chain is a totally ordered *}
-
-lemma chain_tord: "chain F \<Longrightarrow> tord (range F)"
-apply (unfold tord_def, clarify)
-apply (rule nat_less_cases)
-apply (fast intro: chain_mono)+
-done
-
 text {* technical lemmas about @{term lub} and @{term is_lub} *}
 
 lemma lubI: "M <<| x \<Longrightarrow> M <<| lub M"
@@ -154,6 +111,27 @@
 lemma is_lubI: "\<lbrakk>S <| x; \<And>u. S <| u \<Longrightarrow> x \<sqsubseteq> u\<rbrakk> \<Longrightarrow> S <<| x"
 by (unfold is_lub_def, fast)
 
+subsection {* Countable chains *}
+
+definition
+  -- {* Here we use countable chains and I prefer to code them as functions! *}
+  chain :: "(nat \<Rightarrow> 'a::po) \<Rightarrow> bool" where
+  "chain F = (\<forall>i. F i \<sqsubseteq> F (Suc i))"
+
+text {* chains are monotone functions *}
+
+lemma chain_mono [rule_format]: "chain F \<Longrightarrow> x < y \<longrightarrow> F x \<sqsubseteq> F y"
+apply (unfold chain_def)
+apply (induct_tac y)
+apply simp
+apply (blast elim: less_SucE intro: trans_less)
+done
+
+lemma chain_mono3: "\<lbrakk>chain F; x \<le> y\<rbrakk> \<Longrightarrow> F x \<sqsubseteq> F y"
+apply (drule le_imp_less_or_eq)
+apply (blast intro: chain_mono)
+done
+
 lemma chainE: "chain F \<Longrightarrow> F i \<sqsubseteq> F (Suc i)"
 by (unfold chain_def, simp)
 
@@ -193,6 +171,60 @@
   "chain S \<Longrightarrow> range (\<lambda>i. S (i + j)) <<| x = range S <<| x"
 by (simp add: is_lub_def is_ub_range_shift)
 
+text {* the lub of a constant chain is the constant *}
+
+lemma chain_const [simp]: "chain (\<lambda>i. c)"
+by (simp add: chainI)
+
+lemma lub_const: "range (\<lambda>x. c) <<| c"
+by (blast dest: ub_rangeD intro: is_lubI ub_rangeI)
+
+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 F \<Longrightarrow> tord (range F)"
+apply (unfold tord_def, clarify)
+apply (rule nat_less_cases)
+apply (fast intro: chain_mono)+
+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
+
+subsection {* Finite chains *}
+
+definition
+  -- {* finite chains, needed for monotony of continuous functions *}
+  max_in_chain :: "[nat, nat \<Rightarrow> 'a::po] \<Rightarrow> bool" where
+  "max_in_chain i C = (\<forall>j. i \<le> j \<longrightarrow> C i = C j)"
+
+definition
+  finite_chain :: "(nat \<Rightarrow> 'a::po) \<Rightarrow> bool" where
+  "finite_chain C = (chain C \<and> (\<exists>i. max_in_chain i C))"
+
 text {* results about finite chains *}
 
 lemma lub_finch1: "\<lbrakk>chain C; max_in_chain i C\<rbrakk> \<Longrightarrow> range C <<| C i"
@@ -226,23 +258,6 @@
  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")
@@ -274,15 +289,4 @@
 lemma lub_chain_maxelem: "\<lbrakk>Y i = c; \<forall>i. Y i \<sqsubseteq> c\<rbrakk> \<Longrightarrow> lub (range Y) = c"
 by (blast dest: ub_rangeD intro: thelubI is_lubI ub_rangeI)
 
-text {* the lub of a constant chain is the constant *}
-
-lemma chain_const [simp]: "chain (\<lambda>i. c)"
-by (simp add: chainI)
-
-lemma lub_const: "range (\<lambda>x. c) <<| c"
-by (blast dest: ub_rangeD intro: is_lubI ub_rangeI)
-
-lemma thelub_const [simp]: "(\<Squnion>i. c) = c"
-by (rule lub_const [THEN thelubI])
-
 end