Again a small example with unexpected results.
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"
Now i get the following messages:
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
and when i try to run sledgehammer i get:
"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.
Is this due to me messing with ==? Or do i need to set some other sort of restriction for my axioms?
Follow up:
Apparently i should not play with equals :P So i need to define my own relation.
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"
So i guess i have to define my basic properties. reflexiveness, substitution and symmetry seem nice for a start. I could make it generic with 'a => 'a => bool
now i would go on to define more of my relation. to stay with the example:
axiomatization
plus :: "test⇒ test⇒ test" (infixl "+" 35)
where
commutative: "x + y = y + x" and
idemo: "x + x = x"
a) Is this so far correct b) How to proceed from here So far i don't think this would replace subterms out of lemmas which is kinda the point of equivalence.
Your axiom implies e.g. aa = plus aa aa, which is false, because constructors of a datatype are always distinct, by construction. (cf. thm test.distinct)
In fact, if you use axiomatization, you should really know what you're doing – it's very easy to introduce inconsistencies that way. (obviously)
If you want to have a type with certain properties, you have to construct it. For instance, you could define a representation type of your type (e.g. as a datatype), then define some equality relation on it (i.e. what values should be equal to what other values) and then define the ‘real’ type as the quotient type of your representation type over that relation.