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!
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
smime.p7s
Description: S/MIME Cryptographic Signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
