doc-src/TutorialI/todo.tobias

added "rules" method;

"You know my methods. Apply them!"

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

- (#2 * x) = #2 * - x is not proved by arith

a simp command for terms

----------------------------------------------------------------------
primrec 
"(foorec [] []) = []"
"(foorec [] (y # ys)) = (y # (foorec [] ys))"

*** Primrec definition error:
*** extra variables on rhs: "y", "ys"
*** in
*** "((foorec [] ((y::'a_1) # (ys::'a_1 list))) = (y # (foorec [] ys)))"
*** At command "primrec".

Bessere Fehlermeldung!
----------------------------------------------------------------------

Relation: comp -> composition

Add map_cong?? (upto 10% slower)

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.

use arith_tac in recdef to solve termination conditions?
-> new example in Recdef/termination

a tactic for replacing a specific occurrence:
apply(subst [2] thm)

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
===========================

1/2 no longer abbrevs for Suc.
Warning: needs simplification to turn 1 into Suc 0. arith does so
automatically.

recdef: failed tcs no longer shown! (sec:Recursion over nested datatypes)
say something about how conditions are proved?
No, better show failed proof attempts.

Advanced recdef: explain recdef_tc? No. Adjust recdef!

Adjust FP textbook refs: new Bird, Hudak
Discrete math textbook: Rosen?

adjust type of ^ in tab:overloading

an example of induction: !y. A --> B --> C ??

Explain type_definition and mention pre-proved thms in subset.thy?
-> Types/typedef

Appendix: Lexical: long ids.

Warning: infixes automatically become reserved words!

Forward ref from blast proof of Puzzle (AdvancedInd) to Isar proof?

recdef with nested recursion: either an example or at least a pointer to the
literature. In Recdef/termination.thy, at the end.
%FIXME, with one exception: nested recursion.

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

Appendix with list functions.

All theory sources on the web?


Minor additions to the tutorial, unclear where
==============================================

unfold?


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?

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