doc-src/TutorialI/todo.tobias

A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
the tactic has also changed and allows the abstaction over fuction occurences whose type is nat or int.

Implementation
==============

Add map_cong?? (upto 10% slower)

a simp command for terms

Recdef: Get rid of function name in header.
Support mutual recursion (Konrad?)

improve solver in simplifier: treat & and ! ...

better 1 point rules:
!x. !y. x = f y --> P x y  should reduce to  !y. P (f y) y.

it would be nice if @term could deal with ?-vars.
then a number of (unchecked!) @texts could be converted to @terms.

it would be nice if one could get id to the enclosing quotes in the [source] option.

More predefined functions for datatypes: map?

Induction rules for int: int_le/ge_induct?
Needed for ifak example. But is that example worth it?

Komischerweise geht das Splitten von _Annahmen_ auch mit simp_tac, was
ein generelles Feature ist, das man vielleicht mal abstellen sollte.

proper mutual simplification

defs with = and pattern matching??


Minor fixes in the tutorial
===========================

Appendix: Lexical: long ids.

Warning: infixes automatically become reserved words!

Syntax section: syntax annotations not just for consts but also for constdefs and datatype.

Appendix with list functions.

All theory sources on the web?

Possible exercises
==================

Exercises

For extensionality (in Sets chapter): prove
valif o norm = valif
in If-expression case study (Ifexpr)

Nested inductive datatypes: another example/exercise:
 size(t) <= size(subst s t)?

insertion sort: primrec, later recdef

OTree:
 first version only for non-empty trees:
 Tip 'a | Node tree tree
 Then real version?
 First primrec, then recdef?

Ind. sets: define ABC inductively and prove
ABC = {rep A n @ rep B n @ rep C n. True}

Partial rekursive functions / Nontermination:

Exercise: ?! f. !i. f i = if i=0 then 1 else i*f(i-1)
(What about sum? Is there one, a unique one?)

Exercise
Better(?) sum i = fst(while (%(s,i). i=0) (%(s,i). (s+i,i-1)) (0,i))
Prove 0 <= i ==> sum i = i*(i+1) via while-rule

Possible examples/case studies
==============================

Trie: Define functional version
datatype ('a,'b)trie = Trie ('b option) ('a => ('a,'b)trie option)
lookup t [] = value t
lookup t (a#as) = case tries t a of None => None | Some s => lookup s as
Maybe as an exercise?

Trie: function for partial matches (prefixes). Needs sets for spec/proof.

Sets via ordered list of intervals. (Isa/Interval(2))

propositional logic (soundness and completeness?),
predicate logic (soundness?),

Tautology checker. Based on Ifexpr or prop.logic?
Include forward reference in relevant section.

Sorting with comp-parameter and with type class (<)

Recdef:more example proofs:
 if-normalization with measure function,
 nested if-normalization,
 quicksort
 Trie?

New book by Bird?

Steps Towards Mechanizing Program Transformations Using PVS by N. Shankar,
      Science of Computer Programming, 26(1-3):33-57, 1996. 
You can get it from http://www.csl.sri.com/scp95.html

J Moore article Towards a ...
Mergesort, JVM


Additional topics
=================

Recdef with nested recursion?

Extensionality: applications in
- boolean expressions: valif o bool2if = value
- Advanced datatypes exercise subst (f o g) = subst f o subst g

A look at the library?
Map.

Prototyping?

==============================================================