Hi, I have an UPDATE function simplified as:
((a =+ x) ((b =+ y) ((a =+ z) f))) or some other format, where updating on the same element is separated by updating on other elements: ((a =+ x) ((b =+ y) ... ((a =+ z) f) ...)) I wan to remove the redundant inner updates, but when I use UPDATE_EQ,APPLY_UPDATE_ID,APPLY_UPDATE_THM to simplify the term, it doesn't change. One solution I can think of is to decompose the term, remove the inner updates on the same element, construct another term, and prove the new term equals to the original term, and do a rewrite. Before I start writing this function, I'd like to ask if there is anything there already available in HOL to do the work. Thanks. Lu ------------------------------------------------------------------------------ _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
