automatic proofs for equivariance of alphas

Finished proof in Lambda.thy

merged

attempt to manual prove eqvt for alpha

Lifting in Term4.

some tuning of eqvt-infrastructure

some tuning of proofs

typo

merged

half of the pair-abs-equivalence

More on Manual/Trm4

alpha4_equivp and constant lifting.

alpha4_eqvt and alpha4_reflp

fv_eqvt in term4

Updating in Term4.

merge

Prove insert_rsp2

merged

changed header

Minor paper fixes.

temporary fix for CoreHaskell

deleted offending [eqvt]-attribute in Abs; Lambda works again, but there is now a problem in CoreHaskell

merge

Fix the 'subscript' error.

merged

thmdecls can deal with lemmas like alpha_gen which contain pairs or tuples

merge

merge

Separate alpha_definition.

Fix spelling in theory header

Separate define_fv.

tuned and removed dead code

moved a couple of more functions to the library

added a library for basic nominal functions; separated nominal_eqvt file

merged

first working version of the automatic equivariance procedure

Initial cleaning/reorganization in Fv.

merged

preliminary tests

deleted test

merge

merge part: delete_rsp

merge part1: none_memb_nil

added header and more tuning

more tuning

tuned

Working FSet with additional lemmas.

Much more in FSet (currently non-working)

made everything to compile

merged

some small tunings (incompleted work in Lambda.thy)

moved equivariance of map into Nominal2_Eqvt file

early ott paper

Porting lemmas from Quotient package FSet to new FSet.

added alpha-caml paper

implemented in thmdecls the case where eqvt-lemmas are of the form _ ==> _

fixed bug in thmdecls with destructing Trueprop; some initial infrastructure for eqvt-theorems of the form _ ==> _

folded changes from the conference version

added TODO item about parser creating syntax for the wrong type

corrected imports header

tuned

a few tests

added eqvt rules that are more standard

used warning instead of tracing (does not seem to produce stable output)

added small ittems about equivaraince of alpha_gens and name of lam.perm

added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed

changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac

rewrite paragraph introducing equivariance, add citation to Pitts03

edit 'contributions' section so we do not just quote directly from the reviewer

renamed ExLam to Lambda and completed the proof of the strong ind principle; tuned paper

clarified comment about distinct lists in th efuture work section

tuned type-schemes example

updated (comment about weirdo example)

check whether the "weirdo" example from the binding bestiary works with shallow binders

properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper)

merged

some further changes

merged

change some wording in conclusion

remove extra word

merged

added new paper directory for further work

use qualified name as string in concrete atom example

merged

simplify instance proof

polish explanation of additive group syntax

final version of the pearl paper

my final version of the paper

added an induction principle for permutations; removed add_perm construction

isarfied proof about existence of a permutation list

added reference to E. Gunter's work

typos in paper

separated general nominal theory into separate folder

added README and moved examples into separate directory

merged pearl paper with this repository; started litrature subdirectory

submitted version (just in time ;o)

first complete version (slightly less than 3h more to go)

tuned

tuned strong ind section

polished infrastruct section

completed lifting section

more on the lifting section

more on the strong induction section

completed conclusion

merged

merged

updated related work section

fv_fv_bn

Update fv_bn definition for bindings allowed in types for which bn is present.

fv_perm_bn

Minor formula fixes.

fixed alpha_bn

current state

merged

added alpha_bn definition

hfill for right aligning single table cells.

Cleaning the strong induction example.

minor

Fighting with space in displaying strong induction...

starting strong induction

General paper minor fixes.

Forgot to save before commit.

Let with multiple bindings.

Fill the space below the figure.

last commit for now.

more on the conclusion

completed related work section

more on the paper

added an item about alpha-equivalence (the existential should be closer to the abstraction)

polished everything up to TODO

merged

added alpha-definition for ~~ty

permute_bn

abbreviations for \<otimes> and \<oplus>

merged

a test with let having multiple bodies

polished and removed tys from bn-functions.

merge

More on paper

started to polish alpha-equivalence section, but needs more work

started with a related work section

polished and added an example for fvars

cleaned up the section about fv's

tuned beginning of section 4

More on section 5.

More on section 5.

merged

removed "raw" distinction

More on Section 5

Beginning of section 5.

merged

Avoid mentioning other nominal datatypes as it makes things too complicated.

merged

close the missing parenthesis on both sides.

merged

changes to section 2

Clean alpha

clean fv_bn

alpha_bn

Change @{text} to @{term}

alpha

more

fv and fv_bn

more of the paper

merged

Updated strong induction to modified definitions.

Initial renaming

small changes in the core-haskell spec

Update according to paper

merge

merge

Changed to Lists.

clarified core-haskell example

spell check

merge

Abs_gen and Abs_let simplifications.

more on the paper

fixed a problem due to a change in type-def (needs new Isabelle)

merged

more on the paper

got rid of the aux-function on the raw level, by defining it with function on the quotient level

Lets finally abstract lists.

Core Haskell can now use proper strings.

