我正在尝试证明有关多元的一些基本事实 多项式,因此需要一个多次的类型。为了模拟这个,我 使用来自某些未指定类型的变量名的部分函数 到自然数:
type_synonym 'v multi_degree = "'v ⇒ nat"
还有一些涉及有限支持的东西,但这并不 对于这个问题来说真的很重要。然后我定义添加 以明显的逐点方式进行多度:
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)
现在我想说的是,多次加法的结构为 一个可交换幺半群。最明显的写法是这样的 这个:
interpretation md: comm_monoid "op ⊕" "zero_degree"
proof
到目前为止一切顺利:输出是
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
我绝对可以证明这一点!但是如果我现在写
interpretation md: comm_monoid "op ⊕" "zero_degree"
proof
fix a
show "a ⊕ zero_degree = a" by simp
然后我收到警告
Introduced fixed type variable(s): 'c in "a__"
有办法避免警告吗?现在,我已经作弊并证明了 解释与
interpretation md: comm_monoid "op ⊕" "zero_degree"
by (unfold_locales; simp?; rule sym_md_plus)
这是有效的,但对于 future 的读者来说并不完全清楚......
最佳答案
只需写fix a::"'a multi_ Degree"
。如果没有其他约束,Isabelle 会选择 'a
作为类型变量。但是,我认为显式实际绑定(bind)类型变量是一种很好的风格,例如
interpretation md: comm_monoid "op ⊕" "zero_degree :: 'a multi_degree"
proof
fix a :: "'a multi_degree"
还有一点:您可能需要考虑使用 typedef
引入一种新的 multi_ Degree
类型,然后通过提升/传递定义您想要在其上定义的所有函数。 (参见相应手册)
这样做的优点是您可以实例化正确的类型类(例如comm_monoid_add),而不必始终进行区域设置假设。另外,您可以编写 +
和 0
而不是 ⊕
和 zero_ Degree
。
关于polymorphism - 在 isabelle/hol 中证明解释时的多态 "fix"语句,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/33857454/