src/FOL/ex/Miniscope.thy
author haftmann
Tue, 10 Jul 2007 17:30:50 +0200
changeset 23709 fd31da8f752a
parent 19820 0d7564c798d0
child 26342 0f65fa163304
permissions -rw-r--r--
moved lfp_induct2 here
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
19820
0d7564c798d0 removed obsolete ML files;
wenzelm
parents:
diff changeset
     1
(*  Title:      FOL/ex/Miniscope.thy
0d7564c798d0 removed obsolete ML files;
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
0d7564c798d0 removed obsolete ML files;
wenzelm
parents:
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
0d7564c798d0 removed obsolete ML files;
wenzelm
parents:
diff changeset
     4
    Copyright   1994  University of Cambridge
0d7564c798d0 removed obsolete ML files;
wenzelm
parents:
diff changeset
     5
0d7564c798d0 removed obsolete ML files;
wenzelm
parents:
diff changeset
     6
Classical First-Order Logic.
0d7564c798d0 removed obsolete ML files;
wenzelm
parents:
diff changeset
     7
Conversion to nnf/miniscope format: pushing quantifiers in.
0d7564c798d0 removed obsolete ML files;
wenzelm
parents:
diff changeset
     8
Demonstration of formula rewriting by proof.
0d7564c798d0 removed obsolete ML files;
wenzelm
parents:
diff changeset
     9
*)
0d7564c798d0 removed obsolete ML files;
wenzelm
parents:
diff changeset
    10
0d7564c798d0 removed obsolete ML files;
wenzelm
parents:
diff changeset
    11
theory Miniscope
0d7564c798d0 removed obsolete ML files;
wenzelm
parents:
diff changeset
    12
imports FOL
0d7564c798d0 removed obsolete ML files;
wenzelm
parents:
diff changeset
    13
begin
0d7564c798d0 removed obsolete ML files;
wenzelm
parents:
diff changeset
    14
0d7564c798d0 removed obsolete ML files;
wenzelm
parents:
diff changeset
    15
0d7564c798d0 removed obsolete ML files;
wenzelm
parents:
diff changeset
    16
lemmas ccontr = FalseE [THEN classical]
0d7564c798d0 removed obsolete ML files;
wenzelm
parents:
diff changeset
    17
0d7564c798d0 removed obsolete ML files;
wenzelm
parents:
diff changeset
    18
subsection {* Negation Normal Form *}
0d7564c798d0 removed obsolete ML files;
wenzelm
parents:
diff changeset
    19
0d7564c798d0 removed obsolete ML files;
wenzelm
parents:
diff changeset
    20
subsubsection {* de Morgan laws *}
0d7564c798d0 removed obsolete ML files;
wenzelm
parents:
diff changeset
    21
0d7564c798d0 removed obsolete ML files;
wenzelm
parents:
diff changeset
    22
lemma demorgans:
0d7564c798d0 removed obsolete ML files;
wenzelm
parents:
diff changeset
    23
  "~(P&Q) <-> ~P | ~Q"
0d7564c798d0 removed obsolete ML files;
wenzelm
parents:
diff changeset
    24
  "~(P|Q) <-> ~P & ~Q"
0d7564c798d0 removed obsolete ML files;
wenzelm
parents:
diff changeset
    25
  "~~P <-> P"
0d7564c798d0 removed obsolete ML files;
wenzelm
parents:
diff changeset
    26
  "!!P. ~(ALL x. P(x)) <-> (EX x. ~P(x))"
0d7564c798d0 removed obsolete ML files;
wenzelm
parents:
diff changeset
    27
  "!!P. ~(EX x. P(x)) <-> (ALL x. ~P(x))"
0d7564c798d0 removed obsolete ML files;
wenzelm
parents:
diff changeset
    28
  by blast+
0d7564c798d0 removed obsolete ML files;
wenzelm
parents:
diff changeset
    29
0d7564c798d0 removed obsolete ML files;
wenzelm
parents:
diff changeset
    30
(*** Removal of --> and <-> (positive and negative occurrences) ***)
0d7564c798d0 removed obsolete ML files;
wenzelm
parents:
diff changeset
    31
(*Last one is important for computing a compact CNF*)
0d7564c798d0 removed obsolete ML files;
wenzelm
parents:
diff changeset
    32
lemma nnf_simps:
0d7564c798d0 removed obsolete ML files;
wenzelm
parents:
diff changeset
    33
  "(P-->Q) <-> (~P | Q)"
0d7564c798d0 removed obsolete ML files;
wenzelm
parents:
diff changeset
    34
  "~(P-->Q) <-> (P & ~Q)"
0d7564c798d0 removed obsolete ML files;
wenzelm
parents:
diff changeset
    35
  "(P<->Q) <-> (~P | Q) & (~Q | P)"
0d7564c798d0 removed obsolete ML files;
wenzelm
parents:
diff changeset
    36
  "~(P<->Q) <-> (P | Q) & (~P | ~Q)"
0d7564c798d0 removed obsolete ML files;
wenzelm
parents:
diff changeset
    37
  by blast+
