[isabelle-dev] inductive_set vs. 'a set

[Stefan Berghofer]

Quoting Lawrence Paulson <lp15 at cam.ac.uk>:
> I got this message several times when converting theories. There is  
> a workaround, but nevertheless, I think this is a bug.

Hi Larry,

the reason for this problem is the removal of the rules pred_equals_eq and
pred_subset_eq from the rule database used for the predicate / set conversion:

   http://isabelle.in.tum.de/repos/isabelle/rev/a6cb51c314f2

The conversion of lists_mono to predicate notation already failed before the
re-introduction of the set type, but this did not cause an error message
because the monotonicity rule for listsp was already part of the database
of monotonicity rules, and the ill-formed monotonicity rule was simply
ignored. Now that sets are no longer predicates, the conclusion of the
ill-formed rule

   {x. ?A x} <= {x. ?B x} ==> {x. listsp ?A x} <= {x. listsp ?B x}

is no longer an inequality between predicates, and so the rule is rejected.

I will revert (parts of) the above changeset, and maybe also the related ones

   http://isabelle.in.tum.de/repos/isabelle/rev/0af0f674845d
   http://isabelle.in.tum.de/repos/isabelle/rev/a27607030a1c

Do you still remember in which theories you applied your workaround?
Maybe we should take a look at them again.

Greetings,
Stefan