false value "true" (* it has value true with type my_bool *) fun conj :: "my_bool ⇒ my_bool ⇒ my_bool" where "conj true true = true"

Question

我正在尝试这样做。

datatype my_bool = true | false
value "true" (* it has value true with type my_bool *)

fun conj :: "my_bool ⇒ my_bool ⇒ my_bool" where 
"conj true true = true" |
"conj _ _ = false"

lemma "conj true true = true"
  apply (simp only: conj_def)

但我得到了错误。

Undefined fact: "conj_def"⌂

我明白错误，但不明白为什么我不能像定义那样应用一个单步函数。这在函数中是可能的吗？