#
f5b0bca9 |
|
12-Sep-2011 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
WIP: perm_type wasn't building; now it's closer to building. I probably mangled my attempt to extract the 'good stuff' from the old nominal_datatype branch. I have cleaned things up slightly by hiding the 'raw' lswapstr constant. Now the string "lswapstr" maps to a term that is a permutation action, making all the permutation rewrites apply for lswapstr automatically.
|
#
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.
|
#
d92ebd42 |
|
24-Jul-2011 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Revised Barendregt Chapter 11.1 theory
|
#
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.
|
#
cfaa2343 |
|
12-Mar-2009 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Fully support weaker relations than equality that aren't also constants. Start to implement a reduction engine for beta-reduction in the lambda-calculus. Still some wrinkles to work out.
|
#
2b2a6705 |
|
27-Feb-2009 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Fiddle and prettify basic presentation of beta-reduction. Using syntactic patterns, I can now have ``compat_closure beta M N`` (the "compatible closure of the beta-relation) appear as ``M -b-> N``. Also use syntactic patterns to get rid of constants reduction and conversion. Finally, provide Unicode versions of the various arrow symbols so that with the Unicode flag on, the above will come out as M -β-> N Even in just ASCII, I think the theorems look a deal prettier.
|
#
176a481a |
|
26-Nov-2008 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Fixes for these examples, and an updated MANIFEST/README in other-models. The other-models directory had become particularly stale. I obviously need to check that it works more often. (Main problem: change to behaviour of Q.INST.)
|
#
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.
|
#
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).
|