1.1 --- a/etc/isar-keywords-ZF.el	Thu Nov 27 10:28:27 2008 +0100
     1.2 +++ b/etc/isar-keywords-ZF.el	Thu Nov 27 10:29:07 2008 +0100
     1.3 @@ -166,6 +166,7 @@
     1.4      "simproc_setup"
     1.5      "sorry"
     1.6      "subclass"
     1.7 +    "sublocale"
     1.8      "subsect"
     1.9      "subsection"
    1.10      "subsubsect"
    1.11 @@ -415,6 +416,7 @@
    1.12      "interpretation"
    1.13      "lemma"
    1.14      "subclass"
    1.15 +    "sublocale"
    1.16      "theorem"))
    1.17  
    1.18  (defconst isar-keywords-qed

     2.1 --- a/etc/isar-keywords.el	Thu Nov 27 10:28:27 2008 +0100
     2.2 +++ b/etc/isar-keywords.el	Thu Nov 27 10:29:07 2008 +0100
     2.3 @@ -207,6 +207,7 @@
     2.4      "specification"
     2.5      "statespace"
     2.6      "subclass"
     2.7 +    "sublocale"
     2.8      "subsect"
     2.9      "subsection"
    2.10      "subsubsect"
    2.11 @@ -514,6 +515,7 @@
    2.12      "rep_datatype"
    2.13      "specification"
    2.14      "subclass"
    2.15 +    "sublocale"
    2.16      "termination"
    2.17      "theorem"
    2.18      "typedef"))

     3.1 --- a/src/Pure/Isar/expression.ML	Thu Nov 27 10:28:27 2008 +0100
     3.2 +++ b/src/Pure/Isar/expression.ML	Thu Nov 27 10:29:07 2008 +0100
     3.3 @@ -24,6 +24,12 @@
     3.4    val add_locale_i: string -> bstring -> expression_i -> Element.context_i list -> theory ->
     3.5      string * Proof.context
     3.6  
     3.7 +  (* Interpretation *)
     3.8 +  val sublocale: (thm list list -> Proof.context -> Proof.context) ->
     3.9 +    string -> expression -> theory -> Proof.state;
    3.10 +  val sublocale_i: (thm list list -> Proof.context -> Proof.context) ->
    3.11 +    string -> expression_i -> theory -> Proof.state;
    3.12 +
    3.13    (* Debugging and development *)
    3.14    val parse_expression: OuterParse.token list -> expression * OuterParse.token list
    3.15  end;
    3.16 @@ -110,10 +116,13 @@
    3.17  
    3.18  
    3.19  (** Parameters of expression.
    3.20 -   Sanity check of instantiations.
    3.21 -   Positional instantiations are extended to match full length of parameter list. **)
    3.22  
    3.23 -fun parameters_of thy (expr, fixed) =
    3.24 +   Sanity check of instantiations and extraction of implicit parameters.
    3.25 +   The latter only occurs iff strict = false.
    3.26 +   Positional instantiations are extended to match full length of parameter list
    3.27 +   of instantiated locale. **)
    3.28 +
    3.29 +fun parameters_of thy strict (expr, fixed) =
    3.30    let
    3.31      fun reject_dups message xs =
    3.32        let val dups = duplicates (op =) xs
    3.33 @@ -162,14 +171,17 @@
    3.34                in (i', ps'') end) is []
    3.35            in (ps', is') end;
    3.36  
    3.37 -    val (parms, expr') = params_expr expr;
    3.38 +    val (implicit, expr') = params_expr expr;
    3.39  
    3.40 -    val parms' = map (#1 #> Name.name_of) parms;
    3.41 +    val implicit' = map (#1 #> Name.name_of) implicit;
    3.42      val fixed' = map (#1 #> Name.name_of) fixed;
    3.43      val _ = reject_dups "Duplicate fixed parameter(s): " fixed';
    3.44 -    val _ = reject_dups "Parameter(s) declared simultaneously in expression and for clause: " (parms' @ fixed');
    3.45 +    val implicit'' = if strict then []
    3.46 +      else let val _ = reject_dups
    3.47 +          "Parameter(s) declared simultaneously in expression and for clause: " (implicit' @ fixed')
    3.48 +        in map (fn (b, mx) => (b, NONE, mx)) implicit end;
    3.49  
    3.50 -  in (expr', (map (fn (b, mx) => (b, NONE, mx)) parms @ fixed)) end;
    3.51 +  in (expr', implicit'' @ fixed) end;
    3.52  
    3.53  
    3.54  (** Read instantiation **)
    3.55 @@ -410,20 +422,19 @@
    3.56    in (deps, elems', text'') end;
    3.57  
    3.58  
    3.59 +(** Process full context statement: instantiations + elements + conclusion **)
    3.60 +
    3.61 +(* Interleave incremental parsing and type inference over entire parsed stretch. *)
    3.62 +
    3.63  local
    3.64  
    3.65 -(* nice, but for now not needed
    3.66 -fun fold_suffixes f [] y = f [] y
    3.67 -  | fold_suffixes f (x :: xs) y = f (x :: xs) (f xs y);
    3.68 -
    3.69 -fun fold_prefixes f xs y = fold_suffixes (f o rev) (rev xs) y;
    3.70 -*)
    3.71 -
    3.72 -fun prep_elems parse_typ parse_prop parse_inst prep_vars
    3.73 -    do_close context fixed raw_insts raw_elems raw_concl =
    3.74 +fun prep_full_context_statement parse_typ parse_prop parse_inst prep_vars prep_expr
    3.75 +    strict do_close context raw_import raw_elems raw_concl =
    3.76    let
    3.77      val thy = ProofContext.theory_of context;
    3.78  
    3.79 +    val (raw_insts, fixed) = parameters_of thy strict (apfst (prep_expr thy) raw_import);
    3.80 +
    3.81      fun prep_inst (loc, (prfx, inst)) (i, marked, insts, ctxt) =
    3.82        let
    3.83          val (parm_names, parm_types) = NewLocale.params_of thy loc |>
    3.84 @@ -463,7 +474,7 @@
    3.85      val xs = fold (fn Fixes fixes => (fn ps => ps @ map (Name.name_of o #1) fixes) |
    3.86        _ => fn ps => ps) (Fixes fors :: elems) [];
    3.87      val (Ts, ctxt') = fold_map ProofContext.inferred_param xs ctxt; 
    3.88 -    val parms = xs ~~ Ts;
    3.89 +    val parms = xs ~~ Ts;  (* params from expression and elements *)
    3.90  
    3.91      val Fixes fors' = finish_primitive parms I (Fixes fors);
    3.92      val (deps, elems', text) = finish ctxt' parms do_close insts elems ((([], []), ([], [])), ([], [], []));
    3.93 @@ -492,10 +503,11 @@
    3.94  
    3.95  in
    3.96  
    3.97 -fun read_elems x = prep_elems Syntax.parse_typ Syntax.parse_prop parse_inst
    3.98 -  ProofContext.read_vars x;
    3.99 -fun cert_elems x = prep_elems (K I) (K I)  make_inst
   3.100 -  ProofContext.cert_vars x;
   3.101 +fun read_full_context_statement x =
   3.102 +  prep_full_context_statement Syntax.parse_typ Syntax.parse_prop parse_inst
   3.103 +  ProofContext.read_vars intern x;
   3.104 +fun cert_full_context_statement x =
   3.105 +  prep_full_context_statement (K I) (K I) make_inst ProofContext.cert_vars (K I) x;
   3.106  
   3.107  end;
   3.108  
   3.109 @@ -504,46 +516,41 @@
   3.110  
   3.111  local
   3.112  
   3.113 -fun prep_context_statement prep_expr prep_elems activate_elems
   3.114 -    do_close imprt elements raw_concl context =
   3.115 +fun prep_context_statement prep_full_context_statement activate_elems
   3.116 +    strict do_close imprt elements raw_concl context =
   3.117    let
   3.118      val thy = ProofContext.theory_of context;
   3.119  
   3.120 -    val (expr, fixed) = parameters_of thy (apfst (prep_expr thy) imprt);
   3.121 -    val ((parms, fors, deps, elems, concl), (spec, (_, _, defs))) =
   3.122 -      prep_elems do_close context fixed expr elements raw_concl;
   3.123 +    val ((parms, fixed, deps, elems, concl), (spec, (_, _, defs))) =
   3.124 +      prep_full_context_statement strict do_close context imprt elements raw_concl;
   3.125  
   3.126 -    val (_, ctxt0) = ProofContext.add_fixes_i fors context;
   3.127 +    val (_, ctxt0) = ProofContext.add_fixes_i fixed context;
   3.128      val (_, ctxt) = fold (NewLocale.activate_facts thy) deps (NewLocale.empty, ctxt0);  
   3.129      val ((elems', _), ctxt') = activate_elems elems (ProofContext.set_stmt true ctxt);
   3.130    in
   3.131 -    (((fors, deps), (ctxt', elems'), (parms, spec, defs)), concl)
   3.132 +    (((fixed, deps), (ctxt', elems'), (parms, spec, defs)), concl)
   3.133    end;
   3.134  
   3.135  fun prep_statement prep_ctxt elems concl ctxt =
   3.136    let
   3.137 -    val (((_, (ctxt', _), _)), concl) = prep_ctxt false ([], []) elems concl ctxt
   3.138 +    val (((_, (ctxt', _), _)), concl) = prep_ctxt true false ([], []) elems concl ctxt
   3.139    in (concl, ctxt') end;
   3.140  
   3.141  in
   3.142  
   3.143  fun read_statement body concl ctxt =
   3.144 -  prep_statement (prep_context_statement intern read_elems Element.activate) body concl ctxt;
   3.145 +  prep_statement (prep_context_statement read_full_context_statement Element.activate) body concl ctxt;
   3.146  fun cert_statement body concl ctxt =
   3.147 -  prep_statement (prep_context_statement (K I) cert_elems Element.activate_i) body concl ctxt;
   3.148 +  prep_statement (prep_context_statement cert_full_context_statement Element.activate_i) body concl ctxt;
   3.149  
   3.150 -fun read_context imprt body ctxt =
   3.151 -  #1 (prep_context_statement intern read_elems Element.activate true imprt body [] ctxt);
   3.152 -fun cert_context imprt body ctxt =
   3.153 -  #1 (prep_context_statement (K I) cert_elems Element.activate_i true imprt body [] ctxt);
   3.154 +fun read_context strict imprt body ctxt =
   3.155 +  #1 (prep_context_statement read_full_context_statement Element.activate strict true imprt body [] ctxt);
   3.156 +fun cert_context strict imprt body ctxt =
   3.157 +  #1 (prep_context_statement cert_full_context_statement Element.activate_i strict true imprt body [] ctxt);
   3.158  
   3.159  end;
   3.160  
   3.161  
   3.162 -(** Dependencies **)
   3.163 -
   3.164 -
   3.165 -
   3.166  (*** Locale declarations ***)
   3.167  
   3.168  local
   3.169 @@ -695,8 +702,8 @@
   3.170      val _ = NewLocale.test_locale thy name andalso
   3.171        error ("Duplicate definition of locale " ^ quote name);
   3.172  
   3.173 -    val ((fors, deps), (_, body_elems), text as (parms, ((_, exts'), _), defs)) =
   3.174 -      prep_context raw_imprt raw_body thy_ctxt;
   3.175 +    val ((fixed, deps), (_, body_elems), text as (parms, ((_, exts'), _), defs)) =
   3.176 +      prep_context false raw_imprt raw_body thy_ctxt;
   3.177      val ((a_statement, a_intro, a_axioms), (b_statement, b_intro, b_axioms), thy') =
   3.178        define_preds predicate_name text thy;
   3.179  
   3.180 @@ -705,7 +712,7 @@
   3.181        else warning ("Additional type variable(s) in locale specification " ^ quote bname);
   3.182  
   3.183      val satisfy = Element.satisfy_morphism b_axioms;
   3.184 -    val params = fors @
   3.185 +    val params = fixed @
   3.186        (body_elems |> map_filter (fn Fixes fixes => SOME fixes | _ => NONE) |> flat);
   3.187      val (body_elems', defns) = fold_map (defines_to_notes thy) body_elems [];
   3.188  
   3.189 @@ -730,4 +737,59 @@
   3.190  
   3.191  end;
   3.192  
   3.193 +
   3.194 +(*** Interpretation ***)
   3.195 +
   3.196 +(** Witnesses and goals **)
   3.197 +
   3.198 +fun prep_propp propss = propss |> map (map (rpair [] o Element.mark_witness));
   3.199 +
   3.200 +fun prep_result propps thmss =
   3.201 +  ListPair.map (fn (props, thms) => map2 Element.make_witness props thms) (propps, thmss);
   3.202 +
   3.203 +
   3.204 +(** Interpretation between locales: declaring sublocale relationships **)
   3.205 +
   3.206 +local
   3.207 +
   3.208 +fun store_dep target ((name, morph), thms) =
   3.209 +  NewLocale.add_dependency target (name, morph $> Element.satisfy_morphism thms);
   3.210 +
   3.211 +fun gen_sublocale prep_expr
   3.212 +    after_qed target expression thy =
   3.213 +  let
   3.214 +    val target_ctxt = NewLocale.init target thy;
   3.215 +    val target' = NewLocale.intern thy target;
   3.216 +
   3.217 +    val ((_, fixed, deps, _, _), _) = prep_expr true true target_ctxt expression [] [];
   3.218 +    val (_, goal_ctxt) = ProofContext.add_fixes_i fixed target_ctxt;
   3.219 +
   3.220 +    (* proof obligations from deps *)
   3.221 +    fun props_of (name, morph) =
   3.222 +    let
   3.223 +      val (asm, defs) = NewLocale.specification_of thy name;
   3.224 +    in
   3.225 +      (case asm of NONE => defs | SOME asm => asm :: defs) |> map (Morphism.term morph)
   3.226 +    end;
   3.227 +    
   3.228 +    val propss = map props_of deps;
   3.229 +    
   3.230 +    fun after_qed' results =
   3.231 +      fold (store_dep target') (deps ~~ prep_result propss results) #>
   3.232 +      after_qed results;
   3.233 +
   3.234 +  in
   3.235 +    goal_ctxt |>
   3.236 +      Proof.theorem_i NONE after_qed' (prep_propp propss) |>
   3.237 +      Element.refine_witness |> Seq.hd
   3.238 +  end;
   3.239 +
   3.240 +in
   3.241 +
   3.242 +fun sublocale x = gen_sublocale read_full_context_statement x;
   3.243 +fun sublocale_i x = gen_sublocale cert_full_context_statement x;
   3.244 +
   3.245  end;
   3.246 +
   3.247 +
   3.248 +end;

     4.1 --- a/src/Pure/Isar/isar_syn.ML	Thu Nov 27 10:28:27 2008 +0100
     4.2 +++ b/src/Pure/Isar/isar_syn.ML	Thu Nov 27 10:29:07 2008 +0100
     4.3 @@ -399,6 +399,13 @@
     4.4  val opt_prefix = Scan.optional (P.binding --| P.$$$ ":") Name.no_binding;
     4.5  
     4.6  val _ =
     4.7 +  OuterSyntax.command "sublocale"
     4.8 +    "prove sublocale relation between a locale and a locale expression" K.thy_goal
     4.9 +    (P.xname --| (P.$$$ "\\<subseteq>" || P.$$$ "<") -- P.!!! Expression.parse_expression
    4.10 +      >> (fn (loc, expr) =>
    4.11 +        Toplevel.print o (Toplevel.theory_to_proof (Expression.sublocale (K I) loc expr))));
    4.12 +
    4.13 +val _ =
    4.14    OuterSyntax.command "interpretation"
    4.15      "prove and register interpretation of locale expression in theory or locale" K.thy_goal
    4.16      (P.xname --| (P.$$$ "\\<subseteq>" || P.$$$ "<") -- P.!!! SpecParse.locale_expr