[isabelle-dev] Proposing extensions to the Isabelle library?

[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.

Thank you in advance!

-------------- next part --------------
theory LibExt
imports Main
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 {* Orders *}

text {* Given two ordered types,
their product type can be ordered component-wise. *}

definition leq_leq :: "'a::ord \<times> 'b::ord \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool"
where "leq_leq x y \<equiv> fst x \<le> fst y \<and> snd x \<le> snd y"

instantiation prod :: (ord, ord) ord
begin
definition "less_eq_prod \<equiv> leq_leq"
definition "less_prod x y \<equiv> leq_leq x y \<and> \<not> leq_leq y x"
instance
proof qed
end


subsection {* Preorders *}

text {* The product of two preorders is a preorder. *}

lemma leq_leq_refl: "(x::'a::preorder \<times> 'b::preorder) \<le> x"
by (metis leq_leq_def less_eq_prod_def order_refl)

lemma leq_leq_trans: "(x::'a::preorder \<times> 'b::preorder) \<le> y \<Longrightarrow> y \<le> z \<Longrightarrow> x \<le> z"
by (metis (full_types) leq_leq_def less_eq_prod_def order_trans)

instance prod :: (preorder, preorder) preorder
apply (intro_classes)
apply (metis less_prod_def less_eq_prod_def)
apply (metis leq_leq_refl)
apply (metis leq_leq_trans)
done


subsection {* Partial Orders *}

text {* The product of two partial orders is a partial order. *}

lemma leq_leq_antisym: "(x::'a::order \<times> 'b::order) \<le> y \<Longrightarrow> x \<ge> y \<Longrightarrow> x = y"
by (metis leq_leq_def less_eq_prod_def order_eq_iff prod_eqI)

instance prod :: (order, order) order
proof qed (metis leq_leq_antisym)


subsection {* Lattices *}

text {* Given two types with infimum or supremum,
the infimum or supremum for their product can be defined component-wise. *}

definition inf_inf :: "'a::inf \<times> 'b::inf \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'a \<times> 'b"
where "inf_inf x y \<equiv> (fst x \<sqinter> fst y, snd x \<sqinter> snd y)"

definition sup_sup :: "'a::sup \<times> 'b::sup \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'a \<times> 'b"
where "sup_sup x y \<equiv> (fst x \<squnion> fst y, snd x \<squnion> snd y)"

instantiation prod :: (inf, inf) inf
begin
definition "inf_prod \<equiv> inf_inf"
instance
proof qed
end

instantiation prod :: (sup, sup) sup
begin
definition "sup_prod \<equiv> sup_sup"
instance
proof qed
end

text {* The product of two semilattices is a semilattice. *}

lemma inf_inf_le1: "(x::'a::semilattice_inf \<times> 'b::semilattice_inf) \<sqinter> y \<le> x"
unfolding inf_prod_def inf_inf_def
using inf_le1
by (metis Pair_eq leq_leq_def less_eq_prod_def surjective_pairing)

lemma inf_inf_le2: "(x::'a::semilattice_inf \<times> 'b::semilattice_inf) \<sqinter> y \<le> y"
unfolding inf_prod_def inf_inf_def
using inf_le2
by (metis Pair_eq leq_leq_def less_eq_prod_def surjective_pairing)

lemma inf_inf_greatest:
"(x::'a::semilattice_inf \<times> 'b::semilattice_inf) \<le> y \<Longrightarrow> x \<le> z \<Longrightarrow> x \<le> y \<sqinter> z"
unfolding inf_prod_def inf_inf_def less_eq_prod_def leq_leq_def
by (metis fst_eqD le_inf_iff snd_eqD)

instance prod :: (semilattice_inf, semilattice_inf) semilattice_inf
proof qed (auto simp: inf_inf_le1 inf_inf_le2 inf_inf_greatest)

lemma sup_sup_ge1: "(x::'a::semilattice_sup \<times> 'b::semilattice_sup) \<squnion> y \<ge> x"
unfolding sup_prod_def sup_sup_def
using sup_ge1
by (metis Pair_eq leq_leq_def less_eq_prod_def surjective_pairing)

lemma sup_sup_ge2: "(x::'a::semilattice_sup \<times> 'b::semilattice_sup) \<squnion> y \<ge> y"
unfolding sup_prod_def sup_sup_def
using sup_ge2
by (metis Pair_eq leq_leq_def less_eq_prod_def surjective_pairing)

lemma sup_sup_least:
"(x::'a::semilattice_sup \<times> 'b::semilattice_sup) \<ge> y \<Longrightarrow> x \<ge> z \<Longrightarrow> x \<ge> y \<squnion> z"
unfolding sup_prod_def sup_sup_def less_eq_prod_def leq_leq_def
by (metis fst_eqD le_sup_iff snd_eqD)

instance prod :: (semilattice_sup, semilattice_sup) semilattice_sup
proof qed (auto simp: sup_sup_ge1 sup_sup_ge2 sup_sup_least)

text {* The product of two lattices is a lattice. *}

instance prod :: (lattice, lattice) lattice
proof qed


subsection {* Distributive Lattices *}

text {* The product of two distributive lattices is a distributive lattice. *}

lemma sup_sup_inf_inf_distrib1:
"(x::'a::distrib_lattice \<times> 'b::distrib_lattice) \<squnion> (y \<sqinter> z) = (x \<squnion> y) \<sqinter> (x \<squnion> z)"
unfolding inf_prod_def inf_inf_def sup_prod_def sup_sup_def
by (metis fst_eqD snd_eqD sup_inf_distrib1)

instance prod :: (distrib_lattice, distrib_lattice) distrib_lattice
proof qed (metis sup_sup_inf_inf_distrib1)


subsection {* Bounded Lattices *}

text {* Given two types with bottom or top,
the bottom or top of their product is defined component-wise. *}

definition bot_bot :: "'a::bot \<times> 'b::bot"
where "bot_bot \<equiv> (\<bottom>, \<bottom>)"

definition top_top :: "'a::top \<times> 'b::top"
where "top_top \<equiv> (\<top>, \<top>)"

instantiation prod :: (bot, bot) bot
begin
definition "bot_prod \<equiv> bot_bot"
instance
proof qed (auto simp: bot_prod_def bot_bot_def leq_leq_def less_eq_prod_def)
end

instantiation prod :: (top, top) top
begin
definition "top_prod \<equiv> top_top"
instance
proof qed (auto simp: top_prod_def top_top_def leq_leq_def less_eq_prod_def)
end

text {* The product of two bounded lattices is a bounded lattice. *}

instance prod :: (bounded_lattice, bounded_lattice) bounded_lattice
proof qed


subsection {* Complete Lattices *}

text {* Given two types with set infimum or supremum,
the set infimum or supremum for their product can be defined component-wise. *}

definition Inf_Inf :: "('a::Inf \<times> 'b::Inf) set \<Rightarrow> 'a \<times> 'b"
where "Inf_Inf A \<equiv> (\<Sqinter> (fst ` A), \<Sqinter> (snd ` A))"

definition Sup_Sup :: "('a::Sup \<times> 'b::Sup) set \<Rightarrow> 'a \<times> 'b"
where "Sup_Sup A \<equiv> (\<Squnion> (fst ` A), \<Squnion> (snd ` A))"

instantiation prod :: (Inf, Inf) Inf
begin
definition "Inf_prod \<equiv> Inf_Inf"
instance
proof qed
end

instantiation prod :: (Sup, Sup) Sup
begin
definition "Sup_prod \<equiv> Sup_Sup"
instance
proof qed
end

text {* The product of two complete lattices is a complete lattice. *}

lemma Inf_Inf_lower:
"(x::'a::complete_lattice \<times> 'b::complete_lattice) \<in> A \<Longrightarrow> \<Sqinter>A \<le> x"
unfolding Inf_prod_def Inf_Inf_def
by (metis Inf_lower fst_conv imageI leq_leq_def less_eq_prod_def snd_conv)

lemma Inf_Inf_greatest:
"\<forall>x::'a::complete_lattice \<times> 'b::complete_lattice \<in> A. z \<le> x \<Longrightarrow> z \<le> \<Sqinter>A"
unfolding Inf_prod_def Inf_Inf_def less_eq_prod_def leq_leq_def
using Inf_greatest [of "fst ` A" "fst z"] Inf_greatest [of "snd ` A" "snd z"]
by (metis (hide_lams, no_types) fst_eqD image_iff snd_eqD)

lemma Sup_Sup_upper:
"(x::'a::complete_lattice \<times> 'b::complete_lattice) \<in> A \<Longrightarrow> \<Squnion>A \<ge> x"
unfolding Sup_prod_def Sup_Sup_def
by (metis Sup_upper fst_conv imageI leq_leq_def less_eq_prod_def snd_conv)

lemma Sup_Sup_least:
"\<forall>x::'a::complete_lattice \<times> 'b::complete_lattice \<in> A. z \<ge> x \<Longrightarrow> z \<ge> \<Squnion>A"
unfolding Sup_prod_def Sup_Sup_def less_eq_prod_def leq_leq_def
using Sup_least [of "fst ` A" "fst z"] Sup_least [of "snd ` A" "snd z"]
by (metis (hide_lams, no_types) fst_eqD image_iff snd_eqD)

instance prod :: (complete_lattice, complete_lattice) complete_lattice
proof
qed (auto simp: Inf_Inf_lower Inf_Inf_greatest Sup_Sup_upper Sup_Sup_least)

text {* The infimum or supremum of the image of a set,
under a function whose codomain is a product of two complete lattices,
is defined component-wise. *}

lemma INFI_INFI_alt_def:
"INFI A (f::'c \<Rightarrow> 'a::complete_lattice \<times> 'b::complete_lattice) =
 (INFI A (fst o f), INFI A (snd o f))"
unfolding INF_def
by (metis (hide_lams, no_types) Inf_Inf_def Inf_prod_def image_compose)

lemma INF_INF_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 (mono_tags) INFI_INFI_alt_def INF_cong o_apply)

