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, 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 2024 at 16:22 UTC