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