Описание тега isabelle

Описание тега Вопросы с тегом
Isabelle is a generic proof assistant, with Isabelle/HOL as main instance.
2 ответа

Доказательство мощности конечного множества

Как я могу доказать в Изабель простое lemma cd : "card {m∈ℕ. m <4} = 4" заявление? auto не помогает мне и как ни странно sledgehammer время ожидания (даже если я использую разные значения в правой части, например 3 или же 5 чтобы убедиться, что я…
19 фев '17 в 11:22
1 ответ

Матричная арифметика Изабель: det_linear_row_setsum в библиотеке с другой системой обозначений

Недавно я начал использовать доказатель теоремы Изабель. Поскольку я хочу доказать другую лемму, я хотел бы использовать нотацию, отличную от той, которая используется в лемме "det_linear_row_setsum", которую можно найти в библиотеке HOL. Более конк…
25 июн '13 в 14:08
3 ответа

Как использовать получение в экзистенциальных доказательствах?

Я пытался доказать экзистенциальную теорему lemma "∃ x. x * (t :: nat) = t" proof obtain y where "y * t = t" by (auto) но я не смог закончить доказательство. Так что у меня есть необходимые y но как я могу кормить это в первоначальной цели?
01 июл '14 в 14:21
1 ответ

Ошибка при попытке оценить "взаимно"

Я хочу использовать coprime функция, которая определена в Изабель GCD и немного поиграй с этим. Почему value "coprime Suc(Suc 0) Suc(Suc(Suc (Suc 0)))" вернуть ошибку Type unification failed: No type arity fun :: gcd Type error in application: incom…
17 фев '17 в 19:19
1 ответ

Умный образец конструктора во время прувинга с Изабель

Во время изучения главы 3 " Конкретная семантика" мой инструктор упомянул, что некоторые функции были построены с использованием шаблона "умный конструктор", и заявил, что этот шаблон полезен для доказательства теорем. Я гуглил умных конструкторов, …
23 окт '18 в 15:32
1 ответ

Как доказать, что "(∀x. P) ∧ Q ⟹ ∀x. P", используя конъюнкт1 в Изабель?

Я пытаюсь доказать это: lemma assumes 0: "(∀x. P) ∧ Q" shows "∀x. P" proof - show ?thesis using 0 by (rule conjunct1) qed Я собираюсь: Failed to apply initial proof method⌂: using this: (∀x. P) ∧ Q goal (1 subgoal): 1. ∀x. P Что я должен изменить в …
12 дек '14 в 12:56
1 ответ

Извлечение программы с использованием собственных целых чисел / слов (не bignums) из теории Изабель

Этот вопрос возникает в контексте, где Изабель используется для формальной разработки программного обеспечения, а не для чисто математической теории (и из контекста отдельного разработчика). В лучшем случае программы SML, созданные на основе теории …
20 апр '14 в 02:02
1 ответ

Перевод VDM в Изабель

Я пытаюсь перевести модель VDM на Изабель, но почему-то, что я делаю, не работает Следующий пример - функция VDM моей модели Dot_Move_invariant: Dot * Dot -> bool Dot_Move_invariant(d1, d2) == d1 < d2 and let coordinate_1 = Dot_Coord(d1) in le…
12 дек '17 в 20:55
1 ответ

Нормальное определение константы в сравнении с определением лямбда-константы

У меня есть эти два определения. Почему они разворачиваются по-разному? Как я могу доказать леммы о "ой"? (И вообще, в чем разница между этими двумя определениями в Изабель, внутри?) (Пожалуйста, не направляйте меня на внешние ссылки, потому что я о…
24 окт '15 в 17:49
1 ответ

Изабель: проблема с setprod

Имеет ли место следующее равенство в Изабель: setprod f (UNIV :: 'n∷finite set) = setprod (λx. x) (f ` (UNIV :: 'n∷finite set)) Если да, как я могу это доказать? (* tested with Isabelle2013-2 *) theory Notepad imports Main "~~/src/HOL/Library/Polyno…
17 янв '14 в 05:03
0 ответов

Найти леммы, используемые просто / авто / уточнять

Как я могу найти, какие леммы используются простыми, автоматическими методами и т. Д.? В одном конкретном случае у меня есть такая цель: lemma "x ∉ dom S ⟹ Something" apply auto и после применения auto Я получил: ¬ Something ⟹ ∃y. S x = Some y, Я хо…
01 мар '17 в 13:16
1 ответ

Определение конечных множеств в Изабель

Как я могу определить наборы констант в Изабель? Например, что-то вроде {1,2,3} (чтобы придать ему более интересный поворот с 1,2,3 реалами), или {x \in N: x Я думаю, что во всех случаях это должно быть что-то вроде definition a_set :: set where "a_…
18 фев '17 в 14:51
3 ответа

Какое правило использует "применить (правило)" или "доказательство"?

Когда я использую apply (rule) в сценарии применения обычно выбирается соответствующее правило. То же самое относится и к proof в структурированных доказательствах. Где я могу узнать / найти название правила, которое использовалось?
21 мар '13 в 10:36
1 ответ

Знание, когда доказательство в стиле Изара действительно в Изабель

Я работаю над упражнением, пытаясь выучить язык изар. У меня есть следующий скрипт для леммы о списках. lemma "EX ys zs. xs = ys @ zs ∧ (length ys = length zs ∨ length ys = length zs + 1)" proof - show ?thesis by blast (* L *) qed Кажется, Изабель п…
11 янв '19 в 22:56
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
1 ответ

Ошибка сортировки по массе... не равна

Вот тривиальный переводчик с языка foo в bar: type_synonym vname = "string" type_synonym 'a env = "vname ⇒ 'a option" datatype foo_exp = FooBConst bool datatype foo_type = FooBType | FooIType | FooSType datatype bar_exp = BarBConst bool datatype bar…
21 июл '17 в 08:22
1 ответ

Индексы де Брюин в Изабель и Кок

Я хотел бы иметь возможность использовать что-то вроде индексов де Брюйна в Изабель или в Coq, чтобы ссылаться на переменные, которые были введены квантификаторами. Например, вместо того, чтобы писать: forall x. forall y. (p x y) Я хотел бы написать…
04 мар '15 в 23:02
1 ответ

Простая лемма в Изабель

Я пытался научиться использовать Изабель и столкнулся с проблемой. Следующая лемма работает: lemma sum_square: "(a+b)^2=a^2+(2::real)*a*b+b^2" apply (simp add: power2_eq_square) output: (a + b) * (a + b) = a * a + 2 * a * b + b * b однако следующая …
14 дек '14 в 20:38
1 ответ

Создание типа данных с неравенствами в Изабель

Я очень плохо знаком с Изабель и пытаюсь реализовать такой тип данных, как тип данных фрукты = яблоко | Бананы | Мускусная дыня (выбор слов здесь неуместен, чтобы не путать его с попыткой сделать что-то еще) Тем не менее, важно отметить, что Apple ≤…
24 апр '16 в 04:08
0 ответов

Ограничить домен отношения в Изабель

У меня есть отношение, которое не является обоснованным, называем это r1. Он определяется (неявно) как функция: r1: a' => a' => bool Тем не менее, я отмечаю, что если я ограничу тип: r2: b' => b' => bool где b'определяется как тип a' с д…
24 ноя '18 в 19:14