[isabelle-dev] Towards the Isabelle2017 release
Viorel Preoteasa
viorel.preoteasa at aalto.fi
Thu Aug 24 20:54:46 CEST 2017
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.preoteasa at aalto.fi
>>> <mailto:viorel.preoteasa at 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-dev at in.tum.de <mailto:isabelle-dev at in.tum.de>
>>>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>>>
>>> _______________________________________________
>>> isabelle-dev mailing list
>>> isabelle-dev at in.tum.de <mailto:isabelle-dev at in.tum.de>
>>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>>
>>
>>
>> _______________________________________________
>> isabelle-dev mailing list
>> isabelle-dev at in.tum.de
>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>>
>
-------------- next part --------------
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
More information about the isabelle-dev
mailing list