switched to open locales for classes
authorhaftmann
Tue Jun 20 10:10:06 2006 +0200 (2006-06-20)
changeset 19928cb8472f4c5fd
parent 19927 9286e99b2808
child 19929 5c882c3e610b
switched to open locales for classes
src/HOL/ex/Classpackage.thy
src/Pure/Tools/class_package.ML
     1.1 --- a/src/HOL/ex/Classpackage.thy	Mon Jun 19 22:06:36 2006 +0200
     1.2 +++ b/src/HOL/ex/Classpackage.thy	Tue Jun 20 10:10:06 2006 +0200
     1.3 @@ -218,7 +218,7 @@
     1.4  qed
     1.5  
     1.6  interpretation group < monoid
     1.7 -proof
     1.8 +proof -
     1.9    fix x :: "'a"
    1.10    from neutr show "x \<^loc>\<otimes> \<^loc>\<one> = x" .
    1.11  qed
    1.12 @@ -226,7 +226,7 @@
    1.13  instance group < monoid
    1.14  proof
    1.15    fix x :: "'a::group"
    1.16 -  from group.mult_one.neutr [standard] show "x \<otimes> \<one> = x" .
    1.17 +  from group.neutr show "x \<otimes> \<one> = x" .
    1.18  qed
    1.19  
    1.20  lemma (in group) all_inv [intro]:
    1.21 @@ -290,7 +290,7 @@
    1.22  
    1.23  abbreviation (in group)
    1.24    abbrev_pow :: "'a \<Rightarrow> int \<Rightarrow> 'a" (infix "\<^loc>\<up>" 75)
    1.25 -  "x \<^loc>\<up> k == pow k x"
    1.26 +  "x \<^loc>\<up> k \<equiv> pow k x"
    1.27  
    1.28  lemma (in group) int_pow_zero:
    1.29    "x \<^loc>\<up> (0::int) = \<^loc>\<one>"
    1.30 @@ -305,16 +305,16 @@
    1.31                ((x1::'a::group) \<otimes> y1, (x2::'b::group) \<otimes> y2))"
    1.32    mult_one_def: "\<one> == (\<one>::'a::group, \<one>::'b::group)"
    1.33    mult_inv_def: "\<div> x == let (x1, x2) = x in (\<div> x1, \<div> x2)"
    1.34 -by default (simp_all add: split_paired_all group_prod_def semigroup.assoc monoidl.neutl group.invl)
    1.35 +by default (simp_all add: split_paired_all group_prod_def assoc neutl invl)
    1.36  
    1.37  instance group_comm_prod_def: (group_comm, group_comm) * :: group_comm
    1.38 -by default (simp_all add: split_paired_all group_prod_def semigroup.assoc monoidl.neutl group.invl monoid_comm.comm)
    1.39 +by default (simp_all add: split_paired_all group_prod_def assoc neutl invl comm)
    1.40  
    1.41  definition
    1.42    "x = ((2::nat) \<otimes> \<one> \<otimes> 3, (2::int) \<otimes> \<one> \<otimes> \<div> 3, [1::nat, 2] \<otimes> \<one> \<otimes> [1, 2, 3])"
    1.43    "y = (2 :: int, \<div> 2 :: int) \<otimes> \<one> \<otimes> (3, \<div> 3)"
    1.44  
    1.45 -code_generate (ml, haskell) "op \<otimes>" "\<one>" "inv"
    1.46 +code_generate "op \<otimes>" "\<one>" "inv"
    1.47  code_generate (ml, haskell) x
    1.48  code_generate (ml, haskell) y
    1.49  
     2.1 --- a/src/Pure/Tools/class_package.ML	Mon Jun 19 22:06:36 2006 +0200
     2.2 +++ b/src/Pure/Tools/class_package.ML	Tue Jun 20 10:10:06 2006 +0200
     2.3 @@ -63,7 +63,6 @@
     2.4  datatype class_data = ClassData of {
     2.5    name_locale: string,
     2.6    name_axclass: string,
     2.7 -  intro: thm option,
     2.8    var: string,
     2.9    consts: (string * (string * typ)) list
    2.10      (*locale parameter ~> toplevel const*)
    2.11 @@ -86,7 +85,7 @@
    2.12         Symtab.merge (op =) (f1, f2));
    2.13      fun print thy ((gr, _), _) =
    2.14        let
    2.15 -        fun pretty_class gr (name, ClassData {name_locale, name_axclass, intro, var, consts}) =
    2.16 +        fun pretty_class gr (name, ClassData {name_locale, name_axclass, var, consts}) =
    2.17            (Pretty.block o Pretty.fbreaks) [
    2.18              Pretty.str ("class " ^ name ^ ":"),
    2.19              (Pretty.block o Pretty.fbreaks) (
    2.20 @@ -165,11 +164,6 @@
    2.21        |> fold ancestry (the_superclasses thy class);
    2.22    in fold ancestry classes [] end;
    2.23  
    2.24 -fun the_intros thy =
    2.25 -  let
    2.26 -    val gr = (fst o fst o ClassData.get) thy;
    2.27 -  in (map_filter (#intro o rep_classdata o Graph.get_node gr) o Graph.keys) gr end;
    2.28 -
    2.29  fun subst_clsvar v ty_subst =
    2.30    map_type_tfree (fn u as (w, _) =>
    2.31      if w = v then ty_subst else TFree u);
    2.32 @@ -210,13 +204,12 @@
    2.33  
    2.34  (* updaters *)
    2.35  
    2.36 -fun add_class_data (class, (superclasses, name_locale, name_axclass, intro, var, consts)) =
    2.37 +fun add_class_data (class, (superclasses, name_locale, name_axclass, var, consts)) =
    2.38    ClassData.map (fn ((gr, tab), consttab) => ((
    2.39      gr
    2.40      |> Graph.new_node (class, ClassData {
    2.41           name_locale = name_locale,
    2.42           name_axclass = name_axclass,
    2.43 -         intro = intro,
    2.44           var = var,
    2.45           consts = consts
    2.46         })
    2.47 @@ -262,12 +255,9 @@
    2.48  
    2.49  (* tactics and methods *)
    2.50  
    2.51 -fun class_intros thy =
    2.52 -  AxClass.class_intros thy @ the_intros thy;
    2.53 -
    2.54  fun intro_classes_tac facts st =
    2.55    (ALLGOALS (Method.insert_tac facts THEN'
    2.56 -      REPEAT_ALL_NEW (resolve_tac (class_intros (Thm.theory_of_thm st))))
    2.57 +      REPEAT_ALL_NEW (resolve_tac (AxClass.class_intros (Thm.theory_of_thm st))))
    2.58      THEN Tactic.distinct_subgoals_tac) st;
    2.59  
    2.60  fun default_intro_classes_tac [] = intro_classes_tac []
    2.61 @@ -310,27 +300,6 @@
    2.62  
    2.63  local
    2.64  
    2.65 -fun intro_incr thy name expr =
    2.66 -  let
    2.67 -    fun fish_thm basename =
    2.68 -      try (PureThy.get_thm thy) ((Name o NameSpace.append basename) "intro");
    2.69 -  in if expr = Locale.empty
    2.70 -    then fish_thm name
    2.71 -    else fish_thm (name ^ "_axioms")
    2.72 -  end;
    2.73 -
    2.74 -fun add_locale name expr body thy =
    2.75 -  thy
    2.76 -  |> Locale.add_locale true name expr body
    2.77 -  ||>> `(fn thy => intro_incr thy name expr)
    2.78 -  |-> (fn ((name, ctxt), intro) => pair ((name, intro), ctxt));
    2.79 -
    2.80 -fun add_locale_i name expr body thy =
    2.81 -  thy
    2.82 -  |> Locale.add_locale_i true name expr body
    2.83 -  ||>> `(fn thy => intro_incr thy name expr)
    2.84 -  |-> (fn ((name, ctxt), intro) => pair ((name, intro), ctxt));
    2.85 -
    2.86  fun add_axclass_i (name, supsort) axs thy =
    2.87    let
    2.88      val (c, thy') = thy
    2.89 @@ -404,7 +373,7 @@
    2.90            map_aterms (fn Free (c, ty) => Const ((fst o the o AList.lookup (op =) cs_mapp) c, ty)
    2.91                         | t => t)
    2.92          fun prep_asm ((name, atts), ts) =
    2.93 -          ((name, map (Attrib.attribute thy) atts), map subst_assume ts)
    2.94 +          ((NameSpace.base name |> print, map (Attrib.attribute thy) atts), map subst_assume ts)
    2.95        in
    2.96          (map prep_asm o Locale.local_asms_of thy) name_locale
    2.97        end;
    2.98 @@ -416,17 +385,17 @@
    2.99    in
   2.100      thy
   2.101      |> add_locale bname expr raw_elems
   2.102 -    |-> (fn ((name_locale, intro), ctxt) =>
   2.103 +    |-> (fn (name_locale, ctxt) =>
   2.104            `(fn thy => extract_tyvar_consts thy name_locale)
   2.105      #-> (fn (v, (raw_cs_sup, raw_cs_this)) =>
   2.106            add_consts v raw_cs_sup raw_cs_this
   2.107      #-> (fn mapp_this =>
   2.108            `(fn thy => extract_assumes thy name_locale (mapp_sup @ mapp_this))
   2.109      #-> (fn loc_axioms =>
   2.110 -          add_axclass_i (bname, supsort) (map (apfst (apfst (K ""))) loc_axioms)
   2.111 +          add_axclass_i (bname, supsort) loc_axioms
   2.112      #-> (fn (name_axclass, (_, ax_axioms)) =>
   2.113            fold (add_global_constraint v name_axclass) mapp_this
   2.114 -    #> add_class_data (name_locale, (supclasses, name_locale, name_axclass, intro, v, mapp_this))
   2.115 +    #> add_class_data (name_locale, (supclasses, name_locale, name_axclass, v, mapp_this))
   2.116      #> prove_interpretation_i (NameSpace.base name_locale, [])
   2.117            (Locale.Locale name_locale) (map (SOME o mk_const thy name_axclass v) (map snd (mapp_sup @ mapp_this)))
   2.118            ((ALLGOALS o resolve_tac) ax_axioms)
   2.119 @@ -436,8 +405,8 @@
   2.120  
   2.121  in
   2.122  
   2.123 -val class = gen_class add_locale intern_class;
   2.124 -val class_i = gen_class add_locale_i certify_class;
   2.125 +val class = gen_class (Locale.add_locale false) intern_class;
   2.126 +val class_i = gen_class (Locale.add_locale_i false) certify_class;
   2.127  
   2.128  end; (* local *)
   2.129