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