Suppose that we have a closed term x:t in the simply typed lambda calculus (STLC) (i.e. this term does not contain any free variables). You can use the terminology and syntax definitions given here.
Suppose that t is not / does not contain a function type, e.g. in the case of a simple programming language perhaps t can be expressed in the following (inductive) grammar:
ty := Int | Bool | Unit | Array ty
It is a theorem that the STLC is strongly normalizing under beta-reduction (e.g. see the first point here). I want to prove that this implies that the normal form (under beta-reduction) of x:t does not contain any lambda abstractions or applications. If the proof is simple, great. Otherwise a link and a high level description would be nice.
If this is not true, a counter example would be great.
(NOTE: an original formulation of this question was answered by @Taroccoesbrocco, but I had forgotten to specify closed which is important for my situation).
Best Answer
The property you want to prove is false, unless you implicitly suppose more hypotheses that you should make explicit.
For instance, take the simply typed terms $x : \text{Int} \to \text{Int}$ and $y : \text{Int}$, for some distinct variables $x$ and $y$. Then, $xy: \text{Int}$ is a normal (with respect to $\beta$-reduction) simply typed term that contains an application, and whose simple type is ground (that is, not a function type).
Could we weaken your statement by only demanding that the simply typed term does not contain any abstraction? No! A counterexample is the following: take the simply typed term $x : (\text{Int} \to \text{Int}) \to \text{Int}$ and $\lambda y^\text{Int}.y : \text{Int} \to \text{Int}$, for some variable $x$ and $y$. Then, $x(\lambda y.y): \text{Int}$ is a normal (with respect to $\beta$-reduction) simply typed term that contains an abstraction and whose simple type is ground.
Edit after the OP edited his question.
If you add the request that the simply typed term must be closed, then the property you are interested in (the $\beta$-normal form of every closed simply typed term of ground type does not contain any abstraction or application, that is, is a term constant) is true, provided that every term constant is typed with ground type (which is usually the case).
Indeed, it is easy to prove that every closed $\beta$-normal form is either an abstraction or a term constant (this is false if a constant can be typed with an arrow type). But abstractions cannot be of ground type, they are necessarily of arrow type. Hence, every closed simply typed $\beta$-normal form whose type is ground is a constant. To conclude (since the property talks about every simpled typed $\lambda$-term, not only the $\beta$-normal) just use strong normalization (as you correctly mentioned) and subject reduction (that is, if $M:\tau$ and $M \to_\beta N$, then $N : \tau$).