2010-04-19 Cezary Kaliszyk merge
2010-04-19 Cezary Kaliszyk Locations of files in Parser
2010-04-19 Cezary Kaliszyk merge
2010-04-19 Cezary Kaliszyk minor FSet3 edits.
2010-04-18 Christian Urban tuned
2010-04-18 Christian Urban moved some general function into nominal_library.ML
2010-04-18 Christian Urban tuned; transformation functions now take a context, a thm and return a thm
2010-04-18 Christian Urban tuned
2010-04-18 Christian Urban equivariance for alpha_raw in CoreHaskell is automatically derived
2010-04-18 Christian Urban preliminary parser for perm_simp metod
2010-04-16 Christian Urban automatic proofs for equivariance of alphas
2010-04-16 Cezary Kaliszyk Finished proof in Lambda.thy
2010-04-16 Christian Urban merged
2010-04-16 Christian Urban attempt to manual prove eqvt for alpha
2010-04-16 Cezary Kaliszyk Lifting in Term4.
2010-04-16 Christian Urban some tuning of eqvt-infrastructure
2010-04-15 Christian Urban some tuning of proofs
2010-04-15 Christian Urban typo
2010-04-15 Christian Urban merged
2010-04-15 Christian Urban half of the pair-abs-equivalence
2010-04-15 Cezary Kaliszyk More on Manual/Trm4
2010-04-15 Cezary Kaliszyk alpha4_equivp and constant lifting.
2010-04-15 Cezary Kaliszyk alpha4_eqvt and alpha4_reflp
2010-04-15 Cezary Kaliszyk fv_eqvt in term4
2010-04-15 Cezary Kaliszyk Updating in Term4.
2010-04-15 Cezary Kaliszyk merge
2010-04-15 Cezary Kaliszyk Prove insert_rsp2
2010-04-15 Christian Urban merged
2010-04-15 Christian Urban changed header
2010-04-15 Cezary Kaliszyk Minor paper fixes.
2010-04-14 Christian Urban temporary fix for CoreHaskell
2010-04-14 Christian Urban deleted offending [eqvt]-attribute in Abs; Lambda works again, but there is now a problem in CoreHaskell
2010-04-14 Cezary Kaliszyk merge
2010-04-14 Cezary Kaliszyk Fix the 'subscript' error.
2010-04-14 Christian Urban merged
2010-04-14 Christian Urban thmdecls can deal with lemmas like alpha_gen which contain pairs or tuples
2010-04-14 Cezary Kaliszyk merge
2010-04-14 Cezary Kaliszyk merge
2010-04-14 Cezary Kaliszyk Separate alpha_definition.
2010-04-14 Cezary Kaliszyk Fix spelling in theory header
2010-04-14 Cezary Kaliszyk Separate define_fv.
2010-04-14 Christian Urban tuned and removed dead code
2010-04-14 Christian Urban moved a couple of more functions to the library
2010-04-14 Christian Urban added a library for basic nominal functions; separated nominal_eqvt file
2010-04-14 Christian Urban merged
2010-04-14 Christian Urban first working version of the automatic equivariance procedure
2010-04-14 Cezary Kaliszyk Initial cleaning/reorganization in Fv.
2010-04-14 Christian Urban merged
2010-04-14 Christian Urban preliminary tests
2010-04-14 Christian Urban deleted test
2010-04-14 Cezary Kaliszyk merge
2010-04-14 Cezary Kaliszyk merge part: delete_rsp
2010-04-14 Cezary Kaliszyk merge part1: none_memb_nil
2010-04-14 Christian Urban added header and more tuning
2010-04-14 Christian Urban more tuning
2010-04-14 Christian Urban tuned
2010-04-13 Cezary Kaliszyk Working FSet with additional lemmas.
2010-04-13 Cezary Kaliszyk Much more in FSet (currently non-working)
2010-04-13 Christian Urban made everything to compile
2010-04-12 Christian Urban merged
2010-04-12 Christian Urban some small tunings (incompleted work in Lambda.thy)
2010-04-12 Christian Urban moved equivariance of map into Nominal2_Eqvt file
2010-04-12 Christian Urban early ott paper
2010-04-12 Cezary Kaliszyk Porting lemmas from Quotient package FSet to new FSet.
2010-04-12 Christian Urban added alpha-caml paper
2010-04-12 Christian Urban implemented in thmdecls the case where eqvt-lemmas are of the form _ ==> _
2010-04-11 Christian Urban fixed bug in thmdecls with destructing Trueprop; some initial infrastructure for eqvt-theorems of the form _ ==> _
2010-04-11 Christian Urban folded changes from the conference version
2010-04-11 Christian Urban added TODO item about parser creating syntax for the wrong type
2010-04-11 Christian Urban corrected imports header
2010-04-11 Christian Urban tuned
2010-04-11 Christian Urban a few tests
2010-04-11 Christian Urban added eqvt rules that are more standard
2010-04-11 Christian Urban used warning instead of tracing (does not seem to produce stable output)
2010-04-11 Christian Urban added small ittems about equivaraince of alpha_gens and name of lam.perm
2010-04-11 Christian Urban added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
2010-04-09 Christian Urban changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
2010-04-09 Brian Huffman rewrite paragraph introducing equivariance, add citation to Pitts03
2010-04-09 Brian Huffman edit 'contributions' section so we do not just quote directly from the reviewer
2010-04-09 Christian Urban renamed ExLam to Lambda and completed the proof of the strong ind principle; tuned paper
2010-04-08 Christian Urban clarified comment about distinct lists in th efuture work section
2010-04-08 Christian Urban tuned type-schemes example
2010-04-08 Christian Urban updated (comment about weirdo example)
2010-04-08 Christian Urban check whether the "weirdo" example from the binding bestiary works with shallow binders
2010-04-08 Christian Urban properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper)
2010-04-08 Christian Urban merged
2010-04-08 Christian Urban some further changes
2010-04-08 Brian Huffman merged
2010-04-08 Brian Huffman change some wording in conclusion
2010-04-08 Brian Huffman remove extra word
2010-04-08 Christian Urban merged
2010-04-08 Christian Urban added new paper directory for further work
2010-04-08 Brian Huffman use qualified name as string in concrete atom example
2010-04-08 Brian Huffman merged
2010-04-08 Brian Huffman simplify instance proof
2010-04-08 Brian Huffman polish explanation of additive group syntax
2010-04-08 Christian Urban final version of the pearl paper
2010-04-07 Christian Urban my final version of the paper
2010-04-07 Christian Urban added an induction principle for permutations; removed add_perm construction
2010-04-06 Christian Urban isarfied proof about existence of a permutation list
2010-04-06 Christian Urban added reference to E. Gunter's work
2010-04-06 Christian Urban typos in paper
2010-04-04 Christian Urban separated general nominal theory into separate folder
2010-04-03 Christian Urban added README and moved examples into separate directory
2010-04-03 Christian Urban merged pearl paper with this repository; started litrature subdirectory
2010-04-02 Christian Urban submitted version (just in time ;o)
2010-04-02 Christian Urban first complete version (slightly less than 3h more to go)
2010-04-02 Christian Urban tuned
2010-04-02 Christian Urban tuned strong ind section
2010-04-02 Christian Urban polished infrastruct section
2010-04-02 Christian Urban completed lifting section
2010-04-02 Christian Urban more on the lifting section
2010-04-02 Christian Urban more on the strong induction section
2010-04-01 Christian Urban completed conclusion
2010-04-01 Christian Urban merged
2010-04-01 Christian Urban merged
2010-04-01 Christian Urban updated related work section
2010-04-01 Cezary Kaliszyk fv_fv_bn
2010-04-01 Cezary Kaliszyk Update fv_bn definition for bindings allowed in types for which bn is present.
2010-04-01 Cezary Kaliszyk fv_perm_bn
2010-04-01 Cezary Kaliszyk Minor formula fixes.
2010-04-01 Christian Urban fixed alpha_bn
2010-04-01 Christian Urban current state
2010-04-01 Christian Urban merged
2010-04-01 Christian Urban added alpha_bn definition
2010-04-01 Cezary Kaliszyk hfill for right aligning single table cells.
2010-04-01 Cezary Kaliszyk Cleaning the strong induction example.
2010-04-01 Cezary Kaliszyk minor
2010-04-01 Cezary Kaliszyk Fighting with space in displaying strong induction...
2010-04-01 Cezary Kaliszyk starting strong induction
2010-04-01 Cezary Kaliszyk General paper minor fixes.
2010-04-01 Cezary Kaliszyk Forgot to save before commit.
2010-04-01 Cezary Kaliszyk Let with multiple bindings.
2010-04-01 Cezary Kaliszyk Fill the space below the figure.
2010-04-01 Christian Urban last commit for now.
2010-04-01 Christian Urban more on the conclusion
2010-04-01 Christian Urban completed related work section
2010-04-01 Christian Urban more on the paper
2010-03-31 Christian Urban added an item about alpha-equivalence (the existential should be closer to the abstraction)
2010-03-31 Christian Urban polished everything up to TODO
2010-03-31 Christian Urban merged
2010-03-31 Christian Urban added alpha-definition for ~~ty
2010-03-31 Cezary Kaliszyk permute_bn
2010-03-31 Christian Urban abbreviations for \<otimes> and \<oplus>
2010-03-31 Christian Urban merged
2010-03-31 Christian Urban a test with let having multiple bodies
2010-03-31 Christian Urban polished and removed tys from bn-functions.
2010-03-31 Cezary Kaliszyk merge
2010-03-31 Cezary Kaliszyk More on paper
2010-03-31 Christian Urban started to polish alpha-equivalence section, but needs more work
2010-03-31 Christian Urban started with a related work section
2010-03-30 Christian Urban polished and added an example for fvars
2010-03-30 Christian Urban cleaned up the section about fv's
2010-03-30 Christian Urban tuned beginning of section 4
2010-03-30 Cezary Kaliszyk More on section 5.
2010-03-30 Cezary Kaliszyk More on section 5.
2010-03-30 Christian Urban merged
2010-03-30 Christian Urban removed "raw" distinction
2010-03-30 Cezary Kaliszyk More on Section 5
2010-03-30 Cezary Kaliszyk Beginning of section 5.
2010-03-30 Christian Urban merged
2010-03-30 Cezary Kaliszyk Avoid mentioning other nominal datatypes as it makes things too complicated.
2010-03-30 Christian Urban merged
2010-03-30 Cezary Kaliszyk close the missing parenthesis on both sides.
2010-03-30 Christian Urban merged
2010-03-30 Christian Urban changes to section 2
2010-03-30 Cezary Kaliszyk Clean alpha
2010-03-30 Cezary Kaliszyk clean fv_bn
2010-03-30 Cezary Kaliszyk alpha_bn
2010-03-30 Cezary Kaliszyk Change @{text} to @{term}
2010-03-30 Cezary Kaliszyk alpha
2010-03-30 Cezary Kaliszyk more
2010-03-30 Cezary Kaliszyk fv and fv_bn
2010-03-30 Christian Urban more of the paper
2010-03-29 Christian Urban merged
2010-03-29 Cezary Kaliszyk Updated strong induction to modified definitions.
2010-03-29 Cezary Kaliszyk Initial renaming
2010-03-29 Christian Urban small changes in the core-haskell spec
2010-03-29 Cezary Kaliszyk Update according to paper
2010-03-29 Cezary Kaliszyk merge
2010-03-29 Cezary Kaliszyk merge
2010-03-29 Cezary Kaliszyk Changed to Lists.
2010-03-29 Christian Urban clarified core-haskell example
2010-03-29 Christian Urban spell check
2010-03-29 Cezary Kaliszyk merge
2010-03-29 Cezary Kaliszyk Abs_gen and Abs_let simplifications.
2010-03-29 Christian Urban more on the paper
2010-03-28 Christian Urban fixed a problem due to a change in type-def (needs new Isabelle)
2010-03-28 Christian Urban merged
2010-03-28 Christian Urban more on the paper
2010-03-28 Christian Urban got rid of the aux-function on the raw level, by defining it with function on the quotient level
2010-03-27 Cezary Kaliszyk Lets finally abstract lists.
2010-03-27 Cezary Kaliszyk Core Haskell can now use proper strings.
2010-03-27 Cezary Kaliszyk Automatically lift theorems and constants only using the new quotient types. Requires new Isabelle.
2010-03-27 Cezary Kaliszyk Remove list_eq notation.
2010-03-27 Cezary Kaliszyk Get lifted types information from the quotient package.
2010-03-27 Cezary Kaliszyk Equivariance when bn functions are lists.
2010-03-27 Cezary Kaliszyk Accepts lists in FV.
2010-03-27 Cezary Kaliszyk Parsing of list-bn functions into components.
2010-03-27 Cezary Kaliszyk Automatically compute support if only one type of Abs is present in the type.
2010-03-27 Cezary Kaliszyk Manually proved TySch support; All properties of TySch now true.
2010-03-27 Cezary Kaliszyk Generalize Abs_eq_iff.
2010-03-27 Cezary Kaliszyk Minor fix.
2010-03-27 Cezary Kaliszyk New compose lemmas. Reverted alpha_gen sym/trans changes. Equivp for alpha_res should work now.
2010-03-27 Cezary Kaliszyk Initial proof modifications for alpha_res
2010-03-27 Cezary Kaliszyk merge
2010-03-27 Cezary Kaliszyk Fv/Alpha now takes into account Alpha_Type given from the parser.
2010-03-27 Cezary Kaliszyk Minor cleaning.
2010-03-27 Christian Urban merged
2010-03-27 Christian Urban more on the paper
2010-03-27 Cezary Kaliszyk Removed some warnings.
2010-03-26 Cezary Kaliszyk merge
2010-03-26 Cezary Kaliszyk Modified abs_gen_sym and abs_gen_trans so it becomes usable in the proofs.
2010-03-26 Christian Urban merged
2010-03-26 Christian Urban more on the paper
2010-03-26 Christian Urban simplification
2010-03-26 Cezary Kaliszyk merge
2010-03-26 Cezary Kaliszyk Describe 'nominal_datatype2'.
2010-03-26 Cezary Kaliszyk Fixed renamings.
2010-03-26 Christian Urban merged
2010-03-26 Cezary Kaliszyk Removed remaining cheats + some cleaning.
2010-03-26 Cezary Kaliszyk Extract PS7 and PS8 from Test. PS7 needs the same fix as Core Haskell.
2010-03-26 Cezary Kaliszyk Update cheats in TODO.
2010-03-26 Cezary Kaliszyk Removed another cheat and cleaned the code a bit.
2010-03-26 Cezary Kaliszyk Fix Manual/LamEx for experiments.
2010-03-25 Cezary Kaliszyk Proper bn_rsp, for bn functions calling each other.
2010-03-25 Cezary Kaliszyk Gathering things to prove by induction together; removed cheat_bn_eqvt.
2010-03-25 Cezary Kaliszyk Update TODO
2010-03-25 Cezary Kaliszyk Showed ACons_subst.
2010-03-25 Cezary Kaliszyk Only ACons_subst left to show.
2010-03-25 Cezary Kaliszyk Solved all boring subgoals, and looking at properly defning permute_bv
2010-03-25 Cezary Kaliszyk One more copy-and-paste in core-haskell.
2010-03-25 Cezary Kaliszyk Properly defined permute_bn. No more sorry's in Let strong induction.
2010-03-25 Cezary Kaliszyk Showed Let substitution.
2010-03-25 Cezary Kaliszyk Only let substitution is left.
2010-03-25 Cezary Kaliszyk further in the proof
2010-03-25 Cezary Kaliszyk trying to prove the string induction for let.
2010-03-25 Christian Urban added experiemental permute_bn
2010-03-25 Christian Urban first attempt of strong induction for lets with assignments
2010-03-25 Christian Urban more on the paper
2010-03-24 Christian Urban more on the paper
2010-03-24 Cezary Kaliszyk Further in the strong induction proof.
2010-03-24 Cezary Kaliszyk Solved one of the strong-induction goals.
2010-03-24 Cezary Kaliszyk avoiding for atom.
2010-03-24 Cezary Kaliszyk Started proving strong induction.
2010-03-24 Cezary Kaliszyk stating the strong induction; further.
2010-03-24 Cezary Kaliszyk Working on stating induct.
2010-03-24 Christian Urban some tuning; possible fix for strange paper generation
2010-03-24 Christian Urban more on the paper
2010-03-24 Cezary Kaliszyk merge
2010-03-24 Cezary Kaliszyk Showed support of Core Haskell
2010-03-24 Cezary Kaliszyk Support proof modification for Core Haskell.
2010-03-24 Cezary Kaliszyk Experiments with Core Haskell support.
2010-03-24 Cezary Kaliszyk Export all the cheats needed for Core Haskell.
2010-03-24 Cezary Kaliszyk Compute Fv for non-recursive bn functions calling other bn functions
2010-03-24 Cezary Kaliszyk Core Haskell experiments.
2010-03-24 Christian Urban tuned paper
2010-03-23 Christian Urban more of the paper
2010-03-23 Christian Urban merged
2010-03-23 Christian Urban more tuning in the paper
2010-03-23 Cezary Kaliszyk merge
2010-03-23 Cezary Kaliszyk Parsing bn functions that call other bn functions and transmitting this information to fv/alpha.
2010-03-23 Christian Urban merged
2010-03-23 Christian Urban more tuning
2010-03-23 Christian Urban tuned paper
2010-03-23 Christian Urban more on the paper
2010-03-23 Cezary Kaliszyk merge
2010-03-23 Cezary Kaliszyk Modification to Core Haskell to make it accepted with an empty binding function.
2010-03-23 Christian Urban merged
2010-03-23 Christian Urban tuned paper
2010-03-23 Cezary Kaliszyk Initial list unfoldings in Core Haskell.
2010-03-23 Cezary Kaliszyk compiles
2010-03-23 Cezary Kaliszyk More modification needed for compilation
2010-03-23 Cezary Kaliszyk Moved let properties from Term5 to ExLetRec.
2010-03-23 Cezary Kaliszyk Move Let properties to ExLet
2010-03-23 Cezary Kaliszyk Added missing file
2010-03-23 Cezary Kaliszyk More reorganization.
2010-03-23 Cezary Kaliszyk Move Leroy out of Test, rename accordingly.
2010-03-23 Cezary Kaliszyk Term1 is identical to Example 3
2010-03-23 Cezary Kaliszyk Move example3 out.
2010-03-23 Cezary Kaliszyk Move Ex1 and Ex2 out of Test
2010-03-23 Cezary Kaliszyk Move examples which create more permutations out
2010-03-23 Cezary Kaliszyk Move LamEx out of Test.
2010-03-23 Cezary Kaliszyk Move lambda examples to manual
2010-03-23 Cezary Kaliszyk Move manual examples to a subdirectory.
2010-03-23 Cezary Kaliszyk Removed compat tests.
2010-03-23 Cezary Kaliszyk merge
2010-03-23 Cezary Kaliszyk Move Non-respectful examples to NotRsp
2010-03-23 Christian Urban merged
2010-03-23 Christian Urban more on the paper
2010-03-23 Cezary Kaliszyk Move the comment to appropriate place.
2010-03-23 Cezary Kaliszyk Remove compose_eqvt
2010-03-22 Cezary Kaliszyk sym proof with compose.
2010-03-22 Cezary Kaliszyk Marked the place where a compose lemma applies.
2010-03-22 Cezary Kaliszyk merge
2010-03-22 Cezary Kaliszyk equivp_cheat can be removed for all one-permutation examples.
2010-03-22 Christian Urban merged
2010-03-22 Christian Urban more on the paper
2010-03-22 Christian Urban merged
2010-03-22 Christian Urban tuned paper
2010-03-22 Cezary Kaliszyk Got rid of alpha_bn_rsp_cheat.
2010-03-22 Cezary Kaliszyk alpha_bn_rsp_pre automatized.
2010-03-22 Cezary Kaliszyk merge
2010-03-22 Cezary Kaliszyk fv_rsp proved automatically.
2010-03-22 Christian Urban more on the paper
2010-03-22 Christian Urban merged
2010-03-22 Christian Urban tuned paper
2010-03-22 Christian Urban some tuning
2010-03-22 Cezary Kaliszyk Strong induction for Type Schemes.
2010-03-22 Cezary Kaliszyk Fixed missing colon.
2010-03-21 Christian Urban tuned paper
2010-03-20 Christian Urban merged
2010-03-20 Christian Urban proved at_set_avoiding2 which is needed for strong induction principles
2010-03-20 Christian Urban moved lemmas supp_perm_eq and exists_perm to Nominal2_Supp
2010-03-20 Cezary Kaliszyk Size experiments.
2010-03-20 Cezary Kaliszyk Use 'alpha_bn_refl' to get rid of one of the sorrys.
2010-03-20 Cezary Kaliszyk Build alpha-->alphabn implications
2010-03-20 Cezary Kaliszyk Prove reflp for all relations.
2010-03-20 Christian Urban started cleaning up and introduced 3 versions of ~~gen
2010-03-20 Christian Urban moved infinite_Un into mainstream Isabelle; moved permute_boolI/E lemmas
2010-03-19 Christian Urban more work on the paper
2010-03-19 Cezary Kaliszyk Described automatically created funs.
2010-03-19 Cezary Kaliszyk merge
2010-03-19 Cezary Kaliszyk Automatically derive support for datatypes with at-most one binding per constructor.
2010-03-19 Christian Urban picture
2010-03-19 Christian Urban merged
2010-03-19 Christian Urban polished
2010-03-19 Cezary Kaliszyk Update Test to use fset.
2010-03-19 Cezary Kaliszyk merge
2010-03-19 Cezary Kaliszyk Use fs typeclass in showing finite support + some cheat cleaning.
2010-03-19 Christian Urban merged
2010-03-19 Christian Urban more one the paper
2010-03-19 Cezary Kaliszyk Keep only one copy of infinite_Un.
2010-03-19 Cezary Kaliszyk Added a missing 'import'.
2010-03-19 Cezary Kaliszyk Showed the instance: fset::(at) fs
2010-03-19 Cezary Kaliszyk merge
2010-03-19 Cezary Kaliszyk Remove atom_decl from the parser.
2010-03-19 Cezary Kaliszyk TySch strong induction looks ok.
2010-03-19 Cezary Kaliszyk Working on TySch strong induction.
2010-03-19 Cezary Kaliszyk Something is wrong with the statement of strong induction for TySch, as the All case is trivial and Fun case unprovable...
2010-03-19 Christian Urban merged
2010-03-19 Christian Urban more tuning on the paper
2010-03-19 Cezary Kaliszyk The nominal infrastructure for fset. 'fs' missing, but not needed so far.
2010-03-19 Cezary Kaliszyk A few more theorems in FSet.
2010-03-18 Cezary Kaliszyk merge 2
2010-03-18 Cezary Kaliszyk merge 1
2010-03-18 Cezary Kaliszyk support of fset_to_set, support of fmap_atom.
2010-03-18 Christian Urban merged
2010-03-18 Christian Urban more tuning on the paper
2010-03-18 Christian Urban added item about size functions
2010-03-18 Cezary Kaliszyk merge
2010-03-18 Cezary Kaliszyk Reached strong_induction in fset-based TySch. Will not work until isabelle changes are pushed.
2010-03-18 Christian Urban tuned
2010-03-18 Christian Urban another little bit for the introduction
2010-03-18 Cezary Kaliszyk Leroy96 supp=fv and fixes to make it compile
2010-03-18 Christian Urban merged
2010-03-18 Christian Urban more of the introduction
2010-03-18 Cezary Kaliszyk merge
2010-03-18 Cezary Kaliszyk Added a cleaned version of FSet.
2010-03-18 Christian Urban corrected the strong induction principle in the lambda-calculus case; gave a second (oartial) version that is more elegant
2010-03-18 Cezary Kaliszyk Continued description of alpha.
2010-03-18 Cezary Kaliszyk Rename "_property" to ".property"
2010-03-18 Cezary Kaliszyk First part of the description of alpha_ty.
2010-03-18 Cezary Kaliszyk Description of generation of alpha_bn.
2010-03-18 Cezary Kaliszyk case names also for _induct
2010-03-18 Cezary Kaliszyk Case_Names for _inducts. Does not work for _induct yet.
2010-03-18 Cezary Kaliszyk Added fv,bn,distinct,perm to the simplifier.
2010-03-18 Cezary Kaliszyk merge
2010-03-18 Cezary Kaliszyk Simplified the description.
2010-03-18 Christian Urban merged
2010-03-18 Christian Urban slightly more in the paper
2010-03-18 Cezary Kaliszyk Update the description of the generation of fv function.
2010-03-18 Cezary Kaliszyk fv_bn may need to call other fv_bns.
2010-03-18 Cezary Kaliszyk Update TODO.
2010-03-18 Cezary Kaliszyk Which proofs need a 'sorry'.
2010-03-18 Christian Urban added TODO
2010-03-18 Christian Urban vixed variable names
2010-03-18 Christian Urban simplified strong induction proof by using flip
2010-03-18 Cezary Kaliszyk Rename bound variables + minor cleaning.
2010-03-18 Cezary Kaliszyk Move most of the exporting out of the parser.
2010-03-18 Cezary Kaliszyk Prove pseudo-inject (eq-iff) on the exported level and rename appropriately.
2010-03-18 Cezary Kaliszyk Prove eqvts on exported terms.
2010-03-18 Cezary Kaliszyk Clean 'Lift', start working only on exported things in Parser.
2010-03-17 Christian Urban slightly more of the paper
2010-03-17 Christian Urban merged
2010-03-17 Christian Urban paper uses now a heap file - does not compile so long anymore
2010-03-17 Cezary Kaliszyk merge
2010-03-17 Cezary Kaliszyk compose_sym2 works also for term5
2010-03-17 Cezary Kaliszyk Updated Term1, including statement of strong induction.
2010-03-17 Cezary Kaliszyk Proper compose_sym2
2010-03-17 Christian Urban merged
2010-03-17 Christian Urban temporarily disabled tests in Nominal/ROOT
2010-03-17 Christian Urban made paper to compile
2010-03-17 Christian Urban added partial proof for the strong induction principle
2010-03-17 Cezary Kaliszyk Trying to find a compose lemma for 2 arguments.
2010-03-17 Cezary Kaliszyk merge
2010-03-17 Cezary Kaliszyk cheat_alpha_eqvt no longer needed. Cleaned the tracing messages.
2010-03-17 Christian Urban merged
2010-03-17 Christian Urban added proof of supp/fv for type schemes
2010-03-17 Cezary Kaliszyk Updated Type Schemes to automatic lifting. One goal is not true because of the restriction.
2010-03-17 Cezary Kaliszyk Remove Term5a, since it is now identical to Term5.
2010-03-17 Cezary Kaliszyk merge
2010-03-17 Cezary Kaliszyk Finished all proofs in Term5 and Term5n.
2010-03-17 Christian Urban added partial proof of supp for type schemes
2010-03-17 Cezary Kaliszyk Fix in alpha; support of the recursive Let works :)
2010-03-17 Cezary Kaliszyk The recursive supp just has one equation too much.
2010-03-17 Cezary Kaliszyk Fix for the change of alpha_gen.
2010-03-17 Cezary Kaliszyk merge
2010-03-17 Cezary Kaliszyk Generate compound FV and Alpha for recursive bindings.
2010-03-17 Cezary Kaliszyk Lifting theorems with compound fv and compound alpha.
2010-03-17 Christian Urban commented out examples that should not work; but for example type-scheme example should work
2010-03-17 Christian Urban added another supp-proof for the non-recursive case
2010-03-16 Cezary Kaliszyk Revert 7c8cd6eae8e2, now all proofs in Term5 go through, both recursive and not.
2010-03-16 Cezary Kaliszyk merge
2010-03-16 Cezary Kaliszyk The old recursive alpha works fine.
2010-03-16 Christian Urban added the final unfolded result
2010-03-16 Christian Urban merge and proof of support for non-recursive case
2010-03-16 Cezary Kaliszyk Added Term5 non-recursive. The bug is there only for the recursive case.
2010-03-16 Cezary Kaliszyk Alpha is wrong.
2010-03-16 Cezary Kaliszyk alpha_bn doesn't need the permutation in non-recursive case.
2010-03-16 Cezary Kaliszyk alpha5_transp and equivp
2010-03-16 Cezary Kaliszyk alpha5_symp proved.
2010-03-16 Cezary Kaliszyk FV_bn generated for recursive functions as well, and used in main fv for bindings.
2010-03-16 Cezary Kaliszyk The proof in 'Test' gets simpler.
2010-03-16 Cezary Kaliszyk Removed pi o bn = bn' assumption in alpha
2010-03-15 Christian Urban merged (confirmed to work with Isabelle from 6th March)
2010-03-15 Christian Urban another synchronisation
2010-03-15 Christian Urban proof for support when bn-function is present, but fb_function is empty
2010-03-15 Cezary Kaliszyk fv_eqvt_cheat no longer needed.
2010-03-15 Cezary Kaliszyk derive "inducts" from "induct" instead of lifting again is much faster.
2010-03-15 Cezary Kaliszyk build_eqvts works with recursive case if proper induction rule is used.
2010-03-15 Cezary Kaliszyk cheat_alpha_eqvt no longer needed; the proofs work.
2010-03-15 Cezary Kaliszyk LF works with new alpha...?
2010-03-15 Cezary Kaliszyk explicit flag "cheat_equivp"
2010-03-15 Cezary Kaliszyk Prove alpha_gen_compose_eqvt
2010-03-15 Cezary Kaliszyk Use eqvt.
2010-03-15 Christian Urban added preliminary test version....but Test works now
2010-03-15 Christian Urban added an eqvt-proof for bi
2010-03-15 Christian Urban synchronised with main hg-repository; used add_typedef_global in nominal_atoms
2010-03-14 Christian Urban localised the typedef in Attic (requires new Isabelle)
2010-03-13 Christian Urban started supp-fv proofs (is going to work)
2010-03-12 Cezary Kaliszyk Even with pattern simplified to a single clause, the supp equation doesn't seem true.
2010-03-12 Cezary Kaliszyk Still don't know how to prove supp=fv for simplest Let...
2010-03-11 Cezary Kaliszyk Do not fail if the finite support proof fails.
2010-03-11 Christian Urban generalised the supp for atoms to all concrete atoms (not just names)
2010-03-11 Christian Urban support of atoms at the end of Abs.thy
2010-03-11 Cezary Kaliszyk Trying to prove atom_image_fresh_swap
2010-03-11 Cezary Kaliszyk Finite_support proof no longer needed in LF.
2010-03-11 Cezary Kaliszyk Show that the new types are in finite support typeclass.
2010-03-11 Cezary Kaliszyk mk_supports_eq and supports_tac.
2010-03-11 Cezary Kaliszyk merge
2010-03-11 Cezary Kaliszyk Fixes for term1 for new alpha. Still not able to show support equations.
2010-03-11 Christian Urban merged
2010-03-11 Christian Urban finally the proof that new and old alpha agree
2010-03-11 Cezary Kaliszyk Remove "_raw" from lifted theorems.
2010-03-11 Cezary Kaliszyk looking at trm5_equivp
2010-03-11 Cezary Kaliszyk The cheats described explicitely.
2010-03-11 Cezary Kaliszyk The alpha5_eqvt tactic works if I manage to build the goal.
2010-03-11 Cezary Kaliszyk With the 4 cheats, all examples fully lift.
2010-03-11 Cezary Kaliszyk Lift alpha_bn_constants.
2010-03-11 Cezary Kaliszyk Lifting constants.
2010-03-11 Cezary Kaliszyk Proper error message.
2010-03-11 Cezary Kaliszyk Lifting constants works for all examples.
2010-03-11 Cezary Kaliszyk Remove tracing from fv/alpha.
2010-03-11 Cezary Kaliszyk Equivp working only on the standard alpha-equivalences.
2010-03-11 Cezary Kaliszyk explicit cheat_fv_eqvt
2010-03-11 Cezary Kaliszyk extract build_eqvts_tac.
2010-03-11 Cezary Kaliszyk build_eqvts no longer requires permutations.
2010-03-11 Cezary Kaliszyk Add explicit alpha_eqvt_cheat.
2010-03-11 Cezary Kaliszyk Export tactic out of alpha_eqvt.
2010-03-10 Cezary Kaliszyk merge
2010-03-10 Cezary Kaliszyk More tries about the proofs in trm5
2010-03-10 Christian Urban merged
2010-03-10 Christian Urban almost done with showing the equivalence between old and new alpha-equivalence (one subgoal remaining)
2010-03-10 Cezary Kaliszyk alpha_equivp for trm5
2010-03-10 Cezary Kaliszyk Undoing mistakenly committed parser experiments.
2010-03-10 Cezary Kaliszyk alpha_eqvt for recursive term1.
2010-03-10 Cezary Kaliszyk Looking at alpha_eqvt for term5, not much progress.
2010-03-10 Cezary Kaliszyk Reordered examples in Test.
2010-03-10 Cezary Kaliszyk Allows multiple bindings with same lhs.
2010-03-10 Cezary Kaliszyk Linked parser to fv and alpha.
2010-03-10 Cezary Kaliszyk merge
2010-03-10 Cezary Kaliszyk A minor fix for shallow binders. LF works again.
2010-03-10 Christian Urban merged
2010-03-10 Christian Urban parser produces ordered bn-fun information
2010-03-10 Cezary Kaliszyk Testing equalities in trm5, all seems good.
2010-03-10 Cezary Kaliszyk Fv&Alpha seem to work.
2010-03-10 Cezary Kaliszyk include alpha in the definitions.
2010-03-10 Cezary Kaliszyk Filled the algorithm for alpha_bn_arg
2010-03-10 Cezary Kaliszyk rhs of alpha_bn, and template for the arguments.
2010-03-10 Cezary Kaliszyk alpha_bn_constr template
2010-03-10 Cezary Kaliszyk exported template for alpha_bn
2010-03-10 Cezary Kaliszyk merge
2010-03-10 Cezary Kaliszyk Use alpha_bns in normal alpha defs.
2010-03-10 Cezary Kaliszyk alpha_bn_frees
2010-03-09 Christian Urban merged
2010-03-09 Christian Urban added bn-information, but it is not yet ordered according to the dts
2010-03-09 Cezary Kaliszyk Separate lists for separate constructors, to match bn_eqs.
2010-03-09 Cezary Kaliszyk All examples should work.
2010-03-09 Cezary Kaliszyk Fix to get old alpha.
2010-03-09 Cezary Kaliszyk Separate primrecs in Fv.
2010-03-09 Cezary Kaliszyk A version of Fv that takes into account recursive and non-recursive bindings.
2010-03-09 Cezary Kaliszyk Trying to prove that old alpha is the same as new recursive one. Lets still to do.
2010-03-09 Cezary Kaliszyk fv_bi and alpha_bi
2010-03-09 Christian Urban merged
2010-03-09 Christian Urban added first test about new compat
2010-03-09 Cezary Kaliszyk fv_compat
2010-03-09 Christian Urban added another compat example
2010-03-08 Christian Urban added a test-file for compatibility
2010-03-08 Christian Urban added compat definitions to some examples
2010-03-08 Cezary Kaliszyk Proper recognition of atoms and atom sets.
2010-03-08 Christian Urban deleted comments about "weird"
2010-03-08 Christian Urban merged
2010-03-08 Christian Urban updated to new Isabelle
2010-03-08 Cezary Kaliszyk Term5 written as nominal_datatype is the recursive let.
2010-03-08 Cezary Kaliszyk With restricted_nominal=1, exp7 and exp8 work. Not sure about proving bn_rsp there.
2010-03-08 Cezary Kaliszyk More fine-grained nominal restriction for debugging.
2010-03-08 Cezary Kaliszyk Fix permutation addition.
2010-03-08 Cezary Kaliszyk Update the comments
2010-03-08 Cezary Kaliszyk Gather bindings with same binder, and generate only one permutation for them.
2010-03-08 Cezary Kaliszyk Undo effects of simp.
2010-03-07 Christian Urban merged
2010-03-07 Christian Urban updated to renamings in Isabelle
2010-03-04 Christian Urban merged
2010-03-04 Christian Urban merged
2010-03-04 Christian Urban more proofs in Abs and work on Core Haskell
2010-03-03 Christian Urban added a lemma that permutations can be represented as sums of swapping
2010-03-05 Cezary Kaliszyk Still unable to show supp=fv for let with one existential.
2010-03-05 Cezary Kaliszyk Ported LF to the parser interface.
2010-03-05 Cezary Kaliszyk merge
2010-03-05 Cezary Kaliszyk Lift fv and bn eqvts; no need to lift alpha_eqvt.
2010-03-05 Cezary Kaliszyk Not much progress about the single existential let case.
2010-03-05 Cezary Kaliszyk Fixed LF for one quantifier over 2 premises.
2010-03-05 Cezary Kaliszyk Trying to fix the proofs for the single existential... So far failed.
2010-03-04 Cezary Kaliszyk Lift distinct.
2010-03-04 Cezary Kaliszyk Added lifting of pseudo-injectivity, commented out the code again and enabled the weird examples.
2010-03-04 Cezary Kaliszyk Lift BV,FV,Permutations and injection :).
2010-03-04 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 Cezary Kaliszyk A version that just leaves the supp/\supp goal. Obviously not true.
2010-03-04 Cezary Kaliszyk Prove symp and transp of weird without the supp /\ supp = {} assumption.
2010-03-03 Cezary Kaliszyk merge
2010-03-03 Cezary Kaliszyk Experiments with proving weird transp
2010-03-03 Cezary Kaliszyk Code for solving symp goals with multiple existentials.
2010-03-03 Cezary Kaliszyk reflp for multiple quantifiers.
2010-03-03 Christian Urban fixed mess in Test.thy
2010-03-03 Cezary Kaliszyk Fix eqvt for multiple quantifiers.
2010-03-03 Christian Urban only tuned
2010-03-03 Christian Urban merged
2010-03-03 Christian Urban start of paper - does not compile yet
2010-03-03 Christian Urban added ACM style file for ICFP
2010-03-03 Cezary Kaliszyk weird eqvt
2010-03-03 Cezary Kaliszyk Add the supp intersection conditions.
2010-03-02 Cezary Kaliszyk Comment out the part that does not work with 2 quantifiers.
2010-03-02 Cezary Kaliszyk Fixes for the fv problem and alpha problem.
2010-03-02 Christian Urban merged
2010-03-02 Christian Urban preliinary test about alpha-weirdo
2010-03-02 Christian Urban Another problem with permutations in alpha and possibly also in fv
2010-03-02 Christian Urban potential problem with the phd-example, where two permutations are generated, but only one is used
2010-03-02 Cezary Kaliszyk Some tests around Term4. Not sure how to fix the generated fv function.
2010-03-02 Cezary Kaliszyk merge
2010-03-02 Cezary Kaliszyk Porting from Lift to Parser; until defining the Quotient type.
2010-03-02 Cezary Kaliszyk Add image_eqvt and atom_eqvt to eqvt bases.
2010-03-02 Cezary Kaliszyk Include the raw eqvt lemmas.
2010-03-02 Christian Urban merged
2010-03-02 Christian Urban added some more examples from Peter Sewell's bestiary
2010-03-02 Cezary Kaliszyk merge
2010-03-02 Cezary Kaliszyk Minor
2010-03-02 Cezary Kaliszyk Working bv_eqvt
2010-03-02 Cezary Kaliszyk Moving wrappers out of Lift.
2010-03-02 Christian Urban merged
2010-03-02 Christian Urban added distinctness of perms
2010-03-02 Christian Urban updated (added lemma about commuting permutations)
2010-03-02 Cezary Kaliszyk Change type schemes to name set.
2010-03-02 Cezary Kaliszyk More fixes for new alpha, the whole lift script should now work again.
2010-03-02 Cezary Kaliszyk Length fix for nested recursions.
2010-03-02 Cezary Kaliszyk Fix equivp.
2010-03-02 Cezary Kaliszyk Fixed eqvt code.
2010-03-02 Christian Urban most tests work - the ones that do not I commented out
2010-03-02 Cezary Kaliszyk merge
2010-03-02 Cezary Kaliszyk Add a check of fv_functions.
2010-03-02 Christian Urban some tuning
2010-03-02 Cezary Kaliszyk Link calls to Raw permutations, FV definition and alpha_definition into the parser.
2010-03-02 Christian Urban merged
2010-03-02 Christian Urban rawified the bind specs (ready to be used now)
2010-03-01 Cezary Kaliszyk merge
2010-03-01 Cezary Kaliszyk Trying to prove equivariance.
2010-03-01 Christian Urban modified for new binding format - hope it is the intended one
2010-03-01 Christian Urban further code-refactoring in the parser
2010-03-01 Cezary Kaliszyk The new alpha-equivalence and testing in Trm2 and Trm5.
2010-03-01 Christian Urban slight simplification of the raw-decl generation
2010-03-01 Cezary Kaliszyk Example that shows that current alpha is wrong.
2010-03-01 Christian Urban added example from my phd
2010-02-27 Christian Urban streamlined parser
2010-02-26 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 Cezary Kaliszyk More about the general lifting procedure.
2010-02-26 Cezary Kaliszyk Update TODO
2010-02-26 Cezary Kaliszyk Progress with general lifting procedure.
2010-02-26 Cezary Kaliszyk RSP of perms can be shown in one go.
2010-02-26 Cezary Kaliszyk Change in signature of prove_const_rsp for general lifting.
2010-02-26 Cezary Kaliszyk Permutation and FV_Alpha interface change.
2010-02-26 Cezary Kaliszyk To call quotient it is enough to export the alpha frees to proper constants and their respective equivp theorems.
2010-02-25 Cezary Kaliszyk merge
2010-02-25 Cezary Kaliszyk Preparing the generalized lifting procedure
2010-02-25 Christian Urban merged
2010-02-25 Christian Urban added ott-example about Leroy96
2010-02-25 Cezary Kaliszyk Forgot to add one file.
2010-02-25 Cezary Kaliszyk Split Terms into separate files and add them to tests.
2010-02-25 Cezary Kaliszyk merge
2010-02-25 Cezary Kaliszyk Move the eqvt code out of Terms and fixed induction for single-rule examples.
2010-02-25 Christian Urban merged
2010-02-25 Christian Urban a few simplifications
2010-02-25 Christian Urban first attempt to make sense out of the core-haskell definition
2010-02-25 Cezary Kaliszyk Code for proving eqvt, still in Terms.
2010-02-25 Cezary Kaliszyk Use eqvt infrastructure.
2010-02-25 Cezary Kaliszyk Simple function eqvt code.
2010-02-25 Christian Urban added IsaMakefile...but so far included only a test for the parser
2010-02-25 Christian Urban moved Quot package to Attic (still compiles there with "isabelle make")
2010-02-25 Christian Urban merged
2010-02-25 Christian Urban moved Nominal to "toplevel"
2010-02-25 Cezary Kaliszyk Export perm_frees.
2010-02-24 Cezary Kaliszyk Restructuring the code in Perm
2010-02-24 Cezary Kaliszyk Simplified and finised eqvt proofs for t1 and t5
2010-02-24 Cezary Kaliszyk merge
2010-02-24 Cezary Kaliszyk Define lifted perms.
2010-02-24 Christian Urban merged
2010-02-24 Christian Urban parsing and definition of raw datatype and bv-function work (not very beautiful)
2010-02-24 Cezary Kaliszyk With permute_rsp we can lift the instance proofs :).
2010-02-24 Cezary Kaliszyk Note the instance proofs, since they can be easily lifted.
2010-02-24 Cezary Kaliszyk More refactoring and removed references to the global simpset in Perm.
2010-02-24 Cezary Kaliszyk Factor-out 'prove_perm_empty'; I plan to use it in defining permutations on the lifted type.
2010-02-24 Cezary Kaliszyk Regularize finite support proof for trm1
2010-02-24 Cezary Kaliszyk Made the fv-supp proof much more straightforward.
2010-02-24 Cezary Kaliszyk Regularize the proofs about finite support.
2010-02-24 Cezary Kaliszyk Respects of permute and constructors.
2010-02-24 Cezary Kaliszyk Generate fv_rsp automatically.
2010-02-24 Cezary Kaliszyk Define the constants automatically.
2010-02-24 Cezary Kaliszyk Rename also the lifted types to non-capital.
2010-02-24 Cezary Kaliszyk Use the infrastructure in LF. Much shorter :).
2010-02-24 Cezary Kaliszyk Final synchronization of names.
2010-02-24 Cezary Kaliszyk LF renaming part 3 (proper names of alpha equvalences)
2010-02-24 Cezary Kaliszyk LF renaming part 2 (proper fv functions)
2010-02-24 Cezary Kaliszyk merge
2010-02-24 Cezary Kaliszyk LF renaming part1.
2010-02-24 Christian Urban merged
2010-02-24 Christian Urban parsing of function definitions almost works now; still an error with undefined constants
2010-02-23 Cezary Kaliszyk merge
2010-02-23 Cezary Kaliszyk rsp for bv; the only issue is that it requires an appropriate induction principle.
2010-02-23 Christian Urban merged
2010-02-23 Christian Urban declarartion of the raw datatype already works; raw binding functions throw an exception about mutual recursive types
2010-02-23 Cezary Kaliszyk rsp infrastructure.
2010-02-23 Cezary Kaliszyk merge
2010-02-23 Cezary Kaliszyk Progress towards automatic rsp of constants and fv.
2010-02-23 Christian Urban merged
2010-02-23 Christian Urban "raw"-ified the term-constructors and types given in the specification
2010-02-23 Cezary Kaliszyk Looking at proving the rsp rules automatically.
2010-02-23 Cezary Kaliszyk Minor beutification.
2010-02-23 Cezary Kaliszyk Define the quotient from ML
2010-02-23 Cezary Kaliszyk All works in LF but will require renaming.
2010-02-23 Cezary Kaliszyk Reordering in LF.
2010-02-23 Cezary Kaliszyk Fixes for auxiliary datatypes.
2010-02-22 Cezary Kaliszyk Fixed pseudo_injectivity for trm4
2010-02-22 Cezary Kaliszyk Testing auto equivp code.
2010-02-22 Cezary Kaliszyk A tactic for final equivp
2010-02-22 Cezary Kaliszyk More equivp infrastructure.
2010-02-22 Cezary Kaliszyk tactify transp
2010-02-22 Cezary Kaliszyk export the reflp and symp tacs.
2010-02-22 Cezary Kaliszyk Generalize atom_trans and atom_sym.
2010-02-22 Cezary Kaliszyk Some progress about transp
2010-02-22 Cezary Kaliszyk alpha-symmetric addons.
2010-02-22 Cezary Kaliszyk alpha reflexivity
2010-02-22 Cezary Kaliszyk Renaming.
2010-02-22 Cezary Kaliszyk Added missing description.
2010-02-22 Cezary Kaliszyk Added Brian's suggestion.
2010-02-22 Cezary Kaliszyk Update TODO
2010-02-21 Cezary Kaliszyk Removed bindings 'in itself' where possible.
2010-02-20 Cezary Kaliszyk Some adaptation
2010-02-19 Cezary Kaliszyk proof cleaning and standardizing.
2010-02-19 Cezary Kaliszyk Automatic production and proving of pseudo-injectivity.
2010-02-19 Cezary Kaliszyk Experiments for the pseudo-injectivity tactic.
2010-02-19 Cezary Kaliszyk merge
2010-02-19 Cezary Kaliszyk Constructing alpha_inj goal.
2010-02-18 Christian Urban merged
2010-02-18 Christian Urban start work with the parser
2010-02-18 Cezary Kaliszyk Full alpha equivalence + testing in terms. Some differ but it seems the generated version is more correct.
2010-02-18 Cezary Kaliszyk First (non-working) version of alpha-equivalence
2010-02-18 Cezary Kaliszyk Description of the fv procedure.
2010-02-18 Cezary Kaliszyk Testing auto constant lifting.
2010-02-18 Cezary Kaliszyk Fix for new Isabelle (primrec)
2010-02-18 Cezary Kaliszyk Automatic lifting of constants.
2010-02-18 Cezary Kaliszyk Changed back to original version of trm5
2010-02-18 Cezary Kaliszyk The alternate version of trm5 with additional binding. All proofs work the same.
2010-02-18 Cezary Kaliszyk Code for handling atom sets.
2010-02-18 Cezary Kaliszyk Replace Terms by Terms2.
2010-02-18 Cezary Kaliszyk Fixed proofs in Terms2 and found a mistake in Terms.
2010-02-17 Cezary Kaliszyk Terms2 with bindings for binders synchronized with bindings they are used in.
2010-02-17 Cezary Kaliszyk Cleaning of proofs in Terms.
2010-02-17 Cezary Kaliszyk Testing Fv
2010-02-17 Cezary Kaliszyk Fix the strong induction principle.
2010-02-17 Cezary Kaliszyk Reorder
2010-02-17 Cezary Kaliszyk Add bindings of recursive types by free_variables.
2010-02-17 Cezary Kaliszyk Bindings adapted to multiple defined datatypes.
2010-02-17 Cezary Kaliszyk Reorganization
2010-02-17 Cezary Kaliszyk Now should work.
2010-02-17 Cezary Kaliszyk Some optimizations and fixes.
2010-02-17 Cezary Kaliszyk Simplified format of bindings.
2010-02-17 Cezary Kaliszyk Tested the Perm code; works everywhere in Terms.
2010-02-17 Cezary Kaliszyk Wrapped the permutation code.
2010-02-17 Cezary Kaliszyk Description of intended bindings.
2010-02-17 Cezary Kaliszyk Code for generating the fv function, no bindings yet.
2010-02-17 Cezary Kaliszyk merge
2010-02-17 Cezary Kaliszyk indent
2010-02-17 Cezary Kaliszyk merge
2010-02-17 Cezary Kaliszyk Simplifying perm_eq
2010-02-16 Cezary Kaliszyk merge
2010-02-16 Cezary Kaliszyk indenting
2010-02-16 Cezary Kaliszyk Minor
2010-02-16 Cezary Kaliszyk Merge
2010-02-16 Cezary Kaliszyk Ported Stefan's permutation code, still needs some localizing.
2010-02-15 Cezary Kaliszyk merge
2010-02-15 Cezary Kaliszyk Removed varifyT.
2010-02-15 Christian Urban merged
2010-02-15 Christian Urban 2-spaces rule (where it makes sense)
2010-02-15 Cezary Kaliszyk merge
2010-02-15 Cezary Kaliszyk Fixed the definition of less and finished the missing proof.
2010-02-15 Christian Urban further tuning
2010-02-15 Christian Urban small tuning
2010-02-15 Christian Urban tuned the parsing and testing code in quotient_def.ML; cleaned out old stuff in AbsRepTest.thy
2010-02-15 Cezary Kaliszyk der_bname -> derived_bname
2010-02-15 Cezary Kaliszyk Names of files.
2010-02-15 Cezary Kaliszyk Finished introducing the binding.
2010-02-15 Cezary Kaliszyk Synchronize the commands.
2010-02-15 Cezary Kaliszyk Passing the binding to quotient_def
2010-02-15 Cezary Kaliszyk Added a binding to the parser.
2010-02-15 Cezary Kaliszyk Second inline
2010-02-15 Cezary Kaliszyk remove one-line wrapper.
2010-02-12 Cezary Kaliszyk Undid the read_terms change; now compiles.
2010-02-12 Cezary Kaliszyk merge
2010-02-12 Cezary Kaliszyk renamed 'as' to 'is' everywhere.
2010-02-12 Cezary Kaliszyk "is" defined as the keyword
2010-02-12 Christian Urban moved "strange" lemma to quotient_tacs; marked a number of lemmas as unused; tuned
2010-02-12 Cezary Kaliszyk The lattice instantiations are gone from Isabelle/Main, so
2010-02-11 Cezary Kaliszyk the lam/bla example.
2010-02-11 Cezary Kaliszyk Finished a working foo/bar.
2010-02-11 Cezary Kaliszyk fv_foo is not regular.
2010-02-11 Cezary Kaliszyk Testing foo/bar
2010-02-11 Cezary Kaliszyk Even when bv = fv it still doesn't lift.
2010-02-11 Cezary Kaliszyk Added the missing syntax file
2010-02-11 Cezary Kaliszyk Notation available locally
2010-02-11 Cezary Kaliszyk Main renaming + fixes for new Isabelle in IntEx2.
2010-02-11 Cezary Kaliszyk Merging QuotBase into QuotMain.
2010-02-10 Christian Urban removed dead code
2010-02-10 Christian Urban cleaned a bit
2010-02-10 Cezary Kaliszyk lowercase locale
2010-02-10 Cezary Kaliszyk hg-added the added file.
2010-02-10 Cezary Kaliszyk Changes from Makarius's code review + some noticed fixes.
2010-02-10 Cezary Kaliszyk example with a respectful bn function defined over the type itself
2010-02-10 Cezary Kaliszyk Finishe the renaming.
2010-02-10 Cezary Kaliszyk Another mistake found with OTT.
2010-02-10 Cezary Kaliszyk merge
2010-02-10 Cezary Kaliszyk Fixed rbv6, when translating to OTT.
2010-02-10 Cezary Kaliszyk Some cleaning of proofs.
2010-02-10 Christian Urban merged again
2010-02-10 Christian Urban merged
2010-02-10 Cezary Kaliszyk more minor space and bracket modifications.
2010-02-10 Cezary Kaliszyk More changes according to the standards.
2010-02-10 Cezary Kaliszyk A concrete example, with a proof that rbv is not regular and
2010-02-09 Christian Urban proper declaration of types and terms during parsing (removes the varifyT when storing data)
2010-02-09 Christian Urban merged
2010-02-09 Christian Urban slight correction
2010-02-09 Cezary Kaliszyk merge
2010-02-09 Cezary Kaliszyk More about trm6
2010-02-09 Christian Urban merged
2010-02-09 Cezary Kaliszyk the specifications of the respects.
2010-02-09 Cezary Kaliszyk trm6 with the 'Foo' constructor.
2010-02-09 Cezary Kaliszyk removing unnecessary brackets
2010-02-09 Cezary Kaliszyk More indentation cleaning.
2010-02-09 Cezary Kaliszyk 'exc' -> 'exn' and more name and space cleaning.
2010-02-09 Cezary Kaliszyk Fully qualified exception names.
2010-02-09 Cezary Kaliszyk merge
2010-02-09 Cezary Kaliszyk More indentation, names and todo cleaning in the quotient package
2010-02-09 Christian Urban merged
2010-02-09 Christian Urban a few more attempts to show the equivalence between old and new way of defining alpha-equivalence
2010-02-09 Christian Urban minor tuning
2010-02-09 Cezary Kaliszyk Explicitly marked what is bound.
2010-02-09 Cezary Kaliszyk Cleaning and updating in Terms.
2010-02-09 Cezary Kaliszyk Looking at the trm2 example
2010-02-09 Cezary Kaliszyk Fixed pattern matching, now the test in Abs works correctly.
2010-02-08 Christian Urban added a test case
2010-02-08 Christian Urban merged
2010-02-08 Christian Urban moved some lemmas to Nominal; updated all files
2010-02-08 Cezary Kaliszyk merge
2010-02-08 Cezary Kaliszyk Comments.
2010-02-08 Christian Urban slightly tuned
2010-02-08 Cezary Kaliszyk Proper context fixes lifting inside instantiations.
2010-02-08 Cezary Kaliszyk Fixed the context import/export and simplified LFex.
2010-02-08 Christian Urban added 2 papers about core haskell
2010-02-07 Christian Urban fixed lemma name
2010-02-07 Christian Urban updated to latest Nominal2
2010-02-06 Christian Urban minor
2010-02-06 Christian Urban some tuning
2010-02-05 Cezary Kaliszyk merge
2010-02-05 Cezary Kaliszyk merge
2010-02-05 Cezary Kaliszyk Fixes for Bex1 removal.
2010-02-05 Cezary Kaliszyk Cleaned Terms using [lifted] and found a workaround for the instantiation problem.
2010-02-05 Cezary Kaliszyk A procedure that properly instantiates the types too.
2010-02-05 Cezary Kaliszyk More code abstracted away
2010-02-05 Cezary Kaliszyk A bit more intelligent and cleaner code.
2010-02-05 Cezary Kaliszyk merge
2010-02-05 Cezary Kaliszyk A proper version of the attribute
2010-02-05 Christian Urban merged
2010-02-05 Christian Urban eqvts and eqvts_raw are separate thm-lists; otherwise permute_eqvt is problematic as it causes looks in eqvts
2010-02-04 Cezary Kaliszyk The automatic lifting translation function, still with dummy types,
2010-02-04 Cezary Kaliszyk Quotdata_dest needed for lifting theorem translation.
2010-02-04 Christian Urban fixed (permute_eqvt in eqvts makes this simpset always looping)
2010-02-04 Christian Urban rollback of the test
2010-02-04 Christian Urban linked versions - instead of copies
2010-02-04 Christian Urban merged
2010-02-04 Christian Urban restored the old behaviour of having an eqvts list; the transformed theorems are stored in eqvts_raw
2010-02-03 Cezary Kaliszyk More let-rec experiments
2010-02-03 Christian Urban proposal for an alpha equivalence
2010-02-03 Cezary Kaliszyk Lets different.
2010-02-03 Cezary Kaliszyk Simplified the proof.
2010-02-03 Christian Urban merged
2010-02-03 Christian Urban proved that bv for lists respects alpha for terms
2010-02-03 Cezary Kaliszyk Finished remains on the let proof.
2010-02-03 Cezary Kaliszyk merge
2010-02-03 Cezary Kaliszyk Lets are ok.
2010-02-03 Christian Urban merged
2010-02-03 Christian Urban added type-scheme example
2010-02-03 Cezary Kaliszyk merge
2010-02-03 Cezary Kaliszyk Definitions for trm5
2010-02-03 Christian Urban another adaptation for the eqvt-change
2010-02-03 Christian Urban merged
2010-02-03 Christian Urban fixed proofs that broke because of eqvt
2010-02-03 Cezary Kaliszyk Minor fix.
2010-02-03 Cezary Kaliszyk merge
2010-02-03 Cezary Kaliszyk alpha5 pseudo-injective
2010-02-03 Christian Urban fixed proofs in Abs.thy
2010-02-03 Christian Urban merged
2010-02-03 Christian Urban added a first eqvt_tac which pushes permutations inside terms
2010-02-03 Cezary Kaliszyk The alpha-equivalence relation for let-rec. Not sure if correct...
2010-02-03 Cezary Kaliszyk Starting with a let-rec example.
2010-02-03 Cezary Kaliszyk Minor
2010-02-03 Cezary Kaliszyk Some cleaning and eqvt proof
2010-02-03 Cezary Kaliszyk The trm1_support lemma explicitly and stated a strong induction principle.
2010-02-03 Cezary Kaliszyk More ingredients in Terms.
2010-02-02 Cezary Kaliszyk Finished the supp_fv proof; first proof that analyses the structure of 'Let' :)
2010-02-02 Cezary Kaliszyk More in Terms
2010-02-02 Cezary Kaliszyk First experiments in Terms.
2010-02-02 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 Cezary Kaliszyk Disambiguating the syntax.
2010-02-02 Cezary Kaliszyk Minor uncommited changes from LamEx2.
2010-02-02 Cezary Kaliszyk Some equivariance machinery that comes useful in LF.
2010-02-02 Cezary Kaliszyk Generalized the eqvt proof for single binders.
2010-02-02 Cezary Kaliszyk With induct instead of induct_tac, just one induction is sufficient.
2010-02-02 Cezary Kaliszyk General alpha_gen_trans for one-variable abstraction.
2010-02-02 Cezary Kaliszyk With unfolding Rep/Abs_eqvt no longer needed.
2010-02-02 Cezary Kaliszyk Lam2 finished apart from Rep_eqvt.
2010-02-01 Cezary Kaliszyk merge
2010-02-01 Cezary Kaliszyk All should be ok now.
2010-02-01 Christian Urban repaired according to changes in Abs.thy
2010-02-01 Christian Urban added a single-binder alpha equivalence; showed one half of the equivalence proof between general and single binder case
2010-02-01 Christian Urban cleaned
2010-02-01 Christian Urban updated from huffman
2010-02-01 Christian Urban updated from nominal-huffman
2010-02-01 Cezary Kaliszyk Fixed wrong rename.
2010-02-01 Cezary Kaliszyk merge
2010-02-01 Cezary Kaliszyk Lambda based on alpha_gen, under construction.
2010-02-01 Christian Urban updated from huffman - repo
2010-02-01 Christian Urban renamed Abst/abst to Abs/abs
2010-02-01 Christian Urban got rid of RAbst type - is now just pairs
2010-02-01 Cezary Kaliszyk Monotonicity of ~~gen, needed for using it in inductive definitions.
2010-02-01 Cezary Kaliszyk The current state of fv vs supp proofs in LF.
2010-02-01 Cezary Kaliszyk merge
2010-02-01 Cezary Kaliszyk More proofs in the LF example.
2010-02-01 Christian Urban merged
2010-02-01 Christian Urban slight tuning
2010-02-01 Christian Urban renamed function according to the name of the constant
2010-02-01 Christian Urban fixed problem with Bex1_rel renaming
2010-02-01 Cezary Kaliszyk Ported LF to the generic lambda and solved the simpler _supp cases.
2010-01-30 Christian Urban merged
2010-01-30 Christian Urban introduced a generic alpha (but not sure whether it is helpful)
2010-01-29 Cezary Kaliszyk More in the LF example in the new nominal way, all is clear until support.
2010-01-29 Cezary Kaliszyk Fixed the induction problem + some more proofs.
2010-01-29 Cezary Kaliszyk equivariance of rfv and alpha.
2010-01-29 Cezary Kaliszyk Added the experiments with fun and function.
2010-01-29 Christian Urban now also final step is proved - the supp of lambdas is now completely characterised
2010-01-28 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-28 Christian Urban improved the proof slightly by defining alpha as a function and completely characterised the equality between two abstractions
2010-01-28 Christian Urban merged
2010-01-28 Christian Urban general abstraction operator and complete characterisation of its support and freshness
2010-01-28 Cezary Kaliszyk Ported existing part of LF to new permutations and alphas.
2010-01-28 Christian Urban attempt of a general abstraction operator
2010-01-28 Christian Urban attempt to prove equivalence between alpha definitions
2010-01-28 Cezary Kaliszyk End of renaming.
2010-01-28 Cezary Kaliszyk Minor when looking at lam.distinct and lam.inject
2010-01-28 Cezary Kaliszyk Renamed Bexeq to Bex1_rel
2010-01-28 Cezary Kaliszyk Substracting bounds from free variables.
2010-01-28 Cezary Kaliszyk Improper interface for datatype and function packages and proper interface lateron.
2010-01-28 Christian Urban merged
2010-01-28 Christian Urban minor
2010-01-28 Christian Urban test about supp/freshness for lam (old proofs work in principle - for single binders)
2010-01-28 Cezary Kaliszyk Recommited the changes for nitpick
2010-01-27 Cezary Kaliszyk Correct types which fixes the printing.
2010-01-27 Cezary Kaliszyk fv for subterms
2010-01-27 Cezary Kaliszyk Fix the problem with later examples. Maybe need to go back to textual specifications.
2010-01-27 Cezary Kaliszyk Some processing of variables in constructors to get free variables.
2010-01-27 Cezary Kaliszyk Parsing of the input as terms and types, and passing them as such to the function package.
2010-01-27 Cezary Kaliszyk Undid the parsing, as it is not possible with thy->lthy interaction.
2010-01-27 Cezary Kaliszyk merge
2010-01-27 Cezary Kaliszyk Some cleaning of thy vs lthy vs context.
2010-01-27 Christian Urban merged
2010-01-27 Christian Urban tuned comment
2010-01-27 Christian Urban completely ported
2010-01-27 Cezary Kaliszyk Another string in the specification.
2010-01-27 Cezary Kaliszyk Variable takes a 'name'.
2010-01-27 Cezary Kaliszyk merge
2010-01-27 Cezary Kaliszyk When commenting discovered a missing case of Babs->Abs regularization.
2010-01-27 Christian Urban merged
2010-01-27 Christian Urban mostly ported Terms.thy to new Nominal
2010-01-27 Cezary Kaliszyk merge
2010-01-27 Cezary Kaliszyk Commenting regularize
2010-01-27 Christian Urban very rough example file for how nominal2 specification can be parsed
2010-01-27 Christian Urban reordered cases in regularize (will be merged into two cases)
2010-01-27 Christian Urban use of equiv_relation_chk in quotient_term
2010-01-27 Christian Urban some slight tuning
2010-01-27 Christian Urban added Terms to Nominal - Instantiation of two types does not work (ask Florian)
2010-01-27 Christian Urban added another example with indirect recursion over lists
2010-01-26 Christian Urban just moved obsolete material into Attic
2010-01-26 Christian Urban added an LamEx example together with the new nominal infrastructure
2010-01-26 Cezary Kaliszyk Bex1_Bexeq_regular.
2010-01-26 Cezary Kaliszyk Hom Theorem with exists unique
2010-01-26 Cezary Kaliszyk 2 cases for regularize with split, lemmas with split now lift.
2010-01-26 Cezary Kaliszyk Simpler statement that has the problem.
2010-01-26 Cezary Kaliszyk Found a term that does not regularize.
2010-01-26 Cezary Kaliszyk A triple is still ok.
2010-01-26 Cezary Kaliszyk Combined the simpsets in clean_tac and updated the comment. Now cleaning of splits does work.
2010-01-26 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 Cezary Kaliszyk Sigma cleaning works with split_prs (still manual proof).
2010-01-26 Christian Urban tuned
2010-01-26 Christian Urban merged
2010-01-26 Christian Urban cleaning of QuotProd; a little cleaning of QuotList
2010-01-26 Christian Urban added prs and rsp lemmas for Inl and Inr
2010-01-25 Christian Urban used split_option_all lemma
2010-01-25 Christian Urban used the internal Option.map instead of custom option_map
2010-01-26 Cezary Kaliszyk Generalized split_prs and split_rsp
2010-01-26 Cezary Kaliszyk All eq_reflections apart from the one of 'id_apply' can be removed.
2010-01-26 Cezary Kaliszyk continued
2010-01-26 Cezary Kaliszyk More eqreflection/equiv cleaning.
2010-01-26 Cezary Kaliszyk more eq_reflection & other cleaning.
2010-01-26 Cezary Kaliszyk Removing more eq_reflections.
2010-01-25 Christian Urban ids *cannot* be object equalities
2010-01-25 Christian Urban re-inserted lemma in QuotList
2010-01-25 Christian Urban added prs and rsp lemmas for Some and None
2010-01-25 Christian Urban tuned proofs (mainly in QuotProd)
2010-01-25 Christian Urban properly commented out the "unused lemmas section" and moved actually used lemmas elsewhere; added two minor items to the TODO list
2010-01-25 Christian Urban renamed QuotScript to QuotBase
2010-01-25 Christian Urban cleaned some theorems
2010-01-24 Christian Urban test with splits
2010-01-23 Cezary Kaliszyk The alpha equivalence relations for structures in 'Terms'
(0) -1000 -960 +960 +1000 tip