问如何解决伊莎贝尔星无码方程的缺陷

EN

theory AReg imports Main  begin

datatype ('v)regexp = Alp 'v| Alter "('v) regexp" "('v) regexp" (infix "||" 55) | Dot (".")|
                      Star "'v regexp" ("_*") | Plus "('v) regexp"("_+") | Ques "('v) regexp"("_?") 
              

inductive_set star :: "'a list set \<Rightarrow> 'a list set" 
  for r :: "'a list set" where
"[] \<in> star r"|
"x \<in> r\<Longrightarrow> x@x \<in> star r"

primrec sem_reg :: "('a) regexp \<Rightarrow> 'a \<Rightarrow> 'a list set" where 
"sem_reg (Alp a) v = (if a = v then {[v]} else {})"|
"sem_reg (Dot) a= {[a]}"|
"sem_reg (v1||v2) a = (sem_reg v1 a) \<union> (sem_reg v2 a)"|
"sem_reg (Star a) v = star (sem_reg a v)"|
"sem_reg (Plus a) v = star (sem_reg a v) - {[]}"|
"sem_reg (Ques v) a = {[]} \<union> (sem_reg v a)"

value "sem_reg (Star a) v"
value "sem_reg Dot (1::nat)"