# HG changeset patch
# User paulson
# Date 844937174 -7200
# Node ID 8659e3063a3054915a3fe822442205e5fadd1a95
# Parent  c2da3ca231aba705e2efa6c6a5a37bdbd2eb9524
Addition of de Morgan laws

diff -r c2da3ca231ab -r 8659e3063a30 src/HOL/simpdata.ML
--- a/src/HOL/simpdata.ML	Thu Oct 10 10:45:20 1996 +0200
+++ b/src/HOL/simpdata.ML	Thu Oct 10 10:46:14 1996 +0200
@@ -106,24 +106,24 @@
 
   fun gen_all th = forall_elim_vars (#maxidx(rep_thm th)+1) th;
 
-  val simp_thms = map prover
-   [ "(x=x) = True",
-     "(~True) = False", "(~False) = True", "(~ ~ P) = P",
-     "(~P) ~= P", "P ~= (~P)", "(P ~= Q) = (P = (~Q))",
-     "(True=P) = P", "(P=True) = P",
-     "(True --> P) = P", "(False --> P) = True", 
-     "(P --> True) = True", "(P --> P) = True",
-     "(P --> False) = (~P)", "(P --> ~P) = (~P)",
-     "(P & True) = P", "(True & P) = P", 
-     "(P & False) = False", "(False & P) = False", "(P & P) = P",
-     "(P | True) = True", "(True | P) = True", 
-     "(P | False) = P", "(False | P) = P", "(P | P) = P",
-     "((~P) = (~Q)) = (P=Q)",
-     "(!x.P) = P", "(? x.P) = P", "? x. x=t", 
-     "(? x. x=t & P(x)) = P(t)", "(? x. t=x & P(x)) = P(t)", 
-     "(! x. x=t --> P(x)) = P(t)", "(! x. t=x --> P(x)) = P(t)" ];
+in
 
-in
+val simp_thms = map prover
+ [ "(x=x) = True",
+   "(~True) = False", "(~False) = True", "(~ ~ P) = P",
+   "(~P) ~= P", "P ~= (~P)", "(P ~= Q) = (P = (~Q))",
+   "(True=P) = P", "(P=True) = P",
+   "(True --> P) = P", "(False --> P) = True", 
+   "(P --> True) = True", "(P --> P) = True",
+   "(P --> False) = (~P)", "(P --> ~P) = (~P)",
+   "(P & True) = P", "(True & P) = P", 
+   "(P & False) = False", "(False & P) = False", "(P & P) = P",
+   "(P | True) = True", "(True | P) = True", 
+   "(P | False) = P", "(False | P) = P", "(P | P) = P",
+   "((~P) = (~Q)) = (P=Q)",
+   "(!x.P) = P", "(? x.P) = P", "? x. x=t", 
+   "(? x. x=t & P(x)) = P(t)", "(? x. t=x & P(x)) = P(t)", 
+   "(! x. x=t --> P(x)) = P(t)", "(! x. t=x --> P(x)) = P(t)" ];
 
 val meta_eq_to_obj_eq = prove_goal HOL.thy "x==y ==> x=y"
   (fn [prem] => [rewtac prem, rtac refl 1]);
@@ -201,17 +201,6 @@
                  "(ALL x. P x --> Q) = ((EX x.P x) --> Q)",
                  "(ALL x. P --> Q x) = (P --> (ALL x.Q x))"];
 
-val HOL_ss = empty_ss
-      setmksimps (mksimps mksimps_pairs)
-      setsolver (fn prems => resolve_tac (TrueI::refl::prems) ORELSE' atac
-                             ORELSE' etac FalseE)
-      setsubgoaler asm_simp_tac
-      addsimps ([if_True, if_False, o_apply, imp_disj, conj_assoc, disj_assoc,
-                 cases_simp]
-        @ ex_simps @ all_simps @ simp_thms)
-      addcongs [imp_cong];
-
-
 (*In general it seems wrong to add distributive laws by default: they
   might cause exponential blow-up.  But imp_disj has been in for a while
   and cannot be removed without affecting existing proofs.  Moreover, 
@@ -318,6 +307,17 @@
 prove "all_conj_distrib" "(!x. P(x) & Q(x)) = ((! x. P(x)) & (! x. Q(x)))";
 
 
+val HOL_ss = empty_ss
+      setmksimps (mksimps mksimps_pairs)
+      setsolver (fn prems => resolve_tac (TrueI::refl::prems) ORELSE' atac
+                             ORELSE' etac FalseE)
+      setsubgoaler asm_simp_tac
+      addsimps ([if_True, if_False, o_apply, imp_disj, conj_assoc, disj_assoc,
+                 de_Morgan_conj, de_Morgan_disj, not_all, not_ex, cases_simp]
+        @ ex_simps @ all_simps @ simp_thms)
+      addcongs [imp_cong];
+
+
 qed_goal "if_cancel" HOL.thy "(if c then x else x) = x"
   (fn _ => [simp_tac (HOL_ss setloop (split_tac [expand_if])) 1]);