| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Isabelle/Doc/Tutorial/Rules/ (Beweissystem Isabelle Version 2025-1©) Datei vom 16.11.2025 mit Größe 1 kB |
|
Quelle find2.thySprache: Isabelle |
|||||||||||||||
|
(*<*) theory find2 imports Main begin lemma "A ∧ B" (*>*) txt‹\index{finding theorems}\index{searching theorems} In \S\ref{sec:find}, we introduced Proof General's \pgmenu{Find} button for finding theorems in the database via pattern matching. If we are inside a proof, we can be more specific; we can search for introduction, elimination and destruction rules \emph{with respect to the current goal}. For this purpose, \pgmenu{Find} provides three aditional search criteria: \texttt{intro}, \texttt{elim} and \texttt{dest}. For example, given the goal @{subgoals[display,indent=0,margin=65]} you can click on \pgmenu{Find} and type in the search expression \texttt{intro}. You will be shown a few rules ending in ‹==> ?P ∧ ?Q›, among them @{thm[source]conjI}\@. You may even discover that the very theorem you are trying to prove is already in the database. Given the goal› (*<*) oops lemma "A ⟶ A" (*>*) txt‹\vspace{-\bigskipamount} @{subgoals[display,indent=0,margin=65]} the search for \texttt{intro} finds not just @{thm[source] impI} but also @{thm[source] imp_refl}: @{thm imp_refl}. As before, search criteria can be combined freely: for example, \begin{ttbox} "_ \at\ _" intro \end{ttbox} searches for all introduction rules that match the current goal and mention the ‹@› f Searching for elimination and destruction rules via \texttt{elim} and \texttt{dest} is analogous to \texttt{intro} but takes the assumptions into account, too. › (*<*) oops end (*>*)
¤ Dauer der Verarbeitung: 0.13 Sekunden (vorverarbeitet am 2026-04-27) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-05-26