Gergely Buday (Aug 04 2023 at 09:16): Gergely Buday (Aug 04 2023 at 09:16):How can I find the following? I need summation over sets of natural numbers. Is there a definition and the obvious lemmas somewhere? I did not find it in Set.thy or Nat.thy.
Yong Kiam (Aug 04 2023 at 09:22):when I need to find definitions, there are a couple of options I try in the Query panel:
1) try an "obvious" term... in this case typing sum in the query panel will give you what you need
2) try an "obvious" word for the term . typing name:"sum" would give you theorems which have the word "sum" in their names then you can scroll through the theorems to see if your desired term is somewhere there
3) search by type. _ :: nat set => nat would give you terms matching the type you described above (note that this is not all that helpful in this case)
Jonathan Julian Huerta y Munive (Aug 04 2023 at 09:22):Hi, the way I solve this kind of questions is by loading a theory I know needs to use the concept I am searching for, e.g. Main. Type it, e.g. term "sum" and ctrl+click it. Isabelle takes you to the theory that implements this. In this case, Groups_Big: https://isabelle.in.tum.de/dist/library/HOL/HOL/Groups_Big.html
Kevin Kappelmann (Aug 04 2023 at 09:43):https://isabelle.systems/cookbook/src/searching_isabelle/
Last updated: Apr 27 2024 at 20:14 UTC