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
wenzelm@41777
     1
(*  Title:      FOL/ex/Quantifiers_Cla.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@60770
     6
section \<open>First-Order Logic: quantifier examples (classical version)\<close>
wenzelm@23914
     7
wenzelm@23914
     8
theory Quantifiers_Cla
wenzelm@23914
     9
imports FOL
wenzelm@23914
    10
begin
wenzelm@23914
    11
wenzelm@61489
    12
lemma "(\<forall>x y. P(x,y)) \<longrightarrow> (\<forall>y x. P(x,y))"
wenzelm@23914
    13
  by fast
wenzelm@23914
    14
wenzelm@61489
    15
lemma "(\<exists>x y. P(x,y)) \<longrightarrow> (\<exists>y x. P(x,y))"
wenzelm@23914
    16
  by fast
wenzelm@23914
    17
wenzelm@23914
    18
wenzelm@61489
    19
text \<open>Converse is false.\<close>
wenzelm@61489
    20
lemma "(\<forall>x. P(x)) \<or> (\<forall>x. Q(x)) \<longrightarrow> (\<forall>x. P(x) \<or> Q(x))"
wenzelm@23914
    21
  by fast
wenzelm@23914
    22
wenzelm@61489
    23
lemma "(\<forall>x. P \<longrightarrow> Q(x)) \<longleftrightarrow> (P \<longrightarrow> (\<forall>x. Q(x)))"
wenzelm@23914
    24
  by fast
wenzelm@23914
    25
wenzelm@23914
    26
wenzelm@61489
    27
lemma "(\<forall>x. P(x) \<longrightarrow> Q) \<longleftrightarrow> ((\<exists>x. P(x)) \<longrightarrow> Q)"
wenzelm@23914
    28
  by fast
wenzelm@23914
    29
wenzelm@23914
    30
wenzelm@61489
    31
text \<open>Some harder ones.\<close>
wenzelm@23914
    32
wenzelm@61489
    33
lemma "(\<exists>x. P(x) \<or> Q(x)) \<longleftrightarrow> (\<exists>x. P(x)) \<or> (\<exists>x. Q(x))"
wenzelm@23914
    34
  by fast
wenzelm@23914
    35
wenzelm@62020
    36
\<comment> \<open>Converse is false.\<close>
wenzelm@61489
    37
lemma "(\<exists>x. P(x) \<and> Q(x)) \<longrightarrow> (\<exists>x. P(x)) \<and> (\<exists>x. Q(x))"
wenzelm@23914
    38
  by fast
wenzelm@23914
    39
wenzelm@23914
    40
wenzelm@61489
    41
text \<open>Basic test of quantifier reasoning.\<close>
wenzelm@23914
    42
wenzelm@62020
    43
\<comment> \<open>TRUE\<close>
wenzelm@61489
    44
lemma "(\<exists>y. \<forall>x. Q(x,y)) \<longrightarrow> (\<forall>x. \<exists>y. Q(x,y))"
wenzelm@23914
    45
  by fast
wenzelm@23914
    46
wenzelm@61489
    47
lemma "(\<forall>x. Q(x)) \<longrightarrow> (\<exists>x. Q(x))"
wenzelm@23914
    48
  by fast
wenzelm@23914
    49
wenzelm@23914
    50
wenzelm@60770
    51
text \<open>The following should fail, as they are false!\<close>
wenzelm@23914
    52
wenzelm@61489
    53
lemma "(\<forall>x. \<exists>y. Q(x,y)) \<longrightarrow> (\<exists>y. \<forall>x. Q(x,y))"
wenzelm@23914
    54
  apply fast?
wenzelm@23914
    55
  oops
wenzelm@23914
    56
wenzelm@61489
    57
lemma "(\<exists>x. Q(x)) \<longrightarrow> (\<forall>x. Q(x))"
wenzelm@23914
    58
  apply fast?
wenzelm@23914
    59
  oops
wenzelm@23914
    60
wenzelm@61489
    61
schematic_goal "P(?a) \<longrightarrow> (\<forall>x. P(x))"
wenzelm@23914
    62
  apply fast?
wenzelm@23914
    63
  oops
wenzelm@23914
    64
wenzelm@61489
    65
schematic_goal "(P(?a) \<longrightarrow> (\<forall>x. Q(x))) \<longrightarrow> (\<forall>x. P(x) \<longrightarrow> Q(x))"
wenzelm@23914
    66
  apply fast?
wenzelm@23914
    67
  oops
wenzelm@23914
    68
wenzelm@23914
    69
wenzelm@60770
    70
text \<open>Back to things that are provable \dots\<close>
wenzelm@23914
    71
wenzelm@61489
    72
lemma "(\<forall>x. P(x) \<longrightarrow> Q(x)) \<and> (\<exists>x. P(x)) \<longrightarrow> (\<exists>x. Q(x))"
wenzelm@23914
    73
  by fast
wenzelm@23914
    74
wenzelm@62020
    75
text \<open>An example of why \<open>exI\<close> should be delayed as long as possible.\<close>
wenzelm@61489
    76
lemma "(P \<longrightarrow> (\<exists>x. Q(x))) \<and> P \<longrightarrow> (\<exists>x. Q(x))"
wenzelm@23914
    77
  by fast
wenzelm@23914
    78
wenzelm@61489
    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)"
wenzelm@23914
    80
  by fast
wenzelm@23914
    81
wenzelm@61489
    82
lemma "(\<forall>x. Q(x)) \<longrightarrow> (\<exists>x. Q(x))"
wenzelm@23914
    83
  by fast
wenzelm@23914
    84
wenzelm@23914
    85
wenzelm@60770
    86
text \<open>Some slow ones\<close>
wenzelm@23914
    87
wenzelm@61489
    88
text \<open>Principia Mathematica *11.53\<close>
wenzelm@61489
    89
lemma "(\<forall>x y. P(x) \<longrightarrow> Q(y)) \<longleftrightarrow> ((\<exists>x. P(x)) \<longrightarrow> (\<forall>y. Q(y)))"
wenzelm@23914
    90
  by fast
wenzelm@23914
    91
wenzelm@23914
    92
(*Principia Mathematica *11.55  *)
wenzelm@61489
    93
lemma "(\<exists>x y. P(x) \<and> Q(x,y)) \<longleftrightarrow> (\<exists>x. P(x) \<and> (\<exists>y. Q(x,y)))"
wenzelm@23914
    94
  by fast
wenzelm@23914
    95
wenzelm@23914
    96
(*Principia Mathematica *11.61  *)
wenzelm@61489
    97
lemma "(\<exists>y. \<forall>x. P(x) \<longrightarrow> Q(x,y)) \<longrightarrow> (\<forall>x. P(x) \<longrightarrow> (\<exists>y. Q(x,y)))"
wenzelm@23914
    98
  by fast
wenzelm@23914
    99
wenzelm@23914
   100
end