Implementation
==============
Relation: comp -> composition
replace "simp only split" by "split_tac".
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?
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
===========================
explanation of term "contrapositive"/contraposition in Rules?
Index the notion and maybe the rules contrapos_xy
Even: forward ref from problem with "Suc(Suc n) : even" to general solution in
AdvancedInd section.
get rid of use_thy in tutorial?
Explain typographic conventions?
Orderings on numbers (with hint that it is overloaded):
bounded quantifers ALL x<y, <=.
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 nor just for consts but also for constdefs and datatype.
Appendix with list functions.
Move section on rule inversion further to the front, and combine
\subsection{Universal quantifiers in introduction rules}
\subsection{Continuing the `ground terms' example}
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?
==============================================================