What can one assume, what is worth assuming in Isar?

In Isar one uses assume with the premise of the goal so that she can use it building the conclusion.

assume expects to be able to unify with existing premises in the goal

Is this the only use of assume, namely, to get facts from the premises of the goal?

update: as some people consider this too broad, which I do not understand, I try to reformulate the question.

The manual describes the logical content of assume. But what is its usage? Is that confined to only the case when I get a fact from the premises of the goal?

Solution

I see two uses of the assume keyword that are of course two instances of the same process: stating the premises of a property to be proved.

If we take a silly example:

lemma "∀A B C D. A ⟶ B ⟶ C ⟶ D ⟶ (A ∧ B) ∧ (C ∧ D)"
using assms
proof (intro allI impI)
  fix A B C D
  assume A B
  then have "A ∧ B" .. (* or "by rule", "by default", "by simp", ... *)

  { fix E F
    assume E and F
    then have "E ∧ F" ..
  } note H = this

  assume C D then have "C ∧ D" ..
  from H[OF `A ∧ B` `C ∧ D`] show "(A ∧ B) ∧ (C ∧ D)" . (* or "by fact" *)
qed

either assume appears to state the premises generated by a proof command anywhere between proof and show or thus. These assumed properties will have to be a subset of the premises generated by the proof command (here A B C and D).
or assume appears in a block delimited by { and } where you can assume anything you want and then prove a property P stated with have. When the block is closed, a local fact is produced composed of the assumptions as premises, and the property P as a conclusion. In the example, I name it H and use it to prove the last conjunction.