# HG changeset patch # User haftmann # Date 1545207402 0 # Node ID 4880575ec8a17a950b17e85b75a3cbe9021e0968 # Parent c505f251f352e8d4518384a197772c06a94a4d89 tuned proof text diff -r c505f251f352 -r 4880575ec8a1 src/HOL/Hilbert_Choice.thy --- a/src/HOL/Hilbert_Choice.thy Wed Dec 19 08:16:41 2018 +0000 +++ b/src/HOL/Hilbert_Choice.thy Wed Dec 19 08:16:42 2018 +0000 @@ -909,13 +909,14 @@ context complete_distrib_lattice begin -lemma Sup_Inf: "Sup (Inf ` A) = Inf (Sup ` {f ` A | f . (\ Y \ A . f Y \ Y)})" + +lemma Sup_Inf: "\ (Inf ` A) = \ (Sup ` {f ` A |f. \B\A. f B \ B})" proof (rule antisym) - show "\(Inf ` A) \ \(Sup ` {f ` A |f. \Y\A. f Y \ Y})" + show "\ (Inf ` A) \ \ (Sup ` {f ` A |f. \B\A. f B \ B})" apply (rule Sup_least, rule INF_greatest) using Inf_lower2 Sup_upper by auto next - show "\(Sup ` {f ` A |f. \Y\A. f Y \ Y}) \ \(Inf ` A)" + show "\ (Sup ` {f ` A |f. \B\A. f B \ B}) \ \ (Inf ` A)" proof (simp add: Inf_Sup, rule SUP_least, simp, safe) fix f assume "\Y. (\f. Y = f ` A \ (\Y\A. f Y \ Y)) \ f Y \ Y" @@ -976,7 +977,7 @@ using dual_complete_distrib_lattice by (rule complete_distrib_lattice.sup_Inf) -lemma INF_SUP: "(INF y. SUP x. ((P x y)::'a)) = (SUP x. INF y. P (x y) y)" +lemma INF_SUP: "(\y. \x. P x y) = (\f. \x. P (f x) x)" proof (rule antisym) show "(SUP x. INF y. P (x y) y) \ (INF y. SUP x. P x y)" by (rule SUP_least, rule INF_greatest, rule SUP_upper2, simp_all, rule INF_lower2, simp, blast) @@ -1082,11 +1083,11 @@ qed qed -lemma SUP_INF: "(SUP y. INF x. ((P x y)::'a)) = (INF x. SUP y. P (x y) y)" +lemma SUP_INF: "(\y. \x. P x y) = (\x. \y. P (x y) y)" using dual_complete_distrib_lattice by (rule complete_distrib_lattice.INF_SUP) -lemma SUP_INF_set: "(\x\A. \(g ` x)) = (\x\{f ` A |f. \Y\A. f Y \ Y}. \(g ` x))" +lemma SUP_INF_set: "(\x\A. \ (g ` x)) = (\x\{f ` A |f. \Y\A. f Y \ Y}. \ (g ` x))" using dual_complete_distrib_lattice by (rule complete_distrib_lattice.INF_SUP_set) @@ -1102,7 +1103,6 @@ lemma inf_SUP: "a \ (\b\B. f b) = (\b\B. a \ f b)" by (simp add: inf_Sup) - lemma Inf_sup: "\B \ a = (\b\B. b \ a)" by (simp add: sup_Inf sup_commute)