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;
wenzelm@6444
     1
(*  Title:      HOL/Isar_examples/BasicLogic.thy
wenzelm@6444
     2
    ID:         $Id$
wenzelm@6444
     3
    Author:     Markus Wenzel, TU Muenchen
wenzelm@6444
     4
wenzelm@6444
     5
Basic propositional and quantifier reasoning.
wenzelm@6444
     6
*)
wenzelm@6444
     7
wenzelm@7748
     8
header {* Basic reasoning *};
wenzelm@7748
     9
wenzelm@6444
    10
theory BasicLogic = Main:;
wenzelm@6444
    11
wenzelm@7761
    12
wenzelm@7740
    13
subsection {* Some trivialities *};
wenzelm@7740
    14
wenzelm@7604
    15
text {* Just a few toy examples to get an idea of how Isabelle/Isar
wenzelm@7001
    16
  proof documents may look like. *};
wenzelm@7001
    17
wenzelm@6444
    18
lemma I: "A --> A";
wenzelm@6444
    19
proof;
wenzelm@6444
    20
  assume A;
wenzelm@6444
    21
  show A; .;
wenzelm@6444
    22
qed;
wenzelm@6444
    23
wenzelm@6444
    24
lemma K: "A --> B --> A";
wenzelm@6444
    25
proof;
wenzelm@6444
    26
  assume A;
wenzelm@6444
    27
  show "B --> A";
wenzelm@6444
    28
  proof;
wenzelm@6444
    29
    show A; .;
wenzelm@6444
    30
  qed;
wenzelm@6444
    31
qed;
wenzelm@6444
    32
wenzelm@6504
    33
lemma K': "A --> B --> A";
wenzelm@7449
    34
proof;
wenzelm@7449
    35
  assume A;
wenzelm@7449
    36
  thus "B --> A"; ..;
wenzelm@7449
    37
qed;
wenzelm@7449
    38
wenzelm@7449
    39
lemma K'': "A --> B --> A";
wenzelm@7306
    40
proof intro;
wenzelm@6444
    41
  assume A;
wenzelm@6444
    42
  show A; .;
wenzelm@6444
    43
qed;
wenzelm@6444
    44
wenzelm@7449
    45
