Вопросы по теме 'isabelle'
Частичные функции по сравнению с недоопределенными полными функциями
Предположим, у меня есть набор A ⊆ nat . Я хочу смоделировать в Изабель функцию f : A ⇒ Y . Я мог бы использовать либо:
частичная функция, то есть функция типа nat ⇒ Y option или
общая функция, т. е. функция типа nat ⇒ Y , которая не...
419 просмотров
schedule
07.09.2022
Как правильно определить таблицу конечного умножения в Isar?
Предположим, у меня есть бинарный оператор f :: "sT => sT => sT" . Я хочу определить f , чтобы он реализовывал таблицу умножения 4x4 для группы 4 Клейна, показанную здесь в Wiki:
http://en.wikipedia.org/wiki/Klein_four-group
Здесь...
410 просмотров
schedule
17.02.2022
Изабель: транспонировать матрицу, включающую постоянный множитель
В моей теории Изабель у меня есть матрица с постоянным множителем:
...
k :: 'n and c :: 'a
(χ i j. if j = k then c * (A $ i $ j) else A $ i $ j)
Я могу вычислить транспонированную матрицу:
(transpose (χ i j. if j = k then c * (A $ i $ j)...
203 просмотров
schedule
30.08.2023
Как мне отобразить, какие классы типов созданы для nat, int и т. Д.?
Я сделал grep для папки src / HOL с instance+[ ]nat и instantiation+[ ]nat , и, возможно, я нашел все классы типов, которые были созданы для nat .
Поскольку важно, чтобы я также смотрел, как были созданы экземпляры int , rat и real , было...
98 просмотров
schedule
21.10.2022
Доступ к первому элементу матрицы в Isabelle
Доступ к «первому» элементу матрицы
Я хочу написать доказательство тривиального случая определителя матрицы, когда матрица состоит всего из одного элемента (т. е. мощность 'n равна единице).
Таким образом, определитель (или det A ) является...
127 просмотров
schedule
04.04.2022
Равенство между терминами Изабель, в которых используются НЕКОТОРЫЕ
Я немного удивлен, что
value "let x = SOME n. n ∈ {1::int,2} in x = x"
возвращает True . После β-расширения и α-переименования этот термин такой же, как:
value "(SOME na. na ∈ {1::int,2}) = (SOME nb. nb ∈ {1::int,2})"
Я не понимаю,...
79 просмотров
schedule
20.04.2022
Установка [no_vars] для всей теории
У меня есть теория Изабель, которая собирает все мои результаты и представляет только их, поэтому сейчас я бы применил [no_vars] ко всем своим @thm антикавычкам. (Это подавляет вопросительные знаки в схематических переменных, которые нежелательны...
41 просмотров
schedule
13.11.2022
Как правильно использовать ключевое слово «теорема» в Изабель?
Я получил следующий код со страницы Википедии Изабель:
theorem sqrt2_not_rational:
"sqrt (real 2) ∉ ℚ"
proof
assume "sqrt (real 2) ∈ ℚ"
then obtain m n :: nat where
n_nonzero: "n ≠ 0" and sqrt_rat: "¦sqrt (real 2)¦ = real m / real n"...
429 просмотров
schedule
31.12.2022
Транзитивное закрытие тождественного отношения
Я не могу доказать следующее lemma в Изабель :
lemma "Id^* = Id"
Есть идеи, как это доказать?
195 просмотров
schedule
29.03.2022
Синтаксис преобразователя инфиксного отношения в Isabelle
Дано
notation
rtranclp ("(_^**)" [1000] 1000)
Я могу писать, учитывая инфикс op ⇒
"op ⇒⇧*⇧* x x'"
но не намного читабельнее и красивее
"x ⇒⇧*⇧* x'"
Я знаю, что для каждого конкретного отношения (в данном случае ⇒ ) я могу...
279 просмотров
schedule
10.10.2022
Как определить подтипы в Isabelle и что они означают?
Вопрос о подтипах в Изабель очень длинный здесь . Итак, мой простой вопрос заключается в том, как я могу определить тип B как подтип A, если я определяю A, как показано ниже:
typedecl A
Делая это, я хотел бы сделать все операции и...
301 просмотров
schedule
05.03.2022
Применить упрощение к произвольному термину
Я имею в виду термин, скажем, "foo 1 2 a b" , и я хотел бы знать, может ли Изабель упростить его для меня. Я хотел бы написать что-то вроде
simplify "foo 1 2 a b"
и напечатать упрощенный термин в выходном буфере. Это возможно?
Мой...
93 просмотров
schedule
03.05.2024
Замена лямбда-выражения в Isabelle
Учитывая функцию f:
definition f :: "real => real"
where "f x = x"
Я могу показать, что при стремлении n к 0 f(x+n) стремится к f(x) по следующей лемме
lemma "(λn. f(x+n)) -- 0 --> f x"
unfolding f_def
apply (auto intro!:...
616 просмотров
schedule
28.02.2023
Как запустить Афину | Кок | Изабель кодирует удаленно?
Я создавал Web IDE (WIDE) для доказательства теорем в области компьютерных наук. Возможно, вы знаете, что есть 3 наиболее распространенных помощника в доказательствах, которых зовут Афина, Изабель и Кок. Большинство программистов могут забыть свой...
279 просмотров
schedule
02.04.2022
Изабель: новая аксиома для неопределенных функций
Я работаю над теорией, в которой я довольно активно использую экстенсиональные функции, определенные в теории Funcset. Мне нужно работать с функциями, оценивающими функции, где и функция, и значения являются экстенсиональными. Очень досадно, что...
168 просмотров
schedule
22.07.2023
Как обеспечить различие экземпляров переменных типа
Есть ли в Isabelle способ гарантировать, что экземпляры двух переменных типа в локали или предложении будут разными?
В качестве конкретного примера я хочу рассуждать о составной сущности без привязки к конкретному представлению. Для этого я...
137 просмотров
schedule
28.06.2022
Изабель окончание с расстоянием действительных чисел
Может, кто-нибудь поможет мне с доказательством увольнения в Изабель. Я пытаюсь построить из списка A новый подсписок B. Для построения B я снова и снова читаю весь A. Вынимаю элементы и использую результат для поиска следующего элемента. Я...
96 просмотров
schedule
18.12.2022
Ошибка доказательства Изабель при вызове последовательных операций записи
Я новичок в Изабель и обязательствах по доказательству, и в настоящее время я перевожу модель VDM, которую я сделал для игры «Точки и квадраты» (базовые переводы типа VDM были предоставлены нам).
Пока у меня есть два типа записей, Dot :
record...
134 просмотров
schedule
03.05.2024
Изабель: аксиоматизация и быстрая проверка vs autosolve_direct
Снова небольшой пример с неожиданными результатами.
theory Scratch
imports Main
begin
datatype test = aa | bb | plus test test
axiomatization where
testIdemo : "x == plus x x"
lemma test1 : "y == plus y y"
Теперь я получаю следующие...
221 просмотров
schedule
09.10.2023
Использование существующего определения в Isabelle / Hol
Я новый пользователь Isabelle / Hol, и у меня есть некоторая путаница относительно использования существующих определений в Isabelle. Мне нужно определить структуру полной решетки и структуру полного частичного порядка (CPO) в моей модели. Я...
133 просмотров
schedule
28.11.2022
