from:"Andreas Lochbihler"

Re: [isabelle-dev] Testing the QuickCheck setup

2018-08-06 Thread Andreas Lochbihler


Dear Lars,

Testing quickcheck is indeed quite tricky. Do you know which of the quickcheck calls time 
out? Does it happen only with the random generator or also with exhaustive?


It might be that you have a fairly large set of code equations and the timeout already 
kicks in during code generation or compilation with PolyML, though. A larger timeout 
should help there.


Moreover, both statements have two free variables and you rely on the quickcheck 
generators being able to quickly come up with two different values for them. If you are 
not to set on the property, you could alternatively use


lemma "x ~= x" for x :: dec

which will definitely fail on the first generated example.

Hope this helps,
Andreas

On 06/08/18 07:57, Lars Hupel wrote:

Dear list,

I've been trying to test some QuickCheck generators in the CakeML
formalization, like so:



Unfortunately, it seems that they fail occasionally. I've tried
increasing the timeout, but that still seems to be problematic.

Is there a way to make these tests more robust? I don't want to comment
out the checks because much of the QuickCheck setup silently fails if
something is broken; meaning e.g. that Auto QuickCheck just doesn't work
on a proposition where it should work.

Cheers
Lars
___
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] NEWS: op -> ()

2018-01-16 Thread Andreas Lochbihler


On 16/01/18 16:14, Lawrence Paulson wrote:

On 16 Jan 2018, at 14:13, Blanchette, J.C.  wrote:

However, for operators like ==>, which bind on the right,

foo ==>
bar

is actually much more readable than

foo
==> bar


This sort of claim needs to be justified by evidence. We had it the first way 
until the late 1990s. I changed it to the other way while working on large 
proof states connected with crypto protocols. It seemed more readable to me for 
such proofs.


I agree with Larry. I also prefer to write

  foo
  ==> bar

because my assumptions are often very long and I want to spot the conclusion 
immediately.


foo ==> bar
==> baz


As for this last example, we definitely need the earlier syntax [|foo; bar|] 
==> baz, which has been made almost impossible to enable.

It's not too hard: Go to Plugins/Plugin Options/Isabelle/General and enter "brackets" 
under Print mode.


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

Re: [isabelle-dev] Slow builds due to excessive heap images

2017-11-08 Thread Andreas Lochbihler


Hi Makarius,

On 08/11/17 14:13, Makarius wrote:

On 08/11/17 12:35, Tobias Nipkow wrote:


On 07/11/2017 23:13, Makarius wrote:

For Flyspeck-Tame a small performance loss remains. It might be worth
trying to configure the Isabelle/HOL codegen to use FixedInt instead of
regular (unbounded) Int. Thus it could become faster with Poly/ML 5.7.1
than with 5.6.


Just as for Isabelle itself, I don't want generated code to abort with
overflow or even worse to overflow silently.


I also don't want to see FixedInt used routinely instead of proper
mathematical Int.

The idea above is to provide an option for the HOL codegen that is used
specifically for applications like Flyspeck-Tame. It is mainly a
question to codegen experts, if that can be done easily.


My AFP entry Native_Word basically provides the setup for unsigned fixed-size integers, 
but as a separate type uintXX. The same could be done for signed fixed-size integers. The 
problem is how to get from int to uintXX. There are basically two options:


1. Just axiomatize that int are implemented with uintXX. This is potentially 
unsound.

2. Prove that actually no overflow occurs in the computations. The AFP entry 
Berlekamp-Zassenhaus does that for factoring polynomials over finite fields. The basic 
setup is there, but applying it to a particular instance requires quite some work.


FixedInt has the additional challenge that the width is implementation dependent, so this 
requires a few tricks similar to the formalisation of uint in the AFP entry.


In summary: In principle it could be possible to use FixedInt in Flyspec-Tame in a sound 
way, but it would be quite a bit of work.


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

[isabelle-dev] PolyML update

2017-08-11 Thread Andreas Lochbihler


Dear list,

I've been playing around with adding unsigned 64 bit integers to the AFP entry 
Native_Word. In doing so, I realised that PolyML in 64 bit mode has a bug in the Word64 
implementation in the version that the current development version 2a6371fb31f0 uses 
(PolyML 5.6-1). For example, dividing 18446744073709551611 by 3 using the Word64 structure 
gives a wrong result. The problem seems to be fixed in PolyML 5.7. I am now hesitant to 
update my AFP entry because (1) I cannot include all the test cases for Uint64 that I want 
and (2) if PolyML 5.6-1 is also shipped with the next release, then users might prove 
False by exploiting this error.


Are there any plans to update to PolyML 5.7 before the release?

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

Re: [isabelle-dev] Towards a "localized" code generator

2017-07-24 Thread Andreas Lochbihler


Dear Lars,


Well, we here at ETH have another function transformer, which can also
be activated and deactivated basically with almost the same pattern. The
only difference is that at the moment we use a command rather than a
Config value because de- and reactivation in our case has to do a bit
more than just enabling/disabling a function transformer. It also must
swap a few code equations.


Function transformers could also be declared with an attribute, although
there I'd say it's even less clear that attributes should be (ab)used
for that.

Yes, we felt like that, too. That's why we went for a command.


This is an interesting idea. For the above-mentioned function
transformer, we also have code_datatype declarations that must be
switched back and forth. The big advantage of your approach seems to me
that one can envision this alternative setup already where characters
are defined (and similarly for int/nat/set/mapping/...).


Exactly, that's another goal that could be achieved.


But I wonder
whether these bundle targets can be extended later. That is, if is some
unrelated theory, I write my own function for chars by pattern-matching
on Char. If I then import your theory, can I add further declarations
(code drop/code) to the bundle such that subsequent theories get a
consistent setup no matter whether the unbundle the bundle or not?


Currently I'm unaware of any way to extend bundles, except for something
like:

bundle bar begin
   unbundle foo
end

Whether or not extending bundles is possible/canonical in Isar is a
question best answered by Makarius.

Well, originally, bundles were never meant to be extended later. That's what Makarius told 
me back in 2012. Maybe the situation has changed now. But I'd say that this is crucial to 
improve the current state of the art. Otherwise, we'll just have a mess with bundle names.


Independently, a localised code generator would of course be nice.

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

Re: [isabelle-dev] Towards a "localized" code generator

2017-07-24 Thread Andreas Lochbihler


Dear Lars,

On 24/07/17 15:08, Lars Hupel wrote:

1) Function transformers: I want to run a function transformer in
special situations. But I can only register it globally (with
"Code_Preproc.add_functrans"). What I use is the following pattern:

val enabled = Attrib.setup_config_bool @{binding "constructor_funs"} (K
false)

fun functrans ctxt thms = (* implementation *)

val code_functrans = Code_Preproc.simple_functrans (fn ctxt =>
   if Config.get ctxt enabled then
 functrans ctxt
   else
 K NONE)

I'm not sure whether this is how attributes are meant to be used, but at
least I can enable this locally. But as far as I can tell there are only
three function transformers in total, so I'm not sure how relevant this is.
Well, we here at ETH have another function transformer, which can also be activated and 
deactivated basically with almost the same pattern. The only difference is that at the 
moment we use a command rather than a Config value because de- and reactivation in our 
case has to do a bit more than just enabling/disabling a function transformer. It also 
must swap a few code equations.



2) "Fake local" declarations: I want to change the representation of the
"char" type in declared code. By default, it is represented using
numerals in a "non-free" way (i.e. there are invalid representations).
I'd like to replace it with a free representation (bytes), but don't
want this to affect the global theory; or at least, I'd like to avoid
people importing my theory to be affected [0].

Here's my workaround:

ML‹
   fun code_attribute f = Thm.declaration_attribute (fn thm =>
Context.mapping (f thm) I)
›

attribute_setup "code_datatype" = ‹
   Scan.repeat1 Args.term >> (fn terms =>
 code_attribute (K (Code.declare_datatype_global (map dest_Const
terms
›

Now I can use the "bundle" target:


bundle char_byte_representation begin

declare [["code_datatype" char_of_byte]]

declare [[code drop: equal_char_inst.equal_char String.Char]]

(* more ... *)

declare char_byte_literals[code_unfold]

end

Importing this theory doesn't change the code setup. Only when I use
"unbundle" the changes become permanent. However, it doesn't work
properly in an unnamed context with "including" (this is as expected).
There are a lot of occurrences of "code_datatype", often leading to the
problem of artificially splitting up theories into an "abstract" and
"implementation" part.

This is an interesting idea. For the above-mentioned function transformer, we also have 
code_datatype declarations that must be switched back and forth. The big advantage of your 
approach seems to me that one can envision this alternative setup already where characters 
are defined (and similarly for int/nat/set/mapping/...). But I wonder whether these bundle 
targets can be extended later. That is, if is some unrelated theory, I write my own 
function for chars by pattern-matching on Char. If I then import your theory, can I add 
further declarations (code drop/code) to the bundle such that subsequent theories get a 
consistent setup no matter whether the unbundle the bundle or not?


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

Re: [isabelle-dev] [isabelle] Good name for "sublist" predicates

2017-07-03 Thread Andreas Lochbihler


See now Isabelle/4c999b5d78e2.

Andreas

On 30/06/17 21:31, Tobias Nipkow wrote:


On 30/06/2017 20:41, Manuel Eberl wrote:

By the way, I recently encountered a similar (and even more nasty)
name clash, with compact. The following works perfectly

It's "Topological_Spaces.compact" and that should definitely work. We
should probably make the one from Complete_Partial_Order2 qualified. In
my opinion, there is no question that "compact" should be "compact" in
the topological sense.


Yes, that's a no-brainer. I expect Andreas (the author) will not mind hiding or renaming 
that "compact" in the most appropriate way.


Tobias



___
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] [isabelle] Good name for "sublist" predicates

2017-07-03 Thread Andreas Lochbihler


Hi all,

Yes, it absolutely makes sense to change the situation with compact. It is a standard 
notion in order theory, so my suggestion is to make it qualified with ccpo, just like 
admissible and fixp are. I can take care of that.


Andreas

On 30/06/17 21:31, Tobias Nipkow wrote:


On 30/06/2017 20:41, Manuel Eberl wrote:

By the way, I recently encountered a similar (and even more nasty)
name clash, with compact. The following works perfectly

It's "Topological_Spaces.compact" and that should definitely work. We
should probably make the one from Complete_Partial_Order2 qualified. In
my opinion, there is no question that "compact" should be "compact" in
the topological sense.


Yes, that's a no-brainer. I expect Andreas (the author) will not mind hiding or renaming 
that "compact" in the most appropriate way.


Tobias



___
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] [isabelle] Good name for "sublist" predicates

2017-06-30 Thread Andreas Lochbihler


Hi Manuel,

Well, how about changing Sublist.subseq to Sublist.subsequence? And accordingly 
strict_subseq to strict_subsequence or ssubsequence?


Andreas

On 28/06/17 19:49, Manuel Eberl wrote:

Yes, I noticed that as well. I decided to leave it that way since, well,
we do have qualified names.

If anybody has better suggestions, I am open to implementing them.

Manuel


On 2017-06-28 17:05, Andreas Lochbihler wrote:

Dear all,

While porting some of my theories to the current development version,
I've just noticed that the renaming of sublisteq to subseq done by
Manuel in May (639eb3617a86) has one bad effect:

The name subseq is already used in Topological_Spaces to formalise the
concept of a subsequence. This name is now hidden by the definition in
Sublist, in particular when I import HOL-Probability.

Can this name clash be eliminated before the next release such that I
don't have to write Topological_Spaces.subseq everywhere?

Thanks,
Andreas

On 26/05/17 08:16, Tobias Nipkow wrote:

Thank you for your research. I am perfectly happy with "sublist" (for
the contiguous case) and "subseq" (for the general case) and think we
should adopt it.

[Then we would rename sublisteq -> subseq and sublist :: "'a list ⇒
nat set ⇒ 'a list" (in List) to something else, eg sublist_index)

Tobias

On 25/05/2017 21:13, Jasmin Blanchette wrote:



On 25.05.2017, at 20:41, Tobias Nipkow <nip...@in.tum.de> wrote:

I don't think that sublist, subsequence and substring really have
much of a bias in either direction, except possibly substring, but
the latter does indeed sound too specialized.


Wikipedia has a clear bias (and I did not edit it, nor did I look it
up before writing my previous email):

 https://en.wikipedia.org/wiki/Subsequence
 https://en.wikipedia.org/wiki/Substring

Popular algorithm sbooks like Cormen et al. follow the same
definition of subsequence. Standard expressions like "longest
increasing subsequence" depend on this semantics.

As for sublist, all the examples I see by Googling either "sublist",
"is_sublist", "isSublist", or "indexOfSubList" in Java, Python,
Scala, etc., have the contiguous semantics. Including this page:

 http://www4.in.tum.de/lehre/praktika/psv/psv98/Vorlesung5/aufg4.html

I'm not saying we should rename the Isabelle concepts, just that
Isabelle is the odd (wo)man out.

Jasmin




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

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


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

Re: [isabelle-dev] Efficient code for Discrete.log

2017-06-29 Thread Andreas Lochbihler


Hi Manuel,

You are not the first to encouter this problem. Here's my experience:

In 4b1b85f38944, I added code_printings for gcd and decided to add Gcd to the imports of 
Code_Target_Nat. IIRC this broke a few things in the AFP, which I had to fix. Meanwhile, 
Gcd has become part of Main again.


Conversely, the AFP entry Native_Word sets up serialisation for bit operations, and there 
is a specific Code_Target_Bits_Int theory with the relevant adaptations for bit operations 
on integers.


I'd suggest that you setup two theories Code_Target_Complex_Int and 
Code_Target_Complex_Nat that will collect all the code declarations for constants that are 
defined in Complex. I think this is the cleanest approach, even though in the long run, we 
might have a huge number of these specific adaptation theories. Your efficient algorithm 
can go directly into Discrete.thy.


Best,
Andreas



On 29/06/17 15:29, Manuel Eberl wrote:

Hallo,

I'm considering adding efficient code for Discrete.log (the dual logarithm on natural 
numbers). PolyML does provide an IntInf.log2 function that seems reasonably efficient so 
that one can set up code printing. However, I am struggling with one detail:


Where would the code that does this actually reside? I cannot really put it into 
Discrete.thy, because then that would have to import Code_Target_Numeral. I could put it 
into Code_Target_Integer.thy, but then that would have to import Discrete, which does not 
sound right to me either.


I attached what I have so far.

Manuel



___
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] [isabelle] Good name for "sublist" predicates

2017-06-28 Thread Andreas Lochbihler


Dear all,

While porting some of my theories to the current development version, I've just noticed 
that the renaming of sublisteq to subseq done by Manuel in May (639eb3617a86) has one bad 
effect:


The name subseq is already used in Topological_Spaces to formalise the concept of a 
subsequence. This name is now hidden by the definition in Sublist, in particular when I 
import HOL-Probability.


Can this name clash be eliminated before the next release such that I don't have to write 
Topological_Spaces.subseq everywhere?


Thanks,
Andreas

On 26/05/17 08:16, Tobias Nipkow wrote:
Thank you for your research. I am perfectly happy with "sublist" (for the contiguous case) 
and "subseq" (for the general case) and think we should adopt it.


[Then we would rename sublisteq -> subseq and sublist :: "'a list ⇒ nat set ⇒ 'a list" (in 
List) to something else, eg sublist_index)


Tobias

On 25/05/2017 21:13, Jasmin Blanchette wrote:



On 25.05.2017, at 20:41, Tobias Nipkow  wrote:

I don't think that sublist, subsequence and substring really have much of a bias in 
either direction, except possibly substring, but the latter does indeed sound too 
specialized.


Wikipedia has a clear bias (and I did not edit it, nor did I look it up before writing 
my previous email):


https://en.wikipedia.org/wiki/Subsequence
https://en.wikipedia.org/wiki/Substring

Popular algorithm sbooks like Cormen et al. follow the same definition of subsequence. 
Standard expressions like "longest increasing subsequence" depend on this semantics.


As for sublist, all the examples I see by Googling either "sublist", "is_sublist", 
"isSublist", or "indexOfSubList" in Java, Python, Scala, etc., have the contiguous 
semantics. Including this page:


http://www4.in.tum.de/lehre/praktika/psv/psv98/Vorlesung5/aufg4.html

I'm not saying we should rename the Isabelle concepts, just that Isabelle is the odd 
(wo)man out.


Jasmin




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

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

2017-04-24 Thread Andreas Lochbihler

Sure. Whenever I have to push something to the Isabelle repository, I use the Jenkins 
testboard installation to see whether something broke. It works more reliably than the 
previous testboard infrastructure, which often ignored some commits.


Andreas

On 24/04/17 14:46, Makarius wrote:

This is another attempt to open a discussion about Jenkins at TUM.

Are there users of it outside the TUM group?

What is good about it? What is bad about it?


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] Irrefutable patterns in Haskell and Quickcheck/Narrowing

2017-01-14 Thread Andreas Lochbihler

Hi Florian,

Lukas may be able to answer this question better, but here's a comment: You do not need 
the lazy treatment of irrefutable patterns in Haskell as a primitive, because it is easy 
to emulate using selectors. That is, if we have a single-constructor HOL datatype

dataype 'a T = C (s1: 'a) (s2: 'a T) (s3: 'a T list)

then we can introduce a copy of the case operator by

definition case_lazy_T where "case_lazy_T = case_T"
lemma [code]: "case_lazy_T f x = f (s1 x) (s2 x) (s3 x)"

Now, when you want to use the semantics of irrefutable patterns in let-bindings, use 
case_lazy_T in the code equation. If you really want to force the evaluation, then use 
case_T and compile it with the new scheme.

I have not tried this, but my guess is that if you do it this way for the three types 
narrowing_type narrowing_term narrowing_cons of Quickcheck_Narrowing and adjust the code 
equations for the constants in Quickcheck_Narrowing accordingly, then you get back the old 
behaviour.

Hope this helps,
Andreas

On 14/01/17 09:33, Florian Haftmann wrote:

Hi Lukas,

I am currently stuck with a problem in Quickcheck/Narrowing.

After about 10 years it came to surface that code generation for Haskell
may produce irrefutable patterns due to pattern bindings in let clauses.
See ; if I understand
 correctly that
particular semantics allows fancy definitions like the following
fibonacci one-liner: »fib @ (1 : more_fib) = 1 : 1 : [ a + b | (a, b) <-
zip fib more_fib ]«.

However the partial correctness approach of the code generator assumes
that pattern match clauses may silently be dropped, which is made use of
to translate the HOL-ish »partial« undefined conveniently. This breaks
down in presence of irrefutable patterns (see the post on isabelle-users
by Rene Thiemann).

The correction is obvious: for Haskell, only local variables may be
bound by let clauses, but never patterns – these are solely bound by
case clauses, which are strict in Haskell (as in function equations).

This however breaks Quickcheck/Narrowing where the lazy nature of
pattern bindings has been exploited, may be unconsciously. A minimal
example is attached (Quickcheck_Narrowing_Examples.thy) but I also
distilled the generated Haskell code:

The same before and after:
Typerep.hs

Then the difference occurs:
Generated_Code.hs
Before: Generated_Code.A.hs
After: Generated_Code.B.hs

The same before and after:
Narrowing_Engine.hs
Main.hs

The diff ist straight-forward to read:

93,102c93,106
<   let {
< (Narrowing_cons (Narrowing_sum_of_products ps) cfs) = f d;
< (Narrowing_cons ta cas) = a (d - (1 :: Prelude.Int));
< shallow = (0 :: Prelude.Int) < d && non_empty ta;
< aa = (if shallow then map (\ cf (x : xs) -> cf xs (conv cas x)) 
cfs
 ta : ab) ps else []))
<  aa;
---
>   (case f d of {
> Narrowing_cons (Narrowing_sum_of_products ps) cfs ->
>   (case a (d - (1 :: Prelude.Int)) of {
> Narrowing_cons ta cas ->
>   let {
> shallow = (0 :: Prelude.Int) < d && non_empty ta;
> aa = (if shallow then map (\ cf (x : xs) -> cf xs (conv 
cas x)) cfs
>else []);
>   } in Narrowing_cons
>  (Narrowing_sum_of_products
>(if shallow then map (\ ab -> ta : ab) ps else []))
>  aa;
>   });
>   });
112,115c116,122
<   let {
< (Narrowing_cons (Narrowing_sum_of_products ssa) ca) = a d;
< (Narrowing_cons (Narrowing_sum_of_products ssb) cb) = b d;
<   } in Narrowing_cons (Narrowing_sum_of_products (ssa ++ ssb)) (ca ++ 
cb);
---
>   (case a d of {
> Narrowing_cons (Narrowing_sum_of_products ssa) ca ->
>   (case b d of {
> Narrowing_cons (Narrowing_sum_of_products ssb) cb ->
>   Narrowing_cons (Narrowing_sum_of_products (ssa ++ ssb)) (ca 
++ cb);
>   });
>   });

Unfortunately my knowledge is too restricted what could be done here to
restore the intended behaviour economically.

Hence I ask whether you have an idea what is going wrong here.

Thanks a lot!

Florian

___
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] [isabelle] print_statement does not quote variables with reserved names

2016-10-28 Thread Andreas Lochbihler


On 28/10/16 17:03, Makarius wrote:

BTW, there is strictly speaking no need to use fix/assume/show, since
show if/for is already possible, although relatively rarely used.


I use show/if/for regularly in my work (just look at the AFP entry MFMC_Countable to see a 
few examples), but fix/assume/show is more convenient if the proof needs intermediate 
"have" steps between the "assume" and the "show". The show/if/for pattern is possible in 
this case, but I'd have to open another "proof - have ... show ?thesis ... qed" block, 
which introduces clutter and unnecessary indentation.


Also, if there are several goals with the same assumptions, fix/assume/show/show/show/... 
is more concise than having to repeat the assumptions for every show (if each goal needs a 
different proof method invocation).


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

Re: [isabelle-dev] Of lazy lists and friendly corecs

2016-10-07 Thread Andreas Lochbihler


Hi Manuel,

I've played around a bit with lmerge. It magically works if you replace the selectors with 
case statements (in Isabelle/5c2c559f01eb):


