src/FOL/ex/Miniscope.thy
 author haftmann Thu Nov 23 17:03:27 2017 +0000 (21 months ago) changeset 67087 733017b19de9 parent 61489 b8d375aee0df child 68536 e14848001c4c permissions -rw-r--r--
generalized more lemmas
```     1 (*  Title:      FOL/ex/Miniscope.thy
```
```     2     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
```
```     3     Copyright   1994  University of Cambridge
```
```     4
```
```     5 Classical First-Order Logic.
```
```     6 Conversion to nnf/miniscope format: pushing quantifiers in.
```
```     7 Demonstration of formula rewriting by proof.
```
```     8 *)
```
```     9
```
```    10 theory Miniscope
```
```    11 imports FOL
```
```    12 begin
```
```    13
```
```    14 lemmas ccontr = FalseE [THEN classical]
```
```    15
```
```    16 subsection \<open>Negation Normal Form\<close>
```
```    17
```
```    18 subsubsection \<open>de Morgan laws\<close>
```
```    19
```
```    20 lemma demorgans:
```
```    21   "\<not> (P \<and> Q) \<longleftrightarrow> \<not> P \<or> \<not> Q"
```
```    22   "\<not> (P \<or> Q) \<longleftrightarrow> \<not> P \<and> \<not> Q"
```
```    23   "\<not> \<not> P \<longleftrightarrow> P"
```
```    24   "\<And>P. \<not> (\<forall>x. P(x)) \<longleftrightarrow> (\<exists>x. \<not> P(x))"
```
```    25   "\<And>P. \<not> (\<exists>x. P(x)) \<longleftrightarrow> (\<forall>x. \<not> P(x))"
```
```    26   by blast+
```
```    27
```
```    28 (*** Removal of --> and <-> (positive and negative occurrences) ***)
```
```    29 (*Last one is important for computing a compact CNF*)
```
```    30 lemma nnf_simps:
```
```    31   "(P \<longrightarrow> Q) \<longleftrightarrow> (\<not> P \<or> Q)"
```
```    32   "\<not> (P \<longrightarrow> Q) \<longleftrightarrow> (P \<and> \<not> Q)"
```
```    33   "(P \<longleftrightarrow> Q) \<longleftrightarrow> (\<not> P \<or> Q) \<and> (\<not> Q \<or> P)"
```
```    34   "\<not> (P \<longleftrightarrow> Q) \<longleftrightarrow> (P \<or> Q) \<and> (\<not> P \<or> \<not> Q)"
```
```    35   by blast+
```
```    36
```
```    37
```
```    38 (* BEWARE: rewrite rules for <-> can confuse the simplifier!! *)
```
```    39
```
```    40 subsubsection \<open>Pushing in the existential quantifiers\<close>
```
```    41
```
```    42 lemma ex_simps:
```
```    43   "(\<exists>x. P) \<longleftrightarrow> P"
```
```    44   "\<And>P Q. (\<exists>x. P(x) \<and> Q) \<longleftrightarrow> (\<exists>x. P(x)) \<and> Q"
```
```    45   "\<And>P Q. (\<exists>x. P \<and> Q(x)) \<longleftrightarrow> P \<and> (\<exists>x. Q(x))"
```
```    46   "\<And>P Q. (\<exists>x. P(x) \<or> Q(x)) \<longleftrightarrow> (\<exists>x. P(x)) \<or> (\<exists>x. Q(x))"
```
```    47   "\<And>P Q. (\<exists>x. P(x) \<or> Q) \<longleftrightarrow> (\<exists>x. P(x)) \<or> Q"
```
```    48   "\<And>P Q. (\<exists>x. P \<or> Q(x)) \<longleftrightarrow> P \<or> (\<exists>x. Q(x))"
```
```    49   by blast+
```
```    50
```
```    51
```
```    52 subsubsection \<open>Pushing in the universal quantifiers\<close>
```
```    53
```
```    54 lemma all_simps:
```
```    55   "(\<forall>x. P) \<longleftrightarrow> P"
```
```    56   "\<And>P Q. (\<forall>x. P(x) \<and> Q(x)) \<longleftrightarrow> (\<forall>x. P(x)) \<and> (\<forall>x. Q(x))"
```
```    57   "\<And>P Q. (\<forall>x. P(x) \<and> Q) \<longleftrightarrow> (\<forall>x. P(x)) \<and> Q"
```
```    58   "\<And>P Q. (\<forall>x. P \<and> Q(x)) \<longleftrightarrow> P \<and> (\<forall>x. Q(x))"
```
```    59   "\<And>P Q. (\<forall>x. P(x) \<or> Q) \<longleftrightarrow> (\<forall>x. P(x)) \<or> Q"
```
```    60   "\<And>P Q. (\<forall>x. P \<or> Q(x)) \<longleftrightarrow> P \<or> (\<forall>x. Q(x))"
```
```    61   by blast+
```
```    62
```
```    63 lemmas mini_simps = demorgans nnf_simps ex_simps all_simps
```
```    64
```
```    65 ML \<open>
```
```    66 val mini_ss = simpset_of (@{context} addsimps @{thms mini_simps});
```
```    67 fun mini_tac ctxt =
```
```    68   resolve_tac ctxt @{thms ccontr} THEN' asm_full_simp_tac (put_simpset mini_ss ctxt);
```
```    69 \<close>
```
```    70
```
```    71 end
```