# HG changeset patch # User berghofe # Date 1275383089 -7200 # Node ID c10fb22a5e0c907234a12365a3102b0912d88586 # Parent e5419ecf92b7a205e9d03fc4de7ead7ba1c5721f classrel and arity theorems are now stored under proper name in theory. add_arity and add_classrel take extra boolean argument indicating whether theorems should be stored. diff -r e5419ecf92b7 -r c10fb22a5e0c src/Pure/Isar/class_target.ML --- a/src/Pure/Isar/class_target.ML Tue Jun 01 11:01:16 2010 +0200 +++ b/src/Pure/Isar/class_target.ML Tue Jun 01 11:04:49 2010 +0200 @@ -243,7 +243,7 @@ | NONE => I in thy - |> AxClass.add_classrel classrel + |> AxClass.add_classrel true classrel |> ClassData.map (Graph.add_edge (sub, sup)) |> activate_defs sub (these_defs thy diff_sort) |> add_dependency @@ -366,7 +366,7 @@ fun gen_classrel mk_prop classrel thy = let fun after_qed results = - ProofContext.theory ((fold o fold) AxClass.add_classrel results); + ProofContext.theory ((fold o fold) (AxClass.add_classrel true) results); in thy |> ProofContext.init_global @@ -531,7 +531,7 @@ val (tycos, vs, sort) = (#arities o the_instantiation) lthy; val arities_proof = maps (fn tyco => Logic.mk_arities (tyco, map snd vs, sort)) tycos; fun after_qed' results = - Local_Theory.theory (fold (AxClass.add_arity o Thm.varifyT_global) results) + Local_Theory.theory (fold (AxClass.add_arity true o Thm.varifyT_global) results) #> after_qed; in lthy @@ -591,7 +591,7 @@ val sorts = map snd vs; val arities = maps (fn tyco => Logic.mk_arities (tyco, sorts, sort)) tycos; fun after_qed results = ProofContext.theory - ((fold o fold) AxClass.add_arity results); + ((fold o fold) (AxClass.add_arity true) results); in thy |> ProofContext.init_global diff -r e5419ecf92b7 -r c10fb22a5e0c src/Pure/axclass.ML --- a/src/Pure/axclass.ML Tue Jun 01 11:01:16 2010 +0200 +++ b/src/Pure/axclass.ML Tue Jun 01 11:04:49 2010 +0200 @@ -24,8 +24,8 @@ val read_classrel: theory -> xstring * xstring -> class * class val declare_overloaded: string * typ -> theory -> term * theory val define_overloaded: binding -> string * term -> theory -> thm * theory - val add_classrel: thm -> theory -> theory - val add_arity: thm -> theory -> theory + val add_classrel: bool -> thm -> theory -> theory + val add_arity: bool -> thm -> theory -> theory val prove_classrel: class * class -> tactic -> theory -> theory val prove_arity: string * sort list * sort -> tactic -> theory -> theory val define_class: binding * class list -> string list -> @@ -412,46 +412,55 @@ (* primitive rules *) -fun add_classrel raw_th thy = +fun add_classrel store raw_th thy = let val th = Thm.strip_shyps (Thm.transfer thy raw_th); val prop = Thm.plain_prop_of th; fun err () = raise THM ("add_classrel: malformed class relation", 0, [th]); val rel = Logic.dest_classrel prop handle TERM _ => err (); val (c1, c2) = cert_classrel thy rel handle TYPE _ => err (); - val th' = th + val (th', thy') = + if store then PureThy.store_thm + (Binding.name (prefix classrel_prefix (Logic.name_classrel (c1, c2))), th) thy + else (th, thy); + val th'' = th' |> Thm.unconstrainT - |> Drule.instantiate' [SOME (ctyp_of thy (TVar ((Name.aT, 0), [])))] []; + |> Drule.instantiate' [SOME (ctyp_of thy' (TVar ((Name.aT, 0), [])))] []; in - thy + thy' |> Sign.primitive_classrel (c1, c2) - |> (#2 oo put_trancl_classrel) ((c1, c2), th') + |> (#2 oo put_trancl_classrel) ((c1, c2), th'') |> perhaps complete_arities end; -fun add_arity raw_th thy = +fun add_arity store raw_th thy = let val th = Thm.strip_shyps (Thm.transfer thy raw_th); val prop = Thm.plain_prop_of th; fun err () = raise THM ("add_arity: malformed type arity", 0, [th]); - val (t, Ss, c) = Logic.dest_arity prop handle TERM _ => err (); + val arity as (t, Ss, c) = Logic.dest_arity prop handle TERM _ => err (); + + val (th', thy') = + if store then PureThy.store_thm + (Binding.name (prefix arity_prefix (Logic.name_arity arity)), th) thy + else (th, thy); val args = Name.names Name.context Name.aT Ss; val T = Type (t, map TFree args); - val std_vars = map (fn (a, S) => SOME (ctyp_of thy (TVar ((a, 0), [])))) args; + val std_vars = map (fn (a, S) => SOME (ctyp_of thy' (TVar ((a, 0), [])))) args; - val missing_params = Sign.complete_sort thy [c] - |> maps (these o Option.map #params o try (get_info thy)) - |> filter_out (fn (const, _) => can (get_inst_param thy) (const, t)) + val missing_params = Sign.complete_sort thy' [c] + |> maps (these o Option.map #params o try (get_info thy')) + |> filter_out (fn (const, _) => can (get_inst_param thy') (const, t)) |> (map o apsnd o map_atyps) (K T); - val th' = th + val th'' = th' |> Thm.unconstrainT |> Drule.instantiate' std_vars []; in - thy + thy' |> fold (#2 oo declare_overloaded) missing_params |> Sign.primitive_arity (t, Ss, [c]) - |> put_arity ((t, Ss, c), th') + |> put_arity ((t, Ss, c), th'') end; @@ -468,7 +477,7 @@ thy |> PureThy.add_thms [((Binding.name (prefix classrel_prefix (Logic.name_classrel (c1, c2))), th), [])] - |-> (fn [th'] => add_classrel th') + |-> (fn [th'] => add_classrel false th') end; fun prove_arity raw_arity tac thy = @@ -484,7 +493,7 @@ in thy |> PureThy.add_thms (map (rpair []) (map Binding.name names ~~ ths)) - |-> fold add_arity + |-> fold (add_arity false) end; @@ -618,11 +627,11 @@ fun ax_classrel prep = axiomatize (map o prep) (map Logic.mk_classrel) - (map (prefix classrel_prefix o Logic.name_classrel)) add_classrel; + (map (prefix classrel_prefix o Logic.name_classrel)) (add_classrel false); fun ax_arity prep = axiomatize (prep o ProofContext.init_global) Logic.mk_arities - (map (prefix arity_prefix) o Logic.name_arities) add_arity; + (map (prefix arity_prefix) o Logic.name_arities) (add_arity false); fun class_const c = (Logic.const_of_class c, Term.itselfT (Term.aT []) --> propT);