lp15 at cam.ac.uk
Thu Jun 27 13:32:31 CEST 2013
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.
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
> 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: )
> 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.
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
More information about the isabelle-dev