메타 보편적으로 정량화 된 변수의 이름이 바뀐 이유는 무엇입니까?

Question

는 다음과 같은 바보 같은 예를 생각해

theory meta_all 
imports Main 
begin 

lemma strict_subset: "⟦ A ⊂ B ⟧ ⟹ ∃a ∈ B. a ∉ A" 
apply(blast) 
done 

lemma strict_subset2: "∀A B. A ⊂ B ⟶ (∃a ∈ B. a ∉ A)" 
apply(blast) 
done 

lemma "¬ (∃A. A ⊂ A)" 
apply(rule notI) 
apply(erule exE) 

다음으로는 strict_subset 보조 정리를 사용하여 A 및 B 모두 A를 대체하고자하는, 그리고 그것을 그렇게 할 것이다, 그러나 완전히 물리 치고, 기존 A에 Aa의 이름을 바꿉니다 보조 정리를 소개하는 목적. 내가 파생 된 보조 정리 strict_subset2 모든 것이 잘 밖으로 작동 사용하므로 내가 확신하는 경우

apply(insert strict_subset [where A="A" and B="A"]) 

내 논리는 소리입니다.

apply(insert strict_subset2) 
apply(erule_tac x="A" in allE, erule_tac x="A" in allE) 
apply(drule mp, assumption) 
apply(erule bexE, erule notE, assumption) 
done 

end 

점은 대부분의 표준 보조 정리가 strict_subset 아닌 형태 strict_subset2와 이사벨의 제조 업체의 형식은 내 자신의 첫번째 strict_subset2 자신을, ERGO 그래서, 내가 뭘해야 할 내가 의도하지 않았을 수 있다는 것입니다 뭔가 잘못.

A의 이름이 변경된 이유를 알고 싶습니다. 저는 이것이 유형이 정확히 맞으면 메타 범용적인 정량화가 문제가되지 않은 예를 보았다고 생각하기 때문에 타이핑 시스템과 관련이 있다고 생각합니다.

어떻게 든 A의 이름을 바꾸지 못하게 할 수 있습니까?

물론 저는 두 사람의 질문이 실제로 옳은 대답과 관련이 없게 될 가능성이 있습니다. 왜냐하면 저는 여전히 이사벨에게 신선합니다.

추신. 이자벨로부터 좋은 상징을 얻을 수 있습니까?

Answer 1

이것은 좁은 기술적 대답 일 뿐이며,이 실험의 경로가 의미가 있는지 의문을 제기하지 않습니다.

apply(insert strict_subset [where A="A" and B="A"]) 

문제의 subgoal의 상황에서

이 있었다 :

⋀A. A ⊂ A ⟹ False 

하지만 로컬 바인딩 (녹색) A는 subgoal의 소위 "매개 변수를"이다 목표 컨텍스트 내부에 숨겨져 있음을 의미합니다. strict_subset [where A="A" and B="A"]의 사용은 증거 텍스트이 아닌 증명 텍스트의 컨텍스트를 나타냅니다. 따라서 당신은 다른 (무료, 선언되지 않은) A을 얻습니다.이 또한 증명자 출력에서 ​​특별한 강조 표시로 표시됩니다.

암시 적 목표 컨텍스트에서 다이빙을하고 인스턴스화 할 수있게 해주는 특수 (매우 구식) 전술이 있습니다.

apply(cut_tac A = A and B = A in strict_subset) 

지금 당신이 목표 상태 내부의 녹색 A에 대한 인스턴스를 가지고 있지만, 그 또한 규칙의 형태가 너무 하위 목표로 분할되었다, 그리고 그 길을이 이상한 cut_tac 작품 : 다음은 그 예이다.

구조체 ISAR 증명 단계

• : 추론 방향의 지시와 특히 rule

• 약하게 구조화 단계 : erule, drule 기본적 이사벨/ISAR 증명 방법은 다음 catgories 있다는 것을

  는

  참고 , frule

• 암시적인 목표 c를 입력 할 수있는 구식 전술 에뮬레이션 타세의 매개 변수 : rule_tac, erule_tac, drule_tac, frule_tac

PS : 당신이 할 수있는 복사 - 붙여 넣기 유니 코드 출력 이자벨/jEdit과에서이 텍스트 편집기에.

Answer 2

apply (insert strict_subset)을 apply (drule strict_subset)으로 변경해야한다고 생각합니다. 그러면 증명은 apply simp으로 끝날 수 있습니다.

합니다 (insert foo 방법은 그것으로 제공 메타 한정사. 당신이 원하는 것은 함의 foo에 따라 가정 중 하나를 약화 drule foo 방법입니다 완료 추가 전제로 foo를 추가합니다.)

Answer 3

구조적 증명은 명명 설명한 문제를 방지하고 또한 단일 단계 추론을 수행 할 수 :

lemma "¬ (∃A :: 'a set. A ⊂ A)" 
proof 
    assume "∃A :: 'a set. A ⊂ A" 
    then obtain A :: "'a set" where "A ⊂ A" ..   (* by (rule exE) *) 
    then have "∃a ∈ A. a ∉ A" by (rule strict_subset) 
    then obtain a where "a ∉ A" "a ∈ A" ..    (* by (rule bexE) *) 
    then show False ..         (* by (rule notE) *) 
qed 

by rule..는 동일하다. 증명 단계 전에 using [[rule_trace]] (및 find_theorems)을 사용하여 어떤 규칙 rule이 사용 중인지 파악할 수 있습니다.

이 구조는 증명에서 어떤 일이 일어나는지 더욱 분명하게 만듭니다. 물론 적용 스타일은 확실히 더 탐험적인 터치를 가지고 있습니다. (이는 내가 종종 선호하는 이유입니다. 은을 찾을 수 있습니다). 그러나 구조화 된 교정은 더 많은 제어를 제공합니다.