Add mixins to sublocale command.
authorballarin
Sat Dec 18 18:43:13 2010 +0100 (2010-12-18)
changeset 41270dea60d052923
parent 41269 abe867c29e55
child 41271 6da953d30f48
Add mixins to sublocale command.
src/HOL/Statespace/state_space.ML
src/Pure/Isar/class.ML
src/Pure/Isar/expression.ML
src/Pure/Isar/isar_syn.ML
src/Pure/Isar/locale.ML
     1.1 --- a/src/HOL/Statespace/state_space.ML	Sat Dec 18 14:02:14 2010 +0100
     1.2 +++ b/src/HOL/Statespace/state_space.ML	Sat Dec 18 18:43:13 2010 +0100
     1.3 @@ -145,7 +145,7 @@
     1.4  
     1.5  fun prove_interpretation_in ctxt_tac (name, expr) thy =
     1.6     thy
     1.7 -   |> Expression.sublocale_cmd name expr
     1.8 +   |> Expression.sublocale_cmd name expr []
     1.9     |> Proof.global_terminal_proof
    1.10           (Method.Basic (fn ctxt => SIMPLE_METHOD (ctxt_tac ctxt)), NONE)
    1.11     |> ProofContext.theory_of
     2.1 --- a/src/Pure/Isar/class.ML	Sat Dec 18 14:02:14 2010 +0100
     2.2 +++ b/src/Pure/Isar/class.ML	Sat Dec 18 18:43:13 2010 +0100
     2.3 @@ -232,7 +232,7 @@
     2.4        |> filter (is_class thy);
     2.5      val add_dependency = case some_dep_morph
     2.6       of SOME dep_morph => Locale.add_dependency sub
     2.7 -          (sup, dep_morph $> Element.satisfy_morphism (the_list some_wit)) export
     2.8 +          (sup, dep_morph $> Element.satisfy_morphism (the_list some_wit)) NONE export
     2.9        | NONE => I
    2.10    in
    2.11      thy
     3.1 --- a/src/Pure/Isar/expression.ML	Sat Dec 18 14:02:14 2010 +0100
     3.2 +++ b/src/Pure/Isar/expression.ML	Sat Dec 18 18:43:13 2010 +0100
     3.3 @@ -39,12 +39,18 @@
     3.4      (term list list * (string * morphism) list * morphism) * Proof.context
     3.5    val read_goal_expression: expression -> Proof.context ->
     3.6      (term list list * (string * morphism) list * morphism) * Proof.context
     3.7 -  val sublocale: string -> expression_i -> theory -> Proof.state
     3.8 -  val sublocale_cmd: string -> expression -> theory -> Proof.state
     3.9 -  val interpretation: expression_i -> (Attrib.binding * term) list -> theory -> Proof.state
    3.10 -  val interpretation_cmd: expression -> (Attrib.binding * string) list -> theory -> Proof.state
    3.11 -  val interpret: expression_i -> (Attrib.binding * term) list -> bool -> Proof.state -> Proof.state
    3.12 -  val interpret_cmd: expression -> (Attrib.binding * string) list -> bool -> Proof.state -> Proof.state
    3.13 +  val sublocale: string -> expression_i -> (Attrib.binding * term) list ->
    3.14 +    theory -> Proof.state
    3.15 +  val sublocale_cmd: string -> expression -> (Attrib.binding * string) list ->
    3.16 +    theory -> Proof.state
    3.17 +  val interpretation: expression_i -> (Attrib.binding * term) list ->
    3.18 +    theory -> Proof.state
    3.19 +  val interpretation_cmd: expression -> (Attrib.binding * string) list ->
    3.20 +    theory -> Proof.state
    3.21 +  val interpret: expression_i -> (Attrib.binding * term) list ->
    3.22 +    bool -> Proof.state -> Proof.state
    3.23 +  val interpret_cmd: expression -> (Attrib.binding * string) list ->
    3.24 +    bool -> Proof.state -> Proof.state
    3.25  end;
    3.26  
    3.27  structure Expression : EXPRESSION =
    3.28 @@ -802,7 +808,7 @@
    3.29    in
    3.30      context
    3.31      |> Element.generic_note_thmss Thm.lemmaK
    3.32 -      (attrss ~~ map (fn eqn => [([Morphism.thm (export' $> export) eqn],[])]) eqns)
    3.33 +      (attrss ~~ map (fn eqn => [([Morphism.thm (export' $> export) eqn], [])]) eqns)
    3.34      |-> (fn facts => `(fn context => meta_rewrite context facts))
    3.35      |-> (fn eqns => fold (fn ((dep, morph), wits) =>
    3.36        fn context =>
    3.37 @@ -868,20 +874,56 @@
    3.38  
    3.39  local
    3.40  
    3.41 -fun gen_sublocale prep_expr intern raw_target expression thy =
    3.42 +fun note_eqns_dependency target deps witss attrss eqns export export' ctxt =
    3.43 +  let
    3.44 +    fun meta_rewrite ctxt =
    3.45 +      map (Local_Defs.meta_rewrite_rule ctxt #> Drule.abs_def) o maps snd;
    3.46 +    val facts =
    3.47 +      (attrss ~~ map (fn eqn => [([Morphism.thm (export' $> export) eqn], [])]) eqns);
    3.48 +    val eqns' = ctxt |> Context.Proof
    3.49 +      |> Element.generic_note_thmss Thm.lemmaK facts
    3.50 +      |> apsnd Context.the_proof  (* FIXME Context.proof_map_result *)
    3.51 +      |-> (fn facts => `(fn ctxt => meta_rewrite ctxt facts))
    3.52 +      |> fst;  (* FIXME duplication to add_thmss *)
    3.53 +  in
    3.54 +    ctxt
    3.55 +    |> Locale.add_thmss target Thm.lemmaK facts
    3.56 +    |> ProofContext.background_theory (fold (fn ((dep, morph), wits) =>
    3.57 +      fn theory =>
    3.58 +        Locale.add_dependency target
    3.59 +          (dep, morph $> Element.satisfy_morphism
    3.60 +            (map (Element.morph_witness export') wits))
    3.61 +          (Element.eq_morphism theory eqns' |> Option.map (rpair true))
    3.62 +          export theory) (deps ~~ witss))
    3.63 +  end;
    3.64 +
    3.65 +fun gen_sublocale prep_expr intern parse_prop prep_attr raw_target
    3.66 +    expression equations thy =
    3.67    let
    3.68      val target = intern thy raw_target;
    3.69      val target_ctxt = Named_Target.init target thy;
    3.70 -    val ((propss, deps, export), goal_ctxt) = prep_expr expression target_ctxt;
    3.71 +    val ((propss, deps, export), expr_ctxt) = prep_expr expression target_ctxt;
    3.72 +
    3.73 +    val eqns = map (parse_prop expr_ctxt o snd) equations |> Syntax.check_terms expr_ctxt;
    3.74 +    val attrss = map ((apsnd o map) (prep_attr thy) o fst) equations;
    3.75 +    val goal_ctxt = fold Variable.auto_fixes eqns expr_ctxt;
    3.76 +    val export' = Variable.export_morphism goal_ctxt expr_ctxt;
    3.77 +
    3.78 +    fun after_qed witss eqns =
    3.79 +      note_eqns_dependency target deps witss attrss eqns export export';
    3.80 +
    3.81 +  in Element.witness_proof_eqs after_qed propss eqns goal_ctxt end;
    3.82 +(*
    3.83      fun after_qed witss = ProofContext.background_theory
    3.84        (fold (fn ((dep, morph), wits) => Locale.add_dependency
    3.85          target (dep, morph $> Element.satisfy_morphism wits) export) (deps ~~ witss));
    3.86    in Element.witness_proof after_qed propss goal_ctxt end;
    3.87 -
    3.88 +*)
    3.89  in
    3.90  
    3.91 -fun sublocale x = gen_sublocale cert_goal_expression (K I) x;
    3.92 -fun sublocale_cmd x = gen_sublocale read_goal_expression Locale.intern x;
    3.93 +fun sublocale x = gen_sublocale cert_goal_expression (K I) (K I) (K I) x;
    3.94 +fun sublocale_cmd x = gen_sublocale read_goal_expression Locale.intern
    3.95 +  Syntax.parse_prop Attrib.intern_src x;
    3.96  
    3.97  end;
    3.98  
     4.1 --- a/src/Pure/Isar/isar_syn.ML	Sat Dec 18 14:02:14 2010 +0100
     4.2 +++ b/src/Pure/Isar/isar_syn.ML	Sat Dec 18 18:43:13 2010 +0100
     4.3 @@ -414,19 +414,23 @@
     4.4            (begin ? Toplevel.print) o Toplevel.begin_local_theory begin
     4.5              (Expression.add_locale_cmd name Binding.empty expr elems #> snd)));
     4.6  
     4.7 +fun parse_interpretation_arguments mandatory =
     4.8 +  Parse.!!! (Parse_Spec.locale_expression mandatory) --
     4.9 +    Scan.optional
    4.10 +      (Parse.where_ |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":" -- Parse.prop)) [];
    4.11 +
    4.12  val _ =
    4.13    Outer_Syntax.command "sublocale"
    4.14      "prove sublocale relation between a locale and a locale expression" Keyword.thy_goal
    4.15      (Parse.xname --| (Parse.$$$ "\\<subseteq>" || Parse.$$$ "<") --
    4.16 -      Parse.!!! (Parse_Spec.locale_expression false)
    4.17 -      >> (fn (loc, expr) =>
    4.18 -          Toplevel.print o Toplevel.theory_to_proof (Expression.sublocale_cmd loc expr)));
    4.19 +      parse_interpretation_arguments false
    4.20 +      >> (fn (loc, (expr, equations)) =>
    4.21 +          Toplevel.print o Toplevel.theory_to_proof (Expression.sublocale_cmd loc expr equations)));
    4.22  
    4.23  val _ =
    4.24    Outer_Syntax.command "interpretation"
    4.25      "prove interpretation of locale expression in theory" Keyword.thy_goal
    4.26 -    (Parse.!!! (Parse_Spec.locale_expression true) --
    4.27 -      Scan.optional (Parse.where_ |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":" -- Parse.prop)) []
    4.28 +    (parse_interpretation_arguments true
    4.29        >> (fn (expr, equations) => Toplevel.print o
    4.30            Toplevel.theory_to_proof (Expression.interpretation_cmd expr equations)));
    4.31  
    4.32 @@ -434,8 +438,7 @@
    4.33    Outer_Syntax.command "interpret"
    4.34      "prove interpretation of locale expression in proof context"
    4.35      (Keyword.tag_proof Keyword.prf_goal)
    4.36 -    (Parse.!!! (Parse_Spec.locale_expression true) --
    4.37 -      Scan.optional (Parse.where_ |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":" -- Parse.prop)) []
    4.38 +    (parse_interpretation_arguments true
    4.39        >> (fn (expr, equations) => Toplevel.print o
    4.40            Toplevel.proof' (Expression.interpret_cmd expr equations)));
    4.41  
     5.1 --- a/src/Pure/Isar/locale.ML	Sat Dec 18 14:02:14 2010 +0100
     5.2 +++ b/src/Pure/Isar/locale.ML	Sat Dec 18 18:43:13 2010 +0100
     5.3 @@ -71,7 +71,8 @@
     5.4    val amend_registration: string * morphism -> morphism * bool ->
     5.5      morphism -> Context.generic -> Context.generic
     5.6    val registrations_of: Context.generic -> string -> (string * morphism) list
     5.7 -  val add_dependency: string -> string * morphism -> morphism -> theory -> theory
     5.8 +  val add_dependency: string -> string * morphism -> (morphism * bool) option ->
     5.9 +    morphism -> theory -> theory
    5.10  
    5.11    (* Diagnostic *)
    5.12    val all_locales: theory -> string list
    5.13 @@ -292,7 +293,7 @@
    5.14  (
    5.15    type T = ((morphism * morphism) * serial) Idtab.table *
    5.16      (* registrations, indexed by locale name and instance;
    5.17 -       serial points to mixin list *)
    5.18 +       unique serial, points to mixin list *)
    5.19      (((morphism * bool) * serial) list) Inttab.table;
    5.20      (* table of mixin lists, per list mixins in reverse order of declaration;
    5.21         lists indexed by registration serial,
    5.22 @@ -484,7 +485,7 @@
    5.23  
    5.24  (*** Dependencies ***)
    5.25  
    5.26 -fun add_dependency loc (name, morph) export thy =
    5.27 +fun add_dependency loc (name, morph) mixin export thy =
    5.28    let
    5.29      val thy' = (change_locale loc o apsnd) (cons ((name, (morph, export)), serial ())) thy;
    5.30      val context' = Context.Theory thy';