add reconstruction by veriT in method smt
authorfleury <Mathias.Fleury@mpi-inf.mpg.de>
Tue Oct 30 16:24:04 2018 +0100 (7 months ago)
changeset 692058050734eee3e
parent 69204 d5ab1636660b
child 69206 9660bbf5ce7e
add reconstruction by veriT in method smt
CONTRIBUTORS
NEWS
src/HOL/SMT.thy
src/HOL/Tools/SMT/conj_disj_perm.ML
src/HOL/Tools/SMT/smt_config.ML
src/HOL/Tools/SMT/smt_real.ML
src/HOL/Tools/SMT/smt_solver.ML
src/HOL/Tools/SMT/smt_systems.ML
src/HOL/Tools/SMT/smtlib_proof.ML
src/HOL/Tools/SMT/verit_proof.ML
src/HOL/Tools/SMT/verit_proof_parse.ML
src/HOL/Tools/SMT/verit_replay.ML
src/HOL/Tools/SMT/verit_replay_methods.ML
src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
     1.1 --- a/CONTRIBUTORS	Tue Oct 30 16:24:01 2018 +0100
     1.2 +++ b/CONTRIBUTORS	Tue Oct 30 16:24:04 2018 +0100
     1.3 @@ -6,6 +6,9 @@
     1.4  Contributions to this Isabelle version
     1.5  --------------------------------------
     1.6  
     1.7 +* October 2018: Mathias Fleury
     1.8 +  Proof reconstruction for the SMT solver veriT in the smt method
     1.9 +
    1.10  
    1.11  Contributions to Isabelle2018
    1.12  -----------------------------
     2.1 --- a/NEWS	Tue Oct 30 16:24:01 2018 +0100
     2.2 +++ b/NEWS	Tue Oct 30 16:24:04 2018 +0100
     2.3 @@ -55,6 +55,8 @@
     2.4  * Sledgehammer: The URL for SystemOnTPTP, which is used by remote
     2.5  provers, has been updated.
     2.6  
     2.7 +* SMT: reconstruction is now possible using the SMT solver veriT.
     2.8 +
     2.9  * Session HOL-SPARK: .prv files are no longer written to the
    2.10  file-system, but exported to the session database. Results may be
    2.11  retrieved with the "isabelle export" command-line tool like this:
     3.1 --- a/src/HOL/SMT.thy	Tue Oct 30 16:24:01 2018 +0100
     3.2 +++ b/src/HOL/SMT.thy	Tue Oct 30 16:24:04 2018 +0100
     3.3 @@ -190,6 +190,100 @@
     3.4    by (simp add: z3mod_def)
     3.5  
     3.6  
     3.7 +subsection \<open>Extra theorems for veriT reconstruction\<close>
     3.8 +
     3.9 +lemma verit_sko_forall: \<open>(\<forall>x. P x) \<longleftrightarrow> P (SOME x. \<not>P x)\<close>
    3.10 +  using someI[of \<open>\<lambda>x. \<not>P x\<close>]
    3.11 +  by auto
    3.12 +
    3.13 +lemma verit_sko_forall': \<open>P (SOME x. \<not>P x) = A \<Longrightarrow> (\<forall>x. P x) = A\<close>
    3.14 +  by (subst verit_sko_forall)
    3.15 +
    3.16 +lemma verit_sko_forall_indirect: \<open>x = (SOME x. \<not>P x) \<Longrightarrow> (\<forall>x. P x) \<longleftrightarrow> P x\<close>
    3.17 +  using someI[of \<open>\<lambda>x. \<not>P x\<close>]
    3.18 +  by auto
    3.19 +
    3.20 +lemma verit_sko_ex: \<open>(\<exists>x. P x) \<longleftrightarrow> P (SOME x. P x)\<close>
    3.21 +  using someI[of \<open>\<lambda>x. P x\<close>]
    3.22 +  by auto
    3.23 +
    3.24 +lemma verit_sko_ex': \<open>P (SOME x. P x) = A \<Longrightarrow> (\<exists>x. P x) = A\<close>
    3.25 +  by (subst verit_sko_ex)
    3.26 +
    3.27 +lemma verit_sko_ex_indirect: \<open>x = (SOME x. P x) \<Longrightarrow> (\<exists>x. P x) \<longleftrightarrow> P x\<close>
    3.28 +  using someI[of \<open>\<lambda>x. P x\<close>]
    3.29 +  by auto
    3.30 +
    3.31 +lemma verit_Pure_trans:
    3.32 +  \<open>P \<equiv> Q \<Longrightarrow> Q \<Longrightarrow> P\<close>
    3.33 +  by auto
    3.34 +
    3.35 +lemma verit_if_cong:
    3.36 +  assumes \<open>b \<equiv> c\<close>
    3.37 +    and \<open>c \<Longrightarrow> x \<equiv> u\<close>
    3.38 +    and \<open>\<not> c \<Longrightarrow> y \<equiv> v\<close>
    3.39 +  shows \<open>(if b then x else y) \<equiv> (if c then u else v)\<close>
    3.40 +  using assms if_cong[of b c x u] by auto
    3.41 +
    3.42 +lemma verit_if_weak_cong':
    3.43 +  \<open>b \<equiv> c \<Longrightarrow> (if b then x else y) \<equiv> (if c then x else y)\<close>
    3.44 +  by auto
    3.45 +
    3.46 +lemma verit_ite_intro_simp:
    3.47 +  \<open>(if c then (a :: 'a) = (if c then P else Q') else Q) = (if c then a = P else Q)\<close>
    3.48 +  \<open>(if c then R else b = (if c then R' else Q')) =
    3.49 +    (if c then R else b = Q')\<close>
    3.50 +  \<open>(if c then a' = a' else b' = b')\<close>
    3.51 +  by (auto split: if_splits)
    3.52 +
    3.53 +lemma verit_or_neg:
    3.54 +   \<open>(A \<Longrightarrow> B) \<Longrightarrow> B \<or> \<not>A\<close>
    3.55 +   \<open>(\<not>A \<Longrightarrow> B) \<Longrightarrow> B \<or> A\<close>
    3.56 +  by auto
    3.57 +
    3.58 +lemma verit_subst_bool: \<open>P \<Longrightarrow> f True \<Longrightarrow> f P\<close>
    3.59 +  by auto
    3.60 +
    3.61 +lemma verit_and_pos:
    3.62 +  \<open>(a \<Longrightarrow> \<not>b \<or> A) \<Longrightarrow> \<not>(a \<and> b) \<or> A\<close>
    3.63 +  \<open>(a \<Longrightarrow> A) \<Longrightarrow> \<not>a \<or> A\<close>
    3.64 +  \<open>(\<not>a \<Longrightarrow> A) \<Longrightarrow> a \<or> A\<close>
    3.65 +  by blast+
    3.66 +
    3.67 +lemma verit_la_generic:
    3.68 +  \<open>(a::int) \<le> x \<or> a = x \<or> a \<ge> x\<close>
    3.69 +  by linarith
    3.70 +
    3.71 +lemma verit_tmp_bfun_elim:
    3.72 +  \<open>(if b then P True else P False) = P b\<close>
    3.73 +  by (cases b) auto
    3.74 +
    3.75 +lemma verit_eq_true_simplify:
    3.76 +  \<open>(P = True) \<equiv> P\<close>
    3.77 +  by auto
    3.78 +
    3.79 +lemma verit_and_neg:
    3.80 +  \<open>B \<or> B' \<Longrightarrow> (A \<and> B) \<or> \<not>A \<or> B'\<close>
    3.81 +  \<open>B \<or> B' \<Longrightarrow> (\<not>A \<and> B) \<or> A \<or> B'\<close>
    3.82 +  by auto
    3.83 +
    3.84 +lemma verit_forall_inst:
    3.85 +  \<open>A \<longleftrightarrow> B \<Longrightarrow> \<not>A \<or> B\<close>
    3.86 +  \<open>\<not>A \<longleftrightarrow> B \<Longrightarrow> A \<or> B\<close>
    3.87 +  \<open>A \<longleftrightarrow> B \<Longrightarrow> \<not>B \<or> A\<close>
    3.88 +  \<open>A \<longleftrightarrow> \<not>B \<Longrightarrow> B \<or> A\<close>
    3.89 +  \<open>A \<longrightarrow> B \<Longrightarrow> \<not>A \<or> B\<close>
    3.90 +  \<open>\<not>A \<longrightarrow> B \<Longrightarrow> A \<or> B\<close>
    3.91 +  by blast+
    3.92 +
    3.93 +lemma verit_eq_transitive:
    3.94 +  \<open>A = B \<Longrightarrow> B = C \<Longrightarrow> A = C\<close>
    3.95 +  \<open>A = B \<Longrightarrow> C = B \<Longrightarrow> A = C\<close>
    3.96 +  \<open>B = A \<Longrightarrow> B = C \<Longrightarrow> A = C\<close>
    3.97 +  \<open>B = A \<Longrightarrow> C = B \<Longrightarrow> A = C\<close>
    3.98 +  by auto
    3.99 +
   3.100 +
   3.101  subsection \<open>Setup\<close>
   3.102  
   3.103  ML_file "Tools/SMT/smt_util.ML"
   3.104 @@ -218,6 +312,8 @@
   3.105  ML_file "Tools/SMT/z3_replay_rules.ML"
   3.106  ML_file "Tools/SMT/z3_replay_methods.ML"
   3.107  ML_file "Tools/SMT/z3_replay.ML"
   3.108 +ML_file "Tools/SMT/verit_replay_methods.ML"
   3.109 +ML_file "Tools/SMT/verit_replay.ML"
   3.110  ML_file "Tools/SMT/smt_systems.ML"
   3.111  
   3.112  method_setup smt = \<open>
   3.113 @@ -276,7 +372,7 @@
   3.114  
   3.115  declare [[cvc3_options = ""]]
   3.116  declare [[cvc4_options = "--full-saturate-quant --inst-when=full-last-call --inst-no-entail --term-db-mode=relevant --multi-trigger-linear"]]
   3.117 -declare [[verit_options = "--index-sorts --index-fresh-sorts"]]
   3.118 +declare [[verit_options = "--index-fresh-sorts"]]
   3.119  declare [[z3_options = ""]]
   3.120  
   3.121  text \<open>
     4.1 --- a/src/HOL/Tools/SMT/conj_disj_perm.ML	Tue Oct 30 16:24:01 2018 +0100
     4.2 +++ b/src/HOL/Tools/SMT/conj_disj_perm.ML	Tue Oct 30 16:24:04 2018 +0100
     4.3 @@ -124,4 +124,4 @@
     4.4        resolve_tac ctxt [prove_conj_disj_perm ct (Thm.dest_binop (Thm.dest_arg ct))] i
     4.5    | _ => no_tac))
     4.6  
     4.7 -end
     4.8 +end;
     5.1 --- a/src/HOL/Tools/SMT/smt_config.ML	Tue Oct 30 16:24:01 2018 +0100
     5.2 +++ b/src/HOL/Tools/SMT/smt_config.ML	Tue Oct 30 16:24:04 2018 +0100
     5.3 @@ -47,6 +47,7 @@
     5.4    val trace_msg: Proof.context -> ('a -> string) -> 'a -> unit
     5.5    val verbose_msg: Proof.context -> ('a -> string) -> 'a -> unit
     5.6    val statistics_msg: Proof.context -> ('a -> string) -> 'a -> unit
     5.7 +  val veriT_msg: Proof.context -> (unit -> 'a) -> unit
     5.8  
     5.9    (*certificates*)
    5.10    val select_certificates: string -> Context.generic -> Context.generic
    5.11 @@ -179,6 +180,7 @@
    5.12  val read_only_certificates = Attrib.setup_config_bool \<^binding>\<open>smt_read_only_certificates\<close> (K false)
    5.13  val verbose = Attrib.setup_config_bool \<^binding>\<open>smt_verbose\<close> (K true)
    5.14  val trace = Attrib.setup_config_bool \<^binding>\<open>smt_trace\<close> (K false)
    5.15 +val trace_veriT = Attrib.setup_config_bool \<^binding>\<open>smt_debug_verit\<close> (K false)
    5.16  val statistics = Attrib.setup_config_bool \<^binding>\<open>smt_statistics\<close> (K false)
    5.17  val monomorph_limit = Attrib.setup_config_int \<^binding>\<open>smt_monomorph_limit\<close> (K 10)
    5.18  val monomorph_instances = Attrib.setup_config_int \<^binding>\<open>smt_monomorph_instances\<close> (K 500)
    5.19 @@ -198,6 +200,8 @@
    5.20  fun trace_msg ctxt = cond_trace (Config.get ctxt trace)
    5.21  fun statistics_msg ctxt = cond_trace (Config.get ctxt statistics)
    5.22  
    5.23 +fun veriT_msg ctxt (x : unit -> 'a) = if (Config.get ctxt trace_veriT) then ignore(x ()) else ()
    5.24 +
    5.25  
    5.26  (* tools *)
    5.27  
     6.1 --- a/src/HOL/Tools/SMT/smt_real.ML	Tue Oct 30 16:24:01 2018 +0100
     6.2 +++ b/src/HOL/Tools/SMT/smt_real.ML	Tue Oct 30 16:24:04 2018 +0100
     6.3 @@ -110,6 +110,6 @@
     6.4    SMTLIB_Interface.add_logic (10, smtlib_logic) #>
     6.5    setup_builtins #>
     6.6    Z3_Interface.add_mk_builtins z3_mk_builtins #>
     6.7 -  Z3_Replay_Util.add_simproc real_linarith_proc))
     6.8 +  SMT_Replay.add_simproc real_linarith_proc))
     6.9  
    6.10  end;
     7.1 --- a/src/HOL/Tools/SMT/smt_solver.ML	Tue Oct 30 16:24:01 2018 +0100
     7.2 +++ b/src/HOL/Tools/SMT/smt_solver.ML	Tue Oct 30 16:24:04 2018 +0100
     7.3 @@ -90,12 +90,14 @@
     7.4  
     7.5      val _ = SMT_Config.trace_msg ctxt (pretty "Problem:" o split_lines) input
     7.6  
     7.7 -    val {redirected_output = res, output = err, return_code} =
     7.8 -      SMT_Config.with_timeout ctxt (run ctxt name mk_cmd) input
     7.9 +    val ({elapsed, ...}, {redirected_output = res, output = err, return_code}) =
    7.10 +      Timing.timing (SMT_Config.with_timeout ctxt (run ctxt name mk_cmd)) input
    7.11      val _ = SMT_Config.trace_msg ctxt (pretty "Solver:") err
    7.12  
    7.13      val output = drop_suffix (equal "") res
    7.14      val _ = SMT_Config.trace_msg ctxt (pretty "Result:") output
    7.15 +    val _ = SMT_Config.trace_msg ctxt (pretty "Time (ms):") [@{make_string} (Time.toMilliseconds elapsed)]
    7.16 +    val _ = SMT_Config.statistics_msg ctxt (pretty "Time (ms):") [@{make_string} (Time.toMilliseconds elapsed)]
    7.17  
    7.18      val _ = member (op =) normal_return_codes return_code orelse
    7.19        raise SMT_Failure.SMT (SMT_Failure.Abnormal_Termination return_code)
     8.1 --- a/src/HOL/Tools/SMT/smt_systems.ML	Tue Oct 30 16:24:01 2018 +0100
     8.2 +++ b/src/HOL/Tools/SMT/smt_systems.ML	Tue Oct 30 16:24:04 2018 +0100
     8.3 @@ -119,7 +119,7 @@
     8.4    avail = make_avail "VERIT",
     8.5    command = make_command "VERIT",
     8.6    options = (fn ctxt => [
     8.7 -    "--proof-version=1",
     8.8 +    "--proof-version=2",
     8.9      "--proof-prune",
    8.10      "--proof-merge",
    8.11      "--disable-print-success",
    8.12 @@ -129,7 +129,7 @@
    8.13    default_max_relevant = 200 (* FUDGE *),
    8.14    outcome = on_first_non_unsupported_line (outcome_of "unsat" "sat" "unknown"),
    8.15    parse_proof = SOME (K VeriT_Proof_Parse.parse_proof),
    8.16 -  replay = NONE }
    8.17 +  replay = SOME Verit_Replay.replay }
    8.18  
    8.19  end
    8.20  
     9.1 --- a/src/HOL/Tools/SMT/smtlib_proof.ML	Tue Oct 30 16:24:01 2018 +0100
     9.2 +++ b/src/HOL/Tools/SMT/smtlib_proof.ML	Tue Oct 30 16:24:04 2018 +0100
     9.3 @@ -265,10 +265,13 @@
     9.4  fun dest_binding (SMTLIB.S [SMTLIB.Sym name, t]) = (name, Tree t)
     9.5    | dest_binding b = raise SMTLIB_PARSE ("bad SMT let binding format", b)
     9.6  
     9.7 +fun mk_choice (x, T, P) =  HOLogic.choice_const T $ absfree (x, T) P
     9.8 +
     9.9  fun term_of t cx =
    9.10    (case t of
    9.11      SMTLIB.S [SMTLIB.Sym "forall", SMTLIB.S vars, body] => quant HOLogic.mk_all vars body cx
    9.12    | SMTLIB.S [SMTLIB.Sym "exists", SMTLIB.S vars, body] => quant HOLogic.mk_exists vars body cx
    9.13 +  | SMTLIB.S [SMTLIB.Sym "choice", SMTLIB.S vars, body] => quant mk_choice vars body cx
    9.14    | SMTLIB.S [SMTLIB.Sym "let", SMTLIB.S bindings, body] =>
    9.15        with_bindings (map dest_binding bindings) (term_of body) cx
    9.16    | SMTLIB.S (SMTLIB.Sym "!" :: t :: _) => term_of t cx
    10.1 --- a/src/HOL/Tools/SMT/verit_proof.ML	Tue Oct 30 16:24:01 2018 +0100
    10.2 +++ b/src/HOL/Tools/SMT/verit_proof.ML	Tue Oct 30 16:24:04 2018 +0100
    10.3 @@ -12,20 +12,36 @@
    10.4      id: string,
    10.5      rule: string,
    10.6      prems: string list,
    10.7 +    proof_ctxt: term list,
    10.8      concl: term,
    10.9      fixes: string list}
   10.10  
   10.11 +  datatype veriT_replay_node = VeriT_Replay_Node of {
   10.12 +    id: string,
   10.13 +    rule: string,
   10.14 +    args: term list,
   10.15 +    prems: string list,
   10.16 +    proof_ctxt: term list,
   10.17 +    concl: term,
   10.18 +    bounds: (string * typ) list,
   10.19 +    subproof: (string * typ) list * term list * veriT_replay_node list}
   10.20 +
   10.21    (*proof parser*)
   10.22    val parse: typ Symtab.table -> term Symtab.table -> string list ->
   10.23      Proof.context -> veriT_step list * Proof.context
   10.24 +  val parse_replay: typ Symtab.table -> term Symtab.table -> string list ->
   10.25 +    Proof.context -> veriT_replay_node list * Proof.context
   10.26  
   10.27 +  val map_replay_prems: (string list -> string list) -> veriT_replay_node -> veriT_replay_node
   10.28    val veriT_step_prefix : string
   10.29    val veriT_input_rule: string
   10.30 +  val veriT_normalized_input_rule: string
   10.31    val veriT_la_generic_rule : string
   10.32    val veriT_rewrite_rule : string
   10.33    val veriT_simp_arith_rule : string
   10.34 -  val veriT_tmp_ite_elim_rule : string
   10.35    val veriT_tmp_skolemize_rule : string
   10.36 +  val veriT_subproof_rule : string
   10.37 +  val veriT_local_input_rule : string
   10.38  end;
   10.39  
   10.40  structure VeriT_Proof: VERIT_PROOF =
   10.41 @@ -33,33 +49,66 @@
   10.42  
   10.43  open SMTLIB_Proof
   10.44  
   10.45 +datatype raw_veriT_node = Raw_VeriT_Node of {
   10.46 +  id: string,
   10.47 +  rule: string,
   10.48 +  args: SMTLIB.tree,
   10.49 +  prems: string list,
   10.50 +  concl: SMTLIB.tree,
   10.51 +  subproof: raw_veriT_node list}
   10.52 +
   10.53 +fun mk_raw_node id rule args prems concl subproof =
   10.54 +  Raw_VeriT_Node {id = id, rule = rule, args = args, prems = prems, concl = concl,
   10.55 +    subproof = subproof}
   10.56 +
   10.57  datatype veriT_node = VeriT_Node of {
   10.58    id: string,
   10.59    rule: string,
   10.60    prems: string list,
   10.61 +  proof_ctxt: term list,
   10.62    concl: term,
   10.63    bounds: string list}
   10.64  
   10.65 -fun mk_node id rule prems concl bounds =
   10.66 -  VeriT_Node {id = id, rule = rule, prems = prems, concl = concl, bounds = bounds}
   10.67 +fun mk_node id rule prems proof_ctxt concl bounds =
   10.68 +  VeriT_Node {id = id, rule = rule, prems = prems, proof_ctxt = proof_ctxt, concl = concl,
   10.69 +    bounds = bounds}
   10.70 +
   10.71 +datatype veriT_replay_node = VeriT_Replay_Node of {
   10.72 +  id: string,
   10.73 +  rule: string,
   10.74 +  args: term list,
   10.75 +  prems: string list,
   10.76 +  proof_ctxt: term list,
   10.77 +  concl: term,
   10.78 +  bounds: (string * typ) list,
   10.79 +  subproof: (string * typ) list * term list * veriT_replay_node list}
   10.80 +
   10.81 +fun mk_replay_node id rule args prems proof_ctxt concl bounds subproof =
   10.82 +  VeriT_Replay_Node {id = id, rule = rule, args = args, prems = prems, proof_ctxt = proof_ctxt,
   10.83 +    concl = concl, bounds = bounds, subproof = subproof}
   10.84  
   10.85  datatype veriT_step = VeriT_Step of {
   10.86    id: string,
   10.87    rule: string,
   10.88    prems: string list,
   10.89 +  proof_ctxt: term list,
   10.90    concl: term,
   10.91    fixes: string list}
   10.92  
   10.93 -fun mk_step id rule prems concl fixes =
   10.94 -  VeriT_Step {id = id, rule = rule, prems = prems, concl = concl, fixes = fixes}
   10.95 +fun mk_step id rule prems proof_ctxt concl fixes =
   10.96 +  VeriT_Step {id = id, rule = rule, prems = prems, proof_ctxt = proof_ctxt, concl = concl,
   10.97 +    fixes = fixes}
   10.98  
   10.99  val veriT_step_prefix = ".c"
  10.100  val veriT_input_rule = "input"
  10.101  val veriT_la_generic_rule = "la_generic"
  10.102 +val veriT_normalized_input_rule = "__normalized_input" (* arbitrary *)
  10.103  val veriT_rewrite_rule = "__rewrite" (* arbitrary *)
  10.104 +val veriT_subproof_rule = "subproof"
  10.105 +val veriT_local_input_rule = "__local_input" (* arbitrary *)
  10.106  val veriT_simp_arith_rule = "simp_arith"
  10.107 -val veriT_tmp_alphaconv_rule = "tmp_alphaconv"
  10.108 -val veriT_tmp_ite_elim_rule = "tmp_ite_elim"
  10.109 +
  10.110 +(* Even the veriT developer do not know if the following rule can still appear in proofs: *)
  10.111  val veriT_tmp_skolemize_rule = "tmp_skolemize"
  10.112  
  10.113  (* proof parser *)
  10.114 @@ -69,131 +118,229 @@
  10.115    ||>> `(with_fresh_names (term_of p))
  10.116    |>> snd
  10.117  
  10.118 -(*in order to get Z3-style quantification*)
  10.119 -fun repair_quantification (SMTLIB.S (SMTLIB.Sym "forall" :: l)) =
  10.120 -    let val (quantified_vars, t) = split_last (map repair_quantification l)
  10.121 -    in
  10.122 -      SMTLIB.S (SMTLIB.Sym "forall" :: SMTLIB.S quantified_vars :: t :: [])
  10.123 -    end
  10.124 -  | repair_quantification (SMTLIB.S (SMTLIB.Sym "exists" :: l)) =
  10.125 -    let val (quantified_vars, t) = split_last (map repair_quantification l)
  10.126 -    in
  10.127 -      SMTLIB.S (SMTLIB.Sym "exists" :: SMTLIB.S quantified_vars :: t :: [])
  10.128 -    end
  10.129 -  | repair_quantification (SMTLIB.S l) = SMTLIB.S (map repair_quantification l)
  10.130 -  | repair_quantification x = x
  10.131 -
  10.132 -fun replace_bound_var_by_free_var (q $ Abs (var, ty, u)) free_var =
  10.133 -    (case List.find (fn v => String.isPrefix v var) free_var of
  10.134 -      NONE => q $ Abs (var, ty, replace_bound_var_by_free_var u free_var)
  10.135 -    | SOME _ => replace_bound_var_by_free_var (Term.subst_bound (Free (var, ty), u)) free_var)
  10.136 -  | replace_bound_var_by_free_var (u $ v) free_vars = replace_bound_var_by_free_var u free_vars $
  10.137 -     replace_bound_var_by_free_var v free_vars
  10.138 -  | replace_bound_var_by_free_var u _ = u
  10.139 -
  10.140  fun find_type_in_formula (Abs (v, T, u)) var_name =
  10.141      if String.isPrefix var_name v then SOME T else find_type_in_formula u var_name
  10.142    | find_type_in_formula (u $ v) var_name =
  10.143      (case find_type_in_formula u var_name of
  10.144        NONE => find_type_in_formula v var_name
  10.145      | some_T => some_T)
  10.146 +  | find_type_in_formula (Free(v, T)) var_name =
  10.147 +    if String.isPrefix var_name v then SOME T else NONE
  10.148    | find_type_in_formula _ _ = NONE
  10.149  
  10.150 +fun find_type_of_free_in_formula (Free (v, T) $ u) var_name =
  10.151 +    if String.isPrefix var_name v then SOME T else find_type_in_formula u var_name
  10.152 +  | find_type_of_free_in_formula (Abs (v, T, u)) var_name =
  10.153 +    if String.isPrefix var_name v then SOME T else find_type_in_formula u var_name
  10.154 +  | find_type_of_free_in_formula (u $ v) var_name =
  10.155 +    (case find_type_in_formula u var_name of
  10.156 +      NONE => find_type_in_formula v var_name
  10.157 +    | some_T => some_T)
  10.158 +  | find_type_of_free_in_formula _ _ = NONE
  10.159 +
  10.160  fun add_bound_variables_to_ctxt concl =
  10.161    fold (update_binding o
  10.162      (fn s => (s, Term (Free (s, the_default dummyT (find_type_in_formula concl s))))))
  10.163  
  10.164 -fun update_step_and_cx (node as VeriT_Node {id, rule, prems, concl, bounds}) cx =
  10.165 -  if rule = veriT_tmp_ite_elim_rule then
  10.166 -    (mk_node id rule prems concl bounds, add_bound_variables_to_ctxt concl bounds cx)
  10.167 -  else if rule = veriT_tmp_skolemize_rule then
  10.168 -    let val concl' = replace_bound_var_by_free_var concl bounds in
  10.169 -      (mk_node id rule prems concl' [], add_bound_variables_to_ctxt concl bounds cx)
  10.170 -    end
  10.171 -  else
  10.172 -    (node, cx)
  10.173 +
  10.174 +local
  10.175 +
  10.176 +  fun remove_Sym (SMTLIB.Sym y) = y
  10.177 +
  10.178 +  fun extract_symbols bds =
  10.179 +    bds
  10.180 +    |> map (fn SMTLIB.S [SMTLIB.Key _, SMTLIB.Sym x, SMTLIB.Sym y] => [x, y]
  10.181 +            | SMTLIB.S syms => map remove_Sym syms)
  10.182 +    |> flat
  10.183 +
  10.184 +  fun extract_symbols_map bds =
  10.185 +    bds
  10.186 +    |> map (fn SMTLIB.S [SMTLIB.Key _, SMTLIB.Sym x, _] => [x]
  10.187 +            | SMTLIB.S syms =>  map remove_Sym syms)
  10.188 +    |> flat
  10.189 +in
  10.190  
  10.191 -fun fix_subproof_steps ((((id_of_father_step, rule), prems), subproof), ((step_concl, bounds),
  10.192 -    cx)) =
  10.193 +fun bound_vars_by_rule "bind" (SMTLIB.S bds) = extract_symbols bds
  10.194 +  | bound_vars_by_rule "qnt_simplify" (SMTLIB.S bds) = extract_symbols_map bds
  10.195 +  | bound_vars_by_rule "sko_forall" (SMTLIB.S bds) = extract_symbols_map bds
  10.196 +  | bound_vars_by_rule "sko_ex" (SMTLIB.S bds) = extract_symbols_map bds
  10.197 +  | bound_vars_by_rule _ _ = []
  10.198 +
  10.199 +fun global_bound_vars_by_rule _ _ = []
  10.200 +
  10.201 +(* VeriT adds "?" before some variable. *)
  10.202 +fun remove_all_qm (SMTLIB.Sym v :: l) =
  10.203 +    SMTLIB.Sym (perhaps (try (unprefix "?")) v) :: remove_all_qm l
  10.204 +  | remove_all_qm (SMTLIB.S l :: l') = SMTLIB.S (remove_all_qm l) :: remove_all_qm l'
  10.205 +  | remove_all_qm (SMTLIB.Key v :: l) = SMTLIB.Key v :: remove_all_qm l
  10.206 +  | remove_all_qm (v :: l) = v :: remove_all_qm l
  10.207 +  | remove_all_qm [] = []
  10.208 +
  10.209 +fun remove_all_qm2 (SMTLIB.Sym v) = SMTLIB.Sym (perhaps (try (unprefix "?")) v)
  10.210 +  | remove_all_qm2 (SMTLIB.S l) = SMTLIB.S (remove_all_qm l)
  10.211 +  | remove_all_qm2 (SMTLIB.Key v) = SMTLIB.Key v
  10.212 +  | remove_all_qm2 v = v
  10.213 +
  10.214 +val parse_rule_and_args =
  10.215    let
  10.216 -    fun mk_prop_of_term concl =
  10.217 -      concl |> fastype_of concl = @{typ bool} ? curry (op $) @{term Trueprop}
  10.218 -    fun update_prems assumption_id prems =
  10.219 -      map (fn prem => id_of_father_step ^ prem)
  10.220 -          (filter_out (curry (op =) assumption_id) prems)
  10.221 -    fun inline_assumption assumption assumption_id
  10.222 -        (VeriT_Node {id, rule, prems, concl, bounds}) =
  10.223 -      mk_node id rule (update_prems assumption_id prems)
  10.224 -        (@{const Pure.imp} $ mk_prop_of_term assumption $ mk_prop_of_term concl) bounds
  10.225 -    fun find_input_steps_and_inline [] last_step = ([], last_step)
  10.226 -      | find_input_steps_and_inline (VeriT_Node {id = id', rule, prems, concl, bounds} :: steps)
  10.227 -          last_step =
  10.228 -        if rule = veriT_input_rule then
  10.229 -          find_input_steps_and_inline (map (inline_assumption concl id') steps) last_step
  10.230 -        else
  10.231 -          apfst (cons (mk_node (id_of_father_step ^ id') rule prems concl bounds))
  10.232 -            (find_input_steps_and_inline steps (id_of_father_step ^ id'))
  10.233 -    val (subproof', last_step_id) = find_input_steps_and_inline subproof ""
  10.234 -    val prems' =
  10.235 -      if last_step_id = "" then
  10.236 -        prems
  10.237 -      else
  10.238 -        (case prems of
  10.239 -          NONE => SOME [last_step_id]
  10.240 -        | SOME l => SOME (last_step_id :: l))
  10.241 +    fun parse_rule_name (SMTLIB.Sym rule :: l) = (rule, l)
  10.242 +      | parse_rule_name l = (veriT_subproof_rule, l)
  10.243 +    fun parse_args (SMTLIB.Key "args" :: args :: l) = (remove_all_qm2 args, l)
  10.244 +      | parse_args l = (SMTLIB.S [], l)
  10.245    in
  10.246 -    (subproof', (((((id_of_father_step, rule), prems'), step_concl), bounds), cx))
  10.247 +    parse_rule_name
  10.248 +    ##> parse_args
  10.249    end
  10.250  
  10.251 -(*
  10.252 -(set id rule :clauses(...) :args(..) :conclusion (...)).
  10.253 -or
  10.254 -(set id subproof (set ...) :conclusion (...)).
  10.255 -*)
  10.256 +end
  10.257  
  10.258 -fun parse_proof_step cx =
  10.259 +fun parse_raw_proof_step (p :  SMTLIB.tree) : raw_veriT_node =
  10.260    let
  10.261      fun rotate_pair (a, (b, c)) = ((a, b), c)
  10.262      fun get_id (SMTLIB.S [SMTLIB.Sym "set", SMTLIB.Sym id, SMTLIB.S l]) = (id, l)
  10.263        | get_id t = raise Fail ("unrecognized VeriT proof " ^ @{make_string} t)
  10.264 -    fun parse_rule (SMTLIB.Sym rule :: l) = (rule, l)
  10.265      fun parse_source (SMTLIB.Key "clauses" :: SMTLIB.S source ::l) =
  10.266          (SOME (map (fn (SMTLIB.Sym id) => id) source), l)
  10.267        | parse_source l = (NONE, l)
  10.268 -    fun parse_subproof cx id_of_father_step ((subproof_step as SMTLIB.S (SMTLIB.Sym "set" :: _)) :: l) =
  10.269 -        let val (subproof_steps, cx') = parse_proof_step cx subproof_step in
  10.270 -          apfst (apfst (curry (op @) subproof_steps)) (parse_subproof cx' id_of_father_step l)
  10.271 +    fun parse_subproof rule args id_of_father_step ((subproof_step as SMTLIB.S (SMTLIB.Sym "set" :: _)) :: l) =
  10.272 +        let
  10.273 +          val subproof_steps = parse_raw_proof_step subproof_step
  10.274 +        in
  10.275 +          apfst (curry (op ::) subproof_steps) (parse_subproof rule args id_of_father_step l)
  10.276          end
  10.277 -      | parse_subproof cx _ l = (([], cx), l)
  10.278 -    fun skip_args (SMTLIB.Key "args" :: SMTLIB.S _ :: l) = l
  10.279 -      | skip_args l = l
  10.280 -    fun parse_conclusion (SMTLIB.Key "conclusion" :: SMTLIB.S concl :: []) = concl
  10.281 -    fun make_or_from_clausification l =
  10.282 -      foldl1 (fn ((concl1, bounds1), (concl2, bounds2)) =>
  10.283 -        (HOLogic.mk_disj (perhaps (try HOLogic.dest_Trueprop) concl1,
  10.284 -         perhaps (try HOLogic.dest_Trueprop) concl2), bounds1 @ bounds2)) l
  10.285 -    fun to_node (((((id, rule), prems), concl), bounds), cx) =
  10.286 -      (mk_node id rule (the_default [] prems) concl bounds, cx)
  10.287 +      | parse_subproof _ _  _ l = ([], l)
  10.288 +
  10.289 +    fun parse_and_clausify_conclusion (SMTLIB.Key "conclusion" :: SMTLIB.S [] :: []) =
  10.290 +          SMTLIB.Sym "false"
  10.291 +      | parse_and_clausify_conclusion (SMTLIB.Key "conclusion" :: SMTLIB.S concl :: []) =
  10.292 +          (SMTLIB.S (remove_all_qm (SMTLIB.Sym "or" :: concl)))
  10.293 +
  10.294 +    fun to_raw_node ((((((id, rule), args), prems), subproof), concl)) =
  10.295 +      (mk_raw_node id rule args (the_default [] prems) concl subproof)
  10.296    in
  10.297 -    get_id
  10.298 -    ##> parse_rule
  10.299 +    (get_id
  10.300 +    ##> parse_rule_and_args
  10.301 +    #> rotate_pair
  10.302      #> rotate_pair
  10.303      ##> parse_source
  10.304      #> rotate_pair
  10.305 -    ##> skip_args
  10.306 -    #> (fn (((id, rule), prems), sub) => (((id, rule), prems), parse_subproof cx id sub))
  10.307 +    #> (fn ((((id, rule), args), prems), sub) =>
  10.308 +      ((((id, rule), args), prems), parse_subproof rule args id sub))
  10.309      #> rotate_pair
  10.310 -    ##> parse_conclusion
  10.311 -    ##> map repair_quantification
  10.312 -    #> (fn ((((id, rule), prems), (subproof, cx)), terms) =>
  10.313 -         (((((id, rule), prems), subproof), fold_map (fn t => fn cx => node_of t cx) terms cx)))
  10.314 -    ##> apfst (fn [] => (@{const False}, []) | concls => make_or_from_clausification concls)
  10.315 -    #> fix_subproof_steps
  10.316 -    ##> to_node
  10.317 -    #> (fn (subproof, (step, cx)) => (subproof @ [step], cx))
  10.318 -    #-> fold_map update_step_and_cx
  10.319 +    ##> parse_and_clausify_conclusion
  10.320 +    #> to_raw_node)
  10.321 +    p
  10.322 +  end
  10.323 +
  10.324 +fun proof_ctxt_of_rule "bind" t = t
  10.325 +  | proof_ctxt_of_rule "sko_forall" t = t
  10.326 +  | proof_ctxt_of_rule "sko_ex" t = t
  10.327 +  | proof_ctxt_of_rule "let" t = t
  10.328 +  | proof_ctxt_of_rule "qnt_simplify" t = t
  10.329 +  | proof_ctxt_of_rule _ _ = []
  10.330 +
  10.331 +fun args_of_rule "forall_inst" t = t
  10.332 +  | args_of_rule _ _ = []
  10.333 +
  10.334 +fun map_replay_prems f (VeriT_Replay_Node {id, rule, args, prems, proof_ctxt, concl, bounds,
  10.335 +      subproof = (bound, assms, subproof)}) =
  10.336 +  (VeriT_Replay_Node {id = id, rule = rule, args = args, prems = f prems, proof_ctxt = proof_ctxt,
  10.337 +    concl = concl, bounds = bounds, subproof = (bound, assms, map (map_replay_prems f) subproof)})
  10.338 +
  10.339 +fun map_replay_id f (VeriT_Replay_Node {id, rule, args, prems, proof_ctxt, concl, bounds,
  10.340 +      subproof = (bound, assms, subproof)}) =
  10.341 +  (VeriT_Replay_Node {id = f id, rule = rule, args = args, prems = prems, proof_ctxt = proof_ctxt,
  10.342 +    concl = concl, bounds = bounds, subproof = (bound, assms, map (map_replay_id f) subproof)})
  10.343 +
  10.344 +fun id_of_last_step prems =
  10.345 +  if null prems then []
  10.346 +  else
  10.347 +    let val VeriT_Replay_Node {id, ...} = List.last prems in [id] end
  10.348 +
  10.349 +val extract_assumptions_from_subproof =
  10.350 +  let fun extract_assumptions_from_subproof (VeriT_Replay_Node {rule, concl, ...}) =
  10.351 +    if rule = veriT_local_input_rule then [concl] else []
  10.352 +  in
  10.353 +    map extract_assumptions_from_subproof
  10.354 +    #> flat
  10.355    end
  10.356  
  10.357 +fun normalized_rule_name id rule =
  10.358 +  (case (rule = veriT_input_rule, can (unprefix SMTLIB_Interface.assert_prefix) id) of
  10.359 +    (true, true) => veriT_normalized_input_rule
  10.360 +  | (true, _) => veriT_local_input_rule
  10.361 +  | _ => rule)
  10.362 +
  10.363 +fun is_assm_repetition id rule =
  10.364 +  rule = veriT_input_rule andalso can (unprefix SMTLIB_Interface.assert_prefix) id
  10.365 +
  10.366 +fun postprocess_proof ctxt step =
  10.367 +  let fun postprocess (Raw_VeriT_Node {id = id, rule = rule, args = args,
  10.368 +     prems = prems, concl = concl, subproof = subproof}) cx =
  10.369 +    let
  10.370 +      val ((concl, bounds), cx') = node_of concl cx
  10.371 +
  10.372 +      val bound_vars = bound_vars_by_rule rule args
  10.373 +
  10.374 +      (* postprocess conclusion *)
  10.375 +      val new_global_bounds = global_bound_vars_by_rule rule args
  10.376 +      val concl = SMTLIB_Isar.unskolemize_names ctxt concl
  10.377 +
  10.378 +      val _ = (SMT_Config.veriT_msg ctxt) (fn () => @{print} ("id =", id, "concl =", concl))
  10.379 +      val _ = (SMT_Config.veriT_msg ctxt) (fn () => @{print} ("id =", id, "cx' =", cx',
  10.380 +        "bound_vars =", bound_vars))
  10.381 +      val bound_vars = filter_out (member ((op =)) new_global_bounds) bound_vars
  10.382 +      val bound_tvars =
  10.383 +        map (fn s => (s, the (find_type_in_formula concl s))) bound_vars
  10.384 +      val subproof_cx = add_bound_variables_to_ctxt concl bound_vars cx
  10.385 +      val (p : veriT_replay_node list list, _) =
  10.386 +        fold_map postprocess subproof subproof_cx
  10.387 +
  10.388 +      (* postprocess assms *)
  10.389 +      val SMTLIB.S stripped_args = args
  10.390 +      val sanitized_args =
  10.391 +        proof_ctxt_of_rule rule stripped_args
  10.392 +        |> map
  10.393 +            (fn SMTLIB.S [SMTLIB.Key "=", x, y] => SMTLIB.S [SMTLIB.Sym "=", x, y]
  10.394 +            | SMTLIB.S syms =>
  10.395 +                SMTLIB.S (SMTLIB.Sym "and" :: map (fn x => SMTLIB.S [SMTLIB.Sym "=", x, x]) syms)
  10.396 +            | x => x)
  10.397 +      val (termified_args, _) = fold_map node_of sanitized_args subproof_cx |> apfst (map fst)
  10.398 +      val normalized_args = map (SMTLIB_Isar.unskolemize_names ctxt) termified_args
  10.399 +
  10.400 +      val subproof_assms = proof_ctxt_of_rule rule normalized_args
  10.401 +
  10.402 +      (* postprocess arguments *)
  10.403 +      val rule_args = args_of_rule rule stripped_args
  10.404 +      val (termified_args, _) = fold_map term_of rule_args subproof_cx
  10.405 +      val normalized_args = map (SMTLIB_Isar.unskolemize_names ctxt) termified_args
  10.406 +      val rule_args = normalized_args
  10.407 +
  10.408 +      (* fix subproof *)
  10.409 +      val p = flat p
  10.410 +      val p = map (map_replay_prems (map (curry (op ^) id))) p
  10.411 +      val p = map (map_replay_id (curry (op ^) id)) p
  10.412 +
  10.413 +      val extra_assms2 =
  10.414 +        (if rule = veriT_subproof_rule then extract_assumptions_from_subproof p else [])
  10.415 +
  10.416 +      (* fix step *)
  10.417 +      val bound_t =
  10.418 +        bounds
  10.419 +        |> map (fn s => (s, the_default dummyT (find_type_of_free_in_formula concl s)))
  10.420 +      val fixed_prems =
  10.421 +        (if null subproof then prems else map (curry (op ^) id) prems) @
  10.422 +        (if is_assm_repetition id rule then [id] else []) @
  10.423 +        id_of_last_step p
  10.424 +      val normalized_rule = normalized_rule_name id rule
  10.425 +      val step = mk_replay_node id normalized_rule rule_args fixed_prems subproof_assms concl
  10.426 +        bound_t (bound_tvars, subproof_assms @ extra_assms2, p)
  10.427 +    in
  10.428 +       ([step], cx')
  10.429 +    end
  10.430 +  in postprocess step end
  10.431 +
  10.432 +
  10.433  (*subproofs are written on multiple lines: SMTLIB can not parse then, because parentheses are
  10.434  unbalanced on each line*)
  10.435  fun seperate_into_steps lines =
  10.436 @@ -214,111 +361,72 @@
  10.437      seperate lines "" 0
  10.438    end
  10.439  
  10.440 +fun unprefix_all_syms c (SMTLIB.Sym v :: l) =
  10.441 +    SMTLIB.Sym (perhaps (try (unprefix c)) v) :: unprefix_all_syms c l
  10.442 +  | unprefix_all_syms c (SMTLIB.S l :: l') = SMTLIB.S (unprefix_all_syms c l) :: unprefix_all_syms c l'
  10.443 +  | unprefix_all_syms c (SMTLIB.Key v :: l) = SMTLIB.Key v :: unprefix_all_syms c l
  10.444 +  | unprefix_all_syms c (v :: l) = v :: unprefix_all_syms c l
  10.445 +  | unprefix_all_syms _ [] = []
  10.446 +
  10.447  (* VeriT adds "@" before every variable. *)
  10.448 -fun remove_all_at (SMTLIB.Sym v :: l) =
  10.449 -    SMTLIB.Sym (perhaps (try (unprefix "@")) v) :: remove_all_at l
  10.450 -  | remove_all_at (SMTLIB.S l :: l') = SMTLIB.S (remove_all_at l) :: remove_all_at l'
  10.451 -  | remove_all_at (SMTLIB.Key v :: l) = SMTLIB.Key v :: remove_all_at l
  10.452 -  | remove_all_at (v :: l) = v :: remove_all_at l
  10.453 -  | remove_all_at [] = []
  10.454 +val remove_all_ats = unprefix_all_syms "@"
  10.455  
  10.456 -fun find_in_which_step_defined var (VeriT_Node {id, bounds, ...} :: l) =
  10.457 -    (case List.find (fn v => String.isPrefix v var) bounds of
  10.458 -      NONE => find_in_which_step_defined var l
  10.459 -    | SOME _ => id)
  10.460 -  | find_in_which_step_defined var _ = raise Fail ("undefined " ^ var)
  10.461 +val linearize_proof =
  10.462 +  let
  10.463 +    fun linearize (VeriT_Replay_Node {id = id, rule = rule, args = _, prems = prems,
  10.464 +        proof_ctxt = proof_ctxt, concl = concl, bounds = bounds, subproof = (_, _, subproof)}) =
  10.465 +      let
  10.466 +        fun mk_prop_of_term concl =
  10.467 +          concl |> fastype_of concl = @{typ bool} ? curry (op $) @{term Trueprop}
  10.468 +        fun remove_assumption_id assumption_id prems =
  10.469 +          filter_out (curry (op =) assumption_id) prems
  10.470 +        fun inline_assumption assumption assumption_id
  10.471 +            (VeriT_Node {id, rule, prems, proof_ctxt, concl, bounds}) =
  10.472 +          mk_node id rule (remove_assumption_id assumption_id prems) proof_ctxt
  10.473 +            (@{const Pure.imp} $ mk_prop_of_term assumption $ mk_prop_of_term concl) bounds
  10.474 +        fun find_input_steps_and_inline [] = []
  10.475 +          | find_input_steps_and_inline
  10.476 +              (VeriT_Node {id = id', rule, prems, concl, bounds, ...} :: steps) =
  10.477 +            if rule = veriT_input_rule then
  10.478 +              find_input_steps_and_inline (map (inline_assumption concl id') steps)
  10.479 +            else
  10.480 +              mk_node (id') rule prems [] concl bounds :: find_input_steps_and_inline steps
  10.481  
  10.482 -(*Yes every case is possible: the introduced var is not on a special size of the equality sign.*)
  10.483 -fun find_ite_var_in_term (Const (@{const_name If}, _) $ _ $
  10.484 -      (Const (@{const_name HOL.eq}, _) $ Free (var1, _) $ Free (var2, _) ) $
  10.485 -      (Const (@{const_name HOL.eq}, _) $ Free (var3, _) $ Free (var4, _) )) =
  10.486 +        val subproof = flat (map linearize subproof)
  10.487 +        val subproof' = find_input_steps_and_inline subproof
  10.488 +      in
  10.489 +        subproof' @ [mk_node id rule prems proof_ctxt concl (map fst bounds)]
  10.490 +      end
  10.491 +  in linearize end
  10.492 +
  10.493 +local
  10.494 +  fun import_proof_and_post_process typs funs lines ctxt =
  10.495      let
  10.496 -      fun get_number_of_ite_transformed_var var =
  10.497 -        perhaps (try (unprefix "ite")) var
  10.498 -        |> Int.fromString
  10.499 -      fun is_equal_and_has_correct_substring var var' var'' =
  10.500 -        if var = var' andalso String.isPrefix "ite" var then SOME var'
  10.501 -        else if var = var'' andalso String.isPrefix "ite" var then SOME var'' else NONE
  10.502 -      val var1_introduced_var = is_equal_and_has_correct_substring var1 var3 var4
  10.503 -      val var2_introduced_var = is_equal_and_has_correct_substring var3 var1 var2
  10.504 -    in
  10.505 -      (case (var1_introduced_var, var2_introduced_var) of
  10.506 -        (SOME a, SOME b) =>
  10.507 -          (*ill-generated case, might be possible when applying the rule to max a a. Only if the
  10.508 -          variable have been introduced before. Probably an impossible edge case*)
  10.509 -          (case (get_number_of_ite_transformed_var a, get_number_of_ite_transformed_var b) of
  10.510 -            (SOME a, SOME b) => if a < b then var2_introduced_var else var1_introduced_var
  10.511 -            (*Otherwise, it is a name clase between a parameter name and the introduced variable.
  10.512 -             Or the name convention has been changed.*)
  10.513 -          | (NONE, SOME _) => var2_introduced_var
  10.514 -          | (SOME _, NONE) => var2_introduced_var)
  10.515 -      | (_, SOME _) => var2_introduced_var
  10.516 -      | (SOME _, _) => var1_introduced_var)
  10.517 -    end
  10.518 -  | find_ite_var_in_term (Const (@{const_name If}, _) $ _ $
  10.519 -      (Const (@{const_name HOL.eq}, _) $ Free (var, _) $ _ ) $
  10.520 -      (Const (@{const_name HOL.eq}, _) $ Free (var', _) $ _ )) =
  10.521 -    if var = var' then SOME var else NONE
  10.522 -  | find_ite_var_in_term (Const (@{const_name If}, _) $ _ $
  10.523 -      (Const (@{const_name HOL.eq}, _) $ _ $ Free (var, _)) $
  10.524 -      (Const (@{const_name HOL.eq}, _) $ _ $ Free (var', _))) =
  10.525 -    if var = var' then SOME var else NONE
  10.526 -  | find_ite_var_in_term (p $ q) =
  10.527 -    (case find_ite_var_in_term p of
  10.528 -      NONE => find_ite_var_in_term q
  10.529 -    | x => x)
  10.530 -  | find_ite_var_in_term (Abs (_, _, body)) = find_ite_var_in_term body
  10.531 -  | find_ite_var_in_term _ = NONE
  10.532 -
  10.533 -fun correct_veriT_step steps (node as VeriT_Node {id, rule, prems, concl, bounds}) =
  10.534 -  if rule = veriT_tmp_ite_elim_rule then
  10.535 -    if bounds = [] then
  10.536 -      (*if the introduced var has already been defined, adding the definition as a dependency*)
  10.537 -      let
  10.538 -        val new_prems = prems
  10.539 -          |> (case find_ite_var_in_term concl of
  10.540 -               NONE => I
  10.541 -             | SOME var => cons (find_in_which_step_defined var steps))
  10.542 -      in
  10.543 -        VeriT_Node {id = id, rule = rule, prems = new_prems, concl = concl, bounds = bounds}
  10.544 -      end
  10.545 -    else
  10.546 -      (*some new variables are created*)
  10.547 -      let val concl' = replace_bound_var_by_free_var concl bounds in
  10.548 -        mk_node id rule prems concl' []
  10.549 -      end
  10.550 -  else
  10.551 -    node
  10.552 -
  10.553 -fun remove_alpha_conversion _ [] = []
  10.554 -  | remove_alpha_conversion replace_table (VeriT_Node {id, rule, prems, concl, bounds} :: steps) =
  10.555 -    let
  10.556 -      val correct_dependency = map (perhaps (Symtab.lookup replace_table))
  10.557 -      val find_predecessor = perhaps (Symtab.lookup replace_table)
  10.558 -    in
  10.559 -      if rule = veriT_tmp_alphaconv_rule then
  10.560 -        remove_alpha_conversion (Symtab.update (id, find_predecessor (hd prems))
  10.561 -          replace_table) steps
  10.562 -      else
  10.563 -        VeriT_Node {id = id, rule = rule, prems = correct_dependency prems,
  10.564 -          concl = concl, bounds = bounds} :: remove_alpha_conversion replace_table steps
  10.565 -    end
  10.566 -
  10.567 -fun correct_veriT_steps steps =
  10.568 -  steps
  10.569 -  |> map (correct_veriT_step steps)
  10.570 -  |> remove_alpha_conversion Symtab.empty
  10.571 +      val smtlib_lines_without_at =
  10.572 +      seperate_into_steps lines
  10.573 +      |> map SMTLIB.parse
  10.574 +      |> remove_all_ats
  10.575 +    in apfst flat (fold_map (fn l => postprocess_proof ctxt (parse_raw_proof_step l))
  10.576 +      smtlib_lines_without_at (empty_context ctxt typs funs)) end
  10.577 +in
  10.578  
  10.579  fun parse typs funs lines ctxt =
  10.580    let
  10.581 -    val smtlib_lines_without_at = remove_all_at (map SMTLIB.parse (seperate_into_steps lines))
  10.582 -    val (u, env) = apfst flat (fold_map (fn l => fn cx => parse_proof_step cx l)
  10.583 -      smtlib_lines_without_at (empty_context ctxt typs funs))
  10.584 -    val t = correct_veriT_steps u
  10.585 +    val (u, env) = import_proof_and_post_process typs funs lines ctxt
  10.586 +    val t = flat (map linearize_proof u)
  10.587      fun node_to_step (VeriT_Node {id, rule, prems, concl, bounds, ...}) =
  10.588 -      mk_step id rule prems concl bounds
  10.589 +      mk_step id rule prems [] concl bounds
  10.590    in
  10.591      (map node_to_step t, ctxt_of env)
  10.592    end
  10.593  
  10.594 +fun parse_replay typs funs lines ctxt =
  10.595 +  let
  10.596 +    val (u, env) = import_proof_and_post_process typs funs lines ctxt
  10.597 +    val _ = (SMT_Config.veriT_msg ctxt) (fn () => @{print} u)
  10.598 +  in
  10.599 +    (u, ctxt_of env)
  10.600 +  end
  10.601 +end
  10.602 +
  10.603  end;
    11.1 --- a/src/HOL/Tools/SMT/verit_proof_parse.ML	Tue Oct 30 16:24:01 2018 +0100
    11.2 +++ b/src/HOL/Tools/SMT/verit_proof_parse.ML	Tue Oct 30 16:24:04 2018 +0100
    11.3 @@ -37,7 +37,7 @@
    11.4  
    11.5      fun step_of_assume j (_, th) =
    11.6        VeriT_Proof.VeriT_Step {id = SMTLIB_Interface.assert_name_of_index (id_of_index j),
    11.7 -        rule = veriT_input_rule, prems = [], concl = Thm.prop_of th, fixes = []}
    11.8 +        rule = veriT_input_rule, prems = [], proof_ctxt = [], concl = Thm.prop_of th, fixes = []}
    11.9  
   11.10      val (actual_steps, _) = VeriT_Proof.parse typs terms output ctxt
   11.11      val used_assert_ids = fold add_used_asserts_in_step actual_steps []
    12.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    12.2 +++ b/src/HOL/Tools/SMT/verit_replay.ML	Tue Oct 30 16:24:04 2018 +0100
    12.3 @@ -0,0 +1,207 @@
    12.4 +(*  Title:      HOL/Tools/SMT/verit_replay.ML
    12.5 +    Author:     Mathias Fleury, MPII
    12.6 +
    12.7 +VeriT proof parsing and replay.
    12.8 +*)
    12.9 +
   12.10 +signature VERIT_REPLAY =
   12.11 +sig
   12.12 +  val replay: Proof.context -> SMT_Translate.replay_data -> string list -> thm
   12.13 +end;
   12.14 +
   12.15 +structure Verit_Replay: VERIT_REPLAY =
   12.16 +struct
   12.17 +
   12.18 +fun under_fixes f unchanged_prems (prems, nthms) names args (concl, ctxt) =
   12.19 +  let
   12.20 +    val thms1 = unchanged_prems @ map (SMT_Replay.varify ctxt) prems
   12.21 +    val _ =  SMT_Config.veriT_msg ctxt (fn () => @{print}  ("names =", names))
   12.22 +    val thms2 = map snd nthms
   12.23 +    val _ = SMT_Config.veriT_msg ctxt (fn () => @{print} ("prems=", prems))
   12.24 +    val _ = SMT_Config.veriT_msg ctxt (fn () => @{print} ("nthms=", nthms))
   12.25 +    val _ = SMT_Config.veriT_msg ctxt (fn () => @{print} ("thms1=", thms1))
   12.26 +    val _ = SMT_Config.veriT_msg ctxt (fn () => @{print} ("thms2=", thms2))
   12.27 +  in (f ctxt (thms1 @ thms2) args concl) end
   12.28 +
   12.29 +
   12.30 +(** Replaying **)
   12.31 +
   12.32 +fun replay_thm method_for rewrite_rules ll_defs ctxt assumed unchanged_prems prems nthms
   12.33 +    concl_transformation global_transformation args
   12.34 +    (VeriT_Proof.VeriT_Replay_Node {id, rule, concl, bounds,  ...}) =
   12.35 +  let
   12.36 +    val _ = SMT_Config.veriT_msg ctxt (fn () => @{print} id)
   12.37 +    val rewrite = let val thy = Proof_Context.theory_of (empty_simpset ctxt) in
   12.38 +        Raw_Simplifier.rewrite_term thy rewrite_rules []
   12.39 +        #> not (null ll_defs) ? SMTLIB_Isar.unlift_term ll_defs
   12.40 +      end
   12.41 +    val post = let val thy = Proof_Context.theory_of (empty_simpset ctxt) in
   12.42 +        Raw_Simplifier.rewrite_term thy rewrite_rules []
   12.43 +        #> Object_Logic.atomize_term ctxt
   12.44 +        #> not (null ll_defs) ? SMTLIB_Isar.unlift_term ll_defs
   12.45 +        #> SMTLIB_Isar.unskolemize_names ctxt
   12.46 +        #> HOLogic.mk_Trueprop
   12.47 +      end
   12.48 +    val concl = concl
   12.49 +      |> concl_transformation
   12.50 +      |> global_transformation
   12.51 +      |> post
   12.52 +in
   12.53 +  if rule = VeriT_Proof.veriT_input_rule then
   12.54 +    (case Symtab.lookup assumed id of
   12.55 +      SOME (_, thm) => thm)
   12.56 +  else
   12.57 +    under_fixes (method_for rule) unchanged_prems
   12.58 +      (prems, nthms) (map fst bounds)
   12.59 +      (map rewrite args) (concl, ctxt)
   12.60 +end
   12.61 +
   12.62 +fun add_used_asserts_in_step (VeriT_Proof.VeriT_Replay_Node {prems,
   12.63 +    subproof = (_, _, subproof), ...}) =
   12.64 +  union (op =) (map_filter (try SMTLIB_Interface.assert_index_of_name) prems @
   12.65 +     flat (map (fn x => add_used_asserts_in_step x []) subproof))
   12.66 +
   12.67 +fun remove_rewrite_rules_from_rules n =
   12.68 +  (fn (step as VeriT_Proof.VeriT_Replay_Node {id, ...}) =>
   12.69 +    (case try SMTLIB_Interface.assert_index_of_name id of
   12.70 +      NONE => SOME step
   12.71 +    | SOME a => if a < n then NONE else SOME step))
   12.72 +
   12.73 +fun replay_step rewrite_rules ll_defs assumed proof_prems
   12.74 +  (step as VeriT_Proof.VeriT_Replay_Node {id, rule, prems, bounds, args,
   12.75 +     subproof = (fixes, assms, subproof), concl, ...}) state =
   12.76 +  let
   12.77 +    val (proofs, stats, ctxt, concl_tranformation, global_transformation) = state
   12.78 +    val (_, ctxt) = Variable.variant_fixes (map fst bounds) ctxt
   12.79 +      |> (fn (names, ctxt) => (names,
   12.80 +        fold Variable.declare_term [SMTLIB_Isar.unskolemize_names ctxt concl] ctxt))
   12.81 +
   12.82 +    val (names, sub_ctxt) = Variable.variant_fixes (map fst fixes) ctxt
   12.83 +       ||> fold Variable.declare_term (map Free fixes)
   12.84 +    val export_vars =
   12.85 +      Term.subst_free (ListPair.zip (map Free fixes, map Free (ListPair.zip (names, map snd fixes))))
   12.86 +      o concl_tranformation
   12.87 +
   12.88 +    val post = let val thy = Proof_Context.theory_of (empty_simpset ctxt) in
   12.89 +        Raw_Simplifier.rewrite_term thy rewrite_rules []
   12.90 +        #> Object_Logic.atomize_term ctxt
   12.91 +        #> not (null ll_defs) ? SMTLIB_Isar.unlift_term ll_defs
   12.92 +        #> SMTLIB_Isar.unskolemize_names ctxt
   12.93 +        #> HOLogic.mk_Trueprop
   12.94 +      end
   12.95 +    val assms = map (export_vars o global_transformation o post) assms
   12.96 +    val (proof_prems', sub_ctxt2) = Assumption.add_assumes (map (Thm.cterm_of sub_ctxt) assms)
   12.97 +      sub_ctxt
   12.98 +
   12.99 +    val all_proof_prems = proof_prems @ proof_prems'
  12.100 +    val (proofs', stats, _, _, sub_global_rew) =
  12.101 +       fold (replay_step rewrite_rules ll_defs assumed all_proof_prems) subproof
  12.102 +         (assumed, stats, sub_ctxt2, export_vars, global_transformation)
  12.103 +    val export_thm = singleton (Proof_Context.export sub_ctxt2 ctxt)
  12.104 +    val nthms = prems
  12.105 +      |>  map (apsnd export_thm o the o (Symtab.lookup (if null subproof then proofs else proofs')))
  12.106 +    val proof_prems =
  12.107 +       if Verit_Replay_Methods.veriT_step_requires_subproof_assms rule then proof_prems else []
  12.108 +    val replay = Timing.timing (replay_thm Verit_Replay_Methods.method_for rewrite_rules ll_defs
  12.109 +       ctxt assumed [] (proof_prems) nthms concl_tranformation global_transformation args)
  12.110 +    val ({elapsed, ...}, thm) =
  12.111 +      SMT_Config.with_time_limit ctxt SMT_Config.reconstruction_step_timeout replay step
  12.112 +        handle Timeout.TIMEOUT _ => raise SMT_Failure.SMT SMT_Failure.Time_Out
  12.113 +    val stats' = Symtab.cons_list (rule, Time.toMilliseconds elapsed) stats
  12.114 +  in (Symtab.update (id, (map fst bounds, thm)) proofs, stats', ctxt,
  12.115 +       concl_tranformation, sub_global_rew) end
  12.116 +
  12.117 +fun replay_ll_def assms ll_defs rewrite_rules stats ctxt term =
  12.118 +  let
  12.119 +    val rewrite = let val thy = Proof_Context.theory_of (empty_simpset ctxt) in
  12.120 +        Raw_Simplifier.rewrite_term thy rewrite_rules []
  12.121 +        #> not (null ll_defs) ? SMTLIB_Isar.unlift_term ll_defs
  12.122 +      end
  12.123 +   val replay = Timing.timing (SMT_Replay_Methods.prove ctxt (rewrite term))
  12.124 +    val ({elapsed, ...}, thm) =
  12.125 +      SMT_Config.with_time_limit ctxt SMT_Config.reconstruction_step_timeout replay
  12.126 +         (fn _ => Method.insert_tac ctxt (map snd assms) THEN' Classical.fast_tac ctxt)
  12.127 +        handle Timeout.TIMEOUT _ => raise SMT_Failure.SMT SMT_Failure.Time_Out
  12.128 +    val stats' = Symtab.cons_list ("ll_defs", Time.toMilliseconds elapsed) stats
  12.129 +  in
  12.130 +    (thm, stats')
  12.131 +  end
  12.132 +
  12.133 +fun replay outer_ctxt
  12.134 +    ({context = ctxt, typs, terms, rewrite_rules, assms, ll_defs, ...} : SMT_Translate.replay_data)
  12.135 +     output =
  12.136 +  let
  12.137 +    val rewrite_rules =
  12.138 +      filter_out (fn thm => Term.could_unify (Thm.prop_of @{thm verit_eq_true_simplify},
  12.139 +          Thm.prop_of thm))
  12.140 +        rewrite_rules
  12.141 +    val num_ll_defs = length ll_defs
  12.142 +    val index_of_id = Integer.add (~ num_ll_defs)
  12.143 +    val id_of_index = Integer.add num_ll_defs
  12.144 +
  12.145 +    val (actual_steps, ctxt2) =
  12.146 +      VeriT_Proof.parse_replay typs terms output ctxt
  12.147 +
  12.148 +    fun step_of_assume (j, (_, th)) =
  12.149 +      VeriT_Proof.VeriT_Replay_Node {
  12.150 +        id = SMTLIB_Interface.assert_name_of_index (id_of_index j),
  12.151 +        rule = VeriT_Proof.veriT_input_rule,
  12.152 +        args = [],
  12.153 +        prems = [],
  12.154 +        proof_ctxt = [],
  12.155 +        concl = Thm.prop_of th
  12.156 +          |> Raw_Simplifier.rewrite_term (Proof_Context.theory_of
  12.157 +               (empty_simpset ctxt addsimps rewrite_rules)) [] [],
  12.158 +        bounds = [],
  12.159 +        subproof = ([], [], [])}
  12.160 +    val used_assert_ids = fold add_used_asserts_in_step actual_steps []
  12.161 +    fun normalize_tac ctxt = let val thy = Proof_Context.theory_of (empty_simpset ctxt) in
  12.162 +      Raw_Simplifier.rewrite_term thy rewrite_rules [] end
  12.163 +    val used_assm_js =
  12.164 +      map_filter (fn id => let val i = index_of_id id in if i >= 0 then SOME (i, nth assms i)
  12.165 +          else NONE end)
  12.166 +        used_assert_ids
  12.167 +
  12.168 +    val assm_steps = map step_of_assume used_assm_js
  12.169 +    val steps = assm_steps @ actual_steps
  12.170 +
  12.171 +    fun extract (VeriT_Proof.VeriT_Replay_Node {id, rule, concl, bounds, ...}) =
  12.172 +         (id, rule, concl, map fst bounds)
  12.173 +    fun cond rule = rule = VeriT_Proof.veriT_input_rule
  12.174 +    val add_asssert = SMT_Replay.add_asserted Symtab.update Symtab.empty extract cond
  12.175 +    val ((_, _), (ctxt3, assumed)) =
  12.176 +      add_asssert outer_ctxt rewrite_rules assms
  12.177 +        (map_filter (remove_rewrite_rules_from_rules num_ll_defs) steps) ctxt2
  12.178 +
  12.179 +    val used_rew_js =
  12.180 +      map_filter (fn id => let val i = index_of_id id in if i < 0
  12.181 +          then SOME (id, normalize_tac ctxt (nth ll_defs id)) else NONE end)
  12.182 +        used_assert_ids
  12.183 +    val (assumed, stats) = fold (fn ((id, thm)) => fn (assumed, stats) =>
  12.184 +           let val (thm, stats) =  replay_ll_def assms ll_defs rewrite_rules stats ctxt thm
  12.185 +           in (Symtab.update (SMTLIB_Interface.assert_name_of_index id, ([], thm)) assumed, stats)
  12.186 +           end)
  12.187 +         used_rew_js (assumed,  Symtab.empty)
  12.188 +
  12.189 +    val ctxt4 =
  12.190 +      ctxt3
  12.191 +      |> put_simpset (SMT_Replay.make_simpset ctxt3 [])
  12.192 +      |> Config.put SAT.solver (Config.get ctxt3 SMT_Config.sat_solver)
  12.193 +    val len = length steps
  12.194 +    val start = Timing.start ()
  12.195 +    val print_runtime_statistics = SMT_Replay.intermediate_statistics ctxt4 start len
  12.196 +    fun blockwise f (i, x) y =
  12.197 +      (if i > 0 andalso i mod 100 = 0 then print_runtime_statistics i else (); f x y)
  12.198 +    val (proofs, stats, ctxt5, _, _) =
  12.199 +      fold_index (blockwise (replay_step rewrite_rules ll_defs assumed [])) steps
  12.200 +        (assumed, stats, ctxt4, fn x => x, fn x => x)
  12.201 +    val _ = print_runtime_statistics len
  12.202 +    val total = Time.toMilliseconds (#elapsed (Timing.result start))
  12.203 +    val (_, VeriT_Proof.VeriT_Replay_Node {id, ...}) = split_last steps
  12.204 +    val _ = SMT_Config.statistics_msg ctxt5
  12.205 +      (Pretty.string_of o SMT_Replay.pretty_statistics "veriT" total) stats
  12.206 +  in
  12.207 +    Symtab.lookup proofs id |> the |> snd |> singleton (Proof_Context.export ctxt5 outer_ctxt)
  12.208 +  end
  12.209 +
  12.210 +end
    13.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    13.2 +++ b/src/HOL/Tools/SMT/verit_replay_methods.ML	Tue Oct 30 16:24:04 2018 +0100
    13.3 @@ -0,0 +1,843 @@
    13.4 +(*  Title:      HOL/Tools/SMT/verit_replay_methods.ML
    13.5 +    Author:     Mathias Fleury, MPII
    13.6 +
    13.7 +Proof methods for replaying veriT proofs.
    13.8 +*)
    13.9 +
   13.10 +signature VERIT_REPLAY_METHODS =
   13.11 +sig
   13.12 +
   13.13 +  val is_skolemisation: string -> bool
   13.14 +  val is_skolemisation_step: VeriT_Proof.veriT_replay_node -> bool
   13.15 +
   13.16 +  (* methods for veriT proof rules *)
   13.17 +  val method_for: string -> Proof.context -> thm list -> term list -> term ->
   13.18 +     thm
   13.19 +
   13.20 +  val veriT_step_requires_subproof_assms : string -> bool
   13.21 +  val eq_congruent_pred: Proof.context -> 'a -> term -> thm
   13.22 +end;
   13.23 +
   13.24 +
   13.25 +structure Verit_Replay_Methods: VERIT_REPLAY_METHODS =
   13.26 +struct
   13.27 +
   13.28 +(*Some general comments on the proof format:
   13.29 +  1. Double negations are not always removed. This means for example that the equivalence rules
   13.30 +     cannot assume that the double negations have already been removed. Therefore, we match the
   13.31 +     term, instantiate the theorem, then use simp (to remove double negations), and finally use
   13.32 +     assumption.
   13.33 +  2. The reconstruction for rule forall_inst is buggy and tends to be very fragile, because the rule
   13.34 +     is doing much more that is supposed to do. Moreover types can make trivial goals (for the
   13.35 +     boolean structure) impossible to prove.
   13.36 +  3. Duplicate literals are sometimes removed, mostly by the SAT solver. We currently do not care
   13.37 +     about it, since in all cases we have met, a rule like tmp_AC_simp is called to do the
   13.38 +     simplification.
   13.39 +
   13.40 +  Rules unsupported on purpose:
   13.41 +    * Distinct_Elim, XOR, let (we don't need them).
   13.42 +    * tmp_skolemize (because it is not clear if veriT still generates using it).
   13.43 +*)
   13.44 +
   13.45 +datatype verit_rule =
   13.46 +   False | True |
   13.47 +
   13.48 +   (* input: a repeated (normalized) assumption of  assumption of in a subproof *)
   13.49 +   Normalized_Input | Local_Input |
   13.50 +   (* Subproof: *)
   13.51 +   Subproof |
   13.52 +   (* Conjunction: *)
   13.53 +   And | Not_And | And_Pos | And_Neg |
   13.54 +   (* Disjunction"" *)
   13.55 +   Or | Or_Pos | Not_Or | Or_Neg |
   13.56 +   (* Disjunction: *)
   13.57 +   Implies | Implies_Neg1 | Implies_Neg2 | Implies_Pos | Not_Implies1 | Not_Implies2 |
   13.58 +   (* Equivalence: *)
   13.59 +   Equiv_neg1 | Equiv_pos1 | Equiv_pos2 | Equiv_neg2 | Not_Equiv1 | Not_Equiv2 | Equiv1 | Equiv2 |
   13.60 +   (* If-then-else: *)
   13.61 +   ITE_Pos1 | ITE_Pos2 | ITE_Neg1 | ITE_Neg2 | Not_ITE1 | Not_ITE2 | ITE_Intro | ITE1 | ITE2 |
   13.62 +   (* Equality: *)
   13.63 +   Eq_Congruent | Eq_Reflexive | Eq_Transitive | Eq_Congruent_Pred | Trans |  Refl |  Cong |
   13.64 +   (* Arithmetics: *)
   13.65 +   LA_Disequality | LA_Generic | LA_Tautology |  LIA_Generic | LA_Totality | LA_RW_Eq |
   13.66 +   NLA_Generic |
   13.67 +   (* Quantifiers: *)
   13.68 +   Forall_Inst | Qnt_Rm_Unused | Qnt_Join | Qnt_Simplify | Bind | Skolem_Forall | Skolem_Ex |
   13.69 +   (* Resolution: *)
   13.70 +   Theory_Resolution | Resolution |
   13.71 +   (* Various transformation: *)
   13.72 +   Connective_Equiv |
   13.73 +   (* Temporary rules, that the veriT developpers want to remove: *)
   13.74 +   Tmp_AC_Simp |
   13.75 +   Tmp_Bfun_Elim |
   13.76 +   (* Unsupported rule *)
   13.77 +   Unsupported
   13.78 +
   13.79 +val is_skolemisation = member (op =) ["sko_forall", "sko_ex"]
   13.80 +fun is_skolemisation_step (VeriT_Proof.VeriT_Replay_Node {id, ...}) = is_skolemisation id
   13.81 +
   13.82 +fun verit_rule_of "bind" = Bind
   13.83 +  | verit_rule_of "cong" = Cong
   13.84 +  | verit_rule_of "refl" = Refl
   13.85 +  | verit_rule_of "equiv1" = Equiv1
   13.86 +  | verit_rule_of "equiv2" = Equiv2
   13.87 +  | verit_rule_of "equiv_pos1" = Equiv_pos1
   13.88 +  | verit_rule_of "equiv_pos2" = Equiv_pos2
   13.89 +  | verit_rule_of "equiv_neg1" = Equiv_neg1
   13.90 +  | verit_rule_of "equiv_neg2" = Equiv_neg2
   13.91 +  | verit_rule_of "sko_forall" = Skolem_Forall
   13.92 +  | verit_rule_of "sko_ex" = Skolem_Ex
   13.93 +  | verit_rule_of "eq_reflexive" = Eq_Reflexive
   13.94 +  | verit_rule_of "th_resolution" = Theory_Resolution
   13.95 +  | verit_rule_of "forall_inst" = Forall_Inst
   13.96 +  | verit_rule_of "implies_pos" = Implies_Pos
   13.97 +  | verit_rule_of "or" = Or
   13.98 +  | verit_rule_of "not_or" = Not_Or
   13.99 +  | verit_rule_of "resolution" = Resolution
  13.100 +  | verit_rule_of "eq_congruent" = Eq_Congruent
  13.101 +  | verit_rule_of "connective_equiv" = Connective_Equiv
  13.102 +  | verit_rule_of "trans" = Trans
  13.103 +  | verit_rule_of "false" = False
  13.104 +  | verit_rule_of "tmp_AC_simp" = Tmp_AC_Simp
  13.105 +  | verit_rule_of "and" = And
  13.106 +  | verit_rule_of "not_and" = Not_And
  13.107 +  | verit_rule_of "and_pos" = And_Pos
  13.108 +  | verit_rule_of "and_neg" = And_Neg
  13.109 +  | verit_rule_of "or_pos" = Or_Pos
  13.110 +  | verit_rule_of "or_neg" = Or_Neg
  13.111 +  | verit_rule_of "not_equiv1" = Not_Equiv1
  13.112 +  | verit_rule_of "not_equiv2" = Not_Equiv2
  13.113 +  | verit_rule_of "not_implies1" = Not_Implies1
  13.114 +  | verit_rule_of "not_implies2" = Not_Implies2
  13.115 +  | verit_rule_of "implies_neg1" = Implies_Neg1
  13.116 +  | verit_rule_of "implies_neg2" = Implies_Neg2
  13.117 +  | verit_rule_of "implies" = Implies
  13.118 +  | verit_rule_of "tmp_bfun_elim" = Tmp_Bfun_Elim
  13.119 +  | verit_rule_of "ite1" = ITE1
  13.120 +  | verit_rule_of "ite2" = ITE2
  13.121 +  | verit_rule_of "not_ite1" = Not_ITE1
  13.122 +  | verit_rule_of "not_ite2" = Not_ITE2
  13.123 +  | verit_rule_of "ite_pos1" = ITE_Pos1
  13.124 +  | verit_rule_of "ite_pos2" = ITE_Pos2
  13.125 +  | verit_rule_of "ite_neg1" = ITE_Neg1
  13.126 +  | verit_rule_of "ite_neg2" = ITE_Neg2
  13.127 +  | verit_rule_of "ite_intro" = ITE_Intro
  13.128 +  | verit_rule_of "la_disequality" = LA_Disequality
  13.129 +  | verit_rule_of "lia_generic" = LIA_Generic
  13.130 +  | verit_rule_of "la_generic" = LA_Generic
  13.131 +  | verit_rule_of "la_tautology" = LA_Tautology
  13.132 +  | verit_rule_of "la_totality" = LA_Totality
  13.133 +  | verit_rule_of "la_rw_eq"= LA_RW_Eq
  13.134 +  | verit_rule_of "nla_generic"= NLA_Generic
  13.135 +  | verit_rule_of "eq_transitive" = Eq_Transitive
  13.136 +  | verit_rule_of "qnt_rm_unused" = Qnt_Rm_Unused
  13.137 +  | verit_rule_of "qnt_simplify" = Qnt_Simplify
  13.138 +  | verit_rule_of "qnt_join" = Qnt_Join
  13.139 +  | verit_rule_of "eq_congruent_pred" = Eq_Congruent_Pred
  13.140 +  | verit_rule_of "subproof" = Subproof
  13.141 +  | verit_rule_of r =
  13.142 +     if r = VeriT_Proof.veriT_normalized_input_rule then Normalized_Input
  13.143 +     else if r = VeriT_Proof.veriT_local_input_rule then Local_Input
  13.144 +     else Unsupported
  13.145 +
  13.146 +fun string_of_verit_rule Bind = "Bind"
  13.147 +  | string_of_verit_rule Cong = "Cong"
  13.148 +  | string_of_verit_rule Refl = "Refl"
  13.149 +  | string_of_verit_rule Equiv1 = "Equiv1"
  13.150 +  | string_of_verit_rule Equiv2 = "Equiv2"
  13.151 +  | string_of_verit_rule Equiv_pos1 = "Equiv_pos1"
  13.152 +  | string_of_verit_rule Equiv_pos2 = "Equiv_pos2"
  13.153 +  | string_of_verit_rule Equiv_neg1 = "Equiv_neg1"
  13.154 +  | string_of_verit_rule Equiv_neg2 = "Equiv_neg2"
  13.155 +  | string_of_verit_rule Skolem_Forall = "Skolem_Forall"
  13.156 +  | string_of_verit_rule Skolem_Ex = "Skolem_Ex"
  13.157 +  | string_of_verit_rule Eq_Reflexive = "Eq_Reflexive"
  13.158 +  | string_of_verit_rule Theory_Resolution = "Theory_Resolution"
  13.159 +  | string_of_verit_rule Forall_Inst = "forall_inst"
  13.160 +  | string_of_verit_rule Or = "Or"
  13.161 +  | string_of_verit_rule Not_Or = "Not_Or"
  13.162 +  | string_of_verit_rule Resolution = "Resolution"
  13.163 +  | string_of_verit_rule Eq_Congruent = "eq_congruent"
  13.164 +  | string_of_verit_rule Connective_Equiv = "connective_equiv"
  13.165 +  | string_of_verit_rule Trans = "trans"
  13.166 +  | string_of_verit_rule False = "false"
  13.167 +  | string_of_verit_rule And = "and"
  13.168 +  | string_of_verit_rule And_Pos = "and_pos"
  13.169 +  | string_of_verit_rule Not_And = "not_and"
  13.170 +  | string_of_verit_rule And_Neg = "and_neg"
  13.171 +  | string_of_verit_rule Or_Pos = "or_pos"
  13.172 +  | string_of_verit_rule Or_Neg = "or_neg"
  13.173 +  | string_of_verit_rule Tmp_AC_Simp = "tmp_AC_simp"
  13.174 +  | string_of_verit_rule Not_Equiv1 = "not_equiv1"
  13.175 +  | string_of_verit_rule Not_Equiv2 = "not_equiv2"
  13.176 +  | string_of_verit_rule Not_Implies1 = "not_implies1"
  13.177 +  | string_of_verit_rule Not_Implies2 = "not_implies2"
  13.178 +  | string_of_verit_rule Implies_Neg1 = "implies_neg1"
  13.179 +  | string_of_verit_rule Implies_Neg2 = "implies_neg2"
  13.180 +  | string_of_verit_rule Implies = "implies"
  13.181 +  | string_of_verit_rule Tmp_Bfun_Elim = "tmp_bfun_elim"
  13.182 +  | string_of_verit_rule ITE1 = "ite1"
  13.183 +  | string_of_verit_rule ITE2 = "ite2"
  13.184 +  | string_of_verit_rule Not_ITE1 = "not_ite1"
  13.185 +  | string_of_verit_rule Not_ITE2 = "not_ite2"
  13.186 +  | string_of_verit_rule ITE_Pos1 = "ite_pos1"
  13.187 +  | string_of_verit_rule ITE_Pos2 = "ite_pos2"
  13.188 +  | string_of_verit_rule ITE_Neg1 = "ite_neg1"
  13.189 +  | string_of_verit_rule ITE_Neg2 = "ite_neg2"
  13.190 +  | string_of_verit_rule ITE_Intro = "ite_intro"
  13.191 +  | string_of_verit_rule LA_Disequality = "la_disequality"
  13.192 +  | string_of_verit_rule LA_Generic = "la_generic"
  13.193 +  | string_of_verit_rule LIA_Generic = "lia_generic"
  13.194 +  | string_of_verit_rule LA_Tautology = "la_tautology"
  13.195 +  | string_of_verit_rule LA_RW_Eq = "la_rw_eq"
  13.196 +  | string_of_verit_rule LA_Totality = "LA_Totality"
  13.197 +  | string_of_verit_rule NLA_Generic = "nla_generic"
  13.198 +  | string_of_verit_rule Eq_Transitive = "eq_transitive"
  13.199 +  | string_of_verit_rule Qnt_Rm_Unused = "qnt_remove_unused"
  13.200 +  | string_of_verit_rule Qnt_Simplify = "qnt_simplify"
  13.201 +  | string_of_verit_rule Qnt_Join = "qnt_join"
  13.202 +  | string_of_verit_rule Eq_Congruent_Pred = "eq_congruent_pred"
  13.203 +  | string_of_verit_rule Normalized_Input = VeriT_Proof.veriT_normalized_input_rule
  13.204 +  | string_of_verit_rule Local_Input = VeriT_Proof.veriT_normalized_input_rule
  13.205 +  | string_of_verit_rule Subproof = "subproof"
  13.206 +  | string_of_verit_rule r = "Unsupported rule: " ^ @{make_string} r
  13.207 +
  13.208 +(*** Methods to Replay Normal steps ***)
  13.209 +(* sko_forall requires the assumptions to be able to SMT_Replay_Methods.prove the equivalence in case of double
  13.210 +skolemization. See comment below. *)
  13.211 +fun veriT_step_requires_subproof_assms t =
  13.212 +  member (op =) ["refl", "cong", VeriT_Proof.veriT_local_input_rule, "sko_forall",
  13.213 +    "sko_ex"] t
  13.214 +
  13.215 +fun simplify_tac ctxt thms =
  13.216 +  ctxt
  13.217 +  |> empty_simpset
  13.218 +  |> put_simpset HOL_basic_ss
  13.219 +  |> (fn ctxt => ctxt addsimps @{thms not_not eq_commute} addsimps thms)
  13.220 +  |> Simplifier.full_simp_tac
  13.221 +
  13.222 +val bind_thms =
  13.223 +  [@{lemma "(\<And>x x'. P x = Q x) \<Longrightarrow> (\<forall>x. P x) = (\<forall>y. Q y)"
  13.224 +      by blast},
  13.225 +   @{lemma "(\<And>x x'.  P x = Q x) \<Longrightarrow> (\<exists>x. P x) = (\<exists>y. Q y)"
  13.226 +      by blast},
  13.227 +   @{lemma "(\<And>x x'.  P x = Q x) \<Longrightarrow> (\<exists>x. P x = Q x)"
  13.228 +      by blast},
  13.229 +   @{lemma "(\<And>x x'.  P x = Q x) \<Longrightarrow> (\<forall>x. P x = Q x)"
  13.230 +      by blast}]
  13.231 +
  13.232 +fun TRY' tac = fn i => TRY (tac i)
  13.233 +fun REPEAT' tac = fn i => REPEAT (tac i)
  13.234 +fun REPEAT_CHANGED tac = fn i => REPEAT (CHANGED (tac i))
  13.235 +
  13.236 +fun bind ctxt [prems] t = SMT_Replay_Methods.prove ctxt t (fn _ =>
  13.237 +    REPEAT' (resolve_tac ctxt bind_thms)
  13.238 +    THEN' match_tac ctxt [prems]
  13.239 +    THEN' simplify_tac ctxt []
  13.240 +    THEN' REPEAT' (match_tac ctxt [@{thm refl}]))
  13.241 +
  13.242 +
  13.243 +fun refl ctxt thm t =
  13.244 +  (case find_first (fn thm => t = Thm.full_prop_of thm) thm of
  13.245 +      SOME thm => thm
  13.246 +    | NONE =>
  13.247 +        (case try (Z3_Replay_Methods.refl ctxt thm) t of
  13.248 +          NONE =>
  13.249 +          ( Z3_Replay_Methods.cong ctxt thm t)
  13.250 +        | SOME thm => thm))
  13.251 +
  13.252 +local
  13.253 +  fun equiv_pos_neg_term ctxt thm (@{term Trueprop} $
  13.254 +         (@{term HOL.disj} $ (_) $
  13.255 +            ((@{term HOL.disj} $ a $ b)))) =
  13.256 +     Drule.infer_instantiate' ctxt (map (SOME o Thm.cterm_of ctxt) [a, b]) thm
  13.257 +
  13.258 +  fun prove_equiv_pos_neg thm ctxt _ t =
  13.259 +    let val thm = equiv_pos_neg_term ctxt thm t
  13.260 +    in
  13.261 +      SMT_Replay_Methods.prove ctxt t (fn _ =>
  13.262 +        Method.insert_tac ctxt [thm]
  13.263 +        THEN' simplify_tac ctxt [])
  13.264 +    end
  13.265 +in
  13.266 +
  13.267 +val equiv_pos1_thm =
  13.268 +  @{lemma "\<not>(a \<longleftrightarrow> ~b) \<or> a \<or> b"
  13.269 +      by blast+}
  13.270 +
  13.271 +val equiv_pos1 = prove_equiv_pos_neg equiv_pos1_thm
  13.272 +
  13.273 +val equiv_pos2_thm =
  13.274 +  @{lemma  "\<And>a b. ((\<not>a) \<noteq> b) \<or> a \<or> b"
  13.275 +      by blast+}
  13.276 +
  13.277 +val equiv_pos2 = prove_equiv_pos_neg equiv_pos2_thm
  13.278 +
  13.279 +val equiv_neg1_thm =
  13.280 +  @{lemma "(~a \<longleftrightarrow> ~b) \<or> a \<or> b"
  13.281 +      by blast}
  13.282 +
  13.283 +val equiv_neg1 = prove_equiv_pos_neg equiv_neg1_thm
  13.284 +
  13.285 +val equiv_neg2_thm =
  13.286 +  @{lemma "(a \<longleftrightarrow> b) \<or> a \<or> b"
  13.287 +      by blast}
  13.288 +
  13.289 +val equiv_neg2 = prove_equiv_pos_neg equiv_neg2_thm
  13.290 +
  13.291 +end
  13.292 +
  13.293 +(* Most of the code below is due to the proof output of veriT: The description of the rule is wrong
  13.294 +(and according to Pascal Fontaine, it is a bug). Anyway, currently, forall_inst does:
  13.295 +  1. swapping out the forall quantifiers
  13.296 +  2. instantiation
  13.297 +  3. boolean.
  13.298 +
  13.299 +However, types can mess-up things:
  13.300 +  lemma  \<open>(0 < degree a) = (0 \<noteq> degree a) \<Longrightarrow> 0 = degree a \<or> 0 < degree a\<close>
  13.301 +    by fast
  13.302 +works unlike
  13.303 +  lemma  \<open>((0::nat) < degree a) = (0 \<noteq> degree a) \<Longrightarrow> 0 = degree a \<or> 0 < degree a\<close>
  13.304 +    by fast.
  13.305 +Therefore, we use fast and auto as fall-back.
  13.306 +*)
  13.307 +fun forall_inst ctxt _ args t =
  13.308 +  let
  13.309 +    val instantiate =
  13.310 +       fold (fn inst => fn tac =>
  13.311 +         let val thm = Drule.infer_instantiate' ctxt [NONE, SOME (Thm.cterm_of ctxt inst)] @{thm spec}
  13.312 +         in tac THEN' dmatch_tac ctxt [thm]end)
  13.313 +         args
  13.314 +         (K all_tac)
  13.315 +  in
  13.316 +    SMT_Replay_Methods.prove ctxt t (fn _ =>
  13.317 +      resolve_tac ctxt [@{thm disj_not1} RSN (1, @{thm iffD2}) OF [@{thm impI}]]
  13.318 +      THEN' TRY' (Raw_Simplifier.rewrite_goal_tac ctxt @{thms all_simps[symmetric] not_all})
  13.319 +      THEN' TRY' instantiate
  13.320 +      THEN' TRY' (simplify_tac ctxt [])
  13.321 +      THEN' TRY' (SOLVED' (fn _ => HEADGOAL ( (assume_tac ctxt)
  13.322 +         ORELSE'
  13.323 +            TRY' (dresolve_tac ctxt @{thms conjE}
  13.324 +              THEN_ALL_NEW assume_tac ctxt)
  13.325 +         ORELSE'
  13.326 +            TRY' (dresolve_tac ctxt @{thms verit_forall_inst}
  13.327 +              THEN_ALL_NEW assume_tac ctxt))))
  13.328 +      THEN' (TRY' (Classical.fast_tac ctxt))
  13.329 +      THEN' (TRY' (K (Clasimp.auto_tac ctxt))))
  13.330 +    end
  13.331 +
  13.332 +fun or _ [thm] _ = thm
  13.333 +
  13.334 +val implies_pos_thm =
  13.335 +  [@{lemma "\<not>(A \<longrightarrow> B) \<or> \<not>A \<or> B"
  13.336 +      by blast},
  13.337 +  @{lemma "\<not>(\<not>A \<longrightarrow> B) \<or> A \<or> B"
  13.338 +      by blast}]
  13.339 +
  13.340 +fun implies_pos ctxt _ t = SMT_Replay_Methods.prove ctxt t (fn _ =>
  13.341 +  resolve_tac ctxt implies_pos_thm)
  13.342 +
  13.343 +fun extract_rewrite_rule_assumption thms =
  13.344 +  let
  13.345 +    fun is_rewrite_rule thm =
  13.346 +      (case Thm.prop_of thm of
  13.347 +        @{term Trueprop} $ (Const(@{const_name HOL.eq}, _) $ Free(_, _) $ _) => true
  13.348 +      | _ => false)
  13.349 +  in
  13.350 +    thms
  13.351 +    |> filter is_rewrite_rule
  13.352 +    |> map (fn thm => thm COMP @{thm eq_reflection})
  13.353 +  end
  13.354 +
  13.355 +(* We need to unfold the assumptions if we are in a subproof: For multiple skolemization, the context
  13.356 +contains a mapping "verit_vrX \<leadsto> Eps f". The variable "verit_vrX" must be unfolded to "Eps f".
  13.357 +Otherwise, the proof cannot be done. *)
  13.358 +fun skolem_forall ctxt (thms) t  =
  13.359 +  let
  13.360 +    val ts = extract_rewrite_rule_assumption thms
  13.361 +  in
  13.362 +    SMT_Replay_Methods.prove ctxt t (fn _ =>
  13.363 +      REPEAT_CHANGED (resolve_tac ctxt @{thms verit_sko_forall'})
  13.364 +      THEN' TRY' (simplify_tac ctxt ts)
  13.365 +      THEN' TRY'(resolve_tac ctxt thms THEN_ALL_NEW resolve_tac ctxt @{thms refl})
  13.366 +      THEN' TRY' (resolve_tac ctxt @{thms refl}))
  13.367 +  end
  13.368 +
  13.369 +fun skolem_ex ctxt (thms) t  =
  13.370 +  let
  13.371 +    val ts = extract_rewrite_rule_assumption thms
  13.372 +  in
  13.373 +    SMT_Replay_Methods.prove ctxt t (fn _ =>
  13.374 +      Raw_Simplifier.rewrite_goal_tac ctxt ts
  13.375 +      THEN' REPEAT_CHANGED (resolve_tac ctxt @{thms verit_sko_ex'})
  13.376 +      THEN' REPEAT_CHANGED (resolve_tac ctxt thms THEN_ALL_NEW resolve_tac ctxt @{thms refl})
  13.377 +      THEN' TRY' (resolve_tac ctxt @{thms refl}))
  13.378 +  end
  13.379 +
  13.380 +fun eq_reflexive ctxt _ t = SMT_Replay_Methods.prove ctxt t (fn _ =>
  13.381 +  resolve_tac ctxt [@{thm refl}])
  13.382 +
  13.383 +fun connective_equiv ctxt thms t = SMT_Replay_Methods.prove ctxt t (fn _ =>
  13.384 +  Method.insert_tac ctxt thms
  13.385 +  THEN' K (Clasimp.auto_tac ctxt))
  13.386 +
  13.387 +
  13.388 +fun normalized_input ctxt prems t = SMT_Replay_Methods.prove ctxt t (fn _ =>
  13.389 +  Method.insert_tac ctxt prems
  13.390 +  THEN' TRY' (simplify_tac ctxt [])
  13.391 +  THEN' TRY' (K (Clasimp.auto_tac ctxt)))
  13.392 +
  13.393 +val false_rule_thm = @{lemma "\<not>False" by blast}
  13.394 +
  13.395 +fun false_rule ctxt _ t = SMT_Replay_Methods.prove ctxt t (fn _ =>
  13.396 +  resolve_tac ctxt [false_rule_thm])
  13.397 +
  13.398 +
  13.399 +(* transitivity *)
  13.400 +
  13.401 +val trans_bool_thm =
  13.402 +  @{lemma "P = Q \<Longrightarrow> Q \<Longrightarrow> P" by blast}
  13.403 +fun trans _ [thm1, thm2] _ =
  13.404 +      (case (Thm.full_prop_of thm1, Thm.full_prop_of thm2) of
  13.405 +        (@{term Trueprop} $ (Const(@{const_name HOL.eq}, _) $ _ $ t2),
  13.406 +         @{term Trueprop} $ (Const(@{const_name HOL.eq}, _) $ t3 $ _)) =>
  13.407 +        if t2 = t3 then thm1 RSN (1, thm2 RSN (2, @{thm trans}))
  13.408 +        else thm1 RSN (1, (thm2 RS sym) RSN (2, @{thm trans}))
  13.409 +      | _ => trans_bool_thm OF [thm1, thm2])
  13.410 +  | trans ctxt (thm1 :: thm2 :: thms) t =
  13.411 +      trans ctxt (trans ctxt [thm1, thm2] t :: thms) t
  13.412 +
  13.413 +fun tmp_AC_rule ctxt _ t =
  13.414 + let
  13.415 +   val simplify =
  13.416 +     ctxt
  13.417 +     |> empty_simpset
  13.418 +     |> put_simpset HOL_basic_ss
  13.419 +     |> (fn ctxt => ctxt addsimps @{thms ac_simps conj_ac})
  13.420 +     |> Simplifier.full_simp_tac
  13.421 + in SMT_Replay_Methods.prove ctxt t (fn _ =>
  13.422 +   REPEAT_ALL_NEW (simplify_tac ctxt []
  13.423 +     THEN' TRY' simplify
  13.424 +     THEN' TRY' (Classical.fast_tac ctxt))) end
  13.425 +
  13.426 +fun and_rule ctxt prems t = SMT_Replay_Methods.prove ctxt t (fn _ =>
  13.427 +   Method.insert_tac ctxt prems
  13.428 +   THEN' (fn i => REPEAT (dresolve_tac ctxt @{thms conjE} i THEN assume_tac ctxt (i+1)))
  13.429 +   THEN' TRY' (assume_tac ctxt)
  13.430 +   THEN' TRY' (simplify_tac ctxt []))
  13.431 +
  13.432 +fun not_and_rule ctxt prems t = SMT_Replay_Methods.prove ctxt t (fn _ =>
  13.433 +   Method.insert_tac ctxt prems THEN'
  13.434 +   Classical.fast_tac ctxt ORELSE' Clasimp.force_tac ctxt)
  13.435 +
  13.436 +fun not_or_rule ctxt prems t = SMT_Replay_Methods.prove ctxt t (fn _ =>
  13.437 +   Method.insert_tac ctxt prems THEN'
  13.438 +   Classical.fast_tac ctxt ORELSE' Clasimp.force_tac ctxt)
  13.439 +
  13.440 +local
  13.441 +  fun simplify_and_pos ctxt =
  13.442 +    ctxt
  13.443 +    |> empty_simpset
  13.444 +    |> put_simpset HOL_basic_ss
  13.445 +    |> (fn ctxt => ctxt addsimps @{thms eq_commute verit_ite_intro_simp if_cancel}
  13.446 +         addsimps @{thms simp_thms de_Morgan_conj})
  13.447 +    |> Simplifier.full_simp_tac
  13.448 +in
  13.449 +
  13.450 +fun and_pos ctxt _ t =
  13.451 +  SMT_Replay_Methods.prove ctxt t (fn _ =>
  13.452 +  REPEAT_CHANGED (resolve_tac ctxt @{thms verit_and_pos})
  13.453 +  THEN' TRY' (simplify_and_pos ctxt)
  13.454 +  THEN' TRY' (assume_tac ctxt)
  13.455 +  THEN' TRY' (Classical.fast_tac ctxt))
  13.456 +
  13.457 +end
  13.458 +
  13.459 +fun and_neg_rule ctxt _ t = SMT_Replay_Methods.prove ctxt t (fn _ =>
  13.460 +  REPEAT_CHANGED (resolve_tac ctxt @{thms verit_and_neg})
  13.461 +  THEN' simplify_tac ctxt @{thms de_Morgan_conj[symmetric] excluded_middle
  13.462 +    excluded_middle[of \<open>\<not>_\<close>, unfolded not_not]})
  13.463 +
  13.464 +fun or_pos_rule ctxt _ t = SMT_Replay_Methods.prove ctxt t (fn _ =>
  13.465 +  simplify_tac ctxt @{thms simp_thms})
  13.466 +
  13.467 +fun or_neg_rule ctxt _ t = SMT_Replay_Methods.prove ctxt t (fn _ =>
  13.468 +  resolve_tac ctxt @{thms verit_or_neg}
  13.469 +  THEN' (fn i => dresolve_tac ctxt @{thms verit_subst_bool} i
  13.470 +     THEN assume_tac ctxt (i+1))
  13.471 +  THEN' simplify_tac ctxt @{thms simp_thms})
  13.472 +
  13.473 +val not_equiv1_thm =
  13.474 +  @{lemma "\<not>(A \<longleftrightarrow> B) \<Longrightarrow> A \<or> B"
  13.475 +      by blast}
  13.476 +
  13.477 +fun not_equiv1 ctxt [thm] t = SMT_Replay_Methods.prove ctxt t (fn _ =>
  13.478 +  Method.insert_tac ctxt [not_equiv1_thm OF [thm]]
  13.479 +  THEN' simplify_tac ctxt [])
  13.480 +
  13.481 +val not_equiv2_thm =
  13.482 +  @{lemma "\<not>(A \<longleftrightarrow> B) \<Longrightarrow> \<not>A \<or> \<not>B"
  13.483 +      by blast}
  13.484 +
  13.485 +fun not_equiv2 ctxt [thm] t = SMT_Replay_Methods.prove ctxt t (fn _ =>
  13.486 +  Method.insert_tac ctxt [not_equiv2_thm OF [thm]]
  13.487 +  THEN' simplify_tac ctxt [])
  13.488 +
  13.489 +val equiv1_thm =
  13.490 +  @{lemma "(A \<longleftrightarrow> B) \<Longrightarrow> \<not>A \<or> B"
  13.491 +      by blast}
  13.492 +
  13.493 +fun equiv1 ctxt [thm] t = SMT_Replay_Methods.prove ctxt t (fn _ =>
  13.494 +  Method.insert_tac ctxt [equiv1_thm OF [thm]]
  13.495 +  THEN' simplify_tac ctxt [])
  13.496 +
  13.497 +val equiv2_thm =
  13.498 +  @{lemma "(A \<longleftrightarrow> B) \<Longrightarrow> A \<or> \<not>B"
  13.499 +      by blast}
  13.500 +
  13.501 +fun equiv2 ctxt [thm] t = SMT_Replay_Methods.prove ctxt t (fn _ =>
  13.502 +  Method.insert_tac ctxt [equiv2_thm OF [thm]]
  13.503 +  THEN' simplify_tac ctxt [])
  13.504 +
  13.505 +
  13.506 +val not_implies1_thm =
  13.507 +  @{lemma "\<not>(A \<longrightarrow> B) \<Longrightarrow> A"
  13.508 +      by blast}
  13.509 +
  13.510 +fun not_implies1 ctxt [thm] t = SMT_Replay_Methods.prove ctxt t (fn _ =>
  13.511 +  Method.insert_tac ctxt [not_implies1_thm OF [thm]]
  13.512 +  THEN' simplify_tac ctxt [])
  13.513 +
  13.514 +val not_implies2_thm =
  13.515 +  @{lemma "\<not>(A \<longrightarrow>B) \<Longrightarrow> \<not>B"
  13.516 +      by blast}
  13.517 +
  13.518 +fun not_implies2 ctxt [thm] t = SMT_Replay_Methods.prove ctxt t (fn _ =>
  13.519 +  Method.insert_tac ctxt [not_implies2_thm OF [thm]]
  13.520 +  THEN' simplify_tac ctxt [])
  13.521 +
  13.522 +
  13.523 +local
  13.524 +  fun implies_pos_neg_term ctxt thm (@{term Trueprop} $
  13.525 +         (@{term HOL.disj} $ (@{term HOL.implies} $ a $ b) $ _)) =
  13.526 +     Drule.infer_instantiate' ctxt (map (SOME o Thm.cterm_of ctxt) [a, b]) thm
  13.527 +
  13.528 +  fun prove_implies_pos_neg thm ctxt _ t =
  13.529 +    let val thm = implies_pos_neg_term ctxt thm t
  13.530 +    in
  13.531 +      SMT_Replay_Methods.prove ctxt t (fn _ =>
  13.532 +        Method.insert_tac ctxt [thm]
  13.533 +        THEN' simplify_tac ctxt [])
  13.534 +    end
  13.535 +in
  13.536 +
  13.537 +val implies_neg1_thm =
  13.538 +  @{lemma "(a \<longrightarrow> b) \<or> a"
  13.539 +      by blast}
  13.540 +
  13.541 +val implies_neg1  = prove_implies_pos_neg implies_neg1_thm
  13.542 +
  13.543 +val implies_neg2_thm =
  13.544 +  @{lemma "(a \<longrightarrow> b) \<or> \<not>b" by blast}
  13.545 +
  13.546 +val implies_neg2 = prove_implies_pos_neg implies_neg2_thm
  13.547 +
  13.548 +end
  13.549 +
  13.550 +val implies_thm =
  13.551 +  @{lemma "(~a \<longrightarrow> b) \<Longrightarrow> a \<or> b"
  13.552 +       "(a \<longrightarrow> b) \<Longrightarrow> \<not>a \<or> b"
  13.553 +     by blast+}
  13.554 +
  13.555 +fun implies_rules ctxt prems t = SMT_Replay_Methods.prove ctxt t (fn _ =>
  13.556 +  Method.insert_tac ctxt prems
  13.557 +  THEN' resolve_tac ctxt implies_thm
  13.558 +  THEN' assume_tac ctxt)
  13.559 +
  13.560 +
  13.561 +(*
  13.562 +Here is a case where force_tac fails, but auto_tac succeeds:
  13.563 +   Ex (P x) \<noteq> P x c \<Longrightarrow>
  13.564 +   (\<exists>v0. if x then P True v0 else P False v0) \<noteq> (if x then P True c else P False c)
  13.565 +
  13.566 +(this was before we added the eqsubst_tac). Therefore, to be safe, we add the fast, auto, and force.
  13.567 +*)
  13.568 +fun tmp_bfun_elim ctxt prems t = SMT_Replay_Methods.prove ctxt t (fn _ =>
  13.569 +  Method.insert_tac ctxt prems
  13.570 +  THEN' REPEAT_CHANGED (EqSubst.eqsubst_tac ctxt [0] @{thms verit_tmp_bfun_elim})
  13.571 +  THEN' TRY' (simplify_tac ctxt [])
  13.572 +  THEN' (Classical.fast_tac ctxt
  13.573 +    ORELSE' K (Clasimp.auto_tac ctxt)
  13.574 +    ORELSE' Clasimp.force_tac ctxt))
  13.575 +
  13.576 +val ite_pos1_thm =
  13.577 +  @{lemma "\<not>(if x then P else Q) \<or> x \<or> Q"
  13.578 +      by auto}
  13.579 +
  13.580 +fun ite_pos1 ctxt _ t = SMT_Replay_Methods.prove ctxt t (fn _ =>
  13.581 +  resolve_tac ctxt [ite_pos1_thm])
  13.582 +
  13.583 +val ite_pos2_thms =
  13.584 +  @{lemma "\<not>(if x then P else Q) \<or> \<not>x \<or> P" "\<not>(if \<not>x then P else Q) \<or> x \<or> P"
  13.585 +      by auto}
  13.586 +
  13.587 +fun ite_pos2 ctxt _ t = SMT_Replay_Methods.prove ctxt t (fn _ =>
  13.588 +  resolve_tac ctxt ite_pos2_thms)
  13.589 +
  13.590 +val ite_neg1_thms =
  13.591 +  @{lemma "(if x then P else Q) \<or> x \<or> \<not>Q" "(if x then P else \<not>Q) \<or> x \<or> Q"
  13.592 +      by auto}
  13.593 +
  13.594 +fun ite_neg1 ctxt _ t = SMT_Replay_Methods.prove ctxt t (fn _ =>
  13.595 +  resolve_tac ctxt ite_neg1_thms)
  13.596 +
  13.597 +val ite_neg2_thms =
  13.598 +  @{lemma "(if x then P else Q) \<or> \<not>x \<or> \<not>P" "(if \<not>x then P else Q) \<or> x \<or> \<not>P"
  13.599 +          "(if x then \<not>P else Q) \<or> \<not>x \<or> P" "(if \<not>x then \<not>P else Q) \<or> x \<or> P"
  13.600 +      by auto}
  13.601 +
  13.602 +fun ite_neg2 ctxt _ t = SMT_Replay_Methods.prove ctxt t (fn _ =>
  13.603 +  resolve_tac ctxt ite_neg2_thms)
  13.604 +
  13.605 +val ite1_thm =
  13.606 +  @{lemma "(if x then P else Q) \<Longrightarrow> x \<or> Q"
  13.607 +      by (auto split: if_splits) }
  13.608 +
  13.609 +fun ite1 ctxt [thm] t = SMT_Replay_Methods.prove ctxt t (fn _ =>
  13.610 +  resolve_tac ctxt [ite1_thm OF [thm]])
  13.611 +
  13.612 +val ite2_thm =
  13.613 +  @{lemma "(if x then P else Q) \<Longrightarrow> \<not>x \<or> P"
  13.614 +      by (auto split: if_splits) }
  13.615 +
  13.616 +fun ite2 ctxt [thm] t = SMT_Replay_Methods.prove ctxt t (fn _ =>
  13.617 +  resolve_tac ctxt [ite2_thm OF [thm]])
  13.618 +
  13.619 +
  13.620 +val not_ite1_thm =
  13.621 +  @{lemma "\<not>(if x then P else Q) \<Longrightarrow> x \<or> \<not>Q"
  13.622 +      by (auto split: if_splits) }
  13.623 +
  13.624 +fun not_ite1 ctxt [thm] t = SMT_Replay_Methods.prove ctxt t (fn _ =>
  13.625 +  resolve_tac ctxt [not_ite1_thm OF [thm]])
  13.626 +
  13.627 +val not_ite2_thm =
  13.628 +  @{lemma "\<not>(if x then P else Q) \<Longrightarrow> \<not>x \<or> \<not>P"
  13.629 +      by (auto split: if_splits) }
  13.630 +
  13.631 +fun not_ite2 ctxt [thm] t = SMT_Replay_Methods.prove ctxt t (fn _ =>
  13.632 +  resolve_tac ctxt [not_ite2_thm OF [thm]])
  13.633 +
  13.634 +
  13.635 +fun unit_res ctxt thms t =
  13.636 +  let
  13.637 +    val thms = map (Conv.fconv_rule Thm.eta_long_conversion) thms
  13.638 +    val t' = Thm.eta_long_conversion (Object_Logic.dest_judgment ctxt (Thm.cterm_of ctxt t))
  13.639 +    val (_, t2) = Logic.dest_equals (Thm.prop_of t')
  13.640 +    val thm = Z3_Replay_Methods.unit_res ctxt thms t2
  13.641 +  in
  13.642 +    @{thm verit_Pure_trans} OF [t', thm]
  13.643 +  end
  13.644 +
  13.645 +fun ite_intro ctxt _ t =
  13.646 +  let
  13.647 +    fun simplify_ite ctxt =
  13.648 +      ctxt
  13.649 +      |> empty_simpset
  13.650 +      |> put_simpset HOL_basic_ss
  13.651 +      |> (fn ctxt => ctxt addsimps @{thms eq_commute verit_ite_intro_simp if_cancel}
  13.652 +           addsimps @{thms simp_thms})
  13.653 +      |> Simplifier.full_simp_tac
  13.654 +  in
  13.655 +    SMT_Replay_Methods.prove ctxt t (fn _ =>
  13.656 +     (simplify_ite ctxt
  13.657 +     THEN' TRY' (Blast.blast_tac ctxt
  13.658 +       ORELSE' K (Clasimp.auto_tac ctxt)
  13.659 +       ORELSE' Clasimp.force_tac ctxt)))
  13.660 +  end
  13.661 +
  13.662 +
  13.663 +(* Quantifiers *)
  13.664 +
  13.665 +fun qnt_rm_unused ctxt _ t = SMT_Replay_Methods.prove ctxt t (fn _ =>
  13.666 +  Classical.fast_tac ctxt)
  13.667 +
  13.668 +fun qnt_simplify ctxt _ t = SMT_Replay_Methods.prove ctxt t (fn _ =>
  13.669 +  Classical.fast_tac ctxt)
  13.670 +
  13.671 +fun qnt_join ctxt _ t = SMT_Replay_Methods.prove ctxt t (fn _ =>
  13.672 +  Classical.fast_tac ctxt)
  13.673 +
  13.674 +
  13.675 +(* Equality *)
  13.676 +
  13.677 +fun eq_transitive ctxt _ t = SMT_Replay_Methods.prove ctxt t (fn  _ =>
  13.678 +  REPEAT_CHANGED (resolve_tac ctxt [@{thm disj_not1} RSN (1, @{thm iffD2}) OF @{thms impI}])
  13.679 +  THEN' REPEAT' (resolve_tac ctxt @{thms impI})
  13.680 +  THEN' REPEAT' (eresolve_tac ctxt @{thms conjI})
  13.681 +  THEN' REPEAT' (fn i => dresolve_tac ctxt @{thms verit_eq_transitive} i THEN assume_tac ctxt (i+1))
  13.682 +  THEN' resolve_tac ctxt @{thms refl})
  13.683 +
  13.684 +local
  13.685 +
  13.686 +  (* Rewrite might apply below choice. As we do not want to change them (it can break other
  13.687 +  rewriting steps), we cannot use Term.lambda *)
  13.688 +  fun abstract_over_no_choice (v, body) =
  13.689 +    let
  13.690 +      fun abs lev tm =
  13.691 +        if v aconv tm then Bound lev
  13.692 +        else
  13.693 +          (case tm of
  13.694 +            Abs (a, T, t) => Abs (a, T, abs (lev + 1) t)
  13.695 +          | t as (Const (\<^const_name>\<open>Hilbert_Choice.Eps\<close>, _) $ _) => t
  13.696 +          | t $ u =>
  13.697 +              (abs lev t $ (abs lev u handle Same.SAME => u)
  13.698 +                handle Same.SAME => t $ abs lev u)
  13.699 +          | _ => raise Same.SAME);
  13.700 +    in abs 0 body handle Same.SAME => body end;
  13.701 +
  13.702 +  fun lambda_name (x, v) t =
  13.703 +    Abs (if x = "" then Term.term_name v else x, fastype_of v, abstract_over_no_choice (v, t));
  13.704 +
  13.705 +  fun lambda v t = lambda_name ("", v) t;
  13.706 +
  13.707 +  fun extract_equal_terms (Const(\<^const_name>\<open>Trueprop\<close>, _) $ t) =
  13.708 +    let fun ext (Const(\<^const_name>\<open>HOL.disj\<close>, _) $ (Const(\<^const_name>\<open>HOL.Not\<close>, _) $
  13.709 +             (Const(\<^const_name>\<open>HOL.eq\<close>, _) $ t1 $ t2)) $ t) =
  13.710 +           apfst (curry (op ::) (t1, t2)) (ext t)
  13.711 +          | ext t = ([], t)
  13.712 +    in ext t end
  13.713 +  fun eq_congruent_tac ctxt t =
  13.714 +    let
  13.715 +       val (eqs, g) = extract_equal_terms t
  13.716 +       fun replace1 (t1, t2) (g, tac) =
  13.717 +         let
  13.718 +           val abs_t1 = lambda t2 g
  13.719 +           val subst = Drule.infer_instantiate' ctxt (map (SOME o Thm.cterm_of ctxt) [t1, t2, abs_t1])
  13.720 +                @{thm subst}
  13.721 +         in (Term.betapply (abs_t1, t1),
  13.722 +             tac THEN' resolve_tac ctxt [subst]
  13.723 +                 THEN' TRY' (assume_tac ctxt)) end
  13.724 +       val (_, tac) = fold replace1 eqs (g, K all_tac)
  13.725 +    in
  13.726 +       tac
  13.727 +    end
  13.728 +in
  13.729 +
  13.730 +fun eq_congruent_pred ctxt _ t =
  13.731 +   SMT_Replay_Methods.prove ctxt t (fn _ =>
  13.732 +   REPEAT' (resolve_tac ctxt [@{thm disj_not1[of \<open>_ = _\<close>]} RSN (1, @{thm iffD2}) OF @{thms impI}])
  13.733 +   THEN' REPEAT' (eresolve_tac ctxt @{thms conjI})
  13.734 +   THEN' eq_congruent_tac ctxt t
  13.735 +   THEN' resolve_tac ctxt @{thms refl excluded_middle
  13.736 +     excluded_middle[of \<open>\<not>_\<close>, unfolded not_not]})
  13.737 +
  13.738 +end
  13.739 +
  13.740 +
  13.741 +(* subproof *)
  13.742 +
  13.743 +fun subproof ctxt [prem] t =
  13.744 + SMT_Replay_Methods.prove ctxt t (fn _ =>
  13.745 +   (resolve_tac ctxt [@{thm disj_not1} RSN (1, @{thm iffD2}) OF [@{thm impI}],
  13.746 +        @{thm disj_not1[of \<open>\<not>_\<close>, unfolded not_not]} RSN (1, @{thm iffD2}) OF [@{thm impI}]]
  13.747 +     THEN' resolve_tac ctxt [prem]
  13.748 +     THEN_ALL_NEW assume_tac ctxt
  13.749 +     THEN' TRY' (assume_tac ctxt))
  13.750 +   ORELSE' TRY' (Method.insert_tac ctxt [prem] THEN' Blast.blast_tac ctxt))
  13.751 +
  13.752 +
  13.753 +(* la_rw_eq *)
  13.754 +
  13.755 +val la_rw_eq_thm = @{lemma \<open>(a :: nat) = b \<or> (a \<le> b) \<or> (a \<ge> b)\<close>
  13.756 +  by auto}
  13.757 +
  13.758 +fun la_rw_eq ctxt _ t = SMT_Replay_Methods.prove ctxt t (fn _ =>
  13.759 +  resolve_tac ctxt [la_rw_eq_thm])
  13.760 +
  13.761 +(* congruence *)
  13.762 +fun cong ctxt thms = SMT_Replay_Methods.try_provers ctxt
  13.763 +    (string_of_verit_rule Cong) [
  13.764 +  ("basic", SMT_Replay_Methods.cong_basic ctxt thms),
  13.765 +  ("full", SMT_Replay_Methods.cong_full ctxt thms),
  13.766 +  ("unfolding then auto", SMT_Replay_Methods.cong_unfolding_first ctxt thms)] thms
  13.767 +
  13.768 +
  13.769 +fun unsupported rule ctxt thms _ t = SMT_Replay_Methods.replay_error ctxt "Unsupported verit rule"
  13.770 +  rule thms t
  13.771 +
  13.772 +fun ignore_args f ctxt thm _ t = f ctxt thm t
  13.773 +
  13.774 +fun choose Bind = ignore_args bind
  13.775 +  | choose Refl = ignore_args refl
  13.776 +  | choose And_Pos = ignore_args and_pos
  13.777 +  | choose And_Neg = ignore_args and_neg_rule
  13.778 +  | choose Cong = ignore_args cong
  13.779 +  | choose Equiv_pos1 = ignore_args equiv_pos1
  13.780 +  | choose Equiv_pos2 = ignore_args equiv_pos2
  13.781 +  | choose Equiv_neg1 = ignore_args equiv_neg1
  13.782 +  | choose Equiv_neg2 = ignore_args equiv_neg2
  13.783 +  | choose Equiv1 = ignore_args equiv1
  13.784 +  | choose Equiv2 = ignore_args equiv2
  13.785 +  | choose Not_Equiv1 = ignore_args not_equiv1
  13.786 +  | choose Not_Equiv2 = ignore_args not_equiv2
  13.787 +  | choose Not_Implies1 = ignore_args not_implies1
  13.788 +  | choose Not_Implies2 = ignore_args not_implies2
  13.789 +  | choose Implies_Neg1 = ignore_args implies_neg1
  13.790 +  | choose Implies_Neg2 = ignore_args implies_neg2
  13.791 +  | choose Implies_Pos = ignore_args implies_pos
  13.792 +  | choose Implies = ignore_args implies_rules
  13.793 +  | choose Forall_Inst = forall_inst
  13.794 +  | choose Skolem_Forall = ignore_args skolem_forall
  13.795 +  | choose Skolem_Ex = ignore_args skolem_ex
  13.796 +  | choose Or = ignore_args or
  13.797 +  | choose Theory_Resolution = ignore_args unit_res
  13.798 +  | choose Resolution = ignore_args unit_res
  13.799 +  | choose Eq_Reflexive = ignore_args eq_reflexive
  13.800 +  | choose Connective_Equiv = ignore_args connective_equiv
  13.801 +  | choose Trans = ignore_args trans
  13.802 +  | choose False = ignore_args false_rule
  13.803 +  | choose Tmp_AC_Simp = ignore_args tmp_AC_rule
  13.804 +  | choose And = ignore_args and_rule
  13.805 +  | choose Not_And = ignore_args not_and_rule
  13.806 +  | choose Not_Or = ignore_args not_or_rule
  13.807 +  | choose Or_Pos = ignore_args or_pos_rule
  13.808 +  | choose Or_Neg = ignore_args or_neg_rule
  13.809 +  | choose Tmp_Bfun_Elim = ignore_args tmp_bfun_elim
  13.810 +  | choose ITE1 = ignore_args ite1
  13.811 +  | choose ITE2 = ignore_args ite2
  13.812 +  | choose Not_ITE1 = ignore_args not_ite1
  13.813 +  | choose Not_ITE2 = ignore_args not_ite2
  13.814 +  | choose ITE_Pos1 = ignore_args ite_pos1
  13.815 +  | choose ITE_Pos2 = ignore_args ite_pos2
  13.816 +  | choose ITE_Neg1 = ignore_args ite_neg1
  13.817 +  | choose ITE_Neg2 = ignore_args ite_neg2
  13.818 +  | choose ITE_Intro = ignore_args ite_intro
  13.819 +  | choose LA_Disequality = ignore_args Z3_Replay_Methods.arith_th_lemma
  13.820 +  | choose LIA_Generic = ignore_args Z3_Replay_Methods.arith_th_lemma
  13.821 +  | choose LA_Generic = ignore_args Z3_Replay_Methods.arith_th_lemma
  13.822 +  | choose LA_Totality = ignore_args Z3_Replay_Methods.arith_th_lemma
  13.823 +  | choose LA_Tautology = ignore_args Z3_Replay_Methods.arith_th_lemma
  13.824 +  | choose LA_RW_Eq = ignore_args la_rw_eq
  13.825 +  | choose NLA_Generic = ignore_args Z3_Replay_Methods.arith_th_lemma
  13.826 +  | choose Normalized_Input = ignore_args normalized_input
  13.827 +  | choose Qnt_Rm_Unused = ignore_args qnt_rm_unused
  13.828 +  | choose Qnt_Simplify = ignore_args qnt_simplify
  13.829 +  | choose Qnt_Join = ignore_args qnt_join
  13.830 +  | choose Eq_Congruent_Pred = ignore_args eq_congruent_pred
  13.831 +  | choose Eq_Congruent = ignore_args eq_congruent_pred
  13.832 +  | choose Eq_Transitive = ignore_args eq_transitive
  13.833 +  | choose Local_Input = ignore_args refl
  13.834 +  | choose Subproof = ignore_args subproof
  13.835 +  | choose r = unsupported (string_of_verit_rule r)
  13.836 +
  13.837 +type Verit_method = Proof.context -> thm list -> term -> thm
  13.838 +type abs_context = int * term Termtab.table
  13.839 +
  13.840 +fun with_tracing rule method ctxt thms args t =
  13.841 +  let val _ = SMT_Replay_Methods.trace_goal ctxt rule thms t
  13.842 +  in method ctxt thms args t end
  13.843 +
  13.844 +fun method_for rule = with_tracing rule (choose (verit_rule_of rule))
  13.845 +
  13.846 +end;
    14.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Tue Oct 30 16:24:01 2018 +0100
    14.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Tue Oct 30 16:24:04 2018 +0100
    14.3 @@ -55,7 +55,6 @@
    14.4  val vampire_skolemisation_rule = "skolemisation"
    14.5  val veriT_la_generic_rule = "la_generic"
    14.6  val veriT_simp_arith_rule = "simp_arith"
    14.7 -val veriT_tmp_ite_elim_rule = "tmp_ite_elim"
    14.8  val veriT_tmp_skolemize_rule = "tmp_skolemize"
    14.9  val z3_skolemize_rule = Z3_Proof.string_of_rule Z3_Proof.Skolemize
   14.10  val z3_th_lemma_rule_prefix = Z3_Proof.string_of_rule (Z3_Proof.Th_Lemma "")
   14.11 @@ -63,7 +62,7 @@
   14.12  
   14.13  val skolemize_rules =
   14.14    [e_definition_rule, e_skolemize_rule, leo2_extcnf_forall_neg_rule, satallax_skolemize_rule,
   14.15 -   spass_skolemize_rule, vampire_skolemisation_rule, veriT_tmp_ite_elim_rule,
   14.16 +   spass_skolemize_rule, vampire_skolemisation_rule,
   14.17     veriT_tmp_skolemize_rule, waldmeister_skolemize_rule, z3_skolemize_rule, zipperposition_cnf_rule]
   14.18  
   14.19  fun is_ext_rule rule = (rule = leo2_extcnf_equal_neg_rule)