Qiyuan Xu (Dec 01 2021 at 06:41): 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.
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>
The problem is that this is not _local_ to a call, but it is a global change to the theory.
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)
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
Qiyuan Xu (Dec 01 2021 at 06:51):great idea
Last updated: Dec 21 2024 at 16:20 UTC