[isabelle-dev] Proposing extensions to the Isabelle library?
Alessandro Coglio
coglio at kestrel.edu
Thu Dec 13 18:01:42 CET 2012
Hi Tobias, thank you for your answer.
My LibExt also contained some type classes and theorems for finite
lattices and finite linear orders, including a proof that finite
lattices are complete (using the approach with type classes suggested by
Florian Haftmann on isabelle-users some time ago). Do you have any
comment on those?
Sorry for missing Library/Product_Lattice. I suppose it makes sense that
it is not part of Main, since one may want pair-wise or lexicographic
ordering, depending on the application.
I've attached a new LibExt without what's already in Product_Lattice.
I was wondering why Library/Product_Lattice proves prod :: (ord, ord)
ord but not prod :: (inf, inf) inf (and same for sup, Inf, and Sup).
On a semi-related topic, I was wondering why the Isabelle library has
syntactic type classes for many (most?) operators but not for bot and top.
Thanks!
On 12/13/12 4:24 AM, Tobias Nipkow wrote:
> Am 13/12/2012 03:21, schrieb Alessandro Coglio:
>> Hello,
>>
>> Is there a process to propose extensions to the Isabelle library? Is
>> isabelle-dev the right place, as opposed to isabelle-users?
>>
>> As part of an Isabelle project, I've developed some type classes and theorems
>> for orders and lattices (see attached file) that could be of general use.
> I looked at your theory, which deals with orderings on product types, and
> noticed a few things:
>
> 1. We already have Library/Product_ord, but it defines a *lexicographic*
> ordering. Any objections if we rename it to Lex_Product_ord?
>
> 2. We also have a Library/Product_lattice. It covers much the same ground as
> your LibExt. I would not want to add another similar theory, but if you have any
> additional results not contained in Product_lattice already, please filter them
> out and I can add them.
>
> Thanks
> Tobias
>
>> Thank you in advance!
>>
>>
>>
>> _______________________________________________
>> isabelle-dev mailing list
>> 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 LibExt
imports "~~/src/HOL/Library/Product_Lattice"
begin
section {* Library Extensions *}
subsection {* Notations *}
text {* Standard mathematical notations for various operators are introduced. *}
notation
bot ("\<bottom>") and
top ("\<top>") and
inf (infixl "\<sqinter>" 70) and
sup (infixl "\<squnion>" 65) and
Inf ("\<Sqinter>_" [900] 900) and
Sup ("\<Squnion>_" [900] 900)
subsection {* Complete lattices *}
text {* Alternative formulations are introduced for
set infima and suprema over a product of two complete lattices. *}
lemma Inf_prod_alt_def:
"\<Sqinter>(A::('a::complete_lattice \<times> 'b::complete_lattice) set) =
(\<Sqinter> (fst ` A), \<Sqinter> (snd ` A))"
by (auto simp: Inf_prod_def INF_def)
lemma Sup_prod_alt_def:
"\<Squnion>(A::('a::complete_lattice \<times> 'b::complete_lattice) set) =
(\<Squnion> (fst ` A), \<Squnion> (snd ` A))"
by (auto simp: Sup_prod_def SUP_def)
lemma INFI_prod_alt_def:
"INFI A (f::'c \<Rightarrow> 'a::complete_lattice \<times> 'b::complete_lattice) =
(INFI A (fst o f), INFI A (snd o f))"
by (auto simp: INF_def Inf_prod_def image_compose)
lemma SUPR_prod_alt_def:
"SUPR A (f::'c \<Rightarrow> 'a::complete_lattice \<times> 'b::complete_lattice) =
(SUPR A (fst o f), SUPR A (snd o f))"
by (auto simp: SUP_def Sup_prod_def image_compose)
lemma INF_prod_alt_def:
"(INF x:A. ((f x)::'a::complete_lattice \<times> 'b::complete_lattice)) =
(INF x:A. fst (f x), INF x:A. snd (f x))"
by (metis fst_INF snd_INF surjective_pairing)
lemma SUP_prod_alt_def:
"(SUP x:A. ((f x)::'a::complete_lattice \<times> 'b::complete_lattice)) =
(SUP x:A. fst (f x), SUP x:A. snd (f x))"
by (metis fst_SUP snd_SUP surjective_pairing)
subsection {* Complete Distributive Lattices *}
text {* The product of two complete lattices
whose @{const inf} and @{const sup} operators
distribute over @{const Sup} and @{const Inf},
is a complete lattice
whose @{const inf} and @{const sup} operators
distribute over @{const Sup} and @{const Inf}. *}
instance prod ::
(complete_distrib_lattice, complete_distrib_lattice) complete_distrib_lattice
proof
fix x::"'a::complete_distrib_lattice \<times> 'b::complete_distrib_lattice" and A
show "x \<squnion> \<Sqinter>A = (INF y:A. x \<squnion> y)"
by (auto simp: sup_prod_def Inf_prod_def INF_prod_alt_def sup_Inf sup_INF)
next
fix x::"'a::complete_distrib_lattice \<times> 'b::complete_distrib_lattice" and A
show "x \<sqinter> \<Squnion>A = (SUP y:A. x \<sqinter> y)"
by (auto simp: inf_prod_def Sup_prod_def SUP_prod_alt_def inf_Sup inf_SUP)
qed
subsection {* Finite Lattices *}
text {* A type class for finite lattices is introduced. *}
class finite_lattice = finite + lattice
text {* A non-empty finite lattice is a complete lattice.
Since types are never empty in Isabelle/HOL,
a type of class @{class finite_lattice}
should also have class @{class complete_lattice}.
Since in Isabelle/HOL
a subclass must have all the parameters of its superclasses,
class @{class finite_lattice} cannot be a subclass of @{class complete_lattice}.
So class @{class finite_lattice} is extended with
the operators @{const bot}, @{const top}, @{const Inf}, and @{const Sup},
along with assumptions that define these operators
in terms of the ones of class @{class finite_lattice}.
The resulting class is a subclass of @{class complete_lattice}.
Classes @{class bot} and @{class top} already include assumptions that suffice
to define the operators @{const bot} and @{const top} (as proved below),
and so no explicit assumptions on these two operators are needed
in the following type class.%
\footnote{The Isabelle/HOL library does not provide
syntactic classes for the operators @{const bot} and @{const top}.} *}
class finite_lattice_complete = finite_lattice + bot + top + Inf + Sup +
assumes Inf_def: "\<Sqinter>A = Finite_Set.fold (op \<sqinter>) \<top> A"
assumes Sup_def: "\<Squnion>A = Finite_Set.fold (op \<squnion>) \<bottom> A"
-- "No explicit assumptions on @{const bot} or @{const top}."
instance finite_lattice_complete \<subseteq> bounded_lattice
proof qed
-- "This subclass relation eases the proof of the next two lemmas."
lemma finite_lattice_complete_bot_def:
"(\<bottom>::'a::finite_lattice_complete) = \<Sqinter>\<^bsub>fin\<^esub>UNIV"
by (metis finite_UNIV sup_Inf_absorb sup_bot_left iso_tuple_UNIV_I)
-- "Derived definition of @{const bot}."
lemma finite_lattice_complete_top_def:
"(\<top>::'a::finite_lattice_complete) = \<Squnion>\<^bsub>fin\<^esub>UNIV"
by (metis finite_UNIV inf_Sup_absorb inf_top_left iso_tuple_UNIV_I)
-- "Derived definition of @{const top}."
text {* The definitional assumptions
on the operators @{const Inf} and @{const Sup}
of class @{class finite_lattice_complete}
ensure that they yield infimum and supremum,
as required for a complete lattice. *}
lemma finite_lattice_complete_Inf_lower:
"(x::'a::finite_lattice_complete) \<in> A \<Longrightarrow> \<Sqinter>A \<le> x"
unfolding Inf_def
by (metis finite_code le_inf_iff fold_inf_le_inf)
lemma finite_lattice_complete_Inf_greatest:
"\<forall>x::'a::finite_lattice_complete \<in> A. z \<le> x \<Longrightarrow> z \<le> \<Sqinter>A"
unfolding Inf_def
by (metis finite_code inf_le_fold_inf inf_top_right)
lemma finite_lattice_complete_Sup_upper:
"(x::'a::finite_lattice_complete) \<in> A \<Longrightarrow> \<Squnion>A \<ge> x"
unfolding Sup_def
by (metis finite_code le_sup_iff sup_le_fold_sup)
lemma finite_lattice_complete_Sup_least:
"\<forall>x::'a::finite_lattice_complete \<in> A. z \<ge> x \<Longrightarrow> z \<ge> \<Squnion>A"
unfolding Sup_def
by (metis finite_code fold_sup_le_sup sup_bot_right)
instance finite_lattice_complete \<subseteq> complete_lattice
proof
qed (auto simp:
finite_lattice_complete_Inf_lower
finite_lattice_complete_Inf_greatest
finite_lattice_complete_Sup_upper
finite_lattice_complete_Sup_least)
text {* The product of two finite lattices is a finite lattice. *}
instance prod :: (finite_lattice, finite_lattice) finite_lattice
proof qed
lemma finite_Inf_prod:
"\<Sqinter>(A::('a::finite_lattice_complete \<times> 'b::finite_lattice_complete) set) =
Finite_Set.fold (op \<sqinter>) \<top> A"
by (metis Inf_fold_inf finite_code)
lemma finite_Sup_prod:
"\<Squnion>(A::('a::finite_lattice_complete \<times> 'b::finite_lattice_complete) set) =
Finite_Set.fold (op \<squnion>) \<bottom> A"
by (metis Sup_fold_sup finite_code)
instance prod ::
(finite_lattice_complete, finite_lattice_complete) finite_lattice_complete
proof qed (auto simp: finite_Inf_prod finite_Sup_prod)
text {* Functions with a finite domain and with a finite lattice as codomain
form a finite lattice. *}
instance "fun" :: (finite, finite_lattice) finite_lattice
proof qed
lemma finite_Inf_fun:
"\<Sqinter>(A::('a::finite \<Rightarrow> 'b::finite_lattice_complete) set) =
Finite_Set.fold (op \<sqinter>) \<top> A"
by (metis Inf_fold_inf finite_code)
lemma finite_Sup_fun:
"\<Squnion>(A::('a::finite \<Rightarrow> 'b::finite_lattice_complete) set) =
Finite_Set.fold (op \<squnion>) \<bottom> A"
by (metis Sup_fold_sup finite_code)
instance "fun" :: (finite, finite_lattice_complete) finite_lattice_complete
proof qed (auto simp: finite_Inf_fun finite_Sup_fun)
subsection {* Finite Distributive Lattices *}
text {* A type class for finite distributive lattices is introduced. *}
class finite_distrib_lattice = finite + distrib_lattice
text {* A finite distributive lattice is a complete lattice
whose @{const inf} and @{const sup} operators
distribute over @{const Sup} and @{const Inf}. *}
class finite_distrib_lattice_complete =
finite_distrib_lattice + finite_lattice_complete
lemma finite_distrib_lattice_complete_sup_Inf:
"(x::'a::finite_distrib_lattice_complete) \<squnion> \<Sqinter>A = (INF y:A. x \<squnion> y)"
apply (rule finite_induct)
apply (metis finite_code)
apply (metis INF_empty Inf_empty sup_top_right)
apply (metis INF_insert Inf_insert sup_inf_distrib1)
done
lemma finite_distrib_lattice_complete_inf_Sup:
"(x::'a::finite_distrib_lattice_complete) \<sqinter> \<Squnion>A = (SUP y:A. x \<sqinter> y)"
apply (rule finite_induct)
apply (metis finite_code)
apply (metis SUP_empty Sup_empty inf_bot_right)
apply (metis SUP_insert Sup_insert inf_sup_distrib1)
done
instance finite_distrib_lattice_complete \<subseteq> complete_distrib_lattice
proof
qed (auto simp:
finite_distrib_lattice_complete_sup_Inf
finite_distrib_lattice_complete_inf_Sup)
text {* The product of two finite distributive lattices
is a finite distributive lattice. *}
instance prod ::
(finite_distrib_lattice, finite_distrib_lattice) finite_distrib_lattice
proof qed
instance prod ::
(finite_distrib_lattice_complete, finite_distrib_lattice_complete)
finite_distrib_lattice_complete
proof qed
text {* Functions with a finite domain
and with a finite distributive lattice as codomain
form a finite distributive lattice. *}
instance "fun" :: (finite, finite_distrib_lattice) finite_distrib_lattice
proof qed
instance "fun" ::
(finite, finite_distrib_lattice_complete) finite_distrib_lattice_complete
proof qed
subsection {* Linear Orders *}
text {* A linear order is a distributive lattice.
Since in Isabelle/HOL
a subclass must have all the parameters of its superclasses,
class @{class linorder} cannot be a subclass of @{class distrib_lattice}.
So class @{class linorder} is extended with
the operators @{const inf} and @{const sup},
along with assumptions that define these operators
in terms of the ones of class @{class linorder}.
The resulting class is a subclass of @{class distrib_lattice}. *}
class linorder_lattice = linorder + inf + sup +
assumes inf_def: "x \<sqinter> y = (if x \<le> y then x else y)"
assumes sup_def: "x \<squnion> y = (if x \<ge> y then x else y)"
text {* The definitional assumptions
on the operators @{const inf} and @{const sup}
of class @{class linorder_lattice}
ensure that they yield infimum and supremum,
and that they distribute over each other,
as required for a distributive lattice. *}
lemma linorder_lattice_inf_le1:
"(x::'a::linorder_lattice) \<sqinter> y \<le> x"
unfolding inf_def
by (metis (full_types) linorder_linear)
lemma linorder_lattice_inf_le2:
"(x::'a::linorder_lattice) \<sqinter> y \<le> y"
unfolding inf_def
by (metis (full_types) linorder_linear)
lemma linorder_lattice_inf_greatest:
"(x::'a::linorder_lattice) \<le> y \<Longrightarrow> x \<le> z \<Longrightarrow> x \<le> y \<sqinter> z"
unfolding inf_def
by (metis (full_types))
lemma linorder_lattice_sup_ge1:
"(x::'a::linorder_lattice) \<squnion> y \<ge> x"
unfolding sup_def
by (metis (full_types) linorder_linear)
lemma linorder_lattice_sup_ge2:
"(x::'a::linorder_lattice) \<squnion> y \<ge> y"
unfolding sup_def
by (metis (full_types) linorder_linear)
lemma linorder_lattice_sup_least:
"(x::'a::linorder_lattice) \<ge> y \<Longrightarrow> x \<ge> z \<Longrightarrow> x \<ge> y \<squnion> z"
unfolding sup_def
by (metis (full_types))
lemma linorder_lattice_sup_inf_distrib1:
"(x::'a::linorder_lattice) \<squnion> y \<sqinter> z = (x \<squnion> y) \<sqinter> (x \<squnion> z)"
by (auto simp: inf_def sup_def)
instance linorder_lattice \<subseteq> distrib_lattice
proof
qed (auto simp:
linorder_lattice_inf_le1
linorder_lattice_inf_le2
linorder_lattice_inf_greatest
linorder_lattice_sup_ge1
linorder_lattice_sup_ge2
linorder_lattice_sup_least
linorder_lattice_sup_inf_distrib1)
subsection {* Finite Linear Orders *}
text {* A type class for finite linear orders is introduced. *}
class finite_linorder = finite + linorder
text {* A finite linear order is a finite distributive lattice. *}
class finite_linorder_lattice = finite_linorder + linorder_lattice
instance finite_linorder_lattice \<subseteq> finite_distrib_lattice
proof qed
text {* A (non-empty) finite linear order is a complete linear order. *}
class finite_linorder_complete =
finite_linorder_lattice + finite_lattice_complete
instance finite_linorder_complete \<subseteq> complete_linorder
proof qed
text {* A (non-empty) finite linear order is a complete lattice
whose @{const inf} and @{const sup} operators
distribute over @{const Sup} and @{const Inf}. *}
instance finite_linorder_complete \<subseteq> finite_distrib_lattice_complete
proof qed
instance finite_linorder_complete \<subseteq> complete_distrib_lattice
proof qed
end
-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 3735 bytes
Desc: S/MIME Cryptographic Signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20121213/9804eb68/attachment.bin>
More information about the isabelle-dev
mailing list