Quelle  Tacticals.thy   Sprache: Isabelle

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