# HG changeset patch # User haftmann # Date 1398516802 -7200 # Node ID 678a52e676b67c85316c6b57ed01ab2b344597f5 # Parent 2b3710a4fa94f0d658c2e254b9cbb6532d94474f more complete classical rules for Inf and Sup, modelled after theiry counterparts on Inter and Union (and INF and SUP) diff -r 2b3710a4fa94 -r 678a52e676b6 src/HOL/Complete_Lattices.thy --- a/src/HOL/Complete_Lattices.thy Sat Apr 26 13:25:46 2014 +0200 +++ b/src/HOL/Complete_Lattices.thy Sat Apr 26 14:53:22 2014 +0200 @@ -758,35 +758,93 @@ subsection {* Complete lattice on unary and binary predicates *} -lemma INF1_I: "(\x. x \ A \ B x b) \ (\x\A. B x) b" - by auto - -lemma INF2_I: "(\x. x \ A \ B x b c) \ (\x\A. B x) b c" +lemma Inf1_I: + "(\P. P \ A \ P a) \ (\A) a" by auto -lemma INF1_D: "(\x\A. B x) b \ a \ A \ B a b" +lemma INF1_I: + "(\x. x \ A \ B x b) \ (\x\A. B x) b" + by simp + +lemma INF2_I: + "(\x. x \ A \ B x b c) \ (\x\A. B x) b c" + by simp + +lemma Inf2_I: + "(\r. r \ A \ r a b) \ (\A) a b" by auto -lemma INF2_D: "(\x\A. B x) b c \ a \ A \ B a b c" +lemma Inf1_D: + "(\A) a \ P \ A \ P a" by auto -lemma INF1_E: "(\x\A. B x) b \ (B a b \ R) \ (a \ A \ R) \ R" +lemma INF1_D: + "(\x\A. B x) b \ a \ A \ B a b" + by simp + +lemma Inf2_D: + "(\A) a b \ r \ A \ r a b" by auto -lemma INF2_E: "(\x\A. B x) b c \ (B a b c \ R) \ (a \ A \ R) \ R" - by auto +lemma INF2_D: + "(\x\A. B x) b c \ a \ A \ B a b c" + by simp + +lemma Inf1_E: + assumes "(\A) a" + obtains "P a" | "P \ A" + using assms by auto -lemma SUP1_I: "a \ A \ B a b \ (\x\A. B x) b" +lemma INF1_E: + assumes "(\x\A. B x) b" + obtains "B a b" | "a \ A" + using assms by auto + +lemma Inf2_E: + assumes "(\A) a b" + obtains "r a b" | "r \ A" + using assms by auto + +lemma INF2_E: + assumes "(\x\A. B x) b c" + obtains "B a b c" | "a \ A" + using assms by auto + +lemma Sup1_I: + "P \ A \ P a \ (\A) a" by auto -lemma SUP2_I: "a \ A \ B a b c \ (\x\A. B x) b c" +lemma SUP1_I: + "a \ A \ B a b \ (\x\A. B x) b" + by auto + +lemma Sup2_I: + "r \ A \ r a b \ (\A) a b" + by auto + +lemma SUP2_I: + "a \ A \ B a b c \ (\x\A. B x) b c" by auto -lemma SUP1_E: "(\x\A. B x) b \ (\x. x \ A \ B x b \ R) \ R" - by auto +lemma Sup1_E: + assumes "(\A) a" + obtains P where "P \ A" and "P a" + using assms by auto + +lemma SUP1_E: + assumes "(\x\A. B x) b" + obtains x where "x \ A" and "B x b" + using assms by auto -lemma SUP2_E: "(\x\A. B x) b c \ (\x. x \ A \ B x b c \ R) \ R" - by auto +lemma Sup2_E: + assumes "(\A) a b" + obtains r where "r \ A" "r a b" + using assms by auto + +lemma SUP2_E: + assumes "(\x\A. B x) b c" + obtains x where "x \ A" "B x b c" + using assms by auto subsection {* Complete lattice on @{typ "_ set"} *} diff -r 2b3710a4fa94 -r 678a52e676b6 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Sat Apr 26 13:25:46 2014 +0200 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Sat Apr 26 14:53:22 2014 +0200 @@ -3291,7 +3291,8 @@ lemma filter_from_subbase_not_bot: "\X \ B. finite X \ Inf X \ bot \ filter_from_subbase B \ bot" - unfolding trivial_limit_def eventually_filter_from_subbase by auto + unfolding trivial_limit_def eventually_filter_from_subbase + bot_bool_def [symmetric] bot_fun_def [symmetric] bot_unique by simp lemma closure_iff_nhds_not_empty: "x \ closure X \ (\A. \S\A. open S \ x \ S \ X \ A \ {})" diff -r 2b3710a4fa94 -r 678a52e676b6 src/HOL/Relation.thy --- a/src/HOL/Relation.thy Sat Apr 26 13:25:46 2014 +0200 +++ b/src/HOL/Relation.thy Sat Apr 26 14:53:22 2014 +0200 @@ -30,15 +30,25 @@ declare sup2E [elim!] declare sup1CI [intro!] declare sup2CI [intro!] +declare Inf1_I [intro!] declare INF1_I [intro!] +declare Inf2_I [intro!] declare INF2_I [intro!] +declare Inf1_D [elim] declare INF1_D [elim] +declare Inf2_D [elim] declare INF2_D [elim] +declare Inf1_E [elim] declare INF1_E [elim] +declare Inf2_E [elim] declare INF2_E [elim] +declare Sup1_I [intro] declare SUP1_I [intro] +declare Sup2_I [intro] declare SUP2_I [intro] +declare Sup1_E [elim!] declare SUP1_E [elim!] +declare Sup2_E [elim!] declare SUP2_E [elim!] subsection {* Fundamental *}