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: Apr 27 2024 at 12:25 UTC