author | wenzelm |
Fri, 04 Jan 2019 23:22:53 +0100 | |
changeset 69593 | 3dda49e08b9d |
parent 69590 | e65314985426 |
permissions | -rw-r--r-- |
19820 | 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 |
||
60770 | 16 |
subsection \<open>Negation Normal Form\<close> |
19820 | 17 |
|
60770 | 18 |
subsubsection \<open>de Morgan laws\<close> |
19820 | 19 |
|
68536 | 20 |
lemma demorgans1: |
69590 | 21 |
\<open>\<not> (P \<and> Q) \<longleftrightarrow> \<not> P \<or> \<not> Q\<close> |
22 |
\<open>\<not> (P \<or> Q) \<longleftrightarrow> \<not> P \<and> \<not> Q\<close> |
|
23 |
\<open>\<not> \<not> P \<longleftrightarrow> P\<close> |
|
68536 | 24 |
by blast+ |
25 |
||
26 |
lemma demorgans2: |
|
69590 | 27 |
\<open>\<And>P. \<not> (\<forall>x. P(x)) \<longleftrightarrow> (\<exists>x. \<not> P(x))\<close> |
28 |
\<open>\<And>P. \<not> (\<exists>x. P(x)) \<longleftrightarrow> (\<forall>x. \<not> P(x))\<close> |
|
19820 | 29 |
by blast+ |
30 |
||
68536 | 31 |
lemmas demorgans = demorgans1 demorgans2 |
32 |
||
19820 | 33 |
(*** Removal of --> and <-> (positive and negative occurrences) ***) |
34 |
(*Last one is important for computing a compact CNF*) |
|
35 |
lemma nnf_simps: |
|
69590 | 36 |
\<open>(P \<longrightarrow> Q) \<longleftrightarrow> (\<not> P \<or> Q)\<close> |
37 |
\<open>\<not> (P \<longrightarrow> Q) \<longleftrightarrow> (P \<and> \<not> Q)\<close> |
|
38 |
\<open>(P \<longleftrightarrow> Q) \<longleftrightarrow> (\<not> P \<or> Q) \<and> (\<not> Q \<or> P)\<close> |
|
39 |
\<open>\<not> (P \<longleftrightarrow> Q) \<longleftrightarrow> (P \<or> Q) \<and> (\<not> P \<or> \<not> Q)\<close> |
|
19820 | 40 |
by blast+ |
41 |
||
42 |
||
43 |
(* BEWARE: rewrite rules for <-> can confuse the simplifier!! *) |
|
44 |
||
60770 | 45 |
subsubsection \<open>Pushing in the existential quantifiers\<close> |
19820 | 46 |
|
47 |
lemma ex_simps: |
|
69590 | 48 |
\<open>(\<exists>x. P) \<longleftrightarrow> P\<close> |
49 |
\<open>\<And>P Q. (\<exists>x. P(x) \<and> Q) \<longleftrightarrow> (\<exists>x. P(x)) \<and> Q\<close> |
|
50 |
\<open>\<And>P Q. (\<exists>x. P \<and> Q(x)) \<longleftrightarrow> P \<and> (\<exists>x. Q(x))\<close> |
|
51 |
\<open>\<And>P Q. (\<exists>x. P(x) \<or> Q(x)) \<longleftrightarrow> (\<exists>x. P(x)) \<or> (\<exists>x. Q(x))\<close> |
|
52 |
\<open>\<And>P Q. (\<exists>x. P(x) \<or> Q) \<longleftrightarrow> (\<exists>x. P(x)) \<or> Q\<close> |
|
53 |
\<open>\<And>P Q. (\<exists>x. P \<or> Q(x)) \<longleftrightarrow> P \<or> (\<exists>x. Q(x))\<close> |
|
19820 | 54 |
by blast+ |
55 |
||
56 |
||
60770 | 57 |
subsubsection \<open>Pushing in the universal quantifiers\<close> |
19820 | 58 |
|
59 |
lemma all_simps: |
|
69590 | 60 |
\<open>(\<forall>x. P) \<longleftrightarrow> P\<close> |
61 |
\<open>\<And>P Q. (\<forall>x. P(x) \<and> Q(x)) \<longleftrightarrow> (\<forall>x. P(x)) \<and> (\<forall>x. Q(x))\<close> |
|
62 |
\<open>\<And>P Q. (\<forall>x. P(x) \<and> Q) \<longleftrightarrow> (\<forall>x. P(x)) \<and> Q\<close> |
|
63 |
\<open>\<And>P Q. (\<forall>x. P \<and> Q(x)) \<longleftrightarrow> P \<and> (\<forall>x. Q(x))\<close> |
|
64 |
\<open>\<And>P Q. (\<forall>x. P(x) \<or> Q) \<longleftrightarrow> (\<forall>x. P(x)) \<or> Q\<close> |
|
65 |
\<open>\<And>P Q. (\<forall>x. P \<or> Q(x)) \<longleftrightarrow> P \<or> (\<forall>x. Q(x))\<close> |
|
19820 | 66 |
by blast+ |
67 |
||
68 |
lemmas mini_simps = demorgans nnf_simps ex_simps all_simps |
|
69 |
||
60770 | 70 |
ML \<open> |
69593 | 71 |
val mini_ss = simpset_of (\<^context> addsimps @{thms mini_simps}); |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58838
diff
changeset
|
72 |
fun mini_tac ctxt = |
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58838
diff
changeset
|
73 |
resolve_tac ctxt @{thms ccontr} THEN' asm_full_simp_tac (put_simpset mini_ss ctxt); |
60770 | 74 |
\<close> |
19820 | 75 |
|
76 |
end |