778
+ − 1
Highest Priority
+ − 2
================
+ − 3
952
+ − 4
- give examples for the new quantifier translations in regularization
+ − 5
(quotient_term.ML)
+ − 6
+ − 7
503
d2c9a72e52e0
first version of internalised quotient theorems; added FIXME-TODO
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 8
Higher Priority
d2c9a72e52e0
first version of internalised quotient theorems; added FIXME-TODO
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 9
===============
d2c9a72e52e0
first version of internalised quotient theorems; added FIXME-TODO
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 10
1204
+ − 11
+ − 12
- Also, in the interest of making nicer generated documentation, you
+ − 13
might want to change all your "section" headings in Quotient.thy to
+ − 14
"subsection", and add a "header" statement to the top of the file.
+ − 15
Otherwise, each "section" gets its own chapter in the generated pdf,
+ − 16
when the rest of HOL has one chapter per theory file (the chapter
+ − 17
title comes from the "header" statement).
+ − 18
794
f0a78fda343f
added an item about when the same quotient constant is defined twice (throws a bind exception in quoteint_def.ML)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 19
- If the constant definition gives the wrong definition
778
+ − 20
term, one gets a cryptic message about absrep_fun
503
d2c9a72e52e0
first version of internalised quotient theorems; added FIXME-TODO
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 21
794
f0a78fda343f
added an item about when the same quotient constant is defined twice (throws a bind exception in quoteint_def.ML)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 22
- Handle theorems that include Ball/Bex. For this, would
f0a78fda343f
added an item about when the same quotient constant is defined twice (throws a bind exception in quoteint_def.ML)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 23
it help if we introduced separate Bex and Ball constants
f0a78fda343f
added an item about when the same quotient constant is defined twice (throws a bind exception in quoteint_def.ML)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 24
for quotienting?
512
+ − 25
794
f0a78fda343f
added an item about when the same quotient constant is defined twice (throws a bind exception in quoteint_def.ML)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 26
- The user should be able to give quotient_respects and
760
c1989de100b4
various tunings; map_lookup now raises an exception; addition to FIXME-TODO
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 27
preserves theorems in a more natural form.
503
d2c9a72e52e0
first version of internalised quotient theorems; added FIXME-TODO
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 28
d2c9a72e52e0
first version of internalised quotient theorems; added FIXME-TODO
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 29
Lower Priority
d2c9a72e52e0
first version of internalised quotient theorems; added FIXME-TODO
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 30
==============
d2c9a72e52e0
first version of internalised quotient theorems; added FIXME-TODO
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 31
1281
+ − 32
- the quot_lifted attribute should rename variables so they do not
+ − 33
suggest that they talk about raw terms.
+ − 34
778
+ − 35
- accept partial equivalence relations
716
+ − 36
768
e9e205b904e2
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
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 37
- think about what happens if things go wrong (like
e9e205b904e2
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
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 38
theorem cannot be lifted) / proper diagnostic
e9e205b904e2
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
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 39
messages for the user
760
c1989de100b4
various tunings; map_lookup now raises an exception; addition to FIXME-TODO
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 40
713
+ − 41
- inductions from the datatype package have a strange
+ − 42
order of quantifiers in assumptions.
+ − 43
503
d2c9a72e52e0
first version of internalised quotient theorems; added FIXME-TODO
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 44
- find clean ways how to write down the "mathematical"
d2c9a72e52e0
first version of internalised quotient theorems; added FIXME-TODO
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 45
procedure for a possible submission (Peter submitted
d2c9a72e52e0
first version of internalised quotient theorems; added FIXME-TODO
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 46
his work only to TPHOLs 2005...we would have to go
506
+ − 47
maybe for the Journal of Formalised Mathematics)
+ − 48
515
+ − 49
- add tests for adding theorems to the various thm lists
+ − 50
746
+ − 51
- Maybe quotient and equiv theorems like the ones for
+ − 52
[QuotList, QuotOption, QuotPair...] could be automatically
+ − 53
proven?
753
544b05e03ec0
Removed lambdas on the right hand side. This fixes all 'PROBLEM' comments.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 54
768
e9e205b904e2
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
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 55
- Examples: Finite multiset.
e9e205b904e2
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
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 56
e9e205b904e2
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
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 57
- The current syntax of the quotient_definition is
e9e205b904e2
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
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 58
e9e205b904e2
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
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 59
"qconst :: qty"
e9e205b904e2
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
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 60
as "rconst"
e9e205b904e2
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
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 61
e9e205b904e2
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
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 62
Is it possible to have the more Isabelle-like
e9e205b904e2
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
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 63
syntax
e9e205b904e2
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
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 64
e9e205b904e2
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
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 65
qconst :: "qty"
e9e205b904e2
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
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 66
as "rconst"
e9e205b904e2
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
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 67
e9e205b904e2
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
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 68
That means "qconst :: qty" is not read as a term, but
912
+ − 69
as two entities.