# [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?
`
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

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*