src/Sequents/LK/Quantifiers.thy
author wenzelm
Sat Oct 10 20:54:44 2015 +0200 (2015-10-10)
changeset 61386 0a29a984a91b
parent 61385 538100cc4399
permissions -rw-r--r--
more symbols;
     1 (*  Title:      Sequents/LK/Quantifiers.thy
     2     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3     Copyright   1992  University of Cambridge
     4 
     5 Classical sequent calculus: examples with quantifiers.
     6 *)
     7 
     8 theory Quantifiers
     9 imports "../LK"
    10 begin
    11 
    12 lemma "\<turnstile> (\<forall>x. P) \<longleftrightarrow> P"
    13   by fast
    14 
    15 lemma "\<turnstile> (\<forall>x y. P(x,y)) \<longleftrightarrow> (\<forall>y x. P(x,y))"
    16   by fast
    17 
    18 lemma "\<forall>u. P(u), \<forall>v. Q(v) \<turnstile> \<forall>u v. P(u) \<and> Q(v)"
    19   by fast
    20 
    21 
    22 text "Permutation of existential quantifier."
    23 
    24 lemma "\<turnstile> (\<exists>x y. P(x,y)) \<longleftrightarrow> (\<exists>y x. P(x,y))"
    25   by fast
    26 
    27 lemma "\<turnstile> (\<forall>x. P(x) \<and> Q(x)) \<longleftrightarrow> (\<forall>x. P(x)) \<and> (\<forall>x. Q(x))"
    28   by fast
    29 
    30 (*Converse is invalid*)
    31 lemma "\<turnstile> (\<forall>x. P(x)) \<or> (\<forall>x. Q(x)) \<longrightarrow> (\<forall>x. P(x) \<or> Q(x))"
    32   by fast
    33 
    34 
    35 text "Pushing \<forall>into an implication."
    36 
    37 lemma "\<turnstile> (\<forall>x. P \<longrightarrow> Q(x)) \<longleftrightarrow> (P \<longrightarrow> (\<forall>x. Q(x)))"
    38   by fast
    39 
    40 lemma "\<turnstile> (\<forall>x. P(x) \<longrightarrow> Q) \<longleftrightarrow> ((\<exists>x. P(x)) \<longrightarrow> Q)"
    41   by fast
    42 
    43 lemma "\<turnstile> (\<exists>x. P)  \<longleftrightarrow>  P"
    44   by fast
    45 
    46 
    47 text "Distribution of \<exists>over disjunction."
    48 
    49 lemma "\<turnstile> (\<exists>x. P(x) \<or> Q(x)) \<longleftrightarrow> (\<exists>x. P(x)) \<or> (\<exists>x. Q(x))"
    50   by fast
    51 
    52 (*Converse is invalid*)
    53 lemma "\<turnstile> (\<exists>x. P(x) \<and> Q(x)) \<longrightarrow> (\<exists>x. P(x)) \<and> (\<exists>x. Q(x))"
    54   by fast
    55 
    56 
    57 text "Harder examples: classical theorems."
    58 
    59 lemma "\<turnstile> (\<exists>x. P \<longrightarrow> Q(x)) \<longleftrightarrow> (P \<longrightarrow> (\<exists>x. Q(x)))"
    60   by fast
    61 
    62 lemma "\<turnstile> (\<exists>x. P(x) \<longrightarrow> Q) \<longleftrightarrow> (\<forall>x. P(x)) \<longrightarrow> Q"
    63   by fast
    64 
    65 lemma "\<turnstile> (\<forall>x. P(x)) \<or> Q \<longleftrightarrow> (\<forall>x. P(x) \<or> Q)"
    66   by fast
    67 
    68 
    69 text "Basic test of quantifier reasoning"
    70 
    71 lemma "\<turnstile> (\<exists>y. \<forall>x. Q(x,y)) \<longrightarrow> (\<forall>x. \<exists>y. Q(x,y))"
    72   by fast
    73 
    74 lemma "\<turnstile> (\<forall>x. Q(x)) \<longrightarrow> (\<exists>x. Q(x))"
    75   by fast
    76 
    77 
    78 text "The following are invalid!"
    79 
    80 (*INVALID*)
    81 lemma "\<turnstile> (\<forall>x. \<exists>y. Q(x,y)) \<longrightarrow> (\<exists>y. \<forall>x. Q(x,y))"
    82   apply fast?
    83   apply (rule _)
    84   oops
    85 
    86 (*INVALID*)
    87 lemma "\<turnstile> (\<exists>x. Q(x)) \<longrightarrow> (\<forall>x. Q(x))"
    88   apply fast?
    89   apply (rule _)
    90   oops
    91 
    92 (*INVALID*)
    93 schematic_goal "\<turnstile> P(?a) \<longrightarrow> (\<forall>x. P(x))"
    94   apply fast?
    95   apply (rule _)
    96   oops
    97 
    98 (*INVALID*)
    99 schematic_goal "\<turnstile> (P(?a) \<longrightarrow> (\<forall>x. Q(x))) \<longrightarrow> (\<forall>x. P(x) \<longrightarrow> Q(x))"
   100   apply fast?
   101   apply (rule _)
   102   oops
   103 
   104 
   105 text "Back to things that are provable..."
   106 
   107 lemma "\<turnstile> (\<forall>x. P(x) \<longrightarrow> Q(x)) \<and> (\<exists>x. P(x)) \<longrightarrow> (\<exists>x. Q(x))"
   108   by fast
   109 
   110 (*An example of why exR should be delayed as long as possible*)
   111 lemma "\<turnstile> (P \<longrightarrow> (\<exists>x. Q(x))) \<and> P \<longrightarrow> (\<exists>x. Q(x))"
   112   by fast
   113 
   114 
   115 text "Solving for a Var"
   116 
   117 schematic_goal "\<turnstile> (\<forall>x. P(x) \<longrightarrow> Q(f(x))) \<and> (\<forall>x. Q(x) \<longrightarrow> R(g(x))) \<and> P(d) \<longrightarrow> R(?a)"
   118   by fast
   119 
   120 
   121 text "Principia Mathematica *11.53"
   122 
   123 lemma "\<turnstile> (\<forall>x y. P(x) \<longrightarrow> Q(y)) \<longleftrightarrow> ((\<exists>x. P(x)) \<longrightarrow> (\<forall>y. Q(y)))"
   124   by fast
   125 
   126 
   127 text "Principia Mathematica *11.55"
   128 
   129 lemma "\<turnstile> (\<exists>x y. P(x) \<and> Q(x,y)) \<longleftrightarrow> (\<exists>x. P(x) \<and> (\<exists>y. Q(x,y)))"
   130   by fast
   131 
   132 
   133 text "Principia Mathematica *11.61"
   134 
   135 lemma "\<turnstile> (\<exists>y. \<forall>x. P(x) \<longrightarrow> Q(x,y)) \<longrightarrow> (\<forall>x. P(x) \<longrightarrow> (\<exists>y. Q(x,y)))"
   136   by fast
   137 
   138 
   139 (*21 August 88: loaded in 45.7 secs*)
   140 (*18 September 2005: loaded in 0.114 secs*)
   141 
   142 end