Automatically lift theorems and constants only using the new quotient types. Requires new Isabelle.

Remove list_eq notation.

Get lifted types information from the quotient package.

Equivariance when bn functions are lists.

Accepts lists in FV.

Parsing of list-bn functions into components.

Automatically compute support if only one type of Abs is present in the type.

Manually proved TySch support; All properties of TySch now true.

Generalize Abs_eq_iff.

Minor fix.

New compose lemmas. Reverted alpha_gen sym/trans changes. Equivp for alpha_res should work now.

Initial proof modifications for alpha_res

merge

Fv/Alpha now takes into account Alpha_Type given from the parser.

Minor cleaning.

merged

more on the paper

Removed some warnings.

merge

Modified abs_gen_sym and abs_gen_trans so it becomes usable in the proofs.

merged

more on the paper

simplification

merge

Describe 'nominal_datatype2'.

Fixed renamings.

merged

Removed remaining cheats + some cleaning.

Extract PS7 and PS8 from Test. PS7 needs the same fix as Core Haskell.

Update cheats in TODO.

Removed another cheat and cleaned the code a bit.

Fix Manual/LamEx for experiments.

Proper bn_rsp, for bn functions calling each other.

Gathering things to prove by induction together; removed cheat_bn_eqvt.

Update TODO

Showed ACons_subst.

Only ACons_subst left to show.

Solved all boring subgoals, and looking at properly defning permute_bv

One more copy-and-paste in core-haskell.

Properly defined permute_bn. No more sorry's in Let strong induction.

Showed Let substitution.

Only let substitution is left.

further in the proof

trying to prove the string induction for let.

added experiemental permute_bn

first attempt of strong induction for lets with assignments

more on the paper

more on the paper

Further in the strong induction proof.

Solved one of the strong-induction goals.

avoiding for atom.

Started proving strong induction.

stating the strong induction; further.

Working on stating induct.

some tuning; possible fix for strange paper generation

more on the paper

merge

Showed support of Core Haskell

Support proof modification for Core Haskell.

Experiments with Core Haskell support.

Export all the cheats needed for Core Haskell.

Compute Fv for non-recursive bn functions calling other bn functions

Core Haskell experiments.

tuned paper

more of the paper

merged

more tuning in the paper

merge

Parsing bn functions that call other bn functions and transmitting this information to fv/alpha.

merged

more tuning

tuned paper

more on the paper

merge

Modification to Core Haskell to make it accepted with an empty binding function.

merged

tuned paper

Initial list unfoldings in Core Haskell.

compiles

More modification needed for compilation

Moved let properties from Term5 to ExLetRec.

Move Let properties to ExLet

Added missing file

More reorganization.

Move Leroy out of Test, rename accordingly.

Term1 is identical to Example 3

Move example3 out.

Move Ex1 and Ex2 out of Test

Move examples which create more permutations out

Move LamEx out of Test.

Move lambda examples to manual

Move manual examples to a subdirectory.

Removed compat tests.

merge

Move Non-respectful examples to NotRsp

merged

more on the paper

Move the comment to appropriate place.

Remove compose_eqvt

sym proof with compose.

Marked the place where a compose lemma applies.

merge

equivp_cheat can be removed for all one-permutation examples.

merged

more on the paper

merged

tuned paper

Got rid of alpha_bn_rsp_cheat.

alpha_bn_rsp_pre automatized.

merge

fv_rsp proved automatically.

more on the paper

merged

tuned paper

some tuning

Strong induction for Type Schemes.

Fixed missing colon.

tuned paper

merged

proved at_set_avoiding2 which is needed for strong induction principles

moved lemmas supp_perm_eq and exists_perm to Nominal2_Supp

Size experiments.

Use 'alpha_bn_refl' to get rid of one of the sorrys.

Build alpha-->alphabn implications

Prove reflp for all relations.

started cleaning up and introduced 3 versions of ~~gen

moved infinite_Un into mainstream Isabelle; moved permute_boolI/E lemmas

more work on the paper

Described automatically created funs.

merge

Automatically derive support for datatypes with at-most one binding per constructor.

picture

merged

polished

Update Test to use fset.

merge

Use fs typeclass in showing finite support + some cheat cleaning.

merged

more one the paper

Keep only one copy of infinite_Un.

Added a missing 'import'.

Showed the instance: fset::(at) fs

merge

Remove atom_decl from the parser.

TySch strong induction looks ok.

Working on TySch strong induction.

Something is wrong with the statement of strong induction for TySch, as the All case is trivial and Fun case unprovable...

merged

more tuning on the paper

The nominal infrastructure for fset. 'fs' missing, but not needed so far.

A few more theorems in FSet.

merge 2

merge 1

support of fset_to_set, support of fmap_atom.

merged

more tuning on the paper

added item about size functions

merge

Reached strong_induction in fset-based TySch. Will not work until isabelle changes are pushed.

tuned

another little bit for the introduction

Leroy96 supp=fv and fixes to make it compile

merged

more of the introduction

merge

Added a cleaned version of FSet.

