--- a/src/HOL/SMT/SMT_Definitions.thy Tue Oct 20 08:10:47 2009 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,113 +0,0 @@
-(* Title: HOL/SMT/SMT_Definitions.thy
- Author: Sascha Boehme, TU Muenchen
-*)
-
-header {* SMT-specific definitions *}
-
-theory SMT_Definitions
-imports Real Word "~~/src/HOL/Decision_Procs/Dense_Linear_Order"
-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 :: "bool \<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)"
-
-text {* A decision procedure for linear real arithmetic: *}
-
-setup {*
- Arith_Data.add_tactic "Ferrante-Rackoff" (K FerranteRackoff.dlo_tac)
-*}
-
-
-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"
-
-
-section {* First-order logic *}
-
-text {*
-Some SMT solver formats require a strict separation between formulas and terms.
-The following marker symbols are used internally to separate those categories:
-*}
-
-definition formula :: "bool \<Rightarrow> bool" where "formula x = x"
-definition "term" where "term x = x"
-
-text {*
-Predicate symbols also occurring as function symbols are turned into function
-symbols by translating atomic formulas into terms:
-*}
-
-abbreviation holds :: "bool \<Rightarrow> bool" where "holds \<equiv> (\<lambda>P. term P = term True)"
-
-text {*
-The following constant represents equivalence, to be treated differently than
-the (polymorphic) equality predicate:
-*}
-
-definition iff :: "bool \<Rightarrow> bool \<Rightarrow> bool" (infix "iff" 50) where
- "(x iff y) = (x = y)"
-
-end
-