# HG changeset patch
# User nipkow
# Date 1163355730 -3600
# Node ID 1d39091a3208210e6c78e1d72d8bd7c47b5eb4a0
# Parent  3556301c18cdeca4651e9c360d83aa5dc8acff5d
started reorgnization of lattice theories

diff -r 3556301c18cd -r 1d39091a3208 src/HOL/FixedPoint.thy
--- a/src/HOL/FixedPoint.thy	Sat Nov 11 23:58:46 2006 +0100
+++ b/src/HOL/FixedPoint.thy	Sun Nov 12 19:22:10 2006 +0100
@@ -12,42 +12,107 @@
 begin
 
 subsection {* Complete lattices *}
-
+(*FIXME Meet \<rightarrow> Inf *)
 consts
   Meet :: "'a::order set \<Rightarrow> 'a"
-  Join :: "'a::order set \<Rightarrow> 'a"
+  Sup :: "'a::order set \<Rightarrow> 'a"
+
+defs Sup_def: "Sup A == Meet {b. \<forall>a \<in> A. a <= b}"
 
-defs Join_def: "Join A == Meet {b. \<forall>a \<in> A. a <= b}"
-
+definition
+ SUP :: "('a \<Rightarrow> 'b::order) \<Rightarrow> 'b" (binder "SUP " 10)
+"SUP x. f x == Sup (f ` UNIV)"
+(*
+abbreviation
+ bot :: "'a::order"
+"bot == Sup {}"
+*)
 axclass comp_lat < order
   Meet_lower: "x \<in> A \<Longrightarrow> Meet A <= x"
   Meet_greatest: "(\<And>x. x \<in> A \<Longrightarrow> z <= x) \<Longrightarrow> z <= Meet A"
 
-theorem Join_upper: "(x::'a::comp_lat) \<in> A \<Longrightarrow> x <= Join A"
-  by (auto simp: Join_def intro: Meet_greatest)
+theorem Sup_upper: "(x::'a::comp_lat) \<in> A \<Longrightarrow> x <= Sup A"
+  by (auto simp: Sup_def intro: Meet_greatest)
 
-theorem Join_least: "(\<And>x::'a::comp_lat. x \<in> A \<Longrightarrow> x <= z) \<Longrightarrow> Join A <= z"
-  by (auto simp: Join_def intro: Meet_lower)
+theorem Sup_least: "(\<And>x::'a::comp_lat. x \<in> A \<Longrightarrow> x <= z) \<Longrightarrow> Sup A <= z"
+  by (auto simp: Sup_def intro: Meet_lower)
 
 text {* A complete lattice is a lattice *}
 
 lemma is_meet_Meet: "is_meet (\<lambda>(x::'a::comp_lat) y. Meet {x, y})"
   by (auto simp: is_meet_def intro: Meet_lower Meet_greatest)
 
-lemma is_join_Join: "is_join (\<lambda>(x::'a::comp_lat) y. Join {x, y})"
-  by (auto simp: is_join_def intro: Join_upper Join_least)
+lemma is_join_Sup: "is_join (\<lambda>(x::'a::comp_lat) y. Sup {x, y})"
+  by (auto simp: is_join_def intro: Sup_upper Sup_least)
 
 instance comp_lat < lorder
 proof
   from is_meet_Meet show "\<exists>m::'a\<Rightarrow>'a\<Rightarrow>'a. is_meet m" by iprover
-  from is_join_Join show "\<exists>j::'a\<Rightarrow>'a\<Rightarrow>'a. is_join j" by iprover
+  from is_join_Sup show "\<exists>j::'a\<Rightarrow>'a\<Rightarrow>'a. is_join j" by iprover
 qed
 
+subsubsection {* Properties *}
+
 lemma mono_join: "mono f \<Longrightarrow> join (f A) (f B) <= f (join A B)"
-  by (auto simp add: mono_def intro: join_imp_le join_left_le join_right_le)
+  by (auto simp add: mono_def)
 
 lemma mono_meet: "mono f \<Longrightarrow> f (meet A B) <= meet (f A) (f B)"
-  by (auto simp add: mono_def intro: meet_imp_le meet_left_le meet_right_le)
+  by (auto simp add: mono_def)
+
+lemma Sup_insert[simp]: "Sup (insert (a::'a::comp_lat) A) = join a (Sup A)"
+apply(simp add:Sup_def)
+apply(rule order_antisym)
+ apply(rule Meet_lower)
+ apply(clarsimp)
+ apply(rule le_joinI2)
+ apply(rule Meet_greatest)
+ apply blast
+apply simp
+apply rule
+ apply(rule Meet_greatest)apply blast
+apply(rule Meet_greatest)
+apply(rule Meet_lower)
+apply blast
+done
+
+lemma bot_least[simp]: "Sup{} \<le> (x::'a::comp_lat)"
+apply(simp add: Sup_def)
+apply(rule Meet_lower)
+apply blast
+done
+(*
+lemma Meet_singleton[simp]: "Meet{a} = (a::'a::comp_lat)"
+apply(rule order_antisym)
+ apply(simp add: Meet_lower)
+apply(rule Meet_greatest)
+apply(simp)
+done
+*)
+lemma le_SupI: "(l::'a::comp_lat) : M \<Longrightarrow> l \<le> Sup M"
+apply(simp add:Sup_def)
+apply(rule Meet_greatest)
+apply(simp)
+done
+
+lemma le_SUPI: "(l::'a::comp_lat) = M i \<Longrightarrow> l \<le> (SUP i. M i)"
+apply(simp add:SUP_def)
+apply(blast intro:le_SupI)
+done
+
+lemma Sup_leI: "(!!x. x:M \<Longrightarrow> x \<le> u) \<Longrightarrow> Sup M \<le> (u::'a::comp_lat)"
+apply(simp add:Sup_def)
+apply(rule Meet_lower)
+apply(blast)
+done
+
+
+lemma SUP_leI: "(!!i. M i \<le> u) \<Longrightarrow> (SUP i. M i) \<le> (u::'a::comp_lat)"
+apply(simp add:SUP_def)
+apply(blast intro!:Sup_leI)
+done
+
+lemma SUP_const[simp]: "(SUP i. M) = (M::'a::comp_lat)"
+by(simp add:SUP_def join_absorp1)
 
 
 subsection {* Some instances of the type class of complete lattices *}
