A Question on Special Forcings The usual use of forcing begins with a "countable" and "transitive" ground model of $ZFC$ and reaches to a "countable" and "transitive" generic model of $ZFC$ with the "same ordinals". In a discussion a colleague told me about a special forcing by Solovay which begins with a countable transitive model of $ZFC$ and reaches to an "uncountable" transitive generic model. My question is about these kind of special forcings and their possible special uses.
Question: Please introduce a reference about any use of forcing with at least one of the below characteristics:
(a) The ground model is uncountable.
(b) The ground model is not transitive.
(c) The generic model is uncountable.
(d) The generic model is not transitive.
(e) The generic model has more ordinals than ground model. 
 A: I don't agree that the "usual" use of forcing uses only countable transitive models. Perhaps this used to be true, years ago, and forcing is sometimes still taught this way now, because it is somewhat easier to see where the generic filters come from, but neither hypothesis is actually needed to develop a full theory of forcing, and I think that these days it is quite common to understand forcing as an internal ZFC construction that works over any model, not just the countable transitive models.
For example, the Boolean-value approach to forcing allows us to make sense of forcing over the universe, within ZFC. One defines the Boolean values $[\![\varphi]\!]$ for any formula $\varphi$ in the forcing language, by induction on $\varphi$. This allows one to speak of which statements are forceable or not over any model of set theory, and suffices for the consistency proofs. 
Meanwhile, one can turn the Boolean-valued model $V^{\mathbb{B}}$ into an actual classical 2-valued model simply by taking the quotient by an ultrafilter $U\subset\mathbb{B}$, and there is no need for $U$ to be $V$-generic in this process, and even $U\in V$ is completely fine. The elements of the quotient are the equivalence classes with respect to the relation $\sigma\sim_U\tau\iff [\![\sigma=\tau]\!]\in U$. This is not the same as the usual value $\text{val}(\sigma,U)$ assignment, except when $U$ is $V$-generic. This gives rise to the Boolean ultrapower map $j:V\to \check V_U$, defined by $j:x\mapsto [\check x]_U$, which is an elementary embedding of $V$ into the class model $\check V_U$, and $\check V_U$ has its forcing extension $\check V_U[G]$ as a class inside $V$. The generic object $G$ is simply the equivalence class of the name of the generic object $G=[\dot G]_U$. Thus, one never needs to leave $V$ to speak of the forcing extensions of $V$. When there are large cardinals, one can even arrange that $\check V_U$ is transitive, and these Boolean ultrapowers can be viewed as large cardinal embeddings. 
Dan Seabold and I give a fairly thorough account of the Boolean ultrapower in our paper Boolean ultrapowers as large cardinal embeddings. In particular, this paper contains examples of all of the types of examples you request. 
Update. Here is an example that may be more like what you had wanted. 
Theorem. If there is a supercompact cardinal, then there is transitive inner model, containing all ordinals, with a Laver indestructible supercompact cardinal. Similarly, there is an inner model with a supercompact cardinal $\kappa$ for which $2^\kappa=\kappa^+$ and another with a supercompact cardinal $\kappa$ for which $2^\kappa>\kappa^+$. 
Proof. These results and others like it appear in A. Apter, V. Gitman, J. D. Hamkins, “Inner models with large cardinal features usually obtained by forcing,” Archive for Mathematical Logic, 51(2012):257-283. Suppose that $\kappa$ is supercompact in $V$. Let $j:V\to M$ be a $\theta$-supercompactness embedding for some $\theta$ for which $2^{\theta^{\lt\kappa}}=\theta^+$. (This is possible because the SCH holds above any supercompact cardinal.) Let $\mathbb{P}$ be the Laver preparation forcing for $j(\kappa)$ as defined in $M$, but starting above $\theta$. Thus, $\mathbb{P}$ is $\leq\theta$-closed in $M$ and hence also in $V$, and by counting we can see that there are only $\theta^+$ many dense subsets of $\mathbb{P}$ in $V$. So in $V$ we may construct an $M$-generic filter $G\subset \mathbb{P}$. Thus, $M[G]$ is a transitive inner model of $V$ in which $j(\kappa)$ is a Laver indestructible supercompact cardinal. By also combining $\mathbb{P}$ with further forcing, we can ensure that the GCH holds or fails at $j(\kappa)$, or a variety of other situations. QED
The general theorem here is the following, where a partial order $\mathbb{Q}$ is $\lt\kappa$-friendly, if for every $\delta\lt\kappa$, there is a condition below which $\mathbb{Q}$ adds no new subsets to $\delta$. 
Theorem.(Seabold, Hamkins) If $\kappa$ is strongly compact, then for any $\lt\kappa$-friendly notion of forcing, there is a transitive inner model satisfying every sentence forced by $\mathbb{Q}$ over $V$. 
The proof uses Boolean ultrapowers, and the point is that strong compactness is enough to enable one to find a well-founded Boolean ultrapower. 
A: 

This answer supplements the ones given by Hamkins and Golshani.


1. To my knowledge, the first paper to study the construction of generic extensions over uncountable models is the following:
John L. Bell, Uncountable models of ZFC + V $\neq$ L, in Lecture Notes in Math., vol. 537, pp.29-36 (1976).
In the above paper, Bell first shows that if ZFC has a natural model (i.e., one of the form $V_\alpha$ for some $\alpha$), then there are transitive models of ZFC + V $\neq$ L for all cardinalities below $\alpha$.
Bell's paper also includes a result, due independently to Kunen and Vopěnka, which states that if there is an uncountable transitive model of ZFC, then there is an uncountable transitive model of ZFC + V $\neq$ L.
2. It is a theorem of ZFC plus $\diamond_{\aleph_1}$ that $(*)$ below holds:
$(*)$ Every consistent extension of ZFC has a model $M$ of power $\aleph_1$ such that for any poset $P$ in $M$, and any filter $G$ over $P$, $G$ is $P$-generic over $M$ iff  $G$ is already coded in $M$ (in other words, $M$ has no nontrivial generic extensions). 
Note that in $(*)$ $M$ is not claimed to be transitive. An outline of the proof of (2), which relies heavily on a beautiful theorem of Matti Rubin, can be be found on p.1007 of the following paper of mine:
Ali Enayat, Conservative extensions of models of set thery and generalizations, Journal of Symbolic Logic, vol. 51, pp.1005-1021 (1986).
3.  It can be shown, using some deep absoluteness arguments due to Shelah and Schmerl (detailed in the paper below), that indeed $(*)$ is a theorem of ZFC.
James Schmerl, Elementary extensions of models of set theory,  Arch. Math. Logic 39 (2000), pp. 509–514.
PS. I  need to fuse this account with the one which carries my name, but I have not gotten around to it.
A: The reference is " Felgner, Choice functions on sets and classes, Sets and classes (on the work by Paul Bernays), pp. 217–255. Studies in Logic and the Foundations of Math., Vol. 84, North-Holland, Amsterdam, 1976".
In the paper, it is stated that: "However, it is remarkable, that by a modification of Cohen’s method, it is possible to obtain uncountable generic extensions of countable models.
This device is due to Solovay."
The Solovay construction is presented in the paper, which is used to show the independence of AC from ZF.
