-4

見せ方のルール知ってる人いますか

"¦c¦<1 ==> (λn. c^n) ---> 0"

リアルで？

「クエリ」パネルを使用して、次のルールを見つけました。

Limits.LIMSEQ_rabs_realpow_zero2: ¦?c¦ < 1 ⟹ op ^ ?c ---> 0
Limits.LIMSEQ_rabs_realpow_zero: ¦?c¦ < 1 ⟹ op ^ ¦?c¦ ---> 0
Limits.LIMSEQ_realpow_zero: 0 ≤ ?x ⟹ ?x < 1 ⟹ op ^ ?x ---> 0

私はどういうop意味で少し混乱していますが。

4

1 に答える 1

3

あなたが証明しようとしている補題は正確にLIMSEQ_rabs_realpow_zero2です。したがって、 で目標を証明できますapply (rule LIMSEQ_rabs_realpow_zero2)。

たとえば、イザベルで試しterm "λx y. x + y"てterm "λx. 1 + x"みてください。出力は、それぞれop +とになりop + 1ます。

はop ^単に の省略形ですλx y. x ^ y。一般にop、Isabelle は二項中置演算子を 2 つの引数を持つ関数に変換するための構文です (ML に少し似ています)。

于 2016-12-28T22:15:41.123 に答える