Hi, if you don't like stateful tactics, you should also have a look at the library "DatatypeSimps". Moreover, it often helps me to turn off pretty printing of case-expressions via
set_trace "pp_cases" 0 You need rewriting of the "list_CASE" and equality of chars. So, your goal should also be solved via SIMP_TAC std_ss [listTheory.list_case_def, stringTheory.CHR_11] If you want it higher level use the string and list simpsets: SIMP_TAC (list_ss++stringSimps.STRING_ss) [] or use the DatatypeSimps, which work for other types as well: SIMP_TAC (std_ss++stringSimps.STRING_ss++DatatypeSimps.type_rewrites_ss([``:'a list``])) [] Thomas On 04/11/14 04:31, Michael Norrish wrote: > On 04/11/14 13:33, ＂f~鳓ぁぇ wrote: >> Hi, >> I want to prove a goal like this: >> `case "d" of "u" =>1 |"s" =>2|"d" >> =>3 >> |"p" =>4` >> Is there a tactic which can match "d" with the branch "d" and then execute >> this >> branch. > SIMP_TAC (srw_ss()) [] > > or > > SRW_TAC[][] > > should both work on this sort of goal. > > Michael > > > ________________________________ > > The information in this e-mail may be confidential and subject to legal > professional privilege and/or copyright. National ICT Australia Limited > accepts no liability for any damage caused by this email or its attachments. > > ------------------------------------------------------------------------------ > _______________________________________________ > hol-info mailing list > [email protected] > https://lists.sourceforge.net/lists/listinfo/hol-info ------------------------------------------------------------------------------ _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
