src/HOL/SMT.thy
 changeset 41059 d2b1fc1b8e19 parent 40806 59d96f777da3 child 41121 5c5d05963f93
```     1.1 --- a/src/HOL/SMT.thy	Mon Dec 06 16:54:22 2010 +0100
1.2 +++ b/src/HOL/SMT.thy	Tue Dec 07 14:53:12 2010 +0100
1.3 @@ -105,16 +105,18 @@
1.4  subsection {* First-order logic *}
1.5
1.6  text {*
1.7 -Some SMT solvers require a strict separation between formulas and
1.8 -terms.  When translating higher-order into first-order problems,
1.9 -all uninterpreted constants (those not builtin in the target solver)
1.10 +Some SMT solvers only accept problems in first-order logic, i.e.,
1.11 +where formulas and terms are syntactically separated. When
1.12 +translating higher-order into first-order problems, all
1.13 +uninterpreted constants (those not built-in in the target solver)
1.14  are treated as function symbols in the first-order sense.  Their
1.15 -occurrences as head symbols in atoms (i.e., as predicate symbols) is
1.16 -turned into terms by equating such atoms with @{term True} using the
1.17 -following term-level equation symbol.
1.18 +occurrences as head symbols in atoms (i.e., as predicate symbols) are
1.19 +turned into terms by equating such atoms with @{term True}.
1.20 +Whenever the boolean type occurs in first-order terms, it is replaced
1.21 +by the following type.
1.22  *}
1.23
1.24 -definition term_eq :: "bool \<Rightarrow> bool \<Rightarrow> bool" where "term_eq x y = (x = y)"
1.25 +typedecl term_bool
1.26
1.27
1.28
1.29 @@ -159,7 +161,10 @@
1.30
1.31  setup {*
1.32    SMT_Config.setup #>
1.33 +  SMT_Normalize.setup #>
1.34    SMT_Solver.setup #>
1.35 +  SMTLIB_Interface.setup #>
1.36 +  Z3_Interface.setup #>
1.37    Z3_Proof_Reconstruction.setup #>
1.38    SMT_Setup_Solvers.setup
1.39  *}
1.40 @@ -354,9 +359,10 @@
1.41
1.42
1.43
1.44 +hide_type term_bool
1.45  hide_type (open) pattern
1.46 -hide_const Pattern term_eq
1.47 -hide_const (open) trigger pat nopat weight fun_app z3div z3mod
1.48 +hide_const Pattern fun_app
1.49 +hide_const (open) trigger pat nopat weight z3div z3mod
1.50
1.51
1.52
```