use proper context operations (for fresh names of type and term variables, and for hypothetical definitions), monomorphize theorems (instead of terms, necessary for hypothetical definitions made during lambda lifting)
(* Title: HOL/SMT/SMT_Base.thy
Author: Sascha Boehme, TU Muenchen
*)
header {* SMT-specific definitions and basic tools *}
theory SMT_Base
imports Real "~~/src/HOL/Word/Word"
uses
"~~/src/Tools/cache_io.ML"
("Tools/smt_additional_facts.ML")
("Tools/smt_monomorph.ML")
("Tools/smt_normalize.ML")
("Tools/smt_translate.ML")
("Tools/smt_solver.ML")
("Tools/smtlib_interface.ML")
begin
section {* Triggers for quantifier instantiation *}
text {*
Some SMT solvers support triggers for quantifier instantiation. Each trigger
consists of one ore more patterns. A pattern may either be a list of positive
subterms (the first being tagged by "pat" and the consecutive subterms tagged
by "andpat"), or a list of negative subterms (the first being tagged by "nopat"
and the consecutive subterms tagged by "andpat").
*}
datatype pattern = Pattern
definition pat :: "'a \<Rightarrow> pattern"
where "pat _ = Pattern"
definition nopat :: "'a \<Rightarrow> pattern"
where "nopat _ = Pattern"
definition andpat :: "pattern \<Rightarrow> 'a \<Rightarrow> pattern" (infixl "andpat" 60)
where "_ andpat _ = Pattern"
definition trigger :: "pattern list \<Rightarrow> bool \<Rightarrow> bool"
where "trigger _ P = P"
section {* Arithmetic *}
text {*
The sign of @{term "op mod :: int \<Rightarrow> int \<Rightarrow> int"} follows the sign of the
divisor. In contrast to that, the sign of the following operation is that of
the dividend.
*}
definition rem :: "int \<Rightarrow> int \<Rightarrow> int" (infixl "rem" 70)
where "a rem b =
(if (a \<ge> 0 \<and> b < 0) \<or> (a < 0 \<and> b \<ge> 0) then - (a mod b) else a mod b)"
section {* Bitvectors *}
text {*
The following definitions provide additional functions not found in HOL-Word.
*}
definition sdiv :: "'a::len word \<Rightarrow> 'a word \<Rightarrow> 'a word" (infix "sdiv" 70)
where "w1 sdiv w2 = word_of_int (sint w1 div sint w2)"
definition smod :: "'a::len word \<Rightarrow> 'a word \<Rightarrow> 'a word" (infix "smod" 70)
(* sign follows divisor *)
where "w1 smod w2 = word_of_int (sint w1 mod sint w2)"
definition srem :: "'a::len word \<Rightarrow> 'a word \<Rightarrow> 'a word" (infix "srem" 70)
(* sign follows dividend *)
where "w1 srem w2 = word_of_int (sint w1 rem sint w2)"
definition bv_shl :: "'a::len0 word \<Rightarrow> 'a word \<Rightarrow> 'a word"
where "bv_shl w1 w2 = (w1 << unat w2)"
definition bv_lshr :: "'a::len0 word \<Rightarrow> 'a word \<Rightarrow> 'a word"
where "bv_lshr w1 w2 = (w1 >> unat w2)"
definition bv_ashr :: "'a::len word \<Rightarrow> 'a word \<Rightarrow> 'a word"
where "bv_ashr w1 w2 = (w1 >>> unat w2)"
section {* Higher-Order Encoding *}
definition "apply" where "apply f x = f x"
definition array_ext where "array_ext a b = (SOME x. a = b \<or> a x \<noteq> b x)"
lemma fun_upd_eq: "(f = f (x := y)) = (f x = y)"
proof
assume "f = f(x:=y)"
hence "f x = (f(x:=y)) x" by simp
thus "f x = y" by simp
qed (auto simp add: ext)
lemmas array_rules =
ext fun_upd_apply fun_upd_same fun_upd_other fun_upd_upd fun_upd_eq apply_def
section {* First-order logic *}
text {*
Some SMT solver formats require a strict separation between formulas and terms.
During normalization, all uninterpreted constants are treated as function
symbols, and atoms (with uninterpreted head symbol) are turned into terms by
equating them with true using the following term-level equation symbol:
*}
definition term_eq :: "bool \<Rightarrow> bool \<Rightarrow> bool" (infix "term'_eq" 50)
where "(x term_eq y) = (x = y)"
section {* Setup *}
use "Tools/smt_additional_facts.ML"
use "Tools/smt_monomorph.ML"
use "Tools/smt_normalize.ML"
use "Tools/smt_translate.ML"
use "Tools/smt_solver.ML"
use "Tools/smtlib_interface.ML"
setup {* SMT_Solver.setup *}
end