Описание тега isar
Разумное полуавтоматическое обоснование (Isar) - это подход к формальным доказательствам, читаемым человеком (в отличие от сценариев на основе состояний).
3
ответа
Как использовать получение в экзистенциальных доказательствах?
Я пытался доказать экзистенциальную теорему lemma "∃ x. x * (t :: nat) = t" proof obtain y where "y * t = t" by (auto) но я не смог закончить доказательство. Так что у меня есть необходимые y но как я могу кормить это в первоначальной цели?
01 июл '14 в 14:21
1
ответ
Почему не работает правило 'linordered_field_class.frac_le'? (Изабель)
Я пытаюсь использовать правило linordered_field_class.frac_le в доказательстве Изара. Вот фрагмент кода (он может зависеть от предыдущих частей доказательства, но это маловероятно). n имеет тип нац. ... then have 4:"2 ≤ (2^(n+1)::real)" by simp have…
27 дек '16 в 15:15
2
ответа
Полностью заменить внутренний синтаксис в isar?
Я заинтересован в использовании Isar в качестве мета-языка для написания формальных доказательств о J, исполняемой математической нотации и языке программирования, и я хотел бы иметь возможность использовать J в качестве внутреннего синтаксиса. J со…
05 янв '15 в 09:01
0
ответов
Соглашения о стиле кодирования в Изабель / Изаре
TL; DR: Существуют ли соглашения по кодированию для языка Изара? Нужно ли соблюдать стратегию сворачивания jEdit? Моя команда работает над формализацией математики, поэтому одной из наших основных целей является получение удобочитаемых доказательств…
16 фев '19 в 14:03
2
ответа
Таможенные различия в доказательствах
Поддерживает ли Изабель пользовательские различия в регистрах утверждений? Допустим, я хочу доказать утверждение для всех натуральных чисел n, но доказательство совершенно другое в зависимости от того, n четный или нечетный. Можно ли провести такое …
26 янв '18 в 12:02
2
ответа
Укрощение мета-смысла в доказательствах Изара
Доказывая простую теорему, я наткнулся на последствия мета-уровня в доказательстве. Можно ли их иметь или их можно избежать? Если я должен справиться с ними, это правильный способ сделать это? theory Sandbox imports Main begin lemma "(x::nat) > 0…
13 авг '14 в 12:10
2
ответа
Что такое хороший способ определить конечную таблицу умножения в Isar?
Предположим, у меня есть бинарный оператор f :: "sT => sT => sT", Я хочу определить f так что он реализует таблицу умножения 4x4 для группы Кляйна четыре, показанную здесь, на вики: http://en.wikipedia.org/wiki/Klein_four-group Здесь все, что …
29 апр '13 в 04:09
1
ответ
Пропустить подцель во время испытания в Изабель
Я пытаюсь доказать теорему, но застрял на подзадаче (которую я предпочитаю пропустить и доказать позже). Как я могу пропустить это и доказать другие? Сначала я попробовал oops а также sorry но они оба прерывают все доказательство (вместо единственно…
03 фев '15 в 09:43
1
ответ
Могу ли я "сопоставить" "OF" со списком лемм
Я только что написал этот код: lemmas gc_step_intros = normal[OF step.intros(1)] normal[OF step.intros(2)] normal[OF step.intros(3)] normal[OF step.intros(4)] normal[OF step.intros(5)] drop где step.intros на самом деле только 5 лемм. Есть ли удобны…
29 окт '14 в 12:57
1
ответ
Нетипизированные операции над множествами в Изабель
У меня есть следующий код в Изабель: typedecl type1 typedecl type2 consts A::"type1 set" B::"type2 set" Когда я хочу использовать операцию объединения с A и B, как показано ниже: axiomatization where c0: "A ∩ B = {}" Так как A и B - это наборы разны…
11 ноя '14 в 11:10
1
ответ
Как упростить доказательство свойства функции для типа данных?
Я создал небольшое доказательство с намерением создать пример для использования next по доказательствам: theory RedGreen imports Main begin datatype color = RED | GREEN fun green :: "color => color" where "green RED = GREEN" | "green GREEN = GREE…
30 июн '14 в 15:06
1
ответ
Изменение порядка целей (Изабель)
Я хотел бы знать, как изменить порядок целей в следующей ситуации: lemma "P=Q" proof (rule iffI, (*here I would like to swap goal order*), rule ccontr) oops Я хотел бы решение, которое не включает в себя изменение утверждения леммы. Я понимаю что pr…
19 сен '17 в 16:41
1
ответ
Изабель / Изара: Реализация эквалайзера
Я все еще пытаюсь разобраться в отношениях равенства и определить, как их определить в Изабель. К счастью, в справочном руководстве isar 2.3.1 p38f есть глава об этом. Я попытался восстановить приведенный пример. Чтобы избежать совпадений с установл…
12 янв '16 в 15:27
1
ответ
Как определить подтипы в Изабель и что они значат?
Вопрос о подтипах у Изабель очень длинный. Поэтому мой простой вопрос заключается в том, как определить тип B как подтип A, если я определю A, как показано ниже: typedecl A Делая это, я хотел бы сделать все операции и отношения, определенные над A (…
11 ноя '14 в 13:16
1
ответ
Как я обращаюсь к текущей подцели в Изаре?
Я пытаюсь решить упражнение 4.7 из Программирование и доказательство в Изабель. Я сталкиваюсь с делом, где я доказал Ложь и, следовательно, все, но я не могу закрыть дело, потому что я не знаю, как ссылаться на мое обязательство по доказыванию. theo…
03 мар '17 в 15:49
2
ответа
Распечатка / показ подробных шагов методов доказательства (например, простого) в доказательстве в Изабель
Предположим, у меня есть следующий код в Изабель: lemma"[| xs@zs = ys@xs ;[]@xs = []@[] |] => ys=zs" (*never mind the lemma body*) apply simp done В приведенном выше коде метод simp доказывает лемму. Мне интересно увидеть и распечатать подробные …
09 ноя '14 в 06:42
1
ответ
Использование "Иметь... наконец-то есть" в Изабель
Я обычно думаю о also have как работает так: have "P r Q1" by simp also have "... r Q2" by simp also have "... r Q3" by simp ... also have "... r Qn" by simp finally have "P r Qn+1" by simp где "... r Qm" средства "Qm-1 r Qm" а также r это некоторое…
28 дек '16 в 09:41
1
ответ
Определение коэффициента в Изабель
Я все еще пытаюсь рассуждать о семантическом равенстве в Изабель. Я хочу сравнить две формулы и посмотреть, равны ли они. Мне уже говорили, что мне нужны коэффициенты для этого. Поэтому я попытался определить собственный тип-выражения, но, с другой …
19 янв '16 в 16:15
2
ответа
Доступ к элементам типов данных
Возможно ли в Изабель доступ к отдельным элементам типа данных? Допустим, у меня есть следующий тип данных: datatype foo = mat int int int int и (например, в лемме) fixes A :: foo Можно ли получить доступ к отдельным элементам A? Или, в качестве аль…
22 янв '18 в 17:13
1
ответ
Создайте тип с коэффициентом поднятия с полиморфизмом над рабочим множеством и отношением эквивалентности в Изабель /HOL
Я хотел бы создать частный тип с quotient_type в Изабель /HOL, в котором я бы оставил "не сконструированный" непустое множество S и отношение эквивалентности ≡, Цель состоит в том, чтобы я получил общие свойства по отношению к S а также ≡ над множес…
26 фев '15 в 16:08