diff --git a/src/HOL/SMT.thy b/src/HOL/SMT.thy
--- a/src/HOL/SMT.thy
+++ b/src/HOL/SMT.thy
@@ -1,893 +1,895 @@
 (*  Title:      HOL/SMT.thy
     Author:     Sascha Boehme, TU Muenchen
     Author:     Jasmin Blanchette, VU Amsterdam
 *)
 
 section \<open>Bindings to Satisfiability Modulo Theories (SMT) solvers based on SMT-LIB 2\<close>
 
 theory SMT
   imports Divides Numeral_Simprocs
   keywords "smt_status" :: diag
 begin
 
 subsection \<open>A skolemization tactic and proof method\<close>
 
 lemma choices:
   "\<And>Q. \<forall>x. \<exists>y ya. Q x y ya \<Longrightarrow> \<exists>f fa. \<forall>x. Q x (f x) (fa x)"
   "\<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)"
   "\<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)"
   "\<And>Q. \<forall>x. \<exists>y ya yb yc yd. Q x y ya yb yc yd \<Longrightarrow>
      \<exists>f fa fb fc fd. \<forall>x. Q x (f x) (fa x) (fb x) (fc x) (fd x)"
   "\<And>Q. \<forall>x. \<exists>y ya yb yc yd ye. Q x y ya yb yc yd ye \<Longrightarrow>
      \<exists>f fa fb fc fd fe. \<forall>x. Q x (f x) (fa x) (fb x) (fc x) (fd x) (fe x)"
   "\<And>Q. \<forall>x. \<exists>y ya yb yc yd ye yf. Q x y ya yb yc yd ye yf \<Longrightarrow>
      \<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)"
   "\<And>Q. \<forall>x. \<exists>y ya yb yc yd ye yf yg. Q x y ya yb yc yd ye yf yg \<Longrightarrow>
      \<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)"
   by metis+
 
 lemma bchoices:
   "\<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)"
   "\<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)"
   "\<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)"
   "\<And>Q. \<forall>x \<in> S. \<exists>y ya yb yc yd. Q x y ya yb yc yd \<Longrightarrow>
     \<exists>f fa fb fc fd. \<forall>x \<in> S. Q x (f x) (fa x) (fb x) (fc x) (fd x)"
   "\<And>Q. \<forall>x \<in> S. \<exists>y ya yb yc yd ye. Q x y ya yb yc yd ye \<Longrightarrow>
     \<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)"
   "\<And>Q. \<forall>x \<in> S. \<exists>y ya yb yc yd ye yf. Q x y ya yb yc yd ye yf \<Longrightarrow>
     \<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)"
   "\<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>
     \<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)"
   by metis+
 
 ML \<open>
 fun moura_tac ctxt =
   Atomize_Elim.atomize_elim_tac ctxt THEN'
   SELECT_GOAL (Clasimp.auto_tac (ctxt addSIs @{thms choice choices bchoice bchoices}) THEN
     ALLGOALS (Metis_Tactic.metis_tac (take 1 ATP_Proof_Reconstruct.partial_type_encs)
         ATP_Proof_Reconstruct.default_metis_lam_trans ctxt [] ORELSE'
       blast_tac ctxt))
 \<close>
 
 method_setup moura = \<open>
   Scan.succeed (SIMPLE_METHOD' o moura_tac)
 \<close> "solve skolemization goals, especially those arising from Z3 proofs"
 
 hide_fact (open) choices bchoices
 
 
 subsection \<open>Triggers for quantifier instantiation\<close>
 
 text \<open>
 Some SMT solvers support patterns as a quantifier instantiation
 heuristics. Patterns may either be positive terms (tagged by "pat")
 triggering quantifier instantiations -- when the solver finds a
 term matching a positive pattern, it instantiates the corresponding
 quantifier accordingly -- or negative terms (tagged by "nopat")
 inhibiting quantifier instantiations. A list of patterns
 of the same kind is called a multipattern, and all patterns in a
 multipattern are considered conjunctively for quantifier instantiation.
 A list of multipatterns is called a trigger, and their multipatterns
 act disjunctively during quantifier instantiation. Each multipattern
 should mention at least all quantified variables of the preceding
 quantifier block.
 \<close>
 
 typedecl 'a symb_list
 
 consts
   Symb_Nil :: "'a symb_list"
   Symb_Cons :: "'a \<Rightarrow> 'a symb_list \<Rightarrow> 'a symb_list"
 
 typedecl pattern
 
 consts
   pat :: "'a \<Rightarrow> pattern"
   nopat :: "'a \<Rightarrow> pattern"
 
 definition trigger :: "pattern symb_list symb_list \<Rightarrow> bool \<Rightarrow> bool" where
   "trigger _ P = P"
 
 
 subsection \<open>Higher-order encoding\<close>
 
 text \<open>
 Application is made explicit for constants occurring with varying
 numbers of arguments. This is achieved by the introduction of the
 following constant.
 \<close>
 
 definition fun_app :: "'a \<Rightarrow> 'a" where "fun_app f = f"
 
 text \<open>
 Some solvers support a theory of arrays which can be used to encode
 higher-order functions. The following set of lemmas specifies the
 properties of such (extensional) arrays.
 \<close>
 
 lemmas array_rules = ext fun_upd_apply fun_upd_same fun_upd_other  fun_upd_upd fun_app_def
 
 
 subsection \<open>Normalization\<close>
 
 lemma case_bool_if[abs_def]: "case_bool x y P = (if P then x else y)"
   by simp
 
 lemmas Ex1_def_raw = Ex1_def[abs_def]
 lemmas Ball_def_raw = Ball_def[abs_def]
 lemmas Bex_def_raw = Bex_def[abs_def]
 lemmas abs_if_raw = abs_if[abs_def]
 lemmas min_def_raw = min_def[abs_def]
 lemmas max_def_raw = max_def[abs_def]
 
 lemma nat_zero_as_int:
   "0 = nat 0"
   by simp
 
 lemma nat_one_as_int:
   "1 = nat 1"
   by simp
 
 lemma nat_numeral_as_int: "numeral = (\<lambda>i. nat (numeral i))" by simp
 lemma nat_less_as_int: "(<) = (\<lambda>a b. int a < int b)" by simp
 lemma nat_leq_as_int: "(\<le>) = (\<lambda>a b. int a \<le> int b)" by simp
 lemma Suc_as_int: "Suc = (\<lambda>a. nat (int a + 1))" by (rule ext) simp
 lemma nat_plus_as_int: "(+) = (\<lambda>a b. nat (int a + int b))" by (rule ext)+ simp
 lemma nat_minus_as_int: "(-) = (\<lambda>a b. nat (int a - int b))" by (rule ext)+ simp
 lemma nat_times_as_int: "(*) = (\<lambda>a b. nat (int a * int b))" by (simp add: nat_mult_distrib)
 lemma nat_div_as_int: "(div) = (\<lambda>a b. nat (int a div int b))" by (simp add: nat_div_distrib)
 lemma nat_mod_as_int: "(mod) = (\<lambda>a b. nat (int a mod int b))" by (simp add: nat_mod_distrib)
 
 lemma int_Suc: "int (Suc n) = int n + 1" by simp
 lemma int_plus: "int (n + m) = int n + int m" by (rule of_nat_add)
 lemma int_minus: "int (n - m) = int (nat (int n - int m))" by auto
 
 lemma nat_int_comparison:
   fixes a b :: nat
   shows "(a = b) = (int a = int b)"
     and "(a < b) = (int a < int b)"
     and "(a \<le> b) = (int a \<le> int b)"
   by simp_all
 
 lemma int_ops:
   fixes a b :: nat
   shows "int 0 = 0"
     and "int 1 = 1"
     and "int (numeral n) = numeral n"
     and "int (Suc a) = int a + 1"
     and "int (a + b) = int a + int b"
     and "int (a - b) = (if int a < int b then 0 else int a - int b)"
     and "int (a * b) = int a * int b"
     and "int (a div b) = int a div int b"
     and "int (a mod b) = int a mod int b"
   by (auto intro: zdiv_int zmod_int)
 
 lemma int_if:
   fixes a b :: nat
   shows "int (if P then a else b) = (if P then int a else int b)"
   by simp
 
 
 subsection \<open>Integer division and modulo for Z3\<close>
 
 text \<open>
 The following Z3-inspired definitions are overspecified for the case where \<open>l = 0\<close>. This
 Schönheitsfehler is corrected in the \<open>div_as_z3div\<close> and \<open>mod_as_z3mod\<close> theorems.
 \<close>
 
 definition z3div :: "int \<Rightarrow> int \<Rightarrow> int" where
   "z3div k l = (if l \<ge> 0 then k div l else - (k div - l))"
 
 definition z3mod :: "int \<Rightarrow> int \<Rightarrow> int" where
   "z3mod k l = k mod (if l \<ge> 0 then l else - l)"
 
 lemma div_as_z3div:
   "\<forall>k l. k div l = (if l = 0 then 0 else if l > 0 then z3div k l else z3div (- k) (- l))"
   by (simp add: z3div_def)
 
 lemma mod_as_z3mod:
   "\<forall>k l. k mod l = (if l = 0 then k else if l > 0 then z3mod k l else - z3mod (- k) (- l))"
   by (simp add: z3mod_def)
 
 
 subsection \<open>Extra theorems for veriT reconstruction\<close>
 
 lemma verit_sko_forall: \<open>(\<forall>x. P x) \<longleftrightarrow> P (SOME x. \<not>P x)\<close>
   using someI[of \<open>\<lambda>x. \<not>P x\<close>]
   by auto
 
 lemma verit_sko_forall': \<open>P (SOME x. \<not>P x) = A \<Longrightarrow> (\<forall>x. P x) = A\<close>
   by (subst verit_sko_forall)
 
 lemma verit_sko_forall'': \<open>B = A \<Longrightarrow> (SOME x. P x) = A \<equiv> (SOME x. P x) = B\<close>
   by auto
 
 lemma verit_sko_forall_indirect: \<open>x = (SOME x. \<not>P x) \<Longrightarrow> (\<forall>x. P x) \<longleftrightarrow> P x\<close>
   using someI[of \<open>\<lambda>x. \<not>P x\<close>]
   by auto
 
 lemma verit_sko_forall_indirect2:
     \<open>x = (SOME x. \<not>P x) \<Longrightarrow> (\<And>x :: 'a. (P x = P' x)) \<Longrightarrow>(\<forall>x. P' x) \<longleftrightarrow> P x\<close>
   using someI[of \<open>\<lambda>x. \<not>P x\<close>]
   by auto
 
 lemma verit_sko_ex: \<open>(\<exists>x. P x) \<longleftrightarrow> P (SOME x. P x)\<close>
   using someI[of \<open>\<lambda>x. P x\<close>]
   by auto
 
 lemma verit_sko_ex': \<open>P (SOME x. P x) = A \<Longrightarrow> (\<exists>x. P x) = A\<close>
   by (subst verit_sko_ex)
 
 lemma verit_sko_ex_indirect: \<open>x = (SOME x. P x) \<Longrightarrow> (\<exists>x. P x) \<longleftrightarrow> P x\<close>
   using someI[of \<open>\<lambda>x. P x\<close>]
   by auto
 
 lemma verit_sko_ex_indirect2: \<open>x = (SOME x. P x) \<Longrightarrow> (\<And>x. P x = P' x) \<Longrightarrow> (\<exists>x. P' x) \<longleftrightarrow> P x\<close>
   using someI[of \<open>\<lambda>x. P x\<close>]
   by auto
 
 lemma verit_Pure_trans:
   \<open>P \<equiv> Q \<Longrightarrow> Q \<Longrightarrow> P\<close>
   by auto
 
 lemma verit_if_cong:
   assumes \<open>b \<equiv> c\<close>
     and \<open>c \<Longrightarrow> x \<equiv> u\<close>
     and \<open>\<not> c \<Longrightarrow> y \<equiv> v\<close>
   shows \<open>(if b then x else y) \<equiv> (if c then u else v)\<close>
   using assms if_cong[of b c x u] by auto
 
 lemma verit_if_weak_cong':
   \<open>b \<equiv> c \<Longrightarrow> (if b then x else y) \<equiv> (if c then x else y)\<close>
   by auto
 
 lemma verit_or_neg:
    \<open>(A \<Longrightarrow> B) \<Longrightarrow> B \<or> \<not>A\<close>
    \<open>(\<not>A \<Longrightarrow> B) \<Longrightarrow> B \<or> A\<close>
   by auto
 
 lemma verit_subst_bool: \<open>P \<Longrightarrow> f True \<Longrightarrow> f P\<close>
   by auto
 
 lemma verit_and_pos:
-  \<open>(a \<Longrightarrow> \<not>b \<or> A) \<Longrightarrow> \<not>(a \<and> b) \<or> A\<close>
+  \<open>(a \<Longrightarrow> \<not>(b \<and> c) \<or> A) \<Longrightarrow> \<not>(a \<and> b \<and> c) \<or> A\<close>
+  \<open>(a \<Longrightarrow> b \<Longrightarrow> A) \<Longrightarrow> \<not>(a \<and> b) \<or> A\<close>
   \<open>(a \<Longrightarrow> A) \<Longrightarrow> \<not>a \<or> A\<close>
   \<open>(\<not>a \<Longrightarrow> A) \<Longrightarrow> a \<or> A\<close>
   by blast+
 
 lemma verit_or_pos:
    \<open>A \<and> A' \<Longrightarrow> (c \<and> A) \<or> (\<not>c \<and> A')\<close>
    \<open>A \<and> A' \<Longrightarrow> (\<not>c \<and> A) \<or> (c \<and> A')\<close>
   by blast+
 
 
 lemma verit_la_generic:
   \<open>(a::int) \<le> x \<or> a = x \<or> a \<ge> x\<close>
   by linarith
 
 lemma verit_bfun_elim:
   \<open>(if b then P True else P False) = P b\<close>
   \<open>(\<forall>b. P' b) = (P' False \<and> P' True)\<close>
   \<open>(\<exists>b. P' b) = (P' False \<or> P' True)\<close>
   by (cases b) (auto simp: all_bool_eq ex_bool_eq)
 
 lemma verit_eq_true_simplify:
   \<open>(P = True) \<equiv> P\<close>
   by auto
 
 lemma verit_and_neg:
-  \<open>B \<or> B' \<Longrightarrow> (A \<and> B) \<or> \<not>A \<or> B'\<close>
-  \<open>B \<or> B' \<Longrightarrow> (\<not>A \<and> B) \<or> A \<or> B'\<close>
-  by auto
+  \<open>(a \<Longrightarrow> \<not>b \<or> A) \<Longrightarrow> \<not>(a \<and> b) \<or> A\<close>
+  \<open>(a \<Longrightarrow> A) \<Longrightarrow> \<not>a \<or> A\<close>
+  \<open>(\<not>a \<Longrightarrow> A) \<Longrightarrow> a \<or> A\<close>
+  by blast+
 
 lemma verit_forall_inst:
   \<open>A \<longleftrightarrow> B \<Longrightarrow> \<not>A \<or> B\<close>
   \<open>\<not>A \<longleftrightarrow> B \<Longrightarrow> A \<or> B\<close>
   \<open>A \<longleftrightarrow> B \<Longrightarrow> \<not>B \<or> A\<close>
   \<open>A \<longleftrightarrow> \<not>B \<Longrightarrow> B \<or> A\<close>
   \<open>A \<longrightarrow> B \<Longrightarrow> \<not>A \<or> B\<close>
   \<open>\<not>A \<longrightarrow> B \<Longrightarrow> A \<or> B\<close>
   by blast+
 
 lemma verit_eq_transitive:
   \<open>A = B \<Longrightarrow> B = C \<Longrightarrow> A = C\<close>
   \<open>A = B \<Longrightarrow> C = B \<Longrightarrow> A = C\<close>
   \<open>B = A \<Longrightarrow> B = C \<Longrightarrow> A = C\<close>
   \<open>B = A \<Longrightarrow> C = B \<Longrightarrow> A = C\<close>
   by auto
 
 lemma verit_bool_simplify:
   \<open>\<not>(P \<longrightarrow> Q) \<longleftrightarrow> P \<and> \<not>Q\<close>
   \<open>\<not>(P \<or> Q) \<longleftrightarrow> \<not>P \<and> \<not>Q\<close>
   \<open>\<not>(P \<and> Q) \<longleftrightarrow> \<not>P \<or> \<not>Q\<close>
   \<open>(P \<longrightarrow> (Q \<longrightarrow> R)) \<longleftrightarrow> ((P \<and> Q) \<longrightarrow> R)\<close>
   \<open>((P \<longrightarrow> Q) \<longrightarrow> Q) \<longleftrightarrow> P \<or> Q\<close>
   \<open>(Q \<longleftrightarrow> (P \<or> Q)) \<longleftrightarrow> (P \<longrightarrow> Q)\<close> \<comment> \<open>This rule was inverted\<close>
   \<open>P \<and> (P \<longrightarrow> Q) \<longleftrightarrow> P \<and> Q\<close>
   \<open>(P \<longrightarrow> Q) \<and> P \<longleftrightarrow> P \<and> Q\<close>
  (* \<comment>\<open>Additional rules:\<close>
   *  \<open>((P \<longrightarrow> Q) \<longrightarrow> P) \<longleftrightarrow> P\<close>
   *  \<open>((P \<longrightarrow> Q) \<longrightarrow> Q) \<longleftrightarrow> P \<or> Q\<close>
   *  \<open>(P \<longrightarrow> Q) \<or> P\<close> *)
   unfolding not_imp imp_conjL
   by auto
 
 text \<open>We need the last equation for \<^term>\<open>\<not>(\<forall>a b. \<not>P a b)\<close>\<close>
 lemma verit_connective_def: \<comment> \<open>the definition of XOR is missing
   as the operator is not generated by Isabelle\<close>
   \<open>(A = B) \<longleftrightarrow> ((A \<longrightarrow> B) \<and> (B \<longrightarrow> A))\<close>
   \<open>(If A B C) = ((A \<longrightarrow> B) \<and> (\<not>A \<longrightarrow> C))\<close>
   \<open>(\<exists>x. P x) \<longleftrightarrow> \<not>(\<forall>x. \<not>P x)\<close>
   \<open>\<not>(\<exists>x. P x) \<longleftrightarrow> (\<forall>x. \<not>P x)\<close>
   by auto
 
 lemma verit_ite_simplify:
   \<open>(If True B C) = B\<close>
   \<open>(If False B C) = C\<close>
   \<open>(If A' B B) = B\<close>
   \<open>(If (\<not>A') B C) = (If A' C B)\<close>
   \<open>(If c (If c A B) C) = (If c A C)\<close>
   \<open>(If c C (If c A B)) = (If c C B)\<close>
   \<open>(If A' True False) = A'\<close>
   \<open>(If A' False True) \<longleftrightarrow> \<not>A'\<close>
   \<open>(If A' True B') \<longleftrightarrow> A'\<or>B'\<close>
   \<open>(If A' B' False) \<longleftrightarrow> A'\<and>B'\<close>
   \<open>(If A' False B') \<longleftrightarrow> \<not>A'\<and>B'\<close>
   \<open>(If A' B' True) \<longleftrightarrow> \<not>A'\<or>B'\<close>
   \<open>x \<and> True \<longleftrightarrow> x\<close>
   \<open>x \<or> False \<longleftrightarrow> x\<close>
   for B C :: 'a and A' B' C' :: bool
   by auto
 
 lemma verit_and_simplify1:
   \<open>True \<and> b \<longleftrightarrow> b\<close> \<open>b \<and> True \<longleftrightarrow> b\<close>
   \<open>False \<and> b \<longleftrightarrow> False\<close> \<open>b \<and> False \<longleftrightarrow> False\<close>
   \<open>(c \<and> \<not>c) \<longleftrightarrow> False\<close> \<open>(\<not>c \<and> c) \<longleftrightarrow> False\<close>
   \<open>\<not>\<not>a = a\<close>
   by auto
 
 lemmas verit_and_simplify = conj_ac de_Morgan_conj disj_not1
 
 
 lemma verit_or_simplify_1:
   \<open>False \<or> b \<longleftrightarrow> b\<close> \<open>b \<or> False \<longleftrightarrow> b\<close>
   \<open>b \<or> \<not>b\<close>
   \<open>\<not>b \<or> b\<close>
   by auto
 
 lemmas verit_or_simplify = disj_ac
 
 lemma verit_not_simplify:
   \<open>\<not> \<not>b \<longleftrightarrow> b\<close> \<open>\<not>True \<longleftrightarrow> False\<close> \<open>\<not>False \<longleftrightarrow> True\<close>
   by auto
 
 
 lemma verit_implies_simplify:
   \<open>(\<not>a \<longrightarrow> \<not>b) \<longleftrightarrow> (b \<longrightarrow> a)\<close>
   \<open>(False \<longrightarrow> a) \<longleftrightarrow> True\<close>
   \<open>(a \<longrightarrow> True) \<longleftrightarrow> True\<close>
   \<open>(True \<longrightarrow> a) \<longleftrightarrow> a\<close>
   \<open>(a \<longrightarrow> False) \<longleftrightarrow> \<not>a\<close>
   \<open>(a \<longrightarrow> a) \<longleftrightarrow> True\<close>
   \<open>(\<not>a \<longrightarrow> a) \<longleftrightarrow> a\<close>
   \<open>(a \<longrightarrow> \<not>a) \<longleftrightarrow> \<not>a\<close>
   \<open>((a \<longrightarrow> b) \<longrightarrow> b) \<longleftrightarrow> a \<or> b\<close>
   by auto
 
 lemma verit_equiv_simplify:
   \<open>((\<not>a) = (\<not>b)) \<longleftrightarrow> (a = b)\<close>
   \<open>(a = a) \<longleftrightarrow> True\<close>
   \<open>(a = (\<not>a)) \<longleftrightarrow> False\<close>
   \<open>((\<not>a) = a) \<longleftrightarrow> False\<close>
   \<open>(True = a) \<longleftrightarrow> a\<close>
   \<open>(a = True) \<longleftrightarrow> a\<close>
   \<open>(False = a) \<longleftrightarrow> \<not>a\<close>
   \<open>(a = False) \<longleftrightarrow> \<not>a\<close>
   \<open>\<not>\<not>a \<longleftrightarrow> a\<close>
   \<open>(\<not> False) = True\<close>
   for a b :: bool
   by auto
 
 lemmas verit_eq_simplify =
   semiring_char_0_class.eq_numeral_simps eq_refl zero_neq_one num.simps
   neg_equal_zero equal_neg_zero one_neq_zero neg_equal_iff_equal
 
 lemma verit_minus_simplify:
   \<open>(a :: 'a :: cancel_comm_monoid_add) - a = 0\<close>
   \<open>(a :: 'a :: cancel_comm_monoid_add) - 0 = a\<close>
   \<open>0 - (b :: 'b :: {group_add}) = -b\<close>
   \<open>- (- (b :: 'b :: group_add)) = b\<close>
   by auto
 
 lemma verit_sum_simplify:
   \<open>(a :: 'a :: cancel_comm_monoid_add) + 0 = a\<close>
   by auto
 
 lemmas verit_prod_simplify =
 (* already included:
    mult_zero_class.mult_zero_right
    mult_zero_class.mult_zero_left *)
    mult_1
    mult_1_right
 
 lemma verit_comp_simplify1:
   \<open>(a :: 'a ::order) < a \<longleftrightarrow> False\<close>
   \<open>a \<le> a\<close>
   \<open>\<not>(b' \<le> a') \<longleftrightarrow> (a' :: 'b :: linorder) < b'\<close>
   by auto
 
 lemmas verit_comp_simplify =
   verit_comp_simplify1
   le_numeral_simps
   le_num_simps
   less_numeral_simps
   less_num_simps
   zero_less_one
   zero_le_one
   less_neg_numeral_simps
 
 lemma verit_la_disequality:
   \<open>(a :: 'a ::linorder) = b \<or> \<not>a \<le> b \<or> \<not>b \<le> a\<close>
   by auto
 
 context
 begin
 
 text \<open>For the reconstruction, we need to keep the order of the arguments.\<close>
 
 named_theorems smt_arith_multiplication \<open>Theorems to reconstruct arithmetic theorems.\<close>
 
 named_theorems smt_arith_combine \<open>Theorems to reconstruct arithmetic theorems.\<close>
 
 named_theorems smt_arith_simplify \<open>Theorems to combine theorems in the LA procedure\<close>
 
 lemmas [smt_arith_simplify] =
     div_add dvd_numeral_simp divmod_steps less_num_simps le_num_simps if_True if_False divmod_cancel
     dvd_mult dvd_mult2 less_irrefl prod.case numeral_plus_one divmod_step_eq order.refl le_zero_eq
     le_numeral_simps less_numeral_simps mult.right_neutral simp_thms divides_aux_eq
     mult_nonneg_nonneg dvd_imp_mod_0 dvd_add zero_less_one mod_mult_self4 numeral_mod_numeral
     divmod_trivial prod.sel mult.left_neutral div_pos_pos_trivial arith_simps div_add div_mult_self1
     add_le_cancel_left add_le_same_cancel2 not_one_le_zero le_numeral_simps add_le_same_cancel1
     zero_neq_one zero_le_one le_num_simps add_Suc mod_div_trivial nat.distinct mult_minus_right
     add.inverse_inverse distrib_left_numeral mult_num_simps numeral_times_numeral add_num_simps
     divmod_steps rel_simps if_True if_False numeral_div_numeral divmod_cancel prod.case
     add_num_simps one_plus_numeral fst_conv divmod_step_eq arith_simps sub_num_simps dbl_inc_simps
     dbl_simps mult_1 add_le_cancel_right left_diff_distrib_numeral add_uminus_conv_diff zero_neq_one
     zero_le_one One_nat_def add_Suc mod_div_trivial nat.distinct of_int_1 numerals numeral_One
     of_int_numeral add_uminus_conv_diff zle_diff1_eq add_less_same_cancel2 minus_add_distrib
     add_uminus_conv_diff mult.left_neutral semiring_class.distrib_right
     add_diff_cancel_left' add_diff_eq ring_distribs mult_minus_left minus_diff_eq
 
 lemma [smt_arith_simplify]:
   \<open>\<not> (a' :: 'a :: linorder) < b' \<longleftrightarrow> b' \<le> a'\<close>
   \<open>\<not> (a' :: 'a :: linorder) \<le> b' \<longleftrightarrow> b' < a'\<close>
   \<open>(c::int) mod Numeral1 = 0\<close>
   \<open>(a::nat) mod Numeral1 = 0\<close>
   \<open>(c::int) div Numeral1 = c\<close>
   \<open>a div Numeral1 = a\<close>
   \<open>(c::int) mod 1 = 0\<close>
   \<open>a mod 1 = 0\<close>
   \<open>(c::int) div 1 = c\<close>
   \<open>a div 1 = a\<close>
   \<open>\<not>(a' \<noteq> b') \<longleftrightarrow> a' = b'\<close>
   by auto
 
 
 lemma div_mod_decomp: "A = (A div n) * n + (A mod n)" for A :: nat
   by auto
 
 lemma div_less_mono:
   fixes A B :: nat
   assumes "A < B" "0 < n" and
     mod: "A mod n = 0""B mod n = 0"
   shows "(A div n) < (B div n)"
 proof -
   show ?thesis
     using assms(1)
     apply (subst (asm) div_mod_decomp[of "A" n])
     apply (subst (asm) div_mod_decomp[of "B" n])
     unfolding mod
     by (use assms(2,3) in \<open>auto simp: ac_simps\<close>)
 qed
 
 lemma verit_le_mono_div:
   fixes A B :: nat
   assumes "A < B" "0 < n"
   shows "(A div n) + (if B mod n = 0 then 1 else 0) \<le> (B div n)"
   by (auto simp: ac_simps Suc_leI assms less_mult_imp_div_less div_le_mono less_imp_le_nat)
 
 lemmas [smt_arith_multiplication] =
   verit_le_mono_div[THEN mult_le_mono1, unfolded add_mult_distrib]
   div_le_mono[THEN mult_le_mono2, unfolded add_mult_distrib]
 
 lemma div_mod_decomp_int: "A = (A div n) * n + (A mod n)" for A :: int
   by auto
 
 lemma zdiv_mono_strict:
   fixes A B :: int
   assumes "A < B" "0 < n" and
     mod: "A mod n = 0""B mod n = 0"
   shows "(A div n) < (B div n)"
 proof -
   show ?thesis
     using assms(1)
     apply (subst (asm) div_mod_decomp_int[of A n])
     apply (subst (asm) div_mod_decomp_int[of B n])
     unfolding mod
     by (use assms(2,3) in \<open>auto simp: ac_simps\<close>)
 qed
 
 lemma verit_le_mono_div_int:
   fixes A B :: int
   assumes "A < B" "0 < n"
   shows "(A div n) + (if B mod n = 0 then 1 else 0) \<le> (B div n)"
 proof -
   have f2: "B div n = A div n \<or> A div n < B div n"
     by (metis (no_types) assms less_le zdiv_mono1)
   have "B div n \<noteq> A div n \<or> B mod n \<noteq> 0"
     using assms(1) by (metis Groups.add_ac(2) assms(2) eucl_rel_int eucl_rel_int_iff
       group_cancel.rule0 le_add_same_cancel2 not_le)
   then have "B mod n = 0 \<longrightarrow> A div n + (if B mod n = 0 then 1 else 0) \<le> B div n"
     using f2 by (auto dest: zless_imp_add1_zle)
   then show ?thesis
     using assms zdiv_mono1 by auto
 qed
 
 
 lemma verit_less_mono_div_int2:
   fixes A B :: int
   assumes "A \<le> B" "0 < -n"
   shows "(A div n) \<ge> (B div n)"
   using assms(1) assms(2) zdiv_mono1_neg by auto
 
 lemmas [smt_arith_multiplication] =
   verit_le_mono_div_int[THEN mult_left_mono, unfolded int_distrib]
   zdiv_mono1[THEN mult_left_mono, unfolded int_distrib]
 
 lemmas [smt_arith_multiplication] =
   arg_cong[of _ _ \<open>\<lambda>a :: nat. a div n * p\<close> for n p :: nat, THEN sym]
   arg_cong[of _ _ \<open>\<lambda>a :: int. a div n * p\<close> for n p :: int, THEN sym]
 
 lemma [smt_arith_combine]:
   "a < b \<Longrightarrow> c < d \<Longrightarrow> a + c + 2 \<le> b + d"
   "a < b \<Longrightarrow> c \<le> d \<Longrightarrow> a + c + 1 \<le> b + d"
   "a \<le> b \<Longrightarrow> c < d \<Longrightarrow> a + c + 1 \<le> b + d" for a b c :: int
   by auto
 
 lemma [smt_arith_combine]:
   "a < b \<Longrightarrow> c < d \<Longrightarrow> a + c + 2 \<le> b + d"
   "a < b \<Longrightarrow> c \<le> d \<Longrightarrow> a + c + 1 \<le> b + d"
   "a \<le> b \<Longrightarrow> c < d \<Longrightarrow> a + c + 1 \<le> b + d" for a b c :: nat
   by auto
 
 lemmas [smt_arith_combine] =
   add_strict_mono
   add_less_le_mono
   add_mono
   add_le_less_mono
 
 lemma [smt_arith_combine]:
   \<open>m < n \<Longrightarrow> c = d \<Longrightarrow> m + c < n + d\<close>
   \<open>m \<le> n \<Longrightarrow> c = d \<Longrightarrow> m + c \<le> n + d\<close>
   \<open>c = d \<Longrightarrow> m < n \<Longrightarrow> m + c < n + d\<close>
   \<open>c = d \<Longrightarrow> m \<le> n \<Longrightarrow> m + c \<le> n + d\<close>
   for m :: \<open>'a :: ordered_cancel_ab_semigroup_add\<close>
   by (auto intro: ordered_cancel_ab_semigroup_add_class.add_strict_right_mono
     ordered_ab_semigroup_add_class.add_right_mono)
 
 lemma verit_negate_coefficient:
   \<open>a \<le> (b :: 'a :: {ordered_ab_group_add}) \<Longrightarrow> -a \<ge> -b\<close>
   \<open>a < b \<Longrightarrow> -a > -b\<close>
   \<open>a = b \<Longrightarrow> -a = -b\<close>
   by auto
 
 end
 
 lemma verit_ite_intro:
   \<open>(if a then P (if a then a' else b') else Q) \<longleftrightarrow> (if a then P a' else Q)\<close>
   \<open>(if a then P' else Q' (if a then a' else b')) \<longleftrightarrow> (if a then P' else Q' b')\<close>
   \<open>A = f (if a then R else S) \<longleftrightarrow> (if a then A = f R else A = f S)\<close>
   by auto
 
 lemma verit_ite_if_cong:
   fixes x y :: bool
   assumes "b=c"
     and "c \<equiv> True \<Longrightarrow> x = u"
     and "c \<equiv> False \<Longrightarrow> y = v"
   shows "(if b then x else y) \<equiv> (if c then u else v)"
 proof -
   have H: "(if b then x else y) = (if c then u else v)"
     using assms by (auto split: if_splits)
 
   show "(if b then x else y) \<equiv> (if c then u else v)"
     by (subst H) auto
 qed
 
 
 subsection \<open>Setup\<close>
 
 ML_file \<open>Tools/SMT/smt_util.ML\<close>
 ML_file \<open>Tools/SMT/smt_failure.ML\<close>
 ML_file \<open>Tools/SMT/smt_config.ML\<close>
 ML_file \<open>Tools/SMT/smt_builtin.ML\<close>
 ML_file \<open>Tools/SMT/smt_datatypes.ML\<close>
 ML_file \<open>Tools/SMT/smt_normalize.ML\<close>
 ML_file \<open>Tools/SMT/smt_translate.ML\<close>
 ML_file \<open>Tools/SMT/smtlib.ML\<close>
 ML_file \<open>Tools/SMT/smtlib_interface.ML\<close>
 ML_file \<open>Tools/SMT/smtlib_proof.ML\<close>
 ML_file \<open>Tools/SMT/smtlib_isar.ML\<close>
 ML_file \<open>Tools/SMT/z3_proof.ML\<close>
 ML_file \<open>Tools/SMT/z3_isar.ML\<close>
 ML_file \<open>Tools/SMT/smt_solver.ML\<close>
 ML_file \<open>Tools/SMT/cvc4_interface.ML\<close>
 ML_file \<open>Tools/SMT/cvc4_proof_parse.ML\<close>
 ML_file \<open>Tools/SMT/verit_proof.ML\<close>
 ML_file \<open>Tools/SMT/verit_isar.ML\<close>
 ML_file \<open>Tools/SMT/verit_proof_parse.ML\<close>
 ML_file \<open>Tools/SMT/conj_disj_perm.ML\<close>
 ML_file \<open>Tools/SMT/smt_replay_methods.ML\<close>
 ML_file \<open>Tools/SMT/smt_replay.ML\<close>
 ML_file \<open>Tools/SMT/smt_replay_arith.ML\<close>
 ML_file \<open>Tools/SMT/z3_interface.ML\<close>
 ML_file \<open>Tools/SMT/z3_replay_rules.ML\<close>
 ML_file \<open>Tools/SMT/z3_replay_methods.ML\<close>
 ML_file \<open>Tools/SMT/z3_replay.ML\<close>
 ML_file \<open>Tools/SMT/verit_replay_methods.ML\<close>
 ML_file \<open>Tools/SMT/verit_replay.ML\<close>
 ML_file \<open>Tools/SMT/smt_systems.ML\<close>
 
 
 subsection \<open>Configuration\<close>
 
 text \<open>
 The current configuration can be printed by the command
 \<open>smt_status\<close>, which shows the values of most options.
 \<close>
 
 
 subsection \<open>General configuration options\<close>
 
 text \<open>
 The option \<open>smt_solver\<close> can be used to change the target SMT
 solver. The possible values can be obtained from the \<open>smt_status\<close>
 command.
 \<close>
 
 declare [[smt_solver = z3]]
 
 text \<open>
 Since SMT solvers are potentially nonterminating, there is a timeout
 (given in seconds) to restrict their runtime.
 \<close>
 
 declare [[smt_timeout = 1000000]]
 
 text \<open>
 SMT solvers apply randomized heuristics. In case a problem is not
 solvable by an SMT solver, changing the following option might help.
 \<close>
 
 declare [[smt_random_seed = 1]]
 
 text \<open>
 In general, the binding to SMT solvers runs as an oracle, i.e, the SMT
 solvers are fully trusted without additional checks. The following
 option can cause the SMT solver to run in proof-producing mode, giving
 a checkable certificate. This is currently only implemented for Z3.
 \<close>
 
 declare [[smt_oracle = false]]
 
 text \<open>
 Each SMT solver provides several commandline options to tweak its
 behaviour. They can be passed to the solver by setting the following
 options.
 \<close>
 
 declare [[cvc3_options = ""]]
 declare [[cvc4_options = "--full-saturate-quant --inst-when=full-last-call --inst-no-entail --term-db-mode=relevant --multi-trigger-linear"]]
 declare [[verit_options = ""]]
 declare [[z3_options = ""]]
 
 text \<open>
 The SMT method provides an inference mechanism to detect simple triggers
 in quantified formulas, which might increase the number of problems
 solvable by SMT solvers (note: triggers guide quantifier instantiations
 in the SMT solver). To turn it on, set the following option.
 \<close>
 
 declare [[smt_infer_triggers = false]]
 
 text \<open>
 Enable the following option to use built-in support for datatypes,
 codatatypes, and records in CVC4. Currently, this is implemented only
 in oracle mode.
 \<close>
 
 declare [[cvc4_extensions = false]]
 
 text \<open>
 Enable the following option to use built-in support for div/mod, datatypes,
 and records in Z3. Currently, this is implemented only in oracle mode.
 \<close>
 
 declare [[z3_extensions = false]]
 
 
 subsection \<open>Certificates\<close>
 
 text \<open>
 By setting the option \<open>smt_certificates\<close> to the name of a file,
 all following applications of an SMT solver a cached in that file.
 Any further application of the same SMT solver (using the very same
 configuration) re-uses the cached certificate instead of invoking the
 solver. An empty string disables caching certificates.
 
 The filename should be given as an explicit path. It is good
 practice to use the name of the current theory (with ending
 \<open>.certs\<close> instead of \<open>.thy\<close>) as the certificates file.
 Certificate files should be used at most once in a certain theory context,
 to avoid race conditions with other concurrent accesses.
 \<close>
 
 declare [[smt_certificates = ""]]
 
 text \<open>
 The option \<open>smt_read_only_certificates\<close> controls whether only
 stored certificates are should be used or invocation of an SMT solver
 is allowed. When set to \<open>true\<close>, no SMT solver will ever be
 invoked and only the existing certificates found in the configured
 cache are used;  when set to \<open>false\<close> and there is no cached
 certificate for some proposition, then the configured SMT solver is
 invoked.
 \<close>
 
 declare [[smt_read_only_certificates = false]]
 
 
 subsection \<open>Tracing\<close>
 
 text \<open>
 The SMT method, when applied, traces important information. To
 make it entirely silent, set the following option to \<open>false\<close>.
 \<close>
 
 declare [[smt_verbose = true]]
 
 text \<open>
 For tracing the generated problem file given to the SMT solver as
 well as the returned result of the solver, the option
 \<open>smt_trace\<close> should be set to \<open>true\<close>.
 \<close>
 
 declare [[smt_trace = false]]
 
 
 subsection \<open>Schematic rules for Z3 proof reconstruction\<close>
 
 text \<open>
 Several prof rules of Z3 are not very well documented. There are two
 lemma groups which can turn failing Z3 proof reconstruction attempts
 into succeeding ones: the facts in \<open>z3_rule\<close> are tried prior to
 any implemented reconstruction procedure for all uncertain Z3 proof
 rules;  the facts in \<open>z3_simp\<close> are only fed to invocations of
 the simplifier when reconstructing theory-specific proof steps.
 \<close>
 
 lemmas [z3_rule] =
   refl eq_commute conj_commute disj_commute simp_thms nnf_simps
   ring_distribs field_simps times_divide_eq_right times_divide_eq_left
   if_True if_False not_not
   NO_MATCH_def
 
 lemma [z3_rule]:
   "(P \<and> Q) = (\<not> (\<not> P \<or> \<not> Q))"
   "(P \<and> Q) = (\<not> (\<not> Q \<or> \<not> P))"
   "(\<not> P \<and> Q) = (\<not> (P \<or> \<not> Q))"
   "(\<not> P \<and> Q) = (\<not> (\<not> Q \<or> P))"
   "(P \<and> \<not> Q) = (\<not> (\<not> P \<or> Q))"
   "(P \<and> \<not> Q) = (\<not> (Q \<or> \<not> P))"
   "(\<not> P \<and> \<not> Q) = (\<not> (P \<or> Q))"
   "(\<not> P \<and> \<not> Q) = (\<not> (Q \<or> P))"
   by auto
 
 lemma [z3_rule]:
   "(P \<longrightarrow> Q) = (Q \<or> \<not> P)"
   "(\<not> P \<longrightarrow> Q) = (P \<or> Q)"
   "(\<not> P \<longrightarrow> Q) = (Q \<or> P)"
   "(True \<longrightarrow> P) = P"
   "(P \<longrightarrow> True) = True"
   "(False \<longrightarrow> P) = True"
   "(P \<longrightarrow> P) = True"
   "(\<not> (A \<longleftrightarrow> \<not> B)) \<longleftrightarrow> (A \<longleftrightarrow> B)"
   by auto
 
 lemma [z3_rule]:
   "((P = Q) \<longrightarrow> R) = (R \<or> (Q = (\<not> P)))"
   by auto
 
 lemma [z3_rule]:
   "(\<not> True) = False"
   "(\<not> False) = True"
   "(x = x) = True"
   "(P = True) = P"
   "(True = P) = P"
   "(P = False) = (\<not> P)"
   "(False = P) = (\<not> P)"
   "((\<not> P) = P) = False"
   "(P = (\<not> P)) = False"
   "((\<not> P) = (\<not> Q)) = (P = Q)"
   "\<not> (P = (\<not> Q)) = (P = Q)"
   "\<not> ((\<not> P) = Q) = (P = Q)"
   "(P \<noteq> Q) = (Q = (\<not> P))"
   "(P = Q) = ((\<not> P \<or> Q) \<and> (P \<or> \<not> Q))"
   "(P \<noteq> Q) = ((\<not> P \<or> \<not> Q) \<and> (P \<or> Q))"
   by auto
 
 lemma [z3_rule]:
   "(if P then P else \<not> P) = True"
   "(if \<not> P then \<not> P else P) = True"
   "(if P then True else False) = P"
   "(if P then False else True) = (\<not> P)"
   "(if P then Q else True) = ((\<not> P) \<or> Q)"
   "(if P then Q else True) = (Q \<or> (\<not> P))"
   "(if P then Q else \<not> Q) = (P = Q)"
   "(if P then Q else \<not> Q) = (Q = P)"
   "(if P then \<not> Q else Q) = (P = (\<not> Q))"
   "(if P then \<not> Q else Q) = ((\<not> Q) = P)"
   "(if \<not> P then x else y) = (if P then y else x)"
   "(if P then (if Q then x else y) else x) = (if P \<and> (\<not> Q) then y else x)"
   "(if P then (if Q then x else y) else x) = (if (\<not> Q) \<and> P then y else x)"
   "(if P then (if Q then x else y) else y) = (if P \<and> Q then x else y)"
   "(if P then (if Q then x else y) else y) = (if Q \<and> P then x else y)"
   "(if P then x else if P then y else z) = (if P then x else z)"
   "(if P then x else if Q then x else y) = (if P \<or> Q then x else y)"
   "(if P then x else if Q then x else y) = (if Q \<or> P then x else y)"
   "(if P then x = y else x = z) = (x = (if P then y else z))"
   "(if P then x = y else y = z) = (y = (if P then x else z))"
   "(if P then x = y else z = y) = (y = (if P then x else z))"
   by auto
 
 lemma [z3_rule]:
   "0 + (x::int) = x"
   "x + 0 = x"
   "x + x = 2 * x"
   "0 * x = 0"
   "1 * x = x"
   "x + y = y + x"
   by auto
 
 lemma [z3_rule]:  (* for def-axiom *)
   "P = Q \<or> P \<or> Q"
   "P = Q \<or> \<not> P \<or> \<not> Q"
   "(\<not> P) = Q \<or> \<not> P \<or> Q"
   "(\<not> P) = Q \<or> P \<or> \<not> Q"
   "P = (\<not> Q) \<or> \<not> P \<or> Q"
   "P = (\<not> Q) \<or> P \<or> \<not> Q"
   "P \<noteq> Q \<or> P \<or> \<not> Q"
   "P \<noteq> Q \<or> \<not> P \<or> Q"
   "P \<noteq> (\<not> Q) \<or> P \<or> Q"
   "(\<not> P) \<noteq> Q \<or> P \<or> Q"
   "P \<or> Q \<or> P \<noteq> (\<not> Q)"
   "P \<or> Q \<or> (\<not> P) \<noteq> Q"
   "P \<or> \<not> Q \<or> P \<noteq> Q"
   "\<not> P \<or> Q \<or> P \<noteq> Q"
   "P \<or> y = (if P then x else y)"
   "P \<or> (if P then x else y) = y"
   "\<not> P \<or> x = (if P then x else y)"
   "\<not> P \<or> (if P then x else y) = x"
   "P \<or> R \<or> \<not> (if P then Q else R)"
   "\<not> P \<or> Q \<or> \<not> (if P then Q else R)"
   "\<not> (if P then Q else R) \<or> \<not> P \<or> Q"
   "\<not> (if P then Q else R) \<or> P \<or> R"
   "(if P then Q else R) \<or> \<not> P \<or> \<not> Q"
   "(if P then Q else R) \<or> P \<or> \<not> R"
   "(if P then \<not> Q else R) \<or> \<not> P \<or> Q"
   "(if P then Q else \<not> R) \<or> P \<or> R"
   by auto
 
 hide_type (open) symb_list pattern
 hide_const (open) Symb_Nil Symb_Cons trigger pat nopat fun_app z3div z3mod
 
 end
diff --git a/src/HOL/SMT_Examples/SMT_Tests_Verit.thy b/src/HOL/SMT_Examples/SMT_Tests_Verit.thy
--- a/src/HOL/SMT_Examples/SMT_Tests_Verit.thy
+++ b/src/HOL/SMT_Examples/SMT_Tests_Verit.thy
@@ -1,717 +1,720 @@
 (*  Title:      HOL/SMT_Examples/SMT_Tests.thy
     Author:     Sascha Boehme, TU Muenchen
     Author:     Mathias Fleury, MPII, JKU
 *)
 
 section \<open>Tests for the SMT binding\<close>
 
 theory SMT_Tests_Verit
 imports Complex_Main
 begin
 
 declare [[smt_solver=verit]]
 smt_status
 
 text \<open>Most examples are taken from the equivalent Z3 theory called \<^file>\<open>SMT_Tests.thy\<close>,
 and have been taken from various Isabelle and HOL4 developments.\<close>
 
 
 section \<open>Propositional logic\<close>
 
 lemma
   "True"
   "\<not> False"
   "\<not> \<not> True"
   "True \<and> True"
   "True \<or> False"
   "False \<longrightarrow> True"
   "\<not> (False \<longleftrightarrow> True)"
   by smt+
 
 lemma
   "P \<or> \<not> P"
   "\<not> (P \<and> \<not> P)"
   "(True \<and> P) \<or> \<not> P \<or> (False \<and> P) \<or> P"
   "P \<longrightarrow> P"
   "P \<and> \<not> P \<longrightarrow> False"
   "P \<and> Q \<longrightarrow> Q \<and> P"
   "P \<or> Q \<longrightarrow> Q \<or> P"
   "P \<and> Q \<longrightarrow> P \<or> Q"
   "\<not> (P \<or> Q) \<longrightarrow> \<not> P"
   "\<not> (P \<or> Q) \<longrightarrow> \<not> Q"
   "\<not> P \<longrightarrow> \<not> (P \<and> Q)"
   "\<not> Q \<longrightarrow> \<not> (P \<and> Q)"
   "(P \<and> Q) \<longleftrightarrow> (\<not> (\<not> P \<or> \<not> Q))"
   "(P \<and> Q) \<and> R \<longrightarrow> P \<and> (Q \<and> R)"
   "(P \<or> Q) \<or> R \<longrightarrow> P \<or> (Q \<or> R)"
   "(P \<and> Q) \<or> R  \<longrightarrow> (P \<or> R) \<and> (Q \<or> R)"
   "(P \<or> R) \<and> (Q \<or> R) \<longrightarrow> (P \<and> Q) \<or> R"
   "(P \<or> Q) \<and> R \<longrightarrow> (P \<and> R) \<or> (Q \<and> R)"
   "(P \<and> R) \<or> (Q \<and> R) \<longrightarrow> (P \<or> Q) \<and> R"
   "((P \<longrightarrow> Q) \<longrightarrow> P) \<longrightarrow> P"
   "(P \<longrightarrow> R) \<and> (Q \<longrightarrow> R) \<longleftrightarrow> (P \<or> Q \<longrightarrow> R)"
   "(P \<and> Q \<longrightarrow> R) \<longleftrightarrow> (P \<longrightarrow> (Q \<longrightarrow> R))"
   "((P \<longrightarrow> R) \<longrightarrow> R) \<longrightarrow>  ((Q \<longrightarrow> R) \<longrightarrow> R) \<longrightarrow> (P \<and> Q \<longrightarrow> R) \<longrightarrow> R"
   "\<not> (P \<longrightarrow> R) \<longrightarrow>  \<not> (Q \<longrightarrow> R) \<longrightarrow> \<not> (P \<and> Q \<longrightarrow> R)"
   "(P \<longrightarrow> Q \<and> R) \<longleftrightarrow> (P \<longrightarrow> Q) \<and> (P \<longrightarrow> R)"
   "P \<longrightarrow> (Q \<longrightarrow> P)"
   "(P \<longrightarrow> Q \<longrightarrow> R) \<longrightarrow> (P \<longrightarrow> Q)\<longrightarrow> (P \<longrightarrow> R)"
   "(P \<longrightarrow> Q) \<or> (P \<longrightarrow> R) \<longrightarrow> (P \<longrightarrow> Q \<or> R)"
   "((((P \<longrightarrow> Q) \<longrightarrow> P) \<longrightarrow> P) \<longrightarrow> Q) \<longrightarrow> Q"
   "(P \<longrightarrow> Q) \<longrightarrow> (\<not> Q \<longrightarrow> \<not> P)"
   "(P \<longrightarrow> Q \<or> R) \<longrightarrow> (P \<longrightarrow> Q) \<or> (P \<longrightarrow> R)"
   "(P \<longrightarrow> Q) \<and> (Q  \<longrightarrow> P) \<longrightarrow> (P \<longleftrightarrow> Q)"
   "(P \<longleftrightarrow> Q) \<longleftrightarrow> (Q \<longleftrightarrow> P)"
   "\<not> (P \<longleftrightarrow> \<not> P)"
   "(P \<longrightarrow> Q) \<longleftrightarrow> (\<not> Q \<longrightarrow> \<not> P)"
   "P \<longleftrightarrow> P \<longleftrightarrow> P \<longleftrightarrow> P \<longleftrightarrow> P \<longleftrightarrow> P \<longleftrightarrow> P \<longleftrightarrow> P \<longleftrightarrow> P \<longleftrightarrow> P"
   by smt+
 
 lemma
   "(if P then Q1 else Q2) \<longleftrightarrow> ((P \<longrightarrow> Q1) \<and> (\<not> P \<longrightarrow> Q2))"
   "if P then (Q \<longrightarrow> P) else (P \<longrightarrow> Q)"
   "(if P1 \<or> P2 then Q1 else Q2) \<longleftrightarrow> (if P1 then Q1 else if P2 then Q1 else Q2)"
   "(if P1 \<and> P2 then Q1 else Q2) \<longleftrightarrow> (if P1 then if P2 then Q1 else Q2 else Q2)"
   "(P1 \<longrightarrow> (if P2 then Q1 else Q2)) \<longleftrightarrow>
    (if P1 \<longrightarrow> P2 then P1 \<longrightarrow> Q1 else P1 \<longrightarrow> Q2)"
   by smt+
 
 lemma
   "case P of True \<Rightarrow> P | False \<Rightarrow> \<not> P"
   "case P of False \<Rightarrow> \<not> P | True \<Rightarrow> P"
   "case \<not> P of True \<Rightarrow> \<not> P | False \<Rightarrow> P"
   "case P of True \<Rightarrow> (Q \<longrightarrow> P) | False \<Rightarrow> (P \<longrightarrow> Q)"
   by smt+
 
 
 section \<open>First-order logic with equality\<close>
 
 lemma
   "x = x"
   "x = y \<longrightarrow> y = x"
   "x = y \<and> y = z \<longrightarrow> x = z"
   "x = y \<longrightarrow> f x = f y"
   "x = y \<longrightarrow> g x y = g y x"
   "f (f x) = x \<and> f (f (f (f (f x)))) = x \<longrightarrow> f x = x"
   "((if a then b else c) = d) = ((a \<longrightarrow> (b = d)) \<and> (\<not> a \<longrightarrow> (c = d)))"
   by smt+
 
 lemma
   "\<forall>x. x = x"
   "(\<forall>x. P x) \<longleftrightarrow> (\<forall>y. P y)"
   "\<forall>x. P x \<longrightarrow> (\<forall>y. P x \<or> P y)"
   "(\<forall>x. P x \<and> Q x) \<longleftrightarrow> (\<forall>x. P x) \<and> (\<forall>x. Q x)"
   "(\<forall>x. P x) \<or> R \<longleftrightarrow> (\<forall>x. P x \<or> R)"
   "(\<forall>x y z. S x z) \<longleftrightarrow> (\<forall>x z. S x z)"
   "(\<forall>x y. S x y \<longrightarrow> S y x) \<longrightarrow> (\<forall>x. S x y) \<longrightarrow> S y x"
   "(\<forall>x. P x \<longrightarrow> P (f x)) \<and> P d \<longrightarrow> P (f(f(f(d))))"
   "(\<forall>x y. s x y = s y x) \<longrightarrow> a = a \<and> s a b = s b a"
   "(\<forall>s. q s \<longrightarrow> r s) \<and> \<not> r s \<and> (\<forall>s. \<not> r s \<and> \<not> q s \<longrightarrow> p t \<or> q t) \<longrightarrow> p t \<or> r t"
   by smt+
 
 lemma
   "(\<forall>x. P x) \<and> R \<longleftrightarrow> (\<forall>x. P x \<and> R)"
   by smt
 
 lemma
   "\<exists>x. x = x"
   "(\<exists>x. P x) \<longleftrightarrow> (\<exists>y. P y)"
   "(\<exists>x. P x \<or> Q x) \<longleftrightarrow> (\<exists>x. P x) \<or> (\<exists>x. Q x)"
   "(\<exists>x. P x) \<and> R \<longleftrightarrow> (\<exists>x. P x \<and> R)"
   "(\<exists>x y z. S x z) \<longleftrightarrow> (\<exists>x z. S x z)"
   "\<not> ((\<exists>x. \<not> P x) \<and> ((\<exists>x. P x) \<or> (\<exists>x. P x \<and> Q x)) \<and> \<not> (\<exists>x. P x))"
   by smt+
 
 lemma
   "\<exists>x y. x = y"
   "(\<exists>x. P x) \<or> R \<longleftrightarrow> (\<exists>x. P x \<or> R)"
   "\<exists>x. P x \<longrightarrow> P a \<and> P b"
   "(\<exists>x. Q \<longrightarrow> P x) \<longleftrightarrow> (Q \<longrightarrow> (\<exists>x. P x))"
-  supply[[smt_trace]]
   by smt+
 
 lemma
+  "(P False \<or> P True) \<or> \<not> P False"
+  by smt
+
+lemma
   "(\<not> (\<exists>x. P x)) \<longleftrightarrow> (\<forall>x. \<not> P x)"
   "(\<exists>x. P x \<longrightarrow> Q) \<longleftrightarrow> (\<forall>x. P x) \<longrightarrow> Q"
   "(\<forall>x y. R x y = x) \<longrightarrow> (\<exists>y. R x y) = R x c"
   "(if P x then \<not> (\<exists>y. P y) else (\<forall>y. \<not> P y)) \<longrightarrow> P x \<longrightarrow> P y"
   "(\<forall>x y. R x y = x) \<and> (\<forall>x. \<exists>y. R x y) = (\<forall>x. R x c) \<longrightarrow> (\<exists>y. R x y) = R x c"
   by smt+
 
 lemma
   "\<forall>x. \<exists>y. f x y = f x (g x)"
   "(\<not> \<not> (\<exists>x. P x)) \<longleftrightarrow> (\<not> (\<forall>x. \<not> P x))"
   "\<forall>u. \<exists>v. \<forall>w. \<exists>x. f u v w x = f u (g u) w (h u w)"
   "\<exists>x. if x = y then (\<forall>y. y = x \<or> y \<noteq> x) else (\<forall>y. y = (x, x) \<or> y \<noteq> (x, x))"
   "\<exists>x. if x = y then (\<exists>y. y = x \<or> y \<noteq> x) else (\<exists>y. y = (x, x) \<or> y \<noteq> (x, x))"
   "(\<exists>x. \<forall>y. P x \<longleftrightarrow> P y) \<longrightarrow> ((\<exists>x. P x) \<longleftrightarrow> (\<forall>y. P y))"
   "(\<exists>y. \<forall>x. R x y) \<longrightarrow> (\<forall>x. \<exists>y. R x y)"
   by smt+
 
 lemma
   "(\<exists>!x. P x) \<longrightarrow> (\<exists>x. P x)"
   "(\<exists>!x. P x) \<longleftrightarrow> (\<exists>x. P x \<and> (\<forall>y. y \<noteq> x \<longrightarrow> \<not> P y))"
   "P a \<longrightarrow> (\<forall>x. P x \<longrightarrow> x = a) \<longrightarrow> (\<exists>!x. P x)"
   "(\<exists>x. P x) \<and> (\<forall>x y. P x \<and> P y \<longrightarrow> x = y) \<longrightarrow> (\<exists>!x. P x)"
   "(\<exists>!x. P x) \<and> (\<forall>x. P x \<and> (\<forall>y. P y \<longrightarrow> y = x) \<longrightarrow> R) \<longrightarrow> R"
   by smt+
 
 lemma
   "(\<forall>x\<in>M. P x) \<and> c \<in> M \<longrightarrow> P c"
   "(\<exists>x\<in>M. P x) \<or> \<not> (P c \<and> c \<in> M)"
   by smt+
 
 lemma
   "let P = True in P"
   "let P = P1 \<or> P2 in P \<or> \<not> P"
   "let P1 = True; P2 = False in P1 \<and> P2 \<longrightarrow> P2 \<or> P1"
   "(let x = y in x) = y"
   "(let x = y in Q x) \<longleftrightarrow> (let z = y in Q z)"
   "(let x = y1; z = y2 in R x z) \<longleftrightarrow> (let z = y2; x = y1 in R x z)"
   "(let x = y1; z = y2 in R x z) \<longleftrightarrow> (let z = y1; x = y2 in R z x)"
   "let P = (\<forall>x. Q x) in if P then P else \<not> P"
   by smt+
 
 lemma
   "a \<noteq> b \<and> a \<noteq> c \<and> b \<noteq> c \<and> (\<forall>x y. f x = f y \<longrightarrow> y = x) \<longrightarrow> f a \<noteq> f b"
   by smt
 
 lemma
   "(\<forall>x y z. f x y = f x z \<longrightarrow> y = z) \<and> b \<noteq> c \<longrightarrow> f a b \<noteq> f a c"
   "(\<forall>x y z. f x y = f z y \<longrightarrow> x = z) \<and> a \<noteq> d \<longrightarrow> f a b \<noteq> f d b"
   by smt+
 
 
 section \<open>Guidance for quantifier heuristics: patterns\<close>
 
 lemma
   assumes "\<forall>x.
     SMT.trigger (SMT.Symb_Cons (SMT.Symb_Cons (SMT.pat (f x)) SMT.Symb_Nil) SMT.Symb_Nil)
     (f x = x)"
   shows "f 1 = 1"
   using assms by smt
 
 lemma
   assumes "\<forall>x y.
     SMT.trigger (SMT.Symb_Cons (SMT.Symb_Cons (SMT.pat (f x))
       (SMT.Symb_Cons (SMT.pat (g y)) SMT.Symb_Nil)) SMT.Symb_Nil) (f x = g y)"
   shows "f a = g b"
   using assms by smt
 
 
 section \<open>Meta-logical connectives\<close>
 
 lemma
   "True \<Longrightarrow> True"
   "False \<Longrightarrow> True"
   "False \<Longrightarrow> False"
   "P' x \<Longrightarrow> P' x"
   "P \<Longrightarrow> P \<or> Q"
   "Q \<Longrightarrow> P \<or> Q"
   "\<not> P \<Longrightarrow> P \<longrightarrow> Q"
   "Q \<Longrightarrow> P \<longrightarrow> Q"
   "\<lbrakk>P; \<not> Q\<rbrakk> \<Longrightarrow> \<not> (P \<longrightarrow> Q)"
   "P' x \<equiv> P' x"
   "P' x \<equiv> Q' x \<Longrightarrow> P' x = Q' x"
   "P' x = Q' x \<Longrightarrow> P' x \<equiv> Q' x"
   "x \<equiv> y \<Longrightarrow> y \<equiv> z \<Longrightarrow> x \<equiv> (z::'a::type)"
   "x \<equiv> y \<Longrightarrow> (f x :: 'b::type) \<equiv> f y"
   "(\<And>x. g x) \<Longrightarrow> g a \<or> a"
   "(\<And>x y. h x y \<and> h y x) \<Longrightarrow> \<forall>x. h x x"
   "(p \<or> q) \<and> \<not> p \<Longrightarrow> q"
   "(a \<and> b) \<or> (c \<and> d) \<Longrightarrow> (a \<and> b) \<or> (c \<and> d)"
   by smt+
 
 
 section \<open>Natural numbers\<close>
 
 declare [[smt_nat_as_int]]
 
 lemma
   "(0::nat) = 0"
   "(1::nat) = 1"
   "(0::nat) < 1"
   "(0::nat) \<le> 1"
   "(123456789::nat) < 2345678901"
   by smt+
 
 lemma
   "Suc 0 = 1"
   "Suc x = x + 1"
   "x < Suc x"
   "(Suc x = Suc y) = (x = y)"
   "Suc (x + y) < Suc x + Suc y"
   by smt+
 
 lemma
   "(x::nat) + 0 = x"
   "0 + x = x"
   "x + y = y + x"
   "x + (y + z) = (x + y) + z"
   "(x + y = 0) = (x = 0 \<and> y = 0)"
   by smt+
 
 lemma
   "(x::nat) - 0 = x"
   "x < y \<longrightarrow> x - y = 0"
   "x - y = 0 \<or> y - x = 0"
   "(x - y) + y = (if x < y then y else x)"
    "x - y - z = x - (y + z)"
   by smt+
 
 lemma
   "(x::nat) * 0 = 0"
   "0 * x = 0"
   "x * 1 = x"
   "1 * x = x"
   "3 * x = x * 3"
   by smt+
 
 lemma
   "min (x::nat) y \<le> x"
   "min x y \<le> y"
   "min x y \<le> x + y"
   "z < x \<and> z < y \<longrightarrow> z < min x y"
   "min x y = min y x"
   "min x 0 = 0"
   by smt+
 
 lemma
   "max (x::nat) y \<ge> x"
   "max x y \<ge> y"
   "max x y \<ge> (x - y) + (y - x)"
   "z > x \<and> z > y \<longrightarrow> z > max x y"
   "max x y = max y x"
   "max x 0 = x"
   by smt+
 
 lemma
   "0 \<le> (x::nat)"
   "0 < x \<and> x \<le> 1 \<longrightarrow> x = 1"
   "x \<le> x"
   "x \<le> y \<longrightarrow> 3 * x \<le> 3 * y"
   "x < y \<longrightarrow> 3 * x < 3 * y"
   "x < y \<longrightarrow> x \<le> y"
   "(x < y) = (x + 1 \<le> y)"
   "\<not> (x < x)"
   "x \<le> y \<longrightarrow> y \<le> z \<longrightarrow> x \<le> z"
   "x < y \<longrightarrow> y \<le> z \<longrightarrow> x \<le> z"
   "x \<le> y \<longrightarrow> y < z \<longrightarrow> x \<le> z"
   "x < y \<longrightarrow> y < z \<longrightarrow> x < z"
   "x < y \<and> y < z \<longrightarrow> \<not> (z < x)"
   by smt+
 
 declare [[smt_nat_as_int = false]]
 
 
 section \<open>Integers\<close>
 
 lemma
   "(0::int) = 0"
   "(0::int) = (- 0)"
   "(1::int) = 1"
   "\<not> (-1 = (1::int))"
   "(0::int) < 1"
   "(0::int) \<le> 1"
   "-123 + 345 < (567::int)"
   "(123456789::int) < 2345678901"
   "(-123456789::int) < 2345678901"
   by smt+
 
 lemma
   "(x::int) + 0 = x"
   "0 + x = x"
   "x + y = y + x"
   "x + (y + z) = (x + y) + z"
   "(x + y = 0) = (x = -y)"
   by smt+
 
 lemma
   "(-1::int) = - 1"
   "(-3::int) = - 3"
   "-(x::int) < 0 \<longleftrightarrow> x > 0"
   "x > 0 \<longrightarrow> -x < 0"
   "x < 0 \<longrightarrow> -x > 0"
   by smt+
 
 lemma
   "(x::int) - 0 = x"
   "0 - x = -x"
   "x < y \<longrightarrow> x - y < 0"
   "x - y = -(y - x)"
   "x - y = -y + x"
   "x - y - z = x - (y + z)"
   by smt+
 
 lemma
   "(x::int) * 0 = 0"
   "0 * x = 0"
   "x * 1 = x"
   "1 * x = x"
   "x * -1 = -x"
   "-1 * x = -x"
   "3 * x = x * 3"
   by smt+
 
 lemma
   "\<bar>x::int\<bar> \<ge> 0"
   "(\<bar>x\<bar> = 0) = (x = 0)"
   "(x \<ge> 0) = (\<bar>x\<bar> = x)"
   "(x \<le> 0) = (\<bar>x\<bar> = -x)"
   "\<bar>\<bar>x\<bar>\<bar> = \<bar>x\<bar>"
   by smt+
 
 lemma
   "min (x::int) y \<le> x"
   "min x y \<le> y"
   "z < x \<and> z < y \<longrightarrow> z < min x y"
   "min x y = min y x"
   "x \<ge> 0 \<longrightarrow> min x 0 = 0"
   "min x y \<le> \<bar>x + y\<bar>"
   by smt+
 
 lemma
   "max (x::int) y \<ge> x"
   "max x y \<ge> y"
   "z > x \<and> z > y \<longrightarrow> z > max x y"
   "max x y = max y x"
   "x \<ge> 0 \<longrightarrow> max x 0 = x"
   "max x y \<ge> - \<bar>x\<bar> - \<bar>y\<bar>"
   by smt+
 
 lemma
   "0 < (x::int) \<and> x \<le> 1 \<longrightarrow> x = 1"
   "x \<le> x"
   "x \<le> y \<longrightarrow> 3 * x \<le> 3 * y"
   "x < y \<longrightarrow> 3 * x < 3 * y"
   "x < y \<longrightarrow> x \<le> y"
   "(x < y) = (x + 1 \<le> y)"
   "\<not> (x < x)"
   "x \<le> y \<longrightarrow> y \<le> z \<longrightarrow> x \<le> z"
   "x < y \<longrightarrow> y \<le> z \<longrightarrow> x \<le> z"
   "x \<le> y \<longrightarrow> y < z \<longrightarrow> x \<le> z"
   "x < y \<longrightarrow> y < z \<longrightarrow> x < z"
   "x < y \<and> y < z \<longrightarrow> \<not> (z < x)"
   by smt+
 
 
 section \<open>Reals\<close>
 
 lemma
   "(0::real) = 0"
   "(0::real) = -0"
   "(0::real) = (- 0)"
   "(1::real) = 1"
   "\<not> (-1 = (1::real))"
   "(0::real) < 1"
   "(0::real) \<le> 1"
   "-123 + 345 < (567::real)"
   "(123456789::real) < 2345678901"
   "(-123456789::real) < 2345678901"
   by smt+
 
 lemma
   "(x::real) + 0 = x"
   "0 + x = x"
   "x + y = y + x"
   "x + (y + z) = (x + y) + z"
   "(x + y = 0) = (x = -y)"
   by smt+
 
 lemma
   "(-1::real) = - 1"
   "(-3::real) = - 3"
   "-(x::real) < 0 \<longleftrightarrow> x > 0"
   "x > 0 \<longrightarrow> -x < 0"
   "x < 0 \<longrightarrow> -x > 0"
   by smt+
 
 lemma
   "(x::real) - 0 = x"
   "0 - x = -x"
   "x < y \<longrightarrow> x - y < 0"
   "x - y = -(y - x)"
   "x - y = -y + x"
   "x - y - z = x - (y + z)"
   by smt+
 
 lemma
   "(x::real) * 0 = 0"
   "0 * x = 0"
   "x * 1 = x"
   "1 * x = x"
   "x * -1 = -x"
   "-1 * x = -x"
   "3 * x = x * 3"
   by smt+
 
 lemma
   "\<bar>x::real\<bar> \<ge> 0"
   "(\<bar>x\<bar> = 0) = (x = 0)"
   "(x \<ge> 0) = (\<bar>x\<bar> = x)"
   "(x \<le> 0) = (\<bar>x\<bar> = -x)"
   "\<bar>\<bar>x\<bar>\<bar> = \<bar>x\<bar>"
   by smt+
 
 lemma
   "min (x::real) y \<le> x"
   "min x y \<le> y"
   "z < x \<and> z < y \<longrightarrow> z < min x y"
   "min x y = min y x"
   "x \<ge> 0 \<longrightarrow> min x 0 = 0"
   "min x y \<le> \<bar>x + y\<bar>"
   by smt+
 
 lemma
   "max (x::real) y \<ge> x"
   "max x y \<ge> y"
   "z > x \<and> z > y \<longrightarrow> z > max x y"
   "max x y = max y x"
   "x \<ge> 0 \<longrightarrow> max x 0 = x"
   "max x y \<ge> - \<bar>x\<bar> - \<bar>y\<bar>"
   by smt+
 
 lemma
   "x \<le> (x::real)"
   "x \<le> y \<longrightarrow> 3 * x \<le> 3 * y"
   "x < y \<longrightarrow> 3 * x < 3 * y"
   "x < y \<longrightarrow> x \<le> y"
   "\<not> (x < x)"
   "x \<le> y \<longrightarrow> y \<le> z \<longrightarrow> x \<le> z"
   "x < y \<longrightarrow> y \<le> z \<longrightarrow> x \<le> z"
   "x \<le> y \<longrightarrow> y < z \<longrightarrow> x \<le> z"
   "x < y \<longrightarrow> y < z \<longrightarrow> x < z"
   "x < y \<and> y < z \<longrightarrow> \<not> (z < x)"
   by smt+
 
 
 section \<open>Datatypes, records, and typedefs\<close>
 
 subsection \<open>Without support by the SMT solver\<close>
 
 subsubsection \<open>Algebraic datatypes\<close>
 
 lemma
   "x = fst (x, y)"
   "y = snd (x, y)"
   "((x, y) = (y, x)) = (x = y)"
   "((x, y) = (u, v)) = (x = u \<and> y = v)"
   "(fst (x, y, z) = fst (u, v, w)) = (x = u)"
   "(snd (x, y, z) = snd (u, v, w)) = (y = v \<and> z = w)"
   "(fst (snd (x, y, z)) = fst (snd (u, v, w))) = (y = v)"
   "(snd (snd (x, y, z)) = snd (snd (u, v, w))) = (z = w)"
   "(fst (x, y) = snd (x, y)) = (x = y)"
   "p1 = (x, y) \<and> p2 = (y, x) \<longrightarrow> fst p1 = snd p2"
   "(fst (x, y) = snd (x, y)) = (x = y)"
   "(fst p = snd p) = (p = (snd p, fst p))"
   using fst_conv snd_conv prod.collapse
   by smt+
 
 lemma
   "[x] \<noteq> Nil"
   "[x, y] \<noteq> Nil"
   "x \<noteq> y \<longrightarrow> [x] \<noteq> [y]"
   "hd (x # xs) = x"
   "tl (x # xs) = xs"
   "hd [x, y, z] = x"
   "tl [x, y, z] = [y, z]"
   "hd (tl [x, y, z]) = y"
   "tl (tl [x, y, z]) = [z]"
   using list.sel(1,3) list.simps
   by smt+
 
 lemma
   "fst (hd [(a, b)]) = a"
   "snd (hd [(a, b)]) = b"
   using fst_conv snd_conv prod.collapse list.sel(1,3) list.simps
   by smt+
 
 
 subsubsection \<open>Records\<close>
 
 record point =
   cx :: int
   cy :: int
 
 record bw_point = point +
   black :: bool
 
 lemma
   "\<lparr>cx = x, cy = y\<rparr> = \<lparr>cx = x', cy = y'\<rparr> \<Longrightarrow> x = x' \<and> y = y'"
   using point.simps
   by smt
 
 lemma
   "cx \<lparr> cx = 3, cy = 4 \<rparr> = 3"
   "cy \<lparr> cx = 3, cy = 4 \<rparr> = 4"
   "cx \<lparr> cx = 3, cy = 4 \<rparr> \<noteq> cy \<lparr> cx = 3, cy = 4 \<rparr>"
   "\<lparr> cx = 3, cy = 4 \<rparr> \<lparr> cx := 5 \<rparr> = \<lparr> cx = 5, cy = 4 \<rparr>"
   "\<lparr> cx = 3, cy = 4 \<rparr> \<lparr> cy := 6 \<rparr> = \<lparr> cx = 3, cy = 6 \<rparr>"
   "p = \<lparr> cx = 3, cy = 4 \<rparr> \<longrightarrow> p \<lparr> cx := 3 \<rparr> \<lparr> cy := 4 \<rparr> = p"
   "p = \<lparr> cx = 3, cy = 4 \<rparr> \<longrightarrow> p \<lparr> cy := 4 \<rparr> \<lparr> cx := 3 \<rparr> = p"
   using point.simps
   by smt+
 
 lemma
   "\<lparr>cx = x, cy = y, black = b\<rparr> = \<lparr>cx = x', cy = y', black = b'\<rparr> \<Longrightarrow> x = x' \<and> y = y' \<and> b = b'"
   using point.simps bw_point.simps
   by smt
 
 lemma
   "cx \<lparr> cx = 3, cy = 4, black = b \<rparr> = 3"
   "cy \<lparr> cx = 3, cy = 4, black = b \<rparr> = 4"
   "black \<lparr> cx = 3, cy = 4, black = b \<rparr> = b"
   "cx \<lparr> cx = 3, cy = 4, black = b \<rparr> \<noteq> cy \<lparr> cx = 3, cy = 4, black = b \<rparr>"
   "\<lparr> cx = 3, cy = 4, black = b \<rparr> \<lparr> cx := 5 \<rparr> = \<lparr> cx = 5, cy = 4, black = b \<rparr>"
   "\<lparr> cx = 3, cy = 4, black = b \<rparr> \<lparr> cy := 6 \<rparr> = \<lparr> cx = 3, cy = 6, black = b \<rparr>"
   "p = \<lparr> cx = 3, cy = 4, black = True \<rparr> \<longrightarrow>
      p \<lparr> cx := 3 \<rparr> \<lparr> cy := 4 \<rparr> \<lparr> black := True \<rparr> = p"
   "p = \<lparr> cx = 3, cy = 4, black = True \<rparr> \<longrightarrow>
      p \<lparr> cy := 4 \<rparr> \<lparr> black := True \<rparr> \<lparr> cx := 3 \<rparr> = p"
   "p = \<lparr> cx = 3, cy = 4, black = True \<rparr> \<longrightarrow>
      p \<lparr> black := True \<rparr> \<lparr> cx := 3 \<rparr> \<lparr> cy := 4 \<rparr> = p"
   using point.simps bw_point.simps
   by smt+
 
 lemma
   "\<lparr> cx = 3, cy = 4, black = b \<rparr> \<lparr> black := w \<rparr> = \<lparr> cx = 3, cy = 4, black = w \<rparr>"
   "\<lparr> cx = 3, cy = 4, black = True \<rparr> \<lparr> black := False \<rparr> =
      \<lparr> cx = 3, cy = 4, black = False \<rparr>"
   "p \<lparr> cx := 3 \<rparr> \<lparr> cy := 4 \<rparr> \<lparr> black := True \<rparr> =
      p \<lparr> black := True \<rparr> \<lparr> cy := 4 \<rparr> \<lparr> cx := 3 \<rparr>"
     apply (smt add_One add_inc bw_point.update_convs(1) default_unit_def inc.simps(2) one_plus_BitM
       semiring_norm(6,26))
    apply (smt bw_point.update_convs(1))
   apply (smt bw_point.cases_scheme bw_point.update_convs(1) point.update_convs(1,2))
   done
 
 
 subsubsection \<open>Type definitions\<close>
 
 typedef int' = "UNIV::int set" by (rule UNIV_witness)
 
 definition n0 where "n0 = Abs_int' 0"
 definition n1 where "n1 = Abs_int' 1"
 definition n2 where "n2 = Abs_int' 2"
 definition plus' where "plus' n m = Abs_int' (Rep_int' n + Rep_int' m)"
 
 lemma
   "n0 \<noteq> n1"
   "plus' n1 n1 = n2"
   "plus' n0 n2 = n2"
   by (smt n0_def n1_def n2_def plus'_def Abs_int'_inverse Rep_int'_inverse UNIV_I)+
 
 
 subsection \<open>With support by the SMT solver (but without proofs)\<close>
 
 subsubsection \<open>Algebraic datatypes\<close>
 
 lemma
   "x = fst (x, y)"
   "y = snd (x, y)"
   "((x, y) = (y, x)) = (x = y)"
   "((x, y) = (u, v)) = (x = u \<and> y = v)"
   "(fst (x, y, z) = fst (u, v, w)) = (x = u)"
   "(snd (x, y, z) = snd (u, v, w)) = (y = v \<and> z = w)"
   "(fst (snd (x, y, z)) = fst (snd (u, v, w))) = (y = v)"
   "(snd (snd (x, y, z)) = snd (snd (u, v, w))) = (z = w)"
   "(fst (x, y) = snd (x, y)) = (x = y)"
   "p1 = (x, y) \<and> p2 = (y, x) \<longrightarrow> fst p1 = snd p2"
   "(fst (x, y) = snd (x, y)) = (x = y)"
   "(fst p = snd p) = (p = (snd p, fst p))"
   using fst_conv snd_conv prod.collapse
   by smt+
 
 lemma
   "x \<noteq> y \<longrightarrow> [x] \<noteq> [y]"
   "hd (x # xs) = x"
   "tl (x # xs) = xs"
   "hd [x, y, z] = x"
   "tl [x, y, z] = [y, z]"
   "hd (tl [x, y, z]) = y"
   "tl (tl [x, y, z]) = [z]"
   using list.sel(1,3)
   by smt+
 
 lemma
   "fst (hd [(a, b)]) = a"
   "snd (hd [(a, b)]) = b"
   using fst_conv snd_conv prod.collapse list.sel(1,3)
   by smt+
 
 
 subsubsection \<open>Records\<close>
 text \<open>The equivalent theory for Z3 contains more example, but unlike Z3, we are able
 to reconstruct the proofs.\<close>
 
 lemma
   "cx \<lparr> cx = 3, cy = 4 \<rparr> = 3"
   "cy \<lparr> cx = 3, cy = 4 \<rparr> = 4"
   "cx \<lparr> cx = 3, cy = 4 \<rparr> \<noteq> cy \<lparr> cx = 3, cy = 4 \<rparr>"
   "\<lparr> cx = 3, cy = 4 \<rparr> \<lparr> cx := 5 \<rparr> = \<lparr> cx = 5, cy = 4 \<rparr>"
   "\<lparr> cx = 3, cy = 4 \<rparr> \<lparr> cy := 6 \<rparr> = \<lparr> cx = 3, cy = 6 \<rparr>"
   "p = \<lparr> cx = 3, cy = 4 \<rparr> \<longrightarrow> p \<lparr> cx := 3 \<rparr> \<lparr> cy := 4 \<rparr> = p"
   "p = \<lparr> cx = 3, cy = 4 \<rparr> \<longrightarrow> p \<lparr> cy := 4 \<rparr> \<lparr> cx := 3 \<rparr> = p"
   using point.simps
   by smt+
 
 
 lemma
   "cx \<lparr> cx = 3, cy = 4, black = b \<rparr> = 3"
   "cy \<lparr> cx = 3, cy = 4, black = b \<rparr> = 4"
   "black \<lparr> cx = 3, cy = 4, black = b \<rparr> = b"
   "cx \<lparr> cx = 3, cy = 4, black = b \<rparr> \<noteq> cy \<lparr> cx = 3, cy = 4, black = b \<rparr>"
   "\<lparr> cx = 3, cy = 4, black = b \<rparr> \<lparr> cx := 5 \<rparr> = \<lparr> cx = 5, cy = 4, black = b \<rparr>"
   "\<lparr> cx = 3, cy = 4, black = b \<rparr> \<lparr> cy := 6 \<rparr> = \<lparr> cx = 3, cy = 6, black = b \<rparr>"
   "p = \<lparr> cx = 3, cy = 4, black = True \<rparr> \<longrightarrow>
      p \<lparr> cx := 3 \<rparr> \<lparr> cy := 4 \<rparr> \<lparr> black := True \<rparr> = p"
   "p = \<lparr> cx = 3, cy = 4, black = True \<rparr> \<longrightarrow>
      p \<lparr> cy := 4 \<rparr> \<lparr> black := True \<rparr> \<lparr> cx := 3 \<rparr> = p"
   "p = \<lparr> cx = 3, cy = 4, black = True \<rparr> \<longrightarrow>
      p \<lparr> black := True \<rparr> \<lparr> cx := 3 \<rparr> \<lparr> cy := 4 \<rparr> = p"
   using point.simps bw_point.simps
   by smt+
 
 
 section \<open>Functions\<close>
 
 lemma "\<exists>f. map_option f (Some x) = Some (y + x)"
   by (smt option.map(2))
 
 lemma
   "(f (i := v)) i = v"
   "i1 \<noteq> i2 \<longrightarrow> (f (i1 := v)) i2 = f i2"
   "i1 \<noteq> i2 \<longrightarrow> (f (i1 := v1, i2 := v2)) i1 = v1"
   "i1 \<noteq> i2 \<longrightarrow> (f (i1 := v1, i2 := v2)) i2 = v2"
   "i1 = i2 \<longrightarrow> (f (i1 := v1, i2 := v2)) i1 = v2"
   "i1 = i2 \<longrightarrow> (f (i1 := v1, i2 := v2)) i1 = v2"
   "i1 \<noteq> i2 \<and>i1 \<noteq> i3 \<and>  i2 \<noteq> i3 \<longrightarrow> (f (i1 := v1, i2 := v2)) i3 = f i3"
   using fun_upd_same fun_upd_apply
   by smt+
 
 
 section \<open>Sets\<close>
 
 lemma Empty: "x \<notin> {}" by simp
 
 lemmas smt_sets = Empty UNIV_I Un_iff Int_iff
 
 lemma
   "x \<notin> {}"
   "x \<in> UNIV"
   "x \<in> A \<union> B \<longleftrightarrow> x \<in> A \<or> x \<in> B"
   "x \<in> P \<union> {} \<longleftrightarrow> x \<in> P"
   "x \<in> P \<union> UNIV"
   "x \<in> P \<union> Q \<longleftrightarrow> x \<in> Q \<union> P"
   "x \<in> P \<union> P \<longleftrightarrow> x \<in> P"
   "x \<in> P \<union> (Q \<union> R) \<longleftrightarrow> x \<in> (P \<union> Q) \<union> R"
   "x \<in> A \<inter> B \<longleftrightarrow> x \<in> A \<and> x \<in> B"
   "x \<notin> P \<inter> {}"
   "x \<in> P \<inter> UNIV \<longleftrightarrow> x \<in> P"
   "x \<in> P \<inter> Q \<longleftrightarrow> x \<in> Q \<inter> P"
   "x \<in> P \<inter> P \<longleftrightarrow> x \<in> P"
   "x \<in> P \<inter> (Q \<inter> R) \<longleftrightarrow> x \<in> (P \<inter> Q) \<inter> R"
   "{x. x \<in> P} = {y. y \<in> P}"
   by (smt smt_sets)+
 
 end
diff --git a/src/HOL/Tools/SMT/smt_replay_arith.ML b/src/HOL/Tools/SMT/smt_replay_arith.ML
--- a/src/HOL/Tools/SMT/smt_replay_arith.ML
+++ b/src/HOL/Tools/SMT/smt_replay_arith.ML
@@ -1,117 +1,117 @@
 (*  Title:      HOL/Tools/SMT/smt_replay_arith.ML
     Author:     Mathias Fleury, MPII, JKU
 
 Proof methods for replaying arithmetic steps with Farkas Lemma.
 *)
 
 signature SMT_REPLAY_ARITH =
 sig
   val la_farkas_tac: Subgoal.focus -> term list -> thm -> thm Seq.seq;
   val la_farkas: term list -> Proof.context -> int -> tactic;
 end;
 
 structure SMT_Replay_Arith: SMT_REPLAY_ARITH =
 struct
 
 fun extract_number (Const ("SMT.z3div", _) $ (Const ("Groups.uminus_class.uminus", _) $ n1) $ n2) =
       (n1, n2, false)
   | extract_number (Const ("SMT.z3div", _) $ n1 $ n2) = (n1, n2, true)
   | extract_number (Const ("Groups.uminus_class.uminus", _) $ n) =
       (n, HOLogic.numeral_const (fastype_of n) $ HOLogic.one_const, false)
   | extract_number n = (n, HOLogic.numeral_const (fastype_of n) $ HOLogic.one_const, true)
 
 fun try_OF _ thm1 thm2 =
     (thm1 OF [thm2])
     |> single
   handle THM _ => []
 
 fun try_OF_inst ctxt thm1 ((r, q, pos), thm2) =
     map (fn thm =>
       (Drule.infer_instantiate' ctxt (map SOME [Thm.cterm_of ctxt q, Thm.cterm_of ctxt r]) thm,
         pos))
       (try_OF ctxt thm1 thm2)
   handle THM _ => []
 
 fun try_OF_insts ctxt thms thm = map (fn thm1 => try_OF_inst ctxt thm1 thm) thms |> flat
 
 fun try_OFs ctxt thms thm = map (fn thm1 => try_OF ctxt thm1 thm) thms |> flat
 
 fun la_farkas_tac ({context = ctxt, prems, concl,  ...}: Subgoal.focus) args thm =
   let
     fun trace v = (SMT_Config.verit_arith_msg ctxt v; v)
     val _ = trace (fn () => @{print} (prems, concl))
     val arith_thms = Named_Theorems.get ctxt @{named_theorems smt_arith_simplify}
     val verit_arith = Named_Theorems.get ctxt @{named_theorems smt_arith_combine}
     val verit_arith_multiplication = Named_Theorems.get ctxt @{named_theorems smt_arith_multiplication}
     val _ = trace (fn () => @{print}  "******************************************************")
     val _ = trace (fn () => @{print}  "       Multiply by constants                          ")
     val _ = trace (fn () => @{print}  "******************************************************")
     val coeff_prems =
        map extract_number args
        |> (fn xs => ListPair.zip (xs, prems))
     val _ = trace (fn () => @{print} coeff_prems)
     fun negate_if_needed (thm, pos) =
        if pos then thm
        else map (fn thm0 => try_OF ctxt thm0 thm) @{thms verit_negate_coefficient}
          |> flat |> the_single
     val normalized =
       map (try_OF_insts ctxt verit_arith_multiplication) coeff_prems
       |> flat
       |> map negate_if_needed
     fun import_assumption thm (Trues, ctxt) =
        let val (assms, ctxt) = Assumption.add_assumes ((map (Thm.cterm_of ctxt) o Thm.prems_of) thm) ctxt in
          (thm OF assms, (Trues + length assms, ctxt)) end
     val (n :: normalized, (Trues, ctxt_with_assms)) = fold_map import_assumption normalized (0, ctxt)
 
     val _ = trace (fn () => @{print} (n :: normalized))
     val _ = trace (fn () => @{print}   "*****************************************************")
     val _ = trace (fn () => @{print}  "       Combine equalities                             ")
     val _ = trace (fn () => @{print}  "******************************************************")
 
     val combined =
       List.foldl
          (fn (thm1, thm2) =>
            try_OFs ctxt verit_arith thm1
            |> (fn thms => try_OFs ctxt thms thm2)
            |> the_single)
          n
          normalized
       |> singleton (Proof_Context.export ctxt_with_assms ctxt)
     val _ = trace (fn () => @{print} combined)
     fun arith_full_simps ctxt thms =
       ctxt
        |> empty_simpset
       |> put_simpset HOL_basic_ss
        |> (fn ctxt => ctxt addsimps thms
            addsimps arith_thms
            addsimprocs [@{simproc int_div_cancel_numeral_factors}, @{simproc int_combine_numerals},
              @{simproc divide_cancel_numeral_factor}, @{simproc intle_cancel_numerals},
              @{simproc field_combine_numerals}, @{simproc intless_cancel_numerals}])
       |> asm_full_simplify
     val final_False = combined
       |> arith_full_simps ctxt (Named_Theorems.get ctxt @{named_theorems ac_simps})
     val _ = trace (fn () => @{print} final_False)
     val final_theorem = try_OF ctxt thm final_False
   in
     (case final_theorem of
        [thm] => Seq.single (thm OF replicate Trues @{thm TrueI})
     | _ => Seq.empty)
   end
 
 fun TRY' tac = fn i => TRY (tac i)
 fun REPEAT' tac = fn i => REPEAT (tac i)
 
 fun rewrite_only_thms ctxt thms =
   ctxt
   |> empty_simpset
   |> put_simpset HOL_basic_ss
   |> (fn ctxt => ctxt addsimps thms)
   |> Simplifier.full_simp_tac
 
 fun la_farkas args ctxt =
-  REPEAT' (resolve_tac ctxt @{thms verit_and_pos(2,3)})
+  REPEAT' (resolve_tac ctxt @{thms verit_and_pos(3,4)})
   THEN' TRY' (resolve_tac ctxt @{thms ccontr})
   THEN' TRY' (rewrite_only_thms ctxt @{thms linorder_class.not_less linorder_class.not_le not_not})
   THEN' (Subgoal.FOCUS (fn focus => la_farkas_tac focus args) ctxt)
 
 end
\ No newline at end of file
diff --git a/src/HOL/Tools/SMT/verit_proof.ML b/src/HOL/Tools/SMT/verit_proof.ML
--- a/src/HOL/Tools/SMT/verit_proof.ML
+++ b/src/HOL/Tools/SMT/verit_proof.ML
@@ -1,748 +1,859 @@
 (*  Title:      HOL/Tools/SMT/Verit_Proof.ML
     Author:     Mathias Fleury, ENS Rennes
     Author:     Sascha Boehme, TU Muenchen
 
 VeriT proofs: parsing and abstract syntax tree.
 *)
 
 signature VERIT_PROOF =
 sig
   (*proofs*)
   datatype veriT_step = VeriT_Step of {
     id: string,
     rule: string,
     prems: string list,
     proof_ctxt: term list,
     concl: term,
     fixes: string list}
 
   datatype veriT_replay_node = VeriT_Replay_Node of {
     id: string,
     rule: string,
     args: term list,
     prems: string list,
     proof_ctxt: term list,
     concl: term,
     bounds: (string * typ) list,
     declarations: (string * term) list,
     insts: term Symtab.table,
     subproof: (string * typ) list * term list * term list * veriT_replay_node list}
 
   (*proof parser*)
   val parse: typ Symtab.table -> term Symtab.table -> string list ->
     Proof.context -> veriT_step list * Proof.context
   val parse_replay: typ Symtab.table -> term Symtab.table -> string list ->
     Proof.context -> veriT_replay_node list * Proof.context
 
   val step_prefix : string
   val input_rule: string
   val keep_app_symbols: string -> bool
   val keep_raw_lifting: string -> bool
   val normalized_input_rule: string
   val la_generic_rule : string
   val rewrite_rule : string
   val simp_arith_rule : string
   val veriT_deep_skolemize_rule : string
   val veriT_def : string
   val subproof_rule : string
   val local_input_rule : string
+  val not_not_rule : string
+  val contract_rule : string
+  val ite_intro_rule : string
+  val eq_congruent_rule : string
+  val eq_congruent_pred_rule : string
+  val skolemization_steps : string list
 
-  val is_skolemisation: string -> bool
-  val is_skolemisation_step: veriT_replay_node -> bool
+  val is_skolemization: string -> bool
+  val is_skolemization_step: veriT_replay_node -> bool
 
   val number_of_steps: veriT_replay_node list -> int
 
   (*Strategy related*)
   val veriT_strategy : string Config.T
   val veriT_current_strategy : Context.generic -> string list
   val all_veriT_stgies: Context.generic -> string list;
 
   val select_veriT_stgy: string -> Context.generic -> Context.generic;
   val valid_veriT_stgy: string -> Context.generic -> bool;
   val verit_add_stgy: string * string list -> Context.generic -> Context.generic
   val verit_rm_stgy: string -> Context.generic -> Context.generic
 
   (*Global tactic*)
   val verit_tac: Proof.context -> thm list -> int -> tactic
   val verit_tac_stgy: string -> Proof.context -> thm list -> int -> tactic
 end;
 
 structure Verit_Proof: VERIT_PROOF =
 struct
 
 open SMTLIB_Proof
 
 val veriT_strategy_default_name = "default"; (*FUDGE*)
 val veriT_strategy_del_insts_name = "del_insts"; (*FUDGE*)
 val veriT_strategy_rm_insts_name = "ccfv_SIG"; (*FUDGE*)
 val veriT_strategy_ccfv_insts_name = "ccfv_threshold"; (*FUDGE*)
 val veriT_strategy_best_name = "best"; (*FUDGE*)
 
 val veriT_strategy_best = ["--index-sorts", "--index-fresh-sorts", "--triggers-new",
   "--triggers-sel-rm-specific"];
 val veriT_strategy_del_insts = ["--index-sorts", "--index-fresh-sorts", "--ccfv-breadth",
   "--inst-deletion", "--index-SAT-triggers", "--inst-deletion-loops", "--inst-deletion-track-vars",
   "--inst-deletion", "--index-SAT-triggers"];
 val veriT_strategy_rm_insts = ["--index-SIG", "--triggers-new", "--triggers-sel-rm-specific"];
 val veriT_strategy_ccfv_insts = ["--index-sorts", "--index-fresh-sorts", "--triggers-new",
   "--triggers-sel-rm-specific", "--triggers-restrict-combine", "--inst-deletion",
   "--index-SAT-triggers", "--inst-deletion-loops", "--inst-deletion-track-vars", "--inst-deletion",
   "--index-SAT-triggers", "--inst-sorts-threshold=100000", "--ematch-exp=10000000",
   "--ccfv-index=100000", "--ccfv-index-full=1000"]
 
 val veriT_strategy_default = [];
 
 type verit_strategy = {default_strategy: string, strategies: (string * string list) list}
 fun mk_verit_strategy default_strategy strategies : verit_strategy = {default_strategy=default_strategy,strategies=strategies}
 
 val empty_data = mk_verit_strategy veriT_strategy_best_name
   [(veriT_strategy_default_name, veriT_strategy_default),
    (veriT_strategy_del_insts_name, veriT_strategy_del_insts),
    (veriT_strategy_rm_insts_name, veriT_strategy_rm_insts),
    (veriT_strategy_ccfv_insts_name, veriT_strategy_ccfv_insts),
    (veriT_strategy_best_name, veriT_strategy_best)]
 
 fun merge_data ({strategies=strategies1,...}:verit_strategy,
     {default_strategy,strategies=strategies2}:verit_strategy) : verit_strategy =
   mk_verit_strategy default_strategy (AList.merge (op =) (op =) (strategies1, strategies2))
 
 structure Data = Generic_Data
 (
   type T = verit_strategy
   val empty = empty_data
   val extend = I
   val merge = merge_data
 )
 
 fun veriT_current_strategy ctxt =
   let
     val {default_strategy,strategies} = (Data.get ctxt)
   in
     AList.lookup (op=) strategies default_strategy
    |> the
   end
 
 val veriT_strategy = Attrib.setup_config_string \<^binding>\<open>smt_verit_strategy\<close> (K veriT_strategy_best_name);
 
 fun valid_veriT_stgy stgy context =
   let
     val {strategies,...} = Data.get context
   in
     AList.defined (op =) strategies stgy
   end
 
 fun select_veriT_stgy stgy context =
   let
     val {strategies,...} = Data.get context
     val upd = Data.map (K (mk_verit_strategy stgy strategies))
   in
     if not (AList.defined (op =) strategies stgy) then
       error ("Trying to select unknown veriT strategy: " ^ quote stgy)
     else upd context
   end
 
 fun verit_add_stgy stgy context =
   let
     val {default_strategy,strategies} = Data.get context
   in
     Data.map 
       (K (mk_verit_strategy default_strategy (AList.update (op =) stgy strategies)))
       context
   end
 
 fun verit_rm_stgy stgy context =
   let
     val {default_strategy,strategies} = Data.get context
   in
     Data.map 
       (K (mk_verit_strategy default_strategy (AList.delete (op =) stgy strategies)))
       context
   end
 
 fun all_veriT_stgies context =
   let
     val {strategies,...} = Data.get context
    in
     map fst strategies
   end
 
 fun verit_tac ctxt = SMT_Solver.smt_tac (Context.proof_map (SMT_Config.select_solver "verit") ctxt)
 fun verit_tac_stgy stgy ctxt = verit_tac (Context.proof_of (select_veriT_stgy stgy (Context.Proof ctxt)))
 
 datatype raw_veriT_node = Raw_VeriT_Node of {
   id: string,
   rule: string,
   args: SMTLIB.tree,
   prems: string list,
   concl: SMTLIB.tree,
   declarations: (string * SMTLIB.tree) list,
   subproof: raw_veriT_node list}
 
 fun mk_raw_node id rule args prems declarations concl subproof =
   Raw_VeriT_Node {id = id, rule = rule, args = args, prems = prems, declarations = declarations,
     concl = concl, subproof = subproof}
 
 datatype veriT_node = VeriT_Node of {
   id: string,
   rule: string,
   prems: string list,
   proof_ctxt: term list,
-  concl: term,
-  bounds: string list}
+  concl: term}
 
-fun mk_node id rule prems proof_ctxt concl bounds =
-  VeriT_Node {id = id, rule = rule, prems = prems, proof_ctxt = proof_ctxt, concl = concl,
-    bounds = bounds}
+fun mk_node id rule prems proof_ctxt concl =
+  VeriT_Node {id = id, rule = rule, prems = prems, proof_ctxt = proof_ctxt, concl = concl}
 
 datatype veriT_replay_node = VeriT_Replay_Node of {
   id: string,
   rule: string,
   args: term list,
   prems: string list,
   proof_ctxt: term list,
   concl: term,
   bounds: (string * typ) list,
   insts: term Symtab.table,
   declarations: (string * term) list,
   subproof: (string * typ) list * term list * term list * veriT_replay_node list}
 
 fun mk_replay_node id rule args prems proof_ctxt concl bounds insts declarations subproof =
   VeriT_Replay_Node {id = id, rule = rule, args = args, prems = prems, proof_ctxt = proof_ctxt,
     concl = concl, bounds = bounds, insts = insts, declarations = declarations,
     subproof = subproof}
 
 datatype veriT_step = VeriT_Step of {
   id: string,
   rule: string,
   prems: string list,
   proof_ctxt: term list,
   concl: term,
   fixes: string list}
 
 fun mk_step id rule prems proof_ctxt concl fixes =
   VeriT_Step {id = id, rule = rule, prems = prems, proof_ctxt = proof_ctxt, concl = concl,
     fixes = fixes}
 
 val step_prefix = ".c"
 val input_rule = "input"
 val la_generic_rule = "la_generic"
-val normalized_input_rule = "__normalized_input" (* arbitrary *)
-val rewrite_rule = "__rewrite" (* arbitrary *)
+val normalized_input_rule = "__normalized_input" (*arbitrary*)
+val rewrite_rule = "__rewrite" (*arbitrary*)
 val subproof_rule = "subproof"
-val local_input_rule = "__local_input" (* arbitrary *)
+val local_input_rule = "__local_input" (*arbitrary*)
 val simp_arith_rule = "simp_arith"
 val veriT_def = "__skolem_definition" (*arbitrary*)
+val not_not_rule = "not_not"
+val contract_rule = "contraction"
+val eq_congruent_pred_rule = "eq_congruent_pred"
+val eq_congruent_rule = "eq_congruent"
+val ite_intro_rule = "ite_intro"
+val default_skolem_rule = "sko_forall" (*arbitrary, but must be one of the skolems*)
 
-val is_skolemisation = member (op =) ["sko_forall", "sko_ex"]
-val keep_app_symbols = member (op =) ["eq_congruent_pred", "eq_congruent", "ite_intro"]
-val keep_raw_lifting = member (op =) ["eq_congruent_pred", "eq_congruent", "ite_intro"]
+val skolemization_steps = ["sko_forall", "sko_ex"]
+val is_skolemization = member (op =) skolemization_steps
+val keep_app_symbols = member (op =) [eq_congruent_pred_rule, eq_congruent_rule, ite_intro_rule]
+val keep_raw_lifting = member (op =) [eq_congruent_pred_rule, eq_congruent_rule, ite_intro_rule]
+val is_SH_trivial = member (op =) [not_not_rule, contract_rule]
 
-fun is_skolemisation_step (VeriT_Replay_Node {id, ...}) = is_skolemisation id
+fun is_skolemization_step (VeriT_Replay_Node {id, ...}) = is_skolemization id
 
 (* Even the veriT developers do not know if the following rule can still appear in proofs: *)
 val veriT_deep_skolemize_rule = "deep_skolemize"
 
 fun number_of_steps [] = 0
   | number_of_steps ((VeriT_Replay_Node {subproof = (_, _, _, subproof), ...}) :: pf) =
       1 + number_of_steps subproof + number_of_steps pf
 
 (* proof parser *)
 
 fun node_of p cx =
   ([], cx)
   ||>> `(with_fresh_names (term_of p))
   |>> snd
 
 fun find_type_in_formula (Abs (v, T, u)) var_name =
     if String.isPrefix var_name v then SOME T else find_type_in_formula u var_name
   | find_type_in_formula (u $ v) var_name =
     (case find_type_in_formula u var_name of
       NONE => find_type_in_formula v var_name
     | some_T => some_T)
   | find_type_in_formula (Free(v, T)) var_name =
     if String.isPrefix var_name v then SOME T else NONE
   | find_type_in_formula _ _ = NONE
 
 fun synctactic_var_subst old_name new_name (u $ v) =
     (synctactic_var_subst old_name new_name u $ synctactic_var_subst old_name new_name v)
   | synctactic_var_subst old_name new_name (Abs (v, T, u)) =
     Abs (if String.isPrefix old_name v then new_name else v, T,
       synctactic_var_subst old_name new_name u)
   | synctactic_var_subst old_name new_name (Free (v, T)) =
      if String.isPrefix old_name v then Free (new_name, T) else Free (v, T)
   | synctactic_var_subst _ _ t = t
 
 fun synctatic_rew_in_lhs_subst old_name new_name (Const(\<^const_name>\<open>HOL.eq\<close>, T) $ t1 $ t2) =
      Const(\<^const_name>\<open>HOL.eq\<close>, T) $ synctactic_var_subst old_name new_name t1 $ t2
   | synctatic_rew_in_lhs_subst old_name new_name (Const(\<^const_name>\<open>Trueprop\<close>, T) $ t1) =
      Const(\<^const_name>\<open>Trueprop\<close>, T) $ (synctatic_rew_in_lhs_subst old_name new_name t1)
   | synctatic_rew_in_lhs_subst _ _ t = t
 
 fun add_bound_variables_to_ctxt concl =
   fold (update_binding o
     (fn s => (s, Term (Free (s, the_default dummyT (find_type_in_formula concl s))))))
 
 local
 
   fun remove_Sym (SMTLIB.Sym y) = y
     | remove_Sym y = (@{print} y; raise (Fail "failed to match"))
 
   fun extract_symbols bds =
     bds
     |> map (fn SMTLIB.S [SMTLIB.Sym "=", SMTLIB.Sym x, SMTLIB.Sym y] => [[x, y]]
              | SMTLIB.S [SMTLIB.Key "=", SMTLIB.Sym x, SMTLIB.Sym y] => [[x, y]]
              | SMTLIB.S syms => map (single o remove_Sym) syms
              | SMTLIB.Sym x => [[x]]
              | t => raise (Fail ("match error " ^ @{make_string} t)))
     |> flat
 
   (* onepoint can bind a variable to another variable or to a constant *)
   fun extract_qnt_symbols cx bds =
     bds
     |> map (fn SMTLIB.S [SMTLIB.Sym "=", SMTLIB.Sym x, SMTLIB.Sym y] =>
                 (case node_of (SMTLIB.Sym y) cx  of
                   ((_, []), _) => [[x]]
                 | _ => [[x, y]])
              | SMTLIB.S [SMTLIB.Key "=", SMTLIB.Sym x, SMTLIB.Sym y] =>
                 (case node_of (SMTLIB.Sym y) cx  of
                   ((_, []), _) => [[x]]
                 | _ => [[x, y]])
              | SMTLIB.S (SMTLIB.Sym "=" :: SMTLIB.Sym x :: _) => [[x]]
              | SMTLIB.S (SMTLIB.Key "=" :: SMTLIB.Sym x :: _) => [[x]]
              | SMTLIB.S syms => map (single o remove_Sym) syms
              | SMTLIB.Sym x => [[x]]
              | t => raise (Fail ("match error " ^ @{make_string} t)))
     |> flat
 
   fun extract_symbols_map bds =
     bds
     |> map (fn SMTLIB.S [SMTLIB.Sym "=", SMTLIB.Sym x, _] => [[x]]
              | SMTLIB.S syms =>  map (single o remove_Sym) syms)
     |> flat
 in
 
 fun declared_csts _ "__skolem_definition" (SMTLIB.S [SMTLIB.Sym x, typ, _]) = [(x, typ)]
   | declared_csts _ _ _ = []
 
 fun skolems_introduced_by_rule (SMTLIB.S bds) =
    fold (fn (SMTLIB.S [SMTLIB.Sym "=", SMTLIB.Sym _, SMTLIB.Sym y]) => curry (op ::) y) bds []
 
 (*FIXME there is probably a way to use the information given by onepoint*)
 fun bound_vars_by_rule _ "bind" (SMTLIB.S bds) = extract_symbols bds
   | bound_vars_by_rule cx "onepoint" (SMTLIB.S bds) = extract_qnt_symbols cx bds
   | bound_vars_by_rule _ "sko_forall" (SMTLIB.S bds) = extract_symbols_map bds
   | bound_vars_by_rule _ "sko_ex" (SMTLIB.S bds) = extract_symbols_map bds
   | bound_vars_by_rule _ "__skolem_definition" (SMTLIB.S [SMTLIB.Sym x, _, _]) = [[x]]
   | bound_vars_by_rule _ _ _ = []
 
 (* VeriT adds "?" before some variables. *)
 fun remove_all_qm (SMTLIB.Sym v :: l) =
     SMTLIB.Sym (perhaps (try (unprefix "?")) v) :: remove_all_qm l
   | remove_all_qm (SMTLIB.S l :: l') = SMTLIB.S (remove_all_qm l) :: remove_all_qm l'
   | remove_all_qm (SMTLIB.Key v :: l) = SMTLIB.Key v :: remove_all_qm l
   | remove_all_qm (v :: l) = v :: remove_all_qm l
   | remove_all_qm [] = []
 
 fun remove_all_qm2 (SMTLIB.Sym v) = SMTLIB.Sym (perhaps (try (unprefix "?")) v)
   | remove_all_qm2 (SMTLIB.S l) = SMTLIB.S (remove_all_qm l)
   | remove_all_qm2 (SMTLIB.Key v) = SMTLIB.Key v
   | remove_all_qm2 v = v
 
 end
 
 datatype step_kind = ASSUME | ANCHOR | NO_STEP | NORMAL_STEP | SKOLEM
 
 fun parse_raw_proof_steps (limit : string option) (ls : SMTLIB.tree list) (cx : name_bindings) :
      (raw_veriT_node list * SMTLIB.tree list * name_bindings) =
   let
     fun rotate_pair (a, (b, c)) = ((a, b), c)
     fun step_kind [] = (NO_STEP, SMTLIB.S [], [])
       | step_kind ((p as SMTLIB.S (SMTLIB.Sym "anchor" :: _)) :: l) = (ANCHOR, p, l)
       | step_kind ((p as SMTLIB.S (SMTLIB.Sym "assume" :: _)) :: l) = (ASSUME, p, l)
       | step_kind ((p as SMTLIB.S (SMTLIB.Sym "step" :: _)) :: l) = (NORMAL_STEP, p, l)
       | step_kind ((p as SMTLIB.S (SMTLIB.Sym "define-fun" :: _)) :: l) = (SKOLEM, p, l)
     fun parse_skolem (SMTLIB.S [SMTLIB.Sym "define-fun", SMTLIB.Sym id,  _, typ,
            SMTLIB.S (SMTLIB.Sym "!" :: t :: [SMTLIB.Key _, SMTLIB.Sym name])]) cx =
          (*replace the name binding by the constant instead of the full term in order to reduce
            the size of the generated terms and therefore the reconstruction time*)
          let val (l, cx) = (fst oo SMTLIB_Proof.extract_and_update_name_bindings) t cx
             |> apsnd (SMTLIB_Proof.update_name_binding (name, SMTLIB.Sym id))
          in
            (mk_raw_node (id ^ veriT_def) veriT_def (SMTLIB.S [SMTLIB.Sym id, typ, l]) [] []
               (SMTLIB.S [SMTLIB.Sym "=", SMTLIB.Sym id, l]) [], cx)
          end
       | parse_skolem (SMTLIB.S [SMTLIB.Sym "define-fun", SMTLIB.Sym id,  _, typ, SMTLIB.S l]) cx =
          let val (l, cx) = (fst oo SMTLIB_Proof.extract_and_update_name_bindings) (SMTLIB.S l ) cx
          in
            (mk_raw_node (id ^ veriT_def) veriT_def (SMTLIB.S [SMTLIB.Sym id, typ, l]) [] []
               (SMTLIB.S [SMTLIB.Sym "=", SMTLIB.Sym id, l]) [], cx)
          end
       | parse_skolem t _ = raise Fail ("unrecognized VeriT proof " ^ \<^make_string> t)
     fun get_id_cx (SMTLIB.S ((SMTLIB.Sym _) :: (SMTLIB.Sym id) :: l), cx) = (id, (l, cx))
       | get_id_cx t = raise Fail ("unrecognized VeriT proof " ^ \<^make_string> t)
     fun get_id (SMTLIB.S ((SMTLIB.Sym _) :: (SMTLIB.Sym id) :: l)) = (id, l)
       | get_id t = raise Fail ("unrecognized VeriT proof " ^ \<^make_string> t)
     fun parse_source (SMTLIB.Key "premises" :: SMTLIB.S source ::l, cx) =
         (SOME (map (fn (SMTLIB.Sym id) => id) source), (l, cx))
       | parse_source (l, cx) = (NONE, (l, cx))
     fun parse_rule (SMTLIB.Key "rule" :: SMTLIB.Sym r :: l, cx) = (r, (l, cx))
       | parse_rule t = raise Fail ("unrecognized VeriT proof " ^ \<^make_string> t)
     fun parse_anchor_step (SMTLIB.S (SMTLIB.Sym "anchor" :: SMTLIB.Key "step" :: SMTLIB.Sym r :: l), cx) = (r, (l, cx))
       | parse_anchor_step t = raise Fail ("unrecognized VeriT proof " ^ \<^make_string> t)
     fun parse_args (SMTLIB.Key "args" :: args :: l, cx) =
           let val ((args, cx), _) = SMTLIB_Proof.extract_and_update_name_bindings args cx
           in (args, (l, cx)) end
       | parse_args (l, cx) = (SMTLIB.S [], (l, cx))
     fun parse_and_clausify_conclusion (SMTLIB.S (SMTLIB.Sym "cl" :: []) :: l, cx) =
           (SMTLIB.Sym "false", (l, cx))
       | parse_and_clausify_conclusion (SMTLIB.S (SMTLIB.Sym "cl" :: concl) :: l, cx) =
           let val (concl, cx) = fold_map (fst oo SMTLIB_Proof.extract_and_update_name_bindings) concl cx
           in (SMTLIB.S (SMTLIB.Sym "or" :: concl), (l, cx)) end
       | parse_and_clausify_conclusion t = raise Fail ("unrecognized VeriT proof " ^ \<^make_string> t)
     val parse_normal_step =
         get_id_cx
         ##> parse_and_clausify_conclusion
         #> rotate_pair
         ##> parse_rule
         #> rotate_pair
         ##> parse_source
         #> rotate_pair
         ##> parse_args
         #> rotate_pair
 
     fun to_raw_node subproof ((((id, concl), rule), prems), args) =
         mk_raw_node id rule args (the_default [] prems) [] concl subproof
     fun at_discharge NONE _ = false
       | at_discharge (SOME id) p = p |> get_id |> fst |> (fn id2 => id = id2)
   in
     case step_kind ls of
         (NO_STEP, _, _) => ([],[], cx)
       | (NORMAL_STEP, p, l) =>
           if at_discharge limit p then ([], ls, cx) else
             let
               val (s, (_, cx)) =  (p, cx)
                 |> parse_normal_step
                 ||> (fn i => i)
                 |>>  (to_raw_node [])
               val (rp, rl, cx) = parse_raw_proof_steps limit l cx
           in (s :: rp, rl, cx) end
       | (ASSUME, p, l) =>
           let
             val (id, t :: []) = p
               |> get_id
             val ((t, cx), _) = SMTLIB_Proof.extract_and_update_name_bindings t cx
             val s = mk_raw_node id input_rule (SMTLIB.S []) [] [] t []
             val (rp, rl, cx) = parse_raw_proof_steps limit l cx
           in (s :: rp, rl, cx) end
       | (ANCHOR, p, l) =>
           let
             val (anchor_id, (anchor_args, (_, cx))) = (p, cx) |> (parse_anchor_step ##> parse_args)
             val (subproof, discharge_step :: remaining_proof, cx) = parse_raw_proof_steps (SOME anchor_id) l cx
             val (curss, (_, cx)) = parse_normal_step (discharge_step, cx)
             val s = to_raw_node subproof (fst curss, anchor_args)
             val (rp, rl, cx) = parse_raw_proof_steps limit remaining_proof cx
           in (s :: rp, rl, cx) end
       | (SKOLEM, p, l) =>
           let
             val (s, cx) = parse_skolem p cx
             val (rp, rl, cx) = parse_raw_proof_steps limit l cx
           in (s :: rp, rl, cx) end
   end
 
 fun proof_ctxt_of_rule "bind" t = t
   | proof_ctxt_of_rule "sko_forall" t = t
   | proof_ctxt_of_rule "sko_ex" t = t
   | proof_ctxt_of_rule "let" t = t
   | proof_ctxt_of_rule "onepoint" t = t
   | proof_ctxt_of_rule _ _ = []
 
 fun args_of_rule "bind" t = t
   | args_of_rule "la_generic" t = t
   | args_of_rule "lia_generic" t = t
   | args_of_rule _ _ = []
 
 fun insts_of_forall_inst "forall_inst" t = map (fn SMTLIB.S [_, SMTLIB.Sym x, a] => (x, a)) t
   | insts_of_forall_inst _ _ = []
 
 fun id_of_last_step prems =
   if null prems then []
   else
     let val VeriT_Replay_Node {id, ...} = List.last prems in [id] end
 
 fun extract_assumptions_from_subproof subproof =
   let fun extract_assumptions_from_subproof (VeriT_Replay_Node {rule, concl, ...}) assms =
     if rule = local_input_rule then concl :: assms else assms
   in
     fold extract_assumptions_from_subproof subproof []
   end
 
 fun normalized_rule_name id rule =
   (case (rule = input_rule, can (unprefix SMTLIB_Interface.assert_prefix) id) of
     (true, true) => normalized_input_rule
   | (true, _) => local_input_rule
   | _ => rule)
 
 fun is_assm_repetition id rule =
   rule = input_rule andalso can (unprefix SMTLIB_Interface.assert_prefix) id
 
 fun extract_skolem ([SMTLIB.Sym var, typ, choice]) = (var, typ, choice)
   | extract_skolem t = raise Fail ("fail to parse type" ^ @{make_string} t)
 
 (* The preprocessing takes care of:
      1. unfolding the shared terms
      2. extract the declarations of skolems to make sure that there are not unfolded
 *)
 fun preprocess compress step =
   let
     fun expand_assms cs =
       map (fn t => case AList.lookup (op =) cs t of NONE => t | SOME a => a)
     fun expand_lonely_arguments (args as SMTLIB.S [SMTLIB.Sym "=", _, _]) = [args]
       | expand_lonely_arguments (SMTLIB.S S) = map (fn x => SMTLIB.S [SMTLIB.Sym "=", x, x]) S
       | expand_lonely_arguments (x as SMTLIB.Sym _) = [SMTLIB.S [SMTLIB.Sym "=", x, x]]
       | expand_lonely_arguments t = [t]
 
     fun preprocess (Raw_VeriT_Node {id, rule, args, prems, concl, subproof, ...}) (cx, remap_assms)  =
       let
         val stripped_args = args
           |> (fn SMTLIB.S args => args)
           |> map
               (fn SMTLIB.S [SMTLIB.Key "=", x, y] => SMTLIB.S [SMTLIB.Sym "=", x, y]
               | x => x)
           |> (rule = "bind" orelse rule = "onepoint") ? flat o (map expand_lonely_arguments)
           |> `(if rule = veriT_def then single o extract_skolem else K [])
           ||> SMTLIB.S
 
         val (subproof, (cx, _)) = fold_map preprocess subproof (cx, remap_assms) |> apfst flat
         val (skolem_names, stripped_args) = stripped_args
         val remap_assms = (if rule = "or" then (id, hd prems) :: remap_assms else remap_assms)
         (* declare variables in the context *)
         val declarations =
            if rule = veriT_def
            then skolem_names |> map (fn (name, _, choice) => (name, choice))
            else []
       in
         if compress andalso rule = "or"
         then ([], (cx, remap_assms))
         else ([Raw_VeriT_Node {id = id, rule = rule, args = stripped_args,
            prems = expand_assms remap_assms prems, declarations = declarations, concl = concl, subproof = subproof}],
           (cx, remap_assms))
       end
   in preprocess step end
 
 fun filter_split _ [] = ([], [])
   | filter_split f (a :: xs) =
      (if f a then apfst (curry op :: a) else apsnd (curry op :: a)) (filter_split f xs)
 
 fun collect_skolem_defs (Raw_VeriT_Node {rule, subproof = subproof, args, ...}) =
-  (if is_skolemisation rule then map (fn id => id ^ veriT_def) (skolems_introduced_by_rule args) else []) @
+  (if is_skolemization rule then map (fn id => id ^ veriT_def) (skolems_introduced_by_rule args) else []) @
   flat (map collect_skolem_defs subproof)
 
 (*The postprocessing does:
   1. translate the terms to Isabelle syntax, taking care of free variables
   2. remove the ambiguity in the proof terms:
        x \<leadsto> y |- x = x
     means y = x. To remove ambiguity, we use the fact that y is a free variable and replace the term
     by:
       xy \<leadsto> y |- xy = x.
     This is now does not have an ambiguity and we can safely move the "xy \<leadsto> y" to the proof
     assumptions.
 *)
 fun postprocess_proof compress ctxt step cx =
   let
     fun postprocess (Raw_VeriT_Node {id, rule, args, prems, declarations, concl, subproof}) (cx, rew) =
     let
       val _ = (SMT_Config.verit_msg ctxt) (fn () => @{print} ("id =", id, "concl =", concl))
 
       val globally_bound_vars = declared_csts cx rule args
       val cx = fold (update_binding o (fn (s, typ) => (s, Term (Free (s, type_of cx typ)))))
            globally_bound_vars cx
 
       (*find rebound variables specific to the LHS of the equivalence symbol*)
       val bound_vars = bound_vars_by_rule cx rule args
 
       val rhs_vars = fold (fn [t', t] => t <> t' ? (curry (op ::) t) | _ => fn x => x) bound_vars []
       fun not_already_bound cx t = SMTLIB_Proof.lookup_binding cx t = None andalso
           not (member (op =) rhs_vars t)
       val (shadowing_vars, rebound_lhs_vars) = bound_vars
         |> filter_split (fn [t, _] => not_already_bound cx t | _ => true)
         |>> map (single o hd)
         |>> (fn vars => vars @ map (fn [_, t] => [t] | _ => []) bound_vars)
         |>> flat
       val subproof_rew = fold (fn [t, t'] => curry (op ::) (t, t ^ t'))
         rebound_lhs_vars rew
       val subproof_rewriter = fold (fn (t, t') => synctatic_rew_in_lhs_subst t t')
          subproof_rew
 
       val ((concl, bounds), cx') = node_of concl cx
 
       val extra_lhs_vars = map (fn [a,b] => (a, a^b)) rebound_lhs_vars
 
       (* postprocess conclusion *)
       val concl = SMTLIB_Isar.unskolemize_names ctxt (subproof_rewriter concl)
 
       val _ = (SMT_Config.verit_msg ctxt) (fn () => \<^print> ("id =", id, "concl =", concl))
       val _ = (SMT_Config.verit_msg ctxt) (fn () => \<^print> ("id =", id, "cx' =", cx',
         "bound_vars =", bound_vars))
 
       val bound_tvars =
         map (fn s => (s, the (find_type_in_formula concl s)))
          (shadowing_vars @ map snd extra_lhs_vars)
       val subproof_cx =
          add_bound_variables_to_ctxt concl (shadowing_vars @ map snd extra_lhs_vars) cx
 
       fun could_unify (Bound i, Bound j) = i = j
         | could_unify (Var v, Var v') = v = v'
         | could_unify (Free v, Free v') = v = v'
         | could_unify (Const (v, ty), Const (v', ty')) = v = v' andalso ty = ty'
         | could_unify (Abs (_, ty, bdy), Abs (_, ty', bdy')) = ty = ty' andalso could_unify (bdy, bdy')
         | could_unify (u $ v, u' $ v') = could_unify (u, u') andalso could_unify (v, v')
         | could_unify _ = false
       fun is_alpha_renaming t =
           t
           |> HOLogic.dest_Trueprop
           |> HOLogic.dest_eq
           |> could_unify
         handle TERM _ => false
       val alpha_conversion = rule = "bind" andalso is_alpha_renaming concl
 
       val can_remove_subproof =
-        compress andalso (is_skolemisation rule orelse alpha_conversion)
+        compress andalso (is_skolemization rule orelse alpha_conversion)
       val (fixed_subproof : veriT_replay_node list, _) =
          fold_map postprocess (if can_remove_subproof then [] else subproof)
            (subproof_cx, subproof_rew)
 
       val unsk_and_rewrite = SMTLIB_Isar.unskolemize_names ctxt o subproof_rewriter
 
       (* postprocess assms *)
       val stripped_args = args |> (fn SMTLIB.S S => S)
       val sanitized_args = proof_ctxt_of_rule rule stripped_args
 
       val arg_cx =
         subproof_cx
         |> add_bound_variables_to_ctxt concl (shadowing_vars @ map fst extra_lhs_vars)
       val (termified_args, _) = fold_map node_of sanitized_args arg_cx |> apfst (map fst)
       val normalized_args = map unsk_and_rewrite termified_args
 
       val subproof_assms = proof_ctxt_of_rule rule normalized_args
 
       (* postprocess arguments *)
       val rule_args = args_of_rule rule stripped_args
       val (termified_args, _) = fold_map term_of rule_args subproof_cx
       val normalized_args = map unsk_and_rewrite termified_args
       val rule_args = map subproof_rewriter normalized_args
 
       val raw_insts = insts_of_forall_inst rule stripped_args
       fun termify_term (x, t) cx = let val (t, cx) = term_of t cx in ((x, t), cx) end
       val (termified_args, _) = fold_map termify_term raw_insts subproof_cx
       val insts = Symtab.empty
         |> fold (fn (x, t) => fn insts => Symtab.update_new (x, t) insts) termified_args
         |> Symtab.map (K unsk_and_rewrite)
 
       (* declarations *)
       val (declarations, _) = fold_map termify_term declarations cx
         |> apfst (map (apsnd unsk_and_rewrite))
 
       (* fix step *)
       val bound_t = bounds
         |> map (fn s => (s, the (find_type_in_formula concl s)))
 
-      val skolem_defs = (if is_skolemisation rule
+      val skolem_defs = (if is_skolemization rule
          then map (fn id => id ^ veriT_def) (skolems_introduced_by_rule args) else [])
-      val skolems_of_subproof = (if is_skolemisation rule
+      val skolems_of_subproof = (if is_skolemization rule
          then flat (map collect_skolem_defs subproof) else [])
       val fixed_prems =
         prems @ (if is_assm_repetition id rule then [id] else []) @
         skolem_defs @ skolems_of_subproof @ (id_of_last_step fixed_subproof)
 
       (* fix subproof *)
       val normalized_rule = normalized_rule_name id rule
         |> (if compress andalso alpha_conversion then K "refl" else I)
 
       val extra_assms2 =
         (if rule = subproof_rule then extract_assumptions_from_subproof fixed_subproof else [])
 
       val step = mk_replay_node id normalized_rule rule_args fixed_prems subproof_assms concl
         bound_t insts declarations (bound_tvars, subproof_assms, extra_assms2, fixed_subproof)
 
     in
        (step, (cx', rew))
     end
   in
     postprocess step (cx, [])
     |> (fn (step, (cx, _)) => (step, cx))
    end
 
 
 val linearize_proof =
   let
+    fun map_node_concl f (VeriT_Node {id, rule, prems, proof_ctxt, concl}) =
+       mk_node id rule prems proof_ctxt (f concl)
     fun linearize (VeriT_Replay_Node {id = id, rule = rule, args = _, prems = prems,
         proof_ctxt = proof_ctxt, concl = concl, bounds = bounds, insts = _, declarations = _,
-        subproof = (_, _, _, subproof)}) =
+        subproof = (bounds', assms, inputs, subproof)}) =
       let
+        val bounds = distinct (op =) bounds
+        val bounds' = distinct (op =) bounds'
         fun mk_prop_of_term concl =
           concl |> fastype_of concl = \<^typ>\<open>bool\<close> ? curry (op $) \<^term>\<open>Trueprop\<close>
         fun remove_assumption_id assumption_id prems =
           filter_out (curry (op =) assumption_id) prems
+        fun add_assumption assumption concl =
+          \<^const>\<open>Pure.imp\<close> $ mk_prop_of_term assumption $ mk_prop_of_term concl
         fun inline_assumption assumption assumption_id
-            (VeriT_Node {id, rule, prems, proof_ctxt, concl, bounds}) =
+            (VeriT_Node {id, rule, prems, proof_ctxt, concl}) =
           mk_node id rule (remove_assumption_id assumption_id prems) proof_ctxt
-            (\<^const>\<open>Pure.imp\<close> $ mk_prop_of_term assumption $ mk_prop_of_term concl) bounds
+            (add_assumption assumption concl)
         fun find_input_steps_and_inline [] = []
           | find_input_steps_and_inline
-              (VeriT_Node {id = id', rule, prems, concl, bounds, ...} :: steps) =
+              (VeriT_Node {id = id', rule, prems, concl, ...} :: steps) =
             if rule = input_rule then
               find_input_steps_and_inline (map (inline_assumption concl id') steps)
             else
-              mk_node (id') rule prems [] concl bounds :: find_input_steps_and_inline steps
+              mk_node (id') rule prems [] concl :: find_input_steps_and_inline steps
 
-        val subproof = flat (map linearize subproof)
-        val subproof' = find_input_steps_and_inline subproof
+        fun free_bounds bounds (concl) =
+          fold (fn (var, typ) => fn t => Logic.all (Free (var, typ)) t) bounds concl
+        val subproof = subproof
+          |> flat o map linearize
+          |> map (map_node_concl (fold add_assumption (assms @ inputs)))
+          |> map (map_node_concl (free_bounds (bounds @ bounds')))
+          |> find_input_steps_and_inline
+        val concl = free_bounds bounds concl
       in
-        subproof' @ [mk_node id rule prems proof_ctxt concl (map fst bounds)]
+        subproof @ [mk_node id rule prems proof_ctxt concl]
       end
   in linearize end
 
+fun rule_of (VeriT_Replay_Node {rule,...}) = rule
+fun subproof_of (VeriT_Replay_Node {subproof = (_, _, _, subproof),...}) = subproof
+
+
+(* Massage Skolems for Sledgehammer.
+
+We have to make sure that there is an "arrow" in the graph for skolemization steps.
+
+
+A. The normal easy case
+
+This function detects the steps of the form
+  P \<longleftrightarrow> Q :skolemization
+  Q       :resolution with P
+and replace them by
+  Q       :skolemization
+Throwing away the step "P \<longleftrightarrow> Q" completely. This throws away a lot of information, but it does not
+matter too much for Sledgehammer.
+
+
+B. Skolems in subproofs
+Supporting this is more or less hopeless as long as the Isar reconstruction of Sledgehammer
+does not support more features like definitions. veriT is able to generate proofs with skolemization
+happening in subproofs inside the formula. 
+  (assume "A \<or> P"
+   ...
+   P \<longleftrightarrow> Q :skolemization in the subproof
+   ...)
+  hence A \<or> P \<longrightarrow> A \<or> Q :lemma
+  ...
+  R :something with some rule
+and replace them by
+  R :skolemization with some rule
+Without any subproof
+*)
+fun remove_skolem_definitions_proof steps =
+  let
+    fun replace_equivalent_by_imp (judgement $ ((Const(\<^const_name>\<open>HOL.eq\<close>, typ) $ arg1) $ arg2)) =
+       judgement $ ((Const(\<^const_name>\<open>HOL.implies\<close>, typ) $ arg1) $ arg2)
+     | replace_equivalent_by_imp a = a (*This case is probably wrong*)
+    fun remove_skolem_definitions (VeriT_Replay_Node {id = id, rule = rule, args = args,
+         prems = prems,
+        proof_ctxt = proof_ctxt, concl = concl, bounds = bounds, insts = insts,
+        declarations = declarations,
+        subproof = (vars, assms', extra_assms', subproof)}) (prems_to_remove, skolems) =
+    let
+      val prems = prems
+        |> filter_out (member (op =) prems_to_remove)
+      val trivial_step = is_SH_trivial rule
+      fun has_skolem_substep st NONE = if is_skolemization (rule_of st) then SOME (rule_of st)
+             else fold has_skolem_substep (subproof_of st) NONE
+        | has_skolem_substep _ a = a
+      val promote_to_skolem = exists (fn t => member (op =) skolems t) prems
+      val promote_from_assms = fold has_skolem_substep subproof NONE <> NONE
+      val promote_step = promote_to_skolem orelse promote_from_assms
+      val skolem_step_to_skip = is_skolemization rule orelse 
+        (promote_from_assms andalso length prems > 1)
+      val is_skolem = is_skolemization rule orelse promote_step
+      val prems = prems
+        |> filter_out (fn t => member (op =) skolems t)
+        |> is_skolem ? filter_out (String.isPrefix id)
+      val rule = (if promote_step then default_skolem_rule else rule)
+      val subproof = subproof
+        |> (is_skolem ? K []) (*subproofs of skolemization steps are useless for SH*)
+        |> map (fst o (fn st => remove_skolem_definitions st (prems_to_remove, skolems)))
+             (*no new definitions in subproofs*)
+        |> flat
+      val concl = concl
+        |> is_skolem ? replace_equivalent_by_imp
+      val step = (if skolem_step_to_skip orelse rule = veriT_def orelse trivial_step then []
+        else mk_replay_node id rule args prems proof_ctxt concl bounds insts declarations
+            (vars, assms', extra_assms', subproof)
+          |> single)
+      val defs = (if rule = veriT_def orelse trivial_step then id :: prems_to_remove
+         else prems_to_remove)
+      val skolems = (if skolem_step_to_skip then id :: skolems else skolems)
+    in
+      (step, (defs, skolems))
+    end
+  in
+    fold_map remove_skolem_definitions steps ([], [])
+    |> fst
+    |> flat
+  end
+
 local
   fun import_proof_and_post_process typs funs lines ctxt =
     let
       val compress = SMT_Config.compress_verit_proofs ctxt
       val smtlib_lines_without_qm =
         lines
         |> map single
         |> map SMTLIB.parse
         |> map remove_all_qm2
       val (raw_steps, _, _) = 
         parse_raw_proof_steps NONE smtlib_lines_without_qm SMTLIB_Proof.empty_name_binding
       
       fun process step (cx, cx') =
         let fun postprocess step (cx, cx') =
           let val (step, cx) = postprocess_proof compress ctxt step cx
           in (step, (cx, cx')) end
         in uncurry (fold_map postprocess) (preprocess compress step (cx, cx')) end
-       val step =
+      val step =
         (empty_context ctxt typs funs, [])
         |> fold_map process raw_steps
         |> (fn (steps, (cx, _)) => (flat steps, cx))
     in step end
 in
 
 fun parse typs funs lines ctxt =
   let
     val (u, env) = import_proof_and_post_process typs funs lines ctxt
-    val t = flat (map linearize_proof u)
-    fun node_to_step (VeriT_Node {id, rule, prems, concl, bounds, ...}) =
-      mk_step id rule prems [] concl bounds
+    val t = u
+       |> remove_skolem_definitions_proof
+       |> flat o (map linearize_proof)
+    fun node_to_step (VeriT_Node {id, rule, prems, concl, ...}) =
+      mk_step id rule prems [] concl []
   in
     (map node_to_step t, ctxt_of env)
   end
 
 fun parse_replay typs funs lines ctxt =
   let
     val (u, env) = import_proof_and_post_process typs funs lines ctxt
     val _ = (SMT_Config.verit_msg ctxt) (fn () => \<^print> u)
   in
     (u, ctxt_of env)
   end
 end
 
 end;
diff --git a/src/HOL/Tools/SMT/verit_replay.ML b/src/HOL/Tools/SMT/verit_replay.ML
--- a/src/HOL/Tools/SMT/verit_replay.ML
+++ b/src/HOL/Tools/SMT/verit_replay.ML
@@ -1,319 +1,319 @@
 (*  Title:      HOL/Tools/SMT/verit_replay.ML
     Author:     Mathias Fleury, MPII
 
 VeriT proof parsing and replay.
 *)
 
 signature VERIT_REPLAY =
 sig
   val replay: Proof.context -> SMT_Translate.replay_data -> string list -> thm
 end;
 
 structure Verit_Replay: VERIT_REPLAY =
 struct
 
 fun subst_only_free pairs =
   let
      fun substf u =
         (case Termtab.lookup pairs u of
           SOME u' => u'
         | NONE => 
           (case u of
             (Abs(a,T,t)) => Abs(a, T, substf t)
           | (t$u') => substf t $ substf u'
           | u => u))
   in substf end;
 
 
 fun under_fixes f unchanged_prems (prems, nthms) names args insts decls (concl, ctxt) =
   let
     val thms1 = unchanged_prems @ map (SMT_Replay.varify ctxt) prems
     val _ =  SMT_Config.verit_msg ctxt (fn () => \<^print>  ("names =", names))
     val thms2 = map snd nthms
     val _ = SMT_Config.verit_msg ctxt (fn () => \<^print> ("prems=", prems))
     val _ = SMT_Config.verit_msg ctxt (fn () => \<^print> ("nthms=", nthms))
     val _ = SMT_Config.verit_msg ctxt (fn () => \<^print> ("thms1=", thms1))
     val _ = SMT_Config.verit_msg ctxt (fn () => \<^print> ("thms2=", thms2))
   in (f ctxt (thms1 @ thms2) args insts decls concl) end
 
 
 (** Replaying **)
 
 fun replay_thm method_for rewrite_rules ll_defs ctxt assumed unchanged_prems prems nthms
     concl_transformation global_transformation args insts
     (Verit_Proof.VeriT_Replay_Node {id, rule, concl, bounds, declarations = decls, ...}) =
   let
     val _ = SMT_Config.verit_msg ctxt (fn () => \<^print> id)
     val rewrite = let val thy = Proof_Context.theory_of (empty_simpset ctxt) in
         Raw_Simplifier.rewrite_term thy rewrite_rules []
         #> not (null ll_defs andalso Verit_Proof.keep_raw_lifting rule) ? SMTLIB_Isar.unlift_term ll_defs
       end
     val rewrite_concl = if Verit_Proof.keep_app_symbols rule then
           filter (curry Term.could_unify (Thm.concl_of @{thm SMT.fun_app_def}) o Thm.concl_of) rewrite_rules
         else rewrite_rules
     val post = let val thy = Proof_Context.theory_of (empty_simpset ctxt) in
         Raw_Simplifier.rewrite_term thy rewrite_concl []
         #> Object_Logic.atomize_term ctxt
         #> not (null ll_defs) ? SMTLIB_Isar.unlift_term ll_defs
         #> SMTLIB_Isar.unskolemize_names ctxt
         #> HOLogic.mk_Trueprop
       end
     val concl = concl
       |> Term.subst_free concl_transformation
       |> subst_only_free global_transformation
       |> post
   in
     if rule = Verit_Proof.input_rule then
       (case Symtab.lookup assumed id of
         SOME (_, thm) => thm
       | _ => raise Fail ("assumption " ^ @{make_string} id ^ " not found"))
     else
       under_fixes (method_for rule) unchanged_prems
         (prems, nthms) (map fst bounds)
         (map rewrite args)
         (Symtab.map (K rewrite) insts)
         decls
         (concl, ctxt)
       |> Simplifier.simplify (empty_simpset ctxt addsimps rewrite_rules)
   end
 
 fun add_used_asserts_in_step (Verit_Proof.VeriT_Replay_Node {prems,
     subproof = (_, _, _, subproof), ...}) =
   union (op =) (map_filter (try SMTLIB_Interface.assert_index_of_name) prems @
      flat (map (fn x => add_used_asserts_in_step x []) subproof))
 
 fun remove_rewrite_rules_from_rules n =
   (fn (step as Verit_Proof.VeriT_Replay_Node {id, ...}) =>
     (case try SMTLIB_Interface.assert_index_of_name id of
       NONE => SOME step
     | SOME a => if a < n then NONE else SOME step))
 
 
 fun replay_theorem_step rewrite_rules ll_defs assumed inputs proof_prems
   (step as Verit_Proof.VeriT_Replay_Node {id, rule, prems, bounds, args, insts,
      subproof = (fixes, assms, input, subproof), concl, ...}) state =
   let
     val (proofs, stats, ctxt, concl_tranformation, global_transformation) = state
     val (_, ctxt) = Variable.variant_fixes (map fst bounds) ctxt
       |> (fn (names, ctxt) => (names,
         fold Variable.declare_term [SMTLIB_Isar.unskolemize_names ctxt concl] ctxt))
 
     val (names, sub_ctxt) = Variable.variant_fixes (map fst fixes) ctxt
        ||> fold Variable.declare_term (map Free fixes)
     val export_vars = concl_tranformation @
        (ListPair.zip (map Free fixes, map Free (ListPair.zip (names, map snd fixes))))
 
     val post = let val thy = Proof_Context.theory_of (empty_simpset ctxt) in
         Raw_Simplifier.rewrite_term thy ((if Verit_Proof.keep_raw_lifting rule then tl rewrite_rules else rewrite_rules)) []
         #> Object_Logic.atomize_term ctxt
         #> not (null ll_defs andalso Verit_Proof.keep_raw_lifting rule) ? SMTLIB_Isar.unlift_term ll_defs
         #> SMTLIB_Isar.unskolemize_names ctxt
         #> HOLogic.mk_Trueprop
       end
     val assms = map (subst_only_free global_transformation o Term.subst_free (export_vars) o post) assms
     val input = map (subst_only_free global_transformation o Term.subst_free (export_vars) o post) input
     val (all_proof_prems', sub_ctxt2) = Assumption.add_assumes (map (Thm.cterm_of sub_ctxt) (assms @ input))
       sub_ctxt
     fun is_refl thm = Thm.concl_of thm |> (fn (_ $ t) => t) |> HOLogic.dest_eq |> (op =) handle TERM _=> false
     val all_proof_prems' =
         all_proof_prems'
         |> filter_out is_refl
     val proof_prems' = take (length assms) all_proof_prems'
     val input = drop (length assms) all_proof_prems'
     val all_proof_prems = proof_prems @ proof_prems'
     val replay = replay_theorem_step rewrite_rules ll_defs assumed (input @ inputs) all_proof_prems
     val (proofs', stats, _, _, sub_global_rew) =
        fold replay subproof (proofs, stats, sub_ctxt2, export_vars, global_transformation)
 
     val export_thm = singleton (Proof_Context.export sub_ctxt2 ctxt)
 
     (*for sko_ex and sko_forall, assumptions are in proofs',  but the definition of the skolem
        function is in proofs *)
     val nthms = prems
       |> map (apsnd export_thm) o map_filter (Symtab.lookup (if (null subproof) then proofs else proofs'))
-    val nthms' = (if Verit_Proof.is_skolemisation rule
+    val nthms' = (if Verit_Proof.is_skolemization rule
          then prems else [])
       |> map_filter (Symtab.lookup proofs)
     val args = map (Term.subst_free concl_tranformation o subst_only_free global_transformation) args
     val insts = Symtab.map (K (Term.subst_free concl_tranformation o subst_only_free global_transformation)) insts
     val proof_prems =
        if Verit_Replay_Methods.requires_subproof_assms prems rule then proof_prems else []
     val local_inputs =
        if Verit_Replay_Methods.requires_local_input prems rule then input @ inputs else []
     val replay = Timing.timing (replay_thm Verit_Replay_Methods.method_for rewrite_rules ll_defs
        ctxt assumed [] (proof_prems @ local_inputs) (nthms @ nthms') concl_tranformation
        global_transformation args insts)
 
     val ({elapsed, ...}, thm) =
       SMT_Config.with_time_limit ctxt SMT_Config.reconstruction_step_timeout replay step
         handle Timeout.TIMEOUT _ => raise SMT_Failure.SMT SMT_Failure.Time_Out
     val stats' = Symtab.cons_list (rule, Time.toNanoseconds elapsed) stats
 (*     val _ = ((Time.toMilliseconds elapsed > 10 andalso (rule = "cong")) ? @{print})
         ("WARNING slow " ^ id ^ @{make_string} rule ^ ": " ^ string_of_int (Time.toMilliseconds elapsed) ^ " "
          ^ @{make_string} (proof_prems @ local_inputs))
     val _ = ((Time.toMilliseconds elapsed > 10 andalso (rule = "cong")) ? @{print})
         ( (proof_prems @ local_inputs))
     val _ = ((Time.toMilliseconds elapsed > 10 andalso (rule = "cong")) ? @{print})
         thm
     val _ = ((Time.toMilliseconds elapsed > 40) ? @{print})
         ("WARNING slow " ^ id ^ @{make_string} rule ^ ": " ^ string_of_int (Time.toMilliseconds elapsed)) *)
     val proofs = Symtab.update (id, (map fst bounds, thm)) proofs
   in (proofs, stats', ctxt,
        concl_tranformation, sub_global_rew) end
 
 fun replay_definition_step rewrite_rules ll_defs _ _ _
   (Verit_Proof.VeriT_Replay_Node {id, declarations = raw_declarations, subproof = (_, _, _, subproof), ...}) state =
   let
     val _ = if null subproof then ()
           else raise (Fail ("unrecognized veriT proof, definition has a subproof"))
     val (proofs, stats, ctxt, concl_tranformation, global_transformation) = state
     val global_transformer = subst_only_free global_transformation
     val rewrite = let val thy = Proof_Context.theory_of ctxt in
         Raw_Simplifier.rewrite_term thy (rewrite_rules) []
         #> not (null ll_defs) ? SMTLIB_Isar.unlift_term ll_defs
       end
     val start0 = Timing.start ()
     val declaration = map (apsnd (rewrite o global_transformer)) raw_declarations
     val (names, ctxt) = Variable.variant_fixes (map fst declaration) ctxt
        ||> fold Variable.declare_term (map Free (map (apsnd fastype_of) declaration))
     val old_names = map Free (map (fn (a, b) => (a, fastype_of b)) declaration)
     val new_names = map Free (ListPair.zip (names, map (fastype_of o snd) declaration))
     fun update_mapping (a, b) tab = 
           if a <> b andalso Termtab.lookup tab a = NONE
           then Termtab.update_new (a, b) tab else tab
     val global_transformation = global_transformation 
      |> fold update_mapping (ListPair.zip (old_names, new_names))
     val global_transformer = subst_only_free global_transformation
 
     val generate_definition =
       (fn (name, term) => (HOLogic.mk_Trueprop
         (Const(\<^const_name>\<open>HOL.eq\<close>, fastype_of term --> fastype_of term --> @{typ bool}) $
             Free (name, fastype_of term) $ term)))
       #> global_transformer
       #> Thm.cterm_of ctxt
     val decls = map generate_definition declaration
     val (defs, ctxt) = Assumption.add_assumes decls ctxt
     val thms_with_old_name = ListPair.zip (map fst declaration, defs)
     val proofs = fold
       (fn (name, thm) => Symtab.update (id, ([name], @{thm sym} OF [thm])))
       thms_with_old_name proofs
     val total = Time.toNanoseconds (#elapsed (Timing.result start0))
     val stats = Symtab.cons_list ("choice", total) stats
   in (proofs, stats, ctxt, concl_tranformation, global_transformation) end
 
 
 fun replay_assumed assms ll_defs rewrite_rules stats ctxt term =
   let
     val rewrite = let val thy = Proof_Context.theory_of (empty_simpset ctxt) in
         Raw_Simplifier.rewrite_term thy rewrite_rules []
         #> not (null ll_defs) ? SMTLIB_Isar.unlift_term ll_defs
       end
     val replay = Timing.timing (SMT_Replay_Methods.prove ctxt (rewrite term))
     val ({elapsed, ...}, thm) =
       SMT_Config.with_time_limit ctxt SMT_Config.reconstruction_step_timeout replay
          (fn _ => Method.insert_tac ctxt (map snd assms) THEN' Classical.fast_tac ctxt)
         handle Timeout.TIMEOUT _ => raise SMT_Failure.SMT SMT_Failure.Time_Out
     val stats' = Symtab.cons_list (Verit_Proof.input_rule, Time.toNanoseconds elapsed) stats
   in
     (thm, stats')
   end
 
 
 fun replay_step rewrite_rules ll_defs assumed inputs proof_prems
   (step as Verit_Proof.VeriT_Replay_Node {rule, ...}) state =
   if rule = Verit_Proof.veriT_def
   then replay_definition_step rewrite_rules ll_defs assumed inputs proof_prems step state
   else replay_theorem_step rewrite_rules ll_defs assumed inputs proof_prems step state
 
 
 fun replay outer_ctxt
     ({context = ctxt, typs, terms, rewrite_rules, assms, ll_defs, ...} : SMT_Translate.replay_data)
      output =
   let
     val rewrite_rules =
       filter_out (fn thm => Term.could_unify (Thm.prop_of @{thm verit_eq_true_simplify},
           Thm.prop_of thm))
         rewrite_rules
     val num_ll_defs = length ll_defs
     val index_of_id = Integer.add (~ num_ll_defs)
     val id_of_index = Integer.add num_ll_defs
 
     val start0 = Timing.start ()
     val (actual_steps, ctxt2) =
       Verit_Proof.parse_replay typs terms output ctxt
     val parsing_time = Time.toNanoseconds (#elapsed (Timing.result start0))
 
     fun step_of_assume (j, (_, th)) =
       Verit_Proof.VeriT_Replay_Node {
         id = SMTLIB_Interface.assert_name_of_index (id_of_index j),
         rule = Verit_Proof.input_rule,
         args = [],
         prems = [],
         proof_ctxt = [],
         concl = Thm.prop_of th
           |> Raw_Simplifier.rewrite_term (Proof_Context.theory_of
                (empty_simpset ctxt addsimps rewrite_rules)) rewrite_rules [],
         bounds = [],
         insts = Symtab.empty,
         declarations = [],
         subproof = ([], [], [], [])}
     val used_assert_ids = fold add_used_asserts_in_step actual_steps []
     fun normalize_tac ctxt = let val thy = Proof_Context.theory_of (empty_simpset ctxt) in
       Raw_Simplifier.rewrite_term thy rewrite_rules [] end
     val used_assm_js =
       map_filter (fn id => let val i = index_of_id id in if i >= 0 then SOME (i, nth assms i)
           else NONE end)
         used_assert_ids
 
     val assm_steps = map step_of_assume used_assm_js
 
     fun extract (Verit_Proof.VeriT_Replay_Node {id, rule, concl, bounds, ...}) =
          (id, rule, concl, map fst bounds)
     fun cond rule = rule = Verit_Proof.input_rule
     val add_asssert = SMT_Replay.add_asserted Symtab.update Symtab.empty extract cond
     val ((_, _), (ctxt3, assumed)) =
       add_asssert outer_ctxt rewrite_rules assms
         (map_filter (remove_rewrite_rules_from_rules num_ll_defs) assm_steps) ctxt2
 
     val used_rew_js =
       map_filter (fn id => let val i = index_of_id id in if i < 0
           then SOME (id, normalize_tac ctxt (nth ll_defs id)) else NONE end)
         used_assert_ids
     val (assumed, stats) = fold (fn ((id, thm)) => fn (assumed, stats) =>
            let val (thm, stats) = replay_assumed assms ll_defs rewrite_rules stats ctxt thm
            in (Symtab.update (SMTLIB_Interface.assert_name_of_index id, ([], thm)) assumed, stats)
            end)
          used_rew_js (assumed, Symtab.cons_list ("parsing", parsing_time) Symtab.empty)
 
     val ctxt4 =
       ctxt3
       |> put_simpset (SMT_Replay.make_simpset ctxt3 [])
       |> Config.put SAT.solver (Config.get ctxt3 SMT_Config.sat_solver)
     val len = Verit_Proof.number_of_steps actual_steps
     fun steps_with_depth _ [] = []
       | steps_with_depth i (p :: ps) = (i +  Verit_Proof.number_of_steps [p], p) ::
           steps_with_depth (i +  Verit_Proof.number_of_steps [p]) ps
     val actual_steps = steps_with_depth 0 actual_steps
     val start = Timing.start ()
     val print_runtime_statistics = SMT_Replay.intermediate_statistics ctxt4 start len
     fun blockwise f (i, x) (next, y) =
       (if i > next then print_runtime_statistics i else ();
        (if i > next then i + 10 else next, f x y))
     val global_transformation : term Termtab.table = Termtab.empty
     val (_, (proofs, stats, ctxt5, _, _)) =
       fold (blockwise (replay_step rewrite_rules ll_defs assumed [] [])) actual_steps
         (1, (assumed, stats, ctxt4, [], global_transformation))
     val total = Time.toMilliseconds (#elapsed (Timing.result start))
     val (_, (_, Verit_Proof.VeriT_Replay_Node {id, ...})) = split_last actual_steps
     val _ = print_runtime_statistics len
     val thm_with_defs = Symtab.lookup proofs id |> the |> snd
       |> singleton (Proof_Context.export ctxt5 outer_ctxt)
     val _ = SMT_Config.statistics_msg ctxt5
       (Pretty.string_of o SMT_Replay.pretty_statistics "veriT" total) stats
     val _ = SMT_Replay.spying (SMT_Config.spy_verit ctxt) ctxt
       (fn () => SMT_Replay.print_stats (Symtab.dest stats)) "spy_verit"
   in
     Verit_Replay_Methods.discharge ctxt [thm_with_defs] @{term False}
   end
 
 end
diff --git a/src/HOL/Tools/SMT/verit_replay_methods.ML b/src/HOL/Tools/SMT/verit_replay_methods.ML
--- a/src/HOL/Tools/SMT/verit_replay_methods.ML
+++ b/src/HOL/Tools/SMT/verit_replay_methods.ML
@@ -1,1179 +1,1180 @@
 (*  Title:      HOL/Tools/SMT/verit_replay_methods.ML
     Author:     Mathias Fleury, MPII, JKU
 
 Proof method for replaying veriT proofs.
 *)
 
 signature VERIT_REPLAY_METHODS =
 sig
   (*methods for verit proof rules*)
   val method_for: string -> Proof.context -> thm list -> term list -> term Symtab.table ->
      (string * term) list -> term -> thm
 
   val requires_subproof_assms : string list -> string -> bool
   val requires_local_input: string list -> string -> bool
   val eq_congruent_pred: Proof.context -> 'a -> term -> thm
   val discharge: Proof.context -> thm list -> term -> thm
 end;
 
 
 structure Verit_Replay_Methods: VERIT_REPLAY_METHODS =
 struct
 
 (*Some general comments on the proof format:
   1. Double negations are not always removed. This means for example that the equivalence rules
      cannot assume that the double negations have already been removed. Therefore, we match the
      term, instantiate the theorem, then use simp (to remove double negations), and finally use
      assumption.
   2. The reconstruction for rule forall_inst is buggy and tends to be very fragile, because the rule
      is doing much more that is supposed to do. Moreover types can make trivial goals (for the
      boolean structure) impossible to prove.
   3. Duplicate literals are sometimes removed, mostly by the SAT solver.
 
   Rules unsupported on purpose:
     * Distinct_Elim, XOR, let (we don't need them).
     * deep_skolemize (because it is not clear if verit still generates using it).
 *)
 
 datatype verit_rule =
    False | True |
 
    (*input: a repeated (normalized) assumption of  assumption of in a subproof*)
    Normalized_Input | Local_Input |
    (*Subproof:*)
    Subproof |
    (*Conjunction:*)
    And | Not_And | And_Pos | And_Neg |
    (*Disjunction""*)
    Or | Or_Pos | Not_Or | Or_Neg |
    (*Disjunction:*)
    Implies | Implies_Neg1 | Implies_Neg2 | Implies_Pos | Not_Implies1 | Not_Implies2 |
    (*Equivalence:*)
    Equiv_neg1 | Equiv_pos1 | Equiv_pos2 | Equiv_neg2 | Not_Equiv1 | Not_Equiv2 | Equiv1 | Equiv2 |
    (*If-then-else:*)
    ITE_Pos1 | ITE_Pos2 | ITE_Neg1 | ITE_Neg2 | Not_ITE1 | Not_ITE2 | ITE_Intro | ITE1 | ITE2 |
    (*Equality:*)
    Eq_Congruent | Eq_Reflexive | Eq_Transitive | Eq_Congruent_Pred | Trans |  Refl |  Cong |
    (*Arithmetics:*)
    LA_Disequality | LA_Generic | LA_Tautology |  LIA_Generic | LA_Totality | LA_RW_Eq |
    NLA_Generic |
    (*Quantifiers:*)
    Forall_Inst | Qnt_Rm_Unused | Qnt_Join | Onepoint | Bind | Skolem_Forall | Skolem_Ex |
    (*Resolution:*)
    Theory_Resolution | Resolution |
    (*Temporary rules, that the verit developpers want to remove:*)
    AC_Simp |
    Bfun_Elim |
    Qnt_CNF |
    (*Used to introduce skolem constants*)
    Definition |
    (*Former cong rules*)
    Bool_Simplify | Or_Simplify | Not_Simplify | And_Simplify | Equiv_Simplify |
    Implies_Simplify | Connective_Def | Minus_Simplify | Comp_Simplify |
    Eq_Simplify | ITE_Simplify | Sum_Simplify | Prod_Simplify |
    Qnt_Simplify | Not_Not | Tautological_Clause | Duplicate_Literals |
    (*Unsupported rule*)
    Unsupported
 
 
 fun verit_rule_of "bind" = Bind
   | verit_rule_of "cong" = Cong
   | verit_rule_of "refl" = Refl
   | verit_rule_of "equiv1" = Equiv1
   | verit_rule_of "equiv2" = Equiv2
   | verit_rule_of "equiv_pos1" = Equiv_pos1
   | verit_rule_of "equiv_pos2" = Equiv_pos2
   | verit_rule_of "equiv_neg1" = Equiv_neg1
   | verit_rule_of "equiv_neg2" = Equiv_neg2
   | verit_rule_of "sko_forall" = Skolem_Forall
   | verit_rule_of "sko_ex" = Skolem_Ex
   | verit_rule_of "eq_reflexive" = Eq_Reflexive
   | verit_rule_of "th_resolution" = Theory_Resolution
   | verit_rule_of "forall_inst" = Forall_Inst
   | verit_rule_of "implies_pos" = Implies_Pos
   | verit_rule_of "or" = Or
   | verit_rule_of "not_or" = Not_Or
   | verit_rule_of "resolution" = Resolution
-  | verit_rule_of "eq_congruent" = Eq_Congruent
   | verit_rule_of "trans" = Trans
   | verit_rule_of "false" = False
   | verit_rule_of "ac_simp" = AC_Simp
   | verit_rule_of "and" = And
   | verit_rule_of "not_and" = Not_And
   | verit_rule_of "and_pos" = And_Pos
   | verit_rule_of "and_neg" = And_Neg
   | verit_rule_of "or_pos" = Or_Pos
   | verit_rule_of "or_neg" = Or_Neg
   | verit_rule_of "not_equiv1" = Not_Equiv1
   | verit_rule_of "not_equiv2" = Not_Equiv2
   | verit_rule_of "not_implies1" = Not_Implies1
   | verit_rule_of "not_implies2" = Not_Implies2
   | verit_rule_of "implies_neg1" = Implies_Neg1
   | verit_rule_of "implies_neg2" = Implies_Neg2
   | verit_rule_of "implies" = Implies
   | verit_rule_of "bfun_elim" = Bfun_Elim
   | verit_rule_of "ite1" = ITE1
   | verit_rule_of "ite2" = ITE2
   | verit_rule_of "not_ite1" = Not_ITE1
   | verit_rule_of "not_ite2" = Not_ITE2
   | verit_rule_of "ite_pos1" = ITE_Pos1
   | verit_rule_of "ite_pos2" = ITE_Pos2
   | verit_rule_of "ite_neg1" = ITE_Neg1
   | verit_rule_of "ite_neg2" = ITE_Neg2
-  | verit_rule_of "ite_intro" = ITE_Intro
   | verit_rule_of "la_disequality" = LA_Disequality
   | verit_rule_of "lia_generic" = LIA_Generic
   | verit_rule_of "la_generic" = LA_Generic
   | verit_rule_of "la_tautology" = LA_Tautology
   | verit_rule_of "la_totality" = LA_Totality
   | verit_rule_of "la_rw_eq"= LA_RW_Eq
   | verit_rule_of "nla_generic"= NLA_Generic
   | verit_rule_of "eq_transitive" = Eq_Transitive
   | verit_rule_of "qnt_rm_unused" = Qnt_Rm_Unused
   | verit_rule_of "onepoint" = Onepoint
   | verit_rule_of "qnt_join" = Qnt_Join
-  | verit_rule_of "eq_congruent_pred" = Eq_Congruent_Pred
   | verit_rule_of "subproof" = Subproof
   | verit_rule_of "bool_simplify" = Bool_Simplify
   | verit_rule_of "or_simplify" = Or_Simplify
   | verit_rule_of "ite_simplify" = ITE_Simplify
   | verit_rule_of "and_simplify" = And_Simplify
   | verit_rule_of "not_simplify" = Not_Simplify
   | verit_rule_of "equiv_simplify" = Equiv_Simplify
   | verit_rule_of "eq_simplify" = Eq_Simplify
   | verit_rule_of "implies_simplify" = Implies_Simplify
   | verit_rule_of "connective_def" = Connective_Def
   | verit_rule_of "minus_simplify" = Minus_Simplify
   | verit_rule_of "sum_simplify" = Sum_Simplify
   | verit_rule_of "prod_simplify" = Prod_Simplify
   | verit_rule_of "comp_simplify" = Comp_Simplify
   | verit_rule_of "qnt_simplify" = Qnt_Simplify
-  | verit_rule_of "not_not" = Not_Not
   | verit_rule_of "tautology" = Tautological_Clause
-  | verit_rule_of "contraction" = Duplicate_Literals
   | verit_rule_of "qnt_cnf" = Qnt_CNF
   | verit_rule_of r =
      if r = Verit_Proof.normalized_input_rule then Normalized_Input
      else if r = Verit_Proof.local_input_rule then Local_Input
      else if r = Verit_Proof.veriT_def then Definition
+     else if r = Verit_Proof.not_not_rule then Not_Not
+     else if r = Verit_Proof.contract_rule then Duplicate_Literals
+     else if r = Verit_Proof.ite_intro_rule then ITE_Intro
+     else if r = Verit_Proof.eq_congruent_rule then Eq_Congruent
+     else if r = Verit_Proof.eq_congruent_pred_rule then Eq_Congruent_Pred
      else (@{print} ("Unsupport rule", r); Unsupported)
 
 fun string_of_verit_rule Bind = "Bind"
   | string_of_verit_rule Cong = "Cong"
   | string_of_verit_rule Refl = "Refl"
   | string_of_verit_rule Equiv1 = "Equiv1"
   | string_of_verit_rule Equiv2 = "Equiv2"
   | string_of_verit_rule Equiv_pos1 = "Equiv_pos1"
   | string_of_verit_rule Equiv_pos2 = "Equiv_pos2"
   | string_of_verit_rule Equiv_neg1 = "Equiv_neg1"
   | string_of_verit_rule Equiv_neg2 = "Equiv_neg2"
   | string_of_verit_rule Skolem_Forall = "Skolem_Forall"
   | string_of_verit_rule Skolem_Ex = "Skolem_Ex"
   | string_of_verit_rule Eq_Reflexive = "Eq_Reflexive"
   | string_of_verit_rule Theory_Resolution = "Theory_Resolution"
   | string_of_verit_rule Forall_Inst = "forall_inst"
   | string_of_verit_rule Or = "Or"
   | string_of_verit_rule Not_Or = "Not_Or"
   | string_of_verit_rule Resolution = "Resolution"
   | string_of_verit_rule Eq_Congruent = "eq_congruent"
   | string_of_verit_rule Trans = "trans"
   | string_of_verit_rule False = "false"
   | string_of_verit_rule And = "and"
   | string_of_verit_rule And_Pos = "and_pos"
   | string_of_verit_rule Not_And = "not_and"
   | string_of_verit_rule And_Neg = "and_neg"
   | string_of_verit_rule Or_Pos = "or_pos"
   | string_of_verit_rule Or_Neg = "or_neg"
   | string_of_verit_rule AC_Simp = "ac_simp"
   | string_of_verit_rule Not_Equiv1 = "not_equiv1"
   | string_of_verit_rule Not_Equiv2 = "not_equiv2"
   | string_of_verit_rule Not_Implies1 = "not_implies1"
   | string_of_verit_rule Not_Implies2 = "not_implies2"
   | string_of_verit_rule Implies_Neg1 = "implies_neg1"
   | string_of_verit_rule Implies_Neg2 = "implies_neg2"
   | string_of_verit_rule Implies = "implies"
   | string_of_verit_rule Bfun_Elim = "bfun_elim"
   | string_of_verit_rule ITE1 = "ite1"
   | string_of_verit_rule ITE2 = "ite2"
   | string_of_verit_rule Not_ITE1 = "not_ite1"
   | string_of_verit_rule Not_ITE2 = "not_ite2"
   | string_of_verit_rule ITE_Pos1 = "ite_pos1"
   | string_of_verit_rule ITE_Pos2 = "ite_pos2"
   | string_of_verit_rule ITE_Neg1 = "ite_neg1"
   | string_of_verit_rule ITE_Neg2 = "ite_neg2"
   | string_of_verit_rule ITE_Intro = "ite_intro"
   | string_of_verit_rule LA_Disequality = "la_disequality"
   | string_of_verit_rule LA_Generic = "la_generic"
   | string_of_verit_rule LIA_Generic = "lia_generic"
   | string_of_verit_rule LA_Tautology = "la_tautology"
   | string_of_verit_rule LA_RW_Eq = "la_rw_eq"
   | string_of_verit_rule LA_Totality = "LA_Totality"
   | string_of_verit_rule NLA_Generic = "nla_generic"
   | string_of_verit_rule Eq_Transitive = "eq_transitive"
   | string_of_verit_rule Qnt_Rm_Unused = "qnt_remove_unused"
   | string_of_verit_rule Onepoint = "onepoint"
   | string_of_verit_rule Qnt_Join = "qnt_join"
   | string_of_verit_rule Eq_Congruent_Pred = "eq_congruent_pred"
   | string_of_verit_rule Normalized_Input = Verit_Proof.normalized_input_rule
   | string_of_verit_rule Local_Input = Verit_Proof.local_input_rule
   | string_of_verit_rule Subproof = "subproof"
   | string_of_verit_rule Bool_Simplify = "bool_simplify"
   | string_of_verit_rule Equiv_Simplify = "equiv_simplify"
   | string_of_verit_rule Eq_Simplify = "eq_simplify"
   | string_of_verit_rule Not_Simplify = "not_simplify"
   | string_of_verit_rule And_Simplify = "and_simplify"
   | string_of_verit_rule Or_Simplify = "or_simplify"
   | string_of_verit_rule ITE_Simplify = "ite_simplify"
   | string_of_verit_rule Implies_Simplify = "implies_simplify"
   | string_of_verit_rule Connective_Def = "connective_def"
   | string_of_verit_rule Minus_Simplify = "minus_simplify"
   | string_of_verit_rule Sum_Simplify = "sum_simplify"
   | string_of_verit_rule Prod_Simplify = "prod_simplify"
   | string_of_verit_rule Comp_Simplify = "comp_simplify"
   | string_of_verit_rule Qnt_Simplify = "qnt_simplify"
-  | string_of_verit_rule Not_Not = "not_not"
+  | string_of_verit_rule Not_Not = Verit_Proof.not_not_rule
   | string_of_verit_rule Tautological_Clause = "tautology"
-  | string_of_verit_rule Duplicate_Literals = "contraction"
+  | string_of_verit_rule Duplicate_Literals = Verit_Proof.contract_rule
   | string_of_verit_rule Qnt_CNF = "qnt_cnf"
   | string_of_verit_rule r = "Unknown rule: " ^ \<^make_string> r
 
 fun replay_error ctxt msg rule thms t =
   SMT_Replay_Methods.replay_error ctxt msg (string_of_verit_rule rule) thms t
 
 
 (* utility function *)
 
 fun eqsubst_all ctxt thms =
    K ((REPEAT o HEADGOAL) (EqSubst.eqsubst_asm_tac ctxt [0] thms))
    THEN' K ((REPEAT o HEADGOAL) (EqSubst.eqsubst_tac ctxt [0] thms))
 
 fun simplify_tac ctxt thms =
   ctxt
   |> empty_simpset
   |> put_simpset HOL_basic_ss
   |> (fn ctxt => ctxt addsimps @{thms simp_thms} addsimps thms)
   |> Simplifier.asm_full_simp_tac
 
 (* sko_forall requires the assumptions to be able to prove the equivalence in case of double
 skolemization. See comment below. *)
 fun requires_subproof_assms _ t =
   member (op =) ["refl", "sko_forall", "sko_ex", "cong"] t
 
 fun requires_local_input _ t =
   member (op =) [Verit_Proof.local_input_rule] t
 
 (*This is a weaker simplification form. It is weaker, but is also less likely to loop*)
 fun partial_simplify_tac ctxt thms =
   ctxt
   |> empty_simpset
   |> put_simpset HOL_basic_ss
   |> (fn ctxt => ctxt addsimps @{thms simp_thms} addsimps thms)
   |> Simplifier.full_simp_tac
 
 val try_provers = SMT_Replay_Methods.try_provers "verit"
 
 fun TRY' tac = fn i => TRY (tac i)
 fun REPEAT' tac = fn i => REPEAT (tac i)
 fun REPEAT_CHANGED tac = fn i => REPEAT (CHANGED (tac i))
 
 
 (* Bind *)
 
 (*The bind rule is non-obvious due to the handling of quantifiers:
   "\<And>x y a. x = y ==> (\<forall>b. P a b x) \<longleftrightarrow> (\<forall>b. P' a b y)"
   ------------------------------------------------------
             \<forall>a. (\<forall>b x. P a b x) \<longleftrightarrow> (\<forall>b y. P' a b y)
 is a valid application.*)
 
 val bind_thms =
   [@{lemma \<open>(\<And>x x'. x = x' \<Longrightarrow> P x = Q x') \<Longrightarrow> (\<forall>x. P x) = (\<forall>y. Q y)\<close> by blast},
    @{lemma \<open>(\<And>x x'. x = x' \<Longrightarrow> P x = Q x') \<Longrightarrow> (\<exists>x. P x) = (\<exists>y. Q y)\<close> by blast},
    @{lemma \<open>(\<And>x x'. x = x' \<Longrightarrow> P x = Q x') \<Longrightarrow> (\<exists>x. P x = Q x)\<close> by blast},
    @{lemma \<open>(\<And>x x'. x = x' \<Longrightarrow> P x = Q x') \<Longrightarrow> (\<forall>x. P x = Q x)\<close> by blast}]
 
 val bind_thms_same_name =
   [@{lemma \<open>(\<And>x. P x = Q x) \<Longrightarrow> (\<forall>x. P x) = (\<forall>y. Q y)\<close> by blast},
    @{lemma \<open>(\<And>x. P x = Q x) \<Longrightarrow> (\<exists>x. P x) = (\<exists>y. Q y)\<close> by blast},
    @{lemma \<open>(\<And>x. P x = Q x) \<Longrightarrow> (\<exists>x. P x = Q x)\<close> by blast},
    @{lemma \<open>(\<And>x. P x = Q x) \<Longrightarrow> (\<forall>x. P x = Q x)\<close> by blast}]
 
 fun extract_quantified_names_q (_ $ Abs (name, _, t)) =
    apfst (curry (op ::) name) (extract_quantified_names_q t)
   | extract_quantified_names_q t = ([], t)
 
 fun extract_forall_quantified_names_q (Const(\<^const_name>\<open>HOL.All\<close>, _) $ Abs (name, ty, t)) =
    (name,  ty) :: (extract_forall_quantified_names_q t)
   | extract_forall_quantified_names_q _ = []
 
 fun extract_all_forall_quantified_names_q (Const(\<^const_name>\<open>HOL.All\<close>, _) $ Abs (name, _, t)) =
       name :: (extract_all_forall_quantified_names_q t)
   | extract_all_forall_quantified_names_q (t $ u) =
       extract_all_forall_quantified_names_q t @ extract_all_forall_quantified_names_q u
   | extract_all_forall_quantified_names_q _ = []
 
 val extract_quantified_names_ba =
   SMT_Replay_Methods.dest_prop
   #> extract_quantified_names_q
   ##> HOLogic.dest_eq
   ##> fst
   ##> extract_quantified_names_q
   ##> fst
 
 val extract_quantified_names =
   extract_quantified_names_ba
   #> (op @)
 
 val extract_all_forall_quantified_names =
   SMT_Replay_Methods.dest_prop
   #> HOLogic.dest_eq
   #> fst
   #> extract_all_forall_quantified_names_q
 
 
 fun extract_all_exists_quantified_names_q (Const(\<^const_name>\<open>HOL.Ex\<close>, _) $ Abs (name, _, t)) =
       name :: (extract_all_exists_quantified_names_q t)
   | extract_all_exists_quantified_names_q (t $ u) =
       extract_all_exists_quantified_names_q t @ extract_all_exists_quantified_names_q u
   | extract_all_exists_quantified_names_q _ = []
 
 val extract_all_exists_quantified_names =
   SMT_Replay_Methods.dest_prop
   #> HOLogic.dest_eq
   #> fst
   #> extract_all_exists_quantified_names_q
 
 
 val extract_bind_names =
    HOLogic.dest_eq
    #> apply2 (fn (Free (name, _)) => name)
 
 fun combine_quant ctxt ((n1, n2) :: bounds) (n1' :: formula) =
     TRY' (if n1 = n1'
      then if n1 <> n2
        then
          resolve_tac ctxt bind_thms
          THEN' TRY'(resolve_tac ctxt [@{thm refl}])
          THEN' combine_quant ctxt bounds formula
        else resolve_tac ctxt bind_thms_same_name THEN' combine_quant ctxt bounds formula
      else resolve_tac ctxt @{thms allI} THEN' combine_quant ctxt ((n1, n2) :: bounds) formula)
   | combine_quant _ _ _ = K all_tac
 
 fun bind_quants ctxt args t =
   combine_quant ctxt (map extract_bind_names args) (extract_quantified_names t)
 
 fun generalize_prems_q [] prems = prems
   | generalize_prems_q (_ :: quants) prems =
       generalize_prems_q quants (@{thm spec} OF [prems])
 
 fun generalize_prems t = generalize_prems_q (fst (extract_quantified_names_ba t))
 
 fun bind ctxt [prems] args t =
   SMT_Replay_Methods.prove ctxt t (fn _ =>
     bind_quants ctxt args t
     THEN' TRY' (SOLVED' (resolve_tac ctxt [generalize_prems t prems]
       THEN_ALL_NEW TRY' (assume_tac ctxt ORELSE' resolve_tac ctxt @{thms refl}))))
  | bind ctxt thms _ t = replay_error ctxt "invalid bind application" Bind thms t
 
 
 (* Congruence/Refl *)
 
 fun cong ctxt thms = try_provers ctxt
     (string_of_verit_rule Cong) [
   ("basic", SMT_Replay_Methods.cong_basic ctxt thms),
   ("unfolding then reflexivity", SMT_Replay_Methods.cong_unfolding_trivial ctxt thms),
   ("unfolding then auto", SMT_Replay_Methods.cong_unfolding_first ctxt thms),
   ("full", SMT_Replay_Methods.cong_full ctxt thms)] thms
 
 fun refl ctxt thm t =
   (case find_first (fn thm => t = Thm.full_prop_of thm) thm of
       SOME thm => thm
     | NONE =>
         (case try (fn t => SMT_Replay_Methods.match_instantiate ctxt t @{thm refl}) t of
           NONE => cong ctxt thm t
         | SOME thm => thm))
 
 
 (* Instantiation *)
 
 local
 fun dropWhile _ [] = []
   | dropWhile f (x :: xs) = if f x then dropWhile f xs else x :: xs
 in
 
 fun forall_inst ctxt _ _ insts t =
   let
     fun instantiate_and_solve i ({context = ctxt, prems = [prem], ...}: Subgoal.focus) =
         let
           val t = Thm.prop_of prem
           val quants = t
             |> SMT_Replay_Methods.dest_prop
             |> extract_forall_quantified_names_q
           val insts = map (Symtab.lookup insts o fst) (rev quants)
             |> dropWhile (curry (op =) NONE)
             |> rev
           fun option_map _ NONE = NONE
             | option_map f (SOME a) = SOME (f a)
           fun instantiate_with inst prem =
             Drule.infer_instantiate' ctxt [NONE, inst] @{thm spec} OF [prem]
           val inst_thm =
             fold instantiate_with
               (map (option_map (Thm.cterm_of ctxt)) insts)
               prem
         in
            (Method.insert_tac ctxt [inst_thm]
            THEN' TRY' (fn i => assume_tac ctxt i)
            THEN' TRY' (partial_simplify_tac ctxt @{thms eq_commute})) i
         end
      | instantiate_and_solve _ ({context = ctxt, prems = thms, ...}: Subgoal.focus) =
          replay_error ctxt "invalid application" Forall_Inst thms t
   in
     SMT_Replay_Methods.prove ctxt t (fn _ =>
       match_tac ctxt [@{thm disj_not1} RSN (1, @{thm iffD2}) OF [@{thm impI}]]
       THEN' (fn i => Subgoal.FOCUS (instantiate_and_solve i) ctxt i))
   end
 end
 
 
 (* Or *)
 
 fun or _ (thm :: _) _ = thm
   | or ctxt thms t = replay_error ctxt "invalid bind application" Or thms t
 
 
 (* Implication *)
 
 val implies_pos_thm =
   [@{lemma \<open>\<not>(A \<longrightarrow> B) \<or> \<not>A \<or> B\<close> by blast},
   @{lemma \<open>\<not>(\<not>A \<longrightarrow> B) \<or> A \<or> B\<close> by blast}]
 
 fun implies_pos ctxt _ t = SMT_Replay_Methods.prove ctxt t (fn _ =>
   resolve_tac ctxt implies_pos_thm)
 
 fun extract_rewrite_rule_assumption _ thms =
   let
     fun is_rewrite_rule thm =
       (case Thm.prop_of thm of
         \<^term>\<open>Trueprop\<close> $ (Const(\<^const_name>\<open>HOL.eq\<close>, _) $ _ $ Free(_, _)) => true
       | _ => false)
     fun is_context_rule thm =
       (case Thm.prop_of thm of
         \<^term>\<open>Trueprop\<close> $ (Const(\<^const_name>\<open>HOL.eq\<close>, _) $ Free(_, _) $ Free(_, _)) => true
       | _ => false)
     val ctxt_eq =
       thms
       |> filter is_context_rule
     val rew =
       thms
       |> filter_out is_context_rule
       |> filter is_rewrite_rule
   in
     (ctxt_eq, rew)
   end
 
 local
   fun rewrite_all_skolems thm_indirect ctxt (SOME thm :: thms) =
      EqSubst.eqsubst_tac ctxt [0] [thm_indirect OF [thm]]
      THEN' (partial_simplify_tac ctxt (@{thms eq_commute}))
      THEN' rewrite_all_skolems thm_indirect ctxt thms
    | rewrite_all_skolems thm_indirect ctxt (NONE :: thms) = rewrite_all_skolems thm_indirect ctxt thms
    | rewrite_all_skolems _ _ [] = K (all_tac)
 
    fun extract_var_name (thm :: thms) =
        let val name = Thm.concl_of thm
          |> SMT_Replay_Methods.dest_prop
          |> HOLogic.dest_eq
          |> fst
          |> (fn Const(_,_) $ Abs(name, _, _) => [(name,@{thm sym} OF [thm])]
              | _ => [])
        in name :: extract_var_name thms end
     | extract_var_name [] = []
 
 fun skolem_tac extractor thm1 thm2 ctxt thms t  =
   let
     val (ctxt_eq, ts) = extract_rewrite_rule_assumption ctxt thms
     fun ordered_definitions () =
       let
         val var_order = extractor t
         val thm_names_with_var = extract_var_name ts |> flat
       in map (AList.lookup (op =) thm_names_with_var) var_order end
 
   in
     SMT_Replay_Methods.prove ctxt t (fn _ =>
       K (unfold_tac ctxt ctxt_eq)
       THEN' ((SOLVED' (K (unfold_tac ctxt (map (fn thm => thm1 OF [@{thm sym} OF [thm]]) ts))))
         ORELSE'
           (rewrite_all_skolems thm2 ctxt (ordered_definitions ())
           THEN' partial_simplify_tac ctxt @{thms eq_commute})))
   end
 in
 
 val skolem_forall =
   skolem_tac extract_all_forall_quantified_names @{thm verit_sko_forall_indirect}
     @{thm verit_sko_forall_indirect2}
 
 val skolem_ex =
   skolem_tac extract_all_exists_quantified_names @{thm verit_sko_ex_indirect}
     @{thm verit_sko_ex_indirect2}
 
 end
 
 fun eq_reflexive ctxt _ t = SMT_Replay_Methods.match_instantiate ctxt t @{thm refl}
 
 local
   fun not_not_prove ctxt _ =
     K (unfold_tac ctxt @{thms not_not})
     THEN' match_tac ctxt @{thms verit_or_simplify_1}
 
   fun duplicate_literals_prove ctxt prems =
     Method.insert_tac ctxt prems
     THEN' match_tac ctxt @{thms ccontr}
     THEN' K (unfold_tac ctxt @{thms de_Morgan_disj not_not})
     THEN' TRY o CHANGED_PROP o REPEAT_ALL_NEW (ematch_tac ctxt @{thms conjE})
     THEN' CHANGED_PROP o REPEAT_ALL_NEW (ematch_tac ctxt @{thms disjE})
     THEN' REPEAT' (ematch_tac ctxt @{thms notE} THEN' TRY' (assume_tac ctxt))
 
   fun tautological_clause_prove ctxt _ =
     match_tac ctxt @{thms verit_or_neg}
     THEN' K (unfold_tac ctxt @{thms not_not disj_assoc[symmetric]})
     THEN' TRY' (match_tac ctxt @{thms notE} THEN_ALL_NEW assume_tac ctxt)
 in
 
 fun prove_abstract abstracter tac ctxt thms t =
   let
     val thms = map (Conv.fconv_rule Thm.eta_long_conversion) thms
     val t' = Thm.eta_long_conversion (Object_Logic.dest_judgment ctxt (Thm.cterm_of ctxt t))
     val (_, t2) = Logic.dest_equals (Thm.prop_of t')
     val thm =
       SMT_Replay_Methods.prove_abstract ctxt thms t2 tac (
         fold_map (abstracter o SMT_Replay_Methods.dest_thm) thms ##>>
         abstracter (SMT_Replay_Methods.dest_prop t2))
   in
     @{thm verit_Pure_trans} OF [t', thm]
   end
 
 val not_not = prove_abstract SMT_Replay_Methods.abstract_bool_shallow not_not_prove
 
 val tautological_clause =
   prove_abstract SMT_Replay_Methods.abstract_bool_shallow tautological_clause_prove
 
 val duplicate_literals =
   prove_abstract SMT_Replay_Methods.abstract_bool_shallow duplicate_literals_prove
 
 val unit_res = prove_abstract SMT_Replay_Methods.abstract_bool_shallow SMT_Replay_Methods.prop_tac
 
 end
 
 
 fun normalized_input ctxt prems t = SMT_Replay_Methods.prove ctxt t (fn _ =>
   Method.insert_tac ctxt prems
   THEN' TRY' (K (unfold_tac ctxt @{thms SMT.trigger_def}))
   THEN' TRY' (partial_simplify_tac ctxt @{thms eq_commute}))
 
 val false_rule_thm = @{lemma \<open>\<not>False\<close> by blast}
 
 fun false_rule ctxt _ t = SMT_Replay_Methods.match_instantiate ctxt t false_rule_thm
 
 
 (* Transitivity *)
 
 val trans_bool_thm =
   @{lemma \<open>P = Q \<Longrightarrow> Q \<Longrightarrow> P\<close> by blast}
 
 fun trans ctxt thms t =
   let
     val prop_of = HOLogic.dest_Trueprop o Thm.full_prop_of
     fun combine_thms [thm1, thm2] =
           (case (prop_of thm1, prop_of thm2) of
             ((Const(\<^const_name>\<open>HOL.eq\<close>, _) $ t1 $ t2),
              (Const(\<^const_name>\<open>HOL.eq\<close>, _) $ t3 $ t4)) =>
-            if t2 = t3 then thm1 RSN (1, thm2 RSN (2, @{thm trans}))
-            else if t2 = t4 then thm1 RSN ((1, ((thm2 RS sym)) RSN (2, @{thm trans})))
-            else if t1 = t4 then thm2 RSN (1, thm1 RSN (2, @{thm trans}))
+            if t2 aconv t3 then thm1 RSN (1, thm2 RSN (2, @{thm trans}))
+            else if t2 aconv t4 then thm1 RSN ((1, ((thm2 RS sym)) RSN (2, @{thm trans})))
+            else if t1 aconv t4 then thm2 RSN (1, thm1 RSN (2, @{thm trans}))
             else raise Fail "invalid trans theorem"
           | _ => trans_bool_thm OF [thm1, thm2])
       | combine_thms (thm1 :: thm2 :: thms) =
           combine_thms (combine_thms [thm1, thm2] :: thms)
       | combine_thms thms = replay_error ctxt "invalid bind application" Trans thms t
      val t' = Thm.eta_long_conversion (Object_Logic.dest_judgment ctxt (Thm.cterm_of ctxt t))
      val (_, t2) = Logic.dest_equals (Thm.prop_of t')
      val thms = map (Conv.fconv_rule Thm.eta_long_conversion) thms
      val trans_thm = combine_thms thms
   in
      (case (prop_of trans_thm, t2) of
        ((Const(\<^const_name>\<open>HOL.eq\<close>, _) $ t1 $ _),
              (Const(\<^const_name>\<open>HOL.eq\<close>, _) $ t3 $ _)) =>
        if t1 aconv t3 then trans_thm else trans_thm RS sym
       | _ => trans_thm (*to be on the safe side*))
   end
 
 
 fun tmp_AC_rule ctxt thms t =
   SMT_Replay_Methods.prove ctxt t (fn _ =>
     Method.insert_tac ctxt thms
     THEN' REPEAT_ALL_NEW (partial_simplify_tac ctxt @{thms eq_commute}
     THEN' TRY' (simplify_tac ctxt @{thms ac_simps conj_ac})
     THEN' TRY' (Classical.fast_tac ctxt)))
 
 
 (* And/Or *)
 
 local
   fun not_and_rule_prove ctxt prems =
      Method.insert_tac ctxt prems
      THEN' K (unfold_tac ctxt @{thms de_Morgan_conj})
      THEN_ALL_NEW TRY' (assume_tac ctxt)
 
   fun or_pos_prove ctxt _ =
      K (unfold_tac ctxt @{thms de_Morgan_disj not_not})
      THEN' match_tac ctxt @{thms verit_and_pos}
-     THEN' K (unfold_tac ctxt @{thms de_Morgan_conj not_not})
+     THEN' K (unfold_tac ctxt @{thms de_Morgan_conj de_Morgan_disj not_not})
      THEN' TRY' (assume_tac ctxt)
 
   fun not_or_rule_prove ctxt prems =
      Method.insert_tac ctxt prems
      THEN' K (unfold_tac ctxt @{thms de_Morgan_disj not_not})
      THEN' TRY' (REPEAT' (match_tac ctxt @{thms conjI}))
      THEN_ALL_NEW ((REPEAT' (ematch_tac ctxt @{thms conjE}))
        THEN' TRY' (assume_tac ctxt))
 
   fun and_rule_prove ctxt prems =
      Method.insert_tac ctxt prems
      THEN' (fn i => REPEAT (dresolve_tac ctxt @{thms conjE} i THEN assume_tac ctxt (i+1)))
      THEN' TRY' (assume_tac ctxt)
 
   fun and_neg_rule_prove ctxt _ =
-     match_tac ctxt @{thms verit_and_pos}
+     match_tac ctxt @{thms verit_and_neg}
      THEN' K (unfold_tac ctxt @{thms de_Morgan_conj not_not})
      THEN' TRY' (assume_tac ctxt)
 
   fun prover tac = prove_abstract SMT_Replay_Methods.abstract_prop tac
 
 in
 
 val and_rule = prover and_rule_prove
 
 val not_and_rule = prover not_and_rule_prove
 
 val not_or_rule = prover not_or_rule_prove
 
 val or_pos_rule = prover or_pos_prove
 
 val and_neg_rule = prover and_neg_rule_prove
 
 val or_neg_rule = prove_abstract SMT_Replay_Methods.abstract_bool (fn ctxt => fn _ =>
   resolve_tac ctxt @{thms verit_or_neg}
   THEN' K (unfold_tac ctxt @{thms not_not})
   THEN_ALL_NEW
     (REPEAT'
       (SOLVED' (match_tac ctxt @{thms disjI1} THEN_ALL_NEW assume_tac ctxt)
        ORELSE' (match_tac ctxt @{thms disjI2} THEN' TRY' (assume_tac ctxt)))))
 
 fun and_pos ctxt _ t =
   SMT_Replay_Methods.prove ctxt t (fn _ =>
   REPEAT_CHANGED (resolve_tac ctxt @{thms verit_and_pos})
   THEN' TRY' (assume_tac ctxt))
 
 end
 
 
 (* Equivalence Transformation *)
 
 local
   fun prove_equiv equiv_thm ctxt [thm] t = SMT_Replay_Methods.prove ctxt t (fn _ =>
         Method.insert_tac ctxt [equiv_thm OF [thm]]
         THEN' TRY' (assume_tac ctxt))
     | prove_equiv _ ctxt thms t = replay_error ctxt "invalid application in some equiv rule" Unsupported thms t
 in
 
 val not_equiv1 = prove_equiv @{lemma \<open>\<not>(A \<longleftrightarrow> B) \<Longrightarrow> A \<or> B\<close> by blast}
 val not_equiv2 = prove_equiv @{lemma \<open>\<not>(A \<longleftrightarrow> B) \<Longrightarrow> \<not>A \<or> \<not>B\<close> by blast}
 val equiv1  = prove_equiv @{lemma \<open>(A \<longleftrightarrow> B) \<Longrightarrow> \<not>A \<or> B\<close> by blast}
 val equiv2 = prove_equiv @{lemma \<open>(A \<longleftrightarrow> B) \<Longrightarrow> A \<or> \<not>B\<close> by blast}
 val not_implies1 = prove_equiv @{lemma \<open>\<not>(A \<longrightarrow> B) \<Longrightarrow> A\<close> by blast}
 val not_implies2 = prove_equiv @{lemma \<open>\<not>(A \<longrightarrow>B) \<Longrightarrow> \<not>B\<close> by blast}
 
 end
 
 
 (* Equivalence Lemma *)
 (*equiv_pos2 is very important for performance. We have tried various tactics, including
 a specialisation of SMT_Replay_Methods.match_instantiate, but there never was a measurable
 and consistent gain.*)
 local
   fun prove_equiv_pos_neg2 thm ctxt _ t =
     SMT_Replay_Methods.match_instantiate ctxt t thm
 in
 
 val equiv_pos1_thm = @{lemma \<open>\<not>(a \<longleftrightarrow> b) \<or> a \<or> \<not>b\<close> by blast+}
 val equiv_pos1 = prove_equiv_pos_neg2 equiv_pos1_thm
 
 val equiv_pos2_thm = @{lemma \<open>\<And>a b. (a \<noteq> b) \<or> \<not>a \<or> b\<close> by blast+}
 val equiv_pos2 = prove_equiv_pos_neg2 equiv_pos2_thm
 
 val equiv_neg1_thm = @{lemma \<open>(a \<longleftrightarrow> b) \<or> \<not>a \<or> \<not>b\<close> by blast+}
 val equiv_neg1 = prove_equiv_pos_neg2 equiv_neg1_thm
 
 val equiv_neg2_thm = @{lemma \<open>(a \<longleftrightarrow> b) \<or> a \<or> b\<close> by blast}
 val equiv_neg2 = prove_equiv_pos_neg2 equiv_neg2_thm
 
 end
 
 
 local
   fun implies_pos_neg_term ctxt thm (\<^term>\<open>Trueprop\<close> $
          (\<^term>\<open>HOL.disj\<close> $ (\<^term>\<open>HOL.implies\<close> $ a $ b) $ _)) =
          Drule.infer_instantiate' ctxt (map (SOME o Thm.cterm_of ctxt) [a, b]) thm
      | implies_pos_neg_term ctxt thm  t =
         replay_error ctxt "invalid application in Implies" Unsupported [thm] t
 
   fun prove_implies_pos_neg thm ctxt _ t =
     let val thm = implies_pos_neg_term ctxt thm t
     in
       SMT_Replay_Methods.prove ctxt t (fn _ =>
         Method.insert_tac ctxt [thm]
         THEN' TRY' (assume_tac ctxt))
     end
 in
 
 val implies_neg1_thm = @{lemma \<open>(a \<longrightarrow> b) \<or> a\<close> by blast}
 val implies_neg1  = prove_implies_pos_neg implies_neg1_thm
 
 val implies_neg2_thm = @{lemma \<open>(a \<longrightarrow> b) \<or> \<not>b\<close> by blast}
 val implies_neg2 = prove_implies_pos_neg implies_neg2_thm
 
 val implies_thm = @{lemma \<open>(a \<longrightarrow> b) \<Longrightarrow> \<not>a \<or> b\<close> by blast}
 fun implies_rules ctxt prems t = SMT_Replay_Methods.prove ctxt t (fn _ =>
   Method.insert_tac ctxt [implies_thm OF prems]
   THEN' TRY' (assume_tac ctxt))
 
 end
 
 
 (* BFun *)
 
 local
   val bfun_theorems = @{thms verit_bfun_elim}
 in
 
 fun bfun_elim ctxt prems t = SMT_Replay_Methods.prove ctxt t (fn _ =>
   Method.insert_tac ctxt prems
   THEN' TRY' (eqsubst_all ctxt bfun_theorems)
   THEN' TRY' (simplify_tac ctxt @{thms eq_commute all_conj_distrib ex_disj_distrib}))
 
 end
 
 
 (* If-Then-Else *)
 
 local
   fun prove_ite ite_thm thm ctxt =
   resolve_tac ctxt [ite_thm OF [thm]]
   THEN' K (unfold_tac ctxt @{thms not_not})
   THEN' TRY' (assume_tac ctxt)
 in
 
 val ite_pos1_thm =
   @{lemma \<open>\<not>(if x then P else Q) \<or> x \<or> Q\<close> by auto}
 
 fun ite_pos1 ctxt _ t = SMT_Replay_Methods.prove ctxt t (fn _ =>
   resolve_tac ctxt [ite_pos1_thm])
 
 val ite_pos2_thms =
   @{lemma \<open>\<not>(if x then P else Q) \<or> \<not>x \<or> P\<close> \<open>\<not>(if \<not>x then P else Q) \<or> x \<or> P\<close> by auto}
 
 fun ite_pos2 ctxt _ t = SMT_Replay_Methods.prove ctxt t (fn _ => resolve_tac ctxt ite_pos2_thms)
 
 val ite_neg1_thms =
   @{lemma \<open>(if x then P else Q) \<or> x \<or> \<not>Q\<close> \<open>(if x then P else \<not>Q) \<or> x \<or> Q\<close> by auto}
 
 fun ite_neg1 ctxt _ t = SMT_Replay_Methods.prove ctxt t (fn _ => resolve_tac ctxt ite_neg1_thms)
 
 val ite_neg2_thms =
   @{lemma \<open>(if x then P else Q) \<or> \<not>x \<or> \<not>P\<close> \<open>(if \<not>x then P else Q) \<or> x \<or> \<not>P\<close>
           \<open>(if x then \<not>P else Q) \<or> \<not>x \<or> P\<close> \<open>(if \<not>x then \<not>P else Q) \<or> x \<or> P\<close>
       by auto}
 
 fun ite_neg2 ctxt _ t = SMT_Replay_Methods.prove ctxt t (fn _ => resolve_tac ctxt ite_neg2_thms)
 
 val ite1_thm =
   @{lemma \<open>(if x then P else Q) \<Longrightarrow> x \<or> Q\<close> by (auto split: if_splits) }
 
 fun ite1 ctxt [thm] t = SMT_Replay_Methods.prove ctxt t (fn _ => prove_ite ite1_thm thm ctxt)
 
 val ite2_thm =
   @{lemma \<open>(if x then P else Q) \<Longrightarrow> \<not>x \<or> P\<close> by (auto split: if_splits) }
 
 fun ite2 ctxt [thm] t = SMT_Replay_Methods.prove ctxt t (fn _ => prove_ite ite2_thm thm ctxt)
 
 val not_ite1_thm =
   @{lemma \<open>\<not>(if x then P else Q) \<Longrightarrow> x \<or> \<not>Q\<close> by (auto split: if_splits) }
 
 fun not_ite1 ctxt [thm] t = SMT_Replay_Methods.prove ctxt t (fn _ => prove_ite not_ite1_thm thm ctxt)
 
 val not_ite2_thm =
   @{lemma \<open>\<not>(if x then P else Q) \<Longrightarrow> \<not>x \<or> \<not>P\<close> by (auto split: if_splits) }
 
 fun not_ite2 ctxt [thm] t = SMT_Replay_Methods.prove ctxt t (fn _ => prove_ite not_ite2_thm thm ctxt)
 
 (*ite_intro can introduce new terms that are in the proof exactly the sames as the old one, but are
 not internally, hence the possible reordering.*)
 fun ite_intro ctxt _ t =
   let
     fun simplify_ite ctxt thms =
       ctxt
       |> empty_simpset
       |> put_simpset HOL_basic_ss
       |> (fn ctxt => ctxt addsimps thms @ @{thms if_True if_False refl simp_thms if_cancel})
       |> Raw_Simplifier.add_eqcong @{thm verit_ite_if_cong}
       |> Simplifier.full_simp_tac
   in
     SMT_Replay_Methods.prove ctxt t (fn _ => simplify_ite ctxt []
        THEN' TRY' (simplify_ite ctxt @{thms eq_commute}))
   end
 end
 
 
 (* Quantifiers *)
 
 local
   val rm_unused = @{lemma \<open>(\<forall>x. P) = P\<close> \<open>(\<exists>x. P) = P\<close> by blast+}
 
   fun qnt_cnf_tac ctxt =
     simplify_tac ctxt @{thms de_Morgan_conj de_Morgan_disj imp_conv_disj
       iff_conv_conj_imp if_bool_eq_disj ex_simps all_simps ex_disj_distrib
       verit_connective_def(3) all_conj_distrib}
     THEN' TRY' (Blast.blast_tac ctxt)
 in
 fun qnt_rm_unused ctxt _ t = SMT_Replay_Methods.prove ctxt t (fn _ =>
   K (unfold_tac ctxt rm_unused))
 
 fun onepoint ctxt prems t = SMT_Replay_Methods.prove ctxt t (fn _ =>
   Method.insert_tac ctxt prems
   THEN' Simplifier.full_simp_tac (put_simpset HOL_basic_ss (empty_simpset ctxt)
     addsimps @{thms HOL.simp_thms HOL.all_simps}
     addsimprocs [@{simproc HOL.defined_All}, @{simproc HOL.defined_Ex}])
   THEN' TRY' (Blast.blast_tac ctxt)
   THEN' TRY' (Metis_Tactic.metis_tac [] ATP_Problem_Generate.combsN ctxt []))
 
 fun qnt_join ctxt _ t = SMT_Replay_Methods.prove ctxt t Classical.fast_tac
 
 fun qnt_cnf ctxt _ t = SMT_Replay_Methods.prove ctxt t qnt_cnf_tac
 
 fun qnt_simplify ctxt _ t = SMT_Replay_Methods.prove ctxt t (fn _ =>
     partial_simplify_tac ctxt [])
 
 end
 
 (* Equality *)
 
 fun eq_transitive ctxt _ t = SMT_Replay_Methods.prove ctxt t (fn  _ =>
   REPEAT_CHANGED (resolve_tac ctxt [@{thm disj_not1} RSN (1, @{thm iffD2}) OF @{thms impI}])
   THEN' REPEAT' (resolve_tac ctxt @{thms impI})
   THEN' REPEAT' (eresolve_tac ctxt @{thms conjI})
   THEN' REPEAT' (fn i => dresolve_tac ctxt @{thms verit_eq_transitive} i THEN assume_tac ctxt (i+1))
   THEN' resolve_tac ctxt @{thms refl})
 
 local
   fun find_rew rews t t' =
     (case AList.lookup (op =) rews (t, t') of
       SOME thm => SOME (thm COMP @{thm symmetric})
     | NONE =>
       (case AList.lookup (op =) rews (t', t) of
         SOME thm => SOME thm
       | NONE => NONE))
 
   fun eq_pred_conv rews t ctxt ctrm =
     (case find_rew rews t (Thm.term_of ctrm) of
       SOME thm => Conv.rewr_conv thm ctrm
     | NONE =>
       (case t of
         f $ arg =>
           (Conv.fun_conv (eq_pred_conv rews f ctxt) then_conv
              Conv.arg_conv (eq_pred_conv rews arg ctxt)) ctrm
       | _ => Conv.all_conv ctrm))
 
   fun eq_pred_rewrite_tac ({context = ctxt, prems, concl, ...}: Subgoal.focus) =
     let
       val rews = prems
        |> map_filter (try (apfst (HOLogic.dest_eq o Thm.term_of o Object_Logic.dest_judgment ctxt o
             Thm.cconcl_of) o `(fn x => x)))
        |> map (apsnd (fn x => @{thm eq_reflection} OF [x]))
       fun conv_left conv = Conv.arg_conv (Conv.arg_conv conv)
       fun conv_left_neg conv = Conv.arg_conv (Conv.arg_conv (Conv.arg_conv conv))
       val (t1, conv_term) =
         (case Thm.term_of (Object_Logic.dest_judgment ctxt concl) of
           Const(_, _) $ (Const(\<^const_name>\<open>HOL.Not\<close>, _) $ t1) $ _ => (t1, conv_left)
         | Const(_, _) $ t1 $ (Const(\<^const_name>\<open>HOL.Not\<close>, _) $ _) => (t1, conv_left_neg)
         | Const(_, _) $ t1 $ _ => (t1, conv_left)
         | t1 => (t1, conv_left))
     fun throwing_CONVERSION cv i st = Seq.single (Conv.gconv_rule cv i st)
     in
       throwing_CONVERSION (conv_term (eq_pred_conv rews t1 ctxt))
     end
 in
 
 fun eq_congruent_pred ctxt _ t =
    SMT_Replay_Methods.prove ctxt t (fn _ =>
    REPEAT' (resolve_tac ctxt [@{thm disj_not1[of \<open>_ = _\<close>]} RSN (1, @{thm iffD2}) OF @{thms impI}])
    THEN' (fn i => Subgoal.FOCUS (fn focus => eq_pred_rewrite_tac focus i) ctxt i)
    THEN' (resolve_tac ctxt @{thms refl excluded_middle excluded_middle[of \<open>\<not>_\<close>, unfolded not_not]}
      ORELSE' assume_tac ctxt))
 
 val eq_congruent = eq_congruent_pred
 
 end
 
 
 (* Subproof *)
 
 fun subproof ctxt [prem] t =
      SMT_Replay_Methods.prove ctxt t (fn _ =>
       (resolve_tac ctxt [@{thm disj_not1} RSN (1, @{thm iffD2}) OF [@{thm impI}],
            @{thm disj_not1[of \<open>\<not>_\<close>, unfolded not_not]} RSN (1, @{thm iffD2}) OF [@{thm impI}]]
         THEN' resolve_tac ctxt [prem]
         THEN_ALL_NEW assume_tac ctxt
         THEN' TRY' (assume_tac ctxt))
       ORELSE' TRY' (Method.insert_tac ctxt [prem] THEN' Blast.blast_tac ctxt))
   | subproof ctxt prems t =
       replay_error ctxt "invalid application, only one assumption expected" Subproof prems t
 
 
 (* Simplifying Steps *)
 
 (* The reconstruction is a bit tricky: At first we only rewrite only based on the rules that are
 passed as argument. Then we simply use simp_thms to reconstruct all the proofs (and these theorems
 cover all the simplification below).
 *)
 local
   fun rewrite_only_thms ctxt thms =
     ctxt
     |> empty_simpset
     |> put_simpset HOL_basic_ss
     |> (fn ctxt => ctxt addsimps thms)
     |> Simplifier.full_simp_tac
   fun rewrite_thms ctxt thms =
     ctxt
     |> empty_simpset
     |> put_simpset HOL_basic_ss
     |> Raw_Simplifier.add_eqcong @{thm eq_reflection[OF imp_cong]}
     |> (fn ctxt => ctxt addsimps thms addsimps @{thms simp_thms})
     |> Simplifier.full_simp_tac
 
   fun chain_rewrite_thms ctxt thms =
     TRY' (rewrite_only_thms ctxt thms)
     THEN' TRY' (rewrite_thms ctxt thms)
 
   fun chain_rewrite_two_step_with_ac_simps ctxt thms1 thms2 =
     TRY' (rewrite_only_thms ctxt thms1)
     THEN' TRY' (rewrite_thms ctxt thms2)
 
   fun chain_rewrite_thms_two_step ctxt thms1 thms2 thms3 thms4 =
     chain_rewrite_two_step_with_ac_simps ctxt thms1 thms2
     THEN' TRY' (chain_rewrite_two_step_with_ac_simps ctxt thms3 thms4)
 
   val imp_refl = @{lemma \<open>(P \<longrightarrow> P) = True\<close> by blast}
 
 in
 fun rewrite_bool_simplify ctxt _ t =
   SMT_Replay_Methods.prove ctxt t (fn _ =>
    (chain_rewrite_thms ctxt @{thms verit_bool_simplify}))
 
 fun rewrite_and_simplify ctxt _ t =
   SMT_Replay_Methods.prove ctxt t (fn _ =>
    (chain_rewrite_two_step_with_ac_simps ctxt @{thms verit_and_simplify verit_and_simplify1}
      @{thms verit_and_simplify}))
 
 fun rewrite_or_simplify ctxt _ t =
   SMT_Replay_Methods.prove ctxt t (fn _ =>
    (chain_rewrite_two_step_with_ac_simps ctxt @{thms verit_or_simplify verit_or_simplify_1}
-    @{thms verit_or_simplify}))
+    @{thms verit_or_simplify})
+    THEN' TRY' (REPEAT' (match_tac ctxt @{thms verit_and_pos}) THEN' assume_tac ctxt))
 
 fun rewrite_not_simplify ctxt _ t =
   SMT_Replay_Methods.prove ctxt t (fn _ =>
    (rewrite_only_thms ctxt @{thms verit_not_simplify}))
 
 fun rewrite_equiv_simplify ctxt _ t =
   SMT_Replay_Methods.prove ctxt t (fn _ =>
    (rewrite_only_thms ctxt @{thms verit_equiv_simplify}))
 
 fun rewrite_eq_simplify ctxt _ t =
   SMT_Replay_Methods.prove ctxt t (fn _ =>
    (chain_rewrite_two_step_with_ac_simps ctxt
       @{thms verit_eq_simplify}
       (Named_Theorems.get ctxt @{named_theorems ac_simps})))
 
 fun rewrite_implies_simplify ctxt _ t =
   SMT_Replay_Methods.prove ctxt t (fn _ =>
     (rewrite_only_thms ctxt @{thms verit_implies_simplify}))
 
 (* It is more efficient to first fold the implication symbols.
    That is however not enough when symbols appears within
    expressions, hence we also unfold implications in the
    other direction. *)
 fun rewrite_connective_def ctxt _ t =
     SMT_Replay_Methods.prove ctxt t (fn _ =>
       chain_rewrite_thms_two_step ctxt
         (imp_refl :: @{thms not_not verit_connective_def[symmetric]})
         (@{thms verit_connective_def[symmetric]})
         (imp_refl :: @{thms not_not verit_connective_def})
         (@{thms verit_connective_def}))
 
 fun rewrite_minus_simplify ctxt _ t =
     SMT_Replay_Methods.prove ctxt t (fn _ =>
       chain_rewrite_two_step_with_ac_simps ctxt
          @{thms arith_simps verit_minus_simplify}
          (Named_Theorems.get ctxt @{named_theorems ac_simps} @
           @{thms numerals arith_simps arith_special
              numeral_class.numeral.numeral_One}))
 
 fun rewrite_comp_simplify ctxt _ t =
     SMT_Replay_Methods.prove ctxt t (fn _ =>
         chain_rewrite_thms ctxt @{thms verit_comp_simplify})
 
 fun rewrite_ite_simplify ctxt _ t =
   SMT_Replay_Methods.prove ctxt t (fn _ =>
    (rewrite_only_thms ctxt @{thms verit_ite_simplify}))
 end
 
 
 (* Simplifications *)
 
 local
   fun simplify_arith ctxt thms = partial_simplify_tac ctxt
     (thms @ Named_Theorems.get ctxt @{named_theorems ac_simps} @ @{thms arith_simps})
 in
 
 fun sum_simplify ctxt _ t =
   SMT_Replay_Methods.prove ctxt t (fn _ =>
     simplify_arith ctxt @{thms verit_sum_simplify arith_special})
 
 fun prod_simplify ctxt _ t =
   SMT_Replay_Methods.prove ctxt t (fn _ =>
     simplify_arith ctxt @{thms verit_prod_simplify})
 
 end
 
 
 (* Arithmetics *)
 local
 
 val la_rw_eq_thm = @{lemma \<open>(a :: nat) = b \<or> (a \<le> b) \<or> (a \<ge> b)\<close> by auto}
 in
 fun la_rw_eq ctxt _ t = SMT_Replay_Methods.match_instantiate ctxt t la_rw_eq_thm
 
 fun la_generic_prove args ctxt _ = SMT_Replay_Arith.la_farkas args ctxt
 
 fun la_generic ctxt _ args =
   prove_abstract (SMT_Replay_Methods.abstract_arith_shallow ctxt) (la_generic_prove args) ctxt []
 
 fun lia_generic ctxt _ t =
   SMT_Replay_Methods.prove_arith_rewrite SMT_Replay_Methods.abstract_neq ctxt t
 
 fun la_disequality ctxt _ t =
   SMT_Replay_Methods.match_instantiate ctxt t @{thm verit_la_disequality}
 
 end
 
 (* Combining all together *)
 
 fun unsupported rule ctxt thms _ _ _ = SMT_Replay_Methods.replay_error ctxt "Unsupported verit rule"
   rule thms
 
 fun ignore_args f ctxt thm _ _ _ t = f ctxt thm t
 fun ignore_decls f ctxt thm args insts _ t = f ctxt thm args insts t
 fun ignore_insts f ctxt thm args _ _ t = f ctxt thm args t
 
 fun choose And = ignore_args and_rule
   | choose And_Neg = ignore_args and_neg_rule
   | choose And_Pos = ignore_args and_pos
   | choose And_Simplify = ignore_args rewrite_and_simplify
   | choose Bind = ignore_insts bind
   | choose Bool_Simplify = ignore_args rewrite_bool_simplify
   | choose Comp_Simplify = ignore_args rewrite_comp_simplify
   | choose Cong = ignore_args cong
   | choose Connective_Def = ignore_args rewrite_connective_def
   | choose Duplicate_Literals = ignore_args duplicate_literals
   | choose Eq_Congruent = ignore_args eq_congruent
   | choose Eq_Congruent_Pred = ignore_args eq_congruent_pred
   | choose Eq_Reflexive = ignore_args eq_reflexive
   | choose Eq_Simplify = ignore_args rewrite_eq_simplify
   | choose Eq_Transitive = ignore_args eq_transitive
   | choose Equiv1 = ignore_args equiv1
   | choose Equiv2 = ignore_args equiv2
   | choose Equiv_neg1 = ignore_args equiv_neg1
   | choose Equiv_neg2 = ignore_args equiv_neg2
   | choose Equiv_pos1 = ignore_args equiv_pos1
   | choose Equiv_pos2 = ignore_args equiv_pos2
   | choose Equiv_Simplify = ignore_args rewrite_equiv_simplify
   | choose False = ignore_args false_rule
   | choose Forall_Inst = ignore_decls forall_inst
   | choose Implies = ignore_args implies_rules
   | choose Implies_Neg1 = ignore_args implies_neg1
   | choose Implies_Neg2 = ignore_args implies_neg2
   | choose Implies_Pos = ignore_args implies_pos
   | choose Implies_Simplify = ignore_args rewrite_implies_simplify
   | choose ITE1 = ignore_args ite1
   | choose ITE2 = ignore_args ite2
   | choose ITE_Intro = ignore_args ite_intro
   | choose ITE_Neg1 = ignore_args ite_neg1
   | choose ITE_Neg2 = ignore_args ite_neg2
   | choose ITE_Pos1 = ignore_args ite_pos1
   | choose ITE_Pos2 = ignore_args ite_pos2
   | choose ITE_Simplify = ignore_args rewrite_ite_simplify
   | choose LA_Disequality = ignore_args la_disequality
   | choose LA_Generic = ignore_insts la_generic
   | choose LA_RW_Eq = ignore_args la_rw_eq
   | choose LA_Tautology = ignore_args SMT_Replay_Methods.arith_th_lemma_wo_shallow
   | choose LA_Totality = ignore_args SMT_Replay_Methods.arith_th_lemma_wo_shallow
   | choose LIA_Generic = ignore_args lia_generic
   | choose Local_Input = ignore_args refl
   | choose Minus_Simplify = ignore_args rewrite_minus_simplify
   | choose NLA_Generic = ignore_args SMT_Replay_Methods.arith_th_lemma_wo_shallow
   | choose Normalized_Input = ignore_args normalized_input
   | choose Not_And = ignore_args not_and_rule
   | choose Not_Equiv1 = ignore_args not_equiv1
   | choose Not_Equiv2 = ignore_args not_equiv2
   | choose Not_Implies1 = ignore_args not_implies1
   | choose Not_Implies2 = ignore_args not_implies2
   | choose Not_ITE1 = ignore_args not_ite1
   | choose Not_ITE2 = ignore_args not_ite2
   | choose Not_Not = ignore_args not_not
   | choose Not_Or = ignore_args not_or_rule
   | choose Not_Simplify = ignore_args rewrite_not_simplify
   | choose Or = ignore_args or
   | choose Or_Neg = ignore_args or_neg_rule
   | choose Or_Pos = ignore_args or_pos_rule
   | choose Or_Simplify = ignore_args rewrite_or_simplify
   | choose Prod_Simplify = ignore_args prod_simplify
   | choose Qnt_Join = ignore_args qnt_join
   | choose Qnt_Rm_Unused = ignore_args qnt_rm_unused
   | choose Onepoint = ignore_args onepoint
   | choose Qnt_Simplify = ignore_args qnt_simplify
   | choose Refl = ignore_args refl
   | choose Resolution = ignore_args unit_res
   | choose Skolem_Ex = ignore_args skolem_ex
   | choose Skolem_Forall = ignore_args skolem_forall
   | choose Subproof = ignore_args subproof
   | choose Sum_Simplify = ignore_args sum_simplify
   | choose Tautological_Clause = ignore_args tautological_clause
   | choose Theory_Resolution = ignore_args unit_res
   | choose AC_Simp = ignore_args tmp_AC_rule
   | choose Bfun_Elim = ignore_args bfun_elim
   | choose Qnt_CNF = ignore_args qnt_cnf
   | choose Trans = ignore_args trans
   | choose r = unsupported (string_of_verit_rule r)
 
 type verit_method = Proof.context -> thm list -> term -> thm
 type abs_context = int * term Termtab.table
 
 fun with_tracing rule method ctxt thms args insts decls t =
   let val _ = SMT_Replay_Methods.trace_goal ctxt rule thms t
   in method ctxt thms args insts decls t end
 
 fun method_for rule = with_tracing rule (choose (verit_rule_of rule))
 
 fun discharge ctxt [thm] t =
   SMT_Replay_Methods.prove ctxt t (fn _ =>
     resolve_tac ctxt [thm] THEN_ALL_NEW (resolve_tac ctxt @{thms refl}))
 
 end;
diff --git a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
@@ -1,480 +1,480 @@
 (*  Title:      HOL/Tools/Sledgehammer/sledgehammer_isar.ML
     Author:     Jasmin Blanchette, TU Muenchen
     Author:     Steffen Juilf Smolka, TU Muenchen
 
 Isar proof reconstruction from ATP proofs.
 *)
 
 signature SLEDGEHAMMER_ISAR =
 sig
   type atp_step_name = ATP_Proof.atp_step_name
   type ('a, 'b) atp_step = ('a, 'b) ATP_Proof.atp_step
   type 'a atp_proof = 'a ATP_Proof.atp_proof
   type stature = ATP_Problem_Generate.stature
   type one_line_params = Sledgehammer_Proof_Methods.one_line_params
 
   val trace : bool Config.T
 
   type isar_params =
     bool * (string option * string option) * Time.time * real option * bool * bool
     * (term, string) atp_step list * thm
 
   val proof_text : Proof.context -> bool -> bool option -> bool -> (unit -> isar_params) -> int ->
     one_line_params -> string
 end;
 
 structure Sledgehammer_Isar : SLEDGEHAMMER_ISAR =
 struct
 
 open ATP_Util
 open ATP_Problem
 open ATP_Problem_Generate
 open ATP_Proof
 open ATP_Proof_Reconstruct
 open Sledgehammer_Util
 open Sledgehammer_Proof_Methods
 open Sledgehammer_Isar_Proof
 open Sledgehammer_Isar_Preplay
 open Sledgehammer_Isar_Compress
 open Sledgehammer_Isar_Minimize
 
 structure String_Redirect = ATP_Proof_Redirect(
   type key = atp_step_name
   val ord = fn ((s, _ : string list), (s', _)) => fast_string_ord (s, s')
   val string_of = fst)
 
 open String_Redirect
 
 val trace = Attrib.setup_config_bool \<^binding>\<open>sledgehammer_isar_trace\<close> (K false)
 
 val e_definition_rule = "definition"
 val e_skolemize_rule = "skolemize"
 val leo2_extcnf_forall_neg_rule = "extcnf_forall_neg"
 val satallax_skolemize_rule = "tab_ex"
 val vampire_skolemisation_rule = "skolemisation"
 val veriT_la_generic_rule = "la_generic"
 val veriT_simp_arith_rule = "simp_arith"
-val veriT_tmp_skolemize_rule = "tmp_skolemize"
+val veriT_skolemize_rules = Verit_Proof.skolemization_steps
 val z3_skolemize_rule = Z3_Proof.string_of_rule Z3_Proof.Skolemize
 val z3_th_lemma_rule_prefix = Z3_Proof.string_of_rule (Z3_Proof.Th_Lemma "")
 val zipperposition_cnf_rule = "cnf"
 
 val skolemize_rules =
   [e_definition_rule, e_skolemize_rule, leo2_extcnf_forall_neg_rule, satallax_skolemize_rule,
-   spass_skolemize_rule, vampire_skolemisation_rule, veriT_tmp_skolemize_rule, z3_skolemize_rule,
-   zipperposition_cnf_rule]
+   spass_skolemize_rule, vampire_skolemisation_rule, z3_skolemize_rule,
+   zipperposition_cnf_rule] @ veriT_skolemize_rules
 
 fun is_ext_rule rule = (rule = leo2_extcnf_equal_neg_rule)
 val is_maybe_ext_rule = is_ext_rule orf String.isPrefix satallax_tab_rule_prefix
 
 val is_skolemize_rule = member (op =) skolemize_rules
 fun is_arith_rule rule =
   String.isPrefix z3_th_lemma_rule_prefix rule orelse rule = veriT_simp_arith_rule orelse
   rule = veriT_la_generic_rule
 
 fun raw_label_of_num num = (num, 0)
 
 fun label_of_clause [(num, _)] = raw_label_of_num num
   | label_of_clause c = (space_implode "___" (map (fst o raw_label_of_num o fst) c), 0)
 
 fun add_global_fact ss = apsnd (union (op =) ss)
 
 fun add_fact_of_dependency [(_, ss as _ :: _)] = add_global_fact ss
   | add_fact_of_dependency names = apfst (insert (op =) (label_of_clause names))
 
 fun add_line_pass1 (line as (name, role, t, rule, [])) lines =
     (* No dependencies: lemma (for Z3), fact, conjecture, or (for Vampire) internal facts or
        definitions. *)
     if role = Conjecture orelse role = Negated_Conjecture then
       line :: lines
     else if t aconv \<^prop>\<open>True\<close> then
       map (replace_dependencies_in_line (name, [])) lines
     else if role = Lemma orelse role = Hypothesis orelse is_arith_rule rule then
       line :: lines
     else if role = Axiom then
       lines (* axioms (facts) need no proof lines *)
     else
       map (replace_dependencies_in_line (name, [])) lines
   | add_line_pass1 line lines = line :: lines
 
 fun add_lines_pass2 res [] = rev res
   | add_lines_pass2 res ((line as (name, role, t, rule, deps)) :: lines) =
     let
       fun normalize role =
         role = Conjecture ? (HOLogic.dest_Trueprop #> s_not #> HOLogic.mk_Trueprop)
 
       val norm_t = normalize role t
       val is_duplicate =
         exists (fn (prev_name, prev_role, prev_t, _, _) =>
             (prev_role = Hypothesis andalso prev_t aconv t) orelse
             (member (op =) deps prev_name andalso
              Term.aconv_untyped (normalize prev_role prev_t, norm_t)))
           res
 
       fun looks_boring () = t aconv \<^prop>\<open>False\<close> orelse length deps < 2
 
       fun is_skolemizing_line (_, _, _, rule', deps') =
         is_skolemize_rule rule' andalso member (op =) deps' name
 
       fun is_before_skolemize_rule () = exists is_skolemizing_line lines
     in
       if is_duplicate orelse
           (role = Plain andalso not (is_skolemize_rule rule) andalso
            not (is_ext_rule rule) andalso not (is_arith_rule rule) andalso
            not (null lines) andalso looks_boring () andalso not (is_before_skolemize_rule ())) then
         add_lines_pass2 res (map (replace_dependencies_in_line (name, deps)) lines)
       else
         add_lines_pass2 (line :: res) lines
     end
 
 type isar_params =
   bool * (string option * string option) * Time.time * real option * bool * bool
   * (term, string) atp_step list * thm
 
 val basic_systematic_methods = [Metis_Method (NONE, NONE), Meson_Method, Blast_Method, SATx_Method]
 val basic_simp_based_methods = [Auto_Method, Simp_Method, Fastforce_Method, Force_Method]
 val basic_arith_methods = [Linarith_Method, Presburger_Method, Algebra_Method]
 
 val arith_methods = basic_arith_methods @ basic_simp_based_methods @ basic_systematic_methods
 val systematic_methods =
   basic_systematic_methods @ basic_arith_methods @ basic_simp_based_methods @
   [Metis_Method (SOME full_typesN, NONE), Metis_Method (SOME no_typesN, NONE)]
 val rewrite_methods = basic_simp_based_methods @ basic_systematic_methods @ basic_arith_methods
 val skolem_methods = Moura_Method :: systematic_methods
 
 fun isar_proof_text ctxt debug num_chained isar_proofs smt_proofs isar_params
     (one_line_params as ((used_facts, (_, one_line_play)), banner, subgoal, subgoal_count)) =
   let
     val _ = if debug then writeln "Constructing Isar proof..." else ()
 
     fun generate_proof_text () =
       let
         val (verbose, alt_metis_args, preplay_timeout, compress, try0, minimize, atp_proof0, goal) =
           isar_params ()
       in
         if null atp_proof0 then
           one_line_proof_text ctxt 0 one_line_params
         else
           let
             val systematic_methods' = insert (op =) (Metis_Method alt_metis_args) systematic_methods
 
             fun massage_methods (meths as meth :: _) =
               if not try0 then [meth]
               else if smt_proofs then SMT_Method :: meths
               else meths
 
             val (params, _, concl_t) = strip_subgoal goal subgoal ctxt
             val fixes = map (fn (s, T) => (Binding.name s, SOME T, NoSyn)) params
             val ctxt = ctxt |> Variable.set_body false |> Proof_Context.add_fixes fixes |> snd
 
             val do_preplay = preplay_timeout <> Time.zeroTime
             val compress =
               (case compress of
                 NONE => if isar_proofs = NONE andalso do_preplay then 1000.0 else 10.0
               | SOME n => n)
 
             fun is_fixed ctxt = Variable.is_declared ctxt orf Name.is_skolem
             fun skolems_of ctxt t = Term.add_frees t [] |> filter_out (is_fixed ctxt o fst) |> rev
 
             fun get_role keep_role ((num, _), role, t, rule, _) =
               if keep_role role then SOME ((raw_label_of_num num, t), rule) else NONE
 
             val trace = Config.get ctxt trace
 
             val string_of_atp_steps =
               let val to_string = ATP_Proof.string_of_atp_step (Syntax.string_of_term ctxt) I in
                 enclose "[\n" "\n]" o cat_lines o map (enclose "  " "," o to_string)
               end
 
             val atp_proof = atp_proof0
               |> trace ? tap (tracing o prefix "atp_proof0 = " o string_of_atp_steps)
               |> (fn x => fold_rev add_line_pass1 x [])
               |> add_lines_pass2 []
               |> trace ? tap (tracing o prefix "atp_proof = " o string_of_atp_steps)
 
             val conjs =
               map_filter (fn (name, role, _, _, _) =>
                   if member (op =) [Conjecture, Negated_Conjecture] role then SOME name else NONE)
                 atp_proof
             val assms = map_filter (Option.map fst o get_role (curry (op =) Hypothesis)) atp_proof
 
             fun add_lemma ((l, t), rule) ctxt =
               let
                 val (skos, meths) =
                   (if is_skolemize_rule rule then (skolems_of ctxt t, skolem_methods)
                    else if is_arith_rule rule then ([], arith_methods)
                    else ([], rewrite_methods))
                   ||> massage_methods
               in
                 (Prove ([], skos, l, t, [], ([], []), meths, ""),
                  ctxt |> not (null skos) ? (Variable.add_fixes (map fst skos) #> snd))
               end
 
             val (lems, _) =
               fold_map add_lemma (map_filter (get_role (curry (op =) Lemma)) atp_proof) ctxt
 
             val bot = #1 (List.last atp_proof)
 
             val refute_graph =
               atp_proof
               |> map (fn (name, _, _, _, from) => (from, name))
               |> make_refute_graph bot
               |> fold (Atom_Graph.default_node o rpair ()) conjs
 
             val axioms = axioms_of_refute_graph refute_graph conjs
 
             val tainted = tainted_atoms_of_refute_graph refute_graph conjs
             val is_clause_tainted = exists (member (op =) tainted)
             val steps =
               Symtab.empty
               |> fold (fn (name as (s, _), role, t, rule, _) =>
                   Symtab.update_new (s, (rule, t
                     |> (if is_clause_tainted [name] then
                           HOLogic.dest_Trueprop
                           #> role <> Conjecture ? s_not
                           #> fold exists_of (map Var (Term.add_vars t []))
                           #> HOLogic.mk_Trueprop
                         else
                           I))))
                 atp_proof
 
             fun is_referenced_in_step _ (Let _) = false
               | is_referenced_in_step l (Prove (_, _, _, _, subs, (ls, _), _, _)) =
                 member (op =) ls l orelse exists (is_referenced_in_proof l) subs
             and is_referenced_in_proof l (Proof (_, _, steps)) =
               exists (is_referenced_in_step l) steps
 
             fun insert_lemma_in_step lem
                 (step as Prove (qs, fix, l, t, subs, (ls, gs), meths, comment)) =
               let val l' = the (label_of_isar_step lem) in
                 if member (op =) ls l' then
                   [lem, step]
                 else
                   let val refs = map (is_referenced_in_proof l') subs in
                     if length (filter I refs) = 1 then
                       let
                         val subs' = map2 (fn false => I | true => insert_lemma_in_proof lem) refs
                           subs
                       in
                         [Prove (qs, fix, l, t, subs', (ls, gs), meths, comment)]
                       end
                     else
                       [lem, step]
                   end
               end
             and insert_lemma_in_steps lem [] = [lem]
               | insert_lemma_in_steps lem (step :: steps) =
                 if is_referenced_in_step (the (label_of_isar_step lem)) step then
                   insert_lemma_in_step lem step @ steps
                 else
                   step :: insert_lemma_in_steps lem steps
             and insert_lemma_in_proof lem (Proof (fix, assms, steps)) =
               Proof (fix, assms, insert_lemma_in_steps lem steps)
 
             val rule_of_clause_id = fst o the o Symtab.lookup steps o fst
 
             val finish_off = close_form #> rename_bound_vars
 
             fun prop_of_clause [(num, _)] = Symtab.lookup steps num |> the |> snd |> finish_off
               | prop_of_clause names =
                 let
                   val lits =
                     map (HOLogic.dest_Trueprop o snd) (map_filter (Symtab.lookup steps o fst) names)
                 in
                   (case List.partition (can HOLogic.dest_not) lits of
                     (negs as _ :: _, pos as _ :: _) =>
                     s_imp (Library.foldr1 s_conj (map HOLogic.dest_not negs),
                       Library.foldr1 s_disj pos)
                   | _ => fold (curry s_disj) lits \<^term>\<open>False\<close>)
                 end
                 |> HOLogic.mk_Trueprop |> finish_off
 
             fun maybe_show outer c = if outer andalso eq_set (op =) (c, conjs) then [Show] else []
 
             fun isar_steps outer predecessor accum [] =
                 accum
                 |> (if tainted = [] then
                       (* e.g., trivial, empty proof by Z3 *)
                       cons (Prove (if outer then [Show] else [], [], no_label, concl_t, [],
                         sort_facts (the_list predecessor, []), massage_methods systematic_methods',
                         ""))
                     else
                       I)
                 |> rev
               | isar_steps outer _ accum (Have (id, (gamma, c)) :: infs) =
                 let
                   val l = label_of_clause c
                   val t = prop_of_clause c
                   val rule = rule_of_clause_id id
                   val skolem = is_skolemize_rule rule
 
                   val deps = ([], [])
                     |> fold add_fact_of_dependency gamma
                     |> is_maybe_ext_rule rule ? add_global_fact [short_thm_name ctxt ext]
                     |> sort_facts
                   val meths =
                     (if skolem then skolem_methods
                      else if is_arith_rule rule then arith_methods
                      else systematic_methods')
                     |> massage_methods
 
                   fun prove sub facts = Prove (maybe_show outer c, [], l, t, sub, facts, meths, "")
                   fun steps_of_rest step = isar_steps outer (SOME l) (step :: accum) infs
                 in
                   if is_clause_tainted c then
                     (case gamma of
                       [g] =>
                       if skolem andalso is_clause_tainted g then
                         let
                           val skos = skolems_of ctxt (prop_of_clause g)
                           val subproof = Proof (skos, [], rev accum)
                         in
                           isar_steps outer (SOME l) [prove [subproof] ([], [])] infs
                         end
                       else
                         steps_of_rest (prove [] deps)
                     | _ => steps_of_rest (prove [] deps))
                   else
                     steps_of_rest
                       (if skolem then
                          (case skolems_of ctxt t of
                            [] => prove [] deps
                          | skos => Prove ([], skos, l, t, [], deps, meths, ""))
                        else
                          prove [] deps)
                 end
               | isar_steps outer predecessor accum (Cases cases :: infs) =
                 let
                   fun isar_case (c, subinfs) =
                     isar_proof false [] [(label_of_clause c, prop_of_clause c)] [] subinfs
                   val c = succedent_of_cases cases
                   val l = label_of_clause c
                   val t = prop_of_clause c
                   val step =
                     Prove (maybe_show outer c, [], l, t,
                       map isar_case (filter_out (null o snd) cases),
                       sort_facts (the_list predecessor, []), massage_methods systematic_methods',
                       "")
                 in
                   isar_steps outer (SOME l) (step :: accum) infs
                 end
             and isar_proof outer fix assms lems infs =
               Proof (fix, assms,
                 fold_rev insert_lemma_in_steps lems (isar_steps outer NONE [] infs))
 
             val canonical_isar_proof =
               refute_graph
               |> trace ? tap (tracing o prefix "Refute graph:\n" o string_of_refute_graph)
               |> redirect_graph axioms tainted bot
               |> trace ? tap (tracing o prefix "Direct proof:\n" o string_of_direct_proof)
               |> isar_proof true params assms lems
               |> postprocess_isar_proof_remove_show_stuttering
               |> postprocess_isar_proof_remove_unreferenced_steps I
               |> relabel_isar_proof_canonically
 
             val ctxt = ctxt |> enrich_context_with_local_facts canonical_isar_proof
 
             val preplay_data = Unsynchronized.ref Canonical_Label_Tab.empty
 
             val _ = fold_isar_steps (fn meth =>
                 K (set_preplay_outcomes_of_isar_step ctxt preplay_timeout preplay_data meth []))
               (steps_of_isar_proof canonical_isar_proof) ()
 
             fun str_of_preplay_outcome outcome =
               if Lazy.is_finished outcome then string_of_play_outcome (Lazy.force outcome) else "?"
             fun str_of_meth l meth =
               string_of_proof_method [] meth ^ " " ^
               str_of_preplay_outcome
                 (preplay_outcome_of_isar_step_for_method (!preplay_data) l meth)
             fun comment_of l = map (str_of_meth l) #> commas
 
             fun trace_isar_proof label proof =
               if trace then
                 tracing (timestamp () ^ "\n" ^ label ^ ":\n\n" ^
                   string_of_isar_proof ctxt subgoal subgoal_count
                     (comment_isar_proof comment_of proof) ^ "\n")
               else
                 ()
 
             fun comment_of l (meth :: _) =
               (case (verbose,
                   Lazy.force (preplay_outcome_of_isar_step_for_method (!preplay_data) l meth)) of
                 (false, Played _) => ""
               | (_, outcome) => string_of_play_outcome outcome)
 
             val (play_outcome, isar_proof) =
               canonical_isar_proof
               |> tap (trace_isar_proof "Original")
               |> compress_isar_proof ctxt compress preplay_timeout preplay_data
               |> tap (trace_isar_proof "Compressed")
               |> postprocess_isar_proof_remove_unreferenced_steps
                    (keep_fastest_method_of_isar_step (!preplay_data)
                     #> minimize ? minimize_isar_step_dependencies ctxt preplay_data)
               |> tap (trace_isar_proof "Minimized")
               |> `(preplay_outcome_of_isar_proof (!preplay_data))
               ||> (comment_isar_proof comment_of
                    #> chain_isar_proof
                    #> kill_useless_labels_in_isar_proof
                    #> relabel_isar_proof_nicely
                    #> rationalize_obtains_in_isar_proofs ctxt)
           in
             (case (num_chained, add_isar_steps (steps_of_isar_proof isar_proof) 0) of
               (0, 1) =>
               one_line_proof_text ctxt 0
                 (if is_less (play_outcome_ord (play_outcome, one_line_play)) then
                    (case isar_proof of
                      Proof (_, _, [Prove (_, _, _, _, _, (_, gfs), meth :: _, _)]) =>
                      let
                        val used_facts' =
                          map_filter (fn s =>
                             if exists (fn (s', (sc, _)) => s' = s andalso sc = Chained)
                                 used_facts then
                               NONE
                             else
                               SOME (s, (Global, General))) gfs
                      in
                        ((used_facts', (meth, play_outcome)), banner, subgoal, subgoal_count)
                      end)
                  else
                    one_line_params) ^
               (if isar_proofs = SOME true then "\n(No Isar proof available.)" else "")
             | (_, num_steps) =>
               let
                 val msg =
                   (if verbose then [string_of_int num_steps ^ " step" ^ plural_s num_steps]
                    else []) @
                   (if do_preplay then [string_of_play_outcome play_outcome] else [])
               in
                 one_line_proof_text ctxt 0 one_line_params ^
                 "\n\nIsar proof" ^ (commas msg |> not (null msg) ? enclose " (" ")") ^ ":\n" ^
                 Active.sendback_markup_command
                   (string_of_isar_proof ctxt subgoal subgoal_count isar_proof)
               end)
           end
       end
   in
     if debug then
       generate_proof_text ()
     else
       (case try generate_proof_text () of
         SOME s => s
       | NONE =>
         one_line_proof_text ctxt 0 one_line_params ^
         (if isar_proofs = SOME true then "\nWarning: Isar proof construction failed" else ""))
   end
 
 fun isar_proof_would_be_a_good_idea (_, play) =
   (case play of
     Played _ => false
   | Play_Timed_Out time => time > Time.zeroTime
   | Play_Failed => true)
 
 fun proof_text ctxt debug isar_proofs smt_proofs isar_params num_chained
     (one_line_params as ((_, preplay), _, _, _)) =
   (if isar_proofs = SOME true orelse
       (isar_proofs = NONE andalso isar_proof_would_be_a_good_idea preplay) then
      isar_proof_text ctxt debug num_chained isar_proofs smt_proofs isar_params
    else
      one_line_proof_text ctxt num_chained) one_line_params
 
 end;