Снова небольшой пример с неожиданными результатами.
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"
Теперь я получаю следующие сообщения:
Auto solve_direct: The current goal can be solved directly with
Scratch.testIdemo: ?x ≡ test.plus ?x ?x
Auto Quickcheck found a counterexample:
y = aa
Evaluated terms:
test.plus y y = test.plus aa aa
и когда я пытаюсь запустить кувалду, я получаю:
"remote_vampire": Try this: using testIdemo by auto (0.0 ms).
"spass": The prover derived "False" from "test.distinct(5)" and "testIdemo".
This could be due to inconsistent axioms (including "sorry"s) or to a bug in Sledgehammer.
If the problem persists, please contact the Isabelle developers.
Это из-за того, что я возился с ==? Или мне нужно установить какое-то другое ограничение для моих аксиом?
Следовать за:
Очевидно, я не должен играть с равными: P Так что мне нужно определить свое собственное отношение.
axiomatization
testEQ :: "test ⇒ test ⇒ bool" (infixl "=" 1)
where
reflexive [intro]: "x = x" and
substitution [elim]: "x = y ⟹ B x = B y" and
symmetric : "x = y ⟹ y = x"
Итак, я думаю, мне нужно определить мои основные свойства. рефлексивность, подстановка и симметрия кажутся хорошими для начала. Я мог бы сделать его общим с помощью 'a => 'a => bool
теперь я бы пошел дальше, чтобы определить больше моего отношения. чтобы остаться с примером:
axiomatization
plus :: "test⇒ test⇒ test" (infixl "+" 35)
where
commutative: "x + y = y + x" and
idemo: "x + x = x"
а) Это пока правильно б) Как действовать дальше Пока я не думаю, что это заменит подтермины из лемм, что является своего рода точкой эквивалентности.
