[isabelle-dev] find_theorems raises UnequalLengths exception

Brian Huffman brianh at cs.pdx.edu
Thu Nov 18 17:03:09 CET 2010

Hello everyone,

Recently I noticed that in HOLCF, whenever I do a theorem search for
theorems containing the constant "UU" (i.e. bottom), the search fails
with an UnequalLengths exception. I tracked the problem down to this
specific theorem from Fun_Cpo.thy: Before this point, find_theorems
"UU" succeeds, and afterward it causes an error.

lemma app_strict: "UU x = UU"

I found that I can also reproduce the problem directly in HOL:

theory Scratch
imports Orderings

find_theorems "bot"

lemma bot_apply: "bot x = bot"
by (simp only: bot_fun_eq)

find_theorems "bot"

*** exception UnequalLengths raised
*** At command "find_theorems"

After doing "hg bisect", I traced the origin of the problem:


Can anyone figure this out?

- Brian

More information about the isabelle-dev mailing list