Hallo,
i want to create a datatype that allows me to write functions from a nat subset
to another nat subset.
for example i wanna be able to write:
definition f: {1,2,3} => {4,5}
1 -->4, 2-->4, 3-->5
or another one:
definition g : {6,8} => {2,3,4}
So the thing i want to somehow parametrize is "which subset of the nat im
using each time as domain and range" ,
I thought about creating a new datatype : 'a nat
The problem with this is that 'a is instantiated with datatypes, and not sets
like {1,2,3}.
Following solutions are bad:
1. Everytime i want declare a new function, i have to declare by "typedef" the
nat subsets i want as domain and range
2. definition f : "nat => nat" where
"f x = (if x : {1,2,3} then .... else undefined)
This second approach is bad, cause i dont want the domain to be decided as late
as the second line of the declaration, cause after this i want to be able to
program a selector "domain f"
that returns me the domain of f, thats why i want the domain of f to be somehow
incapsulated (parametrized) in the first line "f: nat =>nat " so that i can use
it later.
What would you do in this situation?
Many thanks!
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
