Полиморфные «исправления» утверждений при проверке интерпретаций в isabelle/hol

Question

Я возился, пытаясь доказать некоторые основные факты о многомерных многочленах и поэтому нужен тип для нескольких степеней. Для моделирования этого я использовал частичную функцию от некоторого неопределенного типа имен переменных в натуральные числа:

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) 

, который работает, но не совсем понятно, для будущих читателей ...

Answer 1

Просто напишите fix a :: "'a multi_degree". Изабель будет выбирать 'a как переменную типа, если нет других ограничений. Однако я бы счел хорошим стилем, чтобы явным образом привязывал переменную типа, например. более

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

Одно замечание: вы можете рассмотреть вопрос о введении нового типа для multi_degree с помощью typedef, а затем определить все функции, которые вы хотите, чтобы определить на нем с подъемным/передачи. (см. соответствующие руководства)

Это имеет то преимущество, что вы можете создать экземпляр соответствующих классов классов (например, comm_monoid_add) и не обязательно носить с собой все языковые предположения. Кроме того, вы можете написать + и 0 вместо ⊕ и zero_degree.