@@ -97,7 +162,7 @@
   apply (rule le_boolE)
   apply (rule meet_right_le)
   apply assumption+
-  apply (rule meet_imp_le)
+  apply (rule le_meetI)
   apply (rule le_boolI)
   apply (erule conjunct1)
   apply (rule le_boolI)
@@ -106,7 +171,7 @@
 
 theorem join_bool_eq: "join P Q = (P \<or> Q)"
   apply (rule order_antisym)
-  apply (rule join_imp_le)
+  apply (rule join_leI)
   apply (rule le_boolI)
   apply (erule disjI1)
   apply (rule le_boolI)
@@ -121,15 +186,15 @@
   apply assumption+
   done
 
-theorem Join_bool_eq: "Join A = (EX x:A. x)"
+theorem Sup_bool_eq: "Sup A = (EX x:A. x)"
   apply (rule order_antisym)
-  apply (rule Join_least)
+  apply (rule Sup_least)
   apply (rule le_boolI)
   apply (erule bexI, assumption)
   apply (rule le_boolI)
   apply (erule bexE)
   apply (rule le_boolE)
-  apply (rule Join_upper)
+  apply (rule Sup_upper)
   apply assumption+
   done
 
@@ -221,10 +286,10 @@
 theorem meet_fun_eq: "meet f g = (\<lambda>x. meet (f x) (g x))"
   apply (rule order_antisym)
   apply (rule le_funI)
-  apply (rule meet_imp_le)
+  apply (rule le_meetI)
   apply (rule le_funD [OF meet_left_le])
   apply (rule le_funD [OF meet_right_le])
-  apply (rule meet_imp_le)
+  apply (rule le_meetI)
   apply (rule le_funI)
   apply (rule meet_left_le)
   apply (rule le_funI)
@@ -233,28 +298,28 @@
 
 theorem join_fun_eq: "join f g = (\<lambda>x. join (f x) (g x))"
   apply (rule order_antisym)
-  apply (rule join_imp_le)
+  apply (rule join_leI)
   apply (rule le_funI)
   apply (rule join_left_le)
   apply (rule le_funI)
   apply (rule join_right_le)
   apply (rule le_funI)
-  apply (rule join_imp_le)
+  apply (rule join_leI)
   apply (rule le_funD [OF join_left_le])
   apply (rule le_funD [OF join_right_le])
   done
 
-theorem Join_fun_eq: "Join A = (\<lambda>x. Join {y::'a::comp_lat. EX f:A. y = f x})"
+theorem Sup_fun_eq: "Sup A = (\<lambda>x. Sup {y::'a::comp_lat. EX f:A. y = f x})"
   apply (rule order_antisym)
-  apply (rule Join_least)
+  apply (rule Sup_least)
   apply (rule le_funI)
-  apply (rule Join_upper)
+  apply (rule Sup_upper)
   apply fast
   apply (rule le_funI)
-  apply (rule Join_least)
+  apply (rule Sup_least)
   apply (erule CollectE)
   apply (erule bexE)
-  apply (drule le_funD [OF Join_upper])
+  apply (drule le_funD [OF Sup_upper])
   apply simp
   done
 
@@ -270,14 +335,14 @@
   apply (rule Int_greatest)
   apply (rule meet_left_le)
   apply (rule meet_right_le)
-  apply (rule meet_imp_le)
+  apply (rule le_meetI)
   apply (rule Int_lower1)
   apply (rule Int_lower2)
   done
 
 theorem join_set_eq: "join A B = A \<union> B"
   apply (rule subset_antisym)
-  apply (rule join_imp_le)
+  apply (rule join_leI)
   apply (rule Un_upper1)
   apply (rule Un_upper2)
   apply (rule Un_least)
@@ -285,12 +350,12 @@
   apply (rule join_right_le)
   done
 
-theorem Join_set_eq: "Join S = \<Union>S"
+theorem Sup_set_eq: "Sup S = \<Union>S"
   apply (rule subset_antisym)
-  apply (rule Join_least)
+  apply (rule Sup_least)
   apply (erule Union_upper)
   apply (rule Union_least)
-  apply (erule Join_upper)
+  apply (erule Sup_upper)
   done
 
 
@@ -301,7 +366,7 @@
   "lfp f == Meet {u. f u <= u}"    --{*least fixed point*}
 
   gfp :: "(('a::comp_lat) => 'a) => 'a"
-  "gfp f == Join {u. u <= f u}"    --{*greatest fixed point*}
+  "gfp f == Sup {u. u <= f u}"    --{*greatest fixed point*}
 
 
 subsection{*Proof of Knaster-Tarski Theorem using @{term lfp}*}
@@ -335,7 +400,7 @@
   with mono have "f (meet (lfp f) P) <= f (lfp f)" ..
   also from mono have "f (lfp f) = lfp f" by (rule lfp_unfold [symmetric])
   finally have "f (meet (lfp f) P) <= lfp f" .
-  from this and ind have "f (meet (lfp f) P) <= meet (lfp f) P" by (rule meet_imp_le)
+  from this and ind have "f (meet (lfp f) P) <= meet (lfp f) P" by (rule le_meetI)
   hence "lfp f <= meet (lfp f) P" by (rule lfp_lowerbound)
   also have "meet (lfp f) P <= P" by (rule meet_right_le)
   finally show ?thesis .
@@ -400,10 +465,10 @@
       the set @{term "{u. u \<le> f(u)}"} *}
 
 lemma gfp_upperbound: "X \<le> f X ==> X \<le> gfp f"
-  by (auto simp add: gfp_def intro: Join_upper)
+  by (auto simp add: gfp_def intro: Sup_upper)
 
 lemma gfp_least: "(!!u. u \<le> f u ==> u \<le> X) ==> gfp f \<le> X"
-  by (auto simp add: gfp_def intro: Join_least)
+  by (auto simp add: gfp_def intro: Sup_least)
 
 lemma gfp_lemma2: "mono f ==> gfp f \<le> f (gfp f)"
   by (iprover intro: gfp_least order_trans monoD gfp_upperbound)
