Email Gateway (Aug 18 2022 at 11:47): Email Gateway (Aug 18 2022 at 11:47):From: Jesper Bengtson <jesper.bengtson@it.uu.se>
Greetings
I am trying out the new functions package which shipped with Isabelle 2007. The
function I am trying to create a function for parallel substitution where I
want to reason about the domain and range of the substitution at top level,
i.e. I want to be able to write P[xvec:=Tvec] where xvec and Tvec are lists
rather than P[S] where S is a tuple list. The problem with this approach is
that the function is only defined if the lists xvec and Tvec are of the same
length. I tried writing the following function:
function (domintros) substName :: "name => name list => trm list => trm"
("_[_:=_]" [100, 100, 100] 100)
where
"substName a [] [] = (Name a)"
| "length xs = length Ts ==> substName a (x#xs) (T#Ts) = (if a = x then T else
(substName a xs Ts))"
But at the top of the proof obligations I get a goal which seems pretty
unsolvable to me:
/\P x. [|a. x = (a, [], []) ==> P;
/\xs Ts a xa T. [|length xs = length Ts;
x = (a, xa # xs, T # Ts)|] ==> P|]
==> P
It seems to be some sort of completeness condition for the function.
I've read through the guide of the function package and it is a bit unclear if
it is possible to do what I'm trying to do. There are of course work arounds,
but this would be nicer.
Many thanks.
/Jesper
Email Gateway (Aug 18 2022 at 11:47):From: Alexander Krauss <krauss@in.tum.de>
Jesper,
I am trying out the new functions package which shipped with Isabelle 2007. The
function I am trying to create a function for parallel substitution where I
want to reason about the domain and range of the substitution at top level,
i.e. I want to be able to write P[xvec:=Tvec] where xvec and Tvec are lists
rather than P[S] where S is a tuple list. The problem with this approach is
that the function is only defined if the lists xvec and Tvec are of the same
length. I tried writing the following function:function (domintros) substName :: "name => name list => trm list => trm"
("_[_:=_]" [100, 100, 100] 100)
where
"substName a [] [] = (Name a)"
| "length xs = length Ts ==> substName a (x#xs) (T#Ts) = (if a = x then T else
(substName a xs Ts))"
This is not partiality in the sense of the function package. The special
support with domain predicate, domintros and all that is for functions
which have a possibly nonterminating recursion. Here, you simply want to
omit some cases and leave them undefined in some sense.
What you would do is simply
function (sequential) substName :: "name => name list => trm list => trm"
("_[_:=_]" [100, 100, 100] 100)
where
"substName a [] [] = (Name a)"
| "substName a (x#xs) (T#Ts) =
(if a = x then T else (substName a xs Ts))"
The (sequential) option will add the missing cases and map them to the
unspecified constant "undefined".
You would only need section 7 from the function tutorial if you function
had a recursion that could fail to terminate.
But at the top of the proof obligations I get a goal which seems pretty
unsolvable to me:/\P x. [|a. x = (a, [], []) ==> P;
/\xs Ts a xa T. [|length xs = length Ts;
x = (a, xa # xs, T # Ts)|] ==> P|]
==> PIt seems to be some sort of completeness condition for the function.
Yes. And it is unsolvable, because your equations are incomplete. The
(sequential) option will add the remaining patterns, and you get a
better proof obligation. (solvable with the usual "by pat_completeness
auto"). Or, you simply use "fun", which has (sequential) implicit and
does all proofs for you...
Cheers,
Alex
Email Gateway (Aug 19 2022 at 11:13):From: "Roger H." <s57076@hotmail.com>
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:
Everytime i want declare a new function, i have to declare by "typedef" the nat subsets i want as domain and range
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!
Last updated: Nov 21 2024 at 12:39 UTC