src/Pure/Isar/expression.ML
changeset 41270 dea60d052923
parent 41228 e1fce873b814
child 41435 12585dfb86fe
     1.1 --- a/src/Pure/Isar/expression.ML	Sat Dec 18 14:02:14 2010 +0100
     1.2 +++ b/src/Pure/Isar/expression.ML	Sat Dec 18 18:43:13 2010 +0100
     1.3 @@ -39,12 +39,18 @@
     1.4      (term list list * (string * morphism) list * morphism) * Proof.context
     1.5    val read_goal_expression: expression -> Proof.context ->
     1.6      (term list list * (string * morphism) list * morphism) * Proof.context
     1.7 -  val sublocale: string -> expression_i -> theory -> Proof.state
     1.8 -  val sublocale_cmd: string -> expression -> theory -> Proof.state
     1.9 -  val interpretation: expression_i -> (Attrib.binding * term) list -> theory -> Proof.state
    1.10 -  val interpretation_cmd: expression -> (Attrib.binding * string) list -> theory -> Proof.state
    1.11 -  val interpret: expression_i -> (Attrib.binding * term) list -> bool -> Proof.state -> Proof.state
    1.12 -  val interpret_cmd: expression -> (Attrib.binding * string) list -> bool -> Proof.state -> Proof.state
    1.13 +  val sublocale: string -> expression_i -> (Attrib.binding * term) list ->
    1.14 +    theory -> Proof.state
    1.15 +  val sublocale_cmd: string -> expression -> (Attrib.binding * string) list ->
    1.16 +    theory -> Proof.state
    1.17 +  val interpretation: expression_i -> (Attrib.binding * term) list ->
    1.18 +    theory -> Proof.state
    1.19 +  val interpretation_cmd: expression -> (Attrib.binding * string) list ->
    1.20 +    theory -> Proof.state
    1.21 +  val interpret: expression_i -> (Attrib.binding * term) list ->
    1.22 +    bool -> Proof.state -> Proof.state
    1.23 +  val interpret_cmd: expression -> (Attrib.binding * string) list ->
    1.24 +    bool -> Proof.state -> Proof.state
    1.25  end;
    1.26  
    1.27  structure Expression : EXPRESSION =
    1.28 @@ -802,7 +808,7 @@
    1.29    in
    1.30      context
    1.31      |> Element.generic_note_thmss Thm.lemmaK
    1.32 -      (attrss ~~ map (fn eqn => [([Morphism.thm (export' $> export) eqn],[])]) eqns)
    1.33 +      (attrss ~~ map (fn eqn => [([Morphism.thm (export' $> export) eqn], [])]) eqns)
    1.34      |-> (fn facts => `(fn context => meta_rewrite context facts))
    1.35      |-> (fn eqns => fold (fn ((dep, morph), wits) =>
    1.36        fn context =>
    1.37 @@ -868,20 +874,56 @@
    1.38  
    1.39  local
    1.40  
    1.41 -fun gen_sublocale prep_expr intern raw_target expression thy =
    1.42 +fun note_eqns_dependency target deps witss attrss eqns export export' ctxt =
    1.43 +  let
    1.44 +    fun meta_rewrite ctxt =
    1.45 +      map (Local_Defs.meta_rewrite_rule ctxt #> Drule.abs_def) o maps snd;
    1.46 +    val facts =
    1.47 +      (attrss ~~ map (fn eqn => [([Morphism.thm (export' $> export) eqn], [])]) eqns);
    1.48 +    val eqns' = ctxt |> Context.Proof
    1.49 +      |> Element.generic_note_thmss Thm.lemmaK facts
    1.50 +      |> apsnd Context.the_proof  (* FIXME Context.proof_map_result *)
    1.51 +      |-> (fn facts => `(fn ctxt => meta_rewrite ctxt facts))
    1.52 +      |> fst;  (* FIXME duplication to add_thmss *)
    1.53 +  in
    1.54 +    ctxt
    1.55 +    |> Locale.add_thmss target Thm.lemmaK facts
    1.56 +    |> ProofContext.background_theory (fold (fn ((dep, morph), wits) =>
    1.57 +      fn theory =>
    1.58 +        Locale.add_dependency target
    1.59 +          (dep, morph $> Element.satisfy_morphism
    1.60 +            (map (Element.morph_witness export') wits))
    1.61 +          (Element.eq_morphism theory eqns' |> Option.map (rpair true))
    1.62 +          export theory) (deps ~~ witss))
    1.63 +  end;
    1.64 +
    1.65 +fun gen_sublocale prep_expr intern parse_prop prep_attr raw_target
    1.66 +    expression equations thy =
    1.67    let
    1.68      val target = intern thy raw_target;
    1.69      val target_ctxt = Named_Target.init target thy;
    1.70 -    val ((propss, deps, export), goal_ctxt) = prep_expr expression target_ctxt;
    1.71 +    val ((propss, deps, export), expr_ctxt) = prep_expr expression target_ctxt;
    1.72 +
    1.73 +    val eqns = map (parse_prop expr_ctxt o snd) equations |> Syntax.check_terms expr_ctxt;
    1.74 +    val attrss = map ((apsnd o map) (prep_attr thy) o fst) equations;
    1.75 +    val goal_ctxt = fold Variable.auto_fixes eqns expr_ctxt;
    1.76 +    val export' = Variable.export_morphism goal_ctxt expr_ctxt;
    1.77 +
    1.78 +    fun after_qed witss eqns =
    1.79 +      note_eqns_dependency target deps witss attrss eqns export export';
    1.80 +
    1.81 +  in Element.witness_proof_eqs after_qed propss eqns goal_ctxt end;
    1.82 +(*
    1.83      fun after_qed witss = ProofContext.background_theory
    1.84        (fold (fn ((dep, morph), wits) => Locale.add_dependency
    1.85          target (dep, morph $> Element.satisfy_morphism wits) export) (deps ~~ witss));
    1.86    in Element.witness_proof after_qed propss goal_ctxt end;
    1.87 -
    1.88 +*)
    1.89  in
    1.90  
    1.91 -fun sublocale x = gen_sublocale cert_goal_expression (K I) x;
    1.92 -fun sublocale_cmd x = gen_sublocale read_goal_expression Locale.intern x;
    1.93 +fun sublocale x = gen_sublocale cert_goal_expression (K I) (K I) (K I) x;
    1.94 +fun sublocale_cmd x = gen_sublocale read_goal_expression Locale.intern
    1.95 +  Syntax.parse_prop Attrib.intern_src x;
    1.96  
    1.97  end;
    1.98