2011-12-21 |
Cezary Kaliszyk |
Port CR_Takahashi from Nominal1, no more "sorry" in BetaCR.
|
file |
diff |
annotate
|
2011-12-17 |
Christian Urban |
cleaned examples for stable branch
Nominal2-Isabelle2011-1
|
file |
diff |
annotate
|
2011-12-15 |
Christian Urban |
updated to lates changes in the datatype package
|
file |
diff |
annotate
|
2011-11-08 |
Cezary Kaliszyk |
Add equivariance for alpha_lam_raw and abs_lam.
|
file |
diff |
annotate
|
2011-11-07 |
Christian Urban |
all examples work again after quotient package has been "de-localised"
|
file |
diff |
annotate
|
2011-08-19 |
Cezary Kaliszyk |
Comment out examples with 'True' that do not work because function still does not work
|
file |
diff |
annotate
|
2011-07-22 |
Christian Urban |
completed the eqvt-proofs for functions; they are stored under the name function_name.eqvt and added to the eqvt-list
|
file |
diff |
annotate
|
2011-07-19 |
Christian Urban |
preliminary version of automatically generation the eqvt-lemmas for functions defined with nominal_primrec
|
file |
diff |
annotate
|
2011-07-19 |
Christian Urban |
generated the partial eqvt-theorem for functions
|
file |
diff |
annotate
|
2011-07-18 |
Christian Urban |
added a flag (eqvt) to termination proofs arising fron nominal_primrecs
|
file |
diff |
annotate
|
2011-07-18 |
Christian Urban |
moved eqvt for Option.map
|
file |
diff |
annotate
|
2011-07-05 |
Christian Urban |
added some relatively simple examples from paper by Norrish
|
file |
diff |
annotate
|
2011-07-05 |
Christian Urban |
changed bind to binds in specifications; bind will cause trouble with Monad_Syntax
|
file |
diff |
annotate
|
2011-07-05 |
Christian Urban |
made the tests go through again
|
file |
diff |
annotate
|
2011-07-05 |
Christian Urban |
merged
|
file |
diff |
annotate
|
2011-07-05 |
Christian Urban |
exported various FCB-lemmas to a separate file
|
file |
diff |
annotate
|
2011-07-05 |
Cezary Kaliszyk |
Express trans_db with Option.map and Option.bind. Possibly mbind is a copy of bind?
|
file |
diff |
annotate
|
2011-07-05 |
Cezary Kaliszyk |
Define a version of aux only for same binders. Completeness is fine.
|
file |
diff |
annotate
|
2011-07-05 |
Cezary Kaliszyk |
Move If / Let with 'True' to the end of Lambda
|
file |
diff |
annotate
|
2011-07-04 |
Christian Urban |
added an example that recurses over two arguments; the interesting proof-obligation is not yet done
|
file |
diff |
annotate
|
2011-06-27 |
Christian Urban |
copied all work to Lambda.thy; had to derive a special version of fcb1 for concrete atom
|
file |
diff |
annotate
|
2011-06-26 |
Christian Urban |
another change to the fcb2; this is needed in order to get all proofs through in Lambda.thy
|
file |
diff |
annotate
|
2011-06-23 |
Christian Urban |
the simplifier can simplify "sort (atom a)" if a is a concrete atom type declared with atom_decl
|
file |
diff |
annotate
|
2011-06-22 |
Christian Urban |
some rudimentary infrastructure for storing data about nominal datatypes
|
file |
diff |
annotate
|
2011-06-16 |
Christian Urban |
got rid of the boolean flag in the raw_equivariance function
|
file |
diff |
annotate
|
2011-06-16 |
Christian Urban |
added a test that every function must be of pt-sort
|
file |
diff |
annotate
|
2011-06-15 |
Christian Urban |
added size-lemmas to simplifier; as a result termination can be proved by the standard lexicographic_order method
|
file |
diff |
annotate
|
2011-06-15 |
Cezary Kaliszyk |
Some TODOs
|
file |
diff |
annotate
|
2011-06-10 |
Cezary Kaliszyk |
Move working examples before non-working ones
|
file |
diff |
annotate
|
2011-06-10 |
Cezary Kaliszyk |
Optimized proofs and removed some garbage.
|
file |
diff |
annotate
|
2011-06-10 |
Cezary Kaliszyk |
Slightly modify fcb for list1 and put in common place.
|
file |
diff |
annotate
|
2011-06-09 |
Cezary Kaliszyk |
Eval can be defined with additional freshness
|
file |
diff |
annotate
|
2011-06-09 |
Cezary Kaliszyk |
Minor simplification
|
file |
diff |
annotate
|
2011-06-08 |
Christian Urban |
merged
|
file |
diff |
annotate
|
2011-06-08 |
Christian Urban |
merged
|
file |
diff |
annotate
|
2011-06-07 |
Cezary Kaliszyk |
Simplify ln-trans proof
|
file |
diff |
annotate
|
2011-06-07 |
Cezary Kaliszyk |
cbvs can be easily defined without an invariant
|
file |
diff |
annotate
|
2011-06-07 |
Christian Urban |
defined the "count-bound-variables-occurences" function which has an accumulator like trans
|
file |
diff |
annotate
|
2011-06-07 |
Christian Urban |
merged
|
file |
diff |
annotate
|
2011-06-07 |
Cezary Kaliszyk |
remove garbage (proofs that assumes the invariant outside function)
|
file |
diff |
annotate
|
2011-06-07 |
Cezary Kaliszyk |
Proof of trans with invariant
|
file |
diff |
annotate
|
2011-06-07 |
Christian Urban |
cleaned ups a bit the examples with the invariant framework; exported nominal_function_config datatype into separate structure and file
|
file |
diff |
annotate
|
2011-06-07 |
Christian Urban |
fixed problem with earlier commit about nominal_function_common; added facility for specifying an invariant - added a definition of frees_set which need a finiteness invariant
|
file |
diff |
annotate
|
2011-06-05 |
Christian Urban |
added an option for an invariant (at the moment only a stub)
|
file |
diff |
annotate
|
2011-06-04 |
Cezary Kaliszyk |
Finish and test the locale approach
|
file |
diff |
annotate
|
2011-06-03 |
Christian Urban |
recursion combinator inside a locale
|
file |
diff |
annotate
|
2011-06-02 |
Cezary Kaliszyk |
finished the missing obligations
|
file |
diff |
annotate
|
2011-06-02 |
Christian Urban |
merged
|
file |
diff |
annotate
|
2011-06-02 |
Christian Urban |
a test with a recursion combinator defined on top of nominal_primrec
|
file |
diff |
annotate
|
2011-06-02 |
Cezary Kaliszyk |
Use FCB to simplify proof
|
file |
diff |
annotate
|
2011-06-01 |
Christian Urban |
hopefully final fix for ho-functions
|
file |
diff |
annotate
|
2011-06-01 |
Christian Urban |
first test to fix the problem with free variables
|
file |
diff |
annotate
|
2011-06-01 |
Cezary Kaliszyk |
DB translation using index; easier to reason about.
|
file |
diff |
annotate
|
2011-06-01 |
Cezary Kaliszyk |
Problem: free variables in the goal
|
file |
diff |
annotate
|
2011-06-01 |
Cezary Kaliszyk |
fixed previous commit
|
file |
diff |
annotate
|
2011-06-01 |
Cezary Kaliszyk |
equivariance of db_trans
|
file |
diff |
annotate
|
2011-05-31 |
Christian Urban |
fixed the problem with cps-like functions
|
file |
diff |
annotate
|
2011-05-31 |
Cezary Kaliszyk |
DeBruijn translation in a simplifier friendly way
|
file |
diff |
annotate
|
2011-05-31 |
Cezary Kaliszyk |
map_term can be defined when equivariance is assumed
|
file |
diff |
annotate
|
2011-05-31 |
Cezary Kaliszyk |
map_term is not a function the way it is defined
|
file |
diff |
annotate
|