Stream: Beginner Questions

Topic: Schematic variables to meta-quantified

Lukas Stevens (May 27 2020 at 13:58):

Is there a way to convert a theorem with schematic variables to a theorem with meta-quantified variables?

Mathias Fleury (May 27 2020 at 14:05):

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.

Josh Chen (May 27 2020 at 14:07):

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..

Mathias Fleury (May 27 2020 at 14:15):

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: Apr 19 2024 at 01:05 UTC