src/HOL/Set.ML
changeset 3912 4ed64ad7fb42
parent 3909 e48e2fb8b895
child 3919 c036caebfc75
     1.1 --- a/src/HOL/Set.ML	Fri Oct 17 10:58:44 1997 +0200
     1.2 +++ b/src/HOL/Set.ML	Fri Oct 17 11:00:00 1997 +0200
     1.3 @@ -645,6 +645,22 @@
     1.4  (*** Set reasoning tools ***)
     1.5  
     1.6  
     1.7 +(** Rewrite rules for boolean case-splitting: faster than 
     1.8 +	setloop split_tac[expand_if]
     1.9 +**)
    1.10 +
    1.11 +bind_thm ("expand_if_eq1", read_instantiate [("P", "%x. x = ?b")] expand_if);
    1.12 +bind_thm ("expand_if_eq2", read_instantiate [("P", "%x. ?a = x")] expand_if);
    1.13 +
    1.14 +bind_thm ("expand_if_mem1", 
    1.15 +    read_instantiate_sg (sign_of Set.thy) [("P", "%x. x : ?b")] expand_if);
    1.16 +bind_thm ("expand_if_mem2", 
    1.17 +    read_instantiate_sg (sign_of Set.thy) [("P", "%x. ?a : x")] expand_if);
    1.18 +
    1.19 +val expand_ifs = [if_bool_eq, expand_if_eq1, expand_if_eq2,
    1.20 +		  expand_if_mem1, expand_if_mem2];
    1.21 +
    1.22 +
    1.23  (*Each of these has ALREADY been added to !simpset above.*)
    1.24  val mem_simps = [insert_iff, empty_iff, Un_iff, Int_iff, Compl_iff, Diff_iff, 
    1.25                   mem_Collect_eq,