Re: [isabelle-dev] simplifier and subgoaler not transitive

2012-05-23 Thread Christian Urban


On Thursday, May 24, 2012 at 12:14:14 (+1000), Thomas Sewell wrote:
 > It looks like you want to implement a simproc.

Thanks a lot for the suggestion. My first "iteration"
was implemented via a solver. It worked. But then,
inspired by the neq-simproc in HOL.thy, I already 
modified my code to be a simproc. This seems the slightly
better solution.

 http://www4.in.tum.de/~urbanc/cgi-bin/repos.cgi/nominal2/rev/8f51702e1f2e

 > Then you have to write some code to actually declare and prove the 
 > equality (e.g. with Goal.prove_internal). This may be as simple as 
 > resolving with "atom a # b ==> a = b == False" if necessary and then 
 > simplifying with "atom v # (x, y) = (atom v # x & atom v # y)".

That is roughly what I did.

 > I've never tried adjusting the solver/subgoaler.
 
It is not too complicated - you have to essentially 
write a tactic that will be tried during simplification. 
I am not sure what the overhead is for having a
custom solver. I did not notice any slowdown with my test 
repository using either version. But I guess the
simproc is called only in cases where it possibly
can apply.

 > If you implement the simproc as suggested above though, simp traces will 
 > become very confusing. They'll be interrupted at depth 3 where the 
 > simproc is called by a subtrace starting from depth 0 which describes 
 > the (uninteresting) inner proof. This is particularly annoying if you 
 > set a low tracing depth limit. There is a fix for this (which will put 
 > the subtrace at depth 4), possibly involving Simplifer.inherit_context. 
 
Thanks for the information. Since the simproc-pattern
is rather "specific", it is usually predictable what
should happen. And as usual inserting "val _ = tracing ..." 
judiciously helps. ;o) So I had no need yet to look again 
at the simplifier trace.

Best wishes and thanks again for all the helpful information.

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


Re: [isabelle-dev] simplifier trace (and jedit)

2012-05-23 Thread Christian Sternagel

On 05/23/2012 10:38 PM, Makarius wrote:

On Wed, 23 May 2012, Christian Sternagel wrote:


3) Furthermore, in my course I recommend students (which know about
term rewriting before) to have a look at the simplifier trace whenever
the simplifier does something unexpected or does not terminate.
However, for the latter use-case (i.e., finding cause of
nontermination) I do not even know how to do it myself in jedit. As
soon as I write, e.g., "apply simp" the simplifier starts to loop, if
I don't delete the command it continues looping (and thus the whole
system becomes highly unresponsive very soon), if I delete the
command, the trace is gone too. Is there any way (or workaround), such
that I can generate (part of) the trace of a (potentially) looping
reduction.


The Prover Session panel has check/cancel buttons that are reminiscent
of manual control in PG. The keyboard shortcuts are C-SPACE and
C-BACKSPACE, respectively. You need to avoid rash movements after
cancelation, outerwise the checking process restarts.
I overlooked those, thanks! Unfortunately, this does not work very well 
(or maybe I misunderstood the intended way of use). I don't see the 
purpose of "Check", since it seems that as soon as I start typing again, 
asynchronous checking does start anyway. While clicking on "Cancel" does 
not always cancel the process (or maybe there is just a huge delay, 
since the trace is so big; anyway the result is that jedit becomes 
unresponsive and I basically have to kill it). (The keyboard shortcuts 
do not work for me, C-SPACE is already in use in my GNOME, so I know why 
this does not work, but C-BACKSPACE apparently does backwards deletion 
of a word inside jedit; I'll check whether this works when I set 
different keyboard shortcuts).


cheers

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


Re: [isabelle-dev] simplifier and subgoaler not transitive

2012-05-23 Thread Thomas Sewell

It looks like you want to implement a simproc.

These procedures operate on a family of term patterns and generate 
meta-equalities which the simplifier then applies. In this case I think 
you want to produce rewrites of the form "a = b == False" and "atom v # 
t == True". These rewrites can then be applied anywhere in your term, 
not just the conclusion.


Note that the simproc code, which is passed to Simplifier.simproc, takes 
the current simpset as an argument. Simplifier.prems_of_ss then tells 
you which local assumptions you have to work with. You can hopefully 
come up with some efficient check for whether you will be able to derive 
the needed rewrite from what you have available.


