Andrés Goens (May 31 2024 at 14:25): Andrés Goens (May 31 2024 at 14:25):Hi! I'm new to Isabelle and I'm struggling to understand how to prove something about mutual inductively defined propositions. My example is a bit more complicated, but the issue is the same as with this very simple example with odd/even as mutual inductive propositions:
inductive
even :: "nat ⇒ bool" and
odd :: "nat ⇒ bool"
where
Even_Zero : "even 0" |
Odd_Suc_Even : "even n ⟹ odd (Suc n)" |
Even_Suc_Odd : "odd n ⟹ even (Suc n)"
theorem "even n ⟹ even (n + 2)"
proof
(induction rule: even_odd.induct)
When I try to do a proof by induction here (which for non-mutual inductives works for doing inversion), I get an error:
Failed to apply initial proof method⌂:
goal (1 subgoal):
1. MyTheory.even n ⟹ MyTheory.even (n + 2)
How can I do this kind of inversion? (and/or where could I read more about it?)
Lukas Stevens (May 31 2024 at 14:39):Look at the conclusion of even_odd.induct:
(Union_Find_Rank_Int.even ?x1.0 ⟶ ?P1.0 ?x1.0) ∧ (Union_Find_Rank_Int.odd ?x2.0 ⟶ ?P2.0 ?x2.0)
This can't be unified to your goal even (n + 2). You can instead use even_odd.inducts(1) to prove things about even. This theorem has a variable ?P2.0 that you don't care about so you can instantiate it with taking:
theorem "even n ⟹ even (Suc (Suc n))"
proof
(induction taking: "λx. True" rule: even_odd.inducts(1))
case Even_Zero
then show ?case
by (simp add: Even_Suc_Odd Odd_Suc_Even even_odd.Even_Zero)
next
case (Odd_Suc_Even n)
then show ?case by simp
next
case (Even_Suc_Odd n)
then show ?case
by (simp add: Odd_Suc_Even even_odd.Even_Suc_Odd)
qed
that's pretty neat (makes sense), thanks for the help!
Last updated: Dec 21 2024 at 16:20 UTC