Gergely Buday (Jun 02 2025 at 07:38): Gergely Buday (Jun 02 2025 at 07:38):I can do
lemma commute: "(m::nat) + n = n + m" sorry
lemma meta_commute: "⋀m n. (m::nat) + n = n + m" by (rule commute)
What kind of automation is here under the hood? As I understand, commute's theorem form is with schematic variables:
theorem commute: ?m + ?n = ?n + ?m
which is a kind of universal quantification, which can be turned into meta universal quantification, and by rule does this. Could you elaborate the background?
Jan van Brügge (Jun 02 2025 at 09:37):The schematic variables are just unification variables. And rule does (higher-order) unification. So here, Isabelle unifies ?m with the forall-bound m and ?n with n. This unification succeeds and thus the rule can be applied.
Last updated: Jun 21 2025 at 01:46 UTC