lemma K''': "A --> B --> A";
wenzelm@7449
    46
  by intro;
wenzelm@7449
    47
wenzelm@6444
    48
lemma S: "(A --> B --> C) --> (A --> B) --> A --> C";
wenzelm@6444
    49
proof;
wenzelm@6444
    50
  assume "A --> B --> C";
wenzelm@6444
    51
  show "(A --> B) --> A --> C";
wenzelm@6444
    52
  proof;
wenzelm@6444
    53
    assume "A --> B";
wenzelm@6444
    54
    show "A --> C";
wenzelm@6444
    55
    proof;
wenzelm@6444
    56
      assume A;
wenzelm@6444
    57
      show C;
wenzelm@6444
    58
      proof (rule mp);
wenzelm@6444
    59
	show "B --> C"; by (rule mp);
wenzelm@6444
    60
        show B; by (rule mp);
wenzelm@6444
    61
      qed;
wenzelm@6444
    62
    qed;
wenzelm@6444
    63
  qed;
wenzelm@6444
    64
qed;
wenzelm@6444
    65
wenzelm@7761
    66
wenzelm@7761
    67
subsection {* Variations of backward vs.\ forward reasoning \dots *};
wenzelm@7001
    68
wenzelm@6444
    69
lemma "A & B --> B & A";
wenzelm@6444
    70
proof;
wenzelm@6444
    71
  assume "A & B";
wenzelm@6444
    72
  show "B & A";
wenzelm@6444
    73
  proof;
wenzelm@6444
    74
    show B; by (rule conjunct2);
wenzelm@6444
    75
    show A; by (rule conjunct1);
wenzelm@6444
    76
  qed;
wenzelm@6444
    77
qed;
wenzelm@6444
    78
wenzelm@6444
    79
lemma "A & B --> B & A";
wenzelm@6444
    80
proof;
wenzelm@6444
    81
  assume "A & B";
wenzelm@6444
    82
  then; show "B & A";
wenzelm@6444
    83
  proof;
wenzelm@6444
    84
    assume A B;
wenzelm@7480
    85
    show ?thesis; ..;
wenzelm@6444
    86
  qed;
wenzelm@6444
    87
qed;
wenzelm@6444
    88
wenzelm@6444
    89
lemma "A & B --> B & A";
wenzelm@6444
    90
proof;
wenzelm@7604
    91
  assume "A & B";
wenzelm@7604
    92
  show "B & A";
wenzelm@7604
    93
  proof;
wenzelm@7604
    94
    from prems; show B; ..;
wenzelm@7604
    95
    from prems; show A; ..;
wenzelm@7604
    96
  qed;
wenzelm@7604
    97
qed;
wenzelm@7604
    98
wenzelm@7604
    99
lemma "A & B --> B & A";
wenzelm@7604
   100
proof;
wenzelm@6892
   101
  assume ab: "A & B";
wenzelm@6892
   102
  from ab; have a: A; ..;
wenzelm@6892
   103
  from ab; have b: B; ..;
wenzelm@6892
   104
  from b a; show "B & A"; ..;
wenzelm@6444
   105
qed;
wenzelm@6444
   106
wenzelm@6444
   107
wenzelm@7740
   108
subsection {* A few examples from ``Introduction to Isabelle'' *};
wenzelm@7001
   109
wenzelm@7740
   110
subsubsection {* Propositional proof *};
wenzelm@6444
   111
wenzelm@6444
   112
lemma "P | P --> P";
wenzelm@6444
   113
proof;
wenzelm@6444
   114
  assume "P | P";
wenzelm@6444
   115
  then; show P;
wenzelm@6444
   116
  proof;
wenzelm@6444
   117
    assume P;
wenzelm@6444
   118
    show P; .;
wenzelm@6444
   119
    show P; .;
wenzelm@6444
   120
  qed;
wenzelm@6444
   121
qed;
wenzelm@6444
   122
wenzelm@6444
   123
lemma "P | P --> P";
wenzelm@6444
   124
proof;
wenzelm@6444
   125
  assume "P | P";
wenzelm@6444
   126
  then; show P; ..;
wenzelm@6444
   127
qed;
wenzelm@6444
   128
wenzelm@6444
   129
wenzelm@7740
   130
subsubsection {* Quantifier proof *};
wenzelm@6444
   131
wenzelm@6444
   132
lemma "(EX x. P(f(x))) --> (EX x. P(x))";
wenzelm@6444
   133
proof;
wenzelm@6444
   134
  assume "EX x. P(f(x))";
wenzelm@6444
   135
  then; show "EX x. P(x)";
wenzelm@6444
   136
  proof (rule exE);
wenzelm@6444
   137
    fix a;
wenzelm@7480
   138
    assume "P(f(a))" (is "P(?witness)");
wenzelm@7480
   139
    show ?thesis; by (rule exI [of P ?witness]);
wenzelm@6444
   140
  qed;
wenzelm@6444
   141
qed;
wenzelm@6444
   142
wenzelm@6444
   143
lemma "(EX x. P(f(x))) --> (EX x. P(x))";
wenzelm@6444
   144
proof;
wenzelm@6444
   145
  assume "EX x. P(f(x))";
wenzelm@6444
   146
  then; show "EX x. P(x)";
wenzelm@6444
   147
  proof;
wenzelm@6444
   148
    fix a;
wenzelm@6444
   149
    assume "P(f(a))";
wenzelm@7480
   150
    show ?thesis; ..;
wenzelm@6444
   151
  qed;
wenzelm@6444
   152
qed;
wenzelm@6444
   153
wenzelm@6444
   154
lemma "(EX x. P(f(x))) --> (EX x. P(x))";
wenzelm@6504
   155
  by blast;
wenzelm@6444
   156
wenzelm@6444
   157
wenzelm@7740
   158
subsubsection {* Deriving rules in Isabelle *};
wenzelm@7001
   159
wenzelm@7001
   160
text {* We derive the conjunction elimination rule from the
wenzelm@7001
   161
 projections.  The proof below follows the basic reasoning of the
wenzelm@7001
   162
 script given in the Isabelle Intro Manual closely.  Although, the
wenzelm@7001
   163
 actual underlying operations on rules and proof states are quite
wenzelm@7001
   164
 different: Isabelle/Isar supports non-atomic goals and assumptions
wenzelm@7001
   165
 fully transparently, while the original Isabelle classic script
wenzelm@7001
   166
 depends on the primitive goal command to decompose the rule into
wenzelm@7001
   167
 premises and conclusion, with the result emerging by discharging the
wenzelm@7001
   168
 context again later. *};
wenzelm@7001
   169
wenzelm@7001
   170
theorem conjE: "A & B ==> (A ==> B ==> C) ==> C";
wenzelm@7133
   171
proof -;
wenzelm@7001
   172
  assume ab: "A & B";
wenzelm@7001
   173
  assume ab_c: "A ==> B ==> C";
wenzelm@7001
   174
  show C;
wenzelm@7001
   175
  proof (rule ab_c);
wenzelm@7001
   176
    from ab; show A; ..;
wenzelm@7001
   177
    from ab; show B; ..;
wenzelm@7001
   178
  qed;
wenzelm@7001
   179
qed;
wenzelm@7001
   180
wenzelm@6444
   181
end;