Re: [isabelle] exception UnequalLengths raised (line 543 of "library.ML")

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"
  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"
  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.



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.