src/HOL/SMT/SMT_Base.thy

 
 header {* SMT-specific definitions and basic tools *}
 
 theory SMT_Base
 imports Real "~~/src/HOL/Word/Word"
-  "~~/src/HOL/Decision_Procs/Dense_Linear_Order"
 uses
   "~~/src/Tools/cache_io.ML"
   ("Tools/smt_normalize.ML")
   ("Tools/smt_monomorph.ML")
   ("Tools/smt_translate.ML")

 
 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

 
 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)"
 
-text {* A decision procedure for linear real arithmetic: *}
-
-setup {*
-  Arith_Data.add_tactic "Ferrante-Rackoff" (K FerranteRackoff.dlo_tac)
-*}
 
 
 section {* Bitvectors *}
 
 text {*

 
 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)"

   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 {*

 
 definition iff :: "bool \<Rightarrow> bool \<Rightarrow> bool" (infix "iff" 50) where
   "(x iff y) = (x = y)"
 
 
+
 section {* Setup *}
 
 use "Tools/smt_normalize.ML"
 use "Tools/smt_monomorph.ML"
 use "Tools/smt_translate.ML"