friend_of_corec lmerge :: "int llist ⇒ int llist ⇒ int llist" where
  "lmerge xs ys =
   (case xs of LNil ⇒ (case ys of LNil ⇒ LNil | LCons y ys' ⇒ LCons y ys')
| LCons x xs' ⇒ (case ys of LNil ⇒ LCons x xs' | LCons y ys' ⇒
   if x ≤ y then LCons x (lmerge xs' ys)
   else LCons y (lmerge xs ys')))"
  subgoal by(subst lmerge.code)(simp split: llist.split)
  subgoal by transfer_prover
  done

Hope this helps,
Andreas

On 07/10/16 14:22, Manuel Eberl wrote:

Hallo,

I've been playing around with corec and friends in combination with the lazy 
lists from
"$AFP/Coinductive/Coinductive_List" and encountered the following problem:

Suppose I want a function that takes two (implicitly sorted) lazy lists and 
merges them in
the following fashion:

primcorec lmerge :: "int llist ⇒ int llist ⇒ int llist" where
  "lmerge xs ys = (if lnull xs then ys
   else if lnull ys then xs
   else if lhd xs ≤ lhd ys then LCons (lhd xs) (lmerge (ltl xs) 
ys)
   else LCons (lhd ys) (lmerge xs (ltl ys)))"

I've still not fully understood what ‘friendly’ means, but I should be very 
surprised if
this function were not friendly. So I tried this:

friend_of_corec lmerge where
  "lmerge xs ys = (if lnull xs ∧ lnull ys then LNil
   else if lnull xs then LCons (lhd ys) (ltl ys)
   else if lnull ys then LCons (lhd xs) (ltl xs)
   else if lhd xs ≤ lhd ys then LCons (lhd xs) (lmerge (ltl xs) 
ys)
   else LCons (lhd ys) (lmerge xs (ltl ys)))"

Unfortunately, I get the following error:

exception TYPE raised (line 168 of "consts.ML"): Illegal type for constant
"Coinductive_List.llist.LNil" :: 'b

I now have the following questions:
1. Something like "if lnull xs then ys" works in primcorec, but in corec and
friend_of_corec I have to do odd things like "LCons (lhd ys) (ltl ys)". Is that 
a known
limitation?
2. What is the relationship between primcorec and friendliness? If I have a 
function
defined by primcorec, is the additional step with friend_of_corec fundamentally 
necessary
or is that just a technical issue? (I would have naïvely assumed that
primitively-corecursive functions are always friendly or something like that)
3. What causes the above error and how do I get around it?


Cheers,

Manuel




___
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] Of lazy lists and friendly corecs

2016-10-07 Thread Andreas Lochbihler

Hi Manuel,

a function is friendly if it produces at least one constructor after applying at most one 
constructor to the codatatype argument. This does not have anything to do with primitive 
corecursion, because the codatatype result type need not be a argument type---and even if 
it is, there are primcorec functions which are not friendly, e.g.,

primcorec odds :: "'a stream => 'a stream"
where "odds xs = SCons (shd xs) (odds (stl (stl xs)))"

I leave it to Dmitriy and Jasmin to reply to your problem with the error message about 
lmerge. But in theory this should work (and in fact I've already done it for streams).

> 1. Something like "if lnull xs then ys" works in primcorec, but in corec and
> friend_of_corec I have to do odd things like "LCons (lhd ys) (ltl ys)". Is 
that a known
> limitation?
Yes, this is known to us, but we currently don't have the time to implement all the 
preprocessing features of primcorec for friend_of_corec.

Best,
Andreas

On 07/10/16 14:22, Manuel Eberl wrote:

Hallo,

I've been playing around with corec and friends in combination with the lazy 
lists from
"$AFP/Coinductive/Coinductive_List" and encountered the following problem:

Suppose I want a function that takes two (implicitly sorted) lazy lists and 
merges them in
the following fashion:

primcorec lmerge :: "int llist ⇒ int llist ⇒ int llist" where
  "lmerge xs ys = (if lnull xs then ys
   else if lnull ys then xs
   else if lhd xs ≤ lhd ys then LCons (lhd xs) (lmerge (ltl xs) 
ys)
   else LCons (lhd ys) (lmerge xs (ltl ys)))"

I've still not fully understood what ‘friendly’ means, but I should be very 
surprised if
this function were not friendly. So I tried this:

friend_of_corec lmerge where
  "lmerge xs ys = (if lnull xs ∧ lnull ys then LNil
   else if lnull xs then LCons (lhd ys) (ltl ys)
   else if lnull ys then LCons (lhd xs) (ltl xs)
   else if lhd xs ≤ lhd ys then LCons (lhd xs) (lmerge (ltl xs) 
ys)
   else LCons (lhd ys) (lmerge xs (ltl ys)))"

Unfortunately, I get the following error:

exception TYPE raised (line 168 of "consts.ML"): Illegal type for constant
"Coinductive_List.llist.LNil" :: 'b

I now have the following questions:
1. Something like "if lnull xs then ys" works in primcorec, but in corec and
friend_of_corec I have to do odd things like "LCons (lhd ys) (ltl ys)". Is that 
a known
limitation?
2. What is the relationship between primcorec and friendliness? If I have a 
function
defined by primcorec, is the additional step with friend_of_corec fundamentally 
necessary
or is that just a technical issue? (I would have naïvely assumed that
primitively-corecursive functions are always friendly or something like that)
3. What causes the above error and how do I get around it?

Cheers,

Manuel

___
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] Problem with factorial-ring in combination with containers

2016-10-04 Thread Andreas Lochbihler


Hi Manuel,

My point with "finite" was that for the current default setup, you don't need any type 
class instantiations (see the code equations below). Only if someone imports Card_UNIV 
from HOL/Library (e.g., for FinFun or for Containers), he or she has to do the 
instantiations for finite_UNIV for the types on which they want to execute big operators. 
But most users do not import Card_UNIV, so they are not affected.


Using a copy of "finite" is also possible and maybe even a good idea. The existing 
constant "finite" is an important concept in many theorems. Using a copy "finite_code" in 
the code equations separates code generation from logical reasoning, which is often a good 
thing. However, if we then implement the existing constant "finite" using the equation


  "finite = finite_code"

then we have not gained much and introduced some amount of duplication. And if we stick to 
the existing setup for "finite" with


  "finite (set xs) = True"
  "finite (List.coset ys) = Code.abort ... ..."

then we run into the very same pattern-match problems that René reported. If we delete all 
code equations for "finite", then this renders quickcheck a little bit less useful, 
because it can no longer work on theorems involving finiteness. But I am not sure how much 
quickcheck can do in practice for theorems involving "finite".


Andreas

On 03/10/16 22:51, Manuel Eberl wrote:

Hm, that sounds reasonable.

However, I am not sure whether using "finite" is really such a good
idea; it will lead to people having to instantiate "finite_UNIV" for all
kinds of things all the time.

I think I once considered a similar solution using a copy of "finite"
that does Code.abort in cases where finiteness wasn't obvious (e.g.
complement), but I abandoned that idea for some reason. Still, at the
moment, I think that might be the best solution.

Any thoughts?

Manuel


On 03/10/16 17:37, Andreas Lochbihler wrote:

Hi Manuel,

Indeed, generic iteration over a set is only well-defined if the set is
finite. For an infinite set, the generic iteration combinator returns an
unspecified value, not 0 or 1. In fact, I had imagined a code equation
like you described, namely

  "Gcd A = (if finite A then ... else Code.abort (Gcd A))"

Note that this does *not* pull in finite_UNIV. We could implement the
finiteness test by

  "finite (set xs) = True"
  "finite (List.coset ys) = Code.abort (STR ''Finiteness test on
Complement'') ..."

If one imports HOL/Library/Card_UNIV or Containers, then one has to
provide instances for finite_UNIV and a bunch of other type classes
anyways. That's the price of using more complicated libraries.

AFAICS, it does not really matter whether the iteration combinator takes
an additional argument, because they can be expressed in terms of each
other:

  fold_default dflt f A x = (if finite A then dflst A else
Finite_Set.fold f A x)
  Finite_Set.fold f A x = fold_default (%A. THE ... A ...) f A x

The advantage of fold_default with a default value is that the
finiteness test remains inside the implementation library B whereas with
Finite_Set.fold, the finiteness test must be done whenever one wants to
use the combinator. So this might be an argument in favour of fold_default.

Andreas

On 03/10/16 16:27, Manuel Eberl wrote:

I'm afraid it's not quite as easy as that. You cannot use the existing
combinators for comp_fun_commute for Gcd. For infinite sets, these
combinators return the neutral element (i.e. "0" for Gcd and "1" for
Lcm), but not every infinite set has Gcd 0 or Lcm 1. For setsum/setprod,
this works because it is quite simply defined that way, but for Gcd/Lcm
it is not.

So the alternative would be something like "Gcd A = (if finite A then
 else Code.abort …)". This does not work well either,
because it requires being able to decide "finite A", which typically
introduces the unwanted typeclass requirement "finite_UNIV".

My suggestion would be a combinator that, in order to implement a
function f :: 'a set => 'a, takes as arguments both a fold operation of
type "'a cfc" /and/ the function f itself.

It then performs the fold on any "finite by construction" set (e.g. sets
represented by the "set" constructor) and returns "Code.abort … (f A)"
for anything else (e.g. a set represented by the "coset" constructor).

I planned on implementing this at some point, but I've quite a bit of
other stuff to do and I wanted to discuss it first, so I never really
got around to doing it.

Cheers,

Manuel


On 03/10/16 16:15, Andreas Lochbihler wrote:

Hi René and Manuel,

Indeed, for sets, expressing the code equations in terms of a generic
iteration operation on sets would do the job for most of the cases. The
comp_fun_commute and comp_fu

Re: [isabelle-dev] Problem with factorial-ring in combination with containers

2016-10-03 Thread Andreas Lochbihler

Hi Manuel,

Indeed, generic iteration over a set is only well-defined if the set is finite. For an
infinite set, the generic iteration combinator returns an unspecified value, not 0 or 1.
In fact, I had imagined a code equation like you described, namely

"Gcd A = (if finite A then ... else Code.abort (Gcd A))"

Note that this does *not* pull in finite_UNIV. We could implement the
finiteness test by

"finite (set xs) = True"
"finite (List.coset ys) = Code.abort (STR ''Finiteness test on Complement'')
..."

If one imports HOL/Library/Card_UNIV or Containers, then one has to provide instances for
finite_UNIV and a bunch of other type classes anyways. That's the price of using more
complicated libraries.

AFAICS, it does not really matter whether the iteration combinator takes an additional
argument, because they can be expressed in terms of each other:

fold_default dflt f A x = (if finite A then dflst A else Finite_Set.fold f A
x)
Finite_Set.fold f A x = fold_default (%A. THE ... A ...) f A x

The advantage of fold_default with a default value is that the finiteness test remains
inside the implementation library B whereas with Finite_Set.fold, the finiteness test must
be done whenever one wants to use the combinator. So this might be an argument in favour
of fold_default.

Andreas

On 03/10/16 16:27, Manuel Eberl wrote:

I'm afraid it's not quite as easy as that. You cannot use the existing
combinators for comp_fun_commute for Gcd. For infinite sets, these
combinators return the neutral element (i.e. "0" for Gcd and "1" for
Lcm), but not every infinite set has Gcd 0 or Lcm 1. For setsum/setprod,
this works because it is quite simply defined that way, but for Gcd/Lcm
it is not.

So the alternative would be something like "Gcd A = (if finite A then
else Code.abort …)". This does not work well either,
because it requires being able to decide "finite A", which typically
introduces the unwanted typeclass requirement "finite_UNIV".

My suggestion would be a combinator that, in order to implement a
function f :: 'a set => 'a, takes as arguments both a fold operation of
type "'a cfc" /and/ the function f itself.

It then performs the fold on any "finite by construction" set (e.g. sets
represented by the "set" constructor) and returns "Code.abort … (f A)"
for anything else (e.g. a set represented by the "coset" constructor).

I planned on implementing this at some point, but I've quite a bit of
other stuff to do and I wanted to discuss it first, so I never really
got around to doing it.

Cheers,

Manuel

On 03/10/16 16:15, Andreas Lochbihler wrote:

Hi René and Manuel,

Indeed, for sets, expressing the code equations in terms of a generic
iteration operation on sets would do the job for most of the cases. The
comp_fun_commute and comp_fun_idem types in Containers precisely do
this, but they have not been integrated in the HOL library yet. They
should work all kinds of big operators (setsum, setprod, Gcd, etc) and
could be added to the HOL library.

Of course, some special case tricks no longer work if go for a generic
iteration operation. For example, one could prove "Gcd (List.coset xs) =
1" for natural numbers and declare a code equation. Such things would no
longer be possible, but I am not sure whether they are done at all at
the moment.

Manuel's suggestion of code_abort is a bit cleaner than René's use
Code.abort, because Code.abort does not work with normalisation by
evaluation whereas code_abort does.

Best,
Andreas

On 03/10/16 15:29, Manuel Eberl wrote:

This is a problem that I have given quite some thought in the past. The
problem is the following: You have a theory A providing certain
operations on sets (in this case: Gcd) and a theory B providing
implementations for sets (in this case: Containers).

The problem is that the code equations for the operations from A depend
on the implementation that is chosen for sets. A cannot give code
equations for every possible implementation of sets, while B cannot
possibly import every theory that has operations involving sets and give
code equations for it.

The best possible solution would be to imitate the way it is currently
done for setsum, setprod, etc: Define a sufficiently general combinator
that iterates over the set and give the code equations in A in terms of
this combinator. Then B only has to reimplement this generic combinator.

That would be the cleanest solution, but I'm not sure how such a
combinator would look like. The folding operation would probably have to
satisfy some associativity/commutativity laws and have that information
available at the type level (similar to the cfc type in Containers).

By the way, my current workaround for this problem is to declare all
problematic constants as "code_abort".

Cheers,

Manuel

On 03/10/16 15:21, Thiemann, Rene wrot

Re: [isabelle-dev] Problem with factorial-ring in combination with containers

2016-10-03 Thread Andreas Lochbihler

Hi René and Manuel,

Indeed, for sets, expressing the code equations in terms of a generic iteration operation
on sets would do the job for most of the cases. The comp_fun_commute and comp_fun_idem
types in Containers precisely do this, but they have not been integrated in the HOL
library yet. They should work all kinds of big operators (setsum, setprod, Gcd, etc) and
could be added to the HOL library.

Of course, some special case tricks no longer work if go for a generic iteration
operation. For example, one could prove "Gcd (List.coset xs) = 1" for natural numbers and
declare a code equation. Such things would no longer be possible, but I am not sure
whether they are done at all at the moment.

Manuel's suggestion of code_abort is a bit cleaner than René's use Code.abort, because
Code.abort does not work with normalisation by evaluation whereas code_abort does.

Best,
Andreas

On 03/10/16 15:29, Manuel Eberl wrote:

By the way, my current workaround for this problem is to declare all
problematic constants as "code_abort".

Cheers,

Manuel

On 03/10/16 15:21, Thiemann, Rene wrote:

Dear all,

in the following theory, the export-code fails:

(Isabelle 957ba35d1338, AFP 618f04bf906f)

theory Problem
imports
"~~/src/HOL/Library/Polynomial_Factorial"
"$AFP/thys/Containers/Set_Impl"
begin

definition foo :: "'a :: factorial_semiring_gcd ⇒ 'a ⇒ 'a" where
"foo x y = gcd y x"

definition bar :: "int ⇒ int" where
"bar x = foo x (x - 1)"

export_code bar in Haskell
end

The problem arises from two issues:
- factorial_semiring_gcd requires code for
Gcd :: “Set ‘a => ‘a”, not only for the binary “gcd :: ‘a => ‘a => ‘a”!
- the code-equation for Gcd is Gcd_eucl_set: "Gcd_eucl (set xs) = foldl
gcd_eucl 0 xs”
where “set” is only a constructor if one does not load the container-library.

It would be nice, if one can either alter factorial_semiring_gcd so that it
does not
require “Gcd” anymore, or if the code-equation is modified in a way that permits
co-existence with containers. (Of course, similarly for Lcm).

With best regards,
Akihisa, Sebastiaan, and René

PS: We currently solve the problem by disabling Gcd and Lcm as follows:

lemma [code]: "(Gcd_eucl :: rat set ⇒ rat) = Code.abort (STR ''no Gcd on sets'') (λ
_. Gcd_eucl)" by simp
lemma [code]: "(Lcm_eucl :: rat set ⇒ rat) = Code.abort (STR ''no Lcm on sets'') (λ
_. Lcm_eucl)" by simp
___
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] NEWS: Rename HOL-Multivariate_Analysis to HOL-Analysis and move measure theory from HOL-Probability to HOL-Analysis

2016-08-08 Thread Andreas Lochbihler


Hi Johannes,

You could define the syntax for has_integral to be literally

  "(f Bochner.has_integral x) s"

and similarly for the other. Additionally, you could declare bundles with the existing 
notation


  "(f has_integral x) s"

for both of them (like is nowadays done for the Lifting package syntax). Then, you can 
locally include the notation for the desired integral with "includes", which is more 
flexible than a locale interpretation.


Andreas

On 08/08/16 16:57, Johannes Hölzl wrote:

Am Montag, den 08.08.2016, 15:03 +0100 schrieb Lawrence Paulson:

Thank you for making this change!



My idea would be to rename both integrals into something like:
  has_bc_integral, bc_integrable, bc_integral,
  has_hk_integral, hk_integrable, hk_integral
and consequently rename the integral theorems.

I would greatly prefer renaming the relevant theories instead so that
we have Bochner.has_integral versus Gauge.has_integral, etc. That is
the point of having compound names. I would go so far as to suggest
that equivalent theorems with slightly different names should be
rationalised.


I would prefer this too,  but has_integral is not a name. It is special
syntax, one writes:   (f has_integral x) s

Either we remove the syntax (and add it to a locale to be interpreted
locally) or rename it. Unfortunately the first option is still
problematic. For example, one needs to setup a context to use it, and
then one is not allowed to enter a locale context.

Another problem is that the theory which gets loaded later is always
slightly preferred as it does not need the theory prefix. Only way to
avoid this would be to hide the theorem names. Or put it in a context
and add the "qualified" command prefix.

Unifying the different names (i.e. integral_minus, sub, diff, uminus,
cmult, mult_left, ...) is also on my TODO list.

 - Johannes






___
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] NEWS: proof outline with cases

2016-08-08 Thread Andreas Lochbihler


Hi Makarius,

Just a quick feedback on the proof outlines: they are great! But sometimes quotes are 
needed around the case name (e.g., if it is a keyword like "try" or "oracle", or if it is 
a case of an induction rule by the function package for an equation which has been split 
up by the sequential option, i.e., 3_1 and 3_2). Could you add the missing quotes to the 
outline?


(For reference: tested with Isabelle/eca71be9c948)

Best,
Andreas

On 16/07/16 13:14, Makarius wrote:

*** Prover IDE -- Isabelle/Scala/jEdit ***

* Command 'proof' provides information about proof outline with cases,
e.g. for proof methods "cases", "induct", "goal_cases".


This refers to Isabelle/6c46a1e786da. The main functionality is in
Isabelle/9f8d06f23c09, which also demonstrates how to do such things
with existing PIDE infrastructure.


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] Build NEWS

2016-07-11 Thread Andreas Lochbihler

For published versions, there probably should not be any /devel-entries links. But for 
papers under submission, people may have updated their AFP entries and want the reviewers 
to access the updated material. At least that is what I used to do for many ITP 
submissions. So it might be good to keep the /devel-entries URLs alive at least for some 
transition period.


Andreas

On 11/07/16 08:09, Gerwin Klein wrote:

On 11 Jul 2016, at 16:03, Johannes Hölzl  wrote:


Am Sonntag, den 10.07.2016, 22:37 +0200 schrieb Lars Hupel:

Dear AFP developers,

some of you may have noticed that the "AFP devel" pages have not been
updated since April. This is partly my fault because I migrated the
infrastructure and partly not my fault because the scripts to produce
these pages make a lot of assumptions about the infrastructure :-)

Anyway, there's now a reboot of these pages available at:

   

Note that this is a preview: The status is still [skipped] everywhere
and most download links don't work. This will be fixed some time this
week.

As soon as that's done, the old links ("/devel-entries" and the like)
will go offline.


Can't we just let the /devel-entries redirect to http://devel. ?


That would not be too hard, but



I’m sure there are quite some papers which reference the /devel entries.


I should hope not - they make no sense to cite, because their whole purpose is 
to change on a daily basis.

Cheers,
Gerwin



The information in this e-mail may be confidential and subject to legal 
professional privilege and/or copyright. National ICT Australia Limited accepts 
no liability for any damage caused by this email or its attachments.
___
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] lifting syntax with proper symbols

2016-03-04 Thread Andreas Lochbihler


Hi Makarius,

How about LaTeX \Mapsto for ===>? This is what I use in my papers following Ondrej and 
Brian's paper on lifting.


I'd be happy to have syntax for ===> enabled by default, as it makes transfer and 
parametricity rules much easier to read. I have no opinion on --->.


Andreas

On 04/03/16 11:56, Makarius wrote:

Isabelle2016 has removed quite a lot of old ASCII syntax, and made Isabelle 
symbols the
default where old ASCII syntax is still available.

A notable exception is lifting_syntax with its old-style ASCII-only notation, 
see
http://isabelle.in.tum.de/repos/isabelle/annotate/aeee0a4be6cf/src/HOL/Transfer.thy#l19

locale lifting_syntax
begin
   notation rel_fun (infixr "===>" 55)
   notation map_fun (infixr "--->" 55)
end


I can imagine two reforms:

   * Use proper symbols for these operators (without keeping ASCII
 replacement syntax).

   * Make the notation a global default, i.e. remove the locale and its
 interpretations in applications.


The usual question is which symbols are best.

===> appears to be more frequently used than --->. Based on that observation, 
the new
triple-line arrow ⇛ could be used for ===>, and maybe a bold → for --->.

This is only a first idea. There are many possibilities. It is also possible to 
add new
glyphs to the Isabelle fonts, as long as there are canonical LaTeX macros for 
that and
some code points in the Unicode charts that many be (ab)used for our 
application.

