[isabelle-dev] NEWS: transitivity reasoner

[Clemens Ballarin]

* The transitivity reasoner for partial and linear orders is set up for
locales `order' and `linorder' generated by the new class package.   
Previously
the reasoner was only set up for axiomatic type classes.  Instances  
of the
reasoner are available in all contexts importing or interpreting  
these locales.
The following functionality is provided:
   - method `order' to invoke the reasoner manually.
   - diagnostic command `print_orders' shows which instances of the  
reasoner are
 available in the current context.
As previously, the reasoner is integrated with the simplifier as a  
solver.

Clemens

[isabelle-dev] [isabelle] Simplification in locales

[Clemens Ballarin]

Currently not.  Internally, a locale happens to be an interpretation  
in its decendants.

But note that you could add [cong del] to any interpretations you make.

Clemens


On 3 Jul 2008, at 23:32, John Matthews wrote:

 Is there a way to only apply a theorem attribute
 inside a locale and its descendants, but not in other locale
 interpretations?

[isabelle-dev] includes

[Clemens Ballarin]

Dear all,

I'm planning a major revision of the locale implementation and  
consider removing includes altogether.  Please get in touch if you  
have an application (outside the repository and afp) that depends on  
includes in a critical way.

Clemens

[isabelle-dev] NEWS

[Clemens Ballarin]

* Dropped locale element includes.  This is a major INCOMPATIBILITY.

In existing theorem specifications replace the includes element by the
respective context elements of the included locale, omitting those that
are already present in the theorem specification.  Multiple assume
elements of a locale should be replaced by a single one involving the
locale predicate.  In the proof body, declarations (most notably
theorems) may be regained by interpreting the respective locales in the
proof context as required (command interpret).

If using includes in replacement of a target solely because the
parameter types in the theorem are not as general as in the target,
consider declaring a new locale with additional type constraints on the
parameters (context element constrains).

Clemens

[isabelle-dev] Branch in isabelle repository

[Clemens Ballarin]

Hi all,

I wonder whether the second branch in the repository is intentional.  See

   http://isabelle.in.tum.de/repos/isabelle/graph/a0f38d8d633a

