4 Relation: comp -> composition
6 replace "simp only split" by "split_tac".
8 Add map_cong?? (upto 10% slower)
10 Recdef: Get rid of function name in header.
11 Support mutual recursion (Konrad?)
13 use arith_tac in recdef to solve termination conditions?
14 -> new example in Recdef/termination
16 a tactic for replacing a specific occurrence:
17 apply(substitute [2] thm)
19 it would be nice if @term could deal with ?-vars.
20 then a number of (unchecked!) @texts could be converted to @terms.
22 it would be nice if one could get id to the enclosing quotes in the [source] option.
24 More predefined functions for datatypes: map?
26 Induction rules for int: int_le/ge_induct?
27 Needed for ifak example. But is that example worth it?
29 Komischerweise geht das Splitten von _Annahmen_ auch mit simp_tac, was
30 ein generelles Feature ist, das man vielleicht mal abstellen sollte.
32 proper mutual simplification
34 defs with = and pattern matching??
37 Minor fixes in the tutorial
38 ===========================
40 explanation of term "contrapositive"/contraposition in Rules?
41 Index the notion and maybe the rules contrapos_xy
43 Even: forward ref from problem with "Suc(Suc n) : even" to general solution in
46 get rid of use_thy in tutorial?
48 Explain typographic conventions?
50 Orderings on numbers (with hint that it is overloaded):
51 bounded quantifers ALL x<y, <=.
53 an example of induction: !y. A --> B --> C ??
55 Explain type_definition and mention pre-proved thms in subset.thy?
58 Appendix: Lexical: long ids.
60 Warning: infixes automatically become reserved words!
62 Forward ref from blast proof of Puzzle (AdvancedInd) to Isar proof?
64 recdef with nested recursion: either an example or at least a pointer to the
65 literature. In Recdef/termination.thy, at the end.
66 %FIXME, with one exception: nested recursion.
68 Syntax section: syntax annotations nor just for consts but also for constdefs and datatype.
70 Appendix with list functions.
72 Move section on rule inversion further to the front, and combine
73 \subsection{Universal quantifiers in introduction rules}
74 \subsection{Continuing the `ground terms' example}
77 Minor additions to the tutorial, unclear where
78 ==============================================
82 Mention that simp etc (big step tactics) insist on change?
84 Rules: Introduce "by" (as a kind of shorthand for apply+done, except that it
87 A list of further useful commands (rules? tricks?)
88 prefer, defer, print_simpset (-> print_simps?)
90 An overview of the automatic methods: simp, auto, fast, blast, force,
91 clarify, clarsimp (intro, elim?)
93 Advanced Ind expects rule_format incl (no_asm) (which it currently explains!)
94 Where explained? Should go into a separate section as Inductive needs it as
97 Where is "simplified" explained? Needed by Inductive/AB.thy
99 demonstrate x : set xs in Sets. Or Tricks chapter?
101 Appendix with HOL keywords. Say something about other keywords.
109 %Extend expressions by conditional expressions.
113 Nested inductive datatypes: another example/exercise:
114 size(t) <= size(subst s t)?
116 insertion sort: primrec, later recdef
119 first version only for non-empty trees:
120 Tip 'a | Node tree tree
122 First primrec, then recdef?
124 Ind. sets: define ABC inductively and prove
125 ABC = {rep A n @ rep B n @ rep C n. True}
127 Possible examples/case studies
128 ==============================
130 Trie: Define functional version
131 datatype ('a,'b)trie = Trie ('b option) ('a => ('a,'b)trie option)
132 lookup t [] = value t
133 lookup t (a#as) = case tries t a of None => None | Some s => lookup s as
134 Maybe as an exercise?
136 Trie: function for partial matches (prefixes). Needs sets for spec/proof.
138 Sets via ordered list of intervals. (Isa/Interval(2))
140 propositional logic (soundness and completeness?),
141 predicate logic (soundness?),
143 Tautology checker. Based on Ifexpr or prop.logic?
144 Include forward reference in relevant section.
146 Sorting with comp-parameter and with type class (<)
150 Steps Towards Mechanizing Program Transformations Using PVS by N. Shankar,
151 Science of Computer Programming, 26(1-3):33-57, 1996.
152 You can get it from http://www.csl.sri.com/scp95.html
154 J Moore article Towards a ...
161 Recdef with nested recursion?
163 Extensionality: applications in
164 - boolean expressions: valif o bool2if = value
165 - Advanced datatypes exercise subst (f o g) = subst f o subst g
167 A look at the library?
169 If WF is discussed, make a link to it from AdvancedInd.
173 ==============================================================
178 if-normalization with measure function,
179 nested if-normalization,
186 Partial rekursive functions / Nontermination
188 What appears to be the problem:
191 apply(cut_facts_tac axiom, simp).
196 f x = if $x \in dom(f)$ then ... else arbitrary
198 Example: sum/fact: int -> int (for no good reason because we have nat)
200 Exercise: ?! f. !i. f i = if i=0 then 1 else i*f(i-1)
201 (What about sum? Is there one, a unique one?)
203 [Alternative: include argument that is counted down
204 f x n = if n=0 then None else ...
205 Refer to Boyer and Moore]
207 More complex: same_fst
209 chase(f,x) = if wf{(f x,x) . f x ~= x}
210 then if f x = x then x else chase(f,f x)
213 Prove wf ==> f(chase(f,x)) = chase(f,x)
215 2. While / Tail recursion
217 chase f x = fst(while (%(x,fx). x=fx) (%(x,fx). (fx,f fx)) (x,f x))
219 ==> unfold eqn for chase? Prove fixpoint property?
221 Better(?) sum i = fst(while (%(s,i). i=0) (%(s,i). (s+i,i-1)) (0,i))
222 Prove 0 <= i ==> sum i = i*(i+1) via while-rule
225 ==============================================================