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