Has this generalization of Turing machines studied before? Introduction

Hello, I'm designing a generalized model of Turing machines for a formalization in MIZAR. Mizar needs some concrete objects to work with, so I spent some time figuring out how the "tape" of a Turing machine could be defined since that part is usually left out when introducing Turing machines.
After some thinking I concluded it would be best to use graphs, so I define a "Turing Space" $T$ as a function from an cardinal $C$ to graphs. A position $p$ in the Turing Space is then defined as a function from the cardinal into the vertex sets of these graphs, so that for $c\in C$, $p.c$ is a vertex of $T.c$. From this basis one can built transition functions and so forth.

Examples

Given a double ray (a path graph that is infinite in both directions) $R$ and a positive integer $k$, the function $f_k:k\ni i\mapsto R$ (defined on $\{0,\ldots,k-1\}$) would be a Turing space describing the bands of a $k$-band TM.
Given a positive integer $d$, set $E_d:=\{\{a,b\}:a,b\in\mathbb{Z}^d,\sum|a_i-b_i|=1\}$ and graph $G_d=(\mathbb{Z}^d, E_d)$, this is the grid on $\mathbb{Z}^d$. Now the function $g_d:\{0\}\ni i\mapsto G_d$ describes the hyperspace of a $d$-dimensional TM.
These two examples are of course quite different, as the first has $k$ pointers, that can move in 3 directions (left, right, stay) each, and the second has one pointer that can move in $2d+1$ directions. That they are nevertheless computational equivalent (because they are Turing-complete) is well known. Also both reduce to a simple Turing tape in case of $k=d=1$.
It is easy to see that other well-known tape variants can be described by this definition just as well.

But it doesn't end there

However, the definition above allows much more complex examples for tapes, most notably when using infinite cardinals. And when I'm about defining Turing machines, I wonder why I would restrict the alphabet and set of states to be finite. Of course, these generalizations make it much more difficult to image any kind of realization in the real world. Nevertheless, I think it is kind of interesting if these generalizations of a TM would make it possible to archive something beyond Turing completeness. Other known generalizations such as non deterministic TMs and quantum TMs do not seem to have archived greater computability. Maybe I missed something?

The Question

Has my kind of generalization (the different "Turing Spaces") been studied before? Or any kind of allowing infinite states and/or alphabets besides the kind appearing in quantum TMs?
A general notion of machines based on graphs was given by Wilfried Sieg and John Byrnes in K-Graph Machines: Generalizing Turing's Machines and Arguments. It may or may not be related to what you are doing.

Also note that it is quite easy to find a complete formalization of Turing machines. Why are you saying that "the tape of a Turing machine ... is usually left out when introducing Turing machines". That's an odd thing to say. Let's perform an experiment. For instance, what is unclear about the definition given on Wikipedia (following a standard textbook)? All you need is a formalization of finite sequences, and I'd be flabbergasted if Mizar hasn't got those.