- Tuned handling of oracles
- Put arguments of axms_of_proof and thms_of_proof into "canonical order"

--- a/src/Pure/proofterm.ML	Wed Aug 03 14:49:04 2005 +0200
+++ b/src/Pure/proofterm.ML	Wed Aug 03 16:24:52 2005 +0200
@@ -21,7 +21,7 @@
    | PThm of (string * (string * string list) list) * proof * term * typ list option
    | PAxm of string * term * typ list option
    | Oracle of string * term * typ list option
-   | MinProof of proof list;
+   | MinProof of ((string * term) * proof) list * (string * term) list * (string * term) list;
 
   val %> : proof * term -> proof
 end;
@@ -60,11 +60,13 @@
   val prf_subst_bounds : term list -> proof -> proof
   val prf_subst_pbounds : proof list -> proof -> proof
   val freeze_thaw_prf : proof -> proof * (proof -> proof)
+  val proof_of_min_axm : string * term -> proof
+  val proof_of_min_thm : (string * term) * proof -> proof
 
-  val thms_of_proof : (term * proof) list Symtab.table -> proof ->
+  val thms_of_proof : proof -> (term * proof) list Symtab.table ->
     (term * proof) list Symtab.table
-  val axms_of_proof : proof Symtab.table -> proof -> proof Symtab.table
-  val oracles_of_proof : proof list -> proof -> proof list
+  val axms_of_proof : proof -> proof Symtab.table -> proof Symtab.table
+  val oracles_of_proof : (string * term) list -> proof -> (string * term) list
 
   (** proof terms for specific inference rules **)
   val implies_intr_proof : term -> proof -> proof
@@ -127,57 +129,72 @@
  | PThm of (string * (string * string list) list) * proof * term * typ list option
  | PAxm of string * term * typ list option
  | Oracle of string * term * typ list option
- | MinProof of proof list;
+ | MinProof of ((string * term) * proof) list * (string * term) list * (string * term) list;
 
-fun oracles_of_proof prfs prf =
+fun proof_of_min_axm (s, prop) = PAxm (s, prop, NONE);
+fun proof_of_min_thm ((s, prop), prf) = PThm ((s, []), prf, prop, NONE);
+
+val string_term_ord = prod_ord fast_string_ord Term.fast_term_ord;
+
+fun oracles_of_proof oras prf =
   let
-    fun oras_of (tabs, Abst (_, _, prf)) = oras_of (tabs, prf)
-      | oras_of (tabs, AbsP (_, _, prf)) = oras_of (tabs, prf)
-      | oras_of (tabs, prf % _) = oras_of (tabs, prf)
-      | oras_of (tabs, prf1 %% prf2) = oras_of (oras_of (tabs, prf1), prf2)
-      | oras_of (tabs as (thms, oras), PThm ((name, _), prf, prop, _)) =
-          (case Symtab.lookup (thms, name) of
-             NONE => oras_of ((Symtab.update ((name, [prop]), thms), oras), prf)
-           | SOME ps => if prop mem ps then tabs else
-               oras_of ((Symtab.update ((name, prop::ps), thms), oras), prf))
-      | oras_of ((thms, oras), prf as Oracle _) = (thms, prf ins oras)
-      | oras_of (tabs, MinProof prfs) = Library.foldl oras_of (tabs, prfs)
-      | oras_of (tabs, _) = tabs
+    fun oras_of (Abst (_, _, prf)) = oras_of prf
+      | oras_of (AbsP (_, _, prf)) = oras_of prf
+      | oras_of (prf % _) = oras_of prf
+      | oras_of (prf1 %% prf2) = oras_of prf1 #> oras_of prf2
+      | oras_of (PThm ((name, _), prf, prop, _)) = (fn tabs as (thms, oras) =>
+          case Symtab.lookup (thms, name) of
+            NONE => oras_of prf (Symtab.update ((name, [prop]), thms), oras)
+          | SOME ps => if prop mem ps then tabs else
+              oras_of prf (Symtab.update ((name, prop::ps), thms), oras))
+      | oras_of (Oracle (s, prop, _)) =
+          apsnd (OrdList.insert string_term_ord (s, prop))
+      | oras_of (MinProof (thms, _, oras)) =
+          apsnd (OrdList.union string_term_ord oras) #>
+          fold (oras_of o proof_of_min_thm) thms
+      | oras_of _ = I
   in
