doc-src/TutorialI/todo.tobias
 author huffman Thu Apr 19 10:49:47 2012 +0200 (2012-04-19) changeset 47579 28f6f4ad69bf parent 12492 a4dd02e744e0 permissions -rw-r--r--
tuned lemmas (v)image_id;
removed duplicate of vimage_id
```     1 Implementation
```
```     2 ==============
```
```     3
```
```     4 Add map_cong?? (upto 10% slower)
```
```     5
```
```     6 a simp command for terms
```
```     7
```
```     8 Recdef: Get rid of function name in header.
```
```     9 Support mutual recursion (Konrad?)
```
```    10
```
```    11 improve solver in simplifier: treat & and ! ...
```
```    12
```
```    13 better 1 point rules:
```
```    14 !x. !y. x = f y --> P x y  should reduce to  !y. P (f y) y.
```
```    15
```
```    16 it would be nice if @term could deal with ?-vars.
```
```    17 then a number of (unchecked!) @texts could be converted to @terms.
```
```    18
```
```    19 it would be nice if one could get id to the enclosing quotes in the [source] option.
```
```    20
```
```    21 More predefined functions for datatypes: map?
```
```    22
```
```    23 Induction rules for int: int_le/ge_induct?
```
```    24 Needed for ifak example. But is that example worth it?
```
```    25
```
```    26 Komischerweise geht das Splitten von _Annahmen_ auch mit simp_tac, was
```
```    27 ein generelles Feature ist, das man vielleicht mal abstellen sollte.
```
```    28
```
```    29 proper mutual simplification
```
```    30
```
```    31 defs with = and pattern matching??
```
```    32
```
```    33
```
```    34 Minor fixes in the tutorial
```
```    35 ===========================
```
```    36
```
```    37 Appendix: Lexical: long ids.
```
```    38
```
```    39 Warning: infixes automatically become reserved words!
```
```    40
```
```    41 Syntax section: syntax annotations not just for consts but also for constdefs and datatype.
```
```    42
```
```    43 Appendix with list functions.
```
```    44
```
```    45 All theory sources on the web?
```
```    46
```
```    47 Possible exercises
```
```    48 ==================
```
```    49
```
```    50 Exercises
```
```    51
```
```    52 For extensionality (in Sets chapter): prove
```
```    53 valif o norm = valif
```
```    54 in If-expression case study (Ifexpr)
```
```    55
```
```    56 Nested inductive datatypes: another example/exercise:
```
```    57  size(t) <= size(subst s t)?
```
```    58
```
```    59 insertion sort: primrec, later recdef
```
```    60
```
```    61 OTree:
```
```    62  first version only for non-empty trees:
```
```    63  Tip 'a | Node tree tree
```
```    64  Then real version?
```
```    65  First primrec, then recdef?
```
```    66
```
```    67 Ind. sets: define ABC inductively and prove
```
```    68 ABC = {rep A n @ rep B n @ rep C n. True}
```
```    69
```
```    70 Partial rekursive functions / Nontermination:
```
```    71
```
```    72 Exercise: ?! f. !i. f i = if i=0 then 1 else i*f(i-1)
```
```    73 (What about sum? Is there one, a unique one?)
```
```    74
```
```    75 Exercise
```
```    76 Better(?) sum i = fst(while (%(s,i). i=0) (%(s,i). (s+i,i-1)) (0,i))
```
```    77 Prove 0 <= i ==> sum i = i*(i+1) via while-rule
```
```    78
```
```    79 Possible examples/case studies
```
```    80 ==============================
```
```    81
```
```    82 Trie: Define functional version
```
```    83 datatype ('a,'b)trie = Trie ('b option) ('a => ('a,'b)trie option)
```
```    84 lookup t [] = value t
```
```    85 lookup t (a#as) = case tries t a of None => None | Some s => lookup s as
```
```    86 Maybe as an exercise?
```
```    87
```
```    88 Trie: function for partial matches (prefixes). Needs sets for spec/proof.
```
```    89
```
```    90 Sets via ordered list of intervals. (Isa/Interval(2))
```
```    91
```
```    92 propositional logic (soundness and completeness?),
```
```    93 predicate logic (soundness?),
```
```    94
```
```    95 Tautology checker. Based on Ifexpr or prop.logic?
```
```    96 Include forward reference in relevant section.
```
```    97
```
```    98 Sorting with comp-parameter and with type class (<)
```
```    99
```
```   100 Recdef:more example proofs:
```
```   101  if-normalization with measure function,
```
```   102  nested if-normalization,
```
```   103  quicksort
```
```   104  Trie?
```
```   105
```
```   106 New book by Bird?
```
```   107
```
```   108 Steps Towards Mechanizing Program Transformations Using PVS by N. Shankar,
```
```   109       Science of Computer Programming, 26(1-3):33-57, 1996.
```
```   110 You can get it from http://www.csl.sri.com/scp95.html
```
```   111
```
```   112 J Moore article Towards a ...
```
```   113 Mergesort, JVM
```
```   114
```
```   115
```
```   116 Additional topics
```
```   117 =================
```
```   118
```
```   119 Recdef with nested recursion?
```
```   120
```
```   121 Extensionality: applications in
```
```   122 - boolean expressions: valif o bool2if = value
```
```   123 - Advanced datatypes exercise subst (f o g) = subst f o subst g
```
```   124
```
```   125 A look at the library?
```
```   126 Map.
```
```   127
```
```   128 Prototyping?
```
```   129
```
```   130 ==============================================================
```
{"ft_lang_label":"__label__en","ft_lang_prob":0.6401232,"math_prob":0.885978,"size":3081,"snap":"2019-35-2019-39","text_gpt3_token_len":797,"char_repetition_ratio":0.10919727,"word_repetition_ratio":0.003984064,"special_character_ratio":0.3378773,"punctuation_ratio":0.17252396,"nsfw_num_words":0,"has_unicode_error":false,"math_prob_llama3":0.9767874,"pos_list":[0],"im_url_duplicate_count":[null],"WARC_HEADER":"{\"WARC-Type\":\"response\",\"WARC-Date\":\"2019-08-18T13:42:02Z\",\"WARC-Record-ID\":\"<urn:uuid:154c06be-5e25-444a-9a7f-f045384a94dd>\",\"Content-Length\":\"22126\",\"Content-Type\":\"application/http; msgtype=response\",\"WARC-Warcinfo-ID\":\"<urn:uuid:5eb5cf51-ed13-4719-a1f8-b03d69b0688a>\",\"WARC-Concurrent-To\":\"<urn:uuid:3f196436-23ce-4699-a66a-b8949653e1f0>\",\"WARC-IP-Address\":\"131.159.46.82\",\"WARC-Target-URI\":\"http://isabelle.in.tum.de/repos/isabelle/file/28f6f4ad69bf/doc-src/TutorialI/todo.tobias\",\"WARC-Payload-Digest\":\"sha1:SVVGDRMDKDS6R3L7SN6OMCYDF7R2OUTX\",\"WARC-Block-Digest\":\"sha1:GRDNFM5ZZ7YNUYKAY4O2AN5ZTFATXTTE\",\"WARC-Identified-Payload-Type\":\"application/xhtml+xml\",\"warc_filename\":\"/cc_download/warc_2019/CC-MAIN-2019-35/CC-MAIN-2019-35_segments_1566027313889.29_warc_CC-MAIN-20190818124516-20190818150516-00521.warc.gz\"}"}