equal
deleted
inserted
replaced
59 by simp |
59 by simp |
60 |
60 |
61 lemma INF_cong: "A = B \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> C x = D x) \<Longrightarrow> \<Sqinter>(C ` A) = \<Sqinter>(D ` B)" |
61 lemma INF_cong: "A = B \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> C x = D x) \<Longrightarrow> \<Sqinter>(C ` A) = \<Sqinter>(D ` B)" |
62 by (simp add: image_def) |
62 by (simp add: image_def) |
63 |
63 |
64 lemma INF_cong_simp [cong]: |
64 lemma INF_cong_simp: |
65 "A = B \<Longrightarrow> (\<And>x. x \<in> B =simp=> C x = D x) \<Longrightarrow> \<Sqinter>(C ` A) = \<Sqinter>(D ` B)" |
65 "A = B \<Longrightarrow> (\<And>x. x \<in> B =simp=> C x = D x) \<Longrightarrow> \<Sqinter>(C ` A) = \<Sqinter>(D ` B)" |
66 unfolding simp_implies_def by (fact INF_cong) |
66 unfolding simp_implies_def by (fact INF_cong) |
67 |
67 |
68 end |
68 end |
69 |
69 |
80 by(fact Inf.INF_id_eq) |
80 by(fact Inf.INF_id_eq) |
81 |
81 |
82 lemma SUP_cong: "A = B \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> C x = D x) \<Longrightarrow> \<Squnion>(C ` A) = \<Squnion>(D ` B)" |
82 lemma SUP_cong: "A = B \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> C x = D x) \<Longrightarrow> \<Squnion>(C ` A) = \<Squnion>(D ` B)" |
83 by (fact Inf.INF_cong) |
83 by (fact Inf.INF_cong) |
84 |
84 |
85 lemma SUP_cong_simp [cong]: |
85 lemma SUP_cong_simp: |
86 "A = B \<Longrightarrow> (\<And>x. x \<in> B =simp=> C x = D x) \<Longrightarrow> \<Squnion>(C ` A) = \<Squnion>(D ` B)" |
86 "A = B \<Longrightarrow> (\<And>x. x \<in> B =simp=> C x = D x) \<Longrightarrow> \<Squnion>(C ` A) = \<Squnion>(D ` B)" |
87 by (fact Inf.INF_cong_simp) |
87 by (fact Inf.INF_cong_simp) |
88 |
88 |
89 end |
89 end |
90 |
90 |
434 |
434 |
435 lemma SUP_eq_const: "I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> f i = x) \<Longrightarrow> \<Squnion>(f ` I) = x" |
435 lemma SUP_eq_const: "I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> f i = x) \<Longrightarrow> \<Squnion>(f ` I) = x" |
436 by (auto intro: SUP_eqI) |
436 by (auto intro: SUP_eqI) |
437 |
437 |
438 lemma INF_eq_iff: "I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> f i \<le> c) \<Longrightarrow> \<Sqinter>(f ` I) = c \<longleftrightarrow> (\<forall>i\<in>I. f i = c)" |
438 lemma INF_eq_iff: "I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> f i \<le> c) \<Longrightarrow> \<Sqinter>(f ` I) = c \<longleftrightarrow> (\<forall>i\<in>I. f i = c)" |
439 using INF_eq_const [of I f c] INF_lower [of _ I f] |
439 by (auto intro: INF_eq_const INF_lower antisym) |
440 by (auto intro: antisym cong del: INF_cong_simp) |
|
441 |
440 |
442 lemma SUP_eq_iff: "I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> c \<le> f i) \<Longrightarrow> \<Squnion>(f ` I) = c \<longleftrightarrow> (\<forall>i\<in>I. f i = c)" |
441 lemma SUP_eq_iff: "I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> c \<le> f i) \<Longrightarrow> \<Squnion>(f ` I) = c \<longleftrightarrow> (\<forall>i\<in>I. f i = c)" |
443 using SUP_eq_const [of I f c] SUP_upper [of _ I f] |
442 by (auto intro: SUP_eq_const SUP_upper antisym) |
444 by (auto intro: antisym cong del: SUP_cong_simp) |
|
445 |
443 |
446 end |
444 end |
447 |
445 |
448 context complete_lattice |
446 context complete_lattice |
449 begin |
447 begin |