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