Stream: Beginner Questions

Topic: Simplifying "(if 1 = 0 then P else Q)" to Q

Chengsong Tan (Nov 14 2023 at 16:36):

Hi,

I was trying to prove a lemma with a subgoal whose conclusion is of the form (if 1 = 0 then P else Q),
where P and Q are some (computable but) huge boolean predicates. I would like to convert that goal into just Q.
I am not sure what's the neatest way to do that single change on the goal state.
I tried to prove some lemma like

lemma if_simp1: shows "(if 1 = 0 then P else Q) = Q"
  oops

and then use apply (subst if_simp1) to do that rewriting,
but apparently that does not hold since P/Q might not terminate etc.
How do I restrict the lemma to the terminating case?
Alternatively, how can I do a single step rewriting (if 1 = 0 then P else Q) ----> Q?

Here's a (contrived) MWE:
IfExample.thy

Best wishes,
Chengsong

Lukas Stevens (Nov 14 2023 at 16:46):

How about apply (subst if_not_P)?

Chengsong Tan (Nov 14 2023 at 17:05):

Lukas Stevens said:

How about apply (subst if_not_P)?

Thank you!

Inspired by your answer I also realised that
find_theorems "if False then _ else _ "
gives me the desired theorem.

Last updated: Apr 28 2024 at 01:11 UTC