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