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