src/HOL/simpdata.ML
changeset 4718 fc2ba9fb2135
parent 4681 a331c1f5a23e
child 4743 b3bfcbd9fb93
     1.1 --- a/src/HOL/simpdata.ML	Tue Mar 10 18:26:27 1998 +0100
     1.2 +++ b/src/HOL/simpdata.ML	Tue Mar 10 18:31:32 1998 +0100
     1.3 @@ -208,6 +208,8 @@
     1.4  prove "de_Morgan_conj" "(~(P & Q)) = (~P | ~Q)";
     1.5  prove "not_imp" "(~(P --> Q)) = (P & ~Q)";
     1.6  prove "not_iff" "(P~=Q) = (P = (~Q))";
     1.7 +prove "not1_or" "(~P | Q) = (P --> Q)";
     1.8 +prove "not2_or" "(P | ~Q) = (Q --> P)"; (* changes orientation :-( *)
     1.9  
    1.10  (*Avoids duplication of subgoals after expand_if, when the true and false 
    1.11    cases boil down to the same thing.*) 
    1.12 @@ -354,6 +356,9 @@
    1.13  qed_goal "if_cancel" HOL.thy "(if c then x else x) = x"
    1.14    (K [split_tac [expand_if] 1, blast_tac HOL_cs 1]);
    1.15  
    1.16 +qed_goal "if_eq_cancel" HOL.thy "(if x = y then y else x) = x"
    1.17 +  (K [split_tac [expand_if] 1, blast_tac HOL_cs 1]);
    1.18 +
    1.19  (** 'if' congruence rules: neither included by default! *)
    1.20  
    1.21  (*Simplifies x assuming c and y assuming ~c*)
    1.22 @@ -402,10 +407,10 @@
    1.23      HOL_basic_ss addsimps 
    1.24       ([triv_forall_equality, (* prunes params *)
    1.25         True_implies_equals, (* prune asms `True' *)
    1.26 -       if_True, if_False, if_cancel,
    1.27 +       if_True, if_False, if_cancel, if_eq_cancel,
    1.28         o_apply, imp_disjL, conj_assoc, disj_assoc,
    1.29         de_Morgan_conj, de_Morgan_disj, imp_disj1, imp_disj2, not_imp,
    1.30 -       not_all, not_ex, cases_simp]
    1.31 +       not1_or, not_all, not_ex, cases_simp]
    1.32       @ ex_simps @ all_simps @ simp_thms)
    1.33       addsimprocs [defALL_regroup,defEX_regroup]
    1.34       addcongs [imp_cong];