#
fd124f0c |
|
21-Nov-2019 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Provide λ-calculus versions of unfold and fold functions These functions are currently in unary_recfnsTheory but will probably soon move to nlistTheory. Also clean some other things up, including removing an unnecessary dependency between churchDB and churchlist.
|
#
94b064b9 |
|
15-Aug-2016 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Remove unnecessary structure bracketting As per 89fc99bc3, but on as many examples as a grep -R can find.
|
#
bc294d17 |
|
02-Sep-2011 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Extract a usable half-way point from nominal_datatype branch. This replaces the is_perm predicate with a type embodying that predicate. It doesn't include the subsequent work on allowing multiple 'atom' types.
|
#
25da727d |
|
24-Jul-2011 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Terms and labelled terms now derived from generic terms. This is a big change that points to the implementation of a complete nominal datatype package. The use of generic terms means that we only need to do one hairy quotient, and one hairy derivation of a recursion principle. The recursion principle in question features a new "FCB" (one of the side-conditions that need to be proved in order to get a recursive function admitted). Though I think it's better, it can be a little fiddlier to prove. It's also stronger, so in theory, there may be reasonable functions that the new FCB rejects. It should certainly be possible to automate the bulk of the new fiddly proofs.
|
#
ba932e5d |
|
05-Jun-2011 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Rework lambda-theory scripts to use new varying parameter recursion theorem. Also make work for myself by having some of the script files use 'tight' equality. Later files get switched back to loose (prec = 100) equality, because it was all getting to be too much work.
|
#
621359f7 |
|
13-Jun-2010 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Fix barendregt/chap2Script.sml so that set_MLname is no longer required. Also fix annoying choice of names while I'm at it.
|
#
1271d3b1 |
|
09-Nov-2009 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Move some theorems around; mainly to put cfindleast into churchnumTheory.
|
#
dabbf2b2 |
|
08-Nov-2009 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Checking in to save my work (progress with findleast). Unfortunately recsets doesn't quite build - will fix tomorrow.
|
#
ea177b9c |
|
07-Nov-2009 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Progress with findleast combinator.
|
#
294beb36 |
|
27-Oct-2009 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Forgot to commit simple theorems about Yf in examples/lambda/barendregt.
|
#
32a95312 |
|
19-Apr-2009 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Recast the definition of the Y combinator to be the "traditional" \f. (\x. f (x x)) (\x. f (x x)) rather than the combinator version I had before. Reprove the important characterising theorem. The reason for the switch is to make it easier to reason about normal order reductions involving Y.
|
#
67383085 |
|
09-Apr-2009 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Use new facilities (bounded pre-order rewrites and |>) to simplify a proof about the Y combinator.
|
#
592c6b55 |
|
30-Mar-2009 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Use the new add_relsimp facilities in simpLib to implement the system provided by reductionEval, and to simplify the proofs in chap2Script. While I'm at it, add definitions and characterising theorems about combinators B, C, and Y in chap2Theory.
|
#
695f3a6c |
|
24-Mar-2009 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Show that the numeric pairing functions are computable by providing lambda-terms to do them.
|
#
d2800ab2 |
|
22-Mar-2009 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Changes so that the weakened rewriting of lambda-terms now happens with respect to beta-equality (==), rather than beta-reduction (-b->*). This gives us access to more rewrites. In particular, we get things like church (SUC n) @@ z @@ f == f @@ (church n @@ z @@ f) which is a nice recursive characterisation of what church numerals do, and saves us from having to do too many ghastly things with FUNPOW. With the above equation, neither side reduces to the other (they have a common reduct of course), and so it wasn't a usable rewrite when using -b->*. In addition, to the above, I set up a natrec combinator, which would get typed : 'a -> (num -> 'a -> 'a) -> num -> 'a if we were in a typed world. This combinator gets access to the value of the recursive argument, making predecessor easier to define. Also, give an equation like the one above for church for the cDB function. Many proofs are shorter. Some are slower, but the shortness of expression won me over.
|
#
cb0a0371 |
|
17-Mar-2009 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Add some rewrites about freshness (not being in the free variables of a term) that work better with the simplifier. This breaks a couple of proofs later on in chap2 and chap3 theories, that are easily fixed.
|
#
64d23b61 |
|
15-Mar-2009 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
More useful facts about Omega, including the fact that if you can reach it, you have no beta-normal-form.
|
#
6ee0f460 |
|
14-Mar-2009 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
More facts about normal order reduction paths, including the fact that the self-looping Omega term has an infinite one, and thus, by another theorem just proved, has no beta-normal-form.
|
#
effc431b |
|
01-Oct-2008 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Change export_rewrites back to its old API (without requiring an extra string). When exported, the resulting simpset fragment always picked up the name of the theory to be the base of its name, so there didn't seem much point in giving users a false impression of naming power.
|
#
32cb282d |
|
20-Jul-2008 |
Konrad Slind <konrad.slind@gmail.com> |
More laggards.
|
#
aed05f4e |
|
20-Jul-2008 |
Konrad Slind <konrad.slind@gmail.com> |
A whole mess of small changes intended at making simpsets prettyprint informatively in the interactive loop. Very possibly I haven't updated all the files in the examples directories.
|
#
7cf5c42f |
|
09-Jul-2008 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Completely reorganise these files into some sensible directories. Also, add a file demonstrating that the McKinna-Pollack two-sorted raw syntax does indeed behave properly (links appropriately to beta over quotiented terms).
|