started reorgnization of lattice theories
authornipkow
Sun Nov 12 19:22:10 2006 +0100 (2006-11-12)
changeset 213121d39091a3208
parent 21311 3556301c18cd
child 21313 26fc3a45547c
started reorgnization of lattice theories
src/HOL/FixedPoint.thy
src/HOL/FunDef.thy
src/HOL/LOrder.thy
src/HOL/Lattices.thy
src/HOL/Library/Continuity.thy
src/HOL/Matrix/Matrix.thy
src/HOL/MicroJava/Comp/CorrCompTp.thy
src/HOL/OrderedGroup.thy
src/HOL/Set.thy
src/HOL/UNITY/Transformers.thy
src/HOL/document/root.bib
src/HOL/ex/CTL.thy
     1.1 --- a/src/HOL/FixedPoint.thy	Sat Nov 11 23:58:46 2006 +0100
     1.2 +++ b/src/HOL/FixedPoint.thy	Sun Nov 12 19:22:10 2006 +0100
     1.3 @@ -12,42 +12,107 @@
     1.4  begin
     1.5  
     1.6  subsection {* Complete lattices *}
     1.7 -
     1.8 +(*FIXME Meet \<rightarrow> Inf *)
     1.9  consts
    1.10    Meet :: "'a::order set \<Rightarrow> 'a"
    1.11 -  Join :: "'a::order set \<Rightarrow> 'a"
    1.12 +  Sup :: "'a::order set \<Rightarrow> 'a"
    1.13 +
    1.14 +defs Sup_def: "Sup A == Meet {b. \<forall>a \<in> A. a <= b}"
    1.15  
    1.16 -defs Join_def: "Join A == Meet {b. \<forall>a \<in> A. a <= b}"
    1.17 -
    1.18 +definition
    1.19 + SUP :: "('a \<Rightarrow> 'b::order) \<Rightarrow> 'b" (binder "SUP " 10)
    1.20 +"SUP x. f x == Sup (f ` UNIV)"
    1.21 +(*
    1.22 +abbreviation
    1.23 + bot :: "'a::order"
    1.24 +"bot == Sup {}"
    1.25 +*)
    1.26  axclass comp_lat < order
    1.27    Meet_lower: "x \<in> A \<Longrightarrow> Meet A <= x"
    1.28    Meet_greatest: "(\<And>x. x \<in> A \<Longrightarrow> z <= x) \<Longrightarrow> z <= Meet A"
    1.29  
    1.30 -theorem Join_upper: "(x::'a::comp_lat) \<in> A \<Longrightarrow> x <= Join A"
    1.31 -  by (auto simp: Join_def intro: Meet_greatest)
    1.32 +theorem Sup_upper: "(x::'a::comp_lat) \<in> A \<Longrightarrow> x <= Sup A"
    1.33 +  by (auto simp: Sup_def intro: Meet_greatest)
    1.34  
    1.35 -theorem Join_least: "(\<And>x::'a::comp_lat. x \<in> A \<Longrightarrow> x <= z) \<Longrightarrow> Join A <= z"
    1.36 -  by (auto simp: Join_def intro: Meet_lower)
    1.37 +theorem Sup_least: "(\<And>x::'a::comp_lat. x \<in> A \<Longrightarrow> x <= z) \<Longrightarrow> Sup A <= z"
    1.38 +  by (auto simp: Sup_def intro: Meet_lower)
    1.39  
    1.40  text {* A complete lattice is a lattice *}
    1.41  
    1.42  lemma is_meet_Meet: "is_meet (\<lambda>(x::'a::comp_lat) y. Meet {x, y})"
    1.43    by (auto simp: is_meet_def intro: Meet_lower Meet_greatest)
    1.44  
    1.45 -lemma is_join_Join: "is_join (\<lambda>(x::'a::comp_lat) y. Join {x, y})"
    1.46 -  by (auto simp: is_join_def intro: Join_upper Join_least)
    1.47 +lemma is_join_Sup: "is_join (\<lambda>(x::'a::comp_lat) y. Sup {x, y})"
    1.48 +  by (auto simp: is_join_def intro: Sup_upper Sup_least)
    1.49  
    1.50  instance comp_lat < lorder
    1.51  proof
    1.52    from is_meet_Meet show "\<exists>m::'a\<Rightarrow>'a\<Rightarrow>'a. is_meet m" by iprover
    1.53 -  from is_join_Join show "\<exists>j::'a\<Rightarrow>'a\<Rightarrow>'a. is_join j" by iprover
    1.54 +  from is_join_Sup show "\<exists>j::'a\<Rightarrow>'a\<Rightarrow>'a. is_join j" by iprover
    1.55  qed
    1.56  
    1.57 +subsubsection {* Properties *}
    1.58 +
    1.59  lemma mono_join: "mono f \<Longrightarrow> join (f A) (f B) <= f (join A B)"
    1.60 -  by (auto simp add: mono_def intro: join_imp_le join_left_le join_right_le)
    1.61 +  by (auto simp add: mono_def)
    1.62  
    1.63  lemma mono_meet: "mono f \<Longrightarrow> f (meet A B) <= meet (f A) (f B)"
    1.64 -  by (auto simp add: mono_def intro: meet_imp_le meet_left_le meet_right_le)
    1.65 +  by (auto simp add: mono_def)
    1.66 +
    1.67 +lemma Sup_insert[simp]: "Sup (insert (a::'a::comp_lat) A) = join a (Sup A)"
    1.68 +apply(simp add:Sup_def)
    1.69 +apply(rule order_antisym)
    1.70 + apply(rule Meet_lower)
    1.71 + apply(clarsimp)
    1.72 + apply(rule le_joinI2)
    1.73 + apply(rule Meet_greatest)
    1.74 + apply blast
    1.75 +apply simp
    1.76 +apply rule
    1.77 + apply(rule Meet_greatest)apply blast
    1.78 +apply(rule Meet_greatest)
    1.79 +apply(rule Meet_lower)
    1.80 +apply blast
    1.81 +done
    1.82 +
    1.83 +lemma bot_least[simp]: "Sup{} \<le> (x::'a::comp_lat)"
    1.84 +apply(simp add: Sup_def)
    1.85 +apply(rule Meet_lower)
    1.86 +apply blast
    1.87 +done
    1.88 +(*
    1.89 +lemma Meet_singleton[simp]: "Meet{a} = (a::'a::comp_lat)"
    1.90 +apply(rule order_antisym)
    1.91 + apply(simp add: Meet_lower)
    1.92 +apply(rule Meet_greatest)
    1.93 +apply(simp)
    1.94 +done
    1.95 +*)
    1.96 +lemma le_SupI: "(l::'a::comp_lat) : M \<Longrightarrow> l \<le> Sup M"
    1.97 +apply(simp add:Sup_def)
    1.98 +apply(rule Meet_greatest)
    1.99 +apply(simp)
   1.100 +done
   1.101 +
   1.102 +lemma le_SUPI: "(l::'a::comp_lat) = M i \<Longrightarrow> l \<le> (SUP i. M i)"
   1.103 +apply(simp add:SUP_def)
   1.104 +apply(blast intro:le_SupI)
   1.105 +done
   1.106 +
   1.107 +lemma Sup_leI: "(!!x. x:M \<Longrightarrow> x \<le> u) \<Longrightarrow> Sup M \<le> (u::'a::comp_lat)"
   1.108 +apply(simp add:Sup_def)
   1.109 +apply(rule Meet_lower)
   1.110 +apply(blast)
   1.111 +done
   1.112 +
   1.113 +
   1.114 +lemma SUP_leI: "(!!i. M i \<le> u) \<Longrightarrow> (SUP i. M i) \<le> (u::'a::comp_lat)"
   1.115 +apply(simp add:SUP_def)
   1.116 +apply(blast intro!:Sup_leI)
   1.117 +done
   1.118 +
   1.119 +lemma SUP_const[simp]: "(SUP i. M) = (M::'a::comp_lat)"
   1.120 +by(simp add:SUP_def join_absorp1)
   1.121  
   1.122  
   1.123  subsection {* Some instances of the type class of complete lattices *}
   1.124 @@ -97,7 +162,7 @@
   1.125    apply (rule le_boolE)
   1.126    apply (rule meet_right_le)
   1.127    apply assumption+
   1.128 -  apply (rule meet_imp_le)
   1.129 +  apply (rule le_meetI)
   1.130    apply (rule le_boolI)
   1.131    apply (erule conjunct1)
   1.132    apply (rule le_boolI)
   1.133 @@ -106,7 +171,7 @@
   1.134  
   1.135  theorem join_bool_eq: "join P Q = (P \<or> Q)"
   1.136    apply (rule order_antisym)
   1.137 -  apply (rule join_imp_le)
   1.138 +  apply (rule join_leI)
   1.139    apply (rule le_boolI)
   1.140    apply (erule disjI1)
   1.141    apply (rule le_boolI)
   1.142 @@ -121,15 +186,15 @@
   1.143    apply assumption+
   1.144    done
   1.145  
   1.146 -theorem Join_bool_eq: "Join A = (EX x:A. x)"
   1.147 +theorem Sup_bool_eq: "Sup A = (EX x:A. x)"
   1.148    apply (rule order_antisym)
   1.149 -  apply (rule Join_least)
   1.150 +  apply (rule Sup_least)
   1.151    apply (rule le_boolI)
   1.152    apply (erule bexI, assumption)
   1.153    apply (rule le_boolI)
   1.154    apply (erule bexE)
   1.155    apply (rule le_boolE)
   1.156 -  apply (rule Join_upper)
   1.157 +  apply (rule Sup_upper)
   1.158    apply assumption+
   1.159    done
   1.160  
   1.161 @@ -221,10 +286,10 @@
   1.162  theorem meet_fun_eq: "meet f g = (\<lambda>x. meet (f x) (g x))"
   1.163    apply (rule order_antisym)
   1.164    apply (rule le_funI)
   1.165 -  apply (rule meet_imp_le)
   1.166 +  apply (rule le_meetI)
   1.167    apply (rule le_funD [OF meet_left_le])
   1.168    apply (rule le_funD [OF meet_right_le])
   1.169 -  apply (rule meet_imp_le)
   1.170 +  apply (rule le_meetI)
   1.171    apply (rule le_funI)
   1.172    apply (rule meet_left_le)
   1.173    apply (rule le_funI)
   1.174 @@ -233,28 +298,28 @@
   1.175  
   1.176  theorem join_fun_eq: "join f g = (\<lambda>x. join (f x) (g x))"
   1.177    apply (rule order_antisym)
   1.178 -  apply (rule join_imp_le)
   1.179 +  apply (rule join_leI)
   1.180    apply (rule le_funI)
   1.181    apply (rule join_left_le)
   1.182    apply (rule le_funI)
   1.183    apply (rule join_right_le)
   1.184    apply (rule le_funI)
   1.185 -  apply (rule join_imp_le)
   1.186 +  apply (rule join_leI)
   1.187    apply (rule le_funD [OF join_left_le])
   1.188    apply (rule le_funD [OF join_right_le])
   1.189    done
   1.190  
   1.191 -theorem Join_fun_eq: "Join A = (\<lambda>x. Join {y::'a::comp_lat. EX f:A. y = f x})"
   1.192 +theorem Sup_fun_eq: "Sup A = (\<lambda>x. Sup {y::'a::comp_lat. EX f:A. y = f x})"
   1.193    apply (rule order_antisym)
   1.194 -  apply (rule Join_least)
   1.195 +  apply (rule Sup_least)
   1.196    apply (rule le_funI)
   1.197 -  apply (rule Join_upper)
   1.198 +  apply (rule Sup_upper)
   1.199    apply fast
   1.200    apply (rule le_funI)
   1.201 -  apply (rule Join_least)
   1.202 +  apply (rule Sup_least)
   1.203    apply (erule CollectE)
   1.204    apply (erule bexE)
   1.205 -  apply (drule le_funD [OF Join_upper])
   1.206 +  apply (drule le_funD [OF Sup_upper])
   1.207    apply simp
   1.208    done
   1.209  
   1.210 @@ -270,14 +335,14 @@
   1.211    apply (rule Int_greatest)
   1.212    apply (rule meet_left_le)
   1.213    apply (rule meet_right_le)
   1.214 -  apply (rule meet_imp_le)
   1.215 +  apply (rule le_meetI)
   1.216    apply (rule Int_lower1)
   1.217    apply (rule Int_lower2)
   1.218    done
   1.219  
   1.220  theorem join_set_eq: "join A B = A \<union> B"
   1.221    apply (rule subset_antisym)
   1.222 -  apply (rule join_imp_le)
   1.223 +  apply (rule join_leI)
   1.224    apply (rule Un_upper1)
   1.225    apply (rule Un_upper2)
   1.226    apply (rule Un_least)
   1.227 @@ -285,12 +350,12 @@
   1.228    apply (rule join_right_le)
   1.229    done
   1.230  
   1.231 -theorem Join_set_eq: "Join S = \<Union>S"
   1.232 +theorem Sup_set_eq: "Sup S = \<Union>S"
   1.233    apply (rule subset_antisym)
   1.234 -  apply (rule Join_least)
   1.235 +  apply (rule Sup_least)
   1.236    apply (erule Union_upper)
   1.237    apply (rule Union_least)
   1.238 -  apply (erule Join_upper)
   1.239 +  apply (erule Sup_upper)
   1.240    done
   1.241  
   1.242  
   1.243 @@ -301,7 +366,7 @@
   1.244    "lfp f == Meet {u. f u <= u}"    --{*least fixed point*}
   1.245  
   1.246    gfp :: "(('a::comp_lat) => 'a) => 'a"
   1.247 -  "gfp f == Join {u. u <= f u}"    --{*greatest fixed point*}
   1.248 +  "gfp f == Sup {u. u <= f u}"    --{*greatest fixed point*}
   1.249  
   1.250  
   1.251  subsection{*Proof of Knaster-Tarski Theorem using @{term lfp}*}
   1.252 @@ -335,7 +400,7 @@
   1.253    with mono have "f (meet (lfp f) P) <= f (lfp f)" ..
   1.254    also from mono have "f (lfp f) = lfp f" by (rule lfp_unfold [symmetric])
   1.255    finally have "f (meet (lfp f) P) <= lfp f" .
   1.256 -  from this and ind have "f (meet (lfp f) P) <= meet (lfp f) P" by (rule meet_imp_le)
   1.257 +  from this and ind have "f (meet (lfp f) P) <= meet (lfp f) P" by (rule le_meetI)
   1.258    hence "lfp f <= meet (lfp f) P" by (rule lfp_lowerbound)
   1.259    also have "meet (lfp f) P <= P" by (rule meet_right_le)
   1.260    finally show ?thesis .
   1.261 @@ -400,10 +465,10 @@
   1.262        the set @{term "{u. u \<le> f(u)}"} *}
   1.263  
   1.264  lemma gfp_upperbound: "X \<le> f X ==> X \<le> gfp f"
   1.265 -  by (auto simp add: gfp_def intro: Join_upper)
   1.266 +  by (auto simp add: gfp_def intro: Sup_upper)
   1.267  
   1.268  lemma gfp_least: "(!!u. u \<le> f u ==> u \<le> X) ==> gfp f \<le> X"
   1.269 -  by (auto simp add: gfp_def intro: Join_least)
   1.270 +  by (auto simp add: gfp_def intro: Sup_least)
   1.271  
   1.272  lemma gfp_lemma2: "mono f ==> gfp f \<le> f (gfp f)"
   1.273    by (iprover intro: gfp_least order_trans monoD gfp_upperbound)
   1.274 @@ -429,7 +494,7 @@
   1.275       "[| X \<le> f (join X (gfp f));  mono f |] ==> join X (gfp f) \<le> f (join X (gfp f))"
   1.276    apply (frule gfp_lemma2)
   1.277    apply (drule mono_join)
   1.278 -  apply (rule join_imp_le)
   1.279 +  apply (rule join_leI)
   1.280    apply assumption
   1.281    apply (rule order_trans)
   1.282    apply (rule order_trans)
   1.283 @@ -510,6 +575,7 @@
   1.284    by (rule gfp_upperbound [THEN gfp_least], blast intro: order_trans)
   1.285  
   1.286  
   1.287 +
   1.288  ML
   1.289  {*
   1.290  val lfp_def = thm "lfp_def";
     2.1 --- a/src/HOL/FunDef.thy	Sat Nov 11 23:58:46 2006 +0100
     2.2 +++ b/src/HOL/FunDef.thy	Sun Nov 12 19:22:10 2006 +0100
     2.3 @@ -19,7 +19,7 @@
     2.4  ("Tools/function_package/mutual.ML")
     2.5  ("Tools/function_package/pattern_split.ML")
     2.6  ("Tools/function_package/fundef_package.ML")
     2.7 -("Tools/function_package/fundef_datatype.ML")
     2.8 +(*("Tools/function_package/fundef_datatype.ML")*)
     2.9  ("Tools/function_package/auto_term.ML")
    2.10  begin
    2.11  
     3.1 --- a/src/HOL/LOrder.thy	Sat Nov 11 23:58:46 2006 +0100
     3.2 +++ b/src/HOL/LOrder.thy	Sun Nov 12 19:22:10 2006 +0100
     3.3 @@ -3,18 +3,14 @@
     3.4      Author:  Steven Obua, TU Muenchen
     3.5  *)
     3.6  
     3.7 -header {* Lattice Orders *}
     3.8 +header "Lattice Orders"
     3.9  
    3.10  theory LOrder
    3.11  imports Lattices
    3.12  begin
    3.13  
    3.14 -text {*
    3.15 -  The theory of lattices developed here is taken from the book:
    3.16 -  \begin{itemize}
    3.17 -  \item \emph{Lattice Theory} by Garret Birkhoff, American Mathematical Society 1979. 
    3.18 -  \end{itemize}
    3.19 -*}
    3.20 +text {* The theory of lattices developed here is taken from
    3.21 +\cite{Birkhoff79}.  *}
    3.22  
    3.23  constdefs
    3.24    is_meet :: "(('a::order) \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> bool"
    3.25 @@ -100,7 +96,9 @@
    3.26  lemma meet_right_le: "meet a b \<le> (b::'a::meet_semilorder)"
    3.27  by (insert is_meet_meet, auto simp add: is_meet_def)
    3.28  
    3.29 -lemma meet_imp_le: "x \<le> a \<Longrightarrow> x \<le> b \<Longrightarrow> x \<le> meet a (b::'a::meet_semilorder)"
    3.30 +(* intro! breaks a proof in Hyperreal/SEQ and NumberTheory/IntPrimes *)
    3.31 +lemma le_meetI:
    3.32 + "x \<le> a \<Longrightarrow> x \<le> b \<Longrightarrow> x \<le> meet a (b::'a::meet_semilorder)"
    3.33  by (insert is_meet_meet, auto simp add: is_meet_def)
    3.34  
    3.35  lemma join_left_le: "a \<le> join a (b::'a::join_semilorder)"
    3.36 @@ -109,10 +107,30 @@
    3.37  lemma join_right_le: "b \<le> join a (b::'a::join_semilorder)"
    3.38  by (insert is_join_join, auto simp add: is_join_def)
    3.39  
    3.40 -lemma join_imp_le: "a \<le> x \<Longrightarrow> b \<le> x \<Longrightarrow> join a b \<le> (x::'a::join_semilorder)"
    3.41 +lemma join_leI:
    3.42 + "a \<le> x \<Longrightarrow> b \<le> x \<Longrightarrow> join a b \<le> (x::'a::join_semilorder)"
    3.43  by (insert is_join_join, auto simp add: is_join_def)
    3.44  
    3.45 -lemmas meet_join_le = meet_left_le meet_right_le join_left_le join_right_le
    3.46 +lemmas meet_join_le[simp] = meet_left_le meet_right_le join_left_le join_right_le
    3.47 +
    3.48 +lemma le_meet[simp]: "(x <= meet y z) = (x <= y & x <= z)" (is "?L = ?R")
    3.49 +proof
    3.50 +  assume ?L
    3.51 +  moreover have "meet y z \<le> y" "meet y z <= z" by(simp_all)
    3.52 +  ultimately show ?R by(blast intro:order_trans)
    3.53 +next
    3.54 +  assume ?R thus ?L by (blast intro!:le_meetI)
    3.55 +qed
    3.56 +
    3.57 +lemma join_le[simp]: "(join x y <= z) = (x <= z & y <= z)" (is "?L = ?R")
    3.58 +proof
    3.59 +  assume ?L
    3.60 +  moreover have "x \<le> join x y" "y \<le> join x y" by(simp_all)
    3.61 +  ultimately show ?R by(blast intro:order_trans)
    3.62 +next
    3.63 +  assume ?R thus ?L by (blast intro:join_leI)
    3.64 +qed
    3.65 +
    3.66  
    3.67  lemma is_meet_min: "is_meet (min::'a \<Rightarrow> 'a \<Rightarrow> ('a::linorder))"
    3.68  by (auto simp add: is_meet_def min_def)
    3.69 @@ -139,42 +157,52 @@
    3.70  by (simp add: is_join_join is_join_max is_join_unique)
    3.71  
    3.72  lemma meet_idempotent[simp]: "meet x x = x"
    3.73 -by (rule order_antisym, simp_all add: meet_left_le meet_imp_le)
    3.74 +by (rule order_antisym, simp_all add: le_meetI)
    3.75  
    3.76  lemma join_idempotent[simp]: "join x x = x"
    3.77 -by (rule order_antisym, simp_all add: join_left_le join_imp_le)
    3.78 +by (rule order_antisym, simp_all add: join_leI)
    3.79  
    3.80  lemma meet_comm: "meet x y = meet y x" 
    3.81 -by (rule order_antisym, (simp add: meet_left_le meet_right_le meet_imp_le)+)
    3.82 +by (rule order_antisym, (simp add: le_meetI)+)
    3.83  
    3.84  lemma join_comm: "join x y = join y x"
    3.85 -by (rule order_antisym, (simp add: join_right_le join_left_le join_imp_le)+)
    3.86 +by (rule order_antisym, (simp add: join_leI)+)
    3.87 +
    3.88 +lemma meet_leI1: "x \<le> z \<Longrightarrow> meet x y \<le> z"
    3.89 +apply(subgoal_tac "meet x y <= x")
    3.90 + apply(blast intro:order_trans)
    3.91 +apply simp
    3.92 +done
    3.93 +
    3.94 +lemma meet_leI2: "y \<le> z \<Longrightarrow> meet x y \<le> z"
    3.95 +apply(subgoal_tac "meet x y <= y")
    3.96 + apply(blast intro:order_trans)
    3.97 +apply simp
    3.98 +done
    3.99  
   3.100 -lemma meet_assoc: "meet (meet x y) z = meet x (meet y z)" (is "?l=?r")
   3.101 -proof - 
   3.102 -  have "?l <= meet x y & meet x y <= x & ?l <= z & meet x y <= y" by (simp add: meet_left_le meet_right_le)
   3.103 -  hence "?l <= x & ?l <= y & ?l <= z" by auto
   3.104 -  hence "?l <= ?r" by (simp add: meet_imp_le)
   3.105 -  hence a:"?l <= meet x (meet y z)" by (simp add: meet_imp_le)
   3.106 -  have "?r <= meet y z & meet y z <= y & meet y z <= z & ?r <= x" by (simp add: meet_left_le meet_right_le)  
   3.107 -  hence "?r <= x & ?r <= y & ?r <= z" by (auto) 
   3.108 -  hence "?r <= meet x y & ?r <= z" by (simp add: meet_imp_le)
   3.109 -  hence b:"?r <= ?l" by (simp add: meet_imp_le)
   3.110 -  from a b show "?l = ?r" by auto
   3.111 -qed
   3.112 +lemma le_joinI1: "x \<le> y \<Longrightarrow> x \<le> join y z"
   3.113 +apply(subgoal_tac "y <= join y z")
   3.114 + apply(blast intro:order_trans)
   3.115 +apply simp
   3.116 +done
   3.117 +
   3.118 +lemma le_joinI2: "x \<le> z \<Longrightarrow> x \<le> join y z"
   3.119 +apply(subgoal_tac "z <= join y z")
   3.120 + apply(blast intro:order_trans)
   3.121 +apply simp
   3.122 +done
   3.123  
   3.124 -lemma join_assoc: "join (join x y) z = join x (join y z)" (is "?l=?r")
   3.125 -proof -
   3.126 -  have "join x y <= ?l & x <= join x y & z <= ?l & y <= join x y" by (simp add: join_left_le join_right_le)
   3.127 -  hence "x <= ?l & y <= ?l & z <= ?l" by auto
   3.128 -  hence "join y z <= ?l & x <= ?l" by (simp add: join_imp_le)
   3.129 -  hence a:"?r <= ?l" by (simp add: join_imp_le)
   3.130 -  have "join y z <= ?r & y <= join y z & z <= join y z & x <= ?r" by (simp add: join_left_le join_right_le)
   3.131 -  hence "y <= ?r & z <= ?r & x <= ?r" by auto
   3.132 -  hence "join x y <= ?r & z <= ?r" by (simp add: join_imp_le)
   3.133 -  hence b:"?l <= ?r" by (simp add: join_imp_le)
   3.134 -  from a b show "?l = ?r" by auto
   3.135 -qed
   3.136 +lemma meet_assoc: "meet (meet x y) z = meet x (meet y z)"
   3.137 +apply(rule order_antisym)
   3.138 +apply (simp add:meet_leI1 meet_leI2)
   3.139 +apply (simp add:meet_leI1 meet_leI2)
   3.140 +done
   3.141 +
   3.142 +lemma join_assoc: "join (join x y) z = join x (join y z)"
   3.143 +apply(rule order_antisym)
   3.144 +apply (simp add:le_joinI1 le_joinI2)
   3.145 +apply (simp add:le_joinI1 le_joinI2)
   3.146 +done
   3.147  
   3.148  lemma meet_left_comm: "meet a (meet b c) = meet b (meet a c)"
   3.149  by (simp add: meet_assoc[symmetric, of a b c], simp add: meet_comm[of a b], simp add: meet_assoc)
   3.150 @@ -192,97 +220,69 @@
   3.151  
   3.152  lemmas join_aci = join_assoc join_comm join_left_comm join_left_idempotent
   3.153  
   3.154 -lemma le_def_meet: "(x <= y) = (meet x y = x)" 
   3.155 -proof -
   3.156 -  have u: "x <= y \<longrightarrow> meet x y = x"
   3.157 -  proof 
   3.158 -    assume "x <= y"
   3.159 -    hence "x <= meet x y & meet x y <= x" by (simp add: meet_imp_le meet_left_le)
   3.160 -    thus "meet x y = x" by auto
   3.161 -  qed
   3.162 -  have v:"meet x y = x \<longrightarrow> x <= y" 
   3.163 -  proof 
   3.164 -    have a:"meet x y <= y" by (simp add: meet_right_le)
   3.165 -    assume "meet x y = x"
   3.166 -    hence "x = meet x y" by auto
   3.167 -    with a show "x <= y" by (auto)
   3.168 -  qed
   3.169 -  from u v show ?thesis by blast
   3.170 -qed
   3.171 +lemma le_def_meet: "(x <= y) = (meet x y = x)"
   3.172 +apply rule
   3.173 +apply(simp add: order_antisym)
   3.174 +apply(subgoal_tac "meet x y <= y")
   3.175 +apply(simp)
   3.176 +apply(simp (no_asm))
   3.177 +done
   3.178  
   3.179 -lemma le_def_join: "(x <= y) = (join x y = y)" 
   3.180 -proof -
   3.181 -  have u: "x <= y \<longrightarrow> join x y = y"
   3.182 -  proof 
   3.183 -    assume "x <= y"
   3.184 -    hence "join x y <= y & y <= join x y" by (simp add: join_imp_le join_right_le)
   3.185 -    thus "join x y = y" by auto
   3.186 -  qed
   3.187 -  have v:"join x y = y \<longrightarrow> x <= y" 
   3.188 -  proof 
   3.189 -    have a:"x <= join x y" by (simp add: join_left_le)
   3.190 -    assume "join x y = y"
   3.191 -    hence "y = join x y" by auto
   3.192 -    with a show "x <= y" by (auto)
   3.193 -  qed
   3.194 -  from u v show ?thesis by blast
   3.195 -qed
   3.196 +lemma le_def_join: "(x <= y) = (join x y = y)"
   3.197 +apply rule
   3.198 +apply(simp add: order_antisym)
   3.199 +apply(subgoal_tac "x <= join x y")
   3.200 +apply(simp)
   3.201 +apply(simp (no_asm))
   3.202 +done
   3.203 +
   3.204 +lemma join_absorp2: "a \<le> b \<Longrightarrow> join a b = b" 
   3.205 +by (simp add: le_def_join)
   3.206 +
   3.207 +lemma join_absorp1: "b \<le> a \<Longrightarrow> join a b = a"
   3.208 +by (simp add: le_def_join join_aci)
   3.209 +
   3.210 +lemma meet_absorp1: "a \<le> b \<Longrightarrow> meet a b = a"
   3.211 +by (simp add: le_def_meet)
   3.212 +
   3.213 +lemma meet_absorp2: "b \<le> a \<Longrightarrow> meet a b = b"
   3.214 +by (simp add: le_def_meet meet_aci)
   3.215  
   3.216  lemma meet_join_absorp: "meet x (join x y) = x"
   3.217 -proof -
   3.218 -  have a:"meet x (join x y) <= x" by (simp add: meet_left_le)
   3.219 -  have b:"x <= meet x (join x y)" by (rule meet_imp_le, simp_all add: join_left_le)
   3.220 -  from a b show ?thesis by auto
   3.221 -qed
   3.222 +by(simp add:meet_absorp1)
   3.223  
   3.224  lemma join_meet_absorp: "join x (meet x y) = x"
   3.225 -proof - 
   3.226 -  have a:"x <= join x (meet x y)" by (simp add: join_left_le)
   3.227 -  have b:"join x (meet x y) <= x" by (rule join_imp_le, simp_all add: meet_left_le)
   3.228 -  from a b show ?thesis by auto
   3.229 -qed
   3.230 +by(simp add:join_absorp1)
   3.231  
   3.232  lemma meet_mono: "y \<le> z \<Longrightarrow> meet x y \<le> meet x z"
   3.233 -proof -
   3.234 -  assume a: "y <= z"
   3.235 -  have "meet x y <= x & meet x y <= y" by (simp add: meet_left_le meet_right_le)
   3.236 -  with a have "meet x y <= x & meet x y <= z" by auto 
   3.237 -  thus "meet x y <= meet x z" by (simp add: meet_imp_le)
   3.238 -qed
   3.239 +by(simp add:meet_leI2)
   3.240  
   3.241  lemma join_mono: "y \<le> z \<Longrightarrow> join x y \<le> join x z"
   3.242 -proof -
   3.243 -  assume a: "y \<le> z"
   3.244 -  have "x <= join x z & z <= join x z" by (simp add: join_left_le join_right_le)
   3.245 -  with a have "x <= join x z & y <= join x z" by auto
   3.246 -  thus "join x y <= join x z" by (simp add: join_imp_le)
   3.247 -qed
   3.248 +by(simp add:le_joinI2)
   3.249  
   3.250  lemma distrib_join_le: "join x (meet y z) \<le> meet (join x y) (join x z)" (is "_ <= ?r")
   3.251  proof -
   3.252 -  have a: "x <= ?r" by (rule meet_imp_le, simp_all add: join_left_le)
   3.253 -  from meet_join_le have b: "meet y z <= ?r" 
   3.254 -    by (rule_tac meet_imp_le, (blast intro: order_trans)+)
   3.255 -  from a b show ?thesis by (simp add: join_imp_le)
   3.256 +  have a: "x <= ?r" by (simp_all add:le_meetI)
   3.257 +  have b: "meet y z <= ?r" by (simp add:le_joinI2)
   3.258 +  from a b show ?thesis by (simp add: join_leI)
   3.259  qed
   3.260    
   3.261 -lemma distrib_meet_le: "join (meet x y) (meet x z) \<le> meet x (join y z)" (is "?l <= _") 
   3.262 +lemma distrib_meet_le: "join (meet x y) (meet x z) \<le> meet x (join y z)" (is "?l <= _")
   3.263  proof -
   3.264 -  have a: "?l <= x" by (rule join_imp_le, simp_all add: meet_left_le)
   3.265 -  from meet_join_le have b: "?l <= join y z" 
   3.266 -    by (rule_tac join_imp_le, (blast intro: order_trans)+)
   3.267 -  from a b show ?thesis by (simp add: meet_imp_le)
   3.268 +  have a: "?l <= x" by (simp_all add: join_leI)
   3.269 +  have b: "?l <= join y z" by (simp add:meet_leI2)
   3.270 +  from a b show ?thesis by (simp add: le_meetI)
   3.271  qed
   3.272  
   3.273  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"
   3.274 -by (insert meet_join_le, blast intro: order_trans)
   3.275 +by (auto simp:meet_leI2 meet_leI1)
   3.276  
   3.277  lemma modular_le: "x \<le> z \<Longrightarrow> join x (meet y z) \<le> meet (join x y) z" (is "_ \<Longrightarrow> ?t <= _")
   3.278  proof -
   3.279    assume a: "x <= z"
   3.280 -  have b: "?t <= join x y" by (rule join_imp_le, simp_all add: meet_join_le meet_join_eq_imp_le)
   3.281 -  have c: "?t <= z" by (rule join_imp_le, simp_all add: meet_join_le a)
   3.282 -  from b c show ?thesis by (simp add: meet_imp_le)
   3.283 +  have b: "?t <= join x y" by (simp_all add: join_leI meet_join_eq_imp_le )
   3.284 +  have c: "?t <= z" by (simp_all add: a join_leI)
   3.285 +  from b c show ?thesis by (simp add: le_meetI)
   3.286  qed
   3.287  
   3.288  end
     4.1 --- a/src/HOL/Lattices.thy	Sat Nov 11 23:58:46 2006 +0100
     4.2 +++ b/src/HOL/Lattices.thy	Sun Nov 12 19:22:10 2006 +0100
     4.3 @@ -18,12 +18,12 @@
     4.4  
     4.5  locale lower_semilattice = partial_order +
     4.6    fixes inf :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<sqinter>" 70)
     4.7 -  assumes inf_le1: "x \<sqinter> y \<sqsubseteq> x" and inf_le2: "x \<sqinter> y \<sqsubseteq> y"
     4.8 +  assumes inf_le1[simp]: "x \<sqinter> y \<sqsubseteq> x" and inf_le2[simp]: "x \<sqinter> y \<sqsubseteq> y"
     4.9    and inf_least: "x \<sqsubseteq> y \<Longrightarrow> x \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> y \<sqinter> z"
    4.10  
    4.11  locale upper_semilattice = partial_order +
    4.12    fixes sup :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<squnion>" 65)
    4.13 -  assumes sup_ge1: "x \<sqsubseteq> x \<squnion> y" and sup_ge2: "y \<sqsubseteq> x \<squnion> y"
    4.14 +  assumes sup_ge1[simp]: "x \<sqsubseteq> x \<squnion> y" and sup_ge2[simp]: "y \<sqsubseteq> x \<squnion> y"
    4.15    and sup_greatest: "y \<sqsubseteq> x \<Longrightarrow> z \<sqsubseteq> x \<Longrightarrow> y \<squnion> z \<sqsubseteq> x"
    4.16  
    4.17  locale lattice = lower_semilattice + upper_semilattice
     5.1 --- a/src/HOL/Library/Continuity.thy	Sat Nov 11 23:58:46 2006 +0100
     5.2 +++ b/src/HOL/Library/Continuity.thy	Sun Nov 12 19:22:10 2006 +0100
     5.3 @@ -9,6 +9,85 @@
     5.4  imports Main
     5.5  begin
     5.6  
     5.7 +subsection{*Continuity for complete lattices*}
     5.8 +
     5.9 +constdefs
    5.10 + chain :: "(nat \<Rightarrow> 'a::order) \<Rightarrow> bool"
    5.11 +"chain M == !i. M i \<le> M(Suc i)"
    5.12 + continuous :: "('a::order \<Rightarrow> 'a::order) \<Rightarrow> bool"
    5.13 +"continuous F == !M. chain M \<longrightarrow> F(SUP i. M i) = (SUP i. F(M i))"
    5.14 +
    5.15 +abbreviation
    5.16 + bot :: "'a::order"
    5.17 +"bot == Sup {}"
    5.18 +
    5.19 +lemma SUP_nat_conv:
    5.20 + "(SUP n::nat. M n::'a::comp_lat) = join (M 0) (SUP n. M(Suc n))"
    5.21 +apply(rule order_antisym)
    5.22 + apply(rule SUP_leI)
    5.23 + apply(case_tac n)
    5.24 +  apply simp
    5.25 + apply (blast intro:le_SUPI le_joinI2)
    5.26 +apply(simp)
    5.27 +apply (blast intro:SUP_leI le_SUPI)
    5.28 +done
    5.29 +
    5.30 +lemma continuous_mono: fixes F :: "'a::comp_lat \<Rightarrow> 'a::comp_lat"
    5.31 +  assumes "continuous F" shows "mono F"
    5.32 +proof
    5.33 +  fix A B :: "'a" assume "A <= B"
    5.34 +  let ?C = "%i::nat. if i=0 then A else B"
    5.35 +  have "chain ?C" using `A <= B` by(simp add:chain_def)
    5.36 +  have "F B = join (F A) (F B)"
    5.37 +  proof -
    5.38 +    have "join A B = B" using `A <= B` by (simp add:join_absorp2)
    5.39 +    hence "F B = F(SUP i. ?C i)" by(simp add: SUP_nat_conv)
    5.40 +    also have "\<dots> = (SUP i. F(?C i))"
    5.41 +      using `chain ?C` `continuous F` by(simp add:continuous_def)
    5.42 +    also have "\<dots> = join (F A) (F B)" by(simp add: SUP_nat_conv)
    5.43 +    finally show ?thesis .
    5.44 +  qed
    5.45 +  thus "F A \<le> F B" by(subst le_def_join, simp)
    5.46 +qed
    5.47 +
    5.48 +lemma continuous_lfp:
    5.49 + assumes "continuous F" shows "lfp F = (SUP i. (F^i) bot)"
    5.50 +proof -
    5.51 +  note mono = continuous_mono[OF `continuous F`]
    5.52 +  { fix i have "(F^i) bot \<le> lfp F"
    5.53 +    proof (induct i)
    5.54 +      show "(F^0) bot \<le> lfp F" by simp
    5.55 +    next
    5.56 +      case (Suc i)
    5.57 +      have "(F^(Suc i)) bot = F((F^i) bot)" by simp
    5.58 +      also have "\<dots> \<le> F(lfp F)" by(rule monoD[OF mono Suc])
    5.59 +      also have "\<dots> = lfp F" by(simp add:lfp_unfold[OF mono, symmetric])
    5.60 +      finally show ?case .
    5.61 +    qed }
    5.62 +  hence "(SUP i. (F^i) bot) \<le> lfp F" by (blast intro!:SUP_leI)
    5.63 +  moreover have "lfp F \<le> (SUP i. (F^i) bot)" (is "_ \<le> ?U")
    5.64 +  proof (rule lfp_lowerbound)
    5.65 +    have "chain(%i. (F^i) bot)"
    5.66 +    proof -
    5.67 +      { fix i have "(F^i) bot \<le> (F^(Suc i)) bot"
    5.68 +	proof (induct i)
    5.69 +	  case 0 show ?case by simp
    5.70 +	next
    5.71 +	  case Suc thus ?case using monoD[OF mono Suc] by auto
    5.72 +	qed }
    5.73 +      thus ?thesis by(auto simp add:chain_def)
    5.74 +    qed
    5.75 +    hence "F ?U = (SUP i. (F^(i+1)) bot)" using `continuous F` by (simp add:continuous_def)
    5.76 +    also have "\<dots> \<le> ?U" by(blast intro:SUP_leI le_SUPI)
    5.77 +    finally show "F ?U \<le> ?U" .
    5.78 +  qed
    5.79 +  ultimately show ?thesis by (blast intro:order_antisym)
    5.80 +qed
    5.81 +
    5.82 +text{* The following development is just for sets but presents an up
    5.83 +and a down version of chains and continuity and covers @{const gfp}. *}
    5.84 +
    5.85 +
    5.86  subsection "Chains"
    5.87  
    5.88  definition
     6.1 --- a/src/HOL/Matrix/Matrix.thy	Sat Nov 11 23:58:46 2006 +0100
     6.2 +++ b/src/HOL/Matrix/Matrix.thy	Sun Nov 12 19:22:10 2006 +0100
     6.3 @@ -20,10 +20,10 @@
     6.4    times_matrix_def: "A * B == mult_matrix (op *) (op +) A B"
     6.5  
     6.6  lemma is_meet_combine_matrix_meet: "is_meet (combine_matrix meet)"
     6.7 -  by (simp_all add: is_meet_def le_matrix_def meet_left_le meet_right_le meet_imp_le)
     6.8 +  by (simp_all add: is_meet_def le_matrix_def meet_left_le meet_right_le le_meetI)
     6.9  
    6.10  lemma is_join_combine_matrix_join: "is_join (combine_matrix join)"
    6.11 -  by (simp_all add: is_join_def le_matrix_def join_left_le join_right_le join_imp_le)
    6.12 +  by (simp_all add: is_join_def le_matrix_def join_left_le join_right_le join_leI)
    6.13  
    6.14  instance matrix :: (lordered_ab_group) lordered_ab_group_meet
    6.15  proof 
     7.1 --- a/src/HOL/MicroJava/Comp/CorrCompTp.thy	Sat Nov 11 23:58:46 2006 +0100
     7.2 +++ b/src/HOL/MicroJava/Comp/CorrCompTp.thy	Sun Nov 12 19:22:10 2006 +0100
     7.3 @@ -965,7 +965,6 @@
     7.4  apply (simp only:)
     7.5  apply (rule check_type_mono) apply assumption
     7.6  apply (simp (no_asm_simp)  add: max_ssize_def max_of_list_append max_ac)
     7.7 -apply arith
     7.8  apply (simp add: nth_append)
     7.9  
    7.10  apply (erule conjE)+
     8.1 --- a/src/HOL/OrderedGroup.thy	Sat Nov 11 23:58:46 2006 +0100
     8.2 +++ b/src/HOL/OrderedGroup.thy	Sun Nov 12 19:22:10 2006 +0100
     8.3 @@ -573,37 +573,37 @@
     8.4  
     8.5  lemma add_meet_distrib_left: "a + (meet b c) = meet (a + b) (a + (c::'a::{pordered_ab_group_add, meet_semilorder}))"
     8.6  apply (rule order_antisym)
     8.7 -apply (rule meet_imp_le, simp_all add: meet_join_le)
     8.8 +apply (simp_all add: le_meetI)
     8.9  apply (rule add_le_imp_le_left [of "-a"])
    8.10  apply (simp only: add_assoc[symmetric], simp)
    8.11 -apply (rule meet_imp_le)
    8.12 -apply (rule add_le_imp_le_left[of "a"], simp only: add_assoc[symmetric], simp add: meet_join_le)+
    8.13 +apply rule
    8.14 +apply (rule add_le_imp_le_left[of "a"], simp only: add_assoc[symmetric], simp)+
    8.15  done
    8.16  
    8.17  lemma add_join_distrib_left: "a + (join b c) = join (a + b) (a+ (c::'a::{pordered_ab_group_add, join_semilorder}))" 
    8.18  apply (rule order_antisym)
    8.19  apply (rule add_le_imp_le_left [of "-a"])
    8.20  apply (simp only: add_assoc[symmetric], simp)
    8.21 -apply (rule join_imp_le)
    8.22 -apply (rule add_le_imp_le_left [of "a"], simp only: add_assoc[symmetric], simp add: meet_join_le)+
    8.23 -apply (rule join_imp_le)
    8.24 -apply (simp_all add: meet_join_le)
    8.25 +apply rule
    8.26 +apply (rule add_le_imp_le_left [of "a"], simp only: add_assoc[symmetric], simp)+
    8.27 +apply (rule join_leI)
    8.28 +apply (simp_all)
    8.29  done
    8.30  
    8.31  lemma is_join_neg_meet: "is_join (% (a::'a::{pordered_ab_group_add, meet_semilorder}) b. - (meet (-a) (-b)))"
    8.32  apply (auto simp add: is_join_def)
    8.33 -apply (rule_tac c="meet (-a) (-b)" in add_le_imp_le_right, simp, simp add: add_meet_distrib_left meet_join_le)
    8.34 -apply (rule_tac c="meet (-a) (-b)" in add_le_imp_le_right, simp, simp add: add_meet_distrib_left meet_join_le)
    8.35 +apply (rule_tac c="meet (-a) (-b)" in add_le_imp_le_right, simp, simp add: add_meet_distrib_left)
    8.36 +apply (rule_tac c="meet (-a) (-b)" in add_le_imp_le_right, simp, simp add: add_meet_distrib_left)
    8.37  apply (subst neg_le_iff_le[symmetric]) 
    8.38 -apply (simp add: meet_imp_le)
    8.39 +apply (simp add: le_meetI)
    8.40  done
    8.41  
    8.42  lemma is_meet_neg_join: "is_meet (% (a::'a::{pordered_ab_group_add, join_semilorder}) b. - (join (-a) (-b)))"
    8.43  apply (auto simp add: is_meet_def)
    8.44 -apply (rule_tac c="join (-a) (-b)" in add_le_imp_le_right, simp, simp add: add_join_distrib_left meet_join_le)
    8.45 -apply (rule_tac c="join (-a) (-b)" in add_le_imp_le_right, simp, simp add: add_join_distrib_left meet_join_le)
    8.46 +apply (rule_tac c="join (-a) (-b)" in add_le_imp_le_right, simp, simp add: add_join_distrib_left)
    8.47 +apply (rule_tac c="join (-a) (-b)" in add_le_imp_le_right, simp, simp add: add_join_distrib_left)
    8.48  apply (subst neg_le_iff_le[symmetric]) 
    8.49 -apply (simp add: join_imp_le)
    8.50 +apply (simp add: join_leI)
    8.51  done
    8.52  
    8.53  axclass lordered_ab_group \<subseteq> pordered_ab_group_add, lorder
    8.54 @@ -664,10 +664,10 @@
    8.55  by (simp add: pprt_def nprt_def add_eq_meet_join[symmetric])
    8.56  
    8.57  lemma zero_le_pprt[simp]: "0 \<le> pprt a"
    8.58 -by (simp add: pprt_def meet_join_le)
    8.59 +by (simp add: pprt_def)
    8.60  
    8.61  lemma nprt_le_zero[simp]: "nprt a \<le> 0"
    8.62 -by (simp add: nprt_def meet_join_le)
    8.63 +by (simp add: nprt_def)
    8.64  
    8.65  lemma le_eq_neg: "(a \<le> -b) = (a + b \<le> (0::_::lordered_ab_group))" (is "?l = ?r")
    8.66  proof -
    8.67 @@ -794,7 +794,7 @@
    8.68  
    8.69  lemma abs_ge_zero[simp]: "0 \<le> abs (a::'a::lordered_ab_group_abs)"
    8.70  proof -
    8.71 -  have a:"a <= abs a" and b:"-a <= abs a" by (auto simp add: abs_lattice meet_join_le)
    8.72 +  have a:"a <= abs a" and b:"-a <= abs a" by (auto simp add: abs_lattice)
    8.73    show ?thesis by (rule add_mono[OF a b, simplified])
    8.74  qed
    8.75    
    8.76 @@ -818,27 +818,15 @@
    8.77  qed
    8.78  
    8.79  lemma abs_ge_self: "a \<le> abs (a::'a::lordered_ab_group_abs)"
    8.80 -by (simp add: abs_lattice meet_join_le)
    8.81 +by (simp add: abs_lattice)
    8.82  
    8.83  lemma abs_ge_minus_self: "-a \<le> abs (a::'a::lordered_ab_group_abs)"
    8.84 -by (simp add: abs_lattice meet_join_le)
    8.85 -
    8.86 -lemma le_imp_join_eq: "a \<le> b \<Longrightarrow> join a b = b" 
    8.87 -by (simp add: le_def_join)
    8.88 -
    8.89 -lemma ge_imp_join_eq: "b \<le> a \<Longrightarrow> join a b = a"
    8.90 -by (simp add: le_def_join join_aci)
    8.91 -
    8.92 -lemma le_imp_meet_eq: "a \<le> b \<Longrightarrow> meet a b = a"
    8.93 -by (simp add: le_def_meet)
    8.94 -
    8.95 -lemma ge_imp_meet_eq: "b \<le> a \<Longrightarrow> meet a b = b"
    8.96 -by (simp add: le_def_meet meet_aci)
    8.97 +by (simp add: abs_lattice)
    8.98  
    8.99  lemma abs_prts: "abs (a::_::lordered_ab_group_abs) = pprt a - nprt a"
   8.100  apply (simp add: pprt_def nprt_def diff_minus)
   8.101  apply (simp add: add_meet_join_distribs join_aci abs_lattice[symmetric])
   8.102 -apply (subst le_imp_join_eq, auto)
   8.103 +apply (subst join_absorp2, auto)
   8.104  done
   8.105  
   8.106  lemma abs_minus_cancel [simp]: "abs (-a) = abs(a::'a::lordered_ab_group_abs)"
   8.107 @@ -846,7 +834,7 @@
   8.108  
   8.109  lemma abs_idempotent [simp]: "abs (abs a) = abs (a::'a::lordered_ab_group_abs)"
   8.110  apply (simp add: abs_lattice[of "abs a"])
   8.111 -apply (subst ge_imp_join_eq)
   8.112 +apply (subst join_absorp1)
   8.113  apply (rule order_trans[of _ 0])
   8.114  by auto
   8.115  
   8.116 @@ -900,7 +888,7 @@
   8.117  by (rule abs_of_nonpos, rule order_less_imp_le)
   8.118  
   8.119  lemma abs_leI: "[|a \<le> b; -a \<le> b|] ==> abs a \<le> (b::'a::lordered_ab_group_abs)"
   8.120 -by (simp add: abs_lattice join_imp_le)
   8.121 +by (simp add: abs_lattice join_leI)
   8.122  
   8.123  lemma le_minus_self_iff: "(a \<le> -a) = (a \<le> (0::'a::lordered_ab_group))"
   8.124  proof -
   8.125 @@ -929,10 +917,10 @@
   8.126  proof -
   8.127    have g:"abs a + abs b = join (a+b) (join (-a-b) (join (-a+b) (a + (-b))))" (is "_=join ?m ?n")
   8.128      by (simp add: abs_lattice add_meet_join_distribs join_aci diff_minus)
   8.129 -  have a:"a+b <= join ?m ?n" by (simp add: meet_join_le)
   8.130 -  have b:"-a-b <= ?n" by (simp add: meet_join_le) 
   8.131 -  have c:"?n <= join ?m ?n" by (simp add: meet_join_le)
   8.132 -  from b c have d: "-a-b <= join ?m ?n" by simp
   8.133 +  have a:"a+b <= join ?m ?n" by (simp)
   8.134 +  have b:"-a-b <= ?n" by (simp) 
   8.135 +  have c:"?n <= join ?m ?n" by (simp)
   8.136 +  from b c have d: "-a-b <= join ?m ?n" by(rule order_trans)
   8.137    have e:"-a-b = -(a+b)" by (simp add: diff_minus)
   8.138    from a d e have "abs(a+b) <= join ?m ?n" 
   8.139      by (drule_tac abs_leI, auto)
   8.140 @@ -1174,10 +1162,10 @@
   8.141  val abs_not_less_zero = thm "abs_not_less_zero";
   8.142  val abs_ge_self = thm "abs_ge_self";
   8.143  val abs_ge_minus_self = thm "abs_ge_minus_self";
   8.144 -val le_imp_join_eq = thm "le_imp_join_eq";
   8.145 -val ge_imp_join_eq = thm "ge_imp_join_eq";
   8.146 -val le_imp_meet_eq = thm "le_imp_meet_eq";
   8.147 -val ge_imp_meet_eq = thm "ge_imp_meet_eq";
   8.148 +val le_imp_join_eq = thm "join_absorp2";
   8.149 +val ge_imp_join_eq = thm "join_absorp1";
   8.150 +val le_imp_meet_eq = thm "meet_absorp1";
   8.151 +val ge_imp_meet_eq = thm "meet_absorp2";
   8.152  val abs_prts = thm "abs_prts";
   8.153  val abs_minus_cancel = thm "abs_minus_cancel";
   8.154  val abs_idempotent = thm "abs_idempotent";
     9.1 --- a/src/HOL/Set.thy	Sat Nov 11 23:58:46 2006 +0100
     9.2 +++ b/src/HOL/Set.thy	Sun Nov 12 19:22:10 2006 +0100
     9.3 @@ -1231,6 +1231,9 @@
     9.4  lemma image_constant: "x \<in> A ==> (\<lambda>x. c) ` A = {c}"
     9.5    by auto
     9.6  
     9.7 +lemma image_constant_conv[simp]: "(%x. c) ` A = (if A = {} then {} else {c})"
     9.8 +by auto
     9.9 +
    9.10  lemma image_image: "f ` (g ` A) = (\<lambda>x. f (g x)) ` A"
    9.11    by blast
    9.12  
    10.1 --- a/src/HOL/UNITY/Transformers.thy	Sat Nov 11 23:58:46 2006 +0100
    10.2 +++ b/src/HOL/UNITY/Transformers.thy	Sun Nov 12 19:22:10 2006 +0100
    10.3 @@ -88,7 +88,7 @@
    10.4  done
    10.5  
    10.6  lemma wens_Id [simp]: "wens F Id B = B"
    10.7 -by (simp add: wens_def gfp_def wp_def awp_def Join_set_eq, blast)
    10.8 +by (simp add: wens_def gfp_def wp_def awp_def Sup_set_eq, blast)
    10.9  
   10.10  text{*These two theorems justify the claim that @{term wens} returns the
   10.11  weakest assertion satisfying the ensures property*}
   10.12 @@ -101,7 +101,7 @@
   10.13  
   10.14  lemma wens_ensures: "act \<in> Acts F ==> F \<in> (wens F act B) ensures B"
   10.15  by (simp add: wens_def gfp_def constrains_def awp_def wp_def
   10.16 -              ensures_def transient_def Join_set_eq, blast)
   10.17 +              ensures_def transient_def Sup_set_eq, blast)
   10.18  
   10.19  text{*These two results constitute assertion (4.13) of the thesis*}
   10.20  lemma wens_mono: "(A \<subseteq> B) ==> wens F act A \<subseteq> wens F act B"
   10.21 @@ -110,7 +110,7 @@
   10.22  done
   10.23  
   10.24  lemma wens_weakening: "B \<subseteq> wens F act B"
   10.25 -by (simp add: wens_def gfp_def Join_set_eq, blast)
   10.26 +by (simp add: wens_def gfp_def Sup_set_eq, blast)
   10.27  
   10.28  text{*Assertion (6), or 4.16 in the thesis*}
   10.29  lemma subset_wens: "A-B \<subseteq> wp act B \<inter> awp F (B \<union> A) ==> A \<subseteq> wens F act B" 
   10.30 @@ -119,8 +119,8 @@
   10.31  done
   10.32  
   10.33  text{*Assertion 4.17 in the thesis*}
   10.34 -lemma Diff_wens_constrains: "F \<in> (wens F act A - A) co wens F act A" 
   10.35 -by (simp add: wens_def gfp_def wp_def awp_def constrains_def Join_set_eq, blast)
   10.36 +lemma Diff_wens_constrains: "F \<in> (wens F act A - A) co wens F act A"
   10.37 +by (simp add: wens_def gfp_def wp_def awp_def constrains_def Sup_set_eq, blast)
   10.38    --{*Proved instantly, yet remarkably fragile. If @{text Un_subset_iff}
   10.39        is declared as an iff-rule, then it's almost impossible to prove. 
   10.40        One proof is via @{text meson} after expanding all definitions, but it's
   10.41 @@ -332,7 +332,7 @@
   10.42  
   10.43  lemma wens_single_eq:
   10.44       "wens (mk_program (init, {act}, allowed)) act B = B \<union> wp act B"
   10.45 -by (simp add: wens_def gfp_def wp_def Join_set_eq, blast)
   10.46 +by (simp add: wens_def gfp_def wp_def Sup_set_eq, blast)
   10.47  
   10.48  
   10.49  text{*Next, we express the @{term "wens_set"} for single-assignment programs*}
    11.1 --- a/src/HOL/document/root.bib	Sat Nov 11 23:58:46 2006 +0100
    11.2 +++ b/src/HOL/document/root.bib	Sun Nov 12 19:22:10 2006 +0100
    11.3 @@ -4,3 +4,6 @@
    11.4    publisher = 	 {Cambridge University Press},
    11.5    year = 	 1992
    11.6  }
    11.7 +
    11.8 +@book{Birkhoff79,author={Garret Birkhoff},title={Lattice Theory},
    11.9 +publisher={American Mathematical Society},year=1979}
   11.10 \ No newline at end of file
    12.1 --- a/src/HOL/ex/CTL.thy	Sat Nov 11 23:58:46 2006 +0100
    12.2 +++ b/src/HOL/ex/CTL.thy	Sun Nov 12 19:22:10 2006 +0100
    12.3 @@ -91,7 +91,7 @@
    12.4      proof
    12.5        assume "x \<in> gfp (\<lambda>s. - f (- s))"
    12.6        then obtain u where "x \<in> u" and "u \<subseteq> - f (- u)"
    12.7 -	by (auto simp add: gfp_def Join_set_eq)
    12.8 +	by (auto simp add: gfp_def Sup_set_eq)
    12.9        then have "f (- u) \<subseteq> - u" by auto
   12.10        then have "lfp f \<subseteq> - u" by (rule lfp_lowerbound)
   12.11        from l and this have "x \<notin> u" by auto