src/HOL/Isar_examples/BasicLogic.thy
author wenzelm
Fri Aug 20 15:42:46 1999 +0200 (1999-08-20)
changeset 7306 cd0533d52e55
parent 7233 75cc3a327bd4
child 7449 ebd975549ffe
permissions -rw-r--r--
intro (no +);
     1 (*  Title:      HOL/Isar_examples/BasicLogic.thy
     2     ID:         $Id$
     3     Author:     Markus Wenzel, TU Muenchen
     4 
     5 Basic propositional and quantifier reasoning.
     6 *)
     7 
     8 theory BasicLogic = Main:;
     9 
    10 
    11 text {* Just a few tiny examples to get an idea of how Isabelle/Isar
    12   proof documents may look like. *};
    13 
    14 lemma I: "A --> A";
    15 proof;
    16   assume A;
    17   show A; .;
    18 qed;
    19 
    20 lemma K: "A --> B --> A";
    21 proof;
    22   assume A;
    23   show "B --> A";
    24   proof;
    25     show A; .;
    26   qed;
    27 qed;
    28 
    29 lemma K': "A --> B --> A";
    30 proof intro;
    31   assume A;
    32   show A; .;
    33 qed;
    34 
    35 lemma S: "(A --> B --> C) --> (A --> B) --> A --> C";
    36 proof;
    37   assume "A --> B --> C";
    38   show "(A --> B) --> A --> C";
    39   proof;
    40     assume "A --> B";
    41     show "A --> C";
    42     proof;
    43       assume A;
    44       show C;
    45       proof (rule mp);
    46 	show "B --> C"; by (rule mp);
    47         show B; by (rule mp);
    48       qed;
    49     qed;
    50   qed;
    51 qed;
    52 
    53 
    54 text {* Variations of backward vs.\ forward reasonong \dots *};
    55 
    56 lemma "A & B --> B & A";
    57 proof;
    58   assume "A & B";
    59   show "B & A";
    60   proof;
    61     show B; by (rule conjunct2);
    62     show A; by (rule conjunct1);
    63   qed;
    64 qed;
    65 
    66 lemma "A & B --> B & A";
    67 proof;
    68   assume "A & B";
    69   then; show "B & A";
    70   proof;
    71     assume A B;
    72     show ??thesis; ..;
    73   qed;
    74 qed;
    75 
    76 lemma "A & B --> B & A";
    77 proof;
    78   assume ab: "A & B";
    79   from ab; have a: A; ..;
    80   from ab; have b: B; ..;
    81   from b a; show "B & A"; ..;
    82 qed;
    83 
    84 
    85 section {* Examples from 'Introduction to Isabelle' *};
    86 
    87 text {* 'Propositional proof' *};
    88 
    89 lemma "P | P --> P";
    90 proof;
    91   assume "P | P";
    92   then; show P;
    93   proof;
    94     assume P;
    95     show P; .;
    96     show P; .;
    97   qed;
    98 qed;
    99 
   100 lemma "P | P --> P";
   101 proof;
   102   assume "P | P";
   103   then; show P; ..;
   104 qed;
   105 
   106 
   107 text {* 'Quantifier proof' *};
   108 
   109 lemma "(EX x. P(f(x))) --> (EX x. P(x))";
   110 proof;
   111   assume "EX x. P(f(x))";
   112   then; show "EX x. P(x)";
   113   proof (rule exE);
   114     fix a;
   115     assume "P(f(a))" (is "P(??witness)");
   116     show ??thesis; by (rule exI [of P ??witness]);
   117   qed;
   118 qed;
   119 
   120 lemma "(EX x. P(f(x))) --> (EX x. P(x))";
   121 proof;
   122   assume "EX x. P(f(x))";
   123   then; show "EX x. P(x)";
   124   proof;
   125     fix a;
   126     assume "P(f(a))";
   127     show ??thesis; ..;
   128   qed;
   129 qed;
   130 
   131 lemma "(EX x. P(f(x))) --> (EX x. P(x))";
   132   by blast;
   133 
   134 
   135 subsection {* 'Deriving rules in Isabelle' *};
   136 
   137 text {* We derive the conjunction elimination rule from the
   138  projections.  The proof below follows the basic reasoning of the
   139  script given in the Isabelle Intro Manual closely.  Although, the
   140  actual underlying operations on rules and proof states are quite
   141  different: Isabelle/Isar supports non-atomic goals and assumptions
   142  fully transparently, while the original Isabelle classic script
   143  depends on the primitive goal command to decompose the rule into
   144  premises and conclusion, with the result emerging by discharging the
   145  context again later. *};
   146 
   147 theorem conjE: "A & B ==> (A ==> B ==> C) ==> C";
   148 proof -;
   149   assume ab: "A & B";
   150   assume ab_c: "A ==> B ==> C";
   151   show C;
   152   proof (rule ab_c);
   153     from ab; show A; ..;
   154     from ab; show B; ..;
   155   qed;
   156 qed;
   157 
   158 
   159 end;