Hi Dwi, I would expect that a
ASM_REWRITE_TAC[] does the trick. It would take the assumptions as a rewrite and use it to simplify the goal. In this case, it should simplify the goal to "!s0. Next s0 x = Next s0 x" which is solved thanks to reflexivity. A problem might be free type variables, i.e. that the type of "x" in the assumption and "Next s0 x" in the goal don't match. This seems not to be the case in your example, though. I recommend reading up on REWRITE_TAC and ASM_REWRITE_TAC, as well as ASM_SIMP_TAC and similar stuff in the description and reference manuals. Cheers Thomas On 25.04.2017 09:24, Dwi Teguh Priyantini wrote: > Hi, > > I have a question, > What tactic I should use to solve this problem? > > !s0. flipslv (flipslv (Next s0 x)) = Next s0 x > ---------------------------------------------- > x. flipslv (flipslv x) = x > > The flipslv function is just simply reverses x which is a slv datatype. > > The datatype declaration is written as bellow: > val _ = Hol_datatype` > slv = Single of stdl > | Next of stdl => slv > `; > > And I also have this definitions before: > val flipnext_def = Define `(flipnext (Next a b) c = flipnext b (Next a > c)) > /\ (flipnext (Single a) c = Next a c)`; > > val flipslv_def = Define `(flipslv (Next a b) = flipnext b (Single a)) > /\ (flipslv (Single a) = (Single a))`; > > > I think the pattern has matched (by replace "x" with "Next s0 x"), but I > don't know how to do. Could anyone help me? > Thank you. > > ------------------------------------------------------------------------------ Check out the vibrant tech community on one of the world's most engaging tech sites, Slashdot.org! http://sdm.link/slashdot _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
