[isabelle-dev] SELECT_GOAL

[Lawrence Paulson]

For sure, nested function variables like P (B x) are much too risky to use with automation. It's essential, at the very least, to ensure that P is some definite abstraction.

Larry

On 27 Jun 2013, at 12:00, Makarius <makarius at sketis.net> wrote:

> On Thu, 27 Jun 2013, Makarius wrote:
> 
>> This is a continuation of the following threads from some weeks ago:
>> 
>> [isabelle-dev] auto raises a TYPE exception
> 
> Here is the updated example from that thread for Isabelle/a3b175675843:
> 
> 
> consts P :: "'a set => bool"
> lemma P_Int [intro]:  "P A ==> P B ==> P (A Int B)" sorry
> lemma P_UNIV [intro]: "P UNIV" sorry
> lemma P_INT [intro]: "ALL x : A. P (B x) ==> P (INT x : A. B x)" sorry
> lemma P_UNION [intro]: "ALL x : A. P (B x) ==> P (UN x : A. B x)" sorry
> 
> lemma
>  fixes x :: "'a" and Q :: "'b => bool" and f :: "'a => 'b"
>  shows "EX S. P S & x : S & (ALL xa : S. Q (f xa))"
>  apply (auto simp only: )
>  oops
> 
> 
> This produces a huge trace for HO unification.  Since SELECT_GOAL no longer uses that, it is inherent in the rules that are applied in the proof process. In fact P_INT and P_UNION look a bit ambitious, with conclusions of the form ?P XXX.
> 
> Larry can probably say more how to approach such problems differently.
> 
> 
> 	Makarius
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev