Package prefix is now taken into account when looking up user-defined
authorberghofe
Mon Apr 18 16:33:45 2011 +0200 (2011-04-18)
changeset 423960869ce2006eb
parent 42395 77eedb527068
child 42397 13798dcbdca5
Package prefix is now taken into account when looking up user-defined
types and proof functions.
src/HOL/SPARK/Tools/spark_commands.ML
src/HOL/SPARK/Tools/spark_vcs.ML
     1.1 --- a/src/HOL/SPARK/Tools/spark_commands.ML	Mon Apr 18 15:02:50 2011 +0200
     1.2 +++ b/src/HOL/SPARK/Tools/spark_commands.ML	Mon Apr 18 16:33:45 2011 +0200
     1.3 @@ -13,7 +13,7 @@
     1.4  structure SPARK_Commands: SPARK_COMMANDS =
     1.5  struct
     1.6  
     1.7 -fun spark_open vc_name thy =
     1.8 +fun spark_open (vc_name, prfx) thy =
     1.9    let
    1.10      val vc_path = Thy_Load.check_file (Thy_Load.master_directory thy) (Path.explode vc_name);
    1.11      val (base, header) =
    1.12 @@ -28,7 +28,7 @@
    1.13        (snd (Fdl_Parser.parse_declarations (Path.position fdl_path) (File.read fdl_path)))
    1.14        (Fdl_Parser.parse_rules (Path.position rls_path) (File.read rls_path))
    1.15        (snd (Fdl_Parser.parse_vcs header (Path.position vc_path) (File.read vc_path)))
    1.16 -      base thy
    1.17 +      base prfx thy
    1.18    end;
    1.19  
    1.20  fun add_proof_fun_cmd pf thy =
    1.21 @@ -107,7 +107,7 @@
    1.22    Outer_Syntax.command "spark_open"
    1.23      "open a new SPARK environment and load a SPARK-generated .vcg or .siv file"
    1.24      Keyword.thy_decl
    1.25 -    (Parse.name >> (Toplevel.theory o spark_open));
    1.26 +    (Parse.name -- Parse.parname >> (Toplevel.theory o spark_open));
    1.27  
    1.28  val pfun_type = Scan.option
    1.29    (Args.parens (Parse.list1 Parse.name) --| Args.colon -- Parse.name);
     2.1 --- a/src/HOL/SPARK/Tools/spark_vcs.ML	Mon Apr 18 15:02:50 2011 +0200
     2.2 +++ b/src/HOL/SPARK/Tools/spark_vcs.ML	Mon Apr 18 16:33:45 2011 +0200
     2.3 @@ -8,7 +8,7 @@
     2.4  signature SPARK_VCS =
     2.5  sig
     2.6    val set_vcs: Fdl_Parser.decls -> Fdl_Parser.rules ->
     2.7 -    (string * string) * Fdl_Parser.vcs -> Path.T -> theory -> theory
     2.8 +    (string * string) * Fdl_Parser.vcs -> Path.T -> string -> theory -> theory
     2.9    val add_proof_fun: (typ option -> 'a -> term) ->
    2.10      string * ((string list * string) option * 'a) ->
    2.11      theory -> theory
    2.12 @@ -54,7 +54,8 @@
    2.13          proving: bool,
    2.14          vcs: (string * thm list option *
    2.15            (string * expr) list * (string * expr) list) VCtab.table,
    2.16 -        path: Path.T} option}
    2.17 +        path: Path.T,
    2.18 +        prefix: string} option}
    2.19    val empty : T = {pfuns = Symtab.empty, type_map = Symtab.empty, env = NONE}
    2.20    val extend = I
    2.21    fun merge ({pfuns = pfuns1, type_map = type_map1, env = NONE},
    2.22 @@ -72,6 +73,18 @@
    2.23  
    2.24  val lcase_eq = (op =) o pairself (to_lower o Long_Name.base_name);
    2.25  
    2.26 +fun lookup_prfx "" tab s = Symtab.lookup tab s
    2.27 +  | lookup_prfx prfx tab s = (case Symtab.lookup tab s of
    2.28 +        NONE => Symtab.lookup tab (prfx ^ "__" ^ s)
    2.29 +      | x => x);
    2.30 +
    2.31 +fun strip_prfx s =
    2.32 +  let
    2.33 +    fun strip ys [] = ("", implode ys)
    2.34 +      | strip ys ("_" :: "_" :: xs) = (implode (rev xs), implode ys)
    2.35 +      | strip ys (x :: xs) = strip (x :: ys) xs
    2.36 +  in strip [] (rev (raw_explode s)) end;
    2.37 +
    2.38  fun mk_unop s t =
    2.39    let val T = fastype_of t
    2.40    in Const (s, T --> T) $ t end;
    2.41 @@ -86,14 +99,14 @@
    2.42        HOLogic.mk_setT (HOLogic.mk_prodT (T, U))) $ t $ Abs ("", T, u)
    2.43    end;
    2.44  
    2.45 -fun get_type thy ty =
    2.46 +fun get_type thy prfx ty =
    2.47    let val {type_map, ...} = VCs.get thy
    2.48 -  in Symtab.lookup type_map ty end;
    2.49 +  in lookup_prfx prfx type_map ty end;
    2.50  
    2.51 -fun mk_type _ "integer" = HOLogic.intT
    2.52 -  | mk_type _ "boolean" = HOLogic.boolT
    2.53 -  | mk_type thy ty =
    2.54 -      (case get_type thy ty of
    2.55 +fun mk_type _ _ "integer" = HOLogic.intT
    2.56 +  | mk_type _ _ "boolean" = HOLogic.boolT
    2.57 +  | mk_type thy prfx ty =
    2.58 +      (case get_type thy prfx ty of
    2.59           NONE =>
    2.60             Syntax.check_typ (Proof_Context.init_global thy)
    2.61               (Type (Sign.full_name thy (Binding.name ty), []))
    2.62 @@ -120,9 +133,9 @@
    2.63  
    2.64  val mangle_name = strip_underscores #> strip_tilde;
    2.65  
    2.66 -fun mk_variables thy xs ty (tab, ctxt) =
    2.67 +fun mk_variables thy prfx xs ty (tab, ctxt) =
    2.68    let
    2.69 -    val T = mk_type thy ty;
    2.70 +    val T = mk_type thy prfx ty;
    2.71      val (ys, ctxt') = Name.variants (map mangle_name xs) ctxt;
    2.72      val zs = map (Free o rpair T) ys;
    2.73    in (zs, (fold (Symtab.update o apsnd (rpair ty)) (xs ~~ zs) tab, ctxt')) end;
    2.74 @@ -266,7 +279,7 @@
    2.75    end;
    2.76  
    2.77  
    2.78 -fun check_no_assoc thy s = case get_type thy s of
    2.79 +fun check_no_assoc thy prfx s = case get_type thy prfx s of
    2.80      NONE => ()
    2.81    | SOME _ => error ("Cannot associate a type with " ^ s ^
    2.82        "\nsince it is no record or enumeration type");
    2.83 @@ -280,15 +293,15 @@
    2.84        else SOME ("either has no element " ^ el ^
    2.85          " or it is at the wrong position");
    2.86  
    2.87 -fun add_type_def (s, Basic_Type ty) (ids, thy) =
    2.88 -      (check_no_assoc thy s;
    2.89 +fun add_type_def prfx (s, Basic_Type ty) (ids, thy) =
    2.90 +      (check_no_assoc thy prfx s;
    2.91         (ids,
    2.92          Typedecl.abbrev_global (Binding.name s, [], NoSyn)
    2.93 -          (mk_type thy ty) thy |> snd))
    2.94 +          (mk_type thy prfx ty) thy |> snd))
    2.95  
    2.96 -  | add_type_def (s, Enum_Type els) ((tab, ctxt), thy) =
    2.97 +  | add_type_def prfx (s, Enum_Type els) ((tab, ctxt), thy) =
    2.98        let
    2.99 -        val (thy', tyname) = (case get_type thy s of
   2.100 +        val (thy', tyname) = (case get_type thy prfx s of
   2.101              NONE =>
   2.102                let
   2.103                  val tyb = Binding.name s;
   2.104 @@ -304,9 +317,18 @@
   2.105            | SOME (T as Type (tyname, [])) =>
   2.106                (case Datatype_Data.get_constrs thy tyname of
   2.107                   NONE => assoc_ty_err thy T s "is not a datatype"
   2.108 -               | SOME cs => (case check_enum els cs of
   2.109 -                   NONE => (thy, tyname)
   2.110 -                 | SOME msg => assoc_ty_err thy T s msg)));
   2.111 +               | SOME cs =>
   2.112 +                   let
   2.113 +                     val (prfx', _) = strip_prfx s;
   2.114 +                     val els' =
   2.115 +                       if prfx' = "" then els
   2.116 +                       else map (unprefix (prfx' ^ "__")) els
   2.117 +                         handle Fail _ => error ("Bad enumeration type " ^ s)
   2.118 +                   in
   2.119 +                     case check_enum els' cs of
   2.120 +                       NONE => (thy, tyname)
   2.121 +                     | SOME msg => assoc_ty_err thy T s msg
   2.122 +                   end));
   2.123          val cs = map Const (the (Datatype_Data.get_constrs thy' tyname))
   2.124        in
   2.125          ((fold (Symtab.update_new o apsnd (rpair s)) (els ~~ cs) tab,
   2.126 @@ -314,18 +336,18 @@
   2.127           thy')
   2.128        end
   2.129  
   2.130 -  | add_type_def (s, Array_Type (argtys, resty)) (ids, thy) =
   2.131 -      (check_no_assoc thy s;
   2.132 +  | add_type_def prfx (s, Array_Type (argtys, resty)) (ids, thy) =
   2.133 +      (check_no_assoc thy prfx s;
   2.134         (ids,
   2.135          Typedecl.abbrev_global (Binding.name s, [], NoSyn)
   2.136 -          (foldr1 HOLogic.mk_prodT (map (mk_type thy) argtys) -->
   2.137 -             mk_type thy resty) thy |> snd))
   2.138 +          (foldr1 HOLogic.mk_prodT (map (mk_type thy prfx) argtys) -->
   2.139 +             mk_type thy prfx resty) thy |> snd))
   2.140  
   2.141 -  | add_type_def (s, Record_Type fldtys) (ids, thy) =
   2.142 +  | add_type_def prfx (s, Record_Type fldtys) (ids, thy) =
   2.143        (ids,
   2.144         let val fldTs = maps (fn (flds, ty) =>
   2.145 -         map (rpair (mk_type thy ty)) flds) fldtys
   2.146 -       in case get_type thy s of
   2.147 +         map (rpair (mk_type thy prfx ty)) flds) fldtys
   2.148 +       in case get_type thy prfx s of
   2.149             NONE =>
   2.150               Record.add_record true ([], Binding.name s) NONE
   2.151                 (map (fn (fld, T) => (Binding.name fld, T, NoSyn)) fldTs) thy
   2.152 @@ -349,12 +371,12 @@
   2.153                     thy))
   2.154         end)
   2.155  
   2.156 -  | add_type_def (s, Pending_Type) (ids, thy) =
   2.157 -      (check_no_assoc thy s;
   2.158 +  | add_type_def prfx (s, Pending_Type) (ids, thy) =
   2.159 +      (check_no_assoc thy prfx s;
   2.160         (ids, Typedecl.typedecl_global (Binding.name s, [], NoSyn) thy |> snd));
   2.161  
   2.162  
   2.163 -fun term_of_expr thy types funs pfuns =
   2.164 +fun term_of_expr thy prfx types pfuns =
   2.165    let
   2.166      fun tm_of vs (Funct ("->", [e, e'])) =
   2.167            (HOLogic.mk_imp (fst (tm_of vs e), fst (tm_of vs e')), booleanN)
   2.168 @@ -424,7 +446,7 @@
   2.169  
   2.170        | tm_of vs (Quantifier (s, xs, ty, e)) =
   2.171            let
   2.172 -            val (ys, vs') = mk_variables thy xs ty vs;
   2.173 +            val (ys, vs') = mk_variables thy prfx xs ty vs;
   2.174              val q = (case s of
   2.175                  "for_all" => HOLogic.mk_all
   2.176                | "for_some" => HOLogic.mk_exists)
   2.177 @@ -442,7 +464,7 @@
   2.178                 [e] =>
   2.179                   let
   2.180                     val (t, rcdty) = tm_of vs e;
   2.181 -                   val rT = mk_type thy rcdty
   2.182 +                   val rT = mk_type thy prfx rcdty
   2.183                   in case (get_record_info thy rT, lookup types rcdty) of
   2.184                       (SOME {fields, ...}, SOME (Record_Type fldtys)) =>
   2.185                         (case (find_field fname fields,
   2.186 @@ -462,9 +484,9 @@
   2.187                 [e, e'] =>
   2.188                   let
   2.189                     val (t, rcdty) = tm_of vs e;
   2.190 -                   val rT = mk_type thy rcdty;
   2.191 +                   val rT = mk_type thy prfx rcdty;
   2.192                     val (u, fldty) = tm_of vs e';
   2.193 -                   val fT = mk_type thy fldty
   2.194 +                   val fT = mk_type thy prfx fldty
   2.195                   in case get_record_info thy rT of
   2.196                       SOME {fields, ...} =>
   2.197                         (case find_field fname fields of
   2.198 @@ -490,7 +512,8 @@
   2.199            (case try (unsuffix "__pos") s of
   2.200               SOME tyname => (case es of
   2.201                 [e] => (Const (@{const_name pos},
   2.202 -                 mk_type thy tyname --> HOLogic.intT) $ fst (tm_of vs e), integerN)
   2.203 +                   mk_type thy prfx tyname --> HOLogic.intT) $ fst (tm_of vs e),
   2.204 +                 integerN)
   2.205               | _ => error ("Function " ^ s ^ " expects one argument"))
   2.206             | NONE =>
   2.207  
   2.208 @@ -498,7 +521,8 @@
   2.209            (case try (unsuffix "__val") s of
   2.210               SOME tyname => (case es of
   2.211                 [e] => (Const (@{const_name val},
   2.212 -                 HOLogic.intT --> mk_type thy tyname) $ fst (tm_of vs e), tyname)
   2.213 +                   HOLogic.intT --> mk_type thy prfx tyname) $ fst (tm_of vs e),
   2.214 +                 tyname)
   2.215               | _ => error ("Function " ^ s ^ " expects one argument"))
   2.216             | NONE =>
   2.217  
   2.218 @@ -507,7 +531,7 @@
   2.219                [e] =>
   2.220                  let
   2.221                    val (t, tyname) = tm_of vs e;
   2.222 -                  val T = mk_type thy tyname
   2.223 +                  val T = mk_type thy prfx tyname
   2.224                  in (Const
   2.225                    (if s = "succ" then @{const_name succ}
   2.226                     else @{const_name pred}, T --> T) $ t, tyname)
   2.227 @@ -516,7 +540,7 @@
   2.228  
   2.229            (* user-defined proof function *)
   2.230            else
   2.231 -            (case Symtab.lookup pfuns s of
   2.232 +            (case lookup_prfx prfx pfuns s of
   2.233                 SOME (SOME (_, resty), t) =>
   2.234                   (list_comb (t, map (fst o tm_of vs) es), resty)
   2.235               | _ => error ("Undeclared proof function " ^ s))))))
   2.236 @@ -534,8 +558,9 @@
   2.237            in case lookup types ty of
   2.238                SOME (Array_Type (idxtys, elty)) =>
   2.239                  let
   2.240 -                  val T = foldr1 HOLogic.mk_prodT (map (mk_type thy) idxtys);
   2.241 -                  val U = mk_type thy elty;
   2.242 +                  val T = foldr1 HOLogic.mk_prodT
   2.243 +                    (map (mk_type thy prfx) idxtys);
   2.244 +                  val U = mk_type thy prfx elty;
   2.245                    val fT = T --> U
   2.246                  in
   2.247                    (Const (@{const_name fun_upd}, fT --> T --> U --> fT) $
   2.248 @@ -548,7 +573,7 @@
   2.249  
   2.250        | tm_of vs (Record (s, flds)) =
   2.251            let
   2.252 -            val T = mk_type thy s;
   2.253 +            val T = mk_type thy prfx s;
   2.254              val {extension = (ext_name, _), fields, ...} =
   2.255                (case get_record_info thy T of
   2.256                   NONE => error (s ^ " is not a record type")
   2.257 @@ -572,7 +597,7 @@
   2.258            in
   2.259              (list_comb
   2.260                 (Const (ext_name,
   2.261 -                  map (mk_type thy) ftys @ [HOLogic.unitT] ---> T),
   2.262 +                  map (mk_type thy prfx) ftys @ [HOLogic.unitT] ---> T),
   2.263                  fvals @ [HOLogic.unit]),
   2.264               s)
   2.265            end
   2.266 @@ -581,9 +606,9 @@
   2.267            (case lookup types s of
   2.268               SOME (Array_Type (idxtys, elty)) =>
   2.269                 let
   2.270 -                 val Ts = map (mk_type thy) idxtys;
   2.271 +                 val Ts = map (mk_type thy prfx) idxtys;
   2.272                   val T = foldr1 HOLogic.mk_prodT Ts;
   2.273 -                 val U = mk_type thy elty;
   2.274 +                 val U = mk_type thy prfx elty;
   2.275                   fun mk_idx' T (e, NONE) = HOLogic.mk_set T [fst (tm_of vs e)]
   2.276                     | mk_idx' T (e, SOME e') = Const (@{const_name atLeastAtMost},
   2.277                         T --> T --> HOLogic.mk_setT T) $
   2.278 @@ -618,8 +643,8 @@
   2.279    in tm_of end;
   2.280  
   2.281  
   2.282 -fun term_of_rule thy types funs pfuns ids rule =
   2.283 -  let val tm_of = fst o term_of_expr thy types funs pfuns ids
   2.284 +fun term_of_rule thy prfx types pfuns ids rule =
   2.285 +  let val tm_of = fst o term_of_expr thy prfx types pfuns ids
   2.286    in case rule of
   2.287        Inference_Rule (es, e) => Logic.list_implies
   2.288          (map (HOLogic.mk_Trueprop o tm_of) es, HOLogic.mk_Trueprop (tm_of e))
   2.289 @@ -676,14 +701,14 @@
   2.290  
   2.291  val add_expr_idents = fold_expr (K I) (insert (op =));
   2.292  
   2.293 -fun pfun_type thy (argtys, resty) =
   2.294 -  map (mk_type thy) argtys ---> mk_type thy resty;
   2.295 +fun pfun_type thy prfx (argtys, resty) =
   2.296 +  map (mk_type thy prfx) argtys ---> mk_type thy prfx resty;
   2.297  
   2.298 -fun check_pfun_type thy s t optty1 optty2 =
   2.299 +fun check_pfun_type thy prfx s t optty1 optty2 =
   2.300    let
   2.301      val T = fastype_of t;
   2.302      fun check ty =
   2.303 -      let val U = pfun_type thy ty
   2.304 +      let val U = pfun_type thy prfx ty
   2.305        in
   2.306          T = U orelse
   2.307          error ("Type\n" ^
   2.308 @@ -698,11 +723,13 @@
   2.309  
   2.310  fun upd_option x y = if is_some x then x else y;
   2.311  
   2.312 -fun check_pfuns_types thy funs =
   2.313 +fun check_pfuns_types thy prfx funs =
   2.314    Symtab.map (fn s => fn (optty, t) =>
   2.315 -   let val optty' = lookup funs s
   2.316 +   let val optty' = lookup funs
   2.317 +     (if prfx = "" then s
   2.318 +      else unprefix (prfx ^ "__") s handle Fail _ => s)
   2.319     in
   2.320 -     (check_pfun_type thy s t optty optty';
   2.321 +     (check_pfun_type thy prfx s t optty optty';
   2.322        (NONE |> upd_option optty |> upd_option optty', t))
   2.323     end);
   2.324  
   2.325 @@ -713,9 +740,9 @@
   2.326    (Pretty.big_list "The following verification conditions have not been proved:"
   2.327      (map Pretty.str names)))
   2.328  
   2.329 -fun set_env (env as {funs, ...}) thy = VCs.map (fn
   2.330 +fun set_env (env as {funs, prefix, ...}) thy = VCs.map (fn
   2.331      {pfuns, type_map, env = NONE} =>
   2.332 -      {pfuns = check_pfuns_types thy funs pfuns,
   2.333 +      {pfuns = check_pfuns_types thy prefix funs pfuns,
   2.334         type_map = type_map,
   2.335         env = SOME env}
   2.336    | _ => err_unfinished ()) thy;
   2.337 @@ -724,9 +751,9 @@
   2.338      SOME i => [HOLogic.mk_Trueprop (Var (("C", i), HOLogic.boolT))]
   2.339    | NONE => error ("Bad conclusion identifier: C" ^ s));
   2.340  
   2.341 -fun mk_vc thy types funs pfuns ids (tr, proved, ps, cs) =
   2.342 +fun mk_vc thy prfx types pfuns ids (tr, proved, ps, cs) =
   2.343    let val prop_of =
   2.344 -    HOLogic.mk_Trueprop o fst o term_of_expr thy types funs pfuns ids
   2.345 +    HOLogic.mk_Trueprop o fst o term_of_expr thy prfx types pfuns ids
   2.346    in
   2.347      (tr, proved,
   2.348       Element.Assumes (map (fn (s', e) =>
   2.349 @@ -738,16 +765,16 @@
   2.350  fun fold_vcs f vcs =
   2.351    VCtab.fold (fn (_, (_, _, ps, cs)) => fold f ps #> fold f cs) vcs;
   2.352  
   2.353 -fun pfuns_of_vcs pfuns vcs =
   2.354 +fun pfuns_of_vcs prfx pfuns vcs =
   2.355    fold_vcs (add_expr_pfuns o snd) vcs [] |>
   2.356 -  filter_out (Symtab.defined pfuns);
   2.357 +  filter (is_none o lookup_prfx prfx pfuns);
   2.358  
   2.359 -fun declare_missing_pfuns thy funs pfuns vcs (tab, ctxt) =
   2.360 +fun declare_missing_pfuns thy prfx funs pfuns vcs (tab, ctxt) =
   2.361    let
   2.362      val (fs, (tys, Ts)) =
   2.363 -      pfuns_of_vcs pfuns vcs |>
   2.364 +      pfuns_of_vcs prfx pfuns vcs |>
   2.365        map_filter (fn s => lookup funs s |>
   2.366 -        Option.map (fn ty => (s, (SOME ty, pfun_type thy ty)))) |>
   2.367 +        Option.map (fn ty => (s, (SOME ty, pfun_type thy prfx ty)))) |>
   2.368        split_list ||> split_list;
   2.369      val (fs', ctxt') = Name.variants fs ctxt
   2.370    in
   2.371 @@ -762,11 +789,11 @@
   2.372        {env = SOME {proving = true, ...}, ...} => err_unfinished ()
   2.373      | {pfuns, type_map, env} =>
   2.374          let
   2.375 -          val optty' = (case env of
   2.376 -              SOME {funs, ...} => lookup funs s
   2.377 -            | NONE => NONE);
   2.378 +          val (optty', prfx) = (case env of
   2.379 +              SOME {funs, prefix, ...} => (lookup funs s, prefix)
   2.380 +            | NONE => (NONE, ""));
   2.381            val optty'' = NONE |> upd_option optty |> upd_option optty';
   2.382 -          val t = prep (Option.map (pfun_type thy) optty'') raw_t;
   2.383 +          val t = prep (Option.map (pfun_type thy prfx) optty'') raw_t;
   2.384            val _ = (case fold_aterms (fn u =>
   2.385                if is_Var u orelse is_Free u then insert (op =) u else I) t [] of
   2.386                [] => ()
   2.387 @@ -775,7 +802,7 @@
   2.388                  " contains free variable(s) " ^
   2.389                  commas (map (Syntax.string_of_term_global thy) ts)));
   2.390          in
   2.391 -          (check_pfun_type thy s t optty optty';
   2.392 +          (check_pfun_type thy prfx s t optty optty';
   2.393             if is_some optty'' orelse is_none env then
   2.394               {pfuns = Symtab.update_new (s, (optty'', t)) pfuns,
   2.395                type_map = type_map,
   2.396 @@ -813,29 +840,29 @@
   2.397  
   2.398  fun lookup_vc thy name =
   2.399    (case VCs.get thy of
   2.400 -    {env = SOME {vcs, types, funs, ids, ctxt, ...}, pfuns, ...} =>
   2.401 +    {env = SOME {vcs, types, funs, ids, ctxt, prefix, ...}, pfuns, ...} =>
   2.402        (case VCtab.lookup vcs name of
   2.403 -         SOME vc =>           
   2.404 +         SOME vc =>
   2.405             let val (pfuns', ctxt', ids') =
   2.406 -             declare_missing_pfuns thy funs pfuns vcs ids
   2.407 -           in SOME (ctxt @ [ctxt'], mk_vc thy types funs pfuns' ids' vc) end
   2.408 +             declare_missing_pfuns thy prefix funs pfuns vcs ids
   2.409 +           in SOME (ctxt @ [ctxt'], mk_vc thy prefix types pfuns' ids' vc) end
   2.410         | NONE => NONE)
   2.411    | _ => NONE);
   2.412  
   2.413  fun get_vcs thy = (case VCs.get thy of
   2.414 -    {env = SOME {vcs, types, funs, ids, ctxt, defs, ...}, pfuns, ...} =>
   2.415 +    {env = SOME {vcs, types, funs, ids, ctxt, defs, prefix, ...}, pfuns, ...} =>
   2.416        let val (pfuns', ctxt', ids') =
   2.417 -        declare_missing_pfuns thy funs pfuns vcs ids
   2.418 +        declare_missing_pfuns thy prefix funs pfuns vcs ids
   2.419        in
   2.420          (ctxt @ [ctxt'], defs,
   2.421           VCtab.dest vcs |>
   2.422 -         map (apsnd (mk_vc thy types funs pfuns' ids')))
   2.423 +         map (apsnd (mk_vc thy prefix types pfuns' ids')))
   2.424        end
   2.425    | _ => ([], [], []));
   2.426  
   2.427  fun mark_proved name thms = VCs.map (fn
   2.428      {pfuns, type_map,
   2.429 -     env = SOME {ctxt, defs, types, funs, ids, vcs, path, ...}} =>
   2.430 +     env = SOME {ctxt, defs, types, funs, ids, vcs, path, prefix, ...}} =>
   2.431        {pfuns = pfuns,
   2.432         type_map = type_map,
   2.433         env = SOME {ctxt = ctxt, defs = defs,
   2.434 @@ -843,7 +870,8 @@
   2.435           proving = true,
   2.436           vcs = VCtab.map_entry name (fn (trace, _, ps, cs) =>
   2.437             (trace, SOME thms, ps, cs)) vcs,
   2.438 -         path = path}}
   2.439 +         path = path,
   2.440 +         prefix = prefix}}
   2.441    | x => x);
   2.442  
   2.443  fun close thy =
   2.444 @@ -878,9 +906,9 @@
   2.445  
   2.446  fun mk_rulename (s, i) = Binding.name (s ^ string_of_int i);
   2.447  
   2.448 -fun add_const (s, ty) ((tab, ctxt), thy) =
   2.449 +fun add_const prfx (s, ty) ((tab, ctxt), thy) =
   2.450    let
   2.451 -    val T = mk_type thy ty;
   2.452 +    val T = mk_type thy prfx ty;
   2.453      val b = Binding.name s;
   2.454      val c = Const (Sign.full_name thy b, T)
   2.455    in
   2.456 @@ -889,13 +917,13 @@
   2.457        Sign.add_consts_i [(b, T, NoSyn)] thy))
   2.458    end;
   2.459  
   2.460 -fun add_def types funs pfuns consts (id, (s, e)) (ids as (tab, ctxt), thy) =
   2.461 +fun add_def prfx types pfuns consts (id, (s, e)) (ids as (tab, ctxt), thy) =
   2.462    (case lookup consts s of
   2.463       SOME ty =>
   2.464         let
   2.465 -         val (t, ty') = term_of_expr thy types funs pfuns ids e;
   2.466 -         val T = mk_type thy ty;
   2.467 -         val T' = mk_type thy ty';
   2.468 +         val (t, ty') = term_of_expr thy prfx types pfuns ids e;
   2.469 +         val T = mk_type thy prfx ty;
   2.470 +         val T' = mk_type thy prfx ty';
   2.471           val _ = T = T' orelse
   2.472             error ("Declared type " ^ ty ^ " of " ^ s ^
   2.473               "\ndoes not match type " ^ ty' ^ " in definition");
   2.474 @@ -913,12 +941,12 @@
   2.475         end
   2.476     | NONE => error ("Undeclared constant " ^ s));
   2.477  
   2.478 -fun add_var (s, ty) (ids, thy) =
   2.479 -  let val ([Free p], ids') = mk_variables thy [s] ty ids
   2.480 +fun add_var prfx (s, ty) (ids, thy) =
   2.481 +  let val ([Free p], ids') = mk_variables thy prfx [s] ty ids
   2.482    in (p, (ids', thy)) end;
   2.483  
   2.484 -fun add_init_vars vcs (ids_thy as ((tab, _), _)) =
   2.485 -  fold_map add_var
   2.486 +fun add_init_vars prfx vcs (ids_thy as ((tab, _), _)) =
   2.487 +  fold_map (add_var prfx)
   2.488      (map_filter
   2.489         (fn s => case try (unsuffix "~") s of
   2.490            SOME s' => (case Symtab.lookup tab s' of
   2.491 @@ -935,20 +963,20 @@
   2.492    (map (fn ((s, i), _) => s ^ "(" ^ string_of_int i ^ ")") rules);
   2.493  
   2.494  (* sort definitions according to their dependency *)
   2.495 -fun sort_defs _ _ [] sdefs = rev sdefs
   2.496 -  | sort_defs pfuns consts defs sdefs =
   2.497 +fun sort_defs _ _ _ [] sdefs = rev sdefs
   2.498 +  | sort_defs prfx pfuns consts defs sdefs =
   2.499        (case find_first (fn (_, (_, e)) =>
   2.500 -         forall (Symtab.defined pfuns) (add_expr_pfuns e []) andalso
   2.501 +         forall (is_some o lookup_prfx prfx pfuns) (add_expr_pfuns e []) andalso
   2.502           forall (fn id =>
   2.503             member (fn (s, (_, (s', _))) => s = s') sdefs id orelse
   2.504             consts id)
   2.505               (add_expr_idents e [])) defs of
   2.506 -         SOME d => sort_defs pfuns consts
   2.507 +         SOME d => sort_defs prfx pfuns consts
   2.508             (remove (op =) d defs) (d :: sdefs)
   2.509         | NONE => error ("Bad definitions: " ^ rulenames defs));
   2.510  
   2.511  fun set_vcs ({types, vars, consts, funs} : decls)
   2.512 -      (rules, _) ((_, ident), vcs) path thy =
   2.513 +      (rules, _) ((_, ident), vcs) path prfx thy =
   2.514    let
   2.515      val {pfuns, ...} = VCs.get thy;
   2.516      val (defs, rules') = partition_opt dest_def rules;
   2.517 @@ -965,7 +993,7 @@
   2.518          (filter_out (is_trivial_vc o snd) vcs)) vcs);
   2.519  
   2.520      val _ = (case filter_out (is_some o lookup funs)
   2.521 -        (pfuns_of_vcs pfuns vcs') of
   2.522 +        (pfuns_of_vcs prfx pfuns vcs') of
   2.523          [] => ()
   2.524        | fs => error ("Undeclared proof function(s) " ^ commas fs));
   2.525  
   2.526 @@ -975,27 +1003,27 @@
   2.527          Symtab.update ("true", (HOLogic.true_const, booleanN)),
   2.528          Name.context),
   2.529         thy |> Sign.add_path (Long_Name.base_name ident)) |>
   2.530 -      fold add_type_def (items types) |>
   2.531 -      fold (snd oo add_const) consts' |> (fn ids_thy as ((tab, _), _) =>
   2.532 +      fold (add_type_def prfx) (items types) |>
   2.533 +      fold (snd oo add_const prfx) consts' |> (fn ids_thy as ((tab, _), _) =>
   2.534          ids_thy |>
   2.535 -        fold_map (add_def types funs pfuns consts)
   2.536 -          (sort_defs pfuns (Symtab.defined tab) defs []) ||>>
   2.537 -        fold_map add_var (items vars) ||>>
   2.538 -        add_init_vars vcs');
   2.539 +        fold_map (add_def prfx types pfuns consts)
   2.540 +          (sort_defs prfx pfuns (Symtab.defined tab) defs []) ||>>
   2.541 +        fold_map (add_var prfx) (items vars) ||>>
   2.542 +        add_init_vars prfx vcs');
   2.543  
   2.544      val ctxt =
   2.545        [Element.Fixes (map (fn (s, T) =>
   2.546           (Binding.name s, SOME T, NoSyn)) (vars'' @ ivars)),
   2.547         Element.Assumes (map (fn (id, rl) =>
   2.548           ((mk_rulename id, []),
   2.549 -          [(term_of_rule thy' types funs pfuns ids rl, [])]))
   2.550 +          [(term_of_rule thy' prfx types pfuns ids rl, [])]))
   2.551             other_rules),
   2.552         Element.Notes (Thm.definitionK,
   2.553           [((Binding.name "defns", []), map (rpair [] o single o snd) defs')])]
   2.554            
   2.555    in
   2.556      set_env {ctxt = ctxt, defs = defs', types = types, funs = funs,
   2.557 -      ids = ids, proving = false, vcs = vcs', path = path} thy'
   2.558 +      ids = ids, proving = false, vcs = vcs', path = path, prefix = prfx} thy'
   2.559    end;
   2.560  
   2.561  end;