Если есть какое-то определение параметров локали, которое сделало бы предположения о локали более простыми для написания и / или чтения и / или понимания (либо потому, что функция довольно сложна, так что это упростит формулировку предположений, или его название облегчает чтение и понимание предположений), как лучше определить эту функцию?
В качестве надуманного примера, скажем, мы хотим включить функцию fg в формулировку предположений (на самом деле здесь это не очень полезно):
locale defined_after =
fixes f :: "'a ⇒ 'b ⇒ 'c"
and g :: "'b ⇒ 'a"
assumes "∀a. ∃b. f a b = f (g b) b"
and univ: "(UNIV::'b set) = {b}"
begin
definition fg :: "'b ⇒ 'c" where
"fg b ≡ f (g b) b"
lemma "∀b b'. fg b = fg b'" using univ the_elem_eq by (metis (full_types))
(* etc *)
end
Можно подумать, использовать defines:
locale defined_during =
fixes f :: "'a ⇒ 'b ⇒ 'c"
and g :: "'b ⇒ 'a"
and fg :: "'b ⇒ 'c"
defines fg_def: "fg b ≡ f (g b) b"
assumes "∀a. ∃b. f a b = fg b"
and univ: "(UNIV::'b set) = {b}"
begin
lemma "∀b b'. fg b = fg b'" using univ the_elem_eq by (metis (full_types))
end
но документ locales.pdf, кажется, предполагает, что он устарел (но в чем я не уверен):
Грамматика завершена, за исключением элементов контекста constrains и defines, которые предусмотрены для обратной совместимости.
Ctrl-парение над fg в лемме в локали defined_after называет его constant "local.fg", тогда как в defined_during это fixed fg\nfree variable. Однако он достигает defined_after_def равным defined_during_def (т. Е. В последнем нет никаких дополнительных параметров или допущений), чего не имеет третий вариант:
locale extra_defined_during =
fixes f :: "'a ⇒ 'b ⇒ 'c"
and g :: "'b ⇒ 'a"
and fg :: "'b ⇒ 'c"
assumes fg_def: "fg b ≡ f (g b) b"
and "∀a. ∃b. f a b = fg b"
and univ: "(UNIV::'b set) = {b}"
begin
lemma "∀b b'. fg b = fg b'" using univ the_elem_eq by (metis (full_types))
end
, который также имеет тот же текст Ctrl-hover для fg в лемме, что и локаль defined_during.
Возможно, что-то есть в одном из PDF-файлов на сайте или в файле NEWS, но я не могу найти ничего очевидного. isar-ref.pdf делает комментарий:
Элементы
Оба элемента assumes и defines вносят свой вклад в спецификацию локали. При определении операции, полученной из параметров, definition (§5.4) обычно более уместно.
Но я не уверен, как использовать эту информацию. Предположительно, это говорит о том, что когда кто-то не получает много пользы, выполняя то, о чем я спрашиваю, следует действовать так же, как в локали defined_after (если в кавычках не указано, что можно использовать definition внутри определения локали), что не является что я хочу. (Как отступление: первое предложение этой цитаты подсказало бы мне, что defines как-то эквивалентно третьему варианту, который вводит дополнительный параметр и допущение, но это не так. -than-кажется-Isabelle-jargon "спецификация локали" означает, что объясняет, почему текст Ctrl-hover отличается между первым и вторым вариантом, я не знаю.)