Вопросы по теме 'isabelle'
Применять метод тогда и только тогда, когда он решает текущую цель
Иногда, когда я пишу доказательства в стиле применения, мне нужен способ изменить метод доказательства foo , чтобы
Попробуйте foo на первой цели. Если это решает цель, хорошо; если это не решает ее, вернуться в исходное состояние и...
217 просмотров
schedule
29.02.2024
Как удалить повторяющиеся подцели в Isabelle?
В Изабель иногда встречается сценарий, в котором есть повторяющиеся подцели. Например, представьте себе следующий сценарий проверки:
lemma "a ∧ a"
apply (rule conjI)
с целями:
proof (prove): step 1
goal (2 subgoals):
1. a
2. a...
244 просмотров
schedule
29.12.2023
Как я могу указать заголовок и пакет сгенерированного кода?
Я генерирую код Scala с Изабель. Как указать заголовок для моего файла Scala? Например, я хотел бы иметь что-то вроде этого:
// Generated code. Generated with Isabelle/HOL
// File: blubb.thy line:1234
// Date: Wed, 27.03.2013
// exported code...
144 просмотров
schedule
19.12.2023
Изабель: Почему я получаю совершенно разные результаты при запуске try и sledgehammer?
Когда я смотрю только (это не указано в заголовке) на результаты Sledgehammer, вывод try часто дает разные результаты от sledgehammer, в то время как запуск sledgehammer напрямую дает нулевые (!) результаты.
Теперь я знаю, что целью дизайна...
265 просмотров
schedule
22.03.2024
Что такое шаблон типа Quotient в Изабель?
Что такое "шаблон типа частного" в Изабель?
Я не нашел объяснений в Интернете.
529 просмотров
schedule
30.09.2022
Как передать значение ML в качестве аргумента внешней синтаксической команде?
Я определяю команду внешнего синтаксиса, imake для записи некоторого кода в файл и выполнения некоторых других действий. Предполагаемое использование выглядит следующим образом:
theory Scratch
imports Complex_Main "~/Is0/IsS"
begin
imake...
73 просмотров
schedule
02.11.2023
Использование классов типов для перегрузки нотации конструкторов (теперь проблема с пространством имен)
Это производный вопрос от существующих констант (например, конструкторов) в экземплярах классов типов. .
Короткий вопрос заключается в следующем: Как я могу предотвратить ошибку, возникающую из-за free_constructors , чтобы я мог объединить две...
99 просмотров
schedule
04.12.2023
Проверка завершения для типов продуктов
Изабель принимает следующее определение функции, поэтому средство проверки завершения им довольна:
datatype 'a List = N | C 'a "'a List"
fun dequeue' :: "'a List × 'a List ⇒ ('a option × 'a queue)" where
"dequeue' (N, N) = (None, AQueue N N)"...
37 просмотров
schedule
07.11.2022
Дискриминант с неравенствами
Я новичок в использовании Изабель. Я пытался найти лемму, чтобы решить эту
lemma
fixes x y z k :: real
assumes "x ≠ 0"
and "⋀k. (x*(k)⇧2 + y*k + z) ≥0"
shows "discrim x y z ≤ 0"
использование кувалды не дало мне никаких результатов....
79 просмотров
schedule
17.10.2022
Доказательство мощности более сложного множества
Предположим, у меня есть набор, включающий три соединения {k::nat. 2<k ∧ k ≤ 7 ∧ gcd 3 k = 2} .
Как я могу доказать в Изабель, что мощность этого множества равна 1? (А именно, только k = 6 имеет gcd 3 6 = 2.) То есть, как я могу доказать...
153 просмотров
schedule
11.10.2022
Isabelle2017 не может быть открыт, потому что это от неизвестного разработчика
Настройки безопасности на моем MacBook Pro позволяют устанавливать только приложения из App Store и от определенных разработчиков. Эта политика была установлена моим работодателем, и я не могу ее изменить. Как следствие, я не могу запустить...
172 просмотров
schedule
01.05.2024
Как упростить индуктивный предикат вычислением?
Я определил очень простую объектно-ориентированную модель. Модель определяет набор классов и набор ассоциаций.
nonterminal fmaplets and fmaplet
syntax
"_fmaplet" :: "['a, 'a] ⇒ fmaplet" ("_ /↦⇩f/ _")
"_fmaplets" :: "['a, 'a] ⇒...
82 просмотров
schedule
10.10.2022
Выразите параметрическую аббревиатуру в Isabelle
Я хочу сократить класс эквивалентности точки:
r `` {p}
to
[p]
Каков правильный путь к этому в Изабель?
41 просмотров
schedule
19.11.2022
Доказательство теоремы о классах типов в Изабель
Я должен доказать тривиальность, используя классы типов:
class order =
fixes lesseq :: " 'a ⇒ 'a ⇒ bool" (infix "≼" 50)
assumes refl: "x ≼ x"
and trans: "x ≼ y ⟹ y ≼ z ⟹ x ≼ z"
and...
54 просмотров
schedule
12.12.2022
Взаимодействие с Изабель без графического интерфейса
Я пытаюсь реализовать версию Isabelle / JEdit для командной строки, чтобы
Запустите сервер Isabelle на другом докере / машине
Разрешить интеграцию большего количества редакторов, таких как Vim или Emacs
Разрешить автоматизированным агентам...
61 просмотров
schedule
20.12.2023
Можно ли в Isabelle добавить предположения в область определения функции?
Я не уверен, можно ли публиковать такой дополнительный вопрос, но я все равно это сделаю.
Итак, несколько дней назад я разместил этот вопрос: Как удалить все вхождения подмножества в Isabelle?
Я думал, что ответ был отличным, но при попытке...
70 просмотров
schedule
18.03.2024
