src/HOL/Isar_examples/BasicLogic.thy
author wenzelm
Sat Sep 04 21:13:01 1999 +0200 (1999-09-04)
changeset 7480 0a0e0dbe1269
parent 7449 ebd975549ffe
child 7604 55566b9ec7d7
permissions -rw-r--r--
replaced ?? by ?;
     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 
    21 lemma K: "A --> B --> A";
    22 proof;
    23   assume A;
    24   show "B --> A";
    25   proof;
    26     show A; .;
    27   qed;
    28 qed;
    29 
    30 lemma K': "A --> B --> A";
    31 proof;
    32   assume A;
    33   thus "B --> A"; ..;
    34 qed;
    35 
    36 lemma K'': "A --> B --> A";
    37 proof intro;
    38   assume A;
    39   show A; .;
    40 qed;
    41 
    42 lemma K''': "A --> B --> A";
    43   by intro;
    44 
    45 
    46 lemma S: "(A --> B --> C) --> (A --> B) --> A --> C";
    47 proof;
    48   assume "A --> B --> C";
    49   show "(A --> B) --> A --> C";
    50   proof;
    51     assume "A --> B";
    52     show "A --> C";
    53     proof;
    54       assume A;
    55       show C;
    56       proof (rule mp);
    57 	show "B --> C"; by (rule mp);
    58         show B; by (rule mp);
    59       qed;
    60     qed;
    61   qed;
    62 qed;
    63 
    64 
    65 text {* Variations of backward vs.\ forward reasonong \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 ab: "A & B";
    90   from ab; have a: A; ..;
    91   from ab; have b: B; ..;
    92   from b a; show "B & A"; ..;
    93 qed;
    94 
    95 
    96 section {* Examples from 'Introduction to Isabelle' *};
    97 
    98 text {* 'Propositional proof' *};
    99 
   100 lemma "P | P --> P";
   101 proof;
   102   assume "P | P";
   103   then; show P;
   104   proof;
   105     assume P;
   106     show P; .;
   107     show P; .;
   108   qed;
   109 qed;
   110 
   111 lemma "P | P --> P";
   112 proof;
   113   assume "P | P";
   114   then; show P; ..;
   115 qed;
   116 
   117 
   118 text {* 'Quantifier proof' *};
   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 (rule exE);
   125     fix a;
   126     assume "P(f(a))" (is "P(?witness)");
   127     show ?thesis; by (rule exI [of P ?witness]);
   128   qed;
   129 qed;
   130 
   131 lemma "(EX x. P(f(x))) --> (EX x. P(x))";
   132 proof;
   133   assume "EX x. P(f(x))";
   134   then; show "EX x. P(x)";
   135   proof;
   136     fix a;
   137     assume "P(f(a))";
   138     show ?thesis; ..;
   139   qed;
   140 qed;
   141 
   142 lemma "(EX x. P(f(x))) --> (EX x. P(x))";
   143   by blast;
   144 
   145 
   146 subsection {* 'Deriving rules in Isabelle' *};
   147 
   148 text {* We derive the conjunction elimination rule from the
   149  projections.  The proof below follows the basic reasoning of the
   150  script given in the Isabelle Intro Manual closely.  Although, the
   151  actual underlying operations on rules and proof states are quite
   152  different: Isabelle/Isar supports non-atomic goals and assumptions
   153  fully transparently, while the original Isabelle classic script
   154  depends on the primitive goal command to decompose the rule into
   155  premises and conclusion, with the result emerging by discharging the
   156  context again later. *};
   157 
   158 theorem conjE: "A & B ==> (A ==> B ==> C) ==> C";
   159 proof -;
   160   assume ab: "A & B";
   161   assume ab_c: "A ==> B ==> C";
   162   show C;
   163   proof (rule ab_c);
   164     from ab; show A; ..;
   165     from ab; show B; ..;
   166   qed;
   167 qed;
   168 
   169 
   170 end;