Then you have to write some code to actually declare and prove the 
equality (e.g. with Goal.prove_internal). This may be as simple as 
resolving with "atom a # b ==> a = b == False" if necessary and then 
simplifying with "atom v # (x, y) = (atom v # x & atom v # y)".


I've never tried adjusting the solver/subgoaler.

If you implement the simproc as suggested above though, simp traces will 
become very confusing. They'll be interrupted at depth 3 where the 
simproc is called by a subtrace starting from depth 0 which describes 
the (uninteresting) inner proof. This is particularly annoying if you 
set a low tracing depth limit. There is a fix for this (which will put 
the subtrace at depth 4), possibly involving Simplifer.inherit_context. 
Another workaround might be to put "atom v # (x, y) = (atom v # x & atom 
v # y)" in dest and intro form and just use the classical solver.


Yours,
Thomas.

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


Re: [isabelle-dev] simplifier trace (and jedit)

2012-05-23 Thread Makarius

On Wed, 23 May 2012, Christian Sternagel wrote:

3) Furthermore, in my course I recommend students (which know about term 
rewriting before) to have a look at the simplifier trace whenever the 
simplifier does something unexpected or does not terminate. However, for 
the latter use-case (i.e., finding cause of nontermination) I do not 
even know how to do it myself in jedit. As soon as I write, e.g., "apply 
simp" the simplifier starts to loop, if I don't delete the command it 
continues looping (and thus the whole system becomes highly unresponsive 
very soon), if I delete the command, the trace is gone too. Is there any 
way (or workaround), such that I can generate (part of) the trace of a 
(potentially) looping reduction.


The Prover Session panel has check/cancel buttons that are reminiscent of 
manual control in PG.  The keyboard shortcuts are C-SPACE and C-BACKSPACE, 
respectively.  You need to avoid rash movements after cancelation, 
outerwise the checking process restarts.



Maybe giving a timeout to "apply simp" (but I don't know whether or how 
this is possible) does work?


Long-running commands are generally bad for reactivity.  Using timeouts 
with some kind of iterative deepening of the amount of checking might help 
here.  It is one of the many fine points in the scheduling that can be 
improved beyond the received PG/TTY model, so that manual cancelation can 
be discontinued altogether at some point.



Makarius

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


Re: [isabelle-dev] simplifier trace (and jedit)

2012-05-23 Thread Makarius

On Wed, 23 May 2012, Christian Sternagel wrote:

- Why does "apply (simp only: rule)" and "unfolding rule" behave 
differently? E.g., on the term "Suc 0 = 0" with rule 
"Nat.nat.distinct(2)" the former results in "False", whereas the latter 
does nothing. Is it important that those two commands behave 
differently?


There are several historical accidents here.

Unfolding plain definitions should be unfolding plain definitions, not 
approximative simplification, which does sometimes more sometimes less 
than expected.  Unfortunately, there are user theories out there, that use 
the 'unfolding' command for genuine simplification of facts and goals.


Likewise, (simp only: ...) should use only the given rules to simplify, 
not arbitrary complex loopers that might be there as well.  When I 
introduced the "only" modifiers many years ago, I convinced myself that 
all loopers were trivial in the sense that there are required to solve the 
simplification problem successfully (by rule refl, TrueI etc.).  Later on
quite non-trivial loopers were added, and I missed the opportunity to sort 
this out.


The following sketch has been in my TODO list for many years to iron out 
these confusions:


  * unfold/unfolding strictly unfolds equations of the form c x y = t
in the sense of c == %x y. t

  * (simp only: ...) only keeps trivial loopers, and removes arithmetic
etc.

  * (simp mainly: ...) is like the current (simp only: ...) for
applications that really mean to keep non-trivial tools in the
simplifier.


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


Re: [isabelle-dev] simplifier trace (and jedit)

2012-05-23 Thread Makarius

On Wed, 23 May 2012, Christian Sternagel wrote:


Consider, e.g., the trace resulting from

  lemma "Suc 0 + 0 = 0"
using [[simp_trace]]
apply simp

where we have (among others)

  [1]Applying instance of rewrite rule "Nat.nat.distinct_2":
  Suc ?nat'2 = 0 ≡ False

Why not use the "real" name "Nat.nat.distinct(2)" in the trace (Okay, 
the rule was "preprocessed" by the simplifier, but still, as far as I 
can tell the printed name does not exist)?


