# HG changeset patch # User paulson # Date 867058439 -7200 # Node ID 112cbb8301dcde1e20ff9bae643e3eecfbb9a436 # Parent 5ff4bfab859cd53e7edcd4196462d23bc5e52e68 Removal of structure Context and its replacement by a theorem list of congruence rules for use in CONTEXT_REWRITE_RULE (where definitions are processed) diff -r 5ff4bfab859c -r 112cbb8301dc TFL/post.sml --- a/TFL/post.sml Mon Jun 23 11:30:35 1997 +0200 +++ b/TFL/post.sml Mon Jun 23 11:33:59 1997 +0200 @@ -23,7 +23,8 @@ val define : theory -> string -> string -> string list -> theory * Prim.pattern list - val simplify_defn : simpset -> theory * (string * Prim.pattern list) + val simplify_defn : simpset * thm list + -> theory * (string * Prim.pattern list) -> {rules:thm list, induct:thm, tcs:term list} (*------------------------------------------------------------------------- @@ -31,8 +32,6 @@ val lazyR_def: theory -> term -> {theory:theory, eqns : thm} *-------------------------------------------------------------------------*) - val tflcongs : theory -> thm list - end; @@ -77,7 +76,6 @@ (!claset addSDs [not0_implies_Suc] addss ss) 1), simplifier = Rules.simpl_conv ss []}; -fun tflcongs thy = Prim.Context.read() @ (#case_congs(Thry.extract_info thy)); val concl = #2 o Rules.dest_thm; @@ -185,14 +183,25 @@ val wf_rel_defs = [lex_prod_def, measure_def, inv_image_def]; -fun simplify_defn ss (thy,(id,pats)) = +(*Convert conclusion from = to ==*) +val eq_reflect_list = map (fn th => (th RS eq_reflection) handle _ => th); + +(*--------------------------------------------------------------------------- + * Install the basic context notions. Others (for nat and list and prod) + * have already been added in thry.sml + *---------------------------------------------------------------------------*) +val defaultTflCongs = eq_reflect_list [Thms.LET_CONG, if_cong]; + +fun simplify_defn (ss, tflCongs) (thy,(id,pats)) = let val dummy = deny (id mem map ! (stamps_of_thy thy)) ("Recursive definition " ^ id ^ " would clash with the theory of the same name!") val def = freezeT(get_def thy id) RS meta_eq_to_obj_eq val ss' = ss addsimps ((less_Suc_eq RS iffD2) :: wf_rel_defs) val {theory,rules,TCs,full_pats_TCs,patterns} = - Prim.post_definition ss' (thy,(def,pats)) + Prim.post_definition + (ss', defaultTflCongs @ eq_reflect_list tflCongs) + (thy, (def,pats)) val {lhs=f,rhs} = S.dest_eq(concl def) val (_,[R,_]) = S.strip_comb rhs val {induction, rules, tcs} = @@ -243,14 +252,4 @@ * * *---------------------------------------------------------------------------*) - - - - -(*--------------------------------------------------------------------------- - * Install the basic context notions. Others (for nat and list and prod) - * have already been added in thry.sml - *---------------------------------------------------------------------------*) -val () = Prim.Context.write[Thms.LET_CONG, Thms.COND_CONG]; - end; diff -r 5ff4bfab859c -r 112cbb8301dc TFL/tfl.sig --- a/TFL/tfl.sig Mon Jun 23 11:30:35 1997 +0200 +++ b/TFL/tfl.sig Mon Jun 23 11:33:59 1997 +0200 @@ -17,7 +17,7 @@ val wfrec_definition0 : theory -> string -> term -> term -> theory - val post_definition : simpset -> theory * (thm * pattern list) + val post_definition : simpset * thm list -> theory * (thm * pattern list) -> {theory : theory, rules : thm, TCs : term list list, @@ -25,7 +25,7 @@ patterns : pattern list} (*CURRENTLY UNUSED - val wfrec_eqns : theory -> term list + val wfrec_eqns : simpset * thm list -> theory -> term list -> {WFR : term, proto_def : term, extracta :(thm * term list) list, @@ -46,10 +46,4 @@ -> theory -> {rules:thm, induction:thm, TCs:term list list} -> {rules:thm, induction:thm, nested_tcs:thm list} - - structure Context - : sig - val read : unit -> thm list - val write : thm list -> unit - end end; diff -r 5ff4bfab859c -r 112cbb8301dc TFL/tfl.sml --- a/TFL/tfl.sml Mon Jun 23 11:30:35 1997 +0200 +++ b/TFL/tfl.sml Mon Jun 23 11:33:59 1997 +0200 @@ -355,16 +355,9 @@ * This structure keeps track of congruence rules that aren't derived * from a datatype definition. *---------------------------------------------------------------------------*) -structure Context = -struct - val non_datatype_context = ref []: thm list ref - fun read() = !non_datatype_context - fun write L = (non_datatype_context := L) -end; - fun extraction_thms thy = let val {case_rewrites,case_congs} = Thry.extract_info thy - in (case_rewrites, case_congs@Context.read()) + in (case_rewrites, case_congs) end; @@ -393,7 +386,7 @@ | givens (GIVEN(tm,_)::pats) = tm :: givens pats | givens (OMITTED _::pats) = givens pats; -fun post_definition ss (theory, (def, pats)) = +fun post_definition (ss, tflCongs) (theory, (def, pats)) = let val tych = Thry.typecheck theory val f = #lhs(S.dest_eq(concl def)) val corollary = R.MATCH_MP Thms.WFREC_COROLLARY def @@ -408,7 +401,7 @@ val extract = R.CONTEXT_REWRITE_RULE (ss, f, R, R.ISPECL (map tych [f,R]) Thms.CUT_LEMMA, - context_congs) + tflCongs@context_congs) val (rules, TCs) = ListPair.unzip (map extract corollaries') val rules0 = map (rewrite_rule [Thms.CUT_DEF]) rules val mk_cond_rule = R.FILTER_DISCH_ALL(not o curry (op aconv) WFR) @@ -427,7 +420,7 @@ * extraction commute for the non-nested case. For hol90 users, this * function can be invoked without being in draft mode. * CURRENTLY UNUSED -fun wfrec_eqns ss thy eqns = +fun wfrec_eqns (ss, tflCongs) thy eqns = let val {functional,pats} = mk_functional thy eqns val given_pats = givens pats val {Bvar = f, Body} = S.dest_abs functional @@ -448,7 +441,7 @@ val extract = R.CONTEXT_REWRITE_RULE (ss, f, R1, R.ISPECL (map tych [f,R1]) Thms.CUT_LEMMA, - context_congs) + tflCongs@context_congs) in {proto_def=proto_def, WFR=WFR, pats=pats,