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