notes: proper kind;
authorwenzelm
Tue Nov 21 18:07:38 2006 +0100 (2006-11-21)
changeset 21441940ef3e85c5a
parent 21440 807a39221a58
child 21442 56e54a2afe69
notes: proper kind;
simplified Proof.theorem(_i);
context_statement: ProofContext.set_stmt after import;
src/Pure/Isar/locale.ML
     1.1 --- a/src/Pure/Isar/locale.ML	Tue Nov 21 18:07:37 2006 +0100
     1.2 +++ b/src/Pure/Isar/locale.ML	Tue Nov 21 18:07:38 2006 +0100
     1.3 @@ -886,18 +886,19 @@
     1.4        in ((ctxt', Assumed axs), []) end
     1.5    | activate_elem _ _ ((ctxt, Derived ths), Defines defs) =
     1.6        ((ctxt, Derived ths), [])
     1.7 -  | activate_elem _ is_ext ((ctxt, mode), Notes facts) =
     1.8 +  | activate_elem _ is_ext ((ctxt, mode), Notes (kind, facts)) =
     1.9        let
    1.10          val facts' = Attrib.map_facts (Attrib.attribute_i (ProofContext.theory_of ctxt)) facts;
    1.11 -        val (res, ctxt') = ctxt |> ProofContext.note_thmss_i facts';
    1.12 +        val (res, ctxt') = ctxt |> ProofContext.note_thmss_i kind facts';
    1.13        in ((ctxt', mode), if is_ext then res else []) end;
    1.14  
    1.15  fun activate_elems ax_in_ctxt (((name, ps), mode), elems) ctxt =
    1.16    let
    1.17      val thy = ProofContext.theory_of ctxt;
    1.18      val ((ctxt', _), res) =
    1.19 -        foldl_map (activate_elem ax_in_ctxt (name = "")) ((ProofContext.qualified_names ctxt, mode), elems)
    1.20 -      handle ERROR msg => err_in_locale ctxt msg [(name, map fst ps)]
    1.21 +      foldl_map (activate_elem ax_in_ctxt (name = ""))
    1.22 +        ((ProofContext.qualified_names ctxt, mode), elems)
    1.23 +      handle ERROR msg => err_in_locale ctxt msg [(name, map fst ps)];
    1.24      val ctxt'' = if name = "" then ctxt'
    1.25            else let
    1.26                val ps' = map (fn (n, SOME T) => Free (n, T)) ps;
    1.27 @@ -1005,7 +1006,7 @@
    1.28        in (ctxt', []) end
    1.29    | declare_ext_elem _ (ctxt, Assumes asms) = (ctxt, map #2 asms)
    1.30    | declare_ext_elem _ (ctxt, Defines defs) = (ctxt, map (fn (_, (t, ps)) => [(t, ps)]) defs)
    1.31 -  | declare_ext_elem _ (ctxt, Notes facts) = (ctxt, []);
    1.32 +  | declare_ext_elem _ (ctxt, Notes _) = (ctxt, []);
    1.33  
    1.34  fun declare_elems prep_vars (ctxt, (((name, ps), Assumed _), elems)) =
    1.35      let val (ctxt', propps) =
    1.36 @@ -1093,12 +1094,14 @@
    1.37    | finish_derived _ _ (Derived _) (Constrains _) = NONE
    1.38    | finish_derived sign wits (Derived _) (Assumes asms) = asms
    1.39        |> map (apsnd (map (fn (a, _) => ([Thm.assume (cterm_of sign a)], []))))
    1.40 -      |> Notes |> Element.map_ctxt_values I I (Element.satisfy_thm wits) |> SOME
    1.41 +      |> pair Thm.assumptionK |> Notes
    1.42 +      |> Element.map_ctxt_values I I (Element.satisfy_thm wits) |> SOME
    1.43    | finish_derived sign wits (Derived _) (Defines defs) = defs
    1.44        |> map (apsnd (fn (d, _) => [([Thm.assume (cterm_of sign d)], [])]))
    1.45 -      |> Notes |> Element.map_ctxt_values I I (Element.satisfy_thm wits) |> SOME
    1.46 +      |> pair Thm.definitionK |> Notes
    1.47 +      |> Element.map_ctxt_values I I (Element.satisfy_thm wits) |> SOME
    1.48  
    1.49 -  | finish_derived _ wits _ (Notes facts) = (Notes facts)
    1.50 +  | finish_derived _ wits _ (Notes facts) = Notes facts
    1.51        |> Element.map_ctxt_values I I (Element.satisfy_thm wits) |> SOME;
    1.52  
    1.53  (* CB: for finish_elems (Ext) *)
    1.54 @@ -1390,7 +1393,7 @@
    1.55        activate_facts false prep_facts (context, ps);
    1.56  
    1.57      val (ctxt, (elemss, _)) =
    1.58 -      activate_facts false prep_facts (import_ctxt, qs);
    1.59 +      activate_facts false prep_facts (ProofContext.set_stmt true import_ctxt, qs);
    1.60    in
    1.61      ((((import_ctxt, import_elemss), (ctxt, elemss, syn)),
    1.62        (parms, spec, defs)), concl)
    1.63 @@ -1457,11 +1460,11 @@
    1.64    |> PureThy.note_thmss_i kind args
    1.65    ||> Theory.restore_naming thy;
    1.66  
    1.67 -fun local_note_prefix_i prfx args ctxt =
    1.68 +fun local_note_prefix_i kind prfx args ctxt =
    1.69    ctxt
    1.70    |> ProofContext.qualified_names
    1.71    |> ProofContext.sticky_prefix prfx
    1.72 -  |> ProofContext.note_thmss_i args
    1.73 +  |> ProofContext.note_thmss_i kind args
    1.74    ||> ProofContext.restore_naming ctxt;
    1.75  
    1.76  
    1.77 @@ -1488,7 +1491,7 @@
    1.78  (* store instantiations of args for all registered interpretations
    1.79     of the theory *)
    1.80  
    1.81 -fun note_thmss_registrations kind target args thy =
    1.82 +fun note_thmss_registrations target (kind, args) thy =
    1.83    let
    1.84      val parms = the_locale thy target |> #params |> map fst;
    1.85      val ids = flatten (ProofContext.init thy, intern_expr thy)
    1.86 @@ -1535,16 +1538,17 @@
    1.87  
    1.88  (* locale results *)
    1.89  
    1.90 -fun add_thmss kind loc args ctxt =
    1.91 +fun add_thmss loc kind args ctxt =
    1.92    let
    1.93      val (ctxt', ([(_, [Notes args'])], facts)) =
    1.94 -      activate_facts true cert_facts (ctxt, [((("", []), Assumed []), [Ext (Notes args)])]);
    1.95 +      activate_facts true cert_facts
    1.96 +        (ctxt, [((("", []), Assumed []), [Ext (Notes (kind, args))])]);
    1.97      val ctxt'' = ctxt' |> ProofContext.theory
    1.98        (change_locale loc
    1.99          (fn (axiom, import, elems, params, lparams, term_syntax, regs, intros) =>
   1.100            (axiom, import, elems @ [(Notes args', stamp ())],
   1.101              params, lparams, term_syntax, regs, intros))
   1.102 -      #> note_thmss_registrations kind loc args');
   1.103 +      #> note_thmss_registrations loc args');
   1.104    in (facts, ctxt'') end;
   1.105  
   1.106  
   1.107 @@ -1629,10 +1633,10 @@
   1.108    in ((statement, intro, axioms), defs_thy) end;
   1.109  
   1.110  fun assumes_to_notes (Assumes asms) axms =
   1.111 -    fold_map (fn (a, spec) => fn axs =>
   1.112 -       let val (ps, qs) = chop (length spec) axs
   1.113 -       in ((a, [(ps, [])]), qs) end) asms axms
   1.114 -    |> apfst Notes
   1.115 +      fold_map (fn (a, spec) => fn axs =>
   1.116 +          let val (ps, qs) = chop (length spec) axs
   1.117 +          in ((a, [(ps, [])]), qs) end) asms axms
   1.118 +      |> apfst (curry Notes Thm.assumptionK)
   1.119    | assumes_to_notes e axms = (e, axms);
   1.120  
   1.121  (* CB: the following two change only "new" elems, these have identifier ("", _). *)
   1.122 @@ -1655,7 +1659,7 @@
   1.123  fun change_elemss_hyps axioms elemss =
   1.124    let
   1.125      fun change (id as ("", _), es) =
   1.126 -        (id, map (fn e as (Notes _) => Element.map_ctxt_values I I (Element.satisfy_thm axioms) e
   1.127 +        (id, map (fn e as Notes _ => Element.map_ctxt_values I I (Element.satisfy_thm axioms) e
   1.128                     | e => e) es)
   1.129        | change e = e;
   1.130    in map change elemss end;
   1.131 @@ -1675,7 +1679,8 @@
   1.132              thy |> def_pred aname parms defs exts exts';
   1.133            val elemss' = change_assumes_elemss axioms elemss;
   1.134            val def_thy' = def_thy
   1.135 -            |> PureThy.note_thmss_qualified "" aname [((introN, []), [([intro], [])])]
   1.136 +            |> PureThy.note_thmss_qualified Thm.definitionK
   1.137 +              aname [((introN, []), [([intro], [])])]
   1.138              |> snd;
   1.139            val a_elem = [(("", []), [Assumes [((bname ^ "_" ^ axiomsN, []), [(statement, [])])]])];
   1.140          in ((elemss', [statement]), a_elem, [intro], def_thy') end;
   1.141 @@ -1689,8 +1694,8 @@
   1.142            val elemss'' = change_elemss_hyps axioms elemss';
   1.143            val def_thy' =
   1.144            def_thy
   1.145 -          |> PureThy.note_thmss_qualified "" bname
   1.146 -               [((introN, []), [([intro], [])]),
   1.147 +          |> PureThy.note_thmss_qualified Thm.definitionK bname
   1.148 +              [((introN, []), [([intro], [])]),
   1.149                  ((axiomsN, []), [(map (Drule.standard o Element.conclude_witness) axioms, [])])]
   1.150            |> snd;
   1.151            val b_elem = [(("", []),
   1.152 @@ -1712,7 +1717,9 @@
   1.153        val defs' = map (fn (_, (def, _)) => (("", []), (def, []))) defs
   1.154        val notes = map (fn (a, (def, _)) =>
   1.155          (a, [([assume (cterm_of thy def)], [])])) defs
   1.156 -    in (if is_ext then SOME (Notes notes) else NONE, defns @ [Defines defs']) end
   1.157 +    in
   1.158 +      (if is_ext then SOME (Notes (Thm.definitionK, notes)) else NONE, defns @ [Defines defs'])
   1.159 +    end
   1.160    | defines_to_notes _ _ e defns = (SOME e, defns);
   1.161  
   1.162  fun change_defines_elemss thy elemss defns =
   1.163 @@ -1778,7 +1785,7 @@
   1.164      val elems'' = map_filter (fn (Fixes _) => NONE | e => SOME e) elems';
   1.165      val axs' = map (Element.assume_witness pred_thy) stmt';
   1.166      val loc_ctxt = pred_thy
   1.167 -      |> PureThy.note_thmss_qualified "" bname facts' |> snd
   1.168 +      |> PureThy.note_thmss_qualified Thm.assumptionK bname facts' |> snd
   1.169        |> declare_locale name
   1.170        |> put_locale name
   1.171         {axiom = axs',
   1.172 @@ -1871,16 +1878,16 @@
   1.173  fun gen_activate_facts_elemss get_reg note attrib std put_reg add_wit
   1.174          attn all_elemss new_elemss propss thmss thy_ctxt =
   1.175      let
   1.176 -      fun activate_elem disch (prfx, atts) (Notes facts) thy_ctxt =
   1.177 +      fun activate_elem disch (prfx, atts) (Notes (kind, facts)) thy_ctxt =
   1.178            let
   1.179              val facts' = facts
   1.180                (* discharge hyps in attributes *)
   1.181                |> Attrib.map_facts (attrib thy_ctxt o Args.map_values I I I disch)
   1.182 -              (* insert interpretation attributes *)
   1.183 +              (* append interpretation attributes *)
   1.184                |> map (apfst (apsnd (fn a => a @ map (attrib thy_ctxt) atts)))
   1.185                (* discharge hyps *)
   1.186                |> map (apsnd (map (apfst (map disch))));
   1.187 -          in snd (note prfx facts' thy_ctxt) end
   1.188 +          in snd (note kind prfx facts' thy_ctxt) end
   1.189          | activate_elem _ _ _ thy_ctxt = thy_ctxt;
   1.190  
   1.191        fun activate_elems disch ((id, _), elems) thy_ctxt =
   1.192 @@ -1917,7 +1924,7 @@
   1.193  fun global_activate_facts_elemss x = gen_activate_facts_elemss
   1.194        (fn thy => fn (name, ps) =>
   1.195          get_global_registration thy (name, map Logic.varify ps))
   1.196 -      (global_note_prefix_i "")
   1.197 +      global_note_prefix_i
   1.198        Attrib.attribute_i Drule.standard
   1.199        (fn (name, ps) => put_global_registration (name, map Logic.varify ps))
   1.200        (fn (n, ps) => add_global_witness (n, map Logic.varify ps) o
   1.201 @@ -2114,7 +2121,7 @@
   1.202                          disch (Element.inst_thm thy insts (satisfy th))))) thy) ths
   1.203                end;
   1.204  
   1.205 -            fun activate_elem (Notes facts) thy =
   1.206 +            fun activate_elem (Notes (kind, facts)) thy =
   1.207                  let
   1.208                    val facts' = facts
   1.209                        |> Attrib.map_facts (Attrib.attribute_i thy o
   1.210 @@ -2125,7 +2132,7 @@
   1.211                        |> map (apsnd (map (apfst (map (disch o Element.inst_thm thy insts o satisfy)))))
   1.212                  in
   1.213                    thy
   1.214 -                  |> global_note_prefix_i "" prfx facts'
   1.215 +                  |> global_note_prefix_i kind prfx facts'
   1.216                    |> snd
   1.217                  end
   1.218                | activate_elem _ thy = thy;
   1.219 @@ -2158,7 +2165,7 @@
   1.220        #> after_qed;
   1.221    in
   1.222      ProofContext.init thy
   1.223 -    |> Proof.theorem_i "interpretation" NONE after_qed' (prep_propp propss)
   1.224 +    |> Proof.theorem_i NONE after_qed' (prep_propp propss)
   1.225      |> Element.refine_witness |> Seq.hd
   1.226    end;
   1.227  
   1.228 @@ -2177,7 +2184,7 @@
   1.229        #> after_qed;
   1.230    in
   1.231      goal_ctxt
   1.232 -    |> Proof.theorem_i "interpretation" NONE after_qed' propp
   1.233 +    |> Proof.theorem_i NONE after_qed' propp
   1.234      |> Element.refine_witness |> Seq.hd
   1.235    end;
   1.236