Re: [isabelle-dev] NEWS: generated code as proper theory export

[Mathias Fleury]

Hi Makarius,

> On 31. Jan 2019, at 20:10, Makarius  wrote:
> 
> On 31/01/2019 18:27, Peter Lammich wrote:
>> On Do, 2019-01-31 at 16:03 +0100, Makarius wrote:
>>> I have looked around at typical uses of 'export_code' in AFP. Most of
>>> the time it is just informative: writing a file and looking at it in
>>> the
>>> editor (or via the command-line!?), or doing that on the output
>>> channel.
>>> The isabelle-export: file-system covers that already, i.e. we should
>>> be
>>> able to eliminate almost all generated files from the AFP repository.
>>> 
>>> So "export_code .. file" should just disappear -- it is semantically
>>> illtyped in PIDE: editing the "file" argument will leave a trace of
>>> machine oil spilled to the physical file-system.
>> 
>> The problem here is actually deeper: 
>> Many AFP-entries are designed to export code which then works together
>> with some external code. However, there seems to be no way to test
>> whether this external code works with the generated code. 
> 
> Can you point to these special applications?
> 
> If export_code uses Generated_Files.add_files (in addition to
> Export.export) we get both a check for unique names and an easy way to
> retrieve the exports in Isabelle/ML, e.g. to write to a temporary
> directory and do some tests.

Can you give some more details on how to achieve this?

Concrete application: I have a verified SAT solver (lets call that function 
isasat), an unverified parser, and several large CNF files (each one is several 
MB large). I would like to compile the SAT solver with MLton*, test it on those 
CNF files. With some timings information to identify regression if possible.


> So far I have never seen an application that could not be made stateless
> and thus fit properly into the PIDE model.


Mathias


* Last time I tried, MLton was an order of magnitude faster than Poly/ML. But I 
can rewrite the parser for Poly/ML.

> 
> 
>   Makarius
> 
> ___
> 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

Re: [isabelle-dev] Explorer.thy [was: performance problems]

[Mathias Fleury]

Hi all,


I have my own version of explore 
(https://bitbucket.org/isafol/isafol/src/master/lib/Explorer.thy 
), which does 
not have better pretty printing, but has two variants that I find 
indispensable: explore_have produces "have … if … for …" and explore_lemma 
produces "lemma fixes … assumes … shows …". There is even an option for 
cartouches.



Mathias


> On 12. Sep 2018, at 11:12, Lawrence Paulson  wrote:
> 
> Signed PGP part
> I regard it as indispensable. But it does need better pretty printing. Also I 
> greatly prefer the if/for format to assume/fix.
> 
> Larry
> 
>> On 12 Sep 2018, at 07:23, Florian Haftmann 
>>  wrote:
>> 
 On 7 Sep 2018, at 19:18, Makarius  wrote:
 
 I can't try it out, since theory "Explorer" is missing.
>>> 
>>> Attached. A very cool thing.
>> 
>> Nice to see that old draft from 5 years ago.
>> 
>> I would still agree that such a tool would be tremendously useful, but
>> before going into the distro it would need technical improvement, i.e.
>> more civilized approach toward Isar proof text generation, similar to
>> Sledgehammer_Isar_Proof.
>> 
>> Any opinions on that?
>> 
>> Cheers,
>>  Florian
>> 
>> --
>> 
>> PGP available:
>> http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
>> 
> 
> 

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

Re: [isabelle-dev] NEWS: Isabelle/VSCode

[Mathias Fleury]

Dear Makarius,

I am using Isabelle/VSCode code for a week now. So it is possible to
install and use it.


I mostly like it:

  * I really like VSCode's Control-P to search for commands.

  * the PIDE protocol, unlike "isabelle build", accepts unicode
characters: If the file contains "×⇩r" instead of "\\<^sub>r"
(e.g. because I copy-pasted it) , Isabelle/jEdit and Isabelle/VSCode
will accept the expression, but "isabelle build" will fail. It took
a long time to figure that out, since in Iaabelle/jEdit, the symbols
are shown in the same fashion.

  * there are some weird slow-downs: Every once in a while,
refreshing/jumping to the definition take several seconds. I am not
yet sure whether Isabelle or VSCode is responsible.


