CODEWITHSUNDEEP
isabelle
Dominique Unruh
Dominique Unruh

Reputation: 1276

Isabelle simplifier introduces case distinction for if-statement (why? when?)

If I apply the simp-method to a goal containing an if-expression, the simplifier automatically introduces a case distinction:

lemma "undefined (if x then True else False)"
  apply simp

This gives the goal:

(x ⟶ undefined True) ∧ (¬ x ⟶ undefined False)

My question is: How is the simplifier told to do this? I could find a simplifier-rule for if that would conceivable lead to this behavior, nor a simproc. How can I get a similar behavior for other if-like constants?

Upvotes: 2

Views: 390

Answers (1)

larsrh
larsrh

Reputation: 2659

That feature is enabled by the splitter. The simplifier itself is a big loop that not only performs rewriting, but also afterwards a variety of other things, before it starts rewriting again.

For if, the relevant split rules are if_splits:

?P (if ?Q then ?x else ?y) = ((?Q ⟶ ?P ?x) ∧ (¬ ?Q ⟶ ?P ?y))
?P (if ?Q then ?x else ?y) = (¬ (?Q ∧ ¬ ?P ?x ∨ ¬ ?Q ∧ ¬ ?P ?y))

The first split rule applies to an occurrence of if _ then _ else _ in the conclusion, the latter for an occurrence in a premise. (Both rules are available separately as if_split and if_split_asm.)

case constants for data types have similar rules, e.g. bool.splits:

?P (case ?bool of True ⇒ ?f1.0 | False ⇒ ?f2.0) =
  ((?bool = True ⟶ ?P ?f1.0) ∧ (?bool = False ⟶ ?P ?f2.0))
?P (case ?bool of True ⇒ ?f1.0 | False ⇒ ?f2.0) =
  (¬ (?bool = True ∧ ¬ ?P ?f1.0 ∨ ?bool = False ∧ ¬ ?P ?f2.0))

Rules can be declared as split rules by annotating them with [split].

More information can be found in §9.3.1 of the reference manual. The whole subsection §9.3 explains the simplifier in more detail (although admittedly much knowledge about the simplifier is basically "ancient wisdom").

Upvotes: 2

Related Questions