lemma SUPR_SUPR_alt_def:
"SUPR A (f::'c \<Rightarrow> 'a::complete_lattice \<times> 'b::complete_lattice) =
 (SUPR A (fst o f), SUPR A (snd o f))"
unfolding SUP_def
by (metis (hide_lams, no_types) Sup_Sup_def Sup_prod_def image_compose)

lemma SUP_SUP_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 (mono_tags) SUPR_SUPR_alt_def SUP_cong o_apply)


subsection {* Complete Distributive Lattices *}

text {* The product of two lattices
whose @{const inf} and @{const sup} operators
distribute over @{const Sup} and @{const Inf},
is a lattice
whose @{const inf} and @{const sup} operators
distribute over @{const Sup} and @{const Inf}. *}

lemma sup_sup_Inf_Inf:
"(x::'a::complete_distrib_lattice \<times> 'b::complete_distrib_lattice) \<squnion> \<Sqinter>A =
 (INF y:A. x \<squnion> y)"
by (auto simp:
 sup_prod_def sup_sup_def Inf_prod_def Inf_Inf_def INF_INF_alt_def sup_Inf)

lemma inf_inf_Sup_Sup:
"(x::'a::complete_distrib_lattice \<times> 'b::complete_distrib_lattice) \<sqinter> \<Squnion>A =
 (SUP y:A. x \<sqinter> y)"
by (auto simp:
 inf_prod_def inf_inf_def Sup_prod_def Sup_Sup_def SUP_SUP_alt_def inf_Sup)

instance prod ::
 (complete_distrib_lattice, complete_distrib_lattice) complete_distrib_lattice
proof qed (auto simp: sup_sup_Inf_Inf inf_inf_Sup_Sup)


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_Inf:
"\<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_Sup:
"\<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_Inf finite_Sup_Sup)

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://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20121212/17d837e5/attachment-0001.p7s>