### Abstract

The article provides a collection of experimental general-purpose proof methods for the object logic Isabelle/HOL of the formal proof assistant Isabelle. The methods in the collection offer functionality that is similar to certain aspects of the functionality provided by the standard proof methods of Isabelle that combine classical reasoning and rewriting, such as the method auto, but use a different approach for rewriting. More specifically, these methods allow for the side conditions of the rewrite rules to be solved via intro-resolution.

### License

BSD License

### History

January 7, 2022
  added a switch for backtracking (revision 241da1cdeabf)

### Topics

- Tools

### Session Conditional_Simplification

- CS_Tools
- IHOL_CS
- Reference_Prerequisites
- CS_Reference

### Used by

- Category Theory for ZFC in HOL I: Foundations: Design Patterns, Set Theory, Digraphs, Semicategories

## Cite

×

Conditional_Simplification-AFP

    @article{Conditional_Simplification-AFP,
      author  = {Mihails Milehins},
      title   = {Conditional Simplification},
      journal = {Archive of Formal Proofs},
      month   = {September},
      year    = {2021},
      note    = {\url{https://isa-afp.org/entries/Conditional_Simplification.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Oct 5, 2021 : Isabelle2021
- Sep 14, 2021 : Isabelle2021