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

Reply via email to