--- a/src/FOL/simpdata.ML Thu Jul 13 11:44:02 2000 +0200
+++ b/src/FOL/simpdata.ML Thu Jul 13 12:56:42 2000 +0200
@@ -6,6 +6,50 @@
Simplification data for FOL
*)
+(*** Addition of rules to simpsets and clasets simultaneously ***) (* FIXME move to Provers/clasimp.ML? *)
+
+infix 4 addIffs delIffs;
+
+(*Takes UNCONDITIONAL theorems of the form A<->B to
+ the Safe Intr rule B==>A and
+ the Safe Destruct rule A==>B.
+ Also ~A goes to the Safe Elim rule A ==> ?R
+ Failing other cases, A is added as a Safe Intr rule*)
+local
+ fun addIff ((cla, simp), th) =
+ (case FOLogic.dest_Trueprop (#prop (rep_thm th)) of
+ (Const("Not", _) $ A) =>
+ cla addSEs [zero_var_indexes (th RS notE)]
+ | (Const("op <->", _) $ _ $ _) =>
+ cla addSIs [zero_var_indexes (th RS iffD2)]
+ addSDs [zero_var_indexes (th RS iffD1)]
+ | _ => cla addSIs [th],
+ simp addsimps [th])
+ handle TERM _ => error ("AddIffs: theorem must be unconditional\n" ^
+ string_of_thm th);
+
+ fun delIff ((cla, simp), th) =
+ (case FOLogic.dest_Trueprop (#prop (rep_thm th)) of
+ (Const ("Not", _) $ A) =>
+ cla delrules [zero_var_indexes (th RS notE)]
+ | (Const("op <->", _) $ _ $ _) =>
+ cla delrules [zero_var_indexes (th RS iffD2),
+ cla_make_elim (zero_var_indexes (th RS iffD1))]
+ | _ => cla delrules [th],
+ simp delsimps [th])
+ handle TERM _ => (warning("DelIffs: ignoring conditional theorem\n" ^
+ string_of_thm th); (cla, simp));
+
+ fun store_clasimp (cla, simp) = (claset_ref () := cla; simpset_ref () := simp)
+in
+val op addIffs = foldl addIff;
+val op delIffs = foldl delIff;
+fun AddIffs thms = store_clasimp ((claset (), simpset ()) addIffs thms);
+fun DelIffs thms = store_clasimp ((claset (), simpset ()) delIffs thms);
+end;
+
+
+
(* Elimination of True from asumptions: *)
val True_implies_equals = prove_goal IFOL.thy