https://svhol.pbmichel.de/ 2026-04-21T12:11:24+0200 https://svhol.pbmichel.de/ https://svhol.pbmichel.de/lib/tpl/dokuwiki/images/favicon.ico text/html 2012-04-13T15:53:39+0200 Anonymous (anonymous@undisclosed.example.com) https://svhol.pbmichel.de/reference/assumption?rev=1334325219&do=diff Assumption assumption solves a subgoal if the consequent is (literally) contained in the set of assumptions. Definition " [The assumption method] proves a subgoal by finding a matching assumption." (From “Isabelle/HOL -- A Proof Assisstant for Higher-Order Logic text/html 2011-07-25T12:32:25+0200 Anonymous (anonymous@undisclosed.example.com) https://svhol.pbmichel.de/reference/attribute_examples?rev=1311589945&do=diff Attribute Examples This page contains usage examples for attributes (or directives). of Consider rule/theorem mp: . Using mp [of _ "C ∨ D"] yields the more specific theorem . Note that are no longer schematic variables but specific terms. text/html 2011-07-06T12:08:19+0200 Anonymous (anonymous@undisclosed.example.com) https://svhol.pbmichel.de/reference/drule?rev=1309946899&do=diff drule drule is a proof method. It applies a rule if possible. Definition Assume we have a subgoal and we want to use drule with rule Then, drule does the following: * Unify and for some . The application fails if there is no unifier for any ; otherwise, let text/html 2011-07-06T12:13:15+0200 Anonymous (anonymous@undisclosed.example.com) https://svhol.pbmichel.de/reference/erule?rev=1309947195&do=diff erule erule is a proof method. It applies a rule if possible. Definition Assume we have a subgoal and we want to use erule with rule Then, erule does the following: * Unify with and with simultaneously for some . The application fails if there is no unifier for any text/html 2011-06-22T12:37:33+0200 Anonymous (anonymous@undisclosed.example.com) https://svhol.pbmichel.de/reference/frule?rev=1308739053&do=diff frule frule is a proof method. It applies a rule if possible. Definition Assume we have a subgoal and we want to use frule with rule Then, frule does the following: * Unify and for some . The application fails if there is no unifier for any ; otherwise, let text/html 2011-07-13T12:52:44+0200 Anonymous (anonymous@undisclosed.example.com) https://svhol.pbmichel.de/reference/induct?rev=1310554364&do=diff Induction Induction methods can be used with induction rules to prove theorems over inductive datatypes or sets as well as recursive functions. Note that induction typically creates multiple new subgoals: one for each base case and one for the inductive step. text/html 2011-06-13T22:00:12+0200 Anonymous (anonymous@undisclosed.example.com) https://svhol.pbmichel.de/reference/rename_tac?rev=1307995212&do=diff rename_tac Assigns new identifiers to bound variables from left to right. If there are more variables than new names, the rightmost are renamed. text/html 2011-06-14T22:04:18+0200 Anonymous (anonymous@undisclosed.example.com) https://svhol.pbmichel.de/reference/rotate_tac?rev=1308081858&do=diff rotate_tac Rotates the assumptions by k positions to the left. It can be used to influence which assumption is unified when using methods like drule, frule, erule or even Assumption. text/html 2011-06-13T22:02:31+0200 Anonymous (anonymous@undisclosed.example.com) https://svhol.pbmichel.de/reference/rule?rev=1307995351&do=diff Rule Rule can refer to several things in the context of Isabelle/HOL: * The general concept of rules in logics * The proof method rule text/html 2011-06-13T22:05:52+0200 Anonymous (anonymous@undisclosed.example.com) https://svhol.pbmichel.de/reference/rule_calculus?rev=1307995552&do=diff Rule (calculus) In Logics In a logical calculus, a rule is given by with formula in the considered logic. Of course, might depend on any combination of the . The meaning is this: If you can prove in your calculus, you can also prove . In other terms, a set of rules together with some axioms (rules with text/html 2011-06-22T12:27:18+0200 Anonymous (anonymous@undisclosed.example.com) https://svhol.pbmichel.de/reference/rule_method?rev=1308738438&do=diff rule (method) rule is a proof method. It applies a rule if possible. Definition Assume we have a subgoal and we want to use rule with rule Then, rule does the following: * Unify and . The application fails if there is no unifier; otherwise, let be this unifier. text/html 2013-11-03T15:19:13+0200 Anonymous (anonymous@undisclosed.example.com) https://svhol.pbmichel.de/reference/start?rev=1383488353&do=diff sadfasdf text/html 2011-06-13T22:02:53+0200 Anonymous (anonymous@undisclosed.example.com) https://svhol.pbmichel.de/reference/subgoal_tac?rev=1307995373&do=diff subgoal_tac Adds a formula to the assumptions but adds a subgoal to prove it from the current ones. text/html 2011-06-29T12:50:45+0200 Anonymous (anonymous@undisclosed.example.com) https://svhol.pbmichel.de/reference/theorem_search?rev=1309344645&do=diff Theorem Search By typing C-c C-f, you get a search prompt. You can search for (a combination of) several things: * pattern -- searches for theorems whose expressions match the given pattern. * intro -- searches for theorems which can be applied with text/html 2014-07-29T10:05:58+0200 Anonymous (anonymous@undisclosed.example.com) https://svhol.pbmichel.de/reference/thin_tac?rev=1406621158&do=diff Use thin_tac to throw away assumptions that you don't need in order to prove your subgoal. Thin_tac needs a scheme for knowing, which assumption it should use. The first matching assumption will be deleted. Examples: lemma “⟦P t0;∀t. P t⟧ ⟹ P t0