|
section\<open>Examples of Classical Reasoning\<close>
theory FOL_examples imports FOL begin
lemma "EX y. ALL x. P(y)-->P(x)"
\<comment> \<open>@{subgoals[display,indent=0,margin=65]}\<close>
apply (rule exCI)
\<comment> \<open>@{subgoals[display,indent=0,margin=65]}\<close>
apply (rule allI)
\<comment> \<open>@{subgoals[display,indent=0,margin=65]}\<close>
apply (rule impI)
\<comment> \<open>@{subgoals[display,indent=0,margin=65]}\<close>
apply (erule allE)
\<comment> \<open>@{subgoals[display,indent=0,margin=65]}\<close>
txt\<open>see below for \<open>allI\<close> combined with \<open>swap\<close>\<close>
apply (erule allI [THEN [2] swap])
\<comment> \<open>@{subgoals[display,indent=0,margin=65]}\<close>
apply (rule impI)
\<comment> \<open>@{subgoals[display,indent=0,margin=65]}\<close>
apply (erule notE)
\<comment> \<open>@{subgoals[display,indent=0,margin=65]}\<close>
apply assumption
done
text \<open>
@{thm[display] allI [THEN [2] swap]}
\<close>
lemma "EX y. ALL x. P(y)-->P(x)"
by blast
end
¤ Dauer der Verarbeitung: 0.0 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
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.
|