Recent examples of Unicode ab-use in Isabelle symbol interpretation are:

⤏
⇢
⤜
⪢

These need to be viewed in Isabelle/jEdit to see the point: the official shape 
of the
glyph serves as crude approximation for the intended meaning in Isabelle.


 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] Maintenance work on Jenkins VM

2016-02-01 Thread Andreas Lochbihler

Native_Word should work again in 203deaf5208d (see also 61aeecc4093d), both with GHC 7.8 
and GHC 7.10.


Andreas

On 01/02/16 08:32, Andreas Lochbihler wrote:

Hi Lars,

The theory Uint comes from Native_Word. I'll have a look and see whether this 
can be fixed.

Andreas

On 31/01/16 22:21, Lars Hupel wrote:

* archival of the build logs


As a temporary solution, I have now configured Jenkins to retain all
build logs. I've found some pointers how to make Jenkins store them into
some database, but will need to investigate further.


* installing compilers and setting the various
ISABELLE_GHC/ISABELLE_OCAMLC etc. for Codegenerator_Test


This is also done now. For Haskell, it immediately uncovered a problem:

   <https://ci.isabelle.systems/jenkins/job/isabelle-repo-afp/3/console>

Uint.hs:15:48:
 Ambiguous occurrence `Word'
 It could refer to either `Uint.Word', defined at Uint.hs:12:1
   or `Data.Word.Word',
  imported from `Prelude' at Uint.hs:3:8-11
  (and originally defined in `GHC.Types')
### theory "Impl_Uv_Set"
### 14.656s elapsed time, 16.840s cpu time, 0.572s GC time
*** Failed to load theory "GenCF" (unresolved "Impl_Uv_Set")
*** Code check failed for Haskell: "$ISABELLE_GHC" -XEmptyDataDecls
-XRankNTypes -XScopedTypeVariables -odir build -hidir build -stubdir
build -e "" Generated_Code.hs
*** At command "export_code" (line 384 of
"~~/afp/thys/Collections/GenCF/Impl/Impl_Uv_Set.thy")

This is a legitimate failure, using GHC 7.10.3. The other build machines
use the (outdated) GHC 7.8.x series. Shall I downgrade GHC or would
someone (Florian, Peter?) fix the compilation problem?

Cheers
Lars
___
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] Maintenance work on Jenkins VM

2016-01-31 Thread Andreas Lochbihler


Hi Lars,

The theory Uint comes from Native_Word. I'll have a look and see whether this 
can be fixed.

Andreas

On 31/01/16 22:21, Lars Hupel wrote:

* archival of the build logs


As a temporary solution, I have now configured Jenkins to retain all
build logs. I've found some pointers how to make Jenkins store them into
some database, but will need to investigate further.


* installing compilers and setting the various
ISABELLE_GHC/ISABELLE_OCAMLC etc. for Codegenerator_Test


This is also done now. For Haskell, it immediately uncovered a problem:

   

Uint.hs:15:48:
 Ambiguous occurrence `Word'
 It could refer to either `Uint.Word', defined at Uint.hs:12:1
   or `Data.Word.Word',
  imported from `Prelude' at Uint.hs:3:8-11
  (and originally defined in `GHC.Types')
### theory "Impl_Uv_Set"
### 14.656s elapsed time, 16.840s cpu time, 0.572s GC time
*** Failed to load theory "GenCF" (unresolved "Impl_Uv_Set")
*** Code check failed for Haskell: "$ISABELLE_GHC" -XEmptyDataDecls
-XRankNTypes -XScopedTypeVariables -odir build -hidir build -stubdir
build -e "" Generated_Code.hs
*** At command "export_code" (line 384 of
"~~/afp/thys/Collections/GenCF/Impl/Impl_Uv_Set.thy")

This is a legitimate failure, using GHC 7.10.3. The other build machines
use the (outdated) GHC 7.8.x series. Shall I downgrade GHC or would
someone (Florian, Peter?) fix the compilation problem?

Cheers
Lars
___
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] AFP status

2016-01-12 Thread Andreas Lochbihler


Applicative_Lifting and Stern_Brocot now (AFP/1c0036f62a32) work with 
Isabelle/adcaaf6c9910.

Andreas

On 13/01/16 00:06, Makarius wrote:

The AFP status is much better than last week, but these sessions are still 
broken
(Isabelle/7355fd313cf8 and AFP/87337b54f3eb):

   Applicative_Lifting
   Stern_Brocot
   Sturm_Tarski

In this hot phase of release preparation, we need things continuosly working.


 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] HOL-Codegenerator_Test error

2016-01-12 Thread Andreas Lochbihler


Dear Manuel,

I have not tried this explicitly, but it looks like the standard problem with type classes 
in Scala (see section 7.1 in the code generator tutorial). Probably the problematic code 
equations use two type classes with an operation inherited from the same anchestor. The 
error message in the start of this thread hints at this problem. So you best introduce a 
special type class for Scala (as has already been done for others in the code generator 
tests).


Hope this helps,
Andreas

On 12/01/16 09:56, Manuel Eberl wrote:

I tried to trace this issue and I am really confused now.

The problem is apparently the following code equation I added for "binomial" at 
the end of
Binomial.thy:

lemma binomial_code [code]:
   "(n choose k) =
   (if k > n then 0
   else if 2 * k > n then (n choose (n - k))
   else (fold_atLeastAtMost_nat (op *) (n-k+1) n 1 div fact k))"

If I delete this rule, everything works again. I then tried the following, 
which also
produces the same error:

lemma binomial_code [code]:
"n choose k = (if k ≤ n then fact n div (fact k * fact (n - k)) else 0)"


The following two, on the other hand, work:

lemma binomial_code [code]:
"0 choose k = (if k = 0 then 1 else 0)"
"Suc n choose k = (if k = 0 then 1 else (n choose (k - 1)) + (n choose k))"

lemma binomial_code [code]:
"n choose k = (if k = 0 then 1 else if n = 0 then 0 else ((n - 1) choose (k - 
1)) + ((n -
1) choose k))"


So I thought maybe the "fact" is the problem, but the following works as well, 
even though
it contains "fact":

lemma binomial_code [code]:
   "n choose k =
  (if k = 0 then 1 else if n = 0 ∧ fact n = fact n then 0 else ((n - 1) 
choose (k -
1)) + ((n - 1) choose k))"


Does anybody have any idea what is going on here?


Manuel
___
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] Problem with code generation for non-executable types

2016-01-08 Thread Andreas Lochbihler


Hi Johannes,


 Then the dictionary construction for type constructors does not
 work in ML! The type signature would be the following:

   val test_prod : ('a * 'b) filter

 Which apparently is not allow in ML.
This is the famous value restriction (which I also regularly run into). The standard 
solution is to add a unit closure, because functions may be polymorphic in ML.


Andreas


2.  If your type class contains non-computable data, i.e.

   instantiation bool :: test_class
   begin

   definition "test = if P = NP then top else bot"

   instance proof qed
   end

 You get a non-terminating program at the time point when the
 dictionary for bool :: test_class is constructed. When the
 code equation is hidden with [code del] one gets a exception!

3.  Our current solution is to introduce code_datatype Abs_filter
 Rep_filter [code del] and define for each uniformity:

   uniformity = Abs_filter (%P. Code.abort (STR''FAILED'') (Rep_filter test 
P))

 @Florian: is the an alternative solution?


- Johannes

PS: Here is a short, concrete example:

theory Scratch
   imports Complex_Main
begin

class test_class =
   fixes test :: "'a filter"

instantiation prod :: (test_class, test_class) test_class
begin

definition [code del]: "test = (test ×⇩F test :: ('a × 'b) filter)"

instance proof qed
end

instantiation unit :: test_class
begin

definition [code del]:
   "(test :: unit filter) = bot"

instance proof qed
end

definition "test2 (x::'a::test_class) = (Suc 0)"
definition "test3 = test2 ((), ())"

value [code] "test3"

section ‹Solution›

code_datatype Abs_filter
declare [[code abort: Rep_filter]]

lemma test_Abort: "test = Abs_filter (λP. Code.abort (STR ''test'')
(λx. Rep_filter test P))"
   unfolding Code.abort_def Rep_filter_inverse ..

declare test_Abort[where 'a="'a::test_class * 'b :: test_class", code]
declare test_Abort[where 'a=unit, code]

end






Am Freitag, den 08.01.2016, 09:56 +0100 schrieb Johannes Hölzl:

Hi,

I want to introduce uniform spaces in HOL, for this I need to
introduce
a type class of the form (see the attached bundle):

   class uniformity =
 fixes uniformity :: "('a × 'a) filter"

Note that uniformity is a filter and not a function.

which sits between topological spaces and metric spaces, i.e. every
metric type is also in the following type classes:

   class open_uniformity = "open" + uniformity +
 assumes open_uniformity: "⋀U. open U ⟷ (∀x∈U. eventually (λ(x',
y). x' = x ⟶ y ∈ U) uniformity)"

   class uniformity_dist = dist + uniformity +
 assumes uniformity_dist: "uniformity = (INF e:{0 <..}. principal
{(x, y). dist x y < e})"

Everything works fine until Affinite_Arithmetic, there in
Intersection.thy the code generation fails with the following ML
error:

   Error: Type mismatch in type constraint.
  Value: {uniformity = uniformity_proda} : {uniformity: 'a}
  Constraint: ('a * 'b) uniformity
  Reason:
 Can't unify 'a to (('a * 'b) * ('a * 'b)) filter
(Type variable is free in surrounding scope)
   {uniformity = uniformity_proda} : ('a * 'b) uniformity
   At (line 1619 of "generated code")
   Exception- Fail "Static Errors" raised

I assume this is a strange interaction btw code_abort and the fact
that
uniformity is a filter (datatype 'a filter = _EMPTY) and not a
function.

Does anybody know how to avoid such kind of errors? Do I need to
sprinkle more [code del] or code_abort annotations?

  - Johannes

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

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


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

Re: [isabelle-dev] CoreC++ broken

2016-01-04 Thread Andreas Lochbihler

I had a look and it should work now in 1cdd27b5d78a (with Isabelle2016-RC0). I do not know 
what exactly went wrong or what caused the failure. The problem seems to be related to 
some change in theory imports. It seems as if code_pred cannot retrieve the specification 
of a constant under certain import orders, but I am not familiar enough with these 
Isabelle internals to pinpoint the problem.


Andreas

On 30/12/15 00:20, Makarius wrote:

AFP/CoreC++ is broken (already quite some time).

The current situation:

Isabelle/a70b89a3e02e
AFP/a2c981ab8d39

CoreC++ FAILED
*** Failed to load theory "CoreC++" (unresolved "Execute")
*** No such predicate: "SubObj.path_via"
*** At command "code_pred" (line 214 of 
"~/isabelle/afp-devel/thys/CoreC++/Execute.thy")


 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] find_theorems and type class axioms

2015-11-26 Thread Andreas Lochbihler

Hi Larry,

Type inferences assigns to "dist" the type "'a => 'a => real" where 'a :: metric_space,
and to "norm" the type "'b => real" where 'b :: real_normed_vector (due to the type
constraint manipulations in Real_Vector_Spaces.thy. The theorem dist_norm uses dist and
norm with the sort dist_norm. Consequently, it can find this theorem only if metric_space
and real_normed_vector are both subclasses of dist_norm, but they are not. Thus, it is not
found.

In your concrete application, you can nevertheless apply the theorem dist_norm, because
you have a concrete type (e.g. real) which instantiates both real_normed_vector and
metric_space.

As Florian said, the problem here is really the manipulation of the type for dist and
norm. Maybe Johannes can remember why Brian introduced this.

Best,
Andreas

On 26/11/15 14:34, Lawrence Paulson wrote:

On 26 Nov 2015, at 11:58, Florian Haftmann
wrote:

The sort constraints of constants play *no* role for
searching theorems. The sort constraints of terms to be searched *do*,
and in my view this is the desired behaviour: if I formulate a property
on partial orders, I do not want to be bothered by facts which only
apply to linear orders.

I’m not sure that I understand this statement. At what point do constants
become terms anyway? Consider the following search:

"_<=_" "_=_”

There are two terms, but they are nothing but constants. No theory is implied
(I’m not sure how one could express a search that was specifically about
partial orders that were not linear), and there are more than 2000 hits. They
include statements involving natural numbers, integers and sets. In fact it
would be good to find a way of excluding some of those.

Meanwhile, the search

norm dist

contains only constants, and nevertheless it fails to pick up dist_norm: "dist
x y = norm (x - y)”.

Larry

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

Re: [isabelle-dev] find_theorems and type class axioms

2015-11-19 Thread Andreas Lochbihler


Hi Larry and Florian,

the sort constraints for open, dist, and norm are changed in

http://isabelle.in.tum.de/repos/isabelle/file/e89cfc004f18/src/HOL/Real_Vector_Spaces.thy#l1218

These constraints were introduced by Brian Huffman in 2d91b2416de8 while he was reworking 
the type class hierarchy for topological spaces in 2009. I do not know his reasons for 
this, but I guess that they are meant to save type annotations.


Best,
Andreas


On 19/11/15 10:10, Florian Haftmann wrote:

Hi Larry,


Andreas’s message reminds me that axioms of type classes are still not

picked up:


class dist_norm = dist + norm + minus +
   assumes dist_norm: "dist x y = norm (x - y)”

This item has the status of a theorem. However, the query

dist "norm(_-_)”

doesn’t find it. Surely it should?


my mail from this summer still applies:


There is nothing wrong with type classes here:

class involutory =
   fixes f :: "'a ⇒ 'a"
   assumes involutory: "f (f x) = x"
begin

lemma involutory3:
   "f (f (f x)) = f x"
   by (fact involutory)

end

find_theorems "f"

It seems to be a constraint issue:

find_theorems "_ = norm (_ - _)"
~> 'a::real_normed_vector is inferred
find_theorems "_ = norm ((_::'a::dist_norm) - _)"
~> typing error

Maybe some naughty tweaking of sort constraints or an unforseen
behaviour of coercions, but these are mere guesses.  I do not understand
these parts of the type class hierarchy.


I do not know why and how the default constraints of »dist« are changed,
but this is the basic cause for the behaviour you experience.

Cheers,
Florian



___
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] AFP failures in sessions ConcurrentGC, MonoBoolTranAlgebra, Presburger-Automata, Vickrey_Clarke_Groves

2015-11-15 Thread Andreas Lochbihler

MonoBoolTranAlgebra was failing due to my change in Isabelle/90f54d9e63f2 and the removal 
of theorem fun_eq in favour of arg_cong (I have not investigated when this happened, but 
just adapted the proof scripts), see changesets 53f94abb8704 and 0377b757f016. 
Presburger-Automata had a looping call to simp which looks related to the changes with 
real. It should work now in AFP/935a90e010a2.


Vickey_Clarke_Groves looks related to the changes to "real", but I have not 
tried to fix this.

Best,
Andreas

On 15/11/15 10:38, Florian Haftmann wrote:

isabelle: f1b257607981 tip
afp: 1a688183b05a tip

Any idea what is going on here?

Florian



___
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] NEWS

2015-10-09 Thread Andreas Lochbihler


Dear Ondrej,

Thanks a lot for this. Now I can scrap my own semi-working debugging infrastructure for 
transfer(_prover).


Just a comments: Can you add a flag to transfer_step such that it outputs the rule it used 
as tracing information? My problem is that with big terms, I get a lot of subgoals (> 50). 
If I try to identify missing rules, I check the replacement of the current term in the 
skeleton, but as the skeleton is the last goal, I have to increase the limit of goal 
states and always scroll down in the output panel. Now if I could see the rule directly in 
the output buffer, I could see there directly when something goes wrong.


Best,
Andreas

On 09/10/15 01:52, Ondřej Kunčar wrote:

* Transfer:
   - new methods for interactive debugging of 'transfer' and
 'transfer_prover': 'transfer_start', 'transfer_step',
 'transfer_end', 'transfer_prover_start'
 and 'transfer_prover_end'.

This refers to 46af4f577c7e.

See the Isar Reference Manual and the example file 
"~~/src/HOL/ex/Transfer_Debug.thy".

Ondrej
___
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] NEWS: 'consider' command and "cases" method

2015-09-23 Thread Andreas Lochbihler


Dear Manuel,

consider supports the same syntax as obtains, i.e., you can use "where" as in

  consider "x = ∞" | "x = -∞" | y where "x = ereal y"

Andreas

On 23/09/15 08:41, Manuel Eberl wrote:

Is there a way to use ‘consider’ with fixed variables?

E.g. if I have a rule like ereal_cases:

 (⋀r. x = ereal r ⟹ thesis) ⟹
 (x = ∞ ⟹ thesis) ⟹
 (x = - ∞ ⟹ thesis) ⟹ thesis

I would like to write

 consider "x = ∞" | "x = -∞" | "x = ereal x'" for x'

But that syntax is not supported. Is there another way except the rather
clumsy

 consider "x = ∞" | "x = -∞" | "∃x'. x = ereal x'"

?


Cheers,

Manuel



On 15/06/15 00:11, Makarius wrote:

* New command 'consider' states rules for generalized elimination and
case splitting. This is like a toplevel statement "theorem obtains" used
within a proof body; or like a multi-branch 'obtain' without activation
of the local context elements yet.

* Proof method "cases" allows to specify the rule as first entry of
chained facts.  This is particularly useful with 'consider':

   consider (a) A | (b) B | (c) C 
   then have something
   proof cases
 case a
 then show ?thesis 
   next
 case b
 then show ?thesis 
   next
 case c
 then show ?thesis 
   qed


This refers e.g. to Isabelle/051b200f7578. Some examples are in
~~/src/HOL/Isar_Examples/Structured_Statements.thy

It may be seen as an answer to the open problem of section 5.5.3
"Generalized case-splitting" from my Ph.D. thesis.  There is no need to
support non-linear proof processing in the Isar/VM: 'consider' merely
states and proves the rule, and the "cases" method does the splitting in
a normal backwards proof (with case names).

This means that awkward use of raw proof blocks with "big-bang
integration" by blast is no longer required.  General case-splitting can
now be written explicitly and robustly.


 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


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

Re: [isabelle-dev] JinjaThreads

2015-09-15 Thread Andreas Lochbihler


Hi Makarius,

This might be due to my attempt to repair Predicate_Compile_Examples in 78ece168f5b5. I'll 
see what I can do.


Andreas

On 15/09/15 16:41, Makarius wrote:

This is the situation in Isabelle/0b071f72f330 and AFP/3085eb9e2bb9:

*** Failed to load theory "Execute_Main" (unresolved "Java2Jinja")
*** Failed to load theory "JinjaThreads" (unresolved "Execute_Main")
*** Dependency "member_i_i" -> "case_list" would result in module dependency 
cycle
*** At command "export_code" (line 18 of
"~/isabelle/afp-devel/thys/JinjaThreads/Execute/Java2Jinja.thy")

Any ideas?


 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] JinjaThreads

2015-09-15 Thread Andreas Lochbihler


It should work now again (Isabelle/e4716b792713 and AFP/ec3887abf158).

Sorry for the trouble,
Andreas

On 15/09/15 16:41, Makarius wrote:

This is the situation in Isabelle/0b071f72f330 and AFP/3085eb9e2bb9:

*** Failed to load theory "Execute_Main" (unresolved "Java2Jinja")
*** Failed to load theory "JinjaThreads" (unresolved "Execute_Main")
*** Dependency "member_i_i" -> "case_list" would result in module dependency 
cycle
*** At command "export_code" (line 18 of
"~/isabelle/afp-devel/thys/JinjaThreads/Execute/Java2Jinja.thy")

Any ideas?


 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] [isabelle] Code setup for Fraction_Field

2015-09-10 Thread Andreas Lochbihler


Hi Florian,

I am continuing this thread on isabelle-dev as you have suggested.


3. For fraction fields over polynomials over rings (rather than
fields), one can use subresultants, but I have not been able to find
them formalised in Isabelle. Are they hidden somewhere? If not, are
there any plans to formalise them?


Are subresultants really necessary for this?

definition ppdivmod_rel :: "'a::idom poly ⇒ 'a poly ⇒ 'a poly ⇒ 'a poly
⇒ 'a ⇒ bool"
where
   "ppdivmod_rel x y q r m ⟷ (
   smult m x = q * y + r ∧ (if y = 0 then q = 0 else r = 0 ∨ degree r
< degree y)
   ∧  ( m= (if x=0 ∨ y=0 then 1 else (lead_coeff y) ^ (degree x + 1 -
degree y"


I am somehow lost how the »algebraic stack« is supposed to look like in
the whole example.  Something like Fraction over Poly over Int?

Yes, that's the idea.


Since Poly over Int forms a factorial ring but not an euclidean ring,
the question is how to generalize normalization of quotients a / b
accordingly.  It won't work naturally with type classes:

Poly over Rat --> normalization via gcd / eucl
Poly over Poly over Rat --> somehow different

Hence, some type class magic would be needed to detect whether to use
the rather efficient euclidean algorithm or something different – or
even refrain from normalization at all!?
The type class magic needed for this sort of decision is pretty simple, it's described in 
my paper on AFP/Containers from ITP 2013. You just have to wrap a gcd function in "_ 
option" such that the normalisation algorithm for fraction fields can check whether 
normalisation via gcd is possible or whether something else is needed. If fraction field 
is implemented via code_abstype with the invariant that only normalised fractions occur, 
then the decision about the normalisation algorithm is logically relevant, as the 
normalisation function shows up in the code equations of the form


  fract_of (p + q) =
  normalize_fract ( (fract_of p) (fract_of q))

However, if we do not require normalised fractions and instead use a quotient-like code 
setup for fraction fields with code_datatype, the decision about normalisation need *not* 
be logically relevant. The code equations then look like the following:


  Fract a b + Fract c d =
  normalise_fract ( (a, b) (c, d)))

The function normalise_fract can be a type class parameter, so one can define it 
differently for different types. As it returns the quotiented value, the decision whether 
to normalise and how to normalise is no longer logically relevant. So the choice could 
depend on extra-logical tricks (like inspecting the name of types).


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

Re: [isabelle-dev] NEWS

2015-09-10 Thread Andreas Lochbihler


Hi Florian,

I noticed that the new printing interacts strangely with set comprehensions. In 
Isabelle/92858a52e45b, "{(x, y). P x y}" prints as "Collect (uncurry P)" which I find 
rather hard to read. Are you aware of this effect and could you please restore the former 
situation?


Best,
Andreas

On 10/09/15 12:02, Florian Haftmann wrote:

* Combinator to represent case distinction on products is named
"uncurry", with "split" and "prod_case" retained as input abbreviations.

Partially applied occurences of "uncurry" with eta-contracted body
terms are not printed with special syntax, to provide a compact
notation and getting rid of a special-case print translation.

Hence, the "uncurry"-expressions are printed the following way:

a) fully applied "uncurry f p": explicit case-expression;

b) partially applied with explicit double lambda abstraction in
the body term "uncurry (%a b. t [a, b])": explicit paired abstraction;

