Dear all,

in the past, we used the kernel operation Thm.assume to generate and manage 
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 

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

Reply via email to