I’m new to isabelle and I wanted to use something like automatically simplifying a propositional expression for educational purposes by showing the steps and rules applied. I’m guessing it’s a decidable problem.

For example, enter the expression: ¬P ∨ (P ∧ ¬Q)

And show the steps until you reach: ¬P ∨ ¬Q

Of course, I’ll use it with more complex expressions and at first I don’t know the result. I wanted Isabelle to arrive at the result alone.

I just needed a simple example of how to do it.