# HG changeset patch
# User wenzelm
# Date 1149716077 -7200
# Node ID 0d7564c798d04c04516765b088acc4b396cd9824
# Parent  14de4d05d27524bff74c055daf5d1856e3b791cc
removed obsolete ML files;

diff -r 14de4d05d275 -r 0d7564c798d0 src/FOL/IsaMakefile
--- 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
 
diff -r 14de4d05d275 -r 0d7564c798d0 src/FOL/ex/Miniscope.thy
--- /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
diff -r 14de4d05d275 -r 0d7564c798d0 src/FOL/ex/ROOT.ML
--- 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";
 
diff -r 14de4d05d275 -r 0d7564c798d0 src/FOL/ex/mini.ML
--- 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;
-