g `!x. asn (sin x) = pi / &2 - abs (pi / &2 - (x - &2 * pi * floor ((x + pi / &2) / (&2 * pi))))` ;; e( GEN_TAC );; e( SUBGOAL_THEN `asn (sin x) = asn (sin (pi / &2 - abs (pi / &2 - (x - &2 * pi * floor ( (x + pi / &2) / (&2 * pi) ) ) )) )…

g `!(x:int). x <= &101 ==> (?n k. 91 <= k /\ k <= 101 /\ x = &k - &(11 * n))` ;; e( REPEAT STRIP_TAC );; e( SUBGOAL_THEN `?m:num. &101 - x:int = &m` MP_TAC );; e( ASM_CASES_TAC `&101 - x:int = &0` );; e( EXISTS_TAC `0` THEN ASM_SIMP_TAC []…

内容はこれからですが．．． http://youtu.be/kzGdyRruGo8 http://youtu.be/H3-qtqrjUiM http://youtu.be/AhybiY0JHvg http://youtu.be/NMSzj_xjZxI http://youtu.be/IvaNo8eMN-Q http://youtu.be/VE1nTWgB6eM まとめて http://www.youtube.com/watch?v=kzGd…

PVS にはカユイところに手が届く帰納法が色々と用意されています．例えば subrange_inductions[i: int, j: upfrom(i)]: THEORY BEGIN k: VAR subrange(i, j) p: VAR pred[subrange(i, j)] subrange_induction: LEMMA (p(i) AND (FORALL k: k < j AND p(k) IM…

うらなりに見える Yices ですが．．． http://d.hatena.ne.jp/ehito/searchdiary?word=%C3%E6%B4%D6%C3%CD の例です． lem1:lemma A(0)<x & (exists m:x<=A(m)) => (exists n:A(n)</x>

各システムにおける実数の扱いが平明に記されています． http://hal.inria.fr/docs/00/80/69/20/PDF/article.pdf

以前 Isar で書いた自然数の分解 http://d.hatena.ne.jp/ehito/20130514/1368492752 の PVS 版です． lem_odd_even:lemma forall(n:nat):(n=0 or exists(x:posint,y:nat):odd?(x) & n=x*2^y) %|- lem_odd_even : PROOF %|- (then (induct "n" 1 "NAT_inducti…

Isar で書くと lemma fixes a b :: "real" shows "(a ≠ 0 ∨ a = 0 ∧ b = 0) = (∃x. a * x = b)" (is "?P = ?Q") proof assume ?P moreover have "a ≠ 0 ==> a * (b / a) = b" by auto moreover have "a = 0 ∧ b = 0 ==> ?Q" by auto ultimately show "?Q" by…

PVS のプルーフマネージャは非常に上手く設計されており，ロジカルな展開で迷うことはまずありません． lem0:lemma forall(a,b:real):(a/=0 or (a=0 & b=0)) <=> exists(x:real):a*x=b %|- lem0 : PROOF %|- (then (skeep) %|- (spread (split) %|- ((then (…