src/Pure/thm.ML

   type thm
   type conv = cterm -> thm
   type attribute = Context.generic * thm -> Context.generic * thm
   val rep_thm: thm ->
    {thy_ref: theory_ref,
-    der: bool * Proofterm.proof,
+    der: Deriv.T,
     tags: Properties.T,
     maxidx: int,
     shyps: sort list,
     hyps: term list,
     tpairs: (term * term) list,
     prop: term}
   val crep_thm: thm ->
    {thy_ref: theory_ref,
-    der: bool * Proofterm.proof,
+    der: Deriv.T,
     tags: Properties.T,
     maxidx: int,
     shyps: sort list,
     hyps: cterm list,
     tpairs: (cterm * cterm) list,

 
 (*** Meta theorems ***)
 
 abstype thm = Thm of
  {thy_ref: theory_ref,         (*dynamic reference to theory*)
-  der: bool * Pt.proof,        (*derivation*)
+  der: Deriv.T,                (*derivation*)
   tags: Properties.T,          (*additional annotations/comments*)
   maxidx: int,                 (*maximum index of any Var or TVar*)
   shyps: sort list,            (*sort hypotheses as ordered list*)
   hyps: term list,             (*hypotheses as ordered list*)
   tpairs: (term * term) list,  (*flex-flex pairs*)

 fun theory_of_thm (Thm {thy_ref, ...}) = Theory.deref thy_ref;
 fun maxidx_of (Thm {maxidx, ...}) = maxidx;
 fun maxidx_thm th i = Int.max (maxidx_of th, i);
 fun hyps_of (Thm {hyps, ...}) = hyps;
 fun prop_of (Thm {prop, ...}) = prop;
-fun proof_of (Thm {der = (_, proof), ...}) = proof;
+fun proof_of (Thm {der, ...}) = Deriv.proof_of der;
 fun tpairs_of (Thm {tpairs, ...}) = tpairs;
 
 val concl_of = Logic.strip_imp_concl o prop_of;
 val prems_of = Logic.strip_imp_prems o prop_of;
 val nprems_of = Logic.count_prems o prop_of;

   let
     fun get_ax thy =
       Symtab.lookup (Theory.axiom_table thy) name
       |> Option.map (fn prop =>
            let
-             val der = Pt.infer_derivs' I (false, Pt.axm_proof name prop);
+             val der = Deriv.rule0 (Pt.axm_proof name prop);
              val maxidx = maxidx_of_term prop;
              val shyps = Sorts.insert_term prop [];
            in
              Thm {thy_ref = Theory.check_thy thy, der = der, tags = [],
                maxidx = maxidx, shyps = shyps, hyps = [], tpairs = [], prop = prop}

   map (fn s => (s, get_axiom_i thy s)) (Symtab.keys (Theory.axiom_table thy));
 
 
 (* official name and additional tags *)
 
-fun get_name (Thm {hyps, prop, der = (_, prf), ...}) =
-  Pt.get_name hyps prop prf;
-
-fun put_name name (Thm {thy_ref, der = (ora, prf), tags, maxidx, shyps, hyps, tpairs = [], prop}) =
+fun get_name (Thm {hyps, prop, der, ...}) =
+  Pt.get_name hyps prop (Deriv.proof_of der);
+
+fun put_name name (Thm {thy_ref, der, tags, maxidx, shyps, hyps, tpairs = [], prop}) =
       let
         val thy = Theory.deref thy_ref;
-        val der = (ora, Pt.thm_proof thy name hyps prop prf);
+        val der' = Deriv.uncond_rule (Pt.thm_proof thy name hyps prop) der;
       in
-        Thm {thy_ref = Theory.check_thy thy, der = der, tags = tags, maxidx = maxidx,
+        Thm {thy_ref = Theory.check_thy thy, der = der', tags = tags, maxidx = maxidx,
           shyps = shyps, hyps = hyps, tpairs = [], prop = prop}
       end
   | put_name _ thm = raise THM ("name_thm: unsolved flex-flex constraints", 0, [thm]);
 
 val get_tags = #tags o rep_thm;

 
 
 fun norm_proof (Thm {thy_ref, der, tags, maxidx, shyps, hyps, tpairs, prop}) =
   let
     val thy = Theory.deref thy_ref;
-    val der = Pt.infer_derivs' (Pt.rew_proof thy) der;
-  in
-    Thm {thy_ref = Theory.check_thy thy, der = der, tags = tags, maxidx = maxidx,
+    val der' = Deriv.rule1 (Pt.rew_proof thy) der;
+  in
+    Thm {thy_ref = Theory.check_thy thy, der = der', tags = tags, maxidx = maxidx,
       shyps = shyps, hyps = hyps, tpairs = tpairs, prop = prop}
   end;
 
 fun adjust_maxidx_thm i (th as Thm {thy_ref, der, tags, maxidx, shyps, hyps, tpairs, prop}) =
   if maxidx = i then th

     if T <> propT then
       raise THM ("assume: prop", 0, [])
     else if maxidx <> ~1 then
       raise THM ("assume: variables", maxidx, [])
     else Thm {thy_ref = thy_ref,
-      der = Pt.infer_derivs' I (false, Pt.Hyp prop),
+      der = Deriv.rule0 (Pt.Hyp prop),
       tags = [],
       maxidx = ~1,
       shyps = sorts,
       hyps = [prop],
       tpairs = [],

     (th as Thm {der, maxidx, hyps, shyps, tpairs, prop, ...}) =
   if T <> propT then
     raise THM ("implies_intr: assumptions must have type prop", 0, [th])
   else
     Thm {thy_ref = merge_thys1 ct th,
-      der = Pt.infer_derivs' (Pt.implies_intr_proof A) der,
+      der = Deriv.rule1 (Pt.implies_intr_proof A) der,
       tags = [],
       maxidx = Int.max (maxidxA, maxidx),
       shyps = Sorts.union sorts shyps,
       hyps = OrdList.remove Term.fast_term_ord A hyps,
       tpairs = tpairs,

   in
     case prop of
       Const ("==>", _) $ A $ B =>
         if A aconv propA then
           Thm {thy_ref = merge_thys2 thAB thA,
-            der = Pt.infer_derivs (curry Pt.%%) der derA,
+            der = Deriv.rule2 (curry Pt.%%) der derA,
             tags = [],
             maxidx = Int.max (maxA, maxidx),
             shyps = Sorts.union shypsA shyps,
             hyps = union_hyps hypsA hyps,
             tpairs = union_tpairs tpairsA tpairs,

     (ct as Cterm {t = x, T, sorts, ...})
     (th as Thm {der, maxidx, shyps, hyps, tpairs, prop, ...}) =
   let
     fun result a =
       Thm {thy_ref = merge_thys1 ct th,
-        der = Pt.infer_derivs' (Pt.forall_intr_proof x a) der,
+        der = Deriv.rule1 (Pt.forall_intr_proof x a) der,
         tags = [],
         maxidx = maxidx,
         shyps = Sorts.union sorts shyps,
         hyps = hyps,
         tpairs = tpairs,

     Const ("all", Type ("fun", [Type ("fun", [qary, _]), _])) $ A =>
       if T <> qary then
         raise THM ("forall_elim: type mismatch", 0, [th])
       else
         Thm {thy_ref = merge_thys1 ct th,
-          der = Pt.infer_derivs' (Pt.% o rpair (SOME t)) der,
+          der = Deriv.rule1 (Pt.% o rpair (SOME t)) der,
           tags = [],
           maxidx = Int.max (maxidx, maxt),
           shyps = Sorts.union sorts shyps,
           hyps = hyps,
           tpairs = tpairs,

 (*Reflexivity
   t == t
 *)
 fun reflexive (ct as Cterm {thy_ref, t, T, maxidx, sorts}) =
   Thm {thy_ref = thy_ref,
-    der = Pt.infer_derivs' I (false, Pt.reflexive),
+    der = Deriv.rule0 Pt.reflexive,
     tags = [],
     maxidx = maxidx,
     shyps = sorts,
     hyps = [],
     tpairs = [],

 *)
 fun symmetric (th as Thm {thy_ref, der, maxidx, shyps, hyps, tpairs, prop, ...}) =
   (case prop of
     (eq as Const ("==", Type (_, [T, _]))) $ t $ u =>
       Thm {thy_ref = thy_ref,
-        der = Pt.infer_derivs' Pt.symmetric der,
+        der = Deriv.rule1 Pt.symmetric der,
         tags = [],
         maxidx = maxidx,
         shyps = shyps,
         hyps = hyps,
         tpairs = tpairs,

     case (prop1, prop2) of
       ((eq as Const ("==", Type (_, [T, _]))) $ t1 $ u, Const ("==", _) $ u' $ t2) =>
         if not (u aconv u') then err "middle term"
         else
           Thm {thy_ref = merge_thys2 th1 th2,
-            der = Pt.infer_derivs (Pt.transitive u T) der1 der2,
+            der = Deriv.rule2 (Pt.transitive u T) der1 der2,
             tags = [],
             maxidx = Int.max (max1, max2),
             shyps = Sorts.union shyps1 shyps2,
             hyps = union_hyps hyps1 hyps2,
             tpairs = union_tpairs tpairs1 tpairs2,

     else
       (case t of Abs (_, _, bodt) $ u => subst_bound (u, bodt)
       | _ => raise THM ("beta_conversion: not a redex", 0, []));
   in
     Thm {thy_ref = thy_ref,
-      der = Pt.infer_derivs' I (false, Pt.reflexive),
+      der = Deriv.rule0 Pt.reflexive,
       tags = [],
       maxidx = maxidx,
       shyps = sorts,
       hyps = [],
       tpairs = [],
       prop = Logic.mk_equals (t, t')}
   end;
 
 fun eta_conversion (Cterm {thy_ref, t, T, maxidx, sorts}) =
   Thm {thy_ref = thy_ref,
-    der = Pt.infer_derivs' I (false, Pt.reflexive),
+    der = Deriv.rule0 Pt.reflexive,
     tags = [],
     maxidx = maxidx,
     shyps = sorts,
     hyps = [],
     tpairs = [],
     prop = Logic.mk_equals (t, Envir.eta_contract t)};
 
 fun eta_long_conversion (Cterm {thy_ref, t, T, maxidx, sorts}) =
   Thm {thy_ref = thy_ref,
-    der = Pt.infer_derivs' I (false, Pt.reflexive),
+    der = Deriv.rule0 Pt.reflexive,
     tags = [],
     maxidx = maxidx,
     shyps = sorts,
     hyps = [],
     tpairs = [],

   let
     val (t, u) = Logic.dest_equals prop
       handle TERM _ => raise THM ("abstract_rule: premise not an equality", 0, [th]);
     val result =
       Thm {thy_ref = thy_ref,
-        der = Pt.infer_derivs' (Pt.abstract_rule x a) der,
+        der = Deriv.rule1 (Pt.abstract_rule x a) der,
         tags = [],
         maxidx = maxidx,
         shyps = Sorts.union sorts shyps,
         hyps = hyps,
         tpairs = tpairs,

     case (prop1, prop2) of
       (Const ("==", Type ("fun", [fT, _])) $ f $ g,
        Const ("==", Type ("fun", [tT, _])) $ t $ u) =>
         (chktypes fT tT;
           Thm {thy_ref = merge_thys2 th1 th2,
-            der = Pt.infer_derivs (Pt.combination f g t u fT) der1 der2,
+            der = Deriv.rule2 (Pt.combination f g t u fT) der1 der2,
             tags = [],
             maxidx = Int.max (max1, max2),
             shyps = Sorts.union shyps1 shyps2,
             hyps = union_hyps hyps1 hyps2,
             tpairs = union_tpairs tpairs1 tpairs2,

   in
     case (prop1, prop2) of
       (Const("==>", _) $ A $ B, Const("==>", _) $ B' $ A') =>
         if A aconv A' andalso B aconv B' then
           Thm {thy_ref = merge_thys2 th1 th2,
-            der = Pt.infer_derivs (Pt.equal_intr A B) der1 der2,
+            der = Deriv.rule2 (Pt.equal_intr A B) der1 der2,
             tags = [],
             maxidx = Int.max (max1, max2),
             shyps = Sorts.union shyps1 shyps2,
             hyps = union_hyps hyps1 hyps2,
             tpairs = union_tpairs tpairs1 tpairs2,

   in
     case prop1 of
       Const ("==", _) $ A $ B =>
         if prop2 aconv A then
           Thm {thy_ref = merge_thys2 th1 th2,
-            der = Pt.infer_derivs (Pt.equal_elim A B) der1 der2,
+            der = Deriv.rule2 (Pt.equal_elim A B) der1 der2,
             tags = [],
             maxidx = Int.max (max1, max2),
             shyps = Sorts.union shyps1 shyps2,
             hyps = union_hyps hyps1 hyps2,
             tpairs = union_tpairs tpairs1 tpairs2,

         else
           let
             val tpairs' = tpairs |> map (pairself (Envir.norm_term env))
               (*remove trivial tpairs, of the form t==t*)
               |> filter_out (op aconv);
-            val der = Pt.infer_derivs' (Pt.norm_proof' env) der;
+            val der = Deriv.rule1 (Pt.norm_proof' env) der;
             val prop' = Envir.norm_term env prop;
             val maxidx = maxidx_tpairs tpairs' (maxidx_of_term prop');
             val shyps = Envir.insert_sorts env shyps;
           in
             Thm {thy_ref = Theory.check_thy thy, der = der, tags = [], maxidx = maxidx,

         val tpairs' = map (pairself gen) tpairs;
         val maxidx' = maxidx_tpairs tpairs' (maxidx_of_term prop');
       in
         Thm {
           thy_ref = thy_ref,
-          der = Pt.infer_derivs' (Pt.generalize (tfrees, frees) idx) der,
+          der = Deriv.rule1 (Pt.generalize (tfrees, frees) idx) der,
           tags = [],
           maxidx = maxidx',
           shyps = shyps,
           hyps = hyps,
           tpairs = tpairs',

         val (prop', maxidx1) = subst prop ~1;
         val (tpairs', maxidx') =
           fold_map (fn (t, u) => fn i => subst t i ||>> subst u) tpairs maxidx1;
       in
         Thm {thy_ref = thy_ref',
-          der = Pt.infer_derivs' (fn d =>
+          der = Deriv.rule1 (fn d =>
             Pt.instantiate (map (apsnd #1) instT', map (apsnd #1) inst') d) der,
           tags = [],
           maxidx = maxidx',
           shyps = shyps',
           hyps = hyps,

 fun trivial (Cterm {thy_ref, t =A, T, maxidx, sorts}) =
   if T <> propT then
     raise THM ("trivial: the term must have type prop", 0, [])
   else
     Thm {thy_ref = thy_ref,
-      der = Pt.infer_derivs' I (false, Pt.AbsP ("H", NONE, Pt.PBound 0)),
+      der = Deriv.rule0 (Pt.AbsP ("H", NONE, Pt.PBound 0)),
       tags = [],
       maxidx = maxidx,
       shyps = sorts,
       hyps = [],
       tpairs = [],

 fun class_triv thy c =
   let
     val Cterm {t, maxidx, sorts, ...} =
       cterm_of thy (Logic.mk_inclass (TVar ((Name.aT, 0), [c]), Sign.certify_class thy c))
         handle TERM (msg, _) => raise THM ("class_triv: " ^ msg, 0, []);
-    val der = Pt.infer_derivs' I (false, Pt.PAxm ("Pure.class_triv:" ^ c, t, SOME []));
+    val der = Deriv.rule0 (Pt.PAxm ("Pure.class_triv:" ^ c, t, SOME []));
   in
     Thm {thy_ref = Theory.check_thy thy, der = der, tags = [], maxidx = maxidx,
       shyps = sorts, hyps = [], tpairs = [], prop = t}
   end;
 

     val T' = TVar ((x, i), []);
     val unconstrain = Term.map_types (Term.map_atyps (fn U => if U = T then T' else U));
     val constraints = map (curry Logic.mk_inclass T') S;
   in
     Thm {thy_ref = Theory.merge_refs (thy_ref1, thy_ref2),
-      der = Pt.infer_derivs' I (false, Pt.PAxm ("Pure.unconstrainT", prop, SOME [])),
+      der = Deriv.rule0 (Pt.PAxm ("Pure.unconstrainT", prop, SOME [])),
       tags = [],
       maxidx = Int.max (maxidx, i),
       shyps = Sorts.remove_sort S shyps,
       hyps = hyps,
       tpairs = map (pairself unconstrain) tpairs,

     val prop1 = attach_tpairs tpairs prop;
     val (al, prop2) = Type.varify tfrees prop1;
     val (ts, prop3) = Logic.strip_prems (length tpairs, [], prop2);
   in
     (al, Thm {thy_ref = thy_ref,
-      der = Pt.infer_derivs' (Pt.varify_proof prop tfrees) der,
+      der = Deriv.rule1 (Pt.varify_proof prop tfrees) der,
       tags = [],
       maxidx = Int.max (0, maxidx),
       shyps = shyps,
       hyps = hyps,
       tpairs = rev (map Logic.dest_equals ts),

     val prop1 = attach_tpairs tpairs prop;
     val prop2 = Type.freeze prop1;
     val (ts, prop3) = Logic.strip_prems (length tpairs, [], prop2);
   in
     Thm {thy_ref = thy_ref,
-      der = Pt.infer_derivs' (Pt.freezeT prop1) der,
+      der = Deriv.rule1 (Pt.freezeT prop1) der,
       tags = [],
       maxidx = maxidx_of_term prop2,
       shyps = shyps,
       hyps = hyps,
       tpairs = rev (map Logic.dest_equals ts),

     val (As, B) = Logic.strip_horn prop;
   in
     if T <> propT then raise THM ("lift_rule: the term must have type prop", 0, [])
     else
       Thm {thy_ref = merge_thys1 goal orule,
-        der = Pt.infer_derivs' (Pt.lift_proof gprop inc prop) der,
+        der = Deriv.rule1 (Pt.lift_proof gprop inc prop) der,
         tags = [],
         maxidx = maxidx + inc,
         shyps = Sorts.union shyps sorts,  (*sic!*)
         hyps = hyps,
         tpairs = map (pairself lift_abs) tpairs,

 fun incr_indexes i (thm as Thm {thy_ref, der, maxidx, shyps, hyps, tpairs, prop, ...}) =
   if i < 0 then raise THM ("negative increment", 0, [thm])
   else if i = 0 then thm
   else
     Thm {thy_ref = thy_ref,
-      der = Pt.infer_derivs'
-        (Pt.map_proof_terms (Logic.incr_indexes ([], i)) (Logic.incr_tvar i)) der,
+      der = Deriv.rule1 (Pt.map_proof_terms (Logic.incr_indexes ([], i)) (Logic.incr_tvar i)) der,
       tags = [],
       maxidx = maxidx + i,
       shyps = shyps,
       hyps = hyps,
       tpairs = map (pairself (Logic.incr_indexes ([], i))) tpairs,

     val Thm {thy_ref, der, maxidx, shyps, hyps, prop, ...} = state;
     val thy = Theory.deref thy_ref;
     val (tpairs, Bs, Bi, C) = dest_state (state, i);
     fun newth n (env as Envir.Envir {maxidx, ...}, tpairs) =
       Thm {
-        der = Pt.infer_derivs'
+        der = Deriv.rule1
           ((if Envir.is_empty env then I else (Pt.norm_proof' env)) o
             Pt.assumption_proof Bs Bi n) der,
         tags = [],
         maxidx = maxidx,
         shyps = Envir.insert_sorts env shyps,

   in
     (case find_index Pattern.aeconv (Logic.assum_pairs (~1, Bi)) of
       ~1 => raise THM ("eq_assumption", 0, [state])
     | n =>
         Thm {thy_ref = thy_ref,
-          der = Pt.infer_derivs' (Pt.assumption_proof Bs Bi (n + 1)) der,
+          der = Deriv.rule1 (Pt.assumption_proof Bs Bi (n + 1)) der,
           tags = [],
           maxidx = maxidx,
           shyps = shyps,
           hyps = hyps,
           tpairs = tpairs,

         let val (ps, qs) = chop m asms
         in list_all (params, Logic.list_implies (qs @ ps, concl)) end
       else raise THM ("rotate_rule", k, [state]);
   in
     Thm {thy_ref = thy_ref,
-      der = Pt.infer_derivs' (Pt.rotate_proof Bs Bi m) der,
+      der = Deriv.rule1 (Pt.rotate_proof Bs Bi m) der,
       tags = [],
       maxidx = maxidx,
       shyps = shyps,
       hyps = hyps,
       tpairs = tpairs,

         let val (ps, qs) = chop m moved_prems
         in Logic.list_implies (fixed_prems @ qs @ ps, concl) end
       else raise THM ("permute_prems: k", k, [rl]);
   in
     Thm {thy_ref = thy_ref,
-      der = Pt.infer_derivs' (Pt.permute_prems_prf prems j m) der,
+      der = Deriv.rule1 (Pt.permute_prems_prf prems j m) der,
       tags = [],
       maxidx = maxidx,
       shyps = shyps,
       hyps = hyps,
       tpairs = tpairs,

                 else if match then raise COMPOSE
                 else (*normalize the new rule fully*)
                   (ntps, (map normt (Bs @ As), normt C))
              end
            val th =
-             Thm{der = Pt.infer_derivs
+             Thm{der = Deriv.rule2
                    ((if Envir.is_empty env then I
                      else if Envir.above env smax then
                        (fn f => fn der => f (Pt.norm_proof' env der))
                      else
                        curry op oo (Pt.norm_proof' env))

      (*Modify assumptions, deleting n-th if n>0 for e-resolution*)
      fun newAs(As0, n, dpairs, tpairs) =
        let val (As1, rder') =
          if not lifted then (As0, rder)
          else (map (rename_bvars(dpairs,tpairs,B)) As0,
-           Pt.infer_derivs' (Pt.map_proof_terms
+           Deriv.rule1 (Pt.map_proof_terms
              (rename_bvars (dpairs, tpairs, Bound 0)) I) rder);
        in (map (if flatten then (Logic.flatten_params n) else I) As1, As1, rder', n)
           handle TERM _ =>
           raise THM("bicompose: 1st premise", 0, [orule])
        end;

     fn (thy2, data) =>
       let
         val thy' = Theory.merge (Theory.deref thy_ref1, thy2);
         val (prop, T, maxidx) = Sign.certify_term thy' (oracle (thy', data));
         val shyps' = Sorts.insert_term prop [];
-        val der = (true, Pt.oracle_proof name prop);
+        val der = Deriv.oracle name prop;
       in
         if T <> propT then
           raise THM ("Oracle's result must have type prop: " ^ name, 0, [])
         else
           Thm {thy_ref = Theory.check_thy thy', der = der, tags = [],