Is there a way to convert a theorem with schematic variables to a theorem with meta-quantified variables?
what difference do you make between both? If I try:
consts P :: \<open>nat \<Rightarrow> bool\<close> lemma T1: \<open>P x\<close> for x sorry lemma T2: \<open>\<And>x. P x\<close> sorry lemma T3: \<open>P x\<close> sorry thm T1 T2 T3 (* • P ?x • P ?x • P ?x *)
The resulting theorems are all the same.
Like Mathias said, the two are mostly functionally the same from the end-user (non-ML) point of view. EDIT: Although maybe some things like the
where attribute won't work on quantified variables since those are bound..
If you are doing strange things, potentially the attribute
rule_format might help to normalise theorems to what you want (although it is not clear if this is a good idea or not).
Last updated: Sep 25 2021 at 08:21 UTC