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
|
2011-05-31 |
Cezary Kaliszyk |
Defined translation from nominal to de-Bruijn; with a freshness condition for the lambda case.
|
file |
diff |
annotate
|
2011-05-31 |
Cezary Kaliszyk |
Simple eqvt proofs with perm_simps for clarity
|
file |
diff |
annotate
|
2011-05-30 |
Christian Urban |
functions involving if and case do not throw exceptions anymore; but eqvt_at assumption has now a precondition
|
file |
diff |
annotate
|
2011-05-25 |
Christian Urban |
added eq_iff and distinct lemmas of nominal datatypes to the simplifier
|
file |
diff |
annotate
|
2011-05-14 |
Christian Urban |
added a problem with inductive_cases (reported by Randy)
|
file |
diff |
annotate
|
2011-05-03 |
Christian Urban |
added two mutual recursive inductive definitions
|
file |
diff |
annotate
|
2011-05-03 |
Christian Urban |
proved that lfp is equivariant (that simplifies equivariance proofs of inductively defined predicates)
|
file |
diff |
annotate
|
2011-04-18 |
Christian Urban |
merged
|
file |
diff |
annotate
|
2011-04-18 |
Christian Urban |
added permute_pure back into the nominal_inductive procedure; updated to Isabelle 17 April
|
file |
diff |
annotate
|
2011-04-15 |
Cezary Kaliszyk |
New way of forward elimination of Abs1_eq and simplifications of the function obligation proofs.
|
file |
diff |
annotate
|
2011-04-13 |
Christian Urban |
introduced framework for finetuning eqvt-rules; this solves problem with permute_pure called in nominal_inductive
|
file |
diff |
annotate
|
2011-02-23 |
Cezary Kaliszyk |
Reduce the definition of trans to FCB; test that FCB can be proved with simp rules.
|
file |
diff |
annotate
|
2011-02-01 |
Cezary Kaliszyk |
Only one of the subgoals is needed
|
file |
diff |
annotate
|
2011-01-25 |
Christian Urban |
made eqvt-proof explicit in the function definitions
|
file |
diff |
annotate
|
2011-01-19 |
Christian Urban |
added obtain_fresh lemma; tuned Lambda.thy
|
file |
diff |
annotate
|
2011-01-19 |
Christian Urban |
ported some of the old proofs to serve as testcases
|
file |
diff |
annotate
|
2011-01-19 |
Christian Urban |
defined height as a function that returns an integer
|
file |
diff |
annotate
|
2011-01-18 |
Christian Urban |
defined properly substitution
|
file |
diff |
annotate
|
2011-01-18 |
Christian Urban |
the function translating lambda terms to locally nameless lambda terms; still needs a stronger abs_eq_iff lemma...at the moment only proved for restrictions
|
file |
diff |
annotate
|
2011-01-17 |
Christian Urban |
added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment)
|
file |
diff |
annotate
|
2011-01-17 |
Christian Urban |
added a few examples of functions to Lambda.thy
|
file |
diff |
annotate
|
2011-01-17 |
Christian Urban |
removed old testing code from Lambda.thy
|
file |
diff |
annotate
|
2011-01-09 |
Christian Urban |
solved subgoals for depth and subst function
|
file |
diff |
annotate
|