Dear all,
in the past, we used the kernel operation Thm.assume to generate and manage
proof-obligations.
This had the advantage that they can be displayed and handled transparently;
and then eventually
discharged by later processes.
Apparently, having thm's in the theory context is no longer desired:
fun undeclared_hyps context th =
Thm.hyps_of th
|> filter_out
(case context of
Context.Theory _ => K false
| Context.Proof ctxt =>
(case Hyps.get ctxt of
{checked_hyps = false, ...} => K true
| {hyps, ...} => Termtab.defined hyps));
fun check_hyps context th =
(case undeclared_hyps context th of
[] => th
| undeclared =>
error (Pretty.string_of (Pretty.big_list "Undeclared hyps:"
(map (Pretty.item o single o Syntax.pretty_term (Syntax.init_pretty
context)) undeclared))));
in MoreThm introduces an explicit check for for the command “thm” that makes it
fail in case
of the presence of meta-hype.
A remedy is of course that we manage PO’s fundamentally differently- as terms
with a wrapper that
yields logically true, for instance.
Another way is of course to define our own command thm, of course, without the
check.
Still, we think that the generation of PO’s via Thm.assume is conceptually the
cleanest way.
Do have a particular idea on what is the recommended way to handle this
situation ?
chantal & bu
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
