src/HOL/simpdata.ML
 changeset 1948 78e5bfcbc1e9 parent 1922 ce495557ac33 child 1968 daa97cc96feb
```--- a/src/HOL/simpdata.ML	Tue Sep 03 19:07:23 1996 +0200
+++ b/src/HOL/simpdata.ML	Thu Sep 05 10:23:55 1996 +0200
@@ -71,6 +71,7 @@
"(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. x=t --> P(x)) = P(t)" ];

@@ -87,6 +88,9 @@

val imp_disj   = prover "(P|Q --> R) = ((P-->R)&(Q-->R))";

+(*Avoids duplication of subgoals after expand_if, when the true and false
+  cases boil down to the same thing.*)
+val cases_simp = prover "((P --> Q) & (~P --> Q)) = Q";

val if_True = prove_goalw HOL.thy [if_def] "(if True then x else y) = x"
(fn _=>[fast_tac (HOL_cs addIs [select_equality]) 1]);
@@ -131,18 +135,37 @@
val o_apply = prove_goalw HOL.thy [o_def] "(f o g)(x) = f(g(x))"
(fn _ => [rtac refl 1]);

+(*Miniscoping: pushing in existential quantifiers*)
+val ex_simps = map prover
+		["(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)   = ((EX x.P x) | Q)",
+		 "(EX x. P | Q x)   = (P | (EX x.Q x))",
+		 "(EX x. P x --> Q) = ((ALL x.P x) --> Q)",
+		 "(EX x. P --> Q x) = (P --> (EX x.Q x))"];
+
+(*Miniscoping: pushing in universal quantifiers*)
+val all_simps = map prover
+		["(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))",
+		 "(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]
-        @ simp_thms)
+      addsimps ([if_True, if_False, o_apply, imp_disj, conj_assoc, disj_assoc,
+		 cases_simp]
+        @ ex_simps @ all_simps @ simp_thms)