1.1 --- a/src/Pure/proofterm.ML	Mon Sep 22 15:26:11 2008 +0200
     1.2 +++ b/src/Pure/proofterm.ML	Mon Sep 22 15:26:13 2008 +0200
     1.3 @@ -21,6 +21,7 @@
     1.4     | PThm of string * proof * term * typ list option
     1.5     | PAxm of string * term * typ list option
     1.6     | Oracle of string * term * typ list option
     1.7 +   | Promise of serial * term * typ list option
     1.8     | MinProof of ((string * term) * proof) list * (string * term) list * (string * term) list;
     1.9  
    1.10    val %> : proof * term -> proof
    1.11 @@ -30,10 +31,8 @@
    1.12  sig
    1.13    include BASIC_PROOFTERM
    1.14  
    1.15 -  val infer_derivs : (proof -> proof -> proof) -> bool * proof -> bool * proof -> bool * proof
    1.16 -  val infer_derivs' : (proof -> proof) -> (bool * proof -> bool * proof)
    1.17 -
    1.18    (** primitive operations **)
    1.19 +  val min_proof : proof
    1.20    val proof_combt : proof * term list -> proof
    1.21    val proof_combt' : proof * term option list -> proof
    1.22    val proof_combP : proof * proof list -> proof
    1.23 @@ -66,7 +65,10 @@
    1.24    val thms_of_proof' : proof -> (term * proof) list Symtab.table ->
    1.25      (term * proof) list Symtab.table
    1.26    val axms_of_proof : proof -> proof Symtab.table -> proof Symtab.table
    1.27 -  val oracles_of_proof : (string * term) list -> proof -> (string * term) list
    1.28 +  val mk_min_proof : proof ->
    1.29 +   ((string * term) * proof) list * (string * term) list * (string * term) list ->
    1.30 +   ((string * term) * proof) list * (string * term) list * (string * term) list
    1.31 +  val oracles_of_proof : proof -> (string * term) list -> (string * term) list
    1.32  
    1.33    (** proof terms for specific inference rules **)
    1.34    val implies_intr_proof : term -> proof -> proof
    1.35 @@ -99,8 +101,10 @@
    1.36    val equal_elim : term -> term -> proof -> proof -> proof
    1.37    val axm_proof : string -> term -> proof
    1.38    val oracle_proof : string -> term -> proof
    1.39 +  val promise_proof : serial -> term -> proof
    1.40    val thm_proof : theory -> string -> term list -> term -> proof -> proof
    1.41    val get_name : term list -> term -> proof -> string
    1.42 +  val is_named : proof -> bool
    1.43  
    1.44    (** rewriting on proof terms **)
    1.45    val add_prf_rrule : proof * proof -> theory -> theory
    1.46 @@ -128,6 +132,7 @@
    1.47   | PThm of string * proof * term * typ list option
    1.48   | PAxm of string * term * typ list option
    1.49   | Oracle of string * term * typ list option
    1.50 + | Promise of serial * term * typ list option
    1.51   | MinProof of ((string * term) * proof) list * (string * term) list * (string * term) list;
    1.52  
    1.53  fun proof_of_min_axm (s, prop) = PAxm (s, prop, NONE);
    1.54 @@ -135,7 +140,7 @@
    1.55  
    1.56  val string_term_ord = prod_ord fast_string_ord Term.fast_term_ord;
    1.57  
    1.58 -fun oracles_of_proof oras prf =
    1.59 +fun oracles_of_proof prf oras =
    1.60    let
    1.61      fun oras_of (Abst (_, _, prf)) = oras_of prf
    1.62        | oras_of (AbsP (_, _, prf)) = oras_of prf
    1.63 @@ -213,24 +218,8 @@
    1.64  
    1.65  val proofs = ref 2;
    1.66  
    1.67 -fun err_illegal_level i =
    1.68 -  error ("Illegal level of detail for proof objects: " ^ string_of_int i);
    1.69 -
    1.70 -fun if_ora b = if b then oracles_of_proof else K;
    1.71  val min_proof = MinProof ([], [], []);
    1.72  
    1.73 -fun infer_derivs f (ora1, prf1) (ora2, prf2) =
    1.74 -  let val ora = ora1 orelse ora2 in
    1.75 -    (ora,
    1.76 -      case !proofs of
    1.77 -        2 => f prf1 prf2
    1.78 -      | 1 => MinProof (([], [], []) |> mk_min_proof prf1 |> mk_min_proof prf2)
    1.79 -      | 0 => if ora then MinProof ([], [], if_ora ora2 (if_ora ora1 [] prf1) prf2) else min_proof
    1.80 -      | i => err_illegal_level i)
    1.81 -  end;
    1.82 -
    1.83 -fun infer_derivs' f = infer_derivs (K f) (false, min_proof);
    1.84 -
    1.85  fun (prf %> t) = prf % SOME t;
    1.86  
    1.87  val proof_combt = Library.foldl (op %>);
    1.88 @@ -317,6 +306,7 @@
    1.89  fun change_type opTs (PThm (name, prf, prop, _)) = PThm (name, prf, prop, opTs)
    1.90    | change_type opTs (PAxm (name, prop, _)) = PAxm (name, prop, opTs)
    1.91    | change_type opTs (Oracle (name, prop, _)) = Oracle (name, prop, opTs)
    1.92 +  | change_type opTs (Promise (i, prop, _)) = Promise (i, prop, opTs)
    1.93    | change_type _ prf = prf;
    1.94  
    1.95  
    1.96 @@ -911,6 +901,8 @@
    1.97    if !proofs = 0 then Oracle (name, dummy, NONE)
    1.98    else gen_axm_proof Oracle name prop;
    1.99  
   1.100 +fun promise_proof i prop = gen_axm_proof Promise i prop;
   1.101 +
   1.102  fun shrink_proof thy =
   1.103    let
   1.104      fun shrink ls lev (prf as Abst (a, T, body)) =
   1.105 @@ -946,7 +938,8 @@
   1.106        | shrink' ls lev ts prfs prf =
   1.107            let
   1.108              val prop = (case prf of PThm (_, _, prop, _) => prop | PAxm (_, prop, _) => prop
   1.109 -              | Oracle (_, prop, _) => prop | _ => error "shrink: proof not in normal form");
   1.110 +              | Oracle (_, prop, _) => prop | Promise (_, prop, _) => prop
   1.111 +              | _ => error "shrink: proof not in normal form");
   1.112              val vs = vars_of prop;
   1.113              val (ts', ts'') = chop (length vs) ts;
   1.114              val insts = Library.take (length ts', map (fst o dest_Var) vs) ~~ ts';
   1.115 @@ -1224,6 +1217,10 @@
   1.116      | _ => "")
   1.117    end;
   1.118  
   1.119 +fun is_named (PThm (name, _, _, _)) = name <> ""
   1.120 +  | is_named (PAxm (name, _, _)) = name <> ""
   1.121 +  | is_named _ = false;
   1.122 +
   1.123  end;
   1.124  
   1.125  structure BasicProofterm : BASIC_PROOFTERM = Proofterm;