1(* Title: HOL/SMT.thy 2 Author: Sascha Boehme, TU Muenchen 3 Author: Jasmin Blanchette, VU Amsterdam 4*) 5 6section \<open>Bindings to Satisfiability Modulo Theories (SMT) solvers based on SMT-LIB 2\<close> 7 8theory SMT 9 imports Divides 10 keywords "smt_status" :: diag 11begin 12 13subsection \<open>A skolemization tactic and proof method\<close> 14 15lemma choices: 16 "\<And>Q. \<forall>x. \<exists>y ya. Q x y ya \<Longrightarrow> \<exists>f fa. \<forall>x. Q x (f x) (fa x)" 17 "\<And>Q. \<forall>x. \<exists>y ya yb. Q x y ya yb \<Longrightarrow> \<exists>f fa fb. \<forall>x. Q x (f x) (fa x) (fb x)" 18 "\<And>Q. \<forall>x. \<exists>y ya yb yc. Q x y ya yb yc \<Longrightarrow> \<exists>f fa fb fc. \<forall>x. Q x (f x) (fa x) (fb x) (fc x)" 19 "\<And>Q. \<forall>x. \<exists>y ya yb yc yd. Q x y ya yb yc yd \<Longrightarrow> 20 \<exists>f fa fb fc fd. \<forall>x. Q x (f x) (fa x) (fb x) (fc x) (fd x)" 21 "\<And>Q. \<forall>x. \<exists>y ya yb yc yd ye. Q x y ya yb yc yd ye \<Longrightarrow> 22 \<exists>f fa fb fc fd fe. \<forall>x. Q x (f x) (fa x) (fb x) (fc x) (fd x) (fe x)" 23 "\<And>Q. \<forall>x. \<exists>y ya yb yc yd ye yf. Q x y ya yb yc yd ye yf \<Longrightarrow> 24 \<exists>f fa fb fc fd fe ff. \<forall>x. Q x (f x) (fa x) (fb x) (fc x) (fd x) (fe x) (ff x)" 25 "\<And>Q. \<forall>x. \<exists>y ya yb yc yd ye yf yg. Q x y ya yb yc yd ye yf yg \<Longrightarrow> 26 \<exists>f fa fb fc fd fe ff fg. \<forall>x. Q x (f x) (fa x) (fb x) (fc x) (fd x) (fe x) (ff x) (fg x)" 27 by metis+ 28 29lemma bchoices: 30 "\<And>Q. \<forall>x \<in> S. \<exists>y ya. Q x y ya \<Longrightarrow> \<exists>f fa. \<forall>x \<in> S. Q x (f x) (fa x)" 31 "\<And>Q. \<forall>x \<in> S. \<exists>y ya yb. Q x y ya yb \<Longrightarrow> \<exists>f fa fb. \<forall>x \<in> S. Q x (f x) (fa x) (fb x)" 32 "\<And>Q. \<forall>x \<in> S. \<exists>y ya yb yc. Q x y ya yb yc \<Longrightarrow> \<exists>f fa fb fc. \<forall>x \<in> S. Q x (f x) (fa x) (fb x) (fc x)" 33 "\<And>Q. \<forall>x \<in> S. \<exists>y ya yb yc yd. Q x y ya yb yc yd \<Longrightarrow> 34 \<exists>f fa fb fc fd. \<forall>x \<in> S. Q x (f x) (fa x) (fb x) (fc x) (fd x)" 35 "\<And>Q. \<forall>x \<in> S. \<exists>y ya yb yc yd ye. Q x y ya yb yc yd ye \<Longrightarrow> 36 \<exists>f fa fb fc fd fe. \<forall>x \<in> S. Q x (f x) (fa x) (fb x) (fc x) (fd x) (fe x)" 37 "\<And>Q. \<forall>x \<in> S. \<exists>y ya yb yc yd ye yf. Q x y ya yb yc yd ye yf \<Longrightarrow> 38 \<exists>f fa fb fc fd fe ff. \<forall>x \<in> S. Q x (f x) (fa x) (fb x) (fc x) (fd x) (fe x) (ff x)" 39 "\<And>Q. \<forall>x \<in> S. \<exists>y ya yb yc yd ye yf yg. Q x y ya yb yc yd ye yf yg \<Longrightarrow> 40 \<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)" 41 by metis+ 42 43ML \<open> 44fun moura_tac ctxt = 45 Atomize_Elim.atomize_elim_tac ctxt THEN' 46 SELECT_GOAL (Clasimp.auto_tac (ctxt addSIs @{thms choice choices bchoice bchoices}) THEN 47 ALLGOALS (Metis_Tactic.metis_tac (take 1 ATP_Proof_Reconstruct.partial_type_encs) 48 ATP_Proof_Reconstruct.default_metis_lam_trans ctxt [] ORELSE' 49 blast_tac ctxt)) 50\<close> 51 52method_setup moura = \<open> 53 Scan.succeed (SIMPLE_METHOD' o moura_tac) 54\<close> "solve skolemization goals, especially those arising from Z3 proofs" 55 56hide_fact (open) choices bchoices 57 58 59subsection \<open>Triggers for quantifier instantiation\<close> 60 61text \<open> 62Some SMT solvers support patterns as a quantifier instantiation 63heuristics. Patterns may either be positive terms (tagged by "pat") 64triggering quantifier instantiations -- when the solver finds a 65term matching a positive pattern, it instantiates the corresponding 66quantifier accordingly -- or negative terms (tagged by "nopat") 67inhibiting quantifier instantiations. A list of patterns 68of the same kind is called a multipattern, and all patterns in a 69multipattern are considered conjunctively for quantifier instantiation. 70A list of multipatterns is called a trigger, and their multipatterns 71act disjunctively during quantifier instantiation. Each multipattern 72should mention at least all quantified variables of the preceding 73quantifier block. 74\<close> 75 76typedecl 'a symb_list 77 78consts 79 Symb_Nil :: "'a symb_list" 80 Symb_Cons :: "'a \<Rightarrow> 'a symb_list \<Rightarrow> 'a symb_list" 81 82typedecl pattern 83 84consts 85 pat :: "'a \<Rightarrow> pattern" 86 nopat :: "'a \<Rightarrow> pattern" 87 88definition trigger :: "pattern symb_list symb_list \<Rightarrow> bool \<Rightarrow> bool" where 89 "trigger _ P = P" 90 91 92subsection \<open>Higher-order encoding\<close> 93 94text \<open> 95Application is made explicit for constants occurring with varying 96numbers of arguments. This is achieved by the introduction of the 97following constant. 98\<close> 99 100definition fun_app :: "'a \<Rightarrow> 'a" where "fun_app f = f" 101 102text \<open> 103Some solvers support a theory of arrays which can be used to encode 104higher-order functions. The following set of lemmas specifies the 105properties of such (extensional) arrays. 106\<close> 107 108lemmas array_rules = ext fun_upd_apply fun_upd_same fun_upd_other fun_upd_upd fun_app_def 109 110 111subsection \<open>Normalization\<close> 112 113lemma case_bool_if[abs_def]: "case_bool x y P = (if P then x else y)" 114 by simp 115 116lemmas Ex1_def_raw = Ex1_def[abs_def] 117lemmas Ball_def_raw = Ball_def[abs_def] 118lemmas Bex_def_raw = Bex_def[abs_def] 119lemmas abs_if_raw = abs_if[abs_def] 120lemmas min_def_raw = min_def[abs_def] 121lemmas max_def_raw = max_def[abs_def] 122 123lemma nat_zero_as_int: 124 "0 = nat 0" 125 by simp 126 127lemma nat_one_as_int: 128 "1 = nat 1" 129 by simp 130 131lemma nat_numeral_as_int: "numeral = (\<lambda>i. nat (numeral i))" by simp 132lemma nat_less_as_int: "(<) = (\<lambda>a b. int a < int b)" by simp 133lemma nat_leq_as_int: "(\<le>) = (\<lambda>a b. int a \<le> int b)" by simp 134lemma Suc_as_int: "Suc = (\<lambda>a. nat (int a + 1))" by (rule ext) simp 135lemma nat_plus_as_int: "(+) = (\<lambda>a b. nat (int a + int b))" by (rule ext)+ simp 136lemma nat_minus_as_int: "(-) = (\<lambda>a b. nat (int a - int b))" by (rule ext)+ simp 137lemma nat_times_as_int: "(*) = (\<lambda>a b. nat (int a * int b))" by (simp add: nat_mult_distrib) 138lemma nat_div_as_int: "(div) = (\<lambda>a b. nat (int a div int b))" by (simp add: nat_div_distrib) 139lemma nat_mod_as_int: "(mod) = (\<lambda>a b. nat (int a mod int b))" by (simp add: nat_mod_distrib) 140 141lemma int_Suc: "int (Suc n) = int n + 1" by simp 142lemma int_plus: "int (n + m) = int n + int m" by (rule of_nat_add) 143lemma int_minus: "int (n - m) = int (nat (int n - int m))" by auto 144 145lemma nat_int_comparison: 146 fixes a b :: nat 147 shows "(a = b) = (int a = int b)" 148 and "(a < b) = (int a < int b)" 149 and "(a \<le> b) = (int a \<le> int b)" 150 by simp_all 151 152lemma int_ops: 153 fixes a b :: nat 154 shows "int 0 = 0" 155 and "int 1 = 1" 156 and "int (numeral n) = numeral n" 157 and "int (Suc a) = int a + 1" 158 and "int (a + b) = int a + int b" 159 and "int (a - b) = (if int a < int b then 0 else int a - int b)" 160 and "int (a * b) = int a * int b" 161 and "int (a div b) = int a div int b" 162 and "int (a mod b) = int a mod int b" 163 by (auto intro: zdiv_int zmod_int) 164 165lemma int_if: 166 fixes a b :: nat 167 shows "int (if P then a else b) = (if P then int a else int b)" 168 by simp 169 170 171subsection \<open>Integer division and modulo for Z3\<close> 172 173text \<open> 174The following Z3-inspired definitions are overspecified for the case where \<open>l = 0\<close>. This 175Sch��nheitsfehler is corrected in the \<open>div_as_z3div\<close> and \<open>mod_as_z3mod\<close> theorems. 176\<close> 177 178definition z3div :: "int \<Rightarrow> int \<Rightarrow> int" where 179 "z3div k l = (if l \<ge> 0 then k div l else - (k div - l))" 180 181definition z3mod :: "int \<Rightarrow> int \<Rightarrow> int" where 182 "z3mod k l = k mod (if l \<ge> 0 then l else - l)" 183 184lemma div_as_z3div: 185 "\<forall>k l. k div l = (if l = 0 then 0 else if l > 0 then z3div k l else z3div (- k) (- l))" 186 by (simp add: z3div_def) 187 188lemma mod_as_z3mod: 189 "\<forall>k l. k mod l = (if l = 0 then k else if l > 0 then z3mod k l else - z3mod (- k) (- l))" 190 by (simp add: z3mod_def) 191 192 193subsection \<open>Extra theorems for veriT reconstruction\<close> 194 195lemma verit_sko_forall: \<open>(\<forall>x. P x) \<longleftrightarrow> P (SOME x. \<not>P x)\<close> 196 using someI[of \<open>\<lambda>x. \<not>P x\<close>] 197 by auto 198 199lemma verit_sko_forall': \<open>P (SOME x. \<not>P x) = A \<Longrightarrow> (\<forall>x. P x) = A\<close> 200 by (subst verit_sko_forall) 201 202lemma verit_sko_forall_indirect: \<open>x = (SOME x. \<not>P x) \<Longrightarrow> (\<forall>x. P x) \<longleftrightarrow> P x\<close> 203 using someI[of \<open>\<lambda>x. \<not>P x\<close>] 204 by auto 205 206lemma verit_sko_ex: \<open>(\<exists>x. P x) \<longleftrightarrow> P (SOME x. P x)\<close> 207 using someI[of \<open>\<lambda>x. P x\<close>] 208 by auto 209 210lemma verit_sko_ex': \<open>P (SOME x. P x) = A \<Longrightarrow> (\<exists>x. P x) = A\<close> 211 by (subst verit_sko_ex) 212 213lemma verit_sko_ex_indirect: \<open>x = (SOME x. P x) \<Longrightarrow> (\<exists>x. P x) \<longleftrightarrow> P x\<close> 214 using someI[of \<open>\<lambda>x. P x\<close>] 215 by auto 216 217lemma verit_Pure_trans: 218 \<open>P \<equiv> Q \<Longrightarrow> Q \<Longrightarrow> P\<close> 219 by auto 220 221lemma verit_if_cong: 222 assumes \<open>b \<equiv> c\<close> 223 and \<open>c \<Longrightarrow> x \<equiv> u\<close> 224 and \<open>\<not> c \<Longrightarrow> y \<equiv> v\<close> 225 shows \<open>(if b then x else y) \<equiv> (if c then u else v)\<close> 226 using assms if_cong[of b c x u] by auto 227 228lemma verit_if_weak_cong': 229 \<open>b \<equiv> c \<Longrightarrow> (if b then x else y) \<equiv> (if c then x else y)\<close> 230 by auto 231 232lemma verit_ite_intro_simp: 233 \<open>(if c then (a :: 'a) = (if c then P else Q') else Q) = (if c then a = P else Q)\<close> 234 \<open>(if c then R else b = (if c then R' else Q')) = 235 (if c then R else b = Q')\<close> 236 \<open>(if c then a' = a' else b' = b')\<close> 237 by (auto split: if_splits) 238 239lemma verit_or_neg: 240 \<open>(A \<Longrightarrow> B) \<Longrightarrow> B \<or> \<not>A\<close> 241 \<open>(\<not>A \<Longrightarrow> B) \<Longrightarrow> B \<or> A\<close> 242 by auto 243 244lemma verit_subst_bool: \<open>P \<Longrightarrow> f True \<Longrightarrow> f P\<close> 245 by auto 246 247lemma verit_and_pos: 248 \<open>(a \<Longrightarrow> \<not>b \<or> A) \<Longrightarrow> \<not>(a \<and> b) \<or> A\<close> 249 \<open>(a \<Longrightarrow> A) \<Longrightarrow> \<not>a \<or> A\<close> 250 \<open>(\<not>a \<Longrightarrow> A) \<Longrightarrow> a \<or> A\<close> 251 by blast+ 252 253lemma verit_la_generic: 254 \<open>(a::int) \<le> x \<or> a = x \<or> a \<ge> x\<close> 255 by linarith 256 257lemma verit_tmp_bfun_elim: 258 \<open>(if b then P True else P False) = P b\<close> 259 by (cases b) auto 260 261lemma verit_eq_true_simplify: 262 \<open>(P = True) \<equiv> P\<close> 263 by auto 264 265lemma verit_and_neg: 266 \<open>B \<or> B' \<Longrightarrow> (A \<and> B) \<or> \<not>A \<or> B'\<close> 267 \<open>B \<or> B' \<Longrightarrow> (\<not>A \<and> B) \<or> A \<or> B'\<close> 268 by auto 269 270lemma verit_forall_inst: 271 \<open>A \<longleftrightarrow> B \<Longrightarrow> \<not>A \<or> B\<close> 272 \<open>\<not>A \<longleftrightarrow> B \<Longrightarrow> A \<or> B\<close> 273 \<open>A \<longleftrightarrow> B \<Longrightarrow> \<not>B \<or> A\<close> 274 \<open>A \<longleftrightarrow> \<not>B \<Longrightarrow> B \<or> A\<close> 275 \<open>A \<longrightarrow> B \<Longrightarrow> \<not>A \<or> B\<close> 276 \<open>\<not>A \<longrightarrow> B \<Longrightarrow> A \<or> B\<close> 277 by blast+ 278 279lemma verit_eq_transitive: 280 \<open>A = B \<Longrightarrow> B = C \<Longrightarrow> A = C\<close> 281 \<open>A = B \<Longrightarrow> C = B \<Longrightarrow> A = C\<close> 282 \<open>B = A \<Longrightarrow> B = C \<Longrightarrow> A = C\<close> 283 \<open>B = A \<Longrightarrow> C = B \<Longrightarrow> A = C\<close> 284 by auto 285 286 287subsection \<open>Setup\<close> 288 289ML_file \<open>Tools/SMT/smt_util.ML\<close> 290ML_file \<open>Tools/SMT/smt_failure.ML\<close> 291ML_file \<open>Tools/SMT/smt_config.ML\<close> 292ML_file \<open>Tools/SMT/smt_builtin.ML\<close> 293ML_file \<open>Tools/SMT/smt_datatypes.ML\<close> 294ML_file \<open>Tools/SMT/smt_normalize.ML\<close> 295ML_file \<open>Tools/SMT/smt_translate.ML\<close> 296ML_file \<open>Tools/SMT/smtlib.ML\<close> 297ML_file \<open>Tools/SMT/smtlib_interface.ML\<close> 298ML_file \<open>Tools/SMT/smtlib_proof.ML\<close> 299ML_file \<open>Tools/SMT/smtlib_isar.ML\<close> 300ML_file \<open>Tools/SMT/z3_proof.ML\<close> 301ML_file \<open>Tools/SMT/z3_isar.ML\<close> 302ML_file \<open>Tools/SMT/smt_solver.ML\<close> 303ML_file \<open>Tools/SMT/cvc4_interface.ML\<close> 304ML_file \<open>Tools/SMT/cvc4_proof_parse.ML\<close> 305ML_file \<open>Tools/SMT/verit_proof.ML\<close> 306ML_file \<open>Tools/SMT/verit_isar.ML\<close> 307ML_file \<open>Tools/SMT/verit_proof_parse.ML\<close> 308ML_file \<open>Tools/SMT/conj_disj_perm.ML\<close> 309ML_file \<open>Tools/SMT/smt_replay_methods.ML\<close> 310ML_file \<open>Tools/SMT/smt_replay.ML\<close> 311ML_file \<open>Tools/SMT/z3_interface.ML\<close> 312ML_file \<open>Tools/SMT/z3_replay_rules.ML\<close> 313ML_file \<open>Tools/SMT/z3_replay_methods.ML\<close> 314ML_file \<open>Tools/SMT/z3_replay.ML\<close> 315ML_file \<open>Tools/SMT/verit_replay_methods.ML\<close> 316ML_file \<open>Tools/SMT/verit_replay.ML\<close> 317ML_file \<open>Tools/SMT/smt_systems.ML\<close> 318 319method_setup smt = \<open> 320 Scan.optional Attrib.thms [] >> 321 (fn thms => fn ctxt => 322 METHOD (fn facts => HEADGOAL (SMT_Solver.smt_tac ctxt (thms @ facts)))) 323\<close> "apply an SMT solver to the current goal" 324 325 326subsection \<open>Configuration\<close> 327 328text \<open> 329The current configuration can be printed by the command 330\<open>smt_status\<close>, which shows the values of most options. 331\<close> 332 333 334subsection \<open>General configuration options\<close> 335 336text \<open> 337The option \<open>smt_solver\<close> can be used to change the target SMT 338solver. The possible values can be obtained from the \<open>smt_status\<close> 339command. 340\<close> 341 342declare [[smt_solver = z3]] 343 344text \<open> 345Since SMT solvers are potentially nonterminating, there is a timeout 346(given in seconds) to restrict their runtime. 347\<close> 348 349declare [[smt_timeout = 20]] 350 351text \<open> 352SMT solvers apply randomized heuristics. In case a problem is not 353solvable by an SMT solver, changing the following option might help. 354\<close> 355 356declare [[smt_random_seed = 1]] 357 358text \<open> 359In general, the binding to SMT solvers runs as an oracle, i.e, the SMT 360solvers are fully trusted without additional checks. The following 361option can cause the SMT solver to run in proof-producing mode, giving 362a checkable certificate. This is currently only implemented for Z3. 363\<close> 364 365declare [[smt_oracle = false]] 366 367text \<open> 368Each SMT solver provides several commandline options to tweak its 369behaviour. They can be passed to the solver by setting the following 370options. 371\<close> 372 373declare [[cvc3_options = ""]] 374declare [[cvc4_options = "--full-saturate-quant --inst-when=full-last-call --inst-no-entail --term-db-mode=relevant --multi-trigger-linear"]] 375declare [[verit_options = "--index-fresh-sorts"]] 376declare [[z3_options = ""]] 377 378text \<open> 379The SMT method provides an inference mechanism to detect simple triggers 380in quantified formulas, which might increase the number of problems 381solvable by SMT solvers (note: triggers guide quantifier instantiations 382in the SMT solver). To turn it on, set the following option. 383\<close> 384 385declare [[smt_infer_triggers = false]] 386 387text \<open> 388Enable the following option to use built-in support for datatypes, 389codatatypes, and records in CVC4. Currently, this is implemented only 390in oracle mode. 391\<close> 392 393declare [[cvc4_extensions = false]] 394 395text \<open> 396Enable the following option to use built-in support for div/mod, datatypes, 397and records in Z3. Currently, this is implemented only in oracle mode. 398\<close> 399 400declare [[z3_extensions = false]] 401 402 403subsection \<open>Certificates\<close> 404 405text \<open> 406By setting the option \<open>smt_certificates\<close> to the name of a file, 407all following applications of an SMT solver a cached in that file. 408Any further application of the same SMT solver (using the very same 409configuration) re-uses the cached certificate instead of invoking the 410solver. An empty string disables caching certificates. 411 412The filename should be given as an explicit path. It is good 413practice to use the name of the current theory (with ending 414\<open>.certs\<close> instead of \<open>.thy\<close>) as the certificates file. 415Certificate files should be used at most once in a certain theory context, 416to avoid race conditions with other concurrent accesses. 417\<close> 418 419declare [[smt_certificates = ""]] 420 421text \<open> 422The option \<open>smt_read_only_certificates\<close> controls whether only 423stored certificates are should be used or invocation of an SMT solver 424is allowed. When set to \<open>true\<close>, no SMT solver will ever be 425invoked and only the existing certificates found in the configured 426cache are used; when set to \<open>false\<close> and there is no cached 427certificate for some proposition, then the configured SMT solver is 428invoked. 429\<close> 430 431declare [[smt_read_only_certificates = false]] 432 433 434subsection \<open>Tracing\<close> 435 436text \<open> 437The SMT method, when applied, traces important information. To 438make it entirely silent, set the following option to \<open>false\<close>. 439\<close> 440 441declare [[smt_verbose = true]] 442 443text \<open> 444For tracing the generated problem file given to the SMT solver as 445well as the returned result of the solver, the option 446\<open>smt_trace\<close> should be set to \<open>true\<close>. 447\<close> 448 449declare [[smt_trace = false]] 450 451 452subsection \<open>Schematic rules for Z3 proof reconstruction\<close> 453 454text \<open> 455Several prof rules of Z3 are not very well documented. There are two 456lemma groups which can turn failing Z3 proof reconstruction attempts 457into succeeding ones: the facts in \<open>z3_rule\<close> are tried prior to 458any implemented reconstruction procedure for all uncertain Z3 proof 459rules; the facts in \<open>z3_simp\<close> are only fed to invocations of 460the simplifier when reconstructing theory-specific proof steps. 461\<close> 462 463lemmas [z3_rule] = 464 refl eq_commute conj_commute disj_commute simp_thms nnf_simps 465 ring_distribs field_simps times_divide_eq_right times_divide_eq_left 466 if_True if_False not_not 467 NO_MATCH_def 468 469lemma [z3_rule]: 470 "(P \<and> Q) = (\<not> (\<not> P \<or> \<not> Q))" 471 "(P \<and> Q) = (\<not> (\<not> Q \<or> \<not> P))" 472 "(\<not> P \<and> Q) = (\<not> (P \<or> \<not> Q))" 473 "(\<not> P \<and> Q) = (\<not> (\<not> Q \<or> P))" 474 "(P \<and> \<not> Q) = (\<not> (\<not> P \<or> Q))" 475 "(P \<and> \<not> Q) = (\<not> (Q \<or> \<not> P))" 476 "(\<not> P \<and> \<not> Q) = (\<not> (P \<or> Q))" 477 "(\<not> P \<and> \<not> Q) = (\<not> (Q \<or> P))" 478 by auto 479 480lemma [z3_rule]: 481 "(P \<longrightarrow> Q) = (Q \<or> \<not> P)" 482 "(\<not> P \<longrightarrow> Q) = (P \<or> Q)" 483 "(\<not> P \<longrightarrow> Q) = (Q \<or> P)" 484 "(True \<longrightarrow> P) = P" 485 "(P \<longrightarrow> True) = True" 486 "(False \<longrightarrow> P) = True" 487 "(P \<longrightarrow> P) = True" 488 "(\<not> (A \<longleftrightarrow> \<not> B)) \<longleftrightarrow> (A \<longleftrightarrow> B)" 489 by auto 490 491lemma [z3_rule]: 492 "((P = Q) \<longrightarrow> R) = (R \<or> (Q = (\<not> P)))" 493 by auto 494 495lemma [z3_rule]: 496 "(\<not> True) = False" 497 "(\<not> False) = True" 498 "(x = x) = True" 499 "(P = True) = P" 500 "(True = P) = P" 501 "(P = False) = (\<not> P)" 502 "(False = P) = (\<not> P)" 503 "((\<not> P) = P) = False" 504 "(P = (\<not> P)) = False" 505 "((\<not> P) = (\<not> Q)) = (P = Q)" 506 "\<not> (P = (\<not> Q)) = (P = Q)" 507 "\<not> ((\<not> P) = Q) = (P = Q)" 508 "(P \<noteq> Q) = (Q = (\<not> P))" 509 "(P = Q) = ((\<not> P \<or> Q) \<and> (P \<or> \<not> Q))" 510 "(P \<noteq> Q) = ((\<not> P \<or> \<not> Q) \<and> (P \<or> Q))" 511 by auto 512 513lemma [z3_rule]: 514 "(if P then P else \<not> P) = True" 515 "(if \<not> P then \<not> P else P) = True" 516 "(if P then True else False) = P" 517 "(if P then False else True) = (\<not> P)" 518 "(if P then Q else True) = ((\<not> P) \<or> Q)" 519 "(if P then Q else True) = (Q \<or> (\<not> P))" 520 "(if P then Q else \<not> Q) = (P = Q)" 521 "(if P then Q else \<not> Q) = (Q = P)" 522 "(if P then \<not> Q else Q) = (P = (\<not> Q))" 523 "(if P then \<not> Q else Q) = ((\<not> Q) = P)" 524 "(if \<not> P then x else y) = (if P then y else x)" 525 "(if P then (if Q then x else y) else x) = (if P \<and> (\<not> Q) then y else x)" 526 "(if P then (if Q then x else y) else x) = (if (\<not> Q) \<and> P then y else x)" 527 "(if P then (if Q then x else y) else y) = (if P \<and> Q then x else y)" 528 "(if P then (if Q then x else y) else y) = (if Q \<and> P then x else y)" 529 "(if P then x else if P then y else z) = (if P then x else z)" 530 "(if P then x else if Q then x else y) = (if P \<or> Q then x else y)" 531 "(if P then x else if Q then x else y) = (if Q \<or> P then x else y)" 532 "(if P then x = y else x = z) = (x = (if P then y else z))" 533 "(if P then x = y else y = z) = (y = (if P then x else z))" 534 "(if P then x = y else z = y) = (y = (if P then x else z))" 535 by auto 536 537lemma [z3_rule]: 538 "0 + (x::int) = x" 539 "x + 0 = x" 540 "x + x = 2 * x" 541 "0 * x = 0" 542 "1 * x = x" 543 "x + y = y + x" 544 by (auto simp add: mult_2) 545 546lemma [z3_rule]: (* for def-axiom *) 547 "P = Q \<or> P \<or> Q" 548 "P = Q \<or> \<not> P \<or> \<not> Q" 549 "(\<not> P) = Q \<or> \<not> P \<or> Q" 550 "(\<not> P) = Q \<or> P \<or> \<not> Q" 551 "P = (\<not> Q) \<or> \<not> P \<or> Q" 552 "P = (\<not> Q) \<or> P \<or> \<not> Q" 553 "P \<noteq> Q \<or> P \<or> \<not> Q" 554 "P \<noteq> Q \<or> \<not> P \<or> Q" 555 "P \<noteq> (\<not> Q) \<or> P \<or> Q" 556 "(\<not> P) \<noteq> Q \<or> P \<or> Q" 557 "P \<or> Q \<or> P \<noteq> (\<not> Q)" 558 "P \<or> Q \<or> (\<not> P) \<noteq> Q" 559 "P \<or> \<not> Q \<or> P \<noteq> Q" 560 "\<not> P \<or> Q \<or> P \<noteq> Q" 561 "P \<or> y = (if P then x else y)" 562 "P \<or> (if P then x else y) = y" 563 "\<not> P \<or> x = (if P then x else y)" 564 "\<not> P \<or> (if P then x else y) = x" 565 "P \<or> R \<or> \<not> (if P then Q else R)" 566 "\<not> P \<or> Q \<or> \<not> (if P then Q else R)" 567 "\<not> (if P then Q else R) \<or> \<not> P \<or> Q" 568 "\<not> (if P then Q else R) \<or> P \<or> R" 569 "(if P then Q else R) \<or> \<not> P \<or> \<not> Q" 570 "(if P then Q else R) \<or> P \<or> \<not> R" 571 "(if P then \<not> Q else R) \<or> \<not> P \<or> Q" 572 "(if P then Q else \<not> R) \<or> P \<or> R" 573 by auto 574 575hide_type (open) symb_list pattern 576hide_const (open) Symb_Nil Symb_Cons trigger pat nopat fun_app z3div z3mod 577 578end 579