Mathias



On 01.07.17 19:36, Makarius wrote:
> *** General ***
>
> * Experimental support for Visual Studio Code (VSCode) as alternative
> Isabelle/PIDE front-end, see also
> https://marketplace.visualstudio.com/items?itemName=makarius.isabelle
>
> VSCode is a new type of application that continues the concepts of
> "programmer's editor" and "integrated development environment" towards
> fully semantic editing and debugging -- in a relatively light-weight
> manner. Thus it fits nicely on top of the Isabelle/PIDE infrastructure.
> Technically, VSCode is based on the Electron application framework
> (Node.js + Chromium browser + V8), which is implemented in JavaScript
> and TypeScript, while Isabelle/VSCode mainly consists of Isabelle/Scala
> modules around a Language Server implementation.
>
>
> This refers to Isabelle/8f39d60b943d. The marketplace link above also
> shows a screenshot.
>
> I am interested to hear if anybody manages to run the application:
> presently it lacks the all-inclusive application bundling of Isabelle/jEdit.
>
>
>   Makarius
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev



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

Re: [isabelle-dev] Uses of Jenkins at TUM

[Mathias Fleury]

Hello all,


First, I would like to thank Lars for the time he is spending on Jenkins.


On 24.04.17 17:47, Blanchette, J.C. wrote:
>> On 24 Apr 2017, at 17:12, Andreas Lochbihler 
>> <andreas.lochbih...@inf.ethz.ch> wrote:
>>
>> Sure. Whenever I have to push something to the Isabelle repository, I use 
>> the Jenkins testboard installation to see whether something broke. It works 
>> more reliably than the previous testboard infrastructure, which often 
>> ignored some commits.
> The same applies to me (VU Amsterdam), and I believe Mathias Fleury (MPII 
> Saarbrücken) is also a heavy user of Testboard when he modifies Isabelle 
> (e.g. the multiset library).
>
> From a pure basic user's perspective, I don't see much of a difference 
> between Mira and Jenkins. To me it's just Testboard, and most of the time it 
> works, and then I'm happy. Sometimes Mathias just sends me a link to a patch 
> he's pushed to Testboard for me to review, before he pushes it to Isabelle. 
> That's also very useful.
Indeed. (Actually, patches can be seen here
<https://isabelle.in.tum.de/repos/testboard> or here for AFP-testboard
<https://bitbucket.org/isa-afp/afp-testboard>, but both are unrelated to
Jenkins).
 
