[isabelle-dev] inductive_set vs. 'a set

Stefan Berghofer berghofe at in.tum.de
Mon Jan 9 17:54:56 CET 2012

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:


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


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


More information about the isabelle-dev mailing list