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