@@ -429,7 +494,7 @@
      "[| X \<le> f (join X (gfp f));  mono f |] ==> join X (gfp f) \<le> f (join X (gfp f))"
   apply (frule gfp_lemma2)
   apply (drule mono_join)
-  apply (rule join_imp_le)
+  apply (rule join_leI)
   apply assumption
   apply (rule order_trans)
   apply (rule order_trans)
@@ -510,6 +575,7 @@
   by (rule gfp_upperbound [THEN gfp_least], blast intro: order_trans)
 
 
+
 ML
 {*
 val lfp_def = thm "lfp_def";
diff -r 3556301c18cd -r 1d39091a3208 src/HOL/FunDef.thy
--- a/src/HOL/FunDef.thy	Sat Nov 11 23:58:46 2006 +0100
+++ b/src/HOL/FunDef.thy	Sun Nov 12 19:22:10 2006 +0100
@@ -19,7 +19,7 @@
 ("Tools/function_package/mutual.ML")
 ("Tools/function_package/pattern_split.ML")
 ("Tools/function_package/fundef_package.ML")
-("Tools/function_package/fundef_datatype.ML")
+(*("Tools/function_package/fundef_datatype.ML")*)
 ("Tools/function_package/auto_term.ML")
 begin
 
diff -r 3556301c18cd -r 1d39091a3208 src/HOL/LOrder.thy
--- a/src/HOL/LOrder.thy	Sat Nov 11 23:58:46 2006 +0100
+++ b/src/HOL/LOrder.thy	Sun Nov 12 19:22:10 2006 +0100
@@ -3,18 +3,14 @@
     Author:  Steven Obua, TU Muenchen
 *)
 
-header {* Lattice Orders *}
+header "Lattice Orders"
 
 theory LOrder
 imports Lattices
 begin
 
-text {*
-  The theory of lattices developed here is taken from the book:
-  \begin{itemize}
-  \item \emph{Lattice Theory} by Garret Birkhoff, American Mathematical Society 1979. 
-  \end{itemize}
-*}
+text {* The theory of lattices developed here is taken from
+\cite{Birkhoff79}.  *}
 
 constdefs
   is_meet :: "(('a::order) \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> bool"
@@ -100,7 +96,9 @@
 lemma meet_right_le: "meet a b \<le> (b::'a::meet_semilorder)"
 by (insert is_meet_meet, auto simp add: is_meet_def)
 
-lemma meet_imp_le: "x \<le> a \<Longrightarrow> x \<le> b \<Longrightarrow> x \<le> meet a (b::'a::meet_semilorder)"
+(* intro! breaks a proof in Hyperreal/SEQ and NumberTheory/IntPrimes *)
+lemma le_meetI:
+ "x \<le> a \<Longrightarrow> x \<le> b \<Longrightarrow> x \<le> meet a (b::'a::meet_semilorder)"
 by (insert is_meet_meet, auto simp add: is_meet_def)
 
 lemma join_left_le: "a \<le> join a (b::'a::join_semilorder)"
@@ -109,10 +107,30 @@
 lemma join_right_le: "b \<le> join a (b::'a::join_semilorder)"
 by (insert is_join_join, auto simp add: is_join_def)
 
-lemma join_imp_le: "a \<le> x \<Longrightarrow> b \<le> x \<Longrightarrow> join a b \<le> (x::'a::join_semilorder)"
+lemma join_leI:
+ "a \<le> x \<Longrightarrow> b \<le> x \<Longrightarrow> join a b \<le> (x::'a::join_semilorder)"
 by (insert is_join_join, auto simp add: is_join_def)
 
-lemmas meet_join_le = meet_left_le meet_right_le join_left_le join_right_le
+lemmas meet_join_le[simp] = meet_left_le meet_right_le join_left_le join_right_le
+
+lemma le_meet[simp]: "(x <= meet y z) = (x <= y & x <= z)" (is "?L = ?R")
+proof
+  assume ?L
+  moreover have "meet y z \<le> y" "meet y z <= z" by(simp_all)
+  ultimately show ?R by(blast intro:order_trans)
+next
+  assume ?R thus ?L by (blast intro!:le_meetI)
+qed
+
+lemma join_le[simp]: "(join x y <= z) = (x <= z & y <= z)" (is "?L = ?R")
+proof
+  assume ?L
+  moreover have "x \<le> join x y" "y \<le> join x y" by(simp_all)
+  ultimately show ?R by(blast intro:order_trans)
+next
+  assume ?R thus ?L by (blast intro:join_leI)
+qed
+
 
 lemma is_meet_min: "is_meet (min::'a \<Rightarrow> 'a \<Rightarrow> ('a::linorder))"
 by (auto simp add: is_meet_def min_def)
@@ -139,42 +157,52 @@
 by (simp add: is_join_join is_join_max is_join_unique)
 
 lemma meet_idempotent[simp]: "meet x x = x"
-by (rule order_antisym, simp_all add: meet_left_le meet_imp_le)
+by (rule order_antisym, simp_all add: le_meetI)
 
 lemma join_idempotent[simp]: "join x x = x"
-by (rule order_antisym, simp_all add: join_left_le join_imp_le)
+by (rule order_antisym, simp_all add: join_leI)
 
 lemma meet_comm: "meet x y = meet y x" 
-by (rule order_antisym, (simp add: meet_left_le meet_right_le meet_imp_le)+)
+by (rule order_antisym, (simp add: le_meetI)+)
 
 lemma join_comm: "join x y = join y x"
-by (rule order_antisym, (simp add: join_right_le join_left_le join_imp_le)+)
+by (rule order_antisym, (simp add: join_leI)+)
+
+lemma meet_leI1: "x \<le> z \<Longrightarrow> meet x y \<le> z"
+apply(subgoal_tac "meet x y <= x")
+ apply(blast intro:order_trans)
+apply simp
+done
+
+lemma meet_leI2: "y \<le> z \<Longrightarrow> meet x y \<le> z"
+apply(subgoal_tac "meet x y <= y")
+ apply(blast intro:order_trans)
+apply simp
+done
 
