doc-src/TutorialI/todo.tobias

*** empty log message ***

General questions
=================

Here is an initial list:
clarify, clarsimp, hyp_subst_tac, rename_tac, rotate_tac, split
single step tactics: (e/d/f)rule, insert
with instantiation: (e/d/f)rule_tac, insert_tac

Hide global names like Node.
Why is comp needed in addition to op O?
Explain in syntax section!

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

swap in classical.ML has ugly name Pa in it. Rename.

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

Add map_cong?? (upto 10% slower)
But we should install UN_cong and INT_cong too.

recdef: funny behaviour with map (see email to Konrad.Slind, Recdef/Nested1)

defs with = and pattern matching

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

a tactic for replacing a specific occurrence:
apply(substitute [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.

arithmetic: allow mixed nat/int formulae
-> simplify proof of part1 in Inductive/AB.thy

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

replace simp only split by split_tac.

get rid of use_thy?

Explain typographic conventions?

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

Appendix: Lexical: long ids.

Warning: infixes automatically become reserved words!

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

mention split_split in advanced pair section.

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 nor just for consts but also for constdefs and datatype.

Prove EU exercise in CTL.


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

Tacticals: , ? +

"typedecl" is used in CTL/Base, but where is it introduced?
In More Types chapter? Rephrase the CTL bit accordingly.

print_simpset (-> print_simps?)
(Another subsection Useful theorems, methods, and commands?)

Mention that simp etc (big step tactics) insist on change?

Rules: Introduce "by" (as a kind of shorthand for apply+done, except that it
does more.)

A list of further useful commands (rules? tricks?)
prefer, defer

An overview of the automatic methods: simp, auto, fast, blast, force,
clarify, clarsimp (intro, elim?)

Advanced Ind expects rule_format incl (no_asm) (which it currently explains!)
Where explained?
Inductive also needs rule_format!

Where is "simplified" explained? Needed by Inductive/AB.thy

demonstrate x : set xs in Sets. Or Tricks chapter?

Appendix with HOL keywords. Say something about other keywords.


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

Exercises
%\begin{exercise}
%Extend expressions by conditional expressions.
braucht wfrec!
%\end{exercise}

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}

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

Sets: PDL and CTL

Ind. defs: Grammar (for same number of as and bs),
propositional logic (soundness and completeness?),
predicate logic (soundness?),
CTL proof.

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

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

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

Beef up recdef (see below).
Nested recursion? Mutual recursion?

Nested inductive datatypes: better recursion and induction
(see below)

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?
Functions. Relations. Lfp/Gfp. Map.
If WF is discussed, make a link to it from AdvancedInd.

Prototyping?


Isabelle
========

Get rid of function name in recdef header

More predefined functions for datatypes: map?

1 and 2 on nat?


==============================================================
Nested inductive datatypes: better recursion and induction

Show how to derive simpler primrec functions using eg map. Text:

Returning to the definition of \texttt{subst}, we have to admit that it does
not really need the auxiliary \texttt{substs} function. The \texttt{App}-case
can directly be expressed as
\begin{ttbox}
\input{Datatype/appmap}\end{ttbox}
Although Isabelle insists on the more verbose version, we can easily {\em
  prove} that the \texttt{map}-equation holds: simply by induction on
\texttt{ts} followed by \texttt{Auto_tac}.
lemma "subst s (App f ts) = App f (map (subst s) ts)";
by(induct_tac ts, auto);

Now explain how to remove old eqns from simpset by naming them.
But: the new eqn only helps if the induction schema is also modified
accordingly:

val prems =
Goal "[| !!v. P(Var v); !!f ts. (!!t. t : set ts ==> P t) ==> P(App f ts) |] \
\     ==> P t & (!t: set ts. P t)";
by(induct_tac "t ts" 1);
brs prems 1;
brs prems 1;
by(Blast_tac 1);
by(Simp_tac 1);
by(Asm_simp_tac 1);

Now the following exercise has an easy proof:

\begin{exercise}
  Define a function \texttt{rev_term} of type \texttt{term -> term} that
  recursively reverses the order of arguments of all function symbols in a
  term. Prove that \texttt{rev_term(rev_term t) = t}.
\end{exercise}

==============================================================
Recdef:

nested recursion
more example proofs:
 if-normalization with measure function,
 nested if-normalization,
 quicksort
 Trie?
a case study?

A separate subsection on recdef beyond measure, eg <*lex*> and psubset.
Example: some finite fixpoint computation? MC, Grammar?
How to modify wf-prover?

----------

Partial rekursive functions / Nontermination

What appears to be the problem:
axiom f n = f n + 1
lemma False
apply(cut_facts_tac axiom, simp).

1. Guarded recursion

Scheme:
f x = if $x \in dom(f)$ then ... else arbitrary

Example: sum/fact: int -> int (for no good reason because we have nat)

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

[Alternative: include argument that is counted down
 f x n = if n=0 then None else ...
Refer to Boyer and Moore]

More complex: same_fst

chase(f,x) = if wf{(f x,x) . f x ~= x}
             then if f x = x then x else chase(f,f x)
             else arb

Prove wf ==> f(chase(f,x)) = chase(f,x)

2. While / Tail recursion

chase f x = fst(while (%(x,fx). x=fx) (%(x,fx). (fx,f fx)) (x,f x))

==> unfold eqn for chase? Prove fixpoint property?

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

Mention prototyping?
==============================================================