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