What is an assumption in Isar?

Question

I have the following code:

lemma assumes "A" shows "A ∧ A"
proof -
  show "A ∧ A"
    apply (rule conjI)
    apply assumption

Now, applying conjunction introduction works, but applying the assumption does not.

Seemingly, assumes would introduce an assumption, wouldn't it?

The very same thing happens when I do

lemma a_imp_a_and_a: "A ⟶ A ∧ A"
proof (rule impI)
  assume A
  show "A ∧ A" apply (rule conjI)
   apply assumption

Again, I've thought assume would introduce an assumption that can be solved by

apply assumption

but it does not work.

What is an assumption in Isar that can be solved by apply assumption?

Answer 1

Slawomir already answers the main question of how to refer to assumptions in Isar proofs. (Usually, one does not use the proof method assumption for this.)

I'll try to answer the connected side-question by Gergely how to apply the proof method assumption:

What is an assumption in Isar that can be solved by apply assumption?

The proof method assumption basically says that one of the things in the left-hand-side of the proof state for the particular line matches the current right-hand-side of the goal. This might not be a verbatim match and can require some instantiations or unifications.

Consequently, we must massage the from/using-part of an Isar proof to match the target if we want to perform a step by assumption. This could look like this:

lemma
  assumes ‹A› shows ‹A ∧ A›
proof -
  from conjI[OF ‹A› ‹A›] show ‹A ∧ A› by assumption
qed

The [OF ...] modifier discharges premises in a rule with facts. (The order matters. It's like function application if you see premises as inputs.) Thus, conjI[OF ‹A› ‹A›] is (verbatim) A ∧ A, matching the goal. Therefore, by assumption can finish the proof step.

So, by assumption is about the most trivial proof step one can think of. In Isar however, it is common to use the special notation . for trivial / immediate proof steps. Therefore, the following would be more idiomatic Isar:

lemma
  assumes ‹A› shows ‹A ∧ A›
  using conjI[OF ‹A› ‹A›] .

Actually, the immediate proof method . is even more powerful than the method assumption as it can use higher-order modus ponens, taking the first fact of the line as a rule. This means, we can do without the OF:

lemma
  assumes ‹A› shows ‹A ∧ A›
  using conjI ‹A› ‹A› .

The same would not be possible with the assumption method. (. is equivalent to by this in apply-style.)

Generally, I would suggest to forget about the methods assumption and this in Isar proofs, and just use . to discharge trivial steps. You do not need the two, and their naming is indeed confusing because it clashes with Isar's reserved names for specific facts, namely assms for the assumes-part of a lemma and this for the last fact established.

Answer 2

I assume the question is about how assumptions can be referenced to in an Isar proof. One way to use assumptions is through the assms keyword like this:

lemma assumes "A" shows "A∧A" using assms by simp

Or, if you want on explicit rule application you can you use from and quote the assumption twice as conjI has two assumptions:

lemma assumes "A" shows "A∧A"
proof -
  from ‹A› ‹A› show ?thesis by (rule conjI)
qed

You can also use the assms keyword in the direct rule application but again you have to repeat assms(1) to match the conjI lemma:

lemma assumes "A" shows "A∧A"
proof -
  from assms(1) assms(1) show ?thesis by (rule conjI)
qed

I checked this in Isabelle/ZF, but it should be the same in Isabelle/HOL.