nominal2: Graph

Mercurial Mercurial > hg > nominal2 / graph

summary | shortlog | changelog | graph | tags | bookmarks | branches | files | help
less more | (0) -1000 -300 -100 -60 +60 +100 +300 tip

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

less more | (0) -1000 -300 -100 -60 +60 +100 +300 tip

nominal2