Email Gateway (Aug 19 2022 at 13:29): Email Gateway (Aug 19 2022 at 13:29):From: "Roger H." <s57076@hotmail.com>
Hi,
how can i make "f ∪ g"?
definition f :: "nat ⇀ nat" where
"f = [1 ↦ 0, 2 ↦ 5]"
definition g :: "nat ⇀ nat" where
"g = [3 ↦ 7, 4 ↦ 9]"
definition f_union_g :: "nat ⇀ nat" where
"f_union_g = [1 ↦ 0, 2 ↦ 5, 3 ↦ 7, 4 ↦ 9]"
So how should i define f_union_g?
And generally in what class.thy can i find such operators on partial functions?
Thank you!
Email Gateway (Aug 19 2022 at 13:29):From: John Wickerson <johnwickerson@cantab.net>
Hi Roger,
For this you want "f ++ g". Such things are defined in Map.thy -- see here:
http://isabelle.in.tum.de/library/HOL/HOL/Map.html
Best wishes,
John
Email Gateway (Aug 19 2022 at 13:29):From: Andrew Boyton <Andrew.Boyton@nicta.com.au>
It might be useful to point out that find_consts can be useful for times like this. It's like a very simplified version of Hoogle [1].
You need to generalise what you are searching for, (not nat ⇀ nat but 'a ⇀ 'b), but it finds what you are after.
find_consts "('a ⇀ 'b) ⇒ ('a ⇀ 'b) ⇒ 'a ⇀ 'b"
gives
searched for:
"('a ⇀ 'b) ⇒ ('a ⇀ 'b) ⇒ 'a ⇀ 'b"
found 2 constant(s):
Quickcheck_Exhaustive.cps_plus ::
"(('a ⇒ term list option)
⇒ term list option)
⇒ (('a ⇒ term list option)
⇒ term list option)
⇒ ('a ⇒ term list option)
⇒ term list option"
Map.map_add ::
"('a ⇒ 'b option)
⇒ ('a ⇒ 'b option) ⇒ 'a ⇒ 'b option"
The second, Map.map_add is the one you want, and you can then command click on it to give the definition. ("Map_add" is "++".)
Note that map_add does right overloading, and is thus not an associative operator.
Regards
Andrew
[1]: http://www.haskell.org/hoogle/
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
Email Gateway (Aug 19 2022 at 13:29):From: Tjark Weber <webertj@in.tum.de>
Note that there is a theorem map_add_assoc that proves associativity of
map_add. Perhaps you meant to write that map_add is not commutative.
Best,
Tjark
Last updated: Apr 25 2024 at 12:23 UTC