#
a2328149 |
|
23-Sep-2011 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Adopt ML-style syntax for case expressions and use freed up "||" for bitwise-or. See issue #24.
|
#
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.
|
#
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.
|
#
e141cd4b |
|
15-May-2011 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Rework lambda-term recursion principle proof once more. It's simpler and more polished, mostly following the IJCAR'06 paper by Urban and Berghofer, though slightly simpler even than that. I believe I have one more useful change in me for this development, and then I'll attempt to do the whole thing again, generically in genericTerms. The change to term_posnScript comes about because it relied slightly too much on the exact form of the principle. (Previously tm_recursion was just recursion and not iteration; putting iteration in from the outset seems harmless.)
|
#
506ccc93 |
|
26-Apr-2010 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Implement a new (automatic) simplification for terms like {(x,y)|F}. Such terms rewrite to {}, but with the underlying paired abstractions getting in the way, it's impossible to get a normal rewrite to do the right thing. The implemented conversion also tries to handle the situation where the predicate is T, but this isn't sure to rewrite to UNIV because pattern-forms may preclude it. For example, { x + 1 | T } with x a natural, is not the universal set. The simpset fragment has name GSPEC_SIMP if you need to remove it. The distribution builds at selftest level 1. Selftest level 2 will be tested overnight.
|
#
e3d2a94e |
|
01-Mar-2010 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Proof fixes given general incorporation of LIST_EQ_SIMP_ss.
|
#
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).
|