c) partially applied with eta-contracted body term "uncurry f":
no special syntax, plain "uncurry" combinator.
This aims for maximum readability in a given subterm.
INCOMPATIBILITY.

This refers to e6b1236f9b3d.

This schema emerged after some experimentation and seems to be a
convenient compromise. The longer perspective is to overcome the
case_prod/split schism eventually and consolidate theorem names accordingly.

The next step after this initial cleanup is to tackle the »let (a, b) =
… in …« issue.

Florian



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

2015-09-09 Thread Andreas Lochbihler

Hi Makarius,

I had a brief look at the unchecked files in Predice_Compile_Examples. I have never worked
with these theories, so take my comments with a grain of salt.

Predicate_Compile_Quickcheck_Examples:

In dc2236b19a3d, Lukas removed the testers which are used in this theory and replaced them
with smart_exhaustive. Moreover, this theory stems from the time when 'a set was a synonym
for 'a => bool. The predicate compiler was never adjusted to the separation of predicates
and sets in Isabelle2012 and can only handle predicates.

I replaced the old generators with the new testers and the examples which do not involve
sets work again. Those with sets are completely broken.

Hotel_Example_Small_Generator:

The examples in this file involve sets, so I have no hope to get this working without
addressing the problem with sets.

IMP_3 and IMP_4: These two theories also fail due to sets. However, sets are only used
with the function List.set, so this can be easily avoided.

I've committed some changes in 78ece168f5b5 such that most of the examples work again.
Only Hotel_Example_Small_Generator remains completely broken.

Unfortunately, quickcheck and the predicate compiler have been essentially unmaintained
since Lukas has left. The predicate compiler works fine for inductive predicates, but most
of the extensions that Lukas has implemented (in particular inductify) have not been
maintained are therefore break in many cases. Similarly, Quickcheck internally has a huge
number of compilation modes most of which I consider as untested. The above changeset
activates a few tests again, but as can be seen, the compliation modes break in corner
cases. Ideally, we'd need a thorough clean-up of quickcheck and the predicate compiler,
but I guess nobody is willing to invest the time.

Cheers,
Andreas

On 09/09/15 11:37, Makarius wrote:

Doing some routine maintenance, I've rediscovered this very odd changeset:

changeset: 40055:1f7cc5357d96
user:bulwahn
date:Thu Oct 21 20:26:35 2010 +0200
files: src/HOL/Predicate_Compile_Examples/ROOT.ML
description:
temporary removed Predicate_Compile_Quickcheck_Examples from tests

The comment in the source says "should be added again soon", but that was 5
years ago.

The session HOL-Predicate_Compile_Examples has a few more dead and half-rotten
bits, see
http://isabelle.in.tum.de/repos/isabelle/file/f9fd43d8981d/src/HOL/ROOT#l973

Any ideas what can be done about it? Even just removing rubbish requires some
basic
understanding of the situation.

Makarius

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

[isabelle-dev] goals inserts facts into goal statement

2015-07-24 Thread Andreas Lochbihler

I am trying to replace some of my old usages of case goal_* with the new goals method. In 
the course, I encountered the problem that goal inserts the facts chained in as additional 
assumptions of my goals and also for the case bindings. This is unfortunate when I use 
goals sequenced after rule. Below is a prototypical example:


  lemma foo: [| X; Y; X == Y; Y == X |] == True by simp

  have A and B
  then (* chaining is required to instantiate the free variables in the theorem 
*)
  show True
  proof(rule foo)
case goal_1
...
  next
case goal_2
...

Now, when I replace (rule foo) with (rule foo, goals), the goals methods inserts the facts 
A and B into every subgoal and into the case bindings. Is there a canonical way to avoid this?


I can of course write

  apply(rule foo) proof goals

but this feels like going against the spirit of Isar. Why does goals have to insert 
chained facts at all?


Andreas

PS: I am using Isabelle/3444e0bf9261.

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

Re: [isabelle-dev] Remaining uses of defer_recdef?

2015-06-08 Thread Andreas Lochbihler


On 06/06/15 17:11, Florian Haftmann wrote:

So are there any experience reports that the combinatorial explosion in
pattern matching in fun/function had to be worked around somehow?  Or do
we have to conclude that the pattern complexity of the applications in
src/HOL/Decision_Procs is indeed domain-specific?
I regularly have to work around this explosion problem. One example is in 
JinjaThreads/Common/BinOp.thy where I was not able to define the function binop as a 
whole, but I had to split it up into several definitions - fortunately, there was no 
recursion involved, so this was possible. There must also be a mailing list thread between 
Alexander Krauss and me on this topic, but I was not able to unearth it.


I have run into the same problem (with similar workarounds) a number of times. In case of 
a recursive function, I nowadays write


  f x y z = (case x of ... = (case y of ... = | _ = ...) | _ = ...)

and let simps_of_case split the equations by the pattern. In big cases, simps_of_case runs 
for a minute or two, but there is no hope to get these definitions through with the 
function. Of course, this does not work with overlapping patterns, but I rarely use them 
anyway. The main drawback here is that I do not get a suitable cases rule for the function 
definitions and the proofs accordingly look ugly (especially if I have nested patterns, 
i.e., nested case distinctions and lots of rename_tac+case_tac).


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

Re: [isabelle-dev] datatype takes minutes, but timing panel shows 10s

2015-04-14 Thread Andreas Lochbihler

Hi Dmitriy,

Thanks for investigating. I am really surprised that the code plugin is to blame for the
huge overhead. I don't know the details of the code plugin, but I have an idea of what it
should do: instantiate the equals type class, register the constructors as code
constructors, and declare the pattern-matching equations for case, set, rel, map and
equals as [code].

None of this should involve any fancy proof. In fact, most of the equations should have
already been proven by the free_constructors part or should be easily derived from them by
single-step resolutions. What am I missing?

Andreas

On 13/04/15 12:04, Dmitriy Traytel wrote:

Hi Andreas,

I've investigated this a bit and the slowdown happens in the code plugin in the
instantiation of the equal type class (i.e. datatype (plugins del: code) is
more precise
than the advice below). The number of theorems proved there is quadratic (8000
in your
case).

But it is still not hopeless: those 8000 theorems are proved one after each
other calling
Goal.prove for each of them. It is much faster to form the (balanced)
conjunction, call
Goal.prove (which does among other things type checking) once, and then destroy
the
conjunction. I'm currently testing this on testboard
(http://isabelle.in.tum.de/testboard/Isabelle/rev/1863cdff2010).

Cheers,
Dmitriy

On 09.04.2015 16:11, Andreas Lochbihler wrote:

Hi Dmitriy and Jasmin,

Thanks for the hint with plugins. That really speeds things up. I also suspect
that the
timing panel does not include the forked proof tactics.

Cheers,
Andreas

On 09/04/15 15:55, Dmitriy Traytel wrote:

Hi Andreas,

rather than going dirty, try:

datatype (plugins only:) family ...

It seems that here we are lucky and the slowdown is caused by one of the
plugins. (We'll
investigate which one.)

Cheers,
Dmitriy

PS: Your datatype reminded me of another one, which allows (or allowed) proving
False in a
different theorem prover ;-)
https://sympa.inria.fr/sympa/arc/coq-club/2015-03/msg00134.html

On 09.04.2015 15:44, Jasmin Blanchette wrote:

Hi Andreas,

In Isabelle2014, processing this datatype declaration takes about one minute.
So what
has happened in between? (The Isabelle2014 timing panel is also way off with 8
seconds.)

Thanks for your report. What happened in between is that we generate more
theorems. I
suspect one or a few of them have tactics that scale poorly (e.g. cubic) in the
number
of constructors.

As for the timing panel, I suspect it does not take into consideration the time
spent in
tactics with multithreading on, but I’m not an expert there.

We’ll look into this. You could try “quick_and_dirty” around that particular
datatype to
make things more tolerable in the meantime.

Cheers,

Jasmin

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

Re: [isabelle-dev] datatype takes minutes, but timing panel shows 10s

2015-04-14 Thread Andreas Lochbihler


Hi Dmitriy,


the code plugin defines a new constant (copy of op =) that is used as equality.

datatype x = A | B
export_code equal_x_inst.equal_x in SML

This is precisely the instantiation of the equals type class.


To get it executable (#constructors)^2 equations are proved in a backward 
fashion (I'm
sure it could be easilly done in a forward fashion as well). However, this code 
goes back
to Stefan and Florian, and we didn't attempt to optimize it when integrating it 
with the
new package.

I see.


But isn't the performance now (894d6d863823 ) already acceptable?

I have not tried it yet, because I am busy testing Isabelle2015-RC0.

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

[isabelle-dev] datatype takes minutes, but timing panel shows 10s

2015-04-09 Thread Andreas Lochbihler


Dear BNF and Isabelle/jEdit developers,

Today, I noticed that the datatype command in Isabelle/e936c2828bec is sometimes extremely 
slow. At the end of this mail, there is a large enumeration type where this shows up. 
Processing this definition on my laptop takes about 4 minutes, but the timing panel from 
the Plugins/Isabelle menu just shows 11.398 seconds for the datatype command.


In Isabelle2014, processing this datatype declaration takes about one minute. So what has 
happened in between? (The Isabelle2014 timing panel is also way off with 8 seconds.)


Best,
Andreas

datatype family
  = AF_UNSPEC
  | AF_UNIX
  | AF_INET
  | AF_INET6
  | AF_IMPLINK
  | AF_PUP
  | AF_CHAOS
  | AF_NS
  | AF_NBS
  | AF_ECMA
  | AF_DATAKIT
  | AF_CCITT
  | AF_SNA
  | AF_DECnet
  | AF_DLI
  | AF_LAT
  | AF_HYLINK
  | AF_APPLETALK
  | AF_ROUTE
  | AF_NETBIOS
  | AF_NIT
  | AF_802
  | AF_ISO
  | AF_OSI
  | AF_NETMAN
  | AF_X25
  | AF_AX25
  | AF_OSINET
  | AF_GOSSIP
  | AF_IPX
  | Pseudo_AF_XTP
  | AF_CTF
  | AF_WAN
  | AF_SDL
  | AF_NETWARE
  | AF_NDD
  | AF_INTF
  | AF_COIP
  | AF_CNT
  | Pseudo_AF_RTIP
  | Pseudo_AF_PIP
  | AF_SIP
  | AF_ISDN
  | Pseudo_AF_KEY
  | AF_NATM
  | AF_ARP
  | Pseudo_AF_HDRCMPLT
  | AF_ENCAP
  | AF_LINK
  | AF_RAW
  | AF_RIF
  | AF_NETROM
  | AF_BRIDGE
  | AF_ATMPVC
  | AF_ROSE
  | AF_NETBEUI
  | AF_SECURITY
  | AF_PACKET
  | AF_ASH
  | AF_ECONET
  | AF_ATMSVC
  | AF_IRDA
  | AF_PPPOX
  | AF_WANPIPE
  | AF_BLUETOOTH
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] datatype takes minutes, but timing panel shows 10s

2015-04-09 Thread Andreas Lochbihler


Hi Dmitriy and Jasmin,

Thanks for the hint with plugins. That really speeds things up. I also suspect that the 
timing panel does not include the forked proof tactics.


Cheers,
Andreas

On 09/04/15 15:55, Dmitriy Traytel wrote:

Hi Andreas,

rather than going dirty, try:

datatype (plugins only:) family ...

It seems that here we are lucky and the slowdown is caused by one of the 
plugins. (We'll
investigate which one.)

Cheers,
Dmitriy

PS: Your datatype reminded me of another one, which allows (or allowed) proving 
False in a
different theorem prover ;-)
https://sympa.inria.fr/sympa/arc/coq-club/2015-03/msg00134.html

On 09.04.2015 15:44, Jasmin Blanchette wrote:

Hi Andreas,


In Isabelle2014, processing this datatype declaration takes about one minute. 
So what
has happened in between? (The Isabelle2014 timing panel is also way off with 8 
seconds.)

Thanks for your report. What happened in between is that we generate more 
theorems. I
suspect one or a few of them have tactics that scale poorly (e.g. cubic) in the 
number
of constructors.

As for the timing panel, I suspect it does not take into consideration the time 
spent in
tactics with multithreading on, but I’m not an expert there.

We’ll look into this. You could try “quick_and_dirty” around that particular 
datatype to
make things more tolerable in the meantime.

Cheers,

Jasmin

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



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

Re: [isabelle-dev] isabelle test failed (HOL-NSA-Examples)

2015-03-12 Thread Andreas Lochbihler


It should now work again in 034a4d15b52e. Sorry for the trouble.

Andreas

PS: The error message is not so obscure if you look at the types. The left hand side talks 
about hyper-naturals, the right hand side about nat.


On 12/03/15 13:56, Andreas Lochbihler wrote:

Hi Makarius,

You are right, that's my fault. I'll look into it.

Andreas

On 12/03/15 12:48, Makarius wrote:

On Thu, 12 Mar 2015, Account Isatest wrote:


Unfinished session(s): HOL-NSA-Examples


Presumably this is caused by

changeset:   59676:4762c690a75c
parent:  59654:e327a9ae2d61
user:Andreas Lochbihler
date:Tue Mar 10 16:35:14 2015 +0100
files:   src/HOL/NSA/StarDef.thy
description:
more type class instances


The error message of the NSA transfer proof method is a bit obscure.


 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

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

Re: [isabelle-dev] isabelle test failed (HOL-NSA-Examples)

2015-03-12 Thread Andreas Lochbihler


Hi Makarius,

You are right, that's my fault. I'll look into it.

Andreas

On 12/03/15 12:48, Makarius wrote:

On Thu, 12 Mar 2015, Account Isatest wrote:


Unfinished session(s): HOL-NSA-Examples


Presumably this is caused by

changeset:   59676:4762c690a75c
parent:  59654:e327a9ae2d61
user:Andreas Lochbihler
date:Tue Mar 10 16:35:14 2015 +0100
files:   src/HOL/NSA/StarDef.thy
description:
more type class instances


The error message of the NSA transfer proof method is a bit obscure.


 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] Constructors and the predicate compiler

2015-02-16 Thread Andreas Lochbihler

Dear Florian,

I myself have never looked in detail through the implementation of the predicate compiler,
but I have been a major user. I previously noticed that it does not go well together with
code_datatype. Here are my 50 cents.

On the one hand, the predicate compiler generates code equations, so it should work
together with the code generator. On the other hand, it operates inside Isabelle/HOL, so
it does not have access to the extra-logical features of the code generator such as data
refinement. This is probably the source of the confusion. To me, it seems more sensible to
do everything as in the logic and ignore the code generator setup as much as possible.

The compilation requires that the constructors are invertible inside the logic
(code_datatype's pseudo-constructors are invertible in the generated code, but not
necessarily in the logic). Therefore, IMHO, mode inference has to use Ctr_Sugar, not
Code.is_constr. Otherwise, the compiler will later try to construct a case expression for
a code_datatype pseudo-constructur and raise an Error in case expression: Not a datatype
constructor.

In predicate_compile_proof.ML, the generated equations are proven. The is_constructor
function is used to check whether the constructor should be inverted (using a case
expression). Since this happens inside the logic and has to be coupled with the mode
inference, it should use the same criterion as the mode inference, namely Ctr_Sugar.

I am not familiar with the flatten function in predicate_compile_fun and what exactly it
is good for. My educated guess is that this determines which of the function constants in
an (inductive) definition should be replaced with predicates and which not. If this is
right, then it should also be Ctr_Sugar there.

In summary, I'd say that code_pred should only use Ctr_Sugar and ignore code_datatype
declarations. If a user does use code_datatype, then he is responsible for providing
appropriate code equations for the existing functions, i.e., the constructors and the case
operator, or set up the code preprocessor to eliminate them (cf. the Suc eliminiation in
Code_Target_Nat and friends). Otherwise, users will have a hard time to follow what is
actually going on in code_pred.

Andreas

On 14/02/15 11:25, Florian Haftmann wrote:

Hi all,

while reviewing some technical details of code generation, I stumbled
over a confusion in the predicate compiler regarding what a
»constructor« is supposed to be.

The presumably fundamental notions are given in predicate_compile_aux.ML
(c3ca292c1484) as:

(* check if a term contains only constructor functions *)
(* TODO: another copy in the core! *)
(* FIXME: constructor terms are supposed to be seen in the way the code
generator
sees constructors.*)
fun is_constrt thy = … (* relying on Ctr_Sugar *)

val is_constr = Code.is_constr o Proof_Context.theory_of (* relying on
Code *)

is_constrt is actually only used in predicate_compile_fun.ML:

… Predicate_Compile_Aux.is_constrt …

guarding whether a given term is supposed to stay »as it is«, suggesting
that the postulating comment for is_constrt reflects actually the
intended behaviour, leaving open the question why it has not ever been
implemented like this.

On the other hand is_constr is used in mode_inference.ML:

fun is_invertible_function ctxt (Const (f, _)) = is_constr ctxt f
| is_invertible_function ctxt _ = false

and this seems odd, since a constructor in the sense of the code
generator is by now means invertible, suggesting that here a fundamental
misconception occurs.

From such a superficial analysis it seems to follow that the two
implementations should be actually swapped: is_constrt relying on
Code.is_constr, is_constr relying ont Ctr_Sugar.

To make the confusion perfect, in predicate_compile_proof.ML there is a
third variant:

(* returns true if t is an application of a datatype constructor *)
(* which then consequently would be splitted *)
fun is_constructor ctxt t =
(case fastype_of t of
Type (s, _) = s @{type_name fun} andalso can
(Ctr_Sugar.dest_ctr ctxt s) t
| _ = false)

Can anybody acquainted with the predicate compiler shed some light on this?

Cheers,
Florian

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

Re: [isabelle-dev] AFP: Sourceforge down

2015-02-12 Thread Andreas Lochbihler


Makarius,

I have the impression that your push has not made it to the official afp-code. At least, I 
cannot see it on


http://sourceforge.net/p/afp/code/ci/6ff9a8c6405d04f28365434a0e7bd65ea89aad86/log/

although my commits do show up there.

Andreas

On 10/02/15 23:08, Makarius wrote:

On Tue, 10 Feb 2015, Makarius wrote:


Sourceforge is presently in down due to serious technical problems. This is 
relevant for
afp-devel.

Here is my own clone of it: https://bitbucket.org/makarius/afp-devel

In particular afp-devel/2aa8b0c283eb corresponds to Isabelle/59817f489ce3 with 
its
changes on resolve_tac.


Sourceforge appears to be back, and I have pushed the above material there.


 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] Code preprocessor tracing

2014-10-07 Thread Andreas Lochbihler


Hi Florian,

Thanks for all this.


2. Meanwhile, I really like the new simplifier tracing facility and
hardly ever use the old [[simp_trace]]. Since the new trace offers a lot
of control over the tracing, would it make sense to base the tracing
facility on the new one?


It would definitely make sense, but at the moment I will not put any
personal effort into this.

You are right. There are more urgent things to do. I'll keep it at the back of 
my head.

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

Re: [isabelle-dev] Proposal for localized interpretations

2014-09-18 Thread Andreas Lochbihler

Dear developers,

Jasmin mentioned to me that his new implementation allows to select which plugins should
be applied. Currently, the code generator has its own manager of plugins
(Code.datatype_interpretation) and I would be very happy if certain plugins could be
disabled selectively upon code_datatype commands. For example, in AFP/Coinductive, I would
like code_datatype to not change the code equations for the partial_term_of
instantiations, because it does not (and cannot in general) adapt the equations for
narrowing, but the two should be in sync. At present (AFP/222773085523), I have to undo
the effect of the partial_term_of plugin in Lazy_LList.thy and Lazy_TLList.thy by writing
ugly code equations. It would be much easier to disable the plugin locally for this
declaration.

I would expect that if Jasmin's plugin manager is also used in the code generator, it
would be easy to implement plugin selection for code_datatype, too.

Best,
Andreas

On 05/09/14 10:36, Jasmin Christian Blanchette wrote:

Hi all,

The interpretation mechanism, as defined in Pure/interpretation.ML, is used
in a few places in Isabelle, including the new (co)datatype package, for allowing other tools and
users to register their hooks. Unfortunately, it works at the theory level, which interacts poorly
with local definitions. For example, if you try

locale A =
fixes a :: 'a
assumes a = a
begin

datatype_new 'b x = X 'b

end

with Isabelle2014, you will get

Undeclared hyps:
A a
The error(s) above occurred for the goal statement⌂:
left_total R ⟹ left_total (A.rel_x R)

This error arises in the Transfer hook. I can think of no way to solve this at
the theory level.

To solve this issue, I introduced my own interpretation mechanism, in
HOL/Tools/Ctr_Sugar/local_interpretation.ML, that works both on theories and
local theories. If you look at it, you will see that it is mostly a copy-paste job. The
key insight is that there are three scenarios (taking datatypes as our example):

1. The datatype is defined after the hook is registered.

2a. The datatype is defined before the hook is registered.

2b. The dataype and the hooks are registered in two parallel theories, which
are later merged.

In case 1, one can imagine having the datatype directly giving its local theory to the hook. This
is what local_interpretation.ML does, and this is enough to solve the problem in the
example above. In case 2a and 2b, things have to be done at the theory level, like before, but this
is a rarer case (e.g. we have no local datatypes in Main). Also, the odd signature
management that was necessary before to make 2a and 2b work (cf. my April 2 email to this mailing
list) is now centralized (cf. e6e3b20340be).

