[isabelle-dev] Bug: Possible generalization error in 'Tactic.rule_by_tactic'

[Stefan Berghofer]

Simon Meier wrote:
> The inductive package uses rule_by_tactic with the simpset of the
> context. Moreover, rule_by_tactic is used inside a 'try', which implies
> that such an error may be visible only very indirectly. For an expert of
> this package it may be possible to find a test case.

Hi Simon and Alex,

here is a test case:

  inductive foo :: "'a => 'a => bool"
  where
    "foo x x"

  locale test =
    fixes t P
    assumes ensure_clash [simp]: "t = P"
  begin

  inductive_cases bar: "foo t z"

The problem is that "inductive_cases" instantiates the rule foo.cases,
which happens to contain the schematic variable ?P. If you rename the
locale parameter P to something else (say Q), it works. Unfortunately,
inductive_cases always fails with the error message "Proposition not
an inductive predicate", no matter what error actually occurred
internally ;-(

Greetings,
Stefan

-- 
Dr. Stefan Berghofer               E-Mail: berghofe at in.tum.de
Institut fuer Informatik           Phone: +49 89 289 17328
Technische Universitaet Muenchen   Fax:   +49 89 289 17307
Boltzmannstr. 3                    Room: 01.11.059
85748 Garching, GERMANY            http://www.in.tum.de/~berghofe