--- a/NEWS Fri Apr 17 16:41:30 2009 +0200
+++ b/NEWS Fri Apr 17 16:41:31 2009 +0200
@@ -1,6 +1,12 @@
Isabelle NEWS -- history user-relevant changes
==============================================
+*** Pure ***
+
+* On instantiation of classes, remaining undefined class parameters are
+formally declared. INCOMPATIBILITY.
+
+
*** HOL ***
* Class semiring_div now requires no_zero_divisors and proof of div_mult_mult1;
--- a/src/Pure/axclass.ML Fri Apr 17 16:41:30 2009 +0200
+++ b/src/Pure/axclass.ML Fri Apr 17 16:41:31 2009 +0200
@@ -286,74 +286,6 @@
handle TYPE (msg, _, _) => error msg;
-(* primitive rules *)
-
-fun add_classrel th thy =
- let
- fun err () = raise THM ("add_classrel: malformed class relation", 0, [th]);
- val prop = Thm.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 ();
- in
- thy
- |> Sign.primitive_classrel (c1, c2)
- |> put_classrel ((c1, c2), Thm.close_derivation (Drule.unconstrainTs th))
- |> perhaps complete_arities
- end;
-
-fun add_arity th thy =
- let
- fun err () = raise THM ("add_arity: malformed type arity", 0, [th]);
- val prop = Thm.plain_prop_of (Thm.transfer thy th);
- val (t, Ss, c) = Logic.dest_arity prop handle TERM _ => err ();
- val _ = map (Sign.certify_sort thy) Ss = Ss orelse err ();
- val _ = case filter_out (fn c => can (get_inst_param thy) (c, t)) (params_of thy c)
- of [] => ()
- | cs => Output.legacy_feature
- ("Missing specifications for overloaded parameters " ^ commas_quote cs)
- val th' = Drule.unconstrainTs th;
- in
- thy
- |> Sign.primitive_arity (t, Ss, [c])
- |> put_arity ((t, Ss, c), th')
- end;
-
-
-(* tactical proofs *)
-
-fun prove_classrel raw_rel tac thy =
- let
- val ctxt = ProofContext.init thy;
- val (c1, c2) = cert_classrel thy raw_rel;
- val th = Goal.prove ctxt [] [] (Logic.mk_classrel (c1, c2)) (K tac) handle ERROR msg =>
- cat_error msg ("The error(s) above occurred while trying to prove class relation " ^
- quote (Syntax.string_of_classrel ctxt [c1, c2]));
- in
- thy
- |> PureThy.add_thms [((Binding.name
- (prefix classrel_prefix (Logic.name_classrel (c1, c2))), th), [])]
- |-> (fn [th'] => add_classrel th')
- end;
-
-fun prove_arity raw_arity tac thy =
- let
- val ctxt = ProofContext.init thy;
- val arity = Sign.cert_arity thy raw_arity;
- val names = map (prefix arity_prefix) (Logic.name_arities arity);
- val props = Logic.mk_arities arity;
- val ths = Goal.prove_multi ctxt [] [] props
- (fn _ => Goal.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 (Syntax.string_of_arity ctxt arity));
- in
- thy
- |> PureThy.add_thms (map (rpair []) (map Binding.name names ~~ ths))
- |-> fold add_arity
- end;
-
-
-(* instance parameters and overloaded definitions *)
-
(* declaration and definition of instances of overloaded constants *)
fun declare_overloaded (c, T) thy =
@@ -398,6 +330,74 @@
end;
+(* primitive rules *)
+
+fun add_classrel th thy =
+ let
+ fun err () = raise THM ("add_classrel: malformed class relation", 0, [th]);
+ val prop = Thm.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 ();
+ in
+ thy
+ |> Sign.primitive_classrel (c1, c2)
+ |> put_classrel ((c1, c2), Thm.close_derivation (Drule.unconstrainTs th))
+ |> perhaps complete_arities
+ end;
+
+fun add_arity th thy =
+ let
+ fun err () = raise THM ("add_arity: malformed type arity", 0, [th]);
+ val prop = Thm.plain_prop_of (Thm.transfer thy th);
+ val (t, Ss, c) = Logic.dest_arity prop handle TERM _ => err ();
+ val T = Type (t, map TFree (Name.names Name.context Name.aT Ss));
+ 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 _ = map (Sign.certify_sort thy) Ss = Ss orelse err ();
+ val th' = Drule.unconstrainTs th;
+ in
+ thy
+ |> fold (snd oo declare_overloaded) missing_params
+ |> Sign.primitive_arity (t, Ss, [c])
+ |> put_arity ((t, Ss, c), th')
+ end;
+
+
+(* tactical proofs *)
+
+fun prove_classrel raw_rel tac thy =
+ let
+ val ctxt = ProofContext.init thy;
+ val (c1, c2) = cert_classrel thy raw_rel;
+ val th = Goal.prove ctxt [] [] (Logic.mk_classrel (c1, c2)) (K tac) handle ERROR msg =>
+ cat_error msg ("The error(s) above occurred while trying to prove class relation " ^
+ quote (Syntax.string_of_classrel ctxt [c1, c2]));
+ in
+ thy
+ |> PureThy.add_thms [((Binding.name
+ (prefix classrel_prefix (Logic.name_classrel (c1, c2))), th), [])]
+ |-> (fn [th'] => add_classrel th')
+ end;
+
+fun prove_arity raw_arity tac thy =
+ let
+ val ctxt = ProofContext.init thy;
+ val arity = Sign.cert_arity thy raw_arity;
+ val names = map (prefix arity_prefix) (Logic.name_arities arity);
+ val props = Logic.mk_arities arity;
+ val ths = Goal.prove_multi ctxt [] [] props
+ (fn _ => Goal.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 (Syntax.string_of_arity ctxt arity));
+ in
+ thy
+ |> PureThy.add_thms (map (rpair []) (map Binding.name names ~~ ths))
+ |-> fold add_arity
+ end;
+
+
(** class definitions **)