[isabelle] Reformulation question typedef



Hi,

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}"
sorry

consts
constructNr :: "nat => larger_three"

defs
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.