src/HOL/Isar_examples/BasicLogic.thy
 changeset 7001 8121e11ed765 parent 6892 4a905b4a39c8 child 7005 cc778d613217
```     1.1 --- a/src/HOL/Isar_examples/BasicLogic.thy	Wed Jul 14 10:41:33 1999 +0200
1.2 +++ b/src/HOL/Isar_examples/BasicLogic.thy	Wed Jul 14 12:28:12 1999 +0200
1.3 @@ -8,6 +8,9 @@
1.4  theory BasicLogic = Main:;
1.5
1.6
1.7 +text {* Just a few tiny examples to get an idea of how Isabelle/Isar
1.8 +  proof documents may look like. *};
1.9 +
1.10  lemma I: "A --> A";
1.11  proof;
1.12    assume A;
1.13 @@ -24,7 +27,7 @@
1.14  qed;
1.15
1.16  lemma K': "A --> B --> A";
1.17 -proof single*;
1.18 +proof single+; txt {* better use sufficient-to-show here \dots *};
1.19    assume A;
1.20    show A; .;
1.21  qed;
1.22 @@ -48,6 +51,8 @@
1.23  qed;
1.24
1.25
1.26 +text {* Variations of backward vs.\ forward reasonong \dots *};
1.27 +
1.28  lemma "A & B --> B & A";
1.29  proof;
1.30    assume "A & B";
1.31 @@ -77,7 +82,9 @@
1.32  qed;
1.33
1.34
1.35 -text {* propositional proof (from 'Introduction to Isabelle') *};
1.36 +section {* Examples from 'Introduction to Isabelle' *};
1.37 +
1.38 +text {* 'Propositional proof' *};
1.39
1.40  lemma "P | P --> P";
1.41  proof;
1.42 @@ -97,7 +104,7 @@
1.43  qed;
1.44
1.45
1.46 -text {* quantifier proof (from 'Introduction to Isabelle') *};
1.47 +text {* 'Quantifier proof' *};
1.48
1.49  lemma "(EX x. P(f(x))) --> (EX x. P(x))";
1.50  proof;
1.51 @@ -125,4 +132,28 @@
1.52    by blast;
1.53
1.54
1.55 +subsection {* 'Deriving rules in Isabelle' *};
1.56 +
1.57 +text {* We derive the conjunction elimination rule from the
1.58 + projections.  The proof below follows the basic reasoning of the
1.59 + script given in the Isabelle Intro Manual closely.  Although, the
1.60 + actual underlying operations on rules and proof states are quite
1.61 + different: Isabelle/Isar supports non-atomic goals and assumptions
1.62 + fully transparently, while the original Isabelle classic script
1.63 + depends on the primitive goal command to decompose the rule into
1.64 + premises and conclusion, with the result emerging by discharging the
1.65 + context again later. *};
1.66 +
1.67 +theorem conjE: "A & B ==> (A ==> B ==> C) ==> C";
1.68 +proof same;
1.69 +  assume ab: "A & B";
1.70 +  assume ab_c: "A ==> B ==> C";
1.71 +  show C;
1.72 +  proof (rule ab_c);
1.73 +    from ab; show A; ..;
1.74 +    from ab; show B; ..;
1.75 +  qed;
1.76 +qed;
1.77 +
1.78 +
1.79  end;
```