src/HOL/SMT.thy
 author wenzelm Sun Nov 02 18:21:45 2014 +0100 (2014-11-02) changeset 58889 5b7a9633cfa8 parent 58776 95e58e04e534 child 59015 627a93f67182 permissions -rw-r--r--
 blanchet@58061 ` 1` ```(* Title: HOL/SMT.thy ``` blanchet@56078 ` 2` ``` Author: Sascha Boehme, TU Muenchen ``` blanchet@56078 ` 3` ```*) ``` blanchet@56078 ` 4` wenzelm@58889 ` 5` ```section {* Bindings to Satisfiability Modulo Theories (SMT) solvers based on SMT-LIB 2 *} ``` blanchet@56078 ` 6` blanchet@58061 ` 7` ```theory SMT ``` blanchet@57230 ` 8` ```imports Divides ``` blanchet@58061 ` 9` ```keywords "smt_status" :: diag ``` blanchet@56078 ` 10` ```begin ``` blanchet@56078 ` 11` blanchet@58481 ` 12` ```subsection {* A skolemization tactic and proof method *} ``` blanchet@58481 ` 13` blanchet@58481 ` 14` ```lemma choices: ``` blanchet@58481 ` 15` ``` "\Q. \x. \y ya. Q x y ya \ \f fa. \x. Q x (f x) (fa x)" ``` blanchet@58481 ` 16` ``` "\Q. \x. \y ya yb. Q x y ya yb \ \f fa fb. \x. Q x (f x) (fa x) (fb x)" ``` blanchet@58481 ` 17` ``` "\Q. \x. \y ya yb yc. Q x y ya yb yc \ \f fa fb fc. \x. Q x (f x) (fa x) (fb x) (fc x)" ``` blanchet@58598 ` 18` ``` "\Q. \x. \y ya yb yc yd. Q x y ya yb yc yd \ ``` blanchet@58598 ` 19` ``` \f fa fb fc fd. \x. Q x (f x) (fa x) (fb x) (fc x) (fd x)" ``` blanchet@58598 ` 20` ``` "\Q. \x. \y ya yb yc yd ye. Q x y ya yb yc yd ye \ ``` blanchet@58598 ` 21` ``` \f fa fb fc fd fe. \x. Q x (f x) (fa x) (fb x) (fc x) (fd x) (fe x)" ``` blanchet@58598 ` 22` ``` "\Q. \x. \y ya yb yc yd ye yf. Q x y ya yb yc yd ye yf \ ``` blanchet@58598 ` 23` ``` \f fa fb fc fd fe ff. \x. Q x (f x) (fa x) (fb x) (fc x) (fd x) (fe x) (ff x)" ``` blanchet@58598 ` 24` ``` "\Q. \x. \y ya yb yc yd ye yf yg. Q x y ya yb yc yd ye yf yg \ ``` blanchet@58598 ` 25` ``` \f fa fb fc fd fe ff fg. \x. Q x (f x) (fa x) (fb x) (fc x) (fd x) (fe x) (ff x) (fg x)" ``` blanchet@58481 ` 26` ``` by metis+ ``` blanchet@58481 ` 27` blanchet@58481 ` 28` ```lemma bchoices: ``` blanchet@58481 ` 29` ``` "\Q. \x \ S. \y ya. Q x y ya \ \f fa. \x \ S. Q x (f x) (fa x)" ``` blanchet@58481 ` 30` ``` "\Q. \x \ S. \y ya yb. Q x y ya yb \ \f fa fb. \x \ S. Q x (f x) (fa x) (fb x)" ``` blanchet@58481 ` 31` ``` "\Q. \x \ S. \y ya yb yc. Q x y ya yb yc \ \f fa fb fc. \x \ S. Q x (f x) (fa x) (fb x) (fc x)" ``` blanchet@58598 ` 32` ``` "\Q. \x \ S. \y ya yb yc yd. Q x y ya yb yc yd \ ``` blanchet@58598 ` 33` ``` \f fa fb fc fd. \x \ S. Q x (f x) (fa x) (fb x) (fc x) (fd x)" ``` blanchet@58598 ` 34` ``` "\Q. \x \ S. \y ya yb yc yd ye. Q x y ya yb yc yd ye \ ``` blanchet@58598 ` 35` ``` \f fa fb fc fd fe. \x \ S. Q x (f x) (fa x) (fb x) (fc x) (fd x) (fe x)" ``` blanchet@58598 ` 36` ``` "\Q. \x \ S. \y ya yb yc yd ye yf. Q x y ya yb yc yd ye yf \ ``` blanchet@58598 ` 37` ``` \f fa fb fc fd fe ff. \x \ S. Q x (f x) (fa x) (fb x) (fc x) (fd x) (fe x) (ff x)" ``` blanchet@58598 ` 38` ``` "\Q. \x \ S. \y ya yb yc yd ye yf yg. Q x y ya yb yc yd ye yf yg \ ``` blanchet@58598 ` 39` ``` \f fa fb fc fd fe ff fg. \x \ S. Q x (f x) (fa x) (fb x) (fc x) (fd x) (fe x) (ff x) (fg x)" ``` blanchet@58481 ` 40` ``` by metis+ ``` blanchet@58481 ` 41` blanchet@58481 ` 42` ```ML {* ``` blanchet@58481 ` 43` ```fun moura_tac ctxt = ``` blanchet@58481 ` 44` ``` Atomize_Elim.atomize_elim_tac ctxt THEN' ``` blanchet@58481 ` 45` ``` SELECT_GOAL (Clasimp.auto_tac (ctxt addSIs @{thms choice choices bchoice bchoices}) THEN ``` blanchet@58598 ` 46` ``` ALLGOALS (Metis_Tactic.metis_tac (take 1 ATP_Proof_Reconstruct.partial_type_encs) ``` blanchet@58598 ` 47` ``` ATP_Proof_Reconstruct.default_metis_lam_trans ctxt [] ORELSE' ``` blanchet@58598 ` 48` ``` blast_tac ctxt)) ``` blanchet@58481 ` 49` ```*} ``` blanchet@58481 ` 50` blanchet@58481 ` 51` ```method_setup moura = {* ``` blanchet@58481 ` 52` ``` Scan.succeed (SIMPLE_METHOD' o moura_tac) ``` blanchet@58481 ` 53` ```*} "solve skolemization goals, especially those arising from Z3 proofs" ``` blanchet@58481 ` 54` blanchet@58481 ` 55` ```hide_fact (open) choices bchoices ``` blanchet@58481 ` 56` blanchet@58481 ` 57` blanchet@56078 ` 58` ```subsection {* Triggers for quantifier instantiation *} ``` blanchet@56078 ` 59` blanchet@56078 ` 60` ```text {* ``` blanchet@56078 ` 61` ```Some SMT solvers support patterns as a quantifier instantiation ``` blanchet@57696 ` 62` ```heuristics. Patterns may either be positive terms (tagged by "pat") ``` blanchet@56078 ` 63` ```triggering quantifier instantiations -- when the solver finds a ``` blanchet@56078 ` 64` ```term matching a positive pattern, it instantiates the corresponding ``` blanchet@56078 ` 65` ```quantifier accordingly -- or negative terms (tagged by "nopat") ``` blanchet@57696 ` 66` ```inhibiting quantifier instantiations. A list of patterns ``` blanchet@56078 ` 67` ```of the same kind is called a multipattern, and all patterns in a ``` blanchet@56078 ` 68` ```multipattern are considered conjunctively for quantifier instantiation. ``` blanchet@56078 ` 69` ```A list of multipatterns is called a trigger, and their multipatterns ``` blanchet@57696 ` 70` ```act disjunctively during quantifier instantiation. Each multipattern ``` blanchet@56078 ` 71` ```should mention at least all quantified variables of the preceding ``` blanchet@56078 ` 72` ```quantifier block. ``` blanchet@56078 ` 73` ```*} ``` blanchet@56078 ` 74` blanchet@57230 ` 75` ```typedecl 'a symb_list ``` blanchet@57230 ` 76` blanchet@57230 ` 77` ```consts ``` blanchet@57230 ` 78` ``` Symb_Nil :: "'a symb_list" ``` blanchet@57230 ` 79` ``` Symb_Cons :: "'a \ 'a symb_list \ 'a symb_list" ``` blanchet@57230 ` 80` blanchet@56078 ` 81` ```typedecl pattern ``` blanchet@56078 ` 82` blanchet@56078 ` 83` ```consts ``` blanchet@56078 ` 84` ``` pat :: "'a \ pattern" ``` blanchet@56078 ` 85` ``` nopat :: "'a \ pattern" ``` blanchet@56078 ` 86` blanchet@57230 ` 87` ```definition trigger :: "pattern symb_list symb_list \ bool \ bool" where ``` blanchet@57230 ` 88` ``` "trigger _ P = P" ``` blanchet@56078 ` 89` blanchet@56078 ` 90` blanchet@56078 ` 91` ```subsection {* Higher-order encoding *} ``` blanchet@56078 ` 92` blanchet@56078 ` 93` ```text {* ``` blanchet@56078 ` 94` ```Application is made explicit for constants occurring with varying ``` blanchet@57696 ` 95` ```numbers of arguments. This is achieved by the introduction of the ``` blanchet@56078 ` 96` ```following constant. ``` blanchet@56078 ` 97` ```*} ``` blanchet@56078 ` 98` blanchet@56078 ` 99` ```definition fun_app :: "'a \ 'a" where "fun_app f = f" ``` blanchet@56078 ` 100` blanchet@56078 ` 101` ```text {* ``` blanchet@56078 ` 102` ```Some solvers support a theory of arrays which can be used to encode ``` blanchet@57696 ` 103` ```higher-order functions. The following set of lemmas specifies the ``` blanchet@56078 ` 104` ```properties of such (extensional) arrays. ``` blanchet@56078 ` 105` ```*} ``` blanchet@56078 ` 106` blanchet@56078 ` 107` ```lemmas array_rules = ext fun_upd_apply fun_upd_same fun_upd_other fun_upd_upd fun_app_def ``` blanchet@56078 ` 108` blanchet@56078 ` 109` blanchet@56103 ` 110` ```subsection {* Normalization *} ``` blanchet@56103 ` 111` blanchet@56103 ` 112` ```lemma case_bool_if[abs_def]: "case_bool x y P = (if P then x else y)" ``` blanchet@56103 ` 113` ``` by simp ``` blanchet@56103 ` 114` blanchet@56103 ` 115` ```lemmas Ex1_def_raw = Ex1_def[abs_def] ``` blanchet@56103 ` 116` ```lemmas Ball_def_raw = Ball_def[abs_def] ``` blanchet@56103 ` 117` ```lemmas Bex_def_raw = Bex_def[abs_def] ``` blanchet@56103 ` 118` ```lemmas abs_if_raw = abs_if[abs_def] ``` blanchet@56103 ` 119` ```lemmas min_def_raw = min_def[abs_def] ``` blanchet@56103 ` 120` ```lemmas max_def_raw = max_def[abs_def] ``` blanchet@56103 ` 121` blanchet@56103 ` 122` blanchet@56078 ` 123` ```subsection {* Integer division and modulo for Z3 *} ``` blanchet@56078 ` 124` blanchet@56102 ` 125` ```text {* ``` blanchet@56102 ` 126` ```The following Z3-inspired definitions are overspecified for the case where @{text "l = 0"}. This ``` blanchet@56102 ` 127` ```SchĂ¶nheitsfehler is corrected in the @{text div_as_z3div} and @{text mod_as_z3mod} theorems. ``` blanchet@56102 ` 128` ```*} ``` blanchet@56102 ` 129` blanchet@56078 ` 130` ```definition z3div :: "int \ int \ int" where ``` blanchet@56102 ` 131` ``` "z3div k l = (if l \ 0 then k div l else - (k div - l))" ``` blanchet@56078 ` 132` blanchet@56078 ` 133` ```definition z3mod :: "int \ int \ int" where ``` blanchet@56102 ` 134` ``` "z3mod k l = k mod (if l \ 0 then l else - l)" ``` blanchet@56078 ` 135` blanchet@56101 ` 136` ```lemma div_as_z3div: ``` blanchet@56102 ` 137` ``` "\k l. k div l = (if l = 0 then 0 else if l > 0 then z3div k l else z3div (- k) (- l))" ``` blanchet@56101 ` 138` ``` by (simp add: z3div_def) ``` blanchet@56101 ` 139` blanchet@56101 ` 140` ```lemma mod_as_z3mod: ``` blanchet@56102 ` 141` ``` "\k l. k mod l = (if l = 0 then k else if l > 0 then z3mod k l else - z3mod (- k) (- l))" ``` blanchet@56101 ` 142` ``` by (simp add: z3mod_def) ``` blanchet@56101 ` 143` blanchet@56078 ` 144` blanchet@56078 ` 145` ```subsection {* Setup *} ``` blanchet@56078 ` 146` blanchet@58061 ` 147` ```ML_file "Tools/SMT/smt_util.ML" ``` blanchet@58061 ` 148` ```ML_file "Tools/SMT/smt_failure.ML" ``` blanchet@58061 ` 149` ```ML_file "Tools/SMT/smt_config.ML" ``` blanchet@58061 ` 150` ```ML_file "Tools/SMT/smt_builtin.ML" ``` blanchet@58061 ` 151` ```ML_file "Tools/SMT/smt_datatypes.ML" ``` blanchet@58061 ` 152` ```ML_file "Tools/SMT/smt_normalize.ML" ``` blanchet@58061 ` 153` ```ML_file "Tools/SMT/smt_translate.ML" ``` blanchet@58061 ` 154` ```ML_file "Tools/SMT/smtlib.ML" ``` blanchet@58061 ` 155` ```ML_file "Tools/SMT/smtlib_interface.ML" ``` blanchet@58061 ` 156` ```ML_file "Tools/SMT/smtlib_proof.ML" ``` blanchet@58061 ` 157` ```ML_file "Tools/SMT/smtlib_isar.ML" ``` blanchet@58061 ` 158` ```ML_file "Tools/SMT/z3_proof.ML" ``` blanchet@58061 ` 159` ```ML_file "Tools/SMT/z3_isar.ML" ``` blanchet@58061 ` 160` ```ML_file "Tools/SMT/smt_solver.ML" ``` blanchet@58360 ` 161` ```ML_file "Tools/SMT/cvc4_interface.ML" ``` blanchet@58360 ` 162` ```ML_file "Tools/SMT/verit_proof.ML" ``` blanchet@58360 ` 163` ```ML_file "Tools/SMT/verit_isar.ML" ``` blanchet@58360 ` 164` ```ML_file "Tools/SMT/verit_proof_parse.ML" ``` blanchet@58061 ` 165` ```ML_file "Tools/SMT/z3_interface.ML" ``` blanchet@58061 ` 166` ```ML_file "Tools/SMT/z3_replay_util.ML" ``` blanchet@58061 ` 167` ```ML_file "Tools/SMT/z3_replay_literals.ML" ``` blanchet@58061 ` 168` ```ML_file "Tools/SMT/z3_replay_rules.ML" ``` blanchet@58061 ` 169` ```ML_file "Tools/SMT/z3_replay_methods.ML" ``` blanchet@58061 ` 170` ```ML_file "Tools/SMT/z3_replay.ML" ``` blanchet@58061 ` 171` ```ML_file "Tools/SMT/smt_systems.ML" ``` blanchet@56078 ` 172` blanchet@58061 ` 173` ```method_setup smt = {* ``` blanchet@56078 ` 174` ``` Scan.optional Attrib.thms [] >> ``` blanchet@56078 ` 175` ``` (fn thms => fn ctxt => ``` blanchet@58061 ` 176` ``` METHOD (fn facts => HEADGOAL (SMT_Solver.smt_tac ctxt (thms @ facts)))) ``` blanchet@58072 ` 177` ```*} "apply an SMT solver to the current goal" ``` blanchet@56078 ` 178` blanchet@56078 ` 179` blanchet@56078 ` 180` ```subsection {* Configuration *} ``` blanchet@56078 ` 181` blanchet@56078 ` 182` ```text {* ``` blanchet@56078 ` 183` ```The current configuration can be printed by the command ``` blanchet@58061 ` 184` ```@{text smt_status}, which shows the values of most options. ``` blanchet@56078 ` 185` ```*} ``` blanchet@56078 ` 186` blanchet@56078 ` 187` blanchet@56078 ` 188` ```subsection {* General configuration options *} ``` blanchet@56078 ` 189` blanchet@56078 ` 190` ```text {* ``` blanchet@58061 ` 191` ```The option @{text smt_solver} can be used to change the target SMT ``` blanchet@58061 ` 192` ```solver. The possible values can be obtained from the @{text smt_status} ``` blanchet@56078 ` 193` ```command. ``` blanchet@56078 ` 194` blanchet@57696 ` 195` ```Due to licensing restrictions, Z3 is not enabled by default. Z3 is free ``` blanchet@57237 ` 196` ```for non-commercial applications and can be enabled by setting Isabelle ``` blanchet@57237 ` 197` ```system option @{text z3_non_commercial} to @{text yes}. ``` blanchet@56078 ` 198` ```*} ``` blanchet@56078 ` 199` blanchet@58061 ` 200` ```declare [[smt_solver = z3]] ``` blanchet@56078 ` 201` blanchet@56078 ` 202` ```text {* ``` blanchet@57696 ` 203` ```Since SMT solvers are potentially nonterminating, there is a timeout ``` blanchet@57696 ` 204` ```(given in seconds) to restrict their runtime. ``` blanchet@56078 ` 205` ```*} ``` blanchet@56078 ` 206` blanchet@58061 ` 207` ```declare [[smt_timeout = 20]] ``` blanchet@56078 ` 208` blanchet@56078 ` 209` ```text {* ``` blanchet@57696 ` 210` ```SMT solvers apply randomized heuristics. In case a problem is not ``` blanchet@56078 ` 211` ```solvable by an SMT solver, changing the following option might help. ``` blanchet@56078 ` 212` ```*} ``` blanchet@56078 ` 213` blanchet@58061 ` 214` ```declare [[smt_random_seed = 1]] ``` blanchet@56078 ` 215` blanchet@56078 ` 216` ```text {* ``` blanchet@56078 ` 217` ```In general, the binding to SMT solvers runs as an oracle, i.e, the SMT ``` blanchet@57696 ` 218` ```solvers are fully trusted without additional checks. The following ``` blanchet@56078 ` 219` ```option can cause the SMT solver to run in proof-producing mode, giving ``` blanchet@57696 ` 220` ```a checkable certificate. This is currently only implemented for Z3. ``` blanchet@56078 ` 221` ```*} ``` blanchet@56078 ` 222` blanchet@58061 ` 223` ```declare [[smt_oracle = false]] ``` blanchet@56078 ` 224` blanchet@56078 ` 225` ```text {* ``` blanchet@56078 ` 226` ```Each SMT solver provides several commandline options to tweak its ``` blanchet@57696 ` 227` ```behaviour. They can be passed to the solver by setting the following ``` blanchet@56078 ` 228` ```options. ``` blanchet@56078 ` 229` ```*} ``` blanchet@56078 ` 230` blanchet@58061 ` 231` ```declare [[cvc3_options = ""]] ``` blanchet@58441 ` 232` ```declare [[cvc4_options = "--full-saturate-quant --quant-cf"]] ``` blanchet@58061 ` 233` ```declare [[veriT_options = ""]] ``` blanchet@58061 ` 234` ```declare [[z3_options = ""]] ``` blanchet@56078 ` 235` blanchet@56078 ` 236` ```text {* ``` blanchet@56078 ` 237` ```The SMT method provides an inference mechanism to detect simple triggers ``` blanchet@56078 ` 238` ```in quantified formulas, which might increase the number of problems ``` blanchet@56078 ` 239` ```solvable by SMT solvers (note: triggers guide quantifier instantiations ``` blanchet@57696 ` 240` ```in the SMT solver). To turn it on, set the following option. ``` blanchet@56078 ` 241` ```*} ``` blanchet@56078 ` 242` blanchet@58061 ` 243` ```declare [[smt_infer_triggers = false]] ``` blanchet@56078 ` 244` blanchet@56078 ` 245` ```text {* ``` blanchet@58360 ` 246` ```Enable the following option to use built-in support for datatypes, ``` blanchet@58360 ` 247` ```codatatypes, and records in CVC4. Currently, this is implemented only ``` blanchet@58360 ` 248` ```in oracle mode. ``` blanchet@58360 ` 249` ```*} ``` blanchet@58360 ` 250` blanchet@58360 ` 251` ```declare [[cvc4_extensions = false]] ``` blanchet@58360 ` 252` blanchet@58360 ` 253` ```text {* ``` blanchet@56078 ` 254` ```Enable the following option to use built-in support for div/mod, datatypes, ``` blanchet@57696 ` 255` ```and records in Z3. Currently, this is implemented only in oracle mode. ``` blanchet@56078 ` 256` ```*} ``` blanchet@56078 ` 257` blanchet@58061 ` 258` ```declare [[z3_extensions = false]] ``` blanchet@56078 ` 259` blanchet@56078 ` 260` blanchet@56078 ` 261` ```subsection {* Certificates *} ``` blanchet@56078 ` 262` blanchet@56078 ` 263` ```text {* ``` blanchet@58061 ` 264` ```By setting the option @{text smt_certificates} to the name of a file, ``` blanchet@56078 ` 265` ```all following applications of an SMT solver a cached in that file. ``` blanchet@56078 ` 266` ```Any further application of the same SMT solver (using the very same ``` blanchet@56078 ` 267` ```configuration) re-uses the cached certificate instead of invoking the ``` blanchet@57696 ` 268` ```solver. An empty string disables caching certificates. ``` blanchet@56078 ` 269` blanchet@57696 ` 270` ```The filename should be given as an explicit path. It is good ``` blanchet@56078 ` 271` ```practice to use the name of the current theory (with ending ``` blanchet@56078 ` 272` ```@{text ".certs"} instead of @{text ".thy"}) as the certificates file. ``` blanchet@56078 ` 273` ```Certificate files should be used at most once in a certain theory context, ``` blanchet@56078 ` 274` ```to avoid race conditions with other concurrent accesses. ``` blanchet@56078 ` 275` ```*} ``` blanchet@56078 ` 276` blanchet@58061 ` 277` ```declare [[smt_certificates = ""]] ``` blanchet@56078 ` 278` blanchet@56078 ` 279` ```text {* ``` blanchet@58061 ` 280` ```The option @{text smt_read_only_certificates} controls whether only ``` blanchet@56078 ` 281` ```stored certificates are should be used or invocation of an SMT solver ``` blanchet@57696 ` 282` ```is allowed. When set to @{text true}, no SMT solver will ever be ``` blanchet@56078 ` 283` ```invoked and only the existing certificates found in the configured ``` blanchet@56078 ` 284` ```cache are used; when set to @{text false} and there is no cached ``` blanchet@56078 ` 285` ```certificate for some proposition, then the configured SMT solver is ``` blanchet@56078 ` 286` ```invoked. ``` blanchet@56078 ` 287` ```*} ``` blanchet@56078 ` 288` blanchet@58061 ` 289` ```declare [[smt_read_only_certificates = false]] ``` blanchet@56078 ` 290` blanchet@56078 ` 291` blanchet@56078 ` 292` ```subsection {* Tracing *} ``` blanchet@56078 ` 293` blanchet@56078 ` 294` ```text {* ``` blanchet@57696 ` 295` ```The SMT method, when applied, traces important information. To ``` blanchet@56078 ` 296` ```make it entirely silent, set the following option to @{text false}. ``` blanchet@56078 ` 297` ```*} ``` blanchet@56078 ` 298` blanchet@58061 ` 299` ```declare [[smt_verbose = true]] ``` blanchet@56078 ` 300` blanchet@56078 ` 301` ```text {* ``` blanchet@56078 ` 302` ```For tracing the generated problem file given to the SMT solver as ``` blanchet@56078 ` 303` ```well as the returned result of the solver, the option ``` blanchet@58061 ` 304` ```@{text smt_trace} should be set to @{text true}. ``` blanchet@56078 ` 305` ```*} ``` blanchet@56078 ` 306` blanchet@58061 ` 307` ```declare [[smt_trace = false]] ``` blanchet@56078 ` 308` blanchet@56078 ` 309` blanchet@56078 ` 310` ```subsection {* Schematic rules for Z3 proof reconstruction *} ``` blanchet@56078 ` 311` blanchet@56078 ` 312` ```text {* ``` blanchet@57696 ` 313` ```Several prof rules of Z3 are not very well documented. There are two ``` blanchet@56078 ` 314` ```lemma groups which can turn failing Z3 proof reconstruction attempts ``` blanchet@56078 ` 315` ```into succeeding ones: the facts in @{text z3_rule} are tried prior to ``` blanchet@56078 ` 316` ```any implemented reconstruction procedure for all uncertain Z3 proof ``` blanchet@56078 ` 317` ```rules; the facts in @{text z3_simp} are only fed to invocations of ``` blanchet@56078 ` 318` ```the simplifier when reconstructing theory-specific proof steps. ``` blanchet@56078 ` 319` ```*} ``` blanchet@56078 ` 320` blanchet@58061 ` 321` ```lemmas [z3_rule] = ``` blanchet@56078 ` 322` ``` refl eq_commute conj_commute disj_commute simp_thms nnf_simps ``` blanchet@56078 ` 323` ``` ring_distribs field_simps times_divide_eq_right times_divide_eq_left ``` blanchet@56078 ` 324` ``` if_True if_False not_not ``` hoelzl@58776 ` 325` ``` NO_MATCH_def ``` blanchet@56078 ` 326` blanchet@58061 ` 327` ```lemma [z3_rule]: ``` blanchet@57169 ` 328` ``` "(P \ Q) = (\ (\ P \ \ Q))" ``` blanchet@57169 ` 329` ``` "(P \ Q) = (\ (\ Q \ \ P))" ``` blanchet@57169 ` 330` ``` "(\ P \ Q) = (\ (P \ \ Q))" ``` blanchet@57169 ` 331` ``` "(\ P \ Q) = (\ (\ Q \ P))" ``` blanchet@57169 ` 332` ``` "(P \ \ Q) = (\ (\ P \ Q))" ``` blanchet@57169 ` 333` ``` "(P \ \ Q) = (\ (Q \ \ P))" ``` blanchet@57169 ` 334` ``` "(\ P \ \ Q) = (\ (P \ Q))" ``` blanchet@57169 ` 335` ``` "(\ P \ \ Q) = (\ (Q \ P))" ``` blanchet@56078 ` 336` ``` by auto ``` blanchet@56078 ` 337` blanchet@58061 ` 338` ```lemma [z3_rule]: ``` blanchet@57169 ` 339` ``` "(P \ Q) = (Q \ \ P)" ``` blanchet@57169 ` 340` ``` "(\ P \ Q) = (P \ Q)" ``` blanchet@57169 ` 341` ``` "(\ P \ Q) = (Q \ P)" ``` blanchet@56078 ` 342` ``` "(True \ P) = P" ``` blanchet@56078 ` 343` ``` "(P \ True) = True" ``` blanchet@56078 ` 344` ``` "(False \ P) = True" ``` blanchet@56078 ` 345` ``` "(P \ P) = True" ``` blanchet@56078 ` 346` ``` by auto ``` blanchet@56078 ` 347` blanchet@58061 ` 348` ```lemma [z3_rule]: ``` blanchet@57169 ` 349` ``` "((P = Q) \ R) = (R | (Q = (\ P)))" ``` blanchet@56078 ` 350` ``` by auto ``` blanchet@56078 ` 351` blanchet@58061 ` 352` ```lemma [z3_rule]: ``` blanchet@57169 ` 353` ``` "(\ True) = False" ``` blanchet@57169 ` 354` ``` "(\ False) = True" ``` blanchet@56078 ` 355` ``` "(x = x) = True" ``` blanchet@56078 ` 356` ``` "(P = True) = P" ``` blanchet@56078 ` 357` ``` "(True = P) = P" ``` blanchet@57169 ` 358` ``` "(P = False) = (\ P)" ``` blanchet@57169 ` 359` ``` "(False = P) = (\ P)" ``` blanchet@57169 ` 360` ``` "((\ P) = P) = False" ``` blanchet@57169 ` 361` ``` "(P = (\ P)) = False" ``` blanchet@57169 ` 362` ``` "((\ P) = (\ Q)) = (P = Q)" ``` blanchet@57169 ` 363` ``` "\ (P = (\ Q)) = (P = Q)" ``` blanchet@57169 ` 364` ``` "\ ((\ P) = Q) = (P = Q)" ``` blanchet@57169 ` 365` ``` "(P \ Q) = (Q = (\ P))" ``` blanchet@57169 ` 366` ``` "(P = Q) = ((\ P \ Q) \ (P \ \ Q))" ``` blanchet@57169 ` 367` ``` "(P \ Q) = ((\ P \ \ Q) \ (P \ Q))" ``` blanchet@56078 ` 368` ``` by auto ``` blanchet@56078 ` 369` blanchet@58061 ` 370` ```lemma [z3_rule]: ``` blanchet@57169 ` 371` ``` "(if P then P else \ P) = True" ``` blanchet@57169 ` 372` ``` "(if \ P then \ P else P) = True" ``` blanchet@56078 ` 373` ``` "(if P then True else False) = P" ``` blanchet@57169 ` 374` ``` "(if P then False else True) = (\ P)" ``` blanchet@57169 ` 375` ``` "(if P then Q else True) = ((\ P) \ Q)" ``` blanchet@57169 ` 376` ``` "(if P then Q else True) = (Q \ (\ P))" ``` blanchet@57169 ` 377` ``` "(if P then Q else \ Q) = (P = Q)" ``` blanchet@57169 ` 378` ``` "(if P then Q else \ Q) = (Q = P)" ``` blanchet@57169 ` 379` ``` "(if P then \ Q else Q) = (P = (\ Q))" ``` blanchet@57169 ` 380` ``` "(if P then \ Q else Q) = ((\ Q) = P)" ``` blanchet@57169 ` 381` ``` "(if \ P then x else y) = (if P then y else x)" ``` blanchet@57169 ` 382` ``` "(if P then (if Q then x else y) else x) = (if P \ (\ Q) then y else x)" ``` blanchet@57169 ` 383` ``` "(if P then (if Q then x else y) else x) = (if (\ Q) \ P then y else x)" ``` blanchet@56078 ` 384` ``` "(if P then (if Q then x else y) else y) = (if P \ Q then x else y)" ``` blanchet@56078 ` 385` ``` "(if P then (if Q then x else y) else y) = (if Q \ P then x else y)" ``` blanchet@56078 ` 386` ``` "(if P then x else if P then y else z) = (if P then x else z)" ``` blanchet@56078 ` 387` ``` "(if P then x else if Q then x else y) = (if P \ Q then x else y)" ``` blanchet@56078 ` 388` ``` "(if P then x else if Q then x else y) = (if Q \ P then x else y)" ``` blanchet@56078 ` 389` ``` "(if P then x = y else x = z) = (x = (if P then y else z))" ``` blanchet@56078 ` 390` ``` "(if P then x = y else y = z) = (y = (if P then x else z))" ``` blanchet@56078 ` 391` ``` "(if P then x = y else z = y) = (y = (if P then x else z))" ``` blanchet@56078 ` 392` ``` by auto ``` blanchet@56078 ` 393` blanchet@58061 ` 394` ```lemma [z3_rule]: ``` blanchet@56078 ` 395` ``` "0 + (x::int) = x" ``` blanchet@56078 ` 396` ``` "x + 0 = x" ``` blanchet@56078 ` 397` ``` "x + x = 2 * x" ``` blanchet@56078 ` 398` ``` "0 * x = 0" ``` blanchet@56078 ` 399` ``` "1 * x = x" ``` blanchet@56078 ` 400` ``` "x + y = y + x" ``` blanchet@57230 ` 401` ``` by (auto simp add: mult_2) ``` blanchet@56078 ` 402` blanchet@58061 ` 403` ```lemma [z3_rule]: (* for def-axiom *) ``` blanchet@56078 ` 404` ``` "P = Q \ P \ Q" ``` blanchet@57169 ` 405` ``` "P = Q \ \ P \ \ Q" ``` blanchet@57169 ` 406` ``` "(\ P) = Q \ \ P \ Q" ``` blanchet@57169 ` 407` ``` "(\ P) = Q \ P \ \ Q" ``` blanchet@57169 ` 408` ``` "P = (\ Q) \ \ P \ Q" ``` blanchet@57169 ` 409` ``` "P = (\ Q) \ P \ \ Q" ``` blanchet@57169 ` 410` ``` "P \ Q \ P \ \ Q" ``` blanchet@57169 ` 411` ``` "P \ Q \ \ P \ Q" ``` blanchet@57169 ` 412` ``` "P \ (\ Q) \ P \ Q" ``` blanchet@57169 ` 413` ``` "(\ P) \ Q \ P \ Q" ``` blanchet@57169 ` 414` ``` "P \ Q \ P \ (\ Q)" ``` blanchet@57169 ` 415` ``` "P \ Q \ (\ P) \ Q" ``` blanchet@57169 ` 416` ``` "P \ \ Q \ P \ Q" ``` blanchet@57169 ` 417` ``` "\ P \ Q \ P \ Q" ``` blanchet@56078 ` 418` ``` "P \ y = (if P then x else y)" ``` blanchet@56078 ` 419` ``` "P \ (if P then x else y) = y" ``` blanchet@57169 ` 420` ``` "\ P \ x = (if P then x else y)" ``` blanchet@57169 ` 421` ``` "\ P \ (if P then x else y) = x" ``` blanchet@57169 ` 422` ``` "P \ R \ \ (if P then Q else R)" ``` blanchet@57169 ` 423` ``` "\ P \ Q \ \ (if P then Q else R)" ``` blanchet@57169 ` 424` ``` "\ (if P then Q else R) \ \ P \ Q" ``` blanchet@57169 ` 425` ``` "\ (if P then Q else R) \ P \ R" ``` blanchet@57169 ` 426` ``` "(if P then Q else R) \ \ P \ \ Q" ``` blanchet@57169 ` 427` ``` "(if P then Q else R) \ P \ \ R" ``` blanchet@57169 ` 428` ``` "(if P then \ Q else R) \ \ P \ Q" ``` blanchet@57169 ` 429` ``` "(if P then Q else \ R) \ P \ R" ``` blanchet@56078 ` 430` ``` by auto ``` blanchet@56078 ` 431` blanchet@57230 ` 432` ```hide_type (open) symb_list pattern ``` blanchet@57230 ` 433` ```hide_const (open) Symb_Nil Symb_Cons trigger pat nopat fun_app z3div z3mod ``` blanchet@56078 ` 434` blanchet@56078 ` 435` ```end ```