On Thu, Nov 18, 2010 at 8:25 AM, Lawrence Paulson <[email protected]> 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 >> [email protected] >> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev > > _______________________________________________ Isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
