34 !x. !y. x = f y --> P x y should reduce to !y. P (f y) y. |
34 !x. !y. x = f y --> P x y should reduce to !y. P (f y) y. |
35 |
35 |
36 use arith_tac in recdef to solve termination conditions? |
36 use arith_tac in recdef to solve termination conditions? |
37 -> new example in Recdef/termination |
37 -> new example in Recdef/termination |
38 |
38 |
39 a tactic for replacing a specific occurrence: |
|
40 apply(subst [2] thm) |
|
41 |
|
42 it would be nice if @term could deal with ?-vars. |
39 it would be nice if @term could deal with ?-vars. |
43 then a number of (unchecked!) @texts could be converted to @terms. |
40 then a number of (unchecked!) @texts could be converted to @terms. |
44 |
41 |
45 it would be nice if one could get id to the enclosing quotes in the [source] option. |
42 it would be nice if one could get id to the enclosing quotes in the [source] option. |
46 |
43 |
58 |
55 |
59 |
56 |
60 Minor fixes in the tutorial |
57 Minor fixes in the tutorial |
61 =========================== |
58 =========================== |
62 |
59 |
63 1/2 no longer abbrevs for Suc. |
|
64 Warning: needs simplification to turn 1 into Suc 0. arith does so |
|
65 automatically. |
|
66 |
|
67 recdef: failed tcs no longer shown! (sec:Recursion over nested datatypes) |
|
68 say something about how conditions are proved? |
|
69 No, better show failed proof attempts. |
|
70 |
|
71 Advanced recdef: explain recdef_tc? No. Adjust recdef! |
|
72 |
|
73 Adjust FP textbook refs: new Bird, Hudak |
|
74 Discrete math textbook: Rosen? |
|
75 |
|
76 adjust type of ^ in tab:overloading |
|
77 |
|
78 an example of induction: !y. A --> B --> C ?? |
|
79 |
|
80 Explain type_definition and mention pre-proved thms in subset.thy? |
|
81 -> Types/typedef |
|
82 |
|
83 Appendix: Lexical: long ids. |
60 Appendix: Lexical: long ids. |
84 |
61 |
85 Warning: infixes automatically become reserved words! |
62 Warning: infixes automatically become reserved words! |
86 |
|
87 Forward ref from blast proof of Puzzle (AdvancedInd) to Isar proof? |
|
88 |
|
89 recdef with nested recursion: either an example or at least a pointer to the |
|
90 literature. In Recdef/termination.thy, at the end. |
|
91 %FIXME, with one exception: nested recursion. |
|
92 |
63 |
93 Syntax section: syntax annotations not just for consts but also for constdefs and datatype. |
64 Syntax section: syntax annotations not just for consts but also for constdefs and datatype. |
94 |
65 |
95 Appendix with list functions. |
66 Appendix with list functions. |
96 |
67 |
97 All theory sources on the web? |
68 All theory sources on the web? |
98 |
|
99 |
|
100 Minor additions to the tutorial, unclear where |
|
101 ============================================== |
|
102 |
|
103 unfold? |
|
104 |
|
105 |
69 |
106 Possible exercises |
70 Possible exercises |
107 ================== |
71 ================== |
108 |
72 |
109 Exercises |
73 Exercises |