src/HOL/simpdata.ML
changeset 2251 e0e3836f333d
parent 2250 891eb76b8045
child 2263 c741309167bf
     1.1 --- a/src/HOL/simpdata.ML	Wed Nov 27 13:13:21 1996 +0100
     1.2 +++ b/src/HOL/simpdata.ML	Wed Nov 27 13:51:49 1996 +0100
     1.3 @@ -262,6 +262,9 @@
     1.4                     "(if P then Q else R) = ((P-->Q) & (~P-->R))"
     1.5                     (fn _ => [rtac expand_if 1]);
     1.6  
     1.7 +qed_goal "if_cancel" HOL.thy "(if c then x else x) = x"
     1.8 +  (fn _ => [split_tac [expand_if] 1, fast_tac HOL_cs 1]);
     1.9 +
    1.10  (** 'if' congruence rules: neither included by default! *)
    1.11  
    1.12  (*Simplifies x assuming c and y assuming ~c*)
    1.13 @@ -298,7 +301,8 @@
    1.14        setsolver (fn prems => resolve_tac (TrueI::refl::prems) ORELSE' atac
    1.15                               ORELSE' etac FalseE)
    1.16        setsubgoaler asm_simp_tac
    1.17 -      addsimps ([if_True, if_False, o_apply, imp_disjL, conj_assoc, disj_assoc,
    1.18 +      addsimps ([if_True, if_False, if_cancel,
    1.19 +		 o_apply, imp_disjL, conj_assoc, disj_assoc,
    1.20                   de_Morgan_conj, de_Morgan_disj, not_all, not_ex, cases_simp]
    1.21          @ ex_simps @ all_simps @ simp_thms)
    1.22        addcongs [imp_cong];
    1.23 @@ -315,9 +319,6 @@
    1.24  end;
    1.25  
    1.26  
    1.27 -qed_goal "if_cancel" HOL.thy "(if c then x else x) = x"
    1.28 -  (fn _ => [simp_tac (HOL_ss setloop (split_tac [expand_if])) 1]);
    1.29 -
    1.30  qed_goal "if_distrib" HOL.thy
    1.31    "f(if c then x else y) = (if c then f x else f y)" 
    1.32    (fn _ => [simp_tac (HOL_ss setloop (split_tac [expand_if])) 1]);
    1.33 @@ -330,7 +331,7 @@
    1.34  
    1.35  (*** Install simpsets and datatypes in theory structure ***)
    1.36  
    1.37 -simpset := HOL_ss addsimps [if_cancel];
    1.38 +simpset := HOL_ss;
    1.39  
    1.40  exception SS_DATA of simpset;
    1.41