I would like to propose either replacing the old mechanism by the new one or having both
live in parallel in Pure. It is certainly not perfect, but it is IMO an
improvement over the statu quo. What do you think?

Jasmin

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

Re: [isabelle-dev] Code preprocessor tracing

2014-09-10 Thread Andreas Lochbihler


Hi Florian,

Sorry for the long delay until you get an answer, but I wanted to wait until I can port my 
application from Isabelle2013-2 to 2014. The tracing facility seems to provide some basic 
means to limit the scope of the tracing. I found the two suggestions for improvement:


1. The rewriting with the simplifier can be traced, but I have not been able to activate 
it for function transformers (as, e.g., in Code_Target_Nat for 0/Suc). If tracing for 
function X is active, it might be useful to display the set of equations before and after 
the application of each function transformer.


2. Meanwhile, I really like the new simplifier tracing facility and hardly ever use the 
old [[simp_trace]]. Since the new trace offers a lot of control over the tracing, would it 
make sense to base the tracing facility on the new one?


Thanks for your efforts,
Andreas

On 29/06/14 18:00, Florian Haftmann wrote:

Hi Andreas,

with http://isabelle.in.tum.de/repos/isabelle/rev/020cea57eaa4 I have
provided very basic means to trace the code preprocessor.  Alas, I only
dimly remember what your real requirements are, so feel free to comment
on it.  Anyway, it is a starting point.

Cheers,
Florian


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

[isabelle-dev] Testing of generated code

2014-08-25 Thread Andreas Lochbihler

Hi all,

we have hardly any check that the code generated by the code generator is correct. There
is only the checking option of the command export_code. It calls a target language
compiler to see whether the compiler accepts the code. Since there are more and more
adaptations to serialisation phase in Isabelle and the AFP, I have written a testing
framework for the code generator (pushed on testboard/469a375212c1), which has already
helped me in finding a number of oversights in my AFP entry Native_Word.

The framework provides a command for regression tests of lists of boolean expressions
(command test_code) and for evaluation of single terms (command eval_term). They both
generate code in the given target language(s) plus language-specific drivers, compile and
run the whole and parse back the result using a YXML encoding. The commit contains drivers
for PolyML, MLton, SML/NJ, OCaml, GHC and Scala.

The framework requires some configuration for the target languages. In detail, the
following environment variables have to be set as follows for the different implementations:

ISABELLE_POLYML_PATH point to a PolyML executable poly
ISABELLE_MLTON point to an MLton executable mlton
ISABELLE_SMLNJ point to the SML/NJ executable sml
ISABELLE_OCAMLC point to the OCaml executable ocamlc
ISABELLE_GHC point to the GHC executable ghc (same as for
Quickcheck_Narrowing)
ISABELLE_SCALA point to the Scala binary folder (which contains scala and
scalac)

I do not know how the test systems for the repository are configures w.r.t.

export_code ... checking ...

but this framework only makes sense if we have each supported implementation of a target
language installed on at least one system. In July, Gerwin set up the machines for GHC.
Could anyone take care of the other implementations?

If this works well across all platforms, one might think about moving this upwards into
Main and generalise value [code] accordingly.

Best,
Andreas

PS: Feedback on the code is always welcome.
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Dead and broken theory src/HOL/Library/Quickcheck_Types.thy

2014-08-19 Thread Andreas Lochbihler

See now 8b7508f848ef. Library/Lattice_Constructions contains the remains of 
Library/Quickcheck_Types.


Andreas

On 18/08/14 18:44, Peter Lammich wrote:

However, the constructions might still be useful, as the following comment from 
Peter
Lammich's AFP entry Refine_Monadic shows.

(* TODO: Library/Quickcheck_Types.thy:flat_complete_lattice provides
  an isomorphic contruction. *)


At this point I duplicated the flat complete lattice construction
locally, as I did not want to use rely on a construction from such a
special and unrelated thing as quickcheck.



So, should we keep Quickcheck_Types (maybe under a different name, say
Lattice_Constructions) or drop it?



I think, at least the standard constructions, like flat complete
lattice, should be preserved and either directly go into
Complete_Lattice or, as you proposed, into
HOL/Library/Lattice_Constructions.

--
   Peter




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

Re: [isabelle-dev] Dead and broken theory src/HOL/Library/Quickcheck_Types.thy

2014-08-15 Thread Andreas Lochbihler

In 51aa30c9ee4e, I have added lattice instances for the Enum.finite_* types. As expected,
this suffices for the quickcheck examples in Quickcheck_Lattice_Examples (see 9225b2761126).

This now raises the question what we should do with HOL/Library/Quickcheck_Types. Within
the Isabelle distribution and the AFP, this theory is no longer used anywhere. I expect
that almost nobody relies on the quickcheck setup in there. From the quickcheck point of
view, we can therefore drop this theory. Anyone who needs it can keep their own local copy.

However, the constructions might still be useful, as the following comment from Peter
Lammich's AFP entry Refine_Monadic shows.

(* TODO: Library/Quickcheck_Types.thy:flat_complete_lattice provides
an isomorphic contruction. *)

So, should we keep Quickcheck_Types (maybe under a different name, say
Lattice_Constructions) or drop it?

Andreas

On 11/07/14 15:54, Andreas Lochbihler wrote:

Quickcheck does not use these types, because it is currently configures to only
use the
types finite_1 to finite_3 from Enum, because the finite_types parameter is set
by
default. Quickcheck internally also seems to work differently depending on
whether the
finite_types flag is set.

I have only little insight how the parameters affect the performance of
quickcheck, but I
remember that Quickcheck originally used int as a replacement. Quickcheck_Types
clearly is
from that time. However, int is an infinite type and therefore, quantifiers, set
comprehensions and function equality are not executable. Later, he switched to
the
finite_X types, which instantiate enum, but not the other type classes.

Therefore, I recommend the following:

1. Temporarily fix Quickcheck_Types such that it works again, but leave it in
HOL/Library.
Then, anyone who wants to use quickcheck with infinite types can do so. This
way, the
Quickcheck_Examples session can also be reactivated.

2. Instead of moving Quickcheck_Types to Main, it suffices to make the finite_X
types
instances of the lattice type class hierarchy. Probably most of the stuff in
Quickcheck_Types can be adapted to work with the Enum types as well. Maybe even
all the
test cases in Quickcheck_Lattice_Examples work with the Enum types, too.

I have already done step 1 in 36041934e429 and 8840fa17e17c, but I won't have
time for
step 2 before the fork of the release branch.

Andreas

On 11/07/14 14:28, Tobias Nipkow wrote:

On 11/07/2014 13:43, Andreas Lochbihler wrote:

Quickcheck_Types defines a number of artificial types that quickcheck can use to
instantiate type variables that occur in a theorem. Normally, quickcheck
instantiates them with int provided that the sort constraints do not prevent
this. In Enum.thy, there are already the types finite_X that quickcheck uses for
enumerable types (type class enum) such that quantifiers can be unfolded into
conjunctions or disjunctions.

The types in Quickcheck_Types now do the same for the lattices type class
hierarchy, because int and the finite_X types cannot be used for type variables
with sort lattice (or top/bot/...).

I believe that it should be fairly simple to adjust Quickcheck_Types to
Isabelle2014. However, this only makes sense if it becomes part of Main.
Otherwise, it will remain just a library theory that hardly anyone knows about
and no one uses.

Moreover, we should make sure that Quickcheck_Types fits to the current code
generator setup for lattices. IIRC, Florian has reworked a lot there over the
past years. At the very least, we should have some test cases (e.g. in HOL/ex)
to check that Quickcheck_Types works as expected.

If there's consensus on reviving this theory, I can do the changes to
Quickcheck_Types such that Isabelle2014 digests it. This is probably all that
can be done before the release as most of us will be busy in Vienna next week. A
move to Main is something for the next release.

It looks mildly useful. But then Qickcheck would need to use it, which it
currently obviously does not. If you (or somebody) is able to make that happen,
then I am in favour of reviving that theory.

Tobias

Andreas

On 11/07/14 13:22, Lawrence Paulson wrote:

I’m afraid that I don’t even know what it is.
Larry

On 11 Jul 2014, at 12:21, Florian Haftmann
florian.haftm...@informatik.tu-muenchen.de wrote:

The issue that src/HOL/Library/Quickcheck_Types.thy is dead and broken
has not been addressed since before the last release.

So, which path to follow? Is there any interested in a serious repair
effort? Otherwise, we should honestly drop it.

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

___
isabelle-dev mailing list

Re: [isabelle-dev] ISABELLE_GHC/quickcheck

2014-07-21 Thread Andreas Lochbihler

The Native_Word entry in the AFP contains a number of quickcheck[narrowing] calls that are
set up such that they are tested only if ISABELLE_GHC is set. Therefore, there cannot be
an error message about quickcheck narrowing if ISABELLE_GHC is not set.

Andreas

On 19/07/14 21:30, Gerwin Klein wrote:

Just had a very strange experience with ISABELLE_GHC.

You will have noticed that the AFP test failed the last few days with GHC
compilation errors.

The AFP test settings included the line
ISABELLE_GHC=/opt/local/bin/ghc

Apparently, this caused sessions like Native_Word to fail, even though that is
where ghc is installed on this machine (macbroy2). ghc also happens to be in
the PATH on macbroy2 (pointing to the same /opt/local/bin/ghc), so in an act of
desperation I tried locally removing the above line on the isatest account.
Voila, Native_Word builds fine.

This was on isabelle 2bfbeb0e69cd and afp 4ea6558c319c.

However: on my laptop, with ISABELLE_GHC=/usr/bin/ghc, everything works fine.
Either it’s something about the path or something about the macbroyX machines.

Any ideas what could be going on?

Cheers,
Gerwin

The information in this e-mail may be confidential and subject to legal
professional privilege and/or copyright. National ICT Australia Limited accepts
no liability for any damage caused by this email or its attachments.
___
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] Dead and broken theory src/HOL/Library/Quickcheck_Types.thy

2014-07-11 Thread Andreas Lochbihler

Quickcheck does not use these types, because it is currently configures to only use the
types finite_1 to finite_3 from Enum, because the finite_types parameter is set by
default. Quickcheck internally also seems to work differently depending on whether the
finite_types flag is set.

I have only little insight how the parameters affect the performance of quickcheck, but I
remember that Quickcheck originally used int as a replacement. Quickcheck_Types clearly is
from that time. However, int is an infinite type and therefore, quantifiers, set
comprehensions and function equality are not executable. Later, he switched to the
finite_X types, which instantiate enum, but not the other type classes.

Therefore, I recommend the following:

1. Temporarily fix Quickcheck_Types such that it works again, but leave it in HOL/Library.
Then, anyone who wants to use quickcheck with infinite types can do so. This way, the
Quickcheck_Examples session can also be reactivated.

2. Instead of moving Quickcheck_Types to Main, it suffices to make the finite_X types
instances of the lattice type class hierarchy. Probably most of the stuff in
Quickcheck_Types can be adapted to work with the Enum types as well. Maybe even all the
test cases in Quickcheck_Lattice_Examples work with the Enum types, too.

I have already done step 1 in 36041934e429 and 8840fa17e17c, but I won't have time for
step 2 before the fork of the release branch.

Andreas

On 11/07/14 14:28, Tobias Nipkow wrote:

On 11/07/2014 13:43, Andreas Lochbihler wrote:

The types in Quickcheck_Types now do the same for the lattices type class
hierarchy, because int and the finite_X types cannot be used for type variables
with sort lattice (or top/bot/...).

It looks mildly useful. But then Qickcheck would need to use it, which it
currently obviously does not. If you (or somebody) is able to make that happen,
then I am in favour of reviving that theory.

Tobias

Andreas

On 11/07/14 13:22, Lawrence Paulson wrote:

I’m afraid that I don’t even know what it is.
Larry

On 11 Jul 2014, at 12:21, Florian Haftmann
florian.haftm...@informatik.tu-muenchen.de wrote:

The issue that src/HOL/Library/Quickcheck_Types.thy is dead and broken
has not been addressed since before the last release.

So, which path to follow? Is there any interested in a serious repair
effort? Otherwise, we should honestly drop it.

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

Re: [isabelle-dev] Old 'defs'

2014-07-07 Thread Andreas Lochbihler

There's one use in JinjaThreads which does not fit into the overloading scope: The
constants sc_spurious_wakeups are declared in MM/SC_Collections.thy and MM/SC.thy, but
intentionally not defined. This expresses that the remaining proofs are independent of the
value of the constant, which is in fact just a configuration option. Only later, in
Execute/SC_Schedulers, there is the definition that sets this configuration option.

One could convert this into overloading+definition, but it would be a very degenerate form
of overloading, as the configuration option is a plain boolean, there are no type
variables involved.

Andreas

On 05/07/14 17:15, Makarius wrote:

Are there remaining uses of the old 'defs' command? It is not localized, and
somehow an
odd side-entry to the normal concept of definitional specifications in
contempory Isabelle
(which goes through Local_Theory.define instead of bare-bones foundations).

A hypersearch over Isabelle/251ef0202e71 and AFP/0576573b7840 shows very few
occurrences
of old 'defs', mainly in the form defs (overloaded). Isn't 'overloading' +
'definition'
the canonical way to to that today? Or are fine points that do require the old
form?

We've already managed to eliminate old 'axioms' some time ago. So we could
mark 'defs' as
legacy now, and remove it eventually.

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] unit :: complete_boolean_algebra – 697e0fad9337

2014-06-11 Thread Andreas Lochbihler


Hi Florian,

the simproc unit_eq in

http://isabelle.in.tum.de/repos/isabelle/file/697e0fad9337/src/HOL/Product_Type.thy#l78

rewrites anything of type unit to (), so there's no need to declare the definitions 
introduced in 697e0fad9337 as [simp]. One could declare sup_unit_def, inf_unit_def, 
Sup_unit_def, and Inf_unit_def as [abs_def, simp] such that they get unfolded even if they 
are applied only partially, but I don't know whether that is a good thing to have. 
(Admittedly, the definition of uminus has this [simp] declaration, so it's a bit 
unconsistent at the moment).


Andreas

On 10/06/14 23:02, Florian Haftmann wrote:

Hi Andreas,

I'm wondering whether there is a deliberate reason to declare top, bot
etc. on unit not as simp by default.  Since there is only one element of
unit, proof goals after simp should be trivial…

Florian


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

Re: [isabelle-dev] Remaining uses of Proof General?

2014-05-13 Thread Andreas Lochbihler


Thanks a lot.

Andreas

On 12/05/14 20:07, Florian Haftmann wrote:

1. Violation of well-sortedness constraints: type ... not an instance of
...

declare [[show_sorts]]
code_thms constant to be exported

Then, I use educated guessing and Emacs' incremental search to navigate
the code equations that have been output until I find the fault --
usually, it's just a missing [code] or [code del] declaration for some
constant that has introduced a quantifier or set comprehension.



I would really appreciate support for navigating code equations in the
output (e.g., Ctrl-click on a constant on the RHS of an equation takes
me to the code equation of that constant (in the output of code_thms).

For this particular case, it would also be useful to get the chain of
propagation for the sort constraint like in GHC (arising from the use of
...), but since Isabelle's code generator strengthens sort constraints
for intermediate functions, this would be a list (tree/graph) of
functions that trace the propagation.


I will have to think about something like that seriously.


Here, I have two suggestions for improvements:

a) Provide an entry to the code preprocessor such that I can trace the
transformation of the code equations for a given (set of) constants.
Currently, I only know how to trace the preprocessing of *all* code
equations, but I am not interested in most of this trace.


I will consider this.


b) [code_abbrev] is the worst code generator attribute that I know of,
because there's no reverse [code_abbrev del]. Each time I have to get
rid of a code abbreviation, I have to figure out once again how
[code_abbrev] transforms the theorem before it calls [code_unfold] and
[code_post]. Please add the [code_abbrev del] attribute.


See now http://isabelle.in.tum.de/repos/isabelle/rev/40213e24c8c4


And while I am at it, here is another point that makes my life
unnecessarily hard, but it's not related to jEdit vs. PG:

3. Problems with Code_Evaluation.term_of and friends

The term reconstruction functions are not displayed in code_thms because
of the section obfuscation in Code_Evaluation. I do not understand why
this has to be obfuscated. I always have to go via export_code and read
the generated code to figure out what the code equation for one of these
overloaded constants is. And it's bad luck if export_code raises an
error because some of the code equations are invalid.


See now http://isabelle.in.tum.de/repos/isabelle/rev/1e50fddbe1f5

Florian


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

Re: [isabelle-dev] Remaining uses of Proof General?

2014-05-02 Thread Andreas Lochbihler


On 02/05/14 16:16, Makarius wrote:

On Tue, 29 Apr 2014, Andreas Lochbihler wrote:


 text ‹
@{term ‹A \un B›}
 ›

 Here the \un works as expected -- the cartouche remains intact
 independently of its
 content, as long as the funny parentheses are nested properly.

But this correct nesting is exactly the problem. When I type \un while writing 
the
above, the closing parenthesis are not there yet. The prover sees something like

