src/Pure/Isar/expression.ML
author ballarin
Mon Nov 24 18:03:48 2008 +0100 (2008-11-24)
changeset 28879 db2816a37a34
parent 28872 686963dbf6cd
child 28885 6f6bf52e75bb
permissions -rw-r--r--
Read/cert_statement for theorem statements.
     1 (*  Title:      Pure/Isar/expression.ML
     2     ID:         $Id$
     3     Author:     Clemens Ballarin, TU Muenchen
     4 
     5 New locale development --- experimental.
     6 *)
     7 
     8 signature EXPRESSION =
     9 sig
    10   type 'term map
    11   type 'morph expr
    12 
    13   val empty_expr: 'morph expr
    14 
    15   type expression = (string * string map) expr * (Name.binding * string option * mixfix) list
    16 (*  type expression_i = Morphism.morphism expr * (Name.binding * typ option * mixfix) list *)
    17 
    18   (* Processing of locale statements *)
    19   val read_statement: Element.context list -> (string * string list) list list ->
    20     Proof.context ->  (term * term list) list list * Proof.context;
    21   val cert_statement: Element.context_i list -> (term * term list) list list ->
    22     Proof.context -> (term * term list) list list * Proof.context;
    23 
    24   (* Declaring locales *)
    25   val add_locale: string -> bstring -> expression -> Element.context list -> theory ->
    26     string * Proof.context
    27 (*
    28   val add_locale_i: string -> bstring -> expression_i -> Element.context_i list -> theory ->
    29     string * Proof.context
    30 *)
    31   (* Debugging and development *)
    32   val parse_expression: OuterParse.token list -> expression * OuterParse.token list
    33 end;
    34 
    35 
    36 structure Expression (*: EXPRESSION *) =
    37 struct
    38 
    39 datatype ctxt = datatype Element.ctxt;
    40 
    41 
    42 (*** Expressions ***)
    43 
    44 datatype 'term map =
    45   Positional of 'term option list |
    46   Named of (string * 'term) list;
    47 
    48 datatype 'morph expr = Expr of (string * 'morph) list;
    49 
    50 type expression = (string * string map) expr * (Name.binding * string option * mixfix) list;
    51 
    52 val empty_expr = Expr [];
    53 
    54 
    55 (** Parsing and printing **)
    56 
    57 local
    58 
    59 structure P = OuterParse;
    60 
    61 val loc_keyword = P.$$$ "fixes" || P.$$$ "constrains" || P.$$$ "assumes" ||
    62    P.$$$ "defines" || P.$$$ "notes";
    63 fun plus1_unless test scan =
    64   scan ::: Scan.repeat (P.$$$ "+" |-- Scan.unless test (P.!!! scan));
    65 
    66 val prefix = P.name --| P.$$$ ":";
    67 val named = P.name -- (P.$$$ "=" |-- P.term);
    68 val position = P.maybe P.term;
    69 val instance = P.$$$ "where" |-- P.and_list1 named >> Named ||
    70   Scan.repeat1 position >> Positional;
    71 
    72 in
    73 
    74 val parse_expression =
    75   let
    76     fun expr2 x = P.xname x;
    77     fun expr1 x = (Scan.optional prefix "" -- expr2 --
    78       Scan.optional instance (Named []) >> (fn ((p, l), i) => (l, (p, i)))) x;
    79     fun expr0 x = (plus1_unless loc_keyword expr1 >> Expr) x;
    80   in expr0 -- P.for_fixes end;
    81 
    82 end;
    83 
    84 fun pretty_expr thy (Expr expr) =
    85   let
    86     fun pretty_pos NONE = Pretty.str "_"
    87       | pretty_pos (SOME x) = Pretty.str x;
    88     fun pretty_named (x, y) = [Pretty.str x, Pretty.brk 1, Pretty.str "=",
    89           Pretty.brk 1, Pretty.str y] |> Pretty.block;
    90     fun pretty_ren (Positional ps) = take_suffix is_none ps |> snd |>
    91           map pretty_pos |> Pretty.breaks
    92       | pretty_ren (Named []) = []
    93       | pretty_ren (Named ps) = Pretty.str "where" :: Pretty.brk 1 ::
    94           (ps |> map pretty_named |> Pretty.separate "and");
    95     fun pretty_rename (loc, ("", ren)) =
    96           Pretty.block (Pretty.str (NewLocale.extern thy loc) :: Pretty.brk 1 :: pretty_ren ren) 
    97       | pretty_rename (loc, (prfx, ren)) =
    98           Pretty.block (Pretty.str prfx :: Pretty.brk 1 :: Pretty.str (NewLocale.extern thy loc) ::
    99             Pretty.brk 1 :: pretty_ren ren);
   100   in Pretty.separate "+" (map pretty_rename expr) |> Pretty.block end;
   101 
   102 fun err_in_expr thy msg (Expr expr) =
   103   let
   104     val err_msg =
   105       if null expr then msg
   106       else msg ^ "\n" ^ Pretty.string_of (Pretty.block
   107         [Pretty.str "The above error(s) occurred in expression:", Pretty.brk 1,
   108           pretty_expr thy (Expr expr)])
   109   in error err_msg end;
   110 
   111 
   112 (** Internalise locale names in expr **)
   113 
   114 fun intern thy (Expr instances) = Expr (map (apfst (NewLocale.intern thy)) instances);
   115 
   116 
   117 (** Parameters of expression.
   118    Sanity check of instantiations.
   119    Positional instantiations are extended to match full length of parameter list. **)
   120 
   121 fun parameters_of thy (expr, fixed) =
   122   let
   123     fun reject_dups message xs =
   124       let val dups = duplicates (op =) xs
   125       in
   126         if null dups then () else error (message ^ commas dups)
   127       end;
   128 
   129     fun match_bind (n, b) = (n = Name.name_of b);
   130     fun bind_eq (b1, b2) = (Name.name_of b1 = Name.name_of b2);
   131       (* FIXME: cannot compare bindings for equality. *)
   132 
   133     fun params_loc loc =
   134           (NewLocale.params_of thy loc |> map (fn (p, _, mx) => (p, mx)), loc);
   135     fun params_inst (expr as (loc, (prfx, Positional insts))) =
   136           let
   137             val (ps, loc') = params_loc loc;
   138 	    val d = length ps - length insts;
   139 	    val insts' =
   140 	      if d < 0 then error ("More arguments than parameters in instantiation of locale " ^
   141                 quote (NewLocale.extern thy loc))
   142 	      else insts @ replicate d NONE;
   143             val ps' = (ps ~~ insts') |>
   144               map_filter (fn (p, NONE) => SOME p | (_, SOME _) => NONE);
   145           in
   146             (ps', (loc', (prfx, Positional insts')))
   147           end
   148       | params_inst (expr as (loc, (prfx, Named insts))) =
   149           let
   150             val _ = reject_dups "Duplicate instantiation of the following parameter(s): "
   151               (map fst insts);
   152 
   153             val (ps, loc') = params_loc loc;
   154             val ps' = fold (fn (p, _) => fn ps =>
   155               if AList.defined match_bind ps p then AList.delete match_bind p ps
   156               else error (quote p ^" not a parameter of instantiated expression.")) insts ps;
   157           in
   158             (ps', (loc', (prfx, Named insts)))
   159           end;
   160     fun params_expr (Expr is) =
   161           let
   162             val (is', ps') = fold_map (fn i => fn ps =>
   163               let
   164                 val (ps', i') = params_inst i;
   165                 val ps'' = AList.join bind_eq (fn p => fn (mx1, mx2) =>
   166                   (* FIXME: should check for bindings being the same.
   167                      Instead we check for equal name and syntax. *)
   168                   if mx1 = mx2 then mx1
   169                   else error ("Conflicting syntax for parameter" ^ quote (Name.display p) ^
   170                     " in expression.")) (ps, ps')
   171               in (i', ps'') end) is []
   172           in
   173             (ps', Expr is')
   174           end;
   175 
   176     val (parms, expr') = params_expr expr;
   177 
   178     val parms' = map (#1 #> Name.name_of) parms;
   179     val fixed' = map (#1 #> Name.name_of) fixed;
   180     val _ = reject_dups "Duplicate fixed parameter(s): " fixed';
   181     val _ = reject_dups "Parameter(s) declared simultaneously in expression and for clause: " (parms' @ fixed');
   182 
   183   in (expr', (map (fn (b, mx) => (b, NONE, mx)) parms @ fixed)) end;
   184 
   185 
   186 (** Read instantiation **)
   187 
   188 (* Parse positional or named instantiation *)
   189 
   190 local
   191 
   192 fun prep_inst parse_term parms (Positional insts) ctxt =
   193       (insts ~~ parms) |> map (fn
   194         (NONE, p) => Syntax.parse_term ctxt p |
   195         (SOME t, _) => parse_term ctxt t)
   196   | prep_inst parse_term parms (Named insts) ctxt =
   197       parms |> map (fn p => case AList.lookup (op =) insts p of
   198         SOME t => parse_term ctxt t |
   199         NONE => Syntax.parse_term ctxt p);
   200 
   201 in
   202 
   203 fun parse_inst x = prep_inst Syntax.parse_term x;
   204 fun make_inst x = prep_inst (K I) x;
   205 
   206 end;
   207 
   208 (* Prepare type inference problem for Syntax.check_terms *)
   209 
   210 fun varify_indexT i ty = ty |> Term.map_atyps
   211   (fn TFree (a, S) => TVar ((a, i), S)
   212     | TVar (ai, _) => raise TYPE ("Illegal schematic variable: " ^
   213         quote (Term.string_of_vname ai), [ty], []));
   214 
   215 (* Instantiation morphism *)
   216 
   217 fun inst_morph (parm_names, parm_types) (prfx, insts') ctxt =
   218   let
   219     (* parameters *)
   220     val type_parm_names = fold Term.add_tfreesT parm_types [] |> map fst;
   221 
   222     (* type inference and contexts *)
   223     val parm_types' = map (TypeInfer.paramify_vars o Logic.varifyT) parm_types;
   224     val type_parms = fold Term.add_tvarsT parm_types' [] |> map (Logic.mk_type o TVar);
   225     val arg = type_parms @ map2 TypeInfer.constrain parm_types' insts';
   226     val res = Syntax.check_terms ctxt arg;
   227     val ctxt' = ctxt |> fold Variable.auto_fixes res;
   228     
   229     (* instantiation *)
   230     val (type_parms'', res') = chop (length type_parms) res;
   231     val insts'' = (parm_names ~~ res') |> map_filter
   232       (fn (inst as (x, Free (y, _))) => if x = y then NONE else SOME inst |
   233         inst => SOME inst);
   234     val instT = Symtab.make (type_parm_names ~~ map Logic.dest_type type_parms'');
   235     val inst = Symtab.make insts'';
   236   in
   237     (Element.inst_morphism (ProofContext.theory_of ctxt) (instT, inst) $>
   238       Morphism.name_morphism (Name.qualified prfx), ctxt')
   239   end;
   240 
   241 
   242 (*** Locale processing ***)
   243 
   244 (** Parsing **)
   245 
   246 fun parse_elem prep_typ prep_term ctxt elem =
   247   Element.map_ctxt {name = I, var = I, typ = prep_typ ctxt,
   248     term = prep_term ctxt, fact = I, attrib = I} elem;
   249 
   250 fun parse_concl prep_term ctxt concl =
   251   (map o map) (fn (t, ps) =>
   252     (prep_term ctxt, map (prep_term ctxt) ps)) concl;
   253 
   254 
   255 (** Type checking **)
   256 
   257 fun extract_elem (Fixes fixes) = map (#2 #> the_list #> map (Logic.mk_type #> rpair [])) fixes
   258   | extract_elem (Constrains csts) = map (#2 #> single #> map (Logic.mk_type #> rpair [])) csts
   259   | extract_elem (Assumes asms) = map #2 asms
   260   | extract_elem (Defines defs) = map (fn (_, (t, ps)) => [(t, ps)]) defs
   261   | extract_elem (Notes _) = [];
   262 
   263 fun restore_elem (Fixes fixes, propps) =
   264       (fixes ~~ propps) |> map (fn ((x, _, mx), propp) =>
   265         (x, propp |> map (fst #> Logic.dest_type) |> try hd, mx)) |> Fixes
   266   | restore_elem (Constrains csts, propps) =
   267       (csts ~~ propps) |> map (fn ((x, _), propp) =>
   268         (x, propp |> map (fst #> Logic.dest_type) |> hd)) |> Constrains
   269   | restore_elem (Assumes asms, propps) =
   270       (asms ~~ propps) |> map (fn ((b, _), propp) => (b, propp)) |> Assumes
   271   | restore_elem (Defines defs, propps) =
   272       (defs ~~ propps) |> map (fn ((b, _), [propp]) => (b, propp)) |> Defines
   273   | restore_elem (Notes notes, _) = Notes notes;
   274 
   275 fun check_autofix insts elems concl ctxt =
   276   let
   277     val instss = map (snd o snd) insts |> (map o map) (fn t => (t, []));
   278     val elemss = elems |> map extract_elem;
   279     val all_terms' = (burrow o burrow_fst) (Syntax.check_terms ctxt) (concl @ instss @ flat elemss); 
   280 (*    val (ctxt', all_props') = ProofContext.check_propp_schematic (ctxt, concl @ flat propss); *)
   281     val ctxt'' = (fold o fold) (fn (t, _) => Variable.auto_fixes t) all_terms' ctxt;
   282     val (concl', mores') = chop (length concl) all_terms';
   283     val (insts', elems') = chop (length instss) mores';
   284   in (insts' |> (map o map) fst |> curry (op ~~) insts |> map (fn ((l, (p, _)), is) => (l, (p, is))),
   285     elems' |> unflat elemss |> curry (op ~~) elems |> map restore_elem, concl', ctxt'') end;
   286 
   287 
   288 (** Prepare locale elements **)
   289 
   290 fun declare_elem prep_vars (Fixes fixes) ctxt =
   291       let val (vars, _) = prep_vars fixes ctxt
   292       in ctxt |> ProofContext.add_fixes_i vars |> snd end
   293   | declare_elem prep_vars (Constrains csts) ctxt =
   294       ctxt |> prep_vars (map (fn (x, T) => (Name.binding x, SOME T, NoSyn)) csts) |> snd
   295   | declare_elem _ (Assumes _) ctxt = ctxt
   296   | declare_elem _ (Defines _) ctxt = ctxt
   297   | declare_elem _ (Notes _) ctxt = ctxt;
   298 
   299 (** Finish locale elements, extract specification text **)
   300 
   301 val norm_term = Envir.beta_norm oo Term.subst_atomic;
   302 
   303 fun abstract_thm thy eq =
   304   Thm.assume (Thm.cterm_of thy eq) |> Drule.gen_all |> Drule.abs_def;
   305 
   306 fun bind_def ctxt eq (xs, env, ths) =
   307   let
   308     val ((y, T), b) = LocalDefs.abs_def eq;
   309     val b' = norm_term env b;
   310     val th = abstract_thm (ProofContext.theory_of ctxt) eq;
   311     fun err msg = error (msg ^ ": " ^ quote y);
   312   in
   313     exists (fn (x, _) => x = y) xs andalso
   314       err "Attempt to define previously specified variable";
   315     exists (fn (Free (y', _), _) => y = y' | _ => false) env andalso
   316       err "Attempt to redefine variable";
   317     (Term.add_frees b' xs, (Free (y, T), b') :: env, th :: ths)
   318   end;
   319 
   320 fun eval_text _ _ (Fixes _) text = text
   321   | eval_text _ _ (Constrains _) text = text
   322   | eval_text _ is_ext (Assumes asms)
   323         (((exts, exts'), (ints, ints')), (xs, env, defs)) =
   324       let
   325         val ts = maps (map #1 o #2) asms;
   326         val ts' = map (norm_term env) ts;
   327         val spec' =
   328           if is_ext then ((exts @ ts, exts' @ ts'), (ints, ints'))
   329           else ((exts, exts'), (ints @ ts, ints' @ ts'));
   330       in (spec', (fold Term.add_frees ts' xs, env, defs)) end
   331   | eval_text ctxt _ (Defines defs) (spec, binds) =
   332       (spec, fold (bind_def ctxt o #1 o #2) defs binds)
   333   | eval_text _ _ (Notes _) text = text;
   334 
   335 fun closeup _ _ false elem = elem
   336   | closeup ctxt parms true elem =
   337       let
   338         fun close_frees t =
   339           let
   340             val rev_frees =
   341               Term.fold_aterms (fn Free (x, T) =>
   342                 if AList.defined (op =) parms x then I else insert (op =) (x, T) | _ => I) t [];
   343           in Term.list_all_free (rev rev_frees, t) end;
   344 
   345         fun no_binds [] = []
   346           | no_binds _ = error "Illegal term bindings in context element";
   347       in
   348         (case elem of
   349           Assumes asms => Assumes (asms |> map (fn (a, propps) =>
   350             (a, map (fn (t, ps) => (close_frees t, no_binds ps)) propps)))
   351         | Defines defs => Defines (defs |> map (fn (a, (t, ps)) =>
   352             (a, (close_frees (#2 (LocalDefs.cert_def ctxt t)), no_binds ps))))
   353         | e => e)
   354       end;
   355 
   356 fun finish_primitive parms _ (Fixes fixes) = Fixes (map (fn (binding, _, mx) =>
   357       let val x = Name.name_of binding
   358       in (binding, AList.lookup (op =) parms x, mx) end) fixes)
   359   | finish_primitive _ _ (Constrains _) = Constrains []
   360   | finish_primitive _ close (Assumes asms) = close (Assumes asms)
   361   | finish_primitive _ close (Defines defs) = close (Defines defs)
   362   | finish_primitive _ _ (Notes facts) = Notes facts;
   363 
   364 fun finish_inst ctxt parms do_close (loc, (prfx, inst)) text =
   365   let
   366     val thy = ProofContext.theory_of ctxt;
   367     val (parm_names, parm_types) = NewLocale.params_of thy loc |>
   368       map (fn (b, SOME T, _) => (Name.name_of b, T)) |> split_list;
   369     val (asm, defs) = NewLocale.specification_of thy loc;
   370     val (morph, _) = inst_morph (parm_names, parm_types) (prfx, inst) ctxt;
   371     val asm' = Option.map (Morphism.term morph) asm;
   372     val defs' = map (Morphism.term morph) defs;
   373     val text' = text |>
   374       (if is_some asm
   375         then eval_text ctxt false (Assumes [(Attrib.no_binding, [(the asm', [])])])
   376         else I) |>
   377       (if not (null defs)
   378         then eval_text ctxt false (Defines (map (fn def => (Attrib.no_binding, (def, []))) defs'))
   379         else I)
   380 (* FIXME clone from new_locale.ML *)
   381   in ((loc, morph), text') end;
   382 
   383 fun finish_elem ctxt parms do_close elem text =
   384   let
   385     val elem' = finish_primitive parms (closeup ctxt parms do_close) elem;
   386     val text' = eval_text ctxt true elem' text;
   387   in (elem', text') end
   388   
   389 fun finish ctxt parms do_close insts elems text =
   390   let
   391     val (deps, text') = fold_map (finish_inst ctxt parms do_close) insts text;
   392     val (elems', text'') = fold_map (finish_elem ctxt parms do_close) elems text';
   393   in (deps, elems', text'') end;
   394 
   395 
   396 local
   397 
   398 (* nice, but for now not needed
   399 fun fold_suffixes f [] y = f [] y
   400   | fold_suffixes f (x :: xs) y = f (x :: xs) (f xs y);
   401 
   402 fun fold_prefixes f xs y = fold_suffixes (f o rev) (rev xs) y;
   403 *)
   404 
   405 fun prep_elems parse_typ parse_prop parse_inst prep_vars
   406     do_close context fixed raw_insts raw_elems raw_concl =
   407   let
   408     val thy = ProofContext.theory_of context;
   409 
   410     fun prep_inst (loc, (prfx, inst)) (i, marked, insts, ctxt) =
   411       let
   412         val (parm_names, parm_types) = NewLocale.params_of thy loc |>
   413           map (fn (b, SOME T, _) => (Name.name_of b, T)) |> split_list;
   414         val inst' = parse_inst parm_names inst ctxt;
   415         val parm_types' = map (TypeInfer.paramify_vars o varify_indexT i) parm_types;
   416         val inst'' = map2 TypeInfer.constrain parm_types' inst';
   417         val insts' = insts @ [(loc, (prfx, inst''))];
   418         val (insts'', _, _, ctxt') = check_autofix insts' [] [] ctxt;
   419         val inst''' = insts'' |> List.last |> snd |> snd;
   420         val (morph, _) = inst_morph (parm_names, parm_types) (prfx, inst''') ctxt;
   421         val (marked', ctxt'') = NewLocale.activate_declarations thy (loc, morph) (marked, ctxt);
   422       in (i+1, marked', insts', ctxt'') end;
   423   
   424     fun prep_elem raw_elem (insts, elems, ctxt) =
   425       let
   426         val ctxt' = declare_elem prep_vars raw_elem ctxt;
   427         val elems' = elems @ [parse_elem parse_typ parse_prop ctxt' raw_elem];
   428         (* FIXME term bindings *)
   429         val (_, _, _, ctxt'') = check_autofix insts elems' [] ctxt';
   430       in (insts, elems', ctxt') end;
   431 
   432     fun prep_concl raw_concl (insts, elems, ctxt) =
   433       let
   434         val concl = (map o map) (fn (t, ps) =>
   435           (parse_prop ctxt t, map (parse_prop ctxt) ps)) raw_concl;
   436       in check_autofix insts elems concl ctxt end;
   437 
   438     val fors = prep_vars fixed context |> fst;
   439     val ctxt = context |> ProofContext.add_fixes_i fors |> snd;
   440     val (_, _, insts', ctxt') = fold prep_inst raw_insts (0, NewLocale.empty, [], ctxt);
   441     val (_, elems'', ctxt'') = fold prep_elem raw_elems (insts', [], ctxt');
   442     val (insts, elems, concl, ctxt) = prep_concl raw_concl (insts', elems'', ctxt'');
   443 
   444     (* Retrieve parameter types *)
   445     val xs = fold (fn Fixes fixes => (fn ps => ps @ map (Name.name_of o #1) fixes) |
   446       _ => fn ps => ps) (Fixes fors :: elems) [];
   447     val (Ts, ctxt') = fold_map ProofContext.inferred_param xs ctxt; 
   448     val parms = xs ~~ Ts;
   449 
   450     val Fixes fors' = finish_primitive parms I (Fixes fors);
   451     val (deps, elems', text) = finish ctxt' parms do_close insts elems ((([], []), ([], [])), ([], [], []));
   452     (* text has the following structure:
   453            (((exts, exts'), (ints, ints')), (xs, env, defs))
   454        where
   455          exts: external assumptions (terms in assumes elements)
   456          exts': dito, normalised wrt. env
   457          ints: internal assumptions (terms in assumptions from insts)
   458          ints': dito, normalised wrt. env
   459          xs: the free variables in exts' and ints' and rhss of definitions,
   460            this includes parameters except defined parameters
   461          env: list of term pairs encoding substitutions, where the first term
   462            is a free variable; substitutions represent defines elements and
   463            the rhs is normalised wrt. the previous env
   464          defs: theorems representing the substitutions from defines elements
   465            (thms are normalised wrt. env).
   466        elems is an updated version of raw_elems:
   467          - type info added to Fixes and modified in Constrains
   468          - axiom and definition statement replaced by corresponding one
   469            from proppss in Assumes and Defines
   470          - Facts unchanged
   471        *)
   472 
   473   in ((parms, fors', deps, elems', concl), text) end
   474 
   475 in
   476 
   477 fun read_elems x = prep_elems Syntax.parse_typ Syntax.parse_prop parse_inst
   478   ProofContext.read_vars x;
   479 fun cert_elems x = prep_elems (K I) (K I)  make_inst
   480   ProofContext.cert_vars x;
   481 
   482 end;
   483 
   484 
   485 (* full context statements: import + elements + conclusion *)
   486 
   487 local
   488 
   489 fun prep_context_statement prep_expr prep_elems activate_elems
   490     do_close imprt elements raw_concl context =
   491   let
   492     val thy = ProofContext.theory_of context;
   493 
   494     val (Expr expr, fixed) = parameters_of thy (apfst (prep_expr thy) imprt);
   495     val ((parms, fors, deps, elems, concl), (spec, (_, _, defs))) =
   496       prep_elems do_close context fixed expr elements raw_concl;
   497 
   498     val (_, ctxt0) = ProofContext.add_fixes_i fors context;
   499     val (_, ctxt) = fold (NewLocale.activate_facts thy) deps (NewLocale.empty, ctxt0);  
   500     val ((elems', _), ctxt') = activate_elems elems (ProofContext.set_stmt true ctxt);
   501   in
   502     (((fors, deps), (ctxt', elems'), (parms, spec, defs)), concl)
   503   end;
   504 
   505 fun prep_statement prep_ctxt elems concl ctxt =
   506   let
   507     val (((_, (ctxt', _), _)), concl) = prep_ctxt false (Expr [], []) elems concl ctxt
   508   in (concl, ctxt') end;
   509 
   510 in
   511 
   512 fun read_statement body concl ctxt =
   513   prep_statement (prep_context_statement intern read_elems Element.activate) body concl ctxt;
   514 fun cert_statement body concl ctxt =
   515   prep_statement (prep_context_statement (K I) cert_elems Element.activate_i) body concl ctxt;
   516 
   517 fun read_context imprt body ctxt =
   518   #1 (prep_context_statement intern read_elems Element.activate true imprt body [] ctxt);
   519 fun cert_context imprt body ctxt =
   520   #1 (prep_context_statement (K I) cert_elems Element.activate_i true imprt body [] ctxt);
   521 
   522 end;
   523 
   524 
   525 (** Dependencies **)
   526 
   527 
   528 
   529 (*** Locale declarations ***)
   530 
   531 local
   532 
   533 (* introN: name of theorems for introduction rules of locale and
   534      delta predicates;
   535    axiomsN: name of theorem set with destruct rules for locale predicates,
   536      also name suffix of delta predicates. *)
   537 
   538 val introN = "intro";
   539 val axiomsN = "axioms";
   540 
   541 fun atomize_spec thy ts =
   542   let
   543     val t = Logic.mk_conjunction_balanced ts;
   544     val body = ObjectLogic.atomize_term thy t;
   545     val bodyT = Term.fastype_of body;
   546   in
   547     if bodyT = propT then (t, propT, Thm.reflexive (Thm.cterm_of thy t))
   548     else (body, bodyT, ObjectLogic.atomize (Thm.cterm_of thy t))
   549   end;
   550 
   551 (* achieve plain syntax for locale predicates (without "PROP") *)
   552 
   553 fun aprop_tr' n c = (Syntax.constN ^ c, fn ctxt => fn args =>
   554   if length args = n then
   555     Syntax.const "_aprop" $
   556       Term.list_comb (Syntax.free (Consts.extern (ProofContext.consts_of ctxt) c), args)
   557   else raise Match);
   558 
   559 (* CB: define one predicate including its intro rule and axioms
   560    - bname: predicate name
   561    - parms: locale parameters
   562    - defs: thms representing substitutions from defines elements
   563    - ts: terms representing locale assumptions (not normalised wrt. defs)
   564    - norm_ts: terms representing locale assumptions (normalised wrt. defs)
   565    - thy: the theory
   566 *)
   567 
   568 fun def_pred bname parms defs ts norm_ts thy =
   569   let
   570     val name = Sign.full_name thy bname;
   571 
   572     val (body, bodyT, body_eq) = atomize_spec thy norm_ts;
   573     val env = Term.add_term_free_names (body, []);
   574     val xs = filter (member (op =) env o #1) parms;
   575     val Ts = map #2 xs;
   576     val extraTs = (Term.term_tfrees body \\ fold Term.add_tfreesT Ts [])
   577       |> Library.sort_wrt #1 |> map TFree;
   578     val predT = map Term.itselfT extraTs ---> Ts ---> bodyT;
   579 
   580     val args = map Logic.mk_type extraTs @ map Free xs;
   581     val head = Term.list_comb (Const (name, predT), args);
   582     val statement = ObjectLogic.ensure_propT thy head;
   583 
   584     val ([pred_def], defs_thy) =
   585       thy
   586       |> bodyT = propT ? Sign.add_advanced_trfuns ([], [], [aprop_tr' (length args) name], [])
   587       |> Sign.declare_const [] ((Name.binding bname, predT), NoSyn) |> snd
   588       |> PureThy.add_defs false
   589         [((Thm.def_name bname, Logic.mk_equals (head, body)), [Thm.kind_internal])];
   590     val defs_ctxt = ProofContext.init defs_thy |> Variable.declare_term head;
   591 
   592     val cert = Thm.cterm_of defs_thy;
   593 
   594     val intro = Goal.prove_global defs_thy [] norm_ts statement (fn _ =>
   595       MetaSimplifier.rewrite_goals_tac [pred_def] THEN
   596       Tactic.compose_tac (false, body_eq RS Drule.equal_elim_rule1, 1) 1 THEN
   597       Tactic.compose_tac (false,
   598         Conjunction.intr_balanced (map (Thm.assume o cert) norm_ts), 0) 1);
   599 
   600     val conjuncts =
   601       (Drule.equal_elim_rule2 OF [body_eq,
   602         MetaSimplifier.rewrite_rule [pred_def] (Thm.assume (cert statement))])
   603       |> Conjunction.elim_balanced (length ts);
   604     val axioms = ts ~~ conjuncts |> map (fn (t, ax) =>
   605       Element.prove_witness defs_ctxt t
   606        (MetaSimplifier.rewrite_goals_tac defs THEN
   607         Tactic.compose_tac (false, ax, 0) 1));
   608   in ((statement, intro, axioms), defs_thy) end;
   609 
   610 in
   611 
   612 (* CB: main predicate definition function *)
   613 
   614 fun define_preds pname (parms, ((exts, exts'), (ints, ints')), defs) thy =
   615   let
   616     val (a_pred, a_intro, a_axioms, thy'') =
   617       if null exts then (NONE, NONE, [], thy)
   618       else
   619         let
   620           val aname = if null ints then pname else pname ^ "_" ^ axiomsN;
   621           val ((statement, intro, axioms), thy') =
   622             thy
   623             |> def_pred aname parms defs exts exts';
   624           val (_, thy'') =
   625             thy'
   626             |> Sign.add_path aname
   627             |> Sign.no_base_names
   628             |> PureThy.note_thmss Thm.internalK [((Name.binding introN, []), [([intro], [])])]
   629             ||> Sign.restore_naming thy';
   630           in (SOME statement, SOME intro, axioms, thy'') end;
   631     val (b_pred, b_intro, b_axioms, thy'''') =
   632       if null ints then (NONE, NONE, [], thy'')
   633       else
   634         let
   635           val ((statement, intro, axioms), thy''') =
   636             thy''
   637             |> def_pred pname parms defs (ints @ the_list a_pred) (ints' @ the_list a_pred);
   638           val (_, thy'''') =
   639             thy'''
   640             |> Sign.add_path pname
   641             |> Sign.no_base_names
   642             |> PureThy.note_thmss Thm.internalK
   643                  [((Name.binding introN, []), [([intro], [])]),
   644                   ((Name.binding axiomsN, []),
   645                     [(map (Drule.standard o Element.conclude_witness) axioms, [])])]
   646             ||> Sign.restore_naming thy''';
   647         in (SOME statement, SOME intro, axioms, thy'''') end;
   648   in ((a_pred, a_intro, a_axioms), (b_pred, b_intro, b_axioms), thy'''') end;
   649 
   650 end;
   651 
   652 
   653 local
   654 
   655 fun assumes_to_notes (Assumes asms) axms =
   656       fold_map (fn (a, spec) => fn axs =>
   657           let val (ps, qs) = chop (length spec) axs
   658           in ((a, [(ps, [])]), qs) end) asms axms
   659       |> apfst (curry Notes Thm.assumptionK)
   660   | assumes_to_notes e axms = (e, axms);
   661 
   662 fun defines_to_notes thy (Defines defs) defns =
   663     let
   664       val defs' = map (fn (_, (def, _)) => def) defs
   665       val notes = map (fn (a, (def, _)) =>
   666         (a, [([assume (cterm_of thy def)], [])])) defs
   667     in
   668       (Notes (Thm.definitionK, notes), defns @ defs')
   669     end
   670   | defines_to_notes _ e defns = (e, defns);
   671 
   672 fun gen_add_locale prep_context
   673     bname predicate_name raw_imprt raw_body thy =
   674   let
   675     val thy_ctxt = ProofContext.init thy;
   676     val name = Sign.full_name thy bname;
   677     val _ = NewLocale.test_locale thy name andalso
   678       error ("Duplicate definition of locale " ^ quote name);
   679 
   680     val ((fors, deps), (_, body_elems), text as (parms, ((_, exts'), _), defs)) =
   681       prep_context raw_imprt raw_body thy_ctxt;
   682     val ((a_statement, a_intro, a_axioms), (b_statement, b_intro, b_axioms), thy') =
   683       define_preds predicate_name text thy;
   684 
   685     val extraTs = fold Term.add_tfrees exts' [] \\ fold Term.add_tfreesT (map snd parms) [];
   686     val _ = if null extraTs then ()
   687       else warning ("Additional type variable(s) in locale specification " ^ quote bname);
   688 
   689     val satisfy = Element.satisfy_morphism b_axioms;
   690     val params = fors @
   691       (body_elems |> map_filter (fn Fixes fixes => SOME fixes | _ => NONE) |> flat);
   692     val (body_elems', defns) = fold_map (defines_to_notes thy) body_elems [];
   693 
   694     val notes = body_elems' |>
   695       (fn elems => fold_map assumes_to_notes elems (map Element.conclude_witness a_axioms)) |>
   696       fst |> map (Element.morph_ctxt satisfy) |>
   697       map_filter (fn Notes notes => SOME notes | _ => NONE);
   698 
   699     val deps' = map (fn (l, morph) => (l, morph $> satisfy)) deps;
   700 
   701     val loc_ctxt = thy' |>
   702       NewLocale.register_locale name (extraTs, params)
   703         (if is_some b_statement then b_statement else a_statement, map prop_of defs) ([], [])
   704         (map (fn n => (n, stamp ())) notes |> rev) (map (fn d => (d, stamp ())) deps' |> rev) |>
   705       NewLocale.init name
   706   in (name, loc_ctxt) end;
   707 
   708 in
   709 
   710 val add_locale = gen_add_locale read_context;
   711 (* val add_locale_i = gen_add_locale cert_context; *)
   712 
   713 end;
   714 
   715 end;