[isabelle-dev] SELECT_GOAL

[Makarius]

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