src/HOL/Isar_examples/BasicLogic.thy
author wenzelm
Wed Jul 14 12:28:12 1999 +0200 (1999-07-14)
changeset 7001 8121e11ed765
parent 6892 4a905b4a39c8
child 7005 cc778d613217
permissions -rw-r--r--
Deriving rules in Isabelle;
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@6444
     8
theory BasicLogic = Main:;
wenzelm@6444
     9
wenzelm@6444
    10
wenzelm@7001
    11
text {* Just a few tiny examples to get an idea of how Isabelle/Isar
wenzelm@7001
    12
  proof documents may look like. *};
wenzelm@7001
    13
wenzelm@6444
    14
lemma I: "A --> A";
wenzelm@6444
    15
proof;
wenzelm@6444
    16
  assume A;
wenzelm@6444
    17
  show A; .;
wenzelm@6444
    18
qed;
wenzelm@6444
    19
wenzelm@6444
    20
lemma K: "A --> B --> A";
wenzelm@6444
    21
proof;
wenzelm@6444
    22
  assume A;
wenzelm@6444
    23
  show "B --> A";
wenzelm@6444
    24
  proof;
wenzelm@6444
    25
    show A; .;
wenzelm@6444
    26
  qed;
wenzelm@6444
    27
qed;
wenzelm@6444
    28
wenzelm@6504
    29
lemma K': "A --> B --> A";
wenzelm@7001
    30
proof single+; txt {* better use sufficient-to-show here \dots *};
wenzelm@6444
    31
  assume A;
wenzelm@6444
    32
  show A; .;
wenzelm@6444
    33
qed;
wenzelm@6444
    34
wenzelm@6444
    35
lemma S: "(A --> B --> C) --> (A --> B) --> A --> C";
wenzelm@6444
    36
proof;
wenzelm@6444
    37
  assume "A --> B --> C";
wenzelm@6444
    38
  show "(A --> B) --> A --> C";
wenzelm@6444
    39
  proof;
wenzelm@6444
    40
    assume "A --> B";
wenzelm@6444
    41
    show "A --> C";
wenzelm@6444
    42
    proof;
wenzelm@6444
    43
      assume A;
wenzelm@6444
    44
      show C;
wenzelm@6444
    45
      proof (rule mp);
wenzelm@6444
    46
	show "B --> C"; by (rule mp);
wenzelm@6444
    47
        show B; by (rule mp);
wenzelm@6444
    48
      qed;
wenzelm@6444
    49
    qed;
wenzelm@6444
    50
  qed;
wenzelm@6444
    51
qed;
wenzelm@6444
    52
wenzelm@6444
    53
wenzelm@7001
    54
text {* Variations of backward vs.\ forward reasonong \dots *};
wenzelm@7001
    55
wenzelm@6444
    56
lemma "A & B --> B & A";
wenzelm@6444
    57
proof;
wenzelm@6444
    58
  assume "A & B";
wenzelm@6444
    59
  show "B & A";
wenzelm@6444
    60
  proof;
wenzelm@6444
    61
    show B; by (rule conjunct2);
wenzelm@6444
    62
    show A; by (rule conjunct1);
wenzelm@6444
    63
  qed;
wenzelm@6444
    64
qed;
wenzelm@6444
    65
wenzelm@6444
    66
lemma "A & B --> B & A";
wenzelm@6444
    67
proof;
wenzelm@6444
    68
  assume "A & B";
wenzelm@6444
    69
  then; show "B & A";
wenzelm@6444
    70
  proof;
wenzelm@6444
    71
    assume A B;
wenzelm@6444
    72
    show ??thesis; ..;
wenzelm@6444
    73
  qed;
wenzelm@6444
    74
qed;
wenzelm@6444
    75
wenzelm@6444
    76
lemma "A & B --> B & A";
wenzelm@6444
    77
proof;
wenzelm@6892
    78
  assume ab: "A & B";
wenzelm@6892
    79
  from ab; have a: A; ..;
wenzelm@6892
    80
  from ab; have b: B; ..;
wenzelm@6892
    81
  from b a; show "B & A"; ..;
wenzelm@6444
    82
qed;
wenzelm@6444
    83
wenzelm@6444
    84
