#
1795b9e9 |
|
07-Jun-2018 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Implement easier API entrypoints to get at case_eq theorems Closes #345
|
#
3501e524 |
|
06-May-2018 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Add Option constructor to ThyDataSexp.t
|
#
208bfeaf |
|
16-Apr-2018 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Generate "standard" datatype simpl rewrites as tyinfos are loaded This saves us from having to write them out to disk, which can make for unnecessarily large theory.dat files.
|
#
1e0d2028 |
|
11-Apr-2018 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Re-implement Datatype package with TypeBase sexps (not adjoin)
|
#
53ccf6e4 |
|
11-Apr-2018 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Force users of ThyDataSexp to provide their own merge function Provide a couple of likely candidates for this purpose.
|
#
3ffd27c6 |
|
08-Apr-2018 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Implement code to convert tyinfo's to and from ThyDataSexp.t Format is rather "wordier" than necessary, but the extra (redundant) field names should be helpful for debugging.
|
#
c7b36e85 |
|
15-Mar-2018 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Up to hol.state0
|
#
0b018443 |
|
11-Dec-2017 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Rename TypeBase entrypoints for caseeqsplit and friends Now use case_eq everywhere. Work on github issue #345
|
#
962f50c1 |
|
29-Nov-2017 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Automatically prove "case-eqsplit" theorems and store in TypeBase For :num, this theorem looks like (num_CASE n zc sc = v) <=> (n = 0) ∧ (zc = v) ∨ ∃x. (n = SUC x) ∧ (sc x = v) Such theorems can be powerful rewrites when (large) case-expressions are asserted to be equal to some value or other. These theorems have to be installed somewhat by hand for early types, but from list onwards, the Datatype package handles this. This work leverages earlier work done implementing prove_case_eq_thm (8f16922426). Take the opportunity to rework TypeBasePure's code to use FunctionalRecordUpdate. This is progress with github issue #345.
|
#
15e37a5d |
|
12-Jul-2017 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Fix bug in repeated Datatype calls with mutual recursion Closes #435
|
#
a16605e3 |
|
16-Nov-2015 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Fixes with polymorphic record literals 1. When you write <| fld1 := foo ; fld2 := bar |> there is secretly an ARB term hiding in the result. You don't want that ARB term to be unnecessarily polymorphic. 2. TypeBase.mk_record has to adjust for the possibility that fupds can have types of the form fupd : (α fldty -> β fldty) -> (α,γ) rcd -> (β, γ) rcd Continuing work on github issue #173
|
#
945ba498 |
|
13-Dec-2012 |
Michael Norrish <michael.norrish@nicta.com.au> |
Remove duplication of code between Pmatch and TypeBasePure. The case-syntax code in the latter has moved entirely to Pmatch.
|
#
e5e060cf |
|
04-Dec-2012 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Fix for bug in dest_case caused by use of hd rather than last. It turns out that last will raise a HOL_ERR on the empty list, but hd raises Empty, of course. (This is because we have our own version of last in Lib, and I’m far from sure this is a good idea.)
|
#
3af38550 |
|
04-Dec-2012 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Fix TypeBase’s dest_case entry-points. This makes pretty-printing work.
|
#
79e670ac |
|
20-Nov-2012 |
Michael Norrish <michael.norrish@nicta.com.au> |
Provide toPmatchThry entry-point in TypeBasePure. This converts from a full-blown TypeBase value into a “thry” as required by the Pmatch module. The “thry” type is simply a lookup function that returns case-constant and constructor information for a given type.
|
#
db046fee |
|
13-Nov-2012 |
Michael Norrish <michael.norrish@nicta.com.au> |
Start of project to flip argument order in case constants. One scary (but probably optional) change is to do away with bool_case constant because it is now identical to COND. This could be reversed, but having two constants with exactly the same type and semantics does seem silly. I think the parsing/pretty-printing behaviour can be made sensible even in the face of this unification. Prim_rec’s functions for defining case constants and proving case congruence theorems have been adjusted appropriately. This is relevant to Github issue #97.
|
#
be2f8ea8 |
|
04-Jul-2012 |
Michael Norrish <michael.norrish@nicta.com.au> |
Remove some trailing whitespace.
|
#
33bda56f |
|
26-Jun-2012 |
Konrad Slind <konrad.slind@gmail.com> |
Added size functions for finite sets, maps, and bags. These are helpful for measures supporting recursive definitions and induction schemes. The size functions have been added to the TypeBase, with the intent that Induct, Induct_on, Cases, and Cases_on should be applicable. (However, this has not been checked yet, so these might not work.) The size of a finite set is the number of elements in it, plus the sizes of all the elements. (The size of a set with 0 as an element is larger than that set with the zero deleted.) The size of a finite map is the number of mapped elements, plus the sizes of the mapped elements. Key size is ignored. The size of a finite multiset is the number of elements in the multiset plus the sizes of the elements. There are more extensive orderings (e.g. the multiset order) but they aren't measures, which is important for the way termination proofs are automated.
|
#
5b587535 |
|
26-Jun-2012 |
Konrad Slind <konrad.slind@gmail.com> |
Allow "non-datatypes" in TypeBase to have optional induction thm. Provide appropriate values for this field for finite sets, strings, integers, finite maps and words.
|
#
845531b5 |
|
14-Sep-2011 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Remove trailing whitespace in source files.
|
#
6cac8296 |
|
07-Mar-2011 |
Konrad Slind <konrad.slind@gmail.com> |
Addition of destructors and recognizers for datatypes. So far, I've just got basic support put in. Some other trivial mods as well.
|
#
1bc9f344 |
|
13-Jan-2011 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Change src/bool to src/1 as a prelude to experimentation!
|