Email Gateway (Aug 22 2022 at 20:30): Email Gateway (Aug 22 2022 at 20:30):From: Christopher Hoskin <christopher.hoskin@gmail.com>
This feels like a very stupid question, but I've been staring at it
all afternoon, and can't see the answer.
I'm trying to show that a commutative additive group is a module over
the integers via the map which takes an integer and an element of
class ab_group_add and maps it to an element of class ab_group_add in
the natural way i.e. so that
(0,a) -> 0
(n,a) -> a + (n-1,a) (for n>0)
(-n,a) -> - (n,a) (for n>0).
The closest I've managed to get is:
context ab_group_add begin
primrec natscalar :: "nat ⇒ 'a ⇒ 'a" (infix "∙⇩N" 80) where
natscalar_0: "0∙⇩Na = 0"
| natscalar_Suc: "Suc n ∙⇩N a = a + n∙⇩Na"
function scalar :: "int ⇒ 'a ⇒ 'a" (infix "∙⇩Z" 80) where
"n≥0 ⟹ n∙⇩Za = nat(n)∙⇩Na"
| "¬n≥0 ⟹ n∙⇩Za = - (nat(abs(n))∙⇩Na)"
by auto
but I'm then unable to see how to prove even the simplest equation
e.g. "1∙⇩Za = a"
Possibly a function is the wrong way do do this?
Ultimately I want to show:
interpretation ab_group_add: module scalar
Please can someone offer some pointers?
Thanks.
Christopher
Email Gateway (Aug 22 2022 at 20:31):From: Christopher Hoskin <christopher.hoskin@gmail.com>
Thanks, in the end I did this, which seems to work:
context ab_group_add begin
primrec natscalar :: "nat ⇒ 'a ⇒ 'a" (infix "∙⇩N" 80) where
natscalar_0: "0∙⇩Na = 0"
| natscalar_Suc: "Suc n ∙⇩N a = a + n∙⇩Na"
definition scalar :: "int ⇒ 'a ⇒ 'a" (infix "∙⇩Z" 80) where
"scalar n a = (if n≥0 then nat(n)∙⇩Na else - (nat(abs(n))∙⇩Na))"
Christopher
Email Gateway (Aug 22 2022 at 20:35):From: Akihisa Yamada <akihisayamada@nii.ac.jp>
Hello Christopher,
most likely you wanted to use "fun" instead of "function".
Sometimes it's better not keep staring but look around, like functions
tutorial in Documentation panel :)
Best regards,
Akihisa
Email Gateway (Aug 22 2022 at 20:37):From: Akihisa Yamada <akihisayamada@nii.ac.jp>
Dear Christopher,
ah, I see you had to give up the fancy style of definition. Then what is
good to know is that function demands a manual termination proof, like:
function scalar :: "int ⇒ 'a ⇒ 'a" (infix "∙⇩Z" 80) where
"n≥0 ⟹ n∙⇩Za = nat(n)∙⇩Na"
| "¬n≥0 ⟹ n∙⇩Za = - (nat(abs(n))∙⇩Na)"
by auto
termination by lexicographic_order
lemma "1∙⇩Za = a" by auto
Best regards,
Akihisa
Last updated: Apr 25 2024 at 20:15 UTC