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?

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?

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

In Isabelle/Pure,

standardperforms elementary introduction / elimination steps (rule), introduction of type classes (intro_classes) and locales (intro_locales).In Isabelle/HOL,

standardalso takes classical rules into account (cf. §9.4).

`+`

just means repeats until an error happens

you can write `(rule exI)+`

… or whatever

`standard+`

is not a new tactic

thanks both, I understand now!

Last updated: Nov 11 2024 at 04:22 UTC