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-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
