284 fun read_classrel thy raw_rel = |
284 fun read_classrel thy raw_rel = |
285 cert_classrel thy (pairself (Sign.read_class thy) raw_rel) |
285 cert_classrel thy (pairself (Sign.read_class thy) raw_rel) |
286 handle TYPE (msg, _, _) => error msg; |
286 handle TYPE (msg, _, _) => error msg; |
287 |
287 |
288 |
288 |
289 (* primitive rules *) |
|
290 |
|
291 fun add_classrel th thy = |
|
292 let |
|
293 fun err () = raise THM ("add_classrel: malformed class relation", 0, [th]); |
|
294 val prop = Thm.plain_prop_of (Thm.transfer thy th); |
|
295 val rel = Logic.dest_classrel prop handle TERM _ => err (); |
|
296 val (c1, c2) = cert_classrel thy rel handle TYPE _ => err (); |
|
297 in |
|
298 thy |
|
299 |> Sign.primitive_classrel (c1, c2) |
|
300 |> put_classrel ((c1, c2), Thm.close_derivation (Drule.unconstrainTs th)) |
|
301 |> perhaps complete_arities |
|
302 end; |
|
303 |
|
304 fun add_arity th thy = |
|
305 let |
|
306 fun err () = raise THM ("add_arity: malformed type arity", 0, [th]); |
|
307 val prop = Thm.plain_prop_of (Thm.transfer thy th); |
|
308 val (t, Ss, c) = Logic.dest_arity prop handle TERM _ => err (); |
|
309 val _ = map (Sign.certify_sort thy) Ss = Ss orelse err (); |
|
310 val _ = case filter_out (fn c => can (get_inst_param thy) (c, t)) (params_of thy c) |
|
311 of [] => () |
|
312 | cs => Output.legacy_feature |
|
313 ("Missing specifications for overloaded parameters " ^ commas_quote cs) |
|
314 val th' = Drule.unconstrainTs th; |
|
315 in |
|
316 thy |
|
317 |> Sign.primitive_arity (t, Ss, [c]) |
|
318 |> put_arity ((t, Ss, c), th') |
|
319 end; |
|
320 |
|
321 |
|
322 (* tactical proofs *) |
|
323 |
|
324 fun prove_classrel raw_rel tac thy = |
|
325 let |
|
326 val ctxt = ProofContext.init thy; |
|
327 val (c1, c2) = cert_classrel thy raw_rel; |
|
328 val th = Goal.prove ctxt [] [] (Logic.mk_classrel (c1, c2)) (K tac) handle ERROR msg => |
|
329 cat_error msg ("The error(s) above occurred while trying to prove class relation " ^ |
|
330 quote (Syntax.string_of_classrel ctxt [c1, c2])); |
|
331 in |
|
332 thy |
|
333 |> PureThy.add_thms [((Binding.name |
|
334 (prefix classrel_prefix (Logic.name_classrel (c1, c2))), th), [])] |
|
335 |-> (fn [th'] => add_classrel th') |
|
336 end; |
|
337 |
|
338 fun prove_arity raw_arity tac thy = |
|
339 let |
|
340 val ctxt = ProofContext.init thy; |
|
341 val arity = Sign.cert_arity thy raw_arity; |
|
342 val names = map (prefix arity_prefix) (Logic.name_arities arity); |
|
343 val props = Logic.mk_arities arity; |
|
344 val ths = Goal.prove_multi ctxt [] [] props |
|
345 (fn _ => Goal.precise_conjunction_tac (length props) 1 THEN tac) handle ERROR msg => |
|
346 cat_error msg ("The error(s) above occurred while trying to prove type arity " ^ |
|
347 quote (Syntax.string_of_arity ctxt arity)); |
|
348 in |
|
349 thy |
|
350 |> PureThy.add_thms (map (rpair []) (map Binding.name names ~~ ths)) |
|
351 |-> fold add_arity |
|
352 end; |
|
353 |
|
354 |
|
355 (* instance parameters and overloaded definitions *) |
|
356 |
|
357 (* declaration and definition of instances of overloaded constants *) |
289 (* declaration and definition of instances of overloaded constants *) |
358 |
290 |
359 fun declare_overloaded (c, T) thy = |
291 fun declare_overloaded (c, T) thy = |
360 let |
292 let |
361 val class = case class_of_param thy c |
293 val class = case class_of_param thy c |
393 (Binding.name (Long_Name.base_name c ^ "_" ^ Long_Name.base_name tyco)) b; |
325 (Binding.name (Long_Name.base_name c ^ "_" ^ Long_Name.base_name tyco)) b; |
394 in |
326 in |
395 thy |
327 thy |
396 |> Thm.add_def false false (b', prop) |
328 |> Thm.add_def false false (b', prop) |
397 |>> (fn thm => Drule.transitive_thm OF [eq, thm]) |
329 |>> (fn thm => Drule.transitive_thm OF [eq, thm]) |
|
330 end; |
|
331 |
|
332 |
|
333 (* primitive rules *) |
|
334 |
|
335 fun add_classrel th thy = |
|
336 let |
|
337 fun err () = raise THM ("add_classrel: malformed class relation", 0, [th]); |
|
338 val prop = Thm.plain_prop_of (Thm.transfer thy th); |
|
339 val rel = Logic.dest_classrel prop handle TERM _ => err (); |
|
340 val (c1, c2) = cert_classrel thy rel handle TYPE _ => err (); |
|
341 in |
|
342 thy |
|
343 |> Sign.primitive_classrel (c1, c2) |
|
344 |> put_classrel ((c1, c2), Thm.close_derivation (Drule.unconstrainTs th)) |
|
345 |> perhaps complete_arities |
|
346 end; |
|
347 |
|
348 fun add_arity th thy = |
|
349 let |
|
350 fun err () = raise THM ("add_arity: malformed type arity", 0, [th]); |
|
351 val prop = Thm.plain_prop_of (Thm.transfer thy th); |
|
352 val (t, Ss, c) = Logic.dest_arity prop handle TERM _ => err (); |
|
353 val T = Type (t, map TFree (Name.names Name.context Name.aT Ss)); |
|
354 val missing_params = Sign.complete_sort thy [c] |
|
355 |> maps (these o Option.map #params o try (get_info thy)) |
|
356 |> filter_out (fn (const, _) => can (get_inst_param thy) (const, t)) |
|
357 |> (map o apsnd o map_atyps) (K T); |
|
358 val _ = map (Sign.certify_sort thy) Ss = Ss orelse err (); |
|
359 val th' = Drule.unconstrainTs th; |
|
360 in |
|
361 thy |
|
362 |> fold (snd oo declare_overloaded) missing_params |
|
363 |> Sign.primitive_arity (t, Ss, [c]) |
|
364 |> put_arity ((t, Ss, c), th') |
|
365 end; |
|
366 |
|
367 |
|
368 (* tactical proofs *) |
|
369 |
|
370 fun prove_classrel raw_rel tac thy = |
|
371 let |
|
372 val ctxt = ProofContext.init thy; |
|
373 val (c1, c2) = cert_classrel thy raw_rel; |
|
374 val th = Goal.prove ctxt [] [] (Logic.mk_classrel (c1, c2)) (K tac) handle ERROR msg => |
|
375 cat_error msg ("The error(s) above occurred while trying to prove class relation " ^ |
|
376 quote (Syntax.string_of_classrel ctxt [c1, c2])); |
|
377 in |
|
378 thy |
|
379 |> PureThy.add_thms [((Binding.name |
|
380 (prefix classrel_prefix (Logic.name_classrel (c1, c2))), th), [])] |
|
381 |-> (fn [th'] => add_classrel th') |
|
382 end; |
|
383 |
|
384 fun prove_arity raw_arity tac thy = |
|
385 let |
|
386 val ctxt = ProofContext.init thy; |
|
387 val arity = Sign.cert_arity thy raw_arity; |
|
388 val names = map (prefix arity_prefix) (Logic.name_arities arity); |
|
389 val props = Logic.mk_arities arity; |
|
390 val ths = Goal.prove_multi ctxt [] [] props |
|
391 (fn _ => Goal.precise_conjunction_tac (length props) 1 THEN tac) handle ERROR msg => |
|
392 cat_error msg ("The error(s) above occurred while trying to prove type arity " ^ |
|
393 quote (Syntax.string_of_arity ctxt arity)); |
|
394 in |
|
395 thy |
|
396 |> PureThy.add_thms (map (rpair []) (map Binding.name names ~~ ths)) |
|
397 |-> fold add_arity |
398 end; |
398 end; |
399 |
399 |
400 |
400 |
401 |
401 |
402 (** class definitions **) |
402 (** class definitions **) |