src/Pure/Isar/proof_context.ML
author wenzelm
Mon Nov 09 15:31:04 1998 +0100 (1998-11-09)
changeset 5819 5fff21d4ca3a
child 5874 a58d4528121d
permissions -rw-r--r--
Proof context information.
     1 (*  Title:      Pure/Isar/proof_context.ML
     2     ID:         $Id$
     3     Author:     Markus Wenzel, TU Muenchen
     4 
     5 Proof context information.
     6 
     7 TODO:
     8   - pretty_bind: use syntax (!?) (show_types etc.);
     9   - smash_unifiers: ever invents new vars (???);
    10 *)
    11 
    12 (* FIXME tmp *)
    13 val proof_debug = ref false;
    14 
    15 signature PROOF_CONTEXT =
    16 sig
    17   type context
    18   exception CONTEXT of string * context
    19   val theory_of: context -> theory
    20   val sign_of: context -> Sign.sg
    21   val print_binds: context -> unit
    22   val print_thms: context -> unit
    23   val print_context: context -> unit
    24   val print_proof_data: theory -> unit
    25   val init_context: theory -> context
    26   val read_typ: context -> string -> typ
    27   val cert_typ: context -> typ -> typ
    28   val read_term: context -> string -> term
    29   val read_prop: context -> string -> term
    30   val read_pat: context -> string -> term
    31   val cert_term: context -> term -> term
    32   val cert_prop: context -> term -> term
    33   val declare_term: term -> context -> context
    34   val declare_terms: term list -> context -> context
    35   val add_binds: (indexname * string) list -> context -> context
    36   val add_binds_i: (indexname * term) list -> context -> context
    37   val match_binds: (string * string) list -> context -> context
    38   val match_binds_i: (term * term) list -> context -> context
    39   val thms_closure: context -> xstring -> tthm list option
    40   val get_tthm: context -> string -> tthm
    41   val get_tthms: context -> string -> tthm list
    42   val get_tthmss: context -> string list -> tthm list
    43   val put_tthm: string * tthm -> context -> context
    44   val put_tthms: string * tthm list -> context -> context
    45   val put_tthmss: (string * tthm list) list -> context -> context
    46   val have_tthms: string -> context attribute list
    47     -> (tthm * context attribute list) list -> context -> context * (string * tthm list)
    48   val assumptions: context -> tthm list
    49   val fixed_names: context -> string list
    50   val assume: string -> context attribute list -> string list -> context
    51     -> context * (string * tthm list)
    52   val assume_i: string -> context attribute list -> term list -> context
    53     -> context * (string * tthm list)
    54   val fix: (string * string option) list -> context -> context
    55   val fix_i: (string * typ) list -> context -> context
    56   val setup: (theory -> theory) list
    57 end;
    58 
    59 signature PROOF_CONTEXT_PRIVATE =
    60 sig
    61   include PROOF_CONTEXT
    62   val init_data: Object.kind -> (theory -> Object.T) * (context -> Object.T -> unit)
    63     -> theory -> theory
    64   val print_data: Object.kind -> context -> unit
    65   val get_data: Object.kind -> (Object.T -> 'a) -> context -> 'a
    66   val put_data: Object.kind -> ('a -> Object.T) -> 'a -> context -> context
    67 end;
    68 
    69 
    70 structure ProofContext: PROOF_CONTEXT_PRIVATE =
    71 struct
    72 
    73 
    74 (** datatype context **)
    75 
    76 datatype context =
    77   Context of
    78    {thy: theory,                                (*current theory*)
    79     data: Object.T Symtab.table,                (*user data*)
    80     asms:
    81       (string * tthm list) list *               (*assumes: A ==> _*)
    82       ((string * string) list * string list),   (*fixes: !!x. _*)
    83     binds: (term * typ) Vartab.table,           (*term bindings*)
    84     thms: tthm list Symtab.table,               (*local thms*)
    85     defs:
    86       typ Vartab.table *                        (*type constraints*)
    87       sort Vartab.table *                       (*default sorts*)
    88       int *					(*maxidx*)
    89       string list};                             (*used type variable names*)
    90 
    91 exception CONTEXT of string * context;
    92 
    93 
    94 fun make_context (thy, data, asms, binds, thms, defs) =
    95   Context {thy = thy, data = data, asms = asms, binds = binds, thms = thms, defs = defs};
    96 
    97 fun map_context f (Context {thy, data, asms, binds, thms, defs}) =
    98   make_context (f (thy, data, asms, binds, thms, defs));
    99 
   100 fun theory_of (Context {thy, ...}) = thy;
   101 val sign_of = Theory.sign_of o theory_of;
   102 
   103 
   104 
   105 (** print context information **)
   106 
   107 (* FIXME tmp*)
   108 fun debug f x = if ! proof_debug then f x else ();
   109 
   110 fun print_items prt name items =
   111   let
   112     fun pretty_itms (name, [x]) = Pretty.block [Pretty.str (name ^ ":"), Pretty.brk 1, prt x]
   113       | pretty_itms (name, xs) = Pretty.big_list (name ^ ":") (map prt xs);
   114   in Pretty.writeln (Pretty.big_list name (map pretty_itms items)) end;
   115 
   116 
   117 (* term bindings *)
   118 
   119 fun print_binds (Context {thy, binds, ...}) =
   120   let
   121     val prt_term = Sign.pretty_term (Theory.sign_of thy);
   122 
   123     fun fix_var (x, i) =
   124       (case try Syntax.dest_binding x of
   125         None => Syntax.string_of_vname (x, i)
   126       | Some x' => if i = 0 then "??" ^ x' else Syntax.string_of_vname (x, i));
   127     fun pretty_bind (xi, (t, T)) = Pretty.block
   128       [Pretty.str (fix_var xi), Pretty.str " ==", Pretty.brk 1, prt_term t];
   129   in Pretty.writeln (Pretty.big_list "Term bindings:" (map pretty_bind (Vartab.dest binds))) end;
   130 
   131 
   132 (* local theorems *)
   133 
   134 fun print_thms (Context {thms, ...}) =
   135   print_items Attribute.pretty_tthm "Local theorems:" (Symtab.dest thms);
   136 
   137 
   138 (* main context *)
   139 
   140 fun print_context (ctxt as Context {thy, data = _, asms = (assumes, (fixes, _)), binds = _,
   141     thms = _, defs = (types, sorts, maxidx, used)}) =
   142   let
   143     val sign = Theory.sign_of thy;
   144 
   145     val term_of_tthm = #prop o Thm.rep_thm o Attribute.thm_of;
   146     val prt_term = Sign.pretty_term sign;
   147     val prt_typ = Sign.pretty_typ sign;
   148     val prt_sort = Sign.pretty_sort sign;
   149 
   150     (*theory*)
   151     val pretty_thy = Pretty.block [Pretty.str "Theory:", Pretty.brk 1, Sign.pretty_sg sign];
   152 
   153     (*fixes*)
   154     fun prt_fix (x, x') = Pretty.str (x ^ " = " ^ x');
   155 
   156     (* defaults *)
   157 
   158     fun prt_atom prt prtT (x, X) = Pretty.block
   159       [prt x, Pretty.str " ::", Pretty.brk 1, prtT X];
   160 
   161     fun prt_var (x, ~1) = prt_term (Syntax.free x)
   162       | prt_var xi = prt_term (Syntax.var xi);
   163 
   164     fun prt_varT (x, ~1) = prt_typ (TFree (x, []))
   165       | prt_varT xi = prt_typ (TVar (xi, []));
   166 
   167     val prt_defT = prt_atom prt_var prt_typ;
   168     val prt_defS = prt_atom prt_varT prt_sort;
   169   in
   170     debug Pretty.writeln pretty_thy;
   171     Pretty.writeln (Pretty.big_list "Fixed variables:" (map prt_fix (rev fixes)));
   172     print_items (prt_term o term_of_tthm) "Assumptions:" assumes;
   173     debug print_binds ctxt;
   174     debug print_thms ctxt;
   175     debug Pretty.writeln (Pretty.big_list "Type constraints:" (map prt_defT (Vartab.dest types)));
   176     debug Pretty.writeln (Pretty.big_list "Default sorts:" (map prt_defS (Vartab.dest sorts)));
   177     debug writeln ("Maxidx: " ^ string_of_int maxidx);
   178     debug Pretty.writeln (Pretty.strs ("Used type variable names:" :: used))
   179   end;
   180 
   181 
   182 
   183 (** user data **)
   184 
   185 (* errors *)
   186 
   187 fun of_theory thy = "\nof theory " ^ Sign.str_of_sg (Theory.sign_of thy);
   188 
   189 fun err_inconsistent kinds =
   190   error ("Attempt to merge different versions of " ^ commas_quote kinds ^ " proof data");
   191 
   192 fun err_dup_init thy kind =
   193   error ("Duplicate initialization of " ^ quote kind ^ " proof data" ^ of_theory thy);
   194 
   195 fun err_undef ctxt kind =
   196   raise CONTEXT ("Tried to access undefined " ^ quote kind ^ " proof data", ctxt);
   197 
   198 fun err_uninit ctxt kind =
   199   raise CONTEXT ("Tried to access uninitialized " ^ quote kind ^ " proof data" ^
   200     of_theory (theory_of ctxt), ctxt);
   201 
   202 fun err_access ctxt kind =
   203   raise CONTEXT ("Unauthorized access to " ^ quote kind ^ " proof data" ^
   204     of_theory (theory_of ctxt), ctxt);
   205 
   206 
   207 (* data kind 'Isar/proof_data' *)
   208 
   209 structure ProofDataDataArgs =
   210 struct
   211   val name = "Isar/proof_data";
   212   type T = (Object.kind * ((theory -> Object.T) * (context -> Object.T -> unit))) Symtab.table;
   213 
   214   val empty = Symtab.empty;
   215   val prep_ext = I;
   216   fun merge tabs = Symtab.merge (Object.eq_kind o pairself fst) tabs
   217     handle Symtab.DUPS kinds => err_inconsistent kinds;
   218   fun print _ tab = Pretty.writeln (Pretty.strs (map #1 (Symtab.dest tab)));
   219 end;
   220 
   221 structure ProofDataData = TheoryDataFun(ProofDataDataArgs);
   222 val print_proof_data = ProofDataData.print;
   223 
   224 
   225 (* init proof data *)
   226 
   227 fun init_data kind meths thy =
   228   let
   229     val name = Object.name_of_kind kind;
   230     val tab = Symtab.update_new ((name, (kind, meths)), ProofDataData.get thy)
   231       handle Symtab.DUP _ => err_dup_init thy name;
   232   in thy |> ProofDataData.put tab end;
   233 
   234 
   235 (* access data *)
   236 
   237 fun lookup_data (ctxt as Context {data, ...}) kind =
   238   let
   239     val thy = theory_of ctxt;
   240     val name = Object.name_of_kind kind;
   241   in
   242     (case Symtab.lookup (ProofDataData.get thy, name) of
   243       Some (k, meths) =>
   244         if Object.eq_kind (kind, k) then
   245           (case Symtab.lookup (data, name) of
   246             Some x => (x, meths)
   247           | None => err_undef ctxt name)
   248         else err_access ctxt name
   249     | None => err_uninit ctxt name)
   250   end;
   251 
   252 fun get_data kind f ctxt =
   253   let val (x, _) = lookup_data ctxt kind
   254   in f x handle Match => Object.kind_error kind end;
   255 
   256 fun print_data kind ctxt =
   257   let val (x, (_, prt)) = lookup_data ctxt kind
   258   in prt ctxt x end;
   259 
   260 fun put_data kind f x ctxt =
   261   (lookup_data ctxt kind;
   262     ctxt |> map_context (fn (thy, data, asms, binds, thms, defs) =>
   263       (thy, Symtab.update ((Object.name_of_kind kind, f x), data), asms, binds, thms, defs)));
   264 
   265 
   266 (* init context *)
   267 
   268 fun init_context thy =
   269   let val data = Symtab.map (fn (_, (init, _)) => init thy) (ProofDataData.get thy) in
   270     make_context (thy, data, ([], ([], [])), Vartab.empty, Symtab.empty,
   271       (Vartab.empty, Vartab.empty, ~1, []))
   272   end;
   273 
   274 
   275 
   276 (** prepare types **)
   277 
   278 fun read_typ (ctxt as Context {defs = (_, sorts, _, _), ...}) s =
   279   let
   280     val sign = sign_of ctxt;
   281     fun def_sort xi = Vartab.lookup (sorts, xi);
   282   in
   283     transform_error (Sign.read_typ (sign, def_sort)) s
   284       handle ERROR_MESSAGE msg => raise CONTEXT (msg, ctxt)
   285   end;
   286 
   287 fun cert_typ ctxt raw_T =
   288   Sign.certify_typ (sign_of ctxt) raw_T
   289     handle TYPE (msg, _, _) => raise CONTEXT (msg, ctxt);
   290 
   291 
   292 
   293 (** prepare terms and propositions **)
   294 
   295 (*
   296   (1) read / certify wrt. signature of context
   297   (2) intern Skolem constants
   298   (3) expand term bindings
   299 *)
   300 
   301 
   302 (* read / certify wrt. signature *)     (*exception ERROR*) (*exception TERM*)
   303 
   304 fun read_def_termT sg (types, sorts, used) (s, T) =
   305   Thm.term_of (#1 (Thm.read_def_cterm (sg, types, sorts) used true (s, T)));
   306 
   307 fun read_term_sg sg (defs as (_, _, used)) s =
   308   read_def_termT sg defs (s, TVar ((variant used "'z", 0), logicS));
   309 
   310 fun read_prop_sg sg defs s = read_def_termT sg defs (s, propT);
   311 
   312 
   313 fun cert_term_sg sg t = Thm.term_of (Thm.cterm_of sg t);
   314 
   315 fun cert_prop_sg sg tm =
   316   let
   317     val ctm = Thm.cterm_of sg tm;
   318     val {t, T, ...} = Thm.rep_cterm ctm;
   319   in
   320     if T = propT then t
   321     else raise TERM ("Term not of type prop", [t])
   322   end;
   323 
   324 
   325 (* intern_skolem *)
   326 
   327 fun get_skolem (Context {asms = (_, (fixes, _)), ...}) x = assoc (fixes, x);
   328 
   329 fun check_skolem ctxt check x =
   330   if check andalso can Syntax.dest_skolem x then
   331     raise CONTEXT ("Illegal reference to internal Skolem constant: " ^ quote x, ctxt)
   332   else x;
   333 
   334 fun intern_skolem ctxt check =
   335   let
   336     fun intern (t as Free (x, T)) =
   337           (case get_skolem ctxt (check_skolem ctxt check x) of
   338             Some x' => Free (x', T)
   339           | None => t)
   340       | intern (t $ u) = intern t $ intern u
   341       | intern (Abs (x, T, t)) = Abs (x, T, intern t)
   342       | intern a = a;
   343   in intern end;
   344 
   345 
   346 (* norm_term *)
   347 
   348 (*beta normal form for terms (not eta normal form), chase variables in
   349   bindings environment (code taken from Pure/envir.ML)*)
   350 
   351 fun norm_term (ctxt as Context {binds, ...}) =
   352   let
   353     (*raised when norm has no effect on a term, to do sharing instead of copying*)
   354     exception SAME;
   355 
   356     fun norm (t as Var (xi, T)) =
   357           (case Vartab.lookup (binds, xi) of
   358             Some (u, U) =>
   359               if T = U then (norm u handle SAME => u)
   360               else raise TYPE ("norm_term: ill-typed variable assigment", [T, U], [t, u])
   361           | None =>
   362               if can Syntax.dest_binding (#1 xi) then
   363                 raise CONTEXT ("Unbound binding: " ^ Syntax.string_of_vname xi, ctxt)
   364               else raise SAME)
   365       | norm (Abs (a, T, body)) =  Abs (a, T, norm body)
   366       | norm (Abs (_, _, body) $ t) = normh (subst_bound (t, body))
   367       | norm (f $ t) =
   368           ((case norm f of
   369             Abs (_, _, body) => normh (subst_bound (t, body))
   370           | nf => nf $ (norm t handle SAME => t)) handle SAME => f $ norm t)
   371       | norm _ =  raise SAME
   372     and normh t = norm t handle SAME => t
   373   in normh end;
   374 
   375 
   376 (* read terms *)
   377 
   378 fun gen_read read is_pat (ctxt as Context {binds, defs = (types, sorts, _, used), ...}) s =
   379   let
   380     val sign = sign_of ctxt;
   381 
   382     fun def_type xi =
   383       (case Vartab.lookup (types, xi) of
   384         None => if is_pat then None else apsome #2 (Vartab.lookup (binds, xi))
   385       | some => some);
   386 
   387     fun def_sort xi = Vartab.lookup (sorts, xi);
   388   in
   389     (transform_error (read sign (def_type, def_sort, used)) s
   390       handle TERM (msg, _) => raise CONTEXT (msg, ctxt)
   391       | ERROR_MESSAGE msg => raise CONTEXT (msg, ctxt))
   392     |> intern_skolem ctxt true
   393     |> (if is_pat then I else norm_term ctxt)
   394   end;
   395 
   396 val read_term = gen_read read_term_sg false;
   397 val read_prop = gen_read read_prop_sg false;
   398 val read_pat = gen_read read_term_sg true;
   399 
   400 
   401 (* certify terms *)
   402 
   403 fun gen_cert cert is_pat ctxt t =
   404   (cert (sign_of ctxt) t handle TERM (msg, _) => raise CONTEXT (msg, ctxt))
   405   |> intern_skolem ctxt false
   406   |> (if is_pat then I else norm_term ctxt);
   407 
   408 val cert_term = gen_cert cert_term_sg false;
   409 val cert_prop = gen_cert cert_prop_sg false;
   410 val cert_pat = gen_cert cert_term_sg true;
   411 
   412 
   413 (* declare terms *)
   414 
   415 val ins_types = foldl_aterms
   416   (fn (types, Free (x, T)) => Vartab.update (((x, ~1), T), types)
   417     | (types, Var v) => Vartab.update (v, types)
   418     | (types, _) => types);
   419 
   420 val ins_sorts = foldl_types (foldl_atyps
   421   (fn (sorts, TFree (x, S)) => Vartab.update (((x, ~1), S), sorts)
   422     | (sorts, TVar v) => Vartab.update (v, sorts)
   423     | (sorts, _) => sorts));
   424 
   425 val ins_used = foldl_types (foldl_atyps
   426   (fn (used, TFree (x, _)) => x ins used
   427     | (used, TVar ((x, _), _)) => x ins used
   428     | (used, _) => used));
   429 
   430 fun map_defaults f = map_context
   431   (fn (thy, data, asms, binds, thms, defs) => (thy, data, asms, binds, thms, f defs));
   432 
   433 fun declare (ctxt, t) =
   434   ctxt
   435   |> map_defaults (fn (types, sorts, maxidx, used) => (ins_types (types, t), sorts, maxidx, used))
   436   |> map_defaults (fn (types, sorts, maxidx, used) => (types, ins_sorts (sorts, t), maxidx, used))
   437   |> map_defaults (fn (types, sorts, maxidx, used) => (types, sorts, maxidx, ins_used (used, t)))
   438   |> map_defaults (fn (types, sorts, maxidx, used) =>
   439       (types, sorts, Int.max (maxidx, Term.maxidx_of_term t), used));
   440 
   441 
   442 fun declare_term t ctxt = declare (ctxt, t);
   443 fun declare_terms ts ctxt = foldl declare (ctxt, ts);
   444 
   445 fun prep_declare prep (ctxt, s) =
   446   let val t = prep ctxt s
   447   in (ctxt |> declare_term t, t) end;
   448 
   449 
   450 
   451 (** bindings **)
   452 
   453 (* update_binds *)
   454 
   455 fun upd_bind (ctxt, (xi, t)) =
   456   let val T = fastype_of t in
   457     ctxt
   458     |> declare_term t
   459     |> map_context (fn (thy, data, asms, binds, thms, defs) =>
   460         (thy, data, asms, Vartab.update ((xi, (t, T)), binds), thms, defs))
   461   end;
   462 
   463 fun update_binds bs ctxt = foldl upd_bind (ctxt, bs);
   464 fun update_binds_env env = update_binds (Envir.alist_of env);
   465 
   466 
   467 (* add_binds(_i) -- sequential *)
   468 
   469 fun gen_bind prep (ctxt, (xi as (x, _), raw_t)) =
   470   let val t = prep ctxt raw_t in
   471     if can Syntax.dest_binding x then ctxt |> update_binds [(xi, t)]
   472     else raise CONTEXT ("Illegal variable name for term binding: " ^
   473       quote (Syntax.string_of_vname xi), ctxt)
   474   end;
   475 
   476 fun gen_binds prep binds ctxt = foldl (gen_bind prep) (ctxt, binds);
   477 
   478 val add_binds = gen_binds read_term;
   479 val add_binds_i = gen_binds cert_term;
   480 
   481 
   482 (* match_binds(_i) -- parallel *)
   483 
   484 fun prep_pair prep_pat prep (ctxt, (raw_pat, raw_t)) =
   485   let
   486     val pat = prep_pat ctxt raw_pat;
   487     val (ctxt', t) = prep_declare prep (ctxt, raw_t);
   488   in (ctxt', (pat, t)) end;
   489 
   490 fun gen_match_binds prep_pat prep raw_pairs ctxt =
   491   let
   492     val (ctxt', pairs) = foldl_map (prep_pair prep_pat prep) (ctxt, raw_pairs);
   493     val Context {defs = (_, _, maxidx, _), ...} = ctxt';
   494     val envs = Unify.smash_unifiers (sign_of ctxt', Envir.empty maxidx, pairs);
   495     val env =
   496       (case Seq.pull envs of
   497         None => raise CONTEXT ("Pattern match failed!", ctxt')
   498       | Some (env, _) => env);
   499   in ctxt' |> update_binds_env env end;
   500 
   501 val match_binds = gen_match_binds read_pat read_term;
   502 val match_binds_i = gen_match_binds cert_pat cert_term;
   503 
   504 
   505 
   506 (** theorems **)
   507 
   508 (* thms_closure *)
   509 
   510 fun thms_closure (Context {thy, thms, ...}) =
   511   let
   512     val global_closure = PureThy.thms_closure thy;
   513     fun get name =
   514       (case global_closure name of
   515         None => Symtab.lookup (thms, name)
   516       | some => some);
   517   in get end;
   518 
   519 
   520 (* get_tthm(s) *)
   521 
   522 fun get_tthm (ctxt as Context {thy, thms, ...}) name =
   523   (case Symtab.lookup (thms, name) of
   524     Some [th] => th
   525   | Some _ => raise CONTEXT ("Single theorem expected: " ^ quote name, ctxt)
   526   | None => (PureThy.get_tthm thy name handle THEORY (msg, _) => raise CONTEXT (msg, ctxt)));
   527 
   528 fun get_tthms (ctxt as Context {thy, thms, ...}) name =
   529   (case Symtab.lookup (thms, name) of
   530     Some ths => ths
   531   | None => (PureThy.get_tthms thy name handle THEORY (msg, _) => raise CONTEXT (msg, ctxt)));
   532 
   533 fun get_tthmss ctxt names = flat (map (get_tthms ctxt) names);
   534 
   535 
   536 (* put_tthm(s) *)
   537 
   538 fun put_tthms (name, ths) = map_context
   539   (fn (thy, data, asms, binds, thms, defs) =>
   540     (thy, data, asms, binds, Symtab.update ((name, ths), thms), defs));
   541 
   542 fun put_tthm (name, th) = put_tthms (name, [th]);
   543 
   544 fun put_tthmss [] ctxt = ctxt
   545   | put_tthmss (th :: ths) ctxt = ctxt |> put_tthms th |> put_tthmss ths;
   546 
   547 
   548 (* have_tthms *)
   549 
   550 fun have_tthms name more_attrs ths_attrs ctxt =
   551   let
   552     fun app ((ct, ths), (th, attrs)) =
   553       let val (ct', th') = Attribute.apply ((ct, th), attrs @ more_attrs)
   554       in (ct', th' :: ths) end
   555     val (ctxt', rev_thms) = foldl app ((ctxt, []), ths_attrs);
   556     val thms = rev rev_thms;
   557   in (ctxt' |> put_tthms (name, thms), (name, thms)) end;
   558 
   559 
   560 
   561 (** assumptions **)
   562 
   563 (* get assumptions *)
   564 
   565 fun assumptions (Context {asms = (asms, _), ...}) = flat (map #2 asms);
   566 fun fixed_names (Context {asms = (_, (fixes, _)), ...}) = map #2 fixes;
   567 
   568 
   569 (* assume *)
   570 
   571 fun gen_assume prep name attrs raw_props ctxt =
   572   let
   573     val (ctxt', props) = foldl_map prep (ctxt, raw_props);
   574     val sign = sign_of ctxt';
   575     val ths = map (fn t => ((Thm.assume (Thm.cterm_of sign t), []), [])) props;
   576 
   577     val (ctxt'', (_, tthms)) =
   578       ctxt'
   579       |> have_tthms name (Attribute.tag_assumption :: attrs) ths
   580 
   581     val ctxt''' =
   582       ctxt''
   583       |> map_context (fn (thy, data, (assumes, fixes), binds, thms, defs) =>
   584         (thy, data, (assumes @ [(name, tthms)], fixes), binds, thms, defs));
   585   in (ctxt''', (name, tthms)) end;
   586 
   587 val assume = gen_assume (prep_declare read_prop);
   588 val assume_i = gen_assume (prep_declare cert_prop);
   589 
   590 
   591 (* fix *)
   592 
   593 fun read_skolemT (Context {defs = (_, _, _, used), ...}) None = Type.param used ("'z", logicS)
   594   | read_skolemT ctxt (Some s) = read_typ ctxt s;
   595 
   596 fun gen_fix prep check (ctxt, (x, raw_T)) =
   597   ctxt
   598   |> declare_term (Free (check_skolem ctxt check x, prep ctxt raw_T))
   599   |> map_context (fn (thy, data, (assumes, (fixes, names)), binds, thms, defs) =>
   600       let val x' = variant names x in
   601         (thy, data, (assumes, ((x, Syntax.skolem x') :: fixes, x' :: names)), binds, thms, defs)
   602       end);
   603 
   604 fun gen_fixs prep check xs ctxt = foldl (gen_fix prep check) (ctxt, xs);
   605 
   606 
   607 val fix = gen_fixs read_skolemT true;
   608 val fix_i = gen_fixs cert_typ false;
   609 
   610 
   611 
   612 (** theory setup **)
   613 
   614 val setup = [ProofDataData.init];
   615 
   616 
   617 end;