src/FOL/ex/Quantifiers_Cla.thy
author haftmann
Thu Nov 23 17:03:27 2017 +0000 (21 months ago)
changeset 67087 733017b19de9
parent 62020 5d208fd2507d
child 69590 e65314985426
permissions -rw-r--r--
generalized more lemmas
     1 (*  Title:      FOL/ex/Quantifiers_Cla.thy
     2     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3     Copyright   1991  University of Cambridge
     4 *)
     5 
     6 section \<open>First-Order Logic: quantifier examples (classical version)\<close>
     7 
     8 theory Quantifiers_Cla
     9 imports FOL
    10 begin
    11 
    12 lemma "(\<forall>x y. P(x,y)) \<longrightarrow> (\<forall>y x. P(x,y))"
    13   by fast
    14 
    15 lemma "(\<exists>x y. P(x,y)) \<longrightarrow> (\<exists>y x. P(x,y))"
    16   by fast
    17 
    18 
    19 text \<open>Converse is false.\<close>
    20 lemma "(\<forall>x. P(x)) \<or> (\<forall>x. Q(x)) \<longrightarrow> (\<forall>x. P(x) \<or> Q(x))"
    21   by fast
    22 
    23 lemma "(\<forall>x. P \<longrightarrow> Q(x)) \<longleftrightarrow> (P \<longrightarrow> (\<forall>x. Q(x)))"
    24   by fast
    25 
    26 
    27 lemma "(\<forall>x. P(x) \<longrightarrow> Q) \<longleftrightarrow> ((\<exists>x. P(x)) \<longrightarrow> Q)"
    28   by fast
    29 
    30 
    31 text \<open>Some harder ones.\<close>
    32 
    33 lemma "(\<exists>x. P(x) \<or> Q(x)) \<longleftrightarrow> (\<exists>x. P(x)) \<or> (\<exists>x. Q(x))"
    34   by fast
    35 
    36 \<comment> \<open>Converse is false.\<close>
    37 lemma "(\<exists>x. P(x) \<and> Q(x)) \<longrightarrow> (\<exists>x. P(x)) \<and> (\<exists>x. Q(x))"
    38   by fast
    39 
    40 
    41 text \<open>Basic test of quantifier reasoning.\<close>
    42 
    43 \<comment> \<open>TRUE\<close>
    44 lemma "(\<exists>y. \<forall>x. Q(x,y)) \<longrightarrow> (\<forall>x. \<exists>y. Q(x,y))"
    45   by fast
    46 
    47 lemma "(\<forall>x. Q(x)) \<longrightarrow> (\<exists>x. Q(x))"
    48   by fast
    49 
    50 
    51 text \<open>The following should fail, as they are false!\<close>
    52 
    53 lemma "(\<forall>x. \<exists>y. Q(x,y)) \<longrightarrow> (\<exists>y. \<forall>x. Q(x,y))"
    54   apply fast?
    55   oops
    56 
    57 lemma "(\<exists>x. Q(x)) \<longrightarrow> (\<forall>x. Q(x))"
    58   apply fast?
    59   oops
    60 
    61 schematic_goal "P(?a) \<longrightarrow> (\<forall>x. P(x))"
    62   apply fast?
    63   oops
    64 
    65 schematic_goal "(P(?a) \<longrightarrow> (\<forall>x. Q(x))) \<longrightarrow> (\<forall>x. P(x) \<longrightarrow> Q(x))"
    66   apply fast?
    67   oops
    68 
    69 
    70 text \<open>Back to things that are provable \dots\<close>
    71 
    72 lemma "(\<forall>x. P(x) \<longrightarrow> Q(x)) \<and> (\<exists>x. P(x)) \<longrightarrow> (\<exists>x. Q(x))"
    73   by fast
    74 
    75 text \<open>An example of why \<open>exI\<close> should be delayed as long as possible.\<close>
    76 lemma "(P \<longrightarrow> (\<exists>x. Q(x))) \<and> P \<longrightarrow> (\<exists>x. Q(x))"
    77   by fast
    78 
    79 schematic_goal "(\<forall>x. P(x) \<longrightarrow> Q(f(x))) \<and> (\<forall>x. Q(x) \<longrightarrow> R(g(x))) \<and> P(d) \<longrightarrow> R(?a)"
    80   by fast
    81 
    82 lemma "(\<forall>x. Q(x)) \<longrightarrow> (\<exists>x. Q(x))"
    83   by fast
    84 
    85 
    86 text \<open>Some slow ones\<close>
    87 
    88 text \<open>Principia Mathematica *11.53\<close>
    89 lemma "(\<forall>x y. P(x) \<longrightarrow> Q(y)) \<longleftrightarrow> ((\<exists>x. P(x)) \<longrightarrow> (\<forall>y. Q(y)))"
    90   by fast
    91 
    92 (*Principia Mathematica *11.55  *)
    93 lemma "(\<exists>x y. P(x) \<and> Q(x,y)) \<longleftrightarrow> (\<exists>x. P(x) \<and> (\<exists>y. Q(x,y)))"
    94   by fast
    95 
    96 (*Principia Mathematica *11.61  *)
    97 lemma "(\<exists>y. \<forall>x. P(x) \<longrightarrow> Q(x,y)) \<longrightarrow> (\<forall>x. P(x) \<longrightarrow> (\<exists>y. Q(x,y)))"
    98   by fast
    99 
   100 end