Email Gateway (Aug 22 2022 at 20:25): Email Gateway (Aug 22 2022 at 20:25):From: mailing-list anonymous <mailing.list.anonymous@gmail.com>
Dear All,
I hope it is not entirely inappropriate to provide several further comments
on the progress in the development of an extension of the framework
Types-To-Sets in the form of a reply to a remark that was made in the
previous thread on this subject:
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2019-June/msg00072.html.
I believe that I have finally reached the stage at which the full
automation of the relativization process is possible in certain cases. If
certain conditions are met, the users need not have almost any
understanding of the relativization algorithm and only a minimal amount of
effort is required on their part to perform the relativization. Moreover,
this effort comes down to, primarily, providing lists of definitions and
theorems that they would like to relativize. The enabling feature was the
implementation of the algorithm for the relativization of definitions (the
algorithm was suggested by Fabian Immler).
After my signature, I provide an example of the relativization of a small
section of the theory about preorders from the theory files Orderings.thy
and Set_Interval.thy. This theory provides, approximately, 12 relativized
definitions and 55 new relativized theorems for only one proof that needed
to be done by the user (the proof is that of the parametricity property
that exists between the locale predicates of the class.preorder and the
newly introduced locale preorder_ow). The example is available as part of
the GitHub repository https://github.com/xanonec/HOL-TTS-Ext, where the
development takes place.
The conditions that I am referring to in the previous paragraph are that
only the plain definitions are used in the type-based theory (at this
stage, the relativization of constants obtained using other specification
elements still needs to be performed explicitly by the user) and that the
definitions do not contain Hilbert choice, definite description operator,
undefined constants and other possible sources of 'non-determinism'.
However, usually, it is relatively easy to provide the relativization of
constants obtained using the specification elements other than 'definition'
manually.
Effectively, the framework provides a convenient tool for synthesizing
significant parts of the libraries of relativized results (e.g.
HOL-Algebra) from the type-based counterparts in a nearly automated manner
(e.g. see https://github.com/xanonec/HOL-SML-Relativization).
I believe that I am reaching the stage at which the work can be considered
to be nearly feature-complete. Nevertheless, at this stage, I still welcome
suggestions for the improvement of the functionality.
The only downside is that, by now, I also realised that it will take a
substantial amount of time before I can provide a stable release of the
software. There is still a very substantial amount of software engineering
work that needs to be done before this work can be considered to be
completed. Also, it seems that I will not be able to afford to allow myself
to spend as much time on this project as I was able in the last couple of
months from the beginning of autumn.
Thank you
section ‹Relativization of the results about orders›
theory Simple_Orders
imports
"../TTS"
begin
subsection ‹Definitions I: user-defined relativizations›
locale ord_ow =
fixes 𝔘 :: "'ao set"
and le :: "['ao, 'ao] ⇒ bool" (infix ‹≤⇩o⇩w› 50)
and ls :: "['ao, 'ao] ⇒ bool" (infix ‹<⇩o⇩w› 50)
begin
notation le (‹'(≤⇩o⇩w')›)
and le (infix ‹≤⇩o⇩w› 50)
and ls (‹'(<⇩o⇩w')›)
and ls (infix ‹<⇩o⇩w› 50)
abbreviation (input) ge (infix ‹≥⇩o⇩w› 50) where "x ≥⇩o⇩w y ≡ y ≤⇩o⇩w x"
abbreviation (input) gt (infix ‹>⇩o⇩w› 50) where "x >⇩o⇩w y ≡ y <⇩o⇩w x"
notation ge (‹'(≥⇩o⇩w')›)
and ge (infix ‹≥⇩o⇩w› 50)
and gt (‹'(>⇩o⇩w')›)
and gt (infix ‹>⇩o⇩w› 50)
end
locale preorder_ow = ord_ow 𝔘 le ls
for 𝔘 :: "'ao set" and le ls +
assumes less_le_not_le:
"⟦ x ∈ 𝔘; y ∈ 𝔘 ⟧ ⟹ x <⇩o⇩w y ⟷ x ≤⇩o⇩w y ∧ ¬ (y ≤⇩o⇩w x)"
and order_refl[iff]: "x ∈ 𝔘 ⟹ x ≤⇩o⇩w x"
and order_trans: "⟦ x ∈ 𝔘; y ∈ 𝔘; z ∈ 𝔘; x ≤⇩o⇩w y; y ≤⇩o⇩w z ⟧ ⟹ x
≤⇩o⇩w z"
context
includes lifting_syntax
begin
lemma preorder_transfer[transfer_rule]:
assumes [transfer_rule]: "right_total A"
shows
"((A ===> A ===> (=)) ===> (A ===> A ===> (=)) ===> (=))
(preorder_ow (Collect (Domainp A))) class.preorder"
unfolding preorder_ow_def class.preorder_def
apply transfer_prover_start
apply transfer_step+
by blast
end
subsection ‹Definitions II: automated relativization›
tts_unoverload_definitions
("(≤)::?'a::ord⇒?'a::ord⇒bool", "(<)::?'a::ord⇒?'a::ord⇒bool")
in lessThan_def (‹'(/with _ : (1{..<_})/')›)
and atMost_def (‹'(/with _ : (1{.._})/')›)
and greaterThan_def (‹'(/with _ : (1{_<..})/')›)
and atLeast_def (‹'(/with _ : (1{_..})/')›)
and greaterThanLessThan_def (‹'(/with _ : (1{_<..<_})/')›)
and atLeastLessThan_def (‹'(/with _ _ : (1{_..<_})/')›)
and greaterThanAtMost_def (‹'(/with _ _ : (1{_<.._})/')›)
and atLeastAtMost_def (‹'(/with _ : (1{_.._})/')› )
and min_def (‹'(/with _ : «min» _ _/')› [1000, 1000, 1000] 1000)
and max_def (‹'(/with _ : «max» _ _/')› [1000, 1000, 1000] 1000)
tts_relativize_definitions
types: (?'a ‹𝔘::'a set›)
in lessThan_with_def (‹'(/on _ with _ : (1{..<_})/')›)
and atMost_with_def (‹'(/on _ with _ : (1{.._})/')›)
and greaterThan_with_def (‹'(/on _ with _: (1{_<..})/')›)
and atLeast_with_def (‹'(/on _ with _ : (1{_..})/')›)
and greaterThanLessThan_with_def (‹'(/on _ with _ : (1{_<..<_})/')›)
and atLeastLessThan_with_def (‹'(/on _ with _ _ : (1{_..<_})/')›)
and greaterThanAtMost_with_def (‹'(/on _ with _ _ : (1{_<.._})/')›)
and atLeastAtMost_with_def (‹'(/on _ with _ : (1{_.._})/')›)
and min_with_def
and max_with_def
tts_unoverload_definitions
in bdd_above_def (‹'(/with _ : «bdd'_above» _/')›)
and bdd_below_def (‹'(/with _ : «bdd'_below» _/')›)
tts_relativize_definitions
types: (?'a ‹𝔘::'a set›)
in bdd_above_with_def (‹'(/on _ with _ : «bdd'_above» _/')›)
and bdd_below_with_def (‹'(/on _ with _ : «bdd'_below» _/')›)
subsubsection ‹Relativization of theorems›
context preorder_ow
begin
tts_relativize_facts
types: (?'a 𝔘)
substituting preorder_ow_axioms
trying auto
in preorder_class.less_irrefl
and preorder_class.bdd_below_Ioc
and preorder_class.bdd_above_Ioc
and preorder_class.bdd_above_Iic
and preorder_class.bdd_above_Iio
and preorder_class.bdd_below_Ici
and preorder_class.bdd_below_Ioi
and preorder_class.bdd_above_Icc
and preorder_class.bdd_above_Ioo
and preorder_class.bdd_below_Icc
and preorder_class.bdd_below_Ioo
and preorder_class.bdd_above_Ico
and preorder_class.bdd_below_Ico
and preorder_class.Ioi_le_Ico
and preorder_class.eq_refl
and preorder_class.less_imp_le
and preorder_class.less_not_sym
and preorder_class.less_imp_not_less
and preorder_class.less_asym'
and preorder_class.less_imp_triv
and preorder_class.less_trans
and preorder_class.less_le_trans
and preorder_class.le_less_trans
and preorder_class.bdd_aboveI
and preorder_class.bdd_belowI
and preorder_class.less_asym
and preorder_class.bdd_above_Int1
and preorder_class.bdd_above_Int2
and preorder_class.bdd_below_Int1
and preorder_class.bdd_below_Int2
and preorder_class.bdd_above_mono
and preorder_class.bdd_below_mono
and bdd_above_empty
and preorder_class.bdd_below_empty
tts_relativize_facts
types: (?'a 𝔘) and (?'b ‹𝔘⇩2::'b set›)
substituting preorder_ow_axioms
trying (auto intro: bdd_above_empty bdd_below_empty)
in preorder_class.bdd_belowI2
and preorder_class.bdd_aboveI2
end
tts_statistics
end
Automatically generated unoverloaded definitions:
theorem lessThan_with_def: (with ?less : {..<?u}) ≡ {x. ?less x ?u}
theorem lessThan_with.overloaded: lessThan ≡ lessThan_with (<)
theorem atMost_with_def: (with ?less_eq : {..?u}) ≡ {x. ?less_eq x ?u}
theorem atMost_with.overloaded: atMost ≡ atMost_with (≤)
theorem greaterThan_with_def: (with ?less : {?l<..}) ≡ {x. ?less ?l x}
theorem greaterThan_with.overloaded: greaterThan ≡ greaterThan_with (<)
theorem atLeast_with_def: (with ?less_eq : {?l..}) ≡ {x. ?less_eq ?l x}
theorem atLeast_with.overloaded: atLeast ≡ atLeast_with (≤)
theorem greaterThanLessThan_with_def: (with ?less : {?l<..<?u}) ≡ (with
?less : {?l<..}) ∩ (with ?less : {..<?u})
theorem greaterThanLessThan_with.overloaded: greaterThanLessThan ≡
greaterThanLessThan_with (<)
theorem atLeastLessThan_with_def: (with ?less_eq ?less : {?l..<?u}) ≡ (with
?less_eq : {?l..}) ∩ (with ?less : {..<?u})
theorem atLeastLessThan_with.overloaded: atLeastLessThan ≡
atLeastLessThan_with (≤) (<)
theorem greaterThanAtMost_with_def: (with ?less_eq ?less : {?l<..?u}) ≡
(with ?less : {?l<..}) ∩ (with ?less_eq : {..?u})
theorem greaterThanAtMost_with.overloaded: greaterThanAtMost ≡
greaterThanAtMost_with (≤) (<)
theorem atLeastAtMost_with_def: (with ?less_eq : {?l..?u}) ≡ (with ?less_eq
: {?l..}) ∩ (with ?less_eq : {..?u})
theorem atLeastAtMost_with.overloaded: atLeastAtMost ≡ atLeastAtMost_with
(≤)
theorem min_with_def: (with ?less_eq : «min» ?a ?b) ≡ if ?less_eq ?a ?b
then ?a else ?b
theorem min_with.overloaded: min ≡ min_with (≤)
theorem max_with_def: (with ?less_eq : «max» ?a ?b) ≡ if ?less_eq ?a ?b
then ?b else ?a
theorem max_with.overloaded: max ≡ max_with (≤)
theorem bdd_above_with_def: (with ?less_eq : «bdd_above» ?A) ≡ ∃M. ∀x∈?A.
?less_eq x M
theorem bdd_above_with.overloaded: bdd_above ≡ bdd_above_with (≤)
theorem bdd_below_with_def: (with ?less_eq : «bdd_below» ?A) ≡ ∃m. Ball ?A
(?less_eq m)
theorem bdd_below_with.overloaded: bdd_below ≡ bdd_below_with (≤)
[message truncated]
Last updated: Apr 25 2024 at 01:08 UTC