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