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