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