196 |
196 |
197 fun the_classrel thy (c1, c2) = |
197 fun the_classrel thy (c1, c2) = |
198 (case Symreltab.lookup (proven_classrels_of thy) (c1, c2) of |
198 (case Symreltab.lookup (proven_classrels_of thy) (c1, c2) of |
199 SOME thm => thm |
199 SOME thm => thm |
200 | NONE => error ("Unproven class relation " ^ |
200 | NONE => error ("Unproven class relation " ^ |
201 Syntax.string_of_classrel (ProofContext.init_global thy) [c1, c2])); (* FIXME stale thy (!?) *) |
201 Syntax.string_of_classrel (Proof_Context.init_global thy) [c1, c2])); (* FIXME stale thy (!?) *) |
202 |
202 |
203 fun put_trancl_classrel ((c1, c2), th) thy = |
203 fun put_trancl_classrel ((c1, c2), th) thy = |
204 let |
204 let |
205 val classes = Sorts.classes_of (Sign.classes_of thy); |
205 val classes = Sorts.classes_of (Sign.classes_of thy); |
206 val classrels = proven_classrels_of thy; |
206 val classrels = proven_classrels_of thy; |
243 |
243 |
244 fun the_arity thy (a, Ss, c) = |
244 fun the_arity thy (a, Ss, c) = |
245 (case AList.lookup (op =) (Symtab.lookup_list (proven_arities_of thy) a) (c, Ss) of |
245 (case AList.lookup (op =) (Symtab.lookup_list (proven_arities_of thy) a) (c, Ss) of |
246 SOME (thm, _) => thm |
246 SOME (thm, _) => thm |
247 | NONE => error ("Unproven type arity " ^ |
247 | NONE => error ("Unproven type arity " ^ |
248 Syntax.string_of_arity (ProofContext.init_global thy) (a, Ss, [c]))); (* FIXME stale thy (!?) *) |
248 Syntax.string_of_arity (Proof_Context.init_global thy) (a, Ss, [c]))); (* FIXME stale thy (!?) *) |
249 |
249 |
250 fun thynames_of_arity thy (c, a) = |
250 fun thynames_of_arity thy (c, a) = |
251 Symtab.lookup_list (proven_arities_of thy) a |
251 Symtab.lookup_list (proven_arities_of thy) a |
252 |> map_filter (fn ((c', _), (_, name)) => if c = c' then SOME name else NONE) |
252 |> map_filter (fn ((c', _), (_, name)) => if c = c' then SOME name else NONE) |
253 |> rev; |
253 |> rev; |
357 | xs => raise TYPE ("Class " ^ string_of_sort [c1] ^ " lacks parameter(s) " ^ |
357 | xs => raise TYPE ("Class " ^ string_of_sort [c1] ^ " lacks parameter(s) " ^ |
358 commas_quote xs ^ " of " ^ string_of_sort [c2], [], [])); |
358 commas_quote xs ^ " of " ^ string_of_sort [c2], [], [])); |
359 in (c1, c2) end; |
359 in (c1, c2) end; |
360 |
360 |
361 fun read_classrel thy raw_rel = |
361 fun read_classrel thy raw_rel = |
362 cert_classrel thy (pairself (ProofContext.read_class (ProofContext.init_global thy)) raw_rel) |
362 cert_classrel thy (pairself (Proof_Context.read_class (Proof_Context.init_global thy)) raw_rel) |
363 handle TYPE (msg, _, _) => error msg; |
363 handle TYPE (msg, _, _) => error msg; |
364 |
364 |
365 |
365 |
366 (* declaration and definition of instances of overloaded constants *) |
366 (* declaration and definition of instances of overloaded constants *) |
367 |
367 |
462 |
462 |
463 (* tactical proofs *) |
463 (* tactical proofs *) |
464 |
464 |
465 fun prove_classrel raw_rel tac thy = |
465 fun prove_classrel raw_rel tac thy = |
466 let |
466 let |
467 val ctxt = ProofContext.init_global thy; |
467 val ctxt = Proof_Context.init_global thy; |
468 val (c1, c2) = cert_classrel thy raw_rel; |
468 val (c1, c2) = cert_classrel thy raw_rel; |
469 val th = Goal.prove ctxt [] [] (Logic.mk_classrel (c1, c2)) (K tac) handle ERROR msg => |
469 val th = Goal.prove ctxt [] [] (Logic.mk_classrel (c1, c2)) (K tac) handle ERROR msg => |
470 cat_error msg ("The error(s) above occurred while trying to prove class relation " ^ |
470 cat_error msg ("The error(s) above occurred while trying to prove class relation " ^ |
471 quote (Syntax.string_of_classrel ctxt [c1, c2])); |
471 quote (Syntax.string_of_classrel ctxt [c1, c2])); |
472 in |
472 in |
473 thy |> add_classrel th |
473 thy |> add_classrel th |
474 end; |
474 end; |
475 |
475 |
476 fun prove_arity raw_arity tac thy = |
476 fun prove_arity raw_arity tac thy = |
477 let |
477 let |
478 val ctxt = ProofContext.init_global thy; |
478 val ctxt = Proof_Context.init_global thy; |
479 val arity = ProofContext.cert_arity ctxt raw_arity; |
479 val arity = Proof_Context.cert_arity ctxt raw_arity; |
480 val names = map (prefix arity_prefix) (Logic.name_arities arity); |
480 val names = map (prefix arity_prefix) (Logic.name_arities arity); |
481 val props = Logic.mk_arities arity; |
481 val props = Logic.mk_arities arity; |
482 val ths = Goal.prove_multi ctxt [] [] props |
482 val ths = Goal.prove_multi ctxt [] [] props |
483 (fn _ => Goal.precise_conjunction_tac (length props) 1 THEN tac) handle ERROR msg => |
483 (fn _ => Goal.precise_conjunction_tac (length props) 1 THEN tac) handle ERROR msg => |
484 cat_error msg ("The error(s) above occurred while trying to prove type arity " ^ |
484 cat_error msg ("The error(s) above occurred while trying to prove type arity " ^ |
615 fun ax_classrel prep = |
615 fun ax_classrel prep = |
616 axiomatize (map o prep) (map Logic.mk_classrel) |
616 axiomatize (map o prep) (map Logic.mk_classrel) |
617 (map (prefix classrel_prefix o Logic.name_classrel)) add_classrel; |
617 (map (prefix classrel_prefix o Logic.name_classrel)) add_classrel; |
618 |
618 |
619 fun ax_arity prep = |
619 fun ax_arity prep = |
620 axiomatize (prep o ProofContext.init_global) Logic.mk_arities |
620 axiomatize (prep o Proof_Context.init_global) Logic.mk_arities |
621 (map (prefix arity_prefix) o Logic.name_arities) add_arity; |
621 (map (prefix arity_prefix) o Logic.name_arities) add_arity; |
622 |
622 |
623 fun class_const c = |
623 fun class_const c = |
624 (Logic.const_of_class c, Term.itselfT (Term.aT []) --> propT); |
624 (Logic.const_of_class c, Term.itselfT (Term.aT []) --> propT); |
625 |
625 |
635 end; |
635 end; |
636 |
636 |
637 in |
637 in |
638 |
638 |
639 val axiomatize_class = ax_class Sign.certify_class cert_classrel; |
639 val axiomatize_class = ax_class Sign.certify_class cert_classrel; |
640 val axiomatize_class_cmd = ax_class (ProofContext.read_class o ProofContext.init_global) read_classrel; |
640 val axiomatize_class_cmd = ax_class (Proof_Context.read_class o Proof_Context.init_global) read_classrel; |
641 val axiomatize_classrel = ax_classrel cert_classrel; |
641 val axiomatize_classrel = ax_classrel cert_classrel; |
642 val axiomatize_classrel_cmd = ax_classrel read_classrel; |
642 val axiomatize_classrel_cmd = ax_classrel read_classrel; |
643 val axiomatize_arity = ax_arity ProofContext.cert_arity; |
643 val axiomatize_arity = ax_arity Proof_Context.cert_arity; |
644 val axiomatize_arity_cmd = ax_arity ProofContext.read_arity; |
644 val axiomatize_arity_cmd = ax_arity Proof_Context.read_arity; |
645 |
645 |
646 end; |
646 end; |
647 |
647 |
648 end; |
648 end; |