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;