У меня есть следующий код в Изабель: typedecl Person consts age :: "Person ⇒ int" lemma "⟦(∀p::Person. age p > 20);p ∈ Person⟧⟹ age p > 20" apply (auto) done Метод автоматического доказательства отлично работает и доказывает лемму!...

У меня есть следующий код в Изабель: typedecl type1 typedecl type2 consts A::"type1 set" B::"type2 set" Когда я хочу использовать операцию объединения с A и B, как показано ниже: axiomatization where c0: "A ∩ B = {}"...

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

Поддерживает ли Изабель индивидуальное различение падежей при доказательстве утверждений? Скажем, я хочу доказать утверждение для всех натуральных чисел n , но доказательство будет совершенно другим в зависимости от того, является ли n четным или...

Я хотел преобразовать это доказательство в Isar как упражнение ab (для себя, чтобы изучить Isar), используя только базовые правила естественного вывода (ND) из логики высказываний (например, notI , notE , impI , _4 _... и т. Д.). Я могу легко...

Я пытаюсь выучить язык Isar (по состоянию на Isabelle 2020) и понимаю команду note . Кажется, что это фундаментальный элемент языка, поскольку многие производные элементы определяются на его основе. Я не уверен, что он делает с точки зрения...

Я играл с примером из учебника Isabelle/HOL, чтобы лучше понять соответствие между доказательствами Isar и Tactics. Это версия, которая работает: lemma rtrancl_converseD: "(x,y) ∈ (r ^-1 )^* ⟹ (y,x) ∈ r^* " proof (induct y rule:...