2

次のロケール定義を検討してください。

locale my_locale =
  fixes a :: nat
  assumes "a > 0"
begin

definition "f n ≡ a + n"
lemma f_pos: "f x > 0"
  sorry

end

Isarでは、fまたはの見出語の定義を操作しようとするf_posと、ロケールの仮定と固定変数が表示されなくなります。たとえば、次をthm f_def f_pos返します。

f ?n ≡ a + ?n
0 < f ?x

予想通り。

ただし、MLでこれらの用語について推論しようとすると、「隠された」固定変数が突然公開されます。ML {* @{thm f_def} |> prop_of *}たとえば、次を返します。

Const ("==", "nat ⇒ nat ⇒ prop") $
 (Const ("TestSimple.my_locale.f", "nat ⇒ nat ⇒ nat") $
   Free ("a", "nat") $ Var (("n", 0), "nat")) $
 (Const ("Groups.plus_class.plus", "nat ⇒ nat ⇒ nat") $
   Free ("a", "nat") $ Var (("n", 0), "nat"))

ここで、固定変数aは関数のパラメーターになりますf。

MLのロケール内で作業して、そのようなロケール変数にさらされないようにする方法はありますか？

4

1 に答える 1

2

fパラメータを持たないバージョンは、a単にコマンドによって生成された略語であるように見えますlocale。特に、入力すると次のようにprint_abbrevs表示されます。

local.f ≡ My_Theory.my_locale.f a

これは、ユーザーの観点からはf、略語の後ろに隠れているため、ロケールパラメータがないように見えることを意味します。ただし、舞台裏でfは常にロケールパラメータが付加されているため、MLコードを明示的に処理するようにコーディングする必要があります。

于 2013-03-11T06:21:39.873 に答える