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