--- a/NEWS Tue Mar 06 16:40:32 2007 +0100
+++ b/NEWS Fri Mar 09 08:45:50 2007 +0100
@@ -505,6 +505,105 @@
*** HOL ***
+* Some steps towards more uniform lattice theory development in HOL. Obvious changes:
+
+ constants "meet" and "join" now named "inf" and "sup"
+ constant "Meet" now named "Inf"
+
+ theorem renames:
+ meet_left_le ~> inf_le1
+ meet_right_le ~> inf_le2
+ join_left_le ~> sup_ge1
+ join_right_le ~> sup_ge2
+ meet_join_le ~> inf_sup_ord
+ le_meetI ~> le_infI
+ join_leI ~> le_supI
+ le_meet ~> le_inf_iff
+ le_join ~> ge_sup_conv
+ meet_idempotent ~> inf_idem
+ join_idempotent ~> sup_idem
+ meet_comm ~> inf_commute
+ join_comm ~> sup_commute
+ meet_leI1 ~> le_infI1
+ meet_leI2 ~> le_infI2
+ le_joinI1 ~> le_supI1
+ le_joinI2 ~> le_supI2
+ meet_assoc ~> inf_assoc
+ join_assoc ~> sup_assoc
+ meet_left_comm ~> inf_left_commute
+ meet_left_idempotent ~> inf_left_idem
+ join_left_comm ~> sup_left_commute
+ join_left_idempotent ~> sup_left_idem
+ meet_aci ~> inf_aci
+ join_aci ~> sup_aci
+ le_def_meet ~> le_iff_inf
+ le_def_join ~> le_iff_sup
+ join_absorp2 ~> sup_absorb2
+ join_absorp1 ~> sup_absorb1
+ meet_absorp1 ~> inf_absorb1
+ meet_absorp2 ~> inf_absorb2
+ meet_join_absorp ~> inf_sup_absorb
+ join_meet_absorp ~> sup_inf_absorb
+ distrib_join_le ~> distrib_sup_le
+ distrib_meet_le ~> distrib_inf_le
+
+ add_meet_distrib_left ~> add_inf_distrib_left
+ add_join_distrib_left ~> add_sup_distrib_left
+ is_join_neg_meet ~> is_join_neg_inf
+ is_meet_neg_join ~> is_meet_neg_sup
+ add_meet_distrib_right ~> add_inf_distrib_right
+ add_join_distrib_right ~> add_sup_distrib_right
+ add_meet_join_distribs ~> add_sup_inf_distribs
+ join_eq_neg_meet ~> sup_eq_neg_inf
+ meet_eq_neg_join ~> inf_eq_neg_sup
+ add_eq_meet_join ~> add_eq_inf_sup
+ meet_0_imp_0 ~> inf_0_imp_0
+ join_0_imp_0 ~> sup_0_imp_0
+ meet_0_eq_0 ~> inf_0_eq_0
+ join_0_eq_0 ~> sup_0_eq_0
+ neg_meet_eq_join ~> neg_inf_eq_sup
+ neg_join_eq_meet ~> neg_sup_eq_inf
+ join_eq_if ~> sup_eq_if
+
+ mono_meet ~> mono_inf
+ mono_join ~> mono_sup
+ meet_bool_eq ~> inf_bool_eq
+ join_bool_eq ~> sup_bool_eq
+ meet_fun_eq ~> inf_fun_eq
+ join_fun_eq ~> sup_fun_eq
+ meet_set_eq ~> inf_set_eq
+ join_set_eq ~> sup_set_eq
+ meet1_iff ~> inf1_iff
+ meet2_iff ~> inf2_iff
+ meet1I ~> inf1I
+ meet2I ~> inf2I
+ meet1D1 ~> inf1D1
+ meet2D1 ~> inf2D1
+ meet1D2 ~> inf1D2
+ meet2D2 ~> inf2D2
+ meet1E ~> inf1E
+ meet2E ~> inf2E
+ join1_iff ~> sup1_iff
+ join2_iff ~> sup2_iff
+ join1I1 ~> sup1I1
+ join2I1 ~> sup2I1
+ join1I1 ~> sup1I1
+ join2I2 ~> sup1I2
+ join1CI ~> sup1CI
+ join2CI ~> sup2CI
+ join1E ~> sup1E
+ join2E ~> sup2E
+
+ is_meet_Meet ~> is_meet_Inf
+ Meet_bool_def ~> Inf_bool_def
+ Meet_fun_def ~> Inf_fun_def
+ Meet_greatest ~> Inf_greatest
+ Meet_lower ~> Inf_lower
+ Meet_set_def ~> Inf_set_def
+
+ listsp_meetI ~> listsp_infI
+ listsp_meet_eq ~> listsp_inf_eq
+
* Class (axclass + locale) "preorder" and "linear": facts "refl", "trans" and
"cases" renamed ro "order_refl", "order_trans" and "linorder_cases", to
avoid clashes with HOL "refl" and "trans". INCOMPATIBILITY.
--- a/src/HOL/FixedPoint.thy Tue Mar 06 16:40:32 2007 +0100
+++ b/src/HOL/FixedPoint.thy Fri Mar 09 08:45:50 2007 +0100
@@ -12,16 +12,17 @@
begin
subsection {* Complete lattices *}
-(*FIXME Meet \<rightarrow> Inf *)
+
consts
- Meet :: "'a::order set \<Rightarrow> 'a"
- Sup :: "'a::order set \<Rightarrow> 'a"
+ Inf :: "'a::order set \<Rightarrow> 'a"
-defs Sup_def: "Sup A == Meet {b. \<forall>a \<in> A. a <= b}"
+definition
+ Sup :: "'a::order set \<Rightarrow> 'a" where
+ "Sup A = Inf {b. \<forall>a \<in> A. a \<le> b}"
definition
SUP :: "('a \<Rightarrow> 'b::order) \<Rightarrow> 'b" (binder "SUP " 10) where
- "SUP x. f x == Sup (f ` UNIV)"
+ "(SUP x. f x) = Sup (f ` UNIV)"
(*
abbreviation
@@ -29,69 +30,69 @@
"bot == Sup {}"
*)
class comp_lat = order +
- assumes Meet_lower: "x \<in> A \<Longrightarrow> Meet A \<sqsubseteq> x"
- assumes Meet_greatest: "(\<And>x. x \<in> A \<Longrightarrow> z \<sqsubseteq> x) \<Longrightarrow> z \<sqsubseteq> Meet A"
+ assumes Inf_lower: "x \<in> A \<Longrightarrow> Inf A \<sqsubseteq> x"
+ assumes Inf_greatest: "(\<And>x. x \<in> A \<Longrightarrow> z \<sqsubseteq> x) \<Longrightarrow> z \<sqsubseteq> Inf A"
theorem Sup_upper: "(x::'a::comp_lat) \<in> A \<Longrightarrow> x <= Sup A"
- by (auto simp: Sup_def intro: Meet_greatest)
+ by (auto simp: Sup_def intro: Inf_greatest)
theorem Sup_least: "(\<And>x::'a::comp_lat. x \<in> A \<Longrightarrow> x <= z) \<Longrightarrow> Sup A <= z"
- by (auto simp: Sup_def intro: Meet_lower)
+ by (auto simp: Sup_def intro: Inf_lower)
text {* A complete lattice is a lattice *}
-lemma is_meet_Meet: "is_meet (\<lambda>(x::'a::comp_lat) y. Meet {x, y})"
- by (auto simp: is_meet_def intro: Meet_lower Meet_greatest)
+lemma is_meet_Inf: "is_meet (\<lambda>(x::'a::comp_lat) y. Inf {x, y})"
+ by (auto simp: is_meet_def intro: Inf_lower Inf_greatest)
lemma is_join_Sup: "is_join (\<lambda>(x::'a::comp_lat) y. Sup {x, y})"
by (auto simp: is_join_def intro: Sup_upper Sup_least)
instance comp_lat < lorder
proof
- from is_meet_Meet show "\<exists>m::'a\<Rightarrow>'a\<Rightarrow>'a. is_meet m" by iprover
+ from is_meet_Inf show "\<exists>m::'a\<Rightarrow>'a\<Rightarrow>'a. is_meet m" by iprover
from is_join_Sup show "\<exists>j::'a\<Rightarrow>'a\<Rightarrow>'a. is_join j" by iprover
qed
subsubsection {* Properties *}
-lemma mono_join: "mono f \<Longrightarrow> join (f A) (f B) <= f (join A B)"
+lemma mono_inf: "mono f \<Longrightarrow> f (inf A B) <= inf (f A) (f B)"
by (auto simp add: mono_def)
-lemma mono_meet: "mono f \<Longrightarrow> f (meet A B) <= meet (f A) (f B)"
+lemma mono_sup: "mono f \<Longrightarrow> sup (f A) (f B) <= f (sup A B)"
by (auto simp add: mono_def)
-lemma Sup_insert[simp]: "Sup (insert (a::'a::comp_lat) A) = join a (Sup A)"
+lemma Sup_insert[simp]: "Sup (insert (a::'a::comp_lat) A) = sup a (Sup A)"
apply(simp add:Sup_def)
apply(rule order_antisym)
- apply(rule Meet_lower)
+ apply(rule Inf_lower)
apply(clarsimp)
- apply(rule le_joinI2)
- apply(rule Meet_greatest)
+ apply(rule le_supI2)
+ apply(rule Inf_greatest)
apply blast
apply simp
apply rule
- apply(rule Meet_greatest)apply blast
-apply(rule Meet_greatest)
-apply(rule Meet_lower)
+ apply(rule Inf_greatest)apply blast
+apply(rule Inf_greatest)
+apply(rule Inf_lower)
apply blast
done
lemma bot_least[simp]: "Sup{} \<le> (x::'a::comp_lat)"
apply(simp add: Sup_def)
-apply(rule Meet_lower)
+apply(rule Inf_lower)
apply blast
done
(*
-lemma Meet_singleton[simp]: "Meet{a} = (a::'a::comp_lat)"
+lemma Inf_singleton[simp]: "Inf{a} = (a::'a::comp_lat)"
apply(rule order_antisym)
- apply(simp add: Meet_lower)
-apply(rule Meet_greatest)
+ apply(simp add: Inf_lower)
+apply(rule Inf_greatest)
apply(simp)
done
*)
lemma le_SupI: "(l::'a::comp_lat) : M \<Longrightarrow> l \<le> Sup M"
apply(simp add:Sup_def)
-apply(rule Meet_greatest)
+apply(rule Inf_greatest)
apply(simp)
done
@@ -102,7 +103,7 @@
lemma Sup_leI: "(!!x. x:M \<Longrightarrow> x \<le> u) \<Longrightarrow> Sup M \<le> (u::'a::comp_lat)"
apply(simp add:Sup_def)
-apply(rule Meet_lower)
+apply(rule Inf_lower)
apply(blast)
done
@@ -113,42 +114,43 @@
done
lemma SUP_const[simp]: "(SUP i. M) = (M::'a::comp_lat)"
-by(simp add:SUP_def image_constant_conv join_absorp1)
+by(simp add:SUP_def image_constant_conv sup_absorb1)
subsection {* Some instances of the type class of complete lattices *}
subsubsection {* Booleans *}
-defs Meet_bool_def: "Meet A == ALL x:A. x"
+defs
+ Inf_bool_def: "Inf A == ALL x:A. x"
instance bool :: comp_lat
apply intro_classes
- apply (unfold Meet_bool_def)
+ apply (unfold Inf_bool_def)
apply (iprover intro!: le_boolI elim: ballE)
apply (iprover intro!: ballI le_boolI elim: ballE le_boolE)
done
-theorem meet_bool_eq: "meet P Q = (P \<and> Q)"
+theorem inf_bool_eq: "inf P Q \<longleftrightarrow> P \<and> Q"
apply (rule order_antisym)
apply (rule le_boolI)
apply (rule conjI)
apply (rule le_boolE)
- apply (rule meet_left_le)
+ apply (rule inf_le1)
apply assumption+
apply (rule le_boolE)
- apply (rule meet_right_le)
+ apply (rule inf_le2)
apply assumption+
- apply (rule le_meetI)
+ apply (rule le_infI)
apply (rule le_boolI)
apply (erule conjunct1)
apply (rule le_boolI)
apply (erule conjunct2)
done
-theorem join_bool_eq: "join P Q = (P \<or> Q)"
+theorem sup_bool_eq: "sup P Q \<longleftrightarrow> P \<or> Q"
apply (rule order_antisym)
- apply (rule join_leI)
+ apply (rule le_supI)
apply (rule le_boolI)
apply (erule disjI1)
apply (rule le_boolI)
@@ -156,14 +158,14 @@
apply (rule le_boolI)
apply (erule disjE)
apply (rule le_boolE)
- apply (rule join_left_le)
+ apply (rule sup_ge1)
apply assumption+
apply (rule le_boolE)
- apply (rule join_right_le)
+ apply (rule sup_ge2)
apply assumption+
done
-theorem Sup_bool_eq: "Sup A = (EX x:A. x)"
+theorem Sup_bool_eq: "Sup A \<longleftrightarrow> (\<exists>x \<in> A. x)"
apply (rule order_antisym)
apply (rule Sup_least)
apply (rule le_boolI)
@@ -175,11 +177,12 @@
apply assumption+
done
+
subsubsection {* Functions *}
text {*
-Handy introduction and elimination rules for @{text "\<le>"}
-on unary and binary predicates
+ Handy introduction and elimination rules for @{text "\<le>"}
+ on unary and binary predicates
*}
lemma predicate1I [Pure.intro!, intro!]:
@@ -218,48 +221,49 @@
lemma rev_predicate2D: "P x y ==> P <= Q ==> Q x y"
by (rule predicate2D)
-defs Meet_fun_def: "Meet A == (\<lambda>x. Meet {y. EX f:A. y = f x})"
+defs
+ Inf_fun_def: "Inf A == (\<lambda>x. Inf {y. EX f:A. y = f x})"
instance "fun" :: (type, comp_lat) comp_lat
apply intro_classes
- apply (unfold Meet_fun_def)
+ apply (unfold Inf_fun_def)
apply (rule le_funI)
- apply (rule Meet_lower)
+ apply (rule Inf_lower)
apply (rule CollectI)
apply (rule bexI)
apply (rule refl)
apply assumption
apply (rule le_funI)
- apply (rule Meet_greatest)
+ apply (rule Inf_greatest)
apply (erule CollectE)
apply (erule bexE)
apply (iprover elim: le_funE)
done
-theorem meet_fun_eq: "meet f g = (\<lambda>x. meet (f x) (g x))"
+theorem inf_fun_eq: "inf f g = (\<lambda>x. inf (f x) (g x))"
apply (rule order_antisym)
apply (rule le_funI)
- apply (rule le_meetI)
- apply (rule le_funD [OF meet_left_le])
- apply (rule le_funD [OF meet_right_le])
- apply (rule le_meetI)
+ apply (rule le_infI)
+ apply (rule le_funD [OF inf_le1])
+ apply (rule le_funD [OF inf_le2])
+ apply (rule le_infI)
apply (rule le_funI)
- apply (rule meet_left_le)
+ apply (rule inf_le1)
apply (rule le_funI)
- apply (rule meet_right_le)
+ apply (rule inf_le2)
done
-theorem join_fun_eq: "join f g = (\<lambda>x. join (f x) (g x))"
+theorem sup_fun_eq: "sup f g = (\<lambda>x. sup (f x) (g x))"
apply (rule order_antisym)
- apply (rule join_leI)
+ apply (rule le_supI)
apply (rule le_funI)
- apply (rule join_left_le)
+ apply (rule sup_ge1)
apply (rule le_funI)
- apply (rule join_right_le)
+ apply (rule sup_ge2)
apply (rule le_funI)
- apply (rule join_leI)
- apply (rule le_funD [OF join_left_le])
- apply (rule le_funD [OF join_right_le])
+ apply (rule le_supI)
+ apply (rule le_funD [OF sup_ge1])
+ apply (rule le_funD [OF sup_ge2])
done
theorem Sup_fun_eq: "Sup A = (\<lambda>x. Sup {y::'a::comp_lat. EX f:A. y = f x})"
@@ -278,29 +282,30 @@
subsubsection {* Sets *}
-defs Meet_set_def: "Meet S == \<Inter>S"
+defs
+ Inf_set_def: "Inf S == \<Inter>S"
instance set :: (type) comp_lat
- by intro_classes (auto simp add: Meet_set_def)
+ by intro_classes (auto simp add: Inf_set_def)
-theorem meet_set_eq: "meet A B = A \<inter> B"
+theorem inf_set_eq: "inf A B = A \<inter> B"
apply (rule subset_antisym)
apply (rule Int_greatest)
- apply (rule meet_left_le)
- apply (rule meet_right_le)
- apply (rule le_meetI)
+ apply (rule inf_le1)
+ apply (rule inf_le2)
+ apply (rule le_infI)
apply (rule Int_lower1)
apply (rule Int_lower2)
done
-theorem join_set_eq: "join A B = A \<union> B"
+theorem sup_set_eq: "sup A B = A \<union> B"
apply (rule subset_antisym)
- apply (rule join_leI)
+ apply (rule le_supI)
apply (rule Un_upper1)
apply (rule Un_upper2)
apply (rule Un_least)
- apply (rule join_left_le)
- apply (rule join_right_le)
+ apply (rule sup_ge1)
+ apply (rule sup_ge2)
done
theorem Sup_set_eq: "Sup S = \<Union>S"
@@ -314,25 +319,25 @@
subsection {* Least and greatest fixed points *}
-constdefs
- lfp :: "(('a::comp_lat) => 'a) => 'a"
- "lfp f == Meet {u. f u <= u}" --{*least fixed point*}
+definition
+ lfp :: "('a\<Colon>comp_lat \<Rightarrow> 'a) \<Rightarrow> 'a" where
+ "lfp f = Inf {u. f u \<le> u}" --{*least fixed point*}
- gfp :: "(('a::comp_lat) => 'a) => 'a"
- "gfp f == Sup {u. u <= f u}" --{*greatest fixed point*}
+definition
+ gfp :: "('a\<Colon>comp_lat \<Rightarrow> 'a) \<Rightarrow> 'a" where
+ "gfp f = Sup {u. u \<le> f u}" --{*greatest fixed point*}
subsection{*Proof of Knaster-Tarski Theorem using @{term lfp}*}
-
text{*@{term "lfp f"} is the least upper bound of
the set @{term "{u. f(u) \<le> u}"} *}
lemma lfp_lowerbound: "f A \<le> A ==> lfp f \<le> A"
- by (auto simp add: lfp_def intro: Meet_lower)
+ by (auto simp add: lfp_def intro: Inf_lower)
lemma lfp_greatest: "(!!u. f u \<le> u ==> A \<le> u) ==> A \<le> lfp f"
- by (auto simp add: lfp_def intro: Meet_greatest)
+ by (auto simp add: lfp_def intro: Inf_greatest)
lemma lfp_lemma2: "mono f ==> f (lfp f) \<le> lfp f"
by (iprover intro: lfp_greatest order_trans monoD lfp_lowerbound)
@@ -349,16 +354,16 @@
subsection{*General induction rules for least fixed points*}
theorem lfp_induct:
- assumes mono: "mono f" and ind: "f (meet (lfp f) P) <= P"
+ assumes mono: "mono f" and ind: "f (inf (lfp f) P) <= P"
shows "lfp f <= P"
proof -
- have "meet (lfp f) P <= lfp f" by (rule meet_left_le)
- with mono have "f (meet (lfp f) P) <= f (lfp f)" ..
+ have "inf (lfp f) P <= lfp f" by (rule inf_le1)
+ with mono have "f (inf (lfp f) P) <= f (lfp f)" ..
also from mono have "f (lfp f) = lfp f" by (rule lfp_unfold [symmetric])
- finally have "f (meet (lfp f) P) <= lfp f" .
- from this and ind have "f (meet (lfp f) P) <= meet (lfp f) P" by (rule le_meetI)
- hence "lfp f <= meet (lfp f) P" by (rule lfp_lowerbound)
- also have "meet (lfp f) P <= P" by (rule meet_right_le)
+ finally have "f (inf (lfp f) P) <= lfp f" .
+ from this and ind have "f (inf (lfp f) P) <= inf (lfp f) P" by (rule le_infI)
+ hence "lfp f <= inf (lfp f) P" by (rule lfp_lowerbound)
+ also have "inf (lfp f) P <= P" by (rule inf_le2)
finally show ?thesis .
qed
@@ -368,7 +373,7 @@
and indhyp: "!!x. [| x: f(lfp(f) Int {x. P(x)}) |] ==> P(x)"
shows "P(a)"
by (rule lfp_induct [THEN subsetD, THEN CollectD, OF mono _ lfp])
- (auto simp: meet_set_eq intro: indhyp)
+ (auto simp: inf_set_eq intro: indhyp)
text{*Version of induction for binary relations*}
@@ -399,7 +404,7 @@
lemma def_lfp_induct:
"[| A == lfp(f); mono(f);
- f (meet A P) \<le> P
+ f (inf A P) \<le> P
|] ==> A \<le> P"
by (blast intro: lfp_induct)
@@ -447,25 +452,25 @@
done
lemma coinduct_lemma:
- "[| X \<le> f (join X (gfp f)); mono f |] ==> join X (gfp f) \<le> f (join X (gfp f))"
+ "[| X \<le> f (sup X (gfp f)); mono f |] ==> sup X (gfp f) \<le> f (sup X (gfp f))"
apply (frule gfp_lemma2)
- apply (drule mono_join)
- apply (rule join_leI)
+ apply (drule mono_sup)
+ apply (rule le_supI)
apply assumption
apply (rule order_trans)
apply (rule order_trans)
apply assumption
- apply (rule join_right_le)
+ apply (rule sup_ge2)
apply assumption
done
text{*strong version, thanks to Coen and Frost*}
lemma coinduct_set: "[| mono(f); a: X; X \<subseteq> f(X Un gfp(f)) |] ==> a : gfp(f)"
-by (blast intro: weak_coinduct [OF _ coinduct_lemma, simplified join_set_eq])
+by (blast intro: weak_coinduct [OF _ coinduct_lemma, simplified sup_set_eq])
-lemma coinduct: "[| mono(f); X \<le> f (join X (gfp f)) |] ==> X \<le> gfp(f)"
+lemma coinduct: "[| mono(f); X \<le> f (sup X (gfp f)) |] ==> X \<le> gfp(f)"
apply (rule order_trans)
- apply (rule join_left_le)
+ apply (rule sup_ge1)
apply (erule gfp_upperbound [OF coinduct_lemma])
apply assumption
done
@@ -507,7 +512,7 @@
by (auto intro!: gfp_unfold)
lemma def_coinduct:
- "[| A==gfp(f); mono(f); X \<le> f(join X A) |] ==> X \<le> A"
+ "[| A==gfp(f); mono(f); X \<le> f(sup X A) |] ==> X \<le> A"
by (iprover intro!: coinduct)
lemma def_coinduct_set:
@@ -562,8 +567,8 @@
val le_funI = thm "le_funI";
val le_boolI = thm "le_boolI";
val le_boolI' = thm "le_boolI'";
-val meet_fun_eq = thm "meet_fun_eq";
-val meet_bool_eq = thm "meet_bool_eq";
+val inf_fun_eq = thm "inf_fun_eq";
+val inf_bool_eq = thm "inf_bool_eq";
val le_funE = thm "le_funE";
val le_funD = thm "le_funD";
val le_boolE = thm "le_boolE";
--- a/src/HOL/Hyperreal/StarClasses.thy Tue Mar 06 16:40:32 2007 +0100
+++ b/src/HOL/Hyperreal/StarClasses.thy Fri Mar 09 08:45:50 2007 +0100
@@ -249,7 +249,7 @@
text {*
Some extra trouble is necessary because the class axioms
- for @{term meet} and @{term join} use quantification over
+ for @{term inf} and @{term sup} use quantification over
function spaces.
*}
@@ -279,28 +279,28 @@
instance star :: (lorder) lorder ..
-lemma star_meet_def [transfer_unfold]: "meet = *f2* meet"
+lemma star_inf_def [transfer_unfold]: "inf = *f2* inf"
apply (rule is_meet_unique [OF is_meet_meet])
apply (transfer is_meet_def, rule is_meet_meet)
done
-lemma star_join_def [transfer_unfold]: "join = *f2* join"
+lemma star_sup_def [transfer_unfold]: "sup = *f2* sup"
apply (rule is_join_unique [OF is_join_join])
apply (transfer is_join_def, rule is_join_join)
done
-lemma Standard_meet [simp]:
- "\<lbrakk>x \<in> Standard; y \<in> Standard\<rbrakk> \<Longrightarrow> meet x y \<in> Standard"
-by (simp add: star_meet_def)
+lemma Standard_inf [simp]:
+ "\<lbrakk>x \<in> Standard; y \<in> Standard\<rbrakk> \<Longrightarrow> inf x y \<in> Standard"
+by (simp add: star_inf_def)
-lemma Standard_join [simp]:
- "\<lbrakk>x \<in> Standard; y \<in> Standard\<rbrakk> \<Longrightarrow> join x y \<in> Standard"
-by (simp add: star_join_def)
+lemma Standard_sup [simp]:
+ "\<lbrakk>x \<in> Standard; y \<in> Standard\<rbrakk> \<Longrightarrow> sup x y \<in> Standard"
+by (simp add: star_sup_def)
-lemma star_of_meet [simp]: "star_of (meet x y) = meet (star_of x) (star_of y)"
+lemma star_of_inf [simp]: "star_of (inf x y) = inf (star_of x) (star_of y)"
by transfer (rule refl)
-lemma star_of_join [simp]: "star_of (join x y) = join (star_of x) (star_of y)"
+lemma star_of_sup [simp]: "star_of (sup x y) = sup (star_of x) (star_of y)"
by transfer (rule refl)
subsection {* Ordered group classes *}
--- a/src/HOL/LOrder.thy Tue Mar 06 16:40:32 2007 +0100
+++ b/src/HOL/LOrder.thy Fri Mar 09 08:45:50 2007 +0100
@@ -3,9 +3,9 @@
Author: Steven Obua, TU Muenchen
FIXME integrate properly with lattice locales
-- make it a class?
-- get rid of the implicit there-is-a-meet/join but require eplicit ops.
-Also rename meet/join to inf/sup.
+- get rid of the implicit there-is-a-meet/join but require explicit ops.
+- abandone semilorder axclasses, instead turn lattice locales into classes
+- rename meet/join to inf/sup in all theorems
*)
header "Lattice Orders"
@@ -61,143 +61,134 @@
show "u = v" by ((rule ext)+, simp_all add: order_antisym prems f_le)
qed
-axclass join_semilorder < order
- join_exists: "? j. is_join j"
+lemma is_meet_inf: "is_meet (inf \<Colon> 'a\<Colon>lower_semilattice \<Rightarrow> 'a \<Rightarrow> 'a)"
+unfolding is_meet_def by auto
+
+lemma is_join_sup: "is_join (sup \<Colon> 'a\<Colon>upper_semilattice \<Rightarrow> 'a \<Rightarrow> 'a)"
+unfolding is_join_def by auto
axclass meet_semilorder < order
meet_exists: "? m. is_meet m"
-axclass lorder < join_semilorder, meet_semilorder
+axclass join_semilorder < order
+ join_exists: "? j. is_join j"
+
+axclass lorder < meet_semilorder, join_semilorder
-constdefs
- meet :: "('a::meet_semilorder) \<Rightarrow> 'a \<Rightarrow> 'a"
- "meet == THE m. is_meet m"
- join :: "('a::join_semilorder) \<Rightarrow> 'a \<Rightarrow> 'a"
- "join == THE j. is_join j"
+definition
+ inf :: "('a::meet_semilorder) \<Rightarrow> 'a \<Rightarrow> 'a" where
+ "inf = (THE m. is_meet m)"
-lemma is_meet_meet: "is_meet (meet::'a \<Rightarrow> 'a \<Rightarrow> ('a::meet_semilorder))"
+definition
+ sup :: "('a::join_semilorder) \<Rightarrow> 'a \<Rightarrow> 'a" where
+ "sup = (THE j. is_join j)"
+
+lemma is_meet_meet: "is_meet (inf::'a \<Rightarrow> 'a \<Rightarrow> ('a::meet_semilorder))"
proof -
from meet_exists obtain k::"'a \<Rightarrow> 'a \<Rightarrow> 'a" where "is_meet k" ..
with is_meet_unique[of _ k] show ?thesis
- by (simp add: meet_def theI[of is_meet])
+ by (simp add: inf_def theI [of is_meet])
qed
-lemma meet_unique: "(is_meet m) = (m = meet)"
-by (insert is_meet_meet, auto simp add: is_meet_unique)
-
-lemma is_join_join: "is_join (join::'a \<Rightarrow> 'a \<Rightarrow> ('a::join_semilorder))"
+lemma is_join_join: "is_join (sup::'a \<Rightarrow> 'a \<Rightarrow> ('a::join_semilorder))"
proof -
from join_exists obtain k::"'a \<Rightarrow> 'a \<Rightarrow> 'a" where "is_join k" ..
with is_join_unique[of _ k] show ?thesis
- by (simp add: join_def theI[of is_join])
+ by (simp add: sup_def theI[of is_join])
qed
-lemma join_unique: "(is_join j) = (j = join)"
+lemma meet_unique: "(is_meet m) = (m = inf)"
+by (insert is_meet_meet, auto simp add: is_meet_unique)
+
+lemma join_unique: "(is_join j) = (j = sup)"
by (insert is_join_join, auto simp add: is_join_unique)
-interpretation meet_semilat:
- lower_semilattice ["op \<le> \<Colon> 'a\<Colon>meet_semilorder \<Rightarrow> 'a \<Rightarrow> bool" "op <" meet]
+lemma inf_unique: "(is_meet m) = (m = (Lattices.inf \<Colon> 'a \<Rightarrow> 'a \<Rightarrow> 'a\<Colon>lower_semilattice))"
+by (insert is_meet_inf, auto simp add: is_meet_unique)
+
+lemma sup_unique: "(is_join j) = (j = (Lattices.sup \<Colon> 'a \<Rightarrow> 'a \<Rightarrow> 'a\<Colon>upper_semilattice))"
+by (insert is_join_sup, auto simp add: is_join_unique)
+
+interpretation inf_semilat:
+ lower_semilattice ["op \<le> \<Colon> 'a\<Colon>meet_semilorder \<Rightarrow> 'a \<Rightarrow> bool" "op <" inf]
proof unfold_locales
fix x y z :: "'a\<Colon>meet_semilorder"
- from is_meet_meet have "is_meet meet" by blast
+ from is_meet_meet have "is_meet inf" by blast
note meet = this is_meet_def
- from meet show "meet x y \<le> x" by blast
- from meet show "meet x y \<le> y" by blast
- from meet show "x \<le> y \<Longrightarrow> x \<le> z \<Longrightarrow> x \<le> meet y z" by blast
+ from meet show "inf x y \<le> x" by blast
+ from meet show "inf x y \<le> y" by blast
+ from meet show "x \<le> y \<Longrightarrow> x \<le> z \<Longrightarrow> x \<le> inf y z" by blast
qed
-interpretation join_semilat:
- upper_semilattice ["op \<le> \<Colon> 'a\<Colon>join_semilorder \<Rightarrow> 'a \<Rightarrow> bool" "op <" join]
+interpretation sup_semilat:
+ upper_semilattice ["op \<le> \<Colon> 'a\<Colon>join_semilorder \<Rightarrow> 'a \<Rightarrow> bool" "op <" sup]
proof unfold_locales
fix x y z :: "'a\<Colon>join_semilorder"
- from is_join_join have "is_join join" by blast
+ from is_join_join have "is_join sup" by blast
note join = this is_join_def
- from join show "x \<le> join x y" by blast
- from join show "y \<le> join x y" by blast
- from join show "x \<le> z \<Longrightarrow> y \<le> z \<Longrightarrow> join x y \<le> z" by blast
+ from join show "x \<le> sup x y" by blast
+ from join show "y \<le> sup x y" by blast
+ from join show "x \<le> z \<Longrightarrow> y \<le> z \<Longrightarrow> sup x y \<le> z" by blast
qed
-declare
- join_semilat.antisym_intro[rule del] meet_semilat.antisym_intro[rule del]
- join_semilat.le_supE[rule del] meet_semilat.le_infE[rule del]
-
-interpretation meet_join_lat:
- lattice ["op \<le> \<Colon> 'a\<Colon>lorder \<Rightarrow> 'a \<Rightarrow> bool" "op <" meet join]
-by unfold_locales
-
-lemmas meet_left_le = meet_semilat.inf_le1
-lemmas meet_right_le = meet_semilat.inf_le2
-lemmas le_meetI[rule del] = meet_semilat.le_infI
-(* intro! breaks a proof in Hyperreal/SEQ and NumberTheory/IntPrimes *)
-lemmas join_left_le = join_semilat.sup_ge1
-lemmas join_right_le = join_semilat.sup_ge2
-lemmas join_leI[rule del] = join_semilat.le_supI
-
-lemmas meet_join_le = meet_left_le meet_right_le join_left_le join_right_le
-
-lemmas le_meet = meet_semilat.le_inf_iff
-
-lemmas le_join = join_semilat.ge_sup_conv
+interpretation inf_sup_lat:
+ lattice ["op \<le> \<Colon> 'a\<Colon>lorder \<Rightarrow> 'a \<Rightarrow> bool" "op <" inf sup]
+ by unfold_locales
lemma is_meet_min: "is_meet (min::'a \<Rightarrow> 'a \<Rightarrow> ('a::linorder))"
-by (auto simp add: is_meet_def min_def)
+ by (auto simp add: is_meet_def min_def)
+ lemma is_join_max: "is_join (max::'a \<Rightarrow> 'a \<Rightarrow> ('a::linorder))"
+ by (auto simp add: is_join_def max_def)
-lemma is_join_max: "is_join (max::'a \<Rightarrow> 'a \<Rightarrow> ('a::linorder))"
-by (auto simp add: is_join_def max_def)
-
-instance linorder \<subseteq> meet_semilorder
+instance linorder \<subseteq> lorder
proof
from is_meet_min show "? (m::'a\<Rightarrow>'a\<Rightarrow>('a::linorder)). is_meet m" by auto
-qed
-
-instance linorder \<subseteq> join_semilorder
-proof
from is_join_max show "? (j::'a\<Rightarrow>'a\<Rightarrow>('a::linorder)). is_join j" by auto
qed
-
-instance linorder \<subseteq> lorder ..
-lemma meet_min: "meet = (min :: 'a\<Rightarrow>'a\<Rightarrow>('a::linorder))"
-by (simp add: is_meet_meet is_meet_min is_meet_unique)
+lemma meet_min: "inf = (min \<Colon> 'a\<Colon>{linorder} \<Rightarrow> 'a \<Rightarrow> 'a)"
+ by (simp add: is_meet_meet is_meet_min is_meet_unique)
+lemma join_max: "sup = (max \<Colon> 'a\<Colon>{linorder} \<Rightarrow> 'a \<Rightarrow> 'a)"
+ by (simp add: is_join_join is_join_max is_join_unique)
-lemma join_max: "join = (max :: 'a\<Rightarrow>'a\<Rightarrow>('a::linorder))"
-by (simp add: is_join_join is_join_max is_join_unique)
+lemmas [rule del] = sup_semilat.antisym_intro inf_semilat.antisym_intro
+ sup_semilat.le_supE inf_semilat.le_infE
-lemmas meet_idempotent = meet_semilat.inf_idem
-lemmas join_idempotent = join_semilat.sup_idem
-lemmas meet_comm = meet_semilat.inf_commute
-lemmas join_comm = join_semilat.sup_commute
-lemmas meet_leI1[rule del] = meet_semilat.le_infI1
-lemmas meet_leI2[rule del] = meet_semilat.le_infI2
-lemmas le_joinI1[rule del] = join_semilat.le_supI1
-lemmas le_joinI2[rule del] = join_semilat.le_supI2
-lemmas meet_assoc = meet_semilat.inf_assoc
-lemmas join_assoc = join_semilat.sup_assoc
-lemmas meet_left_comm = meet_semilat.inf_left_commute
-lemmas meet_left_idempotent = meet_semilat.inf_left_idem
-lemmas join_left_comm = join_semilat.sup_left_commute
-lemmas join_left_idempotent= join_semilat.sup_left_idem
-
-lemmas meet_aci = meet_assoc meet_comm meet_left_comm meet_left_idempotent
-lemmas join_aci = join_assoc join_comm join_left_comm join_left_idempotent
-
-lemmas le_def_meet = meet_semilat.le_iff_inf
-lemmas le_def_join = join_semilat.le_iff_sup
-
-lemmas join_absorp2 = join_semilat.sup_absorb2
-lemmas join_absorp1 = join_semilat.sup_absorb1
-
-lemmas meet_absorp1 = meet_semilat.inf_absorb1
-lemmas meet_absorp2 = meet_semilat.inf_absorb2
-
-interpretation meet_join_lat:
- lattice ["op \<le> \<Colon> 'a\<Colon>{meet_semilorder,join_semilorder} \<Rightarrow> 'a \<Rightarrow> bool" "op <" meet join]
-by unfold_locales
-
-lemmas meet_join_absorp = meet_join_lat.inf_sup_absorb
-lemmas join_meet_absorp = meet_join_lat.sup_inf_absorb
-
-lemmas distrib_join_le = meet_join_lat.distrib_sup_le
-lemmas distrib_meet_le = meet_join_lat.distrib_inf_le
+lemmas inf_le1 = inf_semilat.inf_le1
+lemmas inf_le2 = inf_semilat.inf_le2
+lemmas le_infI [rule del] = inf_semilat.le_infI
+ (*intro! breaks a proof in Hyperreal/SEQ and NumberTheory/IntPrimes*)
+lemmas sup_ge1 = sup_semilat.sup_ge1
+lemmas sup_ge2 = sup_semilat.sup_ge2
+lemmas le_supI [rule del] = sup_semilat.le_supI
+lemmas inf_sup_ord = inf_le1 inf_le2 sup_ge1 sup_ge2
+lemmas le_inf_iff = inf_semilat.le_inf_iff
+lemmas ge_sup_conv = sup_semilat.ge_sup_conv
+lemmas inf_idem = inf_semilat.inf_idem
+lemmas sup_idem = sup_semilat.sup_idem
+lemmas inf_commute = inf_semilat.inf_commute
+lemmas sup_commute = sup_semilat.sup_commute
+lemmas le_infI1 [rule del] = inf_semilat.le_infI1
+lemmas le_infI2 [rule del] = inf_semilat.le_infI2
+lemmas le_supI1 [rule del] = sup_semilat.le_supI1
+lemmas le_supI2 [rule del] = sup_semilat.le_supI2
+lemmas inf_assoc = inf_semilat.inf_assoc
+lemmas sup_assoc = sup_semilat.sup_assoc
+lemmas inf_left_commute = inf_semilat.inf_left_commute
+lemmas inf_left_idem = inf_semilat.inf_left_idem
+lemmas sup_left_commute = sup_semilat.sup_left_commute
+lemmas sup_left_idem= sup_semilat.sup_left_idem
+lemmas inf_aci = inf_assoc inf_commute inf_left_commute inf_left_idem
+lemmas sup_aci = sup_assoc sup_commute sup_left_commute sup_left_idem
+lemmas le_iff_inf = inf_semilat.le_iff_inf
+lemmas le_iff_sup = sup_semilat.le_iff_sup
+lemmas sup_absorb2 = sup_semilat.sup_absorb2
+lemmas sup_absorb1 = sup_semilat.sup_absorb1
+lemmas inf_absorb1 = inf_semilat.inf_absorb1
+lemmas inf_absorb2 = inf_semilat.inf_absorb2
+lemmas inf_sup_absorb = inf_sup_lat.inf_sup_absorb
+lemmas sup_inf_absorb = inf_sup_lat.sup_inf_absorb
+lemmas distrib_sup_le = inf_sup_lat.distrib_sup_le
+lemmas distrib_inf_le = inf_sup_lat.distrib_inf_le
end
--- a/src/HOL/Lambda/Commutation.thy Tue Mar 06 16:40:32 2007 +0100
+++ b/src/HOL/Lambda/Commutation.thy Fri Mar 09 08:45:50 2007 +0100
@@ -26,7 +26,7 @@
definition
Church_Rosser :: "('a => 'a => bool) => bool" where
"Church_Rosser R =
- (\<forall>x y. (join R (R^--1))^** x y --> (\<exists>z. R^** x z \<and> R^** y z))"
+ (\<forall>x y. (sup R (R^--1))^** x y --> (\<exists>z. R^** x z \<and> R^** y z))"
abbreviation
confluent :: "('a => 'a => bool) => bool" where
@@ -83,7 +83,7 @@
done
lemma commute_Un:
- "[| commute R T; commute S T |] ==> commute (join R S) T"
+ "[| commute R T; commute S T |] ==> commute (sup R S) T"
apply (unfold commute_def square_def)
apply blast
done
@@ -92,7 +92,7 @@
subsubsection {* diamond, confluence, and union *}
lemma diamond_Un:
- "[| diamond R; diamond S; commute R S |] ==> diamond (join R S)"
+ "[| diamond R; diamond S; commute R S |] ==> diamond (sup R S)"
apply (unfold diamond_def)
apply (assumption | rule commute_Un commute_sym)+
done
@@ -109,7 +109,7 @@
done
lemma confluent_Un:
- "[| confluent R; confluent S; commute (R^**) (S^**) |] ==> confluent (join R S)"
+ "[| confluent R; confluent S; commute (R^**) (S^**) |] ==> confluent (sup R S)"
apply (rule rtrancl_Un_rtrancl' [THEN subst])
apply (blast dest: diamond_Un intro: diamond_confluent)
done
@@ -128,9 +128,9 @@
apply (tactic {* safe_tac HOL_cs *})
apply (tactic {*
blast_tac (HOL_cs addIs
- [thm "join_right_le" RS thm "rtrancl_mono'" RS thm "predicate2D" RS thm "rtrancl_trans'",
+ [thm "sup_ge2" RS thm "rtrancl_mono'" RS thm "predicate2D" RS thm "rtrancl_trans'",
thm "rtrancl_converseI'", thm "conversepI",
- thm "join_left_le" RS thm "rtrancl_mono'" RS thm "predicate2D"]) 1 *})
+ thm "sup_ge1" RS thm "rtrancl_mono'" RS thm "predicate2D"]) 1 *})
apply (erule rtrancl_induct')
apply blast
apply (blast del: rtrancl.rtrancl_refl intro: rtrancl_trans')
--- a/src/HOL/Lambda/Eta.thy Tue Mar 06 16:40:32 2007 +0100
+++ b/src/HOL/Lambda/Eta.thy Fri Mar 09 08:45:50 2007 +0100
@@ -163,7 +163,7 @@
iff del: dB.distinct simp: dB.distinct) (*23 seconds?*)
done
-lemma confluent_beta_eta: "confluent (join beta eta)"
+lemma confluent_beta_eta: "confluent (sup beta eta)"
apply (assumption |
rule square_rtrancl_reflcl_commute confluent_Un
beta_confluent eta_confluent square_beta_eta)+
@@ -366,7 +366,7 @@
qed
theorem eta_postponement:
- assumes st: "(join beta eta)\<^sup>*\<^sup>* s t"
+ assumes st: "(sup beta eta)\<^sup>*\<^sup>* s t"
shows "(eta\<^sup>*\<^sup>* OO beta\<^sup>*\<^sup>*) s t" using st
proof induct
case 1
--- a/src/HOL/Lattices.thy Tue Mar 06 16:40:32 2007 +0100
+++ b/src/HOL/Lattices.thy Fri Mar 09 08:45:50 2007 +0100
@@ -16,42 +16,47 @@
Finite_Set}. In the longer term it may be better to define arbitrary
sups and infs via @{text THE}. *}
-locale lower_semilattice = order +
+class lower_semilattice = order +
fixes inf :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<sqinter>" 70)
- assumes inf_le1[simp]: "x \<sqinter> y \<sqsubseteq> x" and inf_le2[simp]: "x \<sqinter> y \<sqsubseteq> y"
+ assumes inf_le1 [simp]: "x \<sqinter> y \<sqsubseteq> x" and inf_le2 [simp]: "x \<sqinter> y \<sqsubseteq> y"
and inf_greatest: "x \<sqsubseteq> y \<Longrightarrow> x \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> y \<sqinter> z"
-locale upper_semilattice = order +
+class upper_semilattice = order +
fixes sup :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<squnion>" 65)
- assumes sup_ge1[simp]: "x \<sqsubseteq> x \<squnion> y" and sup_ge2[simp]: "y \<sqsubseteq> x \<squnion> y"
+ assumes sup_ge1 [simp]: "x \<sqsubseteq> x \<squnion> y" and sup_ge2 [simp]: "y \<sqsubseteq> x \<squnion> y"
and sup_least: "y \<sqsubseteq> x \<Longrightarrow> z \<sqsubseteq> x \<Longrightarrow> y \<squnion> z \<sqsubseteq> x"
-locale lattice = lower_semilattice + upper_semilattice
+class lattice = lower_semilattice + upper_semilattice
subsubsection{* Intro and elim rules*}
context lower_semilattice
begin
-lemmas antisym_intro[intro!] = antisym
+lemmas antisym_intro [intro!] = antisym
+lemmas (in -) [rule del] = antisym_intro
lemma le_infI1[intro]: "a \<sqsubseteq> x \<Longrightarrow> a \<sqinter> b \<sqsubseteq> x"
apply(subgoal_tac "a \<sqinter> b \<sqsubseteq> a")
apply(blast intro: order_trans)
apply simp
done
+lemmas (in -) [rule del] = le_infI1
lemma le_infI2[intro]: "b \<sqsubseteq> x \<Longrightarrow> a \<sqinter> b \<sqsubseteq> x"
apply(subgoal_tac "a \<sqinter> b \<sqsubseteq> b")
apply(blast intro: order_trans)
apply simp
done
+lemmas (in -) [rule del] = le_infI2
lemma le_infI[intro!]: "x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> b \<Longrightarrow> x \<sqsubseteq> a \<sqinter> b"
by(blast intro: inf_greatest)
+lemmas (in -) [rule del] = le_infI
-lemma le_infE[elim!]: "x \<sqsubseteq> a \<sqinter> b \<Longrightarrow> (x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> b \<Longrightarrow> P) \<Longrightarrow> P"
-by(blast intro: order_trans)
+lemma le_infE [elim!]: "x \<sqsubseteq> a \<sqinter> b \<Longrightarrow> (x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> b \<Longrightarrow> P) \<Longrightarrow> P"
+ by (blast intro: order_trans)
+lemmas (in -) [rule del] = le_infE
lemma le_inf_iff [simp]:
"x \<sqsubseteq> y \<sqinter> z = (x \<sqsubseteq> y \<and> x \<sqsubseteq> z)"
@@ -66,25 +71,31 @@
context upper_semilattice
begin
-lemmas antisym_intro[intro!] = antisym
+lemmas antisym_intro [intro!] = antisym
+lemmas (in -) [rule del] = antisym_intro
lemma le_supI1[intro]: "x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> a \<squnion> b"
apply(subgoal_tac "a \<sqsubseteq> a \<squnion> b")
apply(blast intro: order_trans)
apply simp
done
+lemmas (in -) [rule del] = le_supI1
lemma le_supI2[intro]: "x \<sqsubseteq> b \<Longrightarrow> x \<sqsubseteq> a \<squnion> b"
apply(subgoal_tac "b \<sqsubseteq> a \<squnion> b")
apply(blast intro: order_trans)
apply simp
done
+lemmas (in -) [rule del] = le_supI2
lemma le_supI[intro!]: "a \<sqsubseteq> x \<Longrightarrow> b \<sqsubseteq> x \<Longrightarrow> a \<squnion> b \<sqsubseteq> x"
by(blast intro: sup_least)
+lemmas (in -) [rule del] = le_supI
lemma le_supE[elim!]: "a \<squnion> b \<sqsubseteq> x \<Longrightarrow> (a \<sqsubseteq> x \<Longrightarrow> b \<sqsubseteq> x \<Longrightarrow> P) \<Longrightarrow> P"
-by(blast intro: order_trans)
+ by (blast intro: order_trans)
+lemmas (in -) [rule del] = le_supE
+
lemma ge_sup_conv[simp]:
"x \<squnion> y \<sqsubseteq> z = (x \<sqsubseteq> z \<and> y \<sqsubseteq> z)"
@@ -247,25 +258,24 @@
apply (simp add: max_def linorder_not_le order_less_imp_le)
unfolding min_def max_def by auto
-text{* Now we have inherited antisymmetry as an intro-rule on all
-linear orders. This is a problem because it applies to bool, which is
-undesirable. *}
+text {*
+ Now we have inherited antisymmetry as an intro-rule on all
+ linear orders. This is a problem because it applies to bool, which is
+ undesirable.
+*}
-declare
- min_max.antisym_intro[rule del]
- min_max.le_infI[rule del] min_max.le_supI[rule del]
- min_max.le_supE[rule del] min_max.le_infE[rule del]
- min_max.le_supI1[rule del] min_max.le_supI2[rule del]
- min_max.le_infI1[rule del] min_max.le_infI2[rule del]
+lemmas [rule del] = min_max.antisym_intro min_max.le_infI min_max.le_supI
+ min_max.le_supE min_max.le_infE min_max.le_supI1 min_max.le_supI2
+ min_max.le_infI1 min_max.le_infI2
lemmas le_maxI1 = min_max.sup_ge1
lemmas le_maxI2 = min_max.sup_ge2
lemmas max_ac = min_max.sup_assoc min_max.sup_commute
- mk_left_commute[of max,OF min_max.sup_assoc min_max.sup_commute]
+ mk_left_commute [of max, OF min_max.sup_assoc min_max.sup_commute]
lemmas min_ac = min_max.inf_assoc min_max.inf_commute
- mk_left_commute[of min,OF min_max.inf_assoc min_max.inf_commute]
+ mk_left_commute [of min, OF min_max.inf_assoc min_max.inf_commute]
text {* ML legacy bindings *}
--- a/src/HOL/Library/Continuity.thy Tue Mar 06 16:40:32 2007 +0100
+++ b/src/HOL/Library/Continuity.thy Fri Mar 09 08:45:50 2007 +0100
@@ -24,12 +24,12 @@
"bot \<equiv> Sup {}"
lemma SUP_nat_conv:
- "(SUP n::nat. M n::'a::comp_lat) = join (M 0) (SUP n. M(Suc n))"
+ "(SUP n::nat. M n::'a::comp_lat) = sup (M 0) (SUP n. M(Suc n))"
apply(rule order_antisym)
apply(rule SUP_leI)
apply(case_tac n)
apply simp
- apply (blast intro:le_SUPI le_joinI2)
+ apply (blast intro:le_SUPI le_supI2)
apply(simp)
apply (blast intro:SUP_leI le_SUPI)
done
@@ -40,16 +40,16 @@
fix A B :: "'a" assume "A <= B"
let ?C = "%i::nat. if i=0 then A else B"
have "chain ?C" using `A <= B` by(simp add:chain_def)
- have "F B = join (F A) (F B)"
+ have "F B = sup (F A) (F B)"
proof -
- have "join A B = B" using `A <= B` by (simp add:join_absorp2)
+ have "sup A B = B" using `A <= B` by (simp add:sup_absorb2)
hence "F B = F(SUP i. ?C i)" by(simp add: SUP_nat_conv)
also have "\<dots> = (SUP i. F(?C i))"
using `chain ?C` `continuous F` by(simp add:continuous_def)
- also have "\<dots> = join (F A) (F B)" by(simp add: SUP_nat_conv)
+ also have "\<dots> = sup (F A) (F B)" by(simp add: SUP_nat_conv)
finally show ?thesis .
qed
- thus "F A \<le> F B" by(subst le_def_join, simp)
+ thus "F A \<le> F B" by(subst le_iff_sup, simp)
qed
lemma continuous_lfp:
--- a/src/HOL/Library/Graphs.thy Tue Mar 06 16:40:32 2007 +0100
+++ b/src/HOL/Library/Graphs.thy Fri Mar 09 08:45:50 2007 +0100
@@ -155,10 +155,10 @@
defs (overloaded)
- Meet_graph_def: "Meet == \<lambda>Gs. Graph (\<Inter>(dest_graph ` Gs))"
+ Inf_graph_def: "Inf == \<lambda>Gs. Graph (\<Inter>(dest_graph ` Gs))"
instance graph :: (type, type) comp_lat
- by default (auto simp:Meet_graph_def is_join_def graph_leq_def le_fun_def le_bool_def in_grplus has_edge_def)
+ by default (auto simp: Inf_graph_def is_join_def graph_leq_def le_fun_def le_bool_def in_grplus has_edge_def)
lemma plus_graph_is_join: "is_join ((op +)::('a::type, 'b::monoid_mult) graph \<Rightarrow> ('a,'b) graph \<Rightarrow> ('a,'b) graph)"
unfolding is_join_def
@@ -172,7 +172,7 @@
lemma plus_is_join:
"(op +) =
- (join :: ('a::type, 'b::monoid_mult) graph \<Rightarrow> ('a,'b) graph \<Rightarrow> ('a,'b) graph)"
+ (sup :: ('a::type, 'b::monoid_mult) graph \<Rightarrow> ('a,'b) graph \<Rightarrow> ('a,'b) graph)"
using plus_graph_is_join by (simp add:join_unique)
instance graph :: (type, monoid_mult) semiring_1
@@ -693,7 +693,7 @@
proof (rule prod_eqI)
show "fst ?\<omega> = fst loop"
by (auto simp:path_loop_def path_nth_def split_def k)
-
+
show "snd ?\<omega> = snd loop"
proof (rule nth_equalityI[rule_format])
show leneq: "length (snd ?\<omega>) = length (snd loop)"
@@ -716,11 +716,5 @@
by (simp add:path_nth_def)
qed
qed
-
-
-
-
-
-
end
\ No newline at end of file
--- a/src/HOL/List.thy Tue Mar 06 16:40:32 2007 +0100
+++ b/src/HOL/List.thy Fri Mar 09 08:45:50 2007 +0100
@@ -2228,21 +2228,21 @@
lemmas lists_mono [mono] = listsp_mono [to_set]
-lemma listsp_meetI:
- assumes l: "listsp A l" shows "listsp B l ==> listsp (meet A B) l" using l
+lemma listsp_infI:
+ assumes l: "listsp A l" shows "listsp B l ==> listsp (inf A B) l" using l
by induct blast+
-lemmas lists_IntI = listsp_meetI [to_set]
-
-lemma listsp_meet_eq [simp]: "listsp (meet A B) = meet (listsp A) (listsp B)"
-proof (rule mono_meet [where f=listsp, THEN order_antisym])
+lemmas lists_IntI = listsp_infI [to_set]
+
+lemma listsp_inf_eq [simp]: "listsp (inf A B) = inf (listsp A) (listsp B)"
+proof (rule mono_inf [where f=listsp, THEN order_antisym])
show "mono listsp" by (simp add: mono_def listsp_mono)
- show "meet (listsp A) (listsp B) \<le> listsp (meet A B)" by (blast intro: listsp_meetI)
+ show "inf (listsp A) (listsp B) \<le> listsp (inf A B)" by (blast intro: listsp_infI)
qed
-lemmas listsp_conj_eq [simp] = listsp_meet_eq [simplified meet_fun_eq meet_bool_eq]
-
-lemmas lists_Int_eq [simp] = listsp_meet_eq [to_set]
+lemmas listsp_conj_eq [simp] = listsp_inf_eq [simplified inf_fun_eq inf_bool_eq]
+
+lemmas lists_Int_eq [simp] = listsp_inf_eq [to_set]
lemma append_in_listsp_conv [iff]:
"(listsp A (xs @ ys)) = (listsp A xs \<and> listsp A ys)"
@@ -2791,14 +2791,14 @@
*}
lemma mem_iff [normal post]:
- "(x mem xs) = (x \<in> set xs)"
+ "x mem xs \<longleftrightarrow> x \<in> set xs"
by (induct xs) auto
lemmas in_set_code [code unfold] =
mem_iff [symmetric, THEN eq_reflection]
lemma empty_null [code inline]:
- "(xs = []) = null xs"
+ "xs = [] \<longleftrightarrow> null xs"
by (cases xs) simp_all
lemmas null_empty [normal post] =
@@ -2809,22 +2809,22 @@
by (induct xs) auto
lemma list_all_iff [normal post]:
- "list_all P xs = (\<forall>x \<in> set xs. P x)"
+ "list_all P xs \<longleftrightarrow> (\<forall>x \<in> set xs. P x)"
by (induct xs) auto
lemmas list_ball_code [code unfold] =
list_all_iff [symmetric, THEN eq_reflection]
lemma list_all_append [simp]:
- "list_all P (xs @ ys) = (list_all P xs \<and> list_all P ys)"
+ "list_all P (xs @ ys) \<longleftrightarrow> (list_all P xs \<and> list_all P ys)"
by (induct xs) auto
lemma list_all_rev [simp]:
- "list_all P (rev xs) = list_all P xs"
+ "list_all P (rev xs) \<longleftrightarrow> list_all P xs"
by (simp add: list_all_iff)
lemma list_ex_iff [normal post]:
- "list_ex P xs = (\<exists>x \<in> set xs. P x)"
+ "list_ex P xs \<longleftrightarrow> (\<exists>x \<in> set xs. P x)"
by (induct xs) simp_all
lemmas list_bex_code [code unfold] =
--- a/src/HOL/Matrix/Matrix.thy Tue Mar 06 16:40:32 2007 +0100
+++ b/src/HOL/Matrix/Matrix.thy Fri Mar 09 08:45:50 2007 +0100
@@ -7,23 +7,21 @@
imports MatrixGeneral
begin
-instance matrix :: (minus) minus ..
+instance matrix :: ("{plus, zero}") plus
+ plus_matrix_def: "A + B \<equiv> combine_matrix (op +) A B" ..
-instance matrix :: (plus) plus ..
-
-instance matrix :: ("{plus,times}") times ..
+instance matrix :: ("{minus, zero}") minus
+ minus_matrix_def: "- A \<equiv> apply_matrix uminus A"
+ diff_matrix_def: "A - B \<equiv> combine_matrix (op -) A B" ..
-defs (overloaded)
- plus_matrix_def: "A + B == combine_matrix (op +) A B"
- diff_matrix_def: "A - B == combine_matrix (op -) A B"
- minus_matrix_def: "- A == apply_matrix uminus A"
- times_matrix_def: "A * B == mult_matrix (op *) (op +) A B"
+instance matrix :: ("{plus, times, zero}") times
+ times_matrix_def: "A * B \<equiv> mult_matrix (op *) (op +) A B" ..
-lemma is_meet_combine_matrix_meet: "is_meet (combine_matrix meet)"
- by (simp_all add: is_meet_def le_matrix_def meet_left_le meet_right_le le_meetI)
+lemma is_meet_combine_matrix_meet: "is_meet (combine_matrix inf)"
+ by (simp_all add: is_meet_def le_matrix_def inf_le1 inf_le2 le_infI)
-lemma is_join_combine_matrix_join: "is_join (combine_matrix join)"
- by (simp_all add: is_join_def le_matrix_def join_left_le join_right_le join_leI)
+lemma is_join_combine_matrix_join: "is_join (combine_matrix sup)"
+ by (simp_all add: is_join_def le_matrix_def sup_ge1 sup_ge2 le_supI)
instance matrix :: (lordered_ab_group) lordered_ab_group_meet
proof
@@ -58,7 +56,7 @@
qed
defs (overloaded)
- abs_matrix_def: "abs (A::('a::lordered_ab_group) matrix) == join A (- A)"
+ abs_matrix_def: "abs (A::('a::lordered_ab_group) matrix) == sup A (- A)"
instance matrix :: (lordered_ring) lordered_ring
proof
@@ -78,7 +76,7 @@
apply (rule r_distributive_matrix[simplified r_distributive_def, THEN spec, THEN spec, THEN spec])
apply (simp_all add: associative_def commutative_def ring_eq_simps)
done
- show "abs A = join A (-A)"
+ show "abs A = sup A (-A)"
by (simp add: abs_matrix_def)
assume a: "A \<le> B"
assume b: "0 \<le> C"
@@ -102,7 +100,6 @@
apply (simp add: times_matrix_def)
apply (simp add: Rep_mult_matrix)
done
-
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)"
apply (subst Rep_matrix_inject[symmetric])
@@ -122,9 +119,9 @@
lemma ncols_mult: "ncols ((A::('a::lordered_ring) matrix) * B) <= ncols B"
by (simp add: times_matrix_def mult_ncols)
-constdefs
- one_matrix :: "nat \<Rightarrow> ('a::{zero,one}) matrix"
- "one_matrix n == Abs_matrix (% j i. if j = i & j < n then 1 else 0)"
+definition
+ one_matrix :: "nat \<Rightarrow> ('a::{zero,one}) matrix" where
+ "one_matrix n = Abs_matrix (% j i. if j = i & j < n then 1 else 0)"
lemma Rep_one_matrix[simp]: "Rep_matrix (one_matrix n) j i = (if (j = i & j < n) then 1 else 0)"
apply (simp add: one_matrix_def)
@@ -289,13 +286,13 @@
lemma Rep_minus[simp]: "Rep_matrix (-(A::_::lordered_ab_group)) x y = - (Rep_matrix A x y)"
by (simp add: minus_matrix_def)
-lemma join_matrix: "join (A::('a::lordered_ring) matrix) B = combine_matrix join A B"
- apply (insert join_unique[of "(combine_matrix join)::('a matrix \<Rightarrow> 'a matrix \<Rightarrow> 'a matrix)", simplified is_join_combine_matrix_join])
+lemma join_matrix: "sup (A::('a::lordered_ring) matrix) B = combine_matrix sup A B"
+ apply (insert join_unique[of "(combine_matrix sup)::('a matrix \<Rightarrow> 'a matrix \<Rightarrow> 'a matrix)", simplified is_join_combine_matrix_join])
apply (simp)
done
-lemma meet_matrix: "meet (A::('a::lordered_ring) matrix) B = combine_matrix meet A B"
- apply (insert meet_unique[of "(combine_matrix meet)::('a matrix \<Rightarrow> 'a matrix \<Rightarrow> 'a matrix)", simplified is_meet_combine_matrix_meet])
+lemma meet_matrix: "inf (A::('a::lordered_ring) matrix) B = combine_matrix inf A B"
+ apply (insert meet_unique[of "(combine_matrix inf)::('a matrix \<Rightarrow> 'a matrix \<Rightarrow> 'a matrix)", simplified is_meet_combine_matrix_meet])
apply (simp)
done
--- a/src/HOL/MicroJava/BV/JType.thy Tue Mar 06 16:40:32 2007 +0100
+++ b/src/HOL/MicroJava/BV/JType.thy Fri Mar 09 08:45:50 2007 +0100
@@ -108,7 +108,7 @@
lemma wf_converse_subcls1_impl_acc_subtype:
"wfP ((subcls1 G)^--1) \<Longrightarrow> acc (subtype G)"
apply (unfold Semilat.acc_def lesssub_def)
-apply (drule_tac p = "meet ((subcls1 G)^--1) op \<noteq>" in wfP_subset)
+apply (drule_tac p = "inf ((subcls1 G)^--1) op \<noteq>" in wfP_subset)
apply auto
apply (drule wfP_trancl)
apply (simp add: wfP_eq_minimal)
@@ -151,7 +151,7 @@
apply (erule rtrancl.cases)
apply blast
apply (drule rtrancl_converseI')
-apply (subgoal_tac "(meet (subcls1 G) op \<noteq>)^--1 = (meet ((subcls1 G)^--1) op \<noteq>)")
+apply (subgoal_tac "(inf (subcls1 G) op \<noteq>)^--1 = (inf ((subcls1 G)^--1) op \<noteq>)")
prefer 2
apply (simp add: converse_meet)
apply simp
--- a/src/HOL/OrderedGroup.thy Tue Mar 06 16:40:32 2007 +0100
+++ b/src/HOL/OrderedGroup.thy Fri Mar 09 08:45:50 2007 +0100
@@ -1,3 +1,4 @@
+
(* Title: HOL/OrderedGroup.thy
ID: $Id$
Author: Gertrud Bauer, Steven Obua, Lawrence C Paulson, and Markus Wenzel,
@@ -570,97 +571,99 @@
axclass lordered_ab_group_join < pordered_ab_group_add, join_semilorder
-lemma add_meet_distrib_left: "a + (meet b c) = meet (a + b) (a + (c::'a::{pordered_ab_group_add, meet_semilorder}))"
+lemma add_inf_distrib_left: "a + (inf b c) = inf (a + b) (a + (c::'a::{pordered_ab_group_add, meet_semilorder}))"
apply (rule order_antisym)
-apply (simp_all add: le_meetI)
+apply (simp_all add: le_infI)
apply (rule add_le_imp_le_left [of "-a"])
apply (simp only: add_assoc[symmetric], simp)
apply rule
apply (rule add_le_imp_le_left[of "a"], simp only: add_assoc[symmetric], simp)+
done
-lemma add_join_distrib_left: "a + (join b c) = join (a + b) (a+ (c::'a::{pordered_ab_group_add, join_semilorder}))"
+lemma add_sup_distrib_left: "a + (sup b c) = sup (a + b) (a+ (c::'a::{pordered_ab_group_add, join_semilorder}))"
apply (rule order_antisym)
apply (rule add_le_imp_le_left [of "-a"])
apply (simp only: add_assoc[symmetric], simp)
apply rule
apply (rule add_le_imp_le_left [of "a"], simp only: add_assoc[symmetric], simp)+
-apply (rule join_leI)
+apply (rule le_supI)
apply (simp_all)
done
-lemma is_join_neg_meet: "is_join (% (a::'a::{pordered_ab_group_add, meet_semilorder}) b. - (meet (-a) (-b)))"
+lemma is_join_neg_inf: "is_join (% (a::'a::{pordered_ab_group_add, meet_semilorder}) b. - (inf (-a) (-b)))"
apply (auto simp add: is_join_def)
-apply (rule_tac c="meet (-a) (-b)" in add_le_imp_le_right, simp, simp add: add_meet_distrib_left)
-apply (rule_tac c="meet (-a) (-b)" in add_le_imp_le_right, simp, simp add: add_meet_distrib_left)
+apply (rule_tac c="inf (-a) (-b)" in add_le_imp_le_right, simp, simp add: add_inf_distrib_left)
+apply (rule_tac c="inf (-a) (-b)" in add_le_imp_le_right, simp, simp add: add_inf_distrib_left)
apply (subst neg_le_iff_le[symmetric])
-apply (simp add: le_meetI)
+apply (simp add: le_infI)
done
-lemma is_meet_neg_join: "is_meet (% (a::'a::{pordered_ab_group_add, join_semilorder}) b. - (join (-a) (-b)))"
+lemma is_meet_neg_sup: "is_meet (% (a::'a::{pordered_ab_group_add, join_semilorder}) b. - (sup (-a) (-b)))"
apply (auto simp add: is_meet_def)
-apply (rule_tac c="join (-a) (-b)" in add_le_imp_le_right, simp, simp add: add_join_distrib_left)
-apply (rule_tac c="join (-a) (-b)" in add_le_imp_le_right, simp, simp add: add_join_distrib_left)
+apply (rule_tac c="sup (-a) (-b)" in add_le_imp_le_right, simp, simp add: add_sup_distrib_left)
+apply (rule_tac c="sup (-a) (-b)" in add_le_imp_le_right, simp, simp add: add_sup_distrib_left)
apply (subst neg_le_iff_le[symmetric])
-apply (simp add: join_leI)
+apply (simp add: le_supI)
done
axclass lordered_ab_group \<subseteq> pordered_ab_group_add, lorder
-instance lordered_ab_group_meet \<subseteq> lordered_ab_group
-proof
- show "? j. is_join (j::'a\<Rightarrow>'a\<Rightarrow>('a::lordered_ab_group_meet))" by (blast intro: is_join_neg_meet)
-qed
-
instance lordered_ab_group_join \<subseteq> lordered_ab_group
proof
- show "? m. is_meet (m::'a\<Rightarrow>'a\<Rightarrow>('a::lordered_ab_group_join))" by (blast intro: is_meet_neg_join)
+ show "? m. is_meet (m::'a\<Rightarrow>'a\<Rightarrow>('a::lordered_ab_group_join))" by (blast intro: is_meet_neg_sup)
qed
-lemma add_join_distrib_right: "(join a b) + (c::'a::lordered_ab_group) = join (a+c) (b+c)"
+instance lordered_ab_group_meet \<subseteq> lordered_ab_group
+proof
+ show "? j. is_join (j::'a\<Rightarrow>'a\<Rightarrow>('a::lordered_ab_group_meet))" by (blast intro: is_join_neg_inf)
+qed
+
+lemma add_inf_distrib_right: "(inf a b) + (c::'a::lordered_ab_group) = inf (a+c) (b+c)"
proof -
- have "c + (join a b) = join (c+a) (c+b)" by (simp add: add_join_distrib_left)
+ have "c + (inf a b) = inf (c+a) (c+b)" by (simp add: add_inf_distrib_left)
thus ?thesis by (simp add: add_commute)
qed
-lemma add_meet_distrib_right: "(meet a b) + (c::'a::lordered_ab_group) = meet (a+c) (b+c)"
+lemma add_sup_distrib_right: "(sup a b) + (c::'a::lordered_ab_group) = sup (a+c) (b+c)"
proof -
- have "c + (meet a b) = meet (c+a) (c+b)" by (simp add: add_meet_distrib_left)
+ have "c + (sup a b) = sup (c+a) (c+b)" by (simp add: add_sup_distrib_left)
thus ?thesis by (simp add: add_commute)
qed
-lemmas add_meet_join_distribs = add_meet_distrib_right add_meet_distrib_left add_join_distrib_right add_join_distrib_left
+lemmas add_sup_inf_distribs = add_inf_distrib_right add_inf_distrib_left add_sup_distrib_right add_sup_distrib_left
-lemma join_eq_neg_meet: "join a (b::'a::lordered_ab_group) = - meet (-a) (-b)"
-by (simp add: is_join_unique[OF is_join_join is_join_neg_meet])
+lemma sup_eq_neg_inf: "sup a (b::'a::lordered_ab_group) = - inf (-a) (-b)"
+by (simp add: is_join_unique[OF is_join_join is_join_neg_inf])
-lemma meet_eq_neg_join: "meet a (b::'a::lordered_ab_group) = - join (-a) (-b)"
-by (simp add: is_meet_unique[OF is_meet_meet is_meet_neg_join])
+lemma inf_eq_neg_sup: "inf a (b::'a::lordered_ab_group) = - sup (-a) (-b)"
+by (simp add: is_meet_unique[OF is_meet_meet is_meet_neg_sup])
-lemma add_eq_meet_join: "a + b = (join a b) + (meet a (b::'a::lordered_ab_group))"
+lemma add_eq_inf_sup: "a + b = (sup a b) + (inf a (b::'a::lordered_ab_group))"
proof -
- have "0 = - meet 0 (a-b) + meet (a-b) 0" by (simp add: meet_comm)
- hence "0 = join 0 (b-a) + meet (a-b) 0" by (simp add: meet_eq_neg_join)
- hence "0 = (-a + join a b) + (meet a b + (-b))"
- apply (simp add: add_join_distrib_left add_meet_distrib_right)
+ have "0 = - inf 0 (a-b) + inf (a-b) 0" by (simp add: inf_commute)
+ hence "0 = sup 0 (b-a) + inf (a-b) 0" by (simp add: inf_eq_neg_sup)
+ hence "0 = (-a + sup a b) + (inf a b + (-b))"
+ apply (simp add: add_sup_distrib_left add_inf_distrib_right)
by (simp add: diff_minus add_commute)
thus ?thesis
apply (simp add: compare_rls)
- apply (subst add_left_cancel[symmetric, of "a+b" "join a b + meet a b" "-a"])
+ apply (subst add_left_cancel[symmetric, of "a+b" "sup a b + inf a b" "-a"])
apply (simp only: add_assoc, simp add: add_assoc[symmetric])
done
qed
subsection {* Positive Part, Negative Part, Absolute Value *}
-constdefs
- pprt :: "'a \<Rightarrow> ('a::lordered_ab_group)"
- "pprt x == join x 0"
- nprt :: "'a \<Rightarrow> ('a::lordered_ab_group)"
- "nprt x == meet x 0"
+definition
+ nprt :: "'a \<Rightarrow> ('a::lordered_ab_group)" where
+ "nprt x = inf x 0"
+
+definition
+ pprt :: "'a \<Rightarrow> ('a::lordered_ab_group)" where
+ "pprt x = sup x 0"
lemma prts: "a = pprt a + nprt a"
-by (simp add: pprt_def nprt_def add_eq_meet_join[symmetric])
+by (simp add: pprt_def nprt_def add_eq_inf_sup[symmetric])
lemma zero_le_pprt[simp]: "0 \<le> pprt a"
by (simp add: pprt_def)
@@ -687,53 +690,53 @@
lemma nprt_0[simp]: "nprt 0 = 0" by (simp add: nprt_def)
lemma pprt_eq_id[simp]: "0 <= x \<Longrightarrow> pprt x = x"
- by (simp add: pprt_def le_def_join join_aci)
+ by (simp add: pprt_def le_iff_sup sup_aci)
lemma nprt_eq_id[simp]: "x <= 0 \<Longrightarrow> nprt x = x"
- by (simp add: nprt_def le_def_meet meet_aci)
+ by (simp add: nprt_def le_iff_inf inf_aci)
lemma pprt_eq_0[simp]: "x <= 0 \<Longrightarrow> pprt x = 0"
- by (simp add: pprt_def le_def_join join_aci)
+ by (simp add: pprt_def le_iff_sup sup_aci)
lemma nprt_eq_0[simp]: "0 <= x \<Longrightarrow> nprt x = 0"
- by (simp add: nprt_def le_def_meet meet_aci)
+ by (simp add: nprt_def le_iff_inf inf_aci)
-lemma join_0_imp_0: "join a (-a) = 0 \<Longrightarrow> a = (0::'a::lordered_ab_group)"
+lemma sup_0_imp_0: "sup a (-a) = 0 \<Longrightarrow> a = (0::'a::lordered_ab_group)"
proof -
{
fix a::'a
- assume hyp: "join a (-a) = 0"
- hence "join a (-a) + a = a" by (simp)
- hence "join (a+a) 0 = a" by (simp add: add_join_distrib_right)
- hence "join (a+a) 0 <= a" by (simp)
- hence "0 <= a" by (blast intro: order_trans meet_join_le)
+ assume hyp: "sup a (-a) = 0"
+ hence "sup a (-a) + a = a" by (simp)
+ hence "sup (a+a) 0 = a" by (simp add: add_sup_distrib_right)
+ hence "sup (a+a) 0 <= a" by (simp)
+ hence "0 <= a" by (blast intro: order_trans inf_sup_ord)
}
note p = this
- assume hyp:"join a (-a) = 0"
- hence hyp2:"join (-a) (-(-a)) = 0" by (simp add: join_comm)
+ assume hyp:"sup a (-a) = 0"
+ hence hyp2:"sup (-a) (-(-a)) = 0" by (simp add: sup_commute)
from p[OF hyp] p[OF hyp2] show "a = 0" by simp
qed
-lemma meet_0_imp_0: "meet a (-a) = 0 \<Longrightarrow> a = (0::'a::lordered_ab_group)"
-apply (simp add: meet_eq_neg_join)
-apply (simp add: join_comm)
-apply (erule join_0_imp_0)
+lemma inf_0_imp_0: "inf a (-a) = 0 \<Longrightarrow> a = (0::'a::lordered_ab_group)"
+apply (simp add: inf_eq_neg_sup)
+apply (simp add: sup_commute)
+apply (erule sup_0_imp_0)
done
-lemma join_0_eq_0[simp]: "(join a (-a) = 0) = (a = (0::'a::lordered_ab_group))"
-by (auto, erule join_0_imp_0)
+lemma inf_0_eq_0[simp]: "(inf a (-a) = 0) = (a = (0::'a::lordered_ab_group))"
+by (auto, erule inf_0_imp_0)
-lemma meet_0_eq_0[simp]: "(meet a (-a) = 0) = (a = (0::'a::lordered_ab_group))"
-by (auto, erule meet_0_imp_0)
+lemma sup_0_eq_0[simp]: "(sup a (-a) = 0) = (a = (0::'a::lordered_ab_group))"
+by (auto, erule sup_0_imp_0)
lemma zero_le_double_add_iff_zero_le_single_add[simp]: "(0 \<le> a + a) = (0 \<le> (a::'a::lordered_ab_group))"
proof
assume "0 <= a + a"
- hence a:"meet (a+a) 0 = 0" by (simp add: le_def_meet meet_comm)
- have "(meet a 0)+(meet a 0) = meet (meet (a+a) 0) a" (is "?l=_") by (simp add: add_meet_join_distribs meet_aci)
- hence "?l = 0 + meet a 0" by (simp add: a, simp add: meet_comm)
- hence "meet a 0 = 0" by (simp only: add_right_cancel)
- then show "0 <= a" by (simp add: le_def_meet meet_comm)
+ hence a:"inf (a+a) 0 = 0" by (simp add: le_iff_inf inf_commute)
+ have "(inf a 0)+(inf a 0) = inf (inf (a+a) 0) a" (is "?l=_") by (simp add: add_sup_inf_distribs inf_aci)
+ hence "?l = 0 + inf a 0" by (simp add: a, simp add: inf_commute)
+ hence "inf a 0 = 0" by (simp only: add_right_cancel)
+ then show "0 <= a" by (simp add: le_iff_inf inf_commute)
next
assume a: "0 <= a"
show "0 <= a + a" by (simp add: add_mono[OF a a, simplified])
@@ -759,7 +762,7 @@
qed
axclass lordered_ab_group_abs \<subseteq> lordered_ab_group
- abs_lattice: "abs x = join x (-x)"
+ abs_lattice: "abs x = sup x (-x)"
lemma abs_zero[simp]: "abs 0 = (0::'a::lordered_ab_group_abs)"
by (simp add: abs_lattice)
@@ -773,22 +776,22 @@
thus ?thesis by simp
qed
-lemma neg_meet_eq_join[simp]: "- meet a (b::_::lordered_ab_group) = join (-a) (-b)"
-by (simp add: meet_eq_neg_join)
+lemma neg_inf_eq_sup[simp]: "- inf a (b::_::lordered_ab_group) = sup (-a) (-b)"
+by (simp add: inf_eq_neg_sup)
-lemma neg_join_eq_meet[simp]: "- join a (b::_::lordered_ab_group) = meet (-a) (-b)"
-by (simp del: neg_meet_eq_join add: join_eq_neg_meet)
+lemma neg_sup_eq_inf[simp]: "- sup a (b::_::lordered_ab_group) = inf (-a) (-b)"
+by (simp del: neg_inf_eq_sup add: sup_eq_neg_inf)
-lemma join_eq_if: "join a (-a) = (if a < 0 then -a else (a::'a::{lordered_ab_group, linorder}))"
+lemma sup_eq_if: "sup a (-a) = (if a < 0 then -a else (a::'a::{lordered_ab_group, linorder}))"
proof -
note b = add_le_cancel_right[of a a "-a",symmetric,simplified]
have c: "a + a = 0 \<Longrightarrow> -a = a" by (rule add_right_imp_eq[of _ a], simp)
- show ?thesis by (auto simp add: join_max max_def b linorder_not_less)
+ show ?thesis by (auto simp add: max_def b linorder_not_less join_max)
qed
lemma abs_if_lattice: "\<bar>a\<bar> = (if a < 0 then -a else (a::'a::{lordered_ab_group_abs, linorder}))"
proof -
- show ?thesis by (simp add: abs_lattice join_eq_if)
+ show ?thesis by (simp add: abs_lattice sup_eq_if)
qed
lemma abs_ge_zero[simp]: "0 \<le> abs (a::'a::lordered_ab_group_abs)"
@@ -824,16 +827,16 @@
lemma abs_prts: "abs (a::_::lordered_ab_group_abs) = pprt a - nprt a"
apply (simp add: pprt_def nprt_def diff_minus)
-apply (simp add: add_meet_join_distribs join_aci abs_lattice[symmetric])
-apply (subst join_absorp2, auto)
+apply (simp add: add_sup_inf_distribs sup_aci abs_lattice[symmetric])
+apply (subst sup_absorb2, auto)
done
lemma abs_minus_cancel [simp]: "abs (-a) = abs(a::'a::lordered_ab_group_abs)"
-by (simp add: abs_lattice join_comm)
+by (simp add: abs_lattice sup_commute)
lemma abs_idempotent [simp]: "abs (abs a) = abs (a::'a::lordered_ab_group_abs)"
apply (simp add: abs_lattice[of "abs a"])
-apply (subst join_absorp1)
+apply (subst sup_absorb1)
apply (rule order_trans[of _ 0])
by auto
@@ -847,22 +850,22 @@
qed
lemma zero_le_iff_zero_nprt: "(0 \<le> a) = (nprt a = 0)"
-by (simp add: le_def_meet nprt_def meet_comm)
+by (simp add: le_iff_inf nprt_def inf_commute)
lemma le_zero_iff_zero_pprt: "(a \<le> 0) = (pprt a = 0)"
-by (simp add: le_def_join pprt_def join_comm)
+by (simp add: le_iff_sup pprt_def sup_commute)
lemma le_zero_iff_pprt_id: "(0 \<le> a) = (pprt a = a)"
-by (simp add: le_def_join pprt_def join_comm)
+by (simp add: le_iff_sup pprt_def sup_commute)
lemma zero_le_iff_nprt_id: "(a \<le> 0) = (nprt a = a)"
-by (simp add: le_def_meet nprt_def meet_comm)
+by (simp add: le_iff_inf nprt_def inf_commute)
lemma pprt_mono[simp]: "(a::_::lordered_ab_group) <= b \<Longrightarrow> pprt a <= pprt b"
- by (simp add: le_def_join pprt_def join_aci)
+ by (simp add: le_iff_sup pprt_def sup_aci)
lemma nprt_mono[simp]: "(a::_::lordered_ab_group) <= b \<Longrightarrow> nprt a <= nprt b"
- by (simp add: le_def_meet nprt_def meet_aci)
+ by (simp add: le_iff_inf nprt_def inf_aci)
lemma pprt_neg: "pprt (-x) = - nprt x"
by (simp add: pprt_def nprt_def)
@@ -887,7 +890,7 @@
by (rule abs_of_nonpos, rule order_less_imp_le)
lemma abs_leI: "[|a \<le> b; -a \<le> b|] ==> abs a \<le> (b::'a::lordered_ab_group_abs)"
-by (simp add: abs_lattice join_leI)
+by (simp add: abs_lattice le_supI)
lemma le_minus_self_iff: "(a \<le> -a) = (a \<le> (0::'a::lordered_ab_group))"
proof -
@@ -914,14 +917,14 @@
lemma abs_triangle_ineq: "abs(a+b) \<le> abs a + abs(b::'a::lordered_ab_group_abs)"
proof -
- have g:"abs a + abs b = join (a+b) (join (-a-b) (join (-a+b) (a + (-b))))" (is "_=join ?m ?n")
- by (simp add: abs_lattice add_meet_join_distribs join_aci diff_minus)
- have a:"a+b <= join ?m ?n" by (simp)
+ have g:"abs a + abs b = sup (a+b) (sup (-a-b) (sup (-a+b) (a + (-b))))" (is "_=sup ?m ?n")
+ by (simp add: abs_lattice add_sup_inf_distribs sup_aci diff_minus)
+ have a:"a+b <= sup ?m ?n" by (simp)
have b:"-a-b <= ?n" by (simp)
- have c:"?n <= join ?m ?n" by (simp)
- from b c have d: "-a-b <= join ?m ?n" by(rule order_trans)
+ have c:"?n <= sup ?m ?n" by (simp)
+ from b c have d: "-a-b <= sup ?m ?n" by(rule order_trans)
have e:"-a-b = -(a+b)" by (simp add: diff_minus)
- from a d e have "abs(a+b) <= join ?m ?n"
+ from a d e have "abs(a+b) <= sup ?m ?n"
by (drule_tac abs_leI, auto)
with g[symmetric] show ?thesis by simp
qed
@@ -1126,24 +1129,24 @@
val compare_rls = thms "compare_rls";
val eq_iff_diff_eq_0 = thm "eq_iff_diff_eq_0";
val le_iff_diff_le_0 = thm "le_iff_diff_le_0";
-val add_meet_distrib_left = thm "add_meet_distrib_left";
-val add_join_distrib_left = thm "add_join_distrib_left";
-val is_join_neg_meet = thm "is_join_neg_meet";
-val is_meet_neg_join = thm "is_meet_neg_join";
-val add_join_distrib_right = thm "add_join_distrib_right";
-val add_meet_distrib_right = thm "add_meet_distrib_right";
-val add_meet_join_distribs = thms "add_meet_join_distribs";
-val join_eq_neg_meet = thm "join_eq_neg_meet";
-val meet_eq_neg_join = thm "meet_eq_neg_join";
-val add_eq_meet_join = thm "add_eq_meet_join";
+val add_inf_distrib_left = thm "add_inf_distrib_left";
+val add_sup_distrib_left = thm "add_sup_distrib_left";
+val is_join_neg_inf = thm "is_join_neg_inf";
+val is_meet_neg_sup = thm "is_meet_neg_sup";
+val add_sup_distrib_right = thm "add_sup_distrib_right";
+val add_inf_distrib_right = thm "add_inf_distrib_right";
+val add_sup_inf_distribs = thms "add_sup_inf_distribs";
+val sup_eq_neg_inf = thm "sup_eq_neg_inf";
+val inf_eq_neg_sup = thm "inf_eq_neg_sup";
+val add_eq_inf_sup = thm "add_eq_inf_sup";
val prts = thm "prts";
val zero_le_pprt = thm "zero_le_pprt";
val nprt_le_zero = thm "nprt_le_zero";
val le_eq_neg = thm "le_eq_neg";
-val join_0_imp_0 = thm "join_0_imp_0";
-val meet_0_imp_0 = thm "meet_0_imp_0";
-val join_0_eq_0 = thm "join_0_eq_0";
-val meet_0_eq_0 = thm "meet_0_eq_0";
+val sup_0_imp_0 = thm "sup_0_imp_0";
+val inf_0_imp_0 = thm "inf_0_imp_0";
+val sup_0_eq_0 = thm "sup_0_eq_0";
+val inf_0_eq_0 = thm "inf_0_eq_0";
val zero_le_double_add_iff_zero_le_single_add = thm "zero_le_double_add_iff_zero_le_single_add";
val double_add_le_zero_iff_single_add_le_zero = thm "double_add_le_zero_iff_single_add_le_zero";
val double_add_less_zero_iff_single_less_zero = thm "double_add_less_zero_iff_single_less_zero";
@@ -1151,9 +1154,9 @@
val abs_zero = thm "abs_zero";
val abs_eq_0 = thm "abs_eq_0";
val abs_0_eq = thm "abs_0_eq";
-val neg_meet_eq_join = thm "neg_meet_eq_join";
-val neg_join_eq_meet = thm "neg_join_eq_meet";
-val join_eq_if = thm "join_eq_if";
+val neg_inf_eq_sup = thm "neg_inf_eq_sup";
+val neg_sup_eq_inf = thm "neg_sup_eq_inf";
+val sup_eq_if = thm "sup_eq_if";
val abs_if_lattice = thm "abs_if_lattice";
val abs_ge_zero = thm "abs_ge_zero";
val abs_le_zero_iff = thm "abs_le_zero_iff";
@@ -1161,10 +1164,10 @@
val abs_not_less_zero = thm "abs_not_less_zero";
val abs_ge_self = thm "abs_ge_self";
val abs_ge_minus_self = thm "abs_ge_minus_self";
-val le_imp_join_eq = thm "join_absorp2";
-val ge_imp_join_eq = thm "join_absorp1";
-val le_imp_meet_eq = thm "meet_absorp1";
-val ge_imp_meet_eq = thm "meet_absorp2";
+val le_imp_join_eq = thm "sup_absorb2";
+val ge_imp_join_eq = thm "sup_absorb1";
+val le_imp_meet_eq = thm "inf_absorb1";
+val ge_imp_meet_eq = thm "inf_absorb2";
val abs_prts = thm "abs_prts";
val abs_minus_cancel = thm "abs_minus_cancel";
val abs_idempotent = thm "abs_idempotent";
@@ -1173,8 +1176,6 @@
val le_zero_iff_pprt_id = thm "le_zero_iff_pprt_id";
val zero_le_iff_nprt_id = thm "zero_le_iff_nprt_id";
val iff2imp = thm "iff2imp";
-(* val imp_abs_id = thm "imp_abs_id";
-val imp_abs_neg_id = thm "imp_abs_neg_id"; *)
val abs_leI = thm "abs_leI";
val le_minus_self_iff = thm "le_minus_self_iff";
val minus_le_self_iff = thm "minus_le_self_iff";
--- a/src/HOL/Predicate.thy Tue Mar 06 16:40:32 2007 +0100
+++ b/src/HOL/Predicate.thy Fri Mar 09 08:45:50 2007 +0100
@@ -202,28 +202,28 @@
subsubsection {* Binary union *}
-lemma member_Un [pred_set_conv]: "join (member R) (member S) = member (R Un S)"
- by (simp add: expand_fun_eq join_fun_eq join_bool_eq)
+lemma member_Un [pred_set_conv]: "sup (member R) (member S) = member (R Un S)"
+ by (simp add: expand_fun_eq sup_fun_eq sup_bool_eq)
-lemma member2_Un [pred_set_conv]: "join (member2 R) (member2 S) = member2 (R Un S)"
- by (simp add: expand_fun_eq join_fun_eq join_bool_eq)
+lemma member2_Un [pred_set_conv]: "sup (member2 R) (member2 S) = member2 (R Un S)"
+ by (simp add: expand_fun_eq sup_fun_eq sup_bool_eq)
-lemma join1_iff [simp]: "(join A B x) = (A x | B x)"
- by (simp add: join_fun_eq join_bool_eq)
+lemma sup1_iff [simp]: "sup A B x \<longleftrightarrow> A x | B x"
+ by (simp add: sup_fun_eq sup_bool_eq)
-lemma join2_iff [simp]: "(join A B x y) = (A x y | B x y)"
- by (simp add: join_fun_eq join_bool_eq)
+lemma sup2_iff [simp]: "sup A B x y \<longleftrightarrow> A x y | B x y"
+ by (simp add: sup_fun_eq sup_bool_eq)
-lemma join1I1 [elim?]: "A x ==> join A B x"
+lemma sup1I1 [elim?]: "A x \<Longrightarrow> sup A B x"
by simp
-lemma join2I1 [elim?]: "A x y ==> join A B x y"
+lemma sup2I1 [elim?]: "A x y \<Longrightarrow> sup A B x y"
by simp
-lemma join1I2 [elim?]: "B x ==> join A B x"
+lemma join1I2 [elim?]: "B x \<Longrightarrow> sup A B x"
by simp
-lemma join2I2 [elim?]: "B x y ==> join A B x y"
+lemma sup1I2 [elim?]: "B x y \<Longrightarrow> sup A B x y"
by simp
text {*
@@ -231,55 +231,55 @@
@{text B}.
*}
-lemma join1CI [intro!]: "(~ B x ==> A x) ==> join A B x"
+lemma sup1CI [intro!]: "(~ B x ==> A x) ==> sup A B x"
by auto
-lemma join2CI [intro!]: "(~ B x y ==> A x y) ==> join A B x y"
+lemma sup2CI [intro!]: "(~ B x y ==> A x y) ==> sup A B x y"
by auto
-lemma join1E [elim!]: "join A B x ==> (A x ==> P) ==> (B x ==> P) ==> P"
+lemma sup1E [elim!]: "sup A B x ==> (A x ==> P) ==> (B x ==> P) ==> P"
by simp iprover
-lemma join2E [elim!]: "join A B x y ==> (A x y ==> P) ==> (B x y ==> P) ==> P"
+lemma sup2E [elim!]: "sup A B x y ==> (A x y ==> P) ==> (B x y ==> P) ==> P"
by simp iprover
subsubsection {* Binary intersection *}
-lemma member_Int [pred_set_conv]: "meet (member R) (member S) = member (R Int S)"
- by (simp add: expand_fun_eq meet_fun_eq meet_bool_eq)
+lemma member_Int [pred_set_conv]: "inf (member R) (member S) = member (R Int S)"
+ by (simp add: expand_fun_eq inf_fun_eq inf_bool_eq)
-lemma member2_Int [pred_set_conv]: "meet (member2 R) (member2 S) = member2 (R Int S)"
- by (simp add: expand_fun_eq meet_fun_eq meet_bool_eq)
+lemma member2_Int [pred_set_conv]: "inf (member2 R) (member2 S) = member2 (R Int S)"
+ by (simp add: expand_fun_eq inf_fun_eq inf_bool_eq)
-lemma meet1_iff [simp]: "(meet A B x) = (A x & B x)"
- by (simp add: meet_fun_eq meet_bool_eq)
+lemma inf1_iff [simp]: "inf A B x \<longleftrightarrow> A x \<and> B x"
+ by (simp add: inf_fun_eq inf_bool_eq)
-lemma meet2_iff [simp]: "(meet A B x y) = (A x y & B x y)"
- by (simp add: meet_fun_eq meet_bool_eq)
+lemma inf2_iff [simp]: "inf A B x y \<longleftrightarrow> A x y \<and> B x y"
+ by (simp add: inf_fun_eq inf_bool_eq)
-lemma meet1I [intro!]: "A x ==> B x ==> meet A B x"
+lemma inf1I [intro!]: "A x ==> B x ==> inf A B x"
by simp
-lemma meet2I [intro!]: "A x y ==> B x y ==> meet A B x y"
+lemma inf2I [intro!]: "A x y ==> B x y ==> inf A B x y"
by simp
-lemma meet1D1: "meet A B x ==> A x"
+lemma inf1D1: "inf A B x ==> A x"
by simp
-lemma meet2D1: "meet A B x y ==> A x y"
+lemma inf2D1: "inf A B x y ==> A x y"
by simp
-lemma meet1D2: "meet A B x ==> B x"
+lemma inf1D2: "inf A B x ==> B x"
by simp
-lemma meet2D2: "meet A B x y ==> B x y"
+lemma inf2D2: "inf A B x y ==> B x y"
by simp
-lemma meet1E [elim!]: "meet A B x ==> (A x ==> B x ==> P) ==> P"
+lemma inf1E [elim!]: "inf A B x ==> (A x ==> B x ==> P) ==> P"
by simp
-lemma meet2E [elim!]: "meet A B x y ==> (A x y ==> B x y ==> P) ==> P"
+lemma inf2E [elim!]: "inf A B x y ==> (A x y ==> B x y ==> P) ==> P"
by simp
@@ -357,12 +357,12 @@
by (iprover intro: order_antisym conversepI pred_compI
elim: pred_compE dest: conversepD)
-lemma converse_meet: "(meet r s)^--1 = meet r^--1 s^--1"
- by (simp add: meet_fun_eq meet_bool_eq)
+lemma converse_meet: "(inf r s)^--1 = inf r^--1 s^--1"
+ by (simp add: inf_fun_eq inf_bool_eq)
(iprover intro: conversepI ext dest: conversepD)
-lemma converse_join: "(join r s)^--1 = join r^--1 s^--1"
- by (simp add: join_fun_eq join_bool_eq)
+lemma converse_join: "(sup r s)^--1 = sup r^--1 s^--1"
+ by (simp add: sup_fun_eq sup_bool_eq)
(iprover intro: conversepI ext dest: conversepD)
lemma conversep_noteq [simp]: "(op ~=)^--1 = op ~="
--- a/src/HOL/Ring_and_Field.thy Tue Mar 06 16:40:32 2007 +0100
+++ b/src/HOL/Ring_and_Field.thy Fri Mar 09 08:45:50 2007 +0100
@@ -279,7 +279,7 @@
instance ordered_ring_strict \<subseteq> lordered_ab_group ..
instance ordered_ring_strict \<subseteq> lordered_ring
- by (intro_classes, simp add: abs_if join_eq_if)
+ by intro_classes (simp add: abs_if sup_eq_if)
class pordered_comm_ring = comm_ring + pordered_comm_semiring
--- a/src/HOL/Tools/inductive_package.ML Tue Mar 06 16:40:32 2007 +0100
+++ b/src/HOL/Tools/inductive_package.ML Fri Mar 09 08:45:50 2007 +0100
@@ -533,7 +533,7 @@
[rewrite_goals_tac [inductive_conj_def],
DETERM (rtac raw_fp_induct 1),
REPEAT (resolve_tac [le_funI, le_boolI] 1),
- rewrite_goals_tac (map mk_meta_eq [meet_fun_eq, meet_bool_eq] @ simp_thms'),
+ rewrite_goals_tac (map mk_meta_eq [inf_fun_eq, inf_bool_eq] @ simp_thms'),
(*This disjE separates out the introduction rules*)
REPEAT (FIRSTGOAL (eresolve_tac [disjE, exE, FalseE])),
(*Now break down the individual cases. No disjE here in case
--- a/src/HOL/Tools/res_atp.ML Tue Mar 06 16:40:32 2007 +0100
+++ b/src/HOL/Tools/res_atp.ML Fri Mar 09 08:45:50 2007 +0100
@@ -374,8 +374,8 @@
"NatSimprocs.zero_less_divide_iff_number_of",
"OrderedGroup.abs_0_eq", (*duplicate by symmetry*)
"OrderedGroup.diff_eq_0_iff_eq", (*prolific?*)
- "OrderedGroup.join_0_eq_0",
- "OrderedGroup.meet_0_eq_0",
+ "OrderedGroup.sup_0_eq_0",
+ "OrderedGroup.inf_0_eq_0",
"OrderedGroup.pprt_eq_0", (*obscure*)
"OrderedGroup.pprt_eq_id", (*obscure*)
"OrderedGroup.pprt_mono", (*obscure*)
--- a/src/HOL/Transitive_Closure.thy Tue Mar 06 16:40:32 2007 +0100
+++ b/src/HOL/Transitive_Closure.thy Fri Mar 09 08:45:50 2007 +0100
@@ -43,7 +43,7 @@
abbreviation
reflcl :: "('a => 'a => bool) => 'a => 'a => bool" ("(_^==)" [1000] 1000) where
- "r^== == join r op ="
+ "r^== == sup r op ="
abbreviation
reflcl_set :: "('a \<times> 'a) set => ('a \<times> 'a) set" ("(_^=)" [1000] 999) where
@@ -71,7 +71,7 @@
lemma rtrancl_set_eq [pred_set_conv]: "(member2 r)^** = member2 (r^*)"
by (simp add: rtrancl_set_def)
-lemma reflcl_set_eq [pred_set_conv]: "(join (member2 r) op =) = member2 (r Un Id)"
+lemma reflcl_set_eq [pred_set_conv]: "(sup (member2 r) op =) = member2 (r Un Id)"
by (simp add: expand_fun_eq)
lemmas rtrancl_refl [intro!, Pure.intro!, simp] = rtrancl_refl [to_set]
@@ -190,7 +190,7 @@
lemmas rtrancl_subset = rtrancl_subset' [to_set]
-lemma rtrancl_Un_rtrancl': "(join (R^**) (S^**))^** = (join R S)^**"
+lemma rtrancl_Un_rtrancl': "(sup (R^**) (S^**))^** = (sup R S)^**"
by (blast intro!: rtrancl_subset' intro: rtrancl_mono' [THEN predicate2D])
lemmas rtrancl_Un_rtrancl = rtrancl_Un_rtrancl' [to_set]
@@ -208,7 +208,7 @@
apply (blast intro!: r_into_rtrancl)
done
-lemma rtrancl_r_diff_Id': "(meet r op ~=)^** = r^**"
+lemma rtrancl_r_diff_Id': "(inf r op ~=)^** = r^**"
apply (rule sym)
apply (rule rtrancl_subset')
apply blast+