src/HOL/simpdata.ML
 changeset 13568 6b12df05f358 parent 13462 56610e2ba220 child 13600 9702c8636a7b
```     1.1 --- a/src/HOL/simpdata.ML	Wed Sep 18 18:19:43 2002 +0200
1.2 +++ b/src/HOL/simpdata.ML	Thu Sep 19 16:00:27 2002 +0200
1.3 @@ -136,18 +136,18 @@
1.4
1.5  (*Make meta-equalities.  The operator below is Trueprop*)
1.6
1.7 -fun mk_meta_eq r = r RS eq_reflection;
1.8 +fun mk_meta_eq r = r nRS eq_reflection;
1.9  fun safe_mk_meta_eq r = mk_meta_eq r handle Thm.THM _ => r;
1.10
1.11  fun mk_eq th = case concl_of th of
1.12          Const("==",_)\$_\$_       => th
1.13      |   _\$(Const("op =",_)\$_\$_) => mk_meta_eq th
1.14 -    |   _\$(Const("Not",_)\$_)    => th RS Eq_FalseI
1.15 -    |   _                       => th RS Eq_TrueI;
1.16 -(* last 2 lines requires all formulae to be of the from Trueprop(.) *)
1.17 +    |   _\$(Const("Not",_)\$_)    => th nRS Eq_FalseI
1.18 +    |   _                       => th nRS Eq_TrueI;
1.19 +(* Expects Trueprop(.) if not == *)
1.20
1.21  fun mk_eq_True r =
1.22 -  Some (r RS meta_eq_to_obj_eq RS Eq_TrueI) handle Thm.THM _ => None;
1.23 +  Some (r nRS meta_eq_to_obj_eq nRS Eq_TrueI) handle Thm.THM _ => None;
1.24
1.25  (*Congruence rules for = (instead of ==)*)
1.26  fun mk_meta_cong rl =
1.27 @@ -188,21 +188,15 @@
1.29  val Delsplits        = Splitter.Delsplits;
1.30
1.31 -(*In general it seems wrong to add distributive laws by default: they
1.32 -  might cause exponential blow-up.  But imp_disjL has been in for a while
1.33 -  and cannot be removed without affecting existing proofs.  Moreover,
1.34 -  rewriting by "(P|Q --> R) = ((P-->R)&(Q-->R))" might be justified on the
1.35 -  grounds that it allows simplification of R in the two cases.*)
1.36 -
1.37  val mksimps_pairs =
1.38    [("op -->", [mp]), ("op &", [conjunct1,conjunct2]),
1.39     ("All", [spec]), ("True", []), ("False", []),
1.40     ("If", [if_bool_eq_conj RS iffD1])];
1.41
1.42 -(* ###FIXME: move to Provers/simplifier.ML
1.43 +(*
1.44  val mk_atomize:      (string * thm list) list -> thm -> thm list
1.45 +looks too specific to move it somewhere else
1.46  *)
1.47 -(* ###FIXME: move to Provers/simplifier.ML *)
1.48  fun mk_atomize pairs =
1.49    let fun atoms th =
1.50          (case concl_of th of
1.51 @@ -210,7 +204,7 @@
1.53                  Const(a,_) =>
1.54                    (case assoc(pairs,a) of
1.55 -                     Some(rls) => flat (map atoms ([th] RL rls))
1.56 +                     Some(rls) => flat (map atoms (map (apl(th,op nRS)) rls))
1.57                     | None => [th])
1.58                | _ => [th])
1.59           | _ => [th])
1.60 @@ -237,6 +231,12 @@
1.61      setmkeqTrue mk_eq_True
1.62      setmkcong mk_meta_cong;
1.63
1.64 +(*In general it seems wrong to add distributive laws by default: they
1.65 +  might cause exponential blow-up.  But imp_disjL has been in for a while
1.66 +  and cannot be removed without affecting existing proofs.  Moreover,
1.67 +  rewriting by "(P|Q --> R) = ((P-->R)&(Q-->R))" might be justified on the
1.68 +  grounds that it allows simplification of R in the two cases.*)
1.69 +
1.70  val HOL_ss =