[isabelle] Reformulation question typedef


when i write

typedef larger_three = "{n :: nat. n > 3}"

definition b :: larger_three where
"b = Abs_larger_three 2"
i would like the compiler to reject this instantiation, cause 2 is not larger then 3.

My best solution for this is that the compiler behaves like it accepts it, but secretly makes it undefined:

typedef larger_three = "{n :: nat. n > 3}"

constructNr :: "nat => larger_three"

constructNr_def:  "constructNr k ≡ if k > 3 then Abs_larger_three k else undefined"

definition b :: larger_three where
"b = constructNr 2"

lemma "b = undefined"
by (simp add: b_def constructNr_def)

I would like that the compiler immediately catches this as error, and not behaving as if accepting it and throwing it to undefined.

Can you help me?

Thank you

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.