--- a/src/FOL/IsaMakefile Wed Jun 07 23:21:55 2006 +0200
+++ b/src/FOL/IsaMakefile Wed Jun 07 23:34:37 2006 +0200
@@ -45,8 +45,8 @@
$(LOG)/FOL-ex.gz: $(OUT)/FOL$(ML_SUFFIX) ex/First_Order_Logic.thy \
ex/If.thy ex/IffOracle.thy ex/List.ML ex/List.thy ex/LocaleTest.thy \
- ex/Nat.thy ex/Nat2.ML ex/Nat2.thy ex/Natural_Numbers.thy \
- ex/Prolog.thy ex/ROOT.ML ex/Classical.thy ex/document/root.tex\
+ ex/Nat.thy ex/Nat2.ML ex/Nat2.thy ex/Natural_Numbers.thy ex/Miniscope.thy \
+ ex/Prolog.thy ex/ROOT.ML ex/Classical.thy ex/document/root.tex \
ex/Foundation.thy ex/Intuitionistic.thy ex/Intro.thy ex/prop.ML ex/quant.ML
@$(ISATOOL) usedir $(OUT)/FOL ex
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/FOL/ex/Miniscope.thy Wed Jun 07 23:34:37 2006 +0200
@@ -0,0 +1,72 @@
+(* Title: FOL/ex/Miniscope.thy
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1994 University of Cambridge
+
+Classical First-Order Logic.
+Conversion to nnf/miniscope format: pushing quantifiers in.
+Demonstration of formula rewriting by proof.
+*)
+
+theory Miniscope
+imports FOL
+begin
+
+
+lemmas ccontr = FalseE [THEN classical]
+
+subsection {* Negation Normal Form *}
+
+subsubsection {* de Morgan laws *}
+
+lemma demorgans:
+ "~(P&Q) <-> ~P | ~Q"
+ "~(P|Q) <-> ~P & ~Q"
+ "~~P <-> P"
+ "!!P. ~(ALL x. P(x)) <-> (EX x. ~P(x))"
+ "!!P. ~(EX x. P(x)) <-> (ALL x. ~P(x))"
+ by blast+
+
+(*** Removal of --> and <-> (positive and negative occurrences) ***)
+(*Last one is important for computing a compact CNF*)
+lemma nnf_simps:
+ "(P-->Q) <-> (~P | Q)"
+ "~(P-->Q) <-> (P & ~Q)"
+ "(P<->Q) <-> (~P | Q) & (~Q | P)"
+ "~(P<->Q) <-> (P | Q) & (~P | ~Q)"
+ by blast+
+
+
+(* BEWARE: rewrite rules for <-> can confuse the simplifier!! *)
+
+subsubsection {* Pushing in the existential quantifiers *}
+
+lemma ex_simps:
+ "(EX x. P) <-> P"
+ "!!P Q. (EX x. P(x) & Q) <-> (EX x. P(x)) & Q"
+ "!!P Q. (EX x. P & Q(x)) <-> P & (EX x. Q(x))"
+ "!!P Q. (EX x. P(x) | Q(x)) <-> (EX x. P(x)) | (EX x. Q(x))"
+ "!!P Q. (EX x. P(x) | Q) <-> (EX x. P(x)) | Q"
+ "!!P Q. (EX x. P | Q(x)) <-> P | (EX x. Q(x))"
+ by blast+
+
+
+subsubsection {* Pushing in the universal quantifiers *}
+
+lemma all_simps:
+ "(ALL x. P) <-> P"
+ "!!P Q. (ALL x. P(x) & Q(x)) <-> (ALL x. P(x)) & (ALL x. Q(x))"
+ "!!P Q. (ALL x. P(x) & Q) <-> (ALL x. P(x)) & Q"
+ "!!P Q. (ALL x. P & Q(x)) <-> P & (ALL x. Q(x))"
+ "!!P Q. (ALL x. P(x) | Q) <-> (ALL x. P(x)) | Q"
+ "!!P Q. (ALL x. P | Q(x)) <-> P | (ALL x. Q(x))"
+ by blast+
+
+lemmas mini_simps = demorgans nnf_simps ex_simps all_simps
+
+ML {*
+val mini_ss = simpset() addsimps (thms "mini_simps");
+val mini_tac = rtac (thm "ccontr") THEN' asm_full_simp_tac mini_ss;
+*}
+
+end
--- a/src/FOL/ex/ROOT.ML Wed Jun 07 23:21:55 2006 +0200
+++ b/src/FOL/ex/ROOT.ML Wed Jun 07 23:34:37 2006 +0200
@@ -20,7 +20,7 @@
time_use "quant.ML";
writeln"\n** Classical examples **\n";
-time_use "mini.ML";
+time_use_thy "Miniscope";
time_use_thy "Classical";
time_use_thy "If";
--- a/src/FOL/ex/mini.ML Wed Jun 07 23:21:55 2006 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,66 +0,0 @@
-(* Title: FOL/ex/mini
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1994 University of Cambridge
-
-Classical First-Order Logic
-
-Conversion to nnf/miniscope format: pushing quantifiers in
-
-Demonstration of formula rewriting by proof
-*)
-
-val ccontr = FalseE RS classical;
-
-(**** Negation Normal Form ****)
-
-(*** de Morgan laws ***)
-
-fun prove_fun s =
- (writeln s;
- prove_goal FOL.thy s
- (fn prems => [ (cut_facts_tac prems 1),
- (Cla.fast_tac FOL_cs 1) ]));
-
-val demorgans = map prove_fun
- ["~(P&Q) <-> ~P | ~Q",
- "~(P|Q) <-> ~P & ~Q",
- "~~P <-> P",
- "~(ALL x. P(x)) <-> (EX x. ~P(x))",
- "~(EX x. P(x)) <-> (ALL x. ~P(x))"];
-
-(*** Removal of --> and <-> (positive and negative occurrences) ***)
-(*Last one is important for computing a compact CNF*)
-val nnf_simps = map prove_fun
- ["(P-->Q) <-> (~P | Q)",
- "~(P-->Q) <-> (P & ~Q)",
- "(P<->Q) <-> (~P | Q) & (~Q | P)",
- "~(P<->Q) <-> (P | Q) & (~P | ~Q)"];
-
-(* BEWARE: rewrite rules for <-> can confuse the simplifier!! *)
-
-(*** Pushing in the existential quantifiers ***)
-
-val ex_simps = map prove_fun
- ["(EX x. P) <-> P",
- "(EX x. P(x) & Q) <-> (EX x. P(x)) & Q",
- "(EX x. P & Q(x)) <-> P & (EX x. Q(x))",
- "(EX x. P(x) | Q(x)) <-> (EX x. P(x)) | (EX x. Q(x))",
- "(EX x. P(x) | Q) <-> (EX x. P(x)) | Q",
- "(EX x. P | Q(x)) <-> P | (EX x. Q(x))"];
-
-(*** Pushing in the universal quantifiers ***)
-
-val all_simps = map prove_fun
- ["(ALL x. P) <-> P",
- "(ALL x. P(x) & Q(x)) <-> (ALL x. P(x)) & (ALL x. Q(x))",
- "(ALL x. P(x) & Q) <-> (ALL x. P(x)) & Q",
- "(ALL x. P & Q(x)) <-> P & (ALL x. Q(x))",
- "(ALL x. P(x) | Q) <-> (ALL x. P(x)) | Q",
- "(ALL x. P | Q(x)) <-> P | (ALL x. Q(x))"];
-
-
-val mini_ss=FOL_basic_ss addsimps (demorgans @ nnf_simps @ ex_simps @ all_simps);
-
-val mini_tac = rtac ccontr THEN' asm_full_simp_tac mini_ss;
-