# HG changeset patch # User wenzelm # Date 1114716968 -7200 # Node ID a67343c6ab2a08d45c82485aa49047aceef4120d # Parent 3e9a54e033b975f71271f8193bbb89e43baa7198 sane interfaces for tactical instance proofs (do not expand defs of theory, proper handling of sort instances); keep legacy stuff separate; tuned; diff -r 3e9a54e033b9 -r a67343c6ab2a src/Pure/axclass.ML --- a/src/Pure/axclass.ML Thu Apr 28 21:35:47 2005 +0200 +++ b/src/Pure/axclass.ML Thu Apr 28 21:36:08 2005 +0200 @@ -9,27 +9,29 @@ sig val quiet_mode: bool ref val print_axclasses: theory -> unit - val add_classrel_thms: thm list -> theory -> theory - val add_arity_thms: thm list -> theory -> theory val add_axclass: bclass * xclass list -> ((bstring * string) * Attrib.src list) list -> theory -> theory * {intro: thm, axioms: thm list} val add_axclass_i: bclass * class list -> ((bstring * term) * theory attribute list) list -> theory -> theory * {intro: thm, axioms: thm list} - val add_inst_subclass_x: xclass * xclass -> string list -> thm list - -> tactic option -> theory -> theory + val add_classrel_thms: thm list -> theory -> theory + val add_arity_thms: thm list -> theory -> theory val add_inst_subclass: xclass * xclass -> tactic -> theory -> theory val add_inst_subclass_i: class * class -> tactic -> theory -> theory - val add_inst_arity_x: xstring * string list * string -> string list - -> thm list -> tactic option -> theory -> theory val add_inst_arity: xstring * string list * string -> tactic -> theory -> theory val add_inst_arity_i: string * sort list * sort -> tactic -> theory -> theory - val intro_classes_tac: thm list -> tactic - val default_intro_classes_tac: thm list -> tactic - val axclass_tac: thm list -> tactic val instance_subclass_proof: xclass * xclass -> bool -> theory -> ProofHistory.T val instance_subclass_proof_i: class * class -> bool -> theory -> ProofHistory.T val instance_arity_proof: xstring * string list * string -> bool -> theory -> ProofHistory.T val instance_arity_proof_i: string * sort list * sort -> bool -> theory -> ProofHistory.T + val intro_classes_tac: thm list -> tactic + val default_intro_classes_tac: thm list -> tactic + + (*legacy interfaces*) + val axclass_tac: thm list -> tactic + val add_inst_subclass_x: xclass * xclass -> string list -> thm list + -> tactic option -> theory -> theory + val add_inst_arity_x: xstring * string list * string -> string list + -> thm list -> tactic option -> theory -> theory end; structure AxClass: AX_CLASS = @@ -59,14 +61,6 @@ | dest_varT T = raise TYPE ("dest_varT", [T], []); -(* get axioms and theorems *) - -val is_def = Logic.is_equals o #prop o rep_thm; - -fun witnesses thy names thms = - PureThy.get_thmss thy (map (rpair NONE) names) @ thms @ List.filter is_def (map snd (axioms_of thy)); - - (** abstract syntax operations **) @@ -116,45 +110,6 @@ -(** add theorems as axioms **) - -fun prep_thm_axm thy thm = - let - fun err msg = raise THM ("prep_thm_axm: " ^ msg, 0, [thm]); - - val {sign, hyps, prop, ...} = rep_thm thm; - in - if not (Sign.subsig (sign, Theory.sign_of thy)) then - err "theorem not of same theory" - else if not (null (extra_shyps thm)) orelse not (null hyps) then - err "theorem may not contain hypotheses" - else prop - end; - -(*theorems expressing class relations*) -fun add_classrel_thms thms thy = - let - fun prep_thm thm = - let - val prop = prep_thm_axm thy thm; - val (c1, c2) = dest_classrel prop handle TERM _ => - raise THM ("add_classrel_thms: theorem is not a class relation", 0, [thm]); - in (c1, c2) end; - in Theory.add_classrel_i (map prep_thm thms) thy end; - -(*theorems expressing arities*) -fun add_arity_thms thms thy = - let - fun prep_thm thm = - let - val prop = prep_thm_axm thy thm; - val (t, ss, c) = dest_arity prop handle TERM _ => - raise THM ("add_arity_thms: theorem is not an arity", 0, [thm]); - in (t, ss, [c]) end; - in Theory.add_arities_i (map prep_thm thms) thy end; - - - (** axclass info **) (* data kind 'Pure/axclasses' *) @@ -209,10 +164,19 @@ thy |> AxclassesData.put (Symtab.update ((c, info), AxclassesData.get thy)); +(* class_axms *) + +fun class_axms sign = + let val classes = Sign.classes sign in + map (Thm.class_triv sign) classes @ + List.mapPartial (Option.map #intro o lookup_axclass_info_sg sign) classes + end; + + (** add axiomatic type classes **) -(* errors *) +local fun err_bad_axsort ax c = error ("Sort constraint in axiom " ^ quote ax ^ " not supersort of " ^ quote c); @@ -220,9 +184,6 @@ fun err_bad_tfrees ax = error ("More than one type variable in axiom " ^ quote ax); - -(* ext_axclass *) - fun ext_axclass prep_class prep_axm prep_att (bclass, raw_super_classes) raw_axioms_atts thy = let val sign = Theory.sign_of thy; @@ -274,26 +235,116 @@ |> put_axclass_info class info; in (final_thy, {intro = intro, axioms = axioms}) end; - -(* external interfaces *) +in val add_axclass = ext_axclass Sign.intern_class Theory.read_axm Attrib.global_attribute; val add_axclass_i = ext_axclass (K I) Theory.cert_axm (K I); +end; + + + +(** proven class instantiation **) + +(* add thms to type signature *) + +fun add_classrel_thms thms thy = + let + fun prep_thm thm = + let + val prop = Drule.plain_prop_of (Thm.transfer thy thm); + val (c1, c2) = dest_classrel prop handle TERM _ => + raise THM ("add_classrel_thms: not a class relation", 0, [thm]); + in (c1, c2) end; + in Theory.add_classrel_i (map prep_thm thms) thy end; + +fun add_arity_thms thms thy = + let + fun prep_thm thm = + let + val prop = Drule.plain_prop_of (Thm.transfer thy thm); + val (t, ss, c) = dest_arity prop handle TERM _ => + raise THM ("add_arity_thms: not an arity", 0, [thm]); + in (t, ss, [c]) end; + in Theory.add_arities_i (map prep_thm thms) thy end; + + +(* prepare classes and arities *) + +fun read_class sg c = Sign.certify_class sg (Sign.intern_class sg c); + +fun test_classrel sg cc = (Type.add_classrel (Sign.pp sg) [cc] (Sign.tsig_of sg); cc); +fun cert_classrel sg = test_classrel sg o Library.pairself (Sign.certify_class sg); +fun read_classrel sg = test_classrel sg o Library.pairself (read_class sg); + +fun test_arity sg ar = (Type.add_arities (Sign.pp sg) [ar] (Sign.tsig_of sg); ar); + +fun prep_arity prep_tycon prep_sort prep sg (t, Ss, x) = + test_arity sg (prep_tycon sg t, map (prep_sort sg) Ss, prep sg x); + +val read_arity = prep_arity Sign.intern_tycon Sign.read_sort Sign.read_sort; +val cert_arity = prep_arity (K I) Sign.certify_sort Sign.certify_sort; -(** prove class relations and type arities **) +(* instance declarations -- tactical proof *) + +local -(* class_axms *) +fun ext_inst_subclass prep_classrel raw_cc tac thy = + let + val sign = Theory.sign_of thy; + val (c1, c2) = prep_classrel sign raw_cc; + val txt = quote (Sign.string_of_classrel sign [c1, c2]); + val _ = message ("Proving class inclusion " ^ txt ^ " ..."); + val th = Tactic.prove sign [] [] (mk_classrel (c1, c2)) (K tac) handle ERROR => + error ("The error(s) above occurred while trying to prove " ^ txt); + in add_classrel_thms [th] thy end; -fun class_axms sign = - let val classes = Sign.classes sign in - map (Thm.class_triv sign) classes @ - List.mapPartial (Option.map #intro o lookup_axclass_info_sg sign) classes - end; +fun ext_inst_arity prep_arity raw_arity tac thy = + let + val sign = Theory.sign_of thy; + val arity = prep_arity sign raw_arity; + val txt = quote (Sign.string_of_arity sign arity); + val _ = message ("Proving type arity " ^ txt ^ " ..."); + val props = (mk_arities arity); + val ths = Tactic.prove_multi sign [] [] props + (fn _ => Tactic.smart_conjunction_tac (length props) THEN tac) + handle ERROR => error ("The error(s) above occurred while trying to prove " ^ txt); + in add_arity_thms ths thy end; + +in + +val add_inst_subclass = ext_inst_subclass read_classrel; +val add_inst_subclass_i = ext_inst_subclass cert_classrel; +val add_inst_arity = ext_inst_arity read_arity; +val add_inst_arity_i = ext_inst_arity cert_arity; + +end; -(* proof methods *) +(* instance declarations -- Isar proof *) + +local + +fun inst_proof mk_prop add_thms inst int theory = + theory + |> IsarThy.multi_theorem_i Drule.internalK I ProofContext.export_standard + ("", [fn (thy, th) => (add_thms [th] thy, th)]) [] + (map (fn t => (("", []), [(t, ([], []))])) (mk_prop (Theory.sign_of theory) inst)) int; + +in + +val instance_subclass_proof = + inst_proof (single oo (mk_classrel oo read_classrel)) add_classrel_thms; +val instance_subclass_proof_i = + inst_proof (single oo (mk_classrel oo cert_classrel)) add_classrel_thms; +val instance_arity_proof = inst_proof (mk_arities oo read_arity) add_arity_thms; +val instance_arity_proof_i = inst_proof (mk_arities oo cert_arity) add_arity_thms; + +end; + + +(* tactics and methods *) fun intro_classes_tac facts st = (ALLGOALS (Method.insert_tac facts THEN' @@ -313,109 +364,8 @@ ("default", Method.thms_ctxt_args (Method.METHOD oo default_tac), "apply some intro/elim rule")]]; -(* old-style axclass_tac *) -(*(1) repeatedly resolve goals of form "OFCLASS(ty, c_class)", - try class_trivs first, then "cI" axioms - (2) rewrite goals using user supplied definitions - (3) repeatedly resolve goals with user supplied non-definitions*) - -fun axclass_tac thms = - let - val defs = List.filter is_def thms; - val non_defs = filter_out is_def thms; - in - intro_classes_tac [] THEN - TRY (rewrite_goals_tac defs) THEN - TRY (REPEAT_FIRST (fn i => assume_tac i ORELSE resolve_tac non_defs i)) - end; - - -(* old-style provers *) - -fun prove mk_prop str_of sign prop thms usr_tac = - (Tactic.prove sign [] [] (mk_prop prop) (K (axclass_tac thms THEN (getOpt (usr_tac,all_tac)))) - handle ERROR => error ("The error(s) above occurred while trying to prove " ^ - quote (str_of sign prop))) |> Drule.standard; - -val prove_subclass = prove mk_classrel (fn sg => fn (c1, c2) => - Pretty.string_of_classrel (Sign.pp sg) [c1, c2]); - -val prove_arity = prove mk_arity (fn sg => fn (t, Ss, c) => - Pretty.string_of_arity (Sign.pp sg) (t, Ss, [c])); - - - -(** add proved subclass relations and arities **) - -(* prepare classes and arities *) - -fun read_class sg c = Sign.certify_class sg (Sign.intern_class sg c); - -fun test_classrel sg cc = (Type.add_classrel (Sign.pp sg) [cc] (Sign.tsig_of sg); cc); -fun cert_classrel sg = test_classrel sg o Library.pairself (Sign.certify_class sg); -fun read_classrel sg = test_classrel sg o Library.pairself (read_class sg); - -fun test_arity sg ar = (Type.add_arities (Sign.pp sg) [ar] (Sign.tsig_of sg); ar); - -fun prep_arity prep_tycon prep_sort prep_x sg (t, Ss, x) = - test_arity sg (prep_tycon sg t, map (prep_sort sg) Ss, prep_x sg x); - -val read_arity = prep_arity Sign.intern_tycon Sign.read_sort Sign.read_sort; -val cert_arity = prep_arity (K I) Sign.certify_sort Sign.certify_sort; - - -(* old-style instance declarations *) - -fun ext_inst_subclass prep_classrel raw_c1_c2 names thms usr_tac thy = - let - val sign = Theory.sign_of thy; - val (c1, c2) = prep_classrel sign raw_c1_c2; - in - message ("Proving class inclusion " ^ quote (Sign.string_of_classrel sign [c1, c2]) ^ " ..."); - thy |> add_classrel_thms [prove_subclass sign (c1, c2) (witnesses thy names thms) usr_tac] - end; - -fun ext_inst_arity prep_arity (raw_t, raw_Ss, raw_cs) names thms usr_tac thy = - let - val sign = Theory.sign_of thy; - val (t, Ss, cs) = prep_arity sign (raw_t, raw_Ss, raw_cs); - val wthms = witnesses thy names thms; - fun prove c = - (message ("Proving type arity " ^ - quote (Sign.string_of_arity sign (t, Ss, [c])) ^ " ..."); - prove_arity sign (t, Ss, c) wthms usr_tac); - in add_arity_thms (map prove cs) thy end; - -fun sane_inst_subclass prep sub tac = ext_inst_subclass prep sub [] [] (SOME tac); -fun sane_inst_arity prep arity tac = ext_inst_arity prep arity [] [] (SOME tac); - -val add_inst_subclass_x = ext_inst_subclass read_classrel; -val add_inst_subclass = sane_inst_subclass read_classrel; -val add_inst_subclass_i = sane_inst_subclass cert_classrel; -val add_inst_arity_x = ext_inst_arity read_arity; -val add_inst_arity = sane_inst_arity read_arity; -val add_inst_arity_i = sane_inst_arity cert_arity; - - - -(** instance proof interfaces **) - -fun inst_proof mk_prop add_thms inst int theory = - theory - |> IsarThy.multi_theorem_i Drule.internalK I ProofContext.export_standard - ("", [fn (thy, th) => (add_thms [th] thy, th)]) [] - (map (fn t => (("", []), [(t, ([], []))])) (mk_prop (Theory.sign_of theory) inst)) int; - -val instance_subclass_proof = - inst_proof (single oo (mk_classrel oo read_classrel)) add_classrel_thms; -val instance_subclass_proof_i = - inst_proof (single oo (mk_classrel oo cert_classrel)) add_classrel_thms; -val instance_arity_proof = inst_proof (mk_arities oo read_arity) add_arity_thms; -val instance_arity_proof_i = inst_proof (mk_arities oo cert_arity) add_arity_thms; - - -(* outer syntax *) +(** outer syntax **) local structure P = OuterParse and K = OuterSyntax.Keyword in @@ -435,4 +385,71 @@ end; + + +(** old-style instantiation proofs **) + +(* axclass_tac *) + +(*(1) repeatedly resolve goals of form "OFCLASS(ty, c_class)", + try class_trivs first, then "cI" axioms + (2) rewrite goals using user supplied definitions + (3) repeatedly resolve goals with user supplied non-definitions*) + +val is_def = Logic.is_equals o #prop o rep_thm; + +fun axclass_tac thms = + let + val defs = List.filter is_def thms; + val non_defs = filter_out is_def thms; + in + intro_classes_tac [] THEN + TRY (rewrite_goals_tac defs) THEN + TRY (REPEAT_FIRST (fn i => assume_tac i ORELSE resolve_tac non_defs i)) + end; + + +(* instance declarations *) + +local + +fun prove mk_prop str_of sign prop thms usr_tac = + (Tactic.prove sign [] [] (mk_prop prop) + (K (axclass_tac thms THEN (getOpt (usr_tac, all_tac)))) + handle ERROR => error ("The error(s) above occurred while trying to prove " ^ + quote (str_of sign prop))) |> Drule.standard; + +val prove_subclass = prove mk_classrel (fn sg => fn (c1, c2) => + Pretty.string_of_classrel (Sign.pp sg) [c1, c2]); + +val prove_arity = prove mk_arity (fn sg => fn (t, Ss, c) => + Pretty.string_of_arity (Sign.pp sg) (t, Ss, [c])); + +fun witnesses thy names thms = + PureThy.get_thmss thy (map (rpair NONE) names) @ thms @ List.filter is_def (map snd (axioms_of thy)); + +in + +fun add_inst_subclass_x raw_c1_c2 names thms usr_tac thy = + let + val sign = Theory.sign_of thy; + val (c1, c2) = read_classrel sign raw_c1_c2; + in + message ("Proving class inclusion " ^ quote (Sign.string_of_classrel sign [c1, c2]) ^ " ..."); + thy |> add_classrel_thms [prove_subclass sign (c1, c2) (witnesses thy names thms) usr_tac] + end; + +fun add_inst_arity_x raw_arity names thms usr_tac thy = + let + val sign = Theory.sign_of thy; + val (t, Ss, cs) = read_arity sign raw_arity; + val wthms = witnesses thy names thms; + fun prove c = + (message ("Proving type arity " ^ + quote (Sign.string_of_arity sign (t, Ss, [c])) ^ " ..."); + prove_arity sign (t, Ss, c) wthms usr_tac); + in add_arity_thms (map prove cs) thy end; + end; + +end;