--- a/src/HOL/ex/Classpackage.thy Mon Jun 19 22:06:36 2006 +0200
+++ b/src/HOL/ex/Classpackage.thy Tue Jun 20 10:10:06 2006 +0200
@@ -218,7 +218,7 @@
qed
interpretation group < monoid
-proof
+proof -
fix x :: "'a"
from neutr show "x \<^loc>\<otimes> \<^loc>\<one> = x" .
qed
@@ -226,7 +226,7 @@
instance group < monoid
proof
fix x :: "'a::group"
- from group.mult_one.neutr [standard] show "x \<otimes> \<one> = x" .
+ from group.neutr show "x \<otimes> \<one> = x" .
qed
lemma (in group) all_inv [intro]:
@@ -290,7 +290,7 @@
abbreviation (in group)
abbrev_pow :: "'a \<Rightarrow> int \<Rightarrow> 'a" (infix "\<^loc>\<up>" 75)
- "x \<^loc>\<up> k == pow k x"
+ "x \<^loc>\<up> k \<equiv> pow k x"
lemma (in group) int_pow_zero:
"x \<^loc>\<up> (0::int) = \<^loc>\<one>"
@@ -305,16 +305,16 @@
((x1::'a::group) \<otimes> y1, (x2::'b::group) \<otimes> y2))"
mult_one_def: "\<one> == (\<one>::'a::group, \<one>::'b::group)"
mult_inv_def: "\<div> x == let (x1, x2) = x in (\<div> x1, \<div> x2)"
-by default (simp_all add: split_paired_all group_prod_def semigroup.assoc monoidl.neutl group.invl)
+by default (simp_all add: split_paired_all group_prod_def assoc neutl invl)
instance group_comm_prod_def: (group_comm, group_comm) * :: group_comm
-by default (simp_all add: split_paired_all group_prod_def semigroup.assoc monoidl.neutl group.invl monoid_comm.comm)
+by default (simp_all add: split_paired_all group_prod_def assoc neutl invl comm)
definition
"x = ((2::nat) \<otimes> \<one> \<otimes> 3, (2::int) \<otimes> \<one> \<otimes> \<div> 3, [1::nat, 2] \<otimes> \<one> \<otimes> [1, 2, 3])"
"y = (2 :: int, \<div> 2 :: int) \<otimes> \<one> \<otimes> (3, \<div> 3)"
-code_generate (ml, haskell) "op \<otimes>" "\<one>" "inv"
+code_generate "op \<otimes>" "\<one>" "inv"
code_generate (ml, haskell) x
code_generate (ml, haskell) y
--- a/src/Pure/Tools/class_package.ML Mon Jun 19 22:06:36 2006 +0200
+++ b/src/Pure/Tools/class_package.ML Tue Jun 20 10:10:06 2006 +0200
@@ -63,7 +63,6 @@
datatype class_data = ClassData of {
name_locale: string,
name_axclass: string,
- intro: thm option,
var: string,
consts: (string * (string * typ)) list
(*locale parameter ~> toplevel const*)
@@ -86,7 +85,7 @@
Symtab.merge (op =) (f1, f2));
fun print thy ((gr, _), _) =
let
- fun pretty_class gr (name, ClassData {name_locale, name_axclass, intro, var, consts}) =
+ fun pretty_class gr (name, ClassData {name_locale, name_axclass, var, consts}) =
(Pretty.block o Pretty.fbreaks) [
Pretty.str ("class " ^ name ^ ":"),
(Pretty.block o Pretty.fbreaks) (
@@ -165,11 +164,6 @@
|> fold ancestry (the_superclasses thy class);
in fold ancestry classes [] end;
-fun the_intros thy =
- let
- val gr = (fst o fst o ClassData.get) thy;
- in (map_filter (#intro o rep_classdata o Graph.get_node gr) o Graph.keys) gr end;
-
fun subst_clsvar v ty_subst =
map_type_tfree (fn u as (w, _) =>
if w = v then ty_subst else TFree u);
@@ -210,13 +204,12 @@
(* updaters *)
-fun add_class_data (class, (superclasses, name_locale, name_axclass, intro, var, consts)) =
+fun add_class_data (class, (superclasses, name_locale, name_axclass, var, consts)) =
ClassData.map (fn ((gr, tab), consttab) => ((
gr
|> Graph.new_node (class, ClassData {
name_locale = name_locale,
name_axclass = name_axclass,
- intro = intro,
var = var,
consts = consts
})
@@ -262,12 +255,9 @@
(* tactics and methods *)
-fun class_intros thy =
- AxClass.class_intros thy @ the_intros thy;
-
fun intro_classes_tac facts st =
(ALLGOALS (Method.insert_tac facts THEN'
- REPEAT_ALL_NEW (resolve_tac (class_intros (Thm.theory_of_thm st))))
+ REPEAT_ALL_NEW (resolve_tac (AxClass.class_intros (Thm.theory_of_thm st))))
THEN Tactic.distinct_subgoals_tac) st;
fun default_intro_classes_tac [] = intro_classes_tac []
@@ -310,27 +300,6 @@
local
-fun intro_incr thy name expr =
- let
- fun fish_thm basename =
- try (PureThy.get_thm thy) ((Name o NameSpace.append basename) "intro");
- in if expr = Locale.empty
- then fish_thm name
- else fish_thm (name ^ "_axioms")
- end;
-
-fun add_locale name expr body thy =
- thy
- |> Locale.add_locale true name expr body
- ||>> `(fn thy => intro_incr thy name expr)
- |-> (fn ((name, ctxt), intro) => pair ((name, intro), ctxt));
-
-fun add_locale_i name expr body thy =
- thy
- |> Locale.add_locale_i true name expr body
- ||>> `(fn thy => intro_incr thy name expr)
- |-> (fn ((name, ctxt), intro) => pair ((name, intro), ctxt));
-
fun add_axclass_i (name, supsort) axs thy =
let
val (c, thy') = thy
@@ -404,7 +373,7 @@
map_aterms (fn Free (c, ty) => Const ((fst o the o AList.lookup (op =) cs_mapp) c, ty)
| t => t)
fun prep_asm ((name, atts), ts) =
- ((name, map (Attrib.attribute thy) atts), map subst_assume ts)
+ ((NameSpace.base name |> print, map (Attrib.attribute thy) atts), map subst_assume ts)
in
(map prep_asm o Locale.local_asms_of thy) name_locale
end;
@@ -416,17 +385,17 @@
in
thy
|> add_locale bname expr raw_elems
- |-> (fn ((name_locale, intro), ctxt) =>
+ |-> (fn (name_locale, ctxt) =>
`(fn thy => extract_tyvar_consts thy name_locale)
#-> (fn (v, (raw_cs_sup, raw_cs_this)) =>
add_consts v raw_cs_sup raw_cs_this
#-> (fn mapp_this =>
`(fn thy => extract_assumes thy name_locale (mapp_sup @ mapp_this))
#-> (fn loc_axioms =>
- add_axclass_i (bname, supsort) (map (apfst (apfst (K ""))) loc_axioms)
+ add_axclass_i (bname, supsort) loc_axioms
#-> (fn (name_axclass, (_, ax_axioms)) =>
fold (add_global_constraint v name_axclass) mapp_this
- #> add_class_data (name_locale, (supclasses, name_locale, name_axclass, intro, v, mapp_this))
+ #> add_class_data (name_locale, (supclasses, name_locale, name_axclass, v, mapp_this))
#> prove_interpretation_i (NameSpace.base name_locale, [])
(Locale.Locale name_locale) (map (SOME o mk_const thy name_axclass v) (map snd (mapp_sup @ mapp_this)))
((ALLGOALS o resolve_tac) ax_axioms)
@@ -436,8 +405,8 @@
in
-val class = gen_class add_locale intern_class;
-val class_i = gen_class add_locale_i certify_class;
+val class = gen_class (Locale.add_locale false) intern_class;
+val class_i = gen_class (Locale.add_locale_i false) certify_class;
end; (* local *)