How does one use basic propositional rules in Isar to prove `A ⟶ A ∨ B`?

I wanted to transform this proof to Isar as ab exercise (for myself to learn Isar) using only basic natural deduction rules (ND) from propositional logic (e.g. notI, notE, impI, impE... etc).

I can do it in an apply script easily:

lemma very_simple0: "A ⟶ A ∨ B"
  apply (rule impI) (* A ⟹ A ∨ B *)
  thm disjI1 (* ?P ⟹ ?P ∨ ?Q *)
  apply (rule disjI1) (* A ⟹ A *)
  by assumption

but my attempts at an Isar proof fail:

lemma very_simple1: "A ⟶ A ∨ B"
proof (* TODO why/how does this introduce A by itself*)
  assume A (* probably not neccessary since Isabelle did impI by itself *)
  have "A ⟹ A" by disjI1
  show "A ⟹ A" by assumption
qed

my main error is:

Undefined method: "disjI1"⌂

which seems mysterious to me because the rules worked just fine in the apply script before.

What am I doing wrong?

Note this also leads to an error:

lemma very_simple2: "A ⟶ A ∨ B"
proof impI
  assume A (* probably not neccessary since Isabelle did impI by itself *)
  have "A ⟹ A" by disjI1
  show "A ⟹ A" by assumption
qed

same error as above:

Undefined method: "impI"⌂

why?

Edit:

I learned that a 'method' still requires the work rule impI or metis etc but the script still fails:

lemma very_simple1: "A ⟶ A ∨ B"
proof (rule impI)
  assume A (* probably not neccessary since Isabelle did impI by itself *)
  have "A ⟹ A" by (rule disjI1)
  show "A ⟹ A" by assumption
qed

Edit2:

lemma very_simple1: "A ⟶ A ∨ B"
proof (rule impI)
  have 0: "A ⟹ A ∨ B" by (rule disjI1)
  have 1: "A ⟹ A" by assumption
  from 1 show "True" by assumption
qed

I still can't complete the proof.

Solution

You have several problems.

Let us consider the example:

have "A ⟹ A" by (rule disjI1)

That fails, so first what is the theorem disjI1 actually?

thm disjI1
(* ?P ⟹ ?P ∨ ?Q *)

Due to how rules works, it tries to match the goal "A" with "?P ∨ ?Q", which fails. Now, if your goal has the right form:

have "A ⟹ A ∨ B" by (rule disjI1)

it works!

Second problem:

 proof

is by default equivalent to "proof standard" and applies some theorem by default. Typically, you will use "proof -" to apply no theorem.

Lastly, let us consider your example

lemma very_simple1: "A ⟶ A ∨ B"
proof (rule impI)

In the state view, you see:

proof (state)
goal (1 subgoal):
 1. A ⟹ A ∨ B

This means that the Isar must look like

lemma very_simple1: "A ⟶ A ∨ B"
proof (rule impI)
  assume ‹A›
  show ‹A ∨ B›
    sorry
qed

The fact that show works indicates that proof block has the correct form.

Beware: This is an important step especially at the beginning. ALWAYS start with the assume and the show. Do not wright anything else. If the show does not work, the structure induced by the Isar proof (assume and show) does not match the expected proof (which can be seen in the State panel).

You can do whatever you want from there (including starting a new proof block), but you cannot change that structure without changing which rule was applied.

Let's finish the proof. We want to use the assumption (so we add a then) and the rule to prove the goal.

lemma very_simple1: "A ⟶ A ∨ B"
proof (rule impI)
  assume ‹A›
  then show ‹A ∨ B›
    by (rule disjI1)
qed

Overall, I think you should read the Isar part of the Concrete Semantics.

EDIT: The most important problem is that you misunderstand what Isar is: Isar is not here to help you with the different proof steps (like proving tha "A ==> A"). It is here to do a forward proof: You start from the assumption (here A) and go to the conclusion. So the Isar proof will look like

  assume A
  show "A \/ B"

You never have to repeat the assumption A in the proof!