Mercurial
Mercurial
>
hg
>
nominal2
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
help
less
more
|
(0)
-480
+480
+1000
tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or
revset expression
.
The revision graph only works with JavaScript-enabled browsers.
Changing FOCUS to CSUBGOAL (part 1)
2009-12-04, by Cezary Kaliszyk
abs_rep as ==
2009-12-04, by Cezary Kaliszyk
Cleaning the Quotients file
2009-12-04, by Cezary Kaliszyk
Minor renames and moving
2009-12-04, by Cezary Kaliszyk
Cleaning/review of QuotScript.
2009-12-04, by Cezary Kaliszyk
More cleaning
2009-12-04, by Cezary Kaliszyk
more name cleaning and removing
2009-12-04, by Cezary Kaliszyk
More code cleaning and renaming: moved rsp and prs lemmas from Int to QuotList
2009-12-04, by Cezary Kaliszyk
Cleaning & Renaming coming from QuotList
2009-12-04, by Cezary Kaliszyk
Cleaning in Quotients
2009-12-04, by Cezary Kaliszyk
Even more name changes and cleaning
2009-12-04, by Cezary Kaliszyk
More code cleaning and name changes
2009-12-04, by Cezary Kaliszyk
merge
2009-12-04, by Cezary Kaliszyk
merged
2009-12-04, by Cezary Kaliszyk
smaller theory footprint
2009-12-04, by Christian Urban
merged
2009-12-04, by Christian Urban
merge
2009-12-04, by Christian Urban
smaller theory footprint
2009-12-04, by Christian Urban
More name changes
2009-12-04, by Cezary Kaliszyk
Naming changes
2009-12-04, by Cezary Kaliszyk
code cleaning and renaming
2009-12-04, by Cezary Kaliszyk
merge
2009-12-04, by Cezary Kaliszyk
Removed previous inj_repabs_tac
2009-12-04, by Cezary Kaliszyk
some tuning
2009-12-04, by Christian Urban
merge
2009-12-04, by Cezary Kaliszyk
rep_abs_rsp_tac to replace the last use of instantiate_tac with matching and unification.
2009-12-04, by Cezary Kaliszyk
merged
2009-12-04, by Christian Urban
merged
2009-12-04, by Christian Urban
Change equiv_trans2 to EQUALS_RSP, since we can prove it for any quotient type, not only for eqv relations.
2009-12-04, by Cezary Kaliszyk
compose_tac instead of rtac to avoid unification; some code cleaning.
2009-12-04, by Cezary Kaliszyk
Got to about 5 seconds for the longest proof. APPLY_RSP_TAC' solves the quotient internally without instantiation resulting in a faster proof.
2009-12-04, by Cezary Kaliszyk
Using APPLY_RSP1; again a little bit faster.
2009-12-04, by Cezary Kaliszyk
Fixes after big merge.
2009-12-04, by Cezary Kaliszyk
The big merge; probably non-functional.
2009-12-04, by Cezary Kaliszyk
Testing the new tactic everywhere
2009-12-04, by Cezary Kaliszyk
First version of the deterministic rep-abs-inj-tac.
2009-12-04, by Cezary Kaliszyk
Changing = to \<equiv> in case if we want to use simp.
2009-12-04, by Cezary Kaliszyk
Even better: Completely got rid of the simps in both quotient_tac and inj_repabs_tac
2009-12-04, by Cezary Kaliszyk
merge
2009-12-04, by Cezary Kaliszyk
Made your version work again with LIST_REL_EQ.
2009-12-04, by Cezary Kaliszyk
the error occurs in APPLY_RSP_TAC where the wrong quotient (for LIST_REL) is applied
2009-12-03, by Christian Urban
removed quot argument...not all examples work anymore
2009-12-03, by Christian Urban
merged
2009-12-03, by Christian Urban
merged
2009-12-03, by Christian Urban
first version of internalised quotient theorems; added FIXME-TODO
2009-12-03, by Christian Urban
further dead code
2009-12-03, by Christian Urban
Reintroduced varifyT; we still need it for permutation definition.
2009-12-03, by Cezary Kaliszyk
Updated the examples
2009-12-03, by Cezary Kaliszyk
Fixed previous mistake
2009-12-03, by Cezary Kaliszyk
defs used automatically by clean_tac
2009-12-03, by Cezary Kaliszyk
Added qoutient_consts dest for getting all the constant definitions in the cleaning step.
2009-12-03, by Cezary Kaliszyk
Added the definition to quotient constant data.
2009-12-03, by Cezary Kaliszyk
removing unused code
2009-12-03, by Cezary Kaliszyk
merged
2009-12-03, by Christian Urban
deleted some dead code
2009-12-03, by Christian Urban
Included all_prs and ex_prs in the lambda_prs conversion.
2009-12-03, by Cezary Kaliszyk
further simplification
2009-12-03, by Christian Urban
simplified lambda_prs_conv
2009-12-03, by Christian Urban
deleted now obsolete argument rty everywhere
2009-12-02, by Christian Urban
deleted tests at the beginning of QuotMain
2009-12-02, by Christian Urban
Experiments with OPTION_map
2009-12-02, by Cezary Kaliszyk
merge
2009-12-02, by Cezary Kaliszyk
More experiments with higher order quotients and theorems with non-lifted constants.
2009-12-02, by Cezary Kaliszyk
merged
2009-12-02, by Christian Urban
Lifting to 2 different types :)
2009-12-02, by Cezary Kaliszyk
New APPLY_RSP which finally does automatic partial lifting :). Doesn't support same relation yet.
2009-12-02, by Cezary Kaliszyk
Fixed unlam for non-abstractions and updated list_induct_part proof.
2009-12-02, by Cezary Kaliszyk
Removed the use of 'rty' from APPLY_RSP, finally LF proofs go automatically.
2009-12-02, by Cezary Kaliszyk
The conversion approach works.
2009-12-02, by Cezary Kaliszyk
Trying a conversion based approach.
2009-12-02, by Cezary Kaliszyk
A bit of progress; but the object-logic vs meta-logic distinction is troublesome.
2009-12-02, by Cezary Kaliszyk
Added tactic for dealing with QUOT_TRUE and introducing QUOT_TRUE.
2009-12-02, by Cezary Kaliszyk
back in working state
2009-12-01, by Cezary Kaliszyk
clean
2009-12-01, by Cezary Kaliszyk
fixed previous commit
2009-12-01, by Christian Urban
fixed problems with FOCUS
2009-12-01, by Christian Urban
added a make_inst test
2009-12-01, by Christian Urban
Transformation of QUOT_TRUE assumption by any given function
2009-12-01, by Cezary Kaliszyk
QUOT_TRUE joke
2009-12-01, by Christian Urban
Removed last HOL_ss
2009-12-01, by Cezary Kaliszyk
more cleaning
2009-12-01, by Cezary Kaliszyk
Cleaning 'aps'.
2009-12-01, by Cezary Kaliszyk
merge
2009-11-30, by Cezary Kaliszyk
cleaned inj_regabs_trm
2009-11-30, by Christian Urban
merge
2009-11-30, by Cezary Kaliszyk
clean_tac rewrites the definitions the other way
2009-11-30, by Cezary Kaliszyk
merged
2009-11-30, by Christian Urban
added facilities to get all stored quotient data (equiv thms etc)
2009-11-30, by Christian Urban
More code cleaning
2009-11-30, by Cezary Kaliszyk
Code cleaning.
2009-11-30, by Cezary Kaliszyk
Commented clean-tac
2009-11-30, by Cezary Kaliszyk
Added another induction to LFex
2009-11-30, by Cezary Kaliszyk
tried to improve the inj_repabs_trm function but left the new part commented out
2009-11-29, by Christian Urban
added a new version of QuotMain to experiment with qids
2009-11-29, by Christian Urban
started functions for qid-insertion and fixed a bug in regularise
2009-11-29, by Christian Urban
Removed unnecessary HOL_ss which proved one of the subgoals.
2009-11-29, by Cezary Kaliszyk
Added 'TRY' to refl in clean_tac to get as far as possible. Removed unnecessary [quot_rsp] in FSet. Added necessary [quot_rsp] and one lifted thm in LamEx.
2009-11-29, by Cezary Kaliszyk
introduced a global list of respectfulness lemmas; the attribute is [quot_rsp]
2009-11-29, by Christian Urban
tuned
2009-11-29, by Christian Urban
improved pattern matching inside the inj_repabs_tacs
2009-11-28, by Christian Urban
selective debugging of the inj_repabs_tac (at the moment for step 3 and 4 debugging information is printed)
2009-11-28, by Christian Urban
removed old inj_repabs_tac; kept only the one with (selective) debugging information
2009-11-28, by Christian Urban
renamed r_mk_comb_tac to inj_repabs_tac
2009-11-28, by Christian Urban
tuning
2009-11-28, by Christian Urban
tuned comments
2009-11-28, by Christian Urban
renamed LAMBDA_RES_TAC and WEAK_LAMBDA_RES_TAC to lower case names
2009-11-28, by Christian Urban
Manually finished LF induction.
2009-11-28, by Cezary Kaliszyk
Moved fast instantiation to QuotMain
2009-11-28, by Cezary Kaliszyk
LFex proof a bit further.
2009-11-28, by Cezary Kaliszyk
merge
2009-11-28, by Cezary Kaliszyk
Looking at repabs proof in LF.
2009-11-28, by Cezary Kaliszyk
further proper merge
2009-11-28, by Christian Urban
merged
2009-11-28, by Christian Urban
more simplification
2009-11-28, by Christian Urban
Merged and tested that all works.
2009-11-28, by Cezary Kaliszyk
Finished and tested the new regularize
2009-11-28, by Cezary Kaliszyk
more tuning of the repabs-tactics
2009-11-28, by Christian Urban
fixed examples in IntEx and FSet
2009-11-28, by Christian Urban
merged
2009-11-28, by Christian Urban
fixed previous commit
2009-11-28, by Christian Urban
Cleaned all lemmas about regularisation of Ball and Bex and moved in one place. Second Ball simprox.
2009-11-28, by Cezary Kaliszyk
Merged comment
2009-11-28, by Cezary Kaliszyk
Integrated Stefan's tactic and changed substs to simps with empty context.
2009-11-28, by Cezary Kaliszyk
some slight tuning of the apply-tactic
2009-11-28, by Christian Urban
annotated a proof with all steps and simplified LAMBDA_RES_TAC
2009-11-28, by Christian Urban
Merge
2009-11-27, by Cezary Kaliszyk
The magical code from Stefan, will need to be integrated in the Simproc.
2009-11-27, by Cezary Kaliszyk
replaced FIRST' (map rtac list) with resolve_tac list
2009-11-27, by Christian Urban
Simplifying arguments; got rid of trans2_thm.
2009-11-27, by Cezary Kaliszyk
Cleaning of LFex. Lambda_prs fails to unify in 2 places.
2009-11-27, by Cezary Kaliszyk
Recommit
2009-11-27, by Cezary Kaliszyk
Removing arguments of tactics: absrep, rel_refl, reps_same are computed.
2009-11-27, by Cezary Kaliszyk
More cleaning in QuotMain, identity handling.
2009-11-27, by Cezary Kaliszyk
Minor cleaning
2009-11-27, by Cezary Kaliszyk
tuned
2009-11-27, by Christian Urban
some tuning
2009-11-27, by Christian Urban
simplified gen_frees_tac and properly named abstracted variables
2009-11-27, by Christian Urban
removed CHANGED'
2009-11-27, by Christian Urban
introduced a separate lemma for id_simps
2009-11-27, by Christian Urban
renamed inj_REPABS to inj_repabs_trm
2009-11-27, by Christian Urban
tuned comments and moved slightly some code
2009-11-27, by Christian Urban
deleted obsolete qenv code
2009-11-27, by Christian Urban
renamed REGULARIZE to be regularize
2009-11-27, by Christian Urban
more tuning
2009-11-26, by Christian Urban
deleted get_fun_old and stuff
2009-11-26, by Christian Urban
recommited changes of comments
2009-11-26, by Christian Urban
Merge Again
2009-11-26, by Cezary Kaliszyk
Merged
2009-11-26, by Cezary Kaliszyk
tuned comments
2009-11-26, by Christian Urban
some diagnostic code for r_mk_comb
2009-11-26, by Christian Urban
introduced a new property for Ball and ===> on the left
2009-11-26, by Christian Urban
fixed QuotList
2009-11-26, by Christian Urban
changed left-res
2009-11-26, by Christian Urban
Manually regularized akind_aty_atrm.induct
2009-11-26, by Cezary Kaliszyk
Playing with Monos in LFex.
2009-11-26, by Cezary Kaliszyk
Fixed FSet after merge.
2009-11-26, by Cezary Kaliszyk
merged
2009-11-26, by Christian Urban
test with monos
2009-11-26, by Christian Urban
applic_prs
2009-11-25, by Cezary Kaliszyk
polishing
2009-11-25, by Christian Urban
reordered the code
2009-11-25, by Christian Urban
Moved exception handling to QuotMain and cleaned FSet.
2009-11-25, by Cezary Kaliszyk
Merge
2009-11-25, by Cezary Kaliszyk
Finished manual lifting of list_induct_part :)
2009-11-25, by Cezary Kaliszyk
comments tuning and slight reordering
2009-11-25, by Christian Urban
Merge
2009-11-25, by Cezary Kaliszyk
More moving from QuotMain to UnusedQuotMain
2009-11-25, by Cezary Kaliszyk
deleted some obsolete diagnostic code
2009-11-25, by Christian Urban
Removed unused things from QuotMain.
2009-11-25, by Cezary Kaliszyk
All examples work again.
2009-11-25, by Cezary Kaliszyk
cleaning in MyInt
2009-11-25, by Cezary Kaliszyk
lambda_prs and cleaning the existing examples.
2009-11-25, by Cezary Kaliszyk
merged
2009-11-25, by Christian Urban
fixed the problem with generalising variables; at the moment it is quite a hack
2009-11-25, by Christian Urban
Ho-matching failures...
2009-11-24, by Cezary Kaliszyk
changed unification to matching
2009-11-24, by Christian Urban
unification
2009-11-24, by Christian Urban
Lambda & SOLVED' for new quotient_tac
2009-11-24, by Cezary Kaliszyk
merged
2009-11-24, by Christian Urban
Conversion
2009-11-24, by Cezary Kaliszyk
The non-working procedure_tac.
2009-11-24, by Cezary Kaliszyk
merged
2009-11-24, by Christian Urban
use error instead of raising our own exception
2009-11-24, by Christian Urban
Fixes to the tactic after quotient_tac changed.
2009-11-24, by Cezary Kaliszyk
merged
2009-11-24, by Christian Urban
added a prepare_tac
2009-11-24, by Christian Urban
TRY' for clean_tac
2009-11-24, by Cezary Kaliszyk
Moved cleaning to QuotMain
2009-11-24, by Cezary Kaliszyk
New cleaning tactic
2009-11-24, by Cezary Kaliszyk
explicit phases for the cleaning
2009-11-24, by Christian Urban
Separate regularize_tac
2009-11-24, by Cezary Kaliszyk
Another theorem for which the new regularize differs from old one, so the goal is not proved. But it seems, that the new one is better.
2009-11-24, by Cezary Kaliszyk
More fixes for inj_REPABS
2009-11-24, by Cezary Kaliszyk
addded a tactic, which sets up the three goals of the `algorithm'
2009-11-24, by Christian Urban
fixed the error by a temporary fix (the data of the eqivalence relation should be only its name)
2009-11-23, by Christian Urban
merged
2009-11-23, by Christian Urban
tuned some comments
2009-11-23, by Christian Urban
Another not-typechecking regularized term.
2009-11-23, by Cezary Kaliszyk
domain_type in regularizing equality
2009-11-23, by Cezary Kaliszyk
More theorems lifted in the goal-directed way.
2009-11-23, by Cezary Kaliszyk
Finished temporary goal-directed lift_theorem wrapper.
2009-11-23, by Cezary Kaliszyk
merged
2009-11-23, by Christian Urban
a version of inj_REPABS (needs to be looked at again later)
2009-11-23, by Christian Urban
Fixes for atomize
2009-11-23, by Cezary Kaliszyk
merge
2009-11-23, by Cezary Kaliszyk
lift_thm with a goal.
2009-11-23, by Cezary Kaliszyk
slight change in code layout
2009-11-23, by Christian Urban
Fixes for new code
2009-11-23, by Cezary Kaliszyk
Removing dead code
2009-11-23, by Cezary Kaliszyk
Move atomize_goal to QuotMain
2009-11-23, by Cezary Kaliszyk
Removed second implementation of Regularize/Inject from FSet.
2009-11-23, by Cezary Kaliszyk
Moved new repabs_inj code to QuotMain
2009-11-23, by Cezary Kaliszyk
New repabs behaves the same way as old one.
2009-11-23, by Cezary Kaliszyk
code review with Cezary
2009-11-23, by Christian Urban
The other branch does not seem to work...
2009-11-23, by Cezary Kaliszyk
Fixes for recent changes.
2009-11-23, by Cezary Kaliszyk
updated to Isabelle 22nd November
2009-11-22, by Christian Urban
a little tuning of comments
2009-11-22, by Christian Urban
slight tuning
2009-11-21, by Christian Urban
some debugging code, but cannot find the place where the cprems_of exception is raised
2009-11-21, by Christian Urban
tried to prove the repabs_inj lemma, but failed for the moment
2009-11-21, by Christian Urban
my first version of repabs injection
2009-11-21, by Christian Urban
tuned
2009-11-21, by Christian Urban
tunded
2009-11-21, by Christian Urban
tuned
2009-11-21, by Christian Urban
flagged qenv-stuff as obsolete
2009-11-21, by Christian Urban
simplified get_fun so that it uses directly rty and qty, instead of qenv
2009-11-21, by Christian Urban
started regularize of rtrm/qtrm version; looks quite promising
2009-11-20, by Christian Urban
updated to new Isabelle
2009-11-19, by Christian Urban
fixed the storage of qconst definitions
2009-11-18, by Christian Urban
Still don't know how to do the proof automatically.
2009-11-13, by Cezary Kaliszyk
added some tracing information to all phases of lifting to the function lift_thm
2009-11-13, by Christian Urban
merge of the merge?
2009-11-12, by Cezary Kaliszyk
merged
2009-11-12, by Cezary Kaliszyk
added a FIXME commment
2009-11-12, by Christian Urban
looking up data in quot_info works now (needs qualified string)
2009-11-12, by Christian Urban
changed the quotdata to be a symtab table (needs fixing)
2009-11-12, by Christian Urban
added a container for quotient constants (does not work yet though)
2009-11-12, by Christian Urban
Lifting towards goal and manually finished the proof.
2009-11-11, by Cezary Kaliszyk
merge
2009-11-11, by Cezary Kaliszyk
Modifications while preparing the goal-directed version.
2009-11-11, by Cezary Kaliszyk
updated to new Theory_Data and to new Isabelle
2009-11-11, by Christian Urban
Removed 'Toplevel.program' for polyml 5.3
2009-11-11, by Cezary Kaliszyk
Atomizing a "goal" theorems.
2009-11-10, by Cezary Kaliszyk
More code cleaning and commenting
2009-11-10, by Cezary Kaliszyk
Minor cleaning and removing of some 'handle _'.
2009-11-09, by Cezary Kaliszyk
Cleaning and commenting
2009-11-09, by Cezary Kaliszyk
Fixes for the other get_fun implementation.
2009-11-09, by Cezary Kaliszyk
permutation lifting works now also
2009-11-06, by Christian Urban
merged
2009-11-06, by Christian Urban
updated to new Isabelle version and added a new example file
2009-11-06, by Christian Urban
Minor changes
2009-11-06, by Cezary Kaliszyk
merge
2009-11-06, by Cezary Kaliszyk
fold_rsp
2009-11-06, by Cezary Kaliszyk
tuned the code in quotient and quotient_def
2009-11-06, by Christian Urban
More functionality for lifting list.cases and list.recs.
2009-11-05, by Cezary Kaliszyk
merged
2009-11-05, by Christian Urban
removed typing information from get_fun in quotient_def; *potentially* dangerous
2009-11-05, by Christian Urban
Remaining fixes for polymorphic types. map_append now lifts properly with 'a list and 'b list.
2009-11-05, by Cezary Kaliszyk
removed Simplifier.context
2009-11-05, by Christian Urban
replaced check_term o parse_term by read_term
2009-11-05, by Christian Urban
merged
2009-11-05, by Christian Urban
Infrastructure for polymorphic types
2009-11-05, by Cezary Kaliszyk
Two new tests for get_fun. Second one fails.
2009-11-04, by Cezary Kaliszyk
Type instantiation in regularize
2009-11-04, by Cezary Kaliszyk
Description of regularize
2009-11-04, by Cezary Kaliszyk
Experiments with lifting partially applied constants.
2009-11-04, by Cezary Kaliszyk
more tuning
2009-11-04, by Christian Urban
slightly tuned
2009-11-04, by Christian Urban
merged
2009-11-04, by Christian Urban
separated the quotient_def into a separate file
2009-11-04, by Christian Urban
Experiments in Int
2009-11-04, by Cezary Kaliszyk
fixed definition of PLUS
2009-11-04, by Christian Urban
simplified the quotient_def code
2009-11-04, by Christian Urban
Lifting 'fold1.simps(2)' and some cleaning.
2009-11-04, by Cezary Kaliszyk
Playing with alpha_refl.
2009-11-03, by Cezary Kaliszyk
Alpha.induct now lifts automatically.
2009-11-03, by Cezary Kaliszyk
merge
2009-11-03, by Cezary Kaliszyk
applic_prs
2009-11-03, by Cezary Kaliszyk
simplified the quotient_def code; type of the defined constant must now be given; for-part eliminated
2009-11-03, by Christian Urban
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
2009-11-03, by Cezary Kaliszyk
merge
2009-11-03, by Cezary Kaliszyk
Preparing infrastructure for general FORALL_PRS
2009-11-03, by Cezary Kaliszyk
split quotient.ML into two files
2009-11-02, by Christian Urban
slightly saner way of parsing the quotient_def
2009-11-02, by Christian Urban
merged
2009-11-02, by Christian Urban
changed Type.typ_match to Sign.typ_match
2009-11-02, by Christian Urban
Fixes after optimization and preparing for a general FORALL_PRS
2009-11-02, by Cezary Kaliszyk
Optimization
2009-11-02, by Cezary Kaliszyk
Map does not fully work yet.
2009-11-02, by Cezary Kaliszyk
Fixed quotdata_lookup.
2009-11-02, by Cezary Kaliszyk
fixed problem with maps_update
2009-11-02, by Christian Urban
merged
2009-11-02, by Christian Urban
fixed the problem with types in map
2009-11-02, by Christian Urban
Automatic computation of application preservation and manually finished "alpha.induct". Slow...
2009-10-31, by Cezary Kaliszyk
Regularize for equalities and a better tactic. "alpha.cases" now lifts.
2009-10-30, by Cezary Kaliszyk
Regularization
2009-10-30, by Cezary Kaliszyk
merged
2009-10-30, by Christian Urban
added some facts about fresh and support of lam
2009-10-30, by Christian Urban
Finally merged the code of the versions of regularize and tested examples.
2009-10-30, by Cezary Kaliszyk
Lemmas about fv.
2009-10-30, by Cezary Kaliszyk
changed the order of rfv and reformulated a3 with rfv
2009-10-30, by Christian Urban
merged
2009-10-30, by Christian Urban
not sure what changed here
2009-10-30, by Christian Urban
added fv-function
2009-10-30, by Christian Urban
The proper real_alpha
2009-10-30, by Cezary Kaliszyk
Finding applications and duplicates filtered out in abstractions
2009-10-30, by Cezary Kaliszyk
Cleaning also in Lam
2009-10-30, by Cezary Kaliszyk
Cleaning of the interface to lift.
2009-10-30, by Cezary Kaliszyk
Tried manually lifting real_alpha
2009-10-29, by Cezary Kaliszyk
More tests in Lam
2009-10-29, by Cezary Kaliszyk
Cleaning of 'map id' and 'prod_fun id id' in lower_defs.
2009-10-29, by Cezary Kaliszyk
Using subst for identity definition.
2009-10-29, by Cezary Kaliszyk
Lifting of the 3 lemmas in LamEx
2009-10-29, by Cezary Kaliszyk
Fixed wrong CARD definition and removed the "Does not work anymore" comment.
2009-10-29, by Cezary Kaliszyk
merged
2009-10-29, by Christian Urban
updated some definitions; had to give sometimes different names; somewhere I introduced a bug, since not everything is working anymore (needs fixing!)
2009-10-28, by Christian Urban
ported all constant definitions to new scheme
2009-10-28, by Christian Urban
fixed the definition of alpha; this *breaks* some of the experiments
2009-10-28, by Christian Urban
disambiguate ===> syntax
2009-10-28, by Cezary Kaliszyk
More cleaning in Lam code
2009-10-28, by Cezary Kaliszyk
cleaned FSet
2009-10-28, by Cezary Kaliszyk
Some cleaning
2009-10-28, by Cezary Kaliszyk
Cleaning the unnecessary theorems in 'IntEx'.
2009-10-28, by Cezary Kaliszyk
Fix also in the general procedure.
2009-10-28, by Cezary Kaliszyk
merge
2009-10-28, by Cezary Kaliszyk
Fixes
2009-10-28, by Cezary Kaliszyk
updated all definitions
2009-10-28, by Christian Urban
merged
2009-10-28, by Christian Urban
added infrastructure for defining lifted constants
2009-10-28, by Christian Urban
First experiments with Lambda
2009-10-28, by Cezary Kaliszyk
Fixed mistake in const generation, will postpone this.
2009-10-28, by Cezary Kaliszyk
More finshed proofs and cleaning
2009-10-28, by Cezary Kaliszyk
Proof of append_rsp
2009-10-28, by Cezary Kaliszyk
merged
2009-10-28, by Christian Urban
added a function for matching types
2009-10-28, by Christian Urban
Manual conversion of equality to equivalence allows lifting append_assoc.
2009-10-27, by Cezary Kaliszyk
Simplfied interface to repabs_injection.
2009-10-27, by Cezary Kaliszyk
map_append lifted automatically.
2009-10-27, by Cezary Kaliszyk
Manually lifted Map_Append.
2009-10-27, by Cezary Kaliszyk
Merged
2009-10-27, by Cezary Kaliszyk
Fixed APPLY_RSP vs Cong in the InjRepAbs tactic.
2009-10-27, by Cezary Kaliszyk
tuned
2009-10-27, by Christian Urban
merged
2009-10-27, by Christian Urban
added equiv-thm to the quot_info
2009-10-27, by Christian Urban
Simplifying FSet with new functions.
2009-10-27, by Cezary Kaliszyk
added an example about lambda-terms
2009-10-27, by Christian Urban
made quotients compatiple with Nominal; updated keyword file
2009-10-27, by Christian Urban
merged
2009-10-27, by Christian Urban
Completely cleaned Int.
2009-10-27, by Cezary Kaliszyk
Further reordering in Int code.
2009-10-27, by Cezary Kaliszyk
Simplifying Int.
2009-10-26, by Cezary Kaliszyk
Merge
2009-10-26, by Cezary Kaliszyk
Simplifying Int and Working on map
2009-10-26, by Cezary Kaliszyk
merged
2009-10-26, by Christian Urban
Simplifying code in int
2009-10-26, by Cezary Kaliszyk
Symmetry of integer addition
2009-10-26, by Cezary Kaliszyk
Finished the code for adding lower defs, and more things moved to QuotMain
2009-10-26, by Cezary Kaliszyk
Making all the definitions from the original ones
2009-10-26, by Cezary Kaliszyk
Finished COND_PRS proof.
2009-10-26, by Cezary Kaliszyk
Cleaning and fixing.
2009-10-26, by Cezary Kaliszyk
updated with quotient_def
2009-10-26, by Christian Urban
added code for declaring map-functions
2009-10-25, by Christian Urban
added "print_quotients" command to th ekeyword file
2009-10-25, by Christian Urban
proved the two lemmas in QuotScript (reformulated them without leading forall)
2009-10-25, by Christian Urban
added data-storage about the quotients
2009-10-25, by Christian Urban
added another example file about integers (see HOL/Int.thy)
2009-10-24, by Christian Urban
changed the definitions of liftet constants to use fun_maps
2009-10-24, by Christian Urban
Merge
2009-10-24, by cek
Finally lifted induction, with some manually added simplification lemmas.
2009-10-24, by Cezary Kaliszyk
changed encoding from utf8 to ISO8 (needed to work with xemacs)
2009-10-24, by Christian Urban
Merge
2009-10-24, by cek
Preparing infrastructire for LAMBDA_PRS
2009-10-24, by Cezary Kaliszyk
moved the map_funs setup into QuotMain
2009-10-24, by Christian Urban
Finally completely lift the previously lifted theorems + clean some old stuff
2009-10-24, by Cezary Kaliszyk
More infrastructure for automatic lifting of theorems lifted before
2009-10-24, by Cezary Kaliszyk
More infrastructure for automatic lifting of theorems lifted before
2009-10-24, by Cezary Kaliszyk
Undid wrong merge
2009-10-24, by cek
Tried rolling back
2009-10-24, by cek
Cleaning the mess
2009-10-24, by cek
Merge
2009-10-24, by cek
Better tactic and simplified the proof further
2009-10-24, by cek
fixed problem with incorrect ABS/REP name
2009-10-24, by Christian Urban
Stronger tactic, simpler proof.
2009-10-23, by Cezary Kaliszyk
Split Finite Set example into separate file
2009-10-23, by Cezary Kaliszyk
eqsubst_tac
2009-10-23, by Cezary Kaliszyk
Trying to get a simpler lemma with the whole infrastructure
2009-10-23, by Cezary Kaliszyk
Using RANGE tactical allows getting rid of the quotients immediately.
2009-10-23, by Cezary Kaliszyk
Further developing the tactic and simplifying the proof
2009-10-22, by Cezary Kaliszyk
res_forall_rsp_tac further simplifies the proof
2009-10-22, by Cezary Kaliszyk
Working on the proof and the tactic.
2009-10-22, by Cezary Kaliszyk
The proof gets simplified
2009-10-22, by Cezary Kaliszyk
Removed an assumption
2009-10-22, by Cezary Kaliszyk
The proof now including manually unfolded higher-order RES_FORALL_RSP.
2009-10-22, by Cezary Kaliszyk
The problems with 'abs' term.
2009-10-22, by Cezary Kaliszyk
Simplified the proof with some tactic... Still hangs sometimes.
2009-10-22, by Cezary Kaliszyk
More proof
2009-10-22, by Cezary Kaliszyk
Got rid of instantiations in the proof
2009-10-22, by Cezary Kaliszyk
Removed some debugging messages
2009-10-22, by Cezary Kaliszyk
tuned and attempted to store data about the quotients (does not work yet)
2009-10-22, by Christian Urban
tuned
2009-10-22, by Christian Urban
slight tuning
2009-10-22, by Christian Urban
fixed my_reg
2009-10-21, by Christian Urban
Reorganization of the construction part
2009-10-21, by Cezary Kaliszyk
Simplified proof more
2009-10-21, by Cezary Kaliszyk
Cleaning the code
2009-10-21, by Cezary Kaliszyk
Further reorganization
2009-10-21, by Cezary Kaliszyk
Further reorganizing the file
2009-10-21, by Cezary Kaliszyk
Reordering
2009-10-21, by Cezary Kaliszyk
cterm_instantiate also fails for some strange reason...
2009-10-21, by Cezary Kaliszyk
preparing arguments for res_inst_tac
2009-10-21, by Cezary Kaliszyk
Trying res_inst_tac
2009-10-21, by Cezary Kaliszyk
started to write code for storing data about the quotients
2009-10-20, by Christian Urban
some minor tuning
2009-10-20, by Christian Urban
tuned and fixed the earlier fix
2009-10-20, by Christian Urban
fixed the abs case in my_reg and added an app case
2009-10-20, by Christian Urban
my version of regularise (still needs to be completed)
2009-10-20, by Christian Urban
moved the map-info and fun-info section to quotient.ML
2009-10-20, by Christian Urban
Test if we can already do sth with the transformed theorem.
2009-10-18, by Cezary Kaliszyk
slight fix and tuning
2009-10-18, by Christian Urban
the command "quotient" can now define more than one quotient at the same time; quotients need to be separated by and
2009-10-18, by Christian Urban
Partial simplification of the proof
2009-10-17, by Cezary Kaliszyk
Some QUOTIENTS
2009-10-17, by Cezary Kaliszyk
Only QUOTIENSs are left to fnish proof
2009-10-17, by Cezary Kaliszyk
More higher order unification problems
2009-10-17, by Cezary Kaliszyk
Merged
2009-10-17, by Cezary Kaliszyk
Simplified
2009-10-17, by Cezary Kaliszyk
Further in the proof
2009-10-17, by Cezary Kaliszyk
compose_tac works with the full instantiation.
2009-10-17, by Cezary Kaliszyk
slightly simplified get_fun function
2009-10-17, by Christian Urban
The instantiated version is the same modulo beta
2009-10-17, by Cezary Kaliszyk
Fully manually instantiated. Still fails...
2009-10-17, by Cezary Kaliszyk
Little progress with match/instantiate
2009-10-17, by Cezary Kaliszyk
Fighting with the instantiation
2009-10-16, by Cezary Kaliszyk
Symmetric version of REP_ABS_RSP
2009-10-16, by Cezary Kaliszyk
Progressing with the proof
2009-10-16, by Cezary Kaliszyk
Finally fix get_fun.
2009-10-16, by Cezary Kaliszyk
A fix for one fun_map; doesn't work for more.
2009-10-16, by Cezary Kaliszyk
fixed the problem with function types; but only type_of works; cterm_of does not work
2009-10-16, by Christian Urban
Description of the problem with get_fun.
2009-10-15, by Cezary Kaliszyk
A proper build_goal_term function.
2009-10-15, by Cezary Kaliszyk
Cleaning the code
2009-10-15, by Cezary Kaliszyk
Merged
2009-10-15, by Cezary Kaliszyk
Cleaning the proofs
2009-10-15, by Cezary Kaliszyk
Cleaning the code, part 4
2009-10-15, by Cezary Kaliszyk
slightly improved tyRel
2009-10-15, by Christian Urban
Reordering the code, part 3
2009-10-15, by Cezary Kaliszyk
Reordering the code, part 2.
2009-10-15, by Cezary Kaliszyk
Reordering the code, part 1.
2009-10-15, by Cezary Kaliszyk
Minor cleaning.
2009-10-15, by Cezary Kaliszyk
The definition of Fold1
2009-10-15, by Cezary Kaliszyk
A number of lemmas for REGULARIZE_TAC and regularizing card1.
2009-10-15, by Cezary Kaliszyk
Proving the proper RepAbs version
2009-10-14, by Cezary Kaliszyk
Forgot to save, second part of the commit
2009-10-14, by Cezary Kaliszyk
Manually regularized list_induct2
2009-10-14, by Cezary Kaliszyk
Fixed bug in regularise types. Now we can regularise list.induct.
2009-10-14, by Cezary Kaliszyk
Function for checking recursively if lifting is needed
2009-10-14, by Cezary Kaliszyk
Merge
2009-10-14, by Cezary Kaliszyk
Proper handling of non-lifted quantifiers, testing type freezing.
2009-10-14, by Cezary Kaliszyk
slight simplification of atomize_thm
2009-10-13, by Christian Urban
atomize_thm and meta_quantify.
2009-10-13, by Cezary Kaliszyk
Regularizing HOL all.
2009-10-13, by Cezary Kaliszyk
":" is used for being in a set, "IN" means something else...
2009-10-13, by Cezary Kaliszyk
First (untested) version of regularize for abstractions.
2009-10-13, by Cezary Kaliszyk
restored old version
2009-10-13, by Christian Urban
tuned
2009-10-13, by Christian Urban
slightly modified the parser
2009-10-12, by Christian Urban
deleted diagnostic code
2009-10-12, by Christian Urban
added quotient command (you need to update isar-keywords-prove.el)
2009-10-12, by Christian Urban
added new keyword
2009-10-12, by Christian Urban
Bounded quantifier
2009-10-12, by Cezary Kaliszyk
The tyREL function.
2009-10-12, by Cezary Kaliszyk
started some strange functions
2009-10-12, by Christian Urban
Further with the manual proof
2009-10-12, by Cezary Kaliszyk
Further experiments with proving induction manually
2009-10-09, by Cezary Kaliszyk
Testing if I can prove the regularized version of induction manually
2009-10-09, by Cezary Kaliszyk
exported parts of QuotMain into a separate ML-file
2009-10-08, by Christian Urban
consistent usage of rty (for the raw, unquotient type); tuned a bit the Isar
2009-10-06, by Christian Urban
simplified typedef_quot_type_tac (using MetaSimplifier.rewrite_rule instead of the simplifier)
2009-10-06, by Christian Urban
renamed unlam_def to unabs_def (matching the function abs_def in drule.ML)
2009-10-06, by Christian Urban
less
more
|
(0)
-480
+480
+1000
tip