Mercurial
Mercurial
>
hg
>
nominal2
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
help
less
more
|
(0)
-1000
-480
+480
+1000
tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or
revset expression
.
The revision graph only works with JavaScript-enabled browsers.
Lifting constants.
2010-03-11, by Cezary Kaliszyk
Proper error message.
2010-03-11, by Cezary Kaliszyk
Lifting constants works for all examples.
2010-03-11, by Cezary Kaliszyk
Remove tracing from fv/alpha.
2010-03-11, by Cezary Kaliszyk
Equivp working only on the standard alpha-equivalences.
2010-03-11, by Cezary Kaliszyk
explicit cheat_fv_eqvt
2010-03-11, by Cezary Kaliszyk
extract build_eqvts_tac.
2010-03-11, by Cezary Kaliszyk
build_eqvts no longer requires permutations.
2010-03-11, by Cezary Kaliszyk
Add explicit alpha_eqvt_cheat.
2010-03-11, by Cezary Kaliszyk
Export tactic out of alpha_eqvt.
2010-03-11, by Cezary Kaliszyk
merge
2010-03-10, by Cezary Kaliszyk
More tries about the proofs in trm5
2010-03-10, by Cezary Kaliszyk
merged
2010-03-10, by Christian Urban
almost done with showing the equivalence between old and new alpha-equivalence (one subgoal remaining)
2010-03-10, by Christian Urban
alpha_equivp for trm5
2010-03-10, by Cezary Kaliszyk
Undoing mistakenly committed parser experiments.
2010-03-10, by Cezary Kaliszyk
alpha_eqvt for recursive term1.
2010-03-10, by Cezary Kaliszyk
Looking at alpha_eqvt for term5, not much progress.
2010-03-10, by Cezary Kaliszyk
Reordered examples in Test.
2010-03-10, by Cezary Kaliszyk
Allows multiple bindings with same lhs.
2010-03-10, by Cezary Kaliszyk
Linked parser to fv and alpha.
2010-03-10, by Cezary Kaliszyk
merge
2010-03-10, by Cezary Kaliszyk
A minor fix for shallow binders. LF works again.
2010-03-10, by Cezary Kaliszyk
merged
2010-03-10, by Christian Urban
parser produces ordered bn-fun information
2010-03-10, by Christian Urban
Testing equalities in trm5, all seems good.
2010-03-10, by Cezary Kaliszyk
Fv&Alpha seem to work.
2010-03-10, by Cezary Kaliszyk
include alpha in the definitions.
2010-03-10, by Cezary Kaliszyk
Filled the algorithm for alpha_bn_arg
2010-03-10, by Cezary Kaliszyk
rhs of alpha_bn, and template for the arguments.
2010-03-10, by Cezary Kaliszyk
alpha_bn_constr template
2010-03-10, by Cezary Kaliszyk
exported template for alpha_bn
2010-03-10, by Cezary Kaliszyk
merge
2010-03-10, by Cezary Kaliszyk
Use alpha_bns in normal alpha defs.
2010-03-10, by Cezary Kaliszyk
alpha_bn_frees
2010-03-10, by Cezary Kaliszyk
merged
2010-03-09, by Christian Urban
added bn-information, but it is not yet ordered according to the dts
2010-03-09, by Christian Urban
Separate lists for separate constructors, to match bn_eqs.
2010-03-09, by Cezary Kaliszyk
All examples should work.
2010-03-09, by Cezary Kaliszyk
Fix to get old alpha.
2010-03-09, by Cezary Kaliszyk
Separate primrecs in Fv.
2010-03-09, by Cezary Kaliszyk
A version of Fv that takes into account recursive and non-recursive bindings.
2010-03-09, by Cezary Kaliszyk
Trying to prove that old alpha is the same as new recursive one. Lets still to do.
2010-03-09, by Cezary Kaliszyk
fv_bi and alpha_bi
2010-03-09, by Cezary Kaliszyk
merged
2010-03-09, by Christian Urban
added first test about new compat
2010-03-09, by Christian Urban
fv_compat
2010-03-09, by Cezary Kaliszyk
added another compat example
2010-03-09, by Christian Urban
added a test-file for compatibility
2010-03-08, by Christian Urban
added compat definitions to some examples
2010-03-08, by Christian Urban
Proper recognition of atoms and atom sets.
2010-03-08, by Cezary Kaliszyk
deleted comments about "weird"
2010-03-08, by Christian Urban
merged
2010-03-08, by Christian Urban
updated to new Isabelle
2010-03-08, by Christian Urban
Term5 written as nominal_datatype is the recursive let.
2010-03-08, by Cezary Kaliszyk
With restricted_nominal=1, exp7 and exp8 work. Not sure about proving bn_rsp there.
2010-03-08, by Cezary Kaliszyk
More fine-grained nominal restriction for debugging.
2010-03-08, by Cezary Kaliszyk
Fix permutation addition.
2010-03-08, by Cezary Kaliszyk
Update the comments
2010-03-08, by Cezary Kaliszyk
Gather bindings with same binder, and generate only one permutation for them.
2010-03-08, by Cezary Kaliszyk
Undo effects of simp.
2010-03-08, by Cezary Kaliszyk
merged
2010-03-07, by Christian Urban
updated to renamings in Isabelle
2010-03-07, by Christian Urban
merged
2010-03-04, by Christian Urban
merged
2010-03-04, by Christian Urban
more proofs in Abs and work on Core Haskell
2010-03-04, by Christian Urban
added a lemma that permutations can be represented as sums of swapping
2010-03-03, by Christian Urban
Still unable to show supp=fv for let with one existential.
2010-03-05, by Cezary Kaliszyk
Ported LF to the parser interface.
2010-03-05, by Cezary Kaliszyk
merge
2010-03-05, by Cezary Kaliszyk
Lift fv and bn eqvts; no need to lift alpha_eqvt.
2010-03-05, by Cezary Kaliszyk
Not much progress about the single existential let case.
2010-03-05, by Cezary Kaliszyk
Fixed LF for one quantifier over 2 premises.
2010-03-05, by Cezary Kaliszyk
Trying to fix the proofs for the single existential... So far failed.
2010-03-05, by Cezary Kaliszyk
Lift distinct.
2010-03-04, by Cezary Kaliszyk
Added lifting of pseudo-injectivity, commented out the code again and enabled the weird examples.
2010-03-04, by Cezary Kaliszyk
Lift BV,FV,Permutations and injection :).
2010-03-04, by Cezary Kaliszyk
Comment out Weird and Phd until we have an idea how to handle multiple permutations. Transp that works for multiple existentials.
2010-03-04, by Cezary Kaliszyk
A version that just leaves the supp/\supp goal. Obviously not true.
2010-03-04, by Cezary Kaliszyk
Prove symp and transp of weird without the supp /\ supp = {} assumption.
2010-03-04, by Cezary Kaliszyk
merge
2010-03-03, by Cezary Kaliszyk
Experiments with proving weird transp
2010-03-03, by Cezary Kaliszyk
Code for solving symp goals with multiple existentials.
2010-03-03, by Cezary Kaliszyk
reflp for multiple quantifiers.
2010-03-03, by Cezary Kaliszyk
fixed mess in Test.thy
2010-03-03, by Christian Urban
Fix eqvt for multiple quantifiers.
2010-03-03, by Cezary Kaliszyk
only tuned
2010-03-03, by Christian Urban
merged
2010-03-03, by Christian Urban
start of paper - does not compile yet
2010-03-03, by Christian Urban
added ACM style file for ICFP
2010-03-03, by Christian Urban
weird eqvt
2010-03-03, by Cezary Kaliszyk
Add the supp intersection conditions.
2010-03-03, by Cezary Kaliszyk
Comment out the part that does not work with 2 quantifiers.
2010-03-02, by Cezary Kaliszyk
Fixes for the fv problem and alpha problem.
2010-03-02, by Cezary Kaliszyk
merged
2010-03-02, by Christian Urban
preliinary test about alpha-weirdo
2010-03-02, by Christian Urban
Another problem with permutations in alpha and possibly also in fv
2010-03-02, by Christian Urban
potential problem with the phd-example, where two permutations are generated, but only one is used
2010-03-02, by Christian Urban
Some tests around Term4. Not sure how to fix the generated fv function.
2010-03-02, by Cezary Kaliszyk
merge
2010-03-02, by Cezary Kaliszyk
Porting from Lift to Parser; until defining the Quotient type.
2010-03-02, by Cezary Kaliszyk
Add image_eqvt and atom_eqvt to eqvt bases.
2010-03-02, by Cezary Kaliszyk
Include the raw eqvt lemmas.
2010-03-02, by Cezary Kaliszyk
merged
2010-03-02, by Christian Urban
added some more examples from Peter Sewell's bestiary
2010-03-02, by Christian Urban
merge
2010-03-02, by Cezary Kaliszyk
Minor
2010-03-02, by Cezary Kaliszyk
Working bv_eqvt
2010-03-02, by Cezary Kaliszyk
Moving wrappers out of Lift.
2010-03-02, by Cezary Kaliszyk
merged
2010-03-02, by Christian Urban
added distinctness of perms
2010-03-02, by Christian Urban
updated (added lemma about commuting permutations)
2010-03-02, by Christian Urban
Change type schemes to name set.
2010-03-02, by Cezary Kaliszyk
More fixes for new alpha, the whole lift script should now work again.
2010-03-02, by Cezary Kaliszyk
Length fix for nested recursions.
2010-03-02, by Cezary Kaliszyk
Fix equivp.
2010-03-02, by Cezary Kaliszyk
Fixed eqvt code.
2010-03-02, by Cezary Kaliszyk
most tests work - the ones that do not I commented out
2010-03-02, by Christian Urban
merge
2010-03-02, by Cezary Kaliszyk
Add a check of fv_functions.
2010-03-02, by Cezary Kaliszyk
some tuning
2010-03-02, by Christian Urban
Link calls to Raw permutations, FV definition and alpha_definition into the parser.
2010-03-02, by Cezary Kaliszyk
merged
2010-03-02, by Christian Urban
rawified the bind specs (ready to be used now)
2010-03-02, by Christian Urban
merge
2010-03-01, by Cezary Kaliszyk
Trying to prove equivariance.
2010-03-01, by Cezary Kaliszyk
modified for new binding format - hope it is the intended one
2010-03-01, by Christian Urban
further code-refactoring in the parser
2010-03-01, by Christian Urban
The new alpha-equivalence and testing in Trm2 and Trm5.
2010-03-01, by Cezary Kaliszyk
slight simplification of the raw-decl generation
2010-03-01, by Christian Urban
Example that shows that current alpha is wrong.
2010-03-01, by Cezary Kaliszyk
added example from my phd
2010-03-01, by Christian Urban
streamlined parser
2010-02-27, by Christian Urban
generated the "binding list" from the input; at the moment it is only printed out as tracing; does not yet include the "bind itself binders"
2010-02-26, by Christian Urban
More about the general lifting procedure.
2010-02-26, by Cezary Kaliszyk
Update TODO
2010-02-26, by Cezary Kaliszyk
Progress with general lifting procedure.
2010-02-26, by Cezary Kaliszyk
RSP of perms can be shown in one go.
2010-02-26, by Cezary Kaliszyk
Change in signature of prove_const_rsp for general lifting.
2010-02-26, by Cezary Kaliszyk
Permutation and FV_Alpha interface change.
2010-02-26, by Cezary Kaliszyk
To call quotient it is enough to export the alpha frees to proper constants and their respective equivp theorems.
2010-02-26, by Cezary Kaliszyk
merge
2010-02-25, by Cezary Kaliszyk
Preparing the generalized lifting procedure
2010-02-25, by Cezary Kaliszyk
merged
2010-02-25, by Christian Urban
added ott-example about Leroy96
2010-02-25, by Christian Urban
Forgot to add one file.
2010-02-25, by Cezary Kaliszyk
Split Terms into separate files and add them to tests.
2010-02-25, by Cezary Kaliszyk
merge
2010-02-25, by Cezary Kaliszyk
Move the eqvt code out of Terms and fixed induction for single-rule examples.
2010-02-25, by Cezary Kaliszyk
merged
2010-02-25, by Christian Urban
a few simplifications
2010-02-25, by Christian Urban
first attempt to make sense out of the core-haskell definition
2010-02-25, by Christian Urban
Code for proving eqvt, still in Terms.
2010-02-25, by Cezary Kaliszyk
Use eqvt infrastructure.
2010-02-25, by Cezary Kaliszyk
Simple function eqvt code.
2010-02-25, by Cezary Kaliszyk
added IsaMakefile...but so far included only a test for the parser
2010-02-25, by Christian Urban
moved Quot package to Attic (still compiles there with "isabelle make")
2010-02-25, by Christian Urban
merged
2010-02-25, by Christian Urban
moved Nominal to "toplevel"
2010-02-25, by Christian Urban
Export perm_frees.
2010-02-25, by Cezary Kaliszyk
Restructuring the code in Perm
2010-02-24, by Cezary Kaliszyk
Simplified and finised eqvt proofs for t1 and t5
2010-02-24, by Cezary Kaliszyk
merge
2010-02-24, by Cezary Kaliszyk
Define lifted perms.
2010-02-24, by Cezary Kaliszyk
merged
2010-02-24, by Christian Urban
parsing and definition of raw datatype and bv-function work (not very beautiful)
2010-02-24, by Christian Urban
With permute_rsp we can lift the instance proofs :).
2010-02-24, by Cezary Kaliszyk
Note the instance proofs, since they can be easily lifted.
2010-02-24, by Cezary Kaliszyk
More refactoring and removed references to the global simpset in Perm.
2010-02-24, by Cezary Kaliszyk
Factor-out 'prove_perm_empty'; I plan to use it in defining permutations on the lifted type.
2010-02-24, by Cezary Kaliszyk
Regularize finite support proof for trm1
2010-02-24, by Cezary Kaliszyk
Made the fv-supp proof much more straightforward.
2010-02-24, by Cezary Kaliszyk
Regularize the proofs about finite support.
2010-02-24, by Cezary Kaliszyk
Respects of permute and constructors.
2010-02-24, by Cezary Kaliszyk
Generate fv_rsp automatically.
2010-02-24, by Cezary Kaliszyk
Define the constants automatically.
2010-02-24, by Cezary Kaliszyk
Rename also the lifted types to non-capital.
2010-02-24, by Cezary Kaliszyk
Use the infrastructure in LF. Much shorter :).
2010-02-24, by Cezary Kaliszyk
Final synchronization of names.
2010-02-24, by Cezary Kaliszyk
LF renaming part 3 (proper names of alpha equvalences)
2010-02-24, by Cezary Kaliszyk
LF renaming part 2 (proper fv functions)
2010-02-24, by Cezary Kaliszyk
merge
2010-02-24, by Cezary Kaliszyk
LF renaming part1.
2010-02-24, by Cezary Kaliszyk
merged
2010-02-24, by Christian Urban
parsing of function definitions almost works now; still an error with undefined constants
2010-02-24, by Christian Urban
merge
2010-02-23, by Cezary Kaliszyk
rsp for bv; the only issue is that it requires an appropriate induction principle.
2010-02-23, by Cezary Kaliszyk
merged
2010-02-23, by Christian Urban
declarartion of the raw datatype already works; raw binding functions throw an exception about mutual recursive types
2010-02-23, by Christian Urban
rsp infrastructure.
2010-02-23, by Cezary Kaliszyk
merge
2010-02-23, by Cezary Kaliszyk
Progress towards automatic rsp of constants and fv.
2010-02-23, by Cezary Kaliszyk
merged
2010-02-23, by Christian Urban
"raw"-ified the term-constructors and types given in the specification
2010-02-23, by Christian Urban
Looking at proving the rsp rules automatically.
2010-02-23, by Cezary Kaliszyk
Minor beutification.
2010-02-23, by Cezary Kaliszyk
Define the quotient from ML
2010-02-23, by Cezary Kaliszyk
All works in LF but will require renaming.
2010-02-23, by Cezary Kaliszyk
Reordering in LF.
2010-02-23, by Cezary Kaliszyk
Fixes for auxiliary datatypes.
2010-02-23, by Cezary Kaliszyk
Fixed pseudo_injectivity for trm4
2010-02-22, by Cezary Kaliszyk
Testing auto equivp code.
2010-02-22, by Cezary Kaliszyk
A tactic for final equivp
2010-02-22, by Cezary Kaliszyk
More equivp infrastructure.
2010-02-22, by Cezary Kaliszyk
tactify transp
2010-02-22, by Cezary Kaliszyk
export the reflp and symp tacs.
2010-02-22, by Cezary Kaliszyk
Generalize atom_trans and atom_sym.
2010-02-22, by Cezary Kaliszyk
Some progress about transp
2010-02-22, by Cezary Kaliszyk
alpha-symmetric addons.
2010-02-22, by Cezary Kaliszyk
alpha reflexivity
2010-02-22, by Cezary Kaliszyk
Renaming.
2010-02-22, by Cezary Kaliszyk
Added missing description.
2010-02-22, by Cezary Kaliszyk
Added Brian's suggestion.
2010-02-22, by Cezary Kaliszyk
Update TODO
2010-02-22, by Cezary Kaliszyk
Removed bindings 'in itself' where possible.
2010-02-21, by Cezary Kaliszyk
Some adaptation
2010-02-20, by Cezary Kaliszyk
proof cleaning and standardizing.
2010-02-19, by Cezary Kaliszyk
Automatic production and proving of pseudo-injectivity.
2010-02-19, by Cezary Kaliszyk
Experiments for the pseudo-injectivity tactic.
2010-02-19, by Cezary Kaliszyk
merge
2010-02-19, by Cezary Kaliszyk
Constructing alpha_inj goal.
2010-02-19, by Cezary Kaliszyk
merged
2010-02-18, by Christian Urban
start work with the parser
2010-02-18, by Christian Urban
Full alpha equivalence + testing in terms. Some differ but it seems the generated version is more correct.
2010-02-18, by Cezary Kaliszyk
First (non-working) version of alpha-equivalence
2010-02-18, by Cezary Kaliszyk
Description of the fv procedure.
2010-02-18, by Cezary Kaliszyk
Testing auto constant lifting.
2010-02-18, by Cezary Kaliszyk
Fix for new Isabelle (primrec)
2010-02-18, by Cezary Kaliszyk
Automatic lifting of constants.
2010-02-18, by Cezary Kaliszyk
Changed back to original version of trm5
2010-02-18, by Cezary Kaliszyk
The alternate version of trm5 with additional binding. All proofs work the same.
2010-02-18, by Cezary Kaliszyk
Code for handling atom sets.
2010-02-18, by Cezary Kaliszyk
Replace Terms by Terms2.
2010-02-18, by Cezary Kaliszyk
Fixed proofs in Terms2 and found a mistake in Terms.
2010-02-18, by Cezary Kaliszyk
Terms2 with bindings for binders synchronized with bindings they are used in.
2010-02-17, by Cezary Kaliszyk
Cleaning of proofs in Terms.
2010-02-17, by Cezary Kaliszyk
Testing Fv
2010-02-17, by Cezary Kaliszyk
Fix the strong induction principle.
2010-02-17, by Cezary Kaliszyk
Reorder
2010-02-17, by Cezary Kaliszyk
Add bindings of recursive types by free_variables.
2010-02-17, by Cezary Kaliszyk
Bindings adapted to multiple defined datatypes.
2010-02-17, by Cezary Kaliszyk
Reorganization
2010-02-17, by Cezary Kaliszyk
Now should work.
2010-02-17, by Cezary Kaliszyk
Some optimizations and fixes.
2010-02-17, by Cezary Kaliszyk
Simplified format of bindings.
2010-02-17, by Cezary Kaliszyk
Tested the Perm code; works everywhere in Terms.
2010-02-17, by Cezary Kaliszyk
Wrapped the permutation code.
2010-02-17, by Cezary Kaliszyk
Description of intended bindings.
2010-02-17, by Cezary Kaliszyk
Code for generating the fv function, no bindings yet.
2010-02-17, by Cezary Kaliszyk
merge
2010-02-17, by Cezary Kaliszyk
indent
2010-02-17, by Cezary Kaliszyk
merge
2010-02-17, by Cezary Kaliszyk
Simplifying perm_eq
2010-02-17, by Cezary Kaliszyk
merge
2010-02-16, by Cezary Kaliszyk
indenting
2010-02-16, by Cezary Kaliszyk
Minor
2010-02-16, by Cezary Kaliszyk
Merge
2010-02-16, by Cezary Kaliszyk
Ported Stefan's permutation code, still needs some localizing.
2010-02-16, by Cezary Kaliszyk
merge
2010-02-15, by Cezary Kaliszyk
Removed varifyT.
2010-02-15, by Cezary Kaliszyk
merged
2010-02-15, by Christian Urban
2-spaces rule (where it makes sense)
2010-02-15, by Christian Urban
merge
2010-02-15, by Cezary Kaliszyk
Fixed the definition of less and finished the missing proof.
2010-02-15, by Cezary Kaliszyk
further tuning
2010-02-15, by Christian Urban
small tuning
2010-02-15, by Christian Urban
tuned the parsing and testing code in quotient_def.ML; cleaned out old stuff in AbsRepTest.thy
2010-02-15, by Christian Urban
der_bname -> derived_bname
2010-02-15, by Cezary Kaliszyk
Names of files.
2010-02-15, by Cezary Kaliszyk
Finished introducing the binding.
2010-02-15, by Cezary Kaliszyk
Synchronize the commands.
2010-02-15, by Cezary Kaliszyk
Passing the binding to quotient_def
2010-02-15, by Cezary Kaliszyk
Added a binding to the parser.
2010-02-15, by Cezary Kaliszyk
Second inline
2010-02-15, by Cezary Kaliszyk
remove one-line wrapper.
2010-02-15, by Cezary Kaliszyk
Undid the read_terms change; now compiles.
2010-02-12, by Cezary Kaliszyk
merge
2010-02-12, by Cezary Kaliszyk
renamed 'as' to 'is' everywhere.
2010-02-12, by Cezary Kaliszyk
"is" defined as the keyword
2010-02-12, by Cezary Kaliszyk
moved "strange" lemma to quotient_tacs; marked a number of lemmas as unused; tuned
2010-02-12, by Christian Urban
The lattice instantiations are gone from Isabelle/Main, so
2010-02-12, by Cezary Kaliszyk
the lam/bla example.
2010-02-11, by Cezary Kaliszyk
Finished a working foo/bar.
2010-02-11, by Cezary Kaliszyk
fv_foo is not regular.
2010-02-11, by Cezary Kaliszyk
Testing foo/bar
2010-02-11, by Cezary Kaliszyk
Even when bv = fv it still doesn't lift.
2010-02-11, by Cezary Kaliszyk
Added the missing syntax file
2010-02-11, by Cezary Kaliszyk
Notation available locally
2010-02-11, by Cezary Kaliszyk
Main renaming + fixes for new Isabelle in IntEx2.
2010-02-11, by Cezary Kaliszyk
Merging QuotBase into QuotMain.
2010-02-11, by Cezary Kaliszyk
removed dead code
2010-02-10, by Christian Urban
cleaned a bit
2010-02-10, by Christian Urban
lowercase locale
2010-02-10, by Cezary Kaliszyk
hg-added the added file.
2010-02-10, by Cezary Kaliszyk
Changes from Makarius's code review + some noticed fixes.
2010-02-10, by Cezary Kaliszyk
example with a respectful bn function defined over the type itself
2010-02-10, by Cezary Kaliszyk
Finishe the renaming.
2010-02-10, by Cezary Kaliszyk
Another mistake found with OTT.
2010-02-10, by Cezary Kaliszyk
merge
2010-02-10, by Cezary Kaliszyk
Fixed rbv6, when translating to OTT.
2010-02-10, by Cezary Kaliszyk
Some cleaning of proofs.
2010-02-10, by Cezary Kaliszyk
merged again
2010-02-10, by Christian Urban
merged
2010-02-10, by Christian Urban
more minor space and bracket modifications.
2010-02-10, by Cezary Kaliszyk
More changes according to the standards.
2010-02-10, by Cezary Kaliszyk
A concrete example, with a proof that rbv is not regular and
2010-02-10, by Cezary Kaliszyk
proper declaration of types and terms during parsing (removes the varifyT when storing data)
2010-02-09, by Christian Urban
merged
2010-02-09, by Christian Urban
slight correction
2010-02-09, by Christian Urban
merge
2010-02-09, by Cezary Kaliszyk
More about trm6
2010-02-09, by Cezary Kaliszyk
merged
2010-02-09, by Christian Urban
the specifications of the respects.
2010-02-09, by Cezary Kaliszyk
trm6 with the 'Foo' constructor.
2010-02-09, by Cezary Kaliszyk
removing unnecessary brackets
2010-02-09, by Cezary Kaliszyk
More indentation cleaning.
2010-02-09, by Cezary Kaliszyk
'exc' -> 'exn' and more name and space cleaning.
2010-02-09, by Cezary Kaliszyk
Fully qualified exception names.
2010-02-09, by Cezary Kaliszyk
merge
2010-02-09, by Cezary Kaliszyk
More indentation, names and todo cleaning in the quotient package
2010-02-09, by Cezary Kaliszyk
merged
2010-02-09, by Christian Urban
a few more attempts to show the equivalence between old and new way of defining alpha-equivalence
2010-02-09, by Christian Urban
minor tuning
2010-02-09, by Christian Urban
Explicitly marked what is bound.
2010-02-09, by Cezary Kaliszyk
Cleaning and updating in Terms.
2010-02-09, by Cezary Kaliszyk
Looking at the trm2 example
2010-02-09, by Cezary Kaliszyk
Fixed pattern matching, now the test in Abs works correctly.
2010-02-09, by Cezary Kaliszyk
added a test case
2010-02-08, by Christian Urban
merged
2010-02-08, by Christian Urban
moved some lemmas to Nominal; updated all files
2010-02-08, by Christian Urban
merge
2010-02-08, by Cezary Kaliszyk
Comments.
2010-02-08, by Cezary Kaliszyk
slightly tuned
2010-02-08, by Christian Urban
Proper context fixes lifting inside instantiations.
2010-02-08, by Cezary Kaliszyk
Fixed the context import/export and simplified LFex.
2010-02-08, by Cezary Kaliszyk
added 2 papers about core haskell
2010-02-08, by Christian Urban
fixed lemma name
2010-02-07, by Christian Urban
updated to latest Nominal2
2010-02-07, by Christian Urban
minor
2010-02-06, by Christian Urban
some tuning
2010-02-06, by Christian Urban
merge
2010-02-05, by Cezary Kaliszyk
merge
2010-02-05, by Cezary Kaliszyk
Fixes for Bex1 removal.
2010-02-05, by Cezary Kaliszyk
Cleaned Terms using [lifted] and found a workaround for the instantiation problem.
2010-02-05, by Cezary Kaliszyk
A procedure that properly instantiates the types too.
2010-02-05, by Cezary Kaliszyk
More code abstracted away
2010-02-05, by Cezary Kaliszyk
A bit more intelligent and cleaner code.
2010-02-05, by Cezary Kaliszyk
merge
2010-02-05, by Cezary Kaliszyk
A proper version of the attribute
2010-02-05, by Cezary Kaliszyk
merged
2010-02-05, by Christian Urban
eqvts and eqvts_raw are separate thm-lists; otherwise permute_eqvt is problematic as it causes looks in eqvts
2010-02-05, by Christian Urban
The automatic lifting translation function, still with dummy types,
2010-02-04, by Cezary Kaliszyk
Quotdata_dest needed for lifting theorem translation.
2010-02-04, by Cezary Kaliszyk
fixed (permute_eqvt in eqvts makes this simpset always looping)
2010-02-04, by Christian Urban
rollback of the test
2010-02-04, by Christian Urban
linked versions - instead of copies
2010-02-04, by Christian Urban
merged
2010-02-04, by Christian Urban
restored the old behaviour of having an eqvts list; the transformed theorems are stored in eqvts_raw
2010-02-04, by Christian Urban
More let-rec experiments
2010-02-03, by Cezary Kaliszyk
proposal for an alpha equivalence
2010-02-03, by Christian Urban
Lets different.
2010-02-03, by Cezary Kaliszyk
Simplified the proof.
2010-02-03, by Cezary Kaliszyk
merged
2010-02-03, by Christian Urban
proved that bv for lists respects alpha for terms
2010-02-03, by Christian Urban
Finished remains on the let proof.
2010-02-03, by Cezary Kaliszyk
merge
2010-02-03, by Cezary Kaliszyk
Lets are ok.
2010-02-03, by Cezary Kaliszyk
merged
2010-02-03, by Christian Urban
added type-scheme example
2010-02-03, by Christian Urban
merge
2010-02-03, by Cezary Kaliszyk
Definitions for trm5
2010-02-03, by Cezary Kaliszyk
another adaptation for the eqvt-change
2010-02-03, by Christian Urban
merged
2010-02-03, by Christian Urban
fixed proofs that broke because of eqvt
2010-02-03, by Christian Urban
Minor fix.
2010-02-03, by Cezary Kaliszyk
merge
2010-02-03, by Cezary Kaliszyk
alpha5 pseudo-injective
2010-02-03, by Cezary Kaliszyk
fixed proofs in Abs.thy
2010-02-03, by Christian Urban
merged
2010-02-03, by Christian Urban
added a first eqvt_tac which pushes permutations inside terms
2010-02-03, by Christian Urban
The alpha-equivalence relation for let-rec. Not sure if correct...
2010-02-03, by Cezary Kaliszyk
Starting with a let-rec example.
2010-02-03, by Cezary Kaliszyk
Minor
2010-02-03, by Cezary Kaliszyk
Some cleaning and eqvt proof
2010-02-03, by Cezary Kaliszyk
The trm1_support lemma explicitly and stated a strong induction principle.
2010-02-03, by Cezary Kaliszyk
More ingredients in Terms.
2010-02-03, by Cezary Kaliszyk
Finished the supp_fv proof; first proof that analyses the structure of 'Let' :)
2010-02-02, by Cezary Kaliszyk
More in Terms
2010-02-02, by Cezary Kaliszyk
First experiments in Terms.
2010-02-02, by Cezary Kaliszyk
LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left.
2010-02-02, by Cezary Kaliszyk
Disambiguating the syntax.
2010-02-02, by Cezary Kaliszyk
Minor uncommited changes from LamEx2.
2010-02-02, by Cezary Kaliszyk
Some equivariance machinery that comes useful in LF.
2010-02-02, by Cezary Kaliszyk
Generalized the eqvt proof for single binders.
2010-02-02, by Cezary Kaliszyk
With induct instead of induct_tac, just one induction is sufficient.
2010-02-02, by Cezary Kaliszyk
General alpha_gen_trans for one-variable abstraction.
2010-02-02, by Cezary Kaliszyk
With unfolding Rep/Abs_eqvt no longer needed.
2010-02-02, by Cezary Kaliszyk
Lam2 finished apart from Rep_eqvt.
2010-02-02, by Cezary Kaliszyk
merge
2010-02-01, by Cezary Kaliszyk
All should be ok now.
2010-02-01, by Cezary Kaliszyk
repaired according to changes in Abs.thy
2010-02-01, by Christian Urban
added a single-binder alpha equivalence; showed one half of the equivalence proof between general and single binder case
2010-02-01, by Christian Urban
cleaned
2010-02-01, by Christian Urban
updated from huffman
2010-02-01, by Christian Urban
updated from nominal-huffman
2010-02-01, by Christian Urban
Fixed wrong rename.
2010-02-01, by Cezary Kaliszyk
merge
2010-02-01, by Cezary Kaliszyk
Lambda based on alpha_gen, under construction.
2010-02-01, by Cezary Kaliszyk
updated from huffman - repo
2010-02-01, by Christian Urban
renamed Abst/abst to Abs/abs
2010-02-01, by Christian Urban
got rid of RAbst type - is now just pairs
2010-02-01, by Christian Urban
Monotonicity of ~~gen, needed for using it in inductive definitions.
2010-02-01, by Cezary Kaliszyk
The current state of fv vs supp proofs in LF.
2010-02-01, by Cezary Kaliszyk
merge
2010-02-01, by Cezary Kaliszyk
More proofs in the LF example.
2010-02-01, by Cezary Kaliszyk
merged
2010-02-01, by Christian Urban
slight tuning
2010-02-01, by Christian Urban
renamed function according to the name of the constant
2010-02-01, by Christian Urban
fixed problem with Bex1_rel renaming
2010-02-01, by Christian Urban
Ported LF to the generic lambda and solved the simpler _supp cases.
2010-02-01, by Cezary Kaliszyk
merged
2010-01-30, by Christian Urban
introduced a generic alpha (but not sure whether it is helpful)
2010-01-30, by Christian Urban
More in the LF example in the new nominal way, all is clear until support.
2010-01-29, by Cezary Kaliszyk
Fixed the induction problem + some more proofs.
2010-01-29, by Cezary Kaliszyk
equivariance of rfv and alpha.
2010-01-29, by Cezary Kaliszyk
Added the experiments with fun and function.
2010-01-29, by Cezary Kaliszyk
now also final step is proved - the supp of lambdas is now completely characterised
2010-01-29, by Christian Urban
the supp of a lambda can now be characterised, *provided* the notion of free variables coincides with support on lambda terms
2010-01-29, by Christian Urban
improved the proof slightly by defining alpha as a function and completely characterised the equality between two abstractions
2010-01-28, by Christian Urban
merged
2010-01-28, by Christian Urban
general abstraction operator and complete characterisation of its support and freshness
2010-01-28, by Christian Urban
Ported existing part of LF to new permutations and alphas.
2010-01-28, by Cezary Kaliszyk
attempt of a general abstraction operator
2010-01-28, by Christian Urban
attempt to prove equivalence between alpha definitions
2010-01-28, by Christian Urban
End of renaming.
2010-01-28, by Cezary Kaliszyk
Minor when looking at lam.distinct and lam.inject
2010-01-28, by Cezary Kaliszyk
Renamed Bexeq to Bex1_rel
2010-01-28, by Cezary Kaliszyk
Substracting bounds from free variables.
2010-01-28, by Cezary Kaliszyk
Improper interface for datatype and function packages and proper interface lateron.
2010-01-28, by Cezary Kaliszyk
merged
2010-01-28, by Christian Urban
minor
2010-01-28, by Christian Urban
test about supp/freshness for lam (old proofs work in principle - for single binders)
2010-01-28, by Christian Urban
Recommited the changes for nitpick
2010-01-28, by Cezary Kaliszyk
Correct types which fixes the printing.
2010-01-27, by Cezary Kaliszyk
fv for subterms
2010-01-27, by Cezary Kaliszyk
Fix the problem with later examples. Maybe need to go back to textual specifications.
2010-01-27, by Cezary Kaliszyk
Some processing of variables in constructors to get free variables.
2010-01-27, by Cezary Kaliszyk
Parsing of the input as terms and types, and passing them as such to the function package.
2010-01-27, by Cezary Kaliszyk
Undid the parsing, as it is not possible with thy->lthy interaction.
2010-01-27, by Cezary Kaliszyk
merge
2010-01-27, by Cezary Kaliszyk
Some cleaning of thy vs lthy vs context.
2010-01-27, by Cezary Kaliszyk
merged
2010-01-27, by Christian Urban
tuned comment
2010-01-27, by Christian Urban
completely ported
2010-01-27, by Christian Urban
Another string in the specification.
2010-01-27, by Cezary Kaliszyk
Variable takes a 'name'.
2010-01-27, by Cezary Kaliszyk
merge
2010-01-27, by Cezary Kaliszyk
When commenting discovered a missing case of Babs->Abs regularization.
2010-01-27, by Cezary Kaliszyk
merged
2010-01-27, by Christian Urban
mostly ported Terms.thy to new Nominal
2010-01-27, by Christian Urban
merge
2010-01-27, by Cezary Kaliszyk
Commenting regularize
2010-01-27, by Cezary Kaliszyk
very rough example file for how nominal2 specification can be parsed
2010-01-27, by Christian Urban
reordered cases in regularize (will be merged into two cases)
2010-01-27, by Christian Urban
use of equiv_relation_chk in quotient_term
2010-01-27, by Christian Urban
some slight tuning
2010-01-27, by Christian Urban
added Terms to Nominal - Instantiation of two types does not work (ask Florian)
2010-01-27, by Christian Urban
added another example with indirect recursion over lists
2010-01-27, by Christian Urban
just moved obsolete material into Attic
2010-01-26, by Christian Urban
added an LamEx example together with the new nominal infrastructure
2010-01-26, by Christian Urban
Bex1_Bexeq_regular.
2010-01-26, by Cezary Kaliszyk
Hom Theorem with exists unique
2010-01-26, by Cezary Kaliszyk
2 cases for regularize with split, lemmas with split now lift.
2010-01-26, by Cezary Kaliszyk
Simpler statement that has the problem.
2010-01-26, by Cezary Kaliszyk
Found a term that does not regularize.
2010-01-26, by Cezary Kaliszyk
A triple is still ok.
2010-01-26, by Cezary Kaliszyk
Combined the simpsets in clean_tac and updated the comment. Now cleaning of splits does work.
2010-01-26, by Cezary Kaliszyk
Changed the lambda_prs_simple_conv to use id_apply, now last eq_reflection can be removed from id_simps.
2010-01-26, by Cezary Kaliszyk
Sigma cleaning works with split_prs (still manual proof).
2010-01-26, by Cezary Kaliszyk
tuned
2010-01-26, by Christian Urban
less
more
|
(0)
-1000
-480
+480
+1000
tip