How to fix the bug of No code equations for star in isabelle

user_13276122 0
Viewed 43
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)"

I try to definition the semantics of regular expression. But when I test the Star function, it warns that No code equations for star. How to fix it?

isabelle
1 Answers

The error message tells you that Isabelle does not know how to evaluate star. Given that the set in infinite, you will not be able to define a function that returns all the possible values.

A possible workaround is to use a different evaluation, namely the simplifier:

value [simp] "sem_reg (Star (a::nat regexp)) v"
value [simp] "sem_reg Dot (1::nat)"

This avoids relying on the code generator. But, exactly as you would expect, star is not evaluated.

user_128242070
Related