[isabelle-dev] Towards the Isabelle2017 release

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