corrected the strong induction principle in the lambda-calculus case; gave a second (oartial) version that is more elegant

Continued description of alpha.

Rename "_property" to ".property"

First part of the description of alpha_ty.

Description of generation of alpha_bn.

case names also for _induct

Case_Names for _inducts. Does not work for _induct yet.

Added fv,bn,distinct,perm to the simplifier.

merge

Simplified the description.

merged

slightly more in the paper

Update the description of the generation of fv function.

fv_bn may need to call other fv_bns.

Update TODO.

Which proofs need a 'sorry'.

added TODO

vixed variable names

simplified strong induction proof by using flip

Rename bound variables + minor cleaning.

Move most of the exporting out of the parser.

Prove pseudo-inject (eq-iff) on the exported level and rename appropriately.

Prove eqvts on exported terms.

Clean 'Lift', start working only on exported things in Parser.

slightly more of the paper

merged

paper uses now a heap file - does not compile so long anymore

merge

compose_sym2 works also for term5

Updated Term1, including statement of strong induction.

Proper compose_sym2

merged

temporarily disabled tests in Nominal/ROOT

made paper to compile

added partial proof for the strong induction principle

Trying to find a compose lemma for 2 arguments.

merge

cheat_alpha_eqvt no longer needed. Cleaned the tracing messages.

merged

added proof of supp/fv for type schemes

Updated Type Schemes to automatic lifting. One goal is not true because of the restriction.

Remove Term5a, since it is now identical to Term5.

merge

Finished all proofs in Term5 and Term5n.

added partial proof of supp for type schemes

Fix in alpha; support of the recursive Let works :)

The recursive supp just has one equation too much.

Fix for the change of alpha_gen.

merge

Generate compound FV and Alpha for recursive bindings.

Lifting theorems with compound fv and compound alpha.

commented out examples that should not work; but for example type-scheme example should work

added another supp-proof for the non-recursive case

Revert 7c8cd6eae8e2, now all proofs in Term5 go through, both recursive and not.

merge

The old recursive alpha works fine.

added the final unfolded result

merge and proof of support for non-recursive case

Added Term5 non-recursive. The bug is there only for the recursive case.

Alpha is wrong.

alpha_bn doesn't need the permutation in non-recursive case.

alpha5_transp and equivp

alpha5_symp proved.

FV_bn generated for recursive functions as well, and used in main fv for bindings.

The proof in 'Test' gets simpler.

Removed pi o bn = bn' assumption in alpha

merged (confirmed to work with Isabelle from 6th March)

another synchronisation

proof for support when bn-function is present, but fb_function is empty

fv_eqvt_cheat no longer needed.

derive "inducts" from "induct" instead of lifting again is much faster.

build_eqvts works with recursive case if proper induction rule is used.

cheat_alpha_eqvt no longer needed; the proofs work.

LF works with new alpha...?

explicit flag "cheat_equivp"

Prove alpha_gen_compose_eqvt

Use eqvt.

added preliminary test version....but Test works now

added an eqvt-proof for bi

synchronised with main hg-repository; used add_typedef_global in nominal_atoms

localised the typedef in Attic (requires new Isabelle)

started supp-fv proofs (is going to work)

Even with pattern simplified to a single clause, the supp equation doesn't seem true.

Still don't know how to prove supp=fv for simplest Let...

Do not fail if the finite support proof fails.

generalised the supp for atoms to all concrete atoms (not just names)

support of atoms at the end of Abs.thy

Trying to prove atom_image_fresh_swap

Finite_support proof no longer needed in LF.

Show that the new types are in finite support typeclass.

mk_supports_eq and supports_tac.

merge

Fixes for term1 for new alpha. Still not able to show support equations.

merged

finally the proof that new and old alpha agree

Remove "_raw" from lifted theorems.

looking at trm5_equivp

The cheats described explicitely.

The alpha5_eqvt tactic works if I manage to build the goal.

With the 4 cheats, all examples fully lift.

Lift alpha_bn_constants.

Lifting constants.

Proper error message.

Lifting constants works for all examples.

Remove tracing from fv/alpha.

Equivp working only on the standard alpha-equivalences.

explicit cheat_fv_eqvt

extract build_eqvts_tac.

build_eqvts no longer requires permutations.

Add explicit alpha_eqvt_cheat.

Export tactic out of alpha_eqvt.

merge

More tries about the proofs in trm5

merged

almost done with showing the equivalence between old and new alpha-equivalence (one subgoal remaining)

alpha_equivp for trm5

Undoing mistakenly committed parser experiments.

alpha_eqvt for recursive term1.

Looking at alpha_eqvt for term5, not much progress.

Reordered examples in Test.

Allows multiple bindings with same lhs.

Linked parser to fv and alpha.

merge

A minor fix for shallow binders. LF works again.

merged

parser produces ordered bn-fun information

Testing equalities in trm5, all seems good.

Fv&Alpha seem to work.

include alpha in the definitions.

Filled the algorithm for alpha_bn_arg

rhs of alpha_bn, and template for the arguments.