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