Вопросы по теме 'isabelle'
Ядро верификатора в Isabelle / HOL
Вопрос
Каков основной алгоритм верификатора Isabelle / HOL?
Я ищу что-нибудь на уровне метациркулярного оценщика схем.
Разъяснение
Меня интересует только Verifier , а не стратегии автоматического доказательства теорем.
Контекст
Я...
592 просмотров
schedule
03.07.2022
Генерация кода из локалей без интерпретации
Я хотел бы сгенерировать код из locale определений напрямую, без интерпретации. Пример:
(* A locale, from the code point of view, similar to a class *)
locale MyTest =
fixes L :: "string list"
assumes distinctL: "distinct L"
begin...
152 просмотров
schedule
13.08.2022
Как просмотреть переменные скрытого типа в целях доказательства Изабель?
В Изабель часто можно достичь целей доказательства, когда промежуточный тип терминов имеет решающее значение для правильности доказательства. Например, рассмотрим следующую лемму, преобразующую nat 42 в 'a word , а затем обратно:
theory Test...
924 просмотров
schedule
15.11.2022
Как в Isabelle / jEdit заключить предположения в скобки?
Когда цели отображаются Изабель в ProofGeneral, предположения отображаются в скобках следующим образом:
Однако в Isabelle / jEdit это, похоже, изменилось на стрелки мета-импликации:
Хотя я понимаю, что первое несколько нестандартно,...
613 просмотров
schedule
24.04.2022
Как скрыть многократно определенные константы
Этот вопрос расширяет вопрос Как скрыть определенные константы .
Я импортирую теории A , B и C , возможно, в будущем также D , E , ... Все теории определяют функцию f . Я хочу скрыть определение f в моей текущей теории без изменения...
99 просмотров
schedule
27.07.2023
Какую библиотеку Isabelle повторно использовать для выражения того, что некоторая функция является линейным порядком (на некотором наборе)
В моей формализации Изабель я имею дело с конечными наборами натуральных чисел, и на этих наборах я хотел бы рассмотреть функции, которые обладают свойством быть линейным порядком.
Я вижу, что в библиотеке есть несколько различных формализаций...
90 просмотров
schedule
07.08.2022
Замещающее поведение в Изабель
У меня есть следующая лемма в Изабель:
lemma lem1: "xs ∈ I
⟹ map h1 xs = map (λx. if ∃ys ∈ I. x ∈ set ys then h1 x else h2 x) xs"
by(auto)
который я хочу применить, чтобы показать следующее (с тем же лямбда-выражением):
lemma "xs ∈ I ⟹...
613 просмотров
schedule
24.01.2023
Изабель: запустите кувалду на другом компьютере, а не на моем обычном ПК, на котором работает Isabelle / jEdit
Я работаю с Isabelle / jEdit на своем рабочем столе.
У моего ноутбука 4 ядра, то есть 4 процессора. Но у меня также есть серверный компьютер в соседней комнате. Сервер имеет более 20 процессоров.
Обычно я запускаю sledgehammer и try...
129 просмотров
schedule
07.12.2023
Как описать точки неточности внутри (| |) в Isabelle?
Я знаю, что в Изабель y = x(| i := 1 |) означает, что x и y имеют и имеют только одну точку, i . Это очень точно.
Но что, если я не знаю значения i в y или не могу легко записать его?
Пробовал for all item != i. y = x , но когда i...
70 просмотров
schedule
03.06.2023
Новое изображение кучи Isabelle / Simpl не отображается в jEdit
Недавно я начал использовать Isabelle / jEdit. Я создал образ кучи для записи Simpl AFP. Я использовал инструмент командной строки isabelle build для создания нового изображения. Я могу видеть и использовать изображение с ProofGeneral и Isabelle...
191 просмотров
schedule
25.10.2022
загрузка предварительно скомпилированного образа кучи в Isabelle
Следуя инструкции -use-persistent-heap-images-to-make-loading-of-theories-faster-in-isabelle и еще один совет Я создал образ для Nominal Isabelle:
isabelle build -v -b -d . Nominal2
Образ кучи был создан в ~/.isabelle:...
461 просмотров
schedule
14.03.2023
let-инструкция с оператором НЕКОТОРЫЕ
Я часто хочу писать выражения этой формы
let x = SOME x. x ∈ e1
in e2
это; пусть x будет членом арбитра e1 в e2 . Это довольно многословно и кажется немного странным, что нужно дважды связывать x . Есть ли способ выразить это лучше?
312 просмотров
schedule
19.11.2022
Как доказать основные факты о типах данных и кодовых типах?
Я хотел бы доказать некоторые основные факты о datatype_new и codatatype : у первого нет бесконечного элемента, а у второго он есть.
theory Co
imports BNF
begin
datatype_new natural = Zero | Successor natural
lemma "¬ (∃ x. x =...
147 просмотров
schedule
30.10.2022
Индукция по длине, а затем по правилу индукции для контекстно-свободной грамматики (пример из prog-proof)
Я новичок в Isabelle / HOL (хотя и не в HOL), поэтому я решил начать обучение с работы с примерами в превосходном " prog-proof "учебник .
Я застрял на вопросе по грамматике без контекста (упражнение 3.5 на стр. 43). В этом вопросе вы получите две...
503 просмотров
schedule
15.02.2023
Факторизация предпосылки леммы в качестве определения приводит к сбою в применении метода доказательства (авто) в isabelle
У меня есть следующий код в Изабель:
typedecl Person
consts age :: "Person ⇒ int"
lemma "⟦(∀p::Person. age p > 20);p ∈ Person⟧⟹ age p > 20"
apply (auto)
done
Метод автоматического доказательства отлично работает и доказывает лемму!...
77 просмотров
schedule
30.03.2023
Нетипизированные операции над множествами в Isabelle
У меня есть следующий код в Изабель:
typedecl type1
typedecl type2
consts
A::"type1 set"
B::"type2 set"
Когда я хочу использовать операцию объединения с A и B, как показано ниже:
axiomatization where
c0: "A ∩ B = {}"...
181 просмотров
schedule
30.09.2022
неверная функция карты при определении корекурсивного дерева
Я делаю свои первые эксперименты с codatatype , но я застрял довольно рано. Я начал с этого определения ветвящегося, возможно, бесконечного дерева:
codatatype (lset: 'a) ltree = Node (lnext : "'a ⇒ 'a ltree option")
и некоторые определения...
83 просмотров
schedule
16.06.2023
Решение уравнений с ассоциативным и коммутативным оператором
Рассмотрим такую цель в Изабель (и не беспокойтесь о ccProd и ccFromList ):
ccProd {x} (set xs) ⊔ (ccProd {x} (set ys) ⊔ (ccFromList xs ⊔ (ccFromList ys ⊔ ccProd (set xs) (set ys)))) =
ccProd {x} (set xs) ⊔ (ccFromList xs ⊔ (ccFromList ys ⊔...
119 просмотров
schedule
19.03.2023
Сборка Isabelle на Linux ARM
Кто-нибудь пытался собрать Isabelle на Linux ARM? У меня Fedora 21 на armv7hl. Мне удалось собрать Pure, но не HOL. Кажется, дело в памяти, но я не уверен. Есть ли способ построить его поэтапно? содержимое heaps / polyml-5.5.2_armv7l-linux после...
99 просмотров
schedule
09.05.2022
Автоматическая проверка Изабель
Я начал работать с Изабель несколько недель назад, и мне трудно делать некоторые доказательства автоматически. Я просто использовал правило less_induct, чтобы показать свойство в списке.
theorem cuenta_ordena_1:
"cuenta (ordena xs) y = cuenta xs...
146 просмотров
schedule
10.07.2022
