Proof

This page lists an number of useful tactics together with a few examples that illustrate their use. We also comment on what makes a proof robust or fragile.

Rewriting and Simplification

• rw, fs, lrw, simp, ...
• srw_ss, std_ss, bool_ss, pure_ss
• ARITH_ss
• DNF_ss
• link to writing custom simpsets etc.
• EQUIV_EXTRACT_ss

Abbreviations

• qmatch{_assum,}_abbrev_tac
• qabbrev_tac
• unabbrev_all_tac
• markerTheory.Abbrev_def

Renaming

• qmatch{_assum,}_rename_tac
• qx_gen_tac
• X_CHOOSE_THEN

Matching

• qpat_abbrev_tac
• qpat_assum

Improving automation

• export rewrites
• NO_TAC, TRY, ORELSE, THEN1

ConseqConv stuff

• CONSEQ_REWRITE_CONV / CONSEQ_REWRITE_TAC
• DEPTH_CONSEQ_CONV / DEPTH_CONSEQ_CONV_TAC
• EXISTS_EQ_CONSEQ_CONV / FORALL_EQ_CONSEQ_CONV

Pairs and tuple terms

• FORALL_PROD, EXISTS_PROD, LAMBDA_PROD
• UNCURRY
• PairCases_on
• PABS_ELIM_CONV
• PABS_INTRO_CONV

Conjunctions

• conj_asm{1,2}_tac
• CONJ_ASSOC, ...

Associative/Commutative operators

• AC

Equivalence relations

• any support in simplifier?

Quantifiers

• stuff like RIGHT_FORALL_IMP_THM
• QuantHeuristics
• QUANT_INST_ss [std_qp]
• QUANT_INST_TAC

Interactive proof management

• proofManagerLib.save

computeLib

Conversions

• CONV_TAC

Style

Sanity

The Library Sanity allows to check theorems and whole theories with simple syntactic checks. For example, clashes between theorem names in different theories, dodgy variable names, forgotten or unnecessary quantification etc. can be checked.

lcsymtacs

• -, >>, ...

infix and operator rebinding

semicolons

indentation

opening theories and libraries