src/Pure/Isar/proof_context.ML
changeset 5819 5fff21d4ca3a
child 5874 a58d4528121d
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Mon Nov 09 15:31:04 1998 +0100
     1.3 @@ -0,0 +1,617 @@
     1.4 +(*  Title:      Pure/Isar/proof_context.ML
     1.5 +    ID:         $Id$
     1.6 +    Author:     Markus Wenzel, TU Muenchen
     1.7 +
     1.8 +Proof context information.
     1.9 +
    1.10 +TODO:
    1.11 +  - pretty_bind: use syntax (!?) (show_types etc.);
    1.12 +  - smash_unifiers: ever invents new vars (???);
    1.13 +*)
    1.14 +
    1.15 +(* FIXME tmp *)
    1.16 +val proof_debug = ref false;
    1.17 +
    1.18 +signature PROOF_CONTEXT =
    1.19 +sig
    1.20 +  type context
    1.21 +  exception CONTEXT of string * context
    1.22 +  val theory_of: context -> theory
    1.23 +  val sign_of: context -> Sign.sg
    1.24 +  val print_binds: context -> unit
    1.25 +  val print_thms: context -> unit
    1.26 +  val print_context: context -> unit
    1.27 +  val print_proof_data: theory -> unit
    1.28 +  val init_context: theory -> context
    1.29 +  val read_typ: context -> string -> typ
    1.30 +  val cert_typ: context -> typ -> typ
    1.31 +  val read_term: context -> string -> term
    1.32 +  val read_prop: context -> string -> term
    1.33 +  val read_pat: context -> string -> term
    1.34 +  val cert_term: context -> term -> term
    1.35 +  val cert_prop: context -> term -> term
    1.36 +  val declare_term: term -> context -> context
    1.37 +  val declare_terms: term list -> context -> context
    1.38 +  val add_binds: (indexname * string) list -> context -> context
    1.39 +  val add_binds_i: (indexname * term) list -> context -> context
    1.40 +  val match_binds: (string * string) list -> context -> context
    1.41 +  val match_binds_i: (term * term) list -> context -> context
    1.42 +  val thms_closure: context -> xstring -> tthm list option
    1.43 +  val get_tthm: context -> string -> tthm
    1.44 +  val get_tthms: context -> string -> tthm list
    1.45 +  val get_tthmss: context -> string list -> tthm list
    1.46 +  val put_tthm: string * tthm -> context -> context
    1.47 +  val put_tthms: string * tthm list -> context -> context
    1.48 +  val put_tthmss: (string * tthm list) list -> context -> context
    1.49 +  val have_tthms: string -> context attribute list
    1.50 +    -> (tthm * context attribute list) list -> context -> context * (string * tthm list)
    1.51 +  val assumptions: context -> tthm list
    1.52 +  val fixed_names: context -> string list
    1.53 +  val assume: string -> context attribute list -> string list -> context
    1.54 +    -> context * (string * tthm list)
    1.55 +  val assume_i: string -> context attribute list -> term list -> context
    1.56 +    -> context * (string * tthm list)
    1.57 +  val fix: (string * string option) list -> context -> context
    1.58 +  val fix_i: (string * typ) list -> context -> context
    1.59 +  val setup: (theory -> theory) list
    1.60 +end;
    1.61 +
    1.62 +signature PROOF_CONTEXT_PRIVATE =
    1.63 +sig
    1.64 +  include PROOF_CONTEXT
    1.65 +  val init_data: Object.kind -> (theory -> Object.T) * (context -> Object.T -> unit)
    1.66 +    -> theory -> theory
    1.67 +  val print_data: Object.kind -> context -> unit
    1.68 +  val get_data: Object.kind -> (Object.T -> 'a) -> context -> 'a
    1.69 +  val put_data: Object.kind -> ('a -> Object.T) -> 'a -> context -> context
    1.70 +end;
    1.71 +
    1.72 +
    1.73 +structure ProofContext: PROOF_CONTEXT_PRIVATE =
    1.74 +struct
    1.75 +
    1.76 +
    1.77 +(** datatype context **)
    1.78 +
    1.79 +datatype context =
    1.80 +  Context of
    1.81 +   {thy: theory,                                (*current theory*)
    1.82 +    data: Object.T Symtab.table,                (*user data*)
    1.83 +    asms:
    1.84 +      (string * tthm list) list *               (*assumes: A ==> _*)
    1.85 +      ((string * string) list * string list),   (*fixes: !!x. _*)
    1.86 +    binds: (term * typ) Vartab.table,           (*term bindings*)
    1.87 +    thms: tthm list Symtab.table,               (*local thms*)
    1.88 +    defs:
    1.89 +      typ Vartab.table *                        (*type constraints*)
    1.90 +      sort Vartab.table *                       (*default sorts*)
    1.91 +      int *					(*maxidx*)
    1.92 +      string list};                             (*used type variable names*)
    1.93 +
    1.94 +exception CONTEXT of string * context;
    1.95 +
    1.96 +
    1.97 +fun make_context (thy, data, asms, binds, thms, defs) =
    1.98 +  Context {thy = thy, data = data, asms = asms, binds = binds, thms = thms, defs = defs};
    1.99 +
   1.100 +fun map_context f (Context {thy, data, asms, binds, thms, defs}) =
   1.101 +  make_context (f (thy, data, asms, binds, thms, defs));
   1.102 +
   1.103 +fun theory_of (Context {thy, ...}) = thy;
   1.104 +val sign_of = Theory.sign_of o theory_of;
   1.105 +
   1.106 +
   1.107 +
   1.108 +(** print context information **)
   1.109 +
   1.110 +(* FIXME tmp*)
   1.111 +fun debug f x = if ! proof_debug then f x else ();
   1.112 +
   1.113 +fun print_items prt name items =
   1.114 +  let
   1.115 +    fun pretty_itms (name, [x]) = Pretty.block [Pretty.str (name ^ ":"), Pretty.brk 1, prt x]
   1.116 +      | pretty_itms (name, xs) = Pretty.big_list (name ^ ":") (map prt xs);
   1.117 +  in Pretty.writeln (Pretty.big_list name (map pretty_itms items)) end;
   1.118 +
   1.119 +
   1.120 +(* term bindings *)
   1.121 +
   1.122 +fun print_binds (Context {thy, binds, ...}) =
   1.123 +  let
   1.124 +    val prt_term = Sign.pretty_term (Theory.sign_of thy);
   1.125 +
   1.126 +    fun fix_var (x, i) =
   1.127 +      (case try Syntax.dest_binding x of
   1.128 +        None => Syntax.string_of_vname (x, i)
   1.129 +      | Some x' => if i = 0 then "??" ^ x' else Syntax.string_of_vname (x, i));
   1.130 +    fun pretty_bind (xi, (t, T)) = Pretty.block
   1.131 +      [Pretty.str (fix_var xi), Pretty.str " ==", Pretty.brk 1, prt_term t];
   1.132 +  in Pretty.writeln (Pretty.big_list "Term bindings:" (map pretty_bind (Vartab.dest binds))) end;
   1.133 +
   1.134 +
   1.135 +(* local theorems *)
   1.136 +
   1.137 +fun print_thms (Context {thms, ...}) =
   1.138 +  print_items Attribute.pretty_tthm "Local theorems:" (Symtab.dest thms);
   1.139 +
   1.140 +
   1.141 +(* main context *)
   1.142 +
   1.143 +fun print_context (ctxt as Context {thy, data = _, asms = (assumes, (fixes, _)), binds = _,
   1.144 +    thms = _, defs = (types, sorts, maxidx, used)}) =
   1.145 +  let
   1.146 +    val sign = Theory.sign_of thy;
   1.147 +
   1.148 +    val term_of_tthm = #prop o Thm.rep_thm o Attribute.thm_of;
   1.149 +    val prt_term = Sign.pretty_term sign;
   1.150 +    val prt_typ = Sign.pretty_typ sign;
   1.151 +    val prt_sort = Sign.pretty_sort sign;
   1.152 +
   1.153 +    (*theory*)
   1.154 +    val pretty_thy = Pretty.block [Pretty.str "Theory:", Pretty.brk 1, Sign.pretty_sg sign];
   1.155 +
   1.156 +    (*fixes*)
   1.157 +    fun prt_fix (x, x') = Pretty.str (x ^ " = " ^ x');
   1.158 +
   1.159 +    (* defaults *)
   1.160 +
   1.161 +    fun prt_atom prt prtT (x, X) = Pretty.block
   1.162 +      [prt x, Pretty.str " ::", Pretty.brk 1, prtT X];
   1.163 +
   1.164 +    fun prt_var (x, ~1) = prt_term (Syntax.free x)
   1.165 +      | prt_var xi = prt_term (Syntax.var xi);
   1.166 +
   1.167 +    fun prt_varT (x, ~1) = prt_typ (TFree (x, []))
   1.168 +      | prt_varT xi = prt_typ (TVar (xi, []));
   1.169 +
   1.170 +    val prt_defT = prt_atom prt_var prt_typ;
   1.171 +    val prt_defS = prt_atom prt_varT prt_sort;
   1.172 +  in
   1.173 +    debug Pretty.writeln pretty_thy;
   1.174 +    Pretty.writeln (Pretty.big_list "Fixed variables:" (map prt_fix (rev fixes)));
   1.175 +    print_items (prt_term o term_of_tthm) "Assumptions:" assumes;
   1.176 +    debug print_binds ctxt;
   1.177 +    debug print_thms ctxt;
   1.178 +    debug Pretty.writeln (Pretty.big_list "Type constraints:" (map prt_defT (Vartab.dest types)));
   1.179 +    debug Pretty.writeln (Pretty.big_list "Default sorts:" (map prt_defS (Vartab.dest sorts)));
   1.180 +    debug writeln ("Maxidx: " ^ string_of_int maxidx);
   1.181 +    debug Pretty.writeln (Pretty.strs ("Used type variable names:" :: used))
   1.182 +  end;
   1.183 +
   1.184 +
   1.185 +
   1.186 +(** user data **)
   1.187 +
   1.188 +(* errors *)
   1.189 +
   1.190 +fun of_theory thy = "\nof theory " ^ Sign.str_of_sg (Theory.sign_of thy);
   1.191 +
   1.192 +fun err_inconsistent kinds =
   1.193 +  error ("Attempt to merge different versions of " ^ commas_quote kinds ^ " proof data");
   1.194 +
   1.195 +fun err_dup_init thy kind =
   1.196 +  error ("Duplicate initialization of " ^ quote kind ^ " proof data" ^ of_theory thy);
   1.197 +
   1.198 +fun err_undef ctxt kind =
   1.199 +  raise CONTEXT ("Tried to access undefined " ^ quote kind ^ " proof data", ctxt);
   1.200 +
   1.201 +fun err_uninit ctxt kind =
   1.202 +  raise CONTEXT ("Tried to access uninitialized " ^ quote kind ^ " proof data" ^
   1.203 +    of_theory (theory_of ctxt), ctxt);
   1.204 +
   1.205 +fun err_access ctxt kind =
   1.206 +  raise CONTEXT ("Unauthorized access to " ^ quote kind ^ " proof data" ^
   1.207 +    of_theory (theory_of ctxt), ctxt);
   1.208 +
   1.209 +
   1.210 +(* data kind 'Isar/proof_data' *)
   1.211 +
   1.212 +structure ProofDataDataArgs =
   1.213 +struct
   1.214 +  val name = "Isar/proof_data";
   1.215 +  type T = (Object.kind * ((theory -> Object.T) * (context -> Object.T -> unit))) Symtab.table;
   1.216 +
   1.217 +  val empty = Symtab.empty;
   1.218 +  val prep_ext = I;
   1.219 +  fun merge tabs = Symtab.merge (Object.eq_kind o pairself fst) tabs
   1.220 +    handle Symtab.DUPS kinds => err_inconsistent kinds;
   1.221 +  fun print _ tab = Pretty.writeln (Pretty.strs (map #1 (Symtab.dest tab)));
   1.222 +end;
   1.223 +
   1.224 +structure ProofDataData = TheoryDataFun(ProofDataDataArgs);
   1.225 +val print_proof_data = ProofDataData.print;
   1.226 +
   1.227 +
   1.228 +(* init proof data *)
   1.229 +
   1.230 +fun init_data kind meths thy =
   1.231 +  let
   1.232 +    val name = Object.name_of_kind kind;
   1.233 +    val tab = Symtab.update_new ((name, (kind, meths)), ProofDataData.get thy)
   1.234 +      handle Symtab.DUP _ => err_dup_init thy name;
   1.235 +  in thy |> ProofDataData.put tab end;
   1.236 +
   1.237 +
   1.238 +(* access data *)
   1.239 +
   1.240 +fun lookup_data (ctxt as Context {data, ...}) kind =
   1.241 +  let
   1.242 +    val thy = theory_of ctxt;
   1.243 +    val name = Object.name_of_kind kind;
   1.244 +  in
   1.245 +    (case Symtab.lookup (ProofDataData.get thy, name) of
   1.246 +      Some (k, meths) =>
   1.247 +        if Object.eq_kind (kind, k) then
   1.248 +          (case Symtab.lookup (data, name) of
   1.249 +            Some x => (x, meths)
   1.250 +          | None => err_undef ctxt name)
   1.251 +        else err_access ctxt name
   1.252 +    | None => err_uninit ctxt name)
   1.253 +  end;
   1.254 +
   1.255 +fun get_data kind f ctxt =
   1.256 +  let val (x, _) = lookup_data ctxt kind
   1.257 +  in f x handle Match => Object.kind_error kind end;
   1.258 +
   1.259 +fun print_data kind ctxt =
   1.260 +  let val (x, (_, prt)) = lookup_data ctxt kind
   1.261 +  in prt ctxt x end;
   1.262 +
   1.263 +fun put_data kind f x ctxt =
   1.264 +  (lookup_data ctxt kind;
   1.265 +    ctxt |> map_context (fn (thy, data, asms, binds, thms, defs) =>
   1.266 +      (thy, Symtab.update ((Object.name_of_kind kind, f x), data), asms, binds, thms, defs)));
   1.267 +
   1.268 +
   1.269 +(* init context *)
   1.270 +
   1.271 +fun init_context thy =
   1.272 +  let val data = Symtab.map (fn (_, (init, _)) => init thy) (ProofDataData.get thy) in
   1.273 +    make_context (thy, data, ([], ([], [])), Vartab.empty, Symtab.empty,
   1.274 +      (Vartab.empty, Vartab.empty, ~1, []))
   1.275 +  end;
   1.276 +
   1.277 +
   1.278 +
   1.279 +(** prepare types **)
   1.280 +
   1.281 +fun read_typ (ctxt as Context {defs = (_, sorts, _, _), ...}) s =
   1.282 +  let
   1.283 +    val sign = sign_of ctxt;
   1.284 +    fun def_sort xi = Vartab.lookup (sorts, xi);
   1.285 +  in
   1.286 +    transform_error (Sign.read_typ (sign, def_sort)) s
   1.287 +      handle ERROR_MESSAGE msg => raise CONTEXT (msg, ctxt)
   1.288 +  end;
   1.289 +
   1.290 +fun cert_typ ctxt raw_T =
   1.291 +  Sign.certify_typ (sign_of ctxt) raw_T
   1.292 +    handle TYPE (msg, _, _) => raise CONTEXT (msg, ctxt);
   1.293 +
   1.294 +
   1.295 +
   1.296 +(** prepare terms and propositions **)
   1.297 +
   1.298 +(*
   1.299 +  (1) read / certify wrt. signature of context
   1.300 +  (2) intern Skolem constants
   1.301 +  (3) expand term bindings
   1.302 +*)
   1.303 +
   1.304 +
   1.305 +(* read / certify wrt. signature *)     (*exception ERROR*) (*exception TERM*)
   1.306 +
   1.307 +fun read_def_termT sg (types, sorts, used) (s, T) =
   1.308 +  Thm.term_of (#1 (Thm.read_def_cterm (sg, types, sorts) used true (s, T)));
   1.309 +
   1.310 +fun read_term_sg sg (defs as (_, _, used)) s =
   1.311 +  read_def_termT sg defs (s, TVar ((variant used "'z", 0), logicS));
   1.312 +
   1.313 +fun read_prop_sg sg defs s = read_def_termT sg defs (s, propT);
   1.314 +
   1.315 +
   1.316 +fun cert_term_sg sg t = Thm.term_of (Thm.cterm_of sg t);
   1.317 +
   1.318 +fun cert_prop_sg sg tm =
   1.319 +  let
   1.320 +    val ctm = Thm.cterm_of sg tm;
   1.321 +    val {t, T, ...} = Thm.rep_cterm ctm;
   1.322 +  in
   1.323 +    if T = propT then t
   1.324 +    else raise TERM ("Term not of type prop", [t])
   1.325 +  end;
   1.326 +
   1.327 +
   1.328 +(* intern_skolem *)
   1.329 +
   1.330 +fun get_skolem (Context {asms = (_, (fixes, _)), ...}) x = assoc (fixes, x);
   1.331 +
   1.332 +fun check_skolem ctxt check x =
   1.333 +  if check andalso can Syntax.dest_skolem x then
   1.334 +    raise CONTEXT ("Illegal reference to internal Skolem constant: " ^ quote x, ctxt)
   1.335 +  else x;
   1.336 +
   1.337 +fun intern_skolem ctxt check =
   1.338 +  let
   1.339 +    fun intern (t as Free (x, T)) =
   1.340 +          (case get_skolem ctxt (check_skolem ctxt check x) of
   1.341 +            Some x' => Free (x', T)
   1.342 +          | None => t)
   1.343 +      | intern (t $ u) = intern t $ intern u
   1.344 +      | intern (Abs (x, T, t)) = Abs (x, T, intern t)
   1.345 +      | intern a = a;
   1.346 +  in intern end;
   1.347 +
   1.348 +
   1.349 +(* norm_term *)
   1.350 +
   1.351 +(*beta normal form for terms (not eta normal form), chase variables in
   1.352 +  bindings environment (code taken from Pure/envir.ML)*)
   1.353 +
   1.354 +fun norm_term (ctxt as Context {binds, ...}) =
   1.355 +  let
   1.356 +    (*raised when norm has no effect on a term, to do sharing instead of copying*)
   1.357 +    exception SAME;
   1.358 +
   1.359 +    fun norm (t as Var (xi, T)) =
   1.360 +          (case Vartab.lookup (binds, xi) of
   1.361 +            Some (u, U) =>
   1.362 +              if T = U then (norm u handle SAME => u)
   1.363 +              else raise TYPE ("norm_term: ill-typed variable assigment", [T, U], [t, u])
   1.364 +          | None =>
   1.365 +              if can Syntax.dest_binding (#1 xi) then
   1.366 +                raise CONTEXT ("Unbound binding: " ^ Syntax.string_of_vname xi, ctxt)
   1.367 +              else raise SAME)
   1.368 +      | norm (Abs (a, T, body)) =  Abs (a, T, norm body)
   1.369 +      | norm (Abs (_, _, body) $ t) = normh (subst_bound (t, body))
   1.370 +      | norm (f $ t) =
   1.371 +          ((case norm f of
   1.372 +            Abs (_, _, body) => normh (subst_bound (t, body))
   1.373 +          | nf => nf $ (norm t handle SAME => t)) handle SAME => f $ norm t)
   1.374 +      | norm _ =  raise SAME
   1.375 +    and normh t = norm t handle SAME => t
   1.376 +  in normh end;
   1.377 +
   1.378 +
   1.379 +(* read terms *)
   1.380 +
   1.381 +fun gen_read read is_pat (ctxt as Context {binds, defs = (types, sorts, _, used), ...}) s =
   1.382 +  let
   1.383 +    val sign = sign_of ctxt;
   1.384 +
   1.385 +    fun def_type xi =
   1.386 +      (case Vartab.lookup (types, xi) of
   1.387 +        None => if is_pat then None else apsome #2 (Vartab.lookup (binds, xi))
   1.388 +      | some => some);
   1.389 +
   1.390 +    fun def_sort xi = Vartab.lookup (sorts, xi);
   1.391 +  in
   1.392 +    (transform_error (read sign (def_type, def_sort, used)) s
   1.393 +      handle TERM (msg, _) => raise CONTEXT (msg, ctxt)
   1.394 +      | ERROR_MESSAGE msg => raise CONTEXT (msg, ctxt))
   1.395 +    |> intern_skolem ctxt true
   1.396 +    |> (if is_pat then I else norm_term ctxt)
   1.397 +  end;
   1.398 +
   1.399 +val read_term = gen_read read_term_sg false;
   1.400 +val read_prop = gen_read read_prop_sg false;
   1.401 +val read_pat = gen_read read_term_sg true;
   1.402 +
   1.403 +
   1.404 +(* certify terms *)
   1.405 +
   1.406 +fun gen_cert cert is_pat ctxt t =
   1.407 +  (cert (sign_of ctxt) t handle TERM (msg, _) => raise CONTEXT (msg, ctxt))
   1.408 +  |> intern_skolem ctxt false
   1.409 +  |> (if is_pat then I else norm_term ctxt);
   1.410 +
   1.411 +val cert_term = gen_cert cert_term_sg false;
   1.412 +val cert_prop = gen_cert cert_prop_sg false;
   1.413 +val cert_pat = gen_cert cert_term_sg true;
   1.414 +
   1.415 +
   1.416 +(* declare terms *)
   1.417 +
   1.418 +val ins_types = foldl_aterms
   1.419 +  (fn (types, Free (x, T)) => Vartab.update (((x, ~1), T), types)
   1.420 +    | (types, Var v) => Vartab.update (v, types)
   1.421 +    | (types, _) => types);
   1.422 +
   1.423 +val ins_sorts = foldl_types (foldl_atyps
   1.424 +  (fn (sorts, TFree (x, S)) => Vartab.update (((x, ~1), S), sorts)
   1.425 +    | (sorts, TVar v) => Vartab.update (v, sorts)
   1.426 +    | (sorts, _) => sorts));
   1.427 +
   1.428 +val ins_used = foldl_types (foldl_atyps
   1.429 +  (fn (used, TFree (x, _)) => x ins used
   1.430 +    | (used, TVar ((x, _), _)) => x ins used
   1.431 +    | (used, _) => used));
   1.432 +
   1.433 +fun map_defaults f = map_context
   1.434 +  (fn (thy, data, asms, binds, thms, defs) => (thy, data, asms, binds, thms, f defs));
   1.435 +
   1.436 +fun declare (ctxt, t) =
   1.437 +  ctxt
   1.438 +  |> map_defaults (fn (types, sorts, maxidx, used) => (ins_types (types, t), sorts, maxidx, used))
   1.439 +  |> map_defaults (fn (types, sorts, maxidx, used) => (types, ins_sorts (sorts, t), maxidx, used))
   1.440 +  |> map_defaults (fn (types, sorts, maxidx, used) => (types, sorts, maxidx, ins_used (used, t)))
   1.441 +  |> map_defaults (fn (types, sorts, maxidx, used) =>
   1.442 +      (types, sorts, Int.max (maxidx, Term.maxidx_of_term t), used));
   1.443 +
   1.444 +
   1.445 +fun declare_term t ctxt = declare (ctxt, t);
   1.446 +fun declare_terms ts ctxt = foldl declare (ctxt, ts);
   1.447 +
   1.448 +fun prep_declare prep (ctxt, s) =
   1.449 +  let val t = prep ctxt s
   1.450 +  in (ctxt |> declare_term t, t) end;
   1.451 +
   1.452 +
   1.453 +
   1.454 +(** bindings **)
   1.455 +
   1.456 +(* update_binds *)
   1.457 +
   1.458 +fun upd_bind (ctxt, (xi, t)) =
   1.459 +  let val T = fastype_of t in
   1.460 +    ctxt
   1.461 +    |> declare_term t
   1.462 +    |> map_context (fn (thy, data, asms, binds, thms, defs) =>
   1.463 +        (thy, data, asms, Vartab.update ((xi, (t, T)), binds), thms, defs))
   1.464 +  end;
   1.465 +
   1.466 +fun update_binds bs ctxt = foldl upd_bind (ctxt, bs);
   1.467 +fun update_binds_env env = update_binds (Envir.alist_of env);
   1.468 +
   1.469 +
   1.470 +(* add_binds(_i) -- sequential *)
   1.471 +
   1.472 +fun gen_bind prep (ctxt, (xi as (x, _), raw_t)) =
   1.473 +  let val t = prep ctxt raw_t in
   1.474 +    if can Syntax.dest_binding x then ctxt |> update_binds [(xi, t)]
   1.475 +    else raise CONTEXT ("Illegal variable name for term binding: " ^
   1.476 +      quote (Syntax.string_of_vname xi), ctxt)
   1.477 +  end;
   1.478 +
   1.479 +fun gen_binds prep binds ctxt = foldl (gen_bind prep) (ctxt, binds);
   1.480 +
   1.481 +val add_binds = gen_binds read_term;
   1.482 +val add_binds_i = gen_binds cert_term;
   1.483 +
   1.484 +
   1.485 +(* match_binds(_i) -- parallel *)
   1.486 +
   1.487 +fun prep_pair prep_pat prep (ctxt, (raw_pat, raw_t)) =
   1.488 +  let
   1.489 +    val pat = prep_pat ctxt raw_pat;
   1.490 +    val (ctxt', t) = prep_declare prep (ctxt, raw_t);
   1.491 +  in (ctxt', (pat, t)) end;
   1.492 +
   1.493 +fun gen_match_binds prep_pat prep raw_pairs ctxt =
   1.494 +  let
   1.495 +    val (ctxt', pairs) = foldl_map (prep_pair prep_pat prep) (ctxt, raw_pairs);
   1.496 +    val Context {defs = (_, _, maxidx, _), ...} = ctxt';
   1.497 +    val envs = Unify.smash_unifiers (sign_of ctxt', Envir.empty maxidx, pairs);
   1.498 +    val env =
   1.499 +      (case Seq.pull envs of
   1.500 +        None => raise CONTEXT ("Pattern match failed!", ctxt')
   1.501 +      | Some (env, _) => env);
   1.502 +  in ctxt' |> update_binds_env env end;
   1.503 +
   1.504 +val match_binds = gen_match_binds read_pat read_term;
   1.505 +val match_binds_i = gen_match_binds cert_pat cert_term;
   1.506 +
   1.507 +
   1.508 +
   1.509 +(** theorems **)
   1.510 +
   1.511 +(* thms_closure *)
   1.512 +
   1.513 +fun thms_closure (Context {thy, thms, ...}) =
   1.514 +  let
   1.515 +    val global_closure = PureThy.thms_closure thy;
   1.516 +    fun get name =
   1.517 +      (case global_closure name of
   1.518 +        None => Symtab.lookup (thms, name)
   1.519 +      | some => some);
   1.520 +  in get end;
   1.521 +
   1.522 +
   1.523 +(* get_tthm(s) *)
   1.524 +
   1.525 +fun get_tthm (ctxt as Context {thy, thms, ...}) name =
   1.526 +  (case Symtab.lookup (thms, name) of
   1.527 +    Some [th] => th
   1.528 +  | Some _ => raise CONTEXT ("Single theorem expected: " ^ quote name, ctxt)
   1.529 +  | None => (PureThy.get_tthm thy name handle THEORY (msg, _) => raise CONTEXT (msg, ctxt)));
   1.530 +
   1.531 +fun get_tthms (ctxt as Context {thy, thms, ...}) name =
   1.532 +  (case Symtab.lookup (thms, name) of
   1.533 +    Some ths => ths
   1.534 +  | None => (PureThy.get_tthms thy name handle THEORY (msg, _) => raise CONTEXT (msg, ctxt)));
   1.535 +
   1.536 +fun get_tthmss ctxt names = flat (map (get_tthms ctxt) names);
   1.537 +
   1.538 +
   1.539 +(* put_tthm(s) *)
   1.540 +
   1.541 +fun put_tthms (name, ths) = map_context
   1.542 +  (fn (thy, data, asms, binds, thms, defs) =>
   1.543 +    (thy, data, asms, binds, Symtab.update ((name, ths), thms), defs));
   1.544 +
   1.545 +fun put_tthm (name, th) = put_tthms (name, [th]);
   1.546 +
   1.547 +fun put_tthmss [] ctxt = ctxt
   1.548 +  | put_tthmss (th :: ths) ctxt = ctxt |> put_tthms th |> put_tthmss ths;
   1.549 +
   1.550 +
   1.551 +(* have_tthms *)
   1.552 +
   1.553 +fun have_tthms name more_attrs ths_attrs ctxt =
   1.554 +  let
   1.555 +    fun app ((ct, ths), (th, attrs)) =
   1.556 +      let val (ct', th') = Attribute.apply ((ct, th), attrs @ more_attrs)
   1.557 +      in (ct', th' :: ths) end
   1.558 +    val (ctxt', rev_thms) = foldl app ((ctxt, []), ths_attrs);
   1.559 +    val thms = rev rev_thms;
   1.560 +  in (ctxt' |> put_tthms (name, thms), (name, thms)) end;
   1.561 +
   1.562 +
   1.563 +
   1.564 +(** assumptions **)
   1.565 +
   1.566 +(* get assumptions *)
   1.567 +
   1.568 +fun assumptions (Context {asms = (asms, _), ...}) = flat (map #2 asms);
   1.569 +fun fixed_names (Context {asms = (_, (fixes, _)), ...}) = map #2 fixes;
   1.570 +
   1.571 +
   1.572 +(* assume *)
   1.573 +
   1.574 +fun gen_assume prep name attrs raw_props ctxt =
   1.575 +  let
   1.576 +    val (ctxt', props) = foldl_map prep (ctxt, raw_props);
   1.577 +    val sign = sign_of ctxt';
   1.578 +    val ths = map (fn t => ((Thm.assume (Thm.cterm_of sign t), []), [])) props;
   1.579 +
   1.580 +    val (ctxt'', (_, tthms)) =
   1.581 +      ctxt'
   1.582 +      |> have_tthms name (Attribute.tag_assumption :: attrs) ths
   1.583 +
   1.584 +    val ctxt''' =
   1.585 +      ctxt''
   1.586 +      |> map_context (fn (thy, data, (assumes, fixes), binds, thms, defs) =>
   1.587 +        (thy, data, (assumes @ [(name, tthms)], fixes), binds, thms, defs));
   1.588 +  in (ctxt''', (name, tthms)) end;
   1.589 +
   1.590 +val assume = gen_assume (prep_declare read_prop);
   1.591 +val assume_i = gen_assume (prep_declare cert_prop);
   1.592 +
   1.593 +
   1.594 +(* fix *)
   1.595 +
   1.596 +fun read_skolemT (Context {defs = (_, _, _, used), ...}) None = Type.param used ("'z", logicS)
   1.597 +  | read_skolemT ctxt (Some s) = read_typ ctxt s;
   1.598 +
   1.599 +fun gen_fix prep check (ctxt, (x, raw_T)) =
   1.600 +  ctxt
   1.601 +  |> declare_term (Free (check_skolem ctxt check x, prep ctxt raw_T))
   1.602 +  |> map_context (fn (thy, data, (assumes, (fixes, names)), binds, thms, defs) =>
   1.603 +      let val x' = variant names x in
   1.604 +        (thy, data, (assumes, ((x, Syntax.skolem x') :: fixes, x' :: names)), binds, thms, defs)
   1.605 +      end);
   1.606 +
   1.607 +fun gen_fixs prep check xs ctxt = foldl (gen_fix prep check) (ctxt, xs);
   1.608 +
   1.609 +
   1.610 +val fix = gen_fixs read_skolemT true;
   1.611 +val fix_i = gen_fixs cert_typ false;
   1.612 +
   1.613 +
   1.614 +
   1.615 +(** theory setup **)
   1.616 +
   1.617 +val setup = [ProofDataData.init];
   1.618 +
   1.619 +
   1.620 +end;