Nominal/Parser.thy
2010-05-03 Cezary Kaliszyk remove tracing
2010-05-03 Cezary Kaliszyk Fix Parser
2010-05-02 Christian Urban moved old parser and old fv back into their original places; isabelle make works again
2010-04-30 Cezary Kaliszyk NewParser with Parser functionality, but some cheats included since the order of datayupes is wrong.
2010-04-30 Cezary Kaliszyk Merged nominal_datatype into NewParser until eqvts
2010-04-30 Cezary Kaliszyk more parser/new parser synchronization.
2010-04-30 Cezary Kaliszyk Simplify old parser for integration
2010-04-25 Christian Urban tuned and made to compile
2010-04-24 Christian Urban merged
2010-04-21 Christian Urban merged
2010-04-20 Christian Urban renamed Ex1.thy to SingleLet.thy
2010-04-20 Cezary Kaliszyk Fix of comment
2010-04-19 Cezary Kaliszyk merge
2010-04-19 Cezary Kaliszyk Locations of files in Parser
2010-04-14 Cezary Kaliszyk Initial cleaning/reorganization in Fv.
2010-04-11 Christian Urban tuned
2010-04-04 Christian Urban separated general nominal theory into separate folder
2010-04-01 Cezary Kaliszyk Let with multiple bindings.
2010-03-27 Cezary Kaliszyk Lets finally abstract lists.
2010-03-27 Cezary Kaliszyk Automatically lift theorems and constants only using the new quotient types. Requires new Isabelle.
2010-03-27 Cezary Kaliszyk Get lifted types information from the quotient package.
2010-03-27 Cezary Kaliszyk Parsing of list-bn functions into components.
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 Fv/Alpha now takes into account Alpha_Type given from the parser.
2010-03-26 Cezary Kaliszyk Describe 'nominal_datatype2'.
2010-03-26 Cezary Kaliszyk Removed remaining cheats + some cleaning.
2010-03-26 Cezary Kaliszyk Removed another cheat and cleaned the code a bit.
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-24 Cezary Kaliszyk Export all the cheats needed for Core Haskell.
2010-03-23 Cezary Kaliszyk Parsing bn functions that call other bn functions and transmitting this information to fv/alpha.
2010-03-23 Cezary Kaliszyk Move examples which create more permutations out
2010-03-22 Cezary Kaliszyk equivp_cheat can be removed for all one-permutation examples.
2010-03-22 Cezary Kaliszyk Got rid of alpha_bn_rsp_cheat.
2010-03-22 Cezary Kaliszyk fv_rsp proved automatically.
2010-03-20 Cezary Kaliszyk Use 'alpha_bn_refl' to get rid of one of the sorrys.
2010-03-20 Cezary Kaliszyk Prove reflp for all relations.
2010-03-19 Cezary Kaliszyk Automatically derive support for datatypes with at-most one binding per constructor.
2010-03-19 Cezary Kaliszyk Use fs typeclass in showing finite support + some cheat cleaning.
2010-03-19 Cezary Kaliszyk Remove atom_decl from the parser.
2010-03-18 Cezary Kaliszyk Reached strong_induction in fset-based TySch. Will not work until isabelle changes are pushed.
2010-03-18 Cezary Kaliszyk Rename "_property" to ".property"
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 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 merged
2010-03-17 Christian Urban made paper to compile
2010-03-17 Cezary Kaliszyk cheat_alpha_eqvt no longer needed. Cleaned the tracing messages.
2010-03-17 Cezary Kaliszyk Lifting theorems with compound fv and compound alpha.
2010-03-16 Cezary Kaliszyk Revert 7c8cd6eae8e2, now all proofs in Term5 go through, both recursive and not.
2010-03-16 Cezary Kaliszyk FV_bn generated for recursive functions as well, and used in main fv for bindings.
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 cheat_alpha_eqvt no longer needed; the proofs work.
2010-03-15 Cezary Kaliszyk explicit flag "cheat_equivp"
2010-03-13 Christian Urban started supp-fv proofs (is going to work)
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 support of atoms at the end of Abs.thy
2010-03-11 Cezary Kaliszyk Show that the new types are in finite support typeclass.
2010-03-11 Cezary Kaliszyk Remove "_raw" from lifted theorems.
2010-03-11 Cezary Kaliszyk The cheats described explicitely.
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 Lifting constants works for all examples.
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 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 Undoing mistakenly committed parser experiments.
2010-03-10 Cezary Kaliszyk alpha_eqvt for recursive term1.
2010-03-10 Cezary Kaliszyk Linked parser to fv and alpha.
2010-03-10 Christian Urban parser produces ordered bn-fun information
2010-03-09 Christian Urban added bn-information, but it is not yet ordered according to the dts
2010-03-09 Cezary Kaliszyk A version of Fv that takes into account recursive and non-recursive bindings.
2010-03-08 Christian Urban merged
2010-03-08 Christian Urban updated to new Isabelle
2010-03-08 Cezary Kaliszyk More fine-grained nominal restriction for debugging.
2010-03-05 Cezary Kaliszyk Lift fv and bn eqvts; no need to lift alpha_eqvt.
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-03 Cezary Kaliszyk Fix eqvt for multiple quantifiers.
2010-03-03 Cezary Kaliszyk weird eqvt
2010-03-02 Cezary Kaliszyk Comment out the part that does not work with 2 quantifiers.
2010-03-02 Cezary Kaliszyk Porting from Lift to Parser; until defining the Quotient type.
2010-03-02 Cezary Kaliszyk Working bv_eqvt
2010-03-02 Cezary Kaliszyk Link calls to Raw permutations, FV definition and alpha_definition into the parser.
2010-03-02 Christian Urban rawified the bind specs (ready to be used now)
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 Christian Urban slight simplification of the raw-decl generation
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-25 Christian Urban a few simplifications
2010-02-25 Christian Urban added IsaMakefile...but so far included only a test for the parser
less more (0) tip