Email Gateway (Aug 22 2022 at 20:43): Email Gateway (Aug 22 2022 at 20:43):From: Jonathan Julián Huerta y Munive <jonjulian23@gmail.com>
Hello,
I have been working with the type "('a,'b) vec" from HOL-Analysis, and some
AFP entries. Handling such a big library requires searching for various
constructs that other people have built. I've managed to find many things
with the Ctrl+Click feature but there are others that I'd still like to
learn. In particular:
· What's the proper way to find the file where a theorem of the form
"OFCLASS(_,_)" was proved? E.g. how do I find where the type vec was shown
to be a "ring_1"?
· How can I quickly find the line where a notation was introduced? When I
Ctrl+Click the symbol, it takes me to the definition/abbreviation, but the
notation may have been set up in other places.
· If I use a list of "named_theorems" other people introduced, how do I
tell Isabelle to show me the theorem it just applied (from the many
contained in the list)?
· How do I search if a class/locale has been declared a subclass/sublocale
of another?
Sincerely,
Jonathan Julian Huerta y Munive
Email Gateway (Aug 22 2022 at 20:56):From: Makarius <makarius@sketis.net>
That is a nice summary of things that don't quite work, as far as I can
tell on the spot.
Maybe some expert users know a few tricks as partial solutions.
Makarius
Email Gateway (Aug 22 2022 at 20:56):From: Peter Lammich <lammich@in.tum.de>
I quite frequently use a command
find_in_theorems pattern in thms1 ... thmsn
For example:
find_in_theorems "_+_" "_*_" in algebra_simps field_simps
Results
Rings.semiring_class.distrib_right: algebra_simps(17): (?a + ?b) * ?c
= ?a * ?c + ?b * ?c
Rings.semiring_class.distrib_left: algebra_simps(18): ?a * (?b + ?c)
= ?a * ?b + ?a * ?c
Rings.semiring_class.distrib_left_NO_MATCH: field_simps(17): NO_MATCH
(?x div ?y) ?a ⟹ ?a * (?b + ?c) = ?a * ?b + ?a * ?c
Rings.semiring_class.distrib_right_NO_MATCH: field_simps(18):
NO_MATCH (?x div ?y) ?c ⟹ (?a + ?b) * ?c = ?a * ?c + ?b * ?c
Fields.division_ring_class.add_divide_eq_iff: field_simps(26): ?z ≠ 0
⟹ ?x + ?y / ?z = (?x * ?z + ?y) / ?z
Fields.division_ring_class.divide_add_eq_iff: field_simps(27): ?z ≠ 0
⟹ ?x / ?z + ?y = (?x + ?y * ?z) / ?z
Fields.division_ring_class.minus_divide_add_eq_iff: field_simps(29):
?z ≠ 0 ⟹ - (?x / ?z) + ?y = (- ?x + ?y * ?z) / ?z
Compared to find-theorems, the command is a bit limited, as it does not
support goal-dependent patterns like intro, elim, dest. It's already
suitable to search for certain theorems in large
named_theorems-collections. It will show the "simplest" name of the
theorem, the number of the theorem in the theorem-collection, and the
statement of the theorem.
With a bit of work, this feature could be integrated into the full
find-theorems command, e.g., in a context with a subgoal, you could
then write
find_theorems intro in algebra_simps
I attach my current prototype for the find_in_theorems command
to this mail, in case someone is interested...
Find_In_Theorems.thy
Names_Of_Thm.thy
Email Gateway (Aug 22 2022 at 20:57):From: Wenda Li <wl302@cam.ac.uk>
· How do I search if a class/locale has been declared a subclass/sublocale
of another?
A quick-and-dirty way might be to attempt to prove it. For example, if we are not sure if a field is a sublocale of a semiring, we can put down:
sublocale field ⊆ semiring
and Isabelle will suggest:
Auto solve_direct: the current goal can be solved directly with
local.semiring_axioms: class.semiring (+) (*)
So that we know it is trivially provable and a field is indeed a sublocale of a semiring.
There probably is a better way to do this…
Wenda
Email Gateway (Aug 23 2022 at 08:32):From: Jonathan Julián Huerta y Munive <jonjulian23@gmail.com>
Hello,
We finally have a list of answers to all the questions I did on
11/10/2019 about
various searches in Isabelle. Thanks to Peter, Wenda, Makarius and Fabian
for their replies. Hopefully, the solutions can be integrated in one place.
*>> · If I use a list of "named_theorems" other people introduced, how do
I>> tell Isabelle to show me the theorem it just applied (from the many>>
contained in the list)?*
On Tue, 12 Nov 2019, at 22:19:35 <lammich@in.tum.de> wrote:
I quite frequently use a command find_in_theorems pattern in thms1..thmsn
For example: find_in_theorems "_+_" "_*_" in algebra_simps field_simps
[...]
Compared to find-theorems, the command is a bit limited, as it does not
support goal-dependent patterns like intro, elim, dest. It's already
suitable to search for certain theorems in large
named_theorems-collections. It will show the "simplest" name of the
theorem, the number of the theorem in the theorem-collection, and the
statement of the theorem.
*>> · How do I search if a class/locale has been declared a
subclass/sublocale>> of another?*
On Tue, 12 Nov 2019, at 22:31:34 <wl302@cam.ac.uk> wrote:
A quick-and-dirty way might be to attempt to prove it. For example, if we
are
not sure if a field is a sublocale of a semiring, we can put down:
sublocale field ⊆ semiring and Isabelle will suggest:
Auto solve_direct: the current goal can be solved directly with
local.semiring_axioms: class.semiring (+) (*)
*>> · What's the proper way to find the file where a theorem of the form>>
"OFCLASS(_,_)" was proved? E.g. how do I find where the type vec was
shown>> to be a "ring_1"?>> · How can I quickly find the line where a
notation was introduced? When I>> Ctrl+Click the symbol, it takes me to the
definition/abbreviation, but the>> notation may have been set up in other
places.*
On Mon, Mar 23, 2020 at 5:06 PM <huch@in.tum.de> wrote:
Hi Jonathan,
[... ]I have build a tool (search.isabelle.in.tum.de) which might be
interesting.We can then find where vec was shown to be a ring_1: Filtering by
'instance' commands and 'ring_1' in the source text gives me a single
result
<https://search.isabelle.in.tum.de/#search?page=%5B%5D&q=%7B%22fields%22%3A%5B%7B%22field%22%3A%22Command%22%2C%22terms%22%3A%5B%22instance%22%5D%7D%2C%7B%22field%22%3A%22SourceText%22%2C%22terms%22%3A%5B%22ring_1%22%5D%7D%5D%2C%22usedIn%22%3A%7B%22block%22%3A%22typedef%20('a%2C%20'b)%20vec%20%3D%20%5C%22UNIV%20%3A%3A%20('b%3A%3Afinite%20%E2%87%92%20'a)%20set%5C%22%5Cn%20%20morphisms%20vec_nth%20vec_lambda%20..%22%2C%22ids%22%3A%5B%22Fact.Finite_Cartesian_Product.arity_type_vec%22%2C%22Constant.Finite_Cartesian_Product.vec.vec_lambda%22%2C%22Fact.Finite_Cartesian_Product.vec.vec_lambda_induct%22%2C%22Fact.Finite_Cartesian_Product.vec.vec_lambda_cases%22%2C%22Fact.Finite_Cartesian_Product.vec.vec_lambda_inject%22%2C%22Fact.Finite_Cartesian_Product.vec.vec_lambda_inverse%22%2C%22Constant.Finite_Cartesian_Product.typerep_vec_inst.typerep_vec%22%2C%22Fact.Finite_Cartesian_Product.typerep_vec_inst.typerep_vec%22%2C%22Fact.Finite_Cartesian_Product.vec.type_definition_vec%22%2C%22Fact.Finite_Cartesian_Product.arity_typerep_vec%22%2C%22Fact.Finite_Cartesian_Product.typerep_vec_def%22%2C%22Constant.Finite_Cartesian_Product.vec.vec_nth%22%2C%22Fact.Finite_Cartesian_Product.vec.vec_nth_inject%22%2C%22Fact.Finite_Cartesian_Product.vec.vec_nth_cases%22%2C%22Fact.Finite_Cartesian_Product.vec.vec_nth_induct%22%2C%22Fact.Finite_Cartesian_Product.vec.vec_nth_inverse%22%2C%22Fact.Finite_Cartesian_Product.vec.vec_nth%22%2C%22Type.Finite_Cartesian_Product.vec%22%5D%7D%7D>
in HOL-Analysis.Finite_Cartesian_Product.Hope this is relevant for you! If it is, and you're playing around with
the tool a little, please do consider filling out the feedback form
<https://forms.gle/vw8dhkgtbpXhuCUp6>.
Last updated: Apr 18 2024 at 08:19 UTC