このように仮定に近いサブゴールの証明はsimp任せに出来ますが，多くの場合いきなりサブゴールをshowするのは難しく，そこに至るまでの中間のサブゴールを適宜設けてそれらを証明，統合してshowとなります． もし今回の仮定 "a 0 = 0" からサブゴール "a 0 =…

また，1と名付けた事実の参照は，usingを用いて show "a 0 = 2 ^ 0 - 1" using 1 by simp 更にstaementの前に，fromを用いて from 1 show "a 0 = 2 ^ 0 - 1" by simp とすることもできます．仮定に限らず一般の定理の参照も同様ですが，from，usingでは変数…

つまり１つ目のサブゴールの証明は show "a 0 = 2 ^ 0 - 1" proof simp show "a 0 = 0" proof (simp add: 1) qed qed のようにsimpのみで賄えるわけですから，内側のproofを外側に重ねられそうです．実際 show "a 0 = 2 ^ 0 - 1" proof (simp add: 1) qed の…