# HG changeset patch # User haftmann # Date 1310327799 -7200 # Node ID fe5e846c0839f323e05996d4e434a4de2fcaba97 # Parent d033a34a490a0902d07e9ec246073d8cffa77903 tuned notation diff -r d033a34a490a -r fe5e846c0839 src/HOL/Complete_Lattice.thy --- a/src/HOL/Complete_Lattice.thy Sun Jul 10 21:39:03 2011 +0200 +++ b/src/HOL/Complete_Lattice.thy Sun Jul 10 21:56:39 2011 +0200 @@ -190,58 +190,58 @@ lemma le_INFI: "(\i. i \ A \ u \ M i) \ u \ (\i\A. M i)" by (auto simp add: INFI_def intro: Inf_greatest) -lemma SUP_le_iff: "(SUP i:A. M i) \ u \ (\i \ A. M i \ u)" +lemma SUP_le_iff: "(\i\A. M i) \ u \ (\i \ A. M i \ u)" unfolding SUPR_def by (auto simp add: Sup_le_iff) -lemma le_INF_iff: "u \ (INF i:A. M i) \ (\i \ A. u \ M i)" +lemma le_INF_iff: "u \ (\i\A. M i) \ (\i \ A. u \ M i)" unfolding INFI_def by (auto simp add: le_Inf_iff) -lemma INF_const[simp]: "A \ {} \ (INF i:A. M) = M" +lemma INF_const[simp]: "A \ {} \ (\i\A. M) = M" by (auto intro: antisym INF_leI le_INFI) -lemma SUP_const[simp]: "A \ {} \ (SUP i:A. M) = M" +lemma SUP_const[simp]: "A \ {} \ (\i\A. M) = M" by (auto intro: antisym SUP_leI le_SUPI) lemma INF_mono: - "(\m. m \ B \ \n\A. f n \ g m) \ (INF n:A. f n) \ (INF n:B. g n)" + "(\m. m \ B \ \n\A. f n \ g m) \ (\n\A. f n) \ (\n\B. g n)" by (force intro!: Inf_mono simp: INFI_def) lemma SUP_mono: - "(\n. n \ A \ \m\B. f n \ g m) \ (SUP n:A. f n) \ (SUP n:B. g n)" + "(\n. n \ A \ \m\B. f n \ g m) \ (\n\A. f n) \ (\n\B. g n)" by (force intro!: Sup_mono simp: SUPR_def) -lemma INF_subset: "A \ B \ INFI B f \ INFI A f" +lemma INF_subset: "A \ B \ INFI B f \ INFI A f" by (intro INF_mono) auto -lemma SUP_subset: "A \ B \ SUPR A f \ SUPR B f" +lemma SUP_subset: "A \ B \ SUPR A f \ SUPR B f" by (intro SUP_mono) auto -lemma INF_commute: "(INF i:A. INF j:B. f i j) = (INF j:B. INF i:A. f i j)" +lemma INF_commute: "(\i\A. \j\B. f i j) = (\j\B. \i\A. f i j)" by (iprover intro: INF_leI le_INFI order_trans antisym) -lemma SUP_commute: "(SUP i:A. SUP j:B. f i j) = (SUP j:B. SUP i:A. f i j)" +lemma SUP_commute: "(\i\A. \j\B. f i j) = (\j\B. \i\A. f i j)" by (iprover intro: SUP_leI le_SUPI order_trans antisym) end lemma Inf_less_iff: fixes a :: "'a\{complete_lattice,linorder}" - shows "Inf S < a \ (\x\S. x < a)" + shows "\S \ a \ (\x\S. x \ a)" unfolding not_le[symmetric] le_Inf_iff by auto lemma less_Sup_iff: fixes a :: "'a\{complete_lattice,linorder}" - shows "a < Sup S \ (\x\S. a < x)" + shows "a \ \S \ (\x\S. a \ x)" unfolding not_le[symmetric] Sup_le_iff by auto lemma INF_less_iff: fixes a :: "'a::{complete_lattice,linorder}" - shows "(INF i:A. f i) < a \ (\x\A. f x < a)" + shows "(\i\A. f i) \ a \ (\x\A. f x \ a)" unfolding INFI_def Inf_less_iff by auto lemma less_SUP_iff: fixes a :: "'a::{complete_lattice,linorder}" - shows "a < (SUP i:A. f i) \ (\x\A. a < f x)" + shows "a \ (\i\A. f i) \ (\x\A. a \ f x)" unfolding SUPR_def less_Sup_iff by auto subsection {* @{typ bool} and @{typ "_ \ _"} as complete lattice *} @@ -265,7 +265,7 @@ proof (rule ext)+ fix A :: "'a set" fix P :: "'a \ bool" - show "(INF x:A. P x) \ (\x \ A. P x)" + show "(\x\A. P x) \ (\x\A. P x)" by (auto simp add: Ball_def INFI_def Inf_bool_def) qed @@ -274,7 +274,7 @@ proof (rule ext)+ fix A :: "'a set" fix P :: "'a \ bool" - show "(SUP x:A. P x) \ (\x \ A. P x)" + show "(\x\A. P x) \ (\x\A. P x)" by (auto simp add: Bex_def SUPR_def Sup_bool_def) qed @@ -354,7 +354,7 @@ lemma (in complete_lattice) Inf_less_eq: assumes "\v. v \ A \ v \ u" and "A \ {}" - shows "\A \ u" + shows "\A \ u" proof - from `A \ {}` obtain v where "v \ A" by blast moreover with assms have "v \ u" by blast diff -r d033a34a490a -r fe5e846c0839 src/HOL/Lattices.thy --- a/src/HOL/Lattices.thy Sun Jul 10 21:39:03 2011 +0200 +++ b/src/HOL/Lattices.thy Sun Jul 10 21:56:39 2011 +0200 @@ -68,7 +68,7 @@ text {* Dual lattice *} lemma dual_semilattice: - "class.semilattice_inf (op \) (op >) sup" + "class.semilattice_inf greater_eq greater sup" by (rule class.semilattice_inf.intro, rule dual_order) (unfold_locales, simp_all add: sup_least) @@ -104,7 +104,7 @@ "x \ y \ x \ y = x" by (auto intro: le_infI1 antisym dest: eq_iff [THEN iffD1]) -lemma inf_mono: "a \ c \ b \ d \ a \ b \ c \ d" +lemma inf_mono: "a \ c \ b \ d \ a \ b \ c \ d" by (fast intro: inf_greatest le_infI1 le_infI2) lemma mono_inf: @@ -141,7 +141,7 @@ "x \ y \ x \ y = y" by (auto intro: le_supI2 antisym dest: eq_iff [THEN iffD1]) -lemma sup_mono: "a \ c \ b \ d \ a \ b \ c \ d" +lemma sup_mono: "a \ c \ b \ d \ a \ b \ c \ d" by (fast intro: sup_least le_supI1 le_supI2) lemma mono_sup: @@ -420,7 +420,7 @@ begin lemma dual_bounded_lattice: - "class.bounded_lattice (op \) (op >) (op \) (op \) \ \" + "class.bounded_lattice greater_eq greater sup inf \ \" by unfold_locales (auto simp add: less_le_not_le) end @@ -432,7 +432,7 @@ begin lemma dual_boolean_algebra: - "class.boolean_algebra (\x y. x \ - y) uminus (op \) (op >) (op \) (op \) \ \" + "class.boolean_algebra (\x y. x \ - y) uminus greater_eq greater sup inf \ \" by (rule class.boolean_algebra.intro, rule dual_bounded_lattice, rule dual_distrib_lattice) (unfold_locales, auto simp add: inf_compl_bot sup_compl_top diff_eq) @@ -506,7 +506,7 @@ lemma compl_sup [simp]: "- (x \ y) = - x \ - y" proof - - interpret boolean_algebra "\x y. x \ - y" uminus "op \" "op >" "op \" "op \" \ \ + interpret boolean_algebra "\x y. x \ - y" uminus greater_eq greater sup inf \ \ by (rule dual_boolean_algebra) then show ?thesis by simp qed @@ -523,7 +523,7 @@ qed lemma compl_le_compl_iff: (* TODO: declare [simp] ? *) - "- x \ - y \ y \ x" + "- x \ - y \ y \ x" by (auto dest: compl_mono) end