When I have a goal such as "∀x. P x" in Isabelle, I know that I can write
show "∀x. P x"
proof (rule allI)
However, when the goal is "∀x>0. P x", I cannot do that. Is there a similar rule/method that I can use after proof in order to simplify my goal? I would also be interested in one for the situation where you have a goal of the form "∃x>0. P x".
I'm looking for an Isar proof that uses the proof (rule something) style.
To expand on Lars's answer: ∀x>0. P x is just syntactic sugar for ∀x. x > 0 ⟶ P x. As a consequence, if you want to prove a statement like this, you first have to strip away the universal quantifier with allI and then strip away the implication with impI. You can do something like this:
lemma "∀x>0. P x"
proof (rule allI, rule impI)
Or using intro, which is more or less the same as applying rule until it is not possible anymore:
lemma "∀x>0. P x"
proof (intro allI impI)
Or you can use safe, which eagerly applies all introduction rules that are declared as ‘safe’, such as allI and impI:
lemma "∀x>0. P x"
proof safe
In any case, your new proof state is then
proof (state)
goal (1 subgoal):
1. ⋀x. 0 < x ⟹ P x
And you can proceed like this:
lemma "∀x>0. P (x :: nat)"
proof safe
fix x :: nat assume "x > 0"
show "P x"
Note that I added an annotation; I didn't know what type your P has, so I just used nat. When you fix a variable in Isar and the type is not clear from the assumptions, you will get a warning that a new free type variable was introduced, which is not what you want. When you get that warning, you should add a type annotation to the fix like I did above.
For an existential quantifier, safe will not work because the intro rule exI is not always safe due to technical reasons. The typical proof pattern for an ∃x>0. P x would be something like:
lemma "∃x>0. P (x :: nat)"
proof -
have "42 > (0 :: nat)" by simp
moreover have "P 42" sorry
ultimately show ?thesis by blast
qed
Or a little more explicitly:
lemma "∃x>0. P (x :: nat)"
proof -
have "42 > 0 ∧ P 42" sorry
thus ?thesis by (rule exI)
qed
In cases when the existential witness (i.e. the 42 in this example) does not depend on any variables that you got out of an obtain command, you can also do it more directly:
lemma "∃x>0. P (x :: nat)"
proof (intro exI conjI)
This leaves you with the goals ?x > 0 and P ?x. Note that the ?x is a schematic variable for which you can put it anything. So you can complete the proof like this:
lemma "∃x>0. P (x :: nat)"
proof (intro exI conjI)
show "42 > (0::nat)" by simp
show "P 42" sorry
qed
As I said, this does not work if your existential witness depends on some variable that you got from obtain due to technical restrictions. In that case, you have to fall back to the other solution I mentioned.
The following works in Isabelle2016-1-RC2:
lemma "∀ x>0. P x"
apply (rule allI)
In general, you can also just use apply rule, which will select the default introduction rule. Same is true for the existential quantifier.
