Nominal/Parser.thy
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.
less more (0) -60 tip