-lemma meet_assoc: "meet (meet x y) z = meet x (meet y z)" (is "?l=?r")
-proof - 
-  have "?l <= meet x y & meet x y <= x & ?l <= z & meet x y <= y" by (simp add: meet_left_le meet_right_le)
-  hence "?l <= x & ?l <= y & ?l <= z" by auto
-  hence "?l <= ?r" by (simp add: meet_imp_le)
-  hence a:"?l <= meet x (meet y z)" by (simp add: meet_imp_le)
-  have "?r <= meet y z & meet y z <= y & meet y z <= z & ?r <= x" by (simp add: meet_left_le meet_right_le)  
-  hence "?r <= x & ?r <= y & ?r <= z" by (auto) 
-  hence "?r <= meet x y & ?r <= z" by (simp add: meet_imp_le)
-  hence b:"?r <= ?l" by (simp add: meet_imp_le)
-  from a b show "?l = ?r" by auto
-qed
+lemma le_joinI1: "x \<le> y \<Longrightarrow> x \<le> join y z"
+apply(subgoal_tac "y <= join y z")
+ apply(blast intro:order_trans)
+apply simp
+done
+
+lemma le_joinI2: "x \<le> z \<Longrightarrow> x \<le> join y z"
+apply(subgoal_tac "z <= join y z")
+ apply(blast intro:order_trans)
+apply simp
+done
 
-lemma join_assoc: "join (join x y) z = join x (join y z)" (is "?l=?r")
-proof -
-  have "join x y <= ?l & x <= join x y & z <= ?l & y <= join x y" by (simp add: join_left_le join_right_le)
-  hence "x <= ?l & y <= ?l & z <= ?l" by auto
-  hence "join y z <= ?l & x <= ?l" by (simp add: join_imp_le)
-  hence a:"?r <= ?l" by (simp add: join_imp_le)
-  have "join y z <= ?r & y <= join y z & z <= join y z & x <= ?r" by (simp add: join_left_le join_right_le)
-  hence "y <= ?r & z <= ?r & x <= ?r" by auto
-  hence "join x y <= ?r & z <= ?r" by (simp add: join_imp_le)
-  hence b:"?l <= ?r" by (simp add: join_imp_le)
-  from a b show "?l = ?r" by auto
-qed
+lemma meet_assoc: "meet (meet x y) z = meet x (meet y z)"
+apply(rule order_antisym)
+apply (simp add:meet_leI1 meet_leI2)
+apply (simp add:meet_leI1 meet_leI2)
+done
+
+lemma join_assoc: "join (join x y) z = join x (join y z)"
+apply(rule order_antisym)
+apply (simp add:le_joinI1 le_joinI2)
+apply (simp add:le_joinI1 le_joinI2)
+done
 
 lemma meet_left_comm: "meet a (meet b c) = meet b (meet a c)"
 by (simp add: meet_assoc[symmetric, of a b c], simp add: meet_comm[of a b], simp add: meet_assoc)
@@ -192,97 +220,69 @@
 
 lemmas join_aci = join_assoc join_comm join_left_comm join_left_idempotent
 
-lemma le_def_meet: "(x <= y) = (meet x y = x)" 
-proof -
-  have u: "x <= y \<longrightarrow> meet x y = x"
-  proof 
-    assume "x <= y"
-    hence "x <= meet x y & meet x y <= x" by (simp add: meet_imp_le meet_left_le)
-    thus "meet x y = x" by auto
-  qed
-  have v:"meet x y = x \<longrightarrow> x <= y" 
-  proof 
-    have a:"meet x y <= y" by (simp add: meet_right_le)
-    assume "meet x y = x"
-    hence "x = meet x y" by auto
-    with a show "x <= y" by (auto)
-  qed
-  from u v show ?thesis by blast
-qed
+lemma le_def_meet: "(x <= y) = (meet x y = x)"
+apply rule
+apply(simp add: order_antisym)
+apply(subgoal_tac "meet x y <= y")
+apply(simp)
+apply(simp (no_asm))
+done
 
-lemma le_def_join: "(x <= y) = (join x y = y)" 
-proof -
-  have u: "x <= y \<longrightarrow> join x y = y"
-  proof 
-    assume "x <= y"
-    hence "join x y <= y & y <= join x y" by (simp add: join_imp_le join_right_le)
-    thus "join x y = y" by auto
-  qed
-  have v:"join x y = y \<longrightarrow> x <= y" 
-  proof 
-    have a:"x <= join x y" by (simp add: join_left_le)
-    assume "join x y = y"
-    hence "y = join x y" by auto
-    with a show "x <= y" by (auto)
-  qed
-  from u v show ?thesis by blast
-qed
+lemma le_def_join: "(x <= y) = (join x y = y)"
+apply rule
+apply(simp add: order_antisym)
+apply(subgoal_tac "x <= join x y")
+apply(simp)
+apply(simp (no_asm))
+done
+
+lemma join_absorp2: "a \<le> b \<Longrightarrow> join a b = b" 
+by (simp add: le_def_join)
+
+lemma join_absorp1: "b \<le> a \<Longrightarrow> join a b = a"
+by (simp add: le_def_join join_aci)
+
+lemma meet_absorp1: "a \<le> b \<Longrightarrow> meet a b = a"
+by (simp add: le_def_meet)
+
+lemma meet_absorp2: "b \<le> a \<Longrightarrow> meet a b = b"
+by (simp add: le_def_meet meet_aci)
 
 lemma meet_join_absorp: "meet x (join x y) = x"
-proof -
-  have a:"meet x (join x y) <= x" by (simp add: meet_left_le)
-  have b:"x <= meet x (join x y)" by (rule meet_imp_le, simp_all add: join_left_le)
-  from a b show ?thesis by auto
-qed
+by(simp add:meet_absorp1)
 
 lemma join_meet_absorp: "join x (meet x y) = x"
-proof - 
-  have a:"x <= join x (meet x y)" by (simp add: join_left_le)
-  have b:"join x (meet x y) <= x" by (rule join_imp_le, simp_all add: meet_left_le)
-  from a b show ?thesis by auto
-qed
+by(simp add:join_absorp1)
 
 lemma meet_mono: "y \<le> z \<Longrightarrow> meet x y \<le> meet x z"
