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;
```