19820

1 
(* Title: FOL/ex/Miniscope.thy


2 
ID: $Id$


3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory


4 
Copyright 1994 University of Cambridge


5 


6 
Classical FirstOrder Logic.


7 
Conversion to nnf/miniscope format: pushing quantifiers in.


8 
Demonstration of formula rewriting by proof.


9 
*)


10 


11 
theory Miniscope


12 
imports FOL


13 
begin


14 


15 


16 
lemmas ccontr = FalseE [THEN classical]


17 


18 
subsection {* Negation Normal Form *}


19 


20 
subsubsection {* de Morgan laws *}


21 


22 
lemma demorgans:


23 
"~(P&Q) <> ~P  ~Q"


24 
"~(PQ) <> ~P & ~Q"


25 
"~~P <> P"


26 
"!!P. ~(ALL x. P(x)) <> (EX x. ~P(x))"


27 
"!!P. ~(EX x. P(x)) <> (ALL x. ~P(x))"


28 
by blast+


29 


30 
(*** Removal of > and <> (positive and negative occurrences) ***)


31 
(*Last one is important for computing a compact CNF*)


32 
lemma nnf_simps:


33 
"(P>Q) <> (~P  Q)"


34 
"~(P>Q) <> (P & ~Q)"


35 
"(P<>Q) <> (~P  Q) & (~Q  P)"


36 
"~(P<>Q) <> (P  Q) & (~P  ~Q)"


37 
by blast+


38 


39 


40 
(* BEWARE: rewrite rules for <> can confuse the simplifier!! *)


41 


42 
subsubsection {* Pushing in the existential quantifiers *}


43 


44 
lemma ex_simps:


45 
"(EX x. P) <> P"


46 
"!!P Q. (EX x. P(x) & Q) <> (EX x. P(x)) & Q"


47 
"!!P Q. (EX x. P & Q(x)) <> P & (EX x. Q(x))"


48 
"!!P Q. (EX x. P(x)  Q(x)) <> (EX x. P(x))  (EX x. Q(x))"


49 
"!!P Q. (EX x. P(x)  Q) <> (EX x. P(x))  Q"


50 
"!!P Q. (EX x. P  Q(x)) <> P  (EX x. Q(x))"


51 
by blast+


52 


53 


54 
subsubsection {* Pushing in the universal quantifiers *}


55 


56 
lemma all_simps:


57 
"(ALL x. P) <> P"


58 
"!!P Q. (ALL x. P(x) & Q(x)) <> (ALL x. P(x)) & (ALL x. Q(x))"


59 
"!!P Q. (ALL x. P(x) & Q) <> (ALL x. P(x)) & Q"


60 
"!!P Q. (ALL x. P & Q(x)) <> P & (ALL x. Q(x))"


61 
"!!P Q. (ALL x. P(x)  Q) <> (ALL x. P(x))  Q"


62 
"!!P Q. (ALL x. P  Q(x)) <> P  (ALL x. Q(x))"


63 
by blast+


64 


65 
lemmas mini_simps = demorgans nnf_simps ex_simps all_simps


66 


67 
ML {*


68 
val mini_ss = simpset() addsimps (thms "mini_simps");


69 
val mini_tac = rtac (thm "ccontr") THEN' asm_full_simp_tac mini_ss;


70 
*}


71 


72 
end
