src/Pure/Isar/expression.ML
changeset 38108 b4115423c049
parent 38107 3a46cebd7983
child 38211 8ed3a5fb4d25
     1.1 --- a/src/Pure/Isar/expression.ML	Sat Jul 31 21:14:20 2010 +0200
     1.2 +++ b/src/Pure/Isar/expression.ML	Sat Jul 31 21:14:20 2010 +0200
     1.3 @@ -43,8 +43,8 @@
     1.4    val sublocale_cmd: string -> expression -> theory -> Proof.state
     1.5    val interpretation: expression_i -> (Attrib.binding * term) list -> theory -> Proof.state
     1.6    val interpretation_cmd: expression -> (Attrib.binding * string) list -> theory -> Proof.state
     1.7 -  val interpret: expression_i -> bool -> Proof.state -> Proof.state
     1.8 -  val interpret_cmd: expression -> bool -> Proof.state -> Proof.state
     1.9 +  val interpret: expression_i -> (Attrib.binding * term) list -> bool -> Proof.state -> Proof.state
    1.10 +  val interpret_cmd: expression -> (Attrib.binding * string) list -> bool -> Proof.state -> Proof.state
    1.11  end;
    1.12  
    1.13  structure Expression : EXPRESSION =
    1.14 @@ -790,10 +790,29 @@
    1.15  
    1.16  (*** Interpretation ***)
    1.17  
    1.18 -(** Interpretation in theories **)
    1.19 +(** Interpretation in theories and proof contexts **)
    1.20  
    1.21  local
    1.22  
    1.23 +fun note_eqns_register deps witss attrss eqns export export' context =
    1.24 +  let
    1.25 +    fun meta_rewrite context =
    1.26 +      map (Local_Defs.meta_rewrite_rule (Context.proof_of context) #> Drule.abs_def) o
    1.27 +        maps snd;
    1.28 +  in
    1.29 +    context
    1.30 +    |> Element.generic_note_thmss Thm.lemmaK
    1.31 +      (attrss ~~ map (fn eqn => [([Morphism.thm (export' $> export) eqn],[])]) eqns)
    1.32 +    |-> (fn facts => `(fn context => meta_rewrite context facts))
    1.33 +    |-> (fn eqns => fold (fn ((dep, morph), wits) =>
    1.34 +      fn context =>
    1.35 +        Locale.add_registration (dep, morph $> Element.satisfy_morphism
    1.36 +            (map (Element.morph_witness export') wits))
    1.37 +          (Element.eq_morphism (Context.theory_of context) eqns |>
    1.38 +            Option.map (rpair true))
    1.39 +          export context) (deps ~~ witss))
    1.40 +  end;
    1.41 +
    1.42  fun gen_interpretation prep_expr parse_prop prep_attr
    1.43      expression equations theory =
    1.44    let
    1.45 @@ -805,36 +824,42 @@
    1.46      val goal_ctxt = fold Variable.auto_fixes eqns expr_ctxt;
    1.47      val export' = Variable.export_morphism goal_ctxt expr_ctxt;
    1.48  
    1.49 -    fun note_eqns raw_eqns thy =
    1.50 -      let
    1.51 -        val eqns = map (Morphism.thm (export' $> export)) raw_eqns;
    1.52 -        val eqn_attrss = map2 (fn attrs => fn eqn =>
    1.53 -          ((apsnd o map) (Attrib.attribute_i thy) attrs, [([eqn], [])])) attrss eqns;
    1.54 -        fun meta_rewrite thy =
    1.55 -          map (Local_Defs.meta_rewrite_rule (ProofContext.init_global thy) #> Drule.abs_def) o
    1.56 -            maps snd;
    1.57 -      in
    1.58 -        thy
    1.59 -        |> PureThy.note_thmss Thm.lemmaK eqn_attrss
    1.60 -        |-> (fn facts => `(fn thy => meta_rewrite thy facts))
    1.61 -      end;
    1.62 -
    1.63 -    fun after_qed witss eqns = ProofContext.theory (note_eqns eqns
    1.64 -      #-> (fn eqns => fold (fn ((dep, morph), wits) =>
    1.65 -        fn thy => Context.theory_map
    1.66 -          (Locale.add_registration (dep, morph $> Element.satisfy_morphism
    1.67 -              (map (Element.morph_witness export') wits))
    1.68 -            (Element.eq_morphism thy eqns |> Option.map (rpair true))
    1.69 -            export) thy) (deps ~~ witss)));
    1.70 +    fun after_qed witss eqns = (ProofContext.theory o Context.theory_map)
    1.71 +      (note_eqns_register deps witss attrss eqns export export');
    1.72  
    1.73    in Element.witness_proof_eqs after_qed propss eqns goal_ctxt end;
    1.74  
    1.75 +fun gen_interpret prep_expr parse_prop prep_attr
    1.76 +    expression equations int state =
    1.77 +  let
    1.78 +    val _ = Proof.assert_forward_or_chain state;
    1.79 +    val ctxt = Proof.context_of state;
    1.80 +    val theory = ProofContext.theory_of ctxt;
    1.81 +
    1.82 +    val ((propss, deps, export), expr_ctxt) = prep_expr expression ctxt;
    1.83 +
    1.84 +    val eqns = map (parse_prop expr_ctxt o snd) equations |> Syntax.check_terms expr_ctxt;
    1.85 +    val attrss = map ((apsnd o map) (prep_attr theory) o fst) equations;
    1.86 +    val goal_ctxt = fold Variable.auto_fixes eqns expr_ctxt;
    1.87 +    val export' = Variable.export_morphism goal_ctxt expr_ctxt;
    1.88 +
    1.89 +    fun after_qed witss eqns = (Proof.map_context o Context.proof_map)
    1.90 +      (note_eqns_register deps witss attrss eqns export export');
    1.91 +  in
    1.92 +    state
    1.93 +    |> Element.witness_local_proof_eqs after_qed "interpret" propss eqns goal_ctxt int
    1.94 +  end;
    1.95 +
    1.96  in
    1.97  
    1.98  fun interpretation x = gen_interpretation cert_goal_expression (K I) (K I) x;
    1.99  fun interpretation_cmd x = gen_interpretation read_goal_expression
   1.100    Syntax.parse_prop Attrib.intern_src x;
   1.101  
   1.102 +fun interpret x = gen_interpret cert_goal_expression (K I) (K I) x;
   1.103 +fun interpret_cmd x = gen_interpret read_goal_expression
   1.104 +  Syntax.parse_prop Attrib.intern_src x;
   1.105 +
   1.106  end;
   1.107  
   1.108  
   1.109 @@ -859,36 +884,5 @@
   1.110  
   1.111  end;
   1.112  
   1.113 -
   1.114 -(** Interpretation in proof contexts **)
   1.115 -
   1.116 -local
   1.117 -
   1.118 -fun gen_interpret prep_expr expression int state =
   1.119 -  let
   1.120 -    val _ = Proof.assert_forward_or_chain state;
   1.121 -    val ctxt = Proof.context_of state;
   1.122 -
   1.123 -    val ((propss, regs, export), goal_ctxt) = prep_expr expression ctxt;
   1.124 -
   1.125 -    fun store_reg (name, morph) thms =
   1.126 -      let
   1.127 -        val morph' = morph $> Element.satisfy_morphism thms $> export;
   1.128 -      in Context.proof_map (Locale.activate_facts (name, morph')) end;
   1.129 -
   1.130 -    fun after_qed wits =
   1.131 -      Proof.map_context (fold2 store_reg regs wits);
   1.132 -  in
   1.133 -    state
   1.134 -    |> Element.witness_local_proof after_qed "interpret" propss goal_ctxt int
   1.135 -  end;
   1.136 -
   1.137 -in
   1.138 -
   1.139 -fun interpret x = gen_interpret cert_goal_expression x;
   1.140 -fun interpret_cmd x = gen_interpret read_goal_expression x;
   1.141 -
   1.142  end;
   1.143  
   1.144 -end;
   1.145 -