Isabelle: variable x occurs on right hand side only

Question

inductive S :: "alpha list ⇒ bool" where
 empty : "S []" | 
 step1 : "S w ⟹ S (a # w @ [b])" |
 step2 : "⟦S w1; S w2⟧ ⟹ S (w1 @ w2)"

inductive T :: "alpha list ⇒ bool" where
 empty : "T []" |
 step : "⟦T w1; T w2⟧ ⟹ T (w1 @ [a] @ w2 @ [b])"

fun balanced :: "nat ⇒ alpha list ⇒ bool" where
"balanced 0 w = S w"  |
"balanced (Suc 0) w = S (a # w)" |
"(balanced n w = S (a # m @ w)) ⟹ (balanced (Suc n) w = S (a # a # m @ w))"

I am trying to write a function balanced so that balanced n wis true if and only if S (an @ w) where an is list that contains n number of the same alphalist. For the third equation of the function"(balanced n w = S (a # m @ w)) ⟹ (balanced (Suc n) w = S (a # a # m @ w))" I get the error "Variable "m" occurs on right hand side only:" even though there is m in the left side. The only solution that I can think of is write the function in another way but cannot think of how at the moment.

Answer 1

As it stands, your definition doesn't make much sense. You're trying to fish out m from the result of balanced n w, even though the type returned is a bool. You can't turn that into the specific argument that was passed to S, just like you can't un-mince meat back into a walking chicken.

If you really wanted to say "if there is some m that satisfies this, then use that m", then you need an explicit existential quantifier, and then get your hands on the witness as an actual expression with the SOME operator. I wouldn't recommend that, though.

What you're actually trying to say, I believe, is balanced n w = S (replicate n a @ w). This definition is accepted without issues (if I remembered the argument order of replicate correctly), but for the underlying problem of proving these two grammars equivalent, the definition won't help you.

The point of introducing the balanced intermediate notion in this proof is that you don't have to map a derivation tree to another derivation tree directly. What you actually want is a function that processes the input w recursively, left to right, and doesn't refer to either S or T at all. In other words, you want an algorithm that will decide whether the grammar matches an input. balanced n w = S (replicate n a @ w) is then a good thing to prove about it by induction.

Since this is an exercise (from prog-prove and/or concrete semantics, if anyone's following along at home), I won't just show you the recursive definition right now, though let me know if you get stuck with trying to get it to work.