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
(0) -1000 -240 +240 +1000 tip