--- a/simpdata.ML Thu Aug 25 11:01:45 1994 +0200
+++ b/simpdata.ML Tue Aug 30 10:04:49 1994 +0200
@@ -18,20 +18,20 @@
val not_P_imp_P_iff_F = prover "~P --> (P = False)" RS mp;
val not_P_imp_P_eq_False = not_P_imp_P_iff_F RS eq_reflection;
-fun atomize r =
- case concl_of r of
- Const("Trueprop",_) $ p =>
- (case p of
- Const("op -->",_)$_$_ => atomize(r RS mp)
- | Const("op &",_)$_$_ => atomize(r RS conjunct1) @
- atomize(r RS conjunct2)
- | Const("All",_)$_ => atomize(r RS spec)
- | Const("True",_) => []
- | Const("False",_) => []
- | _ => [r])
- | _ => [r];
+fun atomize pairs =
+ let fun atoms th =
+ (case concl_of th of
+ Const("Trueprop",_) $ p =>
+ (case head_of p of
+ Const(a,_) =>
+ (case assoc(pairs,a) of
+ Some(rls) => flat (map atoms ([th] RL rls))
+ | None => [th])
+ | _ => [th])
+ | _ => [th])
+ in atoms end;
-fun mk_eq r = case concl_of r of
+fun mk_meta_eq r = case concl_of r of
Const("==",_)$_$_ => r
| _$(Const("op =",_)$_$_) => r RS eq_reflection
| _$(Const("not",_)$_) => r RS not_P_imp_P_eq_False
@@ -40,8 +40,6 @@
fun gen_all th = forall_elim_vars (#maxidx(rep_thm th)+1) th;
-fun mk_rews thm = map mk_eq (atomize(gen_all thm));
-
val imp_cong = impI RSN
(2, prove_goal HOL.thy "(P=P')--> (P'--> (Q=Q'))--> ((P-->Q) = (P'-->Q'))"
(fn _=> [fast_tac HOL_cs 1]) RS mp RS mp);
@@ -56,6 +54,7 @@
"(True=P) = P", "(P=True) = P",
"(True --> P) = P", "(False --> P) = True",
"(P --> True) = True", "(P --> P) = True",
+ "(P --> False) = (~P)", "(P --> ~P) = (~P)",
"(P & True) = P", "(True & P) = P",
"(P & False) = False", "(False & P) = False", "(P & P) = P",
"(P | True) = True", "(True | P) = True",
@@ -97,8 +96,14 @@
infix addcongs;
fun ss addcongs congs = ss addeqcongs (congs RL [eq_reflection]);
+val mksimps_pairs =
+ [("op -->", [mp]), ("op &", [conjunct1,conjunct2]),
+ ("All", [spec]), ("True", []), ("False", [])];
+
+fun mksimps pairs = map mk_meta_eq o atomize pairs o gen_all;
+
val HOL_ss = empty_ss
- setmksimps mk_rews
+ setmksimps (mksimps mksimps_pairs)
setsolver (fn prems => resolve_tac (TrueI::refl::prems) ORELSE' atac
ORELSE' etac FalseE)
setsubgoaler asm_simp_tac
@@ -106,7 +111,7 @@
addcongs [imp_cong];
fun split_tac splits =
- mk_case_split_tac (meta_eq_to_obj_eq RS iffD2) (map mk_eq splits);
+ mk_case_split_tac (meta_eq_to_obj_eq RS iffD2) (map mk_meta_eq splits);
(* eliminiation of existential quantifiers in assumptions *)