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