I have now a file with the new class, and all necessary proofs
(both distributivity equalities, bool, set, fun interpretations,
proofs of the old distributivity properties).
I have also the proof that complete linear order is subclass of
the new complete distributive lattice class.
Are there any other subclasses of the current complete distributive
lattice class? This would be something that could cause problems.
Otherwise, the existing complete distrib lattice is subclass
of the one that I implemented, so it should not cause any problems.
All existing results in the current class can be reused without
modification.
My theory works now in Isabelle 2016-1, but I can try it in
Isabelle2017-RC0 also.
I can try to integrate it, but I don't know how to test it
to see if there are any problems with something else.
For reference, I attach the theory file with the new
class of complete distributive lattice.
Best regards,
Viorel
On 8/24/2017 6:40 PM, Florian Haftmann wrote:
As far as I remember, I introduced the complete_distrib_lattice class
after realizing the a complete lattice whose binary operations are
distributive is not necessarily a distributive complete lattice. Hence
the specification of that type class has been contrieved without
consulting literature.
Hence that change should be fine if someone is willing to undertake it
before the RC stabilization phase.
Cheers,
Florian
Am 24.08.2017 um 00:42 schrieb Lawrence Paulson:
Sounds good to me. Can anybody think of an objection?
Larry
On 23 Aug 2017, at 15:17, Viorel Preoteasa <viorel.preote...@aalto.fi
<mailto:viorel.preote...@aalto.fi>> wrote:
Hello,
I am not sure if this is the right place to post this message, but it is
related to the upcoming release as I am prosing adding something
to the Isabelle library.
While working with complete distributive lattices, I noticed that
the Isabelle class complete_distrib_lattice is weaker compared to
what it seems to be regarded as a complete distributive lattice.
As I needed the more general concept, I have developed it,
and if Isabelle community finds it useful to be in the library,
then I could provide the proofs or integrate it myself in the
Complete_Lattice.thy
The only axiom needed for complete distributive lattices is:
Inf_Sup_le: "Inf (Sup ` A) ≤ Sup (Inf ` {f ` A | f . (∀ Y ∈ A . f Y ∈
Y)})"
and from this, the equality and its dual can be proved, as well as
the existing axioms of complete_distrib_lattice and the instantiation
to bool, set and fun.
Best regards,
Viorel
On 2017-08-21 21:24, Makarius wrote:
Dear Isabelle contributors,
we are now definitely heading towards the Isabelle2017 release.
The first official release candidate Isabelle2017-RC1 is anticipated for
2/3-Sep-2017, that is a bit less than 2 weeks from now.
That is also the deadline for any significant additions.
I have already updated the important files NEWS, CONTRIBUTORS, ANNOUNCE
in Isabelle/5c0a3f63057d, but it seems that many potential entries are
still missing.
Please provide entries in NEWS and CONTRIBUTORS for all relevant things
you have done since the last release.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de <mailto:isabelle-...@in.tum.de>
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de <mailto:isabelle-...@in.tum.de>
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
theory Distributive imports Main
begin
section{*Complete Distributive Lattice*}
notation
bot ("\<bottom>") and
top ("\<top>") and
inf (infixl "\<sqinter>" 70)
and sup (infixl "\<squnion>" 65)
context complete_lattice
begin
lemma Sup_Inf_le: "Sup (Inf ` {f ` A | f . (\<forall> Y \<in> A . f Y \<in>
Y)}) \<le> Inf (Sup ` A)"
by (rule SUP_least, clarify, rule INF_greatest, simp add: INF_lower2
Sup_upper)
end
class complete_distributive_lattice = complete_lattice +
assumes Inf_Sup_le: "Inf (Sup ` A) \<le> Sup (Inf ` {f ` A | f . (\<forall> Y
\<in> A . f Y \<in> Y)})"
begin
lemma Inf_Sup: "Inf (Sup ` A) = Sup (Inf ` {f ` A | f . (\<forall> Y \<in> A .
f Y \<in> Y)})"
by (rule antisym, rule Inf_Sup_le, rule Sup_Inf_le)
lemma Sup_Inf: "Sup (Inf ` A) = Inf (Sup ` {f ` A | f . (\<forall> Y \<in> A .
f Y \<in> Y)})"
proof (rule antisym)
show "SUPREMUM A Inf \<le> INFIMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}
Sup"
apply (rule Sup_least, rule INF_greatest)
using Inf_lower2 Sup_upper by auto
next
show "INFIMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} Sup \<le> SUPREMUM A
Inf"
proof (simp add: Inf_Sup, rule_tac 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"
from this have B: "\<And> F . (\<forall> Y \<in> A . F Y \<in> Y)
\<Longrightarrow> \<exists> Z \<in> A . f (F ` A) = F Z"
by auto
show "INFIMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} f \<le> SUPREMUM A
Inf"
proof (cases "\<exists> Z \<in> A . INFIMUM {f ` A |f. \<forall>Y\<in>A. f
Y \<in> Y} f \<le> Inf Z")
case True
from this obtain Z where [simp]: "Z \<in> A" and A: "INFIMUM {f ` A |f.
\<forall>Y\<in>A. f Y \<in> Y} f \<le> Inf Z"
by blast
have B: "... \<le> SUPREMUM A Inf"
by (simp add: SUP_upper)
from A and B show ?thesis
by (drule_tac order_trans, simp_all)
next
case False
from this have X: "\<And> Z . Z \<in> A \<Longrightarrow> \<exists> x . x
\<in> Z \<and> \<not> INFIMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} f \<le>
x"
using Inf_greatest by blast
define F where "F = (\<lambda> Z . SOME x . x \<in> Z \<and> \<not>
INFIMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} f \<le> x)"
have C: "\<And> Y . Y \<in> A \<Longrightarrow> F Y \<in> Y"
using X by (simp add: F_def, rule someI2_ex, auto)
have E: "\<And> Y . Y \<in> A \<Longrightarrow> \<not> INFIMUM {f ` A |f.
\<forall>Y\<in>A. f Y \<in> Y} f \<le> F Y"
using X by (simp add: F_def, rule someI2_ex, auto)
from C and B obtain Z where D: "Z \<in> A " and Y: "f (F ` A) = F Z"
by blast
from E and D have W: "\<not> INFIMUM {f ` A |f. \<forall>Y\<in>A. f Y
\<in> Y} f \<le> F Z"
by simp
from C have "INFIMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} f \<le> f
(F ` A)"
by (rule_tac INF_lower, blast)
from this and W and Y show ?thesis
by simp
qed
qed
qed
lemma dual_complete_distributive_lattice:
"class.complete_distributive_lattice Sup Inf sup (op \<ge>) (op >) inf \<top>
\<bottom>"
apply (rule class.complete_distributive_lattice.intro)
apply (fact dual_complete_lattice)
by (simp add: class.complete_distributive_lattice_axioms_def Sup_Inf)
lemma sup_Inf: "a \<squnion> Inf B = (INF b:B. a \<squnion> b)"
proof (rule antisym)
show "a \<squnion> Inf B \<le> (INF b:B. a \<squnion> b)"
using Inf_lower sup.mono by (rule_tac INF_greatest, fastforce)
next
have "(INF b:B. a \<squnion> b) \<le> INFIMUM {{f {a}, f B} |f. f {a} = a
\<and> f B \<in> B} Sup"
by (rule INF_greatest, auto simp add: INF_lower)
also have "... = a \<squnion> Inf B"
by (cut_tac A = "{{a}, B}" in Sup_Inf, simp)
finally show "(INF b:B. a \<squnion> b) \<le> a \<squnion> Inf B"
by simp
qed
lemma inf_Sup: "a \<sqinter> Sup B = (SUP b:B. a \<sqinter> b)"
proof (rule antisym)
show " (SUP b:B. a \<sqinter> b) \<le> a \<sqinter> Sup B"
by (metis SUP_least Sup_upper inf.orderI inf_idem inf_mono)
next
have "a \<sqinter> Sup B = SUPREMUM {{f {a}, f B} |f. f {a} = a \<and> f B
\<in> B} Inf"
by (cut_tac A = "{{a}, B}" in Inf_Sup, simp)
also have "... \<le> (SUP b:B. a \<sqinter> b)"
by (rule SUP_least, auto simp add: SUP_upper)
finally show "a \<sqinter> Sup B \<le> (SUP b:B. a \<sqinter> b)"
by simp
qed
subclass complete_distrib_lattice
by (standard, rule sup_Inf, rule inf_Sup)
end
instantiation bool :: complete_distributive_lattice
begin
instance proof
fix A :: "(bool set) set"
show "INFIMUM A Sup \<le> SUPREMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}
Inf"
by (clarsimp, fastforce)
qed
end
instantiation "set" :: (type) complete_distributive_lattice
begin
instance proof (standard, clarsimp)
fix A :: "(('a set) set) set"
fix x::'a
define F where "F = (\<lambda> Y . (SOME X . (Y \<in> A \<and> X \<in> Y
\<and> x \<in> X)))"
assume A: "\<forall>xa\<in>A. \<exists>X\<in>xa. x \<in> X"
have B: " (\<forall>xa \<in> F ` A. x \<in> xa)"
by (safe, metis (no_types, lifting) A F_def someI_ex)
have "(\<exists>f. F ` A = f ` A \<and> (\<forall>Y\<in>A. f Y \<in> Y))"
by (rule_tac x = "F" in exI, metis (no_types, lifting) A F_def someI_ex)
from B and this show "\<exists>xa. (\<exists>f. xa = f ` A \<and>
(\<forall>Y\<in>A. f Y \<in> Y)) \<and> (\<forall>xa\<in>xa. x \<in> xa)"
by auto
qed
end
context complete_distributive_lattice
begin
lemma INF_SUP: "(INF y. SUP x. ((P x y)::'a)) = (SUP x. INF y. P (x y) y)"
proof (rule antisym)
show "(SUP x. INF y. P (x y) y) \<le> (INF y. SUP x. P x y)"
by (meson UNIV_I image_eqI INF_lower2 Sup_upper INF_greatest SUP_least)
next
have "(INF y. SUP x. ((P x y))) \<le> Inf (Sup ` {{P x y | x . True} | y .
True })" (is "?A \<le> ?B")
proof (rule_tac INF_greatest, clarsimp)
fix y
have "?A \<le> (SUP x. P x y)"
by (rule INF_lower, simp)
also have "... \<le> Sup {uu. \<exists>x. uu = P x y}"
by (simp add: full_SetCompr_eq)
finally show "?A \<le> Sup {uu. \<exists>x. uu = P x y}"
by simp
qed
also have "... \<le> (SUP x. INF y. P (x y) y)"
proof (subst Inf_Sup, rule_tac SUP_least, clarsimp)
fix f
assume A: "\<forall>Y. (\<exists>y. Y = {uu. \<exists>x. uu = P x y})
\<longrightarrow> f Y \<in> Y"
have "(INF x:{uu. \<exists>y. uu = {uu. \<exists>x. uu = P x y}}. f x)
\<le> (INF y. P ((\<lambda> y. SOME x . f ({P x y | x. True}) = P x y) y) y)"
proof (rule INF_greatest, clarsimp)
fix y
have "(INF x:{uu. \<exists>y. uu = {uu. \<exists>x. uu = P x y}}. f x)
\<le> f {uu. \<exists>x. uu = P x y}"
by (rule_tac INF_lower, blast)
also have "... \<le> P (SOME x. f {uu . \<exists>x. uu = P x y} = P x
y) y"
using A by (rule_tac someI2_ex, auto)
finally show "(INF x:{uu. \<exists>y. uu = {uu. \<exists>x. uu = P x
y}}. f x) \<le> P (SOME x. f {uu . \<exists>x. uu = P x y} = P x y) y"
by simp
qed
also have "... \<le> (SUP x. INF y. P (x y) y)"
by (rule SUP_upper, simp)
finally show "(INF x:{uu. \<exists>y. uu = {uu. \<exists>x. uu = P x y}}.
f x) \<le> (SUP x. INF y. P (x y) y)"
by simp
qed
finally show "(INF y. SUP x. P x y) \<le> (SUP x. INF y. P (x y) y)"
by simp
qed
end
instantiation "fun" :: (type, complete_distributive_lattice)
complete_distributive_lattice
begin
instance proof (standard, simp add: le_fun_def, clarify)
fix A::"('a \<Rightarrow> 'b) set set"
fix x
have "\<And> X . X \<in> A \<Longrightarrow> (INF xa:A. SUP f:xa. f x) \<le>
(SUP f:X. f x)"
by (rule_tac INF_lower, simp)
also have "\<And> X . X \<in> A \<Longrightarrow> (SUP f:X. f x) \<le> Sup {f
x |f. f \<in> X}"
by (metis (mono_tags, lifting) SUP_least Sup_upper mem_Collect_eq)
finally have "(INF xa:A. SUP f:xa. f x) \<le> Inf (Sup ` { {f x | f . f \<in>
X} | X . X \<in> A})"
by (rule_tac INF_greatest, blast)
also have "... \<le> (SUP xa:{f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}. INF
f:xa. f x)"
proof (unfold Inf_Sup, rule SUP_least, clarsimp)
fix f
assume A: "\<forall>Y. (\<exists>X. Y = {f x |f. f \<in> X} \<and> X \<in>
A) \<longrightarrow> f Y \<in> Y"
from this have [simp]: "\<And> xa . xa \<in> A \<Longrightarrow> (SOME g.
g \<in> xa \<and> g x = f {h x |h. h \<in> xa}) x = f {h x |h. h \<in> xa}"
apply (rule_tac Q = "\<lambda> F . F x = f {h x |h. h \<in> xa}" in
someI2_ex)
by (drule_tac x = "{g x | g . g \<in> xa}" in spec, auto)
from A have [simp]: "\<And> Y . Y \<in> A \<Longrightarrow> (SOME g. g
\<in> Y \<and> g x = f {h x |h. h \<in> Y}) \<in> Y"
apply (rule_tac Q = "\<lambda> F . F \<in> Y" in someI2_ex)
by (drule_tac x = "{g x | g . g \<in> Y}" in spec, auto)
have "(INF x:{{f x |f. f \<in> X} |X. X \<in> A}. f x) \<le> (INF
g:((\<lambda> Y . SOME g . g \<in> Y \<and> g x = f({h x | h . h \<in> Y}))
`A). g x)"
by (rule INF_greatest, clarsimp, rule INF_lower, blast)
also have "... \<le> (SUP xa:{f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}. INF
f:xa. f x)"
by (rule SUP_upper, clarsimp, rule_tac x = "((\<lambda> Y . SOME g . g
\<in> Y \<and> g x = f({h x | h . h \<in> Y})))" in exI, simp)
finally show "(INF x:{{f x |f. f \<in> X} |X. X \<in> A}. f x) \<le> (SUP
xa:{f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}. INF f:xa. f x)"
by simp
qed
finally show "(INF xa:A. SUP f:xa. f x) \<le> (SUP xa:{f ` A |f.
\<forall>Y\<in>A. f Y \<in> Y}. INF f:xa. f x)"
by simp
qed
end
context complete_linorder
begin
subclass complete_distributive_lattice
proof (standard, rule ccontr)
fix A
assume "\<not> INFIMUM A Sup \<le> SUPREMUM {f ` A |f. \<forall>Y\<in>A. f Y
\<in> Y} Inf"
from this have C: "INFIMUM A Sup > SUPREMUM {f ` A |f. \<forall>Y\<in>A. f Y
\<in> Y} Inf"
using local.not_le by blast
show "False"
proof (cases "\<exists> z . INFIMUM A Sup > z \<and> z > SUPREMUM {f ` A
|f. \<forall>Y\<in>A. f Y \<in> Y} Inf")
case True
from this obtain z where A: "z < INFIMUM A Sup" and X: "SUPREMUM {f ` A
|f. \<forall>Y\<in>A. f Y \<in> Y} Inf < z"
by blast
from A have "\<And> Y . Y \<in> A \<Longrightarrow> z < Sup Y"
by (meson local.less_INF_D)
from this have B: "\<And> Y . Y \<in> A \<Longrightarrow> \<exists> k
\<in>Y . z < k"
using local.less_Sup_iff by blast
define F where "F = (\<lambda> Y . SOME k . k \<in> Y \<and> z < k)"
have D: "\<And> Y . Y \<in> A \<Longrightarrow> z < F Y"
by (metis (no_types, lifting) F_def B someI_ex)
have E: "\<And> Y . Y \<in> A \<Longrightarrow> F Y \<in> Y"
apply (simp add: F_def)
by (metis (mono_tags, lifting) B someI_ex)
have "z \<le> Inf (F ` A)"
by (simp add: D local.INF_greatest local.order.strict_implies_order)
also have "... \<le> SUPREMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}
Inf"
apply (rule SUP_upper, safe)
using E by blast
finally have "z \<le> SUPREMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}
Inf"
by simp
from X and this show ?thesis
using local.not_less by blast
next
case False
from this have A: "\<And> z . INFIMUM A Sup \<le> z \<or> z \<le>
SUPREMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} Inf"
using local.le_less_linear by blast
from C have "\<And> Y . Y \<in> A \<Longrightarrow> SUPREMUM {f ` A |f.
\<forall>Y\<in>A. f Y \<in> Y} Inf < Sup Y"
by (meson local.less_INF_D)
from this have B: "\<And> Y . Y \<in> A \<Longrightarrow> \<exists> k
\<in>Y . SUPREMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} Inf < k"
using local.less_Sup_iff by blast
define F where "F = (\<lambda> Y . SOME k . k \<in> Y \<and> SUPREMUM {f
` A |f. \<forall>Y\<in>A. f Y \<in> Y} Inf < k)"
have D: "\<And> Y . Y \<in> A \<Longrightarrow> SUPREMUM {f ` A |f.
\<forall>Y\<in>A. f Y \<in> Y} Inf < F Y"
by (metis (no_types, lifting) F_def B someI_ex)
have E: "\<And> Y . Y \<in> A \<Longrightarrow> F Y \<in> Y"
apply (simp add: F_def)
by (metis (mono_tags, lifting) B someI_ex)
have "\<And> Y . Y \<in> A \<Longrightarrow> INFIMUM A Sup \<le> F Y"
using D False local.leI by blast
from this have "INFIMUM A Sup \<le> Inf (F ` A)"
by (simp add: local.INF_greatest)
also have "Inf (F ` A) \<le> SUPREMUM {f ` A |f. \<forall>Y\<in>A. f Y
\<in> Y} Inf"
apply (rule SUP_upper, safe)
using E by blast
finally have "INFIMUM A Sup \<le> SUPREMUM {f ` A |f. \<forall>Y\<in>A. f
Y \<in> Y} Inf"
by simp
from C and this show ?thesis
using local.not_less by blast
qed
qed
end
end
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
