For some purpose, I want to get the smallest length of element in ('a list set) as the InitalState, and the whole set as the FinalState.
But I don't know how to achieve this function and proof.
definition initState :: "v list set\<Rightarrow> 'v list set" where
"initState vset = {x. x\<in>vset \<and> length x \<le> 1}"
This code is wrong.
First, find out what the smallest length is.
definition "minlen vset ≡ Min (length ` vset)"
Use Inf instead of Max if your set can be infinite.
Then pick out a minimum-length element using a description (@ or Eps)
definition "initState vset ≡ @x. x∈vset ∧ length x = minlen vset"
I suspect there may be a better way to define your state space, however: descriptions can be tricky to work with.