Changed naming scheme for theorems generated by interpretations.
authorballarin
Mon Apr 14 17:54:56 2008 +0200 (2008-04-14)
changeset 26645e114be97befe
parent 26644 2f12191282e2
child 26646 540ad65e804c
Changed naming scheme for theorems generated by interpretations.
src/FOL/ex/LocaleTest.thy
src/HOL/MetisExamples/BigO.thy
src/Pure/Isar/locale.ML
     1.1 --- a/src/FOL/ex/LocaleTest.thy	Mon Apr 14 16:42:47 2008 +0200
     1.2 +++ b/src/FOL/ex/LocaleTest.thy	Mon Apr 14 17:54:56 2008 +0200
     1.3 @@ -120,7 +120,7 @@
     1.4  print_interps IA  (* output: i1 *)
     1.5  
     1.6  (* possible accesses *)
     1.7 -thm i1.a.asm_A thm LocaleTest.i1.a.asm_A
     1.8 +thm i1.a.asm_A thm LocaleTest.IA_locale.i1.a.asm_A thm IA_locale.i1.a.asm_A
     1.9  thm i1.asm_A thm LocaleTest.i1.asm_A
    1.10  
    1.11  ML {* check_thm "i1.a.asm_A" *}
    1.12 @@ -134,7 +134,7 @@
    1.13  print_interps IA  (* output: <no prefix>, i1 *)
    1.14  
    1.15  (* possible accesses *)
    1.16 -thm asm_C thm a_b.asm_C thm LocaleTest.a_b.asm_C thm LocaleTest.a_b.asm_C
    1.17 +thm asm_C thm a_b.asm_C thm LocaleTest.IC_locale.a_b.asm_C thm IC_locale.a_b.asm_C
    1.18  
    1.19  ML {* check_thm "asm_C" *}
    1.20  
     2.1 --- a/src/HOL/MetisExamples/BigO.thy	Mon Apr 14 16:42:47 2008 +0200
     2.2 +++ b/src/HOL/MetisExamples/BigO.thy	Mon Apr 14 17:54:56 2008 +0200
     2.3 @@ -371,7 +371,7 @@
     2.4      f : O(g)" 
     2.5    apply (auto simp add: bigo_def)
     2.6  (*Version 1: one-shot proof*)
     2.7 -  apply (metis OrderedGroup.abs_le_D1 Orderings.linorder_class.not_less  order_less_le  Orderings.xt1(12)  Ring_and_Field.abs_mult)
     2.8 +  apply (metis OrderedGroup.abs_le_D1 linorder_class.not_less  order_less_le  Orderings.xt1(12)  Ring_and_Field.abs_mult)
     2.9    done
    2.10  
    2.11  lemma (*bigo_bounded_alt:*) "ALL x. 0 <= f x ==> ALL x. f x <= c * g x ==> 
     3.1 --- a/src/Pure/Isar/locale.ML	Mon Apr 14 16:42:47 2008 +0200
     3.2 +++ b/src/Pure/Isar/locale.ML	Mon Apr 14 17:54:56 2008 +0200
     3.3 @@ -637,7 +637,8 @@
     3.4    distinct (eq_fst (op = : string * string -> bool)) (maps (snd o fst o fst) elemss);
     3.5  
     3.6  
     3.7 -fun params_prefix params = space_implode "_" params;
     3.8 +fun params_qualified params name =
     3.9 +  NameSpace.qualified (space_implode "_" params) name;
    3.10  
    3.11  
    3.12  (* CB: param_types has the following type:
    3.13 @@ -939,7 +940,7 @@
    3.14          val [env] = unify_parms ctxt all_params [map (apfst (Element.rename ren) o apsnd SOME) ps];
    3.15          val elem_morphism =
    3.16            Element.rename_morphism ren $>
    3.17 -          Morphism.name_morphism (NameSpace.qualified (params_prefix params)) $>
    3.18 +          Morphism.name_morphism (params_qualified params) $>
    3.19            Element.instT_morphism thy env;
    3.20          val elems' = map (Element.morph_ctxt elem_morphism) elems;
    3.21        in (((name, map (apsnd SOME) locale_params'), mode'), elems') end;
    3.22 @@ -1583,16 +1584,18 @@
    3.23  
    3.24  (* naming of interpreted theorems *)
    3.25  
    3.26 -fun global_note_prefix_i kind (fully_qualified, prfx) args thy =
    3.27 +fun global_note_prefix_i kind loc (fully_qualified, prfx) args thy =
    3.28    thy
    3.29    |> Sign.qualified_names
    3.30 +  |> Sign.add_path (NameSpace.base loc ^ "_locale")
    3.31    |> (if fully_qualified then Sign.sticky_prefix prfx else Sign.add_path prfx)
    3.32    |> PureThy.note_thmss_i kind args
    3.33    ||> Sign.restore_naming thy;
    3.34  
    3.35 -fun local_note_prefix_i kind (fully_qualified, prfx) args ctxt =
    3.36 +fun local_note_prefix_i kind loc (fully_qualified, prfx) args ctxt =
    3.37    ctxt
    3.38    |> ProofContext.qualified_names
    3.39 +  |> ProofContext.add_path (NameSpace.base loc ^ "_locale")
    3.40    |> (if fully_qualified then ProofContext.sticky_prefix prfx else ProofContext.add_path prfx)
    3.41    |> ProofContext.note_thmss_i kind args
    3.42    ||> ProofContext.restore_naming ctxt;
    3.43 @@ -1696,7 +1699,7 @@
    3.44          val (insts, prems, eqns) = collect_global_witnesses thy imp parms ids vts;
    3.45          val attrib = Attrib.attribute_i thy;
    3.46          val args' = interpret_args thy prfx insts prems eqns atts2 exp attrib args;
    3.47 -      in global_note_prefix_i kind (fully_qualified, prfx) args' thy |> snd end;
    3.48 +      in global_note_prefix_i kind target (fully_qualified, prfx) args' thy |> snd end;
    3.49    in fold activate regs thy end;
    3.50  
    3.51  
    3.52 @@ -2077,14 +2080,14 @@
    3.53      val (propss, eq_props) = chop (length new_elemss) propss;
    3.54      val (thmss, eq_thms) = chop (length new_elemss) thmss;
    3.55  
    3.56 -    fun activate_elem prems eqns exp ((fully_qualified, prfx), atts) (Notes (kind, facts)) thy_ctxt =
    3.57 +    fun activate_elem prems eqns exp loc ((fully_qualified, prfx), atts) (Notes (kind, facts)) thy_ctxt =
    3.58          let
    3.59            val ctxt = mk_ctxt thy_ctxt;
    3.60            val facts' = interpret_args (ProofContext.theory_of ctxt) prfx
    3.61                (Symtab.empty, Symtab.empty) prems eqns atts
    3.62                exp (attrib thy_ctxt) facts;
    3.63 -        in snd (note_interp kind (fully_qualified, prfx) facts' thy_ctxt) end
    3.64 -      | activate_elem _ _ _ _ _ thy_ctxt = thy_ctxt;
    3.65 +        in snd (note_interp kind loc (fully_qualified, prfx) facts' thy_ctxt) end
    3.66 +      | activate_elem _ _ _ _ _ _ thy_ctxt = thy_ctxt;
    3.67  
    3.68      fun activate_elems prems eqns exp ((id, _), elems) thy_ctxt =
    3.69        let
    3.70 @@ -2092,7 +2095,7 @@
    3.71           of SOME x => x
    3.72            | NONE => sys_error ("Unknown registration of " ^ quote (fst id)
    3.73                ^ " while activating facts.");
    3.74 -      in fold (activate_elem prems (the (Idtab.lookup eqns id)) exp prfx_atts) elems thy_ctxt end;
    3.75 +      in fold (activate_elem prems (the (Idtab.lookup eqns id)) exp (fst id) prfx_atts) elems thy_ctxt end;
    3.76  
    3.77      val thy_ctxt' = thy_ctxt
    3.78        (* add registrations *)
    3.79 @@ -2373,7 +2376,7 @@
    3.80                          disch (Element.inst_thm thy insts (satisfy th))))) thy) ths
    3.81                end;
    3.82  
    3.83 -            fun activate_elem (Notes (kind, facts)) thy =
    3.84 +            fun activate_elem (loc, ps) (Notes (kind, facts)) thy =
    3.85                  let
    3.86                    val att_morphism =
    3.87                      Morphism.name_morphism (NameSpace.qualified prfx) $>
    3.88 @@ -2386,12 +2389,12 @@
    3.89                      |> map (apsnd (map (apfst (map (disch o Element.inst_thm thy insts o satisfy)))))
    3.90                  in
    3.91                    thy
    3.92 -                  |> global_note_prefix_i kind (fully_qualified, prfx) facts'
    3.93 +                  |> global_note_prefix_i kind loc (fully_qualified, prfx) facts'
    3.94                    |> snd
    3.95                  end
    3.96 -              | activate_elem _ thy = thy;
    3.97 -
    3.98 -            fun activate_elems (_, elems) thy = fold activate_elem elems thy;
    3.99 +              | activate_elem _ _ thy = thy;
   3.100 +
   3.101 +            fun activate_elems ((id, _), elems) thy = fold (activate_elem id) elems thy;
   3.102  
   3.103            in thy |> fold activate_assumed_id ids_elemss_thmss
   3.104                   |> fold activate_derived_id ids_elemss