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