author wenzelm Wed, 14 Jul 1999 12:28:12 +0200 changeset 7001 8121e11ed765 parent 7000 6920cf9b8623 child 7002 01a4e15ee253
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;```