text {* @{term A \un

lemma foo: ... by ...


But why? In the ancient times, input was always sequential, as depth-first 
traversal of
the intended tree structure.  In less ancient times, some people proposed rigid 
structural
editors to make it impossible to escape from nested boxes (still seen today in 
TeXmacs),
although that is a bit awkward.  In the past 10 years or so, the standard IDE 
approach has
arrived somewhere in the middle: the user is free to type intermediate 
non-sense, but the
editor makes it easy to get it right by default.
I have used such templating mechanism with Eclipse and finally disabled them, because they 
caused me more work than what they saved. I usually prefer to enter both delimiters 
separately and to just see the matching parenthesis highlighted.


The reason is that I often add the delimiters only later. For example, when I write a 
single-identifier term, I use


text {* @{term my_constant} *}

and some time later, I figure out that I have to add something, e.g., a type constraint. 
Hence, I produce the following sequence of edits (the # denotes the position of the cursor)


text {* @{term #my_constant} *}
text {* @{term #my_constant} *}
text {* @{term my_constant#} *}
text {* @{term my_constant :: my_type#} *}
text {* @{term my_constant :: my_type#} *}

With the template mechanisms that I have seen so far, I get the following 
sequence:

text {* @{term #my_constant} *}
text {* @{term #my_constant} *}
text {* @{term #my_constant} *}
text {* @{term my_constant#} *}
text {* @{term my_constant :: my_type#} *}
text {* @{term my_constant :: my_type#} *}
text {* @{term my_constant :: my_type#} *}

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

Re: [isabelle-dev] Remaining uses of Proof General?

2014-04-29 Thread Andreas Lochbihler

Hi Makarius,

On 28/04/14 23:10, Makarius wrote:

a) Given some text like

definition foo where foo = ...

when I add an attribute like [simp]: after the where, I get a symbol completion
popup to
replace the : with the element sign. Usually, my next thing is to move the
cursor with
the cursor keys. But the popup gobbles all the key strokes until I explicitly
close it
with ESC. As colons are used everywhere in Isabelle's outer syntax, it would
really be
great if the popup only appears when I am in inner syntax.

b) Sometimes, when I write a HOL term, I used to not get the completion popup
when I
enter something like \un if there were sufficiently many parse errors in that
partial
term. Even Ctrl-b did not help. However, I cannot reproduce it in a small
example at the
moment.

In the case a), I guess that you still have the completion delay 0.0, while I
presently
work with 0.5 to give the prover a chance to add semantic completion
information, before
any popups are shown.
My completion delay is 0.1. When writing Isabelle terms normally, this is the amount of
time that does not break my flow of typing.

text ‹
@{term ‹A \un B›}
›

Here the \un works as expected -- the cartouche remains intact independently of
its
content, as long as the funny parentheses are nested properly.
But this correct nesting is exactly the problem. When I type \un while writing the above,
the closing parenthesis are not there yet. The prover sees something like

text {* @{term A \un

lemma foo: ... by ...

What is funny is that Proof General was actually one of the main reasons of
moving only
slowly in such token language reforms.
I am glad that PG still works for most of my theories and I try to keep that state as long
as feasible. There are already problems with new keywords declared by AFP entries that are
not listed in the keywords file. I then usually insert ; as a delimiter. But I try to
process such theories with jEdit and only go back to XEmacs/PG when I cannot stand
Isabelle/jEdit any longer (which usually happens when I debug the code generator setup).

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

Re: [isabelle-dev] Remaining uses of Proof General?

2014-04-29 Thread Andreas Lochbihler


On 28/04/14 23:18, Makarius wrote:

On Mon, 28 Apr 2014, Andreas Lochbihler wrote:


2. Reactivity when processing large files

With PG, I knew how to control the Isabelle prover. When I edit a large file in 
a larger
project like JinjaThreads, every now and then, Isabelle changes the background 
colour
from red to gray and then, apparently nothing happens for minutes before 
Isabelle turns
it red again and starts reprocessing. Is there some way to explicitly tell 
Isabelle that
it should now start to check again. Toggling continuous checking does not 
help.
Sometimes, I even have to close the theory file and reopen it again.


This sounds like the Poly/ML RTS is desparately trying to reclaim memory, by 
aggressive
sharing huge amounts of data.  Not long ago that situation lead into real 
memory problems
on my good old 32 GB machine, but David Matthews managed once again to postpone 
the
ultimate JinjaThreads implosion as a black hole of computing resources.

For now just the usual game, according to Tim the Enchanter:

   * What are your exact hardware parameters: CPU, main memory?

Intel® Core™ i7-3630QM CPU @ 2.40GHz, 8GB memory


   * What is your operating system?

Ubuntu 12.04 LTS


   * What are your ML system settings, e.g. as shown by isabelle build -? ?

ML_PLATFORM=x86-linux
ML_HOME=~/.isabelle/contrib/polyml-5.5.1-1/x86-linux
ML_SYSTEM=polyml-5.5.1
ML_OPTIONS=-H 500


   * What are your JVM settings: ISABELLE_JAVA_SYSTEM_OPTIONS and
 JEDIT_JAVA_OPTIONS ?
JEDIT_JAVA_OPTIONS=-Xms128m -Xmx3072m -Xss2m -Dactors.corePoolSize=4 
-Dactors.enableForkJoin=false



   * What are the options threads and parallel_proofs ?

threads = 0, parallel_proofs = 2

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

Re: [isabelle-dev] Remaining uses of Proof General?

2014-04-29 Thread Andreas Lochbihler

On 28/04/14 22:25, Makarius wrote:

On Mon, 28 Apr 2014, Andreas Lochbihler wrote:

My main usage of PG is when I want to construct a complicated proof method call
like

(fastforce intro: ... dest: ... elim: ... simp add: ... cong: ... del: ... simp
del: ...)+

that collapses an apply script of a hundred lines. I haven't yet found a
convenient way
to write the apply script in Isabelle/jEdit, because of reactivity issues (see
item 2
below) and the continuous updates of the output window (when I scroll to some
other part
of the apply script using the cursor keys). Are there key bindings for
scrolling that do
not move the cursor?

This reminds me of a very old insider jokes from the mid-1990-ies: Dieter
Nazareth had
finished the W0 formalization where he had turned half-decent tactic scripts
into such
compact one-liners, and shortly afterwards Wolfgang Naraschewski had to
disentangle that
again for the full W formalization, or rather start from scratch. A few years
later, the
Isar language emerged and made that approach in principle obsolete.
I know, I have myself untangles such one-liners often enough when something has changed.
Nevertheless, I believe that I'm still faster to build these one-liners than write pretty
Isar proofs of hundreds of lines, just because the goal states are huge and all cases are
shown in the same way.

Back to the actual technical questions. What are the main performance
bottle-necks here?
Printing of intermediate goal states? Or applying intermediate steps
repeatedly?
There are hardly any performance problems in terms of computing power, possibly except for
Isabelle processing a slow call to auto over and over again. The efficiency problem is the
interaction with the IDE. I use the Find panel a lot, but then my output panel is not
visible at the same time (that's why I would like to split the right dock in two). And
when I scroll upwards to find a snippet of tactic script that I want to copy, the output
updates and my current goal state is gone. (I know I could disable the updating, but then
I have to enable it manually again.)

I can say more when I understand the actual problem better. In such situations
I normally
have to see the dynamics of how you actually work.

Maybe I can show you what my problems are at ITP in Vienna in July.

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

Re: [isabelle-dev] Remaining uses of Proof General?

2014-04-28 Thread Andreas Lochbihler

Hi Makarius,

Over the past weeks, I've been using Isabelle/jEdit about half of my Isabelle time (and
ProofGeneral 3.7.1.1 with XEmacs the other half). Isabelle/jEdit is great when it comes to
working on small projects or refactoring existing sources. I really like the negative line
spacing setting and completion of fact names! Thanks!

My main usage of PG is when I want to construct a complicated proof method call
like

(fastforce intro: ... dest: ... elim: ... simp add: ... cong: ... del: ... simp
del: ...)+

that collapses an apply script of a hundred lines. I haven't yet found a convenient way to
write the apply script in Isabelle/jEdit, because of reactivity issues (see item 2 below)
and the continuous updates of the output window (when I scroll to some other part of the
apply script using the cursor keys). Are there key bindings for scrolling that do not move
the cursor?

Here are some things that could be improved in Isabelle/jEdit (I am currently on
Isabelle/4e2a0d4e7a82):

1. Symbol completion in PG was absolutely deterministic. The immediate symbol completion
in jEdit works great, too, I merely had to learn new sequences of key strokes. Symbol
completion of non-unique results is not satisfactory.

a) Given some text like

definition foo where foo = ...

when I add an attribute like [simp]: after the where, I get a symbol completion popup to
replace the : with the element sign. Usually, my next thing is to move the cursor with the
cursor keys. But the popup gobbles all the key strokes until I explicitly close it with
ESC. As colons are used everywhere in Isabelle's outer syntax, it would really be great if
the popup only appears when I am in inner syntax.

b) Sometimes, when I write a HOL term, I used to not get the completion popup when I enter
something like \un if there were sufficiently many parse errors in that partial term. Even
Ctrl-b did not help. However, I cannot reproduce it in a small example at the moment.

2. Reactivity when processing large files

With PG, I knew how to control the Isabelle prover. When I edit a large file in a larger
project like JinjaThreads, every now and then, Isabelle changes the background colour from
red to gray and then, apparently nothing happens for minutes before Isabelle turns it red
again and starts reprocessing. Is there some way to explicitly tell Isabelle that it
should now start to check again. Toggling continuous checking does not help. Sometimes,
I even have to close the theory file and reopen it again.

3. Navigation between theories files

In PG, I usually have only a small subset of the loaded theories and ML files open as
buffers, and I conveniently switch between them with Ctrl-x b. In jEdit, I use Ctrl-` to
go to the previous file, but going to a different one is a pain, because I have to search
it in the complete list of open files.

It would be great if there was a list of just those files that I had on my screen
previously, not all loaded files.

Moreover, when I close a file and then press Ctrl-` in the file that shows up, I do not
get to the file I have visited before the two, but to some arbitrary other. Can jEdit
remember the order in which files have been visited? XEmacs at least does this.

Maybe there are already solutions to the above annoyances, I just don't know them. There's
another thing I would like to see in jEdit: The window layout has three columns (one dock
on the left and one on the right) and the middle column (with the editor area) can be
divided in three rows (dock - text - dock). Is there some way that I can split the right
column into two rows to show two information areas at the same time (e.g. Output at the
top and Find below)?

Andreas

On 27/04/14 20:14, Makarius wrote:

Are there any remaining uses of Proof General, e.g. in the situation of current
Isabelle/5b6f4655e2f2 ?

This is neither a joke nor a running gag -- I just can't think of anything
myself after
the introduction of the spell checker.

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] Issues with interpretations

2014-04-02 Thread Andreas Lochbihler


Hi Jasmin,

 1. As long as we define new interpretations (hook types) in the HOL image, we 
can
 reorganize the imports to avoid the evil scenarios. Problems arise when users 
define
 their own interpretations.

I already ran into scenario 3 without registering my own interpretations just by using 
code_datatype (which internally uses interpretation, too). Here's the example:


theory A imports Main begin
typedecl foo
consts Foo :: foo
end

theory B imports A begin
code_datatype Foo
end

theory C imports A begin
code_datatype Foo
end

theory D imports A B begin
end

This gives the same error message as in your scenario 3:

Clash of specifications for constant Typerep.typerep_class.typerep:
  ScratchB.typerep_foo_inst.typerep_foo_def
  ScratchA.typerep_foo_inst.typerep_foo_def



 4. If anybody has any ideas on how to address Scenario 3, please let me know!
I don't think that scenario 3 is the one to address. IMO the hooks should behave as if 
they were executed in the name space of the datatype declaration, so size is doing 
something sensible already. Rather do I think that it seems worthwhile to address scenario 
2 by making name space merges more liberal. If there is a duplicate declaration of a 
constant, one could check whether the declarations of the constants are equivalent, and 
accept if so. Since I am not familiar with the internals, I do not know whether such a 
change is feasible in the current implementation.


Andreas

On 02/04/14 15:34, Jasmin Christian Blanchette wrote:

Hi all,

My work on (co)datatypes and my desire to move Quickcheck_Narrowing out of HOL and into Library have lead 
me to discover several issues with the interpretation mechanism (Pure/interpretation.ML) that is used to 
hook into various modules (e.g., the size-generating extension to datatypes). I will summarize 
my findings below. It might well be that this is already (at least partially) known to some of you.

In the following, I will talk concretely about datatype and their various hooks (size, 
Quickcheck random, Quickcheck narrowing, etc.), but the same issues can arise in 
principle with all the other hooking-mechanism based on 
Pure/interpretation.ML.

Generally, the issues arise when a datatype is introduced in theory A and a 
hook is registered in theory B, and A does not import B.


Scenario 1: Two Types, One Name

In this scenario, we introduce two datatypes with the same base name (t) in 
two different theories:

 theory A
 imports ~~/src/HOL/Datatype
 begin

 datatype t = T

 end

 theory B
 imports ~~/src/HOL/Datatype
 begin

 datatype t = U | V

 end

Then we get a name clash at merge time when pulling in a new hook (such as the one 
defined by Typerep below):

 theory C
 imports A B ~~/src/HOL/Typerep
 begin

 end

 *** Duplicate constant declaration C.typerep_t_inst.typerep_t vs. 
C.typerep_t_inst.typerep_t (line 1 of /Users/blanchet/bugs/scenarios/C.thy)
 *** At command theory (line 1 of /Users/blanchet/bugs/scenarios/C.thy)

The examples above are self-contained and can be tested directly against a HOL or a 
Pure image.

What's happening here is that the Typerep is generating theorems that contain the name t but not the unambiguous 
names A.t vs. B.t, and since the merge takes place in C, the prefix is C. for both.

Interestingly, the size hook bypasses the problem by overriding the path using 
Sign.root_path and Sign.add_path. For example, this works:

 theory C2
 imports A B ~~/src/HOL/Fun_Def
 begin

 thm A.size B.size

 end

Hence, my original idea was to solve the name clash problem for all types by replicating the 
size trick, and perhaps to move the logic up either to the individual hooks or even to 
Pure/interpretation.ML. However, this does not solve all problems, as we will see in Scenario 2.


Scenario 2: The Diamond

 theory D
 imports ~~/src/HOL/Datatype
 begin

 datatype t = T

 end

 theory E
 imports D ~~/src/HOL/Fun_Def
 begin

 end

 theory F
 imports D ~~/src/HOL/Fun_Def
 begin

 end

 theory G
 imports E F
 begin

 end

 *** Duplicate constant declaration D.t.t_size vs. D.t.t_size

The problem is that these constants are defined by both E and F with the same 
name, so the merge in G fails.


Scenario 3: The Specification Duplicate

I thought I could work around the issue raised by Scenario 2 by having Isabelle generate names that 
combine the original theory name where the type was introduced and that where the merge took place 
that generated the name. In other words, generate E.D.t.t_size and 
F.D.t.t_size above. I tried this out, and it *almost* works. For the above theory G, it 
gives

 *** Clash of specifications for constant Nat.size_class.size:
 ***   F.D.t.size_t_inst.size_t_def (line 1 of ~/bugs/scenarios/F.thy)
 ***   E.D.t.size_t_inst.size_t_def (line 1 of ~/bugs/scenarios/E.thy)
 *** At command

Re: [isabelle-dev] 'specification' and 'ax_specification'

2014-03-14 Thread Andreas Lochbihler

I myself found specification quite convenient and use it occasionally, e.g., in 
AFP/Containers/Set_Linorder and a number of my private developments. It's a useful 
shortcut to a definition with SOME and deriving the properties later with someI. It would 
be good if it works with contexts. I have never used ax_specification, though.


Andreas

On 14/03/14 14:44, Makarius wrote:

On Fri, 14 Mar 2014, Jasmin Blanchette wrote:


 * HOL/Tools/choice_specification.ML which is loaded into
   HOL/Hilbert_Choice.thy -- really old stuff that would require serious
   renovation if actually used: 'ax_specification' with its unchecked
   axiomatization is actually unsed, and 'specification' only by
   HOL-Auth (and its many clones).

   A candidate for HOL-Library, after removing the axiomatic part?
   Nitpick seems to have special tricks to cope with it, though.


These special tricks could be taken out. They're not vital in any way.


(This deserves its own mail thread.)

Motivated by the surprise about ``code_pred introduces axioms?'' from last 
October
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2013-October/msg00228.html
I've checked the situation more systematically some weeks ago.

Spurious axiomatizations can lead to unpleasant surprises to users that are 
unaware of the
danger.  We probably can't do anything about code_pred now, but check the 
general
situations about further such trapdoors.


So how about 'ax_specification'?  It is an alternate personality of 
'specification' that
would make it very hard to renovate the latter, if that is desirable at all:
'ax_specification' is unused and 'specification' only used in HOL-Auth and its
derivatives, which appears to have been a demo for that.

There are various possibilities:

   (a) Do nothing and let this old stuff collect more dust.

   (b) Remove 'ax_specification' and brush-up 'specification' a little
   (proper local contexts, PIDE markup etc.).

   (c) Remove both 'ax_specification' and 'specification', and do the
   HOL-Auth applications with a hypothetical context, potentially
   with a proven interpretation of the assumptions.


 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] smt2

2014-03-14 Thread Andreas Lochbihler


Hi Jasmin,


On 14/03/14 14:18, Jasmin Blanchette wrote:

Another candidate is Quickcheck_Narrowing.thy. Nothing in HOL seems to 
depend on it, and (please correct me if I'm mistaken) hardly anybody go into the trouble of setting 
up Quickcheck (and GHC) so that it uses the narrowing strategy.
I guess I am the exception to the rule. I have GHC set up and sometimes try 
quickcheck[narrowing]. Sometimes, it does give better results than the random and 
exhaustive generators. To make one's type work with narrowing, however, is hardly 
documented. Recently, I finally got around to provide narrowing generators for Coinductive 
in the AFP (AFP/1fffd2ebbd28), but I had to study all the implementation of the narrowing 
engine and read up on SmallCheck in order to understand just how to do it. We definitely 
cannot expect most users to figure this out themselves.


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

Re: [isabelle-dev] smt2

2014-03-14 Thread Andreas Lochbihler

Hi Jasmin,

On 14/03/14 16:05, Jasmin Blanchette wrote:

Hi Andreas,

Am 14.03.2014 um 15:26 schrieb Andreas Lochbihler
andreas.lochbih...@inf.ethz.ch:

On 14/03/14 14:18, Jasmin Blanchette wrote:

Another candidate is Quickcheck_Narrowing.thy. Nothing in HOL seems to
depend on it, and (please correct me if I'm mistaken) hardly anybody go into the trouble of setting
up Quickcheck (and GHC) so that it uses the narrowing strategy.

I guess I am the exception to the rule. I have GHC set up and sometimes try
quickcheck[narrowing]. Sometimes, it does give better results than the random
and exhaustive generators.

How big an issue is it to you if we move narrowing to Library?
I don't mind if narrowing is moved to HOL-Library, I'll just add another theory to my list
of theories that I usually import. If you do so, please make sure that the connection to
the datatype packages is kept, i.e., narrowing generators are generated for all datatypes
(even those that are defined while narrowing was not in scope).

From what I understand, you already pull in quite a bit from Library, to the extent
that Coinductive is based on the HOL-Library session. And Quickcheck has a nice
generic interface for registering testers at any point, so technically the move should
be nearly trivial.

IIRC, the AFP policy is (was?) that all entries that import at least one theory from
HOL-Library are based on HOL-Library.

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

[isabelle-dev] Pushing to AFP fails

2014-02-18 Thread Andreas Lochbihler

I am trying to push a changeset to Coinductive to the AFP, but I always get the following 
error message:


  remote: abort: could not lock repository /hg/p/afp/code: Permission denied
  abort: unexpected response: empty string

Until last week, hg push used to work well. Has anything changed?

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

Re: [isabelle-dev] [isabelle] primcorec complains about invalid map function

2014-02-13 Thread Andreas Lochbihler


Hi Jasmin,

On 12/02/14 12:11, Jasmin Blanchette wrote:

Hi Andreas,


I saw that you used the discriminator =, but we already have functions 
Option.is_none and List.null. So far, they have been mainly used for code generation, but 
I have found them very convenient in in my codatatype usages when using the destructor 
style. I think it might be worth a try to give these discriminators official status.


I worked from the principle that is_none and List.null are internal constructs and 
used = to avoid generating more theorems about internal things. Can you confirm that the 
convenience you found in your codatatype usage also applies to datatypes?

 If there is a concensus about making them more public, we can remove the = 
trick.
No, the destructor view is not at all convenient for datatypes, because most functions 
pattern match on the constructors. Therefore, it is better the have the constructors 
explicit. Conditional rewrite rules such as List.null xs == set xs = {} help a bit with 
the destructor view, but having many of them in the simpset considerably slows down the 
simplifier.


However, I found the destructor view very useful even for datatypes when codatatypes are 
mixed with datatypes as in the examples that I have posted earlier in this thread 
(https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2014-February/msg00028.html). In the 
destructor view, selectors and discriminators nicely accumulate, so in my proofs, it 
worked better not to switch to the constructor view.


In summary, I do not want to replace _ = None and _ = [] with null and is_none, I'd 
just like to make null and is_none somewhat official. I am not sure when these 
discriminators can show up in practice, but I thought that only primcorec needs them. So 
from my point of view, it seems sensible to make them the official discriminators.


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

Re: [isabelle-dev] [isabelle] primcorec complains about invalid map function

2014-02-13 Thread Andreas Lochbihler


Hi Jasmin,

On 13/02/14 13:47, Jasmin Blanchette wrote:

Hi Andreas,

Am 13.02.2014 um 13:34 schrieb Andreas Lochbihler 
andreas.lochbih...@inf.ethz.ch:


In summary, I do not want to replace _ = None and _ = [] with null and 
is_none, I'd just like to make null and is_none somewhat official. I am not sure when these 
discriminators can show up in practice, but I thought that only primcorec needs them. So from my 
point of view, it seems sensible to make them the official discriminators.


Now I'm confused. If we do what you just proposed, the discriminators end up appearing in some of the 
generated theorems -- and you observed yourself that the destructor view is not at all convenient for 
datatypes, because most functions pattern match on the constructors. Therefore, it is better the have the 
constructors explicit. For a datatype, being an official discriminator basically amounts to 
appearing in generated theorems. Or did I misunderstood something?
I read the comment to your changeset 3def821deb70, which says that Nat.pred may show up in 
theorems generated by primcorec. This is fine, because the destructor view for codatatypes 
goes well with discriminators and selectors for datatypes. As I do not know where 
discriminators show up in theorems generated by datatype_new, but my guess is that they 
only show up in theorems that the old datatype package does not generate. Moreover, I 
expect that they do not show up in anyhing generated by primrec. So where would it harm to 
make them the official discriminators?


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

Re: [isabelle-dev] [isabelle] Code_String: linorder in String.literal

2013-11-28 Thread Andreas Lochbihler


Hi Florian,


a) Char_ord and List_lexord are not tied together, i.e., a user could
import List_lexord, but not Char_ord, define his own version of order on
String.literal and the generated Haskell code compiles, but it is
unsound (even without any further adaptations by the user). One could
solve this by moving the directive from commit 5 to a new theory
Char_ord_List_lexord that imports both Char_ord and List_lexord -- but
is this sensible?


It would be the canonical solution: provide a supremum for two elements
in a lattice.  I don't claim that it is very beautiful.
I have removed the declaration that supresses the class instance for String from 
List_lexord because of point b below and documented the problem (17d76426c7da). If 
necessary, users can issue the declaration on their own, but then it is their responsibility.



b) If both Code_Char and List_lexord are imported, but class instances
for ord are only required for String.literal and not for lists, the code
generator produces no instantiation at all, i.e., the generated code
does not compile. Is there any possibility to tell the code generator
that if a program needs an instance for String.literal, then it also
needs one for 'a list (but only for Haskell, because we don't want to
force users to have any ordering on list)?



String.literal has always been intended as a technical device for code
generation rather than a full-flown first citizen.
Yes, but that's why we should care particularly about code generation and better make sure 
that the existing functions on String.literal are executable. Users are writing 
increasingly complex programs in Isabelle and they want to interface with other code and 
libraries, and String.literal is one of the basic types for exchanging data.


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

Re: [isabelle-dev] Lexical orders on Lists [was: Code_String: linorder in String.literal]

2013-11-28 Thread Andreas Lochbihler


Hi Florian,

 Just a remark on
 http://isabelle.in.tum.de/repos/isabelle/rev/8c0a27b9c1bd: the matter on
 lexicographic orderings in List.thy is now numerous enough but still
 self-contained to justify a separate theory Lexorder.thy.

I agree that a separate theory would be nice. But before doing so, we should also try to 
consolidate what's there already. The current state in List.thy is as follows (8c0a27b9c1bd):


1. lexord :: ('a * 'a) set = ('a list * 'a list) set
   a set version of the irreflexive lexicographic order, the parameter corresponds 
to 
   equality of elements is determined by op =.

2. lexordp ::('a = 'a = bool) = 'a list = 'a list = bool
   the predicate version of lexord, apparently used only for code generation

3. ord_class.lexordp :: 'a list = 'a list = bool
   a predicate version of the irreflexive lexicographic order
   equality of elements x and y is determined by ~ (x  y)  ~ (y  x)

4. ord_class.lexordp_eq :: 'a list = 'a list = bool
   a predicate version of the reflexive lexicographic order,
   equality of elements x and y is determined by ~ (x  y)  ~ (y  x)

5. lexn defines the length-lexicographic order where only lists of the same
   length are comparable (listed here only for completeness).

3 and 4 also yield parametrized versions ord.lexordp and ord.lexordp_eq where the 
parameter corresponds to op .


While definitions 1 to 4 yield the same when the order on the elements is linear, they 
differ in the details when they are not. I think that none of 1 to 4 is optimal, because:


(i) 1 and 2 explicitly use HOL equality which need not be related to the ordering that is 
passed in (e.g. in a quasi-order) -- they also make the functions dependent on the 
equality type class for code generation, which is a problem for AFP/Containers.


(ii) For non-linear quasi-orders, 3 and 4 do not work well, because they consider all 
unrelated elements as equal, even if they belong to different equivalence classes of the 
quasi-order.


If I could start from scratch, I would define a predicate version like 4, but with 
equality of x and y determined by x = y  y = x. Then, however, the order parameter 
would change from irreflexive to reflexive. I do not know how much breaks if we attempt 
such a change.



I would also
suggest that the predicate version should be done using locales rather
than the canonical type class.


Using the canoncial type class has the advantage that I can write

  lexordp_eq [1,2] [1,3]

and obtain the order on the elements implicitly. With a locale, it is more complicated to 
achieve the same effect.


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

Re: [isabelle-dev] [isabelle] Code_String: linorder in String.literal

2013-11-20 Thread Andreas Lochbihler

Hi René and Florian (and other experts in code generation),

I move this thread from users to dev because it is now getting into detailed discussions
and commit ids.

I've moved my setup for String.literal from Containers to the distribution and pushed the
changes to testboard), but I realised that this is not going to work for Haskell. Even
René's simpler theory file does not produce valid Haskell code. The problem is that
String.literal is mapped to Haskell's type String, but String is a type synonym for
[Char]. Therefore, the Haskell compiler rejects the instantiation

instance Orderings.Ord String where ...

because String = [Char] is not a type constructor. Such instantiations are only generated
when we apply a polymorphic operation which depends on ord is applied to String.literal.
For example:

definition compare where compare = op
definition foo where foo = compare (STR ''a'') (STR ''b'')
export_code foo in Haskell

Overall, we have the following cases to consider when a user invokes export_code and
String.literal is an instance of linorder.

1. 'a list is an instance of linorder using the lexicographic order as in
List_lexord.
This case is simple, we could solve it by declaring to the code generator not to produce
an instantiation for String.literal.

code_printing class_instance String.literal :: linorder = (Haskell) -

2. 'a list is an instance of order with some order other than the lexicographic order
(e.g., as in Library/Prefix_Order). Then, I see no way to solve the problem, because

the two terms

compare (STR ''a'') (STR ''b'')
compare ''a'' ''b''

produce exactly the same Haskell code, but they should evaluate differently. In
particular, the code_printing directive from point 1 would be unsound.

3. 'a list is not an instance of ord. Then, it would be safe to produce a linorder
instantiation for 'a list, but I doubt that the code generator provides such a facility.

Despite case 2, I am still not convinced that linorder on String.literal should require
the lexicographic order on 'a list in the logic. So far, I have done the following:

1. Add a predicate version for a lexicographic order on lists
(http://isabelle.in.tum.de/testboard/Isabelle/rev/8c0a27b9c1bd)

2. Setup lifting for String.literal
(http://isabelle.in.tum.de/testboard/Isabelle/rev/a2d1522cdd54)

3. String.literal instantiates linorder in Library/Char_ord.
(http://isabelle.in.tum.de/testboard/Isabelle/rev/a2eeeb335a48)

4. Library/Code_Char sets up the code_printing for less/less_eq on
String.literal.
(http://isabelle.in.tum.de/testboard/Isabelle/rev/368c70ee1f46)

5. Library/List_lexord issues the class_instance directive from case 1.
(http://isabelle.in.tum.de/testboard/Isabelle/rev/4af7c82463d3)

Unfortunately, I am not completely happy with the setup for Haskell, because

a) Char_ord and List_lexord are not tied together, i.e., a user could import List_lexord,
but not Char_ord, define his own version of order on String.literal and the generated
Haskell code compiles, but it is unsound (even without any further adaptations by the
user). One could solve this by moving the directive from commit 5 to a new theory
Char_ord_List_lexord that imports both Char_ord and List_lexord -- but is this sensible?

b) If both Code_Char and List_lexord are imported, but class instances for ord are only
required for String.literal and not for lists, the code generator produces no
instantiation at all, i.e., the generated code does not compile. Is there any possibility
to tell the code generator that if a program needs an instance for String.literal, then it
also needs one for 'a list (but only for Haskell, because we don't want to force users to
have any ordering on list)?

c) If List_lexord is not imported, but the type class instance for String.literal is
required, the generated Haskell code does not compile.

Do you have any ideas or opinions on that?

Best,
Andreas

PS: Similar problems already occur for the size instance of String.linorder in
Isabelle2013-1, so linorder is not the only problematic case.

On 19/11/13 17:32, René Neumann wrote:

Am 19.11.2013 17:10, schrieb Andreas Lochbihler:

Hi René,

I needed linorder on String.literal, hence I came up with the theory as
in the attachment. It explicitly uses lexord, and only later lifts it to
op , to explicitly show what the order is and not rely on 'magic' from
the (lin)ord(er) class.

Your detour via lexord does not buy you anything, because your theory
depends on List_lexord and therefore imposes the lexicographic order on
lists. Unfortunately, we have two competing order instantiation for
lists in Isabelle (lexicographic order and prefix order). I think that
it is sensible to pick lexicographic orders for String.literal, but this
choice should restrict the choice for list (and string as the type
synonym for char list). In the current version, your theory forces the
lexicographic order on list, too.

It also

Re: [isabelle-dev] [isabelle] General code_abort'd constant

2013-09-27 Thread Andreas Lochbihler


Hi Florian,

in 2b761d9a74f5, I now have replaced Predicate.not_unique with Code.abort. I decided to 
leave Enum.the as is, because there is a special translation for the Eval target such that 
Enum.the raises Match instead of Fail (although I do not know whether the specific setup 
is important).


Andreas

On 26/09/13 17:50, Florian Haftmann wrote:

Hi Andreas,


See now 788730ab7da4, which replaces all code_abort in HOL/Library with
Code.abort.
There are still two code_aborts in HOL (in Predicate and Enum) that
Code.abort should subsume, but Code.abort can only be defined in
String.thy due to the error message parameter it takes, and Predicate
and Enum do not import String. As I am not familiar with the HOL import
graph, I don't know whether one could easily change it such that
Code.abort is available in Predicate and Enum. But even if it is, this
is probably not going to happen before the release.


Making Predicate.thy dependent on String.thy is no problem.  The reason
why Enum.thy is bootstrapped before String.thy is that »enum« allows for
a nice code setup which is also valid in presence of Code_Char.thy.
However you arrange it, there is always one piece of code setup which
cannot be bootstrapped from the beginning.

Hope this helps,
Florian


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

Re: [isabelle-dev] [isabelle] New representation of naturals in Code_Target_Numeral decreases generated code performance

2013-09-20 Thread Andreas Lochbihler


Hi Florian,

newtype in Haskell is not always for free, see for example Joachim's blog post: 
http://www.joachim-breitner.de/blog/archives/610-Adding-safe-coercions-to-Haskell.html


Andreas

On 19/09/13 12:58, Florian Haftmann wrote:

Hi Peter,


When using Code_Target_Numeral instead of the old Efficient_Nat, the
code generator wraps some funny dummy-datatype (nat = Nat of int) around
my natural numbers.

What was the reason behind this change, and is there a way to produce
code working with plain IntInf?


There have been two reasons:
* Proper datatype abstractions: negative integers are not natural
numbers; no explicit check necessary for subtraction of natural numbers.
* When Haskell type classes or Scala implicits are involved, it is
necessary that the mapping of HOL types to target language types is
injective.  The coping with this was nightmare in the previous situation
and is now straight-forward.

As a preface, I have checked these change previously against
Flyspeck_Tame and did not notice any performance difference.


For one of my benchmarks (heavy use of arrays in
Imperative-HOL) this results in doubling the runtime under PolyML. Under
mlton, its only around 15% slower.


Quoting Andreas:

In many cases, such type copies do not affect performance, because the compiler 
can get rid of such type copies after type checking. However, when they are 
nested into some other polymorphic type, this is not always possible. Maybe, 
arrays fall into that class.


I am not sure about that.  If this is the case then I wonder how the
contract in Haskell that »newtype« declarations are always compiled away
is accomplished in Haskell.  Or maybe there is some ML subtlety creeping
in here?  Maybe we should contact David Matthews on that.

Another possibility is that the code setup for Imperative-HOL contains a
performance flaw.  Have you a change to figure out which functions are
the top-wasters in your benchmark?  Then we could inspect these.

Hope this helps,
Florian



___
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] [isabelle] General code_abort'd constant

2013-09-20 Thread Andreas Lochbihler


Hi Jasmin,

I moved this thread from users to devel, because we are now referring to 
changesets ;-).


I would appreciate if all these code_aborts that you mention were consolidated 
to use Code.abort.


I second this. Cf. http://goo.gl/4kR3vu :)

See now 788730ab7da4, which replaces all code_abort in HOL/Library with 
Code.abort.
There are still two code_aborts in HOL (in Predicate and Enum) that Code.abort should 
subsume, but Code.abort can only be defined in String.thy due to the error message 
parameter it takes, and Predicate and Enum do not import String. As I am not familiar with 
the HOL import graph, I don't know whether one could easily change it such that Code.abort 
is available in Predicate and Enum. But even if it is, this is probably not going to 
happen before the release.


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

Re: [isabelle-dev] including raises Attempt to perform non-trivial merge of theories

2013-09-02 Thread Andreas Lochbihler


Hi Makarius,

The error has already gone away in cb82606b8215 when Ondřej moved all the Quotient_... 
theories to Main, i.e., there was no non-trivial merge necessary any more. My concrete 
application works as expected at the moment.


Andreas

On 02/09/13 12:56, Makarius wrote:

On Tue, 13 Aug 2013, Andreas Lochbihler wrote:


I get the error Attempt to perform non-trivial merge of theories when I 
include a
bundle from another theory and there are at least two imports. In the 
attachment,
there's an example.


This should work in Isabelle/ef65d5ee60cf.  Are there any remaining problems in 
the
concrete application behind the example?


 Makarius

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

[isabelle-dev] conflict between code_identifier constant and module_name

2013-09-02 Thread Andreas Lochbihler

Two months ago, Florian replaced code_module with code_identifier (6646bb548c6b). Now, I 
am having trouble using the greater capabilities of code_identifier. I would like to 
assign a constant to a different module, say


code_identifier constant replicate \rightharpoonup (SML) My_Module.rep

Then, code generation works fine as long as there is no module_name involved:

definition test where test = replicate
export_code test in SML
export_code test in SML module_name foo (* fails due to module dependency 
cycles *)

Unfortunately, many idioms internally use module_name -- for example, all of the following 
raise errors due to module dependency cycles:


ML {* @{code test} *}
value [code] test 3 (0 :: nat)
lemma test = foo quickcheck

The same problem also occurs with type constructors. Therefore: What is the intended way 
of using code_identifier with constants?


Best,
Andreas


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

[isabelle-dev] including raises Attempt to perform non-trivial merge of theories

2013-08-13 Thread Andreas Lochbihler


Dear all,

in Isabelle abd760a19e22, I get the error Attempt to perform non-trivial merge of 
theories when I include a bundle from another theory and there are at least two imports.

In the attachment, there's an example.

Best,
Andreas


Scratch.thy
Description: application/extension-thy


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

Re: [isabelle-dev] Problems with Code-Generator

2013-08-12 Thread Andreas Lochbihler


Hi René,

Florian has reworked the setup for target language numerals. I can at least explain why 
you run into the error and provide a workaround.


Code_Target_Nat implements the type nat as an abstract type (code abstype) with 
constructor Code_Target_Nat.Nat, i.e., Code_Target_Nat.Nat must not appear in any equation 
of the code generator. Unfortunately, this declaration also sets up the term_of function 
for type nat to produce terms with this constructor. In the second example, your 
import_proof method uses the term_of function to get a term for the given proof (and the 
number contained in the proof) and introduces along with this number into the goal state.
As term_of uses the forbidden constructor Code_Target_Nat.Nat, when you then apply eval, 
the code generator complains that the abstract constructor is part of the goal state.


The simplest solution is to introduce a new constructor for which you can prove a code 
equation. For example, the following defines a constructor Nat2 and redefines term_of for 
naturals to use Nat2. When you add it to your theory before declaring the parser 
structure, the second example works, too (tested with Isabelle 2b68f4109075). You then 
also have to reflect both nat and int as datatypes.


definition Nat2 :: integer = nat
where [code del]: Nat2 = Nat

lemma [code abstract]: integer_of_nat (Nat2 i) = (if i  0 then 0 else i)
unfolding Nat2_def by transfer simp

lemma [code]:
  term_of_class.term_of n =
   Code_Evaluation.App
 (Code_Evaluation.Const (STR ''Test_Import.Nat2'')
(typerep.Typerep (STR ''fun'')
   [typerep.Typerep (STR ''Code_Numeral.integer'') [],
 typerep.Typerep (STR ''Nat.nat'') []]))
 (term_of_class.term_of (integer_of_nat n))
by(simp add: term_of_anything)

If nobody has a better solution, we should think of including this setup in 
Code_Target_Nat.

Hope this helps,
Andreas

On 12/08/13 10:53, René Thiemann wrote:

Dear all,

Chris and I have recently ported our libraries IsaFoR and TermFun to the 
development version which worked nicely, except for one issue, which arises 
when we want to import external proofs into Isabelle.

The below theory compiles in Isabelle 2013 without problems.

The problem is that no matter, how we adjust the imports / code_reflect 
settings,
we get different errors with the repository version (6a7ee03902c3) when 
invoking the apply eval statement in the last proof:

importing ~~/src/HOL/Library/Code_Target_Numeral, no code_reflect:
   works, but not desired

importing ~~/src/HOL/Library/Code_Target_Numeral, code_reflect mentions nat, 
but not int (as it worked in 2013):
Error: Type error in function application.
Function: Checker.checker : Checker.inta - Checker.proof - bool
Argument: (Int_of_integer (25 : IntInf.int)) : inta
Reason: Can't unify Checker.inta with inta (Different type constructors)

importing ~~/src/HOL/Library/Code_Target_Numeral, code_reflect mentions both 
int and nat:
   previous error disappears, but Abstraction violation: constant 
Code_Target_Nat.Nat in last apply eval

importing ~~/src/HOL/Library/Code_Target_Numeral, code_reflect mentions only 
int, but not nat:
   same as before

trying to also load Code_Binary_Nat also did not help.

Any feedback is welcome.
Cheers,
René




theory Test_Import
imports Main
   ~~/src/HOL/Library/Code_Char
(* in repository: ~~/src/HOL/Library/Code_Target_Numeral *)
(* in 2013: *)
   ~~/src/HOL/Library/Code_Integer
   ~~/src/HOL/Library/Code_Natural
begin

definition parse_digit :: char = nat where
   parse_digit c = (
 if c = CHR ''0'' then 0 else
 if c = CHR ''1'' then 1 else
 if c = CHR ''2'' then 2 else
 if c = CHR ''3'' then 3 else
 if c = CHR ''4'' then 4 else
 if c = CHR ''5'' then 5 else
 if c = CHR ''6'' then 6 else
 if c = CHR ''7'' then 7 else
 if c = CHR ''8'' then 8 else 9)

datatype proof = N nat | I int

definition parse_proof :: string = proof where
   parse_proof input = (case input of
  t # d # _ =
  if t = CHR ''n'' then N (parse_digit d)
  else I (of_nat (parse_digit d)))

definition parse_proof_term :: string = Code_Evaluation.term where
   parse_proof_term input == Code_Evaluation.term_of (parse_proof input)

ML {*
structure Parser =
struct
   val parse = String.explode # @{code parse_proof_term}
end
*}

fun checker :: int = proof = bool where
   checker n (N i) = (of_nat i * of_nat i = n)
| checker n (I i) = (i * i = n)

lemma checker_imp_square: checker n p ⟹ ? x. x * x = n
   by (cases p, auto)

(* precompilation of checker-code, so that it does not need to
be recompiled on every invokation of eval later on,
strangely, in 2013 only nat must be registered as datatype, but not int *)
code_reflect Checker
   datatypes (* in repo: int = _ and *) nat = _ and proof = _
   functions checker Trueprop
declare checker_def[code del]


setup {*
   let
 fun import_proof_tac ctxt input i =
   let
 val thy = Proof_Context.theory_of

Re: [isabelle-dev] New (Co)datatypes: Status Plan (FYI)

2013-08-05 Thread Andreas Lochbihler


Hi Christian,

the two different size functions become relevant as soon as you have a polymorphic 
datatype such as


datatype 'a foo = Foo 'a | Bar 'a foo

Then, foo_size takes size function for every type variable as additional parameters and 
takes them into account, whereas size ignores occurrences of the type variables.


thm foo.size

foo_size fa (Foo a) = fa a + Suc 0
foo_size fa (Bar foo) = foo_size fa foo + Suc 0
size (Foo a) = 0
size (Bar foo) = size foo + Suc 0

The generalised size function can be useful in termination proofs such as

function f :: nat foo = unit where
  f (Foo 0) = ()
| f (Foo (Suc n)) = f (Foo n)
| f (Bar x) = f x
by pat_completeness simp_all
termination by(relation measure (foo_size size)) simp_all

Andreas


On 04/08/13 21:20, Christian Urban wrote:



On Sunday, August 4, 2013 at 20:32:50 (+0200), Dmitriy Traytel wrote:
   I.e. everything that is defined by the new package and
   falls into the fragment of the old package can be registered as an old
   datatype benefiting from all the infrastructure built around it (e.g.
   size function, Quickcheck, and other datatype interpretations).

On the topic of size functions: I found it always odd that
the existing datatype package (however I think this particular
functionality is now provided by the function package) defines
under datatype_name.simps two definitions of the corresponding
size function. Consider for example


   datatype test = A1 | A2 | A3 test

   thm test.size

test_size A1 = 0
test_size A2 = 0
test_size (A3 ?test) = test_size ?test + Suc 0
size A1 = 0
size A2 = 0
size (A3 ?test) = size ?test + Suc 0


Surely, it would be more uniform to have just the equations for
size, no? Is there any usage for the test_size definitions?
If not, then maybe in the course of updating the datatype
package, this oddity can be eliminated (Nominal needed to work
around it). But I am happy to admit that I might miss something
important.

Best wishes,
Christian


___
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] Should code_abort remove the corresponding code equations?

2013-07-18 Thread Andreas Lochbihler

Hi Florian,

On 18/07/13 12:00, Florian Haftmann wrote:

Should code_abort remove the code equation for test? Otherwise the
resulting program might be non-terminating.

I have often run into this problem myself, too, especially in case of
non-termination. I would find it sensible that code_abort deletes the
code equation.

Good equestion. Generally, the code generator does not enforce any
constant to have corresponding code equations. Of the different target
mechanisms (simp, nbe, code) only the latter has an explicit check
whether code equations are present, and this is where code_abort comes in.

Right, but it is not really about the check.
A frequent use case for code_abort is the following:

definition error_case_for_f where error_case_for_f = f

code_abort error_case_for_f

lemma [code]:
f x =
(if test for error condition x
then error_case_for_f x
else do something sensible)

The definition implicitly declares error_case_for_f = f as a default code equation, and
this is still present. If one then generates code (or use simp and nbe), one will get
non-termination for the then branch (and quickcheck can be quite successful in picking the
then branch!). It is just annoying that I have to manually delete the default code equation.

And it is important to really delete it, it does not suffice to change the behaviour of
code_abort in the code target: then, one would run into non-termination with simp and nbe,
which are even harder to debug than the generated code.

Maybe two situations should be distinguished:
* Constants which didn't see any code declaration ever.
* Constants whose code equations have been explicitly deleted.

The first would raise an error, whether the latter would be translated
as exception.
I am not sure I get what you mean here: Do you suggest that code_abort could be eliminated
in favor of this heuristics (if one has deleted the code equation for a constant, the code
generator will implicitly treat it like a code_abort? I am quite happy with explicit
code_abort declarations, because this protects users from overlooking missing equations. I
don't want to grep the generated code for such implicit exceptions all the time.

And I also don't fully understand the first situation. Today, the frequently used
definition packages generate some default code declaration (function, primrec, definition
do, but not (co)inductive(_set), defs, specification). So I'd argue that most constants
nowadays see a code declaration.

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

Re: [isabelle-dev] Should code_abort remove the corresponding code equations?

2013-07-09 Thread Andreas Lochbihler


Hi Johannes,

I have often run into this problem myself, too, especially in case of non-termination. I 
would find it sensible that code_abort deletes the code equation.


Andreas

On 09/07/13 15:28, Johannes Hölzl wrote:

Hi *,

code_abort does not remove the corresponding code equations
(in Isabelle 19764bef2730)

   definition test = True
   code_abort test
   value [code] test -- outputs True

   definition [code del]: test2 = True
   code_abort test2
   value [code] test2 -- raises 'test' exception

Should code_abort remove the code equation for test? Otherwise the
resulting program might be non-terminating.

Greetings,
  - Johannes

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

Re: [isabelle-dev] AFP sitegen

2013-06-06 Thread Andreas Lochbihler

Sorry for the confusion, I never ran sitegen.py myself because I thought that to be the 
priviledge of the editors. As Gerwin has found out, I dropped these links manually in 
376347e6131a because they all were broken after the update on sourceforge. I decided not 
to update them for three reasons:


1. Most other entries do not link to changeset revisions; Category is now the only 
exception. Often they don't even mention the revision ID at all.


2. It is unclear when the links will break again if they are not checked 
automatically.

3. On the entry page, the links are visually the most prominent part of the change 
history, although they are the least relevant bit of information in the change history.


If sitegen.py automatically links to the changesets, I'd be happy. But then, I suggest 
that the links are not formatted as highlighted as they are now.


Andreas

On 06/06/13 08:09, Gerwin Klein wrote:

It looks like Andreas dropped these manually for his entries, so nothing really 
went wrong with the tools, he was just reacting to the sourceforge update 
leading to broken links.

The URL scheme for linking to revision IDs in the new sourceforge setup is

http://sourceforge.net/p/afp/code/ci/change-set-hash

The short hashes that we normally use seem to work fine (it shows you long ones 
by default when you browse).

It's up to the authors to have change set ids as links or not, so I'm not 
adding them back in myself. If Andreas is reading this and prefers having them 
in, by all means put them back.

We haven't really made up our minds if developers should run admin/sitegen 
after updating history in metadata. I'd say, if you feel comfortable using 
sitegen and check that your changes are confined to history (as Chris 
apparently did), this is Ok to do. If you're not feeling comfortable doing this 
yourself, you change will just show up on the devel website the next time 
someone runs sitegen.

We could try make sitegen.py aware of hg revision ids and make it link them 
automatically. If there's a volunteer for implementing this, I'm happy to 
consider this.

Cheers,
Gerwin

On 06.06.2013, at 1:52 PM, Gerwin Klein gerwin.kl...@nicta.com.au wrote:


I'll have a look at it. The links shouldn't be dropped, something is going 
wrong there.

Cheers,
Gerwin

On 06/06/2013, at 1:48 PM, Christian Sternagel c.sterna...@gmail.com wrote:


Btw: the links do not seem to work anyway. But why not replace them with 
working links instead of just dropping them?

On 06/06/2013 12:40 PM, Christian Sternagel wrote:

Dear all,

to update the change history of one of my AFP entries, I ran
admin/sitegen. I noticed that as a result some other sites changed too.
All the changes where along the lines of

-(revision a
href=http://afp.hg.sourceforge.net/hgweb/afp/afp/rev/f74a8be156a7;f74a8be156a7/a)br

+(revision f74a8be156a7)br

in corresponding *.shtml files, i.e., links to changesets are replaced
by the mere short-form changeset ID. Is this on purpose or did I do
something wrong? (I will of course refrain from pushing any changes
until I got an answer.)

cheers

chris



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

Re: [isabelle-dev] I don't understand isatest AFP report

2013-05-15 Thread Andreas Lochbihler

Here's a summary of the story with Containers:

AFP/db25a6127308 to AFP/58dc11da7731 add the Containers entry to AFP-devel in the version
that works with Isabelle2013.

In AFP/664abd899c58, Gerwin dropped the import of Code_Char_ord that Florian removed in
Isabelle/599ff65b85e2. This implicitly dropped the import of Char_ord, which caused some
even more errors.

In AFP/599ff65b85e2, Dmitriy dropped the session Containers-Benchmarks to avoid crashes in
the build tool.

AFP/3f56bba4ee3a contains all the necessary adaptations to run with Isabelle/ae755fd6c883
and re-activates Containers-Benchmarks.

Unfortunately, this situation lasted only for less than 4 hours. Isabelle/a4d81cdebf8b
breaks Containers again, but Ondřej did not notice because the AFP test report is strange.

Andreas

On 15/05/13 13:09, Makarius wrote:

On Wed, 15 May 2013, Ondřej Kunčar wrote:

This is the last report about AFP from isatest:
The status of the following AFP entries changed or remains FAIL:
[Containers] was removed. Last status was ok.
[Launchbury] is new. Status is ok.

Full entry status at http://afp.sourceforge.net/status.shtml

AFP version: development -- hg id 3f56bba4ee3a
Isabelle version: devel -- hg id e116eb9e5e17
Test ended on: macbroy2, Tue May 14 12:28:46 CEST 2013.

It says that Containers was removed. But does it actually mean FAIL? Because
Containers
is currently broken because of my changeset but I didn't learn about it. And
this web
page doesn't list Containers at all (because it was removed? but it's still in
the
repository though): http://afp.sourceforge.net/status.shtml

I am also confused, and still trying to catch up with the ups and downs of this
new
session. Yesterday I had a working situation in Isabelle/ae755fd6c883 and
AFP/0b521abc0487.

I have also spent some time to robustify the Isabelle build process (leading up
to
Isabelle/5fdca5bfc0b4) to prevent sessions bombing the JVM by producing tons of
output.
Here it is via higher-order unification going amiss and producing lots of
tracing
messages. I guess that is actually coming from some transfer tools.

We've had several surprises about HO-unification from TUM people recently, but
I am still
lagging behind to follow-up on all that. (Basically, fully-general HO is
rather ambitious
and rarely used systematically in tool implementations these days.)

Makarius

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

[isabelle-dev] Problem with simproc enat_eq_cancel

2013-03-01 Thread Andreas Lochbihler


Dear all,

in the repository (8a635bf2c86c) and in Isabelle2013, there seems to be 
something wrong with the enat_eq_cancel simproc in Extended_Nat. Can 
someone please look into this? Here's a minimal example:


theory Scratch imports
  ~~/src/HOL/Library/Extended_Nat
begin

definition epred :: enat = enat
where epred n = n - 1

lemma epred_iadd1: a ~= 0 == epred (a + b) = epred a + b
apply(simp add: epred_def)

I would have expected that the call to simp at least unfolds epred_def, 
but it raises the following error:


*** Proof failed.
*** (a + b - 1 = a - 1 + b) = (a + (b + - 1) = a + (- 1 + b))
***  1. (a + b - 1 = b + (a - 1)) = (a + (b + - 1) = a + (b + - 1))
*** The error(s) above occurred for the goal statement:
*** (a + b - 1 = a - 1 + b) = (a + (b + - 1) = a + (- 1 + b))
*** At command apply

The simp trace with simp_debug enabled ends as follows:

[1]Trying procedure Extended_Nat.enat_eq_cancel on:
a + b - 1 = a - 1 + b

simp_trace_depth_limit exceeded!


When I disable the simproc, I am able to prove the lemma:

using [[simproc del:enat_eq_cancel]]
apply(cases a b rule: enat.exhaust[case_product enat.exhaust])
apply(simp_all add: epred_def eSuc_def one_enat_def zero_enat_def split: 
enat.splits)

done

By the way, why does the failure in the simproc yield a proof error at 
all? Usually, simp does not raise Proof failed if it gets stuck somewhere.


Best,
Andreas
___
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

2013-01-31 Thread Andreas Lochbihler


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

On 01/31/2013 12:48 PM, Amine Chaieb wrote:

Hi,

I came across a situation where the order of sublocale declarations
makes a difference in the theory development, which in this case is not
clear to me. Can anyone please clarify the following behaviour within
the simplified case below? Is the behaviour due to purely technical
reasons or is there a deeper sense?

The theory basically defines two locales A and B, which are equivalent
when the parameter is transformed. Within locale A I have an
abbreviation depending on a local fixed parameter. Suppose I have proved
several interesting lemmas for locale A and would like to transfer them
to locale B and vice vesa. The order in which the sublocale declarations
between A and B appear indeed matters (in the form of the presence of an
error related to duplicating the abbreviation declaration)

theory Test
   imports Main
begin

fun iter:: nat \Rightarrow ('a \Rightarrow 'a) \Rightarrow ('a
\Rightarrow 'a \Rightarrow 'a) \Rightarrow 'a \Rightarrow 'a where
   iter 0 f0 f = f0
   | iter (Suc n) f0 f = (\lambdax. f (iter n f0 f x) x)

locale A = fixes f:: int \Rightarrow int \Rightarrow int
   assumes \And a. f a 1 = a 
begin

abbreviation fpower:: int \Rightarrow nat \Rightarrow int (infixr
^f 80) where
   fpower x n == iter n (\lambdax. f 0 1) f x
end

locale B  = fixes g :: int \Rightarrow int \Rightarrow int
   assumes \And a. g a 0 = a

definition d:: (int \Rightarrow int \Rightarrow int) \Rightarrow
(int \Rightarrow int \Rightarrow int)
   where d f = (\lambda a b. 1 - f (1 - a) (1 - b))

lemma dd[simp]: d (d f) = f
   by (simp add: d_def)


lemma AB_iff[simp]: B (d f) = A f
apply (auto simp add: A_def B_def d_def)
apply (erule_tac x=1 -a in allE)
apply simp
done

lemma BA_iff[simp]: A (d g) = B g
   using AB_iff[where f = d g]
   by simp


---

Since A and B are equivalent I introduce a transitional locale for A,
to avoid infinite sublocale relationship

locale AB = A

Now to sublocale: In this order:

sublocale B  A d g
   unfolding BA_iff ..

sublocale AB  B d f
   unfolding AB_iff ..

I get an error at the second sublocale declaration:

*** Duplicate constant declaration local.fpower vs. local.fpower
(line 13 of /home/ac/tmp/Test.thy)
*** At command sublocale (line 43 of /home/ac/tmp/Test.thy)

In this order however, everything works fine:

sublocale AB  B d f
   unfolding AB_iff ..

sublocale B  A d g
   unfolding BA_iff ..

Is there a reason I am missing?

Thank you in advance,
Amine
___
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] Order of sublocale declarations

2013-01-31 Thread Andreas Lochbihler


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

Re: [isabelle-dev] NEWS: more informative errors in lazy enumerations

2012-10-18 Thread Andreas Lochbihler


Hi Makarius,

 Side remark:

 Does anybody remember a use of the 'apply_end' command?
Yes, there are two in JinjaThreads (theory J/ProgressThreaded), although they 
could be fused into the qed. However, I regularly use apply_end when I develop 
the method call for qed to finish off all the remaining cases after having dealt 
with the interesting ones. It usually saves me reprocessing the first 42 goals 
when goal 43 needs another intro/simp/elim rule - and I can interactively 
explore goal 43 immediately. Before I knew about apply_end, I used case goal_43 
thus ?case, but proof methods behave differently there, because the variables 
are fixed in the context (e.g., tuples are not split automatically).


So I opt for keeping apply_end.

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

Re: [isabelle-dev] JinjaThreads does not compile

2012-06-04 Thread Andreas Lochbihler


Hi Stefan,


while doing a testall on the AFP, I noticed that JinjaThreads no longer
compiles. I get the error

*** exception Match raised (line 146)
***
*** At command ML (line 145 of 
/mnt/home/berghofe/isabelle/afp/thys/JinjaThreads/Examples/BufferExample.thy)

This should be now fixed in Isabelle 02d64fd40852.

I also removed the obsolete reference to FinFun in JinjaThreads/Basic
(AFP b060f6386ebc).

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

Re: [isabelle-dev] Nominal and FinFuns from the AFP

2012-05-31 Thread Andreas Lochbihler

Hi Makarius,

At some point, when I have bundles ready to work with the existing
notation commands, we can fine-tune this scheme further, to allow users to
'include' syntax in local situations.
I tried to implement the new syntax for FinFuns with bundles and Brian's
notation attribute
(https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/2012-April/002585.html),
but it was not satisfactory.

There were two show stoppers:

1. I did not know how to get dynamic bundles, i.e., how to add declarations one
after the other to a bundle. Hence, I would have to introduce all the notation
in a single place before which all constants must have been defined.

2. Theory-level commands like interpretation do not work inside an auxiliary
context and neither can they cope wth includes. Hence, I cannot use such
pretty syntax in the parameter instantiations for interpretation. This possibly
also applies to the where clause although I did not need that for FinFun.

Andreas

--
Karlsruher Institut für Technologie
IPD Snelting

Andreas Lochbihler
wissenschaftlicher Mitarbeiter
Am Fasanengarten 5, Geb. 50.34, Raum 025
76131 Karlsruhe

Telefon: +49 721 608-47399
Fax: +49 721 608-48457
E-Mail: andreas.lochbih...@kit.edu
http://pp.info.uni-karlsruhe.de
KIT - Universität des Landes Baden-Württemberg und nationales Forschungszentrum
in der Helmholtz-Gemeinschaft

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

Re: [isabelle-dev] Merge-Sort Implementation (and a question, on induction_schema)

2011-11-03 Thread Andreas Lochbihler


Hi Christian,

I am not completely sure what you mean. It is possible to leave key out of the 
conclusion in sequences_induct.


lemma sequences_induct[case_names Nil singleton IH]:
  assumes P [] and !!x. P [x]
  and !!a b xs. [| key b  key a == P (drop_desc key b xs);
   ~ key b  key a == P (drop_asc key b xs) |]
   == P (a # b # xs)
  shows P xs
using assms by (induction_schema)(pat_completeness, lexicographic_order)

However, when you apply this rule using induct, key is not instantiated by 
unification. In order to use the case Nil syntax in Isar proofs, you must 
explicitly instantiate key in the induction method via the taking clause. 
Otherwise, key is left as an unbound variable in the goal state.

For example:

proof(induct xs taking: concrete_key rule: sequences_induct)

Andreas

--
Karlsruher Institut für Technologie
IPD Snelting

Andreas Lochbihler
wissenschaftlicher Mitarbeiter
Adenauerring 20a, Geb. 50.41, Raum 031
76131 Karlsruhe

Telefon: +49 721 608-47399
Fax: +49 721 608-48457
E-Mail: andreas.lochbih...@kit.edu
http://pp.info.uni-karlsruhe.de
KIT - Universität des Landes Baden-Württemberg und nationales Forschungszentrum 
in der Helmholtz-Gemeinschaft

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

Re: [isabelle-dev] Merge-Sort Implementation (and a question, on induction_schema)

2011-11-02 Thread Andreas Lochbihler


Dear Christian,

 I ironed out the apply-style snippets and simplified some proofs. Also
 Christian's pointer to induction_schema significantly shortened the
 proof of an induction schema I use (sequences_induct).
 induction_schema is really useful! However, another induction schema
 (merge_induct) seems to be wrong for induction_schema. Maybe because
 of an additional assumption? Any ideas?
Induction_schema is picky about the order of assumptions. Additional assumptions 
(typically those for consumes) must be fed into the induction_schema method 
*after* the inductive cases. Moreover, in your lemma sorted_merge_induct, P 
must not take key as argument because all inductive cases simply pass key on 
to P. Otherwise, induction_schema does not terminate. Note that it is not 
necessary to have the key parameter either because unification instantiates 
key when it consumes the first assumption.


Here's how sorted_merge_induct works with induction_schema:

lemma sorted_merge_induct[consumes 1, case_names Nil IH]:
  fixes key::'b \Rightarrow 'a
  assumes sorted (map key xs)
and \Andxs. P xs []
and \Andxs y ys. sorted (map key xs) \Longrightarrow
P (dropWhile (\lambdax. key x \le key y) xs) ys
\Longrightarrow P xs (y#ys)
  shows P xs ys
using assms(2-) assms(1)
apply(induction_schema)

Andreas

--
Karlsruher Institut für Technologie
IPD Snelting

Andreas Lochbihler
wissenschaftlicher Mitarbeiter
Adenauerring 20a, Geb. 50.41, Raum 031
76131 Karlsruhe

Telefon: +49 721 608-47399
Fax: +49 721 608-48457
E-Mail: andreas.lochbih...@kit.edu
http://pp.info.uni-karlsruhe.de
KIT - Universität des Landes Baden-Württemberg und nationales Forschungszentrum 
in der Helmholtz-Gemeinschaft

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

Re: [isabelle-dev] Open Issues with JinjaThreads entry

2011-10-04 Thread Andreas Lochbihler


the traditional isatest's AFP-Test did not report any failures the last few 
days,
but the emerging testboard infrastructure mentions failures over the last few 
versions, and the current tips

76aec35b4898934df700ee54ce4d8fb7b99b0388:AFP,fa3715b35370fd27bc9e6bd03fad4a34b0724af3:Isabelle

still seem to be broken.

For people involved in this issue, here is a more detailed report:

http://isabelle.in.tum.de/reports/Isabelle/report/37c2d104871b443f8b6dbd0a8b8b0314


The report just ends with Interrupt. Is it possible that this is a time-out 
or similar?
I would not call it broken - it's just lack of resources. It important line in 
the log is


Run out of store - interrupting threads

The tail of the output log tells me that the interrupt occured when one of the 
huge locales get opened. On my local machine, JinjaThreads requires to build in 
single-threaded mode about 12G of memory plus a few more when the heap image is 
written.


Andreas

--
Karlsruher Institut für Technologie
IPD Snelting

Andreas Lochbihler
wissenschaftlicher Mitarbeiter
Adenauerring 20a, Geb. 50.41, Raum 031
76131 Karlsruhe

Telefon: +49 721 608-47399
Fax: +49 721 608-48457
E-Mail: andreas.lochbih...@kit.edu
http://pp.info.uni-karlsruhe.de
KIT - Universität des Landes Baden-Württemberg und nationales Forschungszentrum 
in der Helmholtz-Gemeinschaft

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

Re: [isabelle-dev] Fwd: [isabelle] Exception in conv.ML

2011-05-30 Thread Andreas Lochbihler

This fix solves the problem with the exception. I tried it with 574613b47583. 
Can you add it to the repository as I do not have wirte access to that.


Thanks,
Andreas

Lawrence Paulson schrieb:

Thank you for looking there! This is the most plausible culprit. But it is 
strange that this problem has arisen before.

A possible fix is to replace the last line of the function timing_depth_tac in 
that file as follows:

  handle PROVE = Seq.empty | THM _ = Seq.empty;

Andreas, do you want to try this and see if it helps?

Larry

On 27 May 2011, at 15:27, Stefan Berghofer wrote:


Hi Larry and Andreas,

there is another occurrence of gconv_rule in Provers/blast.ML
(in function timing_depth_tac). Since the exception is thrown
when invoking blast, this occurrence of gconv_rule may be the
culprit.




--
Karlsruher Institut für Technologie
IPD Snelting

Andreas Lochbihler
wissenschaftlicher Mitarbeiter
Adenauerring 20a, Geb. 50.41, Raum 023
76131 Karlsruhe

Telefon: +49 721 608-48352
Fax: +49 721 608-48457
E-Mail: andreas.lochbih...@kit.edu
http://pp.info.uni-karlsruhe.de
KIT - Universität des Landes Baden-Württemberg und nationales Forschungszentrum 
in der Helmholtz-Gemeinschaft

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

Re: [isabelle-dev] Fwd: [isabelle] Exception in conv.ML

2011-05-27 Thread Andreas Lochbihler

I'll be happy to provide a trace if you tell me how to obtain one. If I turn on 
Debugging in the settings menu, I only get an empty exception trace in the 
isabelle buffer:


Exception trace for exception - THM raised in conv.ML line 212

End of trace

Andreas

Lawrence Paulson schrieb:

It looks like this exception is raised when gconv_rule cv i th is called and 
the specified subgoal does not exist. The function gconv_rule is called in only 
four places in Pure:

./Isar/element.ML:  (Conv.gconv_rule Drule.beta_eta_conversion 1 r)
./raw_simplifier.ML:  then Conv.gconv_rule (rewrite_cterm mode prover ss) i thm
./raw_simplifier.ML:Seq.single (Conv.gconv_rule (rewrite_cterm mode (SINGLE 
o prover_tac) ss) i thm)
./tactical.ML:fun CONVERSION cv i st = Seq.single (Conv.gconv_rule cv i st)

Without a full trace, it is impossible to be certain which one. I looked in 
raw_simplifier.ML, and the two calls did the necessary check to prevent this 
exception from being raised. The function CONVERSION in tactical.ML does no 
check, but catches exception THM. This leaves the function compose_witness in 
Isar/element.ML, where I see neither a check that the subgoal exists nor an 
exception handler. But I could be wrong, as such checks may be done elsewhere. 
Does anybody else have a suggestion?

Larry

Begin forwarded message:


From: Andreas Lochbihler andreas.lochbih...@kit.edu
Date: 27 May 2011 14:51:27 GMT+01:00
To: isabelle-users isabelle-us...@cl.cam.ac.uk
Subject: [isabelle] Exception in conv.ML

Hi all,

have the following weird behaviour. After having applied auto on my goal, I am 
left with 24 subgoals. Applying 24 copies of the following invokation of the 
blast method solves all 24 subgoals. However, if I try to collaspe all of them 
into a single invokation apply(blast 25 ...)+, I get the exception below.

What is going wrong here? And how can I fix it?

If need be, I can make my theories available, but I doubt that I can produce a 
minimal core example.

apply(blast 25 intro: rtranclp_trans rtranclp_tranclp_tranclp
 treds1r_cons_treds1r List1Red2 treds1t_cons_treds1t
  dest: t)

*** exception THM 1 raised (line 212 of conv.ML):
*** gconv_rule
*** EX es'' xs''.
***P,e # es,n,h' |- (es'', xs'') [--] (stk', loc', pc', xcp') 
***(if tmoves2 (compP2 P) h stk (e # es) pc xcp
*** then h' = h 
***  (if xcp' = Any -- pc  pc' then treds1r else treds1t) P t h
***   (e' # es, xs) (es'', xs'')
*** else EX ta' es' xs'.
*** treds1r P t h (e' # es, xs) (es', xs') 
*** P,t |- es',(h, xs') [-ta'-] es'',(h', xs'') 
*** ta_bisim wbisim1 (extTA2J1 P ta') ta 
*** ¬ tmoves1 P h es' 
*** (calls1 (e' # es) = None 
***  no_calls2 (e # es) pc  es' = e' # es  xs' = xs))
*** At command apply

Best regards,
Andreas

--
Karlsruher Institut für Technologie
IPD Snelting

Andreas Lochbihler
wissenschaftlicher Mitarbeiter
Adenauerring 20a, Geb. 50.41, Raum 023
76131 Karlsruhe

Telefon: +49 721 608-48352
Fax: +49 721 608-48457
E-Mail: andreas.lochbih...@kit.edu
http://pp.info.uni-karlsruhe.de
KIT - Universität des Landes Baden-Württemberg und nationales Forschungszentrum 
in der Helmholtz-Gemeinschaft





--
Karlsruher Institut für Technologie
IPD Snelting

Andreas Lochbihler
wissenschaftlicher Mitarbeiter
Adenauerring 20a, Geb. 50.41, Raum 023
76131 Karlsruhe

Telefon: +49 721 608-48352
Fax: +49 721 608-48457
E-Mail: andreas.lochbih...@kit.edu
http://pp.info.uni-karlsruhe.de
KIT - Universität des Landes Baden-Württemberg und nationales Forschungszentrum 
in der Helmholtz-Gemeinschaft

___
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

2011-01-13 Thread Andreas Lochbihler

 Are there still users of PG 3.x with recent Isabelle snapshots or versions 
 from the repository?
I am using PG 3.7.1.1 with XEmacs 21.4.21 and a recent version from the 
Isabelle repository. My motivation for not switching is that PG 4.x did not 
seem to work with XEmacs when I tried, and I have not yet figured out how to 
set up auto-completion that XEmacs provides with any other Emacs. Does anyone 
know how to do this?

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

[isabelle-dev] Error message Failed to prepare dependency graph

2009-11-17 Thread Andreas Lochbihler

Hi all,

I tried to build (my own version of) JinjaThreads with the Isabelle 
repository version 8cce3a34c122, but it failed with the error message 
Failed to prepare dependency graph. The log of the run ends with:

Loading theory JinjaThreads
### Rule already declared as safe introduction (intro!)
### [| ~ contains_insync ?b; ~ contains_insync ?e |]
### == bisim ?Vs (while (?b) ?e) (while (compE1 ?Vs ?b) compE1 ?Vs ?e) ?xs
val it = () : unit
val it = () : unit
val it = () : unit
val it = () : unit
val it = () : unit
val it = () : unit
*** Failed to prepare dependency graph

Does anyone know what might have gone wrong here and how to generate a 
heap and the dependence graph?

Regards,
Andreas

1 2 >

100 matches

Mail list logo