-proof -
-  assume a: "y <= z"
-  have "meet x y <= x & meet x y <= y" by (simp add: meet_left_le meet_right_le)
-  with a have "meet x y <= x & meet x y <= z" by auto 
-  thus "meet x y <= meet x z" by (simp add: meet_imp_le)
-qed
+by(simp add:meet_leI2)
 
 lemma join_mono: "y \<le> z \<Longrightarrow> join x y \<le> join x z"
-proof -
-  assume a: "y \<le> z"
-  have "x <= join x z & z <= join x z" by (simp add: join_left_le join_right_le)
-  with a have "x <= join x z & y <= join x z" by auto
-  thus "join x y <= join x z" by (simp add: join_imp_le)
-qed
+by(simp add:le_joinI2)
 
 lemma distrib_join_le: "join x (meet y z) \<le> meet (join x y) (join x z)" (is "_ <= ?r")
 proof -
-  have a: "x <= ?r" by (rule meet_imp_le, simp_all add: join_left_le)
-  from meet_join_le have b: "meet y z <= ?r" 
-    by (rule_tac meet_imp_le, (blast intro: order_trans)+)
-  from a b show ?thesis by (simp add: join_imp_le)
+  have a: "x <= ?r" by (simp_all add:le_meetI)
+  have b: "meet y z <= ?r" by (simp add:le_joinI2)
+  from a b show ?thesis by (simp add: join_leI)
 qed
   
-lemma distrib_meet_le: "join (meet x y) (meet x z) \<le> meet x (join y z)" (is "?l <= _") 
+lemma distrib_meet_le: "join (meet x y) (meet x z) \<le> meet x (join y z)" (is "?l <= _")
 proof -
-  have a: "?l <= x" by (rule join_imp_le, simp_all add: meet_left_le)
-  from meet_join_le have b: "?l <= join y z" 
-    by (rule_tac join_imp_le, (blast intro: order_trans)+)
-  from a b show ?thesis by (simp add: meet_imp_le)
+  have a: "?l <= x" by (simp_all add: join_leI)
+  have b: "?l <= join y z" by (simp add:meet_leI2)
+  from a b show ?thesis by (simp add: le_meetI)
 qed
 
 lemma meet_join_eq_imp_le: "a = c \<or> a = d \<or> b = c \<or> b = d \<Longrightarrow> meet a b \<le> join c d"
-by (insert meet_join_le, blast intro: order_trans)
+by (auto simp:meet_leI2 meet_leI1)
 
 lemma modular_le: "x \<le> z \<Longrightarrow> join x (meet y z) \<le> meet (join x y) z" (is "_ \<Longrightarrow> ?t <= _")
 proof -
   assume a: "x <= z"
-  have b: "?t <= join x y" by (rule join_imp_le, simp_all add: meet_join_le meet_join_eq_imp_le)
-  have c: "?t <= z" by (rule join_imp_le, simp_all add: meet_join_le a)
-  from b c show ?thesis by (simp add: meet_imp_le)
+  have b: "?t <= join x y" by (simp_all add: join_leI meet_join_eq_imp_le )
+  have c: "?t <= z" by (simp_all add: a join_leI)
+  from b c show ?thesis by (simp add: le_meetI)
 qed
 
 end
diff -r 3556301c18cd -r 1d39091a3208 src/HOL/Lattices.thy
--- a/src/HOL/Lattices.thy	Sat Nov 11 23:58:46 2006 +0100
+++ b/src/HOL/Lattices.thy	Sun Nov 12 19:22:10 2006 +0100
@@ -18,12 +18,12 @@
 
 locale lower_semilattice = partial_order +
   fixes inf :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<sqinter>" 70)
-  assumes inf_le1: "x \<sqinter> y \<sqsubseteq> x" and inf_le2: "x \<sqinter> y \<sqsubseteq> y"
+  assumes inf_le1[simp]: "x \<sqinter> y \<sqsubseteq> x" and inf_le2[simp]: "x \<sqinter> y \<sqsubseteq> y"
   and inf_least: "x \<sqsubseteq> y \<Longrightarrow> x \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> y \<sqinter> z"
 
 locale upper_semilattice = partial_order +
   fixes sup :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<squnion>" 65)
-  assumes sup_ge1: "x \<sqsubseteq> x \<squnion> y" and sup_ge2: "y \<sqsubseteq> x \<squnion> y"
+  assumes sup_ge1[simp]: "x \<sqsubseteq> x \<squnion> y" and sup_ge2[simp]: "y \<sqsubseteq> x \<squnion> y"
   and sup_greatest: "y \<sqsubseteq> x \<Longrightarrow> z \<sqsubseteq> x \<Longrightarrow> y \<squnion> z \<sqsubseteq> x"
 
 locale lattice = lower_semilattice + upper_semilattice
diff -r 3556301c18cd -r 1d39091a3208 src/HOL/Library/Continuity.thy
--- a/src/HOL/Library/Continuity.thy	Sat Nov 11 23:58:46 2006 +0100
+++ b/src/HOL/Library/Continuity.thy	Sun Nov 12 19:22:10 2006 +0100
@@ -9,6 +9,85 @@
 imports Main
 begin
 
