use_thy "gcd"; goalw thy [divides_def] "x divides 0"; br exI 1; br (mult_0 RS sym) 1; result();Wichtig: einen Beweis immer mit result() oder qed() abschliessen. No subgoals heisst nicht notwendigerweise, das der Beweis erfolgreich war. Hier ist ein Gegenbeispiel:
use_thy "gcd"; goal thy "x divides 0"; by (rewrite_tac [divides_def]); br exI 1; br (mult_0 RS sym) 1; result();
Der Schlüssel ist hier, die richtige Unfikation für die Substitutionsregel zu finden:
val [p]= goal thy "r=s ==> s=r"; br subst 1; back(); back(); br p 1; br refl 1; result();
Eine andere Möglichkeit ist Verwendung von res_inst_tac. Bei dieser Taktik kann man der Unifikation eine Substitution, geschrieben als eine Liste von Paaren bestehend aus dem Variablennamen (ohne das Fragezeichen) und einem Wert, vorgeben.
val [p1,p2]= goal thy "[| r= s; s= t |] ==> r= t"; by (res_inst_tac [("P", "%x. r= x")] subst 1); br p2 1; br p1 1; result();
Hier vergessen wir die Prämissen und verwenden wir mal premises().
goalw thy [Ex_def] "P x==> ? x. P x"; br selectI 1; br (hd(premises())) 1; result();Die Eliminationsregel (genauer gesagt, die Destruktionsregel) des Allquantors erfordert die Kongruenz der Funktionsapplikation, und wieder eine Suche nach der richtigen Unifikation:
val [p]= goalw thy [All_def] "! x. P(x)==> P(y)"; br eqTrueE 1; br fun_cong 1; back(); back(); br p 1; result();
val [p]= goal thy "x=y ==> f(x)= f(y)"; br (p RS subst) 1; br refl 1; result();Dieses Verfahren läßt sich auch einfach auf den zweiten Beweis verallgemeinern:
val [p1,p2]= goal thy "[| x= y; f= g |] ==> f x= g y"; br (p1 RS subst) 1; br (p2 RS subst) 1; br refl 1; result();
goal thy "(A|B)&~A-->B"; br impI 1; be conjE 1; Level 2 (A | B) & ~ A --> B 1. [| A | B; ~ A |] ==> B val it = () : unitEine Rückwärtsresolution mit conjE erzeugt jetzt nur eine Konjunktion mit einer Meta-Variablen, die später wieder durch Rückwärtsresolution mit conjI bewiesen werden muß. Das ist überflüssig, wir können vielmehr direkt mit der Elimination der Disjunktion, gefolgt von der Elimination der Negation, forfahren. Der Rest folgt dann durch Annahme:
be disjE 1; be notE 1; ba 1; ba 1; result();