# 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 "\<lbrakk>(P\<longrightarrow>Q); (Q\<longrightarrow>R); (R\<longrightarrow>S); P\<rbrakk> \<Longrightarrow> S"
+apply (drule mp, assumption)
+apply (drule mp, assumption)
+apply (drule mp, assumption)
+apply (assumption)
+done
+
+lemma "\<lbrakk>(P\<longrightarrow>Q); (Q\<longrightarrow>R); (R\<longrightarrow>S); P\<rbrakk> \<Longrightarrow> S"
+by (drule mp, assumption)+
+
+text{*ORELSE with REPEAT*}
+lemma "\<lbrakk>(Q\<longrightarrow>R); (P\<longrightarrow>Q); x<#5\<longrightarrow>P;  Suc x < #5\<rbrakk> \<Longrightarrow> R" 
+by (drule mp, (assumption|arith))+
+
+text{*exercise: what's going on here?*}
+lemma "\<lbrakk>(P\<and>Q\<longrightarrow>R); (P\<longrightarrow>Q); P\<rbrakk> \<Longrightarrow> R"
+by (drule mp, intro?, assumption+)+
+
+text{*defer and prefer*}
+
+lemma "hard \<and> (P \<or> ~P) \<and> (Q\<longrightarrow>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 \<and> ok2 \<and> doubtful"
+apply intro   --{* @{subgoals[display,indent=0,margin=65]} *}
+prefer 3   --{* @{subgoals[display,indent=0,margin=65]} *}
+oops
+
+
+
+(*needed??*)
+
+lemma "(P\<or>Q) \<and> (R\<or>S) \<Longrightarrow> PP"
+apply elim
+oops
+
+lemma "((P\<or>Q) \<and> R) \<and> (Q \<and> (P\<or>S)) \<Longrightarrow> PP"
+apply (elim conjE)
+oops
+
+lemma "((P\<or>Q) \<and> R) \<and> (Q \<and> (P\<or>S)) \<Longrightarrow> PP"
+apply (erule conjE)+
+oops
+
+end