# HG changeset patch # User wenzelm # Date 1144922455 -7200 # Node ID 03b01c9314fc1bb8730e757f27ff8b1721854aa4 # Parent 3a9d25bdd7f4b65d9753e2b54f23dcb9eb813afd reworded add_axclass(_i): canonical specification format, purely definitional version, always qualify intro/axioms; diff -r 3a9d25bdd7f4 -r 03b01c9314fc src/Pure/axclass.ML --- a/src/Pure/axclass.ML Thu Apr 13 12:00:54 2006 +0200 +++ b/src/Pure/axclass.ML Thu Apr 13 12:00:55 2006 +0200 @@ -8,16 +8,12 @@ signature AX_CLASS = sig val print_axclasses: theory -> unit - val get_info: theory -> class -> {super_classes: class list, intro: thm, axioms: thm list} + val get_info: theory -> class -> {super: sort, def: thm, intro: thm, axioms: thm list} val get_instances: theory -> {classes: unit Graph.T, classrel: ((class * class) * thm) list, arities: ((string * sort list * class) * thm) list} val class_intros: theory -> thm list - val add_axclass: bstring * xstring list -> string list -> - ((bstring * string) * Attrib.src list) list -> theory -> class * theory - val add_axclass_i: bstring * class list -> string list -> - ((bstring * term) * attribute list) list -> theory -> class * theory val params_of_sort: theory -> sort -> string list val cert_classrel: theory -> class * class -> class * class val read_classrel: theory -> xstring * xstring -> class * class @@ -25,6 +21,10 @@ val add_arity: thm -> theory -> theory val prove_classrel: class * class -> tactic -> theory -> theory val prove_arity: string * sort list * sort -> tactic -> theory -> theory + val add_axclass: bstring * xstring list -> string list -> + ((bstring * Attrib.src list) * string list) list -> theory -> class * theory + val add_axclass_i: bstring * class list -> string list -> + ((bstring * attribute list) * term list) list -> theory -> class * theory end; structure AxClass: AX_CLASS = @@ -54,12 +54,13 @@ val axiomsN = "axioms"; datatype axclass = AxClass of - {super_classes: class list, + {super: sort, + def: thm, intro: thm, axioms: thm list}; -fun make_axclass (super_classes, intro, axioms) = - AxClass {super_classes = super_classes, intro = intro, axioms = axioms}; +fun make_axclass (super, def, intro, axioms) = + AxClass {super = super, def = def, intro = intro, axioms = axioms}; type axclasses = axclass Symtab.table * param list; @@ -111,11 +112,12 @@ | pretty_class c cs = Pretty.block (prt_cls c :: Pretty.str " <" :: Pretty.brk 1 :: Pretty.commas (map prt_cls cs)); - fun pretty_axclass (class, AxClass {super_classes, intro, axioms}) = + fun pretty_axclass (class, AxClass {super, def, intro, axioms}) = Pretty.block (Pretty.fbreaks - [pretty_class class super_classes, + [pretty_class class super, Pretty.strs ("parameters:" :: fold (fn (x, c) => if c = class then cons x else I) params []), + ProofContext.pretty_fact ctxt ("def", [def]), ProofContext.pretty_fact ctxt (introN, [intro]), ProofContext.pretty_fact ctxt (axiomsN, axioms)]); in @@ -129,9 +131,6 @@ val get_instances = AxClassData.get #> (fn (_, Instances insts) => insts); - -(** axclass definitions **) - (* lookup *) val lookup_info = Symtab.lookup o #1 o #1 o AxClassData.get; @@ -149,81 +148,8 @@ in map (Thm.class_triv thy) classes @ fold add_intro classes [] end; -(* add_axclass(_i) *) -local - -fun err_bad_axsort ax c = - error ("Sort constraint in axiom " ^ quote ax ^ " not supersort of " ^ quote c); - -fun err_bad_tfrees ax = - error ("More than one type variable in axiom " ^ quote ax); - -fun replace_tfree T = map_term_types (Term.map_atyps (fn TFree _ => T | U => U)); - -fun gen_axclass prep_class prep_axm prep_att - (bclass, raw_super_classes) params raw_axioms_atts thy = - let - val pp = Sign.pp thy; - - val class = Sign.full_name thy bclass; - val super_classes = map (prep_class thy) raw_super_classes; - - val axms = map (prep_axm thy o fst) raw_axioms_atts; - val atts = map (map (prep_att thy) o snd) raw_axioms_atts; - - (*declare class*) - val class_thy = - thy |> Theory.add_classes_i [(bclass, super_classes)]; - - (*prepare abstract axioms*) - fun abs_axm ax = - if null (term_tfrees ax) then - Logic.mk_implies (Logic.mk_inclass (Term.aT [], class), ax) - else replace_tfree (Term.aT [class]) ax; - val abs_axms = map (abs_axm o snd) axms; - - fun axm_sort (name, ax) = - (case term_tfrees ax of - [] => [] - | [(_, S)] => if Sign.subsort class_thy ([class], S) then S else err_bad_axsort name class - | _ => err_bad_tfrees name); - val axS = Sign.certify_sort class_thy (List.concat (map axm_sort axms)); - - val int_axm = Logic.close_form o replace_tfree (Term.aT axS); - fun inclass c = Logic.mk_inclass (Term.aT axS, c); - - val intro_axm = Logic.list_implies - (map inclass super_classes @ map (int_axm o #2) axms, inclass class); - - (*declare axioms and rule*) - val (([intro], [axioms]), axms_thy) = - class_thy - |> Theory.add_path (Logic.const_of_class bclass) - |> PureThy.add_axioms_i [Thm.no_attributes (introN, intro_axm)] - ||>> PureThy.add_axiomss_i [Thm.no_attributes (axiomsN, abs_axms)]; - val info = make_axclass (super_classes, intro, axioms); - - (*store info*) - val (_, final_thy) = - axms_thy - |> Theory.add_finals_i false [Const (Logic.const_of_class class, Term.a_itselfT --> propT)] - |> PureThy.add_thms ((map #1 axms ~~ axioms) ~~ atts) - ||> Theory.restore_naming class_thy - ||> AxClassData.map (apfst (fn (is, ps) => - (Symtab.update (class, info) is, fold (fn x => add_param pp (x, class)) params ps))); - in (class, final_thy) end; - -in - -val add_axclass = gen_axclass Sign.intern_class Theory.read_axm Attrib.attribute; -val add_axclass_i = gen_axclass (K I) Theory.cert_axm (K I); - -end; - - - -(** instantiation proofs **) +(** instances **) (* parameters *) @@ -233,6 +159,9 @@ val params = #2 (#1 (AxClassData.get thy)); in fold (fn (x, c) => if member (op =) range c then cons x else I) params [] end; + +(* class relations *) + fun cert_classrel thy raw_rel = let val (c1, c2) = pairself (Sign.certify_class thy) raw_rel; @@ -261,11 +190,11 @@ thy |> Theory.add_classrel_i [(c1, c2)] |> AxClassData.map (apsnd (map_instances (fn (classes, classrel, arities) => - (classes - |> Graph.default_node (c1, ()) - |> Graph.default_node (c2, ()) - |> Graph.add_edge (c1, c2), - ((c1, c2), th) :: classrel, arities)))) + (classes + |> Graph.default_node (c1, ()) + |> Graph.default_node (c2, ()) + |> Graph.add_edge (c1, c2), + ((c1, c2), th) :: classrel, arities)))) end; fun add_arity th thy = @@ -301,4 +230,81 @@ quote (Sign.string_of_arity thy arity)); in fold add_arity ths thy end; + + +(** axclass definitions **) + +(* add_axclass(_i) *) + +fun gen_axclass prep_class prep_att prep_propp + (bclass, raw_super) params raw_specs thy = + let + val ctxt = ProofContext.init thy; + val pp = ProofContext.pp ctxt; + + + (* prepare specification *) + + val bconst = Logic.const_of_class bclass; + val class = Sign.full_name thy bclass; + val super = map (prep_class thy) raw_super |> Sign.certify_sort thy; + + fun prep_axiom t = + (case Term.add_tfrees t [] of + [(a, S)] => + if Sign.subsort thy (super, S) then t + else error ("Sort constraint of type variable " ^ + setmp show_sorts true (Pretty.string_of_typ pp) (TFree (a, S)) ^ + " needs to be weaker than " ^ Pretty.string_of_sort pp super) + | [] => t + | _ => error ("Multiple type variables in class axiom:\n" ^ Pretty.string_of_term pp t)) + |> map_term_types (Term.map_atyps (fn TFree _ => Term.aT [] | U => U)) + |> Logic.close_form; + + val axiomss = prep_propp (ctxt, map (map (rpair ([], [])) o snd) raw_specs) + |> snd |> map (map (prep_axiom o fst)); + val name_atts = Attrib.map_specs (prep_att thy) raw_specs |> map fst; + + + (* definition *) + + val conjs = map (curry Logic.mk_inclass (Term.aT [])) super @ List.concat axiomss; + val class_eq = + Logic.mk_equals (Logic.mk_inclass (Term.aT [], class), Logic.mk_conjunction_list conjs); + + val ([def], def_thy) = + thy + |> Theory.add_classes_i [(bclass, super)] + |> PureThy.add_defs_i false [((Thm.def_name bconst, class_eq), [])]; + val (raw_intro, (raw_classrel, raw_axioms)) = + (Conjunction.split_defined (length conjs) def) ||> chop (length super); + + + (* facts *) + + val class_triv = Thm.class_triv def_thy class; + val ([(_, [intro]), (_, axioms)], facts_thy) = + def_thy + |> PureThy.note_thmss_qualified "" bconst + [((introN, []), [([Drule.standard raw_intro], [])]), + ((axiomsN, []), [(map (fn th => Drule.standard (class_triv RS th)) raw_axioms, [])])] + ||> fold (fn th => add_classrel (Drule.standard' (class_triv RS th))) raw_classrel; + + + (* result *) + + val result_thy = + facts_thy + |> Sign.add_path bconst + |> PureThy.note_thmss_i "" (name_atts ~~ map Thm.simple_fact (unflat axiomss axioms)) |> snd + |> Sign.restore_naming facts_thy + |> AxClassData.map (apfst (fn (is, ps) => + (Symtab.update (class, make_axclass (super, def, intro, axioms)) is, + fold (fn x => add_param pp (x, class)) params ps))); + + in (class, result_thy) end; + +val add_axclass = gen_axclass Sign.read_class Attrib.attribute ProofContext.read_propp; +val add_axclass_i = gen_axclass Sign.certify_class (K I) ProofContext.cert_propp; + end;