Вопросы по теме 'isabelle'
Как я могу легко написать простые тактики на уровне машинного обучения Изабель?
В теоретическом файле Изабель я могу написать простые однострочные тактики, например следующие:
apply (clarsimp simp: split_def split: prod.splits)
Однако я обнаружил, что, когда я начинаю писать код ML для автоматизации доказательств, для...
1010 просмотров
schedule
22.02.2023
Использование кортежей в определениях
Я хочу создать определение, аргументом которого является кортеж.
definition my_def :: "('a × 'a) ⇒ bool" where
"my_def (a, b) ⟷ a = b"
Однако это не принято. Сообщение об ошибке
Bad arguments on lhs: "(a, b)"
The error(s) above...
455 просмотров
schedule
28.01.2024
Отбросьте переменную в цели в стиле применения
Недавно узнав, , как удалить нежелательную предпосылку в стиле применения доказательство , теперь мне интересно, как удалить ненужную переменную . То есть, допустим, у меня есть цель
1. !!x y z. A ⟹ B ⟹ C
где y не появляется в A , B...
94 просмотров
schedule
27.06.2022
Почему переименовывается метауниверсально квантифицированная переменная и как это предотвратить?
Рассмотрим следующий глупый пример
theory meta_all
imports Main
begin
lemma strict_subset: "⟦ A ⊂ B ⟧ ⟹ ∃a ∈ B. a ∉ A"
apply(blast)
done
lemma strict_subset2: "∀A B. A ⊂ B ⟶ (∃a ∈ B. a ∉ A)"
apply(blast)
done
lemma "¬ (∃A. A ⊂ A)"
apply(rule...
517 просмотров
schedule
22.01.2024
Как скрыть определенные константы
Когда я импортирую файлы теории, которые поставляются с определенными константами (для рекурсивных функций или определений), такими как f , как я могу скрыть такую константу в текущем файле теории? Другими словами, я хочу убедиться, что f...
164 просмотров
schedule
04.01.2023
Какие определения типов допустимы в местных контекстах?
В файле NEWS Изабель я нашел
Команда typedef теперь работает в локальном теоретическом контексте — без введения зависимостей от параметров или предположений, что невозможно в Isabelle/Pure/HOL. Обратите внимание, что логическая среда может...
570 просмотров
schedule
22.07.2022
Изабель: как напечатать результат 1 + 2?
это вопрос новичка.
Я прохожу учебник "Программирование и проверка в Isabelle/HOL".
Я хочу напечатать результат «1 + 2».
Поэтому я написал:
value "1 + 2"
Который дает:
"1 + (1 + 1)"
:: "'a"
Я хотел бы увидеть результат, то...
650 просмотров
schedule
22.05.2023
Изабель: Кувалда находит доказательство, но оно не работает
Часто у меня возникает проблема, что sledgehammer находит доказательство, но когда я вставляю его, оно не прекращается. Думаю, sledgehammer - одна из самых важных частей Изабель, но потом это начинает раздражать, если доказательство не удается....
1685 просмотров
schedule
30.03.2022
Изабель: максимальное значение в векторе
Я хотел бы найти максимум в векторе натуральных чисел. Однако вектор (т. е. «vec») отличается от набора или списка. Я думал о нескольких идеях, которые не сработали, вроде выравнивания или поднятия типа vec или определения рекурсивной функции....
318 просмотров
schedule
16.11.2022
Почему мое определение функции, которая выбирает элемент из конечного набора, несовместимо?
Я хотел бы рассуждать о функциях, которые выбирают один элемент из конечного множества.
Я попытался определить предикат, который сообщает мне, является ли некоторая данная функция такой функцией «выбора»:
definition chooser :: "('a set ⇒ 'a) ⇒...
128 просмотров
schedule
12.03.2022
Как включить трассировку в Isabelle / jEdit
Я фанат vim , но только emacs имеет эту среду Isabelle / HOL. jEdit великолепен, но я не могу использовать
using [[simp_trace=true]]
как в emacs .
Как включить «Трассировку» в jEdit ?
1867 просмотров
schedule
07.01.2023
Как определить «Большинство» в Isabelle/FOL?
Я пытаюсь дополнить FOL.thy квантором MOST , который я намереваюсь определить как простое большинство, т. е.
(MOST x. P(x)) ==> card P(x) > card ~P(x).
Я не знаю, как изменить файл FOL.thy . Под axiomatization думал добавить:...
240 просмотров
schedule
17.12.2022
Изабель: степень многочлена, умноженная на константу
Я работаю с библиотекой HOL/Library/Polynomial.thy .
Простое свойство не сработало. Например, степень 2x *2 равна степени 2x -
Как я могу доказать леммы (т.е. убрать извинения):
lemma mylemma:
fixes y :: "('a::comm_ring_1 poly)"...
105 просмотров
schedule
18.06.2022
Изабель: Метис: состояние доказательства содержит универсальную сортировку {}
Метис предупреждает меня:
Metis: Proof state contains the universal sort {}
("HOL/Tools/Metis/metis_tactic.ML")
Что означает это предупреждение? Означает ли это, что метис-доказательство «менее надежно», чем без предупреждения?
124 просмотров
schedule
05.06.2022
Доказательство A == ›B ==› C == ›B в Изабель
Я озадачен доказательством
A ==> B ==> C ==> B
в Изабель. Очевидно, вы могли
apply simp
но как я могу доказать это с помощью правил?
Как вариант, есть ли способ сбросить использованные simp правила? Спасибо.
285 просмотров
schedule
03.06.2022
Изабель: остановить simp от разделения кортежа
Как я могу остановить метод simp от разделения кортежа на его компоненты?
Пример . Если я напишу
fun foo where "foo z = blah z"
lemma "∃z :: nat × nat × nat × nat × nat. foo z"
состояние доказательства - ∃z. foo z . Если я тогда...
96 просмотров
schedule
05.01.2023
Обеспечить различимость типов данных
Я определил следующий тип данных в Isabelle
datatype bc_t = B | C
и не вижу, как доказать следующую основную лемму
lemma "∀ x::bc_t . (x=B ⟶ x≠C)"
При предположении B≠C доказательство проходит:
lemma "⟦B≠C; x=B⟧ ⟹ x≠C"
by...
106 просмотров
schedule
22.10.2022
Unfold/simp не влияет на доказательство создания экземпляра класса типа primrec.
Еще несколько дней назад я всегда определял тип, а затем доказывал теоремы непосредственно о типе. Теперь я пытаюсь использовать классы типов.
Проблема
Проблема в том, что я не могу создать экземпляр cNAT для моего типа myD ниже, и,...
115 просмотров
schedule
26.08.2022
Как явно связать переменные в доказательстве индукции?
У меня есть тип данных и индуктивный предикат над ним (который на самом деле является семантикой небольшого шага какой-то системы перехода):
datatype dtype = E | A | B dtype
inductive dsem :: "dtype ⇒ dtype ⇒ bool" where
"dsem A E"
| "dsem (B...
170 просмотров
schedule
20.06.2022
Как мне написать эту функцию на SML
Я пытаюсь написать функцию в Isabelle для некоторых задач в задании, и я хотел убедиться, что моя функция работает правильно, поэтому я подумал о тестировании ее в SML, но, похоже, не могу понять, как ее написать . Я никогда не использовал / не...
211 просмотров
schedule
23.03.2022
