isauser (Nov 26 2025 at 09:07): isauser (Nov 26 2025 at 09:07):I'm trying to prove the following lemma:
datatype alpha = a | b
inductive S :: "alpha list ⇒ bool" where
emp: "S []" |
aSb: "S w ⟹ S (a # w @ [b])" |
SS: "S w1 ⟹ S w2 ⟹ S (w1 @ w2)"
lemma "S [a] ⟹ False"
However I've had no success. A proof by cases or by induction (proof(cases rule: S.cases), proof(induction rule: S.induct)) doesn't seem to work - Isabelle generates goals that are impossible to prove. I suspect this is ultimately failing because technically S [a] could be made via S [a] ⟹ S [] ⟹ S ([a] @ []) = S [a], and to prove this construction impossible you first have to proof S [a] impossible - a vicious cycle.
I would be thankful for any tips and pointers for solving this.
Kevin Kappelmann (Nov 26 2025 at 09:11):Try induction "[a]" rule: S.induct
isauser (Nov 26 2025 at 09:21):Thank you! This worked very well. I suppose I should try to better understand all the various forms of induction, it's not the first time where changing the shape of induction made something from impossible to easy to prove.
Alex Hyman (Nov 26 2025 at 15:30):Removed - wrong conversation.
Last updated: Dec 08 2025 at 08:34 UTC