ロケールのパラメーターに何らかの定義があり、ロケールの仮定を書きやすく、読みやすく、理解しやすくする場合 (関数が非常に複雑であるため、仮定のステートメントまたはその名前が単純化されるため)仮定を読みやすく理解しやすくします)、その関数を定義する最良の方法は何ですか?
人為的な例として、関数を仮定のステートメントに組み込みたいとし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
fgロケールのレンマにCtrl キーを押しながらホバリングすると、 defined_afteras という名前になりますconstant "local.fg"が、 in defined_duringit isfixed fg\nfree variableです。defined_after_defしかし、それは等しいことを達成しdefined_during_defます (つまり、後者には追加のパラメーターや仮定はありません)、3 番目のオプションはそうではありません:
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
ロケールと同じfgように、補題にも同じ Ctrl-hover テキストがあります。defined_during
Web サイトの PDF の 1 つまたは NEWS ファイルに何か記載されているのかもしれませんが、明らかなものは見つかりません。isar-ref.pdf は次のようにコメントしています。
assumes要素と要素の両方definesがロケール仕様に貢献します。パラメーターから派生した操作を定義する場合、definition通常は (§5.4) の方が適切です。
しかし、私はこの情報をどのように使用するかわかりません。おそらく、私が求めていることを実行してもあまり利益が得られない場合は、ロケールのように続行する必要があると言っているのでしょうdefined_after(引用符がdefinitionロケール定義内で使用できることを意味しない限り)。これは私が望んでいるものではありません。（余談ですが、この引用の最初の文はdefines、追加のパラメーターと仮定を導入する3番目のオプションと何らかの形で同等であることを私に示唆していたでしょうが、そうではありません。 it-appears-Isabelle-jargon 「ロケール仕様」とは、最初のオプションと 2 番目のオプションで Ctrl-hover テキストが異なる原因を説明することを意味しますが、私にはわかりません。)