Theory Tacticals

theory Tacticals imports Main begin

text‹REPEAT›
lemma "PQ; QR; RS; P  S"
apply (drule mp, assumption)
apply (drule mp, assumption)
apply (drule mp, assumption)
apply (assumption)
done

lemma "PQ; QR; RS; P  S"
by (drule mp, assumption)+

text‹ORELSE with REPEAT›
lemma "QR; PQ; x<5P;  Suc x < 5  R" 
by (drule mp, (assumption|arith))+

text‹exercise: what's going on here?›
lemma "PQR; PQ; P  R"
by (drule mp, (intro conjI)?, assumption+)+

text‹defer and prefer›

lemma "hard  (P  ~P)  (QQ)"
apply (intro conjI)   ― ‹@{subgoals[display,indent=0,margin=65]}
defer 1   ― ‹@{subgoals[display,indent=0,margin=65]}
apply blast+   ― ‹@{subgoals[display,indent=0,margin=65]}
oops

lemma "ok1  ok2  doubtful"
apply (intro conjI)   ― ‹@{subgoals[display,indent=0,margin=65]}
prefer 3   ― ‹@{subgoals[display,indent=0,margin=65]}
oops

lemma "bigsubgoal1  bigsubgoal2  bigsubgoal3  bigsubgoal4  bigsubgoal5  bigsubgoal6"
apply (intro conjI)   ― ‹@{subgoals[display,indent=0,margin=65]}
txt@{subgoals[display,indent=0,margin=65]} 
A total of 6 subgoals...
›
oops



(*needed??*)

lemma "(PQ)  (RS)  PP"
apply (elim conjE disjE)
oops

lemma "((PQ)  R)  (Q  (PS))  PP"
apply (elim conjE)
oops

lemma "((PQ)  R)  (Q  (PS))  PP"
apply (erule conjE)+
oops

end