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
```