ML에서 로케일 가정과 변수를 사용하여 theorems과 용어로 어떻게 추상적으로 작업합니까?

Question

는 다음 로케일 정의 고려 : 나는 f의 정의 나 보조 정리 f_pos 작업을하려고하면, ISAR에서

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

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

end 

을, 로케일 가정 및 고정 변수 나에게서 숨겨져 있습니다. 예를 들어, thm f_def f_pos 수익률은 :

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

예상대로.

그러나 ML에서이 용어에 대해 논리적으로 생각하면 "숨겨진"고정 변수가 갑자기 나타납니다. ML {* @{thm f_def} |> prop_of *}, 예를 들면, 반환 고정 가변 af 함수의 매개 변수가된다

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")) 

한다.

ML에서 로케일 안에서 작업 할 수있는 방법이있어서 로케일 변수에 노출되지 않았습니까?

Answer 1

a 매개 변수가없는 f의 버전은 locale 명령에 의해 생성 된 약어 일뿐입니다. 이것은 그들이 약어 뒤에 숨겨진으로 사용자의 관점에서, f는, 로케일의 매개 변수가 표시되지 않음을 의미

local.f ≡ My_Theory.my_locale.f a 

: 특히, print_abbrevs 쇼를 입력. 그러나 장면 뒤에는 f에 항상 locale 매개 변수가 첨부되어 있으므로 명시 적으로 처리하기 위해 ML 코드를 코딩해야합니다.