Theory Tacticals

theory Tacticals imports Main begin

text‹REPEAT›
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‹ORELSE with REPEAT›
lemma "⟦Q⟶R; P⟶Q; x<5⟶P;  Suc x < 5⟧ ⟹ R" 
by (drule mp, (assumption|arith))+

text‹exercise: what's going on here?›
lemma "⟦P∧Q⟶R; P⟶Q; P⟧ ⟹ R"
by (drule mp, (intro conjI)?, assumption+)+

text‹defer and prefer›

lemma "hard ∧ (P ∨ ~P) ∧ (Q⟶Q)"
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 "(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