src/HOL/SMT.thy
changeset 60758 d8d85a8172b5
parent 60201 90e88e521e0e
child 61611 a9c0572109af
     1.1 --- a/src/HOL/SMT.thy	Sat Jul 18 21:44:18 2015 +0200
     1.2 +++ b/src/HOL/SMT.thy	Sat Jul 18 22:58:50 2015 +0200
     1.3 @@ -2,14 +2,14 @@
     1.4      Author:     Sascha Boehme, TU Muenchen
     1.5  *)
     1.6  
     1.7 -section {* Bindings to Satisfiability Modulo Theories (SMT) solvers based on SMT-LIB 2 *}
     1.8 +section \<open>Bindings to Satisfiability Modulo Theories (SMT) solvers based on SMT-LIB 2\<close>
     1.9  
    1.10  theory SMT
    1.11  imports Divides
    1.12  keywords "smt_status" :: diag
    1.13  begin
    1.14  
    1.15 -subsection {* A skolemization tactic and proof method *}
    1.16 +subsection \<open>A skolemization tactic and proof method\<close>
    1.17  
    1.18  lemma choices:
    1.19    "\<And>Q. \<forall>x. \<exists>y ya. Q x y ya \<Longrightarrow> \<exists>f fa. \<forall>x. Q x (f x) (fa x)"
    1.20 @@ -39,25 +39,25 @@
    1.21      \<exists>f fa fb fc fd fe ff fg. \<forall>x \<in> S. Q x (f x) (fa x) (fb x) (fc x) (fd x) (fe x) (ff x) (fg x)"
    1.22    by metis+
    1.23  
    1.24 -ML {*
    1.25 +ML \<open>
    1.26  fun moura_tac ctxt =
    1.27    Atomize_Elim.atomize_elim_tac ctxt THEN'
    1.28    SELECT_GOAL (Clasimp.auto_tac (ctxt addSIs @{thms choice choices bchoice bchoices}) THEN
    1.29      ALLGOALS (Metis_Tactic.metis_tac (take 1 ATP_Proof_Reconstruct.partial_type_encs)
    1.30          ATP_Proof_Reconstruct.default_metis_lam_trans ctxt [] ORELSE'
    1.31        blast_tac ctxt))
    1.32 -*}
    1.33 +\<close>
    1.34  
    1.35 -method_setup moura = {*
    1.36 +method_setup moura = \<open>
    1.37    Scan.succeed (SIMPLE_METHOD' o moura_tac)
    1.38 -*} "solve skolemization goals, especially those arising from Z3 proofs"
    1.39 +\<close> "solve skolemization goals, especially those arising from Z3 proofs"
    1.40  
    1.41  hide_fact (open) choices bchoices
    1.42  
    1.43  
    1.44 -subsection {* Triggers for quantifier instantiation *}
    1.45 +subsection \<open>Triggers for quantifier instantiation\<close>
    1.46  
    1.47 -text {*
    1.48 +text \<open>
    1.49  Some SMT solvers support patterns as a quantifier instantiation
    1.50  heuristics. Patterns may either be positive terms (tagged by "pat")
    1.51  triggering quantifier instantiations -- when the solver finds a
    1.52 @@ -70,7 +70,7 @@
    1.53  act disjunctively during quantifier instantiation. Each multipattern
    1.54  should mention at least all quantified variables of the preceding
    1.55  quantifier block.
    1.56 -*}
    1.57 +\<close>
    1.58  
    1.59  typedecl 'a symb_list
    1.60  
    1.61 @@ -88,26 +88,26 @@
    1.62    "trigger _ P = P"
    1.63  
    1.64  
    1.65 -subsection {* Higher-order encoding *}
    1.66 +subsection \<open>Higher-order encoding\<close>
    1.67  
    1.68 -text {*
    1.69 +text \<open>
    1.70  Application is made explicit for constants occurring with varying
    1.71  numbers of arguments. This is achieved by the introduction of the
    1.72  following constant.
    1.73 -*}
    1.74 +\<close>
    1.75  
    1.76  definition fun_app :: "'a \<Rightarrow> 'a" where "fun_app f = f"
    1.77  
    1.78 -text {*
    1.79 +text \<open>
    1.80  Some solvers support a theory of arrays which can be used to encode
    1.81  higher-order functions. The following set of lemmas specifies the
    1.82  properties of such (extensional) arrays.
    1.83 -*}
    1.84 +\<close>
    1.85  
    1.86  lemmas array_rules = ext fun_upd_apply fun_upd_same fun_upd_other  fun_upd_upd fun_app_def
    1.87  
    1.88  
    1.89 -subsection {* Normalization *}
    1.90 +subsection \<open>Normalization\<close>
    1.91  
    1.92  lemma case_bool_if[abs_def]: "case_bool x y P = (if P then x else y)"
    1.93    by simp
    1.94 @@ -120,12 +120,12 @@
    1.95  lemmas max_def_raw = max_def[abs_def]
    1.96  
    1.97  
    1.98 -subsection {* Integer division and modulo for Z3 *}
    1.99 +subsection \<open>Integer division and modulo for Z3\<close>
   1.100  
   1.101 -text {*
   1.102 +text \<open>
   1.103  The following Z3-inspired definitions are overspecified for the case where @{text "l = 0"}. This
   1.104  Schönheitsfehler is corrected in the @{text div_as_z3div} and @{text mod_as_z3mod} theorems.
   1.105 -*}
   1.106 +\<close>
   1.107  
   1.108  definition z3div :: "int \<Rightarrow> int \<Rightarrow> int" where
   1.109    "z3div k l = (if l \<ge> 0 then k div l else - (k div - l))"
   1.110 @@ -142,7 +142,7 @@
   1.111    by (simp add: z3mod_def)
   1.112  
   1.113  
   1.114 -subsection {* Setup *}
   1.115 +subsection \<open>Setup\<close>
   1.116  
   1.117  ML_file "Tools/SMT/smt_util.ML"
   1.118  ML_file "Tools/SMT/smt_failure.ML"
   1.119 @@ -171,93 +171,93 @@
   1.120  ML_file "Tools/SMT/z3_replay.ML"
   1.121  ML_file "Tools/SMT/smt_systems.ML"
   1.122  
   1.123 -method_setup smt = {*
   1.124 +method_setup smt = \<open>
   1.125    Scan.optional Attrib.thms [] >>
   1.126      (fn thms => fn ctxt =>
   1.127        METHOD (fn facts => HEADGOAL (SMT_Solver.smt_tac ctxt (thms @ facts))))
   1.128 -*} "apply an SMT solver to the current goal"
   1.129 +\<close> "apply an SMT solver to the current goal"
   1.130  
   1.131  
   1.132 -subsection {* Configuration *}
   1.133 +subsection \<open>Configuration\<close>
   1.134  
   1.135 -text {*
   1.136 +text \<open>
   1.137  The current configuration can be printed by the command
   1.138  @{text smt_status}, which shows the values of most options.
   1.139 -*}
   1.140 +\<close>
   1.141  
   1.142  
   1.143 -subsection {* General configuration options *}
   1.144 +subsection \<open>General configuration options\<close>
   1.145  
   1.146 -text {*
   1.147 +text \<open>
   1.148  The option @{text smt_solver} can be used to change the target SMT
   1.149  solver. The possible values can be obtained from the @{text smt_status}
   1.150  command.
   1.151 -*}
   1.152 +\<close>
   1.153  
   1.154  declare [[smt_solver = z3]]
   1.155  
   1.156 -text {*
   1.157 +text \<open>
   1.158  Since SMT solvers are potentially nonterminating, there is a timeout
   1.159  (given in seconds) to restrict their runtime.
   1.160 -*}
   1.161 +\<close>
   1.162  
   1.163  declare [[smt_timeout = 20]]
   1.164  
   1.165 -text {*
   1.166 +text \<open>
   1.167  SMT solvers apply randomized heuristics. In case a problem is not
   1.168  solvable by an SMT solver, changing the following option might help.
   1.169 -*}
   1.170 +\<close>
   1.171  
   1.172  declare [[smt_random_seed = 1]]
   1.173  
   1.174 -text {*
   1.175 +text \<open>
   1.176  In general, the binding to SMT solvers runs as an oracle, i.e, the SMT
   1.177  solvers are fully trusted without additional checks. The following
   1.178  option can cause the SMT solver to run in proof-producing mode, giving
   1.179  a checkable certificate. This is currently only implemented for Z3.
   1.180 -*}
   1.181 +\<close>
   1.182  
   1.183  declare [[smt_oracle = false]]
   1.184  
   1.185 -text {*
   1.186 +text \<open>
   1.187  Each SMT solver provides several commandline options to tweak its
   1.188  behaviour. They can be passed to the solver by setting the following
   1.189  options.
   1.190 -*}
   1.191 +\<close>
   1.192  
   1.193  declare [[cvc3_options = ""]]
   1.194  declare [[cvc4_options = "--full-saturate-quant --inst-when=full-last-call --inst-no-entail --term-db-mode=relevant"]]
   1.195  declare [[verit_options = ""]]
   1.196  declare [[z3_options = ""]]
   1.197  
   1.198 -text {*
   1.199 +text \<open>
   1.200  The SMT method provides an inference mechanism to detect simple triggers
   1.201  in quantified formulas, which might increase the number of problems
   1.202  solvable by SMT solvers (note: triggers guide quantifier instantiations
   1.203  in the SMT solver). To turn it on, set the following option.
   1.204 -*}
   1.205 +\<close>
   1.206  
   1.207  declare [[smt_infer_triggers = false]]
   1.208  
   1.209 -text {*
   1.210 +text \<open>
   1.211  Enable the following option to use built-in support for datatypes,
   1.212  codatatypes, and records in CVC4. Currently, this is implemented only
   1.213  in oracle mode.
   1.214 -*}
   1.215 +\<close>
   1.216  
   1.217  declare [[cvc4_extensions = false]]
   1.218  
   1.219 -text {*
   1.220 +text \<open>
   1.221  Enable the following option to use built-in support for div/mod, datatypes,
   1.222  and records in Z3. Currently, this is implemented only in oracle mode.
   1.223 -*}
   1.224 +\<close>
   1.225  
   1.226  declare [[z3_extensions = false]]
   1.227  
   1.228  
   1.229 -subsection {* Certificates *}
   1.230 +subsection \<open>Certificates\<close>
   1.231  
   1.232 -text {*
   1.233 +text \<open>
   1.234  By setting the option @{text smt_certificates} to the name of a file,
   1.235  all following applications of an SMT solver a cached in that file.
   1.236  Any further application of the same SMT solver (using the very same
   1.237 @@ -269,11 +269,11 @@
   1.238  @{text ".certs"} instead of @{text ".thy"}) as the certificates file.
   1.239  Certificate files should be used at most once in a certain theory context,
   1.240  to avoid race conditions with other concurrent accesses.
   1.241 -*}
   1.242 +\<close>
   1.243  
   1.244  declare [[smt_certificates = ""]]
   1.245  
   1.246 -text {*
   1.247 +text \<open>
   1.248  The option @{text smt_read_only_certificates} controls whether only
   1.249  stored certificates are should be used or invocation of an SMT solver
   1.250  is allowed. When set to @{text true}, no SMT solver will ever be
   1.251 @@ -281,39 +281,39 @@
   1.252  cache are used;  when set to @{text false} and there is no cached
   1.253  certificate for some proposition, then the configured SMT solver is
   1.254  invoked.
   1.255 -*}
   1.256 +\<close>
   1.257  
   1.258  declare [[smt_read_only_certificates = false]]
   1.259  
   1.260  
   1.261 -subsection {* Tracing *}
   1.262 +subsection \<open>Tracing\<close>
   1.263  
   1.264 -text {*
   1.265 +text \<open>
   1.266  The SMT method, when applied, traces important information. To
   1.267  make it entirely silent, set the following option to @{text false}.
   1.268 -*}
   1.269 +\<close>
   1.270  
   1.271  declare [[smt_verbose = true]]
   1.272  
   1.273 -text {*
   1.274 +text \<open>
   1.275  For tracing the generated problem file given to the SMT solver as
   1.276  well as the returned result of the solver, the option
   1.277  @{text smt_trace} should be set to @{text true}.
   1.278 -*}
   1.279 +\<close>
   1.280  
   1.281  declare [[smt_trace = false]]
   1.282  
   1.283  
   1.284 -subsection {* Schematic rules for Z3 proof reconstruction *}
   1.285 +subsection \<open>Schematic rules for Z3 proof reconstruction\<close>
   1.286  
   1.287 -text {*
   1.288 +text \<open>
   1.289  Several prof rules of Z3 are not very well documented. There are two
   1.290  lemma groups which can turn failing Z3 proof reconstruction attempts
   1.291  into succeeding ones: the facts in @{text z3_rule} are tried prior to
   1.292  any implemented reconstruction procedure for all uncertain Z3 proof
   1.293  rules;  the facts in @{text z3_simp} are only fed to invocations of
   1.294  the simplifier when reconstructing theory-specific proof steps.
   1.295 -*}
   1.296 +\<close>
   1.297  
   1.298  lemmas [z3_rule] =
   1.299    refl eq_commute conj_commute disj_commute simp_thms nnf_simps