[isabelle-dev] inductive_set vs. 'a set

2012-01-09 Thread Makarius 

There is another drop-out concerning 'a set (in Isabelle/05a82dd869ed):

inductive_set
  well_formed_gterm' :: ('f \Rightarrow nat) \Rightarrow 'f gterm set
  for arity :: 'f \Rightarrow nat
where
step[intro!]: \lbrakkargs \in lists (well_formed_gterm' arity);
length args = arity f\rbrakk
   \Longrightarrow (Apply f args) \in well_formed_gterm' arity
monos lists_mono

*** Bad monotonicity theorem:
*** {x. ?A x} = {x. ?B x} == {x. listsp ?A x} = {x. listsp ?B x}
*** At command inductive_set (line 153 of 
~~/doc-src/TutorialI/Inductive/Advanced.thy)



That is probably a bit too exotic to expect NEWS to say what needs to be 
done.  Nonetheless I am curious about the reason of this failure.



Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] inductive_set vs. 'a set

2012-01-09 Thread Stefan Berghofer 

Quoting Lawrence Paulson l...@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

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev