theory Tacticals imports Main begin
text\<open>REPEAT\<close>
lemma "\P\Q; Q\R; R\S; P\ \ S"
apply (drule mp, assumption)
apply (drule mp, assumption)
apply (drule mp, assumption)
apply (assumption)
done
lemma "\P\Q; Q\R; R\S; P\ \ S"
by (drule mp, assumption)+
text\<open>ORELSE with REPEAT\<close>
lemma "\Q\R; P\Q; x<5\P; Suc x < 5\ \ R"
by (drule mp, (assumption|arith))+
text\<open>exercise: what's going on here?\<close>
lemma "\P\Q\R; P\Q; P\ \ R"
by (drule mp, (intro conjI)?, assumption+)+
text\<open>defer and prefer\<close>
lemma "hard \ (P \ ~P) \ (Q\Q)"
apply (intro conjI) \<comment> \<open>@{subgoals[display,indent=0,margin=65]}\<close>
defer 1 \<comment> \<open>@{subgoals[display,indent=0,margin=65]}\<close>
apply blast+ \<comment> \<open>@{subgoals[display,indent=0,margin=65]}\<close>
oops
lemma "ok1 \ ok2 \ doubtful"
apply (intro conjI) \<comment> \<open>@{subgoals[display,indent=0,margin=65]}\<close>
prefer 3 \<comment> \<open>@{subgoals[display,indent=0,margin=65]}\<close>
oops
lemma "bigsubgoal1 \ bigsubgoal2 \ bigsubgoal3 \ bigsubgoal4 \ bigsubgoal5 \ bigsubgoal6"
apply (intro conjI) \<comment> \<open>@{subgoals[display,indent=0,margin=65]}\<close>
txt\<open>@{subgoals[display,indent=0,margin=65]}
A total of 6 subgoals...
\<close>
oops
(*needed??*)
lemma "(P\Q) \ (R\S) \ PP"
apply (elim conjE disjE)
oops
lemma "((P\Q) \ R) \ (Q \ (P\S)) \ PP"
apply (elim conjE)
oops
lemma "((P\Q) \ R) \ (Q \ (P\S)) \ PP"
apply (erule conjE)+
oops
end
¤ Dauer der Verarbeitung: 0.15 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.
|
