# HG changeset patch
# User huffman
# Date 1130973369 -3600
# Node ID 940c2c0ff33a399720866f7dbb2c142f98aa6332
# Parent  b653e18f0a4121de55a7928b67f05d250e77520d
cleaned up; chain_const and thelub_const are simp rules

diff -r b653e18f0a41 -r 940c2c0ff33a src/HOLCF/Porder.thy
--- a/src/HOLCF/Porder.thy	Thu Nov 03 00:12:29 2005 +0100
+++ b/src/HOLCF/Porder.thy	Thu Nov 03 00:16:09 2005 +0100
@@ -51,41 +51,41 @@
 
 subsection {* Chains and least upper bounds *}
 
-consts  
-        "<|"    ::      "['a set,'a::po] \<Rightarrow> bool"       (infixl "<|" 55)
-        "<<|"   ::      "['a set,'a::po] \<Rightarrow> bool"       (infixl "<<|" 55)
-        lub     ::      "'a set \<Rightarrow> 'a::po"
-        tord ::      "'a::po set \<Rightarrow> bool"
-        chain ::     "(nat \<Rightarrow> 'a::po) \<Rightarrow> bool"
-        max_in_chain :: "[nat,nat\<Rightarrow>'a::po]\<Rightarrow>bool"
-        finite_chain :: "(nat\<Rightarrow>'a::po)\<Rightarrow>bool"
+constdefs  
+
+  -- {* class definitions *}
+  is_ub :: "['a set, 'a::po] \<Rightarrow> bool"       (infixl "<|" 55)
+  "S <| x \<equiv> \<forall>y. y \<in> S \<longrightarrow> y \<sqsubseteq> x"
+
+  is_lub :: "['a set, 'a::po] \<Rightarrow> bool"       (infixl "<<|" 55)
+  "S <<| x \<equiv> S <| x \<and> (\<forall>u. S <| u \<longrightarrow> x \<sqsubseteq> u)"
+
+  -- {* Arbitrary chains are total orders *}
+  tord :: "'a::po set \<Rightarrow> bool"
+  "tord S \<equiv> \<forall>x y. x \<in> S \<and> y \<in> S \<longrightarrow> (x \<sqsubseteq> y \<or> y \<sqsubseteq> x)"
+
+  -- {* Here we use countable chains and I prefer to code them as functions! *}
+  chain :: "(nat \<Rightarrow> 'a::po) \<Rightarrow> bool"
+  "chain F \<equiv> \<forall>i. F i \<sqsubseteq> F (Suc i)"
+
+  -- {* finite chains, needed for monotony of continuous functions *}
+  max_in_chain :: "[nat, nat \<Rightarrow> 'a::po] \<Rightarrow> bool"
+  "max_in_chain i C \<equiv> \<forall>j. i \<le> j \<longrightarrow> C i = C j" 
+
+  finite_chain :: "(nat \<Rightarrow> 'a::po) \<Rightarrow> bool"
+  "finite_chain C \<equiv> chain(C) \<and> (\<exists>i. max_in_chain i C)"
+
+  lub :: "'a set \<Rightarrow> 'a::po"
+  "lub S \<equiv> THE x. S <<| x"
 
 syntax
   "@LUB"	:: "('b \<Rightarrow> 'a) \<Rightarrow> 'a"	(binder "LUB " 10)
 
-translations
-  "LUB x. t"	== "lub(range(%x. t))"
-
 syntax (xsymbols)
-  "LUB "	:: "[idts, 'a] \<Rightarrow> 'a"		("(3\<Squnion>_./ _)"[0,10] 10)
-
-defs
-
--- {* class definitions *}
-is_ub_def:       "S <| x \<equiv> \<forall>y. y \<in> S \<longrightarrow> y \<sqsubseteq> x"
-is_lub_def:      "S <<| x \<equiv> S <| x \<and> (\<forall>u. S <| u \<longrightarrow> x \<sqsubseteq> u)"
+  "LUB "	:: "[idts, 'a] \<Rightarrow> 'a"		("(3\<Squnion>_./ _)" [0,10] 10)
 
--- {* Arbitrary chains are total orders *}
-tord_def:     "tord S \<equiv> \<forall>x y. x \<in> S \<and> y \<in> S \<longrightarrow> (x \<sqsubseteq> y \<or> y \<sqsubseteq> x)"
-
--- {* Here we use countable chains and I prefer to code them as functions! *}
-chain_def:        "chain F \<equiv> \<forall>i. F i \<sqsubseteq> F (Suc i)"
-
--- {* finite chains, needed for monotony of continuous functions *}
-max_in_chain_def: "max_in_chain i C \<equiv> \<forall>j. i \<le> j \<longrightarrow> C i = C j" 
-finite_chain_def: "finite_chain C \<equiv> chain(C) \<and> (\<exists>i. max_in_chain i C)"
-
-lub_def:          "lub S \<equiv> THE x. S <<| x"
+translations
+  "\<Squnion>n. t" == "lub(range(\<lambda>n. t))"
 
 text {* lubs are unique *}
 
@@ -229,12 +229,13 @@
 
 text {* the lub of a constant chain is the constant *}
 
-lemma chain_const: "chain (\<lambda>i. c)"
+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)
 
-lemmas thelub_const = lub_const [THEN thelubI, standard]
+lemma thelub_const [simp]: "(\<Squnion>i. c) = c"
+by (rule lub_const [THEN thelubI])
 
-end 
+end