Re: [isabelle-dev] Standard component setup (Re: NEWS)

2012-01-09 Thread Makarius 

On Sun, 8 Jan 2012, Alexander Krauss wrote:


On 01/05/2012 12:19 PM, Jasmin Christian Blanchette wrote:
We are not allowed to distribute Yices. When publishing the components, 
please exclude Yices.


... and Vampire.


Could we instead provide a little script (or Isabelle tool) that turns a 
tarball/zip downloaded from upstream into a packaged Isabelle component?


This would possibly lower the entry barrier for using these systems, and 
should be fine with the licenses. It can also save a little packaging 
work in the future.


I've occasionally spent some thoughts on Z3 as well.  MSR did not mind 
other distribution channels, but the user has to indicate his 
non-commercial status explicit, doing some awkward editing of the 
compinent settings.


This could be somehow facilitated by allowing explicit interactive setup 
for components, say as Scala/JVM module that posts a dialog and asks the 
user to tick a license agreement before the settings are patched 
accordingly. Once that this concept is supported, one could easily include 
an adhoc download as well, say for retrieving Vampire from its official 
website.


Anyway, there are so many other things that could be done to simplify 
deployment.  I am not sure how much priority to apply to this painful 
non-free stuff right now.



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

[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

[isabelle-dev] src/HOLCF/IsaMakefile

2012-01-09 Thread Makarius 

Does the old src/HOLCF/IsaMakefile still have any purpose?

Ever since the inclusion of HOLCF within the regular HOL session library 
it should be subsumed by the main src/HOL/IsaMakefile.  Some recent 
changes appy to both files nonetheless, see 
http://isabelle.in.tum.de/repos/isabelle/log/f363e5a2f8e8/src/HOL/HOLCF/IsaMakefile 
but the old HOLCF version probably has diverged from the HOL one already. 
(Makefiles are hard to maintain anyway.)



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