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