0d7564c798d0 removed obsolete ML files;
wenzelm
parents:
diff changeset
    38
0d7564c798d0 removed obsolete ML files;
wenzelm
parents:
diff changeset
    39
0d7564c798d0 removed obsolete ML files;
wenzelm
parents:
diff changeset
    40
(* BEWARE: rewrite rules for <-> can confuse the simplifier!! *)
0d7564c798d0 removed obsolete ML files;
wenzelm
parents:
diff changeset
    41
0d7564c798d0 removed obsolete ML files;
wenzelm
parents:
diff changeset
    42
subsubsection {* Pushing in the existential quantifiers *}
0d7564c798d0 removed obsolete ML files;
wenzelm
parents:
diff changeset
    43
0d7564c798d0 removed obsolete ML files;
wenzelm
parents:
diff changeset
    44
lemma ex_simps:
0d7564c798d0 removed obsolete ML files;
wenzelm
parents:
diff changeset
    45
  "(EX x. P) <-> P"
0d7564c798d0 removed obsolete ML files;
wenzelm
parents:
diff changeset
    46
  "!!P Q. (EX x. P(x) & Q) <-> (EX x. P(x)) & Q"
0d7564c798d0 removed obsolete ML files;
wenzelm
parents:
diff changeset
    47
  "!!P Q. (EX x. P & Q(x)) <-> P & (EX x. Q(x))"
0d7564c798d0 removed obsolete ML files;
wenzelm
parents:
diff changeset
    48
  "!!P Q. (EX x. P(x) | Q(x)) <-> (EX x. P(x)) | (EX x. Q(x))"
0d7564c798d0 removed obsolete ML files;
wenzelm
parents:
diff changeset
    49
  "!!P Q. (EX x. P(x) | Q) <-> (EX x. P(x)) | Q"
0d7564c798d0 removed obsolete ML files;
wenzelm
parents:
diff changeset
    50
  "!!P Q. (EX x. P | Q(x)) <-> P | (EX x. Q(x))"
0d7564c798d0 removed obsolete ML files;
wenzelm
parents:
diff changeset
    51
  by blast+
0d7564c798d0 removed obsolete ML files;
wenzelm
parents:
diff changeset
    52
0d7564c798d0 removed obsolete ML files;
wenzelm
parents:
diff changeset
    53
0d7564c798d0 removed obsolete ML files;
wenzelm
parents:
diff changeset
    54
subsubsection {* Pushing in the universal quantifiers *}
0d7564c798d0 removed obsolete ML files;
wenzelm
parents:
diff changeset
    55
0d7564c798d0 removed obsolete ML files;
wenzelm
parents:
diff changeset
    56
lemma all_simps:
0d7564c798d0 removed obsolete ML files;
wenzelm
parents:
diff changeset
    57
  "(ALL x. P) <-> P"
0d7564c798d0 removed obsolete ML files;
wenzelm
parents:
diff changeset
    58
  "!!P Q. (ALL x. P(x) & Q(x)) <-> (ALL x. P(x)) & (ALL x. Q(x))"
0d7564c798d0 removed obsolete ML files;
wenzelm
parents:
diff changeset
    59
  "!!P Q. (ALL x. P(x) & Q) <-> (ALL x. P(x)) & Q"
0d7564c798d0 removed obsolete ML files;
wenzelm
parents:
diff changeset
    60
  "!!P Q. (ALL x. P & Q(x)) <-> P & (ALL x. Q(x))"
0d7564c798d0 removed obsolete ML files;
wenzelm
parents:
diff changeset
    61
  "!!P Q. (ALL x. P(x) | Q) <-> (ALL x. P(x)) | Q"
0d7564c798d0 removed obsolete ML files;
wenzelm
parents:
diff changeset
    62
  "!!P Q. (ALL x. P | Q(x)) <-> P | (ALL x. Q(x))"
0d7564c798d0 removed obsolete ML files;
wenzelm
parents:
diff changeset
    63
  by blast+
0d7564c798d0 removed obsolete ML files;
wenzelm
parents:
diff changeset
    64
0d7564c798d0 removed obsolete ML files;
wenzelm
parents:
diff changeset
    65
lemmas mini_simps = demorgans nnf_simps ex_simps all_simps
0d7564c798d0 removed obsolete ML files;
wenzelm
parents:
diff changeset
    66
0d7564c798d0 removed obsolete ML files;
wenzelm
parents:
diff changeset
    67
ML {*
0d7564c798d0 removed obsolete ML files;
wenzelm
parents:
diff changeset
    68
val mini_ss = simpset() addsimps (thms "mini_simps");
0d7564c798d0 removed obsolete ML files;
wenzelm
parents:
diff changeset
    69
val mini_tac = rtac (thm "ccontr") THEN' asm_full_simp_tac mini_ss;
0d7564c798d0 removed obsolete ML files;
wenzelm
parents:
diff changeset
    70
*}
0d7564c798d0 removed obsolete ML files;
wenzelm
parents:
diff changeset
    71
0d7564c798d0 removed obsolete ML files;
wenzelm
parents:
diff changeset
    72
end