--- 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;