src/HOL/Library/Old_SMT.thy
changeset 60500 903bb1495239
parent 59966 c01cea2ba71e
child 61585 a9599d3d7610
     1.1 --- a/src/HOL/Library/Old_SMT.thy	Wed Jun 17 10:57:11 2015 +0200
     1.2 +++ b/src/HOL/Library/Old_SMT.thy	Wed Jun 17 11:03:05 2015 +0200
     1.3 @@ -2,7 +2,7 @@
     1.4      Author:     Sascha Boehme, TU Muenchen
     1.5  *)
     1.6  
     1.7 -section {* Old Version of Bindings to Satisfiability Modulo Theories (SMT) solvers *}
     1.8 +section \<open>Old Version of Bindings to Satisfiability Modulo Theories (SMT) solvers\<close>
     1.9  
    1.10  theory Old_SMT
    1.11  imports "../Real" "../Word/Word"
    1.12 @@ -14,9 +14,9 @@
    1.13  ML_file "Old_SMT/old_smt_config.ML"
    1.14  
    1.15  
    1.16 -subsection {* Triggers for quantifier instantiation *}
    1.17 +subsection \<open>Triggers for quantifier instantiation\<close>
    1.18  
    1.19 -text {*
    1.20 +text \<open>
    1.21  Some SMT solvers support patterns as a quantifier instantiation
    1.22  heuristics.  Patterns may either be positive terms (tagged by "pat")
    1.23  triggering quantifier instantiations -- when the solver finds a
    1.24 @@ -29,7 +29,7 @@
    1.25  act disjunctively during quantifier instantiation.  Each multipattern
    1.26  should mention at least all quantified variables of the preceding
    1.27  quantifier block.
    1.28 -*}
    1.29 +\<close>
    1.30  
    1.31  typedecl pattern
    1.32  
    1.33 @@ -40,17 +40,17 @@
    1.34  definition trigger :: "pattern list list \<Rightarrow> bool \<Rightarrow> bool" where "trigger _ P = P"
    1.35  
    1.36  
    1.37 -subsection {* Quantifier weights *}
    1.38 +subsection \<open>Quantifier weights\<close>
    1.39  
    1.40 -text {*
    1.41 +text \<open>
    1.42  Weight annotations to quantifiers influence the priority of quantifier
    1.43  instantiations.  They should be handled with care for solvers, which support
    1.44  them, because incorrect choices of weights might render a problem unsolvable.
    1.45 -*}
    1.46 +\<close>
    1.47  
    1.48  definition weight :: "int \<Rightarrow> bool \<Rightarrow> bool" where "weight _ P = P"
    1.49  
    1.50 -text {*
    1.51 +text \<open>
    1.52  Weights must be non-negative.  The value @{text 0} is equivalent to providing
    1.53  no weight at all.
    1.54  
    1.55 @@ -63,32 +63,32 @@
    1.56  \item
    1.57  @{term "\<forall>x. weight 3 (P x)"}
    1.58  \end{itemize}
    1.59 -*}
    1.60 +\<close>
    1.61  
    1.62  
    1.63 -subsection {* Higher-order encoding *}
    1.64 +subsection \<open>Higher-order encoding\<close>
    1.65  
    1.66 -text {*
    1.67 +text \<open>
    1.68  Application is made explicit for constants occurring with varying
    1.69  numbers of arguments.  This is achieved by the introduction of the
    1.70  following constant.
    1.71 -*}
    1.72 +\<close>
    1.73  
    1.74  definition fun_app where "fun_app f = f"
    1.75  
    1.76 -text {*
    1.77 +text \<open>
    1.78  Some solvers support a theory of arrays which can be used to encode
    1.79  higher-order functions.  The following set of lemmas specifies the
    1.80  properties of such (extensional) arrays.
    1.81 -*}
    1.82 +\<close>
    1.83  
    1.84  lemmas array_rules = ext fun_upd_apply fun_upd_same fun_upd_other
    1.85    fun_upd_upd fun_app_def
    1.86  
    1.87  
    1.88 -subsection {* First-order logic *}
    1.89 +subsection \<open>First-order logic\<close>
    1.90  
    1.91 -text {*
    1.92 +text \<open>
    1.93  Some SMT solvers only accept problems in first-order logic, i.e.,
    1.94  where formulas and terms are syntactically separated. When
    1.95  translating higher-order into first-order problems, all
    1.96 @@ -98,13 +98,13 @@
    1.97  turned into terms by logically equating such atoms with @{term True}.
    1.98  For technical reasons, @{term True} and @{term False} occurring inside
    1.99  terms are replaced by the following constants.
   1.100 -*}
   1.101 +\<close>
   1.102  
   1.103  definition term_true where "term_true = True"
   1.104  definition term_false where "term_false = False"
   1.105  
   1.106  
   1.107 -subsection {* Integer division and modulo for Z3 *}
   1.108 +subsection \<open>Integer division and modulo for Z3\<close>
   1.109  
   1.110  definition z3div :: "int \<Rightarrow> int \<Rightarrow> int" where
   1.111    "z3div k l = (if 0 \<le> l then k div l else -(k div (-l)))"
   1.112 @@ -113,7 +113,7 @@
   1.113    "z3mod k l = (if 0 \<le> l then k mod l else k mod (-l))"
   1.114  
   1.115  
   1.116 -subsection {* Setup *}
   1.117 +subsection \<open>Setup\<close>
   1.118  
   1.119  ML_file "Old_SMT/old_smt_builtin.ML"
   1.120  ML_file "Old_SMT/old_smt_datatypes.ML"
   1.121 @@ -131,33 +131,33 @@
   1.122  ML_file "Old_SMT/old_z3_model.ML"
   1.123  ML_file "Old_SMT/old_smt_setup_solvers.ML"
   1.124  
   1.125 -setup {*
   1.126 +setup \<open>
   1.127    Old_SMT_Config.setup #>
   1.128    Old_SMT_Normalize.setup #>
   1.129    Old_SMTLIB_Interface.setup #>
   1.130    Old_Z3_Interface.setup #>
   1.131    Old_SMT_Setup_Solvers.setup
   1.132 -*}
   1.133 +\<close>
   1.134  
   1.135 -method_setup old_smt = {*
   1.136 +method_setup old_smt = \<open>
   1.137    Scan.optional Attrib.thms [] >>
   1.138      (fn thms => fn ctxt =>
   1.139        METHOD (fn facts => HEADGOAL (Old_SMT_Solver.smt_tac ctxt (thms @ facts))))
   1.140 -*} "apply an SMT solver to the current goal"
   1.141 +\<close> "apply an SMT solver to the current goal"
   1.142  
   1.143  
   1.144 -subsection {* Configuration *}
   1.145 +subsection \<open>Configuration\<close>
   1.146  
   1.147 -text {*
   1.148 +text \<open>
   1.149  The current configuration can be printed by the command
   1.150  @{text old_smt_status}, which shows the values of most options.
   1.151 -*}
   1.152 +\<close>
   1.153  
   1.154  
   1.155  
   1.156 -subsection {* General configuration options *}
   1.157 +subsection \<open>General configuration options\<close>
   1.158  
   1.159 -text {*
   1.160 +text \<open>
   1.161  The option @{text old_smt_solver} can be used to change the target SMT
   1.162  solver.  The possible values can be obtained from the @{text old_smt_status}
   1.163  command.
   1.164 @@ -166,82 +166,82 @@
   1.165  by default.  Z3 is free for non-commercial applications and can be enabled
   1.166  by setting the @{text OLD_Z3_NON_COMMERCIAL} environment variable to
   1.167  @{text yes}.
   1.168 -*}
   1.169 +\<close>
   1.170  
   1.171  declare [[ old_smt_solver = z3 ]]
   1.172  
   1.173 -text {*
   1.174 +text \<open>
   1.175  Since SMT solvers are potentially non-terminating, there is a timeout
   1.176  (given in seconds) to restrict their runtime.  A value greater than
   1.177  120 (seconds) is in most cases not advisable.
   1.178 -*}
   1.179 +\<close>
   1.180  
   1.181  declare [[ old_smt_timeout = 20 ]]
   1.182  
   1.183 -text {*
   1.184 +text \<open>
   1.185  SMT solvers apply randomized heuristics.  In case a problem is not
   1.186  solvable by an SMT solver, changing the following option might help.
   1.187 -*}
   1.188 +\<close>
   1.189  
   1.190  declare [[ old_smt_random_seed = 1 ]]
   1.191  
   1.192 -text {*
   1.193 +text \<open>
   1.194  In general, the binding to SMT solvers runs as an oracle, i.e, the SMT
   1.195  solvers are fully trusted without additional checks.  The following
   1.196  option can cause the SMT solver to run in proof-producing mode, giving
   1.197  a checkable certificate.  This is currently only implemented for Z3.
   1.198 -*}
   1.199 +\<close>
   1.200  
   1.201  declare [[ old_smt_oracle = false ]]
   1.202  
   1.203 -text {*
   1.204 +text \<open>
   1.205  Each SMT solver provides several commandline options to tweak its
   1.206  behaviour.  They can be passed to the solver by setting the following
   1.207  options.
   1.208 -*}
   1.209 +\<close>
   1.210  
   1.211  declare [[ old_cvc3_options = "" ]]
   1.212  declare [[ old_yices_options = "" ]]
   1.213  declare [[ old_z3_options = "" ]]
   1.214  
   1.215 -text {*
   1.216 +text \<open>
   1.217  Enable the following option to use built-in support for datatypes and
   1.218  records.  Currently, this is only implemented for Z3 running in oracle
   1.219  mode.
   1.220 -*}
   1.221 +\<close>
   1.222  
   1.223  declare [[ old_smt_datatypes = false ]]
   1.224  
   1.225 -text {*
   1.226 +text \<open>
   1.227  The SMT method provides an inference mechanism to detect simple triggers
   1.228  in quantified formulas, which might increase the number of problems
   1.229  solvable by SMT solvers (note: triggers guide quantifier instantiations
   1.230  in the SMT solver).  To turn it on, set the following option.
   1.231 -*}
   1.232 +\<close>
   1.233  
   1.234  declare [[ old_smt_infer_triggers = false ]]
   1.235  
   1.236 -text {*
   1.237 +text \<open>
   1.238  The SMT method monomorphizes the given facts, that is, it tries to
   1.239  instantiate all schematic type variables with fixed types occurring
   1.240  in the problem.  This is a (possibly nonterminating) fixed-point
   1.241  construction whose cycles are limited by the following option.
   1.242 -*}
   1.243 +\<close>
   1.244  
   1.245  declare [[ monomorph_max_rounds = 5 ]]
   1.246  
   1.247 -text {*
   1.248 +text \<open>
   1.249  In addition, the number of generated monomorphic instances is limited
   1.250  by the following option.
   1.251 -*}
   1.252 +\<close>
   1.253  
   1.254  declare [[ monomorph_max_new_instances = 500 ]]
   1.255  
   1.256  
   1.257  
   1.258 -subsection {* Certificates *}
   1.259 +subsection \<open>Certificates\<close>
   1.260  
   1.261 -text {*
   1.262 +text \<open>
   1.263  By setting the option @{text old_smt_certificates} to the name of a file,
   1.264  all following applications of an SMT solver a cached in that file.
   1.265  Any further application of the same SMT solver (using the very same
   1.266 @@ -253,11 +253,11 @@
   1.267  @{text ".certs"} instead of @{text ".thy"}) as the certificates file.
   1.268  Certificate files should be used at most once in a certain theory context,
   1.269  to avoid race conditions with other concurrent accesses.
   1.270 -*}
   1.271 +\<close>
   1.272  
   1.273  declare [[ old_smt_certificates = "" ]]
   1.274  
   1.275 -text {*
   1.276 +text \<open>
   1.277  The option @{text old_smt_read_only_certificates} controls whether only
   1.278  stored certificates are should be used or invocation of an SMT solver
   1.279  is allowed.  When set to @{text true}, no SMT solver will ever be
   1.280 @@ -265,50 +265,50 @@
   1.281  cache are used;  when set to @{text false} and there is no cached
   1.282  certificate for some proposition, then the configured SMT solver is
   1.283  invoked.
   1.284 -*}
   1.285 +\<close>
   1.286  
   1.287  declare [[ old_smt_read_only_certificates = false ]]
   1.288  
   1.289  
   1.290  
   1.291 -subsection {* Tracing *}
   1.292 +subsection \<open>Tracing\<close>
   1.293  
   1.294 -text {*
   1.295 +text \<open>
   1.296  The SMT method, when applied, traces important information.  To
   1.297  make it entirely silent, set the following option to @{text false}.
   1.298 -*}
   1.299 +\<close>
   1.300  
   1.301  declare [[ old_smt_verbose = true ]]
   1.302  
   1.303 -text {*
   1.304 +text \<open>
   1.305  For tracing the generated problem file given to the SMT solver as
   1.306  well as the returned result of the solver, the option
   1.307  @{text old_smt_trace} should be set to @{text true}.
   1.308 -*}
   1.309 +\<close>
   1.310  
   1.311  declare [[ old_smt_trace = false ]]
   1.312  
   1.313 -text {*
   1.314 +text \<open>
   1.315  From the set of assumptions given to the SMT solver, those assumptions
   1.316  used in the proof are traced when the following option is set to
   1.317  @{term true}.  This only works for Z3 when it runs in non-oracle mode
   1.318  (see options @{text old_smt_solver} and @{text old_smt_oracle} above).
   1.319 -*}
   1.320 +\<close>
   1.321  
   1.322  declare [[ old_smt_trace_used_facts = false ]]
   1.323  
   1.324  
   1.325  
   1.326 -subsection {* Schematic rules for Z3 proof reconstruction *}
   1.327 +subsection \<open>Schematic rules for Z3 proof reconstruction\<close>
   1.328  
   1.329 -text {*
   1.330 +text \<open>
   1.331  Several prof rules of Z3 are not very well documented.  There are two
   1.332  lemma groups which can turn failing Z3 proof reconstruction attempts
   1.333  into succeeding ones: the facts in @{text z3_rule} are tried prior to
   1.334  any implemented reconstruction procedure for all uncertain Z3 proof
   1.335  rules;  the facts in @{text z3_simp} are only fed to invocations of
   1.336  the simplifier when reconstructing theory-specific proof steps.
   1.337 -*}
   1.338 +\<close>
   1.339  
   1.340  lemmas [old_z3_rule] =
   1.341    refl eq_commute conj_commute disj_commute simp_thms nnf_simps