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