Aufrufen von Nitpick und Vorschlaghammer zusammen in Isabelle

Question

Wenn ich ein Lemma in Isabelle, gebe ich oft nitpick, und wenn das nicht mir ein Gegenbeispiel geben. Ich gebe dann sledgehammer ein, um zu versuchen, einen Beweis automatisch zu finden.

Ich frage mich: Ist es möglichNitpick und Vorschlaghammer zu berufen, so dass sie gleichzeitig ausgeführt werden? Seit Sledgehammer sendet bereits mein Lemma zu einer Reihe von automatischen Prüfer, könnte nicht einer dieser Prüfer tatsächlich ein Gegenbeispiel-Finder wie Nitpick sein?

Answer 1

Sie können den Befehl try in Isabelle verwenden; es läuft sledgehammer, nitpick, quickcheck und eine Anzahl anderer Löser (wie , simp, force, usw.) parallel, die Ihnen die Ergebnisse des ersten geben, der beendet.

Zum Beispiel läuft wie folgt zusammen:

lemma "(a * (b + 1)) = (a * b + a)" 
    try 

wird ein Gegenbeispiel aus nitpick zurückkehren, was darauf hinweist, dass der Satz in der Regel nicht wahr ist. Hinzufügen eines Typeinschränkung:

lemma "((a :: nat) * (b + 1)) = (a * b + a)" 
    try 

wird nun eine Nachricht zurückgeben Sie sagen, dass simp der Lage ist, das Ziel zu lösen.

Schließlich Ändern der Art Hindernis für die anspruchsvolleren 32 word Typ (erhältlich von Word in HOL-Word):

lemma "((a :: 32 word) * (b + 1)) = (a * b + a)" 
    try 

wird ein Ergebnis aus Vorschlaghammer zurückzukehren.