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]} \<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 quality 100%
¤ Dauer der Verarbeitung: 0.15 Sekunden
(vorverarbeitet)
¤ *© Formatika GbR, Deutschland
