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