-    snd (oras_of ((Symtab.empty, prfs), prf))
+    snd (oras_of prf (Symtab.empty, oras))
   end;
 
-fun thms_of_proof tab (Abst (_, _, prf)) = thms_of_proof tab prf
-  | thms_of_proof tab (AbsP (_, _, prf)) = thms_of_proof tab prf
-  | thms_of_proof tab (prf1 %% prf2) = thms_of_proof (thms_of_proof tab prf1) prf2
-  | thms_of_proof tab (prf % _) = thms_of_proof tab prf
-  | thms_of_proof tab (prf' as PThm ((s, _), prf, prop, _)) =
-      (case Symtab.lookup (tab, s) of
-         NONE => thms_of_proof (Symtab.update ((s, [(prop, prf')]), tab)) prf
-       | SOME ps => if exists (equal prop o fst) ps then tab else
-           thms_of_proof (Symtab.update ((s, (prop, prf')::ps), tab)) prf)
-  | thms_of_proof tab (MinProof prfs) = Library.foldl (uncurry thms_of_proof) (tab, prfs)
-  | thms_of_proof tab _ = tab;
+fun thms_of_proof (Abst (_, _, prf)) = thms_of_proof prf
+  | thms_of_proof (AbsP (_, _, prf)) = thms_of_proof prf
+  | thms_of_proof (prf1 %% prf2) = thms_of_proof prf1 #> thms_of_proof prf2
+  | thms_of_proof (prf % _) = thms_of_proof prf
+  | thms_of_proof (prf' as PThm ((s, _), prf, prop, _)) = (fn tab =>
+      case Symtab.lookup (tab, s) of
+        NONE => thms_of_proof prf (Symtab.update ((s, [(prop, prf')]), tab))
+      | SOME ps => if exists (equal prop o fst) ps then tab else
+          thms_of_proof prf (Symtab.update ((s, (prop, prf')::ps), tab)))
+  | thms_of_proof (MinProof (prfs, _, _)) = fold (thms_of_proof o proof_of_min_thm) prfs
+  | thms_of_proof _ = I;
 
-fun axms_of_proof tab (Abst (_, _, prf)) = axms_of_proof tab prf
-  | axms_of_proof tab (AbsP (_, _, prf)) = axms_of_proof tab prf
-  | axms_of_proof tab (prf1 %% prf2) = axms_of_proof (axms_of_proof tab prf1) prf2
-  | axms_of_proof tab (prf % _) = axms_of_proof tab prf
-  | axms_of_proof tab (prf as PAxm (s, _, _)) = Symtab.update ((s, prf), tab)
-  | axms_of_proof tab (MinProof prfs) = Library.foldl (uncurry axms_of_proof) (tab, prfs)
-  | axms_of_proof tab _ = tab;
+fun axms_of_proof (Abst (_, _, prf)) = axms_of_proof prf
+  | axms_of_proof (AbsP (_, _, prf)) = axms_of_proof prf
+  | axms_of_proof (prf1 %% prf2) = axms_of_proof prf1 #> axms_of_proof prf2
+  | axms_of_proof (prf % _) = axms_of_proof prf
+  | axms_of_proof (prf as PAxm (s, _, _)) = curry Symtab.update (s, prf)
+  | axms_of_proof (MinProof (_, prfs, _)) = fold (axms_of_proof o proof_of_min_axm) prfs
+  | axms_of_proof _ = I;
 
 (** collect all theorems, axioms and oracles **)
 
-fun mk_min_proof (prfs, Abst (_, _, prf)) = mk_min_proof (prfs, prf)
-  | mk_min_proof (prfs, AbsP (_, _, prf)) = mk_min_proof (prfs, prf)
-  | mk_min_proof (prfs, prf % _) = mk_min_proof (prfs, prf)
-  | mk_min_proof (prfs, prf1 %% prf2) = mk_min_proof (mk_min_proof (prfs, prf1), prf2)
-  | mk_min_proof (prfs, prf as PThm _) = prf ins prfs
-  | mk_min_proof (prfs, prf as PAxm _) = prf ins prfs
-  | mk_min_proof (prfs, prf as Oracle _) = prf ins prfs
-  | mk_min_proof (prfs, MinProof prfs') = prfs union prfs'
-  | mk_min_proof (prfs, _) = prfs;
+fun map3 f g h (thms, axms, oras) = (f thms, g axms, h oras);
+
+fun mk_min_proof (Abst (_, _, prf)) = mk_min_proof prf
+  | mk_min_proof (AbsP (_, _, prf)) = mk_min_proof prf
+  | mk_min_proof (prf % _) = mk_min_proof prf
+  | mk_min_proof (prf1 %% prf2) = mk_min_proof prf1 #> mk_min_proof prf2
+  | mk_min_proof (PThm ((s, _), prf, prop, _)) =
+      map3 (OrdList.insert (string_term_ord o pairself fst) ((s, prop), prf)) I I
+  | mk_min_proof (PAxm (s, prop, _)) =
+      map3 I (OrdList.insert string_term_ord (s, prop)) I
+  | mk_min_proof (Oracle (s, prop, _)) =
+      map3 I I (OrdList.insert string_term_ord (s, prop))
+  | mk_min_proof (MinProof (thms, axms, oras)) =
+      map3 (OrdList.union (string_term_ord o pairself fst) thms)
+        (OrdList.union string_term_ord axms) (OrdList.union string_term_ord oras)
+  | mk_min_proof _ = I;
 
 (** proof objects with different levels of detail **)
 
@@ -192,11 +209,11 @@
   (ora1 orelse ora2, 
    case !proofs of
      2 => f prf1 prf2
-   | 1 => MinProof (mk_min_proof (mk_min_proof ([], prf1), prf2))
-   | 0 => MinProof (if_ora ora2 (if_ora ora1 [] prf1) prf2)
+   | 1 => MinProof (([], [], []) |> mk_min_proof prf1 |> mk_min_proof prf2)
+   | 0 => MinProof ([], [], if_ora ora2 (if_ora ora1 [] prf1) prf2)
    | i => err_illegal_level i);
 
-fun infer_derivs' f = infer_derivs (K f) (false, MinProof []);
+fun infer_derivs' f = infer_derivs (K f) (false, MinProof ([], [], []));
 
 fun (prf %> t) = prf % SOME t;
 
@@ -830,7 +847,12 @@
   end;
 
 val axm_proof = gen_axm_proof PAxm;
-val oracle_proof = gen_axm_proof Oracle;
+
+val dummy = Const (Term.dummy_patternN, dummyT);
+
+fun oracle_proof name prop =
+  if !proofs = 0 then Oracle (name, dummy, NONE)
+  else gen_axm_proof Oracle name prop;
 
 fun shrink ls lev (prf as Abst (a, T, body)) =
       let val (b, is, ch, body') = shrink ls (lev+1) body
@@ -1127,7 +1149,7 @@
     val opt_prf = if ! proofs = 2 then
         #4 (shrink [] 0 (rewrite_prf fst (ProofData.get thy)
           (foldr (uncurry implies_intr_proof) prf hyps)))
-      else MinProof (mk_min_proof ([], prf));
+      else MinProof (mk_min_proof prf ([], [], []));
     val head = (case strip_combt (fst (strip_combP prf)) of
         (PThm ((old_name, _), prf', prop', NONE), args') =>
           if (old_name="" orelse old_name=name) andalso