<html><head><meta http-equiv="Content-Type" content="text/html charset=iso-8859-1"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space; ">The main avenue for support is the users' mailing list, which is <a href="mailto:isabelle-users@cl.cam.ac.uk">isabelle-users@cl.cam.ac.uk</a>. You have mailed the developers' list.<div><br></div><div>I do suggest that you frame your question to include more technical detail, because as things stand it's impossible to imagine what you are trying to do.</div><div><br><div>
<span class="Apple-style-span" style="border-collapse: separate; border-spacing: 0px 0px; color: rgb(0, 0, 0); font-family: Helvetica; font-size: 12px; font-style: normal; font-variant: normal; font-weight: normal; letter-spacing: normal; line-height: normal; text-align: auto; -khtml-text-decorations-in-effect: none; text-indent: 0px; -apple-text-size-adjust: auto; text-transform: none; orphans: 2; white-space: normal; widows: 2; word-spacing: 0px; "><div>Larry Paulson</div><br class="Apple-interchange-newline"></span>
</div>
<br><div><div>On 25 Aug 2013, at 20:22, David Blubaugh <<a href="mailto:davidblubaugh2000@yahoo.com">davidblubaugh2000@yahoo.com</a>> wrote:</div><br class="Apple-interchange-newline"><blockquote type="cite"><div><div style="background-color: rgb(255, 255, 255); font-family: 'times new roman', 'new york', times, serif; font-size: 12pt; "><div style="RIGHT: auto"><span style="RIGHT: auto">Hello,</span></div>
<div style="background-color: transparent; font-style: normal; font-family: 'times new roman', 'new york', times, serif; font-size: 16px; right: auto; "><span style="RIGHT: auto"></span> </div>
<div style="RIGHT: auto"><span style="RIGHT: auto"><var id="yui-ie-cursor"></var></span> </div>
<div style="RIGHT: auto"><span style="RIGHT: auto">My name is DAvid Blubaugh.</span></div>
<div style="RIGHT: auto"><span style="RIGHT: auto"></span> </div>
<div style="RIGHT: auto"><span style="RIGHT: auto"></span> </div>
<div style="RIGHT: auto"><span style="RIGHT: auto">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!!</span></div>
<div style="RIGHT: auto"><span style="RIGHT: auto"></span> </div>
<div style="background-color: transparent; font-style: normal; font-family: 'times new roman', 'new york', times, serif; font-size: 16px; right: auto; "><span style="RIGHT: auto">I was wondering if there are any sources of support out there might be interested in such technologies??? </span></div>
<div style="background-color: transparent; font-style: normal; font-family: 'times new roman', 'new york', times, serif; font-size: 16px; right: auto; "><span style="RIGHT: auto"></span> </div>
<div style="background-color: transparent; font-style: normal; font-family: 'times new roman', 'new york', times, serif; font-size: 16px; right: auto; "><span style="RIGHT: auto">thanks,</span></div>
<div style="RIGHT: auto"><span style="RIGHT: auto"></span> </div>
<div style="RIGHT: auto"><span style="RIGHT: auto"></span> </div>
<div style="RIGHT: auto"><span style="RIGHT: auto">David</span></div>
<div style="RIGHT: auto"><span style="RIGHT: auto"></span> </div>
<div style="RIGHT: auto"><span style="RIGHT: auto"></span> </div>
<div style="RIGHT: auto"><span style="RIGHT: auto"></span> </div>
<div><br></div>
<div style="FONT-FAMILY: times new roman, new york, times, serif; FONT-SIZE: 12pt">
<div style="FONT-FAMILY: times new roman, new york, times, serif; FONT-SIZE: 12pt">
<div dir="ltr">
<div style="BORDER-BOTTOM: #ccc 1px solid; BORDER-LEFT: #ccc 1px solid; PADDING-BOTTOM: 0px; LINE-HEIGHT: 0; MARGIN: 5px 0px; PADDING-LEFT: 0px; PADDING-RIGHT: 0px; HEIGHT: 0px; FONT-SIZE: 0px; BORDER-TOP: #ccc 1px solid; BORDER-RIGHT: #ccc 1px solid; PADDING-TOP: 0px" class="hr" contenteditable="false" readonly="true"></div><font size="2" face="Arial"><b><span style="FONT-WEIGHT: bold">From:</span></b> "<a href="mailto:isabelle-dev-request@mailbroy.informatik.tu-muenchen.de">isabelle-dev-request@mailbroy.informatik.tu-muenchen.de</a>" <<a href="mailto:isabelle-dev-request@mailbroy.informatik.tu-muenchen.de">isabelle-dev-request@mailbroy.informatik.tu-muenchen.de</a>><br><b><span style="FONT-WEIGHT: bold">To:</span></b> <a href="mailto:isabelle-dev@mailbroy.informatik.tu-muenchen.de">isabelle-dev@mailbroy.informatik.tu-muenchen.de</a> <br><b><span style="FONT-WEIGHT: bold">Sent:</span></b> Sunday, August 25, 2013 6:00 AM<br><b><span style="FONT-WEIGHT: bold">Subject:</span></b> isabelle-dev Digest, Vol 75, Issue 31<br></font></div>
<div class="y_msg_container"><br>Send isabelle-dev mailing list submissions to<br> <a href="mailto:isabelle-dev@mailbroy.informatik.tu-muenchen.de" ymailto="mailto:isabelle-dev@mailbroy.informatik.tu-muenchen.de">isabelle-dev@mailbroy.informatik.tu-muenchen.de</a><br><br>To subscribe or unsubscribe via the World Wide Web, visit<br> <a href="https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev" target="_blank">https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev</a><br><br>or, via email, send a message with subject or body 'help' to<br> <a href="mailto:isabelle-dev-request@mailbroy.informatik.tu-muenchen.de" ymailto="mailto:isabelle-dev-request@mailbroy.informatik.tu-muenchen.de">isabelle-dev-request@mailbroy.informatik.tu-muenchen.de</a><br><br>You can reach the person managing the list at<br> <a href="mailto:isabelle-dev-owner@mailbroy.informatik.tu-muenchen.de" ymailto="mailto:isabelle-dev-owner@mailbroy.informatik.tu-muenchen.de">isabelle-dev-owner@mailbroy.informatik.tu-muenchen.de</a><br><br>When replying, please edit your Subject line so it is more specific<br>than "Re: Contents of isabelle-dev digest..."<br><br><br>Today's Topics:<br><br> 1. Re: functions over abstract data (Alexander Krauss)<br> 2. Re: The coming release (Alexander Krauss)<br><br><br>----------------------------------------------------------------------<br><br>Message: 1<br>Date: Sat, 24 Aug 2013 23:20:19 +0200<br>From: Alexander Krauss <<a href="mailto:krauss@in.tum.de" ymailto="mailto:krauss@in.tum.de">krauss@in.tum.de</a>><br>To: Christian Sternagel <<a href="mailto:c.sternagel@gmail.com" ymailto="mailto:c.sternagel@gmail.com">c.sternagel@gmail.com</a>><br>Cc: isabelle-dev <<a href="mailto:isabelle-dev@mailbroy.informatik.tu-muenchen.de" ymailto="mailto:isabelle-dev@mailbroy.informatik.tu-muenchen.de">isabelle-dev@mailbroy.informatik.tu-muenchen.de</a>><br>Subject: Re: [isabelle-dev] functions over abstract data<br>Message-ID: <<a href="mailto:52192393.9080503@in.tum.de" ymailto="mailto:52192393.9080503@in.tum.de">52192393.9080503@in.tum.de</a>><br>Content-Type: text/plain; charset=ISO-8859-1; format=flowed<br><br>Hi Chris,<br><br>[...]<br><br>> When defining a function "f", whose result type is "T", it might be<br>> necessary to "peek under the hood" in order to show termination. When<br>> doing this manually, we destroy the abstraction and always have to<br>> reason about the raw-level and even worse, also all the existing<br>> constants with result type T have to be deconstructed in the definition.<br><br>I discussed similar ideas with John Matthews around 2007/8, where we <br>also had a recursive specification of a value that could "internally" be
<br>expressed as a recursive function, even though it was not of function <br>type itself. The (single) motivation at the time was the attempt to <br>define infinite streams, modelled basically as "nat => 'a". However, I <br>abandoned the approach as too complicated. For streams, I believe they <br>should be more naturally defined corecursively. The same might hold for <br>your parsers if you find a good way of expressing it: Your "par" <br>definition is well-formed because the recursive call is wrapped into <br>something else... This looks more like a productivity argument then a <br>termination one, even though, when unfolding, one can be seen as the other.<br><br>Do you know the work of Nils Anders Danielsson on parsers, in particular<br><a href="http://www.cse.chalmers.se/~nad/publications/danielsson-parser-combinators.pdf" target="_blank">http://www.cse.chalmers.se/~nad/publications/danielsson-parser-combinators.pdf</a><br>?<br>I'm not sure what
this would mean in HOL, but it is certainly relevant.<br><br><br>[...]<br>> Here comes my suggestion<br>[...]<br><br>What you are proposing would add substantial complexity to pretty much <br>everything in the function package. While it might be possible to do <br>such a thing ("no obvious deficiencies"), you would pay later when <br>maintaining the stuff. This is too much for what seems to me like a <br>"one-man-feature".<br><br><br>> PS: I started to dive into the function package. My first hurdle is that<br>> for "f" not of function type (as in "par"), no recursive calls are<br>> generated, since "Function_Ctx_Tree.mk_tree" says that "No cong rules<br>> could be found".<br><br>The analysis in the function package assumes basically a form where the <br>arguments of recursive calls can be extracted explicitly. This is a hard <br>assumption, and I see no chance of getting rid of it. The only sensible <br>way of lifting this restriction is
to build some sort of wrapper that <br>reduces some other format to a normal function definition.<br><br>Alex<br><br><br><br>------------------------------<br><br>Message: 2<br>Date: Sat, 24 Aug 2013 23:27:33 +0200<br>From: Alexander Krauss <<a href="mailto:krauss@in.tum.de" ymailto="mailto:krauss@in.tum.de">krauss@in.tum.de</a>><br>To: Makarius <<a href="mailto:makarius@sketis.net" ymailto="mailto:makarius@sketis.net">makarius@sketis.net</a>><br>Cc: <a href="mailto:isabelle-dev@in.tum.de" ymailto="mailto:isabelle-dev@in.tum.de">isabelle-dev@in.tum.de</a><br>Subject: Re: [isabelle-dev] The coming release<br>Message-ID: <<a href="mailto:52192545.1030305@in.tum.de" ymailto="mailto:52192545.1030305@in.tum.de">52192545.1030305@in.tum.de</a>><br>Content-Type: text/plain; charset=ISO-8859-1; format=flowed<br><br>On 08/17/2013 04:05 PM, Makarius wrote:<br>> in the past few weeks the coming release has been mentioned in passing<br>>
several times. So far the precise schedule is not clear, but just from<br>> the distance to Isabelle2013 and the amount of material that is about to<br>> be finished for Isabelle2013-1, it has to be rather soon after the summer.<br>><br>> Since Isabelle is a huge and complex system, things that are relevant<br>> for a release need to be known well in advance.<br><br>There is a small extension to the function package pending, which was <br>written by Manuel Eberl. It produces elimination rules of a new format, <br>and also provides a "fun_cases" command for ad-hoc elimination that is <br>analogous to "inductive_cases".<br><br>Since there is some user demand for it and it is already functionally <br>complete, I'd like to integrate this when I am back from vacation in two <br>weeks, even if there are some minor things to be sorted out.<br><br>Alex<br><br><br><br><br>------------------------------<br><br>Subject: Digest
Footer<br><br>_______________________________________________<br>isabelle-dev mailing list<br><a href="mailto:isabelle-dev@mailbroy.informatik.tu-muenchen.de" ymailto="mailto:isabelle-dev@mailbroy.informatik.tu-muenchen.de">isabelle-dev@mailbroy.informatik.tu-muenchen.de</a><br><a href="https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev" target="_blank">https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev</a><br><br><br>------------------------------<br><br>End of isabelle-dev Digest, Vol 75, Issue 31<br>********************************************<br><br><br></div></div></div></div></div>_______________________________________________<br>isabelle-dev mailing list<br><a href="mailto:isabelle-dev@in.tum.de">isabelle-dev@in.tum.de</a><br>https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev<br></blockquote></div><br></div></body></html>