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.
list of ^*/^+ intro rules. Incl transitivity?
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.
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 ??
Advanced Ind expects rulify, mp and spec. How much really?
recdef: subsection Beyond Measure on lex, finite_psubset, ...
incl Ackermann, which is now at the end of Recdef/termination.thy.
-> Advanced.
Sentence at the end:
If you feel that the definition of recursive functions is overly and maybe
unnecessarily complicated by the requirement of totality you should ponder
the alternative, a logic of partial functions, where recursive definitions
are always wellformed. For a start, there are many
such logics, and no clear winner has emerged. And in all of these logics you
are (more or less frequently) required to reason about the definedness of
terms explicitly. Thus one shifts definedness arguments from definition to
proof time. In HOL you may have to work hard to define a function, but proofs
can then proceed unencumbered by worries about undefinedness.
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.
Advanced:
rule induction where premise not atomic (x1...xn) : R.
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?
Explain what "by" and "." really do, and introduce "done".
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?)
explain rulify before induction section?
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?
==============================================================