Bob Rubbens (Mar 01 2025 at 08:55): Bob Rubbens (Mar 01 2025 at 08:55):Hey everyone, does isabelle support conditional split rules? It doesn't seem like it. In the following snippet, the simp fails to apply my split rule. (The example isn't supposed to make sense, I was just trying to see what the required syntax of split rules is)
lemma xyz [split]: "wf s ⟹ P (do_move s m) = ((fst m = snd m ⟶ P empty_state) ∧ (fst m ≠ snd m ⟶ P ([0] ⊣ A)))"
sorry
lemma abc: "wf s ⟹ do_move s (p, q) ≠ empty_state"
apply simp (* Failed to apply proof method⌂: *)
If I remove the "wf s" in xyz, the apply simp instruction applies the split rule just fine. I need the wf because some of the splits only make sense in the context of a well-formed state. Is there a way to make conditional splits work? Or am I missing some insight in that using conditional splits is a dumb idea?
Mathias Fleury (Mar 01 2025 at 09:17):based on find_theorems "_ ⟹ _" name:split I don't see any with conditions
Mathias Fleury (Mar 01 2025 at 09:18):so might be a limit of the splitter
Bob Rubbens (Mar 01 2025 at 10:03):I keep learning new ways to use find_theorems! Thank you for the clarification.
Last updated: Mar 09 2025 at 12:28 UTC