Mercurial
Mercurial
>
hg
>
nominal2
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
help
less
more
|
(0)
-1000
-240
+240
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.
remove garbage (proofs that assumes the invariant outside function)
2011-06-07, by Cezary Kaliszyk
Proof of trans with invariant
2011-06-07, by Cezary Kaliszyk
Testing invariant in Lambda_F_T
2011-06-07, by Cezary Kaliszyk
cleaned ups a bit the examples with the invariant framework; exported nominal_function_config datatype into separate structure and file
2011-06-07, by 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
2011-06-07, by Christian Urban
slightly stronger property in fundef_ex_prop
2011-06-06, by Christian Urban
added an option for an invariant (at the moment only a stub)
2011-06-05, by Christian Urban
added a more general lemma fro fundef_ex1
2011-06-05, by Christian Urban
Trying the induction on the graph
2011-06-04, by Cezary Kaliszyk
Finish and test the locale approach
2011-06-04, by Cezary Kaliszyk
FiniteSupp precondition in the function is enough to get rid of completeness obligationss
2011-06-03, by Cezary Kaliszyk
recursion combinator inside a locale
2011-06-03, by Christian Urban
merge
2011-06-03, by Cezary Kaliszyk
F for lambda used to define translation to locally nameless
2011-06-03, by Cezary Kaliszyk
typo
2011-06-02, by Christian Urban
removed dead code
2011-06-02, by Christian Urban
finished the missing obligations
2011-06-02, by Cezary Kaliszyk
merged
2011-06-02, by Christian Urban
a test with a recursion combinator defined on top of nominal_primrec
2011-06-02, by Christian Urban
Use FCB to simplify proof
2011-06-02, by Cezary Kaliszyk
merge
2011-06-02, by Cezary Kaliszyk
Remove SMT
2011-06-02, by Cezary Kaliszyk
hopefully final fix for ho-functions
2011-06-01, by Christian Urban
first test to fix the problem with free variables
2011-06-01, by Christian Urban
proved subst for All constructor in type schemes.
2011-06-01, by Cezary Kaliszyk
DB translation using index; easier to reason about.
2011-06-01, by Cezary Kaliszyk
Problem: free variables in the goal
2011-06-01, by Cezary Kaliszyk
fixed previous commit
2011-06-01, by Cezary Kaliszyk
equivariance of db_trans
2011-06-01, by Cezary Kaliszyk
fixed the problem with cps-like functions
2011-05-31, by Christian Urban
DeBruijn translation in a simplifier friendly way
2011-05-31, by Cezary Kaliszyk
map_term can be defined when equivariance is assumed
2011-05-31, by Cezary Kaliszyk
map_term is not a function the way it is defined
2011-05-31, by Cezary Kaliszyk
Defined translation from nominal to de-Bruijn; with a freshness condition for the lambda case.
2011-05-31, by Cezary Kaliszyk
Simple eqvt proofs with perm_simps for clarity
2011-05-31, by Cezary Kaliszyk
tuned last commit
2011-05-31, by Christian Urban
functions involving if and case do not throw exceptions anymore; but eqvt_at assumption has now a precondition
2011-05-31, by Christian Urban
updated to new Isabelle
2011-05-26, by Christian Urban
added eq_iff and distinct lemmas of nominal datatypes to the simplifier
2011-05-25, by Christian Urban
more on slides
2011-05-24, by Christian Urban
added slides for copenhagen
2011-05-22, by Christian Urban
added a problem with inductive_cases (reported by Randy)
2011-05-14, by Christian Urban
misc
2011-05-13, by Christian Urban
made the subtyping work again
2011-05-10, by Christian Urban
updated to new Isabelle (> 9 May)
2011-05-10, by Christian Urban
merged
2011-05-09, by Christian Urban
added two mutual recursive inductive definitions
2011-05-03, by Christian Urban
deleted two functions from the API
2011-05-03, by Christian Urban
proved that lfp is equivariant (that simplifies equivariance proofs of inductively defined predicates)
2011-05-03, by Christian Urban
more on pearl-paper
2011-05-09, by Christian Urban
more on pearl-paper
2011-05-04, by Christian Urban
updated Quotient paper so that it compiles again
2011-05-02, by Christian Urban
merged
2011-04-28, by Christian Urban
added slides for beijing
2011-04-28, by Christian Urban
more to the pearl paper
2011-04-22, by Christian Urban
updated to snapshot Isabelle 19 April
2011-04-19, by Christian Urban
merged
2011-04-18, by Christian Urban
added permute_pure back into the nominal_inductive procedure; updated to Isabelle 17 April
2011-04-18, by Christian Urban
New way of forward elimination of Abs1_eq and simplifications of the function obligation proofs.
2011-04-15, by Cezary Kaliszyk
merged
2011-04-13, by Christian Urban
introduced framework for finetuning eqvt-rules; this solves problem with permute_pure called in nominal_inductive
2011-04-13, by Christian Urban
shanghai slides
2011-04-12, by Christian Urban
pictures for slides
2011-04-11, by Christian Urban
Shanghai slides
2011-04-11, by Christian Urban
more paper
2011-04-10, by Christian Urban
eqvt of supp and fresh is proved using equivariance infrastructure
2011-04-10, by Christian Urban
more paper
2011-04-10, by Christian Urban
more on the paper
2011-04-09, by Christian Urban
tuned paper
2011-04-09, by Christian Urban
tuned paper
2011-04-09, by Christian Urban
typo
2011-04-09, by Christian Urban
more on paper
2011-04-08, by Christian Urban
eqvt_lambda without eta-expansion
2011-04-08, by Christian Urban
changed default preprocessor that does not catch variables only occuring on the right
2011-04-06, by Christian Urban
final version of slides
2011-03-31, by Christian Urban
more on the slides
2011-03-30, by Christian Urban
tuned IsaMakefile
2011-03-30, by Christian Urban
rearranged directories and updated to new Isabelle
2011-03-29, by Christian Urban
precise path to LaTeXsugar
2011-03-16, by Christian Urban
a lit bit more on the pearl-jv paper
2011-03-16, by Christian Urban
ported changes from function package....needs Isabelle 16 March or above
2011-03-16, by Christian Urban
more on the pearl paper
2011-03-15, by Christian Urban
equivariance for All and Ex can be proved in terms of their definition
2011-03-14, by Christian Urban
more on the paper
2011-03-11, by Christian Urban
merged
2011-03-08, by Christian Urban
more on the pearl paper
2011-03-08, by Christian Urban
distinct names at toplevel
2011-03-02, by Cezary Kaliszyk
merge
2011-03-02, by Cezary Kaliszyk
Pairing function
2011-03-02, by Cezary Kaliszyk
updated pearl papers
2011-03-02, by Christian Urban
a bit more tuning
2011-03-01, by Christian Urban
included old test cases for perm_simp into ROOT.ML file
2011-02-28, by Christian Urban
split the library into a basics file; merged Nominal_Eqvt into Nominal_Base
2011-02-28, by Christian Urban
some slight polishing
2011-02-25, by Christian Urban
merged
2011-02-24, by Christian Urban
added a lemma about fresh_star and Abs
2011-02-24, by Christian Urban
Reduce the definition of trans to FCB; test that FCB can be proved with simp rules.
2011-02-23, by Cezary Kaliszyk
typeschemes/subst
2011-02-19, by Cezary Kaliszyk
further experiments with typeschemes subst
2011-02-17, by Cezary Kaliszyk
Finished the proof of a function that invents fresh variable names.
2011-02-17, by Cezary Kaliszyk
added eqvt for length
2011-02-16, by Christian Urban
added eqvt lemmas for filter and distinct
2011-02-16, by Christian Urban
added eqvt for cartesian products
2011-02-07, by Christian Urban
cleaned up the experiments so that the tests go through
2011-02-07, by Christian Urban
merge
2011-02-05, by Cezary Kaliszyk
Experiments defining a function on Let
2011-02-05, by Cezary Kaliszyk
updated TODO
2011-02-04, by Christian Urban
Lambda.thy which works with Nominal_Isabelle2011
2011-02-04, by Christian Urban
merged
2011-02-03, by Christian Urban
removed diagnostic code
2011-02-03, by Christian Urban
Only one of the subgoals is needed
2011-02-01, by Cezary Kaliszyk
Experiments with substitution on set+
2011-02-01, by Cezary Kaliszyk
More properties that relate abs_res and abs_set. Also abs_res with less binders.
2011-02-01, by Cezary Kaliszyk
alpha_res implies alpha_set :)
2011-01-30, by Cezary Kaliszyk
Showing that the binders difference is fresh for the left side solves the goal for 'set'.
2011-01-30, by Cezary Kaliszyk
Experiments with functions
2011-01-29, by Cezary Kaliszyk
some experiments
2011-01-27, by Christian Urban
the proofs with eqvt_at
2011-01-27, by Christian Urban
made eqvt-proof explicit in the function definitions
2011-01-25, by Christian Urban
merge
2011-01-25, by Cezary Kaliszyk
minor
2011-01-25, by Cezary Kaliszyk
Down as infixr
2011-01-25, by Cezary Kaliszyk
added some slides
2011-01-22, by Christian Urban
added Tutorial6
2011-01-23, by Christian Urban
cleaning up
2011-01-22, by Christian Urban
merged
2011-01-22, by Christian Urban
cleaned up Tutorial 3 with solutions
2011-01-22, by Christian Urban
Missing val.simps
2011-01-23, by Cezary Kaliszyk
merge
2011-01-23, by Cezary Kaliszyk
Tutorial 4s
2011-01-23, by Cezary Kaliszyk
cleaned up and solution section
2011-01-22, by Christian Urban
cleaned up tutorial1...added solution file
2011-01-22, by Christian Urban
better version of Tutorial 1
2011-01-22, by Christian Urban
better flow of proofs and definitions and proof
2011-01-21, by Christian Urban
separated type preservation and progress into a separate file
2011-01-21, by Christian Urban
substitution lemma in separate file
2011-01-21, by Christian Urban
added unbind example
2011-01-21, by Christian Urban
a bit tuning
2011-01-21, by Christian Urban
first split of tutorrial theory
2011-01-20, by Christian Urban
added a very rough version of the tutorial; all seems to work
2011-01-19, by Christian Urban
added obtain_fresh lemma; tuned Lambda.thy
2011-01-19, by Christian Urban
base file for the tutorial (contains definitions for heigt, subst and beta-reduction)
2011-01-19, by Christian Urban
ported some of the old proofs to serve as testcases
2011-01-19, by Christian Urban
added eqvt and supp lemma for removeAll (function from List.thy)
2011-01-19, by Christian Urban
theory name as it should be
2011-01-19, by Christian Urban
removed diagnostic code
2011-01-19, by Christian Urban
added Minimal file to test things
2011-01-19, by Christian Urban
defined height as a function that returns an integer
2011-01-19, by Christian Urban
deleted diagnostic code
2011-01-18, by Christian Urban
some tryes about substitution over type-schemes
2011-01-18, by Christian Urban
defined properly substitution
2011-01-18, by Christian Urban
derived stronger Abs_eq_iff2 theorems
2011-01-18, by Christian Urban
made alpha_abs_set_stronger1 stronger
2011-01-18, by Christian Urban
removed finiteness assumption from set_rename_perm
2011-01-18, by Christian Urban
alpha_abs_set_stronger1
2011-01-18, by Cezary Kaliszyk
alpha_abs_let_stronger is not true in the same form
2011-01-18, by Cezary Kaliszyk
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
2011-01-18, by Christian Urban
modified the renaming_perm lemmas
2011-01-18, by Christian Urban
added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment)
2011-01-17, by Christian Urban
added a few examples of functions to Lambda.thy
2011-01-17, by Christian Urban
exported nominal function code to external file
2011-01-17, by Christian Urban
removed old testing code from Lambda.thy
2011-01-17, by Christian Urban
moved high level code from LamTest into the main libraries.
2011-01-17, by Christian Urban
eliminated tracing code; added flag so that equivariance is only proved for the function graph, not the relation
2011-01-17, by Christian Urban
subst also works now
2011-01-15, by Christian Urban
nominal_function works now completely for frees and depth; still a propbelm with subst; no unproved assumptions
2011-01-15, by Christian Urban
strengthened renaming lemmas
2011-01-14, by Christian Urban
added eqvt_lemmas for subset and psubset
2011-01-13, by Christian Urban
a few lemmas about freshness for at and at_base
2011-01-10, by Christian Urban
added a property about finite support in the presense of eqvt_at
2011-01-10, by Christian Urban
instantiated fundef_ex1_eqvt_at theorem with the indction hypothesis
2011-01-09, by Christian Urban
solved subgoals for depth and subst function
2011-01-09, by Christian Urban
added eqvt_at premises in function definition - however not proved at the moment
2011-01-09, by Christian Urban
added one further lemma about equivariance of THE_default
2011-01-07, by Christian Urban
equivariance of THE_default under the uniqueness assumption
2011-01-07, by Christian Urban
derived equivariance for the function graph and function relation
2011-01-07, by Christian Urban
a modified function package where, as a test, True has been injected into the compatibility condictions
2011-01-06, by Christian Urban
removed last traces of debugging code
2011-01-06, by Christian Urban
removed debugging code abd introduced a guarded tracing function
2011-01-06, by Christian Urban
moved Weakening up....it does not compile when put at the last position
2011-01-06, by Christian Urban
tuned
2011-01-06, by Christian Urban
added weakening to the test cases
2011-01-06, by Christian Urban
cleaned up weakening proof and added a version with finit sets
2011-01-06, by Christian Urban
same
2011-01-06, by Christian Urban
some further lemmas for fsets
2011-01-06, by Christian Urban
made sure the raw datatypes and raw functions do not get any mixfix syntax
2011-01-06, by Christian Urban
exported the code into a separate file
2011-01-05, by Christian Urban
strong rule inductions; as an example the weakening lemma works
2011-01-05, by Christian Urban
final version of the ESOP paper; used set+ instead of res as requested by one reviewer
2011-01-04, by Christian Urban
file with most of the strong rule induction development
2011-01-03, by Christian Urban
simple cases for string rule inductions
2011-01-03, by Christian Urban
changed res keyword to set+ for restrictions; comment by a referee
2010-12-31, by Christian Urban
added proper case names for all induct and exhaust theorems
2010-12-31, by Christian Urban
added small example for strong inductions; functions still need a sorry
2010-12-31, by Christian Urban
removed local fix for bug in induction_schema; added setup method for strong inductions
2010-12-30, by Christian Urban
automated all strong induction lemmas
2010-12-28, by Christian Urban
proper application of induction_schema and strong_exhaust rules; needs local fix in induction_schema.ML
2010-12-28, by Christian Urban
generated goals for strong induction theorems.
2010-12-26, by Christian Urban
test with strong inductions
2010-12-23, by Christian Urban
moved all strong_exhaust code to nominal_dt_quot; tuned examples
2010-12-23, by Christian Urban
moved generic functions into nominal_library
2010-12-23, by Christian Urban
slight tuning
2010-12-22, by Christian Urban
slight tuning
2010-12-22, by Christian Urban
tuned examples
2010-12-22, by Christian Urban
added fold_right which produces the correct term for left-infix operators
2010-12-22, by Christian Urban
updated to Isabelle 22 December
2010-12-22, by Christian Urban
a bit tuning
2010-12-22, by Christian Urban
corrected premises of strong exhausts theorems
2010-12-22, by Christian Urban
properly exported strong exhaust theorem; cleaned up some examples
2010-12-22, by Christian Urban
all examples for strong exhausts work; recursive binders need to be treated differently; still unclean version with lots of diagnostic code
2010-12-21, by Christian Urban
one interesting case done
2010-12-19, by Christian Urban
a stronger statement for at_set_avoiding
2010-12-19, by Christian Urban
tuned
2010-12-17, by Christian Urban
tuned
2010-12-17, by Christian Urban
simple cases for strong inducts done; infrastructure for the difficult ones is there
2010-12-16, by Christian Urban
added theorem-rewriter conversion
2010-12-16, by Christian Urban
freshness theorem in strong exhausts; (temporarily includes a cheat_tac to make all tests go through)
2010-12-14, by Christian Urban
created strong_exhausts terms
2010-12-12, by Christian Urban
moved setify and listify functions into the library; introduced versions that have a type argument
2010-12-12, by Christian Urban
updated
2010-12-10, by Christian Urban
a bit more tuning of the paper
2010-12-09, by Christian Urban
brought the paper to 20 pages plus one page appendix
2010-12-09, by Christian Urban
first tests about exhaust
2010-12-08, by Christian Urban
moved some code into the nominal_library
2010-12-08, by Christian Urban
moved definition of raw bn-functions into nominal_dt_rawfuns
2010-12-08, by Christian Urban
kept the nested structure of constructors (belonging to one datatype)
2010-12-08, by Christian Urban
moved general theorems into the libraries
2010-12-07, by Christian Urban
automated permute_bn theorems
2010-12-07, by Christian Urban
updated to changes in Isabelle
2010-12-07, by Christian Urban
deleted nominal_dt_supp.ML
2010-12-06, by Christian Urban
moved code from nominal_dt_supp to nominal_dt_quot
2010-12-06, by Christian Urban
automated alpha_perm_bn theorems
2010-12-06, by Christian Urban
ordered raw_bn_info to agree with the order of the raw_bn_functions; started alpha_bn proof
2010-12-06, by Christian Urban
updated to Isabelle 2nd December
2010-12-03, by Christian Urban
isarfied some of the high-level proofs
2010-11-29, by Christian Urban
added abs_rename_res lemma
2010-11-29, by Christian Urban
completed proofs in Foo2
2010-11-29, by Christian Urban
completed the strong exhausts rules for Foo2 using general lemmas
2010-11-28, by Christian Urban
tuned proof to reduce number of warnings
2010-11-27, by Christian Urban
disabled the Foo examples, because of heavy work
2010-11-27, by Christian Urban
less
more
|
(0)
-1000
-240
+240
tip