[isabelle-dev] find_theorems raises UnequalLengths exception

[Brian Huffman]

On Thu, Nov 18, 2010 at 8:25 AM, Lawrence Paulson <lp15 at cam.ac.uk> wrote:
> That is certainly my change, but I don't understand why preventing self-referential type instantiations should affect the find_theorems function. Can you get a full trace back from the exception?

Here's what I get from turning on the debugging flag in Proof General:

Exception trace for exception - UnequalLengths
Library.~~(2)
Pattern.match(3)cases(5)rigrig1(2)
Pattern.match(3)cases(5)
Pattern.match(3)mtch(4)
Pattern.match(3)
Pattern.matches_subterm(3)msub(2)
Pattern.matches_subterm(3)msub(2)
Pattern.matches_subterm(3)
Find_Theorems.filter_pattern(2)check(3)
Find_Theorems.filter_pattern(2)check(1)
o(2)(1)
Find_Theorems.app_filters(1)app(3)
List.mapPartial(2)
List.mapPartial(2)
List.mapPartial(2)
List.mapPartial(2)
List.mapPartial(2)
List.mapPartial(2)
List.mapPartial(2)
List.mapPartial(2)
Find_Theorems.sorted_filter(2)
Find_Theorems.find_theorems(5)find_all(2)
Find_Theorems.find_theorems(5)find_all(1)
Find_Theorems.print_theorems(5)
Toplevel.apply_tr(3)(1)
Runtime.debugging(2)(1)
End of trace

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

>
> Larry
>
> On 18 Nov 2010, at 16:03, Brian Huffman wrote:
>
>> 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
>> begin
>>
>> 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:
>>
>> http://isabelle.in.tum.de/repos/isabelle/rev/b654fa27fbc4
>>
>> Can anyone figure this out?
>>
>> - Brian
>> _______________________________________________
>> Isabelle-dev mailing list
>> Isabelle-dev at mailbroy.informatik.tu-muenchen.de
>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>
>