# HG changeset patch # User paulson # Date 980157665 -3600 # Node ID 1db8b894ada091bf72ec09e12297b0023443c67f # Parent 36741b4fe1091e6ce61d7f0c012ba2f622cdcdb8 new examples theory Rules/Tacticals.thy diff -r 36741b4fe109 -r 1db8b894ada0 doc-src/TutorialI/IsaMakefile --- a/doc-src/TutorialI/IsaMakefile Sun Jan 21 19:55:25 2001 +0100 +++ b/doc-src/TutorialI/IsaMakefile Mon Jan 22 11:01:05 2001 +0100 @@ -115,8 +115,8 @@ HOL-Rules: HOL $(LOG)/HOL-Rules.gz $(LOG)/HOL-Rules.gz: $(OUT)/HOL Rules/Basic.thy \ - Rules/Blast.thy Rules/Force.thy Rules/Primes.thy Rules/Forward.thy \ - Rules/ROOT.ML + Rules/Blast.thy Rules/Force.thy Rules/Primes.thy Rules/Forward.thy \ + Rules/Tacticals.thy Rules/ROOT.ML @$(USEDIR) Rules @rm -f tutorial.dvi diff -r 36741b4fe109 -r 1db8b894ada0 doc-src/TutorialI/Rules/ROOT.ML --- a/doc-src/TutorialI/Rules/ROOT.ML Sun Jan 21 19:55:25 2001 +0100 +++ b/doc-src/TutorialI/Rules/ROOT.ML Mon Jan 22 11:01:05 2001 +0100 @@ -3,4 +3,5 @@ use_thy "Blast"; use_thy "Force"; use_thy "Forward"; +use_thy "Tacticals"; diff -r 36741b4fe109 -r 1db8b894ada0 doc-src/TutorialI/Rules/Tacticals.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/TutorialI/Rules/Tacticals.thy Mon Jan 22 11:01:05 2001 +0100 @@ -0,0 +1,51 @@ +theory Tacticals = Main: + +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?, assumption+)+ + +text{*defer and prefer*} + +lemma "hard \ (P \ ~P) \ (Q\Q)" +apply intro --{* @{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 --{* @{subgoals[display,indent=0,margin=65]} *} +prefer 3 --{* @{subgoals[display,indent=0,margin=65]} *} +oops + + + +(*needed??*) + +lemma "(P\Q) \ (R\S) \ PP" +apply elim +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