# HG changeset patch # User wenzelm # Date 1146430205 -7200 # Node ID b4bd790f93735b93a9a113dc238af3f81a84b95e # Parent 29fc4e5a638c9afdac5e5180f8494554082786b0 renamed add_axclass(_i) to define_axclass(_i); renamed get_info to get_definition; added axiomatize_class/classrel/arity (supercede Sign.add_classes/classrel/arities); tuned; diff -r 29fc4e5a638c -r b4bd790f9373 src/Pure/axclass.ML --- a/src/Pure/axclass.ML Sun Apr 30 22:50:03 2006 +0200 +++ b/src/Pure/axclass.ML Sun Apr 30 22:50:05 2006 +0200 @@ -2,27 +2,34 @@ ID: $Id$ Author: Markus Wenzel, TU Muenchen -Axiomatic type classes: managing predicates and parameter collections. +Type classes as parameter records and predicates, with explicit +definitions and proofs. *) signature AX_CLASS = sig - val print_axclasses: theory -> unit - val get_info: theory -> class -> {def: thm, intro: thm, axioms: thm list} + val get_definition: theory -> class -> {def: thm, intro: thm, axioms: thm list} val class_intros: theory -> thm list val params_of: theory -> class -> string list val all_params_of: theory -> sort -> string list + val print_axclasses: theory -> unit val cert_classrel: theory -> class * class -> class * class val read_classrel: theory -> xstring * xstring -> class * class val add_classrel: thm -> theory -> theory 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 of_sort: theory -> typ * sort -> thm list - val add_axclass: bstring * xstring list -> string list -> + val define_class: bstring * xstring list -> string list -> ((bstring * Attrib.src list) * string list) list -> theory -> class * theory - val add_axclass_i: bstring * class list -> string list -> + val define_class_i: bstring * class list -> string list -> ((bstring * attribute list) * term list) list -> theory -> class * theory + val axiomatize_class: bstring * xstring list -> theory -> theory + val axiomatize_class_i: bstring * class list -> theory -> theory + val axiomatize_classrel: (xstring * xstring) list -> theory -> theory + val axiomatize_classrel_i: (class * class) list -> theory -> theory + val axiomatize_arity: xstring * string list * string -> theory -> theory + val axiomatize_arity_i: arity -> theory -> theory + val of_sort: theory -> typ * sort -> thm list end; structure AxClass: AX_CLASS = @@ -46,9 +53,10 @@ fold_rev (fn q => if member (op =) ps q then I else add_param pp q) qs ps; -(* axclass *) +(* axclasses *) val introN = "intro"; +val superN = "super"; val axiomsN = "axioms"; datatype axclass = AxClass of @@ -67,6 +75,9 @@ (* instances *) +val classrelN = "classrel"; +val arityN = "arity"; + datatype instances = Instances of {classes: unit Graph.T, (*raw relation -- no closure!*) classrel: ((class * class) * thm) list, @@ -89,7 +100,7 @@ Typtab.join (K (merge (eq_fst op =))) (types1, types2)); -(* data *) +(* setup data *) structure AxClassData = TheoryDataFun (struct @@ -107,24 +118,24 @@ val _ = Context.add_setup AxClassData.init; -(* classes *) +(* retrieve axclasses *) -val lookup_info = Symtab.lookup o #1 o #1 o AxClassData.get; +val lookup_def = Symtab.lookup o #1 o #1 o AxClassData.get; -fun get_info thy c = - (case lookup_info thy c of +fun get_definition thy c = + (case lookup_def thy c of SOME (AxClass info) => info - | NONE => error ("Unknown axclass " ^ quote c)); + | NONE => error ("Undefined type class " ^ quote c)); fun class_intros thy = let fun add_intro c = - (case lookup_info thy c of SOME (AxClass {intro, ...}) => cons intro | _ => I); + (case lookup_def thy c of SOME (AxClass {intro, ...}) => cons intro | _ => I); val classes = Sign.classes thy; in map (Thm.class_triv thy) classes @ fold add_intro classes [] end; -(* parameters *) +(* retrieve parameters *) fun get_params thy pred = let val params = #2 (#1 (AxClassData.get thy)) @@ -134,7 +145,7 @@ fun all_params_of thy S = get_params thy (fn c => Sign.subsort thy (S, [c])); -(* instances *) +(* maintain instances *) val get_instances = AxClassData.get #> (fn (_, ref (Instances insts)) => insts); @@ -158,7 +169,7 @@ (classes, classrel, arities, types |> Typtab.insert_list (eq_fst op =) (T, (c, th)))); -(* print_axclasses *) +(* print data *) fun print_axclasses thy = let @@ -168,7 +179,7 @@ fun pretty_axclass (class, AxClass {def, intro, axioms}) = Pretty.block (Pretty.fbreaks [Pretty.block - [Pretty.str "axclass ", ProofContext.pretty_sort ctxt [class], Pretty.str ":"], + [Pretty.str "class ", ProofContext.pretty_sort ctxt [class], Pretty.str ":"], Pretty.strs ("parameters:" :: params_of thy class), ProofContext.pretty_fact ctxt ("def", [def]), ProofContext.pretty_fact ctxt (introN, [intro]), @@ -177,14 +188,14 @@ -(** instance proofs **) +(** instances **) (* class relations *) fun cert_classrel thy raw_rel = let val (c1, c2) = pairself (Sign.certify_class thy) raw_rel; - val _ = Type.add_classrel (Sign.pp thy) [(c1, c2)] (Sign.tsig_of thy); + val _ = Type.add_classrel (Sign.pp thy) (c1, c2) (Sign.tsig_of thy); val _ = (case subtract (op =) (all_params_of thy [c1]) (all_params_of thy [c2]) of [] => () @@ -205,7 +216,7 @@ val prop = Drule.plain_prop_of (Thm.transfer thy th); val rel = Logic.dest_classrel prop handle TERM _ => err (); val (c1, c2) = cert_classrel thy rel handle TYPE _ => err (); - val thy' = thy |> Theory.add_classrel_i [(c1, c2)]; + val thy' = thy |> Sign.primitive_classrel (c1, c2); val _ = store_classrel thy' ((c1, c2), Drule.unconstrainTs th); in thy' end; @@ -214,7 +225,7 @@ val prop = Drule.plain_prop_of (Thm.transfer thy th); val (t, Ss, c) = Logic.dest_arity prop handle TERM _ => raise THM ("add_arity: malformed type arity", 0, [th]); - val thy' = thy |> Theory.add_arities_i [(t, Ss, [c])]; + val thy' = thy |> Sign.primitive_arity (t, Ss, [c]); val _ = store_arity thy' ((t, Ss, c), Drule.unconstrainTs th); in thy' end; @@ -227,7 +238,11 @@ val th = Goal.prove thy [] [] (Logic.mk_classrel (c1, c2)) (fn _ => tac) handle ERROR msg => cat_error msg ("The error(s) above occurred while trying to prove class relation " ^ quote (Sign.string_of_classrel thy [c1, c2])); - in add_classrel th thy end; + in + thy + |> PureThy.add_thms [((classrelN ^ "_" ^ serial_string (), th), [])] + |-> (fn [th'] => add_classrel th') + end; fun prove_arity raw_arity tac thy = let @@ -237,10 +252,135 @@ (fn _ => Tactic.precise_conjunction_tac (length props) 1 THEN tac) handle ERROR msg => cat_error msg ("The error(s) above occurred while trying to prove type arity " ^ quote (Sign.string_of_arity thy arity)); - in fold add_arity ths thy end; + in + thy + |> PureThy.add_thms (ths |> map (fn th => ((arityN ^ "_" ^ serial_string (), th), []))) + |-> fold add_arity + end; + + + +(** class definitions **) + +local + +fun def_class 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 @ flat axiomss; + val class_eq = + Logic.mk_equals (Logic.mk_inclass (Term.aT [], class), Logic.mk_conjunction_list conjs); + + val ([def], def_thy) = + thy + |> Sign.primitive_class (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); -(* derived instances -- cached *) + (* facts *) + + val class_triv = Thm.class_triv def_thy class; + val ([(_, [intro]), (_, classrel), (_, axioms)], facts_thy) = + def_thy + |> PureThy.note_thmss_qualified "" bconst + [((introN, []), [([Drule.standard raw_intro], [])]), + ((superN, []), [(map Drule.standard raw_classrel, [])]), + ((axiomsN, []), [(map (fn th => Drule.standard (class_triv RS th)) raw_axioms, [])])]; + val _ = map (store_classrel facts_thy) (map (pair class) super ~~ 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 (axclasses, parameters) => + (Symtab.update (class, make_axclass (def, intro, axioms)) axclasses, + fold (fn x => add_param pp (x, class)) params parameters))); + + in (class, result_thy) end; + +in + +val define_class = def_class Sign.read_class Attrib.attribute ProofContext.read_propp; +val define_class_i = def_class Sign.certify_class (K I) ProofContext.cert_propp; + +end; + + +(** axiomatizations **) + +local + +fun axiomatize kind add prep arg thy = + let val specs = arg |> prep thy |> map (fn prop => ((kind ^ "_" ^ serial_string (), prop), [])) + in thy |> PureThy.add_axioms_i specs |-> fold add end; + +fun ax_classrel prep = + axiomatize classrelN add_classrel (fn thy => map (prep thy #> Logic.mk_classrel)); + +fun ax_arity prep = + axiomatize arityN add_arity (fn thy => prep thy #> Logic.mk_arities); + +fun ax_class prep_class prep_classrel (bclass, raw_super) thy = + let + val class = Sign.full_name thy bclass; + val super = map (prep_class thy) raw_super |> Sign.certify_sort thy; + in + thy + |> Sign.primitive_class (bclass, super) + |> ax_classrel prep_classrel (map (fn c => (class, c)) super) + end; + +in + +val axiomatize_class = ax_class Sign.read_class read_classrel; +val axiomatize_class_i = ax_class Sign.certify_class cert_classrel; +val axiomatize_classrel = ax_classrel read_classrel; +val axiomatize_classrel_i = ax_classrel cert_classrel; +val axiomatize_arity = ax_arity Sign.read_arity; +val axiomatize_arity_i = ax_arity Sign.cert_arity; + +end; + + + +(** explicit derivations -- cached **) + +local fun derive_classrel thy (c1, c2) = let @@ -291,6 +431,8 @@ setmp show_sorts true (Sign.string_of_typ thy) T); in derive end; +in + fun of_sort thy (typ, sort) = let fun lookup () = AList.lookup (op =) (Typtab.lookup_list (#types (get_instances thy)) typ); @@ -316,82 +458,6 @@ in () end); in map (the o lookup ()) sort 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 @ flat 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, [])])]; - val _ = map (store_classrel facts_thy) - (map (pair class) super ~~ map Drule.standard 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 (axclasses, parameters) => - (Symtab.update (class, make_axclass (def, intro, axioms)) axclasses, - fold (fn x => add_param pp (x, class)) params parameters))); - - 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; end;