# HG changeset patch
# User paulson
# Date 877079374 -7200
# Node ID 9e393b363c71930c10b595265c9359945655c651
# Parent  96e28b16861c6972f8536fd09e805d74daa2baed
New rewrite rules for simplifying conditionals

diff -r 96e28b16861c -r 9e393b363c71 src/ZF/upair.ML
--- a/src/ZF/upair.ML	Fri Oct 17 11:00:50 1997 +0200
+++ b/src/ZF/upair.ML	Fri Oct 17 11:09:34 1997 +0200
@@ -261,6 +261,20 @@
            (Asm_simp_tac 1),
            (Asm_simp_tac 1) ]);
 
+(** Rewrite rules for boolean case-splitting: faster than 
+	setloop split_tac[expand_if]
+**)
+
+bind_thm ("expand_if_eq1", read_instantiate [("P", "%x. x = ?b")] expand_if);
+bind_thm ("expand_if_eq2", read_instantiate [("P", "%x. ?a = x")] expand_if);
+
+bind_thm ("expand_if_mem1", read_instantiate [("P", "%x. x : ?b")] expand_if);
+bind_thm ("expand_if_mem2", read_instantiate [("P", "%x. ?a : x")] expand_if);
+
+val expand_ifs = [expand_if_eq1, expand_if_eq2,
+		  expand_if_mem1, expand_if_mem2];
+
+(*Logically equivalent to expand_if_mem2*)
 qed_goal "if_iff" ZF.thy "a: if(P,x,y) <-> P & a:x | ~P & a:y"
  (fn _=> [ (simp_tac (!simpset setloop split_tac [expand_if]) 1) ]);