added store/bind_thms;
authorwenzelm
Wed Sep 01 21:09:10 1999 +0200 (1999-09-01)
changeset 74107369a35fb3c2
parent 7409 f8ce7b832598
child 7411 4dbff71ac480
added store/bind_thms;
src/Pure/Thy/thm_database.ML
     1.1 --- a/src/Pure/Thy/thm_database.ML	Wed Sep 01 21:06:57 1999 +0200
     1.2 +++ b/src/Pure/Thy/thm_database.ML	Wed Sep 01 21:09:10 1999 +0200
     1.3 @@ -8,8 +8,9 @@
     1.4  signature BASIC_THM_DATABASE =
     1.5  sig
     1.6    val store_thm: string * thm -> thm
     1.7 -  val qed_thm: thm option ref
     1.8 +  val store_thms: string * thm list -> thm list
     1.9    val bind_thm: string * thm -> unit
    1.10 +  val bind_thms: string * thm list -> unit
    1.11    val qed: string -> unit
    1.12    val qed_goal: string -> theory -> string -> (thm list -> tactic list) -> unit
    1.13    val qed_goalw: string -> theory -> thm list -> string -> (thm list -> tactic list) -> unit
    1.14 @@ -23,7 +24,9 @@
    1.15  signature THM_DATABASE =
    1.16  sig
    1.17    include BASIC_THM_DATABASE
    1.18 +  val qed_thms: thm list ref
    1.19    val ml_store_thm: string * thm -> unit
    1.20 +  val ml_store_thms: string * thm list -> unit
    1.21    val is_ml_identifier: string -> bool
    1.22  end;
    1.23  
    1.24 @@ -35,13 +38,17 @@
    1.25  (* store in theory and generate HTML *)
    1.26  
    1.27  fun store_thm (name, thm) =
    1.28 -  let val thm' = PureThy.smart_store_thm (name, thm)
    1.29 +  let val thm' = hd (PureThy.smart_store_thms (name, [thm]))
    1.30    in Present.theorem name thm'; thm' end;
    1.31  
    1.32 +fun store_thms (name, thms) =
    1.33 +  let val thms' = PureThy.smart_store_thms (name, thms)
    1.34 +  in Present.theorems name thms'; thms' end;
    1.35 +
    1.36  
    1.37  (* store on ML toplevel *)
    1.38  
    1.39 -val qed_thm: thm option ref = ref None;
    1.40 +val qed_thms: thm list ref = ref [];
    1.41  
    1.42  val ml_reserved =
    1.43   ["abstype", "and", "andalso", "as", "case", "do", "datatype", "else",
    1.44 @@ -54,16 +61,25 @@
    1.45  fun is_ml_identifier name =
    1.46    Syntax.is_identifier name andalso not (name mem ml_reserved);
    1.47  
    1.48 +fun warn_ml name =
    1.49 +  if is_ml_identifier name then false
    1.50 +  else (warning ("Cannot bind theorem(s) " ^ quote name ^ " as ML value"); true);
    1.51 +
    1.52  fun ml_store_thm (name, thm) =
    1.53    let val thm' = store_thm (name, thm) in
    1.54 -    if is_ml_identifier name then
    1.55 -      (qed_thm := Some thm';
    1.56 -        use_text true ("val " ^ name ^ " = the (! ThmDatabase.qed_thm);"))
    1.57 -    else warning ("Cannot bind thm " ^ quote name ^ " as ML value")
    1.58 +    if warn_ml name then ()
    1.59 +    else (qed_thms := [thm]; use_text true ("val " ^ name ^ " = hd (! ThmDatabase.qed_thms);"))
    1.60 +  end;
    1.61 +
    1.62 +fun ml_store_thms (name, thms) =
    1.63 +  let val thms' = store_thms (name, thms) in
    1.64 +    if warn_ml name then ()
    1.65 +    else (qed_thms := thms; use_text true ("val " ^ name ^ " = ! ThmDatabase.qed_thms;"))
    1.66    end;
    1.67  
    1.68  fun bind_thm (name, thm) = ml_store_thm (name, standard thm);
    1.69 -fun qed name = ml_store_thm (name, result ());
    1.70 +fun bind_thms (name, thms) = ml_store_thms (name, map standard thms);
    1.71 +fun qed name = ml_store_thm (name, Goals.result ());
    1.72  fun qed_goal name thy goal tacsf = ml_store_thm (name, prove_goal thy goal tacsf);
    1.73  fun qed_goalw name thy rews goal tacsf = ml_store_thm (name, prove_goalw thy rews goal tacsf);
    1.74  
    1.75 @@ -140,7 +156,7 @@
    1.76              let val Some pat = extract prop
    1.77                  val (_,subst) = Pattern.match tsig (pat,obj)
    1.78              in foldl op+
    1.79 -		(0, map (fn (_,t) => size_of_term t) subst)
    1.80 +                (0, map (fn (_,t) => size_of_term t) subst)
    1.81              end
    1.82  
    1.83        fun thm_ord ((p0,s0,_),(p1,s1,_)) =
    1.84 @@ -152,12 +168,12 @@
    1.85                        if Sign.subsig(sign, signobj) andalso
    1.86                           matches(prop,#tsig(Sign.rep_sg signobj))
    1.87                        then
    1.88 -			(nprems_of thm,substsize(prop,#tsig(Sign.rep_sg signobj)),p)::sels
    1.89 +                        (nprems_of thm,substsize(prop,#tsig(Sign.rep_sg signobj)),p)::sels
    1.90                        else sels)
    1.91              end
    1.92          | select([],sels) = sels
    1.93  
    1.94 -  in map (fn (_,_,t) => t) (sort thm_ord (select(named_thms, []))) end; 
    1.95 +  in map (fn (_,_,t) => t) (sort thm_ord (select(named_thms, []))) end;
    1.96  
    1.97  fun find_matching(prop,sign,index,extract) =
    1.98    (case top_const prop of