src/Pure/Isar/expression.ML
changeset 32074 76d6ba08a05f
parent 31989 a290c36e94d6
child 32512 d14762642cdd
child 32800 57fcca4e7c0e
     1.1 --- a/src/Pure/Isar/expression.ML	Wed Jul 15 10:11:13 2009 +0200
     1.2 +++ b/src/Pure/Isar/expression.ML	Wed Jul 15 18:20:08 2009 +0200
     1.3 @@ -788,27 +788,6 @@
     1.4  
     1.5  (*** Interpretation ***)
     1.6  
     1.7 -(** Interpretation between locales: declaring sublocale relationships **)
     1.8 -
     1.9 -local
    1.10 -
    1.11 -fun gen_sublocale prep_expr intern raw_target expression thy =
    1.12 -  let
    1.13 -    val target = intern thy raw_target;
    1.14 -    val target_ctxt = Locale.init target thy;
    1.15 -    val ((propss, deps, export), goal_ctxt) = prep_expr expression target_ctxt;
    1.16 -    fun after_qed witss = ProofContext.theory
    1.17 -      (Locale.add_dependencies target (deps ~~ witss) export);
    1.18 -  in Element.witness_proof after_qed propss goal_ctxt end;
    1.19 -
    1.20 -in
    1.21 -
    1.22 -fun sublocale x = gen_sublocale cert_goal_expression (K I) x;
    1.23 -fun sublocale_cmd x = gen_sublocale read_goal_expression Locale.intern x;
    1.24 -
    1.25 -end;
    1.26 -
    1.27 -
    1.28  (** Interpretation in theories **)
    1.29  
    1.30  local
    1.31 @@ -816,46 +795,31 @@
    1.32  fun gen_interpretation prep_expr parse_prop prep_attr
    1.33      expression equations theory =
    1.34    let
    1.35 -    val ((propss, regs, export), expr_ctxt) = ProofContext.init theory
    1.36 +    val ((propss, deps, export), expr_ctxt) = ProofContext.init theory
    1.37        |> prep_expr expression;
    1.38  
    1.39      val eqns = map (parse_prop expr_ctxt o snd) equations |> Syntax.check_terms expr_ctxt;
    1.40 -    val eq_attns = map ((apsnd o map) (prep_attr theory) o fst) equations;
    1.41 +    val attrss = map ((apsnd o map) (prep_attr theory) o fst) equations;
    1.42      val goal_ctxt = fold Variable.auto_fixes eqns expr_ctxt;
    1.43      val export' = Variable.export_morphism goal_ctxt expr_ctxt;
    1.44  
    1.45 -    fun store_reg ((name, morph), wits) thy =
    1.46 +    fun note_eqns raw_eqns thy =
    1.47        let
    1.48 -        val wits' = map (Element.morph_witness export') wits;
    1.49 -        val morph' = morph $> Element.satisfy_morphism wits';
    1.50 +        val eqns = map (Morphism.thm (export' $> export)) raw_eqns;
    1.51 +        val eqn_attrss = map2 (fn attrs => fn eqn =>
    1.52 +          ((apsnd o map) (Attrib.attribute_i thy) attrs, [([eqn], [])])) attrss eqns;
    1.53 +        fun meta_rewrite thy = map (LocalDefs.meta_rewrite_rule (ProofContext.init thy) #>
    1.54 +          Drule.abs_def) o maps snd;
    1.55        in
    1.56          thy
    1.57 -        |> Locale.add_registration (name, (morph', export))
    1.58 -        |> pair (name, morph')
    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 store_eqns_activate regs [] thy =
    1.64 -          thy
    1.65 -          |> fold (fn (name, morph) =>
    1.66 -               Context.theory_map (Locale.activate_facts (name, morph $> export))) regs
    1.67 -      | store_eqns_activate regs eqs thy =
    1.68 -          let
    1.69 -            val eqs' = eqs |> map (Morphism.thm (export' $> export));
    1.70 -            val morph_eqs = eqs' |> map (LocalDefs.meta_rewrite_rule (ProofContext.init thy) #>
    1.71 -              Drule.abs_def);
    1.72 -            val eq_morph = Element.eq_morphism thy morph_eqs;
    1.73 -            val eq_attns' = map ((apsnd o map) (Attrib.attribute_i thy)) eq_attns;
    1.74 -          in
    1.75 -            thy
    1.76 -            |> fold (fn (name, morph) =>
    1.77 -                Locale.amend_registration eq_morph (name, morph) #>
    1.78 -                Context.theory_map (Locale.activate_facts (name, morph $> eq_morph $> export))) regs
    1.79 -            |> PureThy.note_thmss Thm.lemmaK (eq_attns' ~~ map (fn eq => [([eq], [])]) eqs')
    1.80 -            |> snd
    1.81 -          end;
    1.82 -
    1.83 -    fun after_qed wits eqs = ProofContext.theory (fold_map store_reg (regs ~~ wits)
    1.84 -      #-> (fn regs => store_eqns_activate regs eqs));
    1.85 +    fun after_qed witss eqns = ProofContext.theory (note_eqns eqns
    1.86 +      #-> (fn eqns => fold (fn ((dep, morph), wits) =>
    1.87 +        Locale.add_registration_eqs (dep, morph $> Element.satisfy_morphism
    1.88 +          (map (Element.morph_witness export') wits)) eqns export) (deps ~~ witss)));
    1.89  
    1.90    in Element.witness_proof_eqs after_qed propss eqns goal_ctxt end;
    1.91  
    1.92 @@ -868,12 +832,33 @@
    1.93  end;
    1.94  
    1.95  
    1.96 +(** Interpretation between locales: declaring sublocale relationships **)
    1.97 +
    1.98 +local
    1.99 +
   1.100 +fun gen_sublocale prep_expr intern raw_target expression thy =
   1.101 +  let
   1.102 +    val target = intern thy raw_target;
   1.103 +    val target_ctxt = Locale.init target thy;
   1.104 +    val ((propss, deps, export), goal_ctxt) = prep_expr expression target_ctxt;
   1.105 +    fun after_qed witss = ProofContext.theory
   1.106 +      (fold (fn ((dep, morph), wits) => Locale.add_dependency
   1.107 +        target (dep, morph $> Element.satisfy_morphism wits) export) (deps ~~ witss));
   1.108 +  in Element.witness_proof after_qed propss goal_ctxt end;
   1.109 +
   1.110 +in
   1.111 +
   1.112 +fun sublocale x = gen_sublocale cert_goal_expression (K I) x;
   1.113 +fun sublocale_cmd x = gen_sublocale read_goal_expression Locale.intern x;
   1.114 +
   1.115 +end;
   1.116 +
   1.117 +
   1.118  (** Interpretation in proof contexts **)
   1.119  
   1.120  local
   1.121  
   1.122 -fun gen_interpret prep_expr
   1.123 -    expression int state =
   1.124 +fun gen_interpret prep_expr expression int state =
   1.125    let
   1.126      val _ = Proof.assert_forward_or_chain state;
   1.127      val ctxt = Proof.context_of state;