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