+subsection{*Continuity for complete lattices*}
+
+constdefs
+ chain :: "(nat \<Rightarrow> 'a::order) \<Rightarrow> bool"
+"chain M == !i. M i \<le> M(Suc i)"
+ continuous :: "('a::order \<Rightarrow> 'a::order) \<Rightarrow> bool"
+"continuous F == !M. chain M \<longrightarrow> F(SUP i. M i) = (SUP i. F(M i))"
+
+abbreviation
+ bot :: "'a::order"
+"bot == Sup {}"
+
+lemma SUP_nat_conv:
+ "(SUP n::nat. M n::'a::comp_lat) = join (M 0) (SUP n. M(Suc n))"
+apply(rule order_antisym)
+ apply(rule SUP_leI)
+ apply(case_tac n)
+  apply simp
+ apply (blast intro:le_SUPI le_joinI2)
+apply(simp)
+apply (blast intro:SUP_leI le_SUPI)
+done
+
+lemma continuous_mono: fixes F :: "'a::comp_lat \<Rightarrow> 'a::comp_lat"
+  assumes "continuous F" shows "mono F"
+proof
+  fix A B :: "'a" assume "A <= B"
+  let ?C = "%i::nat. if i=0 then A else B"
+  have "chain ?C" using `A <= B` by(simp add:chain_def)
+  have "F B = join (F A) (F B)"
+  proof -
+    have "join A B = B" using `A <= B` by (simp add:join_absorp2)
+    hence "F B = F(SUP i. ?C i)" by(simp add: SUP_nat_conv)
+    also have "\<dots> = (SUP i. F(?C i))"
+      using `chain ?C` `continuous F` by(simp add:continuous_def)
+    also have "\<dots> = join (F A) (F B)" by(simp add: SUP_nat_conv)
+    finally show ?thesis .
+  qed
+  thus "F A \<le> F B" by(subst le_def_join, simp)
+qed
+
+lemma continuous_lfp:
+ assumes "continuous F" shows "lfp F = (SUP i. (F^i) bot)"
+proof -
+  note mono = continuous_mono[OF `continuous F`]
+  { fix i have "(F^i) bot \<le> lfp F"
+    proof (induct i)
+      show "(F^0) bot \<le> lfp F" by simp
+    next
+      case (Suc i)
+      have "(F^(Suc i)) bot = F((F^i) bot)" by simp
+      also have "\<dots> \<le> F(lfp F)" by(rule monoD[OF mono Suc])
+      also have "\<dots> = lfp F" by(simp add:lfp_unfold[OF mono, symmetric])
+      finally show ?case .
+    qed }
+  hence "(SUP i. (F^i) bot) \<le> lfp F" by (blast intro!:SUP_leI)
+  moreover have "lfp F \<le> (SUP i. (F^i) bot)" (is "_ \<le> ?U")
+  proof (rule lfp_lowerbound)
+    have "chain(%i. (F^i) bot)"
+    proof -
+      { fix i have "(F^i) bot \<le> (F^(Suc i)) bot"
+	proof (induct i)
+	  case 0 show ?case by simp
+	next
+	  case Suc thus ?case using monoD[OF mono Suc] by auto
+	qed }
+      thus ?thesis by(auto simp add:chain_def)
+    qed
+    hence "F ?U = (SUP i. (F^(i+1)) bot)" using `continuous F` by (simp add:continuous_def)
+    also have "\<dots> \<le> ?U" by(blast intro:SUP_leI le_SUPI)
+    finally show "F ?U \<le> ?U" .
+  qed
+  ultimately show ?thesis by (blast intro:order_antisym)
+qed
+
+text{* The following development is just for sets but presents an up
+and a down version of chains and continuity and covers @{const gfp}. *}
+
+
 subsection "Chains"
 
 definition
diff -r 3556301c18cd -r 1d39091a3208 src/HOL/Matrix/Matrix.thy
--- a/src/HOL/Matrix/Matrix.thy	Sat Nov 11 23:58:46 2006 +0100
+++ b/src/HOL/Matrix/Matrix.thy	Sun Nov 12 19:22:10 2006 +0100
@@ -20,10 +20,10 @@
   times_matrix_def: "A * B == mult_matrix (op *) (op +) A B"
 
 lemma is_meet_combine_matrix_meet: "is_meet (combine_matrix meet)"
-  by (simp_all add: is_meet_def le_matrix_def meet_left_le meet_right_le meet_imp_le)
+  by (simp_all add: is_meet_def le_matrix_def meet_left_le meet_right_le le_meetI)
 
 lemma is_join_combine_matrix_join: "is_join (combine_matrix join)"
-  by (simp_all add: is_join_def le_matrix_def join_left_le join_right_le join_imp_le)
+  by (simp_all add: is_join_def le_matrix_def join_left_le join_right_le join_leI)
 
 instance matrix :: (lordered_ab_group) lordered_ab_group_meet
 proof 
diff -r 3556301c18cd -r 1d39091a3208 src/HOL/MicroJava/Comp/CorrCompTp.thy
--- a/src/HOL/MicroJava/Comp/CorrCompTp.thy	Sat Nov 11 23:58:46 2006 +0100
+++ b/src/HOL/MicroJava/Comp/CorrCompTp.thy	Sun Nov 12 19:22:10 2006 +0100
@@ -965,7 +965,6 @@
 apply (simp only:)
 apply (rule check_type_mono) apply assumption
 apply (simp (no_asm_simp)  add: max_ssize_def max_of_list_append max_ac)
-apply arith
 apply (simp add: nth_append)
 
 apply (erule conjE)+
diff -r 3556301c18cd -r 1d39091a3208 src/HOL/OrderedGroup.thy
--- a/src/HOL/OrderedGroup.thy	Sat Nov 11 23:58:46 2006 +0100
+++ b/src/HOL/OrderedGroup.thy	Sun Nov 12 19:22:10 2006 +0100
@@ -573,37 +573,37 @@
 
 lemma add_meet_distrib_left: "a + (meet b c) = meet (a + b) (a + (c::'a::{pordered_ab_group_add, meet_semilorder}))"
 apply (rule order_antisym)
-apply (rule meet_imp_le, simp_all add: meet_join_le)
+apply (simp_all add: le_meetI)
 apply (rule add_le_imp_le_left [of "-a"])
 apply (simp only: add_assoc[symmetric], simp)
-apply (rule meet_imp_le)
-apply (rule add_le_imp_le_left[of "a"], simp only: add_assoc[symmetric], simp add: meet_join_le)+
+apply rule
+apply (rule add_le_imp_le_left[of "a"], simp only: add_assoc[symmetric], simp)+
 done
 
 lemma add_join_distrib_left: "a + (join b c) = join (a + b) (a+ (c::'a::{pordered_ab_group_add, join_semilorder}))" 
 apply (rule order_antisym)
 apply (rule add_le_imp_le_left [of "-a"])
 apply (simp only: add_assoc[symmetric], simp)
