Further in the proof

compose_tac works with the full instantiation.

slightly simplified get_fun function

The instantiated version is the same modulo beta

Fully manually instantiated. Still fails...

Little progress with match/instantiate

Fighting with the instantiation

Symmetric version of REP_ABS_RSP

Progressing with the proof

Finally fix get_fun.

A fix for one fun_map; doesn't work for more.

fixed the problem with function types; but only type_of works; cterm_of does not work

Description of the problem with get_fun.

A proper build_goal_term function.

Cleaning the code

Merged

Cleaning the proofs

Cleaning the code, part 4

slightly improved tyRel

Reordering the code, part 3

Reordering the code, part 2.

Reordering the code, part 1.

Minor cleaning.

The definition of Fold1

A number of lemmas for REGULARIZE_TAC and regularizing card1.

Proving the proper RepAbs version

Forgot to save, second part of the commit

Manually regularized list_induct2

Fixed bug in regularise types. Now we can regularise list.induct.

Function for checking recursively if lifting is needed

Merge

Proper handling of non-lifted quantifiers, testing type freezing.

slight simplification of atomize_thm

atomize_thm and meta_quantify.

Regularizing HOL all.

":" is used for being in a set, "IN" means something else...

First (untested) version of regularize for abstractions.

restored old version

tuned

slightly modified the parser

deleted diagnostic code

added quotient command (you need to update isar-keywords-prove.el)

added new keyword

Bounded quantifier

The tyREL function.

started some strange functions

Further with the manual proof

Further experiments with proving induction manually

Testing if I can prove the regularized version of induction manually

exported parts of QuotMain into a separate ML-file

consistent usage of rty (for the raw, unquotient type); tuned a bit the Isar proof of atomize_eqv.

simplified typedef_quot_type_tac (using MetaSimplifier.rewrite_rule instead of the simplifier)

renamed unlam_def to unabs_def (matching the function abs_def in drule.ML)

tuned; nothing serious

another improvement to unlam_def

one further improvement to unlam_def

simplified the unlam_def function

added an explicit syntax-argument to the function make_def (is needed if the user gives an syntax annotation for quotient types)

used prop_of to get the term of a theorem (replaces crep_thm)

Merged

First theorem with quantifiers. Learned how to use sledgehammer.

simplified the storage of the map-functions by using TheoryDataFun

Just one atomize is enough for the currently lifted theorems. Properly lift 'all' and 'Ex'.

used new cong_tac

First version of handling of the universal quantifier

Handling abstraction correctly.

second test

Test line

Partially fix lifting of card_suc. The quantified variable still needs to be changed.

Tested new build_goal and removed old one, eq_reflection is included in atomize, card_suc tests.

Checked again with the version on my hard-drive backedup yesterday and fixed small whitespace issues.

Merged

added name to prove

consistent state

some tuning of my code

Cleanup

Merged

Cleaning the code with Makarius

Instnatiation with a schematic variable

added ctxt as explicit argument to build_goal; tuned

slightly tuned the comment for unlam

fixed a bug in my code: function typedef_term constructs now now the correct term when the relation is called x

tuned slightly one proof

A version of the tactic that exports variables correctly. It still does not know how to instantiate the obtained theorems.

Minor cleaning: whitespace, commas etc.

Correctly handling abstractions while building goals Use DatatypeAux cong_tac instead of own functions since it handles universal quantifiers properly.

Minor cleanup

Found the source for the exception and added a handle for it.

Make the tactic use Trueprop_cong and atomize.

Proper code for getting the prop out of the theorem.

Using "atomize" the versions with arbitrary Trueprops can be proven.

Proper definition of CARD and some properties of it. Translation should now support Pure assumptions and Trueprops anywhere, but a problem needs to be fixed with the tactic.

some comments

merged

slight tuning

The tactic with REPEAT, CHANGED and a proper simpset.

Merged with my changes from the morning: further working on the tactic and produced goals.

some more beautification

beautification of some proofs

Added more useful quotient facts.

Testing the tactic further.

The tactic still only for fset

Infrastructure for the tactic

More naming/binding suggestions from Makarius

Code cleanup

Cleaning the code

Generalized interpretation, works for all examples.

Fixes after suggestions from Makarius: - indentation - lowercase/uppercase - axioms -> axiomatization - proper operator priorities - proper exception handling

More examples.

Use metavariables in the 'non-lambda' definitions

Make both kinds of definitions.

Changed to the use of "modern interface" (removed the _cmd and passing of strings) Fixed Trueprop handling and the first proof starts working properly.

Initial version of the function that builds goals.

- Build an interpretation for fset from ML level and use it - Added CARD

added the prove command

Fixed

tuned

UNION - Append theorem

update

updated slightly