CODEWITHSUNDEEP
polymorphismisabelle
Rupert Swarbrick
Rupert Swarbrick

Reputation: 2803

Polymorphic "fix" statements when proving interpretations in isabelle/hol

I'm messing around trying to prove some basic facts about multivariate polynomials and so needed a type for a multi-degree. To model this, I used a partial function from some unspecified type of variable names to natural numbers:

type_synonym 'v multi_degree = "'v ⇒ nat"

There's some more stuff involving finite support but that doesn't really matter for this question. I then define addition of multi-degrees in the obvious pointwise way:

definition zero_degree :: "'v multi_degree" where "zero_degree = (λ v. 0)"

definition md_plus :: "'v multi_degree ⇒ 'v multi_degree ⇒ 'v multi_degree" (infix "⊕" 70) where
  "(d1 ⊕ d2) = (λ v. d1 v + d2 v)"

lemma assoc_md_plus [simp]: "d1 ⊕ (d2 ⊕ d3) = (d1 ⊕ d2) ⊕ d3"
  by (rule; simp add: md_plus_def)

lemma ident_zero_degree [simp]: "d ⊕ zero_degree = d" and "zero_degree ⊕ d = d"
  by (auto simp add: md_plus_def zero_degree_def)

lemma sym_md_plus: "d ⊕ d' = d' ⊕ d"
  by (rule; simp add: md_plus_def)

Now I want to say that addition of multi-degrees has the structure of a commutative monoid. The obvious thing to write is something like this:

interpretation md: comm_monoid "op ⊕" "zero_degree"
proof

So far so good: the output is

goal (3 subgoals):
 1. ⋀a b c. (a ⊕ b) ⊕ c = a ⊕ (b ⊕ c)
 2. ⋀a b. a ⊕ b = b ⊕ a
 3. ⋀a. a ⊕ zero_degree = a

which I can definitely prove! However if I now write

interpretation md: comm_monoid "op ⊕" "zero_degree"
proof
  fix a
  show "a ⊕ zero_degree = a" by simp

then I get the warning

Introduced fixed type variable(s): 'c in "a__"

Is there a way to avoid the warning? For now, I've cheated and proved the interpretation with

interpretation md: comm_monoid "op ⊕" "zero_degree"
  by (unfold_locales; simp?; rule sym_md_plus)

which works, but isn't exactly clear to future readers...

Upvotes: 2

Views: 306

Answers (1)

Manuel Eberl
Manuel Eberl

Reputation: 8268

Just write fix a :: "'a multi_degree". Isabelle will pick 'a as a type variable if there are no other constraints. I would, however, consider it good style to actually bind the type variable explicitly, e.g.

interpretation md: comm_monoid "op ⊕" "zero_degree :: 'a multi_degree"
proof
  fix a :: "'a multi_degree"

One more remark: you might want to consider introducing a new type for multi_degree using typedef and then define all the functions you want to define on it with lifting/transfer. (see the corresponding manuals)

This has the advantage that you can instantiate the proper type classes (like comm_monoid_add) and don't have to carry around locale assumptions all the time. Also, you can write + and 0 instead of ⊕ and zero_degree.

Upvotes: 2

Related Questions