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