4 Hide global names like Node.
5 Why is comp needed in addition to op O?
6 Explain in syntax section!
8 defs with = and pattern matching
10 replace "simp only split" by "split_tac".
12 arithmetic: allow mixed nat/int formulae
13 -> simplify proof of part1 in Inductive/AB.thy
15 Add map_cong?? (upto 10% slower)
17 Recdef: Get rid of function name in header.
18 Support mutual recursion (Konrad?)
20 use arith_tac in recdef to solve termination conditions?
21 -> new example in Recdef/termination
23 a tactic for replacing a specific occurrence:
24 apply(substitute [2] thm)
26 it would be nice if @term could deal with ?-vars.
27 then a number of (unchecked!) @texts could be converted to @terms.
29 it would be nice if one could get id to the enclosing quotes in the [source] option.
31 More predefined functions for datatypes: map?
33 Induction rules for int: int_le/ge_induct?
34 Needed for ifak example. But is that example worth it?
37 Minor fixes in the tutorial
38 ===========================
40 explanation of absence of contrapos_pn in Rules?
42 get rid of use_thy in tutorial?
44 Explain typographic conventions?
46 an example of induction: !y. A --> B --> C ??
48 Appendix: Lexical: long ids.
50 Warning: infixes automatically become reserved words!
52 Forward ref from blast proof of Puzzle (AdvancedInd) to Isar proof?
54 mention split_split in advanced pair section.
56 recdef with nested recursion: either an example or at least a pointer to the
57 literature. In Recdef/termination.thy, at the end.
58 %FIXME, with one exception: nested recursion.
60 Syntax section: syntax annotations nor just for consts but also for constdefs and datatype.
62 Appendix with list functions.
65 Minor additions to the tutorial, unclear where
66 ==============================================
70 Mention that simp etc (big step tactics) insist on change?
72 Rules: Introduce "by" (as a kind of shorthand for apply+done, except that it
75 A list of further useful commands (rules? tricks?)
76 prefer, defer, print_simpset (-> print_simps?)
78 An overview of the automatic methods: simp, auto, fast, blast, force,
79 clarify, clarsimp (intro, elim?)
81 Advanced Ind expects rule_format incl (no_asm) (which it currently explains!)
82 Where explained? Should go into a separate section as Inductive needs it as
85 Where is "simplified" explained? Needed by Inductive/AB.thy
87 demonstrate x : set xs in Sets. Or Tricks chapter?
89 Appendix with HOL keywords. Say something about other keywords.
97 %Extend expressions by conditional expressions.
101 Nested inductive datatypes: another example/exercise:
102 size(t) <= size(subst s t)?
104 insertion sort: primrec, later recdef
107 first version only for non-empty trees:
108 Tip 'a | Node tree tree
110 First primrec, then recdef?
112 Ind. sets: define ABC inductively and prove
113 ABC = {rep A n @ rep B n @ rep C n. True}
115 Possible examples/case studies
116 ==============================
118 Trie: Define functional version
119 datatype ('a,'b)trie = Trie ('b option) ('a => ('a,'b)trie option)
120 lookup t [] = value t
121 lookup t (a#as) = case tries t a of None => None | Some s => lookup s as
122 Maybe as an exercise?
124 Trie: function for partial matches (prefixes). Needs sets for spec/proof.
126 Sets via ordered list of intervals. (Isa/Interval(2))
128 propositional logic (soundness and completeness?),
129 predicate logic (soundness?),
131 Tautology checker. Based on Ifexpr or prop.logic?
132 Include forward reference in relevant section.
134 Sorting with comp-parameter and with type class (<)
138 Steps Towards Mechanizing Program Transformations Using PVS by N. Shankar,
139 Science of Computer Programming, 26(1-3):33-57, 1996.
140 You can get it from http://www.csl.sri.com/scp95.html
142 J Moore article Towards a ...
149 Recdef with nested recursion?
151 Extensionality: applications in
152 - boolean expressions: valif o bool2if = value
153 - Advanced datatypes exercise subst (f o g) = subst f o subst g
155 A look at the library?
157 If WF is discussed, make a link to it from AdvancedInd.
161 ==============================================================
166 if-normalization with measure function,
167 nested if-normalization,
174 Partial rekursive functions / Nontermination
176 What appears to be the problem:
179 apply(cut_facts_tac axiom, simp).
184 f x = if $x \in dom(f)$ then ... else arbitrary
186 Example: sum/fact: int -> int (for no good reason because we have nat)
188 Exercise: ?! f. !i. f i = if i=0 then 1 else i*f(i-1)
189 (What about sum? Is there one, a unique one?)
191 [Alternative: include argument that is counted down
192 f x n = if n=0 then None else ...
193 Refer to Boyer and Moore]
195 More complex: same_fst
197 chase(f,x) = if wf{(f x,x) . f x ~= x}
198 then if f x = x then x else chase(f,f x)
201 Prove wf ==> f(chase(f,x)) = chase(f,x)
203 2. While / Tail recursion
205 chase f x = fst(while (%(x,fx). x=fx) (%(x,fx). (fx,f fx)) (x,f x))
207 ==> unfold eqn for chase? Prove fixpoint property?
209 Better(?) sum i = fst(while (%(s,i). i=0) (%(s,i). (s+i,i-1)) (0,i))
210 Prove 0 <= i ==> sum i = i*(i+1) via while-rule
213 ==============================================================