보조 정리에서 보편적 인 정량화를 사용해야합니까?</p> <pre><code>datatype natural = Zero | Succ natural primrec add :: "natural ⇒ natural ⇒ natural" where "add Zero m = m" | "add (Succ n) m = Succ (add n m)" </code></pre> <p>를 들어

Question

내가 수학 당분간

lemma add_succ_right: "⋀ m n. add m (Succ n) = Succ (add m n)" 

을 입증, 보편적 인 정량화하는 것이 중요합니다. 그러나, simplifier에이 사실을 사용하기 위해,하지 않고 그것을하는 것이 좋습니다 :

lemma add_succ_right_rewrite: "add m (Succ n) = Succ (add m n)" 

내가 어떤 상황에서 선호해야 하나 이러한 버전에 대한 일반적인 지혜는 무엇입니까?

Answer 1

이자벨/HOL 보편적 보조 정리 문에서 변수를 통해 정량화하는 방법은 세 가지가 있습니다 또한, 보조 정리 문에서 자유 변수가 자동으로 정량화 될

lemma 1: "⋀m n. add m (Succ n) = Succ (add m n)" 

lemma 2: 
    fixes m n 
    shows "add m (Succ n) = Succ (add m n)" 

lemma 3: "∀m n. add m (Succ n) = Succ (add m n)" 

: 보조 정리 1, 2

lemma 4: "add m (Succ n) = Succ (add m n)" 

및 4는 동일한 정리로 나중에 동일한 방법으로 사용될 수 있습니다. 보조 정리 3은 메타 논리로부터의 정량화 대신에 HOL 보편적 인 한정어를 사용한다. 따라서, 보조 정리 3에서 수량 기호를 인스턴스화하기 위해서는 추가 작업이 필요합니다. 따라서이 버전은 특별한 상황에서만 사용해야합니다.

lemma 1의 버전은 Isar 언어가 현재 상태가 아니었기 때문에 날짜가 구식입니다. 따라서 버전 2 (명시 적으로 수량화 된 변수를 언급하려는 경우) 또는 4 (그렇지 않은 경우)를 선호하는 것이 좋습니다.