# HG changeset patch # User haftmann # Date 1173426350 -3600 # Node ID ee19cdb07528f571f387c18fc9806aabc3036389 # Parent 51a18dd1ea864ae886ca868af54f782ab4ecb777 stepping towards uniform lattice theory development in HOL diff -r 51a18dd1ea86 -r ee19cdb07528 NEWS --- 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. diff -r 51a18dd1ea86 -r ee19cdb07528 src/HOL/FixedPoint.thy --- 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 \ Inf *) + consts - Meet :: "'a::order set \ 'a" - Sup :: "'a::order set \ 'a" + Inf :: "'a::order set \ 'a" -defs Sup_def: "Sup A == Meet {b. \a \ A. a <= b}" +definition + Sup :: "'a::order set \ 'a" where + "Sup A = Inf {b. \a \ A. a \ b}" definition SUP :: "('a \ 'b::order) \ '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 \ A \ Meet A \ x" - assumes Meet_greatest: "(\x. x \ A \ z \ x) \ z \ Meet A" + assumes Inf_lower: "x \ A \ Inf A \ x" + assumes Inf_greatest: "(\x. x \ A \ z \ x) \ z \ Inf A" theorem Sup_upper: "(x::'a::comp_lat) \ A \ x <= Sup A" - by (auto simp: Sup_def intro: Meet_greatest) + by (auto simp: Sup_def intro: Inf_greatest) theorem Sup_least: "(\x::'a::comp_lat. x \ A \ x <= z) \ 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 (\(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 (\(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 (\(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 "\m::'a\'a\'a. is_meet m" by iprover + from is_meet_Inf show "\m::'a\'a\'a. is_meet m" by iprover from is_join_Sup show "\j::'a\'a\'a. is_join j" by iprover qed subsubsection {* Properties *} -lemma mono_join: "mono f \ join (f A) (f B) <= f (join A B)" +lemma mono_inf: "mono f \ f (inf A B) <= inf (f A) (f B)" by (auto simp add: mono_def) -lemma mono_meet: "mono f \ f (meet A B) <= meet (f A) (f B)" +lemma mono_sup: "mono f \ 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{} \ (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 \ l \ 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 \ x \ u) \ Sup M \ (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 \ Q)" +theorem inf_bool_eq: "inf P Q \ P \ 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 \ Q)" +theorem sup_bool_eq: "sup P Q \ P \ 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 \ (\x \ 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 "\"} -on unary and binary predicates + Handy introduction and elimination rules for @{text "\"} + 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 == (\x. Meet {y. EX f:A. y = f x})" +defs + Inf_fun_def: "Inf A == (\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 = (\x. meet (f x) (g x))" +theorem inf_fun_eq: "inf f g = (\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 = (\x. join (f x) (g x))" +theorem sup_fun_eq: "sup f g = (\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 = (\x. Sup {y::'a::comp_lat. EX f:A. y = f x})" @@ -278,29 +282,30 @@ subsubsection {* Sets *} -defs Meet_set_def: "Meet S == \S" +defs + Inf_set_def: "Inf S == \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 \ B" +theorem inf_set_eq: "inf A B = A \ 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 \ B" +theorem sup_set_eq: "sup A B = A \ 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 = \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\comp_lat \ 'a) \ 'a" where + "lfp f = Inf {u. f u \ u}" --{*least fixed point*} - gfp :: "(('a::comp_lat) => 'a) => 'a" - "gfp f == Sup {u. u <= f u}" --{*greatest fixed point*} +definition + gfp :: "('a\comp_lat \ 'a) \ 'a" where + "gfp f = Sup {u. u \ 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) \ u}"} *} lemma lfp_lowerbound: "f A \ A ==> lfp f \ 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 \ u ==> A \ u) ==> A \ 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) \ 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) \ P + f (inf A P) \ P |] ==> A \ P" by (blast intro: lfp_induct) @@ -447,25 +452,25 @@ done lemma coinduct_lemma: - "[| X \ f (join X (gfp f)); mono f |] ==> join X (gfp f) \ f (join X (gfp f))" + "[| X \ f (sup X (gfp f)); mono f |] ==> sup X (gfp f) \ 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 \ 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 \ f (join X (gfp f)) |] ==> X \ gfp(f)" +lemma coinduct: "[| mono(f); X \ f (sup X (gfp f)) |] ==> X \ 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 \ f(join X A) |] ==> X \ A" + "[| A==gfp(f); mono(f); X \ f(sup X A) |] ==> X \ 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"; diff -r 51a18dd1ea86 -r ee19cdb07528 src/HOL/Hyperreal/StarClasses.thy --- 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]: - "\x \ Standard; y \ Standard\ \ meet x y \ Standard" -by (simp add: star_meet_def) +lemma Standard_inf [simp]: + "\x \ Standard; y \ Standard\ \ inf x y \ Standard" +by (simp add: star_inf_def) -lemma Standard_join [simp]: - "\x \ Standard; y \ Standard\ \ join x y \ Standard" -by (simp add: star_join_def) +lemma Standard_sup [simp]: + "\x \ Standard; y \ Standard\ \ sup x y \ 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 *} diff -r 51a18dd1ea86 -r ee19cdb07528 src/HOL/LOrder.thy --- 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 \ 'a\lower_semilattice \ 'a \ 'a)" +unfolding is_meet_def by auto + +lemma is_join_sup: "is_join (sup \ 'a\upper_semilattice \ 'a \ '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) \ 'a \ 'a" - "meet == THE m. is_meet m" - join :: "('a::join_semilorder) \ 'a \ 'a" - "join == THE j. is_join j" +definition + inf :: "('a::meet_semilorder) \ 'a \ 'a" where + "inf = (THE m. is_meet m)" -lemma is_meet_meet: "is_meet (meet::'a \ 'a \ ('a::meet_semilorder))" +definition + sup :: "('a::join_semilorder) \ 'a \ 'a" where + "sup = (THE j. is_join j)" + +lemma is_meet_meet: "is_meet (inf::'a \ 'a \ ('a::meet_semilorder))" proof - from meet_exists obtain k::"'a \ 'a \ '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 \ 'a \ ('a::join_semilorder))" +lemma is_join_join: "is_join (sup::'a \ 'a \ ('a::join_semilorder))" proof - from join_exists obtain k::"'a \ 'a \ '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 \ \ 'a\meet_semilorder \ 'a \ bool" "op <" meet] +lemma inf_unique: "(is_meet m) = (m = (Lattices.inf \ 'a \ 'a \ 'a\lower_semilattice))" +by (insert is_meet_inf, auto simp add: is_meet_unique) + +lemma sup_unique: "(is_join j) = (j = (Lattices.sup \ 'a \ 'a \ 'a\upper_semilattice))" +by (insert is_join_sup, auto simp add: is_join_unique) + +interpretation inf_semilat: + lower_semilattice ["op \ \ 'a\meet_semilorder \ 'a \ bool" "op <" inf] proof unfold_locales fix x y z :: "'a\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 \ x" by blast - from meet show "meet x y \ y" by blast - from meet show "x \ y \ x \ z \ x \ meet y z" by blast + from meet show "inf x y \ x" by blast + from meet show "inf x y \ y" by blast + from meet show "x \ y \ x \ z \ x \ inf y z" by blast qed -interpretation join_semilat: - upper_semilattice ["op \ \ 'a\join_semilorder \ 'a \ bool" "op <" join] +interpretation sup_semilat: + upper_semilattice ["op \ \ 'a\join_semilorder \ 'a \ bool" "op <" sup] proof unfold_locales fix x y z :: "'a\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 \ join x y" by blast - from join show "y \ join x y" by blast - from join show "x \ z \ y \ z \ join x y \ z" by blast + from join show "x \ sup x y" by blast + from join show "y \ sup x y" by blast + from join show "x \ z \ y \ z \ sup x y \ 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 \ \ 'a\lorder \ 'a \ 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 \ \ 'a\lorder \ 'a \ bool" "op <" inf sup] + by unfold_locales lemma is_meet_min: "is_meet (min::'a \ 'a \ ('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 \ 'a \ ('a::linorder))" + by (auto simp add: is_join_def max_def) -lemma is_join_max: "is_join (max::'a \ 'a \ ('a::linorder))" -by (auto simp add: is_join_def max_def) - -instance linorder \ meet_semilorder +instance linorder \ lorder proof from is_meet_min show "? (m::'a\'a\('a::linorder)). is_meet m" by auto -qed - -instance linorder \ join_semilorder -proof from is_join_max show "? (j::'a\'a\('a::linorder)). is_join j" by auto qed - -instance linorder \ lorder .. -lemma meet_min: "meet = (min :: 'a\'a\('a::linorder))" -by (simp add: is_meet_meet is_meet_min is_meet_unique) +lemma meet_min: "inf = (min \ 'a\{linorder} \ 'a \ 'a)" + by (simp add: is_meet_meet is_meet_min is_meet_unique) +lemma join_max: "sup = (max \ 'a\{linorder} \ 'a \ 'a)" + by (simp add: is_join_join is_join_max is_join_unique) -lemma join_max: "join = (max :: 'a\'a\('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 \ \ 'a\{meet_semilorder,join_semilorder} \ 'a \ 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 diff -r 51a18dd1ea86 -r ee19cdb07528 src/HOL/Lambda/Commutation.thy --- 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 = - (\x y. (join R (R^--1))^** x y --> (\z. R^** x z \ R^** y z))" + (\x y. (sup R (R^--1))^** x y --> (\z. R^** x z \ 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') diff -r 51a18dd1ea86 -r ee19cdb07528 src/HOL/Lambda/Eta.thy --- 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 diff -r 51a18dd1ea86 -r ee19cdb07528 src/HOL/Lattices.thy --- 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 \ 'a \ 'a" (infixl "\" 70) - assumes inf_le1[simp]: "x \ y \ x" and inf_le2[simp]: "x \ y \ y" + assumes inf_le1 [simp]: "x \ y \ x" and inf_le2 [simp]: "x \ y \ y" and inf_greatest: "x \ y \ x \ z \ x \ y \ z" -locale upper_semilattice = order + +class upper_semilattice = order + fixes sup :: "'a \ 'a \ 'a" (infixl "\" 65) - assumes sup_ge1[simp]: "x \ x \ y" and sup_ge2[simp]: "y \ x \ y" + assumes sup_ge1 [simp]: "x \ x \ y" and sup_ge2 [simp]: "y \ x \ y" and sup_least: "y \ x \ z \ x \ y \ z \ 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 \ x \ a \ b \ x" apply(subgoal_tac "a \ b \ a") apply(blast intro: order_trans) apply simp done +lemmas (in -) [rule del] = le_infI1 lemma le_infI2[intro]: "b \ x \ a \ b \ x" apply(subgoal_tac "a \ b \ b") apply(blast intro: order_trans) apply simp done +lemmas (in -) [rule del] = le_infI2 lemma le_infI[intro!]: "x \ a \ x \ b \ x \ a \ b" by(blast intro: inf_greatest) +lemmas (in -) [rule del] = le_infI -lemma le_infE[elim!]: "x \ a \ b \ (x \ a \ x \ b \ P) \ P" -by(blast intro: order_trans) +lemma le_infE [elim!]: "x \ a \ b \ (x \ a \ x \ b \ P) \ P" + by (blast intro: order_trans) +lemmas (in -) [rule del] = le_infE lemma le_inf_iff [simp]: "x \ y \ z = (x \ y \ x \ 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 \ a \ x \ a \ b" apply(subgoal_tac "a \ a \ b") apply(blast intro: order_trans) apply simp done +lemmas (in -) [rule del] = le_supI1 lemma le_supI2[intro]: "x \ b \ x \ a \ b" apply(subgoal_tac "b \ a \ b") apply(blast intro: order_trans) apply simp done +lemmas (in -) [rule del] = le_supI2 lemma le_supI[intro!]: "a \ x \ b \ x \ a \ b \ x" by(blast intro: sup_least) +lemmas (in -) [rule del] = le_supI lemma le_supE[elim!]: "a \ b \ x \ (a \ x \ b \ x \ P) \ P" -by(blast intro: order_trans) + by (blast intro: order_trans) +lemmas (in -) [rule del] = le_supE + lemma ge_sup_conv[simp]: "x \ y \ z = (x \ z \ y \ 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 *} diff -r 51a18dd1ea86 -r ee19cdb07528 src/HOL/Library/Continuity.thy --- 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 \ 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 "\ = (SUP i. F(?C i))" using `chain ?C` `continuous F` by(simp add:continuous_def) - also have "\ = join (F A) (F B)" by(simp add: SUP_nat_conv) + also have "\ = sup (F A) (F B)" by(simp add: SUP_nat_conv) finally show ?thesis . qed - thus "F A \ F B" by(subst le_def_join, simp) + thus "F A \ F B" by(subst le_iff_sup, simp) qed lemma continuous_lfp: diff -r 51a18dd1ea86 -r ee19cdb07528 src/HOL/Library/Graphs.thy --- 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 == \Gs. Graph (\(dest_graph ` Gs))" + Inf_graph_def: "Inf == \Gs. Graph (\(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 \ ('a,'b) graph \ ('a,'b) graph)" unfolding is_join_def @@ -172,7 +172,7 @@ lemma plus_is_join: "(op +) = - (join :: ('a::type, 'b::monoid_mult) graph \ ('a,'b) graph \ ('a,'b) graph)" + (sup :: ('a::type, 'b::monoid_mult) graph \ ('a,'b) graph \ ('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 ?\ = fst loop" by (auto simp:path_loop_def path_nth_def split_def k) - + show "snd ?\ = snd loop" proof (rule nth_equalityI[rule_format]) show leneq: "length (snd ?\) = length (snd loop)" @@ -716,11 +716,5 @@ by (simp add:path_nth_def) qed qed - - - - - - end \ No newline at end of file diff -r 51a18dd1ea86 -r ee19cdb07528 src/HOL/List.thy --- 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) \ listsp (meet A B)" by (blast intro: listsp_meetI) + show "inf (listsp A) (listsp B) \ 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 \ listsp A ys)" @@ -2791,14 +2791,14 @@ *} lemma mem_iff [normal post]: - "(x mem xs) = (x \ set xs)" + "x mem xs \ x \ 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 = [] \ 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 = (\x \ set xs. P x)" + "list_all P xs \ (\x \ 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 \ list_all P ys)" + "list_all P (xs @ ys) \ (list_all P xs \ 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) \ list_all P xs" by (simp add: list_all_iff) lemma list_ex_iff [normal post]: - "list_ex P xs = (\x \ set xs. P x)" + "list_ex P xs \ (\x \ set xs. P x)" by (induct xs) simp_all lemmas list_bex_code [code unfold] = diff -r 51a18dd1ea86 -r ee19cdb07528 src/HOL/Matrix/Matrix.thy --- 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 \ combine_matrix (op +) A B" .. -instance matrix :: (plus) plus .. - -instance matrix :: ("{plus,times}") times .. +instance matrix :: ("{minus, zero}") minus + minus_matrix_def: "- A \ apply_matrix uminus A" + diff_matrix_def: "A - B \ 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 \ 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 \ B" assume b: "0 \ 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) \ f 0 = (0::'a) \ 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 \ ('a::{zero,one}) matrix" - "one_matrix n == Abs_matrix (% j i. if j = i & j < n then 1 else 0)" +definition + one_matrix :: "nat \ ('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 \ 'a matrix \ '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 \ 'a matrix \ '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 \ 'a matrix \ '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 \ 'a matrix \ 'a matrix)", simplified is_meet_combine_matrix_meet]) apply (simp) done diff -r 51a18dd1ea86 -r ee19cdb07528 src/HOL/MicroJava/BV/JType.thy --- 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) \ acc (subtype G)" apply (unfold Semilat.acc_def lesssub_def) -apply (drule_tac p = "meet ((subcls1 G)^--1) op \" in wfP_subset) +apply (drule_tac p = "inf ((subcls1 G)^--1) op \" 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 \)^--1 = (meet ((subcls1 G)^--1) op \)") +apply (subgoal_tac "(inf (subcls1 G) op \)^--1 = (inf ((subcls1 G)^--1) op \)") prefer 2 apply (simp add: converse_meet) apply simp diff -r 51a18dd1ea86 -r ee19cdb07528 src/HOL/OrderedGroup.thy --- 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 \ pordered_ab_group_add, lorder -instance lordered_ab_group_meet \ lordered_ab_group -proof - show "? j. is_join (j::'a\'a\('a::lordered_ab_group_meet))" by (blast intro: is_join_neg_meet) -qed - instance lordered_ab_group_join \ lordered_ab_group proof - show "? m. is_meet (m::'a\'a\('a::lordered_ab_group_join))" by (blast intro: is_meet_neg_join) + show "? m. is_meet (m::'a\'a\('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 \ lordered_ab_group +proof + show "? j. is_join (j::'a\'a\('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 \ ('a::lordered_ab_group)" - "pprt x == join x 0" - nprt :: "'a \ ('a::lordered_ab_group)" - "nprt x == meet x 0" +definition + nprt :: "'a \ ('a::lordered_ab_group)" where + "nprt x = inf x 0" + +definition + pprt :: "'a \ ('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 \ 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 \ 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 \ 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 \ 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 \ 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 \ a = (0::'a::lordered_ab_group)" +lemma sup_0_imp_0: "sup a (-a) = 0 \ 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 \ 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 \ 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 \ a + a) = (0 \ (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 \ 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 \ -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: "\a\ = (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 \ 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 \ 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 \ 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 \ 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 \ 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 \ 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 \ 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 \ b; -a \ b|] ==> abs a \ (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 \ -a) = (a \ (0::'a::lordered_ab_group))" proof - @@ -914,14 +917,14 @@ lemma abs_triangle_ineq: "abs(a+b) \ 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"; diff -r 51a18dd1ea86 -r ee19cdb07528 src/HOL/Predicate.thy --- 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 \ 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 \ 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 \ sup A B x" by simp -lemma join2I1 [elim?]: "A x y ==> join A B x y" +lemma sup2I1 [elim?]: "A x y \ sup A B x y" by simp -lemma join1I2 [elim?]: "B x ==> join A B x" +lemma join1I2 [elim?]: "B x \ sup A B x" by simp -lemma join2I2 [elim?]: "B x y ==> join A B x y" +lemma sup1I2 [elim?]: "B x y \ 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 \ A x \ 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 \ A x y \ 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 ~=" diff -r 51a18dd1ea86 -r ee19cdb07528 src/HOL/Ring_and_Field.thy --- 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 \ lordered_ab_group .. instance ordered_ring_strict \ 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 diff -r 51a18dd1ea86 -r ee19cdb07528 src/HOL/Tools/inductive_package.ML --- 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 diff -r 51a18dd1ea86 -r ee19cdb07528 src/HOL/Tools/res_atp.ML --- 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*) diff -r 51a18dd1ea86 -r ee19cdb07528 src/HOL/Transitive_Closure.thy --- 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 \ 'a) set => ('a \ '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+