[isabelle] Schematic and universally quantified variables in forward proofs
- To: isabelle-users at cl.cam.ac.uk
- Subject: [isabelle] Schematic and universally quantified variables in forward proofs
- From: Martin Desharnais <martin.desharnais at gmail.com>
- Date: Wed, 22 May 2019 10:56:09 +0200
- User-agent: Mozilla/5.0 (X11; Linux x86_64; rv:60.0) Gecko/20100101 Thunderbird/60.6.1
Dear Isabelle users,
I have a situation where I am surprised by the result of forward proof
step. Basically, I have a hierarchy of similar theorems that, where each
stronger level implies the next weaker level. In my formalization, I
want to prove the strongest possible theorem, but when using the
results, I actually only need the weaker form.
I want an easy and efficient (in terms of performance and readability)
way to convert from a strong to a week form and I though a forward
instantiation of a lifting lemma ("lifting" in the following example)
would be a good idea.
Now, I can use the lifting lemma without problem in a backward proof,
but when I use it in a forward proof (with OF or THEN), I am surprised
at the resulting instantiation. To get the expected form, I have to
perform a simplification step afterward.
I realize that "some_strong_thm" has schematic variables while the
lemma's hypothesis uses universally quantified variables and I suppose
this is the source of my problem/confusion.
My questions are:
1. Is there a way to change the form from schematic to universally
qualified variables and vice versa?
2. Why does the forward step "lifting[OF some_strong_thm]" unify to this
result? And is there a way to control the unification or change the
lifting lemma to not require the simplification step?
3. Is this the usual Isabelle way of handling such a situation or are
there better alternative?
locale A =
f :: "'a ⇒ bool" and
g :: "'a ⇒ 'a ⇒ bool" and
h :: "'a ⇒ bool"
f_to_h: "f x ⟹ h x" and
some_strong_thm: "f x ⟹ ∃y. f y ∧ g x y"
strong_thm: "⋀x. f x ⟹ ∃y. f y ∧ g x y" and
shows "∃y. h y ∧ g x y"
obtain y where "f y" and "g x y"
using strong_thm[OF assms(2)] by auto
thus ?thesis by (auto intro: f_to_h)
lemma backward_proof: "f x ⟹ ∃y. h y ∧ g x y"
by (auto intro: some_strong_thm lifting)
lemmas forward_proofs =
lifting[OF some_strong_thm, simplified]
(⋀x. f x ⟹ f x) ⟹ f ?x ⟹ ∃y. h y ∧ g ?x y
f ?x ⟹ ∃y. h y ∧ g ?x y
This archive was generated by a fusion of
Pipermail (Mailman edition) and