Stream: Beginner Questions

Topic: ✔ How to prevent splitting of pair in universial quantifi...


view this post on Zulip Qiyuan Xu (Dec 01 2021 at 06:41):

As an example,

lemma "∀x. Q x" for Q :: "('a × 'b) ⇒ bool"
  apply clarify

which results in ⋀a b. Q (a, b),
how to prevent the method clarify splitting the pair to let it result in ⋀x. Q x?
I have removed the simplification rule split_paired_All, but it hasn't worked yet. I guess there are other things I haven't disabled but I cannot figure them out.

view this post on Zulip Mathias Fleury (Dec 01 2021 at 06:47):

I don't recommend it, but:

setup \<open>map_theory_claset (fn ctxt => ctxt delSWrapper ("split_all_tac"))\<close>

view this post on Zulip Mathias Fleury (Dec 01 2021 at 06:47):

The problem is that this is not _local_ to a call, but it is a global change to the theory.

view this post on Zulip Mathias Fleury (Dec 01 2021 at 06:49):

I find it easier to normalize goals with intro allI impI and elimination of exE (for existential quantifier in the assumptions)

view this post on Zulip Mathias Fleury (Dec 01 2021 at 06:51):

For exE, I use normalize_goal+ where:

method normalize_goal =
  (match premises in
    J[thin]: \<open>\<exists>x. _\<close> \<Rightarrow> \<open>rule exE[OF J]\<close>
  \<bar> J[thin]: \<open>_ \<and> _\<close> \<Rightarrow> \<open>rule conjE[OF J]\<close>
  )

(I never have ∀ in goals), but you can easily extend the method to also do rule impI allI conjI

view this post on Zulip Qiyuan Xu (Dec 01 2021 at 06:51):

great idea


Last updated: Aug 13 2022 at 06:26 UTC