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 ⟶
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:
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, 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).
+ 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: Dec 07 2023 at 20:16 UTC