*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] exception UnequalLengths raised (line 543 of "library.ML")*From*: Manuel Eberl <eberlm at in.tum.de>*Date*: Wed, 15 Jul 2015 09:16:35 +0200*In-reply-to*: <CAJ-DSyxnyJq_KS1M_sVRfuhCSPikQw5jrB7r=yrSRuJJ--qiCA@mail.gmail.com>*References*: <CAJ-DSyxnyJq_KS1M_sVRfuhCSPikQw5jrB7r=yrSRuJJ--qiCA@mail.gmail.com>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:31.0) Gecko/20100101 Thunderbird/31.7.0

The problem seems to be in Rule_Cases.extract_assumes, so Makarius is probably the one to answer your question if the UnequalLengths exception is the intended behaviour and where it comes from. However, what I can tell you is that what you are doing is not what you want to do anyway: Your goal at that point is "âx. G â H â x â example G â x â example H". The implication arrow associated to the right, i.e. the goal is "âx. G â H â (x â example G â x â example H)". What this means is that you must fix an x (like you did) and you may assume "G â H" and "x â example G". You may, however, not assume "G â H â x â example G", which is certainly also true, but logically very different. If you do it like this, there is no exception: lemma "G â H â example G â example H" proof fix x :: "nat" assume "G â H" "x â example G" hence "x â example H" proof induction However, the induction does not work out either. As a rule, when applying "induction", you should always give it the terms you want to induct over and the rule it should use (if it is not the default rule, like induction over natural numbers). You do not give it that information, and as a consequence, it just uses some random induction rule, resulting in a very strange result. Therefore, what you really want to do is this: lemma "G â H â example G â example H" proof fix x :: "nat" assume "x â example G" "G â H" hence "x â example H" by (induction x rule: example.induct) auto Note that I swapped the order of the two assumptions because the induction rule example.induct has "?x â example ?H" as a premise and "induction" wants to have these premises first and any additional facts afterwards. You can then even write "apply induction" and it will pick the right rule, but I would nevertheless still give the rule explicitly to make the proof more robust against changes in the background theory. Cheers, Manuel

**Follow-Ups**:

**References**:**[isabelle] exception UnequalLengths raised (line 543 of "library.ML")***From:*Jason Dagit

- Previous by Date: [isabelle] exception UnequalLengths raised (line 543 of "library.ML")
- Next by Date: [isabelle] inductive_set with non-fixed parameters
- Previous by Thread: [isabelle] exception UnequalLengths raised (line 543 of "library.ML")
- Next by Thread: Re: [isabelle] exception UnequalLengths raised (line 543 of "library.ML")
- Cl-isabelle-users July 2015 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list