How do 'tactics' work in proof assistants?
I suspect this answer will be a bit of a ramble.
First, it isn't enough to ask "how tactics work in proof assistants" because they work differently in different proof assistants. There's two main classes of assistant used today: those derived from the original LCF, like Isabelle, HOL and HOL light, and type theory based proof assistants like Coq and Matita. In these two different classes of proof assistant the tactics work in different ways, a reflection that what's going on under the bonnet in e.g. Isabelle is quite different to what's going on under the bonnet in e.g. Matita.
Ask yourself: what's going on when we attempt to prove a proposition P in Matita? We introduce a metavariable X with type P. We then play a game, so to speak, where we refine X, adding more and more structure to the incomplete term, until we get a complete lambda-term (i.e. containing no more metavariables). Once we are in possession of a complete lambda-term, we type check it with respect to P, making sure it inhabits the required type. We then see that in Coq and Matita, a tactic is merely a function from incomplete proof terms to incomplete proof terms, which hopefully adds a bit of structure to the term after application (this observation has motivated quite a bit of recent work by e.g. Jojgov, Pientka, and others).
For instance, the Matita tactic "intro" introduces a lambda-abstraction over the existing term, "cases" introduces a match expression in the term, and "apply" introduces an application of one term to the other. These basic tactics can be strung together, using higher-order functions, to create more complex ones. The basic idea is always the same though: a tactic is always aiming to add a bit of structure to an incomplete proof term.
Note that, implementers aim to give back a term that typechecks again after every tactic application. Strictly speaking, there's no requirement for them to do so, as all that matters for type theory based proof assistants is that, when the user comes to Qed the proof, we are in possession of a proof term that inhabits the proposition P. How we arrived at this proof term is largely irrelevant. However, both Coq and Matita aim to give the user back a (possibly incomplete) proof term that typechecks after every tactic application. Yet this invariant can (and often does) fail, especially in regard to the two syntactic checks that CIC based proof assistants must implement.
In particular, we can carry out what appears to be a valid proof, applying a series of tactics until there are no open goals left. We then come to Qed the supposed proof, only to discover that Matita's termination checker, or its strict positivity checker, complains, as the proof term that was generated by the tactics has invalidated one of these syntactic checks (i.e. a metavariable in argument position to a recursive call was instantiated with a term that is not syntactically smaller than the original argument). This is a reflection that the CIC type theory is, in some sense, not "strong enough", and does not reflect the positivity or size syntactic requirements in its types (an observation that motivates Abel's sized types, and some recent work on positivity types).
On the other hand, LCF-style proof assistants are quite different. Here, the kernel consists of a module (usually implemented in a variant of ML), containing an abstract type "thm", and functions that implement the inference rules of the proof assistant's logic, mapping "thm" to "thm", and so forth. We rely on the typing discipline of ML to ensure that the only way of constructing a value of type "thm" is via these inference rules (basic tactics). Isabelle's kernel is here.
Proofs then consist of a series of applications of these basic tactics (or more complex, larger tactics, which are again made by stringing together simpler tactics using higher-order functions --- in Isabelle, the higher-order functions, called tacticals, can be seen here). Unlike type theory based proof assistants, there is no need in an LCF-style assistant to keep an explicit proof term witness lying around. Correctness of the proof is guaranteed by construction, and our trust in ML's typing discipline (many assistants, e.g. Isabelle, do, however, generate proof terms for their proofs).