[isabelle-dev] Problem with thm and meta-hypothesis

[Burkhart Wolff]

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