makarius at sketis.net
Thu Jun 27 13:00:33 CEST 2013
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.
More information about the isabelle-dev