src/Pure/thm.ML
author wenzelm
Sun Nov 11 20:31:46 2012 +0100 (2012-11-11)
changeset 50081 9b92ee8dec98
parent 49008 a3cdb49c22cc
child 50126 3dec88149176
permissions -rw-r--r--
tuned;
     1 (*  Title:      Pure/thm.ML
     2     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3     Author:     Makarius
     4 
     5 The very core of Isabelle's Meta Logic: certified types and terms,
     6 derivations, theorems, framework rules (including lifting and
     7 resolution), oracles.
     8 *)
     9 
    10 signature BASIC_THM =
    11   sig
    12   (*certified types*)
    13   type ctyp
    14   val rep_ctyp: ctyp ->
    15    {thy_ref: theory_ref,
    16     T: typ,
    17     maxidx: int,
    18     sorts: sort Ord_List.T}
    19   val theory_of_ctyp: ctyp -> theory
    20   val typ_of: ctyp -> typ
    21   val ctyp_of: theory -> typ -> ctyp
    22 
    23   (*certified terms*)
    24   type cterm
    25   exception CTERM of string * cterm list
    26   val rep_cterm: cterm ->
    27    {thy_ref: theory_ref,
    28     t: term,
    29     T: typ,
    30     maxidx: int,
    31     sorts: sort Ord_List.T}
    32   val crep_cterm: cterm ->
    33     {thy_ref: theory_ref, t: term, T: ctyp, maxidx: int, sorts: sort Ord_List.T}
    34   val theory_of_cterm: cterm -> theory
    35   val term_of: cterm -> term
    36   val cterm_of: theory -> term -> cterm
    37   val ctyp_of_term: cterm -> ctyp
    38 
    39   (*theorems*)
    40   type thm
    41   type conv = cterm -> thm
    42   val rep_thm: thm ->
    43    {thy_ref: theory_ref,
    44     tags: Properties.T,
    45     maxidx: int,
    46     shyps: sort Ord_List.T,
    47     hyps: term Ord_List.T,
    48     tpairs: (term * term) list,
    49     prop: term}
    50   val crep_thm: thm ->
    51    {thy_ref: theory_ref,
    52     tags: Properties.T,
    53     maxidx: int,
    54     shyps: sort Ord_List.T,
    55     hyps: cterm Ord_List.T,
    56     tpairs: (cterm * cterm) list,
    57     prop: cterm}
    58   exception THM of string * int * thm list
    59   val theory_of_thm: thm -> theory
    60   val prop_of: thm -> term
    61   val concl_of: thm -> term
    62   val prems_of: thm -> term list
    63   val nprems_of: thm -> int
    64   val cprop_of: thm -> cterm
    65   val cprem_of: thm -> int -> cterm
    66 end;
    67 
    68 signature THM =
    69 sig
    70   include BASIC_THM
    71   val dest_ctyp: ctyp -> ctyp list
    72   val dest_comb: cterm -> cterm * cterm
    73   val dest_fun: cterm -> cterm
    74   val dest_arg: cterm -> cterm
    75   val dest_fun2: cterm -> cterm
    76   val dest_arg1: cterm -> cterm
    77   val dest_abs: string option -> cterm -> cterm * cterm
    78   val apply: cterm -> cterm -> cterm
    79   val lambda_name: string * cterm -> cterm -> cterm
    80   val lambda: cterm -> cterm -> cterm
    81   val adjust_maxidx_cterm: int -> cterm -> cterm
    82   val incr_indexes_cterm: int -> cterm -> cterm
    83   val match: cterm * cterm -> (ctyp * ctyp) list * (cterm * cterm) list
    84   val first_order_match: cterm * cterm -> (ctyp * ctyp) list * (cterm * cterm) list
    85   val fold_terms: (term -> 'a -> 'a) -> thm -> 'a -> 'a
    86   val terms_of_tpairs: (term * term) list -> term list
    87   val full_prop_of: thm -> term
    88   val maxidx_of: thm -> int
    89   val maxidx_thm: thm -> int -> int
    90   val hyps_of: thm -> term list
    91   val tpairs_of: thm -> (term * term) list
    92   val no_prems: thm -> bool
    93   val major_prem_of: thm -> term
    94   val transfer: theory -> thm -> thm
    95   val weaken: cterm -> thm -> thm
    96   val weaken_sorts: sort list -> cterm -> cterm
    97   val extra_shyps: thm -> sort list
    98   val proof_bodies_of: thm list -> proof_body list
    99   val proof_body_of: thm -> proof_body
   100   val proof_of: thm -> proof
   101   val join_proofs: thm list -> unit
   102   val status_of: thm -> {oracle: bool, unfinished: bool, failed: bool}
   103   val future: thm future -> cterm -> thm
   104   val derivation_name: thm -> string
   105   val name_derivation: string -> thm -> thm
   106   val axiom: theory -> string -> thm
   107   val axioms_of: theory -> (string * thm) list
   108   val get_tags: thm -> Properties.T
   109   val map_tags: (Properties.T -> Properties.T) -> thm -> thm
   110   val norm_proof: thm -> thm
   111   val adjust_maxidx_thm: int -> thm -> thm
   112   (*meta rules*)
   113   val assume: cterm -> thm
   114   val implies_intr: cterm -> thm -> thm
   115   val implies_elim: thm -> thm -> thm
   116   val forall_intr: cterm -> thm -> thm
   117   val forall_elim: cterm -> thm -> thm
   118   val reflexive: cterm -> thm
   119   val symmetric: thm -> thm
   120   val transitive: thm -> thm -> thm
   121   val beta_conversion: bool -> conv
   122   val eta_conversion: conv
   123   val eta_long_conversion: conv
   124   val abstract_rule: string -> cterm -> thm -> thm
   125   val combination: thm -> thm -> thm
   126   val equal_intr: thm -> thm -> thm
   127   val equal_elim: thm -> thm -> thm
   128   val flexflex_rule: thm -> thm Seq.seq
   129   val generalize: string list * string list -> int -> thm -> thm
   130   val instantiate: (ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm
   131   val instantiate_cterm: (ctyp * ctyp) list * (cterm * cterm) list -> cterm -> cterm
   132   val trivial: cterm -> thm
   133   val of_class: ctyp * class -> thm
   134   val strip_shyps: thm -> thm
   135   val unconstrainT: thm -> thm
   136   val varifyT_global': (string * sort) list -> thm -> ((string * sort) * indexname) list * thm
   137   val varifyT_global: thm -> thm
   138   val legacy_freezeT: thm -> thm
   139   val lift_rule: cterm -> thm -> thm
   140   val incr_indexes: int -> thm -> thm
   141   val assumption: int -> thm -> thm Seq.seq
   142   val eq_assumption: int -> thm -> thm
   143   val rotate_rule: int -> int -> thm -> thm
   144   val permute_prems: int -> int -> thm -> thm
   145   val rename_params_rule: string list * int -> thm -> thm
   146   val rename_boundvars: term -> term -> thm -> thm
   147   val compose_no_flatten: bool -> thm * int -> int -> thm -> thm Seq.seq
   148   val bicompose: bool -> bool * thm * int -> int -> thm -> thm Seq.seq
   149   val biresolution: bool -> (bool * thm) list -> int -> thm -> thm Seq.seq
   150   val extern_oracles: Proof.context -> xstring list
   151   val add_oracle: binding * ('a -> cterm) -> theory -> (string * ('a -> thm)) * theory
   152 end;
   153 
   154 structure Thm: THM =
   155 struct
   156 
   157 (*** Certified terms and types ***)
   158 
   159 (** certified types **)
   160 
   161 abstype ctyp = Ctyp of
   162  {thy_ref: theory_ref,
   163   T: typ,
   164   maxidx: int,
   165   sorts: sort Ord_List.T}
   166 with
   167 
   168 fun rep_ctyp (Ctyp args) = args;
   169 fun theory_of_ctyp (Ctyp {thy_ref, ...}) = Theory.deref thy_ref;
   170 fun typ_of (Ctyp {T, ...}) = T;
   171 
   172 fun ctyp_of thy raw_T =
   173   let
   174     val T = Sign.certify_typ thy raw_T;
   175     val maxidx = Term.maxidx_of_typ T;
   176     val sorts = Sorts.insert_typ T [];
   177   in Ctyp {thy_ref = Theory.check_thy thy, T = T, maxidx = maxidx, sorts = sorts} end;
   178 
   179 fun dest_ctyp (Ctyp {thy_ref, T = Type (_, Ts), maxidx, sorts}) =
   180       map (fn T => Ctyp {thy_ref = thy_ref, T = T, maxidx = maxidx, sorts = sorts}) Ts
   181   | dest_ctyp cT = raise TYPE ("dest_ctyp", [typ_of cT], []);
   182 
   183 
   184 
   185 (** certified terms **)
   186 
   187 (*certified terms with checked typ, maxidx, and sorts*)
   188 abstype cterm = Cterm of
   189  {thy_ref: theory_ref,
   190   t: term,
   191   T: typ,
   192   maxidx: int,
   193   sorts: sort Ord_List.T}
   194 with
   195 
   196 exception CTERM of string * cterm list;
   197 
   198 fun rep_cterm (Cterm args) = args;
   199 
   200 fun crep_cterm (Cterm {thy_ref, t, T, maxidx, sorts}) =
   201   {thy_ref = thy_ref, t = t, maxidx = maxidx, sorts = sorts,
   202     T = Ctyp {thy_ref = thy_ref, T = T, maxidx = maxidx, sorts = sorts}};
   203 
   204 fun theory_of_cterm (Cterm {thy_ref, ...}) = Theory.deref thy_ref;
   205 fun term_of (Cterm {t, ...}) = t;
   206 
   207 fun ctyp_of_term (Cterm {thy_ref, T, maxidx, sorts, ...}) =
   208   Ctyp {thy_ref = thy_ref, T = T, maxidx = maxidx, sorts = sorts};
   209 
   210 fun cterm_of thy tm =
   211   let
   212     val (t, T, maxidx) = Sign.certify_term thy tm;
   213     val sorts = Sorts.insert_term t [];
   214   in Cterm {thy_ref = Theory.check_thy thy, t = t, T = T, maxidx = maxidx, sorts = sorts} end;
   215 
   216 fun merge_thys0 (Cterm {thy_ref = r1, ...}) (Cterm {thy_ref = r2, ...}) =
   217   Theory.merge_refs (r1, r2);
   218 
   219 
   220 (* destructors *)
   221 
   222 fun dest_comb (Cterm {t = c $ a, T, thy_ref, maxidx, sorts}) =
   223       let val A = Term.argument_type_of c 0 in
   224         (Cterm {t = c, T = A --> T, thy_ref = thy_ref, maxidx = maxidx, sorts = sorts},
   225          Cterm {t = a, T = A, thy_ref = thy_ref, maxidx = maxidx, sorts = sorts})
   226       end
   227   | dest_comb ct = raise CTERM ("dest_comb", [ct]);
   228 
   229 fun dest_fun (Cterm {t = c $ _, T, thy_ref, maxidx, sorts}) =
   230       let val A = Term.argument_type_of c 0
   231       in Cterm {t = c, T = A --> T, thy_ref = thy_ref, maxidx = maxidx, sorts = sorts} end
   232   | dest_fun ct = raise CTERM ("dest_fun", [ct]);
   233 
   234 fun dest_arg (Cterm {t = c $ a, T = _, thy_ref, maxidx, sorts}) =
   235       let val A = Term.argument_type_of c 0
   236       in Cterm {t = a, T = A, thy_ref = thy_ref, maxidx = maxidx, sorts = sorts} end
   237   | dest_arg ct = raise CTERM ("dest_arg", [ct]);
   238 
   239 
   240 fun dest_fun2 (Cterm {t = c $ _ $ _, T, thy_ref, maxidx, sorts}) =
   241       let
   242         val A = Term.argument_type_of c 0;
   243         val B = Term.argument_type_of c 1;
   244       in Cterm {t = c, T = A --> B --> T, thy_ref = thy_ref, maxidx = maxidx, sorts = sorts} end
   245   | dest_fun2 ct = raise CTERM ("dest_fun2", [ct]);
   246 
   247 fun dest_arg1 (Cterm {t = c $ a $ _, T = _, thy_ref, maxidx, sorts}) =
   248       let val A = Term.argument_type_of c 0
   249       in Cterm {t = a, T = A, thy_ref = thy_ref, maxidx = maxidx, sorts = sorts} end
   250   | dest_arg1 ct = raise CTERM ("dest_arg1", [ct]);
   251 
   252 fun dest_abs a (Cterm {t = Abs (x, T, t), T = Type ("fun", [_, U]), thy_ref, maxidx, sorts}) =
   253       let val (y', t') = Term.dest_abs (the_default x a, T, t) in
   254         (Cterm {t = Free (y', T), T = T, thy_ref = thy_ref, maxidx = maxidx, sorts = sorts},
   255           Cterm {t = t', T = U, thy_ref = thy_ref, maxidx = maxidx, sorts = sorts})
   256       end
   257   | dest_abs _ ct = raise CTERM ("dest_abs", [ct]);
   258 
   259 
   260 (* constructors *)
   261 
   262 fun apply
   263   (cf as Cterm {t = f, T = Type ("fun", [dty, rty]), maxidx = maxidx1, sorts = sorts1, ...})
   264   (cx as Cterm {t = x, T, maxidx = maxidx2, sorts = sorts2, ...}) =
   265     if T = dty then
   266       Cterm {thy_ref = merge_thys0 cf cx,
   267         t = f $ x,
   268         T = rty,
   269         maxidx = Int.max (maxidx1, maxidx2),
   270         sorts = Sorts.union sorts1 sorts2}
   271       else raise CTERM ("apply: types don't agree", [cf, cx])
   272   | apply cf cx = raise CTERM ("apply: first arg is not a function", [cf, cx]);
   273 
   274 fun lambda_name
   275   (x, ct1 as Cterm {t = t1, T = T1, maxidx = maxidx1, sorts = sorts1, ...})
   276   (ct2 as Cterm {t = t2, T = T2, maxidx = maxidx2, sorts = sorts2, ...}) =
   277     let val t = Term.lambda_name (x, t1) t2 in
   278       Cterm {thy_ref = merge_thys0 ct1 ct2,
   279         t = t, T = T1 --> T2,
   280         maxidx = Int.max (maxidx1, maxidx2),
   281         sorts = Sorts.union sorts1 sorts2}
   282     end;
   283 
   284 fun lambda t u = lambda_name ("", t) u;
   285 
   286 
   287 (* indexes *)
   288 
   289 fun adjust_maxidx_cterm i (ct as Cterm {thy_ref, t, T, maxidx, sorts}) =
   290   if maxidx = i then ct
   291   else if maxidx < i then
   292     Cterm {maxidx = i, thy_ref = thy_ref, t = t, T = T, sorts = sorts}
   293   else
   294     Cterm {maxidx = Int.max (maxidx_of_term t, i), thy_ref = thy_ref, t = t, T = T, sorts = sorts};
   295 
   296 fun incr_indexes_cterm i (ct as Cterm {thy_ref, t, T, maxidx, sorts}) =
   297   if i < 0 then raise CTERM ("negative increment", [ct])
   298   else if i = 0 then ct
   299   else Cterm {thy_ref = thy_ref, t = Logic.incr_indexes ([], i) t,
   300     T = Logic.incr_tvar i T, maxidx = maxidx + i, sorts = sorts};
   301 
   302 
   303 (* matching *)
   304 
   305 local
   306 
   307 fun gen_match match
   308     (ct1 as Cterm {t = t1, sorts = sorts1, ...},
   309      ct2 as Cterm {t = t2, sorts = sorts2, maxidx = maxidx2, ...}) =
   310   let
   311     val thy = Theory.deref (merge_thys0 ct1 ct2);
   312     val (Tinsts, tinsts) = match thy (t1, t2) (Vartab.empty, Vartab.empty);
   313     val sorts = Sorts.union sorts1 sorts2;
   314     fun mk_cTinst ((a, i), (S, T)) =
   315       (Ctyp {T = TVar ((a, i), S), thy_ref = Theory.check_thy thy, maxidx = i, sorts = sorts},
   316        Ctyp {T = T, thy_ref = Theory.check_thy thy, maxidx = maxidx2, sorts = sorts});
   317     fun mk_ctinst ((x, i), (T, t)) =
   318       let val T = Envir.subst_type Tinsts T in
   319         (Cterm {t = Var ((x, i), T), T = T, thy_ref = Theory.check_thy thy,
   320           maxidx = i, sorts = sorts},
   321          Cterm {t = t, T = T, thy_ref = Theory.check_thy thy, maxidx = maxidx2, sorts = sorts})
   322       end;
   323   in (Vartab.fold (cons o mk_cTinst) Tinsts [], Vartab.fold (cons o mk_ctinst) tinsts []) end;
   324 
   325 in
   326 
   327 val match = gen_match Pattern.match;
   328 val first_order_match = gen_match Pattern.first_order_match;
   329 
   330 end;
   331 
   332 
   333 
   334 (*** Derivations and Theorems ***)
   335 
   336 abstype thm = Thm of
   337  deriv *                        (*derivation*)
   338  {thy_ref: theory_ref,          (*dynamic reference to theory*)
   339   tags: Properties.T,           (*additional annotations/comments*)
   340   maxidx: int,                  (*maximum index of any Var or TVar*)
   341   shyps: sort Ord_List.T,       (*sort hypotheses*)
   342   hyps: term Ord_List.T,        (*hypotheses*)
   343   tpairs: (term * term) list,   (*flex-flex pairs*)
   344   prop: term}                   (*conclusion*)
   345 and deriv = Deriv of
   346  {promises: (serial * thm future) Ord_List.T,
   347   body: Proofterm.proof_body}
   348 with
   349 
   350 type conv = cterm -> thm;
   351 
   352 (*errors involving theorems*)
   353 exception THM of string * int * thm list;
   354 
   355 fun rep_thm (Thm (_, args)) = args;
   356 
   357 fun crep_thm (Thm (_, {thy_ref, tags, maxidx, shyps, hyps, tpairs, prop})) =
   358   let fun cterm max t = Cterm {thy_ref = thy_ref, t = t, T = propT, maxidx = max, sorts = shyps} in
   359    {thy_ref = thy_ref, tags = tags, maxidx = maxidx, shyps = shyps,
   360     hyps = map (cterm ~1) hyps,
   361     tpairs = map (pairself (cterm maxidx)) tpairs,
   362     prop = cterm maxidx prop}
   363   end;
   364 
   365 fun fold_terms f (Thm (_, {tpairs, prop, hyps, ...})) =
   366   fold (fn (t, u) => f t #> f u) tpairs #> f prop #> fold f hyps;
   367 
   368 fun terms_of_tpairs tpairs = fold_rev (fn (t, u) => cons t o cons u) tpairs [];
   369 
   370 fun eq_tpairs ((t, u), (t', u')) = t aconv t' andalso u aconv u';
   371 fun union_tpairs ts us = Library.merge eq_tpairs (ts, us);
   372 val maxidx_tpairs = fold (fn (t, u) => Term.maxidx_term t #> Term.maxidx_term u);
   373 
   374 fun attach_tpairs tpairs prop =
   375   Logic.list_implies (map Logic.mk_equals tpairs, prop);
   376 
   377 fun full_prop_of (Thm (_, {tpairs, prop, ...})) = attach_tpairs tpairs prop;
   378 
   379 val union_hyps = Ord_List.union Term_Ord.fast_term_ord;
   380 val insert_hyps = Ord_List.insert Term_Ord.fast_term_ord;
   381 val remove_hyps = Ord_List.remove Term_Ord.fast_term_ord;
   382 
   383 
   384 (* merge theories of cterms/thms -- trivial absorption only *)
   385 
   386 fun merge_thys1 (Cterm {thy_ref = r1, ...}) (Thm (_, {thy_ref = r2, ...})) =
   387   Theory.merge_refs (r1, r2);
   388 
   389 fun merge_thys2 (Thm (_, {thy_ref = r1, ...})) (Thm (_, {thy_ref = r2, ...})) =
   390   Theory.merge_refs (r1, r2);
   391 
   392 
   393 (* basic components *)
   394 
   395 val theory_of_thm = Theory.deref o #thy_ref o rep_thm;
   396 val maxidx_of = #maxidx o rep_thm;
   397 fun maxidx_thm th i = Int.max (maxidx_of th, i);
   398 val hyps_of = #hyps o rep_thm;
   399 val prop_of = #prop o rep_thm;
   400 val tpairs_of = #tpairs o rep_thm;
   401 
   402 val concl_of = Logic.strip_imp_concl o prop_of;
   403 val prems_of = Logic.strip_imp_prems o prop_of;
   404 val nprems_of = Logic.count_prems o prop_of;
   405 fun no_prems th = nprems_of th = 0;
   406 
   407 fun major_prem_of th =
   408   (case prems_of th of
   409     prem :: _ => Logic.strip_assums_concl prem
   410   | [] => raise THM ("major_prem_of: rule with no premises", 0, [th]));
   411 
   412 (*the statement of any thm is a cterm*)
   413 fun cprop_of (Thm (_, {thy_ref, maxidx, shyps, prop, ...})) =
   414   Cterm {thy_ref = thy_ref, maxidx = maxidx, T = propT, t = prop, sorts = shyps};
   415 
   416 fun cprem_of (th as Thm (_, {thy_ref, maxidx, shyps, prop, ...})) i =
   417   Cterm {thy_ref = thy_ref, maxidx = maxidx, T = propT, sorts = shyps,
   418     t = Logic.nth_prem (i, prop) handle TERM _ => raise THM ("cprem_of", i, [th])};
   419 
   420 (*explicit transfer to a super theory*)
   421 fun transfer thy' thm =
   422   let
   423     val Thm (der, {thy_ref, tags, maxidx, shyps, hyps, tpairs, prop}) = thm;
   424     val thy = Theory.deref thy_ref;
   425     val _ = Theory.subthy (thy, thy') orelse raise THM ("transfer: not a super theory", 0, [thm]);
   426     val is_eq = Theory.eq_thy (thy, thy');
   427     val _ = Theory.check_thy thy;
   428   in
   429     if is_eq then thm
   430     else
   431       Thm (der,
   432        {thy_ref = Theory.check_thy thy',
   433         tags = tags,
   434         maxidx = maxidx,
   435         shyps = shyps,
   436         hyps = hyps,
   437         tpairs = tpairs,
   438         prop = prop})
   439   end;
   440 
   441 (*explicit weakening: maps |- B to A |- B*)
   442 fun weaken raw_ct th =
   443   let
   444     val ct as Cterm {t = A, T, sorts, maxidx = maxidxA, ...} = adjust_maxidx_cterm ~1 raw_ct;
   445     val Thm (der, {tags, maxidx, shyps, hyps, tpairs, prop, ...}) = th;
   446   in
   447     if T <> propT then
   448       raise THM ("weaken: assumptions must have type prop", 0, [])
   449     else if maxidxA <> ~1 then
   450       raise THM ("weaken: assumptions may not contain schematic variables", maxidxA, [])
   451     else
   452       Thm (der,
   453        {thy_ref = merge_thys1 ct th,
   454         tags = tags,
   455         maxidx = maxidx,
   456         shyps = Sorts.union sorts shyps,
   457         hyps = insert_hyps A hyps,
   458         tpairs = tpairs,
   459         prop = prop})
   460   end;
   461 
   462 fun weaken_sorts raw_sorts ct =
   463   let
   464     val Cterm {thy_ref, t, T, maxidx, sorts} = ct;
   465     val thy = Theory.deref thy_ref;
   466     val more_sorts = Sorts.make (map (Sign.certify_sort thy) raw_sorts);
   467     val sorts' = Sorts.union sorts more_sorts;
   468   in Cterm {thy_ref = Theory.check_thy thy, t = t, T = T, maxidx = maxidx, sorts = sorts'} end;
   469 
   470 (*dangling sort constraints of a thm*)
   471 fun extra_shyps (th as Thm (_, {shyps, ...})) =
   472   Sorts.subtract (fold_terms Sorts.insert_term th []) shyps;
   473 
   474 
   475 
   476 (** derivations and promised proofs **)
   477 
   478 fun make_deriv promises oracles thms proof =
   479   Deriv {promises = promises, body = PBody {oracles = oracles, thms = thms, proof = proof}};
   480 
   481 val empty_deriv = make_deriv [] [] [] Proofterm.MinProof;
   482 
   483 
   484 (* inference rules *)
   485 
   486 fun promise_ord ((i, _), (j, _)) = int_ord (j, i);
   487 
   488 fun deriv_rule2 f
   489     (Deriv {promises = ps1, body = PBody {oracles = oras1, thms = thms1, proof = prf1}})
   490     (Deriv {promises = ps2, body = PBody {oracles = oras2, thms = thms2, proof = prf2}}) =
   491   let
   492     val ps = Ord_List.union promise_ord ps1 ps2;
   493     val oras = Proofterm.unions_oracles [oras1, oras2];
   494     val thms = Proofterm.unions_thms [thms1, thms2];
   495     val prf =
   496       (case ! Proofterm.proofs of
   497         2 => f prf1 prf2
   498       | 1 => MinProof
   499       | 0 => MinProof
   500       | i => error ("Illegal level of detail for proof objects: " ^ string_of_int i));
   501   in make_deriv ps oras thms prf end;
   502 
   503 fun deriv_rule1 f = deriv_rule2 (K f) empty_deriv;
   504 fun deriv_rule0 prf = deriv_rule1 I (make_deriv [] [] [] prf);
   505 
   506 fun deriv_rule_unconditional f (Deriv {promises, body = PBody {oracles, thms, proof}}) =
   507   make_deriv promises oracles thms (f proof);
   508 
   509 
   510 (* fulfilled proofs *)
   511 
   512 fun raw_body_of (Thm (Deriv {body, ...}, _)) = body;
   513 fun raw_promises_of (Thm (Deriv {promises, ...}, _)) = promises;
   514 
   515 fun join_promises [] = ()
   516   | join_promises promises = join_promises_of (Future.joins (map snd promises))
   517 and join_promises_of thms = join_promises (Ord_List.make promise_ord (maps raw_promises_of thms));
   518 
   519 fun fulfill_body (Thm (Deriv {promises, body}, {thy_ref, ...})) =
   520   Proofterm.fulfill_norm_proof (Theory.deref thy_ref) (fulfill_promises promises) body
   521 and fulfill_promises promises =
   522   map fst promises ~~ map fulfill_body (Future.joins (map snd promises));
   523 
   524 fun proof_bodies_of thms =
   525   let
   526     val _ = join_promises_of thms;
   527     val bodies = map fulfill_body thms;
   528     val _ = Proofterm.join_bodies bodies;
   529   in bodies end;
   530 
   531 val proof_body_of = singleton proof_bodies_of;
   532 val proof_of = Proofterm.proof_of o proof_body_of;
   533 
   534 val join_proofs = ignore o proof_bodies_of;
   535 
   536 
   537 (* derivation status *)
   538 
   539 fun status_of (Thm (Deriv {promises, body}, _)) =
   540   let
   541     val ps = map (Future.peek o snd) promises;
   542     val bodies = body ::
   543       map_filter (fn SOME (Exn.Res th) => SOME (raw_body_of th) | _ => NONE) ps;
   544     val {oracle, unfinished, failed} = Proofterm.status_of bodies;
   545   in
   546    {oracle = oracle,
   547     unfinished = unfinished orelse exists is_none ps,
   548     failed = failed orelse exists (fn SOME (Exn.Exn _) => true | _ => false) ps}
   549   end;
   550 
   551 
   552 (* future rule *)
   553 
   554 fun future_result i orig_thy orig_shyps orig_prop thm =
   555   let
   556     fun err msg = raise THM ("future_result: " ^ msg, 0, [thm]);
   557     val Thm (Deriv {promises, ...}, {thy_ref, shyps, hyps, tpairs, prop, ...}) = thm;
   558 
   559     val _ = Theory.eq_thy (Theory.deref thy_ref, orig_thy) orelse err "bad theory";
   560     val _ = Theory.check_thy orig_thy;
   561     val _ = prop aconv orig_prop orelse err "bad prop";
   562     val _ = null tpairs orelse err "bad tpairs";
   563     val _ = null hyps orelse err "bad hyps";
   564     val _ = Sorts.subset (shyps, orig_shyps) orelse err "bad shyps";
   565     val _ = forall (fn (j, _) => i <> j) promises orelse err "bad dependencies";
   566     val _ = join_promises promises;
   567   in thm end;
   568 
   569 fun future future_thm ct =
   570   let
   571     val Cterm {thy_ref = thy_ref, t = prop, T, maxidx, sorts} = ct;
   572     val thy = Context.reject_draft (Theory.deref thy_ref);
   573     val _ = T <> propT andalso raise CTERM ("future: prop expected", [ct]);
   574 
   575     val i = serial ();
   576     val future = future_thm |> Future.map (future_result i thy sorts prop);
   577   in
   578     Thm (make_deriv [(i, future)] [] [] (Proofterm.promise_proof thy i prop),
   579      {thy_ref = thy_ref,
   580       tags = [],
   581       maxidx = maxidx,
   582       shyps = sorts,
   583       hyps = [],
   584       tpairs = [],
   585       prop = prop})
   586   end;
   587 
   588 
   589 (* closed derivations with official name *)
   590 
   591 (*non-deterministic, depends on unknown promises*)
   592 fun derivation_name (Thm (Deriv {body, ...}, {shyps, hyps, prop, ...})) =
   593   Proofterm.get_name shyps hyps prop (Proofterm.proof_of body);
   594 
   595 fun name_derivation name (thm as Thm (der, args)) =
   596   let
   597     val Deriv {promises, body} = der;
   598     val {thy_ref, shyps, hyps, prop, tpairs, ...} = args;
   599     val _ = null tpairs orelse raise THM ("put_name: unsolved flex-flex constraints", 0, [thm]);
   600 
   601     val ps = map (apsnd (Future.map fulfill_body)) promises;
   602     val thy = Theory.deref thy_ref;
   603     val (pthm, proof) = Proofterm.thm_proof thy name shyps hyps prop ps body;
   604     val der' = make_deriv [] [] [pthm] proof;
   605     val _ = Theory.check_thy thy;
   606   in Thm (der', args) end;
   607 
   608 
   609 
   610 (** Axioms **)
   611 
   612 fun axiom theory name =
   613   let
   614     fun get_ax thy =
   615       Symtab.lookup (Theory.axiom_table thy) name
   616       |> Option.map (fn prop =>
   617            let
   618              val der = deriv_rule0 (Proofterm.axm_proof name prop);
   619              val maxidx = maxidx_of_term prop;
   620              val shyps = Sorts.insert_term prop [];
   621            in
   622              Thm (der, {thy_ref = Theory.check_thy thy, tags = [],
   623                maxidx = maxidx, shyps = shyps, hyps = [], tpairs = [], prop = prop})
   624            end);
   625   in
   626     (case get_first get_ax (Theory.nodes_of theory) of
   627       SOME thm => thm
   628     | NONE => raise THEORY ("No axiom " ^ quote name, [theory]))
   629   end;
   630 
   631 (*return additional axioms of this theory node*)
   632 fun axioms_of thy =
   633   map (fn s => (s, axiom thy s)) (Symtab.keys (Theory.axiom_table thy));
   634 
   635 
   636 (* tags *)
   637 
   638 val get_tags = #tags o rep_thm;
   639 
   640 fun map_tags f (Thm (der, {thy_ref, tags, maxidx, shyps, hyps, tpairs, prop})) =
   641   Thm (der, {thy_ref = thy_ref, tags = f tags, maxidx = maxidx,
   642     shyps = shyps, hyps = hyps, tpairs = tpairs, prop = prop});
   643 
   644 
   645 (* technical adjustments *)
   646 
   647 fun norm_proof (Thm (der, args as {thy_ref, ...})) =
   648   let
   649     val thy = Theory.deref thy_ref;
   650     val der' = deriv_rule1 (Proofterm.rew_proof thy) der;
   651     val _ = Theory.check_thy thy;
   652   in Thm (der', args) end;
   653 
   654 fun adjust_maxidx_thm i (th as Thm (der, {thy_ref, tags, maxidx, shyps, hyps, tpairs, prop})) =
   655   if maxidx = i then th
   656   else if maxidx < i then
   657     Thm (der, {maxidx = i, thy_ref = thy_ref, tags = tags, shyps = shyps,
   658       hyps = hyps, tpairs = tpairs, prop = prop})
   659   else
   660     Thm (der, {maxidx = Int.max (maxidx_tpairs tpairs (maxidx_of_term prop), i), thy_ref = thy_ref,
   661       tags = tags, shyps = shyps, hyps = hyps, tpairs = tpairs, prop = prop});
   662 
   663 
   664 
   665 (*** Meta rules ***)
   666 
   667 (** primitive rules **)
   668 
   669 (*The assumption rule A |- A*)
   670 fun assume raw_ct =
   671   let val Cterm {thy_ref, t = prop, T, maxidx, sorts} = adjust_maxidx_cterm ~1 raw_ct in
   672     if T <> propT then
   673       raise THM ("assume: prop", 0, [])
   674     else if maxidx <> ~1 then
   675       raise THM ("assume: variables", maxidx, [])
   676     else Thm (deriv_rule0 (Proofterm.Hyp prop),
   677      {thy_ref = thy_ref,
   678       tags = [],
   679       maxidx = ~1,
   680       shyps = sorts,
   681       hyps = [prop],
   682       tpairs = [],
   683       prop = prop})
   684   end;
   685 
   686 (*Implication introduction
   687     [A]
   688      :
   689      B
   690   -------
   691   A ==> B
   692 *)
   693 fun implies_intr
   694     (ct as Cterm {t = A, T, maxidx = maxidxA, sorts, ...})
   695     (th as Thm (der, {maxidx, hyps, shyps, tpairs, prop, ...})) =
   696   if T <> propT then
   697     raise THM ("implies_intr: assumptions must have type prop", 0, [th])
   698   else
   699     Thm (deriv_rule1 (Proofterm.implies_intr_proof A) der,
   700      {thy_ref = merge_thys1 ct th,
   701       tags = [],
   702       maxidx = Int.max (maxidxA, maxidx),
   703       shyps = Sorts.union sorts shyps,
   704       hyps = remove_hyps A hyps,
   705       tpairs = tpairs,
   706       prop = Logic.mk_implies (A, prop)});
   707 
   708 
   709 (*Implication elimination
   710   A ==> B    A
   711   ------------
   712         B
   713 *)
   714 fun implies_elim thAB thA =
   715   let
   716     val Thm (derA, {maxidx = maxA, hyps = hypsA, shyps = shypsA, tpairs = tpairsA,
   717       prop = propA, ...}) = thA
   718     and Thm (der, {maxidx, hyps, shyps, tpairs, prop, ...}) = thAB;
   719     fun err () = raise THM ("implies_elim: major premise", 0, [thAB, thA]);
   720   in
   721     case prop of
   722       Const ("==>", _) $ A $ B =>
   723         if A aconv propA then
   724           Thm (deriv_rule2 (curry Proofterm.%%) der derA,
   725            {thy_ref = merge_thys2 thAB thA,
   726             tags = [],
   727             maxidx = Int.max (maxA, maxidx),
   728             shyps = Sorts.union shypsA shyps,
   729             hyps = union_hyps hypsA hyps,
   730             tpairs = union_tpairs tpairsA tpairs,
   731             prop = B})
   732         else err ()
   733     | _ => err ()
   734   end;
   735 
   736 (*Forall introduction.  The Free or Var x must not be free in the hypotheses.
   737     [x]
   738      :
   739      A
   740   ------
   741   !!x. A
   742 *)
   743 fun forall_intr
   744     (ct as Cterm {t = x, T, sorts, ...})
   745     (th as Thm (der, {maxidx, shyps, hyps, tpairs, prop, ...})) =
   746   let
   747     fun result a =
   748       Thm (deriv_rule1 (Proofterm.forall_intr_proof x a) der,
   749        {thy_ref = merge_thys1 ct th,
   750         tags = [],
   751         maxidx = maxidx,
   752         shyps = Sorts.union sorts shyps,
   753         hyps = hyps,
   754         tpairs = tpairs,
   755         prop = Logic.all_const T $ Abs (a, T, abstract_over (x, prop))});
   756     fun check_occs a x ts =
   757       if exists (fn t => Logic.occs (x, t)) ts then
   758         raise THM ("forall_intr: variable " ^ quote a ^ " free in assumptions", 0, [th])
   759       else ();
   760   in
   761     case x of
   762       Free (a, _) => (check_occs a x hyps; check_occs a x (terms_of_tpairs tpairs); result a)
   763     | Var ((a, _), _) => (check_occs a x (terms_of_tpairs tpairs); result a)
   764     | _ => raise THM ("forall_intr: not a variable", 0, [th])
   765   end;
   766 
   767 (*Forall elimination
   768   !!x. A
   769   ------
   770   A[t/x]
   771 *)
   772 fun forall_elim
   773     (ct as Cterm {t, T, maxidx = maxt, sorts, ...})
   774     (th as Thm (der, {maxidx, shyps, hyps, tpairs, prop, ...})) =
   775   (case prop of
   776     Const ("all", Type ("fun", [Type ("fun", [qary, _]), _])) $ A =>
   777       if T <> qary then
   778         raise THM ("forall_elim: type mismatch", 0, [th])
   779       else
   780         Thm (deriv_rule1 (Proofterm.% o rpair (SOME t)) der,
   781          {thy_ref = merge_thys1 ct th,
   782           tags = [],
   783           maxidx = Int.max (maxidx, maxt),
   784           shyps = Sorts.union sorts shyps,
   785           hyps = hyps,
   786           tpairs = tpairs,
   787           prop = Term.betapply (A, t)})
   788   | _ => raise THM ("forall_elim: not quantified", 0, [th]));
   789 
   790 
   791 (* Equality *)
   792 
   793 (*Reflexivity
   794   t == t
   795 *)
   796 fun reflexive (Cterm {thy_ref, t, T = _, maxidx, sorts}) =
   797   Thm (deriv_rule0 Proofterm.reflexive,
   798    {thy_ref = thy_ref,
   799     tags = [],
   800     maxidx = maxidx,
   801     shyps = sorts,
   802     hyps = [],
   803     tpairs = [],
   804     prop = Logic.mk_equals (t, t)});
   805 
   806 (*Symmetry
   807   t == u
   808   ------
   809   u == t
   810 *)
   811 fun symmetric (th as Thm (der, {thy_ref, maxidx, shyps, hyps, tpairs, prop, ...})) =
   812   (case prop of
   813     (eq as Const ("==", _)) $ t $ u =>
   814       Thm (deriv_rule1 Proofterm.symmetric der,
   815        {thy_ref = thy_ref,
   816         tags = [],
   817         maxidx = maxidx,
   818         shyps = shyps,
   819         hyps = hyps,
   820         tpairs = tpairs,
   821         prop = eq $ u $ t})
   822     | _ => raise THM ("symmetric", 0, [th]));
   823 
   824 (*Transitivity
   825   t1 == u    u == t2
   826   ------------------
   827        t1 == t2
   828 *)
   829 fun transitive th1 th2 =
   830   let
   831     val Thm (der1, {maxidx = max1, hyps = hyps1, shyps = shyps1, tpairs = tpairs1,
   832       prop = prop1, ...}) = th1
   833     and Thm (der2, {maxidx = max2, hyps = hyps2, shyps = shyps2, tpairs = tpairs2,
   834       prop = prop2, ...}) = th2;
   835     fun err msg = raise THM ("transitive: " ^ msg, 0, [th1, th2]);
   836   in
   837     case (prop1, prop2) of
   838       ((eq as Const ("==", Type (_, [T, _]))) $ t1 $ u, Const ("==", _) $ u' $ t2) =>
   839         if not (u aconv u') then err "middle term"
   840         else
   841           Thm (deriv_rule2 (Proofterm.transitive u T) der1 der2,
   842            {thy_ref = merge_thys2 th1 th2,
   843             tags = [],
   844             maxidx = Int.max (max1, max2),
   845             shyps = Sorts.union shyps1 shyps2,
   846             hyps = union_hyps hyps1 hyps2,
   847             tpairs = union_tpairs tpairs1 tpairs2,
   848             prop = eq $ t1 $ t2})
   849      | _ =>  err "premises"
   850   end;
   851 
   852 (*Beta-conversion
   853   (%x. t)(u) == t[u/x]
   854   fully beta-reduces the term if full = true
   855 *)
   856 fun beta_conversion full (Cterm {thy_ref, t, T = _, maxidx, sorts}) =
   857   let val t' =
   858     if full then Envir.beta_norm t
   859     else
   860       (case t of Abs (_, _, bodt) $ u => subst_bound (u, bodt)
   861       | _ => raise THM ("beta_conversion: not a redex", 0, []));
   862   in
   863     Thm (deriv_rule0 Proofterm.reflexive,
   864      {thy_ref = thy_ref,
   865       tags = [],
   866       maxidx = maxidx,
   867       shyps = sorts,
   868       hyps = [],
   869       tpairs = [],
   870       prop = Logic.mk_equals (t, t')})
   871   end;
   872 
   873 fun eta_conversion (Cterm {thy_ref, t, T = _, maxidx, sorts}) =
   874   Thm (deriv_rule0 Proofterm.reflexive,
   875    {thy_ref = thy_ref,
   876     tags = [],
   877     maxidx = maxidx,
   878     shyps = sorts,
   879     hyps = [],
   880     tpairs = [],
   881     prop = Logic.mk_equals (t, Envir.eta_contract t)});
   882 
   883 fun eta_long_conversion (Cterm {thy_ref, t, T = _, maxidx, sorts}) =
   884   Thm (deriv_rule0 Proofterm.reflexive,
   885    {thy_ref = thy_ref,
   886     tags = [],
   887     maxidx = maxidx,
   888     shyps = sorts,
   889     hyps = [],
   890     tpairs = [],
   891     prop = Logic.mk_equals (t, Pattern.eta_long [] t)});
   892 
   893 (*The abstraction rule.  The Free or Var x must not be free in the hypotheses.
   894   The bound variable will be named "a" (since x will be something like x320)
   895       t == u
   896   --------------
   897   %x. t == %x. u
   898 *)
   899 fun abstract_rule a
   900     (Cterm {t = x, T, sorts, ...})
   901     (th as Thm (der, {thy_ref, maxidx, hyps, shyps, tpairs, prop, ...})) =
   902   let
   903     val (t, u) = Logic.dest_equals prop
   904       handle TERM _ => raise THM ("abstract_rule: premise not an equality", 0, [th]);
   905     val result =
   906       Thm (deriv_rule1 (Proofterm.abstract_rule x a) der,
   907        {thy_ref = thy_ref,
   908         tags = [],
   909         maxidx = maxidx,
   910         shyps = Sorts.union sorts shyps,
   911         hyps = hyps,
   912         tpairs = tpairs,
   913         prop = Logic.mk_equals
   914           (Abs (a, T, abstract_over (x, t)), Abs (a, T, abstract_over (x, u)))});
   915     fun check_occs a x ts =
   916       if exists (fn t => Logic.occs (x, t)) ts then
   917         raise THM ("abstract_rule: variable " ^ quote a ^ " free in assumptions", 0, [th])
   918       else ();
   919   in
   920     case x of
   921       Free (a, _) => (check_occs a x hyps; check_occs a x (terms_of_tpairs tpairs); result)
   922     | Var ((a, _), _) => (check_occs a x (terms_of_tpairs tpairs); result)
   923     | _ => raise THM ("abstract_rule: not a variable", 0, [th])
   924   end;
   925 
   926 (*The combination rule
   927   f == g  t == u
   928   --------------
   929     f t == g u
   930 *)
   931 fun combination th1 th2 =
   932   let
   933     val Thm (der1, {maxidx = max1, shyps = shyps1, hyps = hyps1, tpairs = tpairs1,
   934       prop = prop1, ...}) = th1
   935     and Thm (der2, {maxidx = max2, shyps = shyps2, hyps = hyps2, tpairs = tpairs2,
   936       prop = prop2, ...}) = th2;
   937     fun chktypes fT tT =
   938       (case fT of
   939         Type ("fun", [T1, _]) =>
   940           if T1 <> tT then
   941             raise THM ("combination: types", 0, [th1, th2])
   942           else ()
   943       | _ => raise THM ("combination: not function type", 0, [th1, th2]));
   944   in
   945     case (prop1, prop2) of
   946       (Const ("==", Type ("fun", [fT, _])) $ f $ g,
   947        Const ("==", Type ("fun", [tT, _])) $ t $ u) =>
   948         (chktypes fT tT;
   949           Thm (deriv_rule2 (Proofterm.combination f g t u fT) der1 der2,
   950            {thy_ref = merge_thys2 th1 th2,
   951             tags = [],
   952             maxidx = Int.max (max1, max2),
   953             shyps = Sorts.union shyps1 shyps2,
   954             hyps = union_hyps hyps1 hyps2,
   955             tpairs = union_tpairs tpairs1 tpairs2,
   956             prop = Logic.mk_equals (f $ t, g $ u)}))
   957      | _ => raise THM ("combination: premises", 0, [th1, th2])
   958   end;
   959 
   960 (*Equality introduction
   961   A ==> B  B ==> A
   962   ----------------
   963        A == B
   964 *)
   965 fun equal_intr th1 th2 =
   966   let
   967     val Thm (der1, {maxidx = max1, shyps = shyps1, hyps = hyps1, tpairs = tpairs1,
   968       prop = prop1, ...}) = th1
   969     and Thm (der2, {maxidx = max2, shyps = shyps2, hyps = hyps2, tpairs = tpairs2,
   970       prop = prop2, ...}) = th2;
   971     fun err msg = raise THM ("equal_intr: " ^ msg, 0, [th1, th2]);
   972   in
   973     case (prop1, prop2) of
   974       (Const("==>", _) $ A $ B, Const("==>", _) $ B' $ A') =>
   975         if A aconv A' andalso B aconv B' then
   976           Thm (deriv_rule2 (Proofterm.equal_intr A B) der1 der2,
   977            {thy_ref = merge_thys2 th1 th2,
   978             tags = [],
   979             maxidx = Int.max (max1, max2),
   980             shyps = Sorts.union shyps1 shyps2,
   981             hyps = union_hyps hyps1 hyps2,
   982             tpairs = union_tpairs tpairs1 tpairs2,
   983             prop = Logic.mk_equals (A, B)})
   984         else err "not equal"
   985     | _ =>  err "premises"
   986   end;
   987 
   988 (*The equal propositions rule
   989   A == B  A
   990   ---------
   991       B
   992 *)
   993 fun equal_elim th1 th2 =
   994   let
   995     val Thm (der1, {maxidx = max1, shyps = shyps1, hyps = hyps1,
   996       tpairs = tpairs1, prop = prop1, ...}) = th1
   997     and Thm (der2, {maxidx = max2, shyps = shyps2, hyps = hyps2,
   998       tpairs = tpairs2, prop = prop2, ...}) = th2;
   999     fun err msg = raise THM ("equal_elim: " ^ msg, 0, [th1, th2]);
  1000   in
  1001     case prop1 of
  1002       Const ("==", _) $ A $ B =>
  1003         if prop2 aconv A then
  1004           Thm (deriv_rule2 (Proofterm.equal_elim A B) der1 der2,
  1005            {thy_ref = merge_thys2 th1 th2,
  1006             tags = [],
  1007             maxidx = Int.max (max1, max2),
  1008             shyps = Sorts.union shyps1 shyps2,
  1009             hyps = union_hyps hyps1 hyps2,
  1010             tpairs = union_tpairs tpairs1 tpairs2,
  1011             prop = B})
  1012         else err "not equal"
  1013      | _ =>  err"major premise"
  1014   end;
  1015 
  1016 
  1017 
  1018 (**** Derived rules ****)
  1019 
  1020 (*Smash unifies the list of term pairs leaving no flex-flex pairs.
  1021   Instantiates the theorem and deletes trivial tpairs.  Resulting
  1022   sequence may contain multiple elements if the tpairs are not all
  1023   flex-flex.*)
  1024 fun flexflex_rule (th as Thm (der, {thy_ref, maxidx, shyps, hyps, tpairs, prop, ...})) =
  1025   let val thy = Theory.deref thy_ref in
  1026     Unify.smash_unifiers thy tpairs (Envir.empty maxidx)
  1027     |> Seq.map (fn env =>
  1028         if Envir.is_empty env then th
  1029         else
  1030           let
  1031             val tpairs' = tpairs |> map (pairself (Envir.norm_term env))
  1032               (*remove trivial tpairs, of the form t==t*)
  1033               |> filter_out (op aconv);
  1034             val der' = deriv_rule1 (Proofterm.norm_proof' env) der;
  1035             val prop' = Envir.norm_term env prop;
  1036             val maxidx = maxidx_tpairs tpairs' (maxidx_of_term prop');
  1037             val shyps = Envir.insert_sorts env shyps;
  1038           in
  1039             Thm (der', {thy_ref = Theory.check_thy thy, tags = [], maxidx = maxidx,
  1040               shyps = shyps, hyps = hyps, tpairs = tpairs', prop = prop'})
  1041           end)
  1042   end;
  1043 
  1044 
  1045 (*Generalization of fixed variables
  1046            A
  1047   --------------------
  1048   A[?'a/'a, ?x/x, ...]
  1049 *)
  1050 
  1051 fun generalize ([], []) _ th = th
  1052   | generalize (tfrees, frees) idx th =
  1053       let
  1054         val Thm (der, {thy_ref, maxidx, shyps, hyps, tpairs, prop, ...}) = th;
  1055         val _ = idx <= maxidx andalso raise THM ("generalize: bad index", idx, [th]);
  1056 
  1057         val bad_type =
  1058           if null tfrees then K false
  1059           else Term.exists_subtype (fn TFree (a, _) => member (op =) tfrees a | _ => false);
  1060         fun bad_term (Free (x, T)) = bad_type T orelse member (op =) frees x
  1061           | bad_term (Var (_, T)) = bad_type T
  1062           | bad_term (Const (_, T)) = bad_type T
  1063           | bad_term (Abs (_, T, t)) = bad_type T orelse bad_term t
  1064           | bad_term (t $ u) = bad_term t orelse bad_term u
  1065           | bad_term (Bound _) = false;
  1066         val _ = exists bad_term hyps andalso
  1067           raise THM ("generalize: variable free in assumptions", 0, [th]);
  1068 
  1069         val gen = Term_Subst.generalize (tfrees, frees) idx;
  1070         val prop' = gen prop;
  1071         val tpairs' = map (pairself gen) tpairs;
  1072         val maxidx' = maxidx_tpairs tpairs' (maxidx_of_term prop');
  1073       in
  1074         Thm (deriv_rule1 (Proofterm.generalize (tfrees, frees) idx) der,
  1075          {thy_ref = thy_ref,
  1076           tags = [],
  1077           maxidx = maxidx',
  1078           shyps = shyps,
  1079           hyps = hyps,
  1080           tpairs = tpairs',
  1081           prop = prop'})
  1082       end;
  1083 
  1084 
  1085 (*Instantiation of schematic variables
  1086            A
  1087   --------------------
  1088   A[t1/v1, ..., tn/vn]
  1089 *)
  1090 
  1091 local
  1092 
  1093 fun pretty_typing thy t T = Pretty.block
  1094   [Syntax.pretty_term_global thy t, Pretty.str " ::", Pretty.brk 1, Syntax.pretty_typ_global thy T];
  1095 
  1096 fun add_inst (ct, cu) (thy_ref, sorts) =
  1097   let
  1098     val Cterm {t = t, T = T, ...} = ct;
  1099     val Cterm {t = u, T = U, sorts = sorts_u, maxidx = maxidx_u, ...} = cu;
  1100     val thy_ref' = Theory.merge_refs (thy_ref, merge_thys0 ct cu);
  1101     val sorts' = Sorts.union sorts_u sorts;
  1102   in
  1103     (case t of Var v =>
  1104       if T = U then ((v, (u, maxidx_u)), (thy_ref', sorts'))
  1105       else raise TYPE (Pretty.string_of (Pretty.block
  1106        [Pretty.str "instantiate: type conflict",
  1107         Pretty.fbrk, pretty_typing (Theory.deref thy_ref') t T,
  1108         Pretty.fbrk, pretty_typing (Theory.deref thy_ref') u U]), [T, U], [t, u])
  1109     | _ => raise TYPE (Pretty.string_of (Pretty.block
  1110        [Pretty.str "instantiate: not a variable",
  1111         Pretty.fbrk, Syntax.pretty_term_global (Theory.deref thy_ref') t]), [], [t]))
  1112   end;
  1113 
  1114 fun add_instT (cT, cU) (thy_ref, sorts) =
  1115   let
  1116     val Ctyp {T, thy_ref = thy_ref1, ...} = cT
  1117     and Ctyp {T = U, thy_ref = thy_ref2, sorts = sorts_U, maxidx = maxidx_U, ...} = cU;
  1118     val thy' = Theory.deref (Theory.merge_refs (thy_ref, Theory.merge_refs (thy_ref1, thy_ref2)));
  1119     val sorts' = Sorts.union sorts_U sorts;
  1120   in
  1121     (case T of TVar (v as (_, S)) =>
  1122       if Sign.of_sort thy' (U, S) then ((v, (U, maxidx_U)), (Theory.check_thy thy', sorts'))
  1123       else raise TYPE ("Type not of sort " ^ Syntax.string_of_sort_global thy' S, [U], [])
  1124     | _ => raise TYPE (Pretty.string_of (Pretty.block
  1125         [Pretty.str "instantiate: not a type variable",
  1126          Pretty.fbrk, Syntax.pretty_typ_global thy' T]), [T], []))
  1127   end;
  1128 
  1129 in
  1130 
  1131 (*Left-to-right replacements: ctpairs = [..., (vi, ti), ...].
  1132   Instantiates distinct Vars by terms of same type.
  1133   Does NOT normalize the resulting theorem!*)
  1134 fun instantiate ([], []) th = th
  1135   | instantiate (instT, inst) th =
  1136       let
  1137         val Thm (der, {thy_ref, hyps, shyps, tpairs, prop, ...}) = th;
  1138         val (inst', (instT', (thy_ref', shyps'))) =
  1139           (thy_ref, shyps) |> fold_map add_inst inst ||> fold_map add_instT instT;
  1140         val subst = Term_Subst.instantiate_maxidx (instT', inst');
  1141         val (prop', maxidx1) = subst prop ~1;
  1142         val (tpairs', maxidx') =
  1143           fold_map (fn (t, u) => fn i => subst t i ||>> subst u) tpairs maxidx1;
  1144       in
  1145         Thm (deriv_rule1
  1146           (fn d => Proofterm.instantiate (map (apsnd #1) instT', map (apsnd #1) inst') d) der,
  1147          {thy_ref = thy_ref',
  1148           tags = [],
  1149           maxidx = maxidx',
  1150           shyps = shyps',
  1151           hyps = hyps,
  1152           tpairs = tpairs',
  1153           prop = prop'})
  1154       end
  1155       handle TYPE (msg, _, _) => raise THM (msg, 0, [th]);
  1156 
  1157 fun instantiate_cterm ([], []) ct = ct
  1158   | instantiate_cterm (instT, inst) ct =
  1159       let
  1160         val Cterm {thy_ref, t, T, sorts, ...} = ct;
  1161         val (inst', (instT', (thy_ref', sorts'))) =
  1162           (thy_ref, sorts) |> fold_map add_inst inst ||> fold_map add_instT instT;
  1163         val subst = Term_Subst.instantiate_maxidx (instT', inst');
  1164         val substT = Term_Subst.instantiateT_maxidx instT';
  1165         val (t', maxidx1) = subst t ~1;
  1166         val (T', maxidx') = substT T maxidx1;
  1167       in Cterm {thy_ref = thy_ref', t = t', T = T', sorts = sorts', maxidx = maxidx'} end
  1168       handle TYPE (msg, _, _) => raise CTERM (msg, [ct]);
  1169 
  1170 end;
  1171 
  1172 
  1173 (*The trivial implication A ==> A, justified by assume and forall rules.
  1174   A can contain Vars, not so for assume!*)
  1175 fun trivial (Cterm {thy_ref, t =A, T, maxidx, sorts}) =
  1176   if T <> propT then
  1177     raise THM ("trivial: the term must have type prop", 0, [])
  1178   else
  1179     Thm (deriv_rule0 (Proofterm.AbsP ("H", NONE, Proofterm.PBound 0)),
  1180      {thy_ref = thy_ref,
  1181       tags = [],
  1182       maxidx = maxidx,
  1183       shyps = sorts,
  1184       hyps = [],
  1185       tpairs = [],
  1186       prop = Logic.mk_implies (A, A)});
  1187 
  1188 (*Axiom-scheme reflecting signature contents
  1189         T :: c
  1190   -------------------
  1191   OFCLASS(T, c_class)
  1192 *)
  1193 fun of_class (cT, raw_c) =
  1194   let
  1195     val Ctyp {thy_ref, T, ...} = cT;
  1196     val thy = Theory.deref thy_ref;
  1197     val c = Sign.certify_class thy raw_c;
  1198     val Cterm {t = prop, maxidx, sorts, ...} = cterm_of thy (Logic.mk_of_class (T, c));
  1199   in
  1200     if Sign.of_sort thy (T, [c]) then
  1201       Thm (deriv_rule0 (Proofterm.OfClass (T, c)),
  1202        {thy_ref = Theory.check_thy thy,
  1203         tags = [],
  1204         maxidx = maxidx,
  1205         shyps = sorts,
  1206         hyps = [],
  1207         tpairs = [],
  1208         prop = prop})
  1209     else raise THM ("of_class: type not of class " ^ Syntax.string_of_sort_global thy [c], 0, [])
  1210   end;
  1211 
  1212 (*Remove extra sorts that are witnessed by type signature information*)
  1213 fun strip_shyps (thm as Thm (_, {shyps = [], ...})) = thm
  1214   | strip_shyps (thm as Thm (der, {thy_ref, tags, maxidx, shyps, hyps, tpairs, prop})) =
  1215       let
  1216         val thy = Theory.deref thy_ref;
  1217         val algebra = Sign.classes_of thy;
  1218 
  1219         val present = (fold_terms o fold_types o fold_atyps_sorts) (insert (eq_fst op =)) thm [];
  1220         val extra = fold (Sorts.remove_sort o #2) present shyps;
  1221         val witnessed = Sign.witness_sorts thy present extra;
  1222         val extra' = fold (Sorts.remove_sort o #2) witnessed extra
  1223           |> Sorts.minimal_sorts algebra;
  1224         val shyps' = fold (Sorts.insert_sort o #2) present extra';
  1225       in
  1226         Thm (deriv_rule_unconditional
  1227           (Proofterm.strip_shyps_proof algebra present witnessed extra') der,
  1228          {thy_ref = Theory.check_thy thy, tags = tags, maxidx = maxidx,
  1229           shyps = shyps', hyps = hyps, tpairs = tpairs, prop = prop})
  1230       end;
  1231 
  1232 (*Internalize sort constraints of type variables*)
  1233 fun unconstrainT (thm as Thm (der, args)) =
  1234   let
  1235     val Deriv {promises, body} = der;
  1236     val {thy_ref, shyps, hyps, tpairs, prop, ...} = args;
  1237 
  1238     fun err msg = raise THM ("unconstrainT: " ^ msg, 0, [thm]);
  1239     val _ = null hyps orelse err "illegal hyps";
  1240     val _ = null tpairs orelse err "unsolved flex-flex constraints";
  1241     val tfrees = rev (Term.add_tfree_names prop []);
  1242     val _ = null tfrees orelse err ("illegal free type variables " ^ commas_quote tfrees);
  1243 
  1244     val ps = map (apsnd (Future.map fulfill_body)) promises;
  1245     val thy = Theory.deref thy_ref;
  1246     val (pthm as (_, (_, prop', _)), proof) =
  1247       Proofterm.unconstrain_thm_proof thy shyps prop ps body;
  1248     val der' = make_deriv [] [] [pthm] proof;
  1249     val _ = Theory.check_thy thy;
  1250   in
  1251     Thm (der',
  1252      {thy_ref = thy_ref,
  1253       tags = [],
  1254       maxidx = maxidx_of_term prop',
  1255       shyps = [[]],  (*potentially redundant*)
  1256       hyps = [],
  1257       tpairs = [],
  1258       prop = prop'})
  1259   end;
  1260 
  1261 (* Replace all TFrees not fixed or in the hyps by new TVars *)
  1262 fun varifyT_global' fixed (Thm (der, {thy_ref, maxidx, shyps, hyps, tpairs, prop, ...})) =
  1263   let
  1264     val tfrees = fold Term.add_tfrees hyps fixed;
  1265     val prop1 = attach_tpairs tpairs prop;
  1266     val (al, prop2) = Type.varify_global tfrees prop1;
  1267     val (ts, prop3) = Logic.strip_prems (length tpairs, [], prop2);
  1268   in
  1269     (al, Thm (deriv_rule1 (Proofterm.varify_proof prop tfrees) der,
  1270      {thy_ref = thy_ref,
  1271       tags = [],
  1272       maxidx = Int.max (0, maxidx),
  1273       shyps = shyps,
  1274       hyps = hyps,
  1275       tpairs = rev (map Logic.dest_equals ts),
  1276       prop = prop3}))
  1277   end;
  1278 
  1279 val varifyT_global = #2 o varifyT_global' [];
  1280 
  1281 (* Replace all TVars by TFrees that are often new *)
  1282 fun legacy_freezeT (Thm (der, {thy_ref, shyps, hyps, tpairs, prop, ...})) =
  1283   let
  1284     val prop1 = attach_tpairs tpairs prop;
  1285     val prop2 = Type.legacy_freeze prop1;
  1286     val (ts, prop3) = Logic.strip_prems (length tpairs, [], prop2);
  1287   in
  1288     Thm (deriv_rule1 (Proofterm.legacy_freezeT prop1) der,
  1289      {thy_ref = thy_ref,
  1290       tags = [],
  1291       maxidx = maxidx_of_term prop2,
  1292       shyps = shyps,
  1293       hyps = hyps,
  1294       tpairs = rev (map Logic.dest_equals ts),
  1295       prop = prop3})
  1296   end;
  1297 
  1298 
  1299 (*** Inference rules for tactics ***)
  1300 
  1301 (*Destruct proof state into constraints, other goals, goal(i), rest *)
  1302 fun dest_state (state as Thm (_, {prop,tpairs,...}), i) =
  1303   (case  Logic.strip_prems(i, [], prop) of
  1304       (B::rBs, C) => (tpairs, rev rBs, B, C)
  1305     | _ => raise THM("dest_state", i, [state]))
  1306   handle TERM _ => raise THM("dest_state", i, [state]);
  1307 
  1308 (*Prepare orule for resolution by lifting it over the parameters and
  1309 assumptions of goal.*)
  1310 fun lift_rule goal orule =
  1311   let
  1312     val Cterm {t = gprop, T, maxidx = gmax, sorts, ...} = goal;
  1313     val inc = gmax + 1;
  1314     val lift_abs = Logic.lift_abs inc gprop;
  1315     val lift_all = Logic.lift_all inc gprop;
  1316     val Thm (der, {maxidx, shyps, hyps, tpairs, prop, ...}) = orule;
  1317     val (As, B) = Logic.strip_horn prop;
  1318   in
  1319     if T <> propT then raise THM ("lift_rule: the term must have type prop", 0, [])
  1320     else
  1321       Thm (deriv_rule1 (Proofterm.lift_proof gprop inc prop) der,
  1322        {thy_ref = merge_thys1 goal orule,
  1323         tags = [],
  1324         maxidx = maxidx + inc,
  1325         shyps = Sorts.union shyps sorts,  (*sic!*)
  1326         hyps = hyps,
  1327         tpairs = map (pairself lift_abs) tpairs,
  1328         prop = Logic.list_implies (map lift_all As, lift_all B)})
  1329   end;
  1330 
  1331 fun incr_indexes i (thm as Thm (der, {thy_ref, maxidx, shyps, hyps, tpairs, prop, ...})) =
  1332   if i < 0 then raise THM ("negative increment", 0, [thm])
  1333   else if i = 0 then thm
  1334   else
  1335     Thm (deriv_rule1 (Proofterm.incr_indexes i) der,
  1336      {thy_ref = thy_ref,
  1337       tags = [],
  1338       maxidx = maxidx + i,
  1339       shyps = shyps,
  1340       hyps = hyps,
  1341       tpairs = map (pairself (Logic.incr_indexes ([], i))) tpairs,
  1342       prop = Logic.incr_indexes ([], i) prop});
  1343 
  1344 (*Solve subgoal Bi of proof state B1...Bn/C by assumption. *)
  1345 fun assumption i state =
  1346   let
  1347     val Thm (der, {thy_ref, maxidx, shyps, hyps, ...}) = state;
  1348     val thy = Theory.deref thy_ref;
  1349     val (tpairs, Bs, Bi, C) = dest_state (state, i);
  1350     fun newth n (env, tpairs) =
  1351       Thm (deriv_rule1
  1352           ((if Envir.is_empty env then I else (Proofterm.norm_proof' env)) o
  1353             Proofterm.assumption_proof Bs Bi n) der,
  1354        {tags = [],
  1355         maxidx = Envir.maxidx_of env,
  1356         shyps = Envir.insert_sorts env shyps,
  1357         hyps = hyps,
  1358         tpairs =
  1359           if Envir.is_empty env then tpairs
  1360           else map (pairself (Envir.norm_term env)) tpairs,
  1361         prop =
  1362           if Envir.is_empty env then (*avoid wasted normalizations*)
  1363             Logic.list_implies (Bs, C)
  1364           else (*normalize the new rule fully*)
  1365             Envir.norm_term env (Logic.list_implies (Bs, C)),
  1366         thy_ref = Theory.check_thy thy});
  1367 
  1368     val (close, asms, concl) = Logic.assum_problems (~1, Bi);
  1369     val concl' = close concl;
  1370     fun addprfs [] _ = Seq.empty
  1371       | addprfs (asm :: rest) n = Seq.make (fn () => Seq.pull
  1372           (Seq.mapp (newth n)
  1373             (if Term.could_unify (asm, concl) then
  1374               (Unify.unifiers (thy, Envir.empty maxidx, (close asm, concl') :: tpairs))
  1375              else Seq.empty)
  1376             (addprfs rest (n + 1))))
  1377   in addprfs asms 1 end;
  1378 
  1379 (*Solve subgoal Bi of proof state B1...Bn/C by assumption.
  1380   Checks if Bi's conclusion is alpha-convertible to one of its assumptions*)
  1381 fun eq_assumption i state =
  1382   let
  1383     val Thm (der, {thy_ref, maxidx, shyps, hyps, ...}) = state;
  1384     val (tpairs, Bs, Bi, C) = dest_state (state, i);
  1385     val (_, asms, concl) = Logic.assum_problems (~1, Bi);
  1386   in
  1387     (case find_index (fn asm => Pattern.aeconv (asm, concl)) asms of
  1388       ~1 => raise THM ("eq_assumption", 0, [state])
  1389     | n =>
  1390         Thm (deriv_rule1 (Proofterm.assumption_proof Bs Bi (n + 1)) der,
  1391          {thy_ref = thy_ref,
  1392           tags = [],
  1393           maxidx = maxidx,
  1394           shyps = shyps,
  1395           hyps = hyps,
  1396           tpairs = tpairs,
  1397           prop = Logic.list_implies (Bs, C)}))
  1398   end;
  1399 
  1400 
  1401 (*For rotate_tac: fast rotation of assumptions of subgoal i*)
  1402 fun rotate_rule k i state =
  1403   let
  1404     val Thm (der, {thy_ref, maxidx, shyps, hyps, ...}) = state;
  1405     val (tpairs, Bs, Bi, C) = dest_state (state, i);
  1406     val params = Term.strip_all_vars Bi;
  1407     val rest = Term.strip_all_body Bi;
  1408     val asms = Logic.strip_imp_prems rest
  1409     val concl = Logic.strip_imp_concl rest;
  1410     val n = length asms;
  1411     val m = if k < 0 then n + k else k;
  1412     val Bi' =
  1413       if 0 = m orelse m = n then Bi
  1414       else if 0 < m andalso m < n then
  1415         let val (ps, qs) = chop m asms
  1416         in Logic.list_all (params, Logic.list_implies (qs @ ps, concl)) end
  1417       else raise THM ("rotate_rule", k, [state]);
  1418   in
  1419     Thm (deriv_rule1 (Proofterm.rotate_proof Bs Bi m) der,
  1420      {thy_ref = thy_ref,
  1421       tags = [],
  1422       maxidx = maxidx,
  1423       shyps = shyps,
  1424       hyps = hyps,
  1425       tpairs = tpairs,
  1426       prop = Logic.list_implies (Bs @ [Bi'], C)})
  1427   end;
  1428 
  1429 
  1430 (*Rotates a rule's premises to the left by k, leaving the first j premises
  1431   unchanged.  Does nothing if k=0 or if k equals n-j, where n is the
  1432   number of premises.  Useful with etac and underlies defer_tac*)
  1433 fun permute_prems j k rl =
  1434   let
  1435     val Thm (der, {thy_ref, maxidx, shyps, hyps, tpairs, prop, ...}) = rl;
  1436     val prems = Logic.strip_imp_prems prop
  1437     and concl = Logic.strip_imp_concl prop;
  1438     val moved_prems = List.drop (prems, j)
  1439     and fixed_prems = List.take (prems, j)
  1440       handle General.Subscript => raise THM ("permute_prems: j", j, [rl]);
  1441     val n_j = length moved_prems;
  1442     val m = if k < 0 then n_j + k else k;
  1443     val prop' =
  1444       if 0 = m orelse m = n_j then prop
  1445       else if 0 < m andalso m < n_j then
  1446         let val (ps, qs) = chop m moved_prems
  1447         in Logic.list_implies (fixed_prems @ qs @ ps, concl) end
  1448       else raise THM ("permute_prems: k", k, [rl]);
  1449   in
  1450     Thm (deriv_rule1 (Proofterm.permute_prems_proof prems j m) der,
  1451      {thy_ref = thy_ref,
  1452       tags = [],
  1453       maxidx = maxidx,
  1454       shyps = shyps,
  1455       hyps = hyps,
  1456       tpairs = tpairs,
  1457       prop = prop'})
  1458   end;
  1459 
  1460 
  1461 (** User renaming of parameters in a subgoal **)
  1462 
  1463 (*Calls error rather than raising an exception because it is intended
  1464   for top-level use -- exception handling would not make sense here.
  1465   The names in cs, if distinct, are used for the innermost parameters;
  1466   preceding parameters may be renamed to make all params distinct.*)
  1467 fun rename_params_rule (cs, i) state =
  1468   let
  1469     val Thm (der, {thy_ref, tags, maxidx, shyps, hyps, ...}) = state;
  1470     val (tpairs, Bs, Bi, C) = dest_state (state, i);
  1471     val iparams = map #1 (Logic.strip_params Bi);
  1472     val short = length iparams - length cs;
  1473     val newnames =
  1474       if short < 0 then error "More names than abstractions!"
  1475       else Name.variant_list cs (take short iparams) @ cs;
  1476     val freenames = Term.fold_aterms (fn Free (x, _) => insert (op =) x | _ => I) Bi [];
  1477     val newBi = Logic.list_rename_params newnames Bi;
  1478   in
  1479     (case duplicates (op =) cs of
  1480       a :: _ => (warning ("Can't rename.  Bound variables not distinct: " ^ a); state)
  1481     | [] =>
  1482       (case inter (op =) cs freenames of
  1483         a :: _ => (warning ("Can't rename.  Bound/Free variable clash: " ^ a); state)
  1484       | [] =>
  1485         Thm (der,
  1486          {thy_ref = thy_ref,
  1487           tags = tags,
  1488           maxidx = maxidx,
  1489           shyps = shyps,
  1490           hyps = hyps,
  1491           tpairs = tpairs,
  1492           prop = Logic.list_implies (Bs @ [newBi], C)})))
  1493   end;
  1494 
  1495 
  1496 (*** Preservation of bound variable names ***)
  1497 
  1498 fun rename_boundvars pat obj (thm as Thm (der, {thy_ref, tags, maxidx, shyps, hyps, tpairs, prop})) =
  1499   (case Term.rename_abs pat obj prop of
  1500     NONE => thm
  1501   | SOME prop' => Thm (der,
  1502       {thy_ref = thy_ref,
  1503        tags = tags,
  1504        maxidx = maxidx,
  1505        hyps = hyps,
  1506        shyps = shyps,
  1507        tpairs = tpairs,
  1508        prop = prop'}));
  1509 
  1510 
  1511 (* strip_apply f B A strips off all assumptions/parameters from A
  1512    introduced by lifting over B, and applies f to remaining part of A*)
  1513 fun strip_apply f =
  1514   let fun strip (Const ("==>", _) $ _  $ B1)
  1515                 (Const ("==>", _) $ A2 $ B2) = Logic.mk_implies (A2, strip B1 B2)
  1516         | strip ((c as Const ("all", _)) $ Abs (_, _, t1))
  1517                 (      Const ("all", _)  $ Abs (a, T, t2)) = c $ Abs (a, T, strip t1 t2)
  1518         | strip _ A = f A
  1519   in strip end;
  1520 
  1521 fun strip_lifted (Const ("==>", _) $ _ $ B1)
  1522                  (Const ("==>", _) $ _ $ B2) = strip_lifted B1 B2
  1523   | strip_lifted (Const ("all", _) $ Abs (_, _, t1))
  1524                  (Const ("all", _) $ Abs (_, _, t2)) = strip_lifted t1 t2
  1525   | strip_lifted _ A = A;
  1526 
  1527 (*Use the alist to rename all bound variables and some unknowns in a term
  1528   dpairs = current disagreement pairs;  tpairs = permanent ones (flexflex);
  1529   Preserves unknowns in tpairs and on lhs of dpairs. *)
  1530 fun rename_bvs [] _ _ _ _ = K I
  1531   | rename_bvs al dpairs tpairs B As =
  1532       let
  1533         val add_var = fold_aterms (fn Var ((x, _), _) => insert (op =) x | _ => I);
  1534         val vids = []
  1535           |> fold (add_var o fst) dpairs
  1536           |> fold (add_var o fst) tpairs
  1537           |> fold (add_var o snd) tpairs;
  1538         val vids' = fold (add_var o strip_lifted B) As [];
  1539         (*unknowns appearing elsewhere be preserved!*)
  1540         val al' = distinct ((op =) o pairself fst)
  1541           (filter_out (fn (x, y) =>
  1542              not (member (op =) vids' x) orelse
  1543              member (op =) vids x orelse member (op =) vids y) al);
  1544         val unchanged = filter_out (AList.defined (op =) al') vids';
  1545         fun del_clashing clash xs _ [] qs =
  1546               if clash then del_clashing false xs xs qs [] else qs
  1547           | del_clashing clash xs ys ((p as (x, y)) :: ps) qs =
  1548               if member (op =) ys y
  1549               then del_clashing true (x :: xs) (x :: ys) ps qs
  1550               else del_clashing clash xs (y :: ys) ps (p :: qs);
  1551         val al'' = del_clashing false unchanged unchanged al' [];
  1552         fun rename (t as Var ((x, i), T)) =
  1553               (case AList.lookup (op =) al'' x of
  1554                  SOME y => Var ((y, i), T)
  1555                | NONE => t)
  1556           | rename (Abs (x, T, t)) =
  1557               Abs (the_default x (AList.lookup (op =) al x), T, rename t)
  1558           | rename (f $ t) = rename f $ rename t
  1559           | rename t = t;
  1560         fun strip_ren f Ai = f rename B Ai
  1561       in strip_ren end;
  1562 
  1563 (*Function to rename bounds/unknowns in the argument, lifted over B*)
  1564 fun rename_bvars dpairs =
  1565   rename_bvs (fold_rev Term.match_bvars dpairs []) dpairs;
  1566 
  1567 
  1568 (*** RESOLUTION ***)
  1569 
  1570 (** Lifting optimizations **)
  1571 
  1572 (*strip off pairs of assumptions/parameters in parallel -- they are
  1573   identical because of lifting*)
  1574 fun strip_assums2 (Const("==>", _) $ _ $ B1,
  1575                    Const("==>", _) $ _ $ B2) = strip_assums2 (B1,B2)
  1576   | strip_assums2 (Const("all",_)$Abs(a,T,t1),
  1577                    Const("all",_)$Abs(_,_,t2)) =
  1578       let val (B1,B2) = strip_assums2 (t1,t2)
  1579       in  (Abs(a,T,B1), Abs(a,T,B2))  end
  1580   | strip_assums2 BB = BB;
  1581 
  1582 
  1583 (*Faster normalization: skip assumptions that were lifted over*)
  1584 fun norm_term_skip env 0 t = Envir.norm_term env t
  1585   | norm_term_skip env n (Const ("all", _) $ Abs (a, T, t)) =
  1586       let
  1587         val T' = Envir.subst_type (Envir.type_env env) T
  1588         (*Must instantiate types of parameters because they are flattened;
  1589           this could be a NEW parameter*)
  1590       in Logic.all_const T' $ Abs (a, T', norm_term_skip env n t) end
  1591   | norm_term_skip env n (Const ("==>", _) $ A $ B) =
  1592       Logic.mk_implies (A, norm_term_skip env (n - 1) B)
  1593   | norm_term_skip _ _ _ = error "norm_term_skip: too few assumptions??";
  1594 
  1595 
  1596 (*Composition of object rule r=(A1...Am/B) with proof state s=(B1...Bn/C)
  1597   Unifies B with Bi, replacing subgoal i    (1 <= i <= n)
  1598   If match then forbid instantiations in proof state
  1599   If lifted then shorten the dpair using strip_assums2.
  1600   If eres_flg then simultaneously proves A1 by assumption.
  1601   nsubgoal is the number of new subgoals (written m above).
  1602   Curried so that resolution calls dest_state only once.
  1603 *)
  1604 local exception COMPOSE
  1605 in
  1606 fun bicompose_aux flatten match (state, (stpairs, Bs, Bi, C), lifted)
  1607                         (eres_flg, orule, nsubgoal) =
  1608  let val Thm (sder, {maxidx=smax, shyps=sshyps, hyps=shyps, ...}) = state
  1609      and Thm (rder, {maxidx=rmax, shyps=rshyps, hyps=rhyps,
  1610              tpairs=rtpairs, prop=rprop,...}) = orule
  1611          (*How many hyps to skip over during normalization*)
  1612      and nlift = Logic.count_prems (strip_all_body Bi) + (if eres_flg then ~1 else 0)
  1613      val thy = Theory.deref (merge_thys2 state orule);
  1614      (** Add new theorem with prop = '[| Bs; As |] ==> C' to thq **)
  1615      fun addth A (As, oldAs, rder', n) ((env, tpairs), thq) =
  1616        let val normt = Envir.norm_term env;
  1617            (*perform minimal copying here by examining env*)
  1618            val (ntpairs, normp) =
  1619              if Envir.is_empty env then (tpairs, (Bs @ As, C))
  1620              else
  1621              let val ntps = map (pairself normt) tpairs
  1622              in if Envir.above env smax then
  1623                   (*no assignments in state; normalize the rule only*)
  1624                   if lifted
  1625                   then (ntps, (Bs @ map (norm_term_skip env nlift) As, C))
  1626                   else (ntps, (Bs @ map normt As, C))
  1627                 else if match then raise COMPOSE
  1628                 else (*normalize the new rule fully*)
  1629                   (ntps, (map normt (Bs @ As), normt C))
  1630              end
  1631            val th =
  1632              Thm (deriv_rule2
  1633                    ((if Envir.is_empty env then I
  1634                      else if Envir.above env smax then
  1635                        (fn f => fn der => f (Proofterm.norm_proof' env der))
  1636                      else
  1637                        curry op oo (Proofterm.norm_proof' env))
  1638                     (Proofterm.bicompose_proof flatten Bs oldAs As A n (nlift+1))) rder' sder,
  1639                 {tags = [],
  1640                  maxidx = Envir.maxidx_of env,
  1641                  shyps = Envir.insert_sorts env (Sorts.union rshyps sshyps),
  1642                  hyps = union_hyps rhyps shyps,
  1643                  tpairs = ntpairs,
  1644                  prop = Logic.list_implies normp,
  1645                  thy_ref = Theory.check_thy thy})
  1646         in  Seq.cons th thq  end  handle COMPOSE => thq;
  1647      val (rAs,B) = Logic.strip_prems(nsubgoal, [], rprop)
  1648        handle TERM _ => raise THM("bicompose: rule", 0, [orule,state]);
  1649      (*Modify assumptions, deleting n-th if n>0 for e-resolution*)
  1650      fun newAs(As0, n, dpairs, tpairs) =
  1651        let val (As1, rder') =
  1652          if not lifted then (As0, rder)
  1653          else
  1654            let val rename = rename_bvars dpairs tpairs B As0
  1655            in (map (rename strip_apply) As0,
  1656              deriv_rule1 (Proofterm.map_proof_terms (rename K) I) rder)
  1657            end;
  1658        in (map (if flatten then (Logic.flatten_params n) else I) As1, As1, rder', n)
  1659           handle TERM _ =>
  1660           raise THM("bicompose: 1st premise", 0, [orule])
  1661        end;
  1662      val env = Envir.empty(Int.max(rmax,smax));
  1663      val BBi = if lifted then strip_assums2(B,Bi) else (B,Bi);
  1664      val dpairs = BBi :: (rtpairs@stpairs);
  1665 
  1666      (*elim-resolution: try each assumption in turn*)
  1667      fun eres [] = raise THM ("bicompose: no premises", 0, [orule, state])
  1668        | eres (A1 :: As) =
  1669            let
  1670              val A = SOME A1;
  1671              val (close, asms, concl) = Logic.assum_problems (nlift + 1, A1);
  1672              val concl' = close concl;
  1673              fun tryasms [] _ = Seq.empty
  1674                | tryasms (asm :: rest) n =
  1675                    if Term.could_unify (asm, concl) then
  1676                      let val asm' = close asm in
  1677                        (case Seq.pull (Unify.unifiers (thy, env, (asm', concl') :: dpairs)) of
  1678                          NONE => tryasms rest (n + 1)
  1679                        | cell as SOME ((_, tpairs), _) =>
  1680                            Seq.it_right (addth A (newAs (As, n, [BBi, (concl', asm')], tpairs)))
  1681                              (Seq.make (fn () => cell),
  1682                               Seq.make (fn () => Seq.pull (tryasms rest (n + 1)))))
  1683                      end
  1684                    else tryasms rest (n + 1);
  1685            in tryasms asms 1 end;
  1686 
  1687      (*ordinary resolution*)
  1688      fun res () =
  1689        (case Seq.pull (Unify.unifiers (thy, env, dpairs)) of
  1690          NONE => Seq.empty
  1691        | cell as SOME ((_, tpairs), _) =>
  1692            Seq.it_right (addth NONE (newAs (rev rAs, 0, [BBi], tpairs)))
  1693              (Seq.make (fn () => cell), Seq.empty));
  1694  in
  1695    if eres_flg then eres (rev rAs) else res ()
  1696  end;
  1697 end;
  1698 
  1699 fun compose_no_flatten match (orule, nsubgoal) i state =
  1700   bicompose_aux false match (state, dest_state (state, i), false) (false, orule, nsubgoal);
  1701 
  1702 fun bicompose match arg i state =
  1703   bicompose_aux true match (state, dest_state (state,i), false) arg;
  1704 
  1705 (*Quick test whether rule is resolvable with the subgoal with hyps Hs
  1706   and conclusion B.  If eres_flg then checks 1st premise of rule also*)
  1707 fun could_bires (Hs, B, eres_flg, rule) =
  1708     let fun could_reshyp (A1::_) = exists (fn H => Term.could_unify (A1, H)) Hs
  1709           | could_reshyp [] = false;  (*no premise -- illegal*)
  1710     in  Term.could_unify(concl_of rule, B) andalso
  1711         (not eres_flg  orelse  could_reshyp (prems_of rule))
  1712     end;
  1713 
  1714 (*Bi-resolution of a state with a list of (flag,rule) pairs.
  1715   Puts the rule above:  rule/state.  Renames vars in the rules. *)
  1716 fun biresolution match brules i state =
  1717     let val (stpairs, Bs, Bi, C) = dest_state(state,i);
  1718         val lift = lift_rule (cprem_of state i);
  1719         val B = Logic.strip_assums_concl Bi;
  1720         val Hs = Logic.strip_assums_hyp Bi;
  1721         val compose = bicompose_aux true match (state, (stpairs, Bs, Bi, C), true);
  1722         fun res [] = Seq.empty
  1723           | res ((eres_flg, rule)::brules) =
  1724               if !Pattern.trace_unify_fail orelse
  1725                  could_bires (Hs, B, eres_flg, rule)
  1726               then Seq.make (*delay processing remainder till needed*)
  1727                   (fn()=> SOME(compose (eres_flg, lift rule, nprems_of rule),
  1728                                res brules))
  1729               else res brules
  1730     in  Seq.flat (res brules)  end;
  1731 
  1732 
  1733 
  1734 (*** Oracles ***)
  1735 
  1736 (* oracle rule *)
  1737 
  1738 fun invoke_oracle thy_ref1 name oracle arg =
  1739   let val Cterm {thy_ref = thy_ref2, t = prop, T, maxidx, sorts} = oracle arg in
  1740     if T <> propT then
  1741       raise THM ("Oracle's result must have type prop: " ^ name, 0, [])
  1742     else
  1743       let val (ora, prf) = Proofterm.oracle_proof name prop in
  1744         Thm (make_deriv [] [ora] [] prf,
  1745          {thy_ref = Theory.merge_refs (thy_ref1, thy_ref2),
  1746           tags = [],
  1747           maxidx = maxidx,
  1748           shyps = sorts,
  1749           hyps = [],
  1750           tpairs = [],
  1751           prop = prop})
  1752       end
  1753   end;
  1754 
  1755 end;
  1756 end;
  1757 end;
  1758 
  1759 
  1760 (* authentic derivation names *)
  1761 
  1762 structure Oracles = Theory_Data
  1763 (
  1764   type T = unit Name_Space.table;
  1765   val empty : T = Name_Space.empty_table "oracle";
  1766   val extend = I;
  1767   fun merge data : T = Name_Space.merge_tables data;
  1768 );
  1769 
  1770 fun extern_oracles ctxt =
  1771   map #1 (Name_Space.extern_table ctxt (Oracles.get (Proof_Context.theory_of ctxt)));
  1772 
  1773 fun add_oracle (b, oracle) thy =
  1774   let
  1775     val (name, tab') = Name_Space.define (Context.Theory thy) true (b, ()) (Oracles.get thy);
  1776     val thy' = Oracles.put tab' thy;
  1777   in ((name, invoke_oracle (Theory.check_thy thy') name oracle), thy') end;
  1778 
  1779 end;
  1780 
  1781 structure Basic_Thm: BASIC_THM = Thm;
  1782 open Basic_Thm;