'linordered_field_class.frac_le'규칙이 작동하지 않는 이유는 무엇입니까? (Isabelle)

Question

나는 linordered_field_class.frac_le 규칙을 Isar 증명으로 사용하려고합니다. 다음은 코드 조각입니다 (이전의 증명 부분에 따라 다를 수 있지만 이는 거의 없습니다). n은 nat 유형입니다.

... 
    then have 4:"2 ≤ (2^(n+1)::real)" by simp 
    have 1:"(0::real)≤(1::real)" by simp 
    have 2: "1≤(1::real)" by simp 
    have 3:"(0::real)≤(2::real)" by simp 
    from 1 2 3 4 have "1/(2^(n+1))≤1/(2::real)" by (rule linordered_field_class.frac_le) 

나는 규칙을 올바르게 적용했다고 생각하지만 '증명을 완료하지 못했습니다.'라는 불만을 토로합니다. 나는 그것이 유형 오류일지도 모른다고 생각했기 때문에 :: real의 과도 함을 고칠 수 있었지만 해결할 수 없었습니다. 누구든지 문제가 무엇인지, 문제를 해결하는 방법을 알고 있습니까? 또는 그런 종류의 성명을 증명할 수있는 또 다른 방법입니다.

Answer 1

규칙을 보면 세 번째 전제는 0 < ?w의 형식이지만 세 번째 위치에서 체인을 연결한다는 사실은 0 ≤ 2입니다. 0 < 2으로 바꾸면 정상적으로 작동합니다.

auto intro: frac_le 또는 simp add: divide_simps 또는 simp add: field_simps을 작성하여 많은 지루한 수동 단계를 절약 할 수 있습니다. Isabelle의 대수 추론은 기존 자동화를 잘 사용하지 않는 한 매우 지루한 경향이 있습니다.