Instantiierende Sätze in Isabelle

Question

Angenommen, ein Lemma, lasst uns an_equation nennen, beweist, dass die Gleichung f (n) = n * n + 1 für alle ungeraden natürlichen Zahlen n gilt (und f ist eine vorher definierte Funktion).

Wie kann ich dieses Lemma auf konkrete Werte von n instantiieren, so dass ich beweisen kann, sagen wir f (5) = 5 * 5 + 1?

(Es gibt das lemmas Schlüsselwort, mit dem ich lemmas inst = an_equation[where n=5, simplified] beweisen kann, aber das ist nicht ganz das, was ich was. Was ich will,

lemma inst_new : "f(5) = 5*5+1" 

ist aber, wie es gab kaum ein Beispiel um in den üblichen Unterlagen thai ich berate, ich konnte nicht herausfinden, wie man das beweist.)

Answer 1

Sie können freie Variablen in Ihrem Theorem mit den of und where Attributen, z an_equation[of 5] oder an_equation[where n = 5]. Sie können seine Annahmen auch instanziieren, z. Wenn Sie ein Theorem namens foo der Form P x ⟹ Q x haben und ein Theorem namens bar der Form P 5 haben, können Sie foo[OF bar] tun, um das Theorem Q 5 zu erhalten.

Sie können diesen mit thm (z thm foo[of 5]) instanziiert untersuchen und sie in einem Beweis verwenden, um mit using, from usw.

Hinweis, dass der Nachweis Methoden auch Theoreme instanziiert, wenn nötig, zum Beispiel wenn Sie haben, wie oben beschrieben, ist der Satz foo besagt, dass P n ⟹ Q n und Sie haben das Ziel, Q 5, können Sie dies tun:

lemma "Q 5" 
    apply (rule foo) 

Dann wird der Zielzustand ein Teilziel haben, nämlich P 5.

Also, in Ihrem Fall sollte by (rule an_equation) den Trick tun. Etwas wie by (simp add: an_equation) oder using an_equation by simp oder using an_equation by blast würde wahrscheinlich auch funktionieren, aber im Allgemeinen etwas weniger robust sein, da der Simplifier zuerst andere Dinge tun kann und dann die Regel möglicherweise nicht mehr zutrifft.