# HG changeset patch
# User paulson
# Date 844860977 -7200
# Node ID 30a65172e003aa88734a3095dd79aa54f24542d1
# Parent  fb0655539d05dc8567460b6ebd5b20c665a9797c
Added the de Morgan laws (incl quantifier versions) to basic simpset

diff -r fb0655539d05 -r 30a65172e003 src/FOL/simpdata.ML
--- a/src/FOL/simpdata.ML	Wed Oct 09 13:32:33 1996 +0200
+++ b/src/FOL/simpdata.ML	Wed Oct 09 13:36:17 1996 +0200
@@ -83,38 +83,9 @@
   | _ $ (Const("Not",_)$_)      => th RS iff_reflection_F
   | _                           => th RS iff_reflection_T;
 
-structure Induction = InductionFun(struct val spec=IFOL.spec end);
-
-open Simplifier Induction;
-
-(*Add congruence rules for = or <-> (instead of ==) *)
-infix 4 addcongs;
-fun ss addcongs congs =
-    ss addeqcongs (congs RL [eq_reflection,iff_reflection]);
-
-(*Add a simpset to a classical set!*)
-infix 4 addss;
-fun cs addss ss = cs addbefore asm_full_simp_tac ss 1;
-
 
-val IFOL_simps =
-   [refl RS P_iff_T] @ conj_simps @ disj_simps @ not_simps @ 
-    imp_simps @ iff_simps @ quant_simps;
-
-val notFalseI = int_prove_fun "~False";
-val triv_rls = [TrueI,refl,iff_refl,notFalseI];
+(*** Classical laws ***)
 
-val IFOL_ss = 
-  empty_ss 
-  setmksimps (map mk_meta_eq o atomize o gen_all)
-  setsolver  (fn prems => resolve_tac (triv_rls@prems) 
-                          ORELSE' assume_tac
-                          ORELSE' etac FalseE)
-  setsubgoaler asm_simp_tac
-  addsimps IFOL_simps
-  addcongs [imp_cong];
-
-(*Classical version...*)
 fun prove_fun s = 
  (writeln s;  
   prove_goal FOL.thy s
@@ -125,14 +96,6 @@
   cases boil down to the same thing.*) 
 val cases_simp = prove_fun "(P --> Q) & (~P --> Q) <-> Q";
 
-val cla_simps = 
-    cases_simp::
-    map prove_fun
-     ["~(P&Q)  <-> ~P | ~Q",
-      "P | ~P",             "~P | P",
-      "~ ~ P <-> P",        "(~P --> P) <-> P",
-      "(~P <-> ~Q) <-> (P<->Q)"];
-
 (*At present, miniscoping is for classical logic only.  We do NOT include
   distribution of ALL over &, or dually that of EX over |.*)
 
@@ -158,8 +121,6 @@
                  "(ALL x. P(x) --> Q) <-> (EX x.P(x)) --> Q",
                  "(ALL x. P --> Q(x)) <-> P --> (ALL x.Q(x))"];
 
-val FOL_ss = IFOL_ss addsimps (cla_simps @ ex_simps @ all_simps);
-
 fun int_prove nm thm  = qed_goal nm IFOL.thy thm
     (fn prems => [ (cut_facts_tac prems 1), 
                    (Int.fast_tac 1) ]);
@@ -220,3 +181,45 @@
 end;
 
 
+(*** Standard simpsets ***)
+
+structure Induction = InductionFun(struct val spec=IFOL.spec end);
+
+open Simplifier Induction;
+
+(*Add congruence rules for = or <-> (instead of ==) *)
+infix 4 addcongs;
+fun ss addcongs congs =
+    ss addeqcongs (congs RL [eq_reflection,iff_reflection]);
+
+(*Add a simpset to a classical set!*)
+infix 4 addss;
+fun cs addss ss = cs addbefore asm_full_simp_tac ss 1;
+
+val IFOL_simps =
+   [refl RS P_iff_T] @ conj_simps @ disj_simps @ not_simps @ 
+    imp_simps @ iff_simps @ quant_simps;
+
+val notFalseI = int_prove_fun "~False";
+val triv_rls = [TrueI,refl,iff_refl,notFalseI];
+
+val IFOL_ss = 
+  empty_ss 
+  setmksimps (map mk_meta_eq o atomize o gen_all)
+  setsolver  (fn prems => resolve_tac (triv_rls@prems) 
+                          ORELSE' assume_tac
+                          ORELSE' etac FalseE)
+  setsubgoaler asm_simp_tac
+  addsimps IFOL_simps
+  addcongs [imp_cong];
+
+val cla_simps = 
+    [de_Morgan_conj, de_Morgan_disj, not_all, not_ex, cases_simp] @
+    map prove_fun
+     ["~(P&Q)  <-> ~P | ~Q",
+      "P | ~P",             "~P | P",
+      "~ ~ P <-> P",        "(~P --> P) <-> P",
+      "(~P <-> ~Q) <-> (P<->Q)"];
+
+val FOL_ss = IFOL_ss addsimps (cla_simps @ ex_simps @ all_simps);
+