src/HOL/simpdata.ML
changeset 17778 93d7e524417a
parent 17325 d9d50222808e
child 17875 d81094515061
     1.1 --- a/src/HOL/simpdata.ML	Fri Oct 07 18:49:20 2005 +0200
     1.2 +++ b/src/HOL/simpdata.ML	Fri Oct 07 20:41:10 2005 +0200
     1.3 @@ -135,6 +135,39 @@
     1.4    Simplifier.simproc (Theory.sign_of (the_context ()))
     1.5      "defined ALL" ["ALL x. P x"] Quantifier1.rearrange_all;
     1.6  
     1.7 +
     1.8 +(*** simproc for proving "(y = x) == False" from prmise "~(x = y)" ***)
     1.9 +
    1.10 +val use_neq_simproc = ref true;
    1.11 +
    1.12 +local
    1.13 +
    1.14 +val neq_to_EQ_False = thm "not_sym" RS Eq_FalseI;
    1.15 +
    1.16 +fun neq_prover sg ss (eq $ lhs $ rhs) =
    1.17 +let
    1.18 +  fun test thm = (case #prop(rep_thm thm) of
    1.19 +                    _ $ (Not $ (eq' $ l' $ r')) =>
    1.20 +                      Not = HOLogic.Not andalso eq' = eq andalso
    1.21 +                      r' aconv lhs andalso l' aconv rhs
    1.22 +                  | _ => false)
    1.23 +in
    1.24 +  if !use_neq_simproc then
    1.25 +    case Library.find_first test (prems_of_ss ss) of NONE => NONE
    1.26 +    | SOME thm => SOME (thm RS neq_to_EQ_False)
    1.27 +  else NONE
    1.28 +end
    1.29 +
    1.30 +in
    1.31 +
    1.32 +val neq_simproc =
    1.33 +  Simplifier.simproc (the_context ()) "neq_simproc" ["x = y"] neq_prover;
    1.34 +
    1.35 +end;
    1.36 +
    1.37 +
    1.38 +
    1.39 +
    1.40  (*** Simproc for Let ***)
    1.41  
    1.42  val use_let_simproc = ref true;
    1.43 @@ -336,7 +369,7 @@
    1.44         disj_not1, not_all, not_ex, cases_simp,
    1.45         thm "the_eq_trivial", the_sym_eq_trivial]
    1.46       @ ex_simps @ all_simps @ simp_thms)
    1.47 -     addsimprocs [defALL_regroup,defEX_regroup,let_simproc]
    1.48 +     addsimprocs [defALL_regroup,defEX_regroup,neq_simproc,let_simproc]
    1.49       addcongs [imp_cong, simp_implies_cong]
    1.50       addsplits [split_if];
    1.51