Deriving rules in Isabelle;

--- a/src/HOL/Isar_examples/BasicLogic.thy	Wed Jul 14 10:41:33 1999 +0200
+++ b/src/HOL/Isar_examples/BasicLogic.thy	Wed Jul 14 12:28:12 1999 +0200
@@ -8,6 +8,9 @@
 theory BasicLogic = Main:;
 
 
+text {* Just a few tiny examples to get an idea of how Isabelle/Isar
+  proof documents may look like. *};
+
 lemma I: "A --> A";
 proof;
   assume A;
@@ -24,7 +27,7 @@
 qed;
 
 lemma K': "A --> B --> A";
-proof single*;
+proof single+; txt {* better use sufficient-to-show here \dots *};
   assume A;
   show A; .;
 qed;
@@ -48,6 +51,8 @@
 qed;
 
 
+text {* Variations of backward vs.\ forward reasonong \dots *};
+
 lemma "A & B --> B & A";
 proof;
   assume "A & B";
@@ -77,7 +82,9 @@
 qed;
 
 
-text {* propositional proof (from 'Introduction to Isabelle') *};
+section {* Examples from 'Introduction to Isabelle' *};
+
+text {* 'Propositional proof' *};
 
 lemma "P | P --> P";
 proof;
@@ -97,7 +104,7 @@
 qed;
 
 
-text {* quantifier proof (from 'Introduction to Isabelle') *};
+text {* 'Quantifier proof' *};
 
 lemma "(EX x. P(f(x))) --> (EX x. P(x))";
 proof;
@@ -125,4 +132,28 @@
   by blast;
 
 
+subsection {* 'Deriving rules in Isabelle' *};
+
+text {* We derive the conjunction elimination rule from the
+ projections.  The proof below follows the basic reasoning of the
+ script given in the Isabelle Intro Manual closely.  Although, the
+ actual underlying operations on rules and proof states are quite
+ different: Isabelle/Isar supports non-atomic goals and assumptions
+ fully transparently, while the original Isabelle classic script
+ depends on the primitive goal command to decompose the rule into
+ premises and conclusion, with the result emerging by discharging the
+ context again later. *};
+
+theorem conjE: "A & B ==> (A ==> B ==> C) ==> C";
+proof same;
+  assume ab: "A & B";
+  assume ab_c: "A ==> B ==> C";
+  show C;
+  proof (rule ab_c);
+    from ab; show A; ..;
+    from ab; show B; ..;
+  qed;
+qed;
+
+
 end;