src/Pure/thm.ML
author wenzelm
Thu Aug 15 16:02:47 2019 +0200 (9 months ago)
changeset 70533 031620901fcd
parent 70517 9a9003b5c0c1
child 70543 33749040b6f8
permissions -rw-r--r--
support for (fully reconstructed) proof terms in Scala;
proper cache_typs;
     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 infix 0 RS RSN;
    11 
    12 signature BASIC_THM =
    13 sig
    14   type ctyp
    15   type cterm
    16   exception CTERM of string * cterm list
    17   type thm
    18   type conv = cterm -> thm
    19   exception THM of string * int * thm list
    20   val RSN: thm * (int * thm) -> thm
    21   val RS: thm * thm -> thm
    22 end;
    23 
    24 signature THM =
    25 sig
    26   include BASIC_THM
    27   (*certified types*)
    28   val typ_of: ctyp -> typ
    29   val global_ctyp_of: theory -> typ -> ctyp
    30   val ctyp_of: Proof.context -> typ -> ctyp
    31   val dest_ctyp: ctyp -> ctyp list
    32   val dest_ctypN: int -> ctyp -> ctyp
    33   val dest_ctyp0: ctyp -> ctyp
    34   val dest_ctyp1: ctyp -> ctyp
    35   val make_ctyp: ctyp -> ctyp list -> ctyp
    36   (*certified terms*)
    37   val term_of: cterm -> term
    38   val typ_of_cterm: cterm -> typ
    39   val ctyp_of_cterm: cterm -> ctyp
    40   val maxidx_of_cterm: cterm -> int
    41   val global_cterm_of: theory -> term -> cterm
    42   val cterm_of: Proof.context -> term -> cterm
    43   val renamed_term: term -> cterm -> cterm
    44   val dest_comb: cterm -> cterm * cterm
    45   val dest_fun: cterm -> cterm
    46   val dest_arg: cterm -> cterm
    47   val dest_fun2: cterm -> cterm
    48   val dest_arg1: cterm -> cterm
    49   val dest_abs: string option -> cterm -> cterm * cterm
    50   val rename_tvar: indexname -> ctyp -> ctyp
    51   val var: indexname * ctyp -> cterm
    52   val apply: cterm -> cterm -> cterm
    53   val lambda_name: string * cterm -> cterm -> cterm
    54   val lambda: cterm -> cterm -> cterm
    55   val adjust_maxidx_cterm: int -> cterm -> cterm
    56   val incr_indexes_cterm: int -> cterm -> cterm
    57   val match: cterm * cterm ->
    58     ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list
    59   val first_order_match: cterm * cterm ->
    60     ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list
    61   (*theorems*)
    62   val fold_terms: (term -> 'a -> 'a) -> thm -> 'a -> 'a
    63   val fold_atomic_ctyps: (ctyp -> 'a -> 'a) -> thm -> 'a -> 'a
    64   val fold_atomic_cterms: (cterm -> 'a -> 'a) -> thm -> 'a -> 'a
    65   val terms_of_tpairs: (term * term) list -> term list
    66   val full_prop_of: thm -> term
    67   val theory_id: thm -> Context.theory_id
    68   val theory_name: thm -> string
    69   val maxidx_of: thm -> int
    70   val maxidx_thm: thm -> int -> int
    71   val shyps_of: thm -> sort Ord_List.T
    72   val hyps_of: thm -> term list
    73   val prop_of: thm -> term
    74   val tpairs_of: thm -> (term * term) list
    75   val concl_of: thm -> term
    76   val prems_of: thm -> term list
    77   val nprems_of: thm -> int
    78   val no_prems: thm -> bool
    79   val major_prem_of: thm -> term
    80   val cprop_of: thm -> cterm
    81   val cprem_of: thm -> int -> cterm
    82   val cconcl_of: thm -> cterm
    83   val cprems_of: thm -> cterm list
    84   val chyps_of: thm -> cterm list
    85   exception CONTEXT of string * ctyp list * cterm list * thm list * Context.generic option
    86   val theory_of_cterm: cterm -> theory
    87   val theory_of_thm: thm -> theory
    88   val trim_context_ctyp: ctyp -> ctyp
    89   val trim_context_cterm: cterm -> cterm
    90   val transfer_ctyp: theory -> ctyp -> ctyp
    91   val transfer_cterm: theory -> cterm -> cterm
    92   val transfer: theory -> thm -> thm
    93   val transfer': Proof.context -> thm -> thm
    94   val transfer'': Context.generic -> thm -> thm
    95   val join_transfer: theory -> thm -> thm
    96   val join_transfer_context: Proof.context * thm -> Proof.context * thm
    97   val renamed_prop: term -> thm -> thm
    98   val weaken: cterm -> thm -> thm
    99   val weaken_sorts: sort list -> cterm -> cterm
   100   val extra_shyps: thm -> sort list
   101   val proof_bodies_of: thm list -> proof_body list
   102   val proof_body_of: thm -> proof_body
   103   val proof_of: thm -> proof
   104   val consolidate: thm list -> unit
   105   val peek_status: thm -> {oracle: bool, unfinished: bool, failed: bool}
   106   val future: thm future -> cterm -> thm
   107   val derivation_closed: thm -> bool
   108   val derivation_name: thm -> string
   109   val name_derivation: string * Position.T -> thm -> thm
   110   val close_derivation: Position.T -> thm -> thm
   111   val trim_context: thm -> thm
   112   val axiom: theory -> string -> thm
   113   val axioms_of: theory -> (string * thm) list
   114   val get_tags: thm -> Properties.T
   115   val map_tags: (Properties.T -> Properties.T) -> thm -> thm
   116   val norm_proof: thm -> thm
   117   val adjust_maxidx_thm: int -> thm -> thm
   118   (*type classes*)
   119   val the_classrel: theory -> class * class -> thm
   120   val the_arity: theory -> string * sort list * class -> thm
   121   val classrel_proof: theory -> class * class -> proof
   122   val arity_proof: theory -> string * sort list * class -> proof
   123   (*oracles*)
   124   val add_oracle: binding * ('a -> cterm) -> theory -> (string * ('a -> thm)) * theory
   125   val extern_oracles: bool -> Proof.context -> (Markup.T * xstring) list
   126   (*inference rules*)
   127   val assume: cterm -> thm
   128   val implies_intr: cterm -> thm -> thm
   129   val implies_elim: thm -> thm -> thm
   130   val forall_intr: cterm -> thm -> thm
   131   val forall_elim: cterm -> thm -> thm
   132   val reflexive: cterm -> thm
   133   val symmetric: thm -> thm
   134   val transitive: thm -> thm -> thm
   135   val beta_conversion: bool -> conv
   136   val eta_conversion: conv
   137   val eta_long_conversion: conv
   138   val abstract_rule: string -> cterm -> thm -> thm
   139   val combination: thm -> thm -> thm
   140   val equal_intr: thm -> thm -> thm
   141   val equal_elim: thm -> thm -> thm
   142   val solve_constraints: thm -> thm
   143   val flexflex_rule: Proof.context option -> thm -> thm Seq.seq
   144   val generalize: string list * string list -> int -> thm -> thm
   145   val generalize_cterm: string list * string list -> int -> cterm -> cterm
   146   val generalize_ctyp: string list -> int -> ctyp -> ctyp
   147   val instantiate: ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list ->
   148     thm -> thm
   149   val instantiate_cterm: ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list ->
   150     cterm -> cterm
   151   val trivial: cterm -> thm
   152   val of_class: ctyp * class -> thm
   153   val strip_shyps: thm -> thm
   154   val unconstrainT: thm -> thm
   155   val varifyT_global': (string * sort) list -> thm -> ((string * sort) * indexname) list * thm
   156   val varifyT_global: thm -> thm
   157   val legacy_freezeT: thm -> thm
   158   val plain_prop_of: thm -> term
   159   val dest_state: thm * int -> (term * term) list * term list * term * term
   160   val lift_rule: cterm -> thm -> thm
   161   val incr_indexes: int -> thm -> thm
   162   val assumption: Proof.context option -> int -> thm -> thm Seq.seq
   163   val eq_assumption: int -> thm -> thm
   164   val rotate_rule: int -> int -> thm -> thm
   165   val permute_prems: int -> int -> thm -> thm
   166   val bicompose: Proof.context option -> {flatten: bool, match: bool, incremented: bool} ->
   167     bool * thm * int -> int -> thm -> thm Seq.seq
   168   val biresolution: Proof.context option -> bool -> (bool * thm) list -> int -> thm -> thm Seq.seq
   169   val thynames_of_arity: theory -> string * class -> string list
   170   val add_classrel: thm -> theory -> theory
   171   val add_arity: thm -> theory -> theory
   172 end;
   173 
   174 structure Thm: THM =
   175 struct
   176 
   177 (*** Certified terms and types ***)
   178 
   179 (** certified types **)
   180 
   181 datatype ctyp = Ctyp of {cert: Context.certificate, T: typ, maxidx: int, sorts: sort Ord_List.T};
   182 
   183 fun typ_of (Ctyp {T, ...}) = T;
   184 
   185 fun global_ctyp_of thy raw_T =
   186   let
   187     val T = Sign.certify_typ thy raw_T;
   188     val maxidx = Term.maxidx_of_typ T;
   189     val sorts = Sorts.insert_typ T [];
   190   in Ctyp {cert = Context.Certificate thy, T = T, maxidx = maxidx, sorts = sorts} end;
   191 
   192 val ctyp_of = global_ctyp_of o Proof_Context.theory_of;
   193 
   194 fun dest_ctyp (Ctyp {cert, T = Type (_, Ts), maxidx, sorts}) =
   195       map (fn T => Ctyp {cert = cert, T = T, maxidx = maxidx, sorts = sorts}) Ts
   196   | dest_ctyp cT = raise TYPE ("dest_ctyp", [typ_of cT], []);
   197 
   198 fun dest_ctypN n (Ctyp {cert, T, maxidx, sorts}) =
   199   let fun err () = raise TYPE ("dest_ctypN", [T], []) in
   200     (case T of
   201       Type (_, Ts) =>
   202         Ctyp {cert = cert, T = nth Ts n handle General.Subscript => err (),
   203           maxidx = maxidx, sorts = sorts}
   204     | _ => err ())
   205   end;
   206 
   207 val dest_ctyp0 = dest_ctypN 0;
   208 val dest_ctyp1 = dest_ctypN 1;
   209 
   210 fun join_certificate_ctyp (Ctyp {cert, ...}) cert0 = Context.join_certificate (cert0, cert);
   211 fun union_sorts_ctyp (Ctyp {sorts, ...}) sorts0 = Sorts.union sorts0 sorts;
   212 fun maxidx_ctyp (Ctyp {maxidx, ...}) maxidx0 = Int.max (maxidx0, maxidx);
   213 
   214 fun make_ctyp (Ctyp {cert, T, maxidx = _, sorts = _}) cargs =
   215   let
   216     val As = map typ_of cargs;
   217     fun err () = raise TYPE ("make_ctyp", T :: As, []);
   218   in
   219     (case T of
   220       Type (a, args) =>
   221         Ctyp {
   222           cert = fold join_certificate_ctyp cargs cert,
   223           maxidx = fold maxidx_ctyp cargs ~1,
   224           sorts = fold union_sorts_ctyp cargs [],
   225           T = if length args = length cargs then Type (a, As) else err ()}
   226     | _ => err ())
   227   end;
   228 
   229 
   230 
   231 (** certified terms **)
   232 
   233 (*certified terms with checked typ, maxidx, and sorts*)
   234 datatype cterm =
   235   Cterm of {cert: Context.certificate, t: term, T: typ, maxidx: int, sorts: sort Ord_List.T};
   236 
   237 exception CTERM of string * cterm list;
   238 
   239 fun term_of (Cterm {t, ...}) = t;
   240 
   241 fun typ_of_cterm (Cterm {T, ...}) = T;
   242 
   243 fun ctyp_of_cterm (Cterm {cert, T, maxidx, sorts, ...}) =
   244   Ctyp {cert = cert, T = T, maxidx = maxidx, sorts = sorts};
   245 
   246 fun maxidx_of_cterm (Cterm {maxidx, ...}) = maxidx;
   247 
   248 fun global_cterm_of thy tm =
   249   let
   250     val (t, T, maxidx) = Sign.certify_term thy tm;
   251     val sorts = Sorts.insert_term t [];
   252   in Cterm {cert = Context.Certificate thy, t = t, T = T, maxidx = maxidx, sorts = sorts} end;
   253 
   254 val cterm_of = global_cterm_of o Proof_Context.theory_of;
   255 
   256 fun join_certificate0 (Cterm {cert = cert1, ...}, Cterm {cert = cert2, ...}) =
   257   Context.join_certificate (cert1, cert2);
   258 
   259 fun renamed_term t' (Cterm {cert, t, T, maxidx, sorts}) =
   260   if t aconv t' then Cterm {cert = cert, t = t', T = T, maxidx = maxidx, sorts = sorts}
   261   else raise TERM ("renamed_term: terms disagree", [t, t']);
   262 
   263 
   264 (* destructors *)
   265 
   266 fun dest_comb (Cterm {t = c $ a, T, cert, maxidx, sorts}) =
   267       let val A = Term.argument_type_of c 0 in
   268         (Cterm {t = c, T = A --> T, cert = cert, maxidx = maxidx, sorts = sorts},
   269          Cterm {t = a, T = A, cert = cert, maxidx = maxidx, sorts = sorts})
   270       end
   271   | dest_comb ct = raise CTERM ("dest_comb", [ct]);
   272 
   273 fun dest_fun (Cterm {t = c $ _, T, cert, maxidx, sorts}) =
   274       let val A = Term.argument_type_of c 0
   275       in Cterm {t = c, T = A --> T, cert = cert, maxidx = maxidx, sorts = sorts} end
   276   | dest_fun ct = raise CTERM ("dest_fun", [ct]);
   277 
   278 fun dest_arg (Cterm {t = c $ a, T = _, cert, maxidx, sorts}) =
   279       let val A = Term.argument_type_of c 0
   280       in Cterm {t = a, T = A, cert = cert, maxidx = maxidx, sorts = sorts} end
   281   | dest_arg ct = raise CTERM ("dest_arg", [ct]);
   282 
   283 
   284 fun dest_fun2 (Cterm {t = c $ _ $ _, T, cert, maxidx, sorts}) =
   285       let
   286         val A = Term.argument_type_of c 0;
   287         val B = Term.argument_type_of c 1;
   288       in Cterm {t = c, T = A --> B --> T, cert = cert, maxidx = maxidx, sorts = sorts} end
   289   | dest_fun2 ct = raise CTERM ("dest_fun2", [ct]);
   290 
   291 fun dest_arg1 (Cterm {t = c $ a $ _, T = _, cert, maxidx, sorts}) =
   292       let val A = Term.argument_type_of c 0
   293       in Cterm {t = a, T = A, cert = cert, maxidx = maxidx, sorts = sorts} end
   294   | dest_arg1 ct = raise CTERM ("dest_arg1", [ct]);
   295 
   296 fun dest_abs a (Cterm {t = Abs (x, T, t), T = Type ("fun", [_, U]), cert, maxidx, sorts}) =
   297       let val (y', t') = Term.dest_abs (the_default x a, T, t) in
   298         (Cterm {t = Free (y', T), T = T, cert = cert, maxidx = maxidx, sorts = sorts},
   299           Cterm {t = t', T = U, cert = cert, maxidx = maxidx, sorts = sorts})
   300       end
   301   | dest_abs _ ct = raise CTERM ("dest_abs", [ct]);
   302 
   303 
   304 (* constructors *)
   305 
   306 fun rename_tvar (a, i) (Ctyp {cert, T, maxidx, sorts}) =
   307   let
   308     val S =
   309       (case T of
   310         TFree (_, S) => S
   311       | TVar (_, S) => S
   312       | _ => raise TYPE ("rename_tvar: no variable", [T], []));
   313     val _ = if i < 0 then raise TYPE ("rename_tvar: bad index", [TVar ((a, i), S)], []) else ();
   314   in Ctyp {cert = cert, T = TVar ((a, i), S), maxidx = Int.max (i, maxidx), sorts = sorts} end;
   315 
   316 fun var ((x, i), Ctyp {cert, T, maxidx, sorts}) =
   317   if i < 0 then raise TERM ("var: bad index", [Var ((x, i), T)])
   318   else Cterm {cert = cert, t = Var ((x, i), T), T = T, maxidx = Int.max (i, maxidx), sorts = sorts};
   319 
   320 fun apply
   321   (cf as Cterm {t = f, T = Type ("fun", [dty, rty]), maxidx = maxidx1, sorts = sorts1, ...})
   322   (cx as Cterm {t = x, T, maxidx = maxidx2, sorts = sorts2, ...}) =
   323     if T = dty then
   324       Cterm {cert = join_certificate0 (cf, cx),
   325         t = f $ x,
   326         T = rty,
   327         maxidx = Int.max (maxidx1, maxidx2),
   328         sorts = Sorts.union sorts1 sorts2}
   329       else raise CTERM ("apply: types don't agree", [cf, cx])
   330   | apply cf cx = raise CTERM ("apply: first arg is not a function", [cf, cx]);
   331 
   332 fun lambda_name
   333   (x, ct1 as Cterm {t = t1, T = T1, maxidx = maxidx1, sorts = sorts1, ...})
   334   (ct2 as Cterm {t = t2, T = T2, maxidx = maxidx2, sorts = sorts2, ...}) =
   335     let val t = Term.lambda_name (x, t1) t2 in
   336       Cterm {cert = join_certificate0 (ct1, ct2),
   337         t = t, T = T1 --> T2,
   338         maxidx = Int.max (maxidx1, maxidx2),
   339         sorts = Sorts.union sorts1 sorts2}
   340     end;
   341 
   342 fun lambda t u = lambda_name ("", t) u;
   343 
   344 
   345 (* indexes *)
   346 
   347 fun adjust_maxidx_cterm i (ct as Cterm {cert, t, T, maxidx, sorts}) =
   348   if maxidx = i then ct
   349   else if maxidx < i then
   350     Cterm {maxidx = i, cert = cert, t = t, T = T, sorts = sorts}
   351   else
   352     Cterm {maxidx = Int.max (maxidx_of_term t, i), cert = cert, t = t, T = T, sorts = sorts};
   353 
   354 fun incr_indexes_cterm i (ct as Cterm {cert, t, T, maxidx, sorts}) =
   355   if i < 0 then raise CTERM ("negative increment", [ct])
   356   else if i = 0 then ct
   357   else Cterm {cert = cert, t = Logic.incr_indexes ([], [], i) t,
   358     T = Logic.incr_tvar i T, maxidx = maxidx + i, sorts = sorts};
   359 
   360 
   361 
   362 (*** Derivations and Theorems ***)
   363 
   364 (* sort constraints *)
   365 
   366 type constraint = {theory: theory, typ: typ, sort: sort};
   367 
   368 local
   369 
   370 val constraint_ord : constraint * constraint -> order =
   371   Context.theory_id_ord o apply2 (Context.theory_id o #theory)
   372   <<< Term_Ord.typ_ord o apply2 #typ
   373   <<< Term_Ord.sort_ord o apply2 #sort;
   374 
   375 val smash_atyps =
   376   map_atyps (fn TVar (_, S) => Term.aT S | TFree (_, S) => Term.aT S | T => T);
   377 
   378 in
   379 
   380 val union_constraints = Ord_List.union constraint_ord;
   381 
   382 fun insert_constraints thy (T, S) =
   383   let
   384     val ignored =
   385       S = [] orelse
   386         (case T of
   387           TFree (_, S') => S = S'
   388         | TVar (_, S') => S = S'
   389         | _ => false);
   390   in
   391     if ignored then I
   392     else Ord_List.insert constraint_ord {theory = thy, typ = smash_atyps T, sort = S}
   393   end;
   394 
   395 fun insert_constraints_env thy env =
   396   let
   397     val tyenv = Envir.type_env env;
   398     fun insert ([], _) = I
   399       | insert (S, T) = insert_constraints thy (Envir.norm_type tyenv T, S);
   400   in tyenv |> Vartab.fold (insert o #2) end;
   401 
   402 end;
   403 
   404 
   405 (* datatype thm *)
   406 
   407 datatype thm = Thm of
   408  deriv *                        (*derivation*)
   409  {cert: Context.certificate,    (*background theory certificate*)
   410   tags: Properties.T,           (*additional annotations/comments*)
   411   maxidx: int,                  (*maximum index of any Var or TVar*)
   412   constraints: constraint Ord_List.T,  (*implicit proof obligations for sort constraints*)
   413   shyps: sort Ord_List.T,       (*sort hypotheses*)
   414   hyps: term Ord_List.T,        (*hypotheses*)
   415   tpairs: (term * term) list,   (*flex-flex pairs*)
   416   prop: term}                   (*conclusion*)
   417 and deriv = Deriv of
   418  {promises: (serial * thm future) Ord_List.T,
   419   body: Proofterm.proof_body};
   420 
   421 type conv = cterm -> thm;
   422 
   423 (*errors involving theorems*)
   424 exception THM of string * int * thm list;
   425 
   426 fun rep_thm (Thm (_, args)) = args;
   427 
   428 fun fold_terms f (Thm (_, {tpairs, prop, hyps, ...})) =
   429   fold (fn (t, u) => f t #> f u) tpairs #> f prop #> fold f hyps;
   430 
   431 fun fold_atomic_ctyps f (th as Thm (_, {cert, maxidx, shyps, ...})) =
   432   let fun ctyp T = Ctyp {cert = cert, T = T, maxidx = maxidx, sorts = shyps}
   433   in (fold_terms o fold_types o fold_atyps) (f o ctyp) th end;
   434 
   435 fun fold_atomic_cterms f (th as Thm (_, {cert, maxidx, shyps, ...})) =
   436   let fun cterm t T = Cterm {cert = cert, t = t, T = T, maxidx = maxidx, sorts = shyps} in
   437     (fold_terms o fold_aterms)
   438       (fn t as Const (_, T) => f (cterm t T)
   439         | t as Free (_, T) => f (cterm t T)
   440         | t as Var (_, T) => f (cterm t T)
   441         | _ => I) th
   442   end;
   443 
   444 
   445 fun terms_of_tpairs tpairs = fold_rev (fn (t, u) => cons t o cons u) tpairs [];
   446 
   447 fun eq_tpairs ((t, u), (t', u')) = t aconv t' andalso u aconv u';
   448 fun union_tpairs ts us = Library.merge eq_tpairs (ts, us);
   449 val maxidx_tpairs = fold (fn (t, u) => Term.maxidx_term t #> Term.maxidx_term u);
   450 
   451 fun attach_tpairs tpairs prop =
   452   Logic.list_implies (map Logic.mk_equals tpairs, prop);
   453 
   454 fun full_prop_of (Thm (_, {tpairs, prop, ...})) = attach_tpairs tpairs prop;
   455 
   456 
   457 val union_hyps = Ord_List.union Term_Ord.fast_term_ord;
   458 val insert_hyps = Ord_List.insert Term_Ord.fast_term_ord;
   459 val remove_hyps = Ord_List.remove Term_Ord.fast_term_ord;
   460 
   461 fun join_certificate1 (Cterm {cert = cert1, ...}, Thm (_, {cert = cert2, ...})) =
   462   Context.join_certificate (cert1, cert2);
   463 
   464 fun join_certificate2 (Thm (_, {cert = cert1, ...}), Thm (_, {cert = cert2, ...})) =
   465   Context.join_certificate (cert1, cert2);
   466 
   467 
   468 (* basic components *)
   469 
   470 val cert_of = #cert o rep_thm;
   471 val theory_id = Context.certificate_theory_id o cert_of;
   472 val theory_name = Context.theory_id_name o theory_id;
   473 
   474 val maxidx_of = #maxidx o rep_thm;
   475 fun maxidx_thm th i = Int.max (maxidx_of th, i);
   476 val constraints_of = #constraints o rep_thm;
   477 val shyps_of = #shyps o rep_thm;
   478 val hyps_of = #hyps o rep_thm;
   479 val prop_of = #prop o rep_thm;
   480 val tpairs_of = #tpairs o rep_thm;
   481 
   482 val concl_of = Logic.strip_imp_concl o prop_of;
   483 val prems_of = Logic.strip_imp_prems o prop_of;
   484 val nprems_of = Logic.count_prems o prop_of;
   485 fun no_prems th = nprems_of th = 0;
   486 
   487 fun major_prem_of th =
   488   (case prems_of th of
   489     prem :: _ => Logic.strip_assums_concl prem
   490   | [] => raise THM ("major_prem_of: rule with no premises", 0, [th]));
   491 
   492 fun cprop_of (Thm (_, {cert, maxidx, shyps, prop, ...})) =
   493   Cterm {cert = cert, maxidx = maxidx, T = propT, t = prop, sorts = shyps};
   494 
   495 fun cprem_of (th as Thm (_, {cert, maxidx, shyps, prop, ...})) i =
   496   Cterm {cert = cert, maxidx = maxidx, T = propT, sorts = shyps,
   497     t = Logic.nth_prem (i, prop) handle TERM _ => raise THM ("cprem_of", i, [th])};
   498 
   499 fun cconcl_of (th as Thm (_, {cert, maxidx, shyps, ...})) =
   500   Cterm {cert = cert, maxidx = maxidx, T = propT, sorts = shyps, t = concl_of th};
   501 
   502 fun cprems_of (th as Thm (_, {cert, maxidx, shyps, ...})) =
   503   map (fn t => Cterm {cert = cert, maxidx = maxidx, T = propT, sorts = shyps, t = t})
   504     (prems_of th);
   505 
   506 fun chyps_of (Thm (_, {cert, shyps, hyps, ...})) =
   507   map (fn t => Cterm {cert = cert, maxidx = ~1, T = propT, sorts = shyps, t = t}) hyps;
   508 
   509 
   510 (* implicit theory context *)
   511 
   512 exception CONTEXT of string * ctyp list * cterm list * thm list * Context.generic option;
   513 
   514 fun theory_of_cterm (ct as Cterm {cert, ...}) =
   515   Context.certificate_theory cert
   516     handle ERROR msg => raise CONTEXT (msg, [], [ct], [], NONE);
   517 
   518 fun theory_of_thm th =
   519   Context.certificate_theory (cert_of th)
   520     handle ERROR msg => raise CONTEXT (msg, [], [], [th], NONE);
   521 
   522 fun trim_context_ctyp cT =
   523   (case cT of
   524     Ctyp {cert = Context.Certificate_Id _, ...} => cT
   525   | Ctyp {cert = Context.Certificate thy, T, maxidx, sorts} =>
   526       Ctyp {cert = Context.Certificate_Id (Context.theory_id thy),
   527         T = T, maxidx = maxidx, sorts = sorts});
   528 
   529 fun trim_context_cterm ct =
   530   (case ct of
   531     Cterm {cert = Context.Certificate_Id _, ...} => ct
   532   | Cterm {cert = Context.Certificate thy, t, T, maxidx, sorts} =>
   533       Cterm {cert = Context.Certificate_Id (Context.theory_id thy),
   534         t = t, T = T, maxidx = maxidx, sorts = sorts});
   535 
   536 fun trim_context_thm th =
   537   (case th of
   538     Thm (_, {constraints = _ :: _, ...}) =>
   539       raise THM ("trim_context: pending sort constraints", 0, [th])
   540   | Thm (_, {cert = Context.Certificate_Id _, ...}) => th
   541   | Thm (der,
   542       {cert = Context.Certificate thy, tags, maxidx, constraints = [], shyps, hyps,
   543         tpairs, prop}) =>
   544       Thm (der,
   545        {cert = Context.Certificate_Id (Context.theory_id thy),
   546         tags = tags, maxidx = maxidx, constraints = [], shyps = shyps, hyps = hyps,
   547         tpairs = tpairs, prop = prop}));
   548 
   549 fun transfer_ctyp thy' cT =
   550   let
   551     val Ctyp {cert, T, maxidx, sorts} = cT;
   552     val _ =
   553       Context.subthy_id (Context.certificate_theory_id cert, Context.theory_id thy') orelse
   554         raise CONTEXT ("Cannot transfer: not a super theory", [cT], [], [],
   555           SOME (Context.Theory thy'));
   556     val cert' = Context.join_certificate (Context.Certificate thy', cert);
   557   in
   558     if Context.eq_certificate (cert, cert') then cT
   559     else Ctyp {cert = cert', T = T, maxidx = maxidx, sorts = sorts}
   560   end;
   561 
   562 fun transfer_cterm thy' ct =
   563   let
   564     val Cterm {cert, t, T, maxidx, sorts} = ct;
   565     val _ =
   566       Context.subthy_id (Context.certificate_theory_id cert, Context.theory_id thy') orelse
   567         raise CONTEXT ("Cannot transfer: not a super theory", [], [ct], [],
   568           SOME (Context.Theory thy'));
   569     val cert' = Context.join_certificate (Context.Certificate thy', cert);
   570   in
   571     if Context.eq_certificate (cert, cert') then ct
   572     else Cterm {cert = cert', t = t, T = T, maxidx = maxidx, sorts = sorts}
   573   end;
   574 
   575 fun transfer thy' th =
   576   let
   577     val Thm (der, {cert, tags, maxidx, constraints, shyps, hyps, tpairs, prop}) = th;
   578     val _ =
   579       Context.subthy_id (Context.certificate_theory_id cert, Context.theory_id thy') orelse
   580         raise CONTEXT ("Cannot transfer: not a super theory", [], [], [th],
   581           SOME (Context.Theory thy'));
   582     val cert' = Context.join_certificate (Context.Certificate thy', cert);
   583   in
   584     if Context.eq_certificate (cert, cert') then th
   585     else
   586       Thm (der,
   587        {cert = cert',
   588         tags = tags,
   589         maxidx = maxidx,
   590         constraints = constraints,
   591         shyps = shyps,
   592         hyps = hyps,
   593         tpairs = tpairs,
   594         prop = prop})
   595   end;
   596 
   597 val transfer' = transfer o Proof_Context.theory_of;
   598 val transfer'' = transfer o Context.theory_of;
   599 
   600 fun join_transfer thy th =
   601   if Context.subthy_id (Context.theory_id thy, theory_id th) then th
   602   else transfer thy th;
   603 
   604 fun join_transfer_context (ctxt, th) =
   605   if Context.subthy_id (Context.theory_id (Proof_Context.theory_of ctxt), theory_id th) then
   606     (Context.raw_transfer (theory_of_thm th) ctxt, th)
   607   else (ctxt, transfer' ctxt th);
   608 
   609 
   610 (* matching *)
   611 
   612 local
   613 
   614 fun gen_match match
   615     (ct1 as Cterm {t = t1, sorts = sorts1, ...},
   616      ct2 as Cterm {t = t2, sorts = sorts2, maxidx = maxidx2, ...}) =
   617   let
   618     val cert = join_certificate0 (ct1, ct2);
   619     val thy = Context.certificate_theory cert
   620       handle ERROR msg => raise CONTEXT (msg, [], [ct1, ct2], [], NONE);
   621     val (Tinsts, tinsts) = match thy (t1, t2) (Vartab.empty, Vartab.empty);
   622     val sorts = Sorts.union sorts1 sorts2;
   623     fun mk_cTinst ((a, i), (S, T)) =
   624       (((a, i), S), Ctyp {T = T, cert = cert, maxidx = maxidx2, sorts = sorts});
   625     fun mk_ctinst ((x, i), (U, t)) =
   626       let val T = Envir.subst_type Tinsts U in
   627         (((x, i), T), Cterm {t = t, T = T, cert = cert, maxidx = maxidx2, sorts = sorts})
   628       end;
   629   in (Vartab.fold (cons o mk_cTinst) Tinsts [], Vartab.fold (cons o mk_ctinst) tinsts []) end;
   630 
   631 in
   632 
   633 val match = gen_match Pattern.match;
   634 val first_order_match = gen_match Pattern.first_order_match;
   635 
   636 end;
   637 
   638 
   639 (*implicit alpha-conversion*)
   640 fun renamed_prop prop' (Thm (der, {cert, tags, maxidx, constraints, shyps, hyps, tpairs, prop})) =
   641   if prop aconv prop' then
   642     Thm (der, {cert = cert, tags = tags, maxidx = maxidx, constraints = constraints, shyps = shyps,
   643       hyps = hyps, tpairs = tpairs, prop = prop'})
   644   else raise TERM ("renamed_prop: props disagree", [prop, prop']);
   645 
   646 fun make_context ths NONE cert =
   647       (Context.Theory (Context.certificate_theory cert)
   648         handle ERROR msg => raise CONTEXT (msg, [], [], ths, NONE))
   649   | make_context ths (SOME ctxt) cert =
   650       let
   651         val thy_id = Context.certificate_theory_id cert;
   652         val thy_id' = Context.theory_id (Proof_Context.theory_of ctxt);
   653       in
   654         if Context.subthy_id (thy_id, thy_id') then Context.Proof ctxt
   655         else raise CONTEXT ("Bad context", [], [], ths, SOME (Context.Proof ctxt))
   656       end;
   657 
   658 fun make_context_certificate ths opt_ctxt cert =
   659   let
   660     val context = make_context ths opt_ctxt cert;
   661     val cert' = Context.Certificate (Context.theory_of context);
   662   in (context, cert') end;
   663 
   664 (*explicit weakening: maps |- B to A |- B*)
   665 fun weaken raw_ct th =
   666   let
   667     val ct as Cterm {t = A, T, sorts, maxidx = maxidxA, ...} = adjust_maxidx_cterm ~1 raw_ct;
   668     val Thm (der, {tags, maxidx, constraints, shyps, hyps, tpairs, prop, ...}) = th;
   669   in
   670     if T <> propT then
   671       raise THM ("weaken: assumptions must have type prop", 0, [])
   672     else if maxidxA <> ~1 then
   673       raise THM ("weaken: assumptions may not contain schematic variables", maxidxA, [])
   674     else
   675       Thm (der,
   676        {cert = join_certificate1 (ct, th),
   677         tags = tags,
   678         maxidx = maxidx,
   679         constraints = constraints,
   680         shyps = Sorts.union sorts shyps,
   681         hyps = insert_hyps A hyps,
   682         tpairs = tpairs,
   683         prop = prop})
   684   end;
   685 
   686 fun weaken_sorts raw_sorts ct =
   687   let
   688     val Cterm {cert, t, T, maxidx, sorts} = ct;
   689     val thy = theory_of_cterm ct;
   690     val more_sorts = Sorts.make (map (Sign.certify_sort thy) raw_sorts);
   691     val sorts' = Sorts.union sorts more_sorts;
   692   in Cterm {cert = cert, t = t, T = T, maxidx = maxidx, sorts = sorts'} end;
   693 
   694 (*dangling sort constraints of a thm*)
   695 fun extra_shyps (th as Thm (_, {shyps, ...})) =
   696   Sorts.subtract (fold_terms Sorts.insert_term th []) shyps;
   697 
   698 
   699 
   700 (** derivations and promised proofs **)
   701 
   702 fun make_deriv promises oracles thms proof =
   703   Deriv {promises = promises, body = PBody {oracles = oracles, thms = thms, proof = proof}};
   704 
   705 val empty_deriv = make_deriv [] [] [] MinProof;
   706 
   707 
   708 (* inference rules *)
   709 
   710 fun promise_ord ((i, _), (j, _)) = int_ord (j, i);
   711 
   712 fun deriv_rule2 f
   713     (Deriv {promises = ps1, body = PBody {oracles = oracles1, thms = thms1, proof = prf1}})
   714     (Deriv {promises = ps2, body = PBody {oracles = oracles2, thms = thms2, proof = prf2}}) =
   715   let
   716     val ps = Ord_List.union promise_ord ps1 ps2;
   717     val oracles = Proofterm.unions_oracles [oracles1, oracles2];
   718     val thms = Proofterm.unions_thms [thms1, thms2];
   719     val prf =
   720       (case ! Proofterm.proofs of
   721         2 => f prf1 prf2
   722       | 1 => MinProof
   723       | 0 => MinProof
   724       | i => error ("Illegal level of detail for proof objects: " ^ string_of_int i));
   725   in make_deriv ps oracles thms prf end;
   726 
   727 fun deriv_rule1 f = deriv_rule2 (K f) empty_deriv;
   728 fun deriv_rule0 prf = deriv_rule1 I (make_deriv [] [] [] prf);
   729 
   730 fun deriv_rule_unconditional f (Deriv {promises, body = PBody {oracles, thms, proof}}) =
   731   make_deriv promises oracles thms (f proof);
   732 
   733 
   734 (* fulfilled proofs *)
   735 
   736 fun raw_body_of (Thm (Deriv {body, ...}, _)) = body;
   737 fun raw_promises_of (Thm (Deriv {promises, ...}, _)) = promises;
   738 
   739 fun join_promises [] = ()
   740   | join_promises promises = join_promises_of (Future.joins (map snd promises))
   741 and join_promises_of thms = join_promises (Ord_List.make promise_ord (maps raw_promises_of thms));
   742 
   743 fun fulfill_body (th as Thm (Deriv {promises, body}, _)) =
   744   let val fulfilled_promises = map #1 promises ~~ map fulfill_body (Future.joins (map #2 promises))
   745   in Proofterm.fulfill_norm_proof (theory_of_thm th) fulfilled_promises body end;
   746 
   747 fun proof_bodies_of thms = (join_promises_of thms; map fulfill_body thms);
   748 val proof_body_of = singleton proof_bodies_of;
   749 val proof_of = Proofterm.proof_of o proof_body_of;
   750 
   751 val consolidate = ignore o proof_bodies_of;
   752 
   753 
   754 (* derivation status *)
   755 
   756 fun peek_status (Thm (Deriv {promises, body}, _)) =
   757   let
   758     val ps = map (Future.peek o snd) promises;
   759     val bodies = body ::
   760       map_filter (fn SOME (Exn.Res th) => SOME (raw_body_of th) | _ => NONE) ps;
   761     val {oracle, unfinished, failed} = Proofterm.peek_status bodies;
   762   in
   763    {oracle = oracle,
   764     unfinished = unfinished orelse exists is_none ps,
   765     failed = failed orelse exists (fn SOME (Exn.Exn _) => true | _ => false) ps}
   766   end;
   767 
   768 
   769 (* future rule *)
   770 
   771 fun future_result i orig_cert orig_shyps orig_prop thm =
   772   let
   773     fun err msg = raise THM ("future_result: " ^ msg, 0, [thm]);
   774     val Thm (Deriv {promises, ...}, {cert, constraints, shyps, hyps, tpairs, prop, ...}) = thm;
   775 
   776     val _ = Context.eq_certificate (cert, orig_cert) orelse err "bad theory";
   777     val _ = prop aconv orig_prop orelse err "bad prop";
   778     val _ = null constraints orelse err "bad sort constraints";
   779     val _ = null tpairs orelse err "bad flex-flex constraints";
   780     val _ = null hyps orelse err "bad hyps";
   781     val _ = Sorts.subset (shyps, orig_shyps) orelse err "bad shyps";
   782     val _ = forall (fn (j, _) => i <> j) promises orelse err "bad dependencies";
   783     val _ = join_promises promises;
   784   in thm end;
   785 
   786 fun future future_thm ct =
   787   let
   788     val Cterm {cert = cert, t = prop, T, maxidx, sorts} = ct;
   789     val _ = T <> propT andalso raise CTERM ("future: prop expected", [ct]);
   790     val _ =
   791       if Proofterm.proofs_enabled ()
   792       then raise CTERM ("future: proof terms enabled", [ct]) else ();
   793 
   794     val i = serial ();
   795     val future = future_thm |> Future.map (future_result i cert sorts prop);
   796   in
   797     Thm (make_deriv [(i, future)] [] [] MinProof,
   798      {cert = cert,
   799       tags = [],
   800       maxidx = maxidx,
   801       constraints = [],
   802       shyps = sorts,
   803       hyps = [],
   804       tpairs = [],
   805       prop = prop})
   806   end;
   807 
   808 
   809 
   810 (** Axioms **)
   811 
   812 fun axiom thy0 name =
   813   let
   814     fun get_ax thy =
   815       Name_Space.lookup (Theory.axiom_table thy) name
   816       |> Option.map (fn prop =>
   817            let
   818              val der = deriv_rule0 (Proofterm.axm_proof name prop);
   819              val cert = Context.Certificate thy;
   820              val maxidx = maxidx_of_term prop;
   821              val shyps = Sorts.insert_term prop [];
   822            in
   823              Thm (der,
   824                {cert = cert, tags = [], maxidx = maxidx,
   825                  constraints = [], shyps = shyps, hyps = [], tpairs = [], prop = prop})
   826            end);
   827   in
   828     (case get_first get_ax (Theory.nodes_of thy0) of
   829       SOME thm => thm
   830     | NONE => raise THEORY ("No axiom " ^ quote name, [thy0]))
   831   end;
   832 
   833 (*return additional axioms of this theory node*)
   834 fun axioms_of thy =
   835   map (fn (name, _) => (name, axiom thy name)) (Theory.axioms_of thy);
   836 
   837 
   838 (* tags *)
   839 
   840 val get_tags = #tags o rep_thm;
   841 
   842 fun map_tags f (Thm (der, {cert, tags, maxidx, constraints, shyps, hyps, tpairs, prop})) =
   843   Thm (der, {cert = cert, tags = f tags, maxidx = maxidx, constraints = constraints,
   844     shyps = shyps, hyps = hyps, tpairs = tpairs, prop = prop});
   845 
   846 
   847 (* technical adjustments *)
   848 
   849 fun norm_proof (th as Thm (der, args)) =
   850   Thm (deriv_rule1 (Proofterm.rew_proof (theory_of_thm th)) der, args);
   851 
   852 fun adjust_maxidx_thm i
   853     (th as Thm (der, {cert, tags, maxidx, constraints, shyps, hyps, tpairs, prop})) =
   854   if maxidx = i then th
   855   else if maxidx < i then
   856     Thm (der, {maxidx = i, cert = cert, tags = tags, constraints = constraints, shyps = shyps,
   857       hyps = hyps, tpairs = tpairs, prop = prop})
   858   else
   859     Thm (der, {maxidx = Int.max (maxidx_tpairs tpairs (maxidx_of_term prop), i),
   860       cert = cert, tags = tags, constraints = constraints, shyps = shyps,
   861       hyps = hyps, tpairs = tpairs, prop = prop});
   862 
   863 
   864 
   865 (*** Theory data ***)
   866 
   867 (* type classes *)
   868 
   869 structure Aritytab =
   870   Table(
   871     type key = string * sort list * class;
   872     val ord =
   873       fast_string_ord o apply2 #1
   874       <<< fast_string_ord o apply2 #3
   875       <<< list_ord Term_Ord.sort_ord o apply2 #2;
   876   );
   877 
   878 datatype classes = Classes of
   879  {classrels: thm Symreltab.table,
   880   arities: (thm * string * serial) Aritytab.table};
   881 
   882 fun make_classes (classrels, arities) = Classes {classrels = classrels, arities = arities};
   883 
   884 val empty_classes = make_classes (Symreltab.empty, Aritytab.empty);
   885 
   886 (*see Theory.at_begin hook for transitive closure of classrels and arity completion*)
   887 fun merge_classes
   888    (Classes {classrels = classrels1, arities = arities1},
   889     Classes {classrels = classrels2, arities = arities2}) =
   890   let
   891     val classrels' = Symreltab.merge (K true) (classrels1, classrels2);
   892     val arities' = Aritytab.merge (K true) (arities1, arities2);
   893   in make_classes (classrels', arities') end;
   894 
   895 
   896 (* data *)
   897 
   898 structure Data = Theory_Data
   899 (
   900   type T =
   901     unit Name_Space.table *  (*oracles: authentic derivation names*)
   902     classes;  (*type classes within the logic*)
   903 
   904   val empty : T = (Name_Space.empty_table "oracle", empty_classes);
   905   val extend = I;
   906   fun merge ((oracles1, sorts1), (oracles2, sorts2)) : T =
   907     (Name_Space.merge_tables (oracles1, oracles2), merge_classes (sorts1, sorts2));
   908 );
   909 
   910 val get_oracles = #1 o Data.get;
   911 val map_oracles = Data.map o apfst;
   912 
   913 val get_classes = (fn (_, Classes args) => args) o Data.get;
   914 val get_classrels = #classrels o get_classes;
   915 val get_arities = #arities o get_classes;
   916 
   917 fun map_classes f =
   918   (Data.map o apsnd) (fn Classes {classrels, arities} => make_classes (f (classrels, arities)));
   919 fun map_classrels f = map_classes (fn (classrels, arities) => (f classrels, arities));
   920 fun map_arities f = map_classes (fn (classrels, arities) => (classrels, f arities));
   921 
   922 
   923 (* type classes *)
   924 
   925 fun the_classrel thy (c1, c2) =
   926   (case Symreltab.lookup (get_classrels thy) (c1, c2) of
   927     SOME thm => transfer thy thm
   928   | NONE => error ("Unproven class relation " ^
   929       Syntax.string_of_classrel (Proof_Context.init_global thy) [c1, c2]));
   930 
   931 fun the_arity thy (a, Ss, c) =
   932   (case Aritytab.lookup (get_arities thy) (a, Ss, c) of
   933     SOME (thm, _, _) => transfer thy thm
   934   | NONE => error ("Unproven type arity " ^
   935       Syntax.string_of_arity (Proof_Context.init_global thy) (a, Ss, [c])));
   936 
   937 val classrel_proof = proof_of oo the_classrel;
   938 val arity_proof = proof_of oo the_arity;
   939 
   940 
   941 (* solve sort constraints by pro-forma proof *)
   942 
   943 local
   944 
   945 fun union_digest (oracles1, thms1) (oracles2, thms2) =
   946   (Proofterm.unions_oracles [oracles1, oracles2], Proofterm.unions_thms [thms1, thms2]);
   947 
   948 fun thm_digest (Thm (Deriv {body = Proofterm.PBody {oracles, thms, ...}, ...}, _)) =
   949   (oracles, thms);
   950 
   951 fun constraint_digest ({theory = thy, typ, sort, ...}: constraint) =
   952   Sorts.of_sort_derivation (Sign.classes_of thy)
   953    {class_relation = fn _ => fn _ => fn (digest, c1) => fn c2 =>
   954       if c1 = c2 then ([], []) else union_digest digest (thm_digest (the_classrel thy (c1, c2))),
   955     type_constructor = fn (a, _) => fn dom => fn c =>
   956       let val arity_digest = thm_digest (the_arity thy (a, (map o map) #2 dom, c))
   957       in (fold o fold) (union_digest o #1) dom arity_digest end,
   958     type_variable = fn T => map (pair ([], [])) (Type.sort_of_atyp T)}
   959    (typ, sort);
   960 
   961 in
   962 
   963 fun solve_constraints (thm as Thm (_, {constraints = [], ...})) = thm
   964   | solve_constraints (thm as Thm (der, args)) =
   965       let
   966         val {cert, tags, maxidx, constraints, shyps, hyps, tpairs, prop} = args;
   967 
   968         val thy = Context.certificate_theory cert;
   969         val bad_thys =
   970           constraints |> map_filter (fn {theory = thy', ...} =>
   971             if Context.eq_thy (thy, thy') then NONE else SOME thy');
   972         val () =
   973           if null bad_thys then ()
   974           else
   975             raise THEORY ("solve_constraints: bad theories for theorem\n" ^
   976               Syntax.string_of_term_global thy (prop_of thm), thy :: bad_thys);
   977 
   978         val Deriv {promises, body = Proofterm.PBody {oracles, thms, proof}} = der;
   979         val (oracles', thms') = (oracles, thms)
   980           |> fold (fold union_digest o constraint_digest) constraints;
   981         val body' = Proofterm.PBody {oracles = oracles', thms = thms', proof = proof};
   982       in
   983         Thm (Deriv {promises = promises, body = body'},
   984           {constraints = [], cert = cert, tags = tags, maxidx = maxidx,
   985             shyps = shyps, hyps = hyps, tpairs = tpairs, prop = prop})
   986       end;
   987 
   988 end;
   989 
   990 
   991 
   992 (*** Closed theorems with official name ***)
   993 
   994 (*non-deterministic, depends on unknown promises*)
   995 fun derivation_closed (Thm (Deriv {body, ...}, _)) =
   996   Proofterm.compact_proof (Proofterm.proof_of body);
   997 
   998 (*non-deterministic, depends on unknown promises*)
   999 fun derivation_name (Thm (Deriv {body, ...}, {shyps, hyps, prop, ...})) =
  1000   Proofterm.get_name shyps hyps prop (Proofterm.proof_of body);
  1001 
  1002 fun name_derivation name_pos =
  1003   solve_constraints #> (fn thm as Thm (der, args) =>
  1004     let
  1005       val thy = theory_of_thm thm;
  1006 
  1007       val Deriv {promises, body} = der;
  1008       val {shyps, hyps, prop, tpairs, ...} = args;
  1009 
  1010       val _ = null tpairs orelse raise THM ("name_derivation: bad flex-flex constraints", 0, [thm]);
  1011 
  1012       val ps = map (apsnd (Future.map fulfill_body)) promises;
  1013       val (pthm, proof) =
  1014         Proofterm.thm_proof thy (classrel_proof thy) (arity_proof thy)
  1015           name_pos shyps hyps prop ps body;
  1016       val der' = make_deriv [] [] [pthm] proof;
  1017     in Thm (der', args) end);
  1018 
  1019 fun close_derivation pos =
  1020   solve_constraints #> (fn thm =>
  1021     if not (null (tpairs_of thm)) orelse derivation_closed thm then thm
  1022     else name_derivation ("", pos) thm);
  1023 
  1024 val trim_context = solve_constraints #> trim_context_thm;
  1025 
  1026 
  1027 
  1028 (*** Oracles ***)
  1029 
  1030 fun add_oracle (b, oracle_fn) thy =
  1031   let
  1032     val (name, oracles') = Name_Space.define (Context.Theory thy) true (b, ()) (get_oracles thy);
  1033     val thy' = map_oracles (K oracles') thy;
  1034     fun invoke_oracle arg =
  1035       let val Cterm {cert = cert2, t = prop, T, maxidx, sorts} = oracle_fn arg in
  1036         if T <> propT then
  1037           raise THM ("Oracle's result must have type prop: " ^ name, 0, [])
  1038         else
  1039           let val (oracle, prf) = Proofterm.oracle_proof name prop in
  1040             Thm (make_deriv [] [oracle] [] prf,
  1041              {cert = Context.join_certificate (Context.Certificate thy', cert2),
  1042               tags = [],
  1043               maxidx = maxidx,
  1044               constraints = [],
  1045               shyps = sorts,
  1046               hyps = [],
  1047               tpairs = [],
  1048               prop = prop})
  1049           end
  1050       end;
  1051   in ((name, invoke_oracle), thy') end;
  1052 
  1053 fun extern_oracles verbose ctxt =
  1054   map #1 (Name_Space.markup_table verbose ctxt (get_oracles (Proof_Context.theory_of ctxt)));
  1055 
  1056 
  1057 
  1058 (*** Meta rules ***)
  1059 
  1060 (** primitive rules **)
  1061 
  1062 (*The assumption rule A |- A*)
  1063 fun assume raw_ct =
  1064   let val Cterm {cert, t = prop, T, maxidx, sorts} = adjust_maxidx_cterm ~1 raw_ct in
  1065     if T <> propT then
  1066       raise THM ("assume: prop", 0, [])
  1067     else if maxidx <> ~1 then
  1068       raise THM ("assume: variables", maxidx, [])
  1069     else Thm (deriv_rule0 (Proofterm.Hyp prop),
  1070      {cert = cert,
  1071       tags = [],
  1072       maxidx = ~1,
  1073       constraints = [],
  1074       shyps = sorts,
  1075       hyps = [prop],
  1076       tpairs = [],
  1077       prop = prop})
  1078   end;
  1079 
  1080 (*Implication introduction
  1081     [A]
  1082      :
  1083      B
  1084   -------
  1085   A \<Longrightarrow> B
  1086 *)
  1087 fun implies_intr
  1088     (ct as Cterm {t = A, T, maxidx = maxidx1, sorts, ...})
  1089     (th as Thm (der, {maxidx = maxidx2, hyps, constraints, shyps, tpairs, prop, ...})) =
  1090   if T <> propT then
  1091     raise THM ("implies_intr: assumptions must have type prop", 0, [th])
  1092   else
  1093     Thm (deriv_rule1 (Proofterm.implies_intr_proof A) der,
  1094      {cert = join_certificate1 (ct, th),
  1095       tags = [],
  1096       maxidx = Int.max (maxidx1, maxidx2),
  1097       constraints = constraints,
  1098       shyps = Sorts.union sorts shyps,
  1099       hyps = remove_hyps A hyps,
  1100       tpairs = tpairs,
  1101       prop = Logic.mk_implies (A, prop)});
  1102 
  1103 
  1104 (*Implication elimination
  1105   A \<Longrightarrow> B    A
  1106   ------------
  1107         B
  1108 *)
  1109 fun implies_elim thAB thA =
  1110   let
  1111     val Thm (derA,
  1112       {maxidx = maxidx1, hyps = hypsA, constraints = constraintsA, shyps = shypsA,
  1113         tpairs = tpairsA, prop = propA, ...}) = thA
  1114     and Thm (der, {maxidx = maxidx2, hyps, constraints, shyps, tpairs, prop, ...}) = thAB;
  1115     fun err () = raise THM ("implies_elim: major premise", 0, [thAB, thA]);
  1116   in
  1117     (case prop of
  1118       Const ("Pure.imp", _) $ A $ B =>
  1119         if A aconv propA then
  1120           Thm (deriv_rule2 (curry Proofterm.%%) der derA,
  1121            {cert = join_certificate2 (thAB, thA),
  1122             tags = [],
  1123             maxidx = Int.max (maxidx1, maxidx2),
  1124             constraints = union_constraints constraintsA constraints,
  1125             shyps = Sorts.union shypsA shyps,
  1126             hyps = union_hyps hypsA hyps,
  1127             tpairs = union_tpairs tpairsA tpairs,
  1128             prop = B})
  1129         else err ()
  1130     | _ => err ())
  1131   end;
  1132 
  1133 (*Forall introduction.  The Free or Var x must not be free in the hypotheses.
  1134     [x]
  1135      :
  1136      A
  1137   ------
  1138   \<And>x. A
  1139 *)
  1140 fun forall_intr
  1141     (ct as Cterm {maxidx = maxidx1, t = x, T, sorts, ...})
  1142     (th as Thm (der, {maxidx = maxidx2, constraints, shyps, hyps, tpairs, prop, ...})) =
  1143   let
  1144     fun result a =
  1145       Thm (deriv_rule1 (Proofterm.forall_intr_proof x a) der,
  1146        {cert = join_certificate1 (ct, th),
  1147         tags = [],
  1148         maxidx = Int.max (maxidx1, maxidx2),
  1149         constraints = constraints,
  1150         shyps = Sorts.union sorts shyps,
  1151         hyps = hyps,
  1152         tpairs = tpairs,
  1153         prop = Logic.all_const T $ Abs (a, T, abstract_over (x, prop))});
  1154     fun check_occs a x ts =
  1155       if exists (fn t => Logic.occs (x, t)) ts then
  1156         raise THM ("forall_intr: variable " ^ quote a ^ " free in assumptions", 0, [th])
  1157       else ();
  1158   in
  1159     (case x of
  1160       Free (a, _) => (check_occs a x hyps; check_occs a x (terms_of_tpairs tpairs); result a)
  1161     | Var ((a, _), _) => (check_occs a x (terms_of_tpairs tpairs); result a)
  1162     | _ => raise THM ("forall_intr: not a variable", 0, [th]))
  1163   end;
  1164 
  1165 (*Forall elimination
  1166   \<And>x. A
  1167   ------
  1168   A[t/x]
  1169 *)
  1170 fun forall_elim
  1171     (ct as Cterm {t, T, maxidx = maxidx1, sorts, ...})
  1172     (th as Thm (der, {maxidx = maxidx2, constraints, shyps, hyps, tpairs, prop, ...})) =
  1173   (case prop of
  1174     Const ("Pure.all", Type ("fun", [Type ("fun", [qary, _]), _])) $ A =>
  1175       if T <> qary then
  1176         raise THM ("forall_elim: type mismatch", 0, [th])
  1177       else
  1178         Thm (deriv_rule1 (Proofterm.% o rpair (SOME t)) der,
  1179          {cert = join_certificate1 (ct, th),
  1180           tags = [],
  1181           maxidx = Int.max (maxidx1, maxidx2),
  1182           constraints = constraints,
  1183           shyps = Sorts.union sorts shyps,
  1184           hyps = hyps,
  1185           tpairs = tpairs,
  1186           prop = Term.betapply (A, t)})
  1187   | _ => raise THM ("forall_elim: not quantified", 0, [th]));
  1188 
  1189 
  1190 (* Equality *)
  1191 
  1192 (*Reflexivity
  1193   t \<equiv> t
  1194 *)
  1195 fun reflexive (Cterm {cert, t, T = _, maxidx, sorts}) =
  1196   Thm (deriv_rule0 Proofterm.reflexive,
  1197    {cert = cert,
  1198     tags = [],
  1199     maxidx = maxidx,
  1200     constraints = [],
  1201     shyps = sorts,
  1202     hyps = [],
  1203     tpairs = [],
  1204     prop = Logic.mk_equals (t, t)});
  1205 
  1206 (*Symmetry
  1207   t \<equiv> u
  1208   ------
  1209   u \<equiv> t
  1210 *)
  1211 fun symmetric (th as Thm (der, {cert, maxidx, constraints, shyps, hyps, tpairs, prop, ...})) =
  1212   (case prop of
  1213     (eq as Const ("Pure.eq", _)) $ t $ u =>
  1214       Thm (deriv_rule1 Proofterm.symmetric der,
  1215        {cert = cert,
  1216         tags = [],
  1217         maxidx = maxidx,
  1218         constraints = constraints,
  1219         shyps = shyps,
  1220         hyps = hyps,
  1221         tpairs = tpairs,
  1222         prop = eq $ u $ t})
  1223     | _ => raise THM ("symmetric", 0, [th]));
  1224 
  1225 (*Transitivity
  1226   t1 \<equiv> u    u \<equiv> t2
  1227   ------------------
  1228        t1 \<equiv> t2
  1229 *)
  1230 fun transitive th1 th2 =
  1231   let
  1232     val Thm (der1, {maxidx = maxidx1, hyps = hyps1, constraints = constraints1, shyps = shyps1,
  1233         tpairs = tpairs1, prop = prop1, ...}) = th1
  1234     and Thm (der2, {maxidx = maxidx2, hyps = hyps2, constraints = constraints2, shyps = shyps2,
  1235         tpairs = tpairs2, prop = prop2, ...}) = th2;
  1236     fun err msg = raise THM ("transitive: " ^ msg, 0, [th1, th2]);
  1237   in
  1238     case (prop1, prop2) of
  1239       ((eq as Const ("Pure.eq", Type (_, [T, _]))) $ t1 $ u, Const ("Pure.eq", _) $ u' $ t2) =>
  1240         if not (u aconv u') then err "middle term"
  1241         else
  1242           Thm (deriv_rule2 (Proofterm.transitive u T) der1 der2,
  1243            {cert = join_certificate2 (th1, th2),
  1244             tags = [],
  1245             maxidx = Int.max (maxidx1, maxidx2),
  1246             constraints = union_constraints constraints1 constraints2,
  1247             shyps = Sorts.union shyps1 shyps2,
  1248             hyps = union_hyps hyps1 hyps2,
  1249             tpairs = union_tpairs tpairs1 tpairs2,
  1250             prop = eq $ t1 $ t2})
  1251      | _ =>  err "premises"
  1252   end;
  1253 
  1254 (*Beta-conversion
  1255   (\<lambda>x. t) u \<equiv> t[u/x]
  1256   fully beta-reduces the term if full = true
  1257 *)
  1258 fun beta_conversion full (Cterm {cert, t, T = _, maxidx, sorts}) =
  1259   let val t' =
  1260     if full then Envir.beta_norm t
  1261     else
  1262       (case t of Abs (_, _, bodt) $ u => subst_bound (u, bodt)
  1263       | _ => raise THM ("beta_conversion: not a redex", 0, []));
  1264   in
  1265     Thm (deriv_rule0 Proofterm.reflexive,
  1266      {cert = cert,
  1267       tags = [],
  1268       maxidx = maxidx,
  1269       constraints = [],
  1270       shyps = sorts,
  1271       hyps = [],
  1272       tpairs = [],
  1273       prop = Logic.mk_equals (t, t')})
  1274   end;
  1275 
  1276 fun eta_conversion (Cterm {cert, t, T = _, maxidx, sorts}) =
  1277   Thm (deriv_rule0 Proofterm.reflexive,
  1278    {cert = cert,
  1279     tags = [],
  1280     maxidx = maxidx,
  1281     constraints = [],
  1282     shyps = sorts,
  1283     hyps = [],
  1284     tpairs = [],
  1285     prop = Logic.mk_equals (t, Envir.eta_contract t)});
  1286 
  1287 fun eta_long_conversion (Cterm {cert, t, T = _, maxidx, sorts}) =
  1288   Thm (deriv_rule0 Proofterm.reflexive,
  1289    {cert = cert,
  1290     tags = [],
  1291     maxidx = maxidx,
  1292     constraints = [],
  1293     shyps = sorts,
  1294     hyps = [],
  1295     tpairs = [],
  1296     prop = Logic.mk_equals (t, Envir.eta_long [] t)});
  1297 
  1298 (*The abstraction rule.  The Free or Var x must not be free in the hypotheses.
  1299   The bound variable will be named "a" (since x will be something like x320)
  1300       t \<equiv> u
  1301   --------------
  1302   \<lambda>x. t \<equiv> \<lambda>x. u
  1303 *)
  1304 fun abstract_rule a
  1305     (Cterm {t = x, T, sorts, ...})
  1306     (th as Thm (der, {cert, maxidx, hyps, constraints, shyps, tpairs, prop, ...})) =
  1307   let
  1308     val (t, u) = Logic.dest_equals prop
  1309       handle TERM _ => raise THM ("abstract_rule: premise not an equality", 0, [th]);
  1310     val result =
  1311       Thm (deriv_rule1 (Proofterm.abstract_rule x a) der,
  1312        {cert = cert,
  1313         tags = [],
  1314         maxidx = maxidx,
  1315         constraints = constraints,
  1316         shyps = Sorts.union sorts shyps,
  1317         hyps = hyps,
  1318         tpairs = tpairs,
  1319         prop = Logic.mk_equals
  1320           (Abs (a, T, abstract_over (x, t)), Abs (a, T, abstract_over (x, u)))});
  1321     fun check_occs a x ts =
  1322       if exists (fn t => Logic.occs (x, t)) ts then
  1323         raise THM ("abstract_rule: variable " ^ quote a ^ " free in assumptions", 0, [th])
  1324       else ();
  1325   in
  1326     (case x of
  1327       Free (a, _) => (check_occs a x hyps; check_occs a x (terms_of_tpairs tpairs); result)
  1328     | Var ((a, _), _) => (check_occs a x (terms_of_tpairs tpairs); result)
  1329     | _ => raise THM ("abstract_rule: not a variable", 0, [th]))
  1330   end;
  1331 
  1332 (*The combination rule
  1333   f \<equiv> g  t \<equiv> u
  1334   -------------
  1335     f t \<equiv> g u
  1336 *)
  1337 fun combination th1 th2 =
  1338   let
  1339     val Thm (der1, {maxidx = maxidx1, constraints = constraints1, shyps = shyps1,
  1340         hyps = hyps1, tpairs = tpairs1, prop = prop1, ...}) = th1
  1341     and Thm (der2, {maxidx = maxidx2, constraints = constraints2, shyps = shyps2,
  1342         hyps = hyps2, tpairs = tpairs2, prop = prop2, ...}) = th2;
  1343     fun chktypes fT tT =
  1344       (case fT of
  1345         Type ("fun", [T1, _]) =>
  1346           if T1 <> tT then
  1347             raise THM ("combination: types", 0, [th1, th2])
  1348           else ()
  1349       | _ => raise THM ("combination: not function type", 0, [th1, th2]));
  1350   in
  1351     (case (prop1, prop2) of
  1352       (Const ("Pure.eq", Type ("fun", [fT, _])) $ f $ g,
  1353        Const ("Pure.eq", Type ("fun", [tT, _])) $ t $ u) =>
  1354         (chktypes fT tT;
  1355           Thm (deriv_rule2 (Proofterm.combination f g t u fT) der1 der2,
  1356            {cert = join_certificate2 (th1, th2),
  1357             tags = [],
  1358             maxidx = Int.max (maxidx1, maxidx2),
  1359             constraints = union_constraints constraints1 constraints2,
  1360             shyps = Sorts.union shyps1 shyps2,
  1361             hyps = union_hyps hyps1 hyps2,
  1362             tpairs = union_tpairs tpairs1 tpairs2,
  1363             prop = Logic.mk_equals (f $ t, g $ u)}))
  1364      | _ => raise THM ("combination: premises", 0, [th1, th2]))
  1365   end;
  1366 
  1367 (*Equality introduction
  1368   A \<Longrightarrow> B  B \<Longrightarrow> A
  1369   ----------------
  1370        A \<equiv> B
  1371 *)
  1372 fun equal_intr th1 th2 =
  1373   let
  1374     val Thm (der1, {maxidx = maxidx1, constraints = constraints1, shyps = shyps1,
  1375       hyps = hyps1, tpairs = tpairs1, prop = prop1, ...}) = th1
  1376     and Thm (der2, {maxidx = maxidx2, constraints = constraints2, shyps = shyps2,
  1377       hyps = hyps2, tpairs = tpairs2, prop = prop2, ...}) = th2;
  1378     fun err msg = raise THM ("equal_intr: " ^ msg, 0, [th1, th2]);
  1379   in
  1380     (case (prop1, prop2) of
  1381       (Const("Pure.imp", _) $ A $ B, Const("Pure.imp", _) $ B' $ A') =>
  1382         if A aconv A' andalso B aconv B' then
  1383           Thm (deriv_rule2 (Proofterm.equal_intr A B) der1 der2,
  1384            {cert = join_certificate2 (th1, th2),
  1385             tags = [],
  1386             maxidx = Int.max (maxidx1, maxidx2),
  1387             constraints = union_constraints constraints1 constraints2,
  1388             shyps = Sorts.union shyps1 shyps2,
  1389             hyps = union_hyps hyps1 hyps2,
  1390             tpairs = union_tpairs tpairs1 tpairs2,
  1391             prop = Logic.mk_equals (A, B)})
  1392         else err "not equal"
  1393     | _ =>  err "premises")
  1394   end;
  1395 
  1396 (*The equal propositions rule
  1397   A \<equiv> B  A
  1398   ---------
  1399       B
  1400 *)
  1401 fun equal_elim th1 th2 =
  1402   let
  1403     val Thm (der1, {maxidx = maxidx1, constraints = constraints1, shyps = shyps1,
  1404       hyps = hyps1, tpairs = tpairs1, prop = prop1, ...}) = th1
  1405     and Thm (der2, {maxidx = maxidx2, constraints = constraints2, shyps = shyps2,
  1406       hyps = hyps2, tpairs = tpairs2, prop = prop2, ...}) = th2;
  1407     fun err msg = raise THM ("equal_elim: " ^ msg, 0, [th1, th2]);
  1408   in
  1409     (case prop1 of
  1410       Const ("Pure.eq", _) $ A $ B =>
  1411         if prop2 aconv A then
  1412           Thm (deriv_rule2 (Proofterm.equal_elim A B) der1 der2,
  1413            {cert = join_certificate2 (th1, th2),
  1414             tags = [],
  1415             maxidx = Int.max (maxidx1, maxidx2),
  1416             constraints = union_constraints constraints1 constraints2,
  1417             shyps = Sorts.union shyps1 shyps2,
  1418             hyps = union_hyps hyps1 hyps2,
  1419             tpairs = union_tpairs tpairs1 tpairs2,
  1420             prop = B})
  1421         else err "not equal"
  1422      | _ =>  err "major premise")
  1423   end;
  1424 
  1425 
  1426 
  1427 (**** Derived rules ****)
  1428 
  1429 (*Smash unifies the list of term pairs leaving no flex-flex pairs.
  1430   Instantiates the theorem and deletes trivial tpairs.  Resulting
  1431   sequence may contain multiple elements if the tpairs are not all
  1432   flex-flex.*)
  1433 fun flexflex_rule opt_ctxt =
  1434   solve_constraints #> (fn th =>
  1435     let
  1436       val Thm (der, {cert, maxidx, constraints, shyps, hyps, tpairs, prop, ...}) = th;
  1437       val (context, cert') = make_context_certificate [th] opt_ctxt cert;
  1438     in
  1439       Unify.smash_unifiers context tpairs (Envir.empty maxidx)
  1440       |> Seq.map (fn env =>
  1441           if Envir.is_empty env then th
  1442           else
  1443             let
  1444               val tpairs' = tpairs |> map (apply2 (Envir.norm_term env))
  1445                 (*remove trivial tpairs, of the form t \<equiv> t*)
  1446                 |> filter_out (op aconv);
  1447               val der' = deriv_rule1 (Proofterm.norm_proof' env) der;
  1448               val constraints' =
  1449                 insert_constraints_env (Context.certificate_theory cert') env constraints;
  1450               val prop' = Envir.norm_term env prop;
  1451               val maxidx = maxidx_tpairs tpairs' (maxidx_of_term prop');
  1452               val shyps = Envir.insert_sorts env shyps;
  1453             in
  1454               Thm (der', {cert = cert', tags = [], maxidx = maxidx, constraints = constraints',
  1455                 shyps = shyps, hyps = hyps, tpairs = tpairs', prop = prop'})
  1456             end)
  1457     end);
  1458 
  1459 
  1460 (*Generalization of fixed variables
  1461            A
  1462   --------------------
  1463   A[?'a/'a, ?x/x, ...]
  1464 *)
  1465 
  1466 fun generalize ([], []) _ th = th
  1467   | generalize (tfrees, frees) idx th =
  1468       let
  1469         val Thm (der, {cert, maxidx, constraints, shyps, hyps, tpairs, prop, ...}) = th;
  1470         val _ = idx <= maxidx andalso raise THM ("generalize: bad index", idx, [th]);
  1471 
  1472         val bad_type =
  1473           if null tfrees then K false
  1474           else Term.exists_subtype (fn TFree (a, _) => member (op =) tfrees a | _ => false);
  1475         fun bad_term (Free (x, T)) = bad_type T orelse member (op =) frees x
  1476           | bad_term (Var (_, T)) = bad_type T
  1477           | bad_term (Const (_, T)) = bad_type T
  1478           | bad_term (Abs (_, T, t)) = bad_type T orelse bad_term t
  1479           | bad_term (t $ u) = bad_term t orelse bad_term u
  1480           | bad_term (Bound _) = false;
  1481         val _ = exists bad_term hyps andalso
  1482           raise THM ("generalize: variable free in assumptions", 0, [th]);
  1483 
  1484         val gen = Term_Subst.generalize (tfrees, frees) idx;
  1485         val prop' = gen prop;
  1486         val tpairs' = map (apply2 gen) tpairs;
  1487         val maxidx' = maxidx_tpairs tpairs' (maxidx_of_term prop');
  1488       in
  1489         Thm (deriv_rule1 (Proofterm.generalize (tfrees, frees) idx) der,
  1490          {cert = cert,
  1491           tags = [],
  1492           maxidx = maxidx',
  1493           constraints = constraints,
  1494           shyps = shyps,
  1495           hyps = hyps,
  1496           tpairs = tpairs',
  1497           prop = prop'})
  1498       end;
  1499 
  1500 fun generalize_cterm ([], []) _ ct = ct
  1501   | generalize_cterm (tfrees, frees) idx (ct as Cterm {cert, t, T, maxidx, sorts}) =
  1502       if idx <= maxidx then raise CTERM ("generalize_cterm: bad index", [ct])
  1503       else
  1504         Cterm {cert = cert, sorts = sorts,
  1505           T = Term_Subst.generalizeT tfrees idx T,
  1506           t = Term_Subst.generalize (tfrees, frees) idx t,
  1507           maxidx = Int.max (maxidx, idx)};
  1508 
  1509 fun generalize_ctyp [] _ cT = cT
  1510   | generalize_ctyp tfrees idx (Ctyp {cert, T, maxidx, sorts}) =
  1511       if idx <= maxidx then raise CTERM ("generalize_ctyp: bad index", [])
  1512       else
  1513         Ctyp {cert = cert, sorts = sorts,
  1514           T = Term_Subst.generalizeT tfrees idx T,
  1515           maxidx = Int.max (maxidx, idx)};
  1516 
  1517 
  1518 (*Instantiation of schematic variables
  1519            A
  1520   --------------------
  1521   A[t1/v1, ..., tn/vn]
  1522 *)
  1523 
  1524 local
  1525 
  1526 fun pretty_typing thy t T = Pretty.block
  1527   [Syntax.pretty_term_global thy t, Pretty.str " ::", Pretty.brk 1, Syntax.pretty_typ_global thy T];
  1528 
  1529 fun add_inst (v as (_, T), cu) (cert, sorts) =
  1530   let
  1531     val Cterm {t = u, T = U, cert = cert2, sorts = sorts_u, maxidx = maxidx_u, ...} = cu;
  1532     val cert' = Context.join_certificate (cert, cert2);
  1533     val sorts' = Sorts.union sorts_u sorts;
  1534   in
  1535     if T = U then ((v, (u, maxidx_u)), (cert', sorts'))
  1536     else
  1537       let
  1538         val msg =
  1539           (case cert' of
  1540             Context.Certificate thy' =>
  1541               Pretty.string_of (Pretty.block
  1542                [Pretty.str "instantiate: type conflict",
  1543                 Pretty.fbrk, pretty_typing thy' (Var v) T,
  1544                 Pretty.fbrk, pretty_typing thy' u U])
  1545           | Context.Certificate_Id _ => "instantiate: type conflict");
  1546       in raise TYPE (msg, [T, U], [Var v, u]) end
  1547   end;
  1548 
  1549 fun add_instT (v as (_, S), cU) (cert, sorts) =
  1550   let
  1551     val Ctyp {T = U, cert = cert2, sorts = sorts_U, maxidx = maxidx_U, ...} = cU;
  1552     val cert' = Context.join_certificate (cert, cert2);
  1553     val thy' = Context.certificate_theory cert'
  1554       handle ERROR msg => raise CONTEXT (msg, [cU], [], [], NONE);
  1555     val sorts' = Sorts.union sorts_U sorts;
  1556   in
  1557     if Sign.of_sort thy' (U, S) then ((v, (U, maxidx_U)), (cert', sorts'))
  1558     else raise TYPE ("Type not of sort " ^ Syntax.string_of_sort_global thy' S, [U], [])
  1559   end;
  1560 
  1561 in
  1562 
  1563 (*Left-to-right replacements: ctpairs = [..., (vi, ti), ...].
  1564   Instantiates distinct Vars by terms of same type.
  1565   Does NOT normalize the resulting theorem!*)
  1566 fun instantiate ([], []) th = th
  1567   | instantiate (instT, inst) th =
  1568       let
  1569         val Thm (der, {cert, hyps, constraints, shyps, tpairs, prop, ...}) = th;
  1570         val (inst', (instT', (cert', shyps'))) =
  1571           (cert, shyps) |> fold_map add_inst inst ||> fold_map add_instT instT
  1572             handle CONTEXT (msg, cTs, cts, ths, context) =>
  1573               raise CONTEXT (msg, cTs, cts, th :: ths, context);
  1574         val subst = Term_Subst.instantiate_maxidx (instT', inst');
  1575         val (prop', maxidx1) = subst prop ~1;
  1576         val (tpairs', maxidx') =
  1577           fold_map (fn (t, u) => fn i => subst t i ||>> subst u) tpairs maxidx1;
  1578 
  1579         val thy' = Context.certificate_theory cert';
  1580         val constraints' =
  1581           fold (fn ((_, S), (T, _)) => insert_constraints thy' (T, S)) instT' constraints;
  1582       in
  1583         Thm (deriv_rule1
  1584           (fn d => Proofterm.instantiate (map (apsnd #1) instT', map (apsnd #1) inst') d) der,
  1585          {cert = cert',
  1586           tags = [],
  1587           maxidx = maxidx',
  1588           constraints = constraints',
  1589           shyps = shyps',
  1590           hyps = hyps,
  1591           tpairs = tpairs',
  1592           prop = prop'})
  1593         |> solve_constraints
  1594       end
  1595       handle TYPE (msg, _, _) => raise THM (msg, 0, [th]);
  1596 
  1597 fun instantiate_cterm ([], []) ct = ct
  1598   | instantiate_cterm (instT, inst) ct =
  1599       let
  1600         val Cterm {cert, t, T, sorts, ...} = ct;
  1601         val (inst', (instT', (cert', sorts'))) =
  1602           (cert, sorts) |> fold_map add_inst inst ||> fold_map add_instT instT;
  1603         val subst = Term_Subst.instantiate_maxidx (instT', inst');
  1604         val substT = Term_Subst.instantiateT_maxidx instT';
  1605         val (t', maxidx1) = subst t ~1;
  1606         val (T', maxidx') = substT T maxidx1;
  1607       in Cterm {cert = cert', t = t', T = T', sorts = sorts', maxidx = maxidx'} end
  1608       handle TYPE (msg, _, _) => raise CTERM (msg, [ct]);
  1609 
  1610 end;
  1611 
  1612 
  1613 (*The trivial implication A \<Longrightarrow> A, justified by assume and forall rules.
  1614   A can contain Vars, not so for assume!*)
  1615 fun trivial (Cterm {cert, t = A, T, maxidx, sorts}) =
  1616   if T <> propT then
  1617     raise THM ("trivial: the term must have type prop", 0, [])
  1618   else
  1619     Thm (deriv_rule0 (Proofterm.AbsP ("H", NONE, Proofterm.PBound 0)),
  1620      {cert = cert,
  1621       tags = [],
  1622       maxidx = maxidx,
  1623       constraints = [],
  1624       shyps = sorts,
  1625       hyps = [],
  1626       tpairs = [],
  1627       prop = Logic.mk_implies (A, A)});
  1628 
  1629 (*Axiom-scheme reflecting signature contents
  1630         T :: c
  1631   -------------------
  1632   OFCLASS(T, c_class)
  1633 *)
  1634 fun of_class (cT, raw_c) =
  1635   let
  1636     val Ctyp {cert, T, ...} = cT;
  1637     val thy = Context.certificate_theory cert
  1638       handle ERROR msg => raise CONTEXT (msg, [cT], [], [], NONE);
  1639     val c = Sign.certify_class thy raw_c;
  1640     val Cterm {t = prop, maxidx, sorts, ...} = global_cterm_of thy (Logic.mk_of_class (T, c));
  1641   in
  1642     if Sign.of_sort thy (T, [c]) then
  1643       Thm (deriv_rule0 (Proofterm.OfClass (T, c)),
  1644        {cert = cert,
  1645         tags = [],
  1646         maxidx = maxidx,
  1647         constraints = insert_constraints thy (T, [c]) [],
  1648         shyps = sorts,
  1649         hyps = [],
  1650         tpairs = [],
  1651         prop = prop})
  1652     else raise THM ("of_class: type not of class " ^ Syntax.string_of_sort_global thy [c], 0, [])
  1653   end |> solve_constraints;
  1654 
  1655 (*Remove extra sorts that are witnessed by type signature information*)
  1656 fun strip_shyps (thm as Thm (_, {shyps = [], ...})) = thm
  1657   | strip_shyps (thm as Thm (der, {cert, tags, maxidx, constraints, shyps, hyps, tpairs, prop})) =
  1658       let
  1659         val thy = theory_of_thm thm;
  1660         val algebra = Sign.classes_of thy;
  1661 
  1662         val present = (fold_terms o fold_types o fold_atyps_sorts) (insert (eq_fst op =)) thm [];
  1663         val extra = fold (Sorts.remove_sort o #2) present shyps;
  1664         val witnessed = Sign.witness_sorts thy present extra;
  1665         val extra' = fold (Sorts.remove_sort o #2) witnessed extra
  1666           |> Sorts.minimal_sorts algebra;
  1667         val shyps' = fold (Sorts.insert_sort o #2) present extra';
  1668       in
  1669         Thm (deriv_rule_unconditional
  1670           (Proofterm.strip_shyps_proof algebra present witnessed extra') der,
  1671          {cert = cert, tags = tags, maxidx = maxidx, constraints = constraints,
  1672           shyps = shyps', hyps = hyps, tpairs = tpairs, prop = prop})
  1673       end;
  1674 
  1675 (*Internalize sort constraints of type variables*)
  1676 val unconstrainT =
  1677   solve_constraints #> (fn thm as Thm (der, args) =>
  1678     let
  1679       val Deriv {promises, body} = der;
  1680       val {cert, shyps, hyps, tpairs, prop, ...} = args;
  1681       val thy = theory_of_thm thm;
  1682 
  1683       fun err msg = raise THM ("unconstrainT: " ^ msg, 0, [thm]);
  1684       val _ = null hyps orelse err "bad hyps";
  1685       val _ = null tpairs orelse err "bad flex-flex constraints";
  1686       val tfrees = rev (Term.add_tfree_names prop []);
  1687       val _ = null tfrees orelse err ("illegal free type variables " ^ commas_quote tfrees);
  1688 
  1689       val ps = map (apsnd (Future.map fulfill_body)) promises;
  1690       val (pthm, proof) =
  1691         Proofterm.unconstrain_thm_proof thy (classrel_proof thy) (arity_proof thy)
  1692           shyps prop ps body;
  1693       val der' = make_deriv [] [] [pthm] proof;
  1694       val prop' = Proofterm.thm_node_prop (#2 pthm);
  1695     in
  1696       Thm (der',
  1697        {cert = cert,
  1698         tags = [],
  1699         maxidx = maxidx_of_term prop',
  1700         constraints = [],
  1701         shyps = [[]],  (*potentially redundant*)
  1702         hyps = [],
  1703         tpairs = [],
  1704         prop = prop'})
  1705     end);
  1706 
  1707 (*Replace all TFrees not fixed or in the hyps by new TVars*)
  1708 fun varifyT_global' fixed (Thm (der, {cert, maxidx, constraints, shyps, hyps, tpairs, prop, ...})) =
  1709   let
  1710     val tfrees = fold Term.add_tfrees hyps fixed;
  1711     val prop1 = attach_tpairs tpairs prop;
  1712     val (al, prop2) = Type.varify_global tfrees prop1;
  1713     val (ts, prop3) = Logic.strip_prems (length tpairs, [], prop2);
  1714   in
  1715     (al, Thm (deriv_rule1 (Proofterm.varify_proof prop tfrees) der,
  1716      {cert = cert,
  1717       tags = [],
  1718       maxidx = Int.max (0, maxidx),
  1719       constraints = constraints,
  1720       shyps = shyps,
  1721       hyps = hyps,
  1722       tpairs = rev (map Logic.dest_equals ts),
  1723       prop = prop3}))
  1724   end;
  1725 
  1726 val varifyT_global = #2 o varifyT_global' [];
  1727 
  1728 (*Replace all TVars by TFrees that are often new*)
  1729 fun legacy_freezeT (Thm (der, {cert, constraints, shyps, hyps, tpairs, prop, ...})) =
  1730   let
  1731     val prop1 = attach_tpairs tpairs prop;
  1732     val prop2 = Type.legacy_freeze prop1;
  1733     val (ts, prop3) = Logic.strip_prems (length tpairs, [], prop2);
  1734   in
  1735     Thm (deriv_rule1 (Proofterm.legacy_freezeT prop1) der,
  1736      {cert = cert,
  1737       tags = [],
  1738       maxidx = maxidx_of_term prop2,
  1739       constraints = constraints,
  1740       shyps = shyps,
  1741       hyps = hyps,
  1742       tpairs = rev (map Logic.dest_equals ts),
  1743       prop = prop3})
  1744   end;
  1745 
  1746 fun plain_prop_of raw_thm =
  1747   let
  1748     val thm = strip_shyps raw_thm;
  1749     fun err msg = raise THM ("plain_prop_of: " ^ msg, 0, [thm]);
  1750   in
  1751     if not (null (hyps_of thm)) then
  1752       err "theorem may not contain hypotheses"
  1753     else if not (null (extra_shyps thm)) then
  1754       err "theorem may not contain sort hypotheses"
  1755     else if not (null (tpairs_of thm)) then
  1756       err "theorem may not contain flex-flex pairs"
  1757     else prop_of thm
  1758   end;
  1759 
  1760 
  1761 
  1762 (*** Inference rules for tactics ***)
  1763 
  1764 (*Destruct proof state into constraints, other goals, goal(i), rest *)
  1765 fun dest_state (state as Thm (_, {prop,tpairs,...}), i) =
  1766   (case  Logic.strip_prems(i, [], prop) of
  1767       (B::rBs, C) => (tpairs, rev rBs, B, C)
  1768     | _ => raise THM("dest_state", i, [state]))
  1769   handle TERM _ => raise THM("dest_state", i, [state]);
  1770 
  1771 (*Prepare orule for resolution by lifting it over the parameters and
  1772 assumptions of goal.*)
  1773 fun lift_rule goal orule =
  1774   let
  1775     val Cterm {t = gprop, T, maxidx = gmax, sorts, ...} = goal;
  1776     val inc = gmax + 1;
  1777     val lift_abs = Logic.lift_abs inc gprop;
  1778     val lift_all = Logic.lift_all inc gprop;
  1779     val Thm (der, {maxidx, constraints, shyps, hyps, tpairs, prop, ...}) = orule;
  1780     val (As, B) = Logic.strip_horn prop;
  1781   in
  1782     if T <> propT then raise THM ("lift_rule: the term must have type prop", 0, [])
  1783     else
  1784       Thm (deriv_rule1 (Proofterm.lift_proof gprop inc prop) der,
  1785        {cert = join_certificate1 (goal, orule),
  1786         tags = [],
  1787         maxidx = maxidx + inc,
  1788         constraints = constraints,
  1789         shyps = Sorts.union shyps sorts,  (*sic!*)
  1790         hyps = hyps,
  1791         tpairs = map (apply2 lift_abs) tpairs,
  1792         prop = Logic.list_implies (map lift_all As, lift_all B)})
  1793   end;
  1794 
  1795 fun incr_indexes i (thm as Thm (der, {cert, maxidx, constraints, shyps, hyps, tpairs, prop, ...})) =
  1796   if i < 0 then raise THM ("negative increment", 0, [thm])
  1797   else if i = 0 then thm
  1798   else
  1799     Thm (deriv_rule1 (Proofterm.incr_indexes i) der,
  1800      {cert = cert,
  1801       tags = [],
  1802       maxidx = maxidx + i,
  1803       constraints = constraints,
  1804       shyps = shyps,
  1805       hyps = hyps,
  1806       tpairs = map (apply2 (Logic.incr_indexes ([], [], i))) tpairs,
  1807       prop = Logic.incr_indexes ([], [], i) prop});
  1808 
  1809 (*Solve subgoal Bi of proof state B1...Bn/C by assumption. *)
  1810 fun assumption opt_ctxt i state =
  1811   let
  1812     val Thm (der, {cert, maxidx, constraints, shyps, hyps, ...}) = state;
  1813     val (context, cert') = make_context_certificate [state] opt_ctxt cert;
  1814     val (tpairs, Bs, Bi, C) = dest_state (state, i);
  1815     fun newth n (env, tpairs) =
  1816       Thm (deriv_rule1
  1817           ((if Envir.is_empty env then I else Proofterm.norm_proof' env) o
  1818             Proofterm.assumption_proof Bs Bi n) der,
  1819        {tags = [],
  1820         maxidx = Envir.maxidx_of env,
  1821         constraints = insert_constraints_env (Context.certificate_theory cert') env constraints,
  1822         shyps = Envir.insert_sorts env shyps,
  1823         hyps = hyps,
  1824         tpairs =
  1825           if Envir.is_empty env then tpairs
  1826           else map (apply2 (Envir.norm_term env)) tpairs,
  1827         prop =
  1828           if Envir.is_empty env then (*avoid wasted normalizations*)
  1829             Logic.list_implies (Bs, C)
  1830           else (*normalize the new rule fully*)
  1831             Envir.norm_term env (Logic.list_implies (Bs, C)),
  1832         cert = cert'});
  1833 
  1834     val (close, asms, concl) = Logic.assum_problems (~1, Bi);
  1835     val concl' = close concl;
  1836     fun addprfs [] _ = Seq.empty
  1837       | addprfs (asm :: rest) n = Seq.make (fn () => Seq.pull
  1838           (Seq.mapp (newth n)
  1839             (if Term.could_unify (asm, concl) then
  1840               (Unify.unifiers (context, Envir.empty maxidx, (close asm, concl') :: tpairs))
  1841              else Seq.empty)
  1842             (addprfs rest (n + 1))))
  1843   in addprfs asms 1 end;
  1844 
  1845 (*Solve subgoal Bi of proof state B1...Bn/C by assumption.
  1846   Checks if Bi's conclusion is alpha/eta-convertible to one of its assumptions*)
  1847 fun eq_assumption i state =
  1848   let
  1849     val Thm (der, {cert, maxidx, constraints, shyps, hyps, ...}) = state;
  1850     val (tpairs, Bs, Bi, C) = dest_state (state, i);
  1851     val (_, asms, concl) = Logic.assum_problems (~1, Bi);
  1852   in
  1853     (case find_index (fn asm => Envir.aeconv (asm, concl)) asms of
  1854       ~1 => raise THM ("eq_assumption", 0, [state])
  1855     | n =>
  1856         Thm (deriv_rule1 (Proofterm.assumption_proof Bs Bi (n + 1)) der,
  1857          {cert = cert,
  1858           tags = [],
  1859           maxidx = maxidx,
  1860           constraints = constraints,
  1861           shyps = shyps,
  1862           hyps = hyps,
  1863           tpairs = tpairs,
  1864           prop = Logic.list_implies (Bs, C)}))
  1865   end;
  1866 
  1867 
  1868 (*For rotate_tac: fast rotation of assumptions of subgoal i*)
  1869 fun rotate_rule k i state =
  1870   let
  1871     val Thm (der, {cert, maxidx, constraints, shyps, hyps, ...}) = state;
  1872     val (tpairs, Bs, Bi, C) = dest_state (state, i);
  1873     val params = Term.strip_all_vars Bi;
  1874     val rest = Term.strip_all_body Bi;
  1875     val asms = Logic.strip_imp_prems rest
  1876     val concl = Logic.strip_imp_concl rest;
  1877     val n = length asms;
  1878     val m = if k < 0 then n + k else k;
  1879     val Bi' =
  1880       if 0 = m orelse m = n then Bi
  1881       else if 0 < m andalso m < n then
  1882         let val (ps, qs) = chop m asms
  1883         in Logic.list_all (params, Logic.list_implies (qs @ ps, concl)) end
  1884       else raise THM ("rotate_rule", k, [state]);
  1885   in
  1886     Thm (deriv_rule1 (Proofterm.rotate_proof Bs Bi m) der,
  1887      {cert = cert,
  1888       tags = [],
  1889       maxidx = maxidx,
  1890       constraints = constraints,
  1891       shyps = shyps,
  1892       hyps = hyps,
  1893       tpairs = tpairs,
  1894       prop = Logic.list_implies (Bs @ [Bi'], C)})
  1895   end;
  1896 
  1897 
  1898 (*Rotates a rule's premises to the left by k, leaving the first j premises
  1899   unchanged.  Does nothing if k=0 or if k equals n-j, where n is the
  1900   number of premises.  Useful with eresolve_tac and underlies defer_tac*)
  1901 fun permute_prems j k rl =
  1902   let
  1903     val Thm (der, {cert, maxidx, constraints, shyps, hyps, tpairs, prop, ...}) = rl;
  1904     val prems = Logic.strip_imp_prems prop
  1905     and concl = Logic.strip_imp_concl prop;
  1906     val moved_prems = List.drop (prems, j)
  1907     and fixed_prems = List.take (prems, j)
  1908       handle General.Subscript => raise THM ("permute_prems: j", j, [rl]);
  1909     val n_j = length moved_prems;
  1910     val m = if k < 0 then n_j + k else k;
  1911     val prop' =
  1912       if 0 = m orelse m = n_j then prop
  1913       else if 0 < m andalso m < n_j then
  1914         let val (ps, qs) = chop m moved_prems
  1915         in Logic.list_implies (fixed_prems @ qs @ ps, concl) end
  1916       else raise THM ("permute_prems: k", k, [rl]);
  1917   in
  1918     Thm (deriv_rule1 (Proofterm.permute_prems_proof prems j m) der,
  1919      {cert = cert,
  1920       tags = [],
  1921       maxidx = maxidx,
  1922       constraints = constraints,
  1923       shyps = shyps,
  1924       hyps = hyps,
  1925       tpairs = tpairs,
  1926       prop = prop'})
  1927   end;
  1928 
  1929 
  1930 (* strip_apply f B A strips off all assumptions/parameters from A
  1931    introduced by lifting over B, and applies f to remaining part of A*)
  1932 fun strip_apply f =
  1933   let fun strip (Const ("Pure.imp", _) $ _  $ B1)
  1934                 (Const ("Pure.imp", _) $ A2 $ B2) = Logic.mk_implies (A2, strip B1 B2)
  1935         | strip ((c as Const ("Pure.all", _)) $ Abs (_, _, t1))
  1936                 (      Const ("Pure.all", _)  $ Abs (a, T, t2)) = c $ Abs (a, T, strip t1 t2)
  1937         | strip _ A = f A
  1938   in strip end;
  1939 
  1940 fun strip_lifted (Const ("Pure.imp", _) $ _ $ B1)
  1941                  (Const ("Pure.imp", _) $ _ $ B2) = strip_lifted B1 B2
  1942   | strip_lifted (Const ("Pure.all", _) $ Abs (_, _, t1))
  1943                  (Const ("Pure.all", _) $ Abs (_, _, t2)) = strip_lifted t1 t2
  1944   | strip_lifted _ A = A;
  1945 
  1946 (*Use the alist to rename all bound variables and some unknowns in a term
  1947   dpairs = current disagreement pairs;  tpairs = permanent ones (flexflex);
  1948   Preserves unknowns in tpairs and on lhs of dpairs. *)
  1949 fun rename_bvs [] _ _ _ _ = K I
  1950   | rename_bvs al dpairs tpairs B As =
  1951       let
  1952         val add_var = fold_aterms (fn Var ((x, _), _) => insert (op =) x | _ => I);
  1953         val vids = []
  1954           |> fold (add_var o fst) dpairs
  1955           |> fold (add_var o fst) tpairs
  1956           |> fold (add_var o snd) tpairs;
  1957         val vids' = fold (add_var o strip_lifted B) As [];
  1958         (*unknowns appearing elsewhere be preserved!*)
  1959         val al' = distinct ((op =) o apply2 fst)
  1960           (filter_out (fn (x, y) =>
  1961              not (member (op =) vids' x) orelse
  1962              member (op =) vids x orelse member (op =) vids y) al);
  1963         val unchanged = filter_out (AList.defined (op =) al') vids';
  1964         fun del_clashing clash xs _ [] qs =
  1965               if clash then del_clashing false xs xs qs [] else qs
  1966           | del_clashing clash xs ys ((p as (x, y)) :: ps) qs =
  1967               if member (op =) ys y
  1968               then del_clashing true (x :: xs) (x :: ys) ps qs
  1969               else del_clashing clash xs (y :: ys) ps (p :: qs);
  1970         val al'' = del_clashing false unchanged unchanged al' [];
  1971         fun rename (t as Var ((x, i), T)) =
  1972               (case AList.lookup (op =) al'' x of
  1973                  SOME y => Var ((y, i), T)
  1974                | NONE => t)
  1975           | rename (Abs (x, T, t)) =
  1976               Abs (the_default x (AList.lookup (op =) al x), T, rename t)
  1977           | rename (f $ t) = rename f $ rename t
  1978           | rename t = t;
  1979         fun strip_ren f Ai = f rename B Ai
  1980       in strip_ren end;
  1981 
  1982 (*Function to rename bounds/unknowns in the argument, lifted over B*)
  1983 fun rename_bvars dpairs =
  1984   rename_bvs (fold_rev Term.match_bvars dpairs []) dpairs;
  1985 
  1986 
  1987 
  1988 (*** RESOLUTION ***)
  1989 
  1990 (** Lifting optimizations **)
  1991 
  1992 (*strip off pairs of assumptions/parameters in parallel -- they are
  1993   identical because of lifting*)
  1994 fun strip_assums2 (Const("Pure.imp", _) $ _ $ B1,
  1995                    Const("Pure.imp", _) $ _ $ B2) = strip_assums2 (B1,B2)
  1996   | strip_assums2 (Const("Pure.all",_)$Abs(a,T,t1),
  1997                    Const("Pure.all",_)$Abs(_,_,t2)) =
  1998       let val (B1,B2) = strip_assums2 (t1,t2)
  1999       in  (Abs(a,T,B1), Abs(a,T,B2))  end
  2000   | strip_assums2 BB = BB;
  2001 
  2002 
  2003 (*Faster normalization: skip assumptions that were lifted over*)
  2004 fun norm_term_skip env 0 t = Envir.norm_term env t
  2005   | norm_term_skip env n (Const ("Pure.all", _) $ Abs (a, T, t)) =
  2006       let
  2007         val T' = Envir.norm_type (Envir.type_env env) T
  2008         (*Must instantiate types of parameters because they are flattened;
  2009           this could be a NEW parameter*)
  2010       in Logic.all_const T' $ Abs (a, T', norm_term_skip env n t) end
  2011   | norm_term_skip env n (Const ("Pure.imp", _) $ A $ B) =
  2012       Logic.mk_implies (A, norm_term_skip env (n - 1) B)
  2013   | norm_term_skip _ _ _ = error "norm_term_skip: too few assumptions??";
  2014 
  2015 
  2016 (*unify types of schematic variables (non-lifted case)*)
  2017 fun unify_var_types context (th1, th2) env =
  2018   let
  2019     fun unify_vars (T :: Us) = fold (fn U => Pattern.unify_types context (T, U)) Us
  2020       | unify_vars _ = I;
  2021     val add_vars =
  2022       full_prop_of #>
  2023       fold_aterms (fn Var v => Vartab.insert_list (op =) v | _ => I);
  2024     val vars = Vartab.empty |> add_vars th1 |> add_vars th2;
  2025   in SOME (Vartab.fold (unify_vars o #2) vars env) end
  2026   handle Pattern.Unif => NONE;
  2027 
  2028 (*Composition of object rule r=(A1...Am/B) with proof state s=(B1...Bn/C)
  2029   Unifies B with Bi, replacing subgoal i    (1 <= i <= n)
  2030   If match then forbid instantiations in proof state
  2031   If lifted then shorten the dpair using strip_assums2.
  2032   If eres_flg then simultaneously proves A1 by assumption.
  2033   nsubgoal is the number of new subgoals (written m above).
  2034   Curried so that resolution calls dest_state only once.
  2035 *)
  2036 local exception COMPOSE
  2037 in
  2038 fun bicompose_aux opt_ctxt {flatten, match, incremented} (state, (stpairs, Bs, Bi, C), lifted)
  2039                         (eres_flg, orule, nsubgoal) =
  2040  let val Thm (sder, {maxidx=smax, constraints = constraints2, shyps = shyps2, hyps = hyps2, ...}) = state
  2041      and Thm (rder, {maxidx=rmax, constraints = constraints1, shyps = shyps1, hyps = hyps1,
  2042              tpairs=rtpairs, prop=rprop,...}) = orule
  2043          (*How many hyps to skip over during normalization*)
  2044      and nlift = Logic.count_prems (strip_all_body Bi) + (if eres_flg then ~1 else 0)
  2045      val (context, cert) =
  2046        make_context_certificate [state, orule] opt_ctxt (join_certificate2 (state, orule));
  2047      (*Add new theorem with prop = "\<lbrakk>Bs; As\<rbrakk> \<Longrightarrow> C" to thq*)
  2048      fun addth A (As, oldAs, rder', n) ((env, tpairs), thq) =
  2049        let val normt = Envir.norm_term env;
  2050            (*perform minimal copying here by examining env*)
  2051            val (ntpairs, normp) =
  2052              if Envir.is_empty env then (tpairs, (Bs @ As, C))
  2053              else
  2054              let val ntps = map (apply2 normt) tpairs
  2055              in if Envir.above env smax then
  2056                   (*no assignments in state; normalize the rule only*)
  2057                   if lifted
  2058                   then (ntps, (Bs @ map (norm_term_skip env nlift) As, C))
  2059                   else (ntps, (Bs @ map normt As, C))
  2060                 else if match then raise COMPOSE
  2061                 else (*normalize the new rule fully*)
  2062                   (ntps, (map normt (Bs @ As), normt C))
  2063              end
  2064            val constraints' =
  2065              union_constraints constraints1 constraints2
  2066              |> insert_constraints_env (Context.certificate_theory cert) env;
  2067            val th =
  2068              Thm (deriv_rule2
  2069                    ((if Envir.is_empty env then I
  2070                      else if Envir.above env smax then
  2071                        (fn f => fn der => f (Proofterm.norm_proof' env der))
  2072                      else
  2073                        curry op oo (Proofterm.norm_proof' env))
  2074                     (Proofterm.bicompose_proof flatten Bs oldAs As A n (nlift+1))) rder' sder,
  2075                 {tags = [],
  2076                  maxidx = Envir.maxidx_of env,
  2077                  constraints = constraints',
  2078                  shyps = Envir.insert_sorts env (Sorts.union shyps1 shyps2),
  2079                  hyps = union_hyps hyps1 hyps2,
  2080                  tpairs = ntpairs,
  2081                  prop = Logic.list_implies normp,
  2082                  cert = cert})
  2083         in  Seq.cons th thq  end  handle COMPOSE => thq;
  2084      val (rAs,B) = Logic.strip_prems(nsubgoal, [], rprop)
  2085        handle TERM _ => raise THM("bicompose: rule", 0, [orule,state]);
  2086      (*Modify assumptions, deleting n-th if n>0 for e-resolution*)
  2087      fun newAs(As0, n, dpairs, tpairs) =
  2088        let val (As1, rder') =
  2089          if not lifted then (As0, rder)
  2090          else
  2091            let val rename = rename_bvars dpairs tpairs B As0
  2092            in (map (rename strip_apply) As0,
  2093              deriv_rule1 (Proofterm.map_proof_terms (rename K) I) rder)
  2094            end;
  2095        in (map (if flatten then (Logic.flatten_params n) else I) As1, As1, rder', n)
  2096           handle TERM _ =>
  2097           raise THM("bicompose: 1st premise", 0, [orule])
  2098        end;
  2099      val BBi = if lifted then strip_assums2(B,Bi) else (B,Bi);
  2100      val dpairs = BBi :: (rtpairs@stpairs);
  2101 
  2102      (*elim-resolution: try each assumption in turn*)
  2103      fun eres _ [] = raise THM ("bicompose: no premises", 0, [orule, state])
  2104        | eres env (A1 :: As) =
  2105            let
  2106              val A = SOME A1;
  2107              val (close, asms, concl) = Logic.assum_problems (nlift + 1, A1);
  2108              val concl' = close concl;
  2109              fun tryasms [] _ = Seq.empty
  2110                | tryasms (asm :: rest) n =
  2111                    if Term.could_unify (asm, concl) then
  2112                      let val asm' = close asm in
  2113                        (case Seq.pull (Unify.unifiers (context, env, (asm', concl') :: dpairs)) of
  2114                          NONE => tryasms rest (n + 1)
  2115                        | cell as SOME ((_, tpairs), _) =>
  2116                            Seq.it_right (addth A (newAs (As, n, [BBi, (concl', asm')], tpairs)))
  2117                              (Seq.make (fn () => cell),
  2118                               Seq.make (fn () => Seq.pull (tryasms rest (n + 1)))))
  2119                      end
  2120                    else tryasms rest (n + 1);
  2121            in tryasms asms 1 end;
  2122 
  2123      (*ordinary resolution*)
  2124      fun res env =
  2125        (case Seq.pull (Unify.unifiers (context, env, dpairs)) of
  2126          NONE => Seq.empty
  2127        | cell as SOME ((_, tpairs), _) =>
  2128            Seq.it_right (addth NONE (newAs (rev rAs, 0, [BBi], tpairs)))
  2129              (Seq.make (fn () => cell), Seq.empty));
  2130 
  2131      val env0 = Envir.empty (Int.max (rmax, smax));
  2132  in
  2133    (case if incremented then SOME env0 else unify_var_types context (state, orule) env0 of
  2134      NONE => Seq.empty
  2135    | SOME env => if eres_flg then eres env (rev rAs) else res env)
  2136  end;
  2137 end;
  2138 
  2139 fun bicompose opt_ctxt flags arg i state =
  2140   bicompose_aux opt_ctxt flags (state, dest_state (state,i), false) arg;
  2141 
  2142 (*Quick test whether rule is resolvable with the subgoal with hyps Hs
  2143   and conclusion B.  If eres_flg then checks 1st premise of rule also*)
  2144 fun could_bires (Hs, B, eres_flg, rule) =
  2145     let fun could_reshyp (A1::_) = exists (fn H => Term.could_unify (A1, H)) Hs
  2146           | could_reshyp [] = false;  (*no premise -- illegal*)
  2147     in  Term.could_unify(concl_of rule, B) andalso
  2148         (not eres_flg  orelse  could_reshyp (prems_of rule))
  2149     end;
  2150 
  2151 (*Bi-resolution of a state with a list of (flag,rule) pairs.
  2152   Puts the rule above:  rule/state.  Renames vars in the rules. *)
  2153 fun biresolution opt_ctxt match brules i state =
  2154     let val (stpairs, Bs, Bi, C) = dest_state(state,i);
  2155         val lift = lift_rule (cprem_of state i);
  2156         val B = Logic.strip_assums_concl Bi;
  2157         val Hs = Logic.strip_assums_hyp Bi;
  2158         val compose =
  2159           bicompose_aux opt_ctxt {flatten = true, match = match, incremented = true}
  2160             (state, (stpairs, Bs, Bi, C), true);
  2161         fun res [] = Seq.empty
  2162           | res ((eres_flg, rule)::brules) =
  2163               if Config.get_generic (make_context [state] opt_ctxt (cert_of state))
  2164                   Pattern.unify_trace_failure orelse could_bires (Hs, B, eres_flg, rule)
  2165               then Seq.make (*delay processing remainder till needed*)
  2166                   (fn()=> SOME(compose (eres_flg, lift rule, nprems_of rule),
  2167                                res brules))
  2168               else res brules
  2169     in  Seq.flat (res brules)  end;
  2170 
  2171 (*Resolution: exactly one resolvent must be produced*)
  2172 fun tha RSN (i, thb) =
  2173   (case Seq.chop 2 (biresolution NONE false [(false, tha)] i thb) of
  2174     ([th], _) => solve_constraints th
  2175   | ([], _) => raise THM ("RSN: no unifiers", i, [tha, thb])
  2176   | _ => raise THM ("RSN: multiple unifiers", i, [tha, thb]));
  2177 
  2178 (*Resolution: P \<Longrightarrow> Q, Q \<Longrightarrow> R gives P \<Longrightarrow> R*)
  2179 fun tha RS thb = tha RSN (1,thb);
  2180 
  2181 
  2182 
  2183 (**** Type classes ****)
  2184 
  2185 fun standard_tvars thm =
  2186   let
  2187     val thy = theory_of_thm thm;
  2188     val tvars = rev (Term.add_tvars (prop_of thm) []);
  2189     val names = Name.invent Name.context Name.aT (length tvars);
  2190     val tinst =
  2191       map2 (fn (ai, S) => fn b => ((ai, S), global_ctyp_of thy (TVar ((b, 0), S)))) tvars names;
  2192   in instantiate (tinst, []) thm end
  2193 
  2194 
  2195 (* class relations *)
  2196 
  2197 val is_classrel = Symreltab.defined o get_classrels;
  2198 
  2199 fun complete_classrels thy =
  2200   let
  2201     fun complete (c, (_, (all_preds, all_succs))) (finished1, thy1) =
  2202       let
  2203         fun compl c1 c2 (finished2, thy2) =
  2204           if is_classrel thy2 (c1, c2) then (finished2, thy2)
  2205           else
  2206             (false,
  2207               thy2
  2208               |> (map_classrels o Symreltab.update) ((c1, c2),
  2209                 (the_classrel thy2 (c1, c) RS the_classrel thy2 (c, c2))
  2210                 |> standard_tvars
  2211                 |> close_derivation \<^here>
  2212                 |> trim_context));
  2213 
  2214         val proven = is_classrel thy1;
  2215         val preds = Graph.Keys.fold (fn c1 => proven (c1, c) ? cons c1) all_preds [];
  2216         val succs = Graph.Keys.fold (fn c2 => proven (c, c2) ? cons c2) all_succs [];
  2217       in
  2218         fold_product compl preds succs (finished1, thy1)
  2219       end;
  2220   in
  2221     (case Graph.fold complete (Sorts.classes_of (Sign.classes_of thy)) (true, thy) of
  2222       (true, _) => NONE
  2223     | (_, thy') => SOME thy')
  2224   end;
  2225 
  2226 
  2227 (* type arities *)
  2228 
  2229 fun thynames_of_arity thy (a, c) =
  2230   (get_arities thy, []) |-> Aritytab.fold
  2231     (fn ((a', _, c'), (_, name, ser)) => (a = a' andalso c = c') ? cons (name, ser))
  2232   |> sort (int_ord o apply2 #2) |> map #1;
  2233 
  2234 fun insert_arity_completions thy ((t, Ss, c), (th, thy_name, ser)) (finished, arities) =
  2235   let
  2236     val completions =
  2237       Sign.super_classes thy c |> map_filter (fn c1 =>
  2238         if Aritytab.defined arities (t, Ss, c1) then NONE
  2239         else
  2240           let
  2241             val th1 =
  2242               (th RS the_classrel thy (c, c1))
  2243               |> standard_tvars
  2244               |> close_derivation \<^here>
  2245               |> trim_context;
  2246           in SOME ((t, Ss, c1), (th1, thy_name, ser)) end);
  2247     val finished' = finished andalso null completions;
  2248     val arities' = fold Aritytab.update completions arities;
  2249   in (finished', arities') end;
  2250 
  2251 fun complete_arities thy =
  2252   let
  2253     val arities = get_arities thy;
  2254     val (finished, arities') =
  2255       Aritytab.fold (insert_arity_completions thy) arities (true, get_arities thy);
  2256   in
  2257     if finished then NONE
  2258     else SOME (map_arities (K arities') thy)
  2259   end;
  2260 
  2261 val _ =
  2262   Theory.setup
  2263    (Theory.at_begin complete_classrels #>
  2264     Theory.at_begin complete_arities);
  2265 
  2266 
  2267 (* primitive rules *)
  2268 
  2269 fun add_classrel raw_th thy =
  2270   let
  2271     val th = strip_shyps (transfer thy raw_th);
  2272     val prop = plain_prop_of th;
  2273     val (c1, c2) = Logic.dest_classrel prop;
  2274   in
  2275     thy
  2276     |> Sign.primitive_classrel (c1, c2)
  2277     |> map_classrels (Symreltab.update ((c1, c2), th |> unconstrainT |> trim_context))
  2278     |> perhaps complete_classrels
  2279     |> perhaps complete_arities
  2280   end;
  2281 
  2282 fun add_arity raw_th thy =
  2283   let
  2284     val th = strip_shyps (transfer thy raw_th);
  2285     val prop = plain_prop_of th;
  2286     val (t, Ss, c) = Logic.dest_arity prop;
  2287     val ar = ((t, Ss, c), (th |> unconstrainT |> trim_context, Context.theory_name thy, serial ()));
  2288   in
  2289     thy
  2290     |> Sign.primitive_arity (t, Ss, [c])
  2291     |> map_arities (Aritytab.update ar #> curry (insert_arity_completions thy ar) true #> #2)
  2292   end;
  2293 
  2294 end;
  2295 
  2296 structure Basic_Thm: BASIC_THM = Thm;
  2297 open Basic_Thm;