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