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