--- a/src/HOL/simpdata.ML Wed Sep 18 18:19:43 2002 +0200
+++ b/src/HOL/simpdata.ML Thu Sep 19 16:00:27 2002 +0200
@@ -136,18 +136,18 @@
(*Make meta-equalities. The operator below is Trueprop*)
-fun mk_meta_eq r = r RS eq_reflection;
+fun mk_meta_eq r = r nRS eq_reflection;
fun safe_mk_meta_eq r = mk_meta_eq r handle Thm.THM _ => r;
fun mk_eq th = case concl_of th of
Const("==",_)$_$_ => th
| _$(Const("op =",_)$_$_) => mk_meta_eq th
- | _$(Const("Not",_)$_) => th RS Eq_FalseI
- | _ => th RS Eq_TrueI;
-(* last 2 lines requires all formulae to be of the from Trueprop(.) *)
+ | _$(Const("Not",_)$_) => th nRS Eq_FalseI
+ | _ => th nRS Eq_TrueI;
+(* Expects Trueprop(.) if not == *)
fun mk_eq_True r =
- Some (r RS meta_eq_to_obj_eq RS Eq_TrueI) handle Thm.THM _ => None;
+ Some (r nRS meta_eq_to_obj_eq nRS Eq_TrueI) handle Thm.THM _ => None;
(*Congruence rules for = (instead of ==)*)
fun mk_meta_cong rl =
@@ -188,21 +188,15 @@
val Addsplits = Splitter.Addsplits;
val Delsplits = Splitter.Delsplits;
-(*In general it seems wrong to add distributive laws by default: they
- might cause exponential blow-up. But imp_disjL has been in for a while
- and cannot be removed without affecting existing proofs. Moreover,
- rewriting by "(P|Q --> R) = ((P-->R)&(Q-->R))" might be justified on the
- grounds that it allows simplification of R in the two cases.*)
-
val mksimps_pairs =
[("op -->", [mp]), ("op &", [conjunct1,conjunct2]),
("All", [spec]), ("True", []), ("False", []),
("If", [if_bool_eq_conj RS iffD1])];
-(* ###FIXME: move to Provers/simplifier.ML
+(*
val mk_atomize: (string * thm list) list -> thm -> thm list
+looks too specific to move it somewhere else
*)
-(* ###FIXME: move to Provers/simplifier.ML *)
fun mk_atomize pairs =
let fun atoms th =
(case concl_of th of
@@ -210,7 +204,7 @@
(case head_of p of
Const(a,_) =>
(case assoc(pairs,a) of
- Some(rls) => flat (map atoms ([th] RL rls))
+ Some(rls) => flat (map atoms (map (apl(th,op nRS)) rls))
| None => [th])
| _ => [th])
| _ => [th])
@@ -237,6 +231,12 @@
setmkeqTrue mk_eq_True
setmkcong mk_meta_cong;
+(*In general it seems wrong to add distributive laws by default: they
+ might cause exponential blow-up. But imp_disjL has been in for a while
+ and cannot be removed without affecting existing proofs. Moreover,
+ rewriting by "(P|Q --> R) = ((P-->R)&(Q-->R))" might be justified on the
+ grounds that it allows simplification of R in the two cases.*)
+
val HOL_ss =
HOL_basic_ss addsimps
([triv_forall_equality, (* prunes params *)