src/Pure/Isar/expression.ML
changeset 51731 f27e22880cc3
parent 51730 dffc57bfc653
child 51734 d504e349e951
     1.1 --- a/src/Pure/Isar/expression.ML	Sun Apr 21 16:29:40 2013 +0200
     1.2 +++ b/src/Pure/Isar/expression.ML	Sun Apr 21 20:08:13 2013 +0200
     1.3 @@ -804,6 +804,8 @@
     1.4  
     1.5  (*** Interpretation ***)
     1.6  
     1.7 +local
     1.8 +
     1.9  fun read_with_extended_syntax parse_prop deps ctxt props =
    1.10    let
    1.11      val deps_ctxt = fold Locale.activate_declarations deps ctxt;
    1.12 @@ -812,14 +814,18 @@
    1.13        |> Variable.export_terms deps_ctxt ctxt
    1.14    end;
    1.15  
    1.16 +fun read_interpretation prep_expr parse_prop prep_attr expression equations initial_ctxt =
    1.17 +  let
    1.18 +    val ((propss, deps, export), expr_ctxt) = prep_expr expression initial_ctxt;
    1.19 +    val eqns = read_with_extended_syntax parse_prop deps expr_ctxt equations;
    1.20 +    val attrss = map (apsnd (map (prep_attr (Proof_Context.theory_of initial_ctxt))) o fst) equations;
    1.21 +    val goal_ctxt = fold Variable.auto_fixes eqns expr_ctxt;
    1.22 +    val export' = Variable.export_morphism goal_ctxt expr_ctxt;
    1.23 +  in (((propss, deps, export, export'), (eqns, attrss)), goal_ctxt) end;
    1.24 +
    1.25  fun meta_rewrite ctxt = map (Local_Defs.meta_rewrite_rule ctxt #> Drule.abs_def);
    1.26  
    1.27 -
    1.28 -(** Interpretation in theories and proof contexts **)
    1.29 -
    1.30 -local
    1.31 -
    1.32 -fun note_eqns_register note add_registration deps witss attrss eqns export export' ctxt =
    1.33 +fun note_eqns_register note add_registration deps witss eqns attrss export export' ctxt =
    1.34    let
    1.35      val facts = 
    1.36        (attrss ~~ map (fn eqn => [([Morphism.thm (export' $> export) eqn], [])]) eqns);
    1.37 @@ -835,48 +841,50 @@
    1.38          export ctxt'') deps witss
    1.39    end;
    1.40  
    1.41 -fun gen_interpretation prep_expr parse_prop prep_attr
    1.42 -    expression equations thy =
    1.43 +fun generic_interpretation prep_expr parse_prop prep_attr setup_proof note add_registration
    1.44 +    expression equations initial_ctxt = 
    1.45    let
    1.46 -    val initial_ctxt = Named_Target.theory_init thy;
    1.47 -
    1.48 -    val ((propss, deps, export), expr_ctxt) = prep_expr expression initial_ctxt;
    1.49 -    val eqns = read_with_extended_syntax parse_prop deps expr_ctxt equations;
    1.50 +    val (((propss, deps, export, export'), (eqns, attrss)), goal_ctxt) = 
    1.51 +      read_interpretation prep_expr parse_prop prep_attr expression equations initial_ctxt;
    1.52 +    fun after_qed witss eqns =
    1.53 +      note_eqns_register note add_registration deps witss eqns attrss export export';
    1.54 +  in setup_proof after_qed propss eqns goal_ctxt end;
    1.55  
    1.56 -    val attrss = map (apsnd (map (prep_attr thy)) o fst) equations;
    1.57 -    val goal_ctxt = fold Variable.auto_fixes eqns expr_ctxt;
    1.58 -    val export' = Variable.export_morphism goal_ctxt expr_ctxt;
    1.59 +fun gen_interpretation prep_expr parse_prop prep_attr expression equations thy =
    1.60 +  thy
    1.61 +  |> Named_Target.theory_init
    1.62 +  |> generic_interpretation prep_expr parse_prop prep_attr
    1.63 +      Element.witness_proof_eqs
    1.64 +      Local_Theory.notes_kind
    1.65 +      (Proof_Context.background_theory o Context.theory_map ooo Locale.add_registration)
    1.66 +      expression equations;
    1.67  
    1.68 -    val note = Local_Theory.notes_kind;
    1.69 -    val add_registration = Proof_Context.background_theory o Context.theory_map ooo Locale.add_registration;
    1.70 -    fun after_qed witss eqns =
    1.71 -      note_eqns_register note add_registration 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 +fun gen_interpret prep_expr parse_prop prep_attr expression equations int state =
    1.78    let
    1.79      val _ = Proof.assert_forward_or_chain state;
    1.80      val ctxt = Proof.context_of state;
    1.81 -    val thy = Proof_Context.theory_of ctxt;
    1.82 -
    1.83 -    val ((propss, deps, export), expr_ctxt) = prep_expr expression ctxt;
    1.84 -    val eqns = read_with_extended_syntax parse_prop deps expr_ctxt equations;
    1.85 -
    1.86 -    val attrss = map (apsnd (map (prep_attr thy)) o fst) equations;
    1.87 -    val goal_ctxt = fold Variable.auto_fixes eqns expr_ctxt;
    1.88 -    val export' = Variable.export_morphism goal_ctxt expr_ctxt;
    1.89 -
    1.90 -    val note = Attrib.local_notes;
    1.91 -    val add_registration = Context.proof_map ooo Locale.add_registration;
    1.92 -    fun after_qed witss eqns =
    1.93 -      Proof.map_context (note_eqns_register note add_registration deps witss attrss eqns export export')
    1.94 -      #> Proof.reset_facts;
    1.95 -
    1.96 +    fun lift_after_qed after_qed witss eqns = Proof.map_context (after_qed witss eqns) #> Proof.reset_facts;
    1.97 +    fun setup_proof after_qed propss eqns goal_ctxt = 
    1.98 +      Element.witness_local_proof_eqs (lift_after_qed after_qed) "interpret" propss eqns goal_ctxt int state;
    1.99    in
   1.100 -    state
   1.101 -    |> Element.witness_local_proof_eqs after_qed "interpret" propss eqns goal_ctxt int
   1.102 +    generic_interpretation prep_expr parse_prop prep_attr
   1.103 +      setup_proof
   1.104 +      Attrib.local_notes
   1.105 +      (Context.proof_map ooo Locale.add_registration)
   1.106 +      expression equations ctxt
   1.107 +  end;
   1.108 + 
   1.109 +fun gen_sublocale prep_expr prep_loc parse_prop prep_attr before_exit raw_locale expression equations thy =
   1.110 +  let
   1.111 +    val locale = prep_loc thy raw_locale;
   1.112 +  in
   1.113 +    thy
   1.114 +    |> Named_Target.init before_exit locale
   1.115 +    |> generic_interpretation prep_expr parse_prop prep_attr
   1.116 +        Element.witness_proof_eqs
   1.117 +        Local_Theory.notes_kind
   1.118 +        (Proof_Context.background_theory ooo Locale.add_dependency locale)
   1.119 +        expression equations
   1.120    end;
   1.121  
   1.122  in
   1.123 @@ -889,48 +897,6 @@
   1.124  fun interpret_cmd x = gen_interpret read_goal_expression
   1.125    Syntax.parse_prop Attrib.intern_src x;
   1.126  
   1.127 -end;
   1.128 -
   1.129 -
   1.130 -(** Interpretation between locales: declaring sublocale relationships **)
   1.131 -
   1.132 -local
   1.133 -
   1.134 -fun note_eqns_dependency target deps witss attrss eqns export export' ctxt =
   1.135 -  let
   1.136 -    val facts =
   1.137 -      (attrss ~~ map (fn eqn => [([Morphism.thm (export' $> export) eqn], [])]) eqns);
   1.138 -    val (eqns', ctxt') = ctxt
   1.139 -      |> Local_Theory.notes_kind Thm.lemmaK facts
   1.140 -      |-> (fn facts' => `(fn ctxt'' => meta_rewrite ctxt'' (maps snd facts')));
   1.141 -  in
   1.142 -    ctxt'
   1.143 -    |> fold2 (fn (dep, morph) => fn wits => fn ctxt'' =>
   1.144 -      (Proof_Context.background_theory ooo Locale.add_dependency target)
   1.145 -        (dep, morph $> Element.satisfy_morphism (map (Element.transform_witness export') wits))
   1.146 -        (Element.eq_morphism (Proof_Context.theory_of ctxt'') eqns' |> Option.map (rpair true))
   1.147 -        export ctxt'') deps witss
   1.148 -  end;
   1.149 -
   1.150 -fun gen_sublocale prep_expr prep_loc parse_prop prep_attr
   1.151 -    before_exit raw_target expression equations thy =
   1.152 -  let
   1.153 -    val target = prep_loc thy raw_target;
   1.154 -    val initial_ctxt = Named_Target.init before_exit target thy;
   1.155 -
   1.156 -    val ((propss, deps, export), expr_ctxt) = prep_expr expression initial_ctxt;
   1.157 -    val eqns = read_with_extended_syntax parse_prop deps expr_ctxt equations;
   1.158 -
   1.159 -    val attrss = map (apsnd (map (prep_attr thy)) o fst) equations;
   1.160 -    val goal_ctxt = fold Variable.auto_fixes eqns expr_ctxt;
   1.161 -    val export' = Variable.export_morphism goal_ctxt expr_ctxt;
   1.162 -
   1.163 -    fun after_qed witss eqns =
   1.164 -      note_eqns_dependency target deps witss attrss eqns export export';
   1.165 -
   1.166 -  in Element.witness_proof_eqs after_qed propss eqns goal_ctxt end;
   1.167 -in
   1.168 -
   1.169  fun sublocale x = gen_sublocale cert_goal_expression (K I) (K I) (K I) x;
   1.170  fun sublocale_cmd x =
   1.171    gen_sublocale read_goal_expression Locale.check Syntax.parse_prop Attrib.intern_src x;