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