The printed name is of a different category, which is vaguely related to 
the internal derivation object (PThm), but not exactly that.  These names 
should hardly ever occur to the user, but there are some historical 
left-overs as seen here.


The Prover IDE markup already provides a good deal of authentic source 
position information, so one could extend this to cover thm values as 
well.  For example, when I see `prop` in the text, I often want to C-click 
on it to get to the place where the corresponding fact was introduced, but 
the tiny goal/tactic derivation gets between the result and its origin in 
the source.


The simplifier has similar adhoc derivations in mksimps.  Another problem 
are morphisms applied before addsimps.  This distance to the source 
somehow needs to be formalized in a more robust manner.



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


Re: [isabelle-dev] simplifier and subgoaler not transitive

2012-05-23 Thread Makarius

On Tue, 22 May 2012, Christian Urban wrote:


Assuming that this is about the bowels of the simplifier,
I hope this is the right place to ask the following question.


From what I've seen on the thread so far, it is all perfectly normal 
Isabelle user-space.  You did not propose to re-implement the simplifier, 
so it could just as well be discussed on the larger audience of 
isabelle-users.  The experts are out there, and they are using Isabelle 
Professional Edition (aka release).



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


Re: [isabelle-dev] Isabelle2012 post-release mode

2012-05-23 Thread Gerwin Klein
On 23/05/2012, at 9:28 PM, Makarius wrote:
>  * Gerwin should know what needs to be done to release AFP for
>Isabelle2012.

The AFP is now on freeze until the update to 2012 is out. 

I will be branching off for the release itself, but to keep the merge back 
simple, please refrain from committing to the AFP repository until the release 
is out. 

Since everything is building fine at the moment I'm hoping for this to happen 
in no more than a day or two.

Cheers,
Gerwin

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


[isabelle-dev] Isabelle2012 post-release mode

2012-05-23 Thread Makarius

Dear All,

the current situation is as follows:

  * As of Isabelle/c5f7be4a1734 the
http://isabelle.in.tum.de/repos/isabelle-release branch is merged
again with the main line.

  * isatest is back testing http://isabelle.in.tum.de/repos/isabelle

  * We are still waiting for the Sydney mirror to follow Cambridge and
Munich, so that the release can be announced officially.

  * Gerwin should know what needs to be done to release AFP for
Isabelle2012.

  * I am on vacation for the first 3 weeks of June.


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


Re: [isabelle-dev] simplifier and subgoaler not transitive

2012-05-23 Thread Christian Urban

I am amazedby you and the simplifier!

Yes, indeed one rule in question was added by mksimps.
You were spot on. I never knew that they have some 
more-than-special meaning. ;o)

The reason why I prefer to keep the freshness constraints
together is that

   atom a # (x1, x2, x3, x4, x5)

would expand to

   atom a # x1 /\ atom a # x2 /\ ...

thus bloating the goal state.

Poring over the trace again and again, and adding "probes", 
like the ones below (in case somebody is interested), actually 
the trace information is quite instructive. It is just a lot of 
pain to piece everything together...but I guess that is what 
one has to love when working with Isabelle. ;o)

In conclusion, I need to implement a special solver for solving the 
type of goals I want to solve...quite a sophisticated piece of code
the simplifier, but good that it lets me do that. 

Thanks again for all replies!
Christian

ML {*
val test_solver = mk_solver "test solver" 
   (fn ss => fn n => print_tac ("TEST SOLVER"))

fun test_subgoaler ss n = 
   print_tac ("SUBGOALER TEST") THEN asm_simp_tac ss n
*}

declaration {* fn _ =>
  Simplifier.map_ss (fn ss => Simplifier.set_subgoaler test_subgoaler (ss 
addSolver test_solver)) 
*}



