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

[Makarius]

On 31/08/16 11:04, Burkhart Wolff wrote:
> 
> 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))));

Thm.check_hyps is just one more step in tightening the system, to
enforce intended logical context structure on tools.  It is used in key
places where goals and facts are accessed, see Isabelle/625370769fc0
from 11-Jan-2014 (i.e. more than two Isabelle releases ago).

Non-compliant tools can use Thm.unchecked_hyps on a local context, but
not on a global theory.


> A remedy is of course that we manage PO’s fundamentally differently- as terms with a wrapper that 
> yields logically true, for instance.

This sounds reasonable. Using schematic variables and
Logic.mk_term/dest_term or Drule.mk_term/dest_term allows to pass
arbitrary term information into and out of goals. See also the
"implementation" manual, section 2.3.2.


> Another way is of course to define our own command thm, of course, without the check.

This would mean to work against the overall system infrastructure. It is
unlikely to work out properly.


> Still, we think that the generation of PO’s via Thm.assume  is conceptually the cleanest way.

Maybe in a version of Isabelle from more 10-15 years ago. The context
has become very important after 2005, and more and more explicit checks
have emerged.


> isabelle-dev mailing list

BTW, the front page defines this mailing list as follows: "covers the
Isabelle development process, including intermediate repository
versions, and administrative issues concerning the website or testing
infrastructure."

Almost everything else should go to isabelle-users. Using Isabelle/ML
for Isabelle tool development is normal use of Isabelle, not development
of Isabelle itself.


	Makarius