added Proofterm.get_name variants according to krauss/schropp;
authorwenzelm
Thu May 13 17:25:53 2010 +0200 (2010-05-13 ago)
changeset 368777699f7fafde7
parent 36876 1abc27d6c362
child 36878 5caff17a28cd
added Proofterm.get_name variants according to krauss/schropp;
tuned signature;
src/Pure/proofterm.ML
     1.1 --- a/src/Pure/proofterm.ML	Wed May 12 22:43:05 2010 +0200
     1.2 +++ b/src/Pure/proofterm.ML	Thu May 13 17:25:53 2010 +0200
     1.3 @@ -118,11 +118,6 @@
     1.4      arity_proof: theory -> string * sort list * class -> proof} -> unit
     1.5    val axm_proof: string -> term -> proof
     1.6    val oracle_proof: string -> term -> oracle * proof
     1.7 -  val promise_proof: theory -> serial -> term -> proof
     1.8 -  val fulfill_norm_proof: theory -> (serial * proof_body) list -> proof_body -> proof_body
     1.9 -  val thm_proof: theory -> string -> term list -> term ->
    1.10 -    (serial * proof_body future) list -> proof_body -> pthm * proof
    1.11 -  val get_name: term list -> term -> proof -> string
    1.12  
    1.13    (** rewriting on proof terms **)
    1.14    val add_prf_rrule: proof * proof -> theory -> theory
    1.15 @@ -134,6 +129,14 @@
    1.16    val rewrite_proof_notypes: (proof * proof) list *
    1.17      (typ list -> proof -> (proof * proof) option) list -> proof -> proof
    1.18    val rew_proof: theory -> proof -> proof
    1.19 +
    1.20 +  val promise_proof: theory -> serial -> term -> proof
    1.21 +  val fulfill_norm_proof: theory -> (serial * proof_body) list -> proof_body -> proof_body
    1.22 +  val thm_proof: theory -> string -> term list -> term ->
    1.23 +    (serial * proof_body future) list -> proof_body -> pthm * proof
    1.24 +  val get_name: term list -> term -> proof -> string
    1.25 +  val get_name_unconstrained: sort list -> term list -> term -> proof -> string
    1.26 +  val guess_name: proof -> string
    1.27  end
    1.28  
    1.29  structure Proofterm : PROOFTERM =
    1.30 @@ -1413,6 +1416,20 @@
    1.31      | _ => "")
    1.32    end;
    1.33  
    1.34 +fun get_name_unconstrained shyps hyps prop prf =
    1.35 +  let val (_, prop) = Logic.unconstrainT shyps (Logic.list_implies (hyps, prop)) in
    1.36 +    (case strip_combt (fst (strip_combP prf)) of
    1.37 +      (PThm (_, ((name, prop', _), _)), _) => if prop = prop' then name else ""
    1.38 +    | _ => "")
    1.39 +  end;
    1.40 +
    1.41 +fun guess_name (PThm (_, ((name, _, _), _))) = name
    1.42 +  | guess_name (prf %% Hyp _) = guess_name prf
    1.43 +  | guess_name (prf %% OfClass _) = guess_name prf
    1.44 +  | guess_name (prf % NONE) = guess_name prf
    1.45 +  | guess_name (prf % SOME (Var _)) = guess_name prf
    1.46 +  | guess_name _ = "";
    1.47 +
    1.48  end;
    1.49  
    1.50  structure Basic_Proofterm : BASIC_PROOFTERM = Proofterm;