diff -r 7949f97df77a -r 142f1eb707b4 simpdata.ML --- 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);