[isabelle-dev] NEWS: abbrevs and symbols dockable

2016-09-14 Thread Makarius 
*** Prover IDE -- Isabelle/Scala/jEdit ***

* Dockable window "Symbols" also provides access to 'abbrevs' from the
outer syntax of the current theory buffer. This provides clickable
syntax templates, including entries with empty abbrevs name (which are
inaccessible via keyboard completion).

* Additional abbreviations for syntactic completion may be specified
within the theory header as 'abbrevs'. The theory syntax for 'keywords'
has been simplified accordingly: optional abbrevs need to go into the
new 'abbrevs' section.

* Global abbreviations via $ISABELLE_HOME/etc/abbrevs and
$ISABELLE_HOME_USER/etc/abbrevs are no longer supported. Minor
INCOMPATIBILITY, use 'abbrevs' within theory header instead.


This refers to Isabelle/2683c3be36eb (and AFP/88ebc309096a). Examples
for abbrevs within theory headers are here:

  src/HOL/Nonstandard_Analysis/HLim.thy
  src/HOL/Nonstandard_Analysis/HSEQ.thy
  AFP/thys/HereditarilyFinite/HF.thy

After importing such theories, the "Symbols" dockable will update its
"Abbrevs" tab dynamically, according to the buffer syntax. (I have also
added an event handler for the global font size, and re-unified the
symbol GUI rendering with the completion popup.)


With this convenient way to provide input methods (i.e. keyboard
completion or clickable buttons) via regular theory libraries, we can
become more ambitious with fancy notation -- in only *one* version with
the full glory of symbols, sub-/superscripts, bold, bells, whistles.

A still open problem is how to input the place holder character (ASCII
bell) for templates in specifications of 'abbrevs'. Right now it can be
copied from the 'abbrevs' section of src/Pure/Pure.thy or produced via
the following BeanShell snippet:

   buffer.insert(textArea.getCaretPosition(), "\u0007")


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

[isabelle-dev] Jenkins maintenance

2016-09-14 Thread Lars Hupel 
Dear Isabelle developers,

over the weekend, there will be – once again – a scheduled maintenance
on the build infrastructure. I will add some more jobs (which are
running nightly) to test a wider variety of side conditions (mainly
-j/-o threads). I will take this opportunity to tidy up the Jenkins home
page, too. In the unlikely event that something goes wrong with my
deployment scripts and I have to roll back changes,

- there might be cancelled jobs
- there might be bogus mails

You can continue to use the testboard, but be prepared that I might have
to cancel jobs mid-move.

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

Re: [isabelle-dev] not-exists problem

2016-09-14 Thread Lawrence Paulson 
The symmetry between the variables in ~(∃x y. P x y) is completely lost in ∄x. 
∃y. P x y. It’s a terrible notation.
Larry

> On 13 Sep 2016, at 22:56, Jasmin Blanchette  
> wrote:
> 
>> I’m not sure that this suggestion addresses my original problem: that the 
>> use of the negated quantifier (by an output translation, i.e., not by 
>> request) produced a confusing output. This output already contains only a 
>> single variable bound by ∄.
> 
> But to what extent do you find it confusing? Perhaps because our brains are 
> damaged by too much logic and too little math, many of us on this list seemed 
> to have no real issues parsing your example correctly.

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

Re: [isabelle-dev] not-exists problem

2016-09-14 Thread Tobias Nipkow 
This discussion clearly shows that ∃! with multiple bound variables is a recipe 
for confusion and should be avoided.


Tobias

On 14/09/2016 09:49, Peter Lammich wrote:

On Di, 2016-09-13 at 23:35 +, michael.norr...@data61.csiro.au
wrote:

Note that ∃!x. ∃!y. P x y is not equivalent to ∃!xy. P (fst xy) (snd
xy).

If you were going to support ∃!x y at all (and I can certainly see
the argument for forbidding it outright), I'd expect it to map to the
first formula above, and not the second.


So there seems to be no consensus on the meaning of "∃!x y".

Btw: I would strongly argue that a proposition like
"∃!x y. x = abs (y::int)" is wrong, however it holds with the "∃!x.
∃!y"-semantics.

--
  Peter





Michael

On 13/09/2016, 18:41, "isabelle-dev on behalf of Tjark Weber"  wrote:

On Tue, 2016-09-13 at 09:45 +0200, Peter Lammich wrote:
> I would have expected:
> (∄x y. P x y) ⟷ ¬(∃x y. P x y)
> and
> (∃!x y. P x y) ⟷ (∃!xy. P (fst x) (snd x))

+1

Best,
Tjark


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


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

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





smime.p7s
Description: S/MIME Cryptographic Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] not-exists problem

2016-09-14 Thread Peter Lammich 
On Di, 2016-09-13 at 23:35 +, michael.norr...@data61.csiro.au
wrote:
> Note that ∃!x. ∃!y. P x y is not equivalent to ∃!xy. P (fst xy) (snd
> xy).
> 
> If you were going to support ∃!x y at all (and I can certainly see
> the argument for forbidding it outright), I'd expect it to map to the
> first formula above, and not the second.

So there seems to be no consensus on the meaning of "∃!x y".

Btw: I would strongly argue that a proposition like 
"∃!x y. x = abs (y::int)" is wrong, however it holds with the "∃!x.
∃!y"-semantics.

--
  Peter



> 
> Michael
> 
> On 13/09/2016, 18:41, "isabelle-dev on behalf of Tjark Weber"  le-dev-boun...@mailbroy.informatik.tu-muenchen.de on behalf of tjark.
> we...@it.uu.se> wrote:
> 
> On Tue, 2016-09-13 at 09:45 +0200, Peter Lammich wrote:
> > I would have expected:
> > (∄x y. P x y) ⟷ ¬(∃x y. P x y)
> > and
> > (∃!x y. P x y) ⟷ (∃!xy. P (fst x) (snd x))
> 
> +1
> 
> Best,
> Tjark
> 
> 
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/is
> abelle-dev
> 
> 
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabel
> le-dev
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] not-exists problem

2016-09-14 Thread Michael.Norrish 
Note that ∃!x. ∃!y. P x y is not equivalent to ∃!xy. P (fst xy) (snd xy).

If you were going to support ∃!x y at all (and I can certainly see the argument 
for forbidding it outright), I'd expect it to map to the first formula above, 
and not the second.

Michael

On 13/09/2016, 18:41, "isabelle-dev on behalf of Tjark Weber" 
 wrote:

On Tue, 2016-09-13 at 09:45 +0200, Peter Lammich wrote:
> I would have expected:
> (∄x y. P x y) ⟷ ¬(∃x y. P x y)
> and
> (∃!x y. P x y) ⟷ (∃!xy. P (fst x) (snd x))

+1

Best,
Tjark


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


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