# [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.