--- a/simpdata.ML Thu Sep 16 12:21:07 1993 +0200
+++ b/simpdata.ML Thu Sep 16 14:29:14 1993 +0200
@@ -1,3 +1,11 @@
+(* Title: HOL/simpdata.ML
+ ID: $Id$
+ Author: Tobias Nipkow
+ Copyright 1991 University of Cambridge
+
+Instantiation of the generic simplifier
+*)
+
open Simplifier;
local
@@ -34,10 +42,9 @@
fun mk_rews thm = map mk_eq (atomize(gen_all thm));
-val imp_cong_lemma = impI RSN
+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);
-val imp_meta_cong = imp_cong_lemma RS eq_reflection;
val o_apply = prove_goal HOL.thy "(f o g)(x) = f(g(x))"
(fn _ => [ (stac o_def 1), (rtac refl 1) ]);
@@ -84,15 +91,17 @@
"[| b=c; c ==> x=u; ~c ==> y=v |] ==> if(b,x,y) = if(c,u,v)"
(fn rew::prems =>
[stac rew 1, stac expand_if 1, stac expand_if 1,
- fast_tac (HOL_cs addDs prems) 1]) RS eq_reflection;
+ fast_tac (HOL_cs addDs prems) 1]);
+infix addcongs;
+fun ss addcongs congs = ss addeqcongs (congs RL [eq_reflection]);
val HOL_ss = empty_ss
setmksimps mk_rews
setsolver (fn prems => resolve_tac (TrueI::refl::prems))
setsubgoaler asm_simp_tac
addsimps ([if_True, if_False, o_apply] @ simp_thms)
- addcongs [imp_meta_cong];
+ addcongs [imp_cong];
fun split_tac splits =
mk_case_split_tac (meta_obj_reflection RS iffD2) (map mk_eq splits);