formal declaration of undefined parameters after class instantiation
authorhaftmann
Fri Apr 17 16:41:31 2009 +0200 (2009-04-17)
changeset 30951a6e26a248f03
parent 30950 1435a8f01a41
child 30952 7ab2716dd93b
formal declaration of undefined parameters after class instantiation
NEWS
src/Pure/axclass.ML
     1.1 --- a/NEWS	Fri Apr 17 16:41:30 2009 +0200
     1.2 +++ b/NEWS	Fri Apr 17 16:41:31 2009 +0200
     1.3 @@ -1,6 +1,12 @@
     1.4  Isabelle NEWS -- history user-relevant changes
     1.5  ==============================================
     1.6  
     1.7 +*** Pure ***
     1.8 +
     1.9 +* On instantiation of classes, remaining undefined class parameters are
    1.10 +formally declared.  INCOMPATIBILITY.
    1.11 +
    1.12 +
    1.13  *** HOL ***
    1.14  
    1.15  * Class semiring_div now requires no_zero_divisors and proof of div_mult_mult1;
     2.1 --- a/src/Pure/axclass.ML	Fri Apr 17 16:41:30 2009 +0200
     2.2 +++ b/src/Pure/axclass.ML	Fri Apr 17 16:41:31 2009 +0200
     2.3 @@ -286,74 +286,6 @@
     2.4      handle TYPE (msg, _, _) => error msg;
     2.5  
     2.6  
     2.7 -(* primitive rules *)
     2.8 -
     2.9 -fun add_classrel th thy =
    2.10 -  let
    2.11 -    fun err () = raise THM ("add_classrel: malformed class relation", 0, [th]);
    2.12 -    val prop = Thm.plain_prop_of (Thm.transfer thy th);
    2.13 -    val rel = Logic.dest_classrel prop handle TERM _ => err ();
    2.14 -    val (c1, c2) = cert_classrel thy rel handle TYPE _ => err ();
    2.15 -  in
    2.16 -    thy
    2.17 -    |> Sign.primitive_classrel (c1, c2)
    2.18 -    |> put_classrel ((c1, c2), Thm.close_derivation (Drule.unconstrainTs th))
    2.19 -    |> perhaps complete_arities
    2.20 -  end;
    2.21 -
    2.22 -fun add_arity th thy =
    2.23 -  let
    2.24 -    fun err () = raise THM ("add_arity: malformed type arity", 0, [th]);
    2.25 -    val prop = Thm.plain_prop_of (Thm.transfer thy th);
    2.26 -    val (t, Ss, c) = Logic.dest_arity prop handle TERM _ => err ();
    2.27 -    val _ = map (Sign.certify_sort thy) Ss = Ss orelse err ();
    2.28 -    val _ = case filter_out (fn c => can (get_inst_param thy) (c, t)) (params_of thy c)
    2.29 -     of [] => ()
    2.30 -      | cs => Output.legacy_feature
    2.31 -          ("Missing specifications for overloaded parameters " ^ commas_quote cs)
    2.32 -    val th' = Drule.unconstrainTs th;
    2.33 -  in
    2.34 -    thy
    2.35 -    |> Sign.primitive_arity (t, Ss, [c])
    2.36 -    |> put_arity ((t, Ss, c), th')
    2.37 -  end;
    2.38 -
    2.39 -
    2.40 -(* tactical proofs *)
    2.41 -
    2.42 -fun prove_classrel raw_rel tac thy =
    2.43 -  let
    2.44 -    val ctxt = ProofContext.init thy;
    2.45 -    val (c1, c2) = cert_classrel thy raw_rel;
    2.46 -    val th = Goal.prove ctxt [] [] (Logic.mk_classrel (c1, c2)) (K tac) handle ERROR msg =>
    2.47 -      cat_error msg ("The error(s) above occurred while trying to prove class relation " ^
    2.48 -        quote (Syntax.string_of_classrel ctxt [c1, c2]));
    2.49 -  in
    2.50 -    thy
    2.51 -    |> PureThy.add_thms [((Binding.name
    2.52 -        (prefix classrel_prefix (Logic.name_classrel (c1, c2))), th), [])]
    2.53 -    |-> (fn [th'] => add_classrel th')
    2.54 -  end;
    2.55 -
    2.56 -fun prove_arity raw_arity tac thy =
    2.57 -  let
    2.58 -    val ctxt = ProofContext.init thy;
    2.59 -    val arity = Sign.cert_arity thy raw_arity;
    2.60 -    val names = map (prefix arity_prefix) (Logic.name_arities arity);
    2.61 -    val props = Logic.mk_arities arity;
    2.62 -    val ths = Goal.prove_multi ctxt [] [] props
    2.63 -      (fn _ => Goal.precise_conjunction_tac (length props) 1 THEN tac) handle ERROR msg =>
    2.64 -        cat_error msg ("The error(s) above occurred while trying to prove type arity " ^
    2.65 -          quote (Syntax.string_of_arity ctxt arity));
    2.66 -  in
    2.67 -    thy
    2.68 -    |> PureThy.add_thms (map (rpair []) (map Binding.name names ~~ ths))
    2.69 -    |-> fold add_arity
    2.70 -  end;
    2.71 -
    2.72 -
    2.73 -(* instance parameters and overloaded definitions *)
    2.74 -
    2.75  (* declaration and definition of instances of overloaded constants *)
    2.76  
    2.77  fun declare_overloaded (c, T) thy =
    2.78 @@ -398,6 +330,74 @@
    2.79    end;
    2.80  
    2.81  
    2.82 +(* primitive rules *)
    2.83 +
    2.84 +fun add_classrel th thy =
    2.85 +  let
    2.86 +    fun err () = raise THM ("add_classrel: malformed class relation", 0, [th]);
    2.87 +    val prop = Thm.plain_prop_of (Thm.transfer thy th);
    2.88 +    val rel = Logic.dest_classrel prop handle TERM _ => err ();
    2.89 +    val (c1, c2) = cert_classrel thy rel handle TYPE _ => err ();
    2.90 +  in
    2.91 +    thy
    2.92 +    |> Sign.primitive_classrel (c1, c2)
    2.93 +    |> put_classrel ((c1, c2), Thm.close_derivation (Drule.unconstrainTs th))
    2.94 +    |> perhaps complete_arities
    2.95 +  end;
    2.96 +
    2.97 +fun add_arity th thy =
    2.98 +  let
    2.99 +    fun err () = raise THM ("add_arity: malformed type arity", 0, [th]);
   2.100 +    val prop = Thm.plain_prop_of (Thm.transfer thy th);
   2.101 +    val (t, Ss, c) = Logic.dest_arity prop handle TERM _ => err ();
   2.102 +    val T = Type (t, map TFree (Name.names Name.context Name.aT Ss));
   2.103 +    val missing_params = Sign.complete_sort thy [c]
   2.104 +      |> maps (these o Option.map #params o try (get_info thy))
   2.105 +      |> filter_out (fn (const, _) => can (get_inst_param thy) (const, t))
   2.106 +      |> (map o apsnd o map_atyps) (K T);
   2.107 +    val _ = map (Sign.certify_sort thy) Ss = Ss orelse err ();
   2.108 +    val th' = Drule.unconstrainTs th;
   2.109 +  in
   2.110 +    thy
   2.111 +    |> fold (snd oo declare_overloaded) missing_params
   2.112 +    |> Sign.primitive_arity (t, Ss, [c])
   2.113 +    |> put_arity ((t, Ss, c), th')
   2.114 +  end;
   2.115 +
   2.116 +
   2.117 +(* tactical proofs *)
   2.118 +
   2.119 +fun prove_classrel raw_rel tac thy =
   2.120 +  let
   2.121 +    val ctxt = ProofContext.init thy;
   2.122 +    val (c1, c2) = cert_classrel thy raw_rel;
   2.123 +    val th = Goal.prove ctxt [] [] (Logic.mk_classrel (c1, c2)) (K tac) handle ERROR msg =>
   2.124 +      cat_error msg ("The error(s) above occurred while trying to prove class relation " ^
   2.125 +        quote (Syntax.string_of_classrel ctxt [c1, c2]));
   2.126 +  in
   2.127 +    thy
   2.128 +    |> PureThy.add_thms [((Binding.name
   2.129 +        (prefix classrel_prefix (Logic.name_classrel (c1, c2))), th), [])]
   2.130 +    |-> (fn [th'] => add_classrel th')
   2.131 +  end;
   2.132 +
   2.133 +fun prove_arity raw_arity tac thy =
   2.134 +  let
   2.135 +    val ctxt = ProofContext.init thy;
   2.136 +    val arity = Sign.cert_arity thy raw_arity;
   2.137 +    val names = map (prefix arity_prefix) (Logic.name_arities arity);
   2.138 +    val props = Logic.mk_arities arity;
   2.139 +    val ths = Goal.prove_multi ctxt [] [] props
   2.140 +      (fn _ => Goal.precise_conjunction_tac (length props) 1 THEN tac) handle ERROR msg =>
   2.141 +        cat_error msg ("The error(s) above occurred while trying to prove type arity " ^
   2.142 +          quote (Syntax.string_of_arity ctxt arity));
   2.143 +  in
   2.144 +    thy
   2.145 +    |> PureThy.add_thms (map (rpair []) (map Binding.name names ~~ ths))
   2.146 +    |-> fold add_arity
   2.147 +  end;
   2.148 +
   2.149 +
   2.150  
   2.151  (** class definitions **)
   2.152