stepping towards uniform lattice theory development in HOL
authorhaftmann
Fri Mar 09 08:45:50 2007 +0100 (2007-03-09)
changeset 22422ee19cdb07528
parent 22421 51a18dd1ea86
child 22423 c1836b14c63a
stepping towards uniform lattice theory development in HOL
NEWS
src/HOL/FixedPoint.thy
src/HOL/Hyperreal/StarClasses.thy
src/HOL/LOrder.thy
src/HOL/Lambda/Commutation.thy
src/HOL/Lambda/Eta.thy
src/HOL/Lattices.thy
src/HOL/Library/Continuity.thy
src/HOL/Library/Graphs.thy
src/HOL/List.thy
src/HOL/Matrix/Matrix.thy
src/HOL/MicroJava/BV/JType.thy
src/HOL/OrderedGroup.thy
src/HOL/Predicate.thy
src/HOL/Ring_and_Field.thy
src/HOL/Tools/inductive_package.ML
src/HOL/Tools/res_atp.ML
src/HOL/Transitive_Closure.thy
     1.1 --- a/NEWS	Tue Mar 06 16:40:32 2007 +0100
     1.2 +++ b/NEWS	Fri Mar 09 08:45:50 2007 +0100
     1.3 @@ -505,6 +505,105 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* Some steps towards more uniform lattice theory development in HOL.  Obvious changes:
     1.8 +
     1.9 +    constants "meet" and "join" now named "inf" and "sup"
    1.10 +    constant "Meet" now named "Inf"
    1.11 +
    1.12 +  theorem renames:
    1.13 +    meet_left_le            ~> inf_le1
    1.14 +    meet_right_le           ~> inf_le2
    1.15 +    join_left_le            ~> sup_ge1
    1.16 +    join_right_le           ~> sup_ge2
    1.17 +    meet_join_le            ~> inf_sup_ord
    1.18 +    le_meetI                ~> le_infI
    1.19 +    join_leI                ~> le_supI
    1.20 +    le_meet                 ~> le_inf_iff
    1.21 +    le_join                 ~> ge_sup_conv
    1.22 +    meet_idempotent         ~> inf_idem
    1.23 +    join_idempotent         ~> sup_idem
    1.24 +    meet_comm               ~> inf_commute
    1.25 +    join_comm               ~> sup_commute
    1.26 +    meet_leI1               ~> le_infI1
    1.27 +    meet_leI2               ~> le_infI2
    1.28 +    le_joinI1               ~> le_supI1
    1.29 +    le_joinI2               ~> le_supI2
    1.30 +    meet_assoc              ~> inf_assoc
    1.31 +    join_assoc              ~> sup_assoc
    1.32 +    meet_left_comm          ~> inf_left_commute
    1.33 +    meet_left_idempotent    ~> inf_left_idem
    1.34 +    join_left_comm          ~> sup_left_commute
    1.35 +    join_left_idempotent    ~> sup_left_idem
    1.36 +    meet_aci                ~> inf_aci
    1.37 +    join_aci                ~> sup_aci
    1.38 +    le_def_meet             ~> le_iff_inf
    1.39 +    le_def_join             ~> le_iff_sup
    1.40 +    join_absorp2            ~> sup_absorb2
    1.41 +    join_absorp1            ~> sup_absorb1
    1.42 +    meet_absorp1            ~> inf_absorb1
    1.43 +    meet_absorp2            ~> inf_absorb2
    1.44 +    meet_join_absorp        ~> inf_sup_absorb
    1.45 +    join_meet_absorp        ~> sup_inf_absorb
    1.46 +    distrib_join_le         ~> distrib_sup_le
    1.47 +    distrib_meet_le         ~> distrib_inf_le
    1.48 +
    1.49 +    add_meet_distrib_left   ~> add_inf_distrib_left
    1.50 +    add_join_distrib_left   ~> add_sup_distrib_left
    1.51 +    is_join_neg_meet        ~> is_join_neg_inf
    1.52 +    is_meet_neg_join        ~> is_meet_neg_sup
    1.53 +    add_meet_distrib_right  ~> add_inf_distrib_right
    1.54 +    add_join_distrib_right  ~> add_sup_distrib_right
    1.55 +    add_meet_join_distribs  ~> add_sup_inf_distribs
    1.56 +    join_eq_neg_meet        ~> sup_eq_neg_inf
    1.57 +    meet_eq_neg_join        ~> inf_eq_neg_sup
    1.58 +    add_eq_meet_join        ~> add_eq_inf_sup
    1.59 +    meet_0_imp_0            ~> inf_0_imp_0
    1.60 +    join_0_imp_0            ~> sup_0_imp_0
    1.61 +    meet_0_eq_0             ~> inf_0_eq_0
    1.62 +    join_0_eq_0             ~> sup_0_eq_0
    1.63 +    neg_meet_eq_join        ~> neg_inf_eq_sup
    1.64 +    neg_join_eq_meet        ~> neg_sup_eq_inf
    1.65 +    join_eq_if              ~> sup_eq_if
    1.66 +
    1.67 +    mono_meet               ~> mono_inf
    1.68 +    mono_join               ~> mono_sup
    1.69 +    meet_bool_eq            ~> inf_bool_eq
    1.70 +    join_bool_eq            ~> sup_bool_eq
    1.71 +    meet_fun_eq             ~> inf_fun_eq
    1.72 +    join_fun_eq             ~> sup_fun_eq
    1.73 +    meet_set_eq             ~> inf_set_eq
    1.74 +    join_set_eq             ~> sup_set_eq
    1.75 +    meet1_iff               ~> inf1_iff
    1.76 +    meet2_iff               ~> inf2_iff
    1.77 +    meet1I                  ~> inf1I
    1.78 +    meet2I                  ~> inf2I
    1.79 +    meet1D1                 ~> inf1D1
    1.80 +    meet2D1                 ~> inf2D1
    1.81 +    meet1D2                 ~> inf1D2
    1.82 +    meet2D2                 ~> inf2D2
    1.83 +    meet1E                  ~> inf1E
    1.84 +    meet2E                  ~> inf2E
    1.85 +    join1_iff               ~> sup1_iff
    1.86 +    join2_iff               ~> sup2_iff
    1.87 +    join1I1                 ~> sup1I1
    1.88 +    join2I1                 ~> sup2I1
    1.89 +    join1I1                 ~> sup1I1
    1.90 +    join2I2                 ~> sup1I2
    1.91 +    join1CI                 ~> sup1CI
    1.92 +    join2CI                 ~> sup2CI
    1.93 +    join1E                  ~> sup1E
    1.94 +    join2E                  ~> sup2E
    1.95 +
    1.96 +    is_meet_Meet            ~> is_meet_Inf
    1.97 +    Meet_bool_def           ~> Inf_bool_def
    1.98 +    Meet_fun_def            ~> Inf_fun_def
    1.99 +    Meet_greatest           ~> Inf_greatest
   1.100 +    Meet_lower              ~> Inf_lower
   1.101 +    Meet_set_def            ~> Inf_set_def
   1.102 +
   1.103 +    listsp_meetI            ~> listsp_infI
   1.104 +    listsp_meet_eq          ~> listsp_inf_eq
   1.105 +
   1.106  * Class (axclass + locale) "preorder" and "linear": facts "refl", "trans" and
   1.107  "cases" renamed ro "order_refl", "order_trans" and "linorder_cases", to
   1.108  avoid clashes with HOL "refl" and "trans". INCOMPATIBILITY.
     2.1 --- a/src/HOL/FixedPoint.thy	Tue Mar 06 16:40:32 2007 +0100
     2.2 +++ b/src/HOL/FixedPoint.thy	Fri Mar 09 08:45:50 2007 +0100
     2.3 @@ -12,16 +12,17 @@
     2.4  begin
     2.5  
     2.6  subsection {* Complete lattices *}
     2.7 -(*FIXME Meet \<rightarrow> Inf *)
     2.8 +
     2.9  consts
    2.10 -  Meet :: "'a::order set \<Rightarrow> 'a"
    2.11 -  Sup :: "'a::order set \<Rightarrow> 'a"
    2.12 +  Inf :: "'a::order set \<Rightarrow> 'a"
    2.13  
    2.14 -defs Sup_def: "Sup A == Meet {b. \<forall>a \<in> A. a <= b}"
    2.15 +definition
    2.16 +  Sup :: "'a::order set \<Rightarrow> 'a" where
    2.17 +  "Sup A = Inf {b. \<forall>a \<in> A. a \<le> b}"
    2.18  
    2.19  definition
    2.20    SUP :: "('a \<Rightarrow> 'b::order) \<Rightarrow> 'b"  (binder "SUP " 10) where
    2.21 -  "SUP x. f x == Sup (f ` UNIV)"
    2.22 +  "(SUP x. f x) = Sup (f ` UNIV)"
    2.23  
    2.24  (*
    2.25  abbreviation
    2.26 @@ -29,69 +30,69 @@
    2.27    "bot == Sup {}"
    2.28  *)
    2.29  class comp_lat = order +
    2.30 -  assumes Meet_lower: "x \<in> A \<Longrightarrow> Meet A \<sqsubseteq> x"
    2.31 -  assumes Meet_greatest: "(\<And>x. x \<in> A \<Longrightarrow> z \<sqsubseteq> x) \<Longrightarrow> z \<sqsubseteq> Meet A"
    2.32 +  assumes Inf_lower: "x \<in> A \<Longrightarrow> Inf A \<sqsubseteq> x"
    2.33 +  assumes Inf_greatest: "(\<And>x. x \<in> A \<Longrightarrow> z \<sqsubseteq> x) \<Longrightarrow> z \<sqsubseteq> Inf A"
    2.34  
    2.35  theorem Sup_upper: "(x::'a::comp_lat) \<in> A \<Longrightarrow> x <= Sup A"
    2.36 -  by (auto simp: Sup_def intro: Meet_greatest)
    2.37 +  by (auto simp: Sup_def intro: Inf_greatest)
    2.38  
    2.39  theorem Sup_least: "(\<And>x::'a::comp_lat. x \<in> A \<Longrightarrow> x <= z) \<Longrightarrow> Sup A <= z"
    2.40 -  by (auto simp: Sup_def intro: Meet_lower)
    2.41 +  by (auto simp: Sup_def intro: Inf_lower)
    2.42  
    2.43  text {* A complete lattice is a lattice *}
    2.44  
    2.45 -lemma is_meet_Meet: "is_meet (\<lambda>(x::'a::comp_lat) y. Meet {x, y})"
    2.46 -  by (auto simp: is_meet_def intro: Meet_lower Meet_greatest)
    2.47 +lemma is_meet_Inf: "is_meet (\<lambda>(x::'a::comp_lat) y. Inf {x, y})"
    2.48 +  by (auto simp: is_meet_def intro: Inf_lower Inf_greatest)
    2.49  
    2.50  lemma is_join_Sup: "is_join (\<lambda>(x::'a::comp_lat) y. Sup {x, y})"
    2.51    by (auto simp: is_join_def intro: Sup_upper Sup_least)
    2.52  
    2.53  instance comp_lat < lorder
    2.54  proof
    2.55 -  from is_meet_Meet show "\<exists>m::'a\<Rightarrow>'a\<Rightarrow>'a. is_meet m" by iprover
    2.56 +  from is_meet_Inf show "\<exists>m::'a\<Rightarrow>'a\<Rightarrow>'a. is_meet m" by iprover
    2.57    from is_join_Sup show "\<exists>j::'a\<Rightarrow>'a\<Rightarrow>'a. is_join j" by iprover
    2.58  qed
    2.59  
    2.60  subsubsection {* Properties *}
    2.61  
    2.62 -lemma mono_join: "mono f \<Longrightarrow> join (f A) (f B) <= f (join A B)"
    2.63 +lemma mono_inf: "mono f \<Longrightarrow> f (inf A B) <= inf (f A) (f B)"
    2.64    by (auto simp add: mono_def)
    2.65  
    2.66 -lemma mono_meet: "mono f \<Longrightarrow> f (meet A B) <= meet (f A) (f B)"
    2.67 +lemma mono_sup: "mono f \<Longrightarrow> sup (f A) (f B) <= f (sup A B)"
    2.68    by (auto simp add: mono_def)
    2.69  
    2.70 -lemma Sup_insert[simp]: "Sup (insert (a::'a::comp_lat) A) = join a (Sup A)"
    2.71 +lemma Sup_insert[simp]: "Sup (insert (a::'a::comp_lat) A) = sup a (Sup A)"
    2.72  apply(simp add:Sup_def)
    2.73  apply(rule order_antisym)
    2.74 - apply(rule Meet_lower)
    2.75 + apply(rule Inf_lower)
    2.76   apply(clarsimp)
    2.77 - apply(rule le_joinI2)
    2.78 - apply(rule Meet_greatest)
    2.79 + apply(rule le_supI2)
    2.80 + apply(rule Inf_greatest)
    2.81   apply blast
    2.82  apply simp
    2.83  apply rule
    2.84 - apply(rule Meet_greatest)apply blast
    2.85 -apply(rule Meet_greatest)
    2.86 -apply(rule Meet_lower)
    2.87 + apply(rule Inf_greatest)apply blast
    2.88 +apply(rule Inf_greatest)
    2.89 +apply(rule Inf_lower)
    2.90  apply blast
    2.91  done
    2.92  
    2.93  lemma bot_least[simp]: "Sup{} \<le> (x::'a::comp_lat)"
    2.94  apply(simp add: Sup_def)
    2.95 -apply(rule Meet_lower)
    2.96 +apply(rule Inf_lower)
    2.97  apply blast
    2.98  done
    2.99  (*
   2.100 -lemma Meet_singleton[simp]: "Meet{a} = (a::'a::comp_lat)"
   2.101 +lemma Inf_singleton[simp]: "Inf{a} = (a::'a::comp_lat)"
   2.102  apply(rule order_antisym)
   2.103 - apply(simp add: Meet_lower)
   2.104 -apply(rule Meet_greatest)
   2.105 + apply(simp add: Inf_lower)
   2.106 +apply(rule Inf_greatest)
   2.107  apply(simp)
   2.108  done
   2.109  *)
   2.110  lemma le_SupI: "(l::'a::comp_lat) : M \<Longrightarrow> l \<le> Sup M"
   2.111  apply(simp add:Sup_def)
   2.112 -apply(rule Meet_greatest)
   2.113 +apply(rule Inf_greatest)
   2.114  apply(simp)
   2.115  done
   2.116  
   2.117 @@ -102,7 +103,7 @@
   2.118  
   2.119  lemma Sup_leI: "(!!x. x:M \<Longrightarrow> x \<le> u) \<Longrightarrow> Sup M \<le> (u::'a::comp_lat)"
   2.120  apply(simp add:Sup_def)
   2.121 -apply(rule Meet_lower)
   2.122 +apply(rule Inf_lower)
   2.123  apply(blast)
   2.124  done
   2.125  
   2.126 @@ -113,42 +114,43 @@
   2.127  done
   2.128  
   2.129  lemma SUP_const[simp]: "(SUP i. M) = (M::'a::comp_lat)"
   2.130 -by(simp add:SUP_def image_constant_conv join_absorp1)
   2.131 +by(simp add:SUP_def image_constant_conv sup_absorb1)
   2.132  
   2.133  
   2.134  subsection {* Some instances of the type class of complete lattices *}
   2.135  
   2.136  subsubsection {* Booleans *}
   2.137  
   2.138 -defs Meet_bool_def: "Meet A == ALL x:A. x"
   2.139 +defs
   2.140 +  Inf_bool_def: "Inf A == ALL x:A. x"
   2.141  
   2.142  instance bool :: comp_lat
   2.143    apply intro_classes
   2.144 -  apply (unfold Meet_bool_def)
   2.145 +  apply (unfold Inf_bool_def)
   2.146    apply (iprover intro!: le_boolI elim: ballE)
   2.147    apply (iprover intro!: ballI le_boolI elim: ballE le_boolE)
   2.148    done
   2.149  
   2.150 -theorem meet_bool_eq: "meet P Q = (P \<and> Q)"
   2.151 +theorem inf_bool_eq: "inf P Q \<longleftrightarrow> P \<and> Q"
   2.152    apply (rule order_antisym)
   2.153    apply (rule le_boolI)
   2.154    apply (rule conjI)
   2.155    apply (rule le_boolE)
   2.156 -  apply (rule meet_left_le)
   2.157 +  apply (rule inf_le1)
   2.158    apply assumption+
   2.159    apply (rule le_boolE)
   2.160 -  apply (rule meet_right_le)
   2.161 +  apply (rule inf_le2)
   2.162    apply assumption+
   2.163 -  apply (rule le_meetI)
   2.164 +  apply (rule le_infI)
   2.165    apply (rule le_boolI)
   2.166    apply (erule conjunct1)
   2.167    apply (rule le_boolI)
   2.168    apply (erule conjunct2)
   2.169    done
   2.170  
   2.171 -theorem join_bool_eq: "join P Q = (P \<or> Q)"
   2.172 +theorem sup_bool_eq: "sup P Q \<longleftrightarrow> P \<or> Q"
   2.173    apply (rule order_antisym)
   2.174 -  apply (rule join_leI)
   2.175 +  apply (rule le_supI)
   2.176    apply (rule le_boolI)
   2.177    apply (erule disjI1)
   2.178    apply (rule le_boolI)
   2.179 @@ -156,14 +158,14 @@
   2.180    apply (rule le_boolI)
   2.181    apply (erule disjE)
   2.182    apply (rule le_boolE)
   2.183 -  apply (rule join_left_le)
   2.184 +  apply (rule sup_ge1)
   2.185    apply assumption+
   2.186    apply (rule le_boolE)
   2.187 -  apply (rule join_right_le)
   2.188 +  apply (rule sup_ge2)
   2.189    apply assumption+
   2.190    done
   2.191  
   2.192 -theorem Sup_bool_eq: "Sup A = (EX x:A. x)"
   2.193 +theorem Sup_bool_eq: "Sup A \<longleftrightarrow> (\<exists>x \<in> A. x)"
   2.194    apply (rule order_antisym)
   2.195    apply (rule Sup_least)
   2.196    apply (rule le_boolI)
   2.197 @@ -175,11 +177,12 @@
   2.198    apply assumption+
   2.199    done
   2.200  
   2.201 +
   2.202  subsubsection {* Functions *}
   2.203  
   2.204  text {*
   2.205 -Handy introduction and elimination rules for @{text "\<le>"}
   2.206 -on unary and binary predicates
   2.207 +  Handy introduction and elimination rules for @{text "\<le>"}
   2.208 +  on unary and binary predicates
   2.209  *}
   2.210  
   2.211  lemma predicate1I [Pure.intro!, intro!]:
   2.212 @@ -218,48 +221,49 @@
   2.213  lemma rev_predicate2D: "P x y ==> P <= Q ==> Q x y"
   2.214    by (rule predicate2D)
   2.215  
   2.216 -defs Meet_fun_def: "Meet A == (\<lambda>x. Meet {y. EX f:A. y = f x})"
   2.217 +defs
   2.218 +  Inf_fun_def: "Inf A == (\<lambda>x. Inf {y. EX f:A. y = f x})"
   2.219  
   2.220  instance "fun" :: (type, comp_lat) comp_lat
   2.221    apply intro_classes
   2.222 -  apply (unfold Meet_fun_def)
   2.223 +  apply (unfold Inf_fun_def)
   2.224    apply (rule le_funI)
   2.225 -  apply (rule Meet_lower)
   2.226 +  apply (rule Inf_lower)
   2.227    apply (rule CollectI)
   2.228    apply (rule bexI)
   2.229    apply (rule refl)
   2.230    apply assumption
   2.231    apply (rule le_funI)
   2.232 -  apply (rule Meet_greatest)
   2.233 +  apply (rule Inf_greatest)
   2.234    apply (erule CollectE)
   2.235    apply (erule bexE)
   2.236    apply (iprover elim: le_funE)
   2.237    done
   2.238  
   2.239 -theorem meet_fun_eq: "meet f g = (\<lambda>x. meet (f x) (g x))"
   2.240 +theorem inf_fun_eq: "inf f g = (\<lambda>x. inf (f x) (g x))"
   2.241    apply (rule order_antisym)
   2.242    apply (rule le_funI)
   2.243 -  apply (rule le_meetI)
   2.244 -  apply (rule le_funD [OF meet_left_le])
   2.245 -  apply (rule le_funD [OF meet_right_le])
   2.246 -  apply (rule le_meetI)
   2.247 +  apply (rule le_infI)
   2.248 +  apply (rule le_funD [OF inf_le1])
   2.249 +  apply (rule le_funD [OF inf_le2])
   2.250 +  apply (rule le_infI)
   2.251    apply (rule le_funI)
   2.252 -  apply (rule meet_left_le)
   2.253 +  apply (rule inf_le1)
   2.254    apply (rule le_funI)
   2.255 -  apply (rule meet_right_le)
   2.256 +  apply (rule inf_le2)
   2.257    done
   2.258  
   2.259 -theorem join_fun_eq: "join f g = (\<lambda>x. join (f x) (g x))"
   2.260 +theorem sup_fun_eq: "sup f g = (\<lambda>x. sup (f x) (g x))"
   2.261    apply (rule order_antisym)
   2.262 -  apply (rule join_leI)
   2.263 +  apply (rule le_supI)
   2.264    apply (rule le_funI)
   2.265 -  apply (rule join_left_le)
   2.266 +  apply (rule sup_ge1)
   2.267    apply (rule le_funI)
   2.268 -  apply (rule join_right_le)
   2.269 +  apply (rule sup_ge2)
   2.270    apply (rule le_funI)
   2.271 -  apply (rule join_leI)
   2.272 -  apply (rule le_funD [OF join_left_le])
   2.273 -  apply (rule le_funD [OF join_right_le])
   2.274 +  apply (rule le_supI)
   2.275 +  apply (rule le_funD [OF sup_ge1])
   2.276 +  apply (rule le_funD [OF sup_ge2])
   2.277    done
   2.278  
   2.279  theorem Sup_fun_eq: "Sup A = (\<lambda>x. Sup {y::'a::comp_lat. EX f:A. y = f x})"
   2.280 @@ -278,29 +282,30 @@
   2.281  
   2.282  subsubsection {* Sets *}
   2.283  
   2.284 -defs Meet_set_def: "Meet S == \<Inter>S"
   2.285 +defs
   2.286 +  Inf_set_def: "Inf S == \<Inter>S"
   2.287  
   2.288  instance set :: (type) comp_lat
   2.289 -  by intro_classes (auto simp add: Meet_set_def)
   2.290 +  by intro_classes (auto simp add: Inf_set_def)
   2.291  
   2.292 -theorem meet_set_eq: "meet A B = A \<inter> B"
   2.293 +theorem inf_set_eq: "inf A B = A \<inter> B"
   2.294    apply (rule subset_antisym)
   2.295    apply (rule Int_greatest)
   2.296 -  apply (rule meet_left_le)
   2.297 -  apply (rule meet_right_le)
   2.298 -  apply (rule le_meetI)
   2.299 +  apply (rule inf_le1)
   2.300 +  apply (rule inf_le2)
   2.301 +  apply (rule le_infI)
   2.302    apply (rule Int_lower1)
   2.303    apply (rule Int_lower2)
   2.304    done
   2.305  
   2.306 -theorem join_set_eq: "join A B = A \<union> B"
   2.307 +theorem sup_set_eq: "sup A B = A \<union> B"
   2.308    apply (rule subset_antisym)
   2.309 -  apply (rule join_leI)
   2.310 +  apply (rule le_supI)
   2.311    apply (rule Un_upper1)
   2.312    apply (rule Un_upper2)
   2.313    apply (rule Un_least)
   2.314 -  apply (rule join_left_le)
   2.315 -  apply (rule join_right_le)
   2.316 +  apply (rule sup_ge1)
   2.317 +  apply (rule sup_ge2)
   2.318    done
   2.319  
   2.320  theorem Sup_set_eq: "Sup S = \<Union>S"
   2.321 @@ -314,25 +319,25 @@
   2.322  
   2.323  subsection {* Least and greatest fixed points *}
   2.324  
   2.325 -constdefs
   2.326 -  lfp :: "(('a::comp_lat) => 'a) => 'a"
   2.327 -  "lfp f == Meet {u. f u <= u}"    --{*least fixed point*}
   2.328 +definition
   2.329 +  lfp :: "('a\<Colon>comp_lat \<Rightarrow> 'a) \<Rightarrow> 'a" where
   2.330 +  "lfp f = Inf {u. f u \<le> u}"    --{*least fixed point*}
   2.331  
   2.332 -  gfp :: "(('a::comp_lat) => 'a) => 'a"
   2.333 -  "gfp f == Sup {u. u <= f u}"    --{*greatest fixed point*}
   2.334 +definition
   2.335 +  gfp :: "('a\<Colon>comp_lat \<Rightarrow> 'a) \<Rightarrow> 'a" where
   2.336 +  "gfp f = Sup {u. u \<le> f u}"    --{*greatest fixed point*}
   2.337  
   2.338  
   2.339  subsection{*Proof of Knaster-Tarski Theorem using @{term lfp}*}
   2.340  
   2.341 -
   2.342  text{*@{term "lfp f"} is the least upper bound of 
   2.343        the set @{term "{u. f(u) \<le> u}"} *}
   2.344  
   2.345  lemma lfp_lowerbound: "f A \<le> A ==> lfp f \<le> A"
   2.346 -  by (auto simp add: lfp_def intro: Meet_lower)
   2.347 +  by (auto simp add: lfp_def intro: Inf_lower)
   2.348  
   2.349  lemma lfp_greatest: "(!!u. f u \<le> u ==> A \<le> u) ==> A \<le> lfp f"
   2.350 -  by (auto simp add: lfp_def intro: Meet_greatest)
   2.351 +  by (auto simp add: lfp_def intro: Inf_greatest)
   2.352  
   2.353  lemma lfp_lemma2: "mono f ==> f (lfp f) \<le> lfp f"
   2.354    by (iprover intro: lfp_greatest order_trans monoD lfp_lowerbound)
   2.355 @@ -349,16 +354,16 @@
   2.356  subsection{*General induction rules for least fixed points*}
   2.357  
   2.358  theorem lfp_induct:
   2.359 -  assumes mono: "mono f" and ind: "f (meet (lfp f) P) <= P"
   2.360 +  assumes mono: "mono f" and ind: "f (inf (lfp f) P) <= P"
   2.361    shows "lfp f <= P"
   2.362  proof -
   2.363 -  have "meet (lfp f) P <= lfp f" by (rule meet_left_le)
   2.364 -  with mono have "f (meet (lfp f) P) <= f (lfp f)" ..
   2.365 +  have "inf (lfp f) P <= lfp f" by (rule inf_le1)
   2.366 +  with mono have "f (inf (lfp f) P) <= f (lfp f)" ..
   2.367    also from mono have "f (lfp f) = lfp f" by (rule lfp_unfold [symmetric])
   2.368 -  finally have "f (meet (lfp f) P) <= lfp f" .
   2.369 -  from this and ind have "f (meet (lfp f) P) <= meet (lfp f) P" by (rule le_meetI)
   2.370 -  hence "lfp f <= meet (lfp f) P" by (rule lfp_lowerbound)
   2.371 -  also have "meet (lfp f) P <= P" by (rule meet_right_le)
   2.372 +  finally have "f (inf (lfp f) P) <= lfp f" .
   2.373 +  from this and ind have "f (inf (lfp f) P) <= inf (lfp f) P" by (rule le_infI)
   2.374 +  hence "lfp f <= inf (lfp f) P" by (rule lfp_lowerbound)
   2.375 +  also have "inf (lfp f) P <= P" by (rule inf_le2)
   2.376    finally show ?thesis .
   2.377  qed
   2.378  
   2.379 @@ -368,7 +373,7 @@
   2.380        and indhyp: "!!x. [| x: f(lfp(f) Int {x. P(x)}) |] ==> P(x)"
   2.381    shows "P(a)"
   2.382    by (rule lfp_induct [THEN subsetD, THEN CollectD, OF mono _ lfp])
   2.383 -    (auto simp: meet_set_eq intro: indhyp)
   2.384 +    (auto simp: inf_set_eq intro: indhyp)
   2.385  
   2.386  
   2.387  text{*Version of induction for binary relations*}
   2.388 @@ -399,7 +404,7 @@
   2.389  
   2.390  lemma def_lfp_induct: 
   2.391      "[| A == lfp(f); mono(f);
   2.392 -        f (meet A P) \<le> P
   2.393 +        f (inf A P) \<le> P
   2.394       |] ==> A \<le> P"
   2.395    by (blast intro: lfp_induct)
   2.396  
   2.397 @@ -447,25 +452,25 @@
   2.398  done
   2.399  
   2.400  lemma coinduct_lemma:
   2.401 -     "[| X \<le> f (join X (gfp f));  mono f |] ==> join X (gfp f) \<le> f (join X (gfp f))"
   2.402 +     "[| X \<le> f (sup X (gfp f));  mono f |] ==> sup X (gfp f) \<le> f (sup X (gfp f))"
   2.403    apply (frule gfp_lemma2)
   2.404 -  apply (drule mono_join)
   2.405 -  apply (rule join_leI)
   2.406 +  apply (drule mono_sup)
   2.407 +  apply (rule le_supI)
   2.408    apply assumption
   2.409    apply (rule order_trans)
   2.410    apply (rule order_trans)
   2.411    apply assumption
   2.412 -  apply (rule join_right_le)
   2.413 +  apply (rule sup_ge2)
   2.414    apply assumption
   2.415    done
   2.416  
   2.417  text{*strong version, thanks to Coen and Frost*}
   2.418  lemma coinduct_set: "[| mono(f);  a: X;  X \<subseteq> f(X Un gfp(f)) |] ==> a : gfp(f)"
   2.419 -by (blast intro: weak_coinduct [OF _ coinduct_lemma, simplified join_set_eq])
   2.420 +by (blast intro: weak_coinduct [OF _ coinduct_lemma, simplified sup_set_eq])
   2.421  
   2.422 -lemma coinduct: "[| mono(f); X \<le> f (join X (gfp f)) |] ==> X \<le> gfp(f)"
   2.423 +lemma coinduct: "[| mono(f); X \<le> f (sup X (gfp f)) |] ==> X \<le> gfp(f)"
   2.424    apply (rule order_trans)
   2.425 -  apply (rule join_left_le)
   2.426 +  apply (rule sup_ge1)
   2.427    apply (erule gfp_upperbound [OF coinduct_lemma])
   2.428    apply assumption
   2.429    done
   2.430 @@ -507,7 +512,7 @@
   2.431  by (auto intro!: gfp_unfold)
   2.432  
   2.433  lemma def_coinduct:
   2.434 -     "[| A==gfp(f);  mono(f);  X \<le> f(join X A) |] ==> X \<le> A"
   2.435 +     "[| A==gfp(f);  mono(f);  X \<le> f(sup X A) |] ==> X \<le> A"
   2.436  by (iprover intro!: coinduct)
   2.437  
   2.438  lemma def_coinduct_set:
   2.439 @@ -562,8 +567,8 @@
   2.440  val le_funI = thm "le_funI";
   2.441  val le_boolI = thm "le_boolI";
   2.442  val le_boolI' = thm "le_boolI'";
   2.443 -val meet_fun_eq = thm "meet_fun_eq";
   2.444 -val meet_bool_eq = thm "meet_bool_eq";
   2.445 +val inf_fun_eq = thm "inf_fun_eq";
   2.446 +val inf_bool_eq = thm "inf_bool_eq";
   2.447  val le_funE = thm "le_funE";
   2.448  val le_funD = thm "le_funD";
   2.449  val le_boolE = thm "le_boolE";
     3.1 --- a/src/HOL/Hyperreal/StarClasses.thy	Tue Mar 06 16:40:32 2007 +0100
     3.2 +++ b/src/HOL/Hyperreal/StarClasses.thy	Fri Mar 09 08:45:50 2007 +0100
     3.3 @@ -249,7 +249,7 @@
     3.4  
     3.5  text {*
     3.6    Some extra trouble is necessary because the class axioms 
     3.7 -  for @{term meet} and @{term join} use quantification over
     3.8 +  for @{term inf} and @{term sup} use quantification over
     3.9    function spaces.
    3.10  *}
    3.11  
    3.12 @@ -279,28 +279,28 @@
    3.13  
    3.14  instance star :: (lorder) lorder ..
    3.15  
    3.16 -lemma star_meet_def [transfer_unfold]: "meet = *f2* meet"
    3.17 +lemma star_inf_def [transfer_unfold]: "inf = *f2* inf"
    3.18  apply (rule is_meet_unique [OF is_meet_meet])
    3.19  apply (transfer is_meet_def, rule is_meet_meet)
    3.20  done
    3.21  
    3.22 -lemma star_join_def [transfer_unfold]: "join = *f2* join"
    3.23 +lemma star_sup_def [transfer_unfold]: "sup = *f2* sup"
    3.24  apply (rule is_join_unique [OF is_join_join])
    3.25  apply (transfer is_join_def, rule is_join_join)
    3.26  done
    3.27  
    3.28 -lemma Standard_meet [simp]:
    3.29 -  "\<lbrakk>x \<in> Standard; y \<in> Standard\<rbrakk> \<Longrightarrow> meet x y \<in> Standard"
    3.30 -by (simp add: star_meet_def)
    3.31 +lemma Standard_inf [simp]:
    3.32 +  "\<lbrakk>x \<in> Standard; y \<in> Standard\<rbrakk> \<Longrightarrow> inf x y \<in> Standard"
    3.33 +by (simp add: star_inf_def)
    3.34  
    3.35 -lemma Standard_join [simp]:
    3.36 -  "\<lbrakk>x \<in> Standard; y \<in> Standard\<rbrakk> \<Longrightarrow> join x y \<in> Standard"
    3.37 -by (simp add: star_join_def)
    3.38 +lemma Standard_sup [simp]:
    3.39 +  "\<lbrakk>x \<in> Standard; y \<in> Standard\<rbrakk> \<Longrightarrow> sup x y \<in> Standard"
    3.40 +by (simp add: star_sup_def)
    3.41  
    3.42 -lemma star_of_meet [simp]: "star_of (meet x y) = meet (star_of x) (star_of y)"
    3.43 +lemma star_of_inf [simp]: "star_of (inf x y) = inf (star_of x) (star_of y)"
    3.44  by transfer (rule refl)
    3.45  
    3.46 -lemma star_of_join [simp]: "star_of (join x y) = join (star_of x) (star_of y)"
    3.47 +lemma star_of_sup [simp]: "star_of (sup x y) = sup (star_of x) (star_of y)"
    3.48  by transfer (rule refl)
    3.49  
    3.50  subsection {* Ordered group classes *}
     4.1 --- a/src/HOL/LOrder.thy	Tue Mar 06 16:40:32 2007 +0100
     4.2 +++ b/src/HOL/LOrder.thy	Fri Mar 09 08:45:50 2007 +0100
     4.3 @@ -3,9 +3,9 @@
     4.4      Author:  Steven Obua, TU Muenchen
     4.5  
     4.6  FIXME integrate properly with lattice locales
     4.7 -- make it a class?
     4.8 -- get rid of the implicit there-is-a-meet/join but require eplicit ops.
     4.9 -Also rename meet/join to inf/sup. 
    4.10 +- get rid of the implicit there-is-a-meet/join but require explicit ops.
    4.11 +- abandone semilorder axclasses, instead turn lattice locales into classes
    4.12 +- rename meet/join to inf/sup in all theorems
    4.13  *)
    4.14  
    4.15  header "Lattice Orders"
    4.16 @@ -61,143 +61,134 @@
    4.17    show "u = v" by ((rule ext)+, simp_all add: order_antisym prems f_le) 
    4.18  qed
    4.19  
    4.20 -axclass join_semilorder < order
    4.21 -  join_exists: "? j. is_join j"
    4.22 +lemma is_meet_inf: "is_meet (inf \<Colon> 'a\<Colon>lower_semilattice \<Rightarrow> 'a \<Rightarrow> 'a)"
    4.23 +unfolding is_meet_def by auto
    4.24 +
    4.25 +lemma is_join_sup: "is_join (sup \<Colon> 'a\<Colon>upper_semilattice \<Rightarrow> 'a \<Rightarrow> 'a)"
    4.26 +unfolding is_join_def by auto
    4.27  
    4.28  axclass meet_semilorder < order
    4.29    meet_exists: "? m. is_meet m"
    4.30  
    4.31 -axclass lorder < join_semilorder, meet_semilorder
    4.32 +axclass join_semilorder < order
    4.33 +  join_exists: "? j. is_join j"
    4.34 +
    4.35 +axclass lorder < meet_semilorder, join_semilorder
    4.36  
    4.37 -constdefs
    4.38 -  meet :: "('a::meet_semilorder) \<Rightarrow> 'a \<Rightarrow> 'a"
    4.39 -  "meet == THE m. is_meet m"
    4.40 -  join :: "('a::join_semilorder) \<Rightarrow> 'a \<Rightarrow> 'a"
    4.41 -  "join ==  THE j. is_join j"
    4.42 +definition
    4.43 +  inf :: "('a::meet_semilorder) \<Rightarrow> 'a \<Rightarrow> 'a" where
    4.44 +  "inf = (THE m. is_meet m)"
    4.45  
    4.46 -lemma is_meet_meet: "is_meet (meet::'a \<Rightarrow> 'a \<Rightarrow> ('a::meet_semilorder))"
    4.47 +definition
    4.48 +  sup :: "('a::join_semilorder) \<Rightarrow> 'a \<Rightarrow> 'a" where
    4.49 +  "sup = (THE j. is_join j)"
    4.50 +
    4.51 +lemma is_meet_meet: "is_meet (inf::'a \<Rightarrow> 'a \<Rightarrow> ('a::meet_semilorder))"
    4.52  proof -
    4.53    from meet_exists obtain k::"'a \<Rightarrow> 'a \<Rightarrow> 'a" where "is_meet k" ..
    4.54    with is_meet_unique[of _ k] show ?thesis
    4.55 -    by (simp add: meet_def theI[of is_meet])    
    4.56 +    by (simp add: inf_def theI [of is_meet])    
    4.57  qed
    4.58  
    4.59 -lemma meet_unique: "(is_meet m) = (m = meet)" 
    4.60 -by (insert is_meet_meet, auto simp add: is_meet_unique)
    4.61 -
    4.62 -lemma is_join_join: "is_join (join::'a \<Rightarrow> 'a \<Rightarrow> ('a::join_semilorder))"
    4.63 +lemma is_join_join: "is_join (sup::'a \<Rightarrow> 'a \<Rightarrow> ('a::join_semilorder))"
    4.64  proof -
    4.65    from join_exists obtain k::"'a \<Rightarrow> 'a \<Rightarrow> 'a" where "is_join k" ..
    4.66    with is_join_unique[of _ k] show ?thesis
    4.67 -    by (simp add: join_def theI[of is_join])    
    4.68 +    by (simp add: sup_def theI[of is_join])    
    4.69  qed
    4.70  
    4.71 -lemma join_unique: "(is_join j) = (j = join)"
    4.72 +lemma meet_unique: "(is_meet m) = (m = inf)" 
    4.73 +by (insert is_meet_meet, auto simp add: is_meet_unique)
    4.74 +
    4.75 +lemma join_unique: "(is_join j) = (j = sup)"
    4.76  by (insert is_join_join, auto simp add: is_join_unique)
    4.77  
    4.78 -interpretation meet_semilat:
    4.79 -  lower_semilattice ["op \<le> \<Colon> 'a\<Colon>meet_semilorder \<Rightarrow> 'a \<Rightarrow> bool" "op <" meet]
    4.80 +lemma inf_unique: "(is_meet m) = (m = (Lattices.inf \<Colon> 'a \<Rightarrow> 'a \<Rightarrow> 'a\<Colon>lower_semilattice))" 
    4.81 +by (insert is_meet_inf, auto simp add: is_meet_unique)
    4.82 +
    4.83 +lemma sup_unique: "(is_join j) = (j = (Lattices.sup \<Colon> 'a \<Rightarrow> 'a \<Rightarrow> 'a\<Colon>upper_semilattice))"
    4.84 +by (insert is_join_sup, auto simp add: is_join_unique)
    4.85 +
    4.86 +interpretation inf_semilat:
    4.87 +  lower_semilattice ["op \<le> \<Colon> 'a\<Colon>meet_semilorder \<Rightarrow> 'a \<Rightarrow> bool" "op <" inf]
    4.88  proof unfold_locales
    4.89    fix x y z :: "'a\<Colon>meet_semilorder"
    4.90 -  from is_meet_meet have "is_meet meet" by blast
    4.91 +  from is_meet_meet have "is_meet inf" by blast
    4.92    note meet = this is_meet_def
    4.93 -  from meet show "meet x y \<le> x" by blast
    4.94 -  from meet show "meet x y \<le> y" by blast
    4.95 -  from meet show "x \<le> y \<Longrightarrow> x \<le> z \<Longrightarrow> x \<le> meet y z" by blast
    4.96 +  from meet show "inf x y \<le> x" by blast
    4.97 +  from meet show "inf x y \<le> y" by blast
    4.98 +  from meet show "x \<le> y \<Longrightarrow> x \<le> z \<Longrightarrow> x \<le> inf y z" by blast
    4.99  qed
   4.100  
   4.101 -interpretation join_semilat:
   4.102 -  upper_semilattice ["op \<le> \<Colon> 'a\<Colon>join_semilorder \<Rightarrow> 'a \<Rightarrow> bool" "op <" join]
   4.103 +interpretation sup_semilat:
   4.104 +  upper_semilattice ["op \<le> \<Colon> 'a\<Colon>join_semilorder \<Rightarrow> 'a \<Rightarrow> bool" "op <" sup]
   4.105  proof unfold_locales
   4.106    fix x y z :: "'a\<Colon>join_semilorder"
   4.107 -  from is_join_join have "is_join join" by blast
   4.108 +  from is_join_join have "is_join sup" by blast
   4.109    note join = this is_join_def
   4.110 -  from join show "x \<le> join x y" by blast
   4.111 -  from join show "y \<le> join x y" by blast
   4.112 -  from join show "x \<le> z \<Longrightarrow> y \<le> z \<Longrightarrow> join x y \<le> z" by blast
   4.113 +  from join show "x \<le> sup x y" by blast
   4.114 +  from join show "y \<le> sup x y" by blast
   4.115 +  from join show "x \<le> z \<Longrightarrow> y \<le> z \<Longrightarrow> sup x y \<le> z" by blast
   4.116  qed
   4.117  
   4.118 -declare
   4.119 - join_semilat.antisym_intro[rule del] meet_semilat.antisym_intro[rule del]
   4.120 - join_semilat.le_supE[rule del] meet_semilat.le_infE[rule del]
   4.121 -
   4.122 -interpretation meet_join_lat:
   4.123 -  lattice ["op \<le> \<Colon> 'a\<Colon>lorder \<Rightarrow> 'a \<Rightarrow> bool" "op <" meet join]
   4.124 -by unfold_locales
   4.125 -
   4.126 -lemmas meet_left_le = meet_semilat.inf_le1
   4.127 -lemmas meet_right_le = meet_semilat.inf_le2
   4.128 -lemmas le_meetI[rule del] = meet_semilat.le_infI
   4.129 -(* intro! breaks a proof in Hyperreal/SEQ and NumberTheory/IntPrimes *)
   4.130 -lemmas join_left_le = join_semilat.sup_ge1
   4.131 -lemmas join_right_le = join_semilat.sup_ge2
   4.132 -lemmas join_leI[rule del] = join_semilat.le_supI
   4.133 -
   4.134 -lemmas meet_join_le = meet_left_le meet_right_le join_left_le join_right_le
   4.135 -
   4.136 -lemmas le_meet = meet_semilat.le_inf_iff
   4.137 -
   4.138 -lemmas le_join = join_semilat.ge_sup_conv
   4.139 +interpretation inf_sup_lat:
   4.140 +  lattice ["op \<le> \<Colon> 'a\<Colon>lorder \<Rightarrow> 'a \<Rightarrow> bool" "op <" inf sup]
   4.141 +  by unfold_locales
   4.142  
   4.143  lemma is_meet_min: "is_meet (min::'a \<Rightarrow> 'a \<Rightarrow> ('a::linorder))"
   4.144 -by (auto simp add: is_meet_def min_def)
   4.145 +  by (auto simp add: is_meet_def min_def)
   4.146 + lemma is_join_max: "is_join (max::'a \<Rightarrow> 'a \<Rightarrow> ('a::linorder))"
   4.147 +  by (auto simp add: is_join_def max_def)
   4.148  
   4.149 -lemma is_join_max: "is_join (max::'a \<Rightarrow> 'a \<Rightarrow> ('a::linorder))"
   4.150 -by (auto simp add: is_join_def max_def)
   4.151 -
   4.152 -instance linorder \<subseteq> meet_semilorder
   4.153 +instance linorder \<subseteq> lorder
   4.154  proof
   4.155    from is_meet_min show "? (m::'a\<Rightarrow>'a\<Rightarrow>('a::linorder)). is_meet m" by auto
   4.156 -qed
   4.157 -
   4.158 -instance linorder \<subseteq> join_semilorder
   4.159 -proof
   4.160    from is_join_max show "? (j::'a\<Rightarrow>'a\<Rightarrow>('a::linorder)). is_join j" by auto 
   4.161  qed
   4.162 -    
   4.163 -instance linorder \<subseteq> lorder ..
   4.164  
   4.165 -lemma meet_min: "meet = (min :: 'a\<Rightarrow>'a\<Rightarrow>('a::linorder))" 
   4.166 -by (simp add: is_meet_meet is_meet_min is_meet_unique)
   4.167 +lemma meet_min: "inf = (min \<Colon> 'a\<Colon>{linorder} \<Rightarrow> 'a \<Rightarrow> 'a)"
   4.168 +  by (simp add: is_meet_meet is_meet_min is_meet_unique)
   4.169 +lemma join_max: "sup = (max \<Colon> 'a\<Colon>{linorder} \<Rightarrow> 'a \<Rightarrow> 'a)"
   4.170 +  by (simp add: is_join_join is_join_max is_join_unique)
   4.171  
   4.172 -lemma join_max: "join = (max :: 'a\<Rightarrow>'a\<Rightarrow>('a::linorder))"
   4.173 -by (simp add: is_join_join is_join_max is_join_unique)
   4.174 +lemmas [rule del] = sup_semilat.antisym_intro inf_semilat.antisym_intro
   4.175 +  sup_semilat.le_supE inf_semilat.le_infE
   4.176  
   4.177 -lemmas meet_idempotent = meet_semilat.inf_idem
   4.178 -lemmas join_idempotent = join_semilat.sup_idem
   4.179 -lemmas meet_comm = meet_semilat.inf_commute
   4.180 -lemmas join_comm = join_semilat.sup_commute
   4.181 -lemmas meet_leI1[rule del] = meet_semilat.le_infI1
   4.182 -lemmas meet_leI2[rule del] = meet_semilat.le_infI2
   4.183 -lemmas le_joinI1[rule del] = join_semilat.le_supI1
   4.184 -lemmas le_joinI2[rule del] = join_semilat.le_supI2
   4.185 -lemmas meet_assoc = meet_semilat.inf_assoc
   4.186 -lemmas join_assoc = join_semilat.sup_assoc
   4.187 -lemmas meet_left_comm = meet_semilat.inf_left_commute
   4.188 -lemmas meet_left_idempotent = meet_semilat.inf_left_idem
   4.189 -lemmas join_left_comm = join_semilat.sup_left_commute
   4.190 -lemmas join_left_idempotent= join_semilat.sup_left_idem
   4.191 -    
   4.192 -lemmas meet_aci = meet_assoc meet_comm meet_left_comm meet_left_idempotent
   4.193 -lemmas join_aci = join_assoc join_comm join_left_comm join_left_idempotent
   4.194 -
   4.195 -lemmas le_def_meet = meet_semilat.le_iff_inf
   4.196 -lemmas le_def_join = join_semilat.le_iff_sup
   4.197 -
   4.198 -lemmas join_absorp2 = join_semilat.sup_absorb2
   4.199 -lemmas join_absorp1 = join_semilat.sup_absorb1
   4.200 -
   4.201 -lemmas meet_absorp1 = meet_semilat.inf_absorb1
   4.202 -lemmas meet_absorp2 = meet_semilat.inf_absorb2
   4.203 -
   4.204 -interpretation meet_join_lat:
   4.205 -  lattice ["op \<le> \<Colon> 'a\<Colon>{meet_semilorder,join_semilorder} \<Rightarrow> 'a \<Rightarrow> bool" "op <" meet join]
   4.206 -by unfold_locales
   4.207 -
   4.208 -lemmas meet_join_absorp = meet_join_lat.inf_sup_absorb
   4.209 -lemmas join_meet_absorp = meet_join_lat.sup_inf_absorb
   4.210 -
   4.211 -lemmas distrib_join_le = meet_join_lat.distrib_sup_le
   4.212 -lemmas distrib_meet_le = meet_join_lat.distrib_inf_le
   4.213 +lemmas inf_le1 = inf_semilat.inf_le1
   4.214 +lemmas inf_le2 = inf_semilat.inf_le2
   4.215 +lemmas le_infI [rule del] = inf_semilat.le_infI
   4.216 +  (*intro! breaks a proof in Hyperreal/SEQ and NumberTheory/IntPrimes*)
   4.217 +lemmas sup_ge1 = sup_semilat.sup_ge1
   4.218 +lemmas sup_ge2 = sup_semilat.sup_ge2
   4.219 +lemmas le_supI [rule del] = sup_semilat.le_supI
   4.220 +lemmas inf_sup_ord = inf_le1 inf_le2 sup_ge1 sup_ge2
   4.221 +lemmas le_inf_iff = inf_semilat.le_inf_iff
   4.222 +lemmas ge_sup_conv = sup_semilat.ge_sup_conv
   4.223 +lemmas inf_idem = inf_semilat.inf_idem
   4.224 +lemmas sup_idem = sup_semilat.sup_idem
   4.225 +lemmas inf_commute = inf_semilat.inf_commute
   4.226 +lemmas sup_commute = sup_semilat.sup_commute
   4.227 +lemmas le_infI1 [rule del] = inf_semilat.le_infI1
   4.228 +lemmas le_infI2 [rule del] = inf_semilat.le_infI2
   4.229 +lemmas le_supI1 [rule del] = sup_semilat.le_supI1
   4.230 +lemmas le_supI2 [rule del] = sup_semilat.le_supI2
   4.231 +lemmas inf_assoc = inf_semilat.inf_assoc
   4.232 +lemmas sup_assoc = sup_semilat.sup_assoc
   4.233 +lemmas inf_left_commute = inf_semilat.inf_left_commute
   4.234 +lemmas inf_left_idem = inf_semilat.inf_left_idem
   4.235 +lemmas sup_left_commute = sup_semilat.sup_left_commute
   4.236 +lemmas sup_left_idem= sup_semilat.sup_left_idem
   4.237 +lemmas inf_aci = inf_assoc inf_commute inf_left_commute inf_left_idem
   4.238 +lemmas sup_aci = sup_assoc sup_commute sup_left_commute sup_left_idem
   4.239 +lemmas le_iff_inf = inf_semilat.le_iff_inf
   4.240 +lemmas le_iff_sup = sup_semilat.le_iff_sup
   4.241 +lemmas sup_absorb2 = sup_semilat.sup_absorb2
   4.242 +lemmas sup_absorb1 = sup_semilat.sup_absorb1
   4.243 +lemmas inf_absorb1 = inf_semilat.inf_absorb1
   4.244 +lemmas inf_absorb2 = inf_semilat.inf_absorb2
   4.245 +lemmas inf_sup_absorb = inf_sup_lat.inf_sup_absorb
   4.246 +lemmas sup_inf_absorb = inf_sup_lat.sup_inf_absorb
   4.247 +lemmas distrib_sup_le = inf_sup_lat.distrib_sup_le
   4.248 +lemmas distrib_inf_le = inf_sup_lat.distrib_inf_le
   4.249  
   4.250  end
     5.1 --- a/src/HOL/Lambda/Commutation.thy	Tue Mar 06 16:40:32 2007 +0100
     5.2 +++ b/src/HOL/Lambda/Commutation.thy	Fri Mar 09 08:45:50 2007 +0100
     5.3 @@ -26,7 +26,7 @@
     5.4  definition
     5.5    Church_Rosser :: "('a => 'a => bool) => bool" where
     5.6    "Church_Rosser R =
     5.7 -    (\<forall>x y. (join R (R^--1))^** x y --> (\<exists>z. R^** x z \<and> R^** y z))"
     5.8 +    (\<forall>x y. (sup R (R^--1))^** x y --> (\<exists>z. R^** x z \<and> R^** y z))"
     5.9  
    5.10  abbreviation
    5.11    confluent :: "('a => 'a => bool) => bool" where
    5.12 @@ -83,7 +83,7 @@
    5.13    done
    5.14  
    5.15  lemma commute_Un:
    5.16 -    "[| commute R T; commute S T |] ==> commute (join R S) T"
    5.17 +    "[| commute R T; commute S T |] ==> commute (sup R S) T"
    5.18    apply (unfold commute_def square_def)
    5.19    apply blast
    5.20    done
    5.21 @@ -92,7 +92,7 @@
    5.22  subsubsection {* diamond, confluence, and union *}
    5.23  
    5.24  lemma diamond_Un:
    5.25 -    "[| diamond R; diamond S; commute R S |] ==> diamond (join R S)"
    5.26 +    "[| diamond R; diamond S; commute R S |] ==> diamond (sup R S)"
    5.27    apply (unfold diamond_def)
    5.28    apply (assumption | rule commute_Un commute_sym)+
    5.29    done
    5.30 @@ -109,7 +109,7 @@
    5.31    done
    5.32  
    5.33  lemma confluent_Un:
    5.34 -    "[| confluent R; confluent S; commute (R^**) (S^**) |] ==> confluent (join R S)"
    5.35 +    "[| confluent R; confluent S; commute (R^**) (S^**) |] ==> confluent (sup R S)"
    5.36    apply (rule rtrancl_Un_rtrancl' [THEN subst])
    5.37    apply (blast dest: diamond_Un intro: diamond_confluent)
    5.38    done
    5.39 @@ -128,9 +128,9 @@
    5.40    apply (tactic {* safe_tac HOL_cs *})
    5.41     apply (tactic {*
    5.42       blast_tac (HOL_cs addIs
    5.43 -       [thm "join_right_le" RS thm "rtrancl_mono'" RS thm "predicate2D" RS thm "rtrancl_trans'",
    5.44 +       [thm "sup_ge2" RS thm "rtrancl_mono'" RS thm "predicate2D" RS thm "rtrancl_trans'",
    5.45          thm "rtrancl_converseI'", thm "conversepI",
    5.46 -        thm "join_left_le" RS thm "rtrancl_mono'" RS thm "predicate2D"]) 1 *})
    5.47 +        thm "sup_ge1" RS thm "rtrancl_mono'" RS thm "predicate2D"]) 1 *})
    5.48    apply (erule rtrancl_induct')
    5.49     apply blast
    5.50    apply (blast del: rtrancl.rtrancl_refl intro: rtrancl_trans')
     6.1 --- a/src/HOL/Lambda/Eta.thy	Tue Mar 06 16:40:32 2007 +0100
     6.2 +++ b/src/HOL/Lambda/Eta.thy	Fri Mar 09 08:45:50 2007 +0100
     6.3 @@ -163,7 +163,7 @@
     6.4      iff del: dB.distinct simp: dB.distinct)    (*23 seconds?*)
     6.5    done
     6.6  
     6.7 -lemma confluent_beta_eta: "confluent (join beta eta)"
     6.8 +lemma confluent_beta_eta: "confluent (sup beta eta)"
     6.9    apply (assumption |
    6.10      rule square_rtrancl_reflcl_commute confluent_Un
    6.11        beta_confluent eta_confluent square_beta_eta)+
    6.12 @@ -366,7 +366,7 @@
    6.13  qed
    6.14  
    6.15  theorem eta_postponement:
    6.16 -  assumes st: "(join beta eta)\<^sup>*\<^sup>* s t"
    6.17 +  assumes st: "(sup beta eta)\<^sup>*\<^sup>* s t"
    6.18    shows "(eta\<^sup>*\<^sup>* OO beta\<^sup>*\<^sup>*) s t" using st
    6.19  proof induct
    6.20    case 1
     7.1 --- a/src/HOL/Lattices.thy	Tue Mar 06 16:40:32 2007 +0100
     7.2 +++ b/src/HOL/Lattices.thy	Fri Mar 09 08:45:50 2007 +0100
     7.3 @@ -16,42 +16,47 @@
     7.4  Finite_Set}. In the longer term it may be better to define arbitrary
     7.5  sups and infs via @{text THE}. *}
     7.6  
     7.7 -locale lower_semilattice = order +
     7.8 +class lower_semilattice = order +
     7.9    fixes inf :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<sqinter>" 70)
    7.10 -  assumes inf_le1[simp]: "x \<sqinter> y \<sqsubseteq> x" and inf_le2[simp]: "x \<sqinter> y \<sqsubseteq> y"
    7.11 +  assumes inf_le1 [simp]: "x \<sqinter> y \<sqsubseteq> x" and inf_le2 [simp]: "x \<sqinter> y \<sqsubseteq> y"
    7.12    and inf_greatest: "x \<sqsubseteq> y \<Longrightarrow> x \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> y \<sqinter> z"
    7.13  
    7.14 -locale upper_semilattice = order +
    7.15 +class upper_semilattice = order +
    7.16    fixes sup :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<squnion>" 65)
    7.17 -  assumes sup_ge1[simp]: "x \<sqsubseteq> x \<squnion> y" and sup_ge2[simp]: "y \<sqsubseteq> x \<squnion> y"
    7.18 +  assumes sup_ge1 [simp]: "x \<sqsubseteq> x \<squnion> y" and sup_ge2 [simp]: "y \<sqsubseteq> x \<squnion> y"
    7.19    and sup_least: "y \<sqsubseteq> x \<Longrightarrow> z \<sqsubseteq> x \<Longrightarrow> y \<squnion> z \<sqsubseteq> x"
    7.20  
    7.21 -locale lattice = lower_semilattice + upper_semilattice
    7.22 +class lattice = lower_semilattice + upper_semilattice
    7.23  
    7.24  subsubsection{* Intro and elim rules*}
    7.25  
    7.26  context lower_semilattice
    7.27  begin
    7.28  
    7.29 -lemmas antisym_intro[intro!] = antisym
    7.30 +lemmas antisym_intro [intro!] = antisym
    7.31 +lemmas (in -) [rule del] = antisym_intro
    7.32  
    7.33  lemma le_infI1[intro]: "a \<sqsubseteq> x \<Longrightarrow> a \<sqinter> b \<sqsubseteq> x"
    7.34  apply(subgoal_tac "a \<sqinter> b \<sqsubseteq> a")
    7.35   apply(blast intro: order_trans)
    7.36  apply simp
    7.37  done
    7.38 +lemmas (in -) [rule del] = le_infI1
    7.39  
    7.40  lemma le_infI2[intro]: "b \<sqsubseteq> x \<Longrightarrow> a \<sqinter> b \<sqsubseteq> x"
    7.41  apply(subgoal_tac "a \<sqinter> b \<sqsubseteq> b")
    7.42   apply(blast intro: order_trans)
    7.43  apply simp
    7.44  done
    7.45 +lemmas (in -) [rule del] = le_infI2
    7.46  
    7.47  lemma le_infI[intro!]: "x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> b \<Longrightarrow> x \<sqsubseteq> a \<sqinter> b"
    7.48  by(blast intro: inf_greatest)
    7.49 +lemmas (in -) [rule del] = le_infI
    7.50  
    7.51 -lemma le_infE[elim!]: "x \<sqsubseteq> a \<sqinter> b \<Longrightarrow> (x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> b \<Longrightarrow> P) \<Longrightarrow> P"
    7.52 -by(blast intro: order_trans)
    7.53 +lemma le_infE [elim!]: "x \<sqsubseteq> a \<sqinter> b \<Longrightarrow> (x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> b \<Longrightarrow> P) \<Longrightarrow> P"
    7.54 +  by (blast intro: order_trans)
    7.55 +lemmas (in -) [rule del] = le_infE
    7.56  
    7.57  lemma le_inf_iff [simp]:
    7.58   "x \<sqsubseteq> y \<sqinter> z = (x \<sqsubseteq> y \<and> x \<sqsubseteq> z)"
    7.59 @@ -66,25 +71,31 @@
    7.60  context upper_semilattice
    7.61  begin
    7.62  
    7.63 -lemmas antisym_intro[intro!] = antisym
    7.64 +lemmas antisym_intro [intro!] = antisym
    7.65 +lemmas (in -) [rule del] = antisym_intro
    7.66  
    7.67  lemma le_supI1[intro]: "x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> a \<squnion> b"
    7.68  apply(subgoal_tac "a \<sqsubseteq> a \<squnion> b")
    7.69   apply(blast intro: order_trans)
    7.70  apply simp
    7.71  done
    7.72 +lemmas (in -) [rule del] = le_supI1
    7.73  
    7.74  lemma le_supI2[intro]: "x \<sqsubseteq> b \<Longrightarrow> x \<sqsubseteq> a \<squnion> b"
    7.75  apply(subgoal_tac "b \<sqsubseteq> a \<squnion> b")
    7.76   apply(blast intro: order_trans)
    7.77  apply simp
    7.78  done
    7.79 +lemmas (in -) [rule del] = le_supI2
    7.80  
    7.81  lemma le_supI[intro!]: "a \<sqsubseteq> x \<Longrightarrow> b \<sqsubseteq> x \<Longrightarrow> a \<squnion> b \<sqsubseteq> x"
    7.82  by(blast intro: sup_least)
    7.83 +lemmas (in -) [rule del] = le_supI
    7.84  
    7.85  lemma le_supE[elim!]: "a \<squnion> b \<sqsubseteq> x \<Longrightarrow> (a \<sqsubseteq> x \<Longrightarrow> b \<sqsubseteq> x \<Longrightarrow> P) \<Longrightarrow> P"
    7.86 -by(blast intro: order_trans)
    7.87 +  by (blast intro: order_trans)
    7.88 +lemmas (in -) [rule del] = le_supE
    7.89 +
    7.90  
    7.91  lemma ge_sup_conv[simp]:
    7.92   "x \<squnion> y \<sqsubseteq> z = (x \<sqsubseteq> z \<and> y \<sqsubseteq> z)"
    7.93 @@ -247,25 +258,24 @@
    7.94  apply (simp add: max_def linorder_not_le order_less_imp_le)
    7.95  unfolding min_def max_def by auto
    7.96  
    7.97 -text{* Now we have inherited antisymmetry as an intro-rule on all
    7.98 -linear orders. This is a problem because it applies to bool, which is
    7.99 -undesirable. *}
   7.100 +text {*
   7.101 +  Now we have inherited antisymmetry as an intro-rule on all
   7.102 +  linear orders. This is a problem because it applies to bool, which is
   7.103 +  undesirable.
   7.104 +*}
   7.105  
   7.106 -declare
   7.107 - min_max.antisym_intro[rule del]
   7.108 - min_max.le_infI[rule del] min_max.le_supI[rule del]
   7.109 - min_max.le_supE[rule del] min_max.le_infE[rule del]
   7.110 - min_max.le_supI1[rule del] min_max.le_supI2[rule del]
   7.111 - min_max.le_infI1[rule del] min_max.le_infI2[rule del]
   7.112 +lemmas [rule del] = min_max.antisym_intro  min_max.le_infI min_max.le_supI
   7.113 +  min_max.le_supE min_max.le_infE min_max.le_supI1 min_max.le_supI2
   7.114 +  min_max.le_infI1 min_max.le_infI2
   7.115  
   7.116  lemmas le_maxI1 = min_max.sup_ge1
   7.117  lemmas le_maxI2 = min_max.sup_ge2
   7.118   
   7.119  lemmas max_ac = min_max.sup_assoc min_max.sup_commute
   7.120 -               mk_left_commute[of max,OF min_max.sup_assoc min_max.sup_commute]
   7.121 +  mk_left_commute [of max, OF min_max.sup_assoc min_max.sup_commute]
   7.122  
   7.123  lemmas min_ac = min_max.inf_assoc min_max.inf_commute
   7.124 -               mk_left_commute[of min,OF min_max.inf_assoc min_max.inf_commute]
   7.125 +  mk_left_commute [of min, OF min_max.inf_assoc min_max.inf_commute]
   7.126  
   7.127  text {* ML legacy bindings *}
   7.128  
     8.1 --- a/src/HOL/Library/Continuity.thy	Tue Mar 06 16:40:32 2007 +0100
     8.2 +++ b/src/HOL/Library/Continuity.thy	Fri Mar 09 08:45:50 2007 +0100
     8.3 @@ -24,12 +24,12 @@
     8.4    "bot \<equiv> Sup {}"
     8.5  
     8.6  lemma SUP_nat_conv:
     8.7 -  "(SUP n::nat. M n::'a::comp_lat) = join (M 0) (SUP n. M(Suc n))"
     8.8 +  "(SUP n::nat. M n::'a::comp_lat) = sup (M 0) (SUP n. M(Suc n))"
     8.9  apply(rule order_antisym)
    8.10   apply(rule SUP_leI)
    8.11   apply(case_tac n)
    8.12    apply simp
    8.13 - apply (blast intro:le_SUPI le_joinI2)
    8.14 + apply (blast intro:le_SUPI le_supI2)
    8.15  apply(simp)
    8.16  apply (blast intro:SUP_leI le_SUPI)
    8.17  done
    8.18 @@ -40,16 +40,16 @@
    8.19    fix A B :: "'a" assume "A <= B"
    8.20    let ?C = "%i::nat. if i=0 then A else B"
    8.21    have "chain ?C" using `A <= B` by(simp add:chain_def)
    8.22 -  have "F B = join (F A) (F B)"
    8.23 +  have "F B = sup (F A) (F B)"
    8.24    proof -
    8.25 -    have "join A B = B" using `A <= B` by (simp add:join_absorp2)
    8.26 +    have "sup A B = B" using `A <= B` by (simp add:sup_absorb2)
    8.27      hence "F B = F(SUP i. ?C i)" by(simp add: SUP_nat_conv)
    8.28      also have "\<dots> = (SUP i. F(?C i))"
    8.29        using `chain ?C` `continuous F` by(simp add:continuous_def)
    8.30 -    also have "\<dots> = join (F A) (F B)" by(simp add: SUP_nat_conv)
    8.31 +    also have "\<dots> = sup (F A) (F B)" by(simp add: SUP_nat_conv)
    8.32      finally show ?thesis .
    8.33    qed
    8.34 -  thus "F A \<le> F B" by(subst le_def_join, simp)
    8.35 +  thus "F A \<le> F B" by(subst le_iff_sup, simp)
    8.36  qed
    8.37  
    8.38  lemma continuous_lfp:
     9.1 --- a/src/HOL/Library/Graphs.thy	Tue Mar 06 16:40:32 2007 +0100
     9.2 +++ b/src/HOL/Library/Graphs.thy	Fri Mar 09 08:45:50 2007 +0100
     9.3 @@ -155,10 +155,10 @@
     9.4  
     9.5  
     9.6  defs (overloaded)
     9.7 -  Meet_graph_def: "Meet == \<lambda>Gs. Graph (\<Inter>(dest_graph ` Gs))"
     9.8 +  Inf_graph_def: "Inf == \<lambda>Gs. Graph (\<Inter>(dest_graph ` Gs))"
     9.9  
    9.10  instance graph :: (type, type) comp_lat
    9.11 -  by default (auto simp:Meet_graph_def is_join_def graph_leq_def le_fun_def le_bool_def in_grplus has_edge_def)
    9.12 +  by default (auto simp: Inf_graph_def is_join_def graph_leq_def le_fun_def le_bool_def in_grplus has_edge_def)
    9.13  
    9.14  lemma plus_graph_is_join: "is_join ((op +)::('a::type, 'b::monoid_mult) graph \<Rightarrow> ('a,'b) graph \<Rightarrow> ('a,'b) graph)"
    9.15    unfolding is_join_def 
    9.16 @@ -172,7 +172,7 @@
    9.17  
    9.18  lemma plus_is_join:
    9.19    "(op +) =
    9.20 -  (join :: ('a::type, 'b::monoid_mult) graph \<Rightarrow> ('a,'b) graph \<Rightarrow> ('a,'b) graph)"
    9.21 +  (sup :: ('a::type, 'b::monoid_mult) graph \<Rightarrow> ('a,'b) graph \<Rightarrow> ('a,'b) graph)"
    9.22    using plus_graph_is_join by (simp add:join_unique)
    9.23  
    9.24  instance graph :: (type, monoid_mult) semiring_1
    9.25 @@ -693,7 +693,7 @@
    9.26  proof (rule prod_eqI)
    9.27    show "fst ?\<omega> = fst loop"
    9.28      by (auto simp:path_loop_def path_nth_def split_def k)
    9.29 -  
    9.30 +
    9.31    show "snd ?\<omega> = snd loop"
    9.32    proof (rule nth_equalityI[rule_format])
    9.33      show leneq: "length (snd ?\<omega>) = length (snd loop)"
    9.34 @@ -716,11 +716,5 @@
    9.35        by (simp add:path_nth_def)
    9.36    qed
    9.37  qed
    9.38 -      
    9.39 -
    9.40 -
    9.41 -
    9.42 -
    9.43 -
    9.44  
    9.45  end
    9.46 \ No newline at end of file
    10.1 --- a/src/HOL/List.thy	Tue Mar 06 16:40:32 2007 +0100
    10.2 +++ b/src/HOL/List.thy	Fri Mar 09 08:45:50 2007 +0100
    10.3 @@ -2228,21 +2228,21 @@
    10.4  
    10.5  lemmas lists_mono [mono] = listsp_mono [to_set]
    10.6  
    10.7 -lemma listsp_meetI:
    10.8 -  assumes l: "listsp A l" shows "listsp B l ==> listsp (meet A B) l" using l
    10.9 +lemma listsp_infI:
   10.10 +  assumes l: "listsp A l" shows "listsp B l ==> listsp (inf A B) l" using l
   10.11    by induct blast+
   10.12  
   10.13 -lemmas lists_IntI = listsp_meetI [to_set]
   10.14 -
   10.15 -lemma listsp_meet_eq [simp]: "listsp (meet A B) = meet (listsp A) (listsp B)"
   10.16 -proof (rule mono_meet [where f=listsp, THEN order_antisym])
   10.17 +lemmas lists_IntI = listsp_infI [to_set]
   10.18 +
   10.19 +lemma listsp_inf_eq [simp]: "listsp (inf A B) = inf (listsp A) (listsp B)"
   10.20 +proof (rule mono_inf [where f=listsp, THEN order_antisym])
   10.21    show "mono listsp" by (simp add: mono_def listsp_mono)
   10.22 -  show "meet (listsp A) (listsp B) \<le> listsp (meet A B)" by (blast intro: listsp_meetI)
   10.23 +  show "inf (listsp A) (listsp B) \<le> listsp (inf A B)" by (blast intro: listsp_infI)
   10.24  qed
   10.25  
   10.26 -lemmas listsp_conj_eq [simp] = listsp_meet_eq [simplified meet_fun_eq meet_bool_eq]
   10.27 -
   10.28 -lemmas lists_Int_eq [simp] = listsp_meet_eq [to_set]
   10.29 +lemmas listsp_conj_eq [simp] = listsp_inf_eq [simplified inf_fun_eq inf_bool_eq]
   10.30 +
   10.31 +lemmas lists_Int_eq [simp] = listsp_inf_eq [to_set]
   10.32  
   10.33  lemma append_in_listsp_conv [iff]:
   10.34       "(listsp A (xs @ ys)) = (listsp A xs \<and> listsp A ys)"
   10.35 @@ -2791,14 +2791,14 @@
   10.36  *}
   10.37  
   10.38  lemma mem_iff [normal post]:
   10.39 -  "(x mem xs) = (x \<in> set xs)"
   10.40 +  "x mem xs \<longleftrightarrow> x \<in> set xs"
   10.41    by (induct xs) auto
   10.42  
   10.43  lemmas in_set_code [code unfold] =
   10.44    mem_iff [symmetric, THEN eq_reflection]
   10.45  
   10.46  lemma empty_null [code inline]:
   10.47 -  "(xs = []) = null xs"
   10.48 +  "xs = [] \<longleftrightarrow> null xs"
   10.49    by (cases xs) simp_all
   10.50  
   10.51  lemmas null_empty [normal post] =
   10.52 @@ -2809,22 +2809,22 @@
   10.53    by (induct xs) auto
   10.54  
   10.55  lemma list_all_iff [normal post]:
   10.56 -  "list_all P xs = (\<forall>x \<in> set xs. P x)"
   10.57 +  "list_all P xs \<longleftrightarrow> (\<forall>x \<in> set xs. P x)"
   10.58    by (induct xs) auto
   10.59  
   10.60  lemmas list_ball_code [code unfold] =
   10.61    list_all_iff [symmetric, THEN eq_reflection]
   10.62  
   10.63  lemma list_all_append [simp]:
   10.64 -  "list_all P (xs @ ys) = (list_all P xs \<and> list_all P ys)"
   10.65 +  "list_all P (xs @ ys) \<longleftrightarrow> (list_all P xs \<and> list_all P ys)"
   10.66    by (induct xs) auto
   10.67  
   10.68  lemma list_all_rev [simp]:
   10.69 -  "list_all P (rev xs) = list_all P xs"
   10.70 +  "list_all P (rev xs) \<longleftrightarrow> list_all P xs"
   10.71    by (simp add: list_all_iff)
   10.72  
   10.73  lemma list_ex_iff [normal post]:
   10.74 -  "list_ex P xs = (\<exists>x \<in> set xs. P x)"
   10.75 +  "list_ex P xs \<longleftrightarrow> (\<exists>x \<in> set xs. P x)"
   10.76    by (induct xs) simp_all
   10.77  
   10.78  lemmas list_bex_code [code unfold] =
    11.1 --- a/src/HOL/Matrix/Matrix.thy	Tue Mar 06 16:40:32 2007 +0100
    11.2 +++ b/src/HOL/Matrix/Matrix.thy	Fri Mar 09 08:45:50 2007 +0100
    11.3 @@ -7,23 +7,21 @@
    11.4  imports MatrixGeneral
    11.5  begin
    11.6  
    11.7 -instance matrix :: (minus) minus ..
    11.8 +instance matrix :: ("{plus, zero}") plus
    11.9 +  plus_matrix_def: "A + B \<equiv> combine_matrix (op +) A B" ..
   11.10  
   11.11 -instance matrix :: (plus) plus ..
   11.12 -
   11.13 -instance matrix :: ("{plus,times}") times ..
   11.14 +instance matrix :: ("{minus, zero}") minus
   11.15 +  minus_matrix_def: "- A \<equiv> apply_matrix uminus A"
   11.16 +  diff_matrix_def: "A - B \<equiv> combine_matrix (op -) A B" ..
   11.17  
   11.18 -defs (overloaded)
   11.19 -  plus_matrix_def: "A + B == combine_matrix (op +) A B"
   11.20 -  diff_matrix_def: "A - B == combine_matrix (op -) A B"
   11.21 -  minus_matrix_def: "- A == apply_matrix uminus A"
   11.22 -  times_matrix_def: "A * B == mult_matrix (op *) (op +) A B"
   11.23 +instance matrix :: ("{plus, times, zero}") times
   11.24 +  times_matrix_def: "A * B \<equiv> mult_matrix (op *) (op +) A B" ..
   11.25  
   11.26 -lemma is_meet_combine_matrix_meet: "is_meet (combine_matrix meet)"
   11.27 -  by (simp_all add: is_meet_def le_matrix_def meet_left_le meet_right_le le_meetI)
   11.28 +lemma is_meet_combine_matrix_meet: "is_meet (combine_matrix inf)"
   11.29 +  by (simp_all add: is_meet_def le_matrix_def inf_le1 inf_le2 le_infI)
   11.30  
   11.31 -lemma is_join_combine_matrix_join: "is_join (combine_matrix join)"
   11.32 -  by (simp_all add: is_join_def le_matrix_def join_left_le join_right_le join_leI)
   11.33 +lemma is_join_combine_matrix_join: "is_join (combine_matrix sup)"
   11.34 +  by (simp_all add: is_join_def le_matrix_def sup_ge1 sup_ge2 le_supI)
   11.35  
   11.36  instance matrix :: (lordered_ab_group) lordered_ab_group_meet
   11.37  proof 
   11.38 @@ -58,7 +56,7 @@
   11.39  qed
   11.40  
   11.41  defs (overloaded)
   11.42 -  abs_matrix_def: "abs (A::('a::lordered_ab_group) matrix) == join A (- A)"
   11.43 +  abs_matrix_def: "abs (A::('a::lordered_ab_group) matrix) == sup A (- A)"
   11.44  
   11.45  instance matrix :: (lordered_ring) lordered_ring
   11.46  proof
   11.47 @@ -78,7 +76,7 @@
   11.48      apply (rule r_distributive_matrix[simplified r_distributive_def, THEN spec, THEN spec, THEN spec])
   11.49      apply (simp_all add: associative_def commutative_def ring_eq_simps)
   11.50      done  
   11.51 -  show "abs A = join A (-A)" 
   11.52 +  show "abs A = sup A (-A)" 
   11.53      by (simp add: abs_matrix_def)
   11.54    assume a: "A \<le> B"
   11.55    assume b: "0 \<le> C"
   11.56 @@ -102,7 +100,6 @@
   11.57  apply (simp add: times_matrix_def)
   11.58  apply (simp add: Rep_mult_matrix)
   11.59  done
   11.60 - 
   11.61  
   11.62  lemma apply_matrix_add: "! x y. f (x+y) = (f x) + (f y) \<Longrightarrow> f 0 = (0::'a) \<Longrightarrow> apply_matrix f ((a::('a::lordered_ab_group) matrix) + b) = (apply_matrix f a) + (apply_matrix f b)"
   11.63  apply (subst Rep_matrix_inject[symmetric])
   11.64 @@ -122,9 +119,9 @@
   11.65  lemma ncols_mult: "ncols ((A::('a::lordered_ring) matrix) * B) <= ncols B"
   11.66  by (simp add: times_matrix_def mult_ncols)
   11.67  
   11.68 -constdefs
   11.69 -  one_matrix :: "nat \<Rightarrow> ('a::{zero,one}) matrix"
   11.70 -  "one_matrix n == Abs_matrix (% j i. if j = i & j < n then 1 else 0)"
   11.71 +definition
   11.72 +  one_matrix :: "nat \<Rightarrow> ('a::{zero,one}) matrix" where
   11.73 +  "one_matrix n = Abs_matrix (% j i. if j = i & j < n then 1 else 0)"
   11.74  
   11.75  lemma Rep_one_matrix[simp]: "Rep_matrix (one_matrix n) j i = (if (j = i & j < n) then 1 else 0)"
   11.76  apply (simp add: one_matrix_def)
   11.77 @@ -289,13 +286,13 @@
   11.78  lemma Rep_minus[simp]: "Rep_matrix (-(A::_::lordered_ab_group)) x y = - (Rep_matrix A x y)"
   11.79    by (simp add: minus_matrix_def)
   11.80  
   11.81 -lemma join_matrix: "join (A::('a::lordered_ring) matrix) B = combine_matrix join A B"  
   11.82 -  apply (insert join_unique[of "(combine_matrix join)::('a matrix \<Rightarrow> 'a matrix \<Rightarrow> 'a matrix)", simplified is_join_combine_matrix_join])
   11.83 +lemma join_matrix: "sup (A::('a::lordered_ring) matrix) B = combine_matrix sup A B"  
   11.84 +  apply (insert join_unique[of "(combine_matrix sup)::('a matrix \<Rightarrow> 'a matrix \<Rightarrow> 'a matrix)", simplified is_join_combine_matrix_join])
   11.85    apply (simp)
   11.86    done
   11.87  
   11.88 -lemma meet_matrix: "meet (A::('a::lordered_ring) matrix) B = combine_matrix meet A B"
   11.89 -  apply (insert meet_unique[of "(combine_matrix meet)::('a matrix \<Rightarrow> 'a matrix \<Rightarrow> 'a matrix)", simplified is_meet_combine_matrix_meet])
   11.90 +lemma meet_matrix: "inf (A::('a::lordered_ring) matrix) B = combine_matrix inf A B"
   11.91 +  apply (insert meet_unique[of "(combine_matrix inf)::('a matrix \<Rightarrow> 'a matrix \<Rightarrow> 'a matrix)", simplified is_meet_combine_matrix_meet])
   11.92    apply (simp)
   11.93    done
   11.94  
    12.1 --- a/src/HOL/MicroJava/BV/JType.thy	Tue Mar 06 16:40:32 2007 +0100
    12.2 +++ b/src/HOL/MicroJava/BV/JType.thy	Fri Mar 09 08:45:50 2007 +0100
    12.3 @@ -108,7 +108,7 @@
    12.4  lemma wf_converse_subcls1_impl_acc_subtype:
    12.5    "wfP ((subcls1 G)^--1) \<Longrightarrow> acc (subtype G)"
    12.6  apply (unfold Semilat.acc_def lesssub_def)
    12.7 -apply (drule_tac p = "meet ((subcls1 G)^--1) op \<noteq>" in wfP_subset)
    12.8 +apply (drule_tac p = "inf ((subcls1 G)^--1) op \<noteq>" in wfP_subset)
    12.9   apply auto
   12.10  apply (drule wfP_trancl)
   12.11  apply (simp add: wfP_eq_minimal)
   12.12 @@ -151,7 +151,7 @@
   12.13  apply (erule rtrancl.cases)
   12.14   apply blast
   12.15  apply (drule rtrancl_converseI')
   12.16 -apply (subgoal_tac "(meet (subcls1 G) op \<noteq>)^--1 = (meet ((subcls1 G)^--1) op \<noteq>)")
   12.17 +apply (subgoal_tac "(inf (subcls1 G) op \<noteq>)^--1 = (inf ((subcls1 G)^--1) op \<noteq>)")
   12.18   prefer 2
   12.19   apply (simp add: converse_meet)
   12.20  apply simp
    13.1 --- a/src/HOL/OrderedGroup.thy	Tue Mar 06 16:40:32 2007 +0100
    13.2 +++ b/src/HOL/OrderedGroup.thy	Fri Mar 09 08:45:50 2007 +0100
    13.3 @@ -1,3 +1,4 @@
    13.4 +
    13.5  (*  Title:   HOL/OrderedGroup.thy
    13.6      ID:      $Id$
    13.7      Author:  Gertrud Bauer, Steven Obua, Lawrence C Paulson, and Markus Wenzel,
    13.8 @@ -570,97 +571,99 @@
    13.9  
   13.10  axclass lordered_ab_group_join < pordered_ab_group_add, join_semilorder
   13.11  
   13.12 -lemma add_meet_distrib_left: "a + (meet b c) = meet (a + b) (a + (c::'a::{pordered_ab_group_add, meet_semilorder}))"
   13.13 +lemma add_inf_distrib_left: "a + (inf b c) = inf (a + b) (a + (c::'a::{pordered_ab_group_add, meet_semilorder}))"
   13.14  apply (rule order_antisym)
   13.15 -apply (simp_all add: le_meetI)
   13.16 +apply (simp_all add: le_infI)
   13.17  apply (rule add_le_imp_le_left [of "-a"])
   13.18  apply (simp only: add_assoc[symmetric], simp)
   13.19  apply rule
   13.20  apply (rule add_le_imp_le_left[of "a"], simp only: add_assoc[symmetric], simp)+
   13.21  done
   13.22  
   13.23 -lemma add_join_distrib_left: "a + (join b c) = join (a + b) (a+ (c::'a::{pordered_ab_group_add, join_semilorder}))" 
   13.24 +lemma add_sup_distrib_left: "a + (sup b c) = sup (a + b) (a+ (c::'a::{pordered_ab_group_add, join_semilorder}))" 
   13.25  apply (rule order_antisym)
   13.26  apply (rule add_le_imp_le_left [of "-a"])
   13.27  apply (simp only: add_assoc[symmetric], simp)
   13.28  apply rule
   13.29  apply (rule add_le_imp_le_left [of "a"], simp only: add_assoc[symmetric], simp)+
   13.30 -apply (rule join_leI)
   13.31 +apply (rule le_supI)
   13.32  apply (simp_all)
   13.33  done
   13.34  
   13.35 -lemma is_join_neg_meet: "is_join (% (a::'a::{pordered_ab_group_add, meet_semilorder}) b. - (meet (-a) (-b)))"
   13.36 +lemma is_join_neg_inf: "is_join (% (a::'a::{pordered_ab_group_add, meet_semilorder}) b. - (inf (-a) (-b)))"
   13.37  apply (auto simp add: is_join_def)
   13.38 -apply (rule_tac c="meet (-a) (-b)" in add_le_imp_le_right, simp, simp add: add_meet_distrib_left)
   13.39 -apply (rule_tac c="meet (-a) (-b)" in add_le_imp_le_right, simp, simp add: add_meet_distrib_left)
   13.40 +apply (rule_tac c="inf (-a) (-b)" in add_le_imp_le_right, simp, simp add: add_inf_distrib_left)
   13.41 +apply (rule_tac c="inf (-a) (-b)" in add_le_imp_le_right, simp, simp add: add_inf_distrib_left)
   13.42  apply (subst neg_le_iff_le[symmetric]) 
   13.43 -apply (simp add: le_meetI)
   13.44 +apply (simp add: le_infI)
   13.45  done
   13.46  
   13.47 -lemma is_meet_neg_join: "is_meet (% (a::'a::{pordered_ab_group_add, join_semilorder}) b. - (join (-a) (-b)))"
   13.48 +lemma is_meet_neg_sup: "is_meet (% (a::'a::{pordered_ab_group_add, join_semilorder}) b. - (sup (-a) (-b)))"
   13.49  apply (auto simp add: is_meet_def)
   13.50 -apply (rule_tac c="join (-a) (-b)" in add_le_imp_le_right, simp, simp add: add_join_distrib_left)
   13.51 -apply (rule_tac c="join (-a) (-b)" in add_le_imp_le_right, simp, simp add: add_join_distrib_left)
   13.52 +apply (rule_tac c="sup (-a) (-b)" in add_le_imp_le_right, simp, simp add: add_sup_distrib_left)
   13.53 +apply (rule_tac c="sup (-a) (-b)" in add_le_imp_le_right, simp, simp add: add_sup_distrib_left)
   13.54  apply (subst neg_le_iff_le[symmetric]) 
   13.55 -apply (simp add: join_leI)
   13.56 +apply (simp add: le_supI)
   13.57  done
   13.58  
   13.59  axclass lordered_ab_group \<subseteq> pordered_ab_group_add, lorder
   13.60  
   13.61 -instance lordered_ab_group_meet \<subseteq> lordered_ab_group
   13.62 -proof 
   13.63 -  show "? j. is_join (j::'a\<Rightarrow>'a\<Rightarrow>('a::lordered_ab_group_meet))" by (blast intro: is_join_neg_meet)
   13.64 -qed
   13.65 -
   13.66  instance lordered_ab_group_join \<subseteq> lordered_ab_group
   13.67  proof
   13.68 -  show "? m. is_meet (m::'a\<Rightarrow>'a\<Rightarrow>('a::lordered_ab_group_join))" by (blast intro: is_meet_neg_join)
   13.69 +  show "? m. is_meet (m::'a\<Rightarrow>'a\<Rightarrow>('a::lordered_ab_group_join))" by (blast intro: is_meet_neg_sup)
   13.70  qed
   13.71  
   13.72 -lemma add_join_distrib_right: "(join a b) + (c::'a::lordered_ab_group) = join (a+c) (b+c)"
   13.73 +instance lordered_ab_group_meet \<subseteq> lordered_ab_group
   13.74 +proof 
   13.75 +  show "? j. is_join (j::'a\<Rightarrow>'a\<Rightarrow>('a::lordered_ab_group_meet))" by (blast intro: is_join_neg_inf)
   13.76 +qed
   13.77 +
   13.78 +lemma add_inf_distrib_right: "(inf a b) + (c::'a::lordered_ab_group) = inf (a+c) (b+c)"
   13.79  proof -
   13.80 -  have "c + (join a b) = join (c+a) (c+b)" by (simp add: add_join_distrib_left)
   13.81 +  have "c + (inf a b) = inf (c+a) (c+b)" by (simp add: add_inf_distrib_left)
   13.82    thus ?thesis by (simp add: add_commute)
   13.83  qed
   13.84  
   13.85 -lemma add_meet_distrib_right: "(meet a b) + (c::'a::lordered_ab_group) = meet (a+c) (b+c)"
   13.86 +lemma add_sup_distrib_right: "(sup a b) + (c::'a::lordered_ab_group) = sup (a+c) (b+c)"
   13.87  proof -
   13.88 -  have "c + (meet a b) = meet (c+a) (c+b)" by (simp add: add_meet_distrib_left)
   13.89 +  have "c + (sup a b) = sup (c+a) (c+b)" by (simp add: add_sup_distrib_left)
   13.90    thus ?thesis by (simp add: add_commute)
   13.91  qed
   13.92  
   13.93 -lemmas add_meet_join_distribs = add_meet_distrib_right add_meet_distrib_left add_join_distrib_right add_join_distrib_left
   13.94 +lemmas add_sup_inf_distribs = add_inf_distrib_right add_inf_distrib_left add_sup_distrib_right add_sup_distrib_left
   13.95  
   13.96 -lemma join_eq_neg_meet: "join a (b::'a::lordered_ab_group) = - meet (-a) (-b)"
   13.97 -by (simp add: is_join_unique[OF is_join_join is_join_neg_meet])
   13.98 +lemma sup_eq_neg_inf: "sup a (b::'a::lordered_ab_group) = - inf (-a) (-b)"
   13.99 +by (simp add: is_join_unique[OF is_join_join is_join_neg_inf])
  13.100  
  13.101 -lemma meet_eq_neg_join: "meet a (b::'a::lordered_ab_group) = - join (-a) (-b)"
  13.102 -by (simp add: is_meet_unique[OF is_meet_meet is_meet_neg_join])
  13.103 +lemma inf_eq_neg_sup: "inf a (b::'a::lordered_ab_group) = - sup (-a) (-b)"
  13.104 +by (simp add: is_meet_unique[OF is_meet_meet is_meet_neg_sup])
  13.105  
  13.106 -lemma add_eq_meet_join: "a + b = (join a b) + (meet a (b::'a::lordered_ab_group))"
  13.107 +lemma add_eq_inf_sup: "a + b = (sup a b) + (inf a (b::'a::lordered_ab_group))"
  13.108  proof -
  13.109 -  have "0 = - meet 0 (a-b) + meet (a-b) 0" by (simp add: meet_comm)
  13.110 -  hence "0 = join 0 (b-a) + meet (a-b) 0" by (simp add: meet_eq_neg_join)
  13.111 -  hence "0 = (-a + join a b) + (meet a b + (-b))"
  13.112 -    apply (simp add: add_join_distrib_left add_meet_distrib_right)
  13.113 +  have "0 = - inf 0 (a-b) + inf (a-b) 0" by (simp add: inf_commute)
  13.114 +  hence "0 = sup 0 (b-a) + inf (a-b) 0" by (simp add: inf_eq_neg_sup)
  13.115 +  hence "0 = (-a + sup a b) + (inf a b + (-b))"
  13.116 +    apply (simp add: add_sup_distrib_left add_inf_distrib_right)
  13.117      by (simp add: diff_minus add_commute)
  13.118    thus ?thesis
  13.119      apply (simp add: compare_rls)
  13.120 -    apply (subst add_left_cancel[symmetric, of "a+b" "join a b + meet a b" "-a"])
  13.121 +    apply (subst add_left_cancel[symmetric, of "a+b" "sup a b + inf a b" "-a"])
  13.122      apply (simp only: add_assoc, simp add: add_assoc[symmetric])
  13.123      done
  13.124  qed
  13.125  
  13.126  subsection {* Positive Part, Negative Part, Absolute Value *}
  13.127  
  13.128 -constdefs
  13.129 -  pprt :: "'a \<Rightarrow> ('a::lordered_ab_group)"
  13.130 -  "pprt x == join x 0"
  13.131 -  nprt :: "'a \<Rightarrow> ('a::lordered_ab_group)"
  13.132 -  "nprt x == meet x 0"
  13.133 +definition
  13.134 +  nprt :: "'a \<Rightarrow> ('a::lordered_ab_group)" where
  13.135 +  "nprt x = inf x 0"
  13.136 +
  13.137 +definition
  13.138 +  pprt :: "'a \<Rightarrow> ('a::lordered_ab_group)" where
  13.139 +  "pprt x = sup x 0"
  13.140  
  13.141  lemma prts: "a = pprt a + nprt a"
  13.142 -by (simp add: pprt_def nprt_def add_eq_meet_join[symmetric])
  13.143 +by (simp add: pprt_def nprt_def add_eq_inf_sup[symmetric])
  13.144  
  13.145  lemma zero_le_pprt[simp]: "0 \<le> pprt a"
  13.146  by (simp add: pprt_def)
  13.147 @@ -687,53 +690,53 @@
  13.148  lemma nprt_0[simp]: "nprt 0 = 0" by (simp add: nprt_def)
  13.149  
  13.150  lemma pprt_eq_id[simp]: "0 <= x \<Longrightarrow> pprt x = x"
  13.151 -  by (simp add: pprt_def le_def_join join_aci)
  13.152 +  by (simp add: pprt_def le_iff_sup sup_aci)
  13.153  
  13.154  lemma nprt_eq_id[simp]: "x <= 0 \<Longrightarrow> nprt x = x"
  13.155 -  by (simp add: nprt_def le_def_meet meet_aci)
  13.156 +  by (simp add: nprt_def le_iff_inf inf_aci)
  13.157  
  13.158  lemma pprt_eq_0[simp]: "x <= 0 \<Longrightarrow> pprt x = 0"
  13.159 -  by (simp add: pprt_def le_def_join join_aci)
  13.160 +  by (simp add: pprt_def le_iff_sup sup_aci)
  13.161  
  13.162  lemma nprt_eq_0[simp]: "0 <= x \<Longrightarrow> nprt x = 0"
  13.163 -  by (simp add: nprt_def le_def_meet meet_aci)
  13.164 +  by (simp add: nprt_def le_iff_inf inf_aci)
  13.165  
  13.166 -lemma join_0_imp_0: "join a (-a) = 0 \<Longrightarrow> a = (0::'a::lordered_ab_group)"
  13.167 +lemma sup_0_imp_0: "sup a (-a) = 0 \<Longrightarrow> a = (0::'a::lordered_ab_group)"
  13.168  proof -
  13.169    {
  13.170      fix a::'a
  13.171 -    assume hyp: "join a (-a) = 0"
  13.172 -    hence "join a (-a) + a = a" by (simp)
  13.173 -    hence "join (a+a) 0 = a" by (simp add: add_join_distrib_right) 
  13.174 -    hence "join (a+a) 0 <= a" by (simp)
  13.175 -    hence "0 <= a" by (blast intro: order_trans meet_join_le)
  13.176 +    assume hyp: "sup a (-a) = 0"
  13.177 +    hence "sup a (-a) + a = a" by (simp)
  13.178 +    hence "sup (a+a) 0 = a" by (simp add: add_sup_distrib_right) 
  13.179 +    hence "sup (a+a) 0 <= a" by (simp)
  13.180 +    hence "0 <= a" by (blast intro: order_trans inf_sup_ord)
  13.181    }
  13.182    note p = this
  13.183 -  assume hyp:"join a (-a) = 0"
  13.184 -  hence hyp2:"join (-a) (-(-a)) = 0" by (simp add: join_comm)
  13.185 +  assume hyp:"sup a (-a) = 0"
  13.186 +  hence hyp2:"sup (-a) (-(-a)) = 0" by (simp add: sup_commute)
  13.187    from p[OF hyp] p[OF hyp2] show "a = 0" by simp
  13.188  qed
  13.189  
  13.190 -lemma meet_0_imp_0: "meet a (-a) = 0 \<Longrightarrow> a = (0::'a::lordered_ab_group)"
  13.191 -apply (simp add: meet_eq_neg_join)
  13.192 -apply (simp add: join_comm)
  13.193 -apply (erule join_0_imp_0)
  13.194 +lemma inf_0_imp_0: "inf a (-a) = 0 \<Longrightarrow> a = (0::'a::lordered_ab_group)"
  13.195 +apply (simp add: inf_eq_neg_sup)
  13.196 +apply (simp add: sup_commute)
  13.197 +apply (erule sup_0_imp_0)
  13.198  done
  13.199  
  13.200 -lemma join_0_eq_0[simp]: "(join a (-a) = 0) = (a = (0::'a::lordered_ab_group))"
  13.201 -by (auto, erule join_0_imp_0)
  13.202 +lemma inf_0_eq_0[simp]: "(inf a (-a) = 0) = (a = (0::'a::lordered_ab_group))"
  13.203 +by (auto, erule inf_0_imp_0)
  13.204  
  13.205 -lemma meet_0_eq_0[simp]: "(meet a (-a) = 0) = (a = (0::'a::lordered_ab_group))"
  13.206 -by (auto, erule meet_0_imp_0)
  13.207 +lemma sup_0_eq_0[simp]: "(sup a (-a) = 0) = (a = (0::'a::lordered_ab_group))"
  13.208 +by (auto, erule sup_0_imp_0)
  13.209  
  13.210  lemma zero_le_double_add_iff_zero_le_single_add[simp]: "(0 \<le> a + a) = (0 \<le> (a::'a::lordered_ab_group))"
  13.211  proof
  13.212    assume "0 <= a + a"
  13.213 -  hence a:"meet (a+a) 0 = 0" by (simp add: le_def_meet meet_comm)
  13.214 -  have "(meet a 0)+(meet a 0) = meet (meet (a+a) 0) a" (is "?l=_") by (simp add: add_meet_join_distribs meet_aci)
  13.215 -  hence "?l = 0 + meet a 0" by (simp add: a, simp add: meet_comm)
  13.216 -  hence "meet a 0 = 0" by (simp only: add_right_cancel)
  13.217 -  then show "0 <= a" by (simp add: le_def_meet meet_comm)    
  13.218 +  hence a:"inf (a+a) 0 = 0" by (simp add: le_iff_inf inf_commute)
  13.219 +  have "(inf a 0)+(inf a 0) = inf (inf (a+a) 0) a" (is "?l=_") by (simp add: add_sup_inf_distribs inf_aci)
  13.220 +  hence "?l = 0 + inf a 0" by (simp add: a, simp add: inf_commute)
  13.221 +  hence "inf a 0 = 0" by (simp only: add_right_cancel)
  13.222 +  then show "0 <= a" by (simp add: le_iff_inf inf_commute)    
  13.223  next  
  13.224    assume a: "0 <= a"
  13.225    show "0 <= a + a" by (simp add: add_mono[OF a a, simplified])
  13.226 @@ -759,7 +762,7 @@
  13.227  qed
  13.228  
  13.229  axclass lordered_ab_group_abs \<subseteq> lordered_ab_group
  13.230 -  abs_lattice: "abs x = join x (-x)"
  13.231 +  abs_lattice: "abs x = sup x (-x)"
  13.232  
  13.233  lemma abs_zero[simp]: "abs 0 = (0::'a::lordered_ab_group_abs)"
  13.234  by (simp add: abs_lattice)
  13.235 @@ -773,22 +776,22 @@
  13.236    thus ?thesis by simp
  13.237  qed
  13.238  
  13.239 -lemma neg_meet_eq_join[simp]: "- meet a (b::_::lordered_ab_group) = join (-a) (-b)"
  13.240 -by (simp add: meet_eq_neg_join)
  13.241 +lemma neg_inf_eq_sup[simp]: "- inf a (b::_::lordered_ab_group) = sup (-a) (-b)"
  13.242 +by (simp add: inf_eq_neg_sup)
  13.243  
  13.244 -lemma neg_join_eq_meet[simp]: "- join a (b::_::lordered_ab_group) = meet (-a) (-b)"
  13.245 -by (simp del: neg_meet_eq_join add: join_eq_neg_meet)
  13.246 +lemma neg_sup_eq_inf[simp]: "- sup a (b::_::lordered_ab_group) = inf (-a) (-b)"
  13.247 +by (simp del: neg_inf_eq_sup add: sup_eq_neg_inf)
  13.248  
  13.249 -lemma join_eq_if: "join a (-a) = (if a < 0 then -a else (a::'a::{lordered_ab_group, linorder}))"
  13.250 +lemma sup_eq_if: "sup a (-a) = (if a < 0 then -a else (a::'a::{lordered_ab_group, linorder}))"
  13.251  proof -
  13.252    note b = add_le_cancel_right[of a a "-a",symmetric,simplified]
  13.253    have c: "a + a = 0 \<Longrightarrow> -a = a" by (rule add_right_imp_eq[of _ a], simp)
  13.254 -  show ?thesis by (auto simp add: join_max max_def b linorder_not_less)
  13.255 +  show ?thesis by (auto simp add: max_def b linorder_not_less join_max)
  13.256  qed
  13.257  
  13.258  lemma abs_if_lattice: "\<bar>a\<bar> = (if a < 0 then -a else (a::'a::{lordered_ab_group_abs, linorder}))"
  13.259  proof -
  13.260 -  show ?thesis by (simp add: abs_lattice join_eq_if)
  13.261 +  show ?thesis by (simp add: abs_lattice sup_eq_if)
  13.262  qed
  13.263  
  13.264  lemma abs_ge_zero[simp]: "0 \<le> abs (a::'a::lordered_ab_group_abs)"
  13.265 @@ -824,16 +827,16 @@
  13.266  
  13.267  lemma abs_prts: "abs (a::_::lordered_ab_group_abs) = pprt a - nprt a"
  13.268  apply (simp add: pprt_def nprt_def diff_minus)
  13.269 -apply (simp add: add_meet_join_distribs join_aci abs_lattice[symmetric])
  13.270 -apply (subst join_absorp2, auto)
  13.271 +apply (simp add: add_sup_inf_distribs sup_aci abs_lattice[symmetric])
  13.272 +apply (subst sup_absorb2, auto)
  13.273  done
  13.274  
  13.275  lemma abs_minus_cancel [simp]: "abs (-a) = abs(a::'a::lordered_ab_group_abs)"
  13.276 -by (simp add: abs_lattice join_comm)
  13.277 +by (simp add: abs_lattice sup_commute)
  13.278  
  13.279  lemma abs_idempotent [simp]: "abs (abs a) = abs (a::'a::lordered_ab_group_abs)"
  13.280  apply (simp add: abs_lattice[of "abs a"])
  13.281 -apply (subst join_absorp1)
  13.282 +apply (subst sup_absorb1)
  13.283  apply (rule order_trans[of _ 0])
  13.284  by auto
  13.285  
  13.286 @@ -847,22 +850,22 @@
  13.287  qed
  13.288  
  13.289  lemma zero_le_iff_zero_nprt: "(0 \<le> a) = (nprt a = 0)"
  13.290 -by (simp add: le_def_meet nprt_def meet_comm)
  13.291 +by (simp add: le_iff_inf nprt_def inf_commute)
  13.292  
  13.293  lemma le_zero_iff_zero_pprt: "(a \<le> 0) = (pprt a = 0)"
  13.294 -by (simp add: le_def_join pprt_def join_comm)
  13.295 +by (simp add: le_iff_sup pprt_def sup_commute)
  13.296  
  13.297  lemma le_zero_iff_pprt_id: "(0 \<le> a) = (pprt a = a)"
  13.298 -by (simp add: le_def_join pprt_def join_comm)
  13.299 +by (simp add: le_iff_sup pprt_def sup_commute)
  13.300  
  13.301  lemma zero_le_iff_nprt_id: "(a \<le> 0) = (nprt a = a)"
  13.302 -by (simp add: le_def_meet nprt_def meet_comm)
  13.303 +by (simp add: le_iff_inf nprt_def inf_commute)
  13.304  
  13.305  lemma pprt_mono[simp]: "(a::_::lordered_ab_group) <= b \<Longrightarrow> pprt a <= pprt b"
  13.306 -  by (simp add: le_def_join pprt_def join_aci)
  13.307 +  by (simp add: le_iff_sup pprt_def sup_aci)
  13.308  
  13.309  lemma nprt_mono[simp]: "(a::_::lordered_ab_group) <= b \<Longrightarrow> nprt a <= nprt b"
  13.310 -  by (simp add: le_def_meet nprt_def meet_aci)
  13.311 +  by (simp add: le_iff_inf nprt_def inf_aci)
  13.312  
  13.313  lemma pprt_neg: "pprt (-x) = - nprt x"
  13.314    by (simp add: pprt_def nprt_def)
  13.315 @@ -887,7 +890,7 @@
  13.316  by (rule abs_of_nonpos, rule order_less_imp_le)
  13.317  
  13.318  lemma abs_leI: "[|a \<le> b; -a \<le> b|] ==> abs a \<le> (b::'a::lordered_ab_group_abs)"
  13.319 -by (simp add: abs_lattice join_leI)
  13.320 +by (simp add: abs_lattice le_supI)
  13.321  
  13.322  lemma le_minus_self_iff: "(a \<le> -a) = (a \<le> (0::'a::lordered_ab_group))"
  13.323  proof -
  13.324 @@ -914,14 +917,14 @@
  13.325  
  13.326  lemma abs_triangle_ineq: "abs(a+b) \<le> abs a + abs(b::'a::lordered_ab_group_abs)"
  13.327  proof -
  13.328 -  have g:"abs a + abs b = join (a+b) (join (-a-b) (join (-a+b) (a + (-b))))" (is "_=join ?m ?n")
  13.329 -    by (simp add: abs_lattice add_meet_join_distribs join_aci diff_minus)
  13.330 -  have a:"a+b <= join ?m ?n" by (simp)
  13.331 +  have g:"abs a + abs b = sup (a+b) (sup (-a-b) (sup (-a+b) (a + (-b))))" (is "_=sup ?m ?n")
  13.332 +    by (simp add: abs_lattice add_sup_inf_distribs sup_aci diff_minus)
  13.333 +  have a:"a+b <= sup ?m ?n" by (simp)
  13.334    have b:"-a-b <= ?n" by (simp) 
  13.335 -  have c:"?n <= join ?m ?n" by (simp)
  13.336 -  from b c have d: "-a-b <= join ?m ?n" by(rule order_trans)
  13.337 +  have c:"?n <= sup ?m ?n" by (simp)
  13.338 +  from b c have d: "-a-b <= sup ?m ?n" by(rule order_trans)
  13.339    have e:"-a-b = -(a+b)" by (simp add: diff_minus)
  13.340 -  from a d e have "abs(a+b) <= join ?m ?n" 
  13.341 +  from a d e have "abs(a+b) <= sup ?m ?n" 
  13.342      by (drule_tac abs_leI, auto)
  13.343    with g[symmetric] show ?thesis by simp
  13.344  qed
  13.345 @@ -1126,24 +1129,24 @@
  13.346  val compare_rls = thms "compare_rls";
  13.347  val eq_iff_diff_eq_0 = thm "eq_iff_diff_eq_0";
  13.348  val le_iff_diff_le_0 = thm "le_iff_diff_le_0";
  13.349 -val add_meet_distrib_left = thm "add_meet_distrib_left";
  13.350 -val add_join_distrib_left = thm "add_join_distrib_left";
  13.351 -val is_join_neg_meet = thm "is_join_neg_meet";
  13.352 -val is_meet_neg_join = thm "is_meet_neg_join";
  13.353 -val add_join_distrib_right = thm "add_join_distrib_right";
  13.354 -val add_meet_distrib_right = thm "add_meet_distrib_right";
  13.355 -val add_meet_join_distribs = thms "add_meet_join_distribs";
  13.356 -val join_eq_neg_meet = thm "join_eq_neg_meet";
  13.357 -val meet_eq_neg_join = thm "meet_eq_neg_join";
  13.358 -val add_eq_meet_join = thm "add_eq_meet_join";
  13.359 +val add_inf_distrib_left = thm "add_inf_distrib_left";
  13.360 +val add_sup_distrib_left = thm "add_sup_distrib_left";
  13.361 +val is_join_neg_inf = thm "is_join_neg_inf";
  13.362 +val is_meet_neg_sup = thm "is_meet_neg_sup";
  13.363 +val add_sup_distrib_right = thm "add_sup_distrib_right";
  13.364 +val add_inf_distrib_right = thm "add_inf_distrib_right";
  13.365 +val add_sup_inf_distribs = thms "add_sup_inf_distribs";
  13.366 +val sup_eq_neg_inf = thm "sup_eq_neg_inf";
  13.367 +val inf_eq_neg_sup = thm "inf_eq_neg_sup";
  13.368 +val add_eq_inf_sup = thm "add_eq_inf_sup";
  13.369  val prts = thm "prts";
  13.370  val zero_le_pprt = thm "zero_le_pprt";
  13.371  val nprt_le_zero = thm "nprt_le_zero";
  13.372  val le_eq_neg = thm "le_eq_neg";
  13.373 -val join_0_imp_0 = thm "join_0_imp_0";
  13.374 -val meet_0_imp_0 = thm "meet_0_imp_0";
  13.375 -val join_0_eq_0 = thm "join_0_eq_0";
  13.376 -val meet_0_eq_0 = thm "meet_0_eq_0";
  13.377 +val sup_0_imp_0 = thm "sup_0_imp_0";
  13.378 +val inf_0_imp_0 = thm "inf_0_imp_0";
  13.379 +val sup_0_eq_0 = thm "sup_0_eq_0";
  13.380 +val inf_0_eq_0 = thm "inf_0_eq_0";
  13.381  val zero_le_double_add_iff_zero_le_single_add = thm "zero_le_double_add_iff_zero_le_single_add";
  13.382  val double_add_le_zero_iff_single_add_le_zero = thm "double_add_le_zero_iff_single_add_le_zero";
  13.383  val double_add_less_zero_iff_single_less_zero = thm "double_add_less_zero_iff_single_less_zero";
  13.384 @@ -1151,9 +1154,9 @@
  13.385  val abs_zero = thm "abs_zero";
  13.386  val abs_eq_0 = thm "abs_eq_0";
  13.387  val abs_0_eq = thm "abs_0_eq";
  13.388 -val neg_meet_eq_join = thm "neg_meet_eq_join";
  13.389 -val neg_join_eq_meet = thm "neg_join_eq_meet";
  13.390 -val join_eq_if = thm "join_eq_if";
  13.391 +val neg_inf_eq_sup = thm "neg_inf_eq_sup";
  13.392 +val neg_sup_eq_inf = thm "neg_sup_eq_inf";
  13.393 +val sup_eq_if = thm "sup_eq_if";
  13.394  val abs_if_lattice = thm "abs_if_lattice";
  13.395  val abs_ge_zero = thm "abs_ge_zero";
  13.396  val abs_le_zero_iff = thm "abs_le_zero_iff";
  13.397 @@ -1161,10 +1164,10 @@
  13.398  val abs_not_less_zero = thm "abs_not_less_zero";
  13.399  val abs_ge_self = thm "abs_ge_self";
  13.400  val abs_ge_minus_self = thm "abs_ge_minus_self";
  13.401 -val le_imp_join_eq = thm "join_absorp2";
  13.402 -val ge_imp_join_eq = thm "join_absorp1";
  13.403 -val le_imp_meet_eq = thm "meet_absorp1";
  13.404 -val ge_imp_meet_eq = thm "meet_absorp2";
  13.405 +val le_imp_join_eq = thm "sup_absorb2";
  13.406 +val ge_imp_join_eq = thm "sup_absorb1";
  13.407 +val le_imp_meet_eq = thm "inf_absorb1";
  13.408 +val ge_imp_meet_eq = thm "inf_absorb2";
  13.409  val abs_prts = thm "abs_prts";
  13.410  val abs_minus_cancel = thm "abs_minus_cancel";
  13.411  val abs_idempotent = thm "abs_idempotent";
  13.412 @@ -1173,8 +1176,6 @@
  13.413  val le_zero_iff_pprt_id = thm "le_zero_iff_pprt_id";
  13.414  val zero_le_iff_nprt_id = thm "zero_le_iff_nprt_id";
  13.415  val iff2imp = thm "iff2imp";
  13.416 -(* val imp_abs_id = thm "imp_abs_id";
  13.417 -val imp_abs_neg_id = thm "imp_abs_neg_id"; *)
  13.418  val abs_leI = thm "abs_leI";
  13.419  val le_minus_self_iff = thm "le_minus_self_iff";
  13.420  val minus_le_self_iff = thm "minus_le_self_iff";
    14.1 --- a/src/HOL/Predicate.thy	Tue Mar 06 16:40:32 2007 +0100
    14.2 +++ b/src/HOL/Predicate.thy	Fri Mar 09 08:45:50 2007 +0100
    14.3 @@ -202,28 +202,28 @@
    14.4  
    14.5  subsubsection {* Binary union *}
    14.6  
    14.7 -lemma member_Un [pred_set_conv]: "join (member R) (member S) = member (R Un S)"
    14.8 -  by (simp add: expand_fun_eq join_fun_eq join_bool_eq)
    14.9 +lemma member_Un [pred_set_conv]: "sup (member R) (member S) = member (R Un S)"
   14.10 +  by (simp add: expand_fun_eq sup_fun_eq sup_bool_eq)
   14.11  
   14.12 -lemma member2_Un [pred_set_conv]: "join (member2 R) (member2 S) = member2 (R Un S)"
   14.13 -  by (simp add: expand_fun_eq join_fun_eq join_bool_eq)
   14.14 +lemma member2_Un [pred_set_conv]: "sup (member2 R) (member2 S) = member2 (R Un S)"
   14.15 +  by (simp add: expand_fun_eq sup_fun_eq sup_bool_eq)
   14.16  
   14.17 -lemma join1_iff [simp]: "(join A B x) = (A x | B x)"
   14.18 -  by (simp add: join_fun_eq join_bool_eq)
   14.19 +lemma sup1_iff [simp]: "sup A B x \<longleftrightarrow> A x | B x"
   14.20 +  by (simp add: sup_fun_eq sup_bool_eq)
   14.21  
   14.22 -lemma join2_iff [simp]: "(join A B x y) = (A x y | B x y)"
   14.23 -  by (simp add: join_fun_eq join_bool_eq)
   14.24 +lemma sup2_iff [simp]: "sup A B x y \<longleftrightarrow> A x y | B x y"
   14.25 +  by (simp add: sup_fun_eq sup_bool_eq)
   14.26  
   14.27 -lemma join1I1 [elim?]: "A x ==> join A B x"
   14.28 +lemma sup1I1 [elim?]: "A x \<Longrightarrow> sup A B x"
   14.29    by simp
   14.30  
   14.31 -lemma join2I1 [elim?]: "A x y ==> join A B x y"
   14.32 +lemma sup2I1 [elim?]: "A x y \<Longrightarrow> sup A B x y"
   14.33    by simp
   14.34  
   14.35 -lemma join1I2 [elim?]: "B x ==> join A B x"
   14.36 +lemma join1I2 [elim?]: "B x \<Longrightarrow> sup A B x"
   14.37    by simp
   14.38  
   14.39 -lemma join2I2 [elim?]: "B x y ==> join A B x y"
   14.40 +lemma sup1I2 [elim?]: "B x y \<Longrightarrow> sup A B x y"
   14.41    by simp
   14.42  
   14.43  text {*
   14.44 @@ -231,55 +231,55 @@
   14.45    @{text B}.
   14.46  *}
   14.47  
   14.48 -lemma join1CI [intro!]: "(~ B x ==> A x) ==> join A B x"
   14.49 +lemma sup1CI [intro!]: "(~ B x ==> A x) ==> sup A B x"
   14.50    by auto
   14.51  
   14.52 -lemma join2CI [intro!]: "(~ B x y ==> A x y) ==> join A B x y"
   14.53 +lemma sup2CI [intro!]: "(~ B x y ==> A x y) ==> sup A B x y"
   14.54    by auto
   14.55  
   14.56 -lemma join1E [elim!]: "join A B x ==> (A x ==> P) ==> (B x ==> P) ==> P"
   14.57 +lemma sup1E [elim!]: "sup A B x ==> (A x ==> P) ==> (B x ==> P) ==> P"
   14.58    by simp iprover
   14.59  
   14.60 -lemma join2E [elim!]: "join A B x y ==> (A x y ==> P) ==> (B x y ==> P) ==> P"
   14.61 +lemma sup2E [elim!]: "sup A B x y ==> (A x y ==> P) ==> (B x y ==> P) ==> P"
   14.62    by simp iprover
   14.63  
   14.64  
   14.65  subsubsection {* Binary intersection *}
   14.66  
   14.67 -lemma member_Int [pred_set_conv]: "meet (member R) (member S) = member (R Int S)"
   14.68 -  by (simp add: expand_fun_eq meet_fun_eq meet_bool_eq)
   14.69 +lemma member_Int [pred_set_conv]: "inf (member R) (member S) = member (R Int S)"
   14.70 +  by (simp add: expand_fun_eq inf_fun_eq inf_bool_eq)
   14.71  
   14.72 -lemma member2_Int [pred_set_conv]: "meet (member2 R) (member2 S) = member2 (R Int S)"
   14.73 -  by (simp add: expand_fun_eq meet_fun_eq meet_bool_eq)
   14.74 +lemma member2_Int [pred_set_conv]: "inf (member2 R) (member2 S) = member2 (R Int S)"
   14.75 +  by (simp add: expand_fun_eq inf_fun_eq inf_bool_eq)
   14.76  
   14.77 -lemma meet1_iff [simp]: "(meet A B x) = (A x & B x)"
   14.78 -  by (simp add: meet_fun_eq meet_bool_eq)
   14.79 +lemma inf1_iff [simp]: "inf A B x \<longleftrightarrow> A x \<and> B x"
   14.80 +  by (simp add: inf_fun_eq inf_bool_eq)
   14.81  
   14.82 -lemma meet2_iff [simp]: "(meet A B x y) = (A x y & B x y)"
   14.83 -  by (simp add: meet_fun_eq meet_bool_eq)
   14.84 +lemma inf2_iff [simp]: "inf A B x y \<longleftrightarrow> A x y \<and> B x y"
   14.85 +  by (simp add: inf_fun_eq inf_bool_eq)
   14.86  
   14.87 -lemma meet1I [intro!]: "A x ==> B x ==> meet A B x"
   14.88 +lemma inf1I [intro!]: "A x ==> B x ==> inf A B x"
   14.89    by simp
   14.90  
   14.91 -lemma meet2I [intro!]: "A x y ==> B x y ==> meet A B x y"
   14.92 +lemma inf2I [intro!]: "A x y ==> B x y ==> inf A B x y"
   14.93    by simp
   14.94  
   14.95 -lemma meet1D1: "meet A B x ==> A x"
   14.96 +lemma inf1D1: "inf A B x ==> A x"
   14.97    by simp
   14.98  
   14.99 -lemma meet2D1: "meet A B x y ==> A x y"
  14.100 +lemma inf2D1: "inf A B x y ==> A x y"
  14.101    by simp
  14.102  
  14.103 -lemma meet1D2: "meet A B x ==> B x"
  14.104 +lemma inf1D2: "inf A B x ==> B x"
  14.105    by simp
  14.106  
  14.107 -lemma meet2D2: "meet A B x y ==> B x y"
  14.108 +lemma inf2D2: "inf A B x y ==> B x y"
  14.109    by simp
  14.110  
  14.111 -lemma meet1E [elim!]: "meet A B x ==> (A x ==> B x ==> P) ==> P"
  14.112 +lemma inf1E [elim!]: "inf A B x ==> (A x ==> B x ==> P) ==> P"
  14.113    by simp
  14.114  
  14.115 -lemma meet2E [elim!]: "meet A B x y ==> (A x y ==> B x y ==> P) ==> P"
  14.116 +lemma inf2E [elim!]: "inf A B x y ==> (A x y ==> B x y ==> P) ==> P"
  14.117    by simp
  14.118  
  14.119  
  14.120 @@ -357,12 +357,12 @@
  14.121    by (iprover intro: order_antisym conversepI pred_compI
  14.122      elim: pred_compE dest: conversepD)
  14.123  
  14.124 -lemma converse_meet: "(meet r s)^--1 = meet r^--1 s^--1"
  14.125 -  by (simp add: meet_fun_eq meet_bool_eq)
  14.126 +lemma converse_meet: "(inf r s)^--1 = inf r^--1 s^--1"
  14.127 +  by (simp add: inf_fun_eq inf_bool_eq)
  14.128      (iprover intro: conversepI ext dest: conversepD)
  14.129  
  14.130 -lemma converse_join: "(join r s)^--1 = join r^--1 s^--1"
  14.131 -  by (simp add: join_fun_eq join_bool_eq)
  14.132 +lemma converse_join: "(sup r s)^--1 = sup r^--1 s^--1"
  14.133 +  by (simp add: sup_fun_eq sup_bool_eq)
  14.134      (iprover intro: conversepI ext dest: conversepD)
  14.135  
  14.136  lemma conversep_noteq [simp]: "(op ~=)^--1 = op ~="
    15.1 --- a/src/HOL/Ring_and_Field.thy	Tue Mar 06 16:40:32 2007 +0100
    15.2 +++ b/src/HOL/Ring_and_Field.thy	Fri Mar 09 08:45:50 2007 +0100
    15.3 @@ -279,7 +279,7 @@
    15.4  instance ordered_ring_strict \<subseteq> lordered_ab_group ..
    15.5  
    15.6  instance ordered_ring_strict \<subseteq> lordered_ring
    15.7 -  by (intro_classes, simp add: abs_if join_eq_if)
    15.8 +  by intro_classes (simp add: abs_if sup_eq_if)
    15.9  
   15.10  class pordered_comm_ring = comm_ring + pordered_comm_semiring
   15.11  
    16.1 --- a/src/HOL/Tools/inductive_package.ML	Tue Mar 06 16:40:32 2007 +0100
    16.2 +++ b/src/HOL/Tools/inductive_package.ML	Fri Mar 09 08:45:50 2007 +0100
    16.3 @@ -533,7 +533,7 @@
    16.4          [rewrite_goals_tac [inductive_conj_def],
    16.5           DETERM (rtac raw_fp_induct 1),
    16.6           REPEAT (resolve_tac [le_funI, le_boolI] 1),
    16.7 -         rewrite_goals_tac (map mk_meta_eq [meet_fun_eq, meet_bool_eq] @ simp_thms'),
    16.8 +         rewrite_goals_tac (map mk_meta_eq [inf_fun_eq, inf_bool_eq] @ simp_thms'),
    16.9           (*This disjE separates out the introduction rules*)
   16.10           REPEAT (FIRSTGOAL (eresolve_tac [disjE, exE, FalseE])),
   16.11           (*Now break down the individual cases.  No disjE here in case
    17.1 --- a/src/HOL/Tools/res_atp.ML	Tue Mar 06 16:40:32 2007 +0100
    17.2 +++ b/src/HOL/Tools/res_atp.ML	Fri Mar 09 08:45:50 2007 +0100
    17.3 @@ -374,8 +374,8 @@
    17.4     "NatSimprocs.zero_less_divide_iff_number_of",
    17.5     "OrderedGroup.abs_0_eq", (*duplicate by symmetry*)
    17.6     "OrderedGroup.diff_eq_0_iff_eq", (*prolific?*)
    17.7 -   "OrderedGroup.join_0_eq_0",
    17.8 -   "OrderedGroup.meet_0_eq_0",
    17.9 +   "OrderedGroup.sup_0_eq_0",
   17.10 +   "OrderedGroup.inf_0_eq_0",
   17.11     "OrderedGroup.pprt_eq_0",   (*obscure*)
   17.12     "OrderedGroup.pprt_eq_id",   (*obscure*)
   17.13     "OrderedGroup.pprt_mono",   (*obscure*)
    18.1 --- a/src/HOL/Transitive_Closure.thy	Tue Mar 06 16:40:32 2007 +0100
    18.2 +++ b/src/HOL/Transitive_Closure.thy	Fri Mar 09 08:45:50 2007 +0100
    18.3 @@ -43,7 +43,7 @@
    18.4  
    18.5  abbreviation
    18.6    reflcl :: "('a => 'a => bool) => 'a => 'a => bool"  ("(_^==)" [1000] 1000) where
    18.7 -  "r^== == join r op ="
    18.8 +  "r^== == sup r op ="
    18.9  
   18.10  abbreviation
   18.11    reflcl_set :: "('a \<times> 'a) set => ('a \<times> 'a) set"  ("(_^=)" [1000] 999) where
   18.12 @@ -71,7 +71,7 @@
   18.13  lemma rtrancl_set_eq [pred_set_conv]: "(member2 r)^** = member2 (r^*)"
   18.14    by (simp add: rtrancl_set_def)
   18.15  
   18.16 -lemma reflcl_set_eq [pred_set_conv]: "(join (member2 r) op =) = member2 (r Un Id)"
   18.17 +lemma reflcl_set_eq [pred_set_conv]: "(sup (member2 r) op =) = member2 (r Un Id)"
   18.18    by (simp add: expand_fun_eq)
   18.19  
   18.20  lemmas rtrancl_refl [intro!, Pure.intro!, simp] = rtrancl_refl [to_set]
   18.21 @@ -190,7 +190,7 @@
   18.22  
   18.23  lemmas rtrancl_subset = rtrancl_subset' [to_set]
   18.24  
   18.25 -lemma rtrancl_Un_rtrancl': "(join (R^**) (S^**))^** = (join R S)^**"
   18.26 +lemma rtrancl_Un_rtrancl': "(sup (R^**) (S^**))^** = (sup R S)^**"
   18.27    by (blast intro!: rtrancl_subset' intro: rtrancl_mono' [THEN predicate2D])
   18.28  
   18.29  lemmas rtrancl_Un_rtrancl = rtrancl_Un_rtrancl' [to_set]
   18.30 @@ -208,7 +208,7 @@
   18.31    apply (blast intro!: r_into_rtrancl)
   18.32    done
   18.33  
   18.34 -lemma rtrancl_r_diff_Id': "(meet r op ~=)^** = r^**"
   18.35 +lemma rtrancl_r_diff_Id': "(inf r op ~=)^** = r^**"
   18.36    apply (rule sym)
   18.37    apply (rule rtrancl_subset')
   18.38    apply blast+