[isabelle-dev] support for ideas using isabelle hol

David Blubaugh davidblubaugh2000 at yahoo.com
Sun Aug 25 21:22:49 CEST 2013

My name is DAvid Blubaugh.
I want to state that I am in the process of using advanced machine learning techniques to use Isabelle HOL to inspect and develop quality assurance for software applications 1!!
I was wondering if there are any sources of support out there might be interested in such technologies???  

From: "isabelle-dev-request at mailbroy.informatik.tu-muenchen.de" <isabelle-dev-request at mailbroy.informatik.tu-muenchen.de>
To: isabelle-dev at mailbroy.informatik.tu-muenchen.de 
Sent: Sunday, August 25, 2013 6:00 AM
Subject: isabelle-dev Digest, Vol 75, Issue 31

Send isabelle-dev mailing list submissions to
    isabelle-dev at mailbroy.informatik.tu-muenchen.de

To subscribe or unsubscribe via the World Wide Web, visit

or, via email, send a message with subject or body 'help' to
    isabelle-dev-request at mailbroy.informatik.tu-muenchen.de

You can reach the person managing the list at
    isabelle-dev-owner at mailbroy.informatik.tu-muenchen.de

When replying, please edit your Subject line so it is more specific
than "Re: Contents of isabelle-dev digest..."

Today's Topics:

  1. Re: functions over abstract data (Alexander Krauss)
  2. Re: The coming release (Alexander Krauss)


Message: 1
Date: Sat, 24 Aug 2013 23:20:19 +0200
From: Alexander Krauss <krauss at in.tum.de>
To: Christian Sternagel <c.sternagel at gmail.com>
Cc: isabelle-dev <isabelle-dev at mailbroy.informatik.tu-muenchen.de>
Subject: Re: [isabelle-dev] functions over abstract data
Message-ID: <52192393.9080503 at in.tum.de>
Content-Type: text/plain; charset=ISO-8859-1; format=flowed

Hi Chris,


> When defining a function "f", whose result type is "T", it might be
> necessary to "peek under the hood" in order to show termination. When
> doing this manually, we destroy the abstraction and always have to
> reason about the raw-level and even worse, also all the existing
> constants with result type T have to be deconstructed in the definition.

I discussed similar ideas with John Matthews around 2007/8, where we 
also had a recursive specification of a value that could "internally" be 
expressed as a recursive function, even though it was not of function 
type itself. The (single) motivation at the time was the attempt to 
define infinite streams, modelled basically as "nat => 'a". However, I 
abandoned the approach as too complicated. For streams, I believe they 
should be more naturally defined corecursively. The same might hold for 
your parsers if you find a good way of expressing it: Your "par" 
definition is well-formed because the recursive call is wrapped into 
something else... This looks more like a productivity argument then a 
termination one, even though, when unfolding, one can be seen as the other.

Do you know the work of Nils Anders Danielsson on parsers, in particular
I'm not sure what this would mean in HOL, but it is certainly relevant.

> Here comes my suggestion

What you are proposing would add substantial complexity to pretty much 
everything in the function package. While it might be possible to do 
such a thing ("no obvious deficiencies"), you would pay later when 
maintaining the stuff. This is too much for what seems to me like a 

> PS: I started to dive into the function package. My first hurdle is that
> for "f" not of function type (as in "par"), no recursive calls are
> generated, since "Function_Ctx_Tree.mk_tree" says that "No cong rules
> could be found".

The analysis in the function package assumes basically a form where the 
arguments of recursive calls can be extracted explicitly. This is a hard 
assumption, and I see no chance of getting rid of it. The only sensible 
way of lifting this restriction is to build some sort of wrapper that 
reduces some other format to a normal function definition.



Message: 2
Date: Sat, 24 Aug 2013 23:27:33 +0200
From: Alexander Krauss <krauss at in.tum.de>
To: Makarius <makarius at sketis.net>
Cc: isabelle-dev at in.tum.de
Subject: Re: [isabelle-dev] The coming release
Message-ID: <52192545.1030305 at in.tum.de>
Content-Type: text/plain; charset=ISO-8859-1; format=flowed

On 08/17/2013 04:05 PM, Makarius wrote:
> in the past few weeks the coming release has been mentioned in passing
> several times.  So far the precise schedule is not clear, but just from
> the distance to Isabelle2013 and the amount of material that is about to
> be finished for Isabelle2013-1, it has to be rather soon after the summer.
> Since Isabelle is a huge and complex system, things that are relevant
> for a release need to be known well in advance.

There is a small extension to the function package pending, which was 
written by Manuel Eberl. It produces elimination rules of a new format, 
and also provides a "fun_cases" command for ad-hoc elimination that is 
analogous to "inductive_cases".

Since there is some user demand for it and it is already functionally 
complete, I'd like to integrate this when I am back from vacation in two 
weeks, even if there are some minor things to be sorted out.



Subject: Digest Footer

isabelle-dev mailing list
isabelle-dev at mailbroy.informatik.tu-muenchen.de


End of isabelle-dev Digest, Vol 75, Issue 31
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20130825/56acc58d/attachment.html>

More information about the isabelle-dev mailing list