summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

doc-src/TutorialI/todo.tobias

author | wenzelm |

Sun, 15 Oct 2000 19:50:35 +0200 | |

changeset 10220 | 2a726de6e124 |

parent 10217 | e61e7e1eacaf |

child 10236 | 7626cb4e1407 |

permissions | -rw-r--r-- |

proper symbol markup with \isamath, \isatext;
support sub/super scripts:

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. 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 rule_format incl (no_asm) (which it currently explains! Where explained? 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? 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? ==============================================================