> What is good about it?
(I don't remember enough of the previous system to compare it to Jenkins.)

  * automatic testing (I have forgotten to add files a couple of times).

  * timings

(https://ci.isabelle.systems/statistics/isabelle-nightly-benchmark/index.html).
It is useful to see how it evolves over time.


>  What is bad about it?
I am trying very hard to not break Isabelle and the AFP. Therefore, I
hate receiving an email of Jenkins telling me that I have broken something.

  * Spurious timeouts (like nightly-mac
<https://ci.isabelle.systems/jenkins/job/isabelle-nightly-mac/>
currently). At some point, there were timeouts that appeared after
one of my changes, but I could not reproduce them (they were related
to timeouts of quickcheck). Interestingly, I am now in the opposite
situation: At home, I currently have a lot of timeouts related to
"export_code" in Refine_Imperative_HOL that do not appear in
Jenkins. I will send another email to the mailing list related to that.

  * Testing both Isabelle and AFP changes would be nice. This is
especially important for multisets that are not widely used in
Isabelle: Most bad simp rule break the AFP, not Isabelle.



However, both problems are hard to solve and I am happy with the current
situation. I even run a Jenkins instance at home.



Mathias
> Jasmin
>
> ___
> 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

Re: [isabelle-dev] macOS Sierra 10.12

[Mathias Fleury]

Hello Makarius,


> Has anybody tried Sierra already? That can be done by the .dmg provided
> on http://isabelle.in.tum.de/devel 

I am using Isabelle devel and RC0 on Sierra (for two weeks), without problem so 
far.


Mathias



> The official platform support scheme for Isabelle is documented in
> Isabelle/Admin/PLATFORMS:
> http://isabelle.in.tum.de/repos/isabelle/file/692a1b317316/Admin/PLATFORMS#l25
> 
> It shows that Mac OS X 10.11 El Capitan is listed without a proof by
> some reference machine (it is my old laptop at the moment). 10.12 is
> missing altogether, because I can't run that without giving Apple some
> money for hardware.
> 
> Filling this platform-support hole requires some remotely accessible
> machine that can be also used in interactive SSH and Apple terminal
> sessions: a batch-only test as presently done in Jenkins is not sufficient.

> If it cannot be done, we need to rethink Isabelle support on Mac OS X
> (err macOS).
> 
> About 10 years ago, I have become a part-time Mac user, because it was
> not sufficient to trust the sporadic testing by full-time Mac users.
> 
> We've got used to a situation where almost everything works, but that
> does not continue automatically out of custom.
> 
> 
>   Makarius
> 
> ___
> 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

Re: [isabelle-dev] Simplification theorems with more general typeclasses

[Mathias Fleury]

For the record, I have now pushed the change to Isabelle, see 
http://isabelle.in.tum.de/reports/Isabelle/rev/3365c8ec67bd 
<http://isabelle.in.tum.de/reports/Isabelle/rev/3365c8ec67bd>.

Mathias

> On 05 Jul 2016, at 14:03, Mathias Fleury <mathias.fle...@ens-rennes.fr> wrote:
> 
> Hi all,
> 
> after some more experiments, I found out that there is another difference 
> between explicit typeclass annotations and lemmas in the context: the former 
> theorems are included in instantiations but are not included in 
> interpretations. This usually does not make a difference, since there is 
> usually a single order on a type.
> 
> Instead, I introduced an additional typeclass to the hierarchy. The change 
> was successfully tested on testboard (mercurial diff 
> <http://isabelle.in.tum.de/repos/testboard/rev/18f26b6779ad>, status 
> <https://ci.isabelle.systems/jenkins/job/testboard/117/>), and does not need 
> any AFP change.
> 
> 
> Does someone have an opinion on this change?
> 
> 
> Mathias
>  
>> On 04 Jul 2016, at 14:20, Mathias Fleury <mathias.fle...@ens-rennes.fr 
>> <mailto:mathias.fle...@ens-rennes.fr>> wrote:
>> 
>> Hi Johannes,
>> 
>> 
>> the multiset ordering (contrary to the subset ordering) does not have this 
>> property:
>> 
>>  lemma "{#0#} <= {#Suc 0#}”
>>unfolding Multiset_Order.le_multiset⇩H⇩O by auto
>> 
>> (the actual notation is #⊆# and not <=).
>> 
>> 
>> I tried locally to apply the changes of my previous email this week-end. 
>> Except some proofs inside the typeclass definitions (i.e. in the files 
>> Groups.thy, Rings.thy, and Missing_Ring.thy), no other changes were needed 
>> in Isabelle or the AFP.
>> 
>> 
>> Thanks for your answer,
>> Mathias
>> 
>> 
>>> On 04 Jul 2016, at 13:22, Johannes Hölzl <hoe...@in.tum.de 
>>> <mailto:hoe...@in.tum.de>> wrote:
>>> 
>>> Hi Mathias,
>>> 
>>> there is at least the type class 'canonically_ordered_monoid' which has
>>> the property a <= b <--> ?c. a + c = b which implies 0 <= a for all a.
>>> Are the multisets already in this typeclass?
>>> 
>>>  - Johannes
>>> 
>>> 
>>> Am Dienstag, den 28.06.2016, 10:04 +0100 schrieb Mathias Fleury:
>>>> Dear type-classes and simplifier experts,
>>>> 
>>>> in the plan of instantiating multisets with the multiset ordering, I
>>>> am trying to instantiate the multisets with additional typeclasses to
>>>> get specific simplification theorems. The aim is to mimic the
>>>> simplifier’s behaviour of other types like natural numbers. One of my
>>>> problems can be nicely illustrated by the following lemma: “M <= M +
>>>> N <-> 0 <= N”. 
>>>> 
>>>> 
>>>> Analog simplification rules already exist for rings (e.g., natural
>>>> numbers*) and ordered groups too:
>>>>thm
>>>> Rings.linordered_semiring_class.less_eq_add_cancel_left_greater_eq_ze
>>>> ro
>>>>thm Groups.ordered_ab_group_add_class.le_add_same_cancel1
>>>> Both rules are stating that “M <= M + N <—> 0 <= N” and are marked as
>>>> [simp].
>>>> 
>>>> 
>>>> However, the multisets are neither a group (no inverse for the law
>>>> “+”) nor a ring (no multiplication). I could duplicate the theorems,
>>>> but I noticed that the proofs of the theorems do only rely on the
>>>> fact it is a monoid_add (for the zero element) and an
>>>> ordered_ab_semigroup_add_imp_le (for the order). The following
>>>> theorem would work too and is general enough to include the multiset
>>>> case:
>>>> 
>>>> lemma le_add_same_cancel1 [simp]:
>>>>   “(a :: 'a :: {monoid_add, ordered_ab_semigroup_add_imp_le}) ≤ a + b
>>>> ⟷ 0 ≤ b”
>>>>   using add_le_cancel_left [of a 0] by simp
>>>> 
>>>> 
>>>> Are there any obvious differences between this more general version
>>>> with explicit type class annotations
>>>> and Groups.ordered_ab_group_add_class.le_add_same_cancel1? If no,
>>>> would it make sense to use this version in Isabelle?
>>>> 
>>>> 
>>>> 
>>>> Thanks in advance,
>>>> Mathias Fleury
>>>> 
>>>> 
>>>> 
>>>> 
>>>> * for natural numbers, the simproc
>>&

Re: [isabelle-dev] Simplification theorems with more general typeclasses

[Mathias Fleury]

Hi all,

after some more experiments, I found out that there is another difference 
between explicit typeclass annotations and lemmas in the context: the former 
theorems are included in instantiations but are not included in 
interpretations. This usually does not make a difference, since there is 
usually a single order on a type.

Instead, I introduced an additional typeclass to the hierarchy. The change was 
successfully tested on testboard (mercurial diff 
<http://isabelle.in.tum.de/repos/testboard/rev/18f26b6779ad>, status 
<https://ci.isabelle.systems/jenkins/job/testboard/117/>), and does not need 
any AFP change.


Does someone have an opinion on this change?


Mathias
 
> On 04 Jul 2016, at 14:20, Mathias Fleury <mathias.fle...@ens-rennes.fr> wrote:
> 
> Hi Johannes,
> 
> 
> the multiset ordering (contrary to the subset ordering) does not have this 
> property:
> 
>   lemma "{#0#} <= {#Suc 0#}”
> unfolding Multiset_Order.le_multiset⇩H⇩O by auto
> 
> (the actual notation is #⊆# and not <=).
> 
> 
> I tried locally to apply the changes of my previous email this week-end. 
> Except some proofs inside the typeclass definitions (i.e. in the files 
> Groups.thy, Rings.thy, and Missing_Ring.thy), no other changes were needed in 
> Isabelle or the AFP.
> 
> 
> Thanks for your answer,
> Mathias
> 
> 
>> On 04 Jul 2016, at 13:22, Johannes Hölzl <hoe...@in.tum.de 
>> <mailto:hoe...@in.tum.de>> wrote:
>> 
>> Hi Mathias,
>> 
>> there is at least the type class 'canonically_ordered_monoid' which has
>> the property a <= b <--> ?c. a + c = b which implies 0 <= a for all a.
>> Are the multisets already in this typeclass?
>> 
>>  - Johannes
>> 
>> 
>> Am Dienstag, den 28.06.2016, 10:04 +0100 schrieb Mathias Fleury:
>>> Dear type-classes and simplifier experts,
>>> 
>>> in the plan of instantiating multisets with the multiset ordering, I
>>> am trying to instantiate the multisets with additional typeclasses to
>>> get specific simplification theorems. The aim is to mimic the
>>> simplifier’s behaviour of other types like natural numbers. One of my
>>> problems can be nicely illustrated by the following lemma: “M <= M +
>>> N <-> 0 <= N”. 
>>> 
>>> 
>>> Analog simplification rules already exist for rings (e.g., natural
>>> numbers*) and ordered groups too:
>>> thm
>>> Rings.linordered_semiring_class.less_eq_add_cancel_left_greater_eq_ze
>>> ro
>>> thm Groups.ordered_ab_group_add_class.le_add_same_cancel1
>>> Both rules are stating that “M <= M + N <—> 0 <= N” and are marked as
>>> [simp].
>>> 
>>> 
>>> However, the multisets are neither a group (no inverse for the law
>>> “+”) nor a ring (no multiplication). I could duplicate the theorems,
>>> but I noticed that the proofs of the theorems do only rely on the
>>> fact it is a monoid_add (for the zero element) and an
>>> ordered_ab_semigroup_add_imp_le (for the order). The following
>>> theorem would work too and is general enough to include the multiset
>>> case:
>>> 
>>> lemma le_add_same_cancel1 [simp]:
>>>   “(a :: 'a :: {monoid_add, ordered_ab_semigroup_add_imp_le}) ≤ a + b
>>> ⟷ 0 ≤ b”
>>>   using add_le_cancel_left [of a 0] by simp
>>> 
>>> 
>>> Are there any obvious differences between this more general version
>>> with explicit type class annotations
>>> and Groups.ordered_ab_group_add_class.le_add_same_cancel1? If no,
>>> would it make sense to use this version in Isabelle?
>>> 
>>> 
>>> 
>>> Thanks in advance,
>>> Mathias Fleury
>>> 
>>> 
>>> 
>>> 
>>> * for natural numbers, the simproc
>>> Numeral_Simprocs.natle_cancel_numerals is able to do it too.
>>> ___
>>> isabelle-dev mailing list
>>> isabelle-...@in.tum.de <mailto:isabelle-...@in.tum.de>
>>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabel
>>> le-dev
>> ___
>> isabelle-dev mailing list
>> isabelle-...@in.tum.de <mailto: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

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

Re: [isabelle-dev] Simplification theorems with more general typeclasses

[Mathias Fleury]

Hi Johannes,


the multiset ordering (contrary to the subset ordering) does not have this 
property:

lemma "{#0#} <= {#Suc 0#}”
  unfolding Multiset_Order.le_multiset⇩H⇩O by auto

(the actual notation is #⊆# and not <=).


I tried locally to apply the changes of my previous email this week-end. Except 
some proofs inside the typeclass definitions (i.e. in the files Groups.thy, 
Rings.thy, and Missing_Ring.thy), no other changes were needed in Isabelle or 
the AFP.


Thanks for your answer,
Mathias


> On 04 Jul 2016, at 13:22, Johannes Hölzl <hoe...@in.tum.de> wrote:
> 
> Hi Mathias,
> 
> there is at least the type class 'canonically_ordered_monoid' which has
> the property a <= b <--> ?c. a + c = b which implies 0 <= a for all a.
> Are the multisets already in this typeclass?
> 
>  - Johannes
> 
> 
> Am Dienstag, den 28.06.2016, 10:04 +0100 schrieb Mathias Fleury:
>> Dear type-classes and simplifier experts,
>> 
>> in the plan of instantiating multisets with the multiset ordering, I
>> am trying to instantiate the multisets with additional typeclasses to
>> get specific simplification theorems. The aim is to mimic the
>> simplifier’s behaviour of other types like natural numbers. One of my
>> problems can be nicely illustrated by the following lemma: “M <= M +
>> N <-> 0 <= N”. 
>> 
>> 
>> Analog simplification rules already exist for rings (e.g., natural
>> numbers*) and ordered groups too:
>>  thm
>> Rings.linordered_semiring_class.less_eq_add_cancel_left_greater_eq_ze
>> ro
>>  thm Groups.ordered_ab_group_add_class.le_add_same_cancel1
>> Both rules are stating that “M <= M + N <—> 0 <= N” and are marked as
>> [simp].
>> 
>> 
>> However, the multisets are neither a group (no inverse for the law
>> “+”) nor a ring (no multiplication). I could duplicate the theorems,
>> but I noticed that the proofs of the theorems do only rely on the
>> fact it is a monoid_add (for the zero element) and an
>> ordered_ab_semigroup_add_imp_le (for the order). The following
>> theorem would work too and is general enough to include the multiset
>> case:
>> 
>> lemma le_add_same_cancel1 [simp]:
>>   “(a :: 'a :: {monoid_add, ordered_ab_semigroup_add_imp_le}) ≤ a + b
>> ⟷ 0 ≤ b”
>>   using add_le_cancel_left [of a 0] by simp
>> 
>> 
>> Are there any obvious differences between this more general version
>> with explicit type class annotations
>> and Groups.ordered_ab_group_add_class.le_add_same_cancel1? If no,
>> would it make sense to use this version in Isabelle?
>> 
>> 
>> 
>> Thanks in advance,
>> Mathias Fleury
>> 
>> 
>> 
>> 
>> * for natural numbers, the simproc
>> Numeral_Simprocs.natle_cancel_numerals is able to do it too.
>> ___
>> 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

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

[isabelle-dev] Simplification theorems with more general typeclasses

[Mathias Fleury]

Dear type-classes and simplifier experts,

in the plan of instantiating multisets with the multiset ordering, I am trying 
to instantiate the multisets with additional typeclasses to get specific 
simplification theorems. The aim is to mimic the simplifier’s behaviour of 
other types like natural numbers. One of my problems can be nicely illustrated 
by the following lemma: “M <= M + N <-> 0 <= N”. 


Analog simplification rules already exist for rings (e.g., natural numbers*) 
and ordered groups too:
thm 
Rings.linordered_semiring_class.less_eq_add_cancel_left_greater_eq_zero
thm Groups.ordered_ab_group_add_class.le_add_same_cancel1
Both rules are stating that “M <= M + N <—> 0 <= N” and are marked as [simp].


However, the multisets are neither a group (no inverse for the law “+”) nor a 
ring (no multiplication). I could duplicate the theorems, but I noticed that 
the proofs of the theorems do only rely on the fact it is a monoid_add (for the 
zero element) and an ordered_ab_semigroup_add_imp_le (for the order). The 
following theorem would work too and is general enough to include the multiset 
case:

lemma le_add_same_cancel1 [simp]:
  “(a :: 'a :: {monoid_add, ordered_ab_semigroup_add_imp_le}) ≤ a + b ⟷ 0 ≤ b”
  using add_le_cancel_left [of a 0] by simp


Are there any obvious differences between this more general version with 
explicit type class annotations and 
Groups.ordered_ab_group_add_class.le_add_same_cancel1? If no, would it make 
sense to use this version in Isabelle?



Thanks in advance,
Mathias Fleury




* for natural numbers, the simproc Numeral_Simprocs.natle_cancel_numerals is 
able to do it too.___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

[isabelle-dev] Lemmas about tranclp and lexn

[Mathias Fleury]

Dear list,

I stumbled upon some lemmas that have a counterpart in Isabelle (like 
rtranclp_mono vs tranclp_mono), but are not included. Is there a reason why the 
following lemmas are not included in Isabelle?

rtranclp vs tranclp:

there is a rtranclp_mono "r ≤ s ==> r^** ≤ s^**", but no tranclp_mono. Given 
the tranclp_mono, it should probably be:

lemma tranclp_mono:
  "r⇧+⇧+ a b ⟹ r ≤ s ⟹ s⇧+⇧+ a b"
using rtranclp_mono by (auto dest!: tranclpD intro: rtranclp_into_tranclp2)


there is a rtranclp_idemp and a rtrancl_idemp marked as simp "(r^**)^** = 
r^**", but no trancl_idemp nor tranclp_idemp

lemma trancl_idemp: "(r⇧+)⇧+ = r⇧+"
  by simp

lemmas tranclp_idemp = trancl_idemp[to_pred]


Transitivity of lexord vs lexn:
there is a lexord_transI "trans r ⟹ trans (lexord r)", but no lexn_transI

(I have not been able to factor the case distinction below; the proof uses the 
new consider keyword)

lemma lexn_transI:
  assumes trans: "trans r"
  shows "trans (lexn r n)"
unfolding trans_def
proof (intro allI impI)
  fix as bs cs
  assume asbs: "(as, bs) ∈ lexn r n" and bscs: "(bs, cs) ∈ lexn r n"

  obtain abs a b as' bs' where
n: "length as = n" and "length bs = n" and
as: "as = abs @ a # as'" and
bs: "bs = abs @ b # bs'" and
abr: "(a, b) ∈ r"
using asbs unfolding lexn_conv by blast

  obtain bcs b' c' cs' bs' where
n': "length cs = n" and "length bs = n" and
bs': "bs = bcs @ b' # bs'" and
cs: "cs = bcs @ c' # cs'" and
b'c'r: "(b', c') ∈ r"
using bscs unfolding lexn_conv by blast
  consider (le) "length bcs < length abs"
| (eq) "length bcs = length abs"
| (ge) "length bcs > length abs" by linarith
  then show "(as, cs) ∈ lexn r n"
proof cases
  let ?k = "length bcs"
  case le
  hence "as ! ?k = bs ! ?k" unfolding as bs by (simp add: nth_append)
  hence "(as ! ?k, cs ! ?k) ∈ r" using b'c'r unfolding bs' cs by auto
  moreover
have "length bcs < length as" using le unfolding as by simp
from id_take_nth_drop[OF this] have "as = take ?k as @ as ! ?k # drop 
(Suc ?k) as" .
  moreover
have "length bcs < length cs" unfolding cs by simp
from id_take_nth_drop[OF this] have "cs = take ?k cs @ cs ! ?k # drop 
(Suc ?k) cs" .
  moreover have "take ?k as = take ?k cs"
using le arg_cong[OF bs, of "take (length bcs)"] unfolding cs as bs' by 
auto
  ultimately show ?thesis using n n' unfolding lexn_conv by auto
next
  let ?k = "length abs"
  case ge
  hence "bs ! ?k = cs ! ?k" unfolding bs' cs by (simp add: nth_append)
  hence "(as ! ?k, cs ! ?k) ∈ r" using abr unfolding as bs by auto
  moreover
have "length abs < length as" using ge unfolding as by simp
from id_take_nth_drop[OF this] have "as = take ?k as @ as ! ?k # drop 
(Suc ?k) as" .
  moreover
have "length abs < length cs" using n n' unfolding as by simp
from id_take_nth_drop[OF this] have "cs = take ?k cs @ cs ! ?k # drop 
(Suc ?k) cs" .
  moreover have "take ?k as = take ?k cs"
using ge arg_cong[OF bs', of "take (length abs)"] unfolding cs as bs by 
auto
  ultimately show ?thesis using n n' unfolding lexn_conv by auto
next
  let ?k = "length abs"
  case eq
  hence "abs = bcs" "b = b'" using bs bs' by auto
  moreover hence "(a, c') ∈ r" using abr b'c'r trans unfolding trans_def by 
blast
  ultimately show ?thesis using n n' unfolding lexn_conv as bs cs by auto
qed
qed


Best regards,

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

[isabelle-dev] Isabelle/jEdit - Sidekick

[Mathias Fleury]

Hello list,

in the sidekick there is a "sub-panel"^1 below the sidekick (see the red 
rectangle in the joint screenshot). Is there a way to have line breaks in it? 
The difference between it and the tooltips that appear in the sidekick, is that 
the tooltips disappear, when moving the cursor, while the content of the 
"sub-panel" does not.


I think it would be even more useful if the full multiline theorem could be 
printed out (in the sidekick itself, there is not enough space).

Thanks,
Mathias


PS: I am posting to the dev mailing list, since the jEdit version changed since 
the 2015 release, but there are no line-breaks either in the stable version.


^1 it is probably not its real name, but I haven't found a better one in the 
Isabelle/jedit manual, 

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

Re: [isabelle-dev] NEWS: State panel

[Mathias Fleury]

Hello Makarius,

this might be intended, but in Isabelle/a99125aa964f from this morning the 
errors and warnings still goes to the output panel, which means that both panel 
have to be opened at the same time. 


Could you give us some insights about your workflow (for theorem proving) with 
the new state panel? I tried it this morning, but it did not fit nicely in my 
workflow, where I look at the output panel after typing a tactic to see if the 
goal is solved or what remains to prove. I would say that having ENTER bound to 
a command like "Insert Newline, Indent and update state panel" would be close 
enough to my workflow, but still solve the performance issues, you mentioned. 
Feedback from other users would be interesting here.


As a side question, is there a way to have two different panels docked at 
bottom open at the same time (i.e. splitting the bottom area into two parts and 
have two different panels in each)?


Thanks,
Mathias

> On 9 Nov 2015, at 21:41, Makarius  wrote:
> 
> * The State panel manages explicit proof state output, with jEdit action
> "isabelle.update-state" (shortcut S+ENTER) to trigger update according
> to cursor position.
> 
> * The Output panel no longer shows proof state output by default. This
> reduces resource requirements of prover time and GUI space.
> INCOMPATIBILITY, use the State panel instead or enable option
> "editor_output_state".
> 
> 
> This refers to Isabelle/bb20f11dd842.  The State panel has been around for a 
> while, without mentioning it explicitly.  It should now be sufficiently 
> consolidated for production use; even old GUI timing problems that caused 
> excessive flashing due to repaints should no longer happen.
> 
> Disabling option editor_output_state allows to get back to the traditional 
> Isabelle/jEdit behaviour, but tradtionalists might actually like the new 
> State panel better, because it is closer to Proof General (in the newer 
> 3-buffer model, not the truely traditional 2-buffer model).
> 
> 
>   Makarius
> 
> ___
> 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

Re: [isabelle-dev] Update of jdk and jedit components

[Mathias Fleury]

Thanks for the information,

Mathias

> On 4 Nov 2015, at 15:55, Makarius <makar...@sketis.net> wrote:
> 
> On Wed, 4 Nov 2015, Mathias Fleury wrote:
> 
>> I am a bit surprised that the content of the tooltips and the output panel 
>> can be changed (both in 6d513469f9b2 and Isabelle_23-Oct-2015).
>> 
>> Step to reproduce:
>> * open a theory file
>> * type a lemma
>> * select some text of the output panel
>> * type any letter
>> 
>> Result: the selected text is gone and replaced by what has been typed.
>> Expected: the output panel should not be changed.
> 
> This odd behaviour stems from d40f906bb13f, which is the update to 
> jedit-5.3.0.  The jedit-changes file says:
> 
>  - Allow editing, but not saving, of read only files.
>(Feature request #422 - Dale Anson)
> 
> The corresponding tracker item 
> http://sourceforge.net/p/jedit/feature-requests/422 reads like this:
> 
>  Jedit must allow user to make edits in a readonly files. It is very
>  wrong to disable this in any case: jedit is the _text editor_
> 
> Just from the wording, the feature request was formally wrong, and would not 
> have gone through on any Isabelle mailing list.
> 
> 
> This incident means I need to figure out a different way to avoid edits on 
> output-only text areas.
> 
> 
>   Makarius

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

Re: [isabelle-dev] Update of jdk and jedit components

[Mathias Fleury]

Hello Makarius,

I am a bit surprised that the content of the tooltips and the output panel can 
be changed (both in 6d513469f9b2 and Isabelle_23-Oct-2015).

Step to reproduce:
  * open a theory file
  * type a lemma
  * select some text of the output panel
  * type any letter

Result: the selected text is gone and replaced by what has been typed. 
Expected: the output panel should not be changed.


Strangely, the delete key keeps removing text from the theory buffer. I could 
not reproduce this behavior in Isabelle2015, but I do not know when this 
started.

Mathias

> On 23 Oct 2015, at 23:22, Makarius  wrote:
> 
> In Isabelle/d40f906bb13f there is now jdk-8u66 and jedit-5.3.0.  There are 
> relatively few changes from upstream; this is mainly consolidation.
> 
> As we are slowly approaching the pre-release mode, it is important to keep an 
> eye an all the fine points on all platforms.  Does Java 8 really work as it 
> should?
> 
> 
> Here is a full integration test of the application bundles for Linux, 
> Windows, Windows 64, Mac OS X:
> 
>  http://www4.in.tum.de/~wenzelm/test/Isabelle_23-Oct-2015
> 
> 
> Various details of the "app" have changed in the past few weeks, so it is 
> important to take a look if it conforms to the principle of monotonic 
> improvements that we've had in Isabelle for almost 30 years.
> 
> For example, all platforms now uniformly support a single-instance model of 
> the main desktop application.
> 
> 
>   Makarius
> ___
> 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