K is a rewrite-based executable semantic framework in which programming languages, type systems and formal analysis tools can be defined using configurations, computations and rules. K supports a module design for programming language specifications, with different language features separated in different modules. This is supported through a subsort system and K features called localization and concision. By these features and other features, language specifications can be defined in K effectively. In this paper we define a complete static semantics of K named IsaK-Static, in the interactive theorem prover Isabelle/HOL , to study these features. Specially, it defines the full static behavior of K a useful sort system for K and suggests several undesirable behaviors in the current K implementations (K 3.6 and K 4.0). To the best of our knowledge, IsaK-Static is the most complete of any existing K specification. We also provide an OCaml based executable full K interpreter generated automatically from the K specification in Isabelle.