src/HOL/Isar_examples/BasicLogic.thy
author wenzelm
Sat Jul 03 00:26:00 1999 +0200 (1999-07-03)
changeset 6892 4a905b4a39c8
parent 6881 91a2c8b8269a
child 7001 8121e11ed765
permissions -rw-r--r--
tuned;
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@6444
    11
lemma I: "A --> A";
wenzelm@6444
    12
proof;
wenzelm@6444
    13
  assume A;
wenzelm@6444
    14
  show A; .;
wenzelm@6444
    15
qed;
wenzelm@6444
    16
wenzelm@6444
    17
lemma K: "A --> B --> A";
wenzelm@6444
    18
proof;
wenzelm@6444
    19
  assume A;
wenzelm@6444
    20
  show "B --> A";
wenzelm@6444
    21
  proof;
wenzelm@6444
    22
    show A; .;
wenzelm@6444
    23
  qed;
wenzelm@6444
    24
qed;
wenzelm@6444
    25
wenzelm@6504
    26
lemma K': "A --> B --> A";
wenzelm@6444
    27
proof single*;
wenzelm@6444
    28
  assume A;
wenzelm@6444
    29
  show A; .;
wenzelm@6444
    30
qed;
wenzelm@6444
    31
wenzelm@6444
    32
lemma S: "(A --> B --> C) --> (A --> B) --> A --> C";
wenzelm@6444
    33
proof;
wenzelm@6444
    34
  assume "A --> B --> C";
wenzelm@6444
    35
  show "(A --> B) --> A --> C";
wenzelm@6444
    36
  proof;
wenzelm@6444
    37
    assume "A --> B";
wenzelm@6444
    38
    show "A --> C";
wenzelm@6444
    39
    proof;
wenzelm@6444
    40
      assume A;
wenzelm@6444
    41
      show C;
wenzelm@6444
    42
      proof (rule mp);
wenzelm@6444
    43
	show "B --> C"; by (rule mp);
wenzelm@6444
    44
        show B; by (rule mp);
wenzelm@6444
    45
      qed;
wenzelm@6444
    46
    qed;
wenzelm@6444
    47
  qed;
wenzelm@6444
    48
qed;
wenzelm@6444
    49
wenzelm@6444
    50
wenzelm@6444
    51
lemma "A & B --> B & A";
wenzelm@6444
    52
proof;
wenzelm@6444
    53
  assume "A & B";
wenzelm@6444
    54
  show "B & A";
wenzelm@6444
    55
  proof;
wenzelm@6444
    56
    show B; by (rule conjunct2);
wenzelm@6444
    57
    show A; by (rule conjunct1);
wenzelm@6444
    58
  qed;
wenzelm@6444
    59
qed;
wenzelm@6444
    60
wenzelm@6444
    61
lemma "A & B --> B & A";
wenzelm@6444
    62
proof;
wenzelm@6444
    63
  assume "A & B";
wenzelm@6444
    64
  then; show "B & A";
wenzelm@6444
    65
  proof;
wenzelm@6444
    66
    assume A B;
wenzelm@6444
    67
    show ??thesis; ..;
wenzelm@6444
    68
  qed;
wenzelm@6444
    69
qed;
wenzelm@6444
    70
wenzelm@6444
    71
lemma "A & B --> B & A";
wenzelm@6444
    72
proof;
wenzelm@6892
    73
  assume ab: "A & B";
wenzelm@6892
    74
  from ab; have a: A; ..;
wenzelm@6892
    75
  from ab; have b: B; ..;
wenzelm@6892
    76
  from b a; show "B & A"; ..;
wenzelm@6444
    77
qed;
wenzelm@6444
    78
wenzelm@6444
    79
wenzelm@6746
    80
text {* propositional proof (from 'Introduction to Isabelle') *};
wenzelm@6444
    81
wenzelm@6444
    82
lemma "P | P --> P";
wenzelm@6444
    83
proof;
wenzelm@6444
    84
  assume "P | P";
wenzelm@6444
    85
  then; show P;
wenzelm@6444
    86
  proof;
wenzelm@6444
    87
    assume P;
wenzelm@6444
    88
    show P; .;
wenzelm@6444
    89
    show P; .;
wenzelm@6444
    90
  qed;
wenzelm@6444
    91
qed;
wenzelm@6444
    92
wenzelm@6444
    93
lemma "P | P --> P";
wenzelm@6444
    94
proof;
wenzelm@6444
    95
  assume "P | P";
wenzelm@6444
    96
  then; show P; ..;
wenzelm@6444
    97
qed;
wenzelm@6444
    98
wenzelm@6444
    99
wenzelm@6746
   100
text {* quantifier proof (from 'Introduction to Isabelle') *};
wenzelm@6444
   101
wenzelm@6444
   102
lemma "(EX x. P(f(x))) --> (EX x. P(x))";
wenzelm@6444
   103
proof;
wenzelm@6444
   104
  assume "EX x. P(f(x))";
wenzelm@6444
   105
  then; show "EX x. P(x)";
wenzelm@6444
   106
  proof (rule exE);
wenzelm@6444
   107
    fix a;
wenzelm@6444
   108
    assume "P(f(a))" (is "P(??witness)");
wenzelm@6881
   109
    show ??thesis; by (rule exI [of P ??witness]);
wenzelm@6444
   110
  qed;
wenzelm@6444
   111
qed;
wenzelm@6444
   112
wenzelm@6444
   113
lemma "(EX x. P(f(x))) --> (EX x. P(x))";
wenzelm@6444
   114
proof;
wenzelm@6444
   115
  assume "EX x. P(f(x))";
wenzelm@6444
   116
  then; show "EX x. P(x)";
wenzelm@6444
   117
  proof;
wenzelm@6444
   118
    fix a;
wenzelm@6444
   119
    assume "P(f(a))";
wenzelm@6444
   120
    show ??thesis; ..;
wenzelm@6444
   121
  qed;
wenzelm@6444
   122
qed;
wenzelm@6444
   123
wenzelm@6444
   124
lemma "(EX x. P(f(x))) --> (EX x. P(x))";
wenzelm@6504
   125
  by blast;
wenzelm@6444
   126
wenzelm@6444
   127
wenzelm@6444
   128
end;