I need to use some equational reasoning but I am not interested in redefining all the underlying theory. My goal is to use existing SMT solvers as done by sledgehammer. For instance, assume this theory of equality with some simple arithmetics,
datatype expr = Var string
| Const nat
datatype constraint = Eq "expr * expr" (* E1 = E2 *)
fun SAT :: "constraint list ⇒ bool" where
"SAT L = undefined (* calling an SMT-solver here *)"
The type constraint list contains constraints that embed logical constraints that I wish to send to an SMT solver to return true (if possible). And hence assert that the following should return false
value "SAT [Eq(Var ''X1'', Var ''X2''), (* X1 = X2*)
Eq(Var ''X1'', Const 0), (* X1 = 0 *)
Eq(Var ''X2'', Const (Suc 0))]" (* X2 = 1 *)
How shall I proceed to do so?