Ist es möglich, eine Liste aller Prädikate und Funktionen zu erhalten, die ich von in Isabelle verwenden kann?Alle verfügbaren Prädikate in Isabelle
Weil es meistens passiert, dass ich anfange, von Hand ein Prädikat zu definieren, das ich für einen Beweis brauche (wie coprime), nur um zu bemerken, dass es bereits existiert.
Es gibt find_consts, die die definierten Konstanten entweder nach Typ oder nach Namen ähnlich wie find_theorems, z. find_consts "'a list => nat" oder find_consts name:"lim". Offenbar finden sich hier auch Abkürzungen wie coprime (Abkürzung für gcd a b = 1).
Natürlich kann dies nur Konstanten finden, die in einer der Theorien definiert wurden Sie tatsächlich geladen haben (entweder direkt oder indirekt). Es besteht immer die Möglichkeit, dass das von Ihnen benötigte Konzept bereits irgendwo in ~~/src/HOL/Library oder einem anderen Teil der Distribution oder im AFP formalisiert wurde.
Als ich vermute, dass dies der Fall ist, ich grep nur die Verteilung oder die AFP für einen entsprechenden Keyword oder frage ich jemanden, der es wissen könnte. Hier auf StackOverflow zu fragen, könnte auch eine gute Idee sein, etwas Ähnliches herauszufinden, da es eine Reihe von professionellen Isabelle-Benutzern gibt, die diese Site häufig besuchen und gute Kenntnisse darüber haben, was da ist und was nicht.
Das sind tolle Tipps, danke! Aber kannst du mir sagen, wo genau du 'Koprime' gefunden hast? Weil die Suche nach 'nat => nat 'den Koprime nicht zurückgegeben hat. Ich bin auch ein wenig verwirrt, warum "find_consts" Funktionen zurückgibt, anstatt Konstanten, wie ich es von der Benennung erwartet hätte. – nicht
Funktionen sind auch Konstanten, nur solche, die einen Funktionstyp haben. "Konstante" in Isabelle bedeutet nur, dass es ein Wert ist, der in der Hintergrundtheorie erklärt wurde, im Gegensatz zu z.B. eine gebundene oder freie Variable. –
Wenn überhaupt, sollten Sie nach 'nat ⇒ nat ⇒ bool' gesucht haben, um' 'coprime' zu finden. Leider funktioniert dies auch nicht, da die Koprimalität unter Verwendung der GCD definiert ist und GCD nicht auf "nat" sondern viel allgemeiner definiert ist. Der einzige vernünftige Weg, es zu finden, ist namentlich, d.h. 'find_consts name: coprime'. (Du könntest nach ''a ⇒' a ⇒ bool 'suchen, aber das wird so viel anderes zurückgeben, dass du dort nie etwas Nützliches findest) –