Removal of structure Context and its replacement by a theorem list of
authorpaulson
Mon Jun 23 11:33:59 1997 +0200 (1997-06-23)
changeset 3459112cbb8301dc
parent 3458 5ff4bfab859c
child 3460 5d71eed16fbe
Removal of structure Context and its replacement by a theorem list of
congruence rules for use in CONTEXT_REWRITE_RULE (where definitions are
processed)
TFL/post.sml
TFL/tfl.sig
TFL/tfl.sml
     1.1 --- a/TFL/post.sml	Mon Jun 23 11:30:35 1997 +0200
     1.2 +++ b/TFL/post.sml	Mon Jun 23 11:33:59 1997 +0200
     1.3 @@ -23,7 +23,8 @@
     1.4     val define   : theory -> string -> string -> string list 
     1.5                    -> theory * Prim.pattern list
     1.6  
     1.7 -   val simplify_defn : simpset -> theory * (string * Prim.pattern list)
     1.8 +   val simplify_defn : simpset * thm list 
     1.9 +                        -> theory * (string * Prim.pattern list)
    1.10                          -> {rules:thm list, induct:thm, tcs:term list}
    1.11  
    1.12    (*-------------------------------------------------------------------------
    1.13 @@ -31,8 +32,6 @@
    1.14         val lazyR_def: theory -> term -> {theory:theory, eqns : thm}
    1.15     *-------------------------------------------------------------------------*)
    1.16  
    1.17 -   val tflcongs : theory -> thm list
    1.18 -
    1.19    end;
    1.20  
    1.21  
    1.22 @@ -77,7 +76,6 @@
    1.23  			  (!claset addSDs [not0_implies_Suc] addss ss) 1),
    1.24      simplifier = Rules.simpl_conv ss []};
    1.25  
    1.26 -fun tflcongs thy = Prim.Context.read() @ (#case_congs(Thry.extract_info thy));
    1.27  
    1.28  
    1.29  val concl = #2 o Rules.dest_thm;
    1.30 @@ -185,14 +183,25 @@
    1.31  
    1.32  val wf_rel_defs = [lex_prod_def, measure_def, inv_image_def];
    1.33  
    1.34 -fun simplify_defn ss (thy,(id,pats)) =
    1.35 +(*Convert conclusion from = to ==*)
    1.36 +val eq_reflect_list = map (fn th => (th RS eq_reflection) handle _ => th);
    1.37 +
    1.38 +(*---------------------------------------------------------------------------
    1.39 + * Install the basic context notions. Others (for nat and list and prod) 
    1.40 + * have already been added in thry.sml
    1.41 + *---------------------------------------------------------------------------*)
    1.42 +val defaultTflCongs = eq_reflect_list [Thms.LET_CONG, if_cong];
    1.43 +
    1.44 +fun simplify_defn (ss, tflCongs) (thy,(id,pats)) =
    1.45     let val dummy = deny (id  mem  map ! (stamps_of_thy thy))
    1.46                          ("Recursive definition " ^ id ^ 
    1.47                           " would clash with the theory of the same name!")
    1.48         val def =  freezeT(get_def thy id)   RS   meta_eq_to_obj_eq
    1.49         val ss' = ss addsimps ((less_Suc_eq RS iffD2) :: wf_rel_defs)
    1.50         val {theory,rules,TCs,full_pats_TCs,patterns} = 
    1.51 -                Prim.post_definition ss' (thy,(def,pats))
    1.52 +                Prim.post_definition
    1.53 +		   (ss', defaultTflCongs @ eq_reflect_list tflCongs)
    1.54 +		   (thy, (def,pats))
    1.55         val {lhs=f,rhs} = S.dest_eq(concl def)
    1.56         val (_,[R,_]) = S.strip_comb rhs
    1.57         val {induction, rules, tcs} = 
    1.58 @@ -243,14 +252,4 @@
    1.59   *
    1.60   *
    1.61   *---------------------------------------------------------------------------*)
    1.62 -
    1.63 -
    1.64 -
    1.65 -
    1.66 -(*---------------------------------------------------------------------------
    1.67 - * Install the basic context notions. Others (for nat and list and prod) 
    1.68 - * have already been added in thry.sml
    1.69 - *---------------------------------------------------------------------------*)
    1.70 -val () = Prim.Context.write[Thms.LET_CONG, Thms.COND_CONG];
    1.71 -
    1.72  end;
     2.1 --- a/TFL/tfl.sig	Mon Jun 23 11:30:35 1997 +0200
     2.2 +++ b/TFL/tfl.sig	Mon Jun 23 11:33:59 1997 +0200
     2.3 @@ -17,7 +17,7 @@
     2.4  
     2.5     val wfrec_definition0 : theory -> string -> term -> term -> theory
     2.6  
     2.7 -   val post_definition : simpset -> theory * (thm * pattern list)
     2.8 +   val post_definition : simpset * thm list -> theory * (thm * pattern list)
     2.9  				 -> {theory : theory,
    2.10  				     rules  : thm, 
    2.11  				       TCs  : term list list,
    2.12 @@ -25,7 +25,7 @@
    2.13  				  patterns  : pattern list}
    2.14  
    2.15  (*CURRENTLY UNUSED
    2.16 -   val wfrec_eqns : theory -> term list
    2.17 +   val wfrec_eqns : simpset * thm list -> theory -> term list
    2.18                       -> {WFR : term, 
    2.19                           proto_def : term,
    2.20                           extracta :(thm * term list) list,
    2.21 @@ -46,10 +46,4 @@
    2.22                       -> theory 
    2.23                        -> {rules:thm, induction:thm, TCs:term list list}
    2.24                         -> {rules:thm, induction:thm, nested_tcs:thm list}
    2.25 -
    2.26 -   structure Context
    2.27 -     : sig
    2.28 -         val read : unit -> thm list
    2.29 -         val write : thm list -> unit
    2.30 -       end
    2.31  end;
     3.1 --- a/TFL/tfl.sml	Mon Jun 23 11:30:35 1997 +0200
     3.2 +++ b/TFL/tfl.sml	Mon Jun 23 11:33:59 1997 +0200
     3.3 @@ -355,16 +355,9 @@
     3.4   * This structure keeps track of congruence rules that aren't derived
     3.5   * from a datatype definition.
     3.6   *---------------------------------------------------------------------------*)
     3.7 -structure Context =
     3.8 -struct
     3.9 -  val non_datatype_context = ref []: thm list ref
    3.10 -  fun read() = !non_datatype_context
    3.11 -  fun write L = (non_datatype_context := L)
    3.12 -end;
    3.13 -
    3.14  fun extraction_thms thy = 
    3.15   let val {case_rewrites,case_congs} = Thry.extract_info thy
    3.16 - in (case_rewrites, case_congs@Context.read())
    3.17 + in (case_rewrites, case_congs)
    3.18   end;
    3.19  
    3.20  
    3.21 @@ -393,7 +386,7 @@
    3.22    | givens (GIVEN(tm,_)::pats) = tm :: givens pats
    3.23    | givens (OMITTED _::pats)   = givens pats;
    3.24  
    3.25 -fun post_definition ss (theory, (def, pats)) =
    3.26 +fun post_definition (ss, tflCongs) (theory, (def, pats)) =
    3.27   let val tych = Thry.typecheck theory 
    3.28       val f = #lhs(S.dest_eq(concl def))
    3.29       val corollary = R.MATCH_MP Thms.WFREC_COROLLARY def
    3.30 @@ -408,7 +401,7 @@
    3.31       val extract = R.CONTEXT_REWRITE_RULE 
    3.32  	             (ss, f, R,
    3.33  		      R.ISPECL (map tych [f,R]) Thms.CUT_LEMMA,
    3.34 -		      context_congs)
    3.35 +		      tflCongs@context_congs)
    3.36       val (rules, TCs) = ListPair.unzip (map extract corollaries')
    3.37       val rules0 = map (rewrite_rule [Thms.CUT_DEF]) rules
    3.38       val mk_cond_rule = R.FILTER_DISCH_ALL(not o curry (op aconv) WFR)
    3.39 @@ -427,7 +420,7 @@
    3.40   * extraction commute for the non-nested case. For hol90 users, this 
    3.41   * function can be invoked without being in draft mode.
    3.42   * CURRENTLY UNUSED
    3.43 -fun wfrec_eqns ss thy eqns =
    3.44 +fun wfrec_eqns (ss, tflCongs) thy eqns =
    3.45   let val {functional,pats} = mk_functional thy eqns
    3.46       val given_pats = givens pats
    3.47       val {Bvar = f, Body} = S.dest_abs functional
    3.48 @@ -448,7 +441,7 @@
    3.49       val extract = R.CONTEXT_REWRITE_RULE 
    3.50  	               (ss, f, R1, 
    3.51  		        R.ISPECL (map tych [f,R1]) Thms.CUT_LEMMA, 
    3.52 -			context_congs)
    3.53 +			tflCongs@context_congs)
    3.54   in {proto_def=proto_def, 
    3.55       WFR=WFR, 
    3.56       pats=pats,