Email Gateway (Aug 22 2022 at 16:29): Email Gateway (Aug 22 2022 at 16:29):From: "zhaoyongwang@gmail.com" <zhaoyongwang@gmail.com>
Dear all,
I am trying to use functor in Isabelle. Anyone has some examples of the "functor" keyword in Isabelle/HOL?
Thanks.
Yongwang
Email Gateway (Aug 22 2022 at 16:29):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Yongwang,
What do you want to achieve by using "functor"? The functor command in Isabelle is in
Isabelle2017 only used by the quotient/lifting/transfer packages. You can register a map
functor for your own types with the functor command. Here is an abstract example for a
binary type constructor with a covariant ('a) and a contravariant ('b) argument.
typedecl ('a, 'b) F
consts map_F :: "('a => 'a') => ('b' => 'b) => ('a, 'b) F => ('a', 'b') F"
functor map_F <proof of the functor laws>
Hope this helps,
Andreas
Email Gateway (Aug 22 2022 at 16:30):From: "zhaoyongwang@gmail.com" <zhaoyongwang@gmail.com>
Thanks, Andreas. I am studying functional programming in Isabelle/HOL, so tried to use functors.
According to your suggestions, I have the following spec. My question is how I can use the functor maptree now? Is there something new with "maptree" now?
datatype 'a tree = Leaf 'a | Node "'a tree" "'a tree"
primrec maptree :: "('a ⇒ 'b) ⇒ 'a tree ⇒ 'b tree"
where "maptree f (Leaf a) = Leaf (f a)" |
"maptree f (Node l r) = Node (maptree f l) (maptree f r)"
lemma lmmt1: "(maptree f ∘ maptree g) x = (maptree (f ∘ g)) x"
apply(induct x)
using maplist2.simps by auto
lemma lmmt2: "(maptree id) x = id x"
apply(induct x)
using maptree.simps by auto
functor maptree
proof
show "⋀f g x. (maptree f ∘ maptree g) x = maptree (f ∘ g) x"
using lmmt1 by simp
show "maptree id = id"
using lmmt2 by blast
qed
Yongwang
Email Gateway (Aug 22 2022 at 16:30):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Yongwang,
First of all, the datatype package already generates a map function for your tree, which
is called map_tree. You also get the functor properties proven, the lemmas are called
tree.map_id and tree.map_comp.
As I said, the functor command is currently only used by lifting/transfer/quotient. So
unless you do not plan to define a quotient type over your trees or to lift a type
quotient through the tree type, the functor declaration does not have any effect for you.
Andreas
Email Gateway (Aug 22 2022 at 16:30):From: Lars Hupel <hupel@in.tum.de>
According to your suggestions, I have the following spec. My question is how I can use the functor maptree now? Is there something new with "maptree" now?
datatype 'a tree = Leaf 'a | Node "'a tree" "'a tree"
primrec maptree :: "('a ⇒ 'b) ⇒ 'a tree ⇒ 'b tree"
where "maptree f (Leaf a) = Leaf (f a)" |
"maptree f (Node l r) = Node (maptree f l) (maptree f r)"
The "maptree" function already exists and is called "map_tree". Such
functions are automatically generated by the "datatype" command. It also
proves the relevant functor lemmas (as you did manually).
functor maptree
proof
show "⋀f g x. (maptree f ∘ maptree g) x = maptree (f ∘ g) x"
using lmmt1 by simp
show "maptree id = id"
using lmmt2 by blast
qed
Unless you plan on using quotient types, there's no point in registering
your custom map function as a "functor". It is a mere technical detail.
Cheers
Lars
Last updated: Apr 26 2024 at 12:28 UTC