author oheimb Tue, 10 Mar 1998 18:31:32 +0100 changeset 4718 fc2ba9fb2135 parent 4717 1370ad043564 child 4719 21af5c0be0c9
new rewrite rules not1_or, not2_or, and if_eq_cancel added not1_or and if_eq_cancel to simpset()
 src/HOL/simpdata.ML file | annotate | diff | comparison | revisions
```--- a/src/HOL/simpdata.ML	Tue Mar 10 18:26:27 1998 +0100
+++ b/src/HOL/simpdata.ML	Tue Mar 10 18:31:32 1998 +0100
@@ -208,6 +208,8 @@
prove "de_Morgan_conj" "(~(P & Q)) = (~P | ~Q)";
prove "not_imp" "(~(P --> Q)) = (P & ~Q)";
prove "not_iff" "(P~=Q) = (P = (~Q))";
+prove "not1_or" "(~P | Q) = (P --> Q)";
+prove "not2_or" "(P | ~Q) = (Q --> P)"; (* changes orientation :-( *)

(*Avoids duplication of subgoals after expand_if, when the true and false
cases boil down to the same thing.*)
@@ -354,6 +356,9 @@
qed_goal "if_cancel" HOL.thy "(if c then x else x) = x"
(K [split_tac [expand_if] 1, blast_tac HOL_cs 1]);

+qed_goal "if_eq_cancel" HOL.thy "(if x = y then y else x) = x"
+  (K [split_tac [expand_if] 1, blast_tac HOL_cs 1]);
+
(** 'if' congruence rules: neither included by default! *)

(*Simplifies x assuming c and y assuming ~c*)
@@ -402,10 +407,10 @@