Unfortunately, it means that my revised locales code is now hidden  
from tip :-(

Clemens

[isabelle-dev] Branch in isabelle repository

[Clemens Ballarin]

Actually, having a closer look at the actual graph, this is a false  
alarm.  The the visualisation on that web page is misleading if not  
wrong.

Clemens


Quoting Clemens Ballarin ballarin at in.tum.de:

 Hi all,

 I wonder whether the second branch in the repository is intentional.  See

   http://isabelle.in.tum.de/repos/isabelle/graph/a0f38d8d633a

 Unfortunately, it means that my revised locales code is now hidden from
 tip :-(

 Clemens
 ___
 Isabelle-dev mailing list
 Isabelle-dev at mailbroy.informatik.tu-muenchen.de
 https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

[isabelle-dev] NEWS

[Clemens Ballarin]

* Thoroughly revised locales tutorial.  New section on conditional
interpretation.

[isabelle-dev] JinjaThreads

[Clemens Ballarin]

JinjaThreads doesn't seem to run out of the box (on macbroy2, with  
Poly/ML 5.3.0).  It seems to run out of memory.


I use ML_OPTIONS=-H 500, but I would assume the AFP sets this appropriately.

Probably this is a known issue, but I don't know where to check for  
the automatic AFP logs.


Clemens


macbroy2:admin ballarin$ ./testall JinjaThreads
Testing [JinjaThreads]
cd /Users/ballarin/isabelle/test/src/HOL;  
/Users/ballarin/isabelle/test/bin/isabelle make HOL-Word

make[2]: Nothing to be done for `Pure'.
Building HOL-Word ...
Finished HOL-Word (0:00:42 elapsed time, 0:01:13 cpu time, factor 1.73)
cd ..; /Users/ballarin/isabelle/test/bin/isabelle usedir -v true -i  
true -g true -d pdf -V outline=/proof,/ML   
/Users/ballarin/.isabelle//heaps/polyml-5.3.0_x86-darwin/HOL-Word  
JinjaThreads

Running HOL-Word-JinjaThreads ...

Run out of store - interrupting threads
Run out of store - interrupting threads
Run out of store - interrupting threads
Run out of store - interrupting threads
Run out of store - interrupting threads
Run out of store - interrupting threads
Failed to recover - exiting
Failed to recover - exiting
HOL-Word-JinjaThreads FAILED
(see also  
/Users/ballarin/.isabelle//heaps/polyml-5.3.0_x86-darwin/log/HOL-Word-JinjaThreads)


### (\^const==
###   (\^constHOL.Trueprop
### (_applC \taured1'r
###   (_cargs P
### (_cargs t
###   (_cargs h
### (_cargs (_tuple a (_tuple_arg xs))
###   (_tuple a' (_tuple_arg xs'
###   (\^constHOL.Trueprop
### (_applC \taured1'r
###   (_cargs P
### (_cargs t
###   (_cargs h
### (_cargs
###   (_tuple (\^constExpr.exp.AAss a i e)  
(_tuple_arg xs))

###   (_tuple
### (\^constExpr.exp.LAss  
(\^constExpr.exp.AAcc a' i) e)

### (_tuple_arg xs')
### Fortunately, only one parse tree is type correct.
### You may still want to disambiguate your grammar or your input.

make: ***  
[/Users/ballarin/.isabelle//heaps/polyml-5.3.0_x86-darwin/log/HOL-Word-JinjaThreads.gz] Error  
1

Finished [JinjaThreads]
The following tests failed:
JinjaThreads
Please check logs.

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

[isabelle-dev] NEWS

[Clemens Ballarin]

The upcoming release (which I guess will be called Isabelle 2011-0  
Dispensable Debate) will have the following notable extensions to  
locale interpretation:


* Locale interpretation commands 'interpret' and 'sublocale' accept
lists of equations to map definitions in a locale to appropriate
entities in the context of the interpretation.  The 'interpretation'
command already provided this functionality.

* New diagnostic command 'print_dependencies' prints the locale
instances that would be activated if the specified expression was
interpreted in the current context.  Variant 'print_dependencies!'
assumes a context without interpretations.

The mixins for the sublocale command feature (first item above) is a  
bit experimental.  In particular, it does not provide inheritance of  
mixins as interpretation and interpret do.  It is not yet clear to me  
how to best do this.  In any case, future extensions are expected to  
be compatible to the current state.


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

Re: [isabelle-dev] Proof General 4.1pre

[Clemens Ballarin]

Quoting Makarius makar...@sketis.net:

Are there still users of PG 3.x with recent Isabelle snapshots or  
versions from the repository?


I do.  I recently tried to use PG 4.0 with Aquamacs 2.1.  That didn't  
seem to work, so I went back to PG 3.7.1.1 and Carbon Emacs 1.6 (based  
on GNU Emacs 22.3.1).  I'd prefer using Aquamacs for the native  
cut-copy-paste.


One thing that didn't work was fonts (under the assumption Unicode  
would produce the same results for both combinations; I have not  
special fonts installed), and instructions how to do this with minimal  
intervention would be appreciated.  I think also the Isabelle/PG  
interaction did not work properly, and that's why I gave up in the end.


PG 3.7.1.1 and Carbon Emacs 1.6 have their issues as well, but I know  
how to live with them ...


Clemens

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

Re: [isabelle-dev] Proof General 4.1 on Mac OS X

[Clemens Ballarin]

I repeated my recent try of ProofGeneral on my Mac with   
ProofGeneral-4.1pre110118.  If used with Aquamacs I observe these  
issues:


- Menus respond slowly ( 1 second) when invoked for the first  time.   
This is fine if Aquamacs is used without ProofGeneral.

- Noise on the background shell.
- Fontification fails in one situation.  See attached image.
- Long arrows are displayed as boxes (I probably don't have a suitable  
font for this.)

- Light blue background of processed portion of the buffer is hard to see.

Unicode symbols that are available are displayed in the right size.   
This is much better than with my previous setup with PG 3.7.1.1 and  
Carbonemacs.


If the slow menus can be fixed this might be a suitable companion for  
Isabelle 2011.


Clemens

PS.  I did use this configuration:
- Aquamacs 2.1 distribution
- ProofGeneral-4.1pre110118
- MacOS X 10.5.8


Quoting Makarius makar...@sketis.net:


On Fri, 21 Jan 2011, Mamoun FILALI-AMINE wrote:

a remark: previously, there was aquamacs instead of emacs? I find   
auqamacs more convenient than emacs.


In recent Isabelle releases the default combination was Proof   
General 3.7.1.1 with Aquamacs based on Emacs 22.  That turned out as  
 half-decent, half-working -- after many weeks of desparate search  
in  the Mac OS X ecosphere.


In Isabelle2011 the default Proof General is going to be 4.1, which   
has quite different Emacs requirements, and generally quite   
different behaviour concerning special symbols etc.



So far, I did not spend much time to try all possible combinations   
of Emacsen with PG 4.1.  According to ProofGeneral/COMPATIBILITY,   
plain GNU Emacs 23.2 is recommended (aka the no nonsense version).  
  Aquamacs 2.1 is also based on that code base, so it could in   
principle work as well, despite fancy additions.


When I've tried the slightly older Aquamacs 2.0 some months ago, it   
turned out much slower than plain GNU Emacs 23 -- see also   
http://proofgeneral.inf.ed.ac.uk/trac/ticket/324 -- but that might   
be obsolete in several respects.



I hope to get more concrete feedback from Mac users.  So far I've   
mainly found out that most people are stuck with very old versions   
of Proof General, sometimes even in combination with ancient XEmacs.



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





attachment: Picture 1.png___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

[isabelle-dev] Poly/ML

[Clemens Ballarin]

After updating my Isabelle repository (which I haven't done for quite  
a while) Poly/ML stopped to start up.  I have 5.2 and according to the  
release notes this is no longer supported.  Do I need to build 5.4 for  
myself or do we provide a pre-built version for MacOS 10.5 somewhere?   
The Isabelle download page is surprisingly silent about Poly/ML  
nowadays.


Clemens

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

[isabelle-dev] Sledgehammer

[Clemens Ballarin]

While doing an 'isabelle makeall all' on my local machine, I  
encountered the error


  Sledgehammering...
  *** Unexpected outcome: unknown.
  *** At command sledgehammer (line 26 of  
/Users/ballarin/isabelle/hg/src/HOL/Metis_Examples/Proxies.thy)



I guess I lack some sort of heavy equipment here.  What surprises me  
is that on macbroy2 I don't have set up sledgehammer either, but I  
don't get this error.


Clemens

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

Re: [isabelle-dev] Sledgehammer

[Clemens Ballarin]

Hi Jasmin,

Thanks for this hint.  It turns out that I had set E_HOME to some  
bogus location.  Residue of some old setup...  Now it work fine.


Clemens


Quoting Jasmin Christian Blanchette jasmin.blanche...@gmail.com:


Am 24.06.2011 um 20:13 schrieb Clemens Ballarin:

While doing an 'isabelle makeall all' on my local machine, I  
encountered the error


 Sledgehammering...
 *** Unexpected outcome: unknown.
 *** At command sledgehammer (line 26 of  
/Users/ballarin/isabelle/hg/src/HOL/Metis_Examples/Proxies.thy)



I guess I lack some sort of heavy equipment here.  What surprises  
me is that on macbroy2 I don't have set up sledgehammer either, but  
I don't get this error.


These tests have a test to check whether you have the necessary  
equipment, so this is strange. Could you tell me what


ML {* getenv E_HOME *}

outputs on this installation and if it's not the empty string check  
whether there's an executable eproof script in that directory.  
Also, what happens if you write


lemma x = y == y = x
sledgehammer [e, verbose]

?

Thanks,

Jasmin




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

Re: [isabelle-dev] HOL/ex/Set_Algebras

[Clemens Ballarin]

I wondered when somebody would ask this.  What's going on here is a  
hack, and I'm not very happy about it.


If you follow up the imported theory, you will find some code that  
provides a clone of the interpretation command (under the same name!)  
with some added functionality (definitions).  This clone is used in  
some theories about operational semantics throughout HOL.  I have not  
fully understood what the clone does, but the code is outdated, and I  
believe it can be gotten rid of easily.  I don't see any added value  
in a command that makes both definitions and an interpretation.  Its  
purpose might have been to make the interpretation notationally  
simpler.  But that's no longer required, since 'where' clauses in  
interpretation now anticipate the syntax of the interpreted context,  
which makes writing left hand sides of the equations in the 'where'  
clauses easier.  (I hope what I write makes sense to anybody at all.)   
For example, one may write


  interpretation power: lattice Pow X op \subseteq
where power.meet = (\lambdaA \in Pow X. \lambdaB \in Pow  
X. A \inter B)
  and power.dual.meet = (\lambdaA \in Pow X. \lambdaB  
\in Pow X. A \union B)


where the locale 'lattice' has the (pseudo-)constants 'meet' and  
'dual.meet'.  If you look at a similar example in  
src/HOL/ex/LocaleTest2.thy (interpretation in line 490) you will see  
that this used to be a lot clumsier, involving the foundational  
constants.


Clemens


Quoting Alexander Krauss kra...@in.tum.de:


Hi all,

while backporting HOL/Library/Set_Algebras to use type classes again  
(a remaining point of the 'a set transition), I noticed that there  
is now a clone of that file in HOL/ex. The changelog says:



changeset:   41581:c34415351b6d
user:haftmann
date:Sat Jan 15 20:05:29 2011 +0100
summary: experimental variant of interpretation with  
simultaneous definitions, plus example


Unfortunately, nothing in the file itself states what it should  
demonstrate. Instead, the original comments remain, so there is  
plenty of opportunity for getting totally confused.


What should we do with the clone? Are there maybe other examples  
that can demonstrate interpretations with simultaneous definitions,  
so that we can simply remove it?


Alex
___
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] HOL/ex/Set_Algebras

[Clemens Ballarin]

Hi Florian,

Thanks for the clarification.


Its purpose
might have been to make the interpretation notationally simpler.


the story behind is not about syntax.  It is really about the
simultaneous definitions.  For a motivation, you can have a look at the
tutorial on code generation, section »Further issues«, »Locales and
interpretation«, where the pattern behind interpretation plus definition
is spelt out using the constant »funpows«.


This looks to me like a special case, but maybe one that is  
encountered frequently when generating code.  What do you intend to  
do?  Provide a special version of interpretation for code generation?


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

Re: [isabelle-dev] Interpretation [was HOL/ex/Set_Algebras]

[Clemens Ballarin]

Hi Florian,

I understood that much.  What I was hoping for was an answer on a more  
technical level.  The definition + interpretation pattern seem a  
useful thing to have.  But it sounds like, if you change the main  
interpretation command like this, you will break it for intended use  
cases (or at least clutter up user's theories with definitions they  
might not want to have).


Maybe what you want is an alternative command to 'interpretation'.   
Creating definitions from definition to me is not interpreting  
something in some other context by means of existing entities, but  
creating a new instance of something.  The interpretation command  
refrains from doing so for good reasons (i.e. flexibility).


Clemens


Quoting Florian Haftmann florian.haftm...@informatik.tu-muenchen.de:


Hi Clemens,


the story behind is not about syntax.  It is really about the
simultaneous definitions.  For a motivation, you can have a look at the
tutorial on code generation, section »Further issues«, »Locales and
interpretation«, where the pattern behind interpretation plus definition
is spelt out using the constant »funpows«.


This looks to me like a special case, but maybe one that is encountered
frequently when generating code.  What do you intend to do?  Provide a
special version of interpretation for code generation?


the intension is:

def (in foo) bar where ...
  --[ interpretation foo: ... ]--
def (in -) bar where ...

rather than

def (in foo) bar where ...
  --[ interpretation foo: ... ]--
abbreviation (in -) bar where ...

with --[ ... ]-- being the interpretation morphism.  The interpretation +
defines pattern was something which could be accomplished rather simple,
so I decided to make an experimental start with this in December 2010.

Cheers,
Florian

--

PGP available:
http://home.informatik.tu-muenchen.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] Locale interpretation with mixins

[Clemens Ballarin]

Hi Florian,

What is called mixin in the implementation is a transfer principle  
that is applied in addition to the interpretation morphism.  Currently  
users can only give equations, which yield rewrite morphisms, and  
consequently, the term 'mixin' appears nowhere in the documentation.   
On the other hand, the locale core 'knows' nothing about the  
equations.  For it, their are just general transfer principles.


Regarding your questions:

a) This is intentional.  Mathematics is full of examples where a  
concept can be defined differently (more easily) in a situation that  
is more concrete.  I might have to tweak inheritance of rewrite  
morphisms in the future, though, and that's why the documentation is  
relatively vague.


b) I don't yet see how one could reliably predict which equations  
should be unfolded.  This might be more obvious in the class package.   
For interpretation, we don't even know whether a rewrite morphism is  
related to a definition.


An alternative proof avoiding the 'OF construction' in your example is  
attached.


Clemens


Quoting Florian Haftmann florian.haftm...@informatik.tu-muenchen.de:


Hi Clemens,

I stumbled over two issues in locale interpretation.

a) According to the tutorial, in situation like these

  locale A = ?
--[ interpretation A: instantiation phi + mixin eqn]--  theory

  locale B = A + ?
--[ interpretation B: instantiation phi] -- theory

the mixin eqn is implicitly propagated to interpretation B.  I can
observe this (cf. theory Locale_Mixin_Subsumption_2.thy).

However, in a slightly more general situation

  locale A = ?
--[ interpretation A: instantiation phi + mixin eqn]--  theory

  locale B = A + ?
--[ interpretation B: instantiation phi'] --theory

where phi' is a more special variant of phi wrt. types, this does not
hold, i.e. eqn is not part of B (cf. theory
Locale_Mixin_Subsumption_1.thy, in which this situation appears quite
natural).

Is this behaviour intentional or a misfit?

b) The examples also show another issue: equations stemming from mixins
in interpretations are not applied to the interpretation proposition to
prove itself; consequently, if the assumption part of a locale to
interpret refers to derived definitions inside the locale, the proof of
this requires to handle the primitive expanded version of those
definitions rather than the definitions modulo the given mixins (hence
the ? [OF this] ? construction in the proofs in the examples).

This situations reminds of similiar experiences with derived definitions
and the class target, or even the target infrastructure in general,
where the equations stemming from derived definitions must be folded and
unfolded in critical situation, cf. e.g.
http://isabelle.in.tum.de/repos/isabelle/file/064394a1afb7/src/Pure/Isar/class_declaration.ML#l69
where the fundamental introduction rule for class membership is
preprocessed with those equations (»Class.these_defs«).  Maybe something
similar needs to be done here;  due to the dynamic nature of the
problem, I forsee no other possibility than to extend unfold_locales to
consider mixin equations also by folding them in the remaining goals.

Btw. these question have arisen when I spent some thought about the
future of Tools/interpretation_with_defs.ML

All the best,
Florian

--

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de





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

Re: [isabelle-dev] Interpretation with definitions [was Locale interpretation with mixins]

[Clemens Ballarin]

Hi Florian,

I appreciate that you now follow my reasoning that changes to the  
locales core machinery are not necessary for getting this  
functionality.  However, I don't think we should change how locale  
expressions work.  Currently we have:


  locale loc = fixes x assumes about_x: x = x

  interpretation const: loc less_eq by unfold_locales (rule refl)
  thm const.about_x -- {* op \le = op \le *}

  interpretation var: loc less_eq for less_eq by unfold_locales (rule refl)
  thm var.about_x  -- {* ?less_eq = ?less_eq *}

Also, I'm afraid I fail to understand the difference between 'where x  
= t' and 'where x is t'.


Clemens


Quoting Florian Haftmann florian.haftm...@informatik.tu-muenchen.de:


Hi Clemens, hi Makarius,

let me continue concerning syntax:

The current syntax in Tools/interpretation_with_defs.ML is just a proof
of concept:

interpretation L inst
  where
bar = t
  defines f is foo

A much better idea could be to give the new defs in a for-clause:

interpretation L inst
  for f :: T
  where
foo = f
bar = t

where the implicit definitions (f) are mentioned in the for-clause.

One could also think about hiding away the full generality of a) from
the user (for which there might be good reasons) and have something like

interpretation L inst
  for f :: T
  where
f is foo
t is bar

Or the where clause could be integrated completely into the locale
expression using named syntax:

interpretation L (| f := foo, t := bar |)
  for f :: T

Cheers,
Florian

--

PGP available:
http://home.informatik.tu-muenchen.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

[isabelle-dev] Unable to push to Isabelle reop

[Clemens Ballarin]

I'm recently getting

clemens-ballarins-macbook-air:IsarRef ballarin$ hg push
Password:
remote: Not trusting file  
/home/isabelle-repository/repos/isabelle/.hg/hgrc from untrusted user  
wenzelm, group isabelle
pushing to  
ssh://balla...@macbroy2.informatik.tu-muenchen.de//home/isabelle-repository/repos/isabelle

searching for changes
remote: Not trusting file  
/mnt/nfsbroy/home/isabelle-repository/repos/isabelle/.hg/hgrc from  
untrusted user wenzelm, group isabelle
remote: abort: could not lock repository  
/home/isabelle-repository/repos/isabelle: Permission denied

abort: unexpected response: empty string

I wonder whether this is related to the recently 'broken' repository,  
or are my permissions degrading?


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

Re: [isabelle-dev] Unable to push to Isabelle reop

[Clemens Ballarin]

Macbroy20 works for me.  Thanks, Florian and Alex.

Clemens


Quoting Alexander Krauss kra...@in.tum.de:


Quoting Clemens Ballarin balla...@in.tum.de:
[...]
pushing to  
ssh://balla...@macbroy2.informatik.tu-muenchen.de//home/isabelle-repository/repos/isabelle

searching for changes
remote: Not trusting file  
/mnt/nfsbroy/home/isabelle-repository/repos/isabelle/.hg/hgrc from  
untrusted user wenzelm, group isabelle
remote: abort: could not lock repository  
/home/isabelle-repository/repos/isabelle: Permission denied

abort: unexpected response: empty string

I wonder whether this is related to the recently 'broken'  
repository, or are my permissions degrading?


This may be a side effect of Makarius' re-cloning.
Maybe try another host as gateway? macbroy2 has a somewhat  
non-standard setup. Do you get the same result when using, e.g.  
macbroy20?


Alex




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

Re: [isabelle-dev] PLATFORMS

[Clemens Ballarin]

Any chance of still working on Leopard if I neither use jEdit nor any  
of the external provers?


Clemens


Quoting Makarius makar...@sketis.net:


Isabelle/10584ca5785f has an updated version of Admin/PLATFORMS.

Executive summary:

  * Mac OS Mountain Lion is now supported (macbroy30)

  * Mac OS Leopard has been discontinued

  * old 32 bit Mac hardware is no longer usable (lack of Java 7)

  * explicit ISABELLE_PLATFORM32 helps to make the platform jungle
a bit more robust to configure (this is relevant for component
settings)


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] document_output vs. old document_dump/document_dump_mode

[Clemens Ballarin]

For my most recent locales paper some tex files are generated with  
Isabelle 2009-1 because it uses the old axclass interface.  The rest  
is produced with a current repository version.  All files are dumped  
to the same document folder.  I wonder whether there is any chance to  
convert this somewhat absurd setup to the new mechanism.


Clemens


Currently Quoting Makarius makar...@sketis.net:

Are there remaining uses (or users) of the old document_dump /  
document_dump_mode options?  This corresponds to former options -D  
and -C of isabelle usedir.


The meaning of these features has become quite difficult to define,  
so it looks like they are better discontinued.


If there are remaining cases of difficult IsaMakefile/usedir  
configurations that still use them, they can be discussed here to  
see if anything is still missing in the new build tool to replace  
them.



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] Interpretation with definitions [was Locale interpretation with mixins]

[Clemens Ballarin]

Hi Florian,


Anyway, I am not so much concerned about syntax.  My primary intention
is to get rid of the experimental code in interpretation_with_defs.ML,
according to the following agenda:
a) Decide for a particular syntax (at the moment this can only be (*) as
it is conservative)
b) Enhance »interpretation« accordingly.  Also a different command can
be considered, but the interfaces in expression.ML must be extended in
any case.


If you must do this, please provide a separate command, don't just  
modify 'interpretation'.  Generalisation of 'interpretation' to locale  
targets as a light-weight variant to 'sublocale' is still on the  
roadmap (although without a concrete date) and I would like to avoid  
additional complications here.  Also, I've worked hard for  
'interpretation', 'interpret' and 'sublocale' to have uniform syntax,  
and I would like this to remain so.


Eventually, we will need to follow the route suggested by Makarius in  
the other fork of this thread, so local definitions behave properly in  
tools like the simplifier.


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

Re: [isabelle-dev] Locale interpretation with mixins

[Clemens Ballarin]

Quoting Makarius makar...@sketis.net:

It means that a constant c that depends on context parameters x y  
z is turned into a fountational constant loc.c in the background,  
and then re-imported into the local context as loc.c x y z.  Later  
it might get re-interpreted such that its dependency on former  
context parameters is turned into terms (by intepretation) or the  
whole thing loc.c t1 t2 t3 is replaced by something else  
(rewriting via mixins etc.).


If we can mark 'loc.c x y z' to make it atomic in tools like the  
simplifier (or, for uniformity, the entire system) I believe we are  
much better off.  Let's use angular brackets to mark the atomic part:  
loc.c x y z.  When parameters are instantiated, the thing should  
remain atomic: loc.c t1 t2 t3, because it denotes a constant in some  
other context.  If a rewrite morphism is applied, say loc.c t1 t2 t3  
= t4, then it should not remain atomic, for it is now the compound  
term the user turned it into.



So when the code generator sees an interpreted function application
loc.c t1 t2 t3 x y z it should somehow do the right thing, in  
taking it as (loc.c t1 t2 t3) x y z, and considering the inner  
part as atomic entity (and instance of c defined earlier in the  
abstract context).



On our running gag list with have at least these related issues:

  * codgeneration as sketched above

  * behaviour of the Simplifier on seemingly atomic constants c (due
to abbreviations) that are actually of the form loc.c x y z

  * stability and expectedness of abbreviations, as they are printed

  * the Haftmann/Wenzel educated guess here
 
http://isabelle.in.tum.de/repos/isabelle/file/38af9102ee75/src/Pure/Isar/named_target.ML#l56

which can be traced back here:
http://isabelle.in.tum.de/repos/isabelle/rev/9dd61cb753ae
(Fall/Winter 2007 was the time where we desparately tried to recover
from the 2006/2007 gap in the Isabelle release chain).


Is there any nice, sane, simple approach to all that?


My impression it that this would address the first two points; I don't  
have enough insight to judge the others.


Some months ago I mentally experimented with a notion of explicit  
boundaries for locale contexts and somehow follow the structure of  
interpretations.


I'm not sure, but what you describe seems more elaborate than what I  
sketched above.


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

Re: [isabelle-dev] Order of sublocale declarations

[Clemens Ballarin]

Hi Andreas,

The failure happens while reading the locale expression, which is a  
sequence of locale instances:


  A s + B t + C u + ...

When reading the locale expression, we aim at achieving two conflicting goals:
- Type inference over the entire expression
- Syntax declarations of an instance are available when parsing the  
next instance.  That is, syntax from A s is available in t, and so on.


This is achieved by incrementally interleaved phases of parsing, type  
inference and declaration activation.  I suspect that when processing  
the example, there is a point where the equality of the definitions  
has not yet been established, and this is why the example fails.


I tend to always use qualifiers, which helps avoid the problem.

Clemens


Quoting Andreas Lochbihler andreas.lochbih...@inf.ethz.ch:


Hi Amine,

let's look at what happens:

A defines the constant local.fpower as A.fpower f
AB inherits it from A, i.e., we have local.fpower == A.fpower f (1)
B  A d g produces local.fpower == A.fpower (d g)
AB  B d f inherits this as local.fpower == A.fpower (d (d f)) (2)

As the locale infrastructure does not know about d (d f) = f, it  
considers two different declarations of local.fpower from (1) and  
(2) as not being the same and therefore tries to declare both of  
them - which the local context infrastructure rejects.


You can either use prefixes to disambiguate local.fpower like in  
sublocale AB  b!: B d f

This gives you (1) and local.b.fpower == A.fpower (d (d f)).
Or, tell the locale infrastructure to rewrite d (d f) = f:

sublocale AB  B d f where d (d f) == f

The second approach only works if you order the sublocale  
declarations like in your second case. I do not know why, but I  
believe it has technical reasons; Clemens might be able to tell you  
more.


Andreas

On 01/31/2013 02:56 PM, Amine Chaieb wrote:

Thanks Andreas. Does this mean that this sublocale scenario is
prohibited? And if so, is it due to technical reasons or is there a
fundamental problem here?

Amine.

On 01/31/2013 02:04 PM, Andreas Lochbihler wrote:

Hi Amine,

the error message in the second case is only delayed: You get it, once
you open the AB context again (context AB begin). In the first case,
it shows up immediately, because the sublocale command already
constructs the context AB enriched with B.

Best,
Andreas



___
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] Automated testing questions

[Clemens Ballarin]

Dear Developers,

What it the current best practice for testing my change to Isabelle?   
There used to be testboard, but I'm unsure how that evolved.  Is there  
a similar service for testing my change to Isabelle against the AFP?


Also, which server should I use for pushing my changes to Isabelle so  
as to avoid repository trouble?


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

Re: [isabelle-dev] Interpretation in arbitrary targets.

[Clemens Ballarin]

Hi Florian,

I'm in favour of generalising interpretation to targets, but in my  
opinion it would not be right to provide the sublocale command as the  
interpretation command in a locale context.  There are two reasons:


1. sublocale modifies the locale graph of the underlying theory.  This  
is a big change and shouldn't happen as a side effect of a command in  
a target context.


2. sublocale and interpretation are more different than it looks:  
interpretation provides inheritance of mixins (or, from the user  
perspective, rewrite morphisms) and it is possible to amend mixins in  
interpretation (currently only through the API).


On the other hand, I see that interpretation in a locale context can  
help working in an incremental fashion in such a context (which I  
assume is the motivation for your patches).


So, what should interpretation in a locale be like?  Currently,  
sublocale is used for two purposes:


a) relating two locales to each other (such as a total order is a lattice)

b) import (a typically small number of) lemmas, which are needed for  
establishing some result, from one locale A into another locale B


While sublocale is perfect for a), in b) there is a big overhead  
caused by importing all theorems from A into B whenever B is  
activated, while all that's needed is importing theorems from A to B  
once.  The latter is what we should try to address by a variant of the  
interpretation command for locale contexts.  Here's my proposal:


context B begin
  ...
  interpretation A
  ...
end

makes the interpretation of A available in the block up to the closing  
'end'.  The interpretation will not be persisted; results are only  
available temporarily to aid establishing some results in B.  Of  
course, this would mean that the literal command


interpretation (in B) A

is useless, but that wouldn't hurt.  On the other hand, if users  
started to use this feature, locale hierarchies could become less  
complex and, as a consequence, theories faster (well, become slower  
more slowly...).  When interpreting a hierarchy A - A' - A''  
incrementally, the pattern would be


context B begin
  interpretation A
  interpretation A'
  interpretation A''
end
sublocale B  A''

that is, one additional sublocale declaration would be sufficient to  
persist the incremental development.


What do you think of these ideas?  I would appreciate, if you could  
work towards them (I myself never quite mastered the intricacies of  
the ML level target code).


Clemens


Quoting Florian Haftmann florian.haftm...@informatik.tu-muenchen.de:


There is a series of minimal invasive patches to generalize
»interpretation« / »sublocale« to »interpretation« in arbitrary targets,
not just theories and locales. The patches are inspectible at

http://isabelle.in.tum.de/~haftmann/cgi-bin/repos/interpretation

Explanations follow. It is good tradition not to muddle with the module
system code arbitrarily, therefore this rather unconventional approach
to gain feedback.

1.
http://isabelle.in.tum.de/~haftmann/cgi-bin/repos/interpretation/rev/21821401c5a5
Identity juggling to prepare following steps.

2.
http://isabelle.in.tum.de/~haftmann/cgi-bin/repos/interpretation/rev/aee4c6577ff7

Ironing out a FIXME in the code. This already gives a hint how the
existing code base naturally converges to unify »interpretation« and
»sublocale«.

3.
http://isabelle.in.tum.de/~haftmann/cgi-bin/repos/interpretation/rev/f6bc704b5cd6

In order to let »interpretation« and »sublocale« converge, the close
marriage of »interpretation« and »interpret« must be given up. This is a
step back only in the first instance ? it would still be possible to
factor out common code of the resulting unified »interpretation« and
»interpret« in a separate step afterwards. In the same breath the
(operationally void!) switch from »ctxt« to »lthy« yields the key clue
of the whole story.

4.
http://isabelle.in.tum.de/~haftmann/cgi-bin/repos/interpretation/rev/9d5c8a5251d5

This establishes sharing of »interpretation« and »sublocale« as far as
appropriate.

5.
http://isabelle.in.tum.de/~haftmann/cgi-bin/repos/interpretation/rev/1d3a62ef74dd

Identity juggling to prepare following steps.

6.
http://isabelle.in.tum.de/~haftmann/cgi-bin/repos/interpretation/rev/dd6dd81381fb

This is the key step: »subscription« as target operation to make
»interpretation« work regardless of the underlying target.
The »potential_reinit« is a wart: when interpreting locales into
locales, the new facts must be provided in the local theory context of
this locale also, and I have up after a few experiments with
Locale.activate_facts etc. Note the same situation has been occuring in
»subclass« for years now. Here it is more critical since interpretation
should be fully target-ignorant (unlike subclass which always knows that
it operates on classes). However I have let it stand for the moment as a
conceptual preview. I'm 

Re: [isabelle-dev] Interpretation in arbitrary targets.

[Clemens Ballarin]

Quoting Florian Haftmann florian.haftm...@informatik.tu-muenchen.de:


Let those thoughts sink further few days.  If there is no veto until Apr
7th, I would go ahead to turn the patches upstream.


Well, here is my veto.

I don't see that much of a discussion has taken place yet, and I am  
very unhappy about the concepts and terminology you are trying to  
introduce.  As you are aware, I do have another job, which makes  
responding as quickly as you would like impossible.  I do hope,  
though, that we can get this discussion further within this month.


Clemens

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

Re: [isabelle-dev] Interpretation in arbitrary targets.

[Clemens Ballarin]

Quoting Florian Haftmann florian.haftm...@informatik.tu-muenchen.de:


Let those thoughts sink further few days.  If there is no veto until Apr
7th, I would go ahead to turn the patches upstream.


You have proposed a change about which doubts were raised.  I don't  
consider it acceptable to then announce a deadline after which you  
will go ahead and push.  People simply may not be able to respond in  
time, especially in a vacation period.


Regarding interpretation vs sublocale

We are talking about user interface design, and this means choosing  
appropriate metaphors for what certain commands do.  People familiar  
with the history of locales may remember that the precursor of the  
sublocale command was


  interpretation l  e

before I changed that to sublocale in the reimplementation.  This  
change was motivated by the realisation that interpretation between  
locales essentially means changing the module hierarchy.  This is a  
remarkable feature for a module system, which deserves emphasis and  
isn't really appropriately described by 'interpretation'.  In  
contrast, interpretation in theories just interprets locales in  
theories (even though with subscription), there is no additional  
value.


From this perspective (which is the perspective of the designer!) it  
seems wrong to put interpretation in locales and theories in one  
category, and local interpretation (as it might be called) in locale  
contexts and in proof contexts in the other.  Even, if this made some  
aspects of the implementation more elegant.  Let me note that, of  
course, the user interface design should not make the implementation  
unnecessarily complicated (but I believe we are far away from that).


In this light, if a version of the sublocale command seems necessary  
in context blocks, why no call it 'sublocale'?  Of course, the global  
version should remain


  sublocale l  e.

It should not be turned into

  sublocale (in l) e

because the former much more clearly indicates the change to the  
locale hierarchy.  This design has the additional benefits that users  
don't need to change existing proof documents, terminology in the  
literature remains up to date, and, most importantly, the sublocale  
command is clearly recognisable in context blocks.


There were two more aspects in the recent discussion.  I will pick  
them up in separate e-mails since this has got too long already.


Clemens

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

Re: [isabelle-dev] Local interpretation [was Interpretation in arbitrary targets.]

[Clemens Ballarin]

Quoting Florian Haftmann florian.haftm...@informatik.tu-muenchen.de:


context B begin
  context
  begin
interpretation A
  end
end


This looks attractive, but could you please elaborate the semantics:
- What would be the effect of the interpretation from the inner block  
on the outer block?

- What would be the effect of the entire sequence on B?

Clemens

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

Re: [isabelle-dev] Private modifier and qualifiers [was Interpretation in arbitrary targets.]

[Clemens Ballarin]

Quoting Makarius makar...@sketis.net:


On Tue, 26 Mar 2013, Florian Haftmann wrote:

Note that we have one more aspect in the back-end that could help  
here: the 'private' modifier.


What would the 'private' modifier do in general?  This sounds like a  
new concept.


The following may or may not be related: I recently spent some thought  
on getting rid of the mandatory vs optional distinction of qualifiers.  
 In any case this will likely have considerable impact, so here's the  
idea:


Currently there is the strange feature that abbreviations are only  
unfolded under morphisms that are the identity on term parameters.   
From what I see on the mailing lists this has confused users.   
Instead, I would propose to change the criterion to that abbreviations  
are only unfolded under morphisms that do not change the name part  
(i.e. without qualification).  This would mean that for an unqualified  
instance syntax remained available while for a qualified instance  
syntax redeclaration would be necessary.


This would, of course, require some experimentation, but for now I  
just would like to learn whether the 'private' modifier would be  
related and should be taken into consideration.


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

Re: [isabelle-dev] Interpretation in arbitrary targets.

[Clemens Ballarin]

Hi Florian,


I do not object to your suggestion, and it is clearly in reach within
the current code base.  But... it is a different thing.  Your suggestion
is to make sublocale work in locale targets seamlessly.  But something like

instantiation ...
begin

sublocale ...

instance ...

end

then just does not make sense: either it is not covered (or blocked) by
the implementation, or »sublocale« is just the wrong wording since it
assumes locales on both producer and consumer side so to speak.


I don't know what interpretation (or sublocale) would mean in an  
instantiation context, so I cannot tell what would be more  
appropriate.  It seems natural though, that, if additional commands  
are to be 'targetized', some commands will not be meaningful in some  
kinds of targets.  So, if sublocale were only available in locale  
targets, I wouldn't consider that a problem.  (If sublocale
were not available in locale targets, I wouldn't consider that a  
problem either, but that's not the the point of this discussion.)


In any case, it would make sense to discuss what a command would mean  
in all of the targets (and where it is not meaningful) before making  
it available in some targets.



You might ask at first what interpretation in instantiation blocks is
supposed to be.  I think it can be a neat pattern to approach
instantiation by default definitions; here the interpretation would
provide that OFCLASS theorem to prove the claimed instance relationship
finally or something alike.


I'm unsure whether I understand this fully.  But to me it looks like  
the purpose of the instantiation target is to declare instance  
relations between classes.  If that is the case, then there is no  
further need to stress the 'subscriptive' nature and it might be  
legitimate to just call the command 'interpretation'.  But, of course,  
it depends on what the command would actually do.  I guess this would  
replace some existing command that already exists.


This is different if the target is a locale.  The purpose of a locale  
target is to work in a locale, not add relations between locales.  We  
don't have a sublocale target, whose purpose could be to establish  
interpretation relations between locales.  Instead there is just the  
sublocale command, which is fairly primitive.  The mechanisms offered  
by the instantiation target, which lets one make the necessary  
constructions needed for the instantiation in a clean way, are much  
more elaborate.



Two asides:


Of course, the global

version should remain

  sublocale l  e.

It should not be turned into

  sublocale (in l) e


foo (in l) ...

is equivalent to

context l
begin

foo ...

end

by construction.  We cannot have just one of them.


That sounds a bit dogmatic.  If additional commands are made available  
for targets, then the syntax should clearly be more flexible if better  
intuition can be achieved.



It is also notable that we have definitions in locales (although this is
far beneath your great achievements with sublocale etc.).  With them it
is the case that we provide them *uniformly* for theories, locales and
other targets (something which has been commented as seemingly trivial,
»but maybe this is the achievement.« ).


I strongly believe that definitions in locales are a great  
achievement.  Without them all the other work would not have been  
worth it.  I hope, though, it has become clear that I'm not opposed to  
having interpretation in locale contexts by principle, I'm merely  
opposed to explaining them in the way you propose.


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

Re: [isabelle-dev] Interpretation in arbitrary targets.

[Clemens Ballarin]

Hi Florian,


I still see us disagree on how far the local theory game can be driven
wrt. interpretation, nevertheless I can imagine that there is an
intermediate road map which we can agree on:

* Extend sublocale for use within locale targets s.t.


This is fine with me.  Will this work for named targets including  
classes or just locales?



Rationale: We have 30 occurences of sublocale in HOL/*.thy and 80%   and
more occur with the pattern


That's not very much.  In any case, in future, I would prefer a  
discussion starting from the problem towards a solution, not from a  
solution to the actual problem.



* Equip interpretation in non-theory targets to allow confined,
non-persistent interpretations.

  context B
  begin

  interpretation EXPR

  end

  would not add a dependency to B.


Here, it's not clear whether the interpretation just wouldn't add a  
dependency, or wouldn't modify B at all.


Please clarify.

Clemens

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

Re: [isabelle-dev] Interpretation in arbitrary targets.

[Clemens Ballarin]

Quoting Makarius makar...@sketis.net:


On Fri, 12 Apr 2013, Clemens Ballarin wrote:

That sounds a bit dogmatic.  If additional commands are made  
available for targets, then the syntax should clearly be more  
flexible if better intuition can be achieved.


That is just a matter of modularity of concepts: the older (in a)  
notation was slightly generalized at some point to allow named  
contexts as sketched above, and the relation between the two is as  
pointed out by Florian.


I am aware of the modularity aspect of this.  My criticism is that  
deviations from the current approach in favour of preferable notation  
are not even considered.  In any case, I'm not sure how useful the old  
notation still is.  Maybe it can be given up at some point.


Clemens

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

Re: [isabelle-dev] Interpretation in arbitrary targets.

[Clemens Ballarin]

Hi Florian,

OK, then we agree on this.

Please let me know if you need to make changes to locales.ML.  I want  
to make sure that routes out of certain quirks there don't get blocked  
accidentally.


Clemens


Quoting Florian Haftmann florian.haftm...@informatik.tu-muenchen.de:


Hi Clemens,


I still see us disagree on how far the local theory game can be driven
wrt. interpretation, nevertheless I can imagine that there is an
intermediate road map which we can agree on:

* Extend sublocale for use within locale targets s.t.


This is fine with me.  Will this work for named targets including
classes or just locales?


it will work within locales, and thus within type classes.


* Equip interpretation in non-theory targets to allow confined,
non-persistent interpretations.

  context B
  begin

  interpretation EXPR

  end

  would not add a dependency to B.


Here, it's not clear whether the interpretation just wouldn't add a
dependency, or wouldn't modify B at all.


It should not modify B at all -- with the restriction that ad-hoc
contexts currently may leak nontheless in certain situations (cf.
Makarius' statement).

Florian

--

PGP available:
http://home.informatik.tu-muenchen.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] Interpretation in arbitrary targets.

[Clemens Ballarin]

This view is correct, but it is not the whole story.  Since the system  
maintains a graph of interpretations and follows them transitively,  
the effect achieved by


  sublocale locale  expression

is much like

  instance class  sort

of the old user interface to type classes.  This relationship is  
discussed in the new paper (Section 5.2).


Clemens


Quoting Tobias Nipkow nip...@in.tum.de:


Let me just make some remarks as a user. At ITP 2011 I published a paper
http://www21.in.tum.de/~nipkow/pubs/itp11.html where I showed how to  
use locales

to structure stepwise development of modules (see p11). In that context I
intentionally used the notation

interpretation (in A) B-expr

instead of sublocale in an implementation step. Of course I comment on the
deviation in the notation saying that I have chosen this variation of
interpretation because it is more intuitive (see p10). I do find it more
intuitive because it tells me clearly what is going on: some locale  
expression

is interpreted in some locale. And this is also how you explain sublocale in
your locale tutorial. Hence Florian's suggestions made a lot of sense to me.

Tobias


Am 17/04/2013 22:28, schrieb Clemens Ballarin:

Quoting Makarius makar...@sketis.net:


On Fri, 12 Apr 2013, Clemens Ballarin wrote:


That sounds a bit dogmatic.  If additional commands are made available for
targets, then the syntax should clearly be more flexible if  
better intuition

can be achieved.


That is just a matter of modularity of concepts: the older (in  
a) notation

was slightly generalized at some point to allow named contexts as sketched
above, and the relation between the two is as pointed out by Florian.


I am aware of the modularity aspect of this.  My criticism is that  
deviations

from the current approach in favour of preferable notation are not even
considered.  In any case, I'm not sure how useful the old notation still is.
Maybe it can be given up at some point.

Clemens

___
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 mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Interpretation in arbitrary targets.

[Clemens Ballarin]

Quoting Makarius makar...@sketis.net:


Does it mean you propose to discontinue (in a) at some point?


Exactly.  Too early right now, but eventually this might make sense --  
especially if the IDE provides suitable refactorings.  Of course, this  
wouldn't let us scrap a lot of code, but the Isar language could  
become cleaner.


Clemens

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

Re: [isabelle-dev] Interpretation in arbitrary targets.

[Clemens Ballarin]

Quoting Lars Noschinski nosch...@in.tum.de:

How is interpretation related to print_context? It seems that  
neither interpret nor interpretation extends the context as  
displayed by print_context?


I don't know the answer to that, but for a particular locale x you  
should be able to find all active interpretations in a context by


  print_interps x

Clemens

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

[isabelle-dev] Isar syntax regression

[Clemens Ballarin]

I wonder whether

  then interpret Min!: semilattice_order_set min less_eq less.

(without a space before the dot) is now intended Isar syntax.  I found  
this in src/HOL/Big_Operators.thy, so I guess this is accepted in  
batch mode.  PG doesn't accept it, but apparently JEdit does.


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

Re: [isabelle-dev] Shadowing of theorem names in locales

[Clemens Ballarin]

I recently tried to make HOL-Algebra compliant to this, but  
unfortunately got stuck in HOL already, where Big_Operators didn't  
comply either (but that's unlikely the only theory).


If we are serious about forbidding duplicate theorem names eventually  
we probably need to start by introducing a flag to enable/disable  
this, so that it doesn't get introduced by accident to theories where  
duplicate names had already been eliminated.  As other have noted  
before, this is not going to be a one-man effort.  It is quite a bit  
of work, but more importantly, it involves design decisions (namely  
whether to rename theorems or introduce qualifiers) which is best done  
by a theory's author.


Clemens


Quoting Makarius makar...@sketis.net:


On Tue, 9 Oct 2012, Makarius wrote:


On Sun, 7 Oct 2012, Florian Haftmann wrote:


After some pondering I would argue that this should be forbidden:
* (Complete) shadowing is a constant source of confusion.
* Global interpretations are impossible then, since they would result in
two global theorems with the same name.


I've started some experiments with this idea and will report the  
empirical results soon ...


After some detours I am now back on Isabelle/28e37eab4e6f.

In principle, the last big reform of locale + interpretation name  
space prefixes has addressed the situation already, where each  
locale scope is locally strict, but composing several of them in  
locale expressions etc. works by mandatory or non-mandatory prefixes.


Actual strictness checking is part of the underlying name space  
policy, when bindings are applied and react with some naming. The  
local context of the locale construction is particularly important  
here.  It was merely a historical left-over that fact bindings were  
not checked strictly:


  (1) in distant past facts were never strict and totally un-authentic

  (2) the Isar proof body mode allows to override 'notes' as it does for
  'fixes'.

So with the ch-strict changeset applied to the critical spot of  
local notes, the namespace policy enforces the concentual locale  
scopes.


Applying this in practice leads to many surprises about situations  
found in existing theory libraries, though.  Some of the changsets  
leading up to Isabelle/28e37eab4e6f already sort this out.  Some  
other ad-hoc changes are attached as ch-test here.



With Isabelle/28e37eab4e6f + ch-strict + ch-test and AFP/77f79b2076f1
the following sessions fail:

BDD, Dijkstra_Shortest_Path, Free-Groups, Group-Ring-Module,  
HOL-Algebra, HOL-Number_Theory, HOL-ex, JinjaThreads, KBPs,  
Markov_Models, Ordinal, Ordinary_Differential_Equations,  
Pi_Calculus, Presburger-Automata, PseudoHoops, Psi_Calculi,  
Refine_Monadic, Simpl, Slicing, Topology, Transitive-Closure-II,  
Valuation


So the question if ch-strict can be activated soon is mainly a  
matter of library space.  It is up to emerging volunteers to sort it  
out further.


(For me it was interesting to see how Isabell/jEdit works on the  
JinjaThreads monster session.  See also AFP/77f79b2076f1 of the  
result of investing 3GB for poly, 4GB for java, and quite a bit of  
CPU time and elapsed time.)



Makarius




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

Re: [isabelle-dev] Shadowing of theorem names in locales

[Clemens Ballarin]

Quoting Florian Haftmann florian.haftm...@informatik.tu-muenchen.de:


If you point we to particular
occurences, I am willing to polish them accordingly.


There are several versions of bounded_iff in the locales of that  
theory (and lattice locales from imported theories).  To find all  
problematic theorems, you probably want to apply Makarius' ch-strict  
patch.  I attach this and the other one from his original message.   
The second patch no longer applies, though.


Clemens


# HG changeset patch
# User wenzelm
# Date 1349877701 -7200
# Node ID f1455859ff039bb15cb2ff451cc2eb91cb14116b
# Parent  28e37eab4e6fa7065d872ae8fcc5978a93ea0845
strict namespace policy for local facts, in correspondance with local terms 
(cf. Variable.is_body);

diff -r 28e37eab4e6f -r f1455859ff03 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.MLWed Oct 10 15:39:01 2012 +0200
+++ b/src/Pure/Isar/proof_context.MLWed Oct 10 16:01:41 2012 +0200
@@ -952,7 +952,8 @@
 val (res, ctxt') = fold_map app facts ctxt;
 val thms = Global_Theory.name_thms false false name (flat res);
 val Mode {stmt, ...} = get_mode ctxt;
-  in ((name, thms), ctxt' | update_thms {strict = false, index = stmt} (b, 
SOME thms)) end);
+val strict = not (Variable.is_body ctxt);
+  in ((name, thms), ctxt' | update_thms {strict = strict, index = stmt} (b, 
SOME thms)) end);
 
 fun put_thms index thms ctxt = ctxt
   | map_naming (K Name_Space.local_naming)
# HG changeset patch
# User wenzelm
# Date 1349877725 -7200
# Node ID 9e0ea0b5bab5f5c7de77f135a21d76f763d22c47
# Parent  f1455859ff039bb15cb2ff451cc2eb91cb14116b
some attempts to accomodate strict facts;

diff -r f1455859ff03 -r 9e0ea0b5bab5 src/HOL/IMP/Abs_Int_Den/Abs_Int_den2.thy
--- a/src/HOL/IMP/Abs_Int_Den/Abs_Int_den2.thy  Wed Oct 10 16:01:41 2012 +0200
+++ b/src/HOL/IMP/Abs_Int_Den/Abs_Int_den2.thy  Wed Oct 10 16:02:05 2012 +0200
@@ -74,7 +74,7 @@
 iter' m n f x =
   (let f' = (\lambday. x \squnion f y) in iter_down f' n (iter_up f' m x))
 
-lemma iter'_pfp_above:
+lemma WN_iter'_pfp_above:
 shows f(iter' m n f x0) \sqsubseteq iter' m n f x0
 and x0 \sqsubseteq iter' m n f x0
 using iter_up_pfp[of \lambdax. x0 \squnion f x] iter_down_pfp[of 
\lambdax. x0 \squnion f x]
@@ -198,7 +198,7 @@
 and bfilter_ivl' is bfilter
 and AI_ivl' is AI
 and aval_ivl' is aval'
-proof qed (auto simp: iter'_pfp_above)
+proof qed (auto simp: WN_iter'_pfp_above)
 
 value [code] list_up(AI_ivl' test3_ivl Top)
 value [code] list_up(AI_ivl' test4_ivl Top)
diff -r f1455859ff03 -r 9e0ea0b5bab5 src/HOL/Library/Code_Integer.thy
--- a/src/HOL/Library/Code_Integer.thy  Wed Oct 10 16:01:41 2012 +0200
+++ b/src/HOL/Library/Code_Integer.thy  Wed Oct 10 16:02:05 2012 +0200
@@ -31,7 +31,7 @@
   done
 qed
 
-lemma (in ring_1) of_int_code:
+lemma (in ring_1) of_int_code':
   of_int k = (if k = 0 then 0
  else if k  0 then - of_int (- k)
  else let
@@ -45,7 +45,7 @@
   of_int_add [symmetric]) (simp add: * mult_commute)
 qed
 
-declare of_int_code [code]
+declare of_int_code' [code]
 
 text {*
   HOL numeral expressions are mapped to integer literals
diff -r f1455859ff03 -r 9e0ea0b5bab5 src/HOL/Library/Target_Numeral.thy
--- a/src/HOL/Library/Target_Numeral.thyWed Oct 10 16:01:41 2012 +0200
+++ b/src/HOL/Library/Target_Numeral.thyWed Oct 10 16:02:05 2012 +0200
@@ -605,7 +605,7 @@
   k  l \longleftrightarrow (of_int k :: Target_Numeral.int)  of_int l
   by (simp add: less_int_def)
 
-lemma (in ring_1) of_int_code:
+lemma (in ring_1) of_int_code':
   of_int k = (if k = 0 then 0
  else if k  0 then - of_int (- k)
  else let
@@ -619,7 +619,7 @@
   of_int_add [symmetric]) (simp add: * mult_commute)
 qed
 
-declare of_int_code [code]
+declare of_int_code' [code]
 
 
 subsection {* Implementation for @{typ nat} *}
@@ -707,7 +707,7 @@
   num_of_nat = Target_Numeral.num_of_int \circ of_nat
   by (simp add: fun_eq_iff num_of_int_def of_nat_def)
 
-lemma (in semiring_1) of_nat_code:
+lemma (in semiring_1) of_nat_code':
   of_nat n = (if n = 0 then 0
  else let
(m, q) = divmod_nat n 2;
@@ -721,7 +721,7 @@
   (simp add: * mult_commute of_nat_mult add_commute)
 qed
 
-declare of_nat_code [code]
+declare of_nat_code' [code]
 
 text {* Conversions between @{typ nat} and @{typ int} *}
 
diff -r f1455859ff03 -r 9e0ea0b5bab5 
src/HOL/Probability/Finite_Product_Measure.thy
--- a/src/HOL/Probability/Finite_Product_Measure.thyWed Oct 10 16:01:41 
2012 +0200
+++ b/src/HOL/Probability/Finite_Product_Measure.thyWed Oct 10 16:02:05 
2012 +0200
@@ -696,7 +696,7 @@
   qed
 qed
 
-sublocale finite_product_sigma_finite \subseteq sigma_finite_measure 
Pi\^isubM I M
+sublocale finite_product_sigma_finite \subseteq Pi: sigma_finite_measure 
Pi\^isubM I M
   using sigma_finite[OF finite_index] .
 
 lemma (in finite_product_sigma_finite) measure_times:
diff -r f1455859ff03 -r 9e0ea0b5bab5 src/HOL/Probability/Probability_Measure.thy
--- 

[isabelle-dev] isabelle jedit -l HOL fails

[Clemens Ballarin]

After updating the repository today (and a seemingly good run of  
'isabelle components -a') 'isabelle jedit -l HOL' gives me


2013-10-01 20:42:22.345 java[35294:903] *** NSInvocation: warning:  
object 0x10ad24390 of class 'ThreadUtilities' does not implement  
methodSignatureForSelector: -- trouble ahead
2013-10-01 20:42:22.348 java[35294:903] *** NSInvocation: warning:  
object 0x10ad24390 of class 'ThreadUtilities' does not implement  
doesNotRecognizeSelector: -- abort
/Users/ballarin/isabelle/repo/lib/Tools/java: line 1: 35294 Trace/BPT  
trap  $ISABELLE_JDK_HOME/bin/$PRG $@


I'm still on MacOSX 10.6.8 Snow Leopard.  Any ideas?

Clemens

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

Re: [isabelle-dev] Shadowing of theorem names in locales

[Clemens Ballarin]

On 28 December, 2013 19:53 CET, Florian Haftmann 
florian.haftm...@informatik.tu-muenchen.de wrote: 
 
 HOL-Complex now builds with strict naming policy for facts (again).

Thanks, that's cool.

 I have stumbled over something which needs some consideration: with
 strict naming policy, locales can be compromised by »injecting«
 duplicate facts to imported locales.

That's not cool, but I would say that is a user error.  There are other ways of 
compromising locales, for example with the sublocale command.

 This does not exhibit itself until
 the compromised locale context is (re-)entered, and I think this is not
 desirable.  My first spontaneous thought is that strictness should not
 apply during the initialisation of a locale context.

I wouldn't want to add special treatment for this.  Currently we can only 
ensure that a locale is intact by visiting its context.  It would be better if 
integrity checking could be done in an incremental fashion.  But that would 
require much more sophistication.

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

Re: [isabelle-dev] Shadowing of theorem names in locales

[Clemens Ballarin]

For the processing of locale expression, facts are not really required.  Having 
all information related to syntax should be sufficient.  I cannot tell, though, 
whether facts may contain syntax in disguise of certain attributes.

Clemens


On 10 February, 2014 16:14 CET, Makarius makar...@sketis.net wrote: 
 
 On Fri, 10 Jan 2014, Clemens Ballarin wrote:
 
  This does not exhibit itself until the compromised locale context is 
  (re-)entered, and I think this is not desirable.  My first spontaneous 
  thought is that strictness should not apply during the initialisation 
  of a locale context.
 
  I wouldn't want to add special treatment for this.  Currently we can 
  only ensure that a locale is intact by visiting its context.  It would 
  be better if integrity checking could be done in an incremental fashion. 
  But that would require much more sophistication.
 
 There is a more general problem behind this: re-initializing a locale 
 context is quite expensive, but we traditionally do this at certain 
 important checkpoints when processing locale expressions.  For example, in 
 AFP/JinjaThreads the time for defining some huge locales is dominated by 
 that re-init phase for the imports, and later only few facts are actually 
 required.
 
 Several minutes (hours?) could probably be saved by maintaining facts 
 within the context in a lazy manner: the name space is strict, but its 
 values are only produced on demand.  I have no clear idea, though, how 
 that would impact practical realiablity of locale expressions.
 
 Or is that actually an answer to the problem above: assuming that re-init 
 is fast, it could be done more often to check the name space, but its 
 transformed results remain unchecked.
 
 
   Makarius
 
 
 
 

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

Re: [isabelle-dev] Shadowing of theorem names in locales

[Clemens Ballarin]

 On 21 March, 2014 17:26 CET, Makarius makar...@sketis.net wrote: 
 
 On Tue, 11 Feb 2014, Clemens Ballarin wrote:
 
  For the processing of locale expression, facts are not really required. 
  Having all information related to syntax should be sufficient.  I cannot 
  tell, though, whether facts may contain syntax in disguise of certain 
  attributes.
 
 In principle there could be arbitrary declarations disguised as 
 declaration attributes of facts, but the general sanity assumption is that 
 this is not done.  The separate concept of syntax_declaration was 
 introduced for that, when we sorted this out several years ago.

To be more precise about what I had said above: I actually believe that syntax 
is only required when parsing a locale (i.e. reading it for the first time).  
When activating it later, everything should be set, and the syntax should no 
longer matter.

Clemens
 

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

[isabelle-dev] Isabelle/jedit reports that file was changed on disk

[Clemens Ballarin]

I occasionally get a modal dialog reporting that a the file I currently edit 
was changed on disk by another program and therefore automatically reloaded.  I 
didn't touch or modify the program myself, and ls -l does not indicate a recent 
modification either.

This is for a fairly recent repository build (7da3e398804c) with all components 
as requested by this configuration.

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

Re: [isabelle-dev] Problem with type inference in locale expressions

[Clemens Ballarin]

Is this a regression in the type inference of locale expressions, or has it 
always (i.e. since 2009) been like this?

Clemens

 
On 04 September, 2014 09:21 CEST, Florian Haftmann 
florian.haftm...@informatik.tu-muenchen.de wrote: 
 
 At d6a2e3567f95, I am currently analysing a problem with type inference
 in locale expressions: when leaving types implicit, imported parameters
 are given disjoint types despite they could be unified, and are so if
 given explicit type annotations.  The problem occurs if the imported
 locales themselves have dependencies on other locales containing a
 definition.
 
 The reason why this is really annyoing is that it breaks certain class
 specifications to typecheck and currently effectively prevents me from
 adding such a simple thing as product over lists.
 
 See attached theory for quite minimal examples.
 
 I will have to investigate this further.
 
   Florian
 
 -- 
 
 PGP available:
 http://home.informatik.tu-muenchen.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] Problem with type inference in locale expressions

[Clemens Ballarin]

This is what I expected.  Type inference of locale expressions is inherently 
heuristic and probably you are hitting this.  (This could be verified further 
with a stack trace).  For more background, see also this earlier message: 
https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/2013-February/003821.html

Clemens


On 05 September, 2014 20:12 CEST, Florian Haftmann 
florian.haftm...@informatik.tu-muenchen.de wrote: 
 
  Is this a regression in the type inference of locale expressions, or has it 
  always (i.e. since 2009) been like this?
 
 Using the attached retrofitted theory, the same behaviour occurs:
 
  $ /opt/Isabelle2009/Isabelle2009/bin/isabelle tty
  val it = () : unit
  val commit = fn : unit - bool
  Welcome to Isabelle/HOL (Isabelle2009: April 2009)
  theory Foo imports Class_Clash begin
  Loading theory Class_Clash
  parameters
f :: 'a = 'a = 'a
  constants
F :: 'a = 'a = 'a
  parameters
f :: 'a = 'a = 'a
  constants
F :: 'a = 'a = 'a
  plus
:: 'a = 'a = 'a
  inf
:: 'b = 'b = 'b
  plus
:: 'a = 'a = 'a
  inf
:: 'a = 'a = 'a
  plus
:: 'a = 'a = 'a
  inf
:: 'a = 'a = 'a
  *** Type unification failed
  *** Type error in application: Incompatible operand type
  *** 
  *** Operator:  op = inf :: ('b = 'b = 'b) = bool
  *** Operand:   plus :: 'a = 'a = 'a
  *** 
  *** At command locale (line 64 of /data/tum/drawer/thy/Class_Clash.thy).
  Error - Database is not opened for writing.
  val it = () : unit
 
 There is strong evidence that it has always been like this.
 
 Shall I just chance my luck and dive into the sources?
 
 Cheers,
   Florian
 
 
   
  On 04 September, 2014 09:21 CEST, Florian Haftmann 
  florian.haftm...@informatik.tu-muenchen.de wrote: 
   
  At d6a2e3567f95, I am currently analysing a problem with type inference
  in locale expressions: when leaving types implicit, imported parameters
  are given disjoint types despite they could be unified, and are so if
  given explicit type annotations.  The problem occurs if the imported
  locales themselves have dependencies on other locales containing a
  definition.
 
  The reason why this is really annyoing is that it breaks certain class 
  specifications to typecheck and currently effectively prevents me from 
  adding such a simple thing as product over lists.
 
  See attached theory for quite minimal examples.
 
  I will have to investigate this further.
 
 Florian
 
  -- 
 
  PGP available:
  http://home.informatik.tu-muenchen.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
  
 
 -- 
 
 PGP available:
 http://home.informatik.tu-muenchen.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

[isabelle-dev] Regression in the sublocale command

[Clemens Ballarin]

Hi Florian,

I'm investigating a regression which prevents identifying certain equivalent 
locales through circular sublocale declarations:

  sublocale loc1  x: loc2 A c (* sigma_1 *)
where x.b == B and x.d == e (* tau_1 *)
  sorry

  sublocale loc2  x: loc1 A b (* sigma_2 *)
where x.c == C and x.e == d (* tau_2 *)
  sorry (* loops from changeset 8fab871a2a6f *)

The last sorry loops, which is unfortunate, because it forces certain 
workarounds on my current project.  In a fairly lengthy debug session I figured 
out that it is the simplifier that loops.  This is an indication that the 
morphisms tau_1 and tau_2 are applied simultaneously, which they should not.  
In any case, the behaviour appears to have been introduced quite a while ago in 
8fab871a2a6f, which is in the first batch of your changes to the locale 
interpretation commands.

Clemens

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

Re: [isabelle-dev] Regression in the sublocale command

[Clemens Ballarin]

My conclusion of this discussion is that with 8fab871a2a6f the sublocale 
command immediately visits its target after the qed, which it didn't before.  
This now causes the command to loop.  Is this correct?

Clemens


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

Re: [isabelle-dev] Regression in the sublocale command

[Clemens Ballarin]

On 14 February, 2015 10:11 CET, Florian Haftmann 
florian.haftm...@informatik.tu-muenchen.de wrote: 
 
 I guess you found out using bisection.  But I read some incertainty in
 your words »appears to have been introduced«.  Is the changeset
 8fab871a2a6f a reliable entrance point or a first approximation?

That particular problem is present in 8fab871a2a6f but not its parent (but who 
knows how often that behaviour changed in the history?)  It looks like there 
are more of these kinds of problems lurking, but unfortunately, I no longer 
fully understand the code, so I will have to rely on your help.  In particular, 
I would like to know what went wrong here.

Clemens
 

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

Re: [isabelle-dev] Regression in the sublocale command

[Clemens Ballarin]

I forgot to attach the example.  Loops here also for 4862f3dc9540 (12 Feb 2015).

Clemens


On 14 February, 2015 14:25 CET, Florian Haftmann 
florian.haftm...@informatik.tu-muenchen.de wrote:

 Hi Clemens,

 I am struggling to reproduce the behaviour you describe.  Find attached
 my attempt to contrieve an example.  Unfortunately, the looping is not
 reproducible in c3ca292c1484.  Can you provide more detail?

 Thanks,
   Florian

 Am 12.02.2015 um 22:19 schrieb Clemens Ballarin:
  Hi Florian,
 
  I'm investigating a regression which prevents identifying certain 
  equivalent locales through circular sublocale declarations:
 
sublocale loc1  x: loc2 A c (* sigma_1 *)
  where x.b == B and x.d == e (* tau_1 *)
sorry
 
sublocale loc2  x: loc1 A b (* sigma_2 *)
  where x.c == C and x.e == d (* tau_2 *)
sorry (* loops from changeset 8fab871a2a6f *)
 
  The last sorry loops, which is unfortunate, because it forces certain 
  workarounds on my current project.  In a fairly lengthy debug session I 
  figured out that it is the simplifier that loops.  This is an indication 
  that the morphisms tau_1 and tau_2 are applied simultaneously, which they 
  should not.  In any case, the behaviour appears to have been introduced 
  quite a while ago in 8fab871a2a6f, which is in the first batch of your 
  changes to the locale interpretation commands.
 
  Clemens
 
  ___
  isabelle-dev mailing list
  isabelle-...@in.tum.de
  https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
 

 --

 PGP available:
 http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de






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

Re: [isabelle-dev] Regression in the sublocale command

[Clemens Ballarin]

  This might indicate that something is wrong in the local theory stack
  here, maybe the last line in
  
  fun locale_dependency locale dep_morph mixin export =
(Local_Theory.raw_theory ooo Locale.add_dependency locale) dep_morph 
  mixin export
# Locale.activate_fragment_nonbrittle dep_morph mixin export;
  
  from generic_target.ML
 
 I can confirm that.

Thanks!  If you could provide me with a patch that works around the issue in 
the local theories, that could help me investigate the remaining problem.

The looping print_locale hints at an issue in dependency resolution itself.  I 
don't know whether the example has ever worked (probably it has not), but I 
find it useful enough to pursue.

Clemens


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

Re: [isabelle-dev] [isabelle] Contracting Abbreviations of Locale Definitions

[Clemens Ballarin]

Related to the below discussion on isabelle-users, I have now refined the patch 
I had circulated then.  Here is the NEWS entry:

* More gentle suppression of syntax along locale morphisms while
printing terms.  Previously 'abbreviation' and 'notation' declarations

would be suppressed for morphisms (except term identity).  Now merely
'notation' is suppressed.  This can be of great help when working with

complex locale hierarchies, because proof states are displayed much
more succinctly.  It also means that only notation needs to be
redeclared if desired, as illustrated by this example:

  locale struct = fixes composition :: "'a => 'a => 'a" (infixl "\" 65)
  begin
definition derived (infixl "\" 65) where ...
  end

  locale morphism =
left!: struct composition + right!: struct composition'
for composition (infix "\" 65) and composition' (infix "\''" 65)
  begin
notation right.derived ("\''")
  end

The full patch is attached.  Interestingly, it is fully compatible also with 
the AFP.  Since I'm not particularly familiar with generic_target.ML I'm 
posting it here for feedback.  My intention is to push this in the near future.

Clemens


On 28 July, 2015 12:12 CEST, Andreas Lochbihler 
<andreas.lochbih...@inf.ethz.ch> wrote:

> Hi Julian,
>
> First of all, I would be very happy if you could solve this problem of missing
> contractions. Clemens has never showed me an example where folding of 
> abbreviations would
> lead to non-termination. And I do not know precisely how abbreviations and 
> locales are
> implemented, so it is hard for me to decide whether something would lead to a 
> problem.
> Nevertheless, here is another example:
>
> locale l = fixes f :: "('a ⇒ 'a) ⇒ 'a ⇒ 'a"
> definition (in l) foo where "foo ≡ f (%x. x)"
> interpretation l "id" where "l.foo id == id (%x. x)" sorry
>
> If the interpretation installs abbreviations which respect the rewrite 
> morphism, then the
> abbreviation reads as "id (%x. x) == id (%x. x)" which clearly loops. If it 
> does not, then
> "id (%x. x)" is always printed as "foo".  This might not be optimal, as the 
> right-hand
> sides can be arbitrary general terms that should remain the way they are.
>
> Andreas
>
> On 28/07/15 11:33, Julian Brunner wrote:
> > Hi Andreas,
> >
> > Good call on the overlapping abbreviations, I did not consider this case. 
> > However, the
> > conflict already arises with the current implementation. Consider the 
> > following:
> >
> > locale foo =
> >fixes f :: "'a => 'a => bool"
> >fixes g :: "'a => 'a => 'a => bool"
> > begin
> >
> >definition test where "test = f"
> >sublocale f!: foo f "% x y z. g y z x" by this
> >
> > end
> >
> > This generates the following abbreviations (they end up in the Consts 
> > record in this order):
> >
> > f.test == foo.test f
> > f.f.test == foo.test f
> > test == foo.test f
> >
> > Since 'test' only depends on the parameter f, which is interpreted under 
> > the identity
> > morphism (eta contraction seems to matter here, so this does not happen 
> > with your original
> > example), all of these abbreviations are set up to be contracted before 
> > printing. In fact,
> > 'test' is printed as 'f.test' (presumably due to the order of the 
> > abbreviations in the
> > Consts record).
> >
> > Given that these contraction conflicts are already a problem as it is, I do 
> > not think that
> > it would make things significantly worse to allow contraction of 
> > abbreviations introduced
> > via other morphisms (barring other problems like the one you discussed with 
> > Clemens Ballarin).
> >
> > On Tue, Jul 28, 2015 at 8:53 AM Andreas Lochbihler 
> > <andreas.lochbih...@inf.ethz.ch
> > <mailto:andreas.lochbih...@inf.ethz.ch>> wrote:
> >
> > Hi Julian,
> >
> > I also regularly suffer from these pretty-printing nightmares, but I 
> > vaguely remember a
> > discussion with Clemens Ballarin on the subject. IIRC the problem is 
> > that it is not clear
> > whether collapsing the abbreviations terminates in all cases. Clemens 
> > has never showed me
> > an example where it actually happens, though.
> >
> > Yet, I can still think of difficult situations as as the following:
> >
> > locale foo =
> > fixes f :: "'a => 'a => bool"
> > and g :: "'a => 'a => 'a => bool&q

[isabelle-dev] Changes to the locale syntax

[Clemens Ballarin]

I'm planning two moderate changes to the locale syntax:

* The default of qualifiers in locale expressions will change from optional 
("?") to mandatory ("!") in the context of "locale" and "sublocale".  This 
brings these commands in line with "interpretation" and "interpret".  In larger 
developments it is apparent that this is the better default.

* As already mentioned in my previous message, I plan to change the keyword for 
rewrite morphisms from "where" to "rewrites".  This is to better distinguish 
these from named instantiations in locale expressions.  The syntax will then be

  sublocale A < B where y = x for x rewrites "z = w"

rather than

  sublocale A < B where y = x for x where "z = w"

Clemens

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

Re: [isabelle-dev] Future of permanent_interpretation

[Clemens Ballarin]

On 26 October, 2015 10:38 CET, Tobias Nipkow <nip...@in.tum.de> wrote: 
 
> My desire to generate code from locale interpretations w/o having to make a 
> number of trivial function definitions was what started this whole business a 
> number of years back. Florian's very useful implementation of that really 
> needs 
> to make it into Main.

It could simply be integrated with the current interpretation and sublocale 
commands, where the definitions could be supplied in a separate clause, as 
suggested by Florian, perhaps using "defines" as keyword.  Would this suit your 
needs?

(Independently I intend to change the keyword for the rewrite morphisms clause 
of these commands from "where" to "rewrites", to better distinguish it from 
named instantiations in locale expressions.)

> My understanding of "sublocale" is that it is an interpretation within a 
> locale 
> and I have used that explanation in papers because I find it very succinct. 
> Thus 
> I would welcome if the same keyword is used.

This view is of course valid, but it isn't the whole story.  With "sublocale" 
these interpretations are orchestrated in a manner such that the locale 
hierarchy is effectively changed.  Now I can see that there might be domains 
where this more abstract view is not relevant, but when working with a 
hierarchy of locales representing algebraic structures it is certainly 
appropriate.  It should also be kept in mind that "sublocale" is established in 
the locale documentation including my JAR paper [1].  If the desire for a 
different keyword is so strong, perhaps an alias might be a solution.

Clemens

[1] Clemens Ballarin. Locales: a module system for mathematical theories. 
Journal of Automated Reasoning, 52(2):123–153, 2014.


> On 25/10/2015 11:16, Clemens Ballarin wrote:
> > Hi Florian,
> >
> > this proposal goes too far, of perhaps, not far enough.  Let me explain.
> >
> > There is of course nothing wrong with providing new commands and 
> > enhancements for frequent use cases.  However, I don't see a good reason 
> > why users should be forced to write 'permanent_interpretation' where they 
> > could write 'interpretation' or 'sublocale'.
> >
> > I don't object to a careful evolution of the user interface to locales, but 
> > I don't think you're heading in the right direction.  Your 
> > 'permanent_interpretation' lets users make some definitions followed by, 
> > depending on the context, an interpretation or a sublocale declaration.  
> > This is certainly useful, but it is not general enough for making it the 
> > preferred command.  For example, it doesn't permit function declarations.  
> > It also blurs the distinction between 'interpretation' and 'sublocale' by 
> > calling the latter 'permanent_interpretation' when in a locale context, but 
> > not at the level of theories, but instead calling the former 
> > 'permanent_interpretation' at the level of theories.
> >
> > It should be kept in mind that in the current design the 'interpretation' 
> > commands are effective for the lifetime of their context: in theories they 
> > are therefore permanent, in context blocks they persist for that block and 
> > within a proof 'interpret' provides services for that proof.  This is 
> > pretty straightforward.  On the other hand, 'locale' and 'sublocale' are 
> > theory-level commands that relate a locale to a locale expression (which in 
> > both cases becomes a sublocale of the locale).  Their only difference is 
> > that 'locale' declares a new locale while 'sublocale' refers to an existing 
> > one.  We have allowed the use of 'sublocale' in locale contexts as a 
> > notational convenience, but I don't consider it a good idea to further blur 
> > the distinction between 'interpretation' and 'sublocale'.  Calling 
> > 'sublocale' 'permanent_interpretation' in some contexts and 'sublocale' in 
> > others is certainly bad.  The current design is, of course, not cast in 
> > stone, but for changing it, there has to be a 
> consistent vision first, so we know where we are heading.
> >
> > Certainly, your work has partly been inspired by the feeling that the 
> > current locale commands only provide the bare basics for manipulating 
> > locales.  For example, basing an interpretation or sublocale declaration on 
> > definitions is certainly something that could be done in a fancier manner.  
> > The situation is perhaps a bit similar to that of 'axclass' several years 
> > ago, where your work on type classes has improved the user experience 
> > dramatically.  If you would like to bring locales forward, you might 
> > consider developing ideas alo

Re: [isabelle-dev] Future of permanent_interpretation

[Clemens Ballarin]

 On 09 November, 2015 11:56 CET, Makarius  wrote: 
 
> It is formally trivial to have 'permanent_interpretation' in Isabelle/Pure 
> as separate command. If there is a simple way to have just one 
> 'interpretation' command with 'defines' vs. 'rewrites', I would prefer 
> that.

I would prefer to just have 'interpretation' as well.  Possibly 'sublocale' 
should also be extended by a 'defines' clause.

Clemens
 
 


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

Re: [isabelle-dev] Changes to the locale syntax

[Clemens Ballarin]

I have now committed these changes.

Clemens


On 28 October, 2015 21:53 CET, "Clemens Ballarin" <balla...@in.tum.de> wrote: 
 
> I'm planning two moderate changes to the locale syntax:
> 
> * The default of qualifiers in locale expressions will change from optional 
> ("?") to mandatory ("!") in the context of "locale" and "sublocale".  This 
> brings these commands in line with "interpretation" and "interpret".  In 
> larger developments it is apparent that this is the better default.
> 
> * As already mentioned in my previous message, I plan to change the keyword 
> for rewrite morphisms from "where" to "rewrites".  This is to better 
> distinguish these from named instantiations in locale expressions.  The 
> syntax will then be
> 
>   sublocale A < B where y = x for x rewrites "z = w"
> 
> rather than
> 
>   sublocale A < B where y = x for x where "z = w"
> 
> Clemens
> 
> ___
> 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] Future of permanent_interpretation

[Clemens Ballarin]

Hi Florian,

thanks for your feedback.  Local theories have done Isabelle and its users a 
great service in presenting a uniform view of different kinds of declarations 
in several contexts, and the locales reimplementation would have been much more 
painful without them.  However, if "local everything" forces us to name 
commands in the proof language after features that I would consider secondary 
(permanent vs. ephemeral interpretation) rather than primary (simple 
interpretation vs. interpretation that changes the locale hierarchy) then we 
need to check whether we are pushing this idea too far.

Clemens


On 29 October, 2015 11:41 CET, Florian Haftmann 
 wrote: 
 
> (this continues the previous mail)
> 
>  Certainly, your work has partly been inspired by the feeling that
>  the current locale commands only provide the bare basics for
>  manipulating locales.  For example, basing an interpretation or
>  sublocale declaration on definitions is certainly something that
>  could be done in a fancier manner.
> 
> According to my feelings, the whole locale machinery is an excellent and
> powerful part of the systems.  The addition of mixin definitions as
> special case of mixin rewrites do not touch the foundations (locale.ML /
> expression.ML) at all – there is no restriction to achieve the same
> result without them.  This implementation simplicity is the main reason
> I dared to undertake this adventure.
> 
> > This is certainly useful, but it is not general enough for making it the 
> > preferred command.  For example, it doesn't permit function declarations.  
> 
> I don't think this generality is needed.  The idea behind mixin
> definitions could be fomulated as »reinterpret this term as a new
> definition«; the properties are already there afterwards, there is no
> need for definitional extensions or construct them.
> 
> > The required definitions and proofs for an interpretation could for example 
> > be collected in a dedicated context in a step-by-step manner similar to 
> > that of class instantiation.
> 
> This could be thought of, but is another story.
> 
> > Your work also seems to be inspired by the desire to gradually rename 
> > 'sublocale' to 'interpretation', which I find surprising, because, compared 
> > to classes, 'sublocale' is the direct analogue of 'subclass' and 
> > 'interpretation' is the direct analogue of 'instantiation
> > '.
> 
> You are right with the type class / locale analogy.  But type classes
> only permit the algebraic view, they are too restricted for the »local
> everything« approach.  As mentioned in my previous mail, I am happy to
> leave both views stand in the long run, if we find a way to sort out the
> (now still hypothetic) corner cases of epheremal interpretation on the
> theory level and permanent interpretation in a nested context.
> 
> -- 
> 
> PGP available:
> http://home.informatik.tu-muenchen.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] [isabelle] Contracting Abbreviations of Locale Definitions

[Clemens Ballarin]

I have now committed this.  See isabelle/e89cfc004f18; the AFP didn't require 
changes.

The final version does not activate abbreviations as aggressively as my first 
proposal.  This was necessary so abbreviations are not propagated over rewrite 
morphisms, which would have been very confusing.

I did check that this change does not accidentally change any of the Isabelle 
documentation.  I also ran Makarius' termination stress test on Isabelle and 
the AFP.  The latter needed timeout_scale=8.

Clemens


On 08 November, 2015 18:59 CET, Makarius  wrote: 
 
> On Sat, 7 Nov 2015, Makarius wrote:
> 
> > Since the actual change to src/Pure/Isar/generic_target.ML is so small, 
> > we should just go ahead with it -- after a full test with AFP.
> 
> The option "timeout_scale" from Isabelle/a2f0f659a3c2 should help to do 
> this.
> 
> Note that AFP is presently a bit broken:
> 
>[RIPEMD-160-SPARK] is still on FAIL.
>[ShortestPath] is still on FAIL.
>[Graph_Theory] is still on FAIL.
> 
>Full entry status at http://afp.sourceforge.net/status.shtml
> 
>AFP version: development -- hg id f433a3e7bbf1
>Isabelle version: devel -- hg id 15952a05133c
> 
> 
>   Makarius
 
 
 
 

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

Re: [isabelle-dev] Example for global interpretation into instantiation [was: Future of permanent_interpretation]

[Clemens Ballarin]

Hi Florian,

I didn't have time to look at your patches, and since I only have superficial 
knowledge of instantiation contexts I didn't fully understand the example 
either.  I guess though that the purpose of these global interpretations is to 
propagate some constant declarations into the surrounding theory.  If this is 
useful we should certainly have such a command.

What I still fail to understand is why you want to use 'global_interpretation' 
as keyword if the command occurs directly in a theory.  This is redundant.  I 
now take this as a temporary solution until there is some better terminology 
for distinguishing kinds of interpretations, and I very much hope that we will 
not get into another debate about renaming 'interpretation' to 
'global_interpretation' or similar after the 2016 release.

Clemens


On 17 December, 2015 17:49 CET, Florian Haftmann 
 wrote: 
 
> Hi Clemens,
> 
> I have found a potential example for global interpretation into
> instantiation in the existing Isabelle sources.
> 
> The example is presented in the attached patches, which can be applied
> in alphabetical order on top of 32a530a5c54c.
> 
> The first patch experimentally introduces a global_interpretation
> keyword, which is then used in theory src/HOL/Library/Saturated.thy:
> 
> instantiation sat :: (len) "{Inf, Sup}"
> begin
> 
> global_interpretation Inf_sat: semilattice_neutr_set min "top :: 'a sat"
>   defines Inf_sat = Inf_sat.F
>   by standard (simp add: min_def)
> 
> global_interpretation Sup_sat: semilattice_neutr_set max "bot :: 'a sat"
>   defines Sup_sat = Sup_sat.F
>   by standard (simp add: max_def bot.extremum_unique)
> 
> end
> 
> Here we have a clear distinction between interpretation, which would
> only last until the closing end, and the explicitly permanent global
> interpretation which provides the necessary instance definitions.
> 
> This pattern, which uses interpretation as a kind of simple definitional
> package, is very common nowadays, as can be seen in theories like
> src/HOL/Groups_Big.thy, src/HOL/Groups_List.thy,
> src/HOL/Lattices_Big.thy or src/HOL/Library/Multiset.thy.
> 
> I have prepared this to give some evidence that my insistence on proper
> distinction between (confined) interpretation and (permanent) global
> interpretation has significant practical implications (although the
> experimental nature of the patches exhibits some issues in the internal
> machinery which would have to worked out properly first).  So, it is
> really a good idea to have a separate keyword »global_interpretation«.
> 
> Hence, before letting »permanent_interpretation« stand as it is, I would
> really prefer to replace the existing occurrences by
> »global_interpretation«, to avoid confusion in the long run.
> 
> So, my minimal plan for the upcoming release would be:
> * Provide »global_interpretation« as separate keyword.
> * Discontinue »permanent_interpretation« entirely – remaining
> occurrences are suitable for »global_interpretation«.
> * »interpretation« retains its current traditional semantics.  No
> systematic replacement by »global_interpretation«.
> * Polish the documentation accordingly.
> 
> I have no idea whether you have a time slot to consider and give
> feedback on this; anyway this plan is quite minimal invasive wrt.
> existing sources, so I am confident that it is appropriate for the
> upcoming release.
> 
> All the best,
> Florian
> 
> -- 
> 
> PGP available:
> http://home.informatik.tu-muenchen.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] Future of permanent_interpretation

[Clemens Ballarin]

Hi Florian,

I looked at the documentation generated with this patch, and the first 
impression of the "Locale interpretation" section is that it now looks funny -- 
probably due to the transitional nature of the patch.  For "interpretation" 
there are now two declarations and two productions, while previously they were 
merged into one.  The current state is confusing.  Readers must be able to 
quickly identify what is relevant by looking at the keyword.

From what I saw it looks as if we could get rid of a second keyword for 
interpretation by just merging the "defines" clauses into "interpretation".  I 
am not concerned about the "defines" clause only being available in some kinds 
of contexts.  From a user perspective, being able to say "interpretation" 
regardless of the context will be more natural than having to remember whether 
"interpretation" or "permanent_interpretation" (for example) is the right 
keyword.  The command could simply raise an error if a "defines" clause is used 
in situations where it is not available.

Regarding your concerns b) and c) I'm not sure I fully understand them.  
Regarding b), while it might be conceptually possible to make an interpretation 
from a locale context (say) in a theory, I don't think the proof document would 
read very well.  Regarding c), making an interpretation in a theory but confine 
it to the closing "end" keyword of the theory, this is conceivable, but do we 
have a use case for this?  Should we decide to go for such functionality in the 
future I would be more comfortable with modifiers rather than long keywords.

I have seen that you use the term 'mixin definition' in NEWS and isar-ref.  I'm 
not sure this is needed but if so it must be explained.

Clemens


On 15 November, 2015 10:53 CET, Florian Haftmann 
 wrote: 
 
> For further discussion, see now fd4ac1530d63, particulary
> src/Pure/Isar/interpretation.ML and 5.7.3 »Locale interpretation« in
> *isar-ref*.
> 
> This goes along the following lines:
> 
> * »Interpretation« in general is used as generic heading for every kind
> of intepretation into different destination contexts.
> * *interpretation* in particular denotes interpretation into a confined
> context. (The wording in the implementation is not yet consistent,
> ranging from »epheremal« to »confined«; I have a slight inclination to
> stick to the latter). *interpret* is the variant for proof blocks. This
> use of terminology IMHO is consistent with typical uses in mathematics
> and there had been little debate about that so far.
> 
> So far for the seemingly non-controversial matter.
> 
> Concerning the »persistent« / »permanent« / »subscribing« kinds of
> interpretation, there are two conflicting views so far:
> 
> * Each local theory can »subscribe« to locales, given that it underlying
> target implements it. Hence all targets (particularly, global theories
> and locales) are treated uniformly, using one keyword
> *permanent_interpretation.*
> * The user interfaces emphasizes the non-trivial differences between
> »subscription« into global theories and into locales, particularly the
> side effects of the latter on the existing locale hierarchy.
> 
> Personally I have no strong inclination to follow the one or the other
> and I am happy to abandon the first in favour for the second. However
> then I also suggest a dedicated keyword for interpretation into global
> theories:
> a) *interpretation* would otherwise be strangely overloaded, allowing
> mixin definitions on the level of global theories but not in other local
> theories.
> b) Conceptually it would also be possible to allow »subscribing«
> interpretation into global theories inside a nested local theory
> (although it is not clear whether our current implementation is actually
> suitable for that). Then *theory* … *context* … *begin … interpretation*
> would be ambiguous.
> c) Similarly, also a theory itself can be seen as a confined context
> block, making *theory* … *interpretation* itself ambiguous.
> Suitable candidates could be *theory_interpretation *or
> *global_interpreation*. Better suggestions welcome. Of course, the
> actual replacement would not occur in the upcoming but a later release.
> 
> On that single matter I want to excite some feedback before continuing.
> Also suggestions on 5.7.3 »Locale interpretation« in *isar-ref* are welcome.
> 
> Cheers,
>   Florian
> 
> -- 
> 
> PGP available:
> http://home.informatik.tu-muenchen.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] Supported Poly/ML versions

[Clemens Ballarin]

On 13 February, 2016 16:22 CET, Makarius  wrote: 
 
> > IMHO this sounds too obscure to be useful. How many users are actually 
> > aware of that possibility?
> 
> Maybe 2-3 people on this mailing list, but this is only a guess. So lets 
> make a constructive proof and count the people who show up here to say 
> that they knew that already.

I used this a while ago, with the help of Makarius, to debug a looping 
sublocale invocation.

> It is indeed all very obscure.  Time is better invested in making the 
> Poly/ML 5.6 debugger work for the Pure bootstrap as well, and add some 
> explicit support for exceptions to it.

I agree.

Clemens

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

[isabelle-dev] \mu and \nu in HOL-Algebra [was Re: Towards the Isabelle2017 release]

[Clemens Ballarin]

Dear Florian,


For the final record:


Concerning \mu and \nu, I am currently investigating whether an import
swap could re-establish the situation known from Isabelle2016-1


see http://isabelle.in.tum.de/repos/isabelle/rev/5a42eddc11c1


I had overlooked that \mu and \nu are global constants when importing 
this material, which I had received from Simon Foster.  This needs to be 
addressed properly.


Your workaround merely helps users of Group, not of Complete_Lattice.  
Moreover, it doesn't make sense that Complete_Lattice imports Group, and 
that the structure theorem about subgroups is now in lattice theory.


I request you revert this patch.

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

[isabelle-dev] \mu and \nu in HOL-Algebra [was Re: Towards the Isabelle2017 release]

[Clemens Ballarin]

On 2017-08-24 09:38, Thiemann, Rene wrote:


  If one imports HOL-Algebra.Multiplicative_Group (which we actually do
  via some transitive import), then \mu (LFP), \nu (GFP) and
  \phi (Euler’s totient function) become constants.


Unless I hear otherwise I will replace \mu by LFP and \nu by GFP.

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

Re: [isabelle-dev] \mu and \nu in HOL-Algebra [was Re: Towards the Isabelle2017 release]

[Clemens Ballarin]

On 2017-08-31 13:54, Florian Haftmann wrote:


The theorem in question requires both the notion of subgroup and
complete lattices, hence the import order dictates in which theory the
theorem has to reside (btw. the current import order is similar to
HOL-Main where Complete_Lattices comes after Groups).


The theorem in question is that of the subgroups of a group forming a 
complete lattice.  Such theorems exist for many algebraic structures.  
Following your approach they would all end up in Complete_Lattice, 
making that a very big theory.  I had decided against that.


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

Re: [isabelle-dev] \mu and \nu in HOL-Algebra [was Re: Towards the Isabelle2017 release]

[Clemens Ballarin]

On 2017-08-24 09:38, Thiemann, Rene wrote:

  If one imports HOL-Algebra.Multiplicative_Group (which we actually 
do

  via some transitive import), then \mu (LFP), \nu (GFP) and
  \phi (Euler’s totient function) become constants.


Unless I hear otherwise I will replace \mu by LFP and \nu by GFP.


I have done so now.  I also restored the original import order.

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

[isabelle-dev] Up-to-date instructions for 'isabelle afp_build -A'

[Clemens Ballarin]

Dear Maintainers of Isabelle / the AFP,

Where would I find instructions on actually getting 'isabelle afp_build 
-A' to run through?  I was hoping to find that in 
/doc/regression-test.md but that merely states the command.


It appears that I would need to set ML_PLATFORM=x86_64-darwin for the 
large sessions but then some magic seems to defeat that and builds are 
still for x86-darwin.


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

[isabelle-dev] NEWS: Locale rewrite morphism moved into expressions

[Clemens Ballarin]

In addition to Makarius' recent performance improvements, there is a 
modest reform to the way rewrite morphism are integrated with locales.  
Previously they were added as an after-thought to the interpretation 
commands.  Now they are integrated with locale expressions.


The main advantage is that situations where locale expressions lead to 
duplicate constant declaration errors can now better be avoided.  In 
principle, rewrite morphisms could also be allowed in locale 
declarations.  This would imply a proof block after every locale 
declaration, so I haven't done so.


These are the relevant NEWS entries:

* Rewrites clauses (keyword 'rewrites') were moved into the locale
expression syntax, where they are part of locale instances.  In
interpretation commands rewrites clauses now need to occur before
'for' and 'defines'.  Minor INCOMPATIBILITY.

* For rewrites clauses, if activating a locale instance fails, fall
back to reading the clause first.  This helps avoid qualification of
locale instances where the qualifier's sole purpose is avoiding
duplicate constant declarations.

These are the relevant changesets in Isabelle and the AFP:

http://isabelle.in.tum.de/repos/isabelle/rev/b6ce18784872
  Proper rewrite morphisms in locale instances.
http://isabelle.in.tum.de/repos/isabelle/rev/d5a7f2c54655
  Fall back to reading rewrite morphism first if activation fails 
without it.

http://isabelle.in.tum.de/repos/isabelle/rev/0f8cb5568b63
  Drop rewrites after defines in interpretations.

https://bitbucket.org/isa-afp/afp-devel/commits/744680a5363124dad21569ea3fdc431d5aad2e00
  Rewrites clauses are now part of locale expressions.
https://bitbucket.org/isa-afp/afp-devel/commits/6bfd6925be04049bc9d0833708ae42685a3ac6b9
  Pull rewrites clause in front of defines.

Some internal cleanup is still to come.

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

[isabelle-dev] Deadlock while building HOL-Proof

[Clemens Ballarin]

While building HOL-Proof I observe a deadlock, usually after 13 min CPU 
time.  It can be worked around with ISABELLE_BUILD_OPTIONS="threads=1".  
The deadlock occurs most of the time.  The earliest changeset I was able 
to reproduce this with is


  changeset:   67675:738f170f43ee
  user:paulson 
  date:Tue Feb 20 09:34:03 2018 +
  summary: Merge

This includes changes to HOL/Tools and Pure/Concurrent.
'isabelle build' reports these settings:

  ML_PLATFORM="x86-darwin"
  ML_HOME="/Users/ballarin/.isabelle/contrib/polyml-5.7.1-5/x86-darwin"
  ML_SYSTEM="polyml-5.7.1"
  ML_OPTIONS="--minheap 500"

The deadlock happens on a MacBook Pro:

  macOS 10.13.3 (17D102)
  2,7 GHz Intel Core i5
  8 GB 1867 MHz DDR3

Please let me know if I can provide any other useful information.

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