src/HOL/Isar_examples/BasicLogic.thy
 author wenzelm Sat Sep 25 13:18:38 1999 +0200 (1999-09-25) changeset 7604 55566b9ec7d7 parent 7480 0a0e0dbe1269 child 7740 2fbe5ce9845f permissions -rw-r--r--
tuned;
```     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 toy 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 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 section {* Examples from 'Introduction to Isabelle' *};
```
```   107
```
```   108 text {* '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 text {* '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 subsection {* '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
```
```   180 end;
```