src/FOL/ex/Quantifiers_Int.thy
author wenzelm
Fri Apr 23 23:35:43 2010 +0200 (2010-04-23)
changeset 36319 8feb2c4bef1a
parent 31974 e81979a703a4
child 51798 ad3a241def73
permissions -rw-r--r--
mark schematic statements explicitly;
     1 (*  Title:      FOL/ex/Quantifiers_Int.thy
     2     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3     Copyright   1991  University of Cambridge
     4 *)
     5 
     6 header {* First-Order Logic: quantifier examples (intuitionistic version) *}
     7 
     8 theory Quantifiers_Int
     9 imports IFOL
    10 begin
    11 
    12 lemma "(ALL x y. P(x,y))  -->  (ALL y x. P(x,y))"
    13   by (tactic "IntPr.fast_tac 1")
    14 
    15 lemma "(EX x y. P(x,y)) --> (EX y x. P(x,y))"
    16   by (tactic "IntPr.fast_tac 1")
    17 
    18 
    19 -- {* Converse is false *}
    20 lemma "(ALL x. P(x)) | (ALL x. Q(x)) --> (ALL x. P(x) | Q(x))"
    21   by (tactic "IntPr.fast_tac 1")
    22 
    23 lemma "(ALL x. P-->Q(x))  <->  (P--> (ALL x. Q(x)))"
    24   by (tactic "IntPr.fast_tac 1")
    25 
    26 
    27 lemma "(ALL x. P(x)-->Q)  <->  ((EX x. P(x)) --> Q)"
    28   by (tactic "IntPr.fast_tac 1")
    29 
    30 
    31 text {* Some harder ones *}
    32 
    33 lemma "(EX x. P(x) | Q(x)) <-> (EX x. P(x)) | (EX x. Q(x))"
    34   by (tactic "IntPr.fast_tac 1")
    35 
    36 -- {* Converse is false *}
    37 lemma "(EX x. P(x)&Q(x)) --> (EX x. P(x))  &  (EX x. Q(x))"
    38   by (tactic "IntPr.fast_tac 1")
    39 
    40 
    41 text {* Basic test of quantifier reasoning *}
    42 
    43 -- {* TRUE *}
    44 lemma "(EX y. ALL x. Q(x,y)) -->  (ALL x. EX y. Q(x,y))"
    45   by (tactic "IntPr.fast_tac 1")
    46 
    47 lemma "(ALL x. Q(x))  -->  (EX x. Q(x))"
    48   by (tactic "IntPr.fast_tac 1")
    49 
    50 
    51 text {* The following should fail, as they are false! *}
    52 
    53 lemma "(ALL x. EX y. Q(x,y))  -->  (EX y. ALL x. Q(x,y))"
    54   apply (tactic "IntPr.fast_tac 1")?
    55   oops
    56 
    57 lemma "(EX x. Q(x))  -->  (ALL x. Q(x))"
    58   apply (tactic "IntPr.fast_tac 1")?
    59   oops
    60 
    61 schematic_lemma "P(?a) --> (ALL x. P(x))"
    62   apply (tactic "IntPr.fast_tac 1")?
    63   oops
    64 
    65 schematic_lemma "(P(?a) --> (ALL x. Q(x))) --> (ALL x. P(x) --> Q(x))"
    66   apply (tactic "IntPr.fast_tac 1")?
    67   oops
    68 
    69 
    70 text {* Back to things that are provable \dots *}
    71 
    72 lemma "(ALL x. P(x)-->Q(x)) & (EX x. P(x)) --> (EX x. Q(x))"
    73   by (tactic "IntPr.fast_tac 1")
    74 
    75 -- {* An example of why exI should be delayed as long as possible *}
    76 lemma "(P --> (EX x. Q(x))) & P --> (EX x. Q(x))"
    77   by (tactic "IntPr.fast_tac 1")
    78 
    79 schematic_lemma "(ALL x. P(x)-->Q(f(x))) & (ALL x. Q(x)-->R(g(x))) & P(d) --> R(?a)"
    80   by (tactic "IntPr.fast_tac 1")
    81 
    82 lemma "(ALL x. Q(x))  -->  (EX x. Q(x))"
    83   by (tactic "IntPr.fast_tac 1")
    84 
    85 
    86 text {* Some slow ones *}
    87 
    88 -- {* Principia Mathematica *11.53 *}
    89 lemma "(ALL x y. P(x) --> Q(y)) <-> ((EX x. P(x)) --> (ALL y. Q(y)))"
    90   by (tactic "IntPr.fast_tac 1")
    91 
    92 (*Principia Mathematica *11.55  *)
    93 lemma "(EX x y. P(x) & Q(x,y)) <-> (EX x. P(x) & (EX y. Q(x,y)))"
    94   by (tactic "IntPr.fast_tac 1")
    95 
    96 (*Principia Mathematica *11.61  *)
    97 lemma "(EX y. ALL x. P(x) --> Q(x,y)) --> (ALL x. P(x) --> (EX y. Q(x,y)))"
    98   by (tactic "IntPr.fast_tac 1")
    99 
   100 end