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'
2010-01-23 Cezary Kaliszyk More experiments with defining the homomorphism directly, lifting of 'distinct' and of 'exhaust'.
2010-01-23 Cezary Kaliszyk Trying to define hom for the lifted type directly.
2010-01-22 Cezary Kaliszyk Proper alpha equivalence for Sigma calculus.
2010-01-21 Cezary Kaliszyk Changed fun_map and rel_map to definitions.
2010-01-21 Cezary Kaliszyk Lifted Peter's Sigma lemma with Ex1.
2010-01-21 Cezary Kaliszyk Automatic injection of Bexeq
2010-01-21 Cezary Kaliszyk Automatic cleaning of Bexeq<->Ex1 theorems.
2010-01-21 Cezary Kaliszyk Using Bexeq_rsp, and manually lifted lemma with Ex1.
2010-01-21 Cezary Kaliszyk Bexeq definition, Ex1_prs lemma, Bex1_rsp lemma, compiles.
2010-01-21 Cezary Kaliszyk The missing rule.
2010-01-21 Cezary Kaliszyk Ex1 -> Bex1 Regularization, Preparing Exeq.
2010-01-20 Cezary Kaliszyk Added the Sigma Calculus example
2010-01-20 Cezary Kaliszyk Better error messages for non matching quantifiers.
2010-01-20 Cezary Kaliszyk Statement of term1_hom_rsp
2010-01-20 Christian Urban proved that the function is a function
2010-01-20 Cezary Kaliszyk term1_hom as a function
2010-01-19 Cezary Kaliszyk A version of hom with quantifiers.
2010-01-17 Christian Urban added permutation functions for the raw calculi
2010-01-16 Christian Urban fixed broken (partial) proof
2010-01-16 Christian Urban used "new" alpha-equivalence relation (according to new scheme); proved equivalence theorems and so on
2010-01-16 Christian Urban liftin and lifing_tac can now lift several "and"-separated goals at once; the raw-theorems have to be given in the order of goals
2010-01-15 Christian Urban added a partial proof under which conditions rlam_rec Respects alpha...I guess something like this is true; this means the Hom lemmas need to have preconditions
2010-01-15 Christian Urban tried to witness the hom-lemma with the recursion combinator from rlam....does not work yet completely
2010-01-15 Christian Urban merged
2010-01-15 Christian Urban added free_variable function (do not know about the algorithm yet)
2010-01-15 Cezary Kaliszyk hom lifted to hom', so it is true. Infrastructure for partially regularized quantifiers. Nicer errors for regularize.
2010-01-15 Christian Urban slight tuning of relation_error
2010-01-15 Cezary Kaliszyk Appropriate respects and a statement of the lifted hom lemma
2010-01-15 Christian Urban recursion-hom for lambda
2010-01-15 Cezary Kaliszyk Incorrect version of the homomorphism lemma
2010-01-14 Christian Urban trivial
2010-01-14 Christian Urban tuned quotient_typ.ML
2010-01-14 Christian Urban tuned quotient_def.ML and cleaned somewhat LamEx.thy
2010-01-14 Christian Urban a few more lemmas...except supp of lambda-abstractions
2010-01-14 Christian Urban removed one sorry
2010-01-14 Christian Urban nearly all of the proof
2010-01-14 Christian Urban right generalisation
2010-01-14 Cezary Kaliszyk First subgoal.
2010-01-14 Christian Urban setup for strong induction
2010-01-14 Cezary Kaliszyk exported absrep_const for nitpick.
2010-01-14 Cezary Kaliszyk minor
2010-01-14 Cezary Kaliszyk Simplified matches_typ.
2010-01-14 Christian Urban added bound-variable functions to terms
2010-01-14 Christian Urban merged
2010-01-14 Christian Urban added 3 calculi with interesting binding structure
2010-01-14 Cezary Kaliszyk produce defs with lthy, like prs and ids
2010-01-14 Cezary Kaliszyk Remove SOLVED from quotient_tac. Move atomize_eqv to 'Unused'.
2010-01-14 Cezary Kaliszyk Finished organising an efficient datastructure for qconst_info.
2010-01-14 Cezary Kaliszyk Undid changes from symtab to termtab, since we need to lookup specialized types.
2010-01-13 Cezary Kaliszyk Moved the matches_typ function outside a?d simplified it.
2010-01-13 Christian Urban one more item in the list of Markus
2010-01-13 Cezary Kaliszyk Put relation_error as a separate function.
2010-01-13 Cezary Kaliszyk Better error message for definition failure.
2010-01-13 Cezary Kaliszyk merge
2010-01-13 Cezary Kaliszyk Stored Termtab for constant information.
2010-01-13 Christian Urban merged
2010-01-13 Christian Urban deleted SOLVED'
2010-01-13 Cezary Kaliszyk Removed the 'oops' in IntEx.
2010-01-13 Christian Urban tuned
2010-01-13 Christian Urban added SOLVED' which is now part of Isabelle....must be removed eventually
2010-01-13 Christian Urban merged
2010-01-12 Christian Urban tuned
2010-01-12 Christian Urban absrep_fun and equiv_relation do not produce anymore spurious maps; two problems arose in IntEx, which are marked with "INJECTION PROBLEM"
2010-01-12 Cezary Kaliszyk More indenting, bracket removing and comment restructuring.
2010-01-12 Cezary Kaliszyk Finished replacing OO by OOO
2010-01-12 Cezary Kaliszyk Change OO to OOO in FSet3.
2010-01-12 Cezary Kaliszyk minor comment editing
2010-01-12 Cezary Kaliszyk modifying comments/indentation in quotient_term.ml
2010-01-12 Cezary Kaliszyk Cleaning comments, indentation etc in quotient_tacs.
2010-01-12 Cezary Kaliszyk No more exception handling in rep_abs_rsp_tac
2010-01-12 Cezary Kaliszyk handle all is no longer necessary in lambda_prs.
2010-01-12 Cezary Kaliszyk removed 3 hacks.
2010-01-12 Cezary Kaliszyk Updated some comments.
2010-01-12 Cezary Kaliszyk merge
2010-01-12 Cezary Kaliszyk Removed exception handling from equals_rsp_tac.
2010-01-11 Christian Urban added an abbreviation for OOO
2010-01-11 Cezary Kaliszyk merge
2010-01-11 Cezary Kaliszyk Undid the non-working part.
2010-01-11 Christian Urban started to adhere to Wenzel-Standard
2010-01-11 Cezary Kaliszyk Changing exceptions to 'try', part 1.
2010-01-11 Cezary Kaliszyk removed quotdata_lookup_type
2010-01-11 Cezary Kaliszyk Fix for testing matching constants in regularize.
2010-01-11 Christian Urban tuned previous commit further
2010-01-10 Christian Urban the chk-functions in quotient_term also simplify the result according to the id_simps; had to remove id_def from this theorem list though; this caused in FSet3 that relied on this rule; the problem is marked with "ID PROBLEM"
2010-01-09 Christian Urban introduced separate match function
2010-01-09 Christian Urban removed obsolete equiv_relation and rnamed new_equiv_relation
2010-01-08 Cezary Kaliszyk New_relations, all works again including concat examples.
2010-01-08 Cezary Kaliszyk map and rel simps for all quotients; needed when changing the relations to aggregate ones.
2010-01-08 Cezary Kaliszyk id_simps needs to be taken out not used directly, otherwise the new lemmas are not there.
2010-01-08 Cezary Kaliszyk Experimients with fconcat_insert
2010-01-08 Cezary Kaliszyk Modifications for new_equiv_rel, part2
2010-01-08 Cezary Kaliszyk Modifictaions for new_relation.
2010-01-08 Cezary Kaliszyk Proved concat_empty.
2010-01-07 Cezary Kaliszyk Replacing equivp by reflp in the assumptions leads to non-provable subgoals in the gen_pre lemmas.
2010-01-07 Cezary Kaliszyk some cleaning.
2010-01-07 Cezary Kaliszyk First generalization.
2010-01-07 Cezary Kaliszyk The working proof of the special case.
2010-01-07 Cezary Kaliszyk Reduced the proof to two simple but not obvious to prove facts.
2010-01-07 Cezary Kaliszyk More cleaning and commenting AbsRepTest. Now tests work; just slow.
2010-01-07 Cezary Kaliszyk cleaning in AbsRepTest.
2010-01-06 Cezary Kaliszyk Further in the proof
2010-01-06 Cezary Kaliszyk Tried to prove the lemma manually; only left with quotient proofs.
2010-01-06 Cezary Kaliszyk Sledgehammer bug.
2010-01-05 Cezary Kaliszyk merge
2010-01-05 Cezary Kaliszyk Trying the proof
2010-01-05 Christian Urban merged
2010-01-05 Cezary Kaliszyk Struggling with composition
2010-01-05 Cezary Kaliszyk Trying to state composition quotient.
2010-01-05 Christian Urban proper handling of error messages (code copy - maybe this can be avoided)
2010-01-05 Christian Urban added a new version of equiv_relation (is not yet used anywhere except in AbsRepTest)
2010-01-05 Cezary Kaliszyk Readded 'regularize_to_injection' which I believe will be needed.
2010-01-02 Christian Urban added a warning to the quotient_type definition, if a map function is missing
2010-01-01 Christian Urban tuned
2010-01-01 Christian Urban a slight change to abs/rep generation
2010-01-01 Christian Urban tuned
2010-01-01 Christian Urban fixed comment errors
2010-01-01 Christian Urban some slight tuning
2009-12-31 Christian Urban renamed transfer to transform (Markus)
2009-12-30 cu some small changes
2009-12-27 Christian Urban added a functor that allows checking what is added to the theorem lists
2009-12-26 Christian Urban corrected wrong [quot_respect] attribute; tuned
2009-12-26 Christian Urban renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
2009-12-26 Christian Urban added an item about when the same quotient constant is defined twice (throws a bind exception in quoteint_def.ML)
2009-12-26 Christian Urban as expected problems occure when lifting concat lemmas
2009-12-26 Christian Urban tuned
2009-12-26 Christian Urban commeted the absrep function
2009-12-26 Christian Urban generalised absrep function; needs consolidation
2009-12-24 Christian Urban tuned
2009-12-24 Christian Urban added sanity checks for quotient_type
2009-12-24 Christian Urban made the quotient_type definition more like typedef; now type variables need to be explicitly given
2009-12-23 Christian Urban used Local_Theory.declaration for storing quotdata
2009-12-23 Christian Urban tuning
2009-12-23 Christian Urban renamed some fields in the info records
2009-12-23 Christian Urban modified mk_resp_arg so that the user can give terms as equivalence relations, not just constants
2009-12-23 Christian Urban cleaed a bit function mk_typedef_main
2009-12-23 Christian Urban renamed QUOT_TYPE to Quot_Type
2009-12-23 Christian Urban explicit handling of mem_def, avoiding the use of the simplifier; this fixes some quotient_type definitions
2009-12-23 Christian Urban corrected map declarations for Sum and Prod; moved absrep_fun examples in separate file
2009-12-22 Christian Urban added "Highest Priority" category; and tuned slightly code
2009-12-22 Christian Urban added a print_maps command; updated the keyword file accordingly
2009-12-22 Christian Urban renamed get_fun to absrep_fun; introduced explicit checked versions of the term functions
2009-12-22 Christian Urban tuned
2009-12-22 Christian Urban moved get_fun into quotient_term; this simplifies the overall including structure of the package
2009-12-22 Christian Urban tuned comments; renamed QUOT_TRUE to Quot_True; atomize_eqv seems to not be neccessary (has it been added to Isabelle)...it is now comented out and everything still works
2009-12-22 Christian Urban on the hunt for what condition raises which exception in the CLEVER CODE of calculate_inst
2009-12-22 Christian Urban simplified calculate_instance; worked around some clever code; clever code is unfortunately still there...needs to be removed
2009-12-21 Christian Urban used eq_reflection not with OF, but directly in @{thm ...}
2009-12-21 Christian Urban cleaned a bit calculate_inst a bit; eta-contraction seems to be not necessary? (all examples go through)
2009-12-21 Christian Urban get_fun needed change to cope with "('a fset) fset" types...this needs composition (op o); now id_simps contains also id_o and o_id, and map_id is also added in QuotList.thy; regularize and cleaning needed to be hacked (indicated by "HACK")...THIS NEEDS ATTENTION!!!; except two lemmas in IntEx, all examples go through; added considerable material to FSet3; tuned FIXME-TODO
2009-12-19 Christian Urban on suggestion of Tobias renamed "quotient_def" to "quotient_definition"; needs new keyword file
2009-12-19 Christian Urban renamed "quotient" command to "quotient_type"; needs new keyword file to be installed
2009-12-19 Christian Urban this file is now obsolete; replaced by isar-keywords-quot.el
2009-12-19 Christian Urban with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place
2009-12-19 Christian Urban added a very old paper about Quotients in Isabelle (related work)
2009-12-19 Christian Urban avoided global "open"s - replaced by local "open"s
2009-12-19 Christian Urban small tuning
2009-12-19 Christian Urban various tunings; map_lookup now raises an exception; addition to FIXME-TODO
2009-12-17 Christian Urban minor cleaning
2009-12-17 Christian Urban moved the QuotMain code into two ML-files
2009-12-16 Christian Urban complete fix for IsaMakefile
2009-12-16 Christian Urban first fix
2009-12-16 Christian Urban merged
2009-12-16 Christian Urban added a paper for possible notes
2009-12-16 Cezary Kaliszyk Removed lambdas on the right hand side. This fixes all 'PROBLEM' comments.
2009-12-15 Cezary Kaliszyk lambda_prs & solve_quotient_assum cleaned.
2009-12-15 Christian Urban some commenting
2009-12-14 Cezary Kaliszyk Fixed previous commit.
2009-12-14 Cezary Kaliszyk merge
2009-12-14 Cezary Kaliszyk Moved DETERM inside Repeat & added SOLVE around quotient_tac.
2009-12-14 Cezary Kaliszyk merge.
2009-12-14 Cezary Kaliszyk FIXME/TODO.
2009-12-14 Cezary Kaliszyk reply to question in code
2009-12-14 Cezary Kaliszyk Reply in code.
2009-12-14 Cezary Kaliszyk Replies to questions from the weekend: Uncommenting the renamed theorem commented out in 734.
2009-12-13 Christian Urban a few code annotations
2009-12-13 Christian Urban another pass on apply_rsp
2009-12-13 Christian Urban managed to simplify apply_rsp
2009-12-12 Christian Urban tried to simplify apply_rsp_tac; failed at the moment; added some questions
2009-12-12 Christian Urban some trivial changes
2009-12-12 Christian Urban trivial cleaning of make_inst
2009-12-12 Christian Urban tried to improve test; but fails
2009-12-12 Christian Urban merged
2009-12-12 Christian Urban annotated some questions to the code; some simple changes
2009-12-12 Cezary Kaliszyk Answering the question in code.
2009-12-12 Christian Urban merged
2009-12-12 Christian Urban trivial
2009-12-12 Christian Urban tuned code
2009-12-12 Cezary Kaliszyk Minor
2009-12-12 Cezary Kaliszyk Some proofs.
2009-12-12 Cezary Kaliszyk Proof of finite_set_storng_cases_raw.
2009-12-12 Cezary Kaliszyk A bracket was missing; with it proved the 'definitely false' lemma.
2009-12-12 Christian Urban renamed quotient.ML to quotient_typ.ML
2009-12-11 Christian Urban merged
2009-12-11 Christian Urban tuned
2009-12-11 Christian Urban started to have a look at it; redefined the relation
2009-12-11 Cezary Kaliszyk More name and indentation cleaning.
2009-12-11 Cezary Kaliszyk Merge + Added LarryInt & Fset3 to tests.
2009-12-11 Cezary Kaliszyk Renaming
2009-12-11 Christian Urban merged
2009-12-11 Christian Urban deleted struct_match by Pattern.match (fixes a problem in LarryInt)
2009-12-11 Cezary Kaliszyk FSet3 minor fixes + cases
2009-12-11 Christian Urban added Int example from Larry
2009-12-11 Cezary Kaliszyk Added FSet3 with a formalisation of finite sets based on Michael's one.
2009-12-11 Cezary Kaliszyk Updated TODO list together.
2009-12-11 Cezary Kaliszyk Merge
2009-12-11 Cezary Kaliszyk More theorem renaming.
2009-12-11 Cezary Kaliszyk Renamed theorems in IntEx2 to conform to names in Int.
2009-12-11 Cezary Kaliszyk Updated comments.
2009-12-11 Christian Urban merged
2009-12-11 Christian Urban tuned
2009-12-11 Christian Urban renamed Larrys example
2009-12-11 Cezary Kaliszyk New syntax for definitions.
2009-12-11 Christian Urban changed error message
2009-12-11 Christian Urban reformulated the lemma lifting_procedure as ML value; gave better warning message for injection case
2009-12-10 Christian Urban slightly tuned
2009-12-10 Christian Urban merged
2009-12-10 Christian Urban added Larry's theory; introduced lemma equivpI; added something to the TODO about error messages
2009-12-10 Christian Urban added maps-printout and tuned some comments
2009-12-10 Cezary Kaliszyk Option and Sum quotients.
2009-12-10 Cezary Kaliszyk Regularized the hard lemma.
2009-12-10 Cezary Kaliszyk Simplification of Babses for regularize; will probably become injection
2009-12-10 Cezary Kaliszyk Found the problem with ttt3.
2009-12-10 Cezary Kaliszyk minor
2009-12-10 Cezary Kaliszyk Moved Unused part of locale to Unused QuotMain.
2009-12-10 Cezary Kaliszyk Moved 'int_induct' to IntEx to keep IntEx2 being just theory of integers in order.
2009-12-10 Cezary Kaliszyk Removed 'Presburger' as it introduces int & other minor cleaning in Int2.
2009-12-10 Christian Urban more tuning
2009-12-10 Christian Urban tuned
2009-12-10 Christian Urban simplified the instantiation of QUOT_TRUE in procedure_tac
2009-12-10 Christian Urban completed previous commit
2009-12-10 Christian Urban deleted DT/NDT diagnostic code
2009-12-10 Christian Urban moved the interpretation code into Unused.thy
2009-12-10 Christian Urban added an attempt to get a finite set theory
2009-12-10 Christian Urban removed memb and used standard mem (member from List.thy)
2009-12-10 Christian Urban merged
(0) -1000 -960 +960 +1000 tip