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