--- a/src/HOL/Hilbert_Choice.thy Wed Dec 19 12:26:38 2018 +0100
+++ b/src/HOL/Hilbert_Choice.thy Wed Dec 19 13:07:02 2018 +0100
@@ -909,13 +909,14 @@
context complete_distrib_lattice
begin
-lemma Sup_Inf: "Sup (Inf ` A) = Inf (Sup ` {f ` A | f . (\<forall> Y \<in> A . f Y \<in> Y)})"
+
+lemma Sup_Inf: "\<Squnion> (Inf ` A) = \<Sqinter> (Sup ` {f ` A |f. \<forall>B\<in>A. f B \<in> B})"
proof (rule antisym)
- show "\<Squnion>(Inf ` A) \<le> \<Sqinter>(Sup ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y})"
+ show "\<Squnion> (Inf ` A) \<le> \<Sqinter> (Sup ` {f ` A |f. \<forall>B\<in>A. f B \<in> B})"
apply (rule Sup_least, rule INF_greatest)
using Inf_lower2 Sup_upper by auto
next
- show "\<Sqinter>(Sup ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}) \<le> \<Squnion>(Inf ` A)"
+ show "\<Sqinter> (Sup ` {f ` A |f. \<forall>B\<in>A. f B \<in> B}) \<le> \<Squnion> (Inf ` A)"
proof (simp add: Inf_Sup, rule SUP_least, simp, safe)
fix f
assume "\<forall>Y. (\<exists>f. Y = f ` A \<and> (\<forall>Y\<in>A. f Y \<in> Y)) \<longrightarrow> f Y \<in> 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: "(\<Sqinter>y. \<Squnion>x. P x y) = (\<Squnion>f. \<Sqinter>x. P (f x) x)"
proof (rule antisym)
show "(SUP x. INF y. P (x y) y) \<le> (INF y. SUP x. P x y)"
by (rule SUP_least, rule INF_greatest, rule SUP_upper2, simp_all, rule INF_lower2, simp, blast)
@@ -1018,30 +1019,33 @@
by simp
qed
-lemma INF_SUP_set: "(\<Sqinter>x\<in>A. \<Squnion>(g ` x)) = (\<Squnion>x\<in>{f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}. \<Sqinter>(g ` x))"
+lemma INF_SUP_set: "(\<Sqinter>B\<in>A. \<Squnion>(g ` B)) = (\<Squnion>B\<in>{f ` A |f. \<forall>C\<in>A. f C \<in> C}. \<Sqinter>(g ` B))"
proof (rule antisym)
- have [simp]: "\<And>f xa. \<forall>Y\<in>A. f Y \<in> Y \<Longrightarrow> xa \<in> A \<Longrightarrow> (\<Sqinter>x\<in>A. g (f x)) \<le> g (f xa)"
- by (rule INF_lower2, blast+)
- have B: "\<And>f xa. \<forall>Y\<in>A. f Y \<in> Y \<Longrightarrow> xa \<in> A \<Longrightarrow> f xa \<in> xa"
- by blast
- have A: "\<And>f xa. \<forall>Y\<in>A. f Y \<in> Y \<Longrightarrow> xa \<in> A \<Longrightarrow> (\<Sqinter>x\<in>A. g (f x)) \<le> \<Squnion>(g ` xa)"
- by (rule SUP_upper2, rule B, simp_all, simp)
- show "(\<Squnion>x\<in>{f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}. \<Sqinter>a\<in>x. g a) \<le> (\<Sqinter>x\<in>A. \<Squnion>a\<in>x. g a)"
- apply (rule SUP_least, simp, safe, rule INF_greatest, simp)
- by (rule A)
+ have "\<Sqinter> ((g \<circ> f) ` A) \<le> \<Squnion> (g ` B)" if "\<And>B. B \<in> A \<Longrightarrow> f B \<in> B" and "B \<in> A"
+ for f and B
+ using that by (auto intro: SUP_upper2 INF_lower2)
+ then show "(\<Squnion>x\<in>{f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}. \<Sqinter>a\<in>x. g a) \<le> (\<Sqinter>x\<in>A. \<Squnion>a\<in>x. g a)"
+ by (auto intro!: SUP_least INF_greatest)
next
show "(\<Sqinter>x\<in>A. \<Squnion>a\<in>x. g a) \<le> (\<Squnion>x\<in>{f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}. \<Sqinter>a\<in>x. g a)"
proof (cases "{} \<in> A")
case True
then show ?thesis
- by (rule INF_lower2, simp_all)
+ by (rule INF_lower2) simp_all
next
case False
- have [simp]: "\<And>x xa xb. xb \<in> A \<Longrightarrow> x xb \<in> xb \<Longrightarrow> (\<Sqinter>xa. if xa \<in> A then if x xa \<in> xa then g (x xa) else \<bottom> else \<top>) \<le> g (x xb)"
+ have *: "\<And>f B. B \<in> A \<Longrightarrow> f B \<in> B \<Longrightarrow>
+ (\<Sqinter>B. if B \<in> A then if f B \<in> B then g (f B) else \<bottom> else \<top>) \<le> g (f B)"
+ by (rule INF_lower2, auto)
+ have **: "\<And>f B. B \<in> A \<Longrightarrow> f B \<notin> B \<Longrightarrow>
+ (\<Sqinter>B. if B \<in> A then if f B \<in> B then g (f B) else \<bottom> else \<top>) \<le> g (SOME x. x \<in> B)"
by (rule INF_lower2, auto)
- have [simp]: " \<And>x xa y. y \<in> A \<Longrightarrow> x y \<notin> y \<Longrightarrow> (\<Sqinter>xa. if xa \<in> A then if x xa \<in> xa then g (x xa) else \<bottom> else \<top>) \<le> g (SOME x. x \<in> y)"
- by (rule INF_lower2, auto)
- have [simp]: "\<And>x. (\<Sqinter>xa. if xa \<in> A then if x xa \<in> xa then g (x xa) else \<bottom> else \<top>) \<le> (\<Squnion>x\<in>{f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}. \<Sqinter>x\<in>x. g x)"
+ have ****: "\<And>f B. B \<in> A \<Longrightarrow>
+ (\<Sqinter>B. if B \<in> A then if f B \<in> B then g (f B) else \<bottom> else \<top>)
+ \<le> (if f B \<in> B then g (f B) else g (SOME x. x \<in> B))"
+ by (rule INF_lower2) auto
+ have ***: "\<And>x. (\<Sqinter>B. if B \<in> A then if x B \<in> B then g (x B) else \<bottom> else \<top>)
+ \<le> (\<Squnion>x\<in>{f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}. \<Sqinter>x\<in>x. g x)"
proof -
fix x
define F where "F = (\<lambda> (y::'b set) . if x y \<in> y then x y else (SOME x . x \<in>y))"
@@ -1051,7 +1055,10 @@
using B by blast
show "(\<Sqinter>xa. if xa \<in> A then if x xa \<in> xa then g (x xa) else \<bottom> else \<top>) \<le> (\<Squnion>x\<in>{f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}. \<Sqinter>x\<in>x. g x)"
using A apply (rule SUP_upper2)
- by (simp add: F_def, rule INF_greatest, auto)
+ apply (simp add: F_def)
+ apply (rule INF_greatest)
+ apply (auto simp add: * **)
+ done
qed
{fix x
@@ -1071,16 +1078,16 @@
also have "... = (\<Squnion>x. \<Sqinter>xa. if xa \<in> A then if x xa \<in> xa then g (x xa) else \<bottom> else \<top>)"
by (simp add: INF_SUP)
also have "... \<le> (\<Squnion>x\<in>{f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}. \<Sqinter>a\<in>x. g a)"
- by (rule SUP_least, simp)
+ by (rule SUP_least, simp add: ***)
finally show ?thesis by simp
qed
qed
-lemma SUP_INF: "(SUP y. INF x. ((P x y)::'a)) = (INF x. SUP y. P (x y) y)"
+lemma SUP_INF: "(\<Squnion>y. \<Sqinter>x. P x y) = (\<Sqinter>x. \<Squnion>y. P (x y) y)"
using dual_complete_distrib_lattice
by (rule complete_distrib_lattice.INF_SUP)
-lemma SUP_INF_set: "(\<Squnion>x\<in>A. \<Sqinter>(g ` x)) = (\<Sqinter>x\<in>{f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}. \<Squnion>(g ` x))"
+lemma SUP_INF_set: "(\<Squnion>x\<in>A. \<Sqinter> (g ` x)) = (\<Sqinter>x\<in>{f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}. \<Squnion> (g ` x))"
using dual_complete_distrib_lattice
by (rule complete_distrib_lattice.INF_SUP_set)
@@ -1096,7 +1103,6 @@
lemma inf_SUP: "a \<sqinter> (\<Squnion>b\<in>B. f b) = (\<Squnion>b\<in>B. a \<sqinter> f b)"
by (simp add: inf_Sup)
-
lemma Inf_sup: "\<Sqinter>B \<squnion> a = (\<Sqinter>b\<in>B. b \<squnion> a)"
by (simp add: sup_Inf sup_commute)