(*Correct version, delaying use of "spec" until last*)
schematic_goal "?p : (ALL x y. P(x,y)) --> (ALL z w. P(w,z))" apply (rule impI) apply (rule allI) apply (rule allI) apply (drule spec) apply (drule spec) apply assumption done
subsubsection \<open>Demonstration of \<open>fast\<close>\<close>
schematic_goal "?p : (EX y. ALL x. J(y,x) <-> ~J(x,x))
--> ~ (ALL x. EX y. ALL z. J(z,y) <-> ~ J(z,x))" apply (tactic \<open>fast_tac \<^context> FOLP_cs 1\<close>) done
schematic_goal "?p : ALL x. P(x,f(x)) <->
(EX y. (ALL z. P(z,y) --> P(z,f(x))) & P(x,y))" apply (tactic \<open>fast_tac \<^context> FOLP_cs 1\<close>) done
subsubsection \<open>Derivation of conjunction elimination rule\<close>
schematic_goal assumes major: "p : P&Q" and minor: "!!x y. [| x : P; y : Q |] ==> f(x, y) : R" shows"?p : R" apply (rule minor) apply (rule major [THEN conjunct1]) apply (rule major [THEN conjunct2]) done
text\<open>Alternative proof of the result above\<close>
schematic_goal assumes major: "p : ~P" and minor: "q : P" shows"?p : R" apply (rule minor [THEN major [unfolded not_def, THEN mp, THEN FalseE]]) done
end
¤ Dauer der Verarbeitung: 0.2 Sekunden
(vorverarbeitet)
¤
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