-apply (rule join_imp_le)
-apply (rule add_le_imp_le_left [of "a"], simp only: add_assoc[symmetric], simp add: meet_join_le)+
-apply (rule join_imp_le)
-apply (simp_all add: meet_join_le)
+apply rule
+apply (rule add_le_imp_le_left [of "a"], simp only: add_assoc[symmetric], simp)+
+apply (rule join_leI)
+apply (simp_all)
 done
 
 lemma is_join_neg_meet: "is_join (% (a::'a::{pordered_ab_group_add, meet_semilorder}) b. - (meet (-a) (-b)))"
 apply (auto simp add: is_join_def)
-apply (rule_tac c="meet (-a) (-b)" in add_le_imp_le_right, simp, simp add: add_meet_distrib_left meet_join_le)
-apply (rule_tac c="meet (-a) (-b)" in add_le_imp_le_right, simp, simp add: add_meet_distrib_left meet_join_le)
+apply (rule_tac c="meet (-a) (-b)" in add_le_imp_le_right, simp, simp add: add_meet_distrib_left)
+apply (rule_tac c="meet (-a) (-b)" in add_le_imp_le_right, simp, simp add: add_meet_distrib_left)
 apply (subst neg_le_iff_le[symmetric]) 
-apply (simp add: meet_imp_le)
+apply (simp add: le_meetI)
 done
 
 lemma is_meet_neg_join: "is_meet (% (a::'a::{pordered_ab_group_add, join_semilorder}) b. - (join (-a) (-b)))"
 apply (auto simp add: is_meet_def)
-apply (rule_tac c="join (-a) (-b)" in add_le_imp_le_right, simp, simp add: add_join_distrib_left meet_join_le)
-apply (rule_tac c="join (-a) (-b)" in add_le_imp_le_right, simp, simp add: add_join_distrib_left meet_join_le)
+apply (rule_tac c="join (-a) (-b)" in add_le_imp_le_right, simp, simp add: add_join_distrib_left)
+apply (rule_tac c="join (-a) (-b)" in add_le_imp_le_right, simp, simp add: add_join_distrib_left)
 apply (subst neg_le_iff_le[symmetric]) 
-apply (simp add: join_imp_le)
+apply (simp add: join_leI)
 done
 
 axclass lordered_ab_group \<subseteq> pordered_ab_group_add, lorder
@@ -664,10 +664,10 @@
 by (simp add: pprt_def nprt_def add_eq_meet_join[symmetric])
 
 lemma zero_le_pprt[simp]: "0 \<le> pprt a"
-by (simp add: pprt_def meet_join_le)
+by (simp add: pprt_def)
 
 lemma nprt_le_zero[simp]: "nprt a \<le> 0"
-by (simp add: nprt_def meet_join_le)
+by (simp add: nprt_def)
 
 lemma le_eq_neg: "(a \<le> -b) = (a + b \<le> (0::_::lordered_ab_group))" (is "?l = ?r")
 proof -
@@ -794,7 +794,7 @@
 
 lemma abs_ge_zero[simp]: "0 \<le> abs (a::'a::lordered_ab_group_abs)"
 proof -
-  have a:"a <= abs a" and b:"-a <= abs a" by (auto simp add: abs_lattice meet_join_le)
+  have a:"a <= abs a" and b:"-a <= abs a" by (auto simp add: abs_lattice)
   show ?thesis by (rule add_mono[OF a b, simplified])
 qed
   
@@ -818,27 +818,15 @@
 qed
 
 lemma abs_ge_self: "a \<le> abs (a::'a::lordered_ab_group_abs)"
-by (simp add: abs_lattice meet_join_le)
+by (simp add: abs_lattice)
 
 lemma abs_ge_minus_self: "-a \<le> abs (a::'a::lordered_ab_group_abs)"
-by (simp add: abs_lattice meet_join_le)
-
-lemma le_imp_join_eq: "a \<le> b \<Longrightarrow> join a b = b" 
-by (simp add: le_def_join)
-
-lemma ge_imp_join_eq: "b \<le> a \<Longrightarrow> join a b = a"
-by (simp add: le_def_join join_aci)
-
-lemma le_imp_meet_eq: "a \<le> b \<Longrightarrow> meet a b = a"
-by (simp add: le_def_meet)
-
-lemma ge_imp_meet_eq: "b \<le> a \<Longrightarrow> meet a b = b"
-by (simp add: le_def_meet meet_aci)
+by (simp add: abs_lattice)
 
 lemma abs_prts: "abs (a::_::lordered_ab_group_abs) = pprt a - nprt a"
 apply (simp add: pprt_def nprt_def diff_minus)
 apply (simp add: add_meet_join_distribs join_aci abs_lattice[symmetric])
-apply (subst le_imp_join_eq, auto)
+apply (subst join_absorp2, auto)
 done
 
 lemma abs_minus_cancel [simp]: "abs (-a) = abs(a::'a::lordered_ab_group_abs)"
@@ -846,7 +834,7 @@
 
 lemma abs_idempotent [simp]: "abs (abs a) = abs (a::'a::lordered_ab_group_abs)"
 apply (simp add: abs_lattice[of "abs a"])
-apply (subst ge_imp_join_eq)
+apply (subst join_absorp1)
 apply (rule order_trans[of _ 0])
 by auto
 
@@ -900,7 +888,7 @@
 by (rule abs_of_nonpos, rule order_less_imp_le)
 
 lemma abs_leI: "[|a \<le> b; -a \<le> b|] ==> abs a \<le> (b::'a::lordered_ab_group_abs)"
-by (simp add: abs_lattice join_imp_le)
+by (simp add: abs_lattice join_leI)
 
 lemma le_minus_self_iff: "(a \<le> -a) = (a \<le> (0::'a::lordered_ab_group))"
 proof -
@@ -929,10 +917,10 @@
 proof -
   have g:"abs a + abs b = join (a+b) (join (-a-b) (join (-a+b) (a + (-b))))" (is "_=join ?m ?n")
     by (simp add: abs_lattice add_meet_join_distribs join_aci diff_minus)
-  have a:"a+b <= join ?m ?n" by (simp add: meet_join_le)
-  have b:"-a-b <= ?n" by (simp add: meet_join_le) 
-  have c:"?n <= join ?m ?n" by (simp add: meet_join_le)
-  from b c have d: "-a-b <= join ?m ?n" by simp
+  have a:"a+b <= join ?m ?n" by (simp)
+  have b:"-a-b <= ?n" by (simp) 
+  have c:"?n <= join ?m ?n" by (simp)
+  from b c have d: "-a-b <= join ?m ?n" by(rule order_trans)
   have e:"-a-b = -(a+b)" by (simp add: diff_minus)
   from a d e have "abs(a+b) <= join ?m ?n" 
     by (drule_tac abs_leI, auto)
