# HG changeset patch # User haftmann # Date 1186758264 -7200 # Node ID fbf1646b267c8a9e033f7a953c1b92af550b3e74 # Parent 5c4913b478f5cee1ffc7536febdce12e76ce472e ClassPackage renamed to Class diff -r 5c4913b478f5 -r fbf1646b267c src/HOL/Nominal/nominal_atoms.ML --- a/src/HOL/Nominal/nominal_atoms.ML Fri Aug 10 17:04:20 2007 +0200 +++ b/src/HOL/Nominal/nominal_atoms.ML Fri Aug 10 17:04:24 2007 +0200 @@ -409,14 +409,14 @@ val cls_name = Sign.full_name thy' ("pt_"^ak_name); val at_inst = PureThy.get_thm thy' (Name ("at_"^ak_name'^"_inst")); - val proof1 = EVERY [ClassPackage.intro_classes_tac [], + val proof1 = EVERY [Class.intro_classes_tac [], rtac ((at_inst RS at_pt_inst) RS pt1) 1, rtac ((at_inst RS at_pt_inst) RS pt2) 1, rtac ((at_inst RS at_pt_inst) RS pt3) 1, atac 1]; val simp_s = HOL_basic_ss addsimps PureThy.get_thmss thy' [Name (ak_name^"_prm_"^ak_name'^"_def")]; - val proof2 = EVERY [ClassPackage.intro_classes_tac [], REPEAT (asm_simp_tac simp_s 1)]; + val proof2 = EVERY [Class.intro_classes_tac [], REPEAT (asm_simp_tac simp_s 1)]; in thy' @@ -441,7 +441,7 @@ val pt_inst = PureThy.get_thm thy (Name ("pt_"^ak_name^"_inst")); fun pt_proof thm = - EVERY [ClassPackage.intro_classes_tac [], + EVERY [Class.intro_classes_tac [], rtac (thm RS pt1) 1, rtac (thm RS pt2) 1, rtac (thm RS pt3) 1, atac 1]; val pt_thm_fun = at_thm RS (pt_inst RS (pt_inst RS pt_fun_inst)); @@ -488,12 +488,12 @@ (if ak_name = ak_name' then let val at_thm = PureThy.get_thm thy' (Name ("at_"^ak_name^"_inst")); - in EVERY [ClassPackage.intro_classes_tac [], + in EVERY [Class.intro_classes_tac [], rtac ((at_thm RS fs_at_inst) RS fs1) 1] end else let val dj_inst = PureThy.get_thm thy' (Name ("dj_"^ak_name'^"_"^ak_name)); val simp_s = HOL_basic_ss addsimps [dj_inst RS dj_supp, finite_emptyI]; - in EVERY [ClassPackage.intro_classes_tac [], asm_simp_tac simp_s 1] end) + in EVERY [Class.intro_classes_tac [], asm_simp_tac simp_s 1] end) in AxClass.prove_arity (qu_name,[],[qu_class]) proof thy' end) ak_names thy) ak_names thy18; @@ -510,7 +510,7 @@ let val cls_name = Sign.full_name thy ("fs_"^ak_name); val fs_inst = PureThy.get_thm thy (Name ("fs_"^ak_name^"_inst")); - fun fs_proof thm = EVERY [ClassPackage.intro_classes_tac [], rtac (thm RS fs1) 1]; + fun fs_proof thm = EVERY [Class.intro_classes_tac [], rtac (thm RS fs1) 1]; val fs_thm_unit = fs_unit_inst; val fs_thm_prod = fs_inst RS (fs_inst RS fs_prod_inst); @@ -557,7 +557,7 @@ val pt_inst = PureThy.get_thm thy'' (Name ("pt_"^ak_name''^"_inst")); val at_inst = PureThy.get_thm thy'' (Name ("at_"^ak_name''^"_inst")); in - EVERY [ClassPackage.intro_classes_tac [], + EVERY [Class.intro_classes_tac [], rtac (at_inst RS (pt_inst RS pt_perm_compose)) 1] end) else @@ -569,7 +569,7 @@ [Name (ak_name' ^"_prm_"^ak_name^"_def"), Name (ak_name''^"_prm_"^ak_name^"_def")])); in - EVERY [ClassPackage.intro_classes_tac [], simp_tac simp_s 1] + EVERY [Class.intro_classes_tac [], simp_tac simp_s 1] end)) in AxClass.prove_arity (name,[],[cls_name]) proof thy'' @@ -592,7 +592,7 @@ val pt_inst = PureThy.get_thm thy' (Name ("pt_"^ak_name^"_inst")); val at_inst = PureThy.get_thm thy' (Name ("at_"^ak_name^"_inst")); - fun cp_proof thm = EVERY [ClassPackage.intro_classes_tac [],rtac (thm RS cp1) 1]; + fun cp_proof thm = EVERY [Class.intro_classes_tac [],rtac (thm RS cp1) 1]; val cp_thm_unit = cp_unit_inst; val cp_thm_prod = cp_inst RS (cp_inst RS cp_prod_inst); @@ -623,7 +623,7 @@ let val qu_class = Sign.full_name thy ("pt_"^ak_name); val simp_s = HOL_basic_ss addsimps [defn]; - val proof = EVERY [ClassPackage.intro_classes_tac [], REPEAT (asm_simp_tac simp_s 1)]; + val proof = EVERY [Class.intro_classes_tac [], REPEAT (asm_simp_tac simp_s 1)]; in AxClass.prove_arity (discrete_ty,[],[qu_class]) proof thy end) ak_names; @@ -634,7 +634,7 @@ val qu_class = Sign.full_name thy ("fs_"^ak_name); val supp_def = @{thm "Nominal.supp_def"}; val simp_s = HOL_ss addsimps [supp_def,Collect_const,finite_emptyI,defn]; - val proof = EVERY [ClassPackage.intro_classes_tac [], asm_simp_tac simp_s 1]; + val proof = EVERY [Class.intro_classes_tac [], asm_simp_tac simp_s 1]; in AxClass.prove_arity (discrete_ty,[],[qu_class]) proof thy end) ak_names; @@ -645,7 +645,7 @@ val qu_class = Sign.full_name thy ("cp_"^ak_name^"_"^ak_name'); val supp_def = @{thm "Nominal.supp_def"}; val simp_s = HOL_ss addsimps [defn]; - val proof = EVERY [ClassPackage.intro_classes_tac [], asm_simp_tac simp_s 1]; + val proof = EVERY [Class.intro_classes_tac [], asm_simp_tac simp_s 1]; in AxClass.prove_arity (discrete_ty,[],[qu_class]) proof thy end) ak_names)) ak_names; diff -r 5c4913b478f5 -r fbf1646b267c src/HOL/Nominal/nominal_package.ML --- a/src/HOL/Nominal/nominal_package.ML Fri Aug 10 17:04:20 2007 +0200 +++ b/src/HOL/Nominal/nominal_package.ML Fri Aug 10 17:04:24 2007 +0200 @@ -502,7 +502,7 @@ in foldl (fn ((s, tvs), thy) => AxClass.prove_arity (s, replicate (length tvs) (cp_class :: classes), [cp_class]) - (ClassPackage.intro_classes_tac [] THEN ALLGOALS (resolve_tac thms)) thy) + (Class.intro_classes_tac [] THEN ALLGOALS (resolve_tac thms)) thy) thy (full_new_type_names' ~~ tyvars) end; @@ -510,7 +510,7 @@ fold (fn name1 => fold (composition_instance name1) atoms) atoms |> curry (Library.foldr (fn ((i, (tyname, args, _)), thy) => AxClass.prove_arity (tyname, replicate (length args) classes, classes) - (ClassPackage.intro_classes_tac [] THEN REPEAT (EVERY + (Class.intro_classes_tac [] THEN REPEAT (EVERY [resolve_tac perm_empty_thms 1, resolve_tac perm_append_thms 1, resolve_tac perm_eq_thms 1, assume_tac 1])) thy)) @@ -681,7 +681,7 @@ AxClass.prove_arity (Sign.intern_type thy name, replicate (length tvs) (classes @ cp_classes), [class]) - (EVERY [ClassPackage.intro_classes_tac [], + (EVERY [Class.intro_classes_tac [], rewrite_goals_tac [perm_def], asm_full_simp_tac (simpset_of thy addsimps [Rep_inverse]) 1, asm_full_simp_tac (simpset_of thy addsimps @@ -706,7 +706,7 @@ AxClass.prove_arity (Sign.intern_type thy name, replicate (length tvs) (classes @ cp_classes), [class]) - (EVERY [ClassPackage.intro_classes_tac [], + (EVERY [Class.intro_classes_tac [], rewrite_goals_tac [perm_def], asm_full_simp_tac (simpset_of thy addsimps ((Rep RS perm_closed1 RS Abs_inverse) :: @@ -1142,7 +1142,7 @@ in fold (fn T => AxClass.prove_arity (fst (dest_Type T), replicate (length sorts) [class], [class]) - (ClassPackage.intro_classes_tac [] THEN resolve_tac ths 1)) newTs thy + (Class.intro_classes_tac [] THEN resolve_tac ths 1)) newTs thy end) (atoms ~~ finite_supp_thms); (**** strong induction theorem ****) diff -r 5c4913b478f5 -r fbf1646b267c src/HOL/Tools/datatype_abs_proofs.ML --- a/src/HOL/Tools/datatype_abs_proofs.ML Fri Aug 10 17:04:20 2007 +0200 +++ b/src/HOL/Tools/datatype_abs_proofs.ML Fri Aug 10 17:04:24 2007 +0200 @@ -428,7 +428,7 @@ in thy |> AxClass.prove_arity (tyco, replicate n HOLogic.typeS, [HOLogic.class_size]) - (ClassPackage.intro_classes_tac []) + (Class.intro_classes_tac []) end val (size_def_thms, thy') = diff -r 5c4913b478f5 -r fbf1646b267c src/HOL/Tools/datatype_package.ML --- a/src/HOL/Tools/datatype_package.ML Fri Aug 10 17:04:20 2007 +0200 +++ b/src/HOL/Tools/datatype_package.ML Fri Aug 10 17:04:24 2007 +0200 @@ -566,7 +566,7 @@ in thy |> AxClass.prove_arity (tyco, replicate n HOLogic.typeS, [HOLogic.class_size]) - (ClassPackage.intro_classes_tac []) + (Class.intro_classes_tac []) end val thy2' = thy diff -r 5c4913b478f5 -r fbf1646b267c src/HOLCF/Tools/pcpodef_package.ML --- a/src/HOLCF/Tools/pcpodef_package.ML Fri Aug 10 17:04:20 2007 +0200 +++ b/src/HOLCF/Tools/pcpodef_package.ML Fri Aug 10 17:04:24 2007 +0200 @@ -94,7 +94,7 @@ fun make_po tac theory = theory |> TypedefPackage.add_typedef_i def (SOME name) (t, vs, mx) set opt_morphs tac ||> AxClass.prove_arity (full_tname, lhs_sorts, ["Porder.sq_ord"]) - (ClassPackage.intro_classes_tac []) + (Class.intro_classes_tac []) ||>> PureThy.add_defs_i true [Thm.no_attributes less_def] |-> (fn ((_, {type_definition, set_def, ...}), [less_definition]) => AxClass.prove_arity (full_tname, lhs_sorts, ["Porder.po"]) diff -r 5c4913b478f5 -r fbf1646b267c src/Provers/classical.ML --- a/src/Provers/classical.ML Fri Aug 10 17:04:20 2007 +0200 +++ b/src/Provers/classical.ML Fri Aug 10 17:04:24 2007 +0200 @@ -1022,7 +1022,7 @@ fun default_tac rules ctxt cs facts = HEADGOAL (rule_tac rules ctxt cs facts) ORELSE - ClassPackage.default_intro_classes_tac facts; + Class.default_intro_classes_tac facts; in val rule = METHOD_CLASET' o rule_tac; diff -r 5c4913b478f5 -r fbf1646b267c src/Pure/Isar/class.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/Isar/class.ML Fri Aug 10 17:04:24 2007 +0200 @@ -0,0 +1,682 @@ +(* Title: Pure/Isar/class.ML + ID: $Id$ + Author: Florian Haftmann, TU Muenchen + +Type classes derived from primitive axclasses and locales. +*) + +signature CLASS = +sig + val fork_mixfix: bool -> string option -> mixfix -> mixfix * mixfix + + val axclass_cmd: bstring * xstring list + -> ((bstring * Attrib.src list) * string list) list -> theory -> class * theory + val class: bstring -> class list -> Element.context_i Locale.element list + -> string list -> theory -> string * Proof.context + val class_cmd: bstring -> string list -> Element.context Locale.element list + -> string list -> theory -> string * Proof.context + val instance_arity: arity list -> ((bstring * Attrib.src list) * term) list + -> theory -> Proof.state + val instance_arity_cmd: (bstring * string list * string) list + -> ((bstring * Attrib.src list) * string) list + -> theory -> Proof.state + val prove_instance_arity: tactic -> arity list + -> ((bstring * Attrib.src list) * term) list + -> theory -> theory + val instance_class: class * class -> theory -> Proof.state + val instance_class_cmd: string * string -> theory -> Proof.state + val instance_sort: class * sort -> theory -> Proof.state + val instance_sort_cmd: string * string -> theory -> Proof.state + val prove_instance_sort: tactic -> class * sort -> theory -> theory + + val class_of_locale: theory -> string -> class option + val add_const_in_class: string -> (string * term) * Syntax.mixfix + -> theory -> theory + + val print_classes: theory -> unit + val intro_classes_tac: thm list -> tactic + val default_intro_classes_tac: thm list -> tactic +end; + +structure Class : CLASS = +struct + +(** auxiliary **) + +fun fork_mixfix is_loc some_class mx = + let + val mx' = Syntax.unlocalize_mixfix mx; + val mx_global = if is_some some_class orelse (is_loc andalso mx = mx') + then NoSyn else mx'; + val mx_local = if is_loc then mx else NoSyn; + in (mx_global, mx_local) end; + +fun axclass_cmd (class, raw_superclasses) raw_specs thy = + let + val ctxt = ProofContext.init thy; + val superclasses = map (Sign.read_class thy) raw_superclasses; + val name_atts = map ((apsnd o map) (Attrib.attribute thy) o fst) raw_specs; + val axiomss = ProofContext.read_propp (ctxt, map (map (rpair []) o snd) raw_specs) + |> snd + |> (map o map) fst; + in AxClass.define_class (class, superclasses) [] (name_atts ~~ axiomss) thy end; + + +(** axclasses with implicit parameter handling **) + +(* axclass instances *) + +local + +fun gen_instance mk_prop add_thm after_qed insts thy = + let + fun after_qed' results = + ProofContext.theory ((fold o fold) add_thm results #> after_qed); + in + thy + |> ProofContext.init + |> Proof.theorem_i NONE after_qed' ((map (fn t => [(t, [])]) o maps (mk_prop thy)) insts) + end; + +in + +val axclass_instance_arity = + gen_instance (Logic.mk_arities oo Sign.cert_arity) AxClass.add_arity; +val axclass_instance_sort = + gen_instance (single oo (Logic.mk_classrel oo AxClass.cert_classrel)) + AxClass.add_classrel I o single; + +end; (*local*) + + +(* introducing axclasses with implicit parameter handling *) + +fun axclass_params (name, raw_superclasses) raw_consts raw_dep_axioms other_consts thy = + let + val superclasses = map (Sign.certify_class thy) raw_superclasses; + val consts = (map o apfst o apsnd) (Sign.certify_typ thy) raw_consts; + val prefix = Logic.const_of_class name; + fun mk_const_name c = NameSpace.map_base (NameSpace.append prefix) + (Sign.full_name thy c); + fun add_const ((c, ty), syn) = + Sign.add_consts_authentic [(c, ty, syn)] + #> pair (mk_const_name c, ty); + fun mk_axioms cs thy = + raw_dep_axioms thy cs + |> (map o apsnd o map) (Sign.cert_prop thy) + |> rpair thy; + fun add_constraint class (c, ty) = + Sign.add_const_constraint_i (c, SOME + (Term.map_type_tfree (fn (v, _) => TFree (v, [class])) ty)); + in + thy + |> Theory.add_path prefix + |> fold_map add_const consts + ||> Theory.restore_naming thy + |-> (fn cs => mk_axioms cs + #-> (fn axioms_prop => AxClass.define_class (name, superclasses) + (map fst cs @ other_consts) axioms_prop + #-> (fn class => `(fn thy => AxClass.get_definition thy class) + #-> (fn {intro, axioms, ...} => fold (add_constraint class) cs + #> pair (class, ((intro, (map Thm.prop_of axioms, axioms)), cs)))))) + end; + + +(* instances with implicit parameter handling *) + +local + +fun gen_read_def thy prep_att read_def ((raw_name, raw_atts), raw_t) = + let + val (_, t) = read_def thy (raw_name, raw_t); + val ((c, ty), _) = Sign.cert_def (Sign.pp thy) t; + val atts = map (prep_att thy) raw_atts; + val insts = Consts.typargs (Sign.consts_of thy) (c, ty); + val name = case raw_name + of "" => NONE + | _ => SOME raw_name; + in (c, (insts, ((name, t), atts))) end; + +fun read_def_cmd thy = gen_read_def thy Attrib.intern_src Theory.read_axm; +fun read_def thy = gen_read_def thy (K I) (K I); + +fun gen_instance_arity prep_arity read_def do_proof raw_arities raw_defs theory = + let + val arities = map (prep_arity theory) raw_arities; + val _ = if null arities then error "at least one arity must be given" else (); + val _ = case (duplicates (op =) o map #1) arities + of [] => () + | dupl_tycos => error ("type constructors occur more than once in arities: " + ^ (commas o map quote) dupl_tycos); + val super_sort = (Graph.all_succs o #classes o Sorts.rep_algebra o Sign.classes_of) theory + fun get_consts_class tyco ty class = + let + val cs = (these o Option.map snd o try (AxClass.params_of_class theory)) class; + val subst_ty = map_type_tfree (K ty); + in + map (fn (c, ty) => (c, ((tyco, class), subst_ty ty))) cs + end; + fun get_consts_sort (tyco, asorts, sort) = + let + val ty = Type (tyco, map (fn (v, sort) => TVar ((v, 0), sort)) (Name.names Name.context "'a" asorts)) + in maps (get_consts_class tyco ty) (super_sort sort) end; + val cs = maps get_consts_sort arities; + fun mk_typnorm thy (ty, ty_sc) = + case try (Sign.typ_match thy (Logic.varifyT ty_sc, ty)) Vartab.empty + of SOME env => SOME (Logic.varifyT #> Envir.typ_subst_TVars env #> Logic.unvarifyT) + | NONE => NONE; + fun read_defs defs cs thy_read = + let + fun read raw_def cs = + let + val (c, (inst, ((name_opt, t), atts))) = read_def thy_read raw_def; + val ty = Consts.instance (Sign.consts_of thy_read) (c, inst); + val ((tyco, class), ty') = case AList.lookup (op =) cs c + of NONE => error ("illegal definition for constant " ^ quote c) + | SOME class_ty => class_ty; + val name = case name_opt + of NONE => Thm.def_name (Logic.name_arity (tyco, [], c)) + | SOME name => name; + val t' = case mk_typnorm thy_read (ty', ty) + of NONE => error ("illegal definition for constant " ^ + quote (c ^ "::" ^ setmp show_sorts true + (Sign.string_of_typ thy_read) ty)) + | SOME norm => map_types norm t + in (((class, tyco), ((name, t'), atts)), AList.delete (op =) c cs) end; + in fold_map read defs cs end; + val (defs, _) = read_defs raw_defs cs + (fold Sign.primitive_arity arities (Theory.copy theory)); + fun get_remove_contraint c thy = + let + val ty = Sign.the_const_constraint thy c; + in + thy + |> Sign.add_const_constraint_i (c, NONE) + |> pair (c, Logic.unvarifyT ty) + end; + fun add_defs defs thy = + thy + |> PureThy.add_defs_i true (map ((apsnd o map) (Attrib.attribute thy) o snd) defs) + |-> (fn thms => pair (map fst defs ~~ thms)); + fun after_qed cs defs thy = + thy + |> fold Sign.add_const_constraint_i (map (apsnd SOME) cs) + |> fold (Code.add_func false o snd) defs; + in + theory + |> fold_map get_remove_contraint (map fst cs |> distinct (op =)) + ||>> add_defs defs + |-> (fn (cs, defs) => do_proof (after_qed cs defs) arities) + end; + +fun instance_arity_cmd' do_proof = gen_instance_arity Sign.read_arity read_def_cmd do_proof; +fun instance_arity' do_proof = gen_instance_arity Sign.cert_arity read_def do_proof; +fun tactic_proof tac after_qed arities = + fold (fn arity => AxClass.prove_arity arity tac) arities + #> after_qed; + +in + +val instance_arity_cmd = instance_arity_cmd' axclass_instance_arity; +val instance_arity = instance_arity' axclass_instance_arity; +val prove_instance_arity = instance_arity' o tactic_proof; + +end; (*local*) + + + +(** combining locales and axclasses **) + +(* theory data *) + +datatype class_data = ClassData of { + locale: string, + consts: (string * string) list + (*locale parameter ~> toplevel theory constant*), + v: string option, + intro: thm +} * thm list (*derived defs*); + +fun rep_classdata (ClassData c) = c; + +fun merge_pair f1 f2 ((x1, y1), (x2, y2)) = (f1 (x1, x2), f2 (y1, y2)); + +structure ClassData = TheoryDataFun +( + type T = class_data Graph.T * class Symtab.table (*locale name ~> class name*); + val empty = (Graph.empty, Symtab.empty); + val copy = I; + val extend = I; + fun merge _ = merge_pair (Graph.merge (K true)) (Symtab.merge (K true)); +); + + +(* queries *) + +val lookup_class_data = Option.map rep_classdata oo try o Graph.get_node o fst o ClassData.get; +fun class_of_locale thy = Symtab.lookup ((snd o ClassData.get) thy); + +fun the_class_data thy class = + case lookup_class_data thy class + of NONE => error ("undeclared class " ^ quote class) + | SOME data => data; + +val ancestry = Graph.all_succs o fst o ClassData.get; + +fun param_map thy = + let + fun params class = + let + val const_typs = (#params o AxClass.get_definition thy) class; + val const_names = (#consts o fst o the_class_data thy) class; + in + (map o apsnd) (fn c => (c, (the o AList.lookup (op =) const_typs) c)) const_names + end; + in maps params o ancestry thy end; + +fun these_defs thy = maps (these o Option.map snd o lookup_class_data thy) o ancestry thy; + +fun these_intros thy = + Graph.fold (fn (_, (data, _)) => insert Thm.eq_thm ((#intro o fst o rep_classdata) data)) + ((fst o ClassData.get) thy) []; + +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 Sign.certify_sort thy o Sign.super_classes thy) class], + Option.map (Pretty.str o prefix "locale: " o #locale o fst) (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.all_classes) + algebra + end; + + +(* updaters *) + +fun add_class_data ((class, superclasses), (locale, consts, v, intro)) = + ClassData.map (fn (gr, tab) => ( + gr + |> Graph.new_node (class, ClassData ({ locale = locale, consts = consts, + v = v, intro = intro }, [])) + |> fold (curry Graph.add_edge class) superclasses, + tab + |> Symtab.update (locale, class) + )); + +fun add_class_const_thm (class, thm) = (ClassData.map o apfst o Graph.map_node class) + (fn ClassData (data, thms) => ClassData (data, thm :: thms)); + +(* tactics and methods *) + +fun intro_classes_tac facts st = + let + val thy = Thm.theory_of_thm st; + val classes = Sign.all_classes thy; + val class_trivs = map (Thm.class_triv thy) classes; + val class_intros = these_intros thy; + fun add_axclass_intro class = + case try (AxClass.get_definition thy) class of SOME {intro, ...} => cons intro | _ => I; + val axclass_intros = fold add_axclass_intro classes []; + in + st + |> ((ALLGOALS (Method.insert_tac facts THEN' + REPEAT_ALL_NEW (resolve_tac (class_trivs @ class_intros @ axclass_intros)))) + THEN Tactic.distinct_subgoals_tac) + end; + +fun default_intro_classes_tac [] = intro_classes_tac [] + | default_intro_classes_tac _ = Tactical.no_tac; (*no error message!*) + +fun default_tac rules ctxt facts = + HEADGOAL (Method.some_rule_tac rules ctxt facts) ORELSE + default_intro_classes_tac facts; + +val _ = Context.add_setup (Method.add_methods + [("intro_classes", Method.no_args (Method.METHOD intro_classes_tac), + "back-chain introduction rules of classes"), + ("default", Method.thms_ctxt_args (Method.METHOD oo default_tac), + "apply some intro/elim rule")]); + + +(* tactical interfaces to locale commands *) + +fun prove_interpretation tac prfx_atts expr insts thy = + thy + |> Locale.interpretation_i I prfx_atts expr insts + |> Proof.global_terminal_proof (Method.Basic (K (Method.SIMPLE_METHOD tac), Position.none), NONE) + |> ProofContext.theory_of; + +fun prove_interpretation_in tac after_qed (name, expr) thy = + thy + |> Locale.interpretation_in_locale (ProofContext.theory after_qed) (name, expr) + |> Proof.global_terminal_proof (Method.Basic (K (Method.SIMPLE_METHOD tac), Position.none), NONE) + |> ProofContext.theory_of; + + +(* constructing class introduction and other rules from axclass and locale rules *) + +fun mk_instT class = Symtab.empty + |> Symtab.update (AxClass.param_tyvarname, TFree (AxClass.param_tyvarname, [class])); + +fun mk_inst class param_names cs = + Symtab.empty + |> fold2 (fn v => fn (c, ty) => Symtab.update (v, Const + (c, Term.map_type_tfree (fn (v, _) => TFree (v, [class])) ty))) param_names cs; + +fun OF_LAST thm1 thm2 = + let + val n = (length o Logic.strip_imp_prems o prop_of) thm2; + in (thm1 RSN (n, thm2)) end; + +fun strip_all_ofclass thy sort = + let + val typ = TVar ((AxClass.param_tyvarname, 0), sort); + fun prem_inclass t = + case Logic.strip_imp_prems t + of ofcls :: _ => try Logic.dest_inclass ofcls + | [] => NONE; + fun strip_ofclass class thm = + thm OF (fst o AxClass.of_sort thy (typ, [class])) AxClass.cache; + fun strip thm = case (prem_inclass o Thm.prop_of) thm + of SOME (_, class) => thm |> strip_ofclass class |> strip + | NONE => thm; + in strip end; + +fun class_intro thy locale class sups = + let + fun class_elim class = + case (map Drule.unconstrainTs o #axioms o AxClass.get_definition thy) class + of [thm] => SOME thm + | [] => NONE; + val pred_intro = case Locale.intros thy locale + of ([ax_intro], [intro]) => intro |> OF_LAST ax_intro |> SOME + | ([intro], []) => SOME intro + | ([], [intro]) => SOME intro + | _ => NONE; + val pred_intro' = pred_intro + |> Option.map (fn intro => intro OF map_filter class_elim sups); + val class_intro = (#intro o AxClass.get_definition thy) class; + val raw_intro = case pred_intro' + of SOME pred_intro => class_intro |> OF_LAST pred_intro + | NONE => class_intro; + val sort = Sign.super_classes thy class; + val typ = TVar ((AxClass.param_tyvarname, 0), sort); + val defs = these_defs thy sups; + in + raw_intro + |> Drule.instantiate' [SOME (Thm.ctyp_of thy typ)] [] + |> strip_all_ofclass thy sort + |> Thm.strip_shyps + |> MetaSimplifier.rewrite_rule defs + |> Drule.unconstrainTs + end; + +fun interpretation_in_rule thy (class1, class2) = + let + val (params, consts) = split_list (param_map thy [class1]); + (*FIXME also remember this at add_class*) + fun mk_axioms class = + let + val name_locale = (#locale o fst o the_class_data thy) class; + val inst = mk_inst class params consts; + in + Locale.global_asms_of thy name_locale + |> maps snd + |> (map o map_aterms) (fn Free (s, _) => (the o Symtab.lookup inst) s | t => t) + |> (map o map_types o map_atyps) (fn TFree _ => TFree ("'a", [class1]) | T => T) + |> map (ObjectLogic.ensure_propT thy) + end; + val (prems, concls) = pairself mk_axioms (class1, class2); + in + Goal.prove_global thy [] prems (Logic.mk_conjunction_list concls) + (Locale.intro_locales_tac true (ProofContext.init thy)) + end; + + +(* classes *) + +local + +fun read_param thy raw_t = + let + val t = Sign.read_term thy raw_t + in case try dest_Const t + of SOME (c, _) => c + | NONE => error ("Not a constant: " ^ Sign.string_of_term thy t) + end; + +fun gen_class add_locale prep_class prep_param bname + raw_supclasses raw_elems raw_other_consts thy = + let + (*FIXME need proper concept for reading locale statements*) + fun subst_classtyvar (_, _) = + TFree (AxClass.param_tyvarname, []) + | subst_classtyvar (v, sort) = + error ("Sort constraint illegal in type class, for type variable " ^ v ^ "::" ^ Sign.string_of_sort thy sort); + (*val subst_classtyvars = Element.map_ctxt {name = I, var = I, term = I, + typ = Term.map_type_tfree subst_classtyvar, fact = I, attrib = I};*) + val other_consts = map (prep_param thy) raw_other_consts; + val (elems, includes) = fold_rev (fn Locale.Elem e => apfst (cons e) + | Locale.Expr i => apsnd (cons i)) raw_elems ([], []); + val supclasses = map (prep_class thy) raw_supclasses; + val sups = filter (is_some o lookup_class_data thy) supclasses + |> Sign.certify_sort thy; + val supsort = Sign.certify_sort thy supclasses; + val suplocales = map (Locale.Locale o #locale o fst o the_class_data thy) sups; + val supexpr = Locale.Merge (suplocales @ includes); + val supparams = (map fst o Locale.parameters_of_expr thy) + (Locale.Merge suplocales); + val supconsts = AList.make (the o AList.lookup (op =) (param_map thy sups)) + (map fst supparams); + (*val elems_constrains = map + (Element.Constrains o apsnd (Term.map_type_tfree subst_classtyvar)) supparams;*) + fun mk_tyvar (_, sort) = TFree (AxClass.param_tyvarname, + if Sign.subsort thy (supsort, sort) then sort else error + ("Sort " ^ Sign.string_of_sort thy sort + ^ " is less general than permitted least general sort " + ^ Sign.string_of_sort thy supsort)); + fun extract_params thy name_locale = + let + val params = Locale.parameters_of thy name_locale; + val v = case (maps typ_tfrees o map (snd o fst)) params + of (v, _) :: _ => SOME v + | _ => NONE; + in + (v, (map (fst o fst) params, params + |> (map o apfst o apsnd o Term.map_type_tfree) mk_tyvar + |> (map o apsnd) (fork_mixfix true NONE #> fst) + |> chop (length supconsts) + |> snd)) + end; + fun extract_assumes name_locale params thy cs = + let + val consts = supconsts @ (map (fst o fst) params ~~ cs); + fun subst (Free (c, ty)) = + Const ((fst o the o AList.lookup (op =) consts) c, ty) + | subst t = t; + val super_defs = these_defs thy sups; + fun prep_asm ((name, atts), ts) = + ((NameSpace.base name, map (Attrib.attribute thy) atts), + (map o map_aterms) ((*MetaSimplifier.rewrite_term thy super_defs [] o *)subst) ts); + in + Locale.global_asms_of thy name_locale + |> map prep_asm + end; + fun note_intro name_axclass class_intro = + PureThy.note_thmss_qualified "" ((Logic.const_of_class o NameSpace.base) name_axclass) + [(("intro", []), [([class_intro], [])])] + #> snd + in + thy + |> add_locale (SOME "") bname supexpr ((*elems_constrains @*) elems) + |-> (fn name_locale => ProofContext.theory_result ( + `(fn thy => extract_params thy name_locale) + #-> (fn (v, (param_names, params)) => + axclass_params (bname, supsort) params (extract_assumes name_locale params) other_consts + #-> (fn (name_axclass, ((_, (ax_terms, ax_axioms)), consts)) => + `(fn thy => class_intro thy name_locale name_axclass sups) + #-> (fn class_intro => + add_class_data ((name_axclass, sups), + (name_locale, map (fst o fst) params ~~ map fst consts, v, + class_intro)) + (*FIXME: class_data should already contain data relevant + for interpretation; use this later for class target*) + (*FIXME: general export_fixes which may be parametrized + with pieces of an emerging class*) + #> note_intro name_axclass class_intro + #> prove_interpretation ((ALLGOALS o ProofContext.fact_tac) ax_axioms) + ((false, Logic.const_of_class bname), []) (Locale.Locale name_locale) + ((mk_instT name_axclass, mk_inst name_axclass param_names (map snd supconsts @ consts)), []) + #> pair name_axclass + ))))) + end; + +in + +val class_cmd = gen_class Locale.add_locale Sign.intern_class read_param; +val class = gen_class Locale.add_locale_i Sign.certify_class (K I); + +end; (*local*) + +local + +fun instance_subclass (class1, class2) thy = + let + val interp = interpretation_in_rule thy (class1, class2); + val ax = #axioms (AxClass.get_definition thy class1); + val intro = #intro (AxClass.get_definition thy class2) + |> Drule.instantiate' [SOME (Thm.ctyp_of thy + (TVar ((AxClass.param_tyvarname, 0), [class1])))] []; + val thm = + intro + |> OF_LAST (interp OF ax) + |> strip_all_ofclass thy (Sign.super_classes thy class2); + in + thy |> AxClass.add_classrel thm + end; + +fun instance_subsort (class, sort) thy = + let + val super_sort = (Graph.all_succs o #classes o Sorts.rep_algebra + o Sign.classes_of) thy sort; + val classes = filter_out (fn class' => Sign.subsort thy ([class], [class'])) + (rev super_sort); + in + thy |> fold (curry instance_subclass class) classes + end; + +fun instance_sort' do_proof (class, sort) theory = + let + val loc_name = (#locale o fst o the_class_data theory) class; + val loc_expr = + (Locale.Merge o map (Locale.Locale o #locale o fst o the_class_data theory)) sort; + in + theory + |> do_proof (instance_subsort (class, sort)) (loc_name, loc_expr) + end; + +fun gen_instance_sort prep_class prep_sort (raw_class, raw_sort) theory = + let + val class = prep_class theory raw_class; + val sort = prep_sort theory raw_sort; + in + theory + |> instance_sort' (Locale.interpretation_in_locale o ProofContext.theory) (class, sort) + end; + +fun gen_instance_class prep_class (raw_class, raw_superclass) theory = + let + val class = prep_class theory raw_class; + val superclass = prep_class theory raw_superclass; + in + theory + |> axclass_instance_sort (class, superclass) + end; + +in + +val instance_sort_cmd = gen_instance_sort Sign.read_class Sign.read_sort; +val instance_sort = gen_instance_sort Sign.certify_class Sign.certify_sort; +val prove_instance_sort = instance_sort' o prove_interpretation_in; +val instance_class_cmd = gen_instance_class Sign.read_class; +val instance_class = gen_instance_class Sign.certify_class; + +end; (*local*) + + +(** class target **) + +fun export_fixes thy class = + let + val v = (#v o fst o the_class_data thy) class; + val constrain_sort = curry (Sorts.inter_sort (Sign.classes_of thy)) [class]; + val subst_typ = Term.map_type_tfree (fn var as (w, sort) => + if SOME w = v then TFree (w, constrain_sort sort) else TFree var); + val consts = param_map thy [class]; + fun subst_aterm (t as Free (v, ty)) = (case AList.lookup (op =) consts v + of SOME (c, _) => Const (c, ty) + | NONE => t) + | subst_aterm t = t; + in map_types subst_typ #> Term.map_aterms subst_aterm end; + +fun add_const_in_class class ((c, rhs), syn) thy = + let + val prfx = (Logic.const_of_class o NameSpace.base) class; + fun mk_name inject c = + let + val n1 = Sign.full_name thy c; + val n2 = NameSpace.qualifier n1; + val n3 = NameSpace.base n1; + in NameSpace.implode (n2 :: inject @ [n3]) end; + val abbr' = mk_name [prfx, prfx] c; + val rhs' = export_fixes thy class rhs; + val ty' = Term.fastype_of rhs'; + val def = (c, Logic.mk_equals (Const (mk_name [prfx] c, ty'), rhs')); + val (syn', _) = fork_mixfix true NONE syn; + fun interpret def = + let + val def' = symmetric def + val tac = (ALLGOALS o ProofContext.fact_tac) [def']; + val name_locale = (#locale o fst o the_class_data thy) class; + val def_eq = Thm.prop_of def'; + val (params, consts) = split_list (param_map thy [class]); + in + prove_interpretation tac ((false, prfx), []) (Locale.Locale name_locale) + ((mk_instT class, mk_inst class params consts), [def_eq]) + #> add_class_const_thm (class, def') + end; + in + thy + |> Sign.hide_consts_i true [abbr'] + |> Sign.add_path prfx + |> Sign.add_consts_authentic [(c, ty', syn')] + |> Sign.parent_path + |> Sign.sticky_prefix prfx + |> PureThy.add_defs_i false [(def, [])] + |-> (fn [def] => interpret def) + |> Sign.restore_naming thy + end; + +end; diff -r 5c4913b478f5 -r fbf1646b267c src/Pure/Isar/theory_target.ML --- a/src/Pure/Isar/theory_target.ML Fri Aug 10 17:04:20 2007 +0200 +++ b/src/Pure/Isar/theory_target.ML Fri Aug 10 17:04:24 2007 +0200 @@ -83,12 +83,12 @@ let val U = map #2 xs ---> T; val t = Term.list_comb (Const (Sign.full_name thy c, U), map Free xs); - val (mx1, mx2) = ClassPackage.fork_mixfix is_loc some_class mx; + val (mx1, mx2) = Class.fork_mixfix is_loc some_class mx; val thy' = Sign.add_consts_authentic [(c, U, mx1)] thy; in (((c, mx2), t), thy') end; fun const_class (SOME class) ((c, _), mx) (_, t) = - ClassPackage.add_const_in_class class ((c, t), mx) + Class.add_const_in_class class ((c, t), mx) | const_class NONE _ _ = I; val (abbrs, lthy') = lthy @@ -136,7 +136,7 @@ val ((lhs as Const (full_c, _), rhs), lthy1) = lthy |> LocalTheory.theory_result (Sign.add_abbrev (#1 prmode) (c, u')); - val (mx1, mx2) = ClassPackage.fork_mixfix is_loc some_class mx; + val (mx1, mx2) = Class.fork_mixfix is_loc some_class mx; in lthy1 |> LocalTheory.theory (Sign.add_notation prmode [(lhs, mx1)]) @@ -341,7 +341,7 @@ let val thy = ProofContext.theory_of ctxt; val is_loc = loc <> ""; - val some_class = ClassPackage.class_of_locale thy loc; + val some_class = Class.class_of_locale thy loc; in ctxt |> Data.put (if is_loc then SOME loc else NONE) diff -r 5c4913b478f5 -r fbf1646b267c src/Pure/Tools/class_package.ML --- a/src/Pure/Tools/class_package.ML Fri Aug 10 17:04:20 2007 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,686 +0,0 @@ -(* Title: Pure/Tools/class_package.ML - ID: $Id$ - Author: Florian Haftmann, TU Muenchen - -Type classes derived from primitive axclasses and locales. -*) - -signature CLASS_PACKAGE = -sig - val fork_mixfix: bool -> string option -> mixfix -> mixfix * mixfix - - val axclass_cmd: bstring * xstring list - -> ((bstring * Attrib.src list) * string list) list -> theory -> class * theory - val class: bstring -> class list -> Element.context_i Locale.element list - -> string list -> theory -> string * Proof.context - val class_cmd: bstring -> string list -> Element.context Locale.element list - -> string list -> theory -> string * Proof.context - val instance_arity: arity list -> ((bstring * Attrib.src list) * term) list - -> theory -> Proof.state - val instance_arity_cmd: (bstring * string list * string) list - -> ((bstring * Attrib.src list) * string) list - -> theory -> Proof.state - val prove_instance_arity: tactic -> arity list - -> ((bstring * Attrib.src list) * term) list - -> theory -> theory - val instance_class: class * class -> theory -> Proof.state - val instance_class_cmd: string * string -> theory -> Proof.state - val instance_sort: class * sort -> theory -> Proof.state - val instance_sort_cmd: string * string -> theory -> Proof.state - val prove_instance_sort: tactic -> class * sort -> theory -> theory - - val class_of_locale: theory -> string -> class option - val add_const_in_class: string -> (string * term) * Syntax.mixfix - -> theory -> theory - - val print_classes: theory -> unit - val intro_classes_tac: thm list -> tactic - val default_intro_classes_tac: thm list -> tactic -end; - -structure ClassPackage : CLASS_PACKAGE = -struct - -(** auxiliary **) - -fun fork_mixfix is_loc some_class mx = - let - val mx' = Syntax.unlocalize_mixfix mx; - val mx_global = if is_some some_class orelse (is_loc andalso mx = mx') - then NoSyn else mx'; - val mx_local = if is_loc then mx else NoSyn; - in (mx_global, mx_local) end; - -fun axclass_cmd (class, raw_superclasses) raw_specs thy = - let - val ctxt = ProofContext.init thy; - val superclasses = map (Sign.read_class thy) raw_superclasses; - val name_atts = map ((apsnd o map) (Attrib.attribute thy) o fst) raw_specs; - val axiomss = ProofContext.read_propp (ctxt, map (map (rpair []) o snd) raw_specs) - |> snd - |> (map o map) fst; - in AxClass.define_class (class, superclasses) [] (name_atts ~~ axiomss) thy end; - - -(** AxClasses with implicit parameter handling **) - -(* AxClass instances *) - -local - -fun gen_instance mk_prop add_thm after_qed insts thy = - let - fun after_qed' results = - ProofContext.theory ((fold o fold) add_thm results #> after_qed); - in - thy - |> ProofContext.init - |> Proof.theorem_i NONE after_qed' ((map (fn t => [(t, [])]) o maps (mk_prop thy)) insts) - end; - -in - -val axclass_instance_arity = - gen_instance (Logic.mk_arities oo Sign.cert_arity) AxClass.add_arity; -val axclass_instance_sort = - gen_instance (single oo (Logic.mk_classrel oo AxClass.cert_classrel)) - AxClass.add_classrel I o single; - -end; (*local*) - - -(* introducing axclasses with implicit parameter handling *) - -fun axclass_params (name, raw_superclasses) raw_consts raw_dep_axioms other_consts thy = - let - val superclasses = map (Sign.certify_class thy) raw_superclasses; - val consts = (map o apfst o apsnd) (Sign.certify_typ thy) raw_consts; - val prefix = Logic.const_of_class name; - fun mk_const_name c = NameSpace.map_base (NameSpace.append prefix) - (Sign.full_name thy c); - fun add_const ((c, ty), syn) = - Sign.add_consts_authentic [(c, ty, syn)] - #> pair (mk_const_name c, ty); - fun mk_axioms cs thy = - raw_dep_axioms thy cs - |> (map o apsnd o map) (Sign.cert_prop thy) - |> rpair thy; - fun add_constraint class (c, ty) = - Sign.add_const_constraint_i (c, SOME - (Term.map_type_tfree (fn (v, _) => TFree (v, [class])) ty)); - in - thy - |> Theory.add_path prefix - |> fold_map add_const consts - ||> Theory.restore_naming thy - |-> (fn cs => mk_axioms cs - #-> (fn axioms_prop => AxClass.define_class (name, superclasses) - (map fst cs @ other_consts) axioms_prop - #-> (fn class => `(fn thy => AxClass.get_definition thy class) - #-> (fn {intro, axioms, ...} => fold (add_constraint class) cs - #> pair (class, ((intro, (map Thm.prop_of axioms, axioms)), cs)))))) - end; - - -(* instances with implicit parameter handling *) - -local - -fun gen_read_def thy prep_att read_def ((raw_name, raw_atts), raw_t) = - let - val (_, t) = read_def thy (raw_name, raw_t); - val ((c, ty), _) = Sign.cert_def (Sign.pp thy) t; - val atts = map (prep_att thy) raw_atts; - val insts = Consts.typargs (Sign.consts_of thy) (c, ty); - val name = case raw_name - of "" => NONE - | _ => SOME raw_name; - in (c, (insts, ((name, t), atts))) end; - -fun read_def_cmd thy = gen_read_def thy Attrib.intern_src Theory.read_axm; -fun read_def thy = gen_read_def thy (K I) (K I); - -fun gen_instance_arity prep_arity read_def do_proof raw_arities raw_defs theory = - let - val arities = map (prep_arity theory) raw_arities; - val _ = if null arities then error "at least one arity must be given" else (); - val _ = case (duplicates (op =) o map #1) arities - of [] => () - | dupl_tycos => error ("type constructors occur more than once in arities: " - ^ (commas o map quote) dupl_tycos); - val super_sort = (Graph.all_succs o #classes o Sorts.rep_algebra o Sign.classes_of) theory - fun get_consts_class tyco ty class = - let - val cs = (these o Option.map snd o try (AxClass.params_of_class theory)) class; - val subst_ty = map_type_tfree (K ty); - in - map (fn (c, ty) => (c, ((tyco, class), subst_ty ty))) cs - end; - fun get_consts_sort (tyco, asorts, sort) = - let - val ty = Type (tyco, map (fn (v, sort) => TVar ((v, 0), sort)) (Name.names Name.context "'a" asorts)) - in maps (get_consts_class tyco ty) (super_sort sort) end; - val cs = maps get_consts_sort arities; - fun mk_typnorm thy (ty, ty_sc) = - case try (Sign.typ_match thy (Logic.varifyT ty_sc, ty)) Vartab.empty - of SOME env => SOME (Logic.varifyT #> Envir.typ_subst_TVars env #> Logic.unvarifyT) - | NONE => NONE; - fun read_defs defs cs thy_read = - let - fun read raw_def cs = - let - val (c, (inst, ((name_opt, t), atts))) = read_def thy_read raw_def; - val ty = Consts.instance (Sign.consts_of thy_read) (c, inst); - val ((tyco, class), ty') = case AList.lookup (op =) cs c - of NONE => error ("illegal definition for constant " ^ quote c) - | SOME class_ty => class_ty; - val name = case name_opt - of NONE => Thm.def_name (Logic.name_arity (tyco, [], c)) - | SOME name => name; - val t' = case mk_typnorm thy_read (ty', ty) - of NONE => error ("illegal definition for constant " ^ - quote (c ^ "::" ^ setmp show_sorts true - (Sign.string_of_typ thy_read) ty)) - | SOME norm => map_types norm t - in (((class, tyco), ((name, t'), atts)), AList.delete (op =) c cs) end; - in fold_map read defs cs end; - val (defs, _) = read_defs raw_defs cs - (fold Sign.primitive_arity arities (Theory.copy theory)); - fun get_remove_contraint c thy = - let - val ty = Sign.the_const_constraint thy c; - in - thy - |> Sign.add_const_constraint_i (c, NONE) - |> pair (c, Logic.unvarifyT ty) - end; - fun add_defs defs thy = - thy - |> PureThy.add_defs_i true (map ((apsnd o map) (Attrib.attribute thy) o snd) defs) - |-> (fn thms => pair (map fst defs ~~ thms)); - fun after_qed cs defs thy = - thy - |> fold Sign.add_const_constraint_i (map (apsnd SOME) cs) - |> fold (CodegenData.add_func false o snd) defs; - in - theory - |> fold_map get_remove_contraint (map fst cs |> distinct (op =)) - ||>> add_defs defs - |-> (fn (cs, defs) => do_proof (after_qed cs defs) arities) - end; - -fun instance_arity_cmd' do_proof = gen_instance_arity Sign.read_arity read_def_cmd do_proof; -fun instance_arity' do_proof = gen_instance_arity Sign.cert_arity read_def do_proof; -fun tactic_proof tac after_qed arities = - fold (fn arity => AxClass.prove_arity arity tac) arities - #> after_qed; - -in - -val instance_arity_cmd = instance_arity_cmd' axclass_instance_arity; -val instance_arity = instance_arity' axclass_instance_arity; -val prove_instance_arity = instance_arity' o tactic_proof; - -end; (*local*) - - - -(** combining locales and axclasses **) - -(* theory data *) - -datatype class_data = ClassData of { - locale: string, - consts: (string * string) list - (*locale parameter ~> toplevel theory constant*), - v: string option, - intro: thm -} * thm list (*derived defs*); - -fun rep_classdata (ClassData c) = c; - -fun merge_pair f1 f2 ((x1, y1), (x2, y2)) = (f1 (x1, x2), f2 (y1, y2)); - -structure ClassData = TheoryDataFun -( - type T = class_data Graph.T * class Symtab.table (*locale name ~> class name*); - val empty = (Graph.empty, Symtab.empty); - val copy = I; - val extend = I; - fun merge _ = merge_pair (Graph.merge (K true)) (Symtab.merge (K true)); -); - - -(* queries *) - -val lookup_class_data = Option.map rep_classdata oo try o Graph.get_node o fst o ClassData.get; -fun class_of_locale thy = Symtab.lookup ((snd o ClassData.get) thy); - -fun the_class_data thy class = - case lookup_class_data thy class - of NONE => error ("undeclared class " ^ quote class) - | SOME data => data; - -val ancestry = Graph.all_succs o fst o ClassData.get; - -fun param_map thy = - let - fun params class = - let - val const_typs = (#params o AxClass.get_definition thy) class; - val const_names = (#consts o fst o the_class_data thy) class; - in - (map o apsnd) (fn c => (c, (the o AList.lookup (op =) const_typs) c)) const_names - end; - in maps params o ancestry thy end; - -fun these_defs thy = maps (these o Option.map snd o lookup_class_data thy) o ancestry thy; - -fun these_intros thy = - Graph.fold (fn (_, (data, _)) => insert Thm.eq_thm ((#intro o fst o rep_classdata) data)) - ((fst o ClassData.get) thy) []; - -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 Sign.certify_sort thy o Sign.super_classes thy) class], - Option.map (Pretty.str o prefix "locale: " o #locale o fst) (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.all_classes) - algebra - end; - - -(* updaters *) - -fun add_class_data ((class, superclasses), (locale, consts, v, intro)) = - ClassData.map (fn (gr, tab) => ( - gr - |> Graph.new_node (class, ClassData ({ locale = locale, consts = consts, - v = v, intro = intro }, [])) - |> fold (curry Graph.add_edge class) superclasses, - tab - |> Symtab.update (locale, class) - )); - -fun add_class_const_thm (class, thm) = (ClassData.map o apfst o Graph.map_node class) - (fn ClassData (data, thms) => ClassData (data, thm :: thms)); - -(* tactics and methods *) - -fun intro_classes_tac facts st = - let - val thy = Thm.theory_of_thm st; - val classes = Sign.all_classes thy; - val class_trivs = map (Thm.class_triv thy) classes; - val class_intros = these_intros thy; - fun add_axclass_intro class = - case try (AxClass.get_definition thy) class of SOME {intro, ...} => cons intro | _ => I; - val axclass_intros = fold add_axclass_intro classes []; - in - st - |> ((ALLGOALS (Method.insert_tac facts THEN' - REPEAT_ALL_NEW (resolve_tac (class_trivs @ class_intros @ axclass_intros)))) - THEN Tactic.distinct_subgoals_tac) - end; - -fun default_intro_classes_tac [] = intro_classes_tac [] - | default_intro_classes_tac _ = Tactical.no_tac; (*no error message!*) - -fun default_tac rules ctxt facts = - HEADGOAL (Method.some_rule_tac rules ctxt facts) ORELSE - default_intro_classes_tac facts; - -val _ = Context.add_setup (Method.add_methods - [("intro_classes", Method.no_args (Method.METHOD intro_classes_tac), - "back-chain introduction rules of classes"), - ("default", Method.thms_ctxt_args (Method.METHOD oo default_tac), - "apply some intro/elim rule")]); - - -(* tactical interfaces to locale commands *) - -fun prove_interpretation tac prfx_atts expr insts thy = - thy - |> Locale.interpretation_i I prfx_atts expr insts - |> Proof.global_terminal_proof (Method.Basic (K (Method.SIMPLE_METHOD tac), Position.none), NONE) - |> ProofContext.theory_of; - -fun prove_interpretation_in tac after_qed (name, expr) thy = - thy - |> Locale.interpretation_in_locale (ProofContext.theory after_qed) (name, expr) - |> Proof.global_terminal_proof (Method.Basic (K (Method.SIMPLE_METHOD tac), Position.none), NONE) - |> ProofContext.theory_of; - - -(* constructing class introduction and other rules from axclass and locale rules *) - -fun mk_instT class = Symtab.empty - |> Symtab.update (AxClass.param_tyvarname, TFree (AxClass.param_tyvarname, [class])); - -fun mk_inst class param_names cs = - Symtab.empty - |> fold2 (fn v => fn (c, ty) => Symtab.update (v, Const - (c, Term.map_type_tfree (fn (v, _) => TFree (v, [class])) ty))) param_names cs; - -fun OF_LAST thm1 thm2 = - let - val n = (length o Logic.strip_imp_prems o prop_of) thm2; - in (thm1 RSN (n, thm2)) end; - -fun strip_all_ofclass thy sort = - let - val typ = TVar ((AxClass.param_tyvarname, 0), sort); - fun prem_inclass t = - case Logic.strip_imp_prems t - of ofcls :: _ => try Logic.dest_inclass ofcls - | [] => NONE; - fun strip_ofclass class thm = - thm OF (fst o AxClass.of_sort thy (typ, [class])) AxClass.cache; - fun strip thm = case (prem_inclass o Thm.prop_of) thm - of SOME (_, class) => thm |> strip_ofclass class |> strip - | NONE => thm; - in strip end; - -fun class_intro thy locale class sups = - let - fun class_elim class = - case (map Drule.unconstrainTs o #axioms o AxClass.get_definition thy) class - of [thm] => SOME thm - | [] => NONE; - val pred_intro = case Locale.intros thy locale - of ([ax_intro], [intro]) => intro |> OF_LAST ax_intro |> SOME - | ([intro], []) => SOME intro - | ([], [intro]) => SOME intro - | _ => NONE; - val pred_intro' = pred_intro - |> Option.map (fn intro => intro OF map_filter class_elim sups); - val class_intro = (#intro o AxClass.get_definition thy) class; - val raw_intro = case pred_intro' - of SOME pred_intro => class_intro |> OF_LAST pred_intro - | NONE => class_intro; - val sort = Sign.super_classes thy class; - val typ = TVar ((AxClass.param_tyvarname, 0), sort); - val defs = these_defs thy sups; - in - raw_intro - |> Drule.instantiate' [SOME (Thm.ctyp_of thy typ)] [] - |> strip_all_ofclass thy sort - |> Thm.strip_shyps - |> MetaSimplifier.rewrite_rule defs - |> Drule.unconstrainTs - end; - -fun interpretation_in_rule thy (class1, class2) = - let - val (params, consts) = split_list (param_map thy [class1]); - (*FIXME also remember this at add_class*) - fun mk_axioms class = - let - val name_locale = (#locale o fst o the_class_data thy) class; - val inst = mk_inst class params consts; - in - Locale.global_asms_of thy name_locale - |> maps snd - |> (map o map_aterms) (fn Free (s, _) => (the o Symtab.lookup inst) s | t => t) - |> (map o map_types o map_atyps) (fn TFree _ => TFree ("'a", [class1]) | T => T) - |> map (ObjectLogic.ensure_propT thy) - end; - val (prems, concls) = pairself mk_axioms (class1, class2); - in - Goal.prove_global thy [] prems (Logic.mk_conjunction_list concls) - (Locale.intro_locales_tac true (ProofContext.init thy)) - end; - - -(* classes *) - -local - -fun read_param thy raw_t = - let - val t = Sign.read_term thy raw_t - in case try dest_Const t - of SOME (c, _) => c - | NONE => error ("Not a constant: " ^ Sign.string_of_term thy t) - end; - -fun gen_class add_locale prep_class prep_param bname - raw_supclasses raw_elems raw_other_consts thy = - let - (*FIXME need proper concept for reading locale statements*) - fun subst_classtyvar (_, _) = - TFree (AxClass.param_tyvarname, []) - | subst_classtyvar (v, sort) = - error ("Sort constraint illegal in type class, for type variable " ^ v ^ "::" ^ Sign.string_of_sort thy sort); - (*val subst_classtyvars = Element.map_ctxt {name = I, var = I, term = I, - typ = Term.map_type_tfree subst_classtyvar, fact = I, attrib = I};*) - val other_consts = map (prep_param thy) raw_other_consts; - val (elems, includes) = fold_rev (fn Locale.Elem e => apfst (cons e) - | Locale.Expr i => apsnd (cons i)) raw_elems ([], []); - val supclasses = map (prep_class thy) raw_supclasses; - val sups = filter (is_some o lookup_class_data thy) supclasses - |> Sign.certify_sort thy; - val supsort = Sign.certify_sort thy supclasses; - val suplocales = map (Locale.Locale o #locale o fst o the_class_data thy) sups; - val supexpr = Locale.Merge (suplocales @ includes); - val supparams = (map fst o Locale.parameters_of_expr thy) - (Locale.Merge suplocales); - val supconsts = AList.make (the o AList.lookup (op =) (param_map thy sups)) - (map fst supparams); - (*val elems_constrains = map - (Element.Constrains o apsnd (Term.map_type_tfree subst_classtyvar)) supparams;*) - fun mk_tyvar (_, sort) = TFree (AxClass.param_tyvarname, - if Sign.subsort thy (supsort, sort) then sort else error - ("Sort " ^ Sign.string_of_sort thy sort - ^ " is less general than permitted least general sort " - ^ Sign.string_of_sort thy supsort)); - fun extract_params thy name_locale = - let - val params = Locale.parameters_of thy name_locale; - val v = case (maps typ_tfrees o map (snd o fst)) params - of (v, _) :: _ => SOME v - | _ => NONE; - in - (v, (map (fst o fst) params, params - |> (map o apfst o apsnd o Term.map_type_tfree) mk_tyvar - |> (map o apsnd) (fork_mixfix true NONE #> fst) - |> chop (length supconsts) - |> snd)) - end; - fun extract_assumes name_locale params thy cs = - let - val consts = supconsts @ (map (fst o fst) params ~~ cs); - fun subst (Free (c, ty)) = - Const ((fst o the o AList.lookup (op =) consts) c, ty) - | subst t = t; - val super_defs = these_defs thy sups; - fun prep_asm ((name, atts), ts) = - ((NameSpace.base name, map (Attrib.attribute thy) atts), - (map o map_aterms) ((*MetaSimplifier.rewrite_term thy super_defs [] o *)subst) ts); - in - Locale.global_asms_of thy name_locale - |> map prep_asm - end; - fun note_intro name_axclass class_intro = - PureThy.note_thmss_qualified "" ((Logic.const_of_class o NameSpace.base) name_axclass) - [(("intro", []), [([class_intro], [])])] - #> snd - in - thy - |> add_locale (SOME "") bname supexpr ((*elems_constrains @*) elems) - |-> (fn name_locale => ProofContext.theory_result ( - `(fn thy => extract_params thy name_locale) - #-> (fn (v, (param_names, params)) => - axclass_params (bname, supsort) params (extract_assumes name_locale params) other_consts - #-> (fn (name_axclass, ((_, (ax_terms, ax_axioms)), consts)) => - `(fn thy => class_intro thy name_locale name_axclass sups) - #-> (fn class_intro => - add_class_data ((name_axclass, sups), - (name_locale, map (fst o fst) params ~~ map fst consts, v, - class_intro)) - (*FIXME: class_data should already contain data relevant - for interpretation; use this later for class target*) - (*FIXME: general export_fixes which may be parametrized - with pieces of an emerging class*) - #> note_intro name_axclass class_intro - #> prove_interpretation ((ALLGOALS o ProofContext.fact_tac) ax_axioms) - ((false, Logic.const_of_class bname), []) (Locale.Locale name_locale) - ((mk_instT name_axclass, mk_inst name_axclass param_names (map snd supconsts @ consts)), []) - #> pair name_axclass - ))))) - end; - -in - -val class_cmd = gen_class Locale.add_locale Sign.intern_class read_param; -val class = gen_class Locale.add_locale_i Sign.certify_class (K I); - -end; (*local*) - -local - -fun singular_instance_subclass (class1, class2) thy = - let - val interp = interpretation_in_rule thy (class1, class2); - val ax = #axioms (AxClass.get_definition thy class1); - val intro = #intro (AxClass.get_definition thy class2) - |> Drule.instantiate' [SOME (Thm.ctyp_of thy - (TVar ((AxClass.param_tyvarname, 0), [class1])))] []; - val thm = - intro - |> OF_LAST (interp OF ax) - |> strip_all_ofclass thy (Sign.super_classes thy class2); - in - thy |> AxClass.add_classrel thm - end; - -fun instance_subsort (class, sort) thy = - let - val super_sort = (Graph.all_succs o #classes o Sorts.rep_algebra - o Sign.classes_of) thy sort; - val classes = filter_out (fn class' => Sign.subsort thy ([class], [class'])) - (rev super_sort); - in - thy |> fold (curry singular_instance_subclass class) classes - end; - -fun instance_sort' do_proof (class, sort) theory = - let - val loc_name = (#locale o fst o the_class_data theory) class; - val loc_expr = - (Locale.Merge o map (Locale.Locale o #locale o fst o the_class_data theory)) sort; - in - theory - |> do_proof (instance_subsort (class, sort)) (loc_name, loc_expr) - end; - -fun gen_instance_sort prep_class prep_sort (raw_class, raw_sort) theory = - let - val class = prep_class theory raw_class; - val sort = prep_sort theory raw_sort; - in - theory - |> instance_sort' (Locale.interpretation_in_locale o ProofContext.theory) (class, sort) - end; - -fun gen_instance_class prep_class (raw_class, raw_superclass) theory = - let - val class = prep_class theory raw_class; - val superclass = prep_class theory raw_superclass; - in - theory - |> axclass_instance_sort (class, superclass) - end; - -in - -val instance_sort_cmd = gen_instance_sort Sign.read_class Sign.read_sort; -val instance_sort = gen_instance_sort Sign.certify_class Sign.certify_sort; -val prove_instance_sort = instance_sort' o prove_interpretation_in; -val instance_class_cmd = gen_instance_class Sign.read_class; -val instance_class = gen_instance_class Sign.certify_class; - -end; (*local*) - - -(** class target **) - -fun export_fixes thy class = - let - val v = (#v o fst o the_class_data thy) class; - val constrain_sort = curry (Sorts.inter_sort (Sign.classes_of thy)) [class]; - val subst_typ = Term.map_type_tfree (fn var as (w, sort) => - if SOME w = v then TFree (w, constrain_sort sort) else TFree var); - val consts = param_map thy [class]; - fun subst_aterm (t as Free (v, ty)) = (case AList.lookup (op =) consts v - of SOME (c, _) => Const (c, ty) - | NONE => t) - | subst_aterm t = t; - in map_types subst_typ #> Term.map_aterms subst_aterm end; - -fun add_const_in_class class ((c, rhs), syn) thy = - let - val prfx = (Logic.const_of_class o NameSpace.base) class; - fun mk_name inject c = - let - val n1 = Sign.full_name thy c; - val n2 = NameSpace.qualifier n1; - val n3 = NameSpace.base n1; - in NameSpace.implode (n2 :: inject @ [n3]) end; - val abbr' = mk_name [prfx, prfx] c; - val rhs' = export_fixes thy class rhs; - val ty' = Term.fastype_of rhs'; - val def = (c, Logic.mk_equals (Const (mk_name [prfx] c, ty'), rhs')); - val (syn', _) = fork_mixfix true NONE syn; - fun interpret def = - let - val def' = symmetric def - val tac = (ALLGOALS o ProofContext.fact_tac) [def']; - val name_locale = (#locale o fst o the_class_data thy) class; - val def_eq = Thm.prop_of def'; - val (params, consts) = split_list (param_map thy [class]); - in - prove_interpretation tac ((false, prfx), []) (Locale.Locale name_locale) - ((mk_instT class, mk_inst class params consts), [def_eq]) - #> add_class_const_thm (class, def') - end; - in - thy - |> Sign.hide_consts_i true [abbr'] - |> Sign.add_path prfx - |> Sign.add_consts_authentic [(c, ty', syn')] - |> Sign.parent_path - |> Sign.sticky_prefix prfx - |> PureThy.add_defs_i false [(def, [])] - |-> (fn [def] => interpret def) - |> Sign.restore_naming thy - end; - - -(** experimental interpretation_in **) - - -end;