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