Email Gateway (Aug 22 2022 at 20:36): Email Gateway (Aug 22 2022 at 20:36):From: mailing-list anonymous <mailing.list.anonymous@gmail.com>
Dear All,
I noticed that many theorems in the theory Set_Interval (part of the main
HOL library) can be generalized. For example, certain theorems that are
stated for linear orders are applicable to partial orders and certain
theorems that are stated for partial orders are applicable to preorders:
the code listing below provides a non-exhaustive list of examples (I use
Isabelle2019 as a reference, but, I believe, the situation is similar in
Isabelle-dev). Was there a good reason for not stating these theorems in
the more general form? Also, please let me know whether it is worth
mentioning other similar issues on the mailing list.
Thank you
(* The proofs were obtained using Sledgehammer. However, of course, I can
provide proofs of reasonable quality upon request, if necessary. *)
section ‹Example›
theory example
imports Main
begin
(*lemma atLeast_eq_iff [iff]:
"(atLeast x = atLeast y) = (x = (y::'a::linorder))"
by (blast intro: order_antisym order_trans)*)
lemma atLeast_eq_iff [iff]: "(atLeast x = atLeast y) = (x = (y::'a::order))"
by (metis antisym atLeast_iff order_refl)
(*lemma atMost_eq_iff [iff]: "(atMost x = atMost y) = (x =
(y::'a::linorder))"
by (blast intro: order_antisym order_trans)*)
lemma atMost_eq_iff [iff]: "(atMost x = atMost y) = (x = (y::'a::order))"
by (metis atLeastAtMost_def atLeastAtMost_singleton_iff)
(*lemma single_Diff_lessThan [simp]: "!!k:: 'a::order. {k} - lessThan k =
{k}"
by auto*)
lemma single_Diff_lessThan[simp]: "!!k:: 'a::preorder. {k} - lessThan k =
{k}"
by auto
(*lemma atLeast_subset_iff[iff]:
"(atLeast x ⊆ atLeast y) = (y ≤ (x::'a::order))"
by (blast intro: order_trans)*)
lemma atLeast_subset_iff'[iff]:
"(atLeast x ⊆ atLeast y) = (y ≤ (x::'a::preorder))"
by (meson atLeast_iff in_mono order_refl order_trans subsetI)
(*lemma atMost_subset_iff[iff]: "(atMost x ⊆ atMost y) = (x ≤
(y::'a::order))"
by (blast intro: order_trans)*)
lemma atMost_subset_iff[iff]: "(atMost x ⊆ atMost y) = (x ≤
(y::'a::preorder))"
by (meson atMost_iff in_mono order_refl order_trans subsetI)
subsubsection‹Emptyness, singletons, subset›
(* The following theorems are stated in the context of Orderings.order in
the theory Set_Interval. *)
context Orderings.preorder
begin
lemma atLeastatMost_empty[simp]:
"b < a ⟹ {a..b} = {}"
by (metis equals0I local.less_le_not_le local.order_trans
ord.atLeastAtMost_iff)
lemma atLeastatMost_empty_iff[simp]:
"{a..b} = {} ⟷ (¬ a ≤ b)"
by (metis empty_iff equals0I local.order_refl local.order_trans
ord.atLeastAtMost_iff)
lemma atLeastatMost_empty_iff2[simp]:
"{} = {a..b} ⟷ (¬ a ≤ b)"
using local.atLeastatMost_empty_iff by blast
lemma atLeastLessThan_empty[simp]:
"b <= a ⟹ {a..<b} = {}"
by (metis equals0I local.le_less_trans local.less_le_not_le
ord.atLeastLessThan_iff)
lemma atLeastLessThan_empty_iff[simp]:
"{a..<b} = {} ⟷ (¬ a < b)"
using local.le_less_trans by auto
lemma atLeastLessThan_empty_iff2[simp]:
"{} = {a..<b} ⟷ (¬ a < b)"
using local.atLeastLessThan_empty_iff by blast
lemma greaterThanAtMost_empty[simp]: "l ≤ k ==> {k<..l} = {}"
by (metis equals0I local.less_le_not_le local.less_le_trans
ord.greaterThanAtMost_iff)
lemma greaterThanAtMost_empty_iff[simp]: "{k<..l} = {} ⟷ ¬ k < l"
using local.greaterThanAtMost_def local.less_le_trans by auto
lemma greaterThanAtMost_empty_iff2[simp]: "{} = {k<..l} ⟷ ¬ k < l"
using local.greaterThanAtMost_empty_iff by blast
lemma greaterThanLessThan_empty[simp]:"l ≤ k ==> {k<..<l} = {}"
by (metis equals0I local.le_less_trans local.less_irrefl local.less_trans
ord.greaterThanLessThan_iff)
lemma atLeastatMost_subset_iff[simp]:
"{a..b} ≤ {c..d} ⟷ (¬ a ≤ b) ∨ c ≤ a ∧ b ≤ d"
by (meson local.atLeastAtMost_iff local.eq_refl local.order_trans subsetD
subsetI)
lemma atLeastatMost_psubset_iff:
"{a..b} < {c..d} ⟷
((¬ a ≤ b) ∨ c ≤ a ∧ b ≤ d ∧ (c < a ∨ b < d)) ∧ c ≤ d"
by (smt local.atLeastatMost_subset_iff local.less_le_not_le psubset_eq
subset_not_subset_eq)
lemma Icc_subset_Ici_iff[simp]:
"{l..h} ⊆ {l'..} = (¬ l≤h ∨ l≥l')"
by (metis emptyE local.atLeastAtMost_iff local.atLeastatMost_empty_iff
local.eq_refl ord.atLeast_iff subsetD subsetI)
lemma Icc_subset_Iic_iff[simp]:
"{l..h} ⊆ {..h'} = (¬ l≤h ∨ h≤h')"
by (metis Int_iff Int_subset_iff empty_subsetI inf_absorb2
local.atLeastAtMost_iff local.atLeastatMost_empty_iff2
local.atLeastatMost_subset_iff local.atMost_iff local.order_refl
ord.atLeastAtMost_def)
lemma not_Ici_eq_empty[simp]: "{l..} ≠ {}"
by blast
lemma not_Iic_eq_empty[simp]: "{..h} ≠ {}"
by blast
end
end
Email Gateway (Aug 22 2022 at 20:37):From: Lawrence Paulson <lp15@cam.ac.uk>
Yes, there are many such issues. Whenever a theorem can be straightforwardly generalised, please let us know so that we can fix it.
Larry Paulson
Email Gateway (Aug 22 2022 at 20:37):From: mailing-list anonymous <mailing.list.anonymous@gmail.com>
Dear Lawrence Paulson,
Thank you for your email. I am glad that the information that I provided
was useful. Please find a list of several further results that can be
easily generalized in the code listing below.
Thank you
section ‹Example›
theory example
imports Complex_Main
begin
(from order)
context preorder
begin
(Transitive_Closure)
lemma acyclicI_order:
fixes f :: "'b ⇒ 'a"
assumes *: "⋀a b. (a, b) ∈ r ⟹ f b < f a"
shows "acyclic r"
sorry
end
(from linorder)
context order
begin
(Orderings)
lemma antisym_conv1: "¬ x < y ⟹ x ≤ y ⟷ x = y"
sorry
(Orderings)
lemma antisym_conv2: "x ≤ y ⟹ ¬ x < y ⟷ x = y"
sorry
(Orderings)
lemma leD: "y ≤ x ⟹ ¬ x < y"
sorry
(Topological_Spaces)
lemma less_separate:
assumes "x < y"
shows "∃a b. x ∈ {..< a} ∧ y ∈ {b <..} ∧ {..< a} ∩ {b <..} = {}"
sorry
end
(from dense_linorder)
context linorder
begin
(Set_Interval)
lemma atLeastAtMost_subseteq_atLeastLessThan_iff:
"{a .. b} ⊆ { c ..< d } ⟷ (a ≤ b ⟶ c ≤ a ∧ b < d)"
sorry
end
Last updated: Nov 21 2024 at 12:39 UTC