isar

-1зной

1ответ

Что делает глубина в выводе Isar Virtual Machine?

Вот доказательство: theory Example imports Main begin datatype natural = Zero | Succ natural lemma "⋀ n. n = Succ m ⟹ n ≠ Zero" proof - fix n assume "n = Succ m" from this show "n ≠ Zero"

1зной

2ответ

Введение Правило «∀r> 0» в Isabelle

Когда у меня есть цель, такие как "∀x. P x" в Изабеллу, я знаю, что я могу написать show "∀x. P x" proof (rule allI) Однако, когда цель "∀x>0. P x", я не могу этого сделать , Есть ли аналогичное пр

1зной

1ответ

Sledgehammer дает достаточных доказательств Tactic

У меня есть theory Even imports Main begin inductive structural_even :: "nat ⇒ bool" where "structural_even 0" | "structural_even n ⟹ structural_even (Suc(Suc n))" fun computat

1зной

2ответ

Доказательство простой арифметической инструкции с переписыванием в Isabelle

Я пытаюсь доказать различие большого дела в Изабель для некоторого (концептуально) простого арифметического утверждения. Во время доказательства я наткнулся на следующую подцель. ⋀d l k. 0 < d ⟹

2зной

1ответ

Использование «также есть ... наконец» в Isabelle

я обычно думаю о also have, как работает так: have "P r Q1" by simp also have "... r Q2" by simp also have "... r Q3" by simp ... also have "... r Qn" by simp finally have "P r Qn+1" by simp гд

-4зной

1ответ

Предела с^п (с |c| <1) является 0 (Isabelle)

Кто-нибудь знают правила для показа "¦c¦<1 ==> (λn. c^n) ---> 0" в реале? Я нашел следующие правила с помощью «запроса» панели: Limits.LIMSEQ_rabs_realpow_zero2: ¦?c¦ < 1 ⟹ op^?c ---> 0 Limits.LIMS

1зной

1ответ

Определение quotient_type в Isabelle

Я все еще пытаюсь рассуждать о семантическом равенстве в Изабель. Я хочу сравнить две формулы и посмотреть, равны ли они. Мне сказали, что для этого мне нужны quotienttypes. Итак, я попытался определи