Email Gateway (Aug 22 2022 at 19:41): Email Gateway (Aug 22 2022 at 19:41):From: Martin Desharnais <martin.desharnais@gmail.com>
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:
Is there a way to change the form from schematic to universally
qualified variables and vice versa?
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?
Is this the usual Isabelle way of handling such a situation or are
there better alternative?
Regards,
Martin Desharnais
Simplified example:
locale A =
fixes
f :: "'a ⇒ bool" and
g :: "'a ⇒ 'a ⇒ bool" and
h :: "'a ⇒ bool"
assumes
f_to_h: "f x ⟹ h x" and
some_strong_thm: "f x ⟹ ∃y. f y ∧ g x y"
begin
lemma lifting:
assumes
strong_thm: "⋀x. f x ⟹ ∃y. f y ∧ g x y" and
"f x"
shows "∃y. h y ∧ g x y"
proof -
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)
qed
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]
lifting[OF some_strong_thm, simplified]
(*
theorem forward_proofs:
(⋀x. f x ⟹ f x) ⟹ f ?x ⟹ ∃y. h y ∧ g ?x y
f ?x ⟹ ∃y. h y ∧ g ?x y
*)
end
Last updated: Apr 20 2024 at 12:26 UTC