4 - (#2 * x) = #2 * - x is not proved by arith
6 a simp command for terms
8 ----------------------------------------------------------------------
11 "(foorec [] (y # ys)) = (y # (foorec [] ys))"
13 *** Primrec definition error:
14 *** extra variables on rhs: "y", "ys"
16 *** "((foorec [] ((y::'a_1) # (ys::'a_1 list))) = (y # (foorec [] ys)))"
17 *** At command "primrec".
19 Bessere Fehlermeldung!
20 ----------------------------------------------------------------------
22 Relation: comp -> composition
24 Add map_cong?? (upto 10% slower)
26 Recdef: Get rid of function name in header.
27 Support mutual recursion (Konrad?)
29 use arith_tac in recdef to solve termination conditions?
30 -> new example in Recdef/termination
32 a tactic for replacing a specific occurrence:
35 it would be nice if @term could deal with ?-vars.
36 then a number of (unchecked!) @texts could be converted to @terms.
38 it would be nice if one could get id to the enclosing quotes in the [source] option.
40 More predefined functions for datatypes: map?
42 Induction rules for int: int_le/ge_induct?
43 Needed for ifak example. But is that example worth it?
45 Komischerweise geht das Splitten von _Annahmen_ auch mit simp_tac, was
46 ein generelles Feature ist, das man vielleicht mal abstellen sollte.
48 proper mutual simplification
50 defs with = and pattern matching??
53 Minor fixes in the tutorial
54 ===========================
56 recdef: failed tcs no longer shown!
58 Advanced recdef: explain recdef_tc?
60 say something about definitional approach. In recdef section? At the end?
62 I guess we should say "HOL" everywhere, with a remark early on about the
63 differences between our HOL and the other one.
65 warning: simp of asms from l to r; may require reordering (rotate_tac)
67 Adjust FP textbook refs: new Bird, Hudak
68 Discrete math textbook: Rosen?
70 say something about "abbreviations" when defs are introduced.
72 adjust type of ^ in tab:overloading
74 an example of induction: !y. A --> B --> C ??
76 Explain type_definition and mention pre-proved thms in subset.thy?
79 Appendix: Lexical: long ids.
81 Warning: infixes automatically become reserved words!
83 Forward ref from blast proof of Puzzle (AdvancedInd) to Isar proof?
85 recdef with nested recursion: either an example or at least a pointer to the
86 literature. In Recdef/termination.thy, at the end.
87 %FIXME, with one exception: nested recursion.
89 Syntax section: syntax annotations nor just for consts but also for constdefs and datatype.
91 Appendix with list functions.
93 Move section on rule inversion further to the front, and combine
94 \subsection{Universal quantifiers in introduction rules}
95 \subsection{Continuing the `ground terms' example}
98 Minor additions to the tutorial, unclear where
99 ==============================================
109 For extensionality (in Sets chapter): prove
111 in If-expression case study (Ifexpr)
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 Partial rekursive functions / Nontermination:
129 Exercise: ?! f. !i. f i = if i=0 then 1 else i*f(i-1)
130 (What about sum? Is there one, a unique one?)
133 Better(?) sum i = fst(while (%(s,i). i=0) (%(s,i). (s+i,i-1)) (0,i))
134 Prove 0 <= i ==> sum i = i*(i+1) via while-rule
136 Possible examples/case studies
137 ==============================
139 Trie: Define functional version
140 datatype ('a,'b)trie = Trie ('b option) ('a => ('a,'b)trie option)
141 lookup t [] = value t
142 lookup t (a#as) = case tries t a of None => None | Some s => lookup s as
143 Maybe as an exercise?
145 Trie: function for partial matches (prefixes). Needs sets for spec/proof.
147 Sets via ordered list of intervals. (Isa/Interval(2))
149 propositional logic (soundness and completeness?),
150 predicate logic (soundness?),
152 Tautology checker. Based on Ifexpr or prop.logic?
153 Include forward reference in relevant section.
155 Sorting with comp-parameter and with type class (<)
157 Recdef:more example proofs:
158 if-normalization with measure function,
159 nested if-normalization,
165 Steps Towards Mechanizing Program Transformations Using PVS by N. Shankar,
166 Science of Computer Programming, 26(1-3):33-57, 1996.
167 You can get it from http://www.csl.sri.com/scp95.html
169 J Moore article Towards a ...
176 Recdef with nested recursion?
178 Extensionality: applications in
179 - boolean expressions: valif o bool2if = value
180 - Advanced datatypes exercise subst (f o g) = subst f o subst g
182 A look at the library?
187 ==============================================================