Email Gateway (Aug 19 2022 at 16:13): Email Gateway (Aug 19 2022 at 16:13):From: Buday Gergely <gbuday@karolyrobert.hu>
Hi Martin,
what is your definition of @ ? Did you get it from the Tutorial? As I mentioned it would be better to provide us a working Isabelle theory containing
theory Blabla
imports main
and all the necessary definitions so we could try it out.
Email Gateway (Aug 19 2022 at 16:13):From: Buday Gergely <gbuday@karolyrobert.hu>
Hi Martin,
You need to understand the definitions in your theory file, the ’a list datatype definition and the definition of app by primrec. Both define an infix operator (see infixr ”#” and infixr ”@”).
@ is an append operation that joins two _lists_, i.e. xs @ ys works when xs and ys are both of type ’a list for some fixed type ’a.
In the above ’a is called a type variable.
When I load your theory into Isabelle/JEdit,
primrec rotate1 :: "'a list => 'a list" where
"rotate1 [] = []" |
"rotate1 (x # xs) = xs # [x]"
Isabelle says that the second clause of the rotate1 definition has an error. You cannot write xs # [x] as the left operand should be of type ‘a but it is of type ‘a list.
Concerning your mmap definition
primrec mmap :: "'a => 'b => 'a list => 'a list" where
"mmap f [] = []" |
"mmap f ((mmap f x) # (mmap f xs)) = mmap f (x # xs)"
this is seriously broken, you exchange the left hand side of the second clause with the right hand side, for example. The correct version is
primrec mmap :: "('a => 'b) => 'a list => 'b list" where
"mmap f [] = []" |
"mmap f (x # xs) = (f x) # (mmap f xs)"
mmap’s first argument is not a scalar element of type ‘a but a function that maps from ‘a to ‘b. Since that, it produces a ‘b list from an ‘a list.
I suggest you to learn functional programming first, preferably with Standard ML as that is close to the higher order logic notation that Isabelle uses.
And please do not send many messages to the list at once.
Best Wishes
Email Gateway (Aug 19 2022 at 16:39):From: Buday Gergely <gbuday@karolyrobert.hu>
Hi,
primrec rotate1 :: "'a list => 'a list" where
"rotate1 [] = []" |
"rotate1 (x # xs) = xs @ [x]"
value "rotate1 (1 # 2 # 3 # 4 # [])"
What is the purpose of this function? I cannot figure this out from your code.
value "mmap +1 (1 # 2 # [])"
failed to parse term
I guess you want to create a function by "+1" but Isabelle does not understand this syntax.
value "map (λt. t + 1) [0,1,2]"
is the correct way to express that. The presence of space after the dot is significant.
Last updated: Apr 25 2024 at 08:20 UTC