On Wednesday, May 23, 2012 at 11:39:53 (+1000), Thomas Sewell wrote:
 > Question: it looks to me like "(atom v # (x, y)) = (atom v # x & atom v 
 > # y)"
 > 
 > It also looks like what you're trying to do is allow the system to 
 > reason with the above equality without actually giving it that equality. 
 > It looks like you've provided the equality in one direction as a rewrite 
 > rule and in the other direction by adjusting mksimps (just guessing 
 > here, but that's what it looks like).
 > 
 > Did I guess right? If so, I know why that won't work :-) The new rewrite 
 > rules created by mksimps aren't themselves candidates for 
 > simplification, so the system won't apply Nominal2_Base.fresh_at_base_2 
 > to them, which was what resulted in further progress on goal #2.
 > 
 > Those are all giant guesses. Am I anywhere near the mark?
 > 
 > More directly, why not just add the rewrite at the top of this email to 
 > the simpset? This will reduce all of these sharp statements to trivial 
 > inequalities. This is the approach that fits with the general design of 
 > the simplifier. Not the structure you want? Too many inequalities? In 
 > that case you really need a guided solver - giving the simplifier 
 > opportunities for wild exploration will just slow everything down.
 > 
 > Yours,
 >  Thomas.
 > 
 > On 23/05/12 02:23, Christian Urban wrote:
 > > Dear All,
 > >
 > > Assuming that this is about the bowels of the simplifier,
 > > I hope this is the right place to ask the following question.
 > >
 > > The simplifier has a subgoaler, which helps with rewriting
 > > conditional lemmas. This simplifiying/subgoaling process seems
 > > to be not transitive (probably is not meant to be). The problem
 > > that arises for me is the following: I have set up the simplifier
 > > to automatically solve the first two lemmas:
 > >
 > >lemma "atom v # (x1, x2) ==>  atom v # x1"
 > >apply(simp)
 > >done
 > >
 > >lemma "atom v # x1 ==>  v \  x1"
 > >apply(simp)
 > >done
 > >
 > > but it chokes, if I am trying to string both lemmas
 > > together
 > >
 > >lemma "atom v # (x1, x2) ==>  v \  x1"
 > >apply(simp) --"fails"
 > >
 > > Is there some magic that I can make the simplifier to
 > > deal also with the latter goal?
 > >
 > > The cool thing about jEdit is that I have the simplifier
 > > traces of all three goals next to each other (the trick
 > > is to disable the auto update). Unfortunately, I am
 > > not very good at reading these traces. The only thing I
 > > can say is that the simplifier starts off with goal 1
 > > and 3 in the same direction, but then things start to
 > > diverge. Is there a place where one can read up about
 > > the tracing information of the simplifier? The traces
 > > are attached for reference.
 > >
 > > Best wishes and thanks for any help,
 > > Christian
 > >
 > >
 > >
 > > GOAL 1
 > > ==
 > >
 > >   [1]SIMPLIFIER INVOKED ON THE FOLLOWING TERM:
 > > atom v ♯ (x1, x2) ⟹ atom v ♯ x1
 > >   [1]Applying instance of rewrite rule "??.unknown":
 > > ?a1 ♯ ?x1.1 ⟹ ?a1 ♯ ?x2.1 ⟹ ?a1 ♯ (?x1.1, ?x2.1) ≡ True
 > >   [1]Trying to rewrite:
 > > atom v ♯ x1 ⟹ atom v ♯ t ⟹ atom v ♯ (x1, x2) ≡ True
 > >   [2]SIMPLIFIER INVOKED ON THE FOLLOWING TERM:
 > > atom v ♯ x1
 > >   [1]FAILED
 > > atom v ♯ x1 ⟹ atom v ♯ t ⟹ atom v ♯ (x1, x2) ≡ True
 > >   [1]Adding rewrite rule "??.unknown":
 > > atom v ♯ x1 ≡ True
 > >   [1]Adding rewrite rule "??.unknown":
 > > atom v ♯ t ≡ True
 > >   [1]Applying instance of rewrite rule "??.unknown":
 > > atom v ♯ x1 ≡ True
 > >   [1]Rewriting:
 > > atom v ♯ x1 ≡ True
 > >   proof (prove): step 1
 > >
 > > goal:
 > > No subgoals!
 > >
 > >
 > > GOAL 2
 > > ==
 > >
 > >   [1]SIMPLIFIER INVOKED ON THE FOLLOWING TERM:
 > > atom v ♯ x1 ⟹ v ≠ x1

Re: [isabelle-dev] simplifier trace (and jedit)

2012-05-23 Thread Tobias Nipkow
Am 23/05/2012 06:15, schrieb Christian Sternagel:
> - in the "[1]Rewriting:" messages, we actually just see the redex and the
> contractum, but not the context of a rewrite step. Why not show the whole 
> terms?
> (One reason against this is the high redundancy and potentially huge size of
> such traces, but on the other hand, they are traces and only generated when
> requested.)

Size is indeed an issue, but also that it would be a considerable amount of work
to implement it properly. Ideally you want an interactive tracer anyway, which
is yet more work.

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