Implementation

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

Hide global names like Node.

Why is comp needed in addition to op O?

Explain in syntax section!

defs with = and pattern matching

replace "simp only split" by "split_tac".

arithmetic: allow mixed nat/int formulae

-> simplify proof of part1 in Inductive/AB.thy

Add map_cong?? (upto 10% slower)

Recdef: Get rid of function name in header.

Support mutual recursion (Konrad?)

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.

More predefined functions for datatypes: map?

Induction rules for int: int_le/ge_induct?

Needed for ifak example. But is that example worth it?

Minor fixes in the tutorial

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

explanation of absence of contrapos_pn in Rules?

get rid of use_thy in tutorial?

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.

Appendix with list functions.

Minor additions to the tutorial, unclear where

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

Tacticals: , ? +

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, print_simpset (-> print_simps?)

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? Should go into a separate section as Inductive needs it as

well.

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

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

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.

If WF is discussed, make a link to it from AdvancedInd.

Prototyping?

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

Recdef:

nested recursion

more example proofs:

 if-normalization with measure function,

 nested if-normalization,

 quicksort

 Trie?

a case study?

----------

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?

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