wenzelm@7001
    85
section {* Examples from 'Introduction to Isabelle' *};
wenzelm@7001
    86
wenzelm@7001
    87
text {* 'Propositional proof' *};
wenzelm@6444
    88
wenzelm@6444
    89
lemma "P | P --> P";
wenzelm@6444
    90
proof;
wenzelm@6444
    91
  assume "P | P";
wenzelm@6444
    92
  then; show P;
wenzelm@6444
    93
  proof;
wenzelm@6444
    94
    assume P;
wenzelm@6444
    95
    show P; .;
wenzelm@6444
    96
    show P; .;
wenzelm@6444
    97
  qed;
wenzelm@6444
    98
qed;
wenzelm@6444
    99
wenzelm@6444
   100
lemma "P | P --> P";
wenzelm@6444
   101
proof;
wenzelm@6444
   102
  assume "P | P";
wenzelm@6444
   103
  then; show P; ..;
wenzelm@6444
   104
qed;
wenzelm@6444
   105
wenzelm@6444
   106
wenzelm@7001
   107
text {* 'Quantifier proof' *};
wenzelm@6444
   108
wenzelm@6444
   109
lemma "(EX x. P(f(x))) --> (EX x. P(x))";
wenzelm@6444
   110
proof;
wenzelm@6444
   111
  assume "EX x. P(f(x))";
wenzelm@6444
   112
  then; show "EX x. P(x)";
wenzelm@6444
   113
  proof (rule exE);
wenzelm@6444
   114
    fix a;
wenzelm@6444
   115
    assume "P(f(a))" (is "P(??witness)");
wenzelm@6881
   116
    show ??thesis; by (rule exI [of P ??witness]);
wenzelm@6444
   117
  qed;
wenzelm@6444
   118
qed;
wenzelm@6444
   119
wenzelm@6444
   120
lemma "(EX x. P(f(x))) --> (EX x. P(x))";
wenzelm@6444
   121
proof;
wenzelm@6444
   122
  assume "EX x. P(f(x))";
wenzelm@6444
   123
  then; show "EX x. P(x)";
wenzelm@6444
   124
  proof;
wenzelm@6444
   125
    fix a;
wenzelm@6444
   126
    assume "P(f(a))";
wenzelm@6444
   127
    show ??thesis; ..;
wenzelm@6444
   128
  qed;
wenzelm@6444
   129
qed;
wenzelm@6444
   130
wenzelm@6444
   131
lemma "(EX x. P(f(x))) --> (EX x. P(x))";
wenzelm@6504
   132
  by blast;
wenzelm@6444
   133
wenzelm@6444
   134
wenzelm@7001
   135
subsection {* 'Deriving rules in Isabelle' *};
wenzelm@7001
   136
wenzelm@7001
   137
text {* We derive the conjunction elimination rule from the
wenzelm@7001
   138
 projections.  The proof below follows the basic reasoning of the
wenzelm@7001
   139
 script given in the Isabelle Intro Manual closely.  Although, the
wenzelm@7001
   140
 actual underlying operations on rules and proof states are quite
wenzelm@7001
   141
 different: Isabelle/Isar supports non-atomic goals and assumptions
wenzelm@7001
   142
 fully transparently, while the original Isabelle classic script
wenzelm@7001
   143
 depends on the primitive goal command to decompose the rule into
wenzelm@7001
   144
 premises and conclusion, with the result emerging by discharging the
wenzelm@7001
   145
 context again later. *};
wenzelm@7001
   146
wenzelm@7001
   147
theorem conjE: "A & B ==> (A ==> B ==> C) ==> C";
wenzelm@7001
   148
proof same;
wenzelm@7001
   149
  assume ab: "A & B";
wenzelm@7001
   150
  assume ab_c: "A ==> B ==> C";
wenzelm@7001
   151
  show C;
wenzelm@7001
   152
  proof (rule ab_c);
wenzelm@7001
   153
    from ab; show A; ..;
wenzelm@7001
   154
    from ab; show B; ..;
wenzelm@7001
   155
  qed;
wenzelm@7001
   156
qed;
wenzelm@7001
   157
wenzelm@7001
   158
wenzelm@6444
   159
end;