[isabelle] Schematic and universally quantified variables in forward proofs



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.