# HG changeset patch # User haftmann # Date 1167390660 -3600 # Node ID fe474e69e603dafb8e32ec0a91bab98224a27c6c # Parent 663108ee4eef4a26b6dd9447697ebeaa41a127b5 simplified class_package diff -r 663108ee4eef -r fe474e69e603 src/HOL/Tools/datatype_codegen.ML --- a/src/HOL/Tools/datatype_codegen.ML Fri Dec 29 03:57:01 2006 +0100 +++ b/src/HOL/Tools/datatype_codegen.ML Fri Dec 29 12:11:00 2006 +0100 @@ -26,7 +26,7 @@ -> ((string * sort) list * (string * (bool * (string * typ list) list)) list) val get_codetypes_arities: theory -> (string * bool) list -> sort -> (string * (((string * sort list) * sort) * term list)) list option - val prove_codetypes_arities: (thm list -> tactic) -> (string * bool) list -> sort + val prove_codetypes_arities: tactic -> (string * bool) list -> sort -> (((string * sort list) * sort) list -> (string * term list) list -> theory -> ((bstring * attribute list) * term) list * theory) -> (((string * sort list) * sort) list -> (string * term list) list -> theory -> theory) @@ -612,7 +612,7 @@ |> not (null arities) ? ( f arities css #-> (fn defs => - ClassPackage.prove_instance_arity tac arities ("", []) defs + ClassPackage.prove_instance_arity tac arities defs #> after_qed arities css)) end; @@ -631,7 +631,7 @@ CodegenData.add_funcl (c, CodegenData.lazy get_thms) thy end; in - prove_codetypes_arities (K (ClassPackage.intro_classes_tac [])) + prove_codetypes_arities (ClassPackage.intro_classes_tac []) (map (fn (tyco, (is_dt, _)) => (tyco, is_dt)) specs) [HOLogic.class_eq] ((K o K o pair) []) ((K o K) (fold add_eq_thms specs)) end; diff -r 663108ee4eef -r fe474e69e603 src/HOL/ex/Classpackage.thy --- a/src/HOL/ex/Classpackage.thy Fri Dec 29 03:57:01 2006 +0100 +++ b/src/HOL/ex/Classpackage.thy Fri Dec 29 12:11:00 2006 +0100 @@ -16,14 +16,14 @@ "m \ n \ m + n" proof fix m n q :: nat - from semigroup_nat_def show "m \ n \ q = m \ (n \ q)" by simp + from mult_nat_def show "m \ n \ q = m \ (n \ q)" by simp qed instance int :: semigroup "k \ l \ k + l" proof fix k l j :: int - from semigroup_int_def show "k \ l \ j = k \ (l \ j)" by simp + from mult_int_def show "k \ l \ j = k \ (l \ j)" by simp qed instance list :: (type) semigroup @@ -32,7 +32,7 @@ fix xs ys zs :: "'a list" show "xs \ ys \ zs = xs \ (ys \ zs)" proof - - from semigroup_list_def have "\xs ys\'a list. xs \ ys \ xs @ ys" . + from mult_list_def have "\xs ys\'a list. xs \ ys \ xs @ ys" . thus ?thesis by simp qed qed @@ -41,15 +41,15 @@ fixes one :: 'a ("\<^loc>\") assumes neutl: "\<^loc>\ \<^loc>\ x = x" -instance monoidl_num_def: nat :: monoidl and int :: monoidl +instance nat :: monoidl and int :: monoidl "\ \ 0" "\ \ 0" proof fix n :: nat - from monoidl_num_def show "\ \ n = n" by simp + from mult_nat_def one_nat_def show "\ \ n = n" by simp next fix k :: int - from monoidl_num_def show "\ \ k = k" by simp + from mult_int_def one_int_def show "\ \ k = k" by simp qed instance list :: (type) monoidl @@ -59,7 +59,7 @@ show "\ \ xs = xs" proof - from mult_list_def have "\xs ys\'a list. xs \ ys \ xs @ ys" . - moreover from monoidl_list_def have "\ \ []\'a list" by simp + moreover from one_list_def have "\ \ []\'a list" by simp ultimately show ?thesis by simp qed qed @@ -67,13 +67,13 @@ class monoid = monoidl + assumes neutr: "x \<^loc>\ \<^loc>\ = x" -instance monoid_list_def: list :: (type) monoid +instance list :: (type) monoid proof fix xs :: "'a list" show "xs \ \ = xs" proof - from mult_list_def have "\xs ys\'a list. xs \ ys \ xs @ ys" . - moreover from monoid_list_def have "\ \ []\'a list" by simp + moreover from one_list_def have "\ \ []\'a list" by simp ultimately show ?thesis by simp qed qed @@ -81,19 +81,19 @@ class monoid_comm = monoid + assumes comm: "x \<^loc>\ y = y \<^loc>\ x" -instance monoid_comm_num_def: nat :: monoid_comm and int :: monoid_comm +instance nat :: monoid_comm and int :: monoid_comm proof fix n :: nat - from monoid_comm_num_def show "n \ \ = n" by simp + from mult_nat_def one_nat_def show "n \ \ = n" by simp next fix n m :: nat - from monoid_comm_num_def show "n \ m = m \ n" by simp + from mult_nat_def show "n \ m = m \ n" by simp next fix k :: int - from monoid_comm_num_def show "k \ \ = k" by simp + from mult_int_def one_int_def show "k \ \ = k" by simp next fix k l :: int - from monoid_comm_num_def show "k \ l = l \ k" by simp + from mult_int_def show "k \ l = l \ k" by simp qed context monoid @@ -181,11 +181,11 @@ class group_comm = group + monoid_comm -instance group_comm_int_def: int :: group_comm +instance int :: group_comm "\
k \ - (k\int)" proof fix k :: int - from group_comm_int_def show "\
k \ k = \" by simp + from mult_int_def one_int_def inv_int_def show "\
k \ k = \" by simp qed lemma (in group) cancel: @@ -296,27 +296,27 @@ "\<^loc>\ \<^loc>\ (k\int) = \<^loc>\" using pow_def nat_pow_one inv_one by simp -instance semigroup_prod_def: * :: (semigroup, semigroup) semigroup +instance * :: (semigroup, semigroup) semigroup mult_prod_def: "x \ y \ let (x1, x2) = x; (y1, y2) = y in (x1 \ y1, x2 \ y2)" -by default (simp_all add: split_paired_all semigroup_prod_def assoc) +by default (simp_all add: split_paired_all mult_prod_def assoc) -instance monoidl_prod_def: * :: (monoidl, monoidl) monoidl +instance * :: (monoidl, monoidl) monoidl one_prod_def: "\ \ (\, \)" -by default (simp_all add: split_paired_all monoidl_prod_def neutl) +by default (simp_all add: split_paired_all mult_prod_def one_prod_def neutl) -instance monoid_prod_def: * :: (monoid, monoid) monoid -by default (simp_all add: split_paired_all monoid_prod_def neutr) +instance * :: (monoid, monoid) monoid +by default (simp_all add: split_paired_all mult_prod_def one_prod_def neutr) -instance monoid_comm_prod_def: * :: (monoid_comm, monoid_comm) monoid_comm -by default (simp_all add: split_paired_all monoidl_prod_def comm) +instance * :: (monoid_comm, monoid_comm) monoid_comm +by default (simp_all add: split_paired_all mult_prod_def comm) -instance group_prod_def: * :: (group, group) group +instance * :: (group, group) group inv_prod_def: "\
x \ let (x1, x2) = x in (\
x1, \
x2)" -by default (simp_all add: split_paired_all group_prod_def invl) +by default (simp_all add: split_paired_all mult_prod_def one_prod_def inv_prod_def invl) -instance group_comm_prod_def: * :: (group_comm, group_comm) group_comm -by default (simp_all add: split_paired_all group_prod_def comm) +instance * :: (group_comm, group_comm) group_comm +by default (simp_all add: split_paired_all mult_prod_def comm) definition "X a b c = (a \ \ \ b, a \ \ \ b, [a, b] \ \ \ [a, b, c])" diff -r 663108ee4eef -r fe474e69e603 src/HOL/ex/CodeCollections.thy --- a/src/HOL/ex/CodeCollections.thy Fri Dec 29 03:57:01 2006 +0100 +++ b/src/HOL/ex/CodeCollections.thy Fri Dec 29 12:11:00 2006 +0100 @@ -37,7 +37,7 @@ instance unit :: order "u \ v \ True" "u < v \ False" - by default (simp_all add: order_unit_def) + by default (simp_all add: less_eq_unit_def less_unit_def) fun le_option' :: "'a\order option \ 'a option \ bool" where "le_option' None y \ True" @@ -47,7 +47,7 @@ instance option :: (order) order "x \ y \ le_option' x y" "x < y \ x \ y \ x \ y" -proof (default, unfold order_option_def) +proof (default, unfold less_eq_option_def less_option_def) fix x show "le_option' x x" by (cases x) simp_all next @@ -69,7 +69,7 @@ "None \ y \ True" "Some x \ None \ False" "Some v \ Some w \ v \ w" - unfolding order_option_def le_option'.simps by rule+ + unfolding less_eq_option_def less_option_def le_option'.simps by rule+ lemma forall_all [simp]: "list_all P xs \ (\x\set xs. P x)" @@ -99,12 +99,11 @@ end instance bool :: fin - (* FIXME: better name handling of definitions *) - "_1": "fin == [False, True]" + "fin == [False, True]" by default (simp_all add: fin_bool_def) instance unit :: fin - "_2": "fin == [()]" + "fin == [()]" by default (simp_all add: fin_unit_def) fun @@ -136,7 +135,7 @@ qed instance * :: (fin, fin) fin - "_3": "fin == product fin fin" + "fin == product fin fin" apply default apply (simp_all add: "fin_*_def") apply (unfold split_paired_all) @@ -145,7 +144,7 @@ done instance option :: (fin) fin - "_4": "fin == None # map Some fin" + "fin == None # map Some fin" proof (default, unfold fin_option_def) fix x :: "'a::fin option" show "x \ set (None # map Some fin)" diff -r 663108ee4eef -r fe474e69e603 src/HOL/ex/CodeEval.thy --- a/src/HOL/ex/CodeEval.thy Fri Dec 29 03:57:01 2006 +0100 +++ b/src/HOL/ex/CodeEval.thy Fri Dec 29 12:11:00 2006 +0100 @@ -40,9 +40,8 @@ fun mk arities _ thy = (maps (fn ((tyco, asorts), _) => [(("", []), TypOf.mk_typ_of_def (Type (tyco, map TFree (Name.names Name.context "'a" asorts))))]) arities, thy); - fun tac _ = ClassPackage.intro_classes_tac []; fun hook specs = - DatatypeCodegen.prove_codetypes_arities tac + DatatypeCodegen.prove_codetypes_arities (ClassPackage.intro_classes_tac []) (map (fn (tyco, (is_dt, _)) => (tyco, is_dt)) specs) [TypOf.class_typ_of] mk ((K o K) I) in DatatypeCodegen.add_codetypes_hook_bootstrap hook end @@ -101,11 +100,10 @@ |> PrimrecPackage.gen_primrec thy_note thy_def "" defs' |> snd end; - fun tac _ = ClassPackage.intro_classes_tac []; fun hook specs = if (fst o hd) specs = (fst o dest_Type) Embed.typ_typ then I else - DatatypeCodegen.prove_codetypes_arities tac + DatatypeCodegen.prove_codetypes_arities (ClassPackage.intro_classes_tac []) (map (fn (tyco, (is_dt, _)) => (tyco, is_dt)) specs) [TermOf.class_term_of] ((K o K o pair) []) mk in DatatypeCodegen.add_codetypes_hook_bootstrap hook end diff -r 663108ee4eef -r fe474e69e603 src/Pure/Tools/class_package.ML --- a/src/Pure/Tools/class_package.ML Fri Dec 29 03:57:01 2006 +0100 +++ b/src/Pure/Tools/class_package.ML Fri Dec 29 12:11:00 2006 +0100 @@ -12,13 +12,13 @@ val class_i: bstring -> class list -> Element.context_i Locale.element list -> theory -> string * Proof.context val instance_arity: ((bstring * string list) * string) list - -> bstring * Attrib.src list -> ((bstring * Attrib.src list) * string) list + -> ((bstring * Attrib.src list) * string) list -> theory -> Proof.state val instance_arity_i: ((bstring * sort list) * sort) list - -> bstring * attribute list -> ((bstring * attribute list) * term) list + -> ((bstring * attribute list) * term) list -> theory -> Proof.state - val prove_instance_arity: (thm list -> tactic) -> ((string * sort list) * sort) list - -> bstring * attribute list -> ((bstring * attribute list) * term) list + val prove_instance_arity: tactic -> ((string * sort list) * sort) list + -> ((bstring * attribute list) * term) list -> theory -> theory val instance_sort: string * string -> theory -> Proof.state val instance_sort_i: class * sort -> theory -> Proof.state @@ -49,14 +49,13 @@ (** theory data **) datatype class_data = ClassData of { - name_locale: string, - name_axclass: string, + locale: string, var: string, consts: (string * (string * typ)) list (*locale parameter ~> toplevel theory constant*), propnames: string list, defs: thm list -} * thm list Symtab.table; +}; fun rep_classdata (ClassData c) = c; @@ -67,29 +66,12 @@ val empty = Symtab.empty; val copy = I; val extend = I; - fun merge _ = Symtab.join (fn _ => fn (ClassData (classd, instd1), ClassData (_, instd2)) => - (ClassData (classd, Symtab.merge (K true) (instd1, instd2)))); - fun print thy data = - let - fun pretty_class (name, ClassData ({name_locale, name_axclass, var, consts, ...}, _)) = - (Pretty.block o Pretty.fbreaks) [ - Pretty.str ("class " ^ name ^ ":"), - Pretty.str ("locale: " ^ name_locale), - Pretty.str ("axclass: " ^ name_axclass), - Pretty.str ("class variable: " ^ var), - (Pretty.block o Pretty.fbreaks) ( - Pretty.str "constants: " - :: map (fn (_, (c, ty)) => Pretty.str (c ^ " :: " ^ Sign.string_of_typ thy ty)) consts - ) - ] - in - (Pretty.writeln o Pretty.chunks o map pretty_class o Symtab.dest) data - end; + fun merge _ = Symtab.merge (K true); + fun print _ _ = (); end ); val _ = Context.add_setup ClassData.init; -val print_classes = ClassData.print; (* queries *) @@ -113,42 +95,64 @@ |> fold ancestry ((maps proj_class o Sign.super_classes thy) class); in fold ancestry classes [] end; -val the_parm_map = #consts o fst oo the_class_data; +val the_parm_map = #consts oo the_class_data; -val the_propnames = #propnames o fst oo the_class_data; +val the_propnames = #propnames oo the_class_data; fun subst_clsvar v ty_subst = map_type_tfree (fn u as (w, _) => if w = v then ty_subst else TFree u); +fun print_classes thy = + let + val algebra = Sign.classes_of thy; + val arities = + Symtab.empty + |> Symtab.fold (fn (tyco, arities) => fold (fn (class, _) => + Symtab.map_default (class, []) (insert (op =) tyco)) arities) + ((#arities o Sorts.rep_algebra) algebra); + val the_arities = these o Symtab.lookup arities; + fun mk_arity class tyco = + let + val Ss = Sorts.mg_domain algebra tyco [class]; + in Sign.pretty_arity thy (tyco, Ss, [class]) end; + fun mk_param (c, ty) = Pretty.str (Sign.extern_const thy c ^ " :: " + ^ setmp show_sorts false (Sign.string_of_typ thy o Type.strip_sorts) ty); + fun mk_entry class = (Pretty.block o Pretty.fbreaks o map_filter I) [ + (SOME o Pretty.str) ("class " ^ class ^ ":"), + (SOME o Pretty.block) [Pretty.str "supersort: ", + (Sign.pretty_sort thy o Sorts.certify_sort algebra o Sorts.super_classes algebra) class], + Option.map (Pretty.str o prefix "locale: " o #locale) (lookup_class_data thy class), + ((fn [] => NONE | ps => (SOME o Pretty.block o Pretty.fbreaks) (Pretty.str "parameters:" :: ps)) o map mk_param + o these o Option.map #params o try (AxClass.get_definition thy)) class, + (SOME o Pretty.block o Pretty.breaks) [ + Pretty.str "instances:", + Pretty.list "" "" (map (mk_arity class) (the_arities class)) + ] + ] + in + (Pretty.writeln o Pretty.chunks o separate (Pretty.str "") o map mk_entry o Sorts.classes) algebra + end; + (* updaters *) -fun add_class_data (class, (name_locale, name_axclass, var, consts, propnames)) = +fun add_class_data (class, (locale, var, consts, propnames)) = ClassData.map ( - Symtab.update_new (class, ClassData ({ - name_locale = name_locale, - name_axclass = name_axclass, + Symtab.update_new (class, ClassData { + locale = locale, var = var, consts = consts, propnames = propnames, - defs = []}, Symtab.empty)) + defs = []}) ); fun add_def (class, thm) = - ClassData.map ( - Symtab.map_entry class (fn ClassData ({ name_locale, name_axclass, - var, consts, propnames, defs }, instd) => ClassData ({ name_locale = name_locale, - name_axclass = name_axclass, var = var, - consts = consts, propnames = propnames, defs = thm :: defs }, instd)) - ); - - -fun add_inst_def ((class, tyco), thm) = - ClassData.map ( - Symtab.map_entry class (fn ClassData (classd, instd) => - ClassData (classd, Symtab.insert_list eq_thm (tyco, thm) instd)) - ); + (ClassData.map o Symtab.map_entry class) + (fn ClassData { locale, + var, consts, propnames, defs } => ClassData { locale = locale, + var = var, + consts = consts, propnames = propnames, defs = thm :: defs }); (* experimental class target *) @@ -166,7 +170,7 @@ fun export_def thy loc = let val class = loc (*FIXME*); - val data = (fst o the_class_data thy) class; + val data = the_class_data thy class; val consts = #consts data; val v = #var data; val subst_typ = Term.map_type_tfree (fn var as (w, sort) => @@ -183,7 +187,7 @@ fun export_thm thy loc = let val class = loc (*FIXME*); - val thms = (#defs o fst o the_class_data thy) class; + val thms = (#defs o the_class_data thy) class; in MetaSimplifier.rewrite_rule thms end; @@ -312,12 +316,11 @@ val supclasses = map (prep_class thy) raw_supclasses; val supsort = supclasses - |> map (#name_axclass o fst o the_class_data thy) |> Sign.certify_sort thy |> (fn [] => Sign.defaultS thy | S => S); (* FIXME Why syntax defaultS? *) val expr_supclasses = Locale.Merge - (map (Locale.Locale o #name_locale o fst o the_class_data thy) supclasses); - val expr = Locale.Merge (map (Locale.Locale o #name_locale o fst o the_class_data thy) supclasses + (map (Locale.Locale o #locale o the_class_data thy) supclasses); + val expr = Locale.Merge (map (Locale.Locale o #locale o the_class_data thy) supclasses @ exprs); val mapp_sup = AList.make (the o AList.lookup (op =) ((flat o map (the_parm_map thy) o the_ancestry thy) supclasses)) @@ -375,7 +378,7 @@ add_axclass_i (bname, supsort) (map (fst o snd) mapp_this) loc_axioms #-> (fn (name_axclass, (_, ax_axioms)) => fold (add_global_constraint v name_axclass) mapp_this - #> add_class_data (name_locale, (name_locale, name_axclass, v, mapp_this, + #> add_class_data (name_locale, (name_locale, v, mapp_this, map (fst o fst) loc_axioms)) #> prove_interpretation_i (Logic.const_of_class bname, []) (Locale.Locale name_locale) (map (SOME o mk_const thy name_axclass v) (map snd (mapp_sup @ mapp_this))) @@ -406,7 +409,7 @@ fun read_def thy = gen_read_def thy Attrib.attribute read_axm; fun read_def_i thy = gen_read_def thy (K I) (K I); -fun gen_instance_arity prep_arity prep_att read_def do_proof raw_arities (raw_name, raw_atts) raw_defs theory = +fun gen_instance_arity prep_arity prep_att read_def do_proof raw_arities raw_defs theory = let fun prep_arity' ((tyco, asorts), sort) = prep_arity theory (tyco, asorts, sort); val arities = map prep_arity' raw_arities; @@ -416,12 +419,6 @@ of [] => () | dupl_tycos => error ("type constructors occur more than once in arities: " ^ (commas o map quote) dupl_tycos); - val (bind_always, name) = case raw_name - of "" => (false, Thm.def_name ((space_implode "_" o map NameSpace.base) - (maps (fn (tyco, _, sort) => sort @ [tyco]) - (sort (fn ((tyco1, _, _), (tyco2, _, _)) => string_ord (tyco1, tyco2)) arities)))) - | _ => (true, raw_name); - val atts = map (prep_att theory) raw_atts; fun get_consts_class tyco ty class = let val (_, cs) = AxClass.params_of_class theory class; @@ -469,21 +466,6 @@ thy |> PureThy.add_defs_i true (map snd defs) |-> (fn thms => pair (map fst defs ~~ thms)); - fun note_all thy = - (*FIXME: should avoid binding duplicated names*) - let - val bind = bind_always orelse not (can (PureThy.get_thms thy) (Name name)); - val thms = maps (fn (tyco, _, sort) => maps (fn class => - Symtab.lookup_list - ((the_default Symtab.empty o Option.map snd o try (the_class_data thy)) class) tyco) - (the_ancestry thy sort)) arities; - in if bind then - thy - |> PureThy.note_thmss_i (*qualified*) Thm.internalK [((name, atts), [(thms, [])])] - |> snd - else - thy - end; fun after_qed cs thy = thy |> fold Sign.add_const_constraint_i (map (apsnd SOME) cs); @@ -491,24 +473,21 @@ theory |> fold_map get_remove_contraint (map fst cs |> distinct (op =)) ||>> add_defs defs - |-> (fn (cs, def_thms) => - fold add_inst_def def_thms - #> note_all - #> do_proof (map snd def_thms) (after_qed cs) arities) + |-> (fn (cs, def_thms) => do_proof (after_qed cs) arities) end; fun instance_arity' do_proof = gen_instance_arity Sign.read_arity Attrib.attribute read_def do_proof; fun instance_arity_i' do_proof = gen_instance_arity Sign.cert_arity (K I) read_def_i do_proof; -fun tactic_proof tac def_thms after_qed arities = - fold (fn arity => AxClass.prove_arity arity (tac def_thms)) arities +fun tactic_proof tac after_qed arities = + fold (fn arity => AxClass.prove_arity arity tac) arities #> after_qed; in -val instance_arity = instance_arity' (K axclass_instance_arity_i); -val instance_arity_i = instance_arity_i' (K axclass_instance_arity_i); +val instance_arity = instance_arity' axclass_instance_arity_i; +val instance_arity_i = instance_arity_i' axclass_instance_arity_i; val prove_instance_arity = instance_arity_i' o tactic_proof; end; (*local*) @@ -526,11 +505,11 @@ let val class = prep_class theory raw_class; val sort = prep_sort theory raw_sort; - val loc_name = (#name_locale o fst o the_class_data theory) class; + val loc_name = (#locale o the_class_data theory) class; val loc_expr = - (Locale.Merge o map (Locale.Locale o #name_locale o fst o the_class_data theory)) sort; + (Locale.Merge o map (Locale.Locale o #locale o the_class_data theory)) sort; val const_names = (map (NameSpace.base o fst o snd) - o maps (#consts o fst o the_class_data theory) + o maps (#consts o the_class_data theory) o the_ancestry theory) [class]; fun get_thms thy = the_ancestry thy sort @@ -604,9 +583,9 @@ val instanceP = OuterSyntax.command instanceK "prove type arity or subclass relation" K.thy_goal (( P.xname -- ((P.$$$ "\\" || P.$$$ "<") |-- P.!!! P.xname) >> wrap_add_instance_sort - || P.opt_thm_name ":" -- (P.and_list1 parse_arity -- Scan.repeat (P.opt_thm_name ":" -- P.prop)) - >> (fn (("", []), ([((tyco, asorts), sort)], [])) => axclass_instance_arity I [(tyco, asorts, sort)] - | (natts, (arities, defs)) => instance_arity arities natts defs) + || P.and_list1 parse_arity -- Scan.repeat (P.opt_thm_name ":" -- P.prop) + >> (fn ([((tyco, asorts), sort)], []) => axclass_instance_arity I [(tyco, asorts, sort)] + | (arities, defs) => instance_arity arities defs) ) >> (Toplevel.print oo Toplevel.theory_to_proof)); val print_classesP =