Re: [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

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

[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


___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev