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.
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.
I find it easier to normalize goals with
intro allI impI and elimination of
exE (for existential quantifier in the assumptions)
For exE, I use
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
Last updated: Aug 13 2022 at 06:26 UTC