## Stream: Beginner Questions

### Topic: multiple "automatic" proof steps

#### Artem Khovanov (Jul 19 2023 at 22:00):

As I understand, a `proof ... qed` block automatically applies a standard introduction rule to the goal, allowing constructions like

``````show "∀x. P x"
proof
fix x
show P x sorry
qed
``````

I know that I can supress this introduction rule application by using `proof -`. However, in certain cases I would like to chain together multiple standard introduction rules automatically. For instance, I would like to prove the following:

``````lemma add_transfer [transfer_rule]:
includes lifting_syntax
shows "(poly_compare R ===> poly_compare R ===> poly_compare R)
(⊕⇘poly_ring R⇙) (⊕⇘UP R⇙)"
unfolding rel_fun_def
``````

This gives me the state
```∀x y. poly_compare R x y ⟶ (∀z w. poly_compare R z w ⟶ poly_compare R (x ⊕⇘poly_ring R⇙ z) (y ⊕⇘UP R⇙ w))```
I want to do something like

``````proof
fix x y z w assume "poly_compare R x y" "poly_compare R z w"
thus "poly_compare R (x ⊕⇘poly_ring R⇙ z) (y ⊕⇘UP R⇙ w))" sorry
qed
``````

which requires applying 6 of these "obvious" introduction rules in order. I have managed to apply these rules by using 6 nested `proof` environments, but somehow I suspect this is not the idiomatic solution...

How can I write this proof in this natural way?

#### Artem Khovanov (Jul 19 2023 at 22:24):

I've now found an answer to my problem by looking at the example given here:
https://isabelle.zulipchat.com/#narrow/stream/238552-Beginner-Questions/topic/difference.20between.20.60proof.60.20and.20.60proof.20-.60/near/375626388
As I understand, `proof standard+` applies as many of these standard natural deduction rules as it can. So in my case the following works:

``````proof standard+
fix x y z w assume "poly_compare R x y" "poly_compare R z w"
thus "poly_compare R (x ⊕⇘poly_ring R⇙ z) (y ⊕⇘UP R⇙ w))" sorry
qed
``````

However, looking in the reference manual section 6.4.2 (p. 146), I cannot find any reference to this `standard+` method for the initial refinement step. Does anyone know where I can find full documentation of relevant initial proof methods?

#### Wolfgang Jeltsch (Jul 19 2023 at 23:29):

Well, at the end of said subsection, on page 148, it says the following:

In Isabelle/Pure, standard performs elementary introduction / elimination steps (rule), introduction of type classes (intro_classes) and locales (intro_locales).

In Isabelle/HOL, standard also takes classical rules into account (cf. §9.4).

#### Mathias Fleury (Jul 20 2023 at 04:49):

`+` just means repeats until an error happens

#### Mathias Fleury (Jul 20 2023 at 04:49):

you can write `(rule exI)+` … or whatever

#### Mathias Fleury (Jul 20 2023 at 04:50):

`standard+` is not a new tactic

#### Artem Khovanov (Jul 20 2023 at 15:34):

thanks both, I understand now!

Last updated: Dec 07 2023 at 20:16 UTC