@@ -1174,10 +1162,10 @@
 val abs_not_less_zero = thm "abs_not_less_zero";
 val abs_ge_self = thm "abs_ge_self";
 val abs_ge_minus_self = thm "abs_ge_minus_self";
-val le_imp_join_eq = thm "le_imp_join_eq";
-val ge_imp_join_eq = thm "ge_imp_join_eq";
-val le_imp_meet_eq = thm "le_imp_meet_eq";
-val ge_imp_meet_eq = thm "ge_imp_meet_eq";
+val le_imp_join_eq = thm "join_absorp2";
+val ge_imp_join_eq = thm "join_absorp1";
+val le_imp_meet_eq = thm "meet_absorp1";
+val ge_imp_meet_eq = thm "meet_absorp2";
 val abs_prts = thm "abs_prts";
 val abs_minus_cancel = thm "abs_minus_cancel";
 val abs_idempotent = thm "abs_idempotent";
diff -r 3556301c18cd -r 1d39091a3208 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Sat Nov 11 23:58:46 2006 +0100
+++ b/src/HOL/Set.thy	Sun Nov 12 19:22:10 2006 +0100
@@ -1231,6 +1231,9 @@
 lemma image_constant: "x \<in> A ==> (\<lambda>x. c) ` A = {c}"
   by auto
 
+lemma image_constant_conv[simp]: "(%x. c) ` A = (if A = {} then {} else {c})"
+by auto
+
 lemma image_image: "f ` (g ` A) = (\<lambda>x. f (g x)) ` A"
   by blast
 
diff -r 3556301c18cd -r 1d39091a3208 src/HOL/UNITY/Transformers.thy
--- a/src/HOL/UNITY/Transformers.thy	Sat Nov 11 23:58:46 2006 +0100
+++ b/src/HOL/UNITY/Transformers.thy	Sun Nov 12 19:22:10 2006 +0100
@@ -88,7 +88,7 @@
 done
 
 lemma wens_Id [simp]: "wens F Id B = B"
-by (simp add: wens_def gfp_def wp_def awp_def Join_set_eq, blast)
+by (simp add: wens_def gfp_def wp_def awp_def Sup_set_eq, blast)
 
 text{*These two theorems justify the claim that @{term wens} returns the
 weakest assertion satisfying the ensures property*}
@@ -101,7 +101,7 @@
 
 lemma wens_ensures: "act \<in> Acts F ==> F \<in> (wens F act B) ensures B"
 by (simp add: wens_def gfp_def constrains_def awp_def wp_def
-              ensures_def transient_def Join_set_eq, blast)
+              ensures_def transient_def Sup_set_eq, blast)
 
 text{*These two results constitute assertion (4.13) of the thesis*}
 lemma wens_mono: "(A \<subseteq> B) ==> wens F act A \<subseteq> wens F act B"
@@ -110,7 +110,7 @@
 done
 
 lemma wens_weakening: "B \<subseteq> wens F act B"
-by (simp add: wens_def gfp_def Join_set_eq, blast)
+by (simp add: wens_def gfp_def Sup_set_eq, blast)
 
 text{*Assertion (6), or 4.16 in the thesis*}
 lemma subset_wens: "A-B \<subseteq> wp act B \<inter> awp F (B \<union> A) ==> A \<subseteq> wens F act B" 
@@ -119,8 +119,8 @@
 done
 
 text{*Assertion 4.17 in the thesis*}
-lemma Diff_wens_constrains: "F \<in> (wens F act A - A) co wens F act A" 
-by (simp add: wens_def gfp_def wp_def awp_def constrains_def Join_set_eq, blast)
+lemma Diff_wens_constrains: "F \<in> (wens F act A - A) co wens F act A"
+by (simp add: wens_def gfp_def wp_def awp_def constrains_def Sup_set_eq, blast)
   --{*Proved instantly, yet remarkably fragile. If @{text Un_subset_iff}
       is declared as an iff-rule, then it's almost impossible to prove. 
       One proof is via @{text meson} after expanding all definitions, but it's
@@ -332,7 +332,7 @@
 
 lemma wens_single_eq:
      "wens (mk_program (init, {act}, allowed)) act B = B \<union> wp act B"
-by (simp add: wens_def gfp_def wp_def Join_set_eq, blast)
+by (simp add: wens_def gfp_def wp_def Sup_set_eq, blast)
 
 
 text{*Next, we express the @{term "wens_set"} for single-assignment programs*}
diff -r 3556301c18cd -r 1d39091a3208 src/HOL/document/root.bib
--- a/src/HOL/document/root.bib	Sat Nov 11 23:58:46 2006 +0100
+++ b/src/HOL/document/root.bib	Sun Nov 12 19:22:10 2006 +0100
@@ -4,3 +4,6 @@
   publisher = 	 {Cambridge University Press},
   year = 	 1992
 }
+
+@book{Birkhoff79,author={Garret Birkhoff},title={Lattice Theory},
+publisher={American Mathematical Society},year=1979}
\ No newline at end of file
diff -r 3556301c18cd -r 1d39091a3208 src/HOL/ex/CTL.thy
--- a/src/HOL/ex/CTL.thy	Sat Nov 11 23:58:46 2006 +0100
+++ b/src/HOL/ex/CTL.thy	Sun Nov 12 19:22:10 2006 +0100
@@ -91,7 +91,7 @@
     proof
       assume "x \<in> gfp (\<lambda>s. - f (- s))"
       then obtain u where "x \<in> u" and "u \<subseteq> - f (- u)"
-	by (auto simp add: gfp_def Join_set_eq)
+	by (auto simp add: gfp_def Sup_set_eq)
       then have "f (- u) \<subseteq> - u" by auto
       then have "lfp f \<subseteq> - u" by (rule lfp_lowerbound)
       from l and this have "x \<notin> u" by auto