--- a/CONTRIBUTORS Tue Oct 30 22:08:36 2018 +0100
+++ b/CONTRIBUTORS Tue Oct 30 22:59:06 2018 +0100
@@ -6,6 +6,9 @@
Contributions to this Isabelle version
--------------------------------------
+* October 2018: Mathias Fleury
+ Proof reconstruction for the SMT solver veriT in the smt method
+
Contributions to Isabelle2018
-----------------------------
--- a/NEWS Tue Oct 30 22:08:36 2018 +0100
+++ b/NEWS Tue Oct 30 22:59:06 2018 +0100
@@ -55,6 +55,8 @@
* Sledgehammer: The URL for SystemOnTPTP, which is used by remote
provers, has been updated.
+* SMT: reconstruction is now possible using the SMT solver veriT.
+
* Session HOL-SPARK: .prv files are no longer written to the
file-system, but exported to the session database. Results may be
retrieved with the "isabelle export" command-line tool like this:
--- a/src/HOL/Data_Structures/Array_Braun.thy Tue Oct 30 22:08:36 2018 +0100
+++ b/src/HOL/Data_Structures/Array_Braun.thy Tue Oct 30 22:59:06 2018 +0100
@@ -266,11 +266,11 @@
subsection "Faster"
-fun braun_of_rec :: "'a \<Rightarrow> nat \<Rightarrow> 'a tree" where
-"braun_of_rec x n = (if n=0 then Leaf
+fun braun_of_naive :: "'a \<Rightarrow> nat \<Rightarrow> 'a tree" where
+"braun_of_naive x n = (if n=0 then Leaf
else let m = (n-1) div 2
- in if odd n then Node (braun_of_rec x m) x (braun_of_rec x m)
- else Node (braun_of_rec x (m + 1)) x (braun_of_rec x m))"
+ in if odd n then Node (braun_of_naive x m) x (braun_of_naive x m)
+ else Node (braun_of_naive x (m + 1)) x (braun_of_naive x m))"
fun braun2_of :: "'a \<Rightarrow> nat \<Rightarrow> 'a tree * 'a tree" where
"braun2_of x n = (if n = 0 then (Leaf, Node Leaf x Leaf)
--- a/src/HOL/SMT.thy Tue Oct 30 22:08:36 2018 +0100
+++ b/src/HOL/SMT.thy Tue Oct 30 22:59:06 2018 +0100
@@ -190,6 +190,100 @@
by (simp add: z3mod_def)
+subsection \<open>Extra theorems for veriT reconstruction\<close>
+
+lemma verit_sko_forall: \<open>(\<forall>x. P x) \<longleftrightarrow> P (SOME x. \<not>P x)\<close>
+ using someI[of \<open>\<lambda>x. \<not>P x\<close>]
+ by auto
+
+lemma verit_sko_forall': \<open>P (SOME x. \<not>P x) = A \<Longrightarrow> (\<forall>x. P x) = A\<close>
+ by (subst verit_sko_forall)
+
+lemma verit_sko_forall_indirect: \<open>x = (SOME x. \<not>P x) \<Longrightarrow> (\<forall>x. P x) \<longleftrightarrow> P x\<close>
+ using someI[of \<open>\<lambda>x. \<not>P x\<close>]
+ by auto
+
+lemma verit_sko_ex: \<open>(\<exists>x. P x) \<longleftrightarrow> P (SOME x. P x)\<close>
+ using someI[of \<open>\<lambda>x. P x\<close>]
+ by auto
+
+lemma verit_sko_ex': \<open>P (SOME x. P x) = A \<Longrightarrow> (\<exists>x. P x) = A\<close>
+ by (subst verit_sko_ex)
+
+lemma verit_sko_ex_indirect: \<open>x = (SOME x. P x) \<Longrightarrow> (\<exists>x. P x) \<longleftrightarrow> P x\<close>
+ using someI[of \<open>\<lambda>x. P x\<close>]
+ by auto
+
+lemma verit_Pure_trans:
+ \<open>P \<equiv> Q \<Longrightarrow> Q \<Longrightarrow> P\<close>
+ by auto
+
+lemma verit_if_cong:
+ assumes \<open>b \<equiv> c\<close>
+ and \<open>c \<Longrightarrow> x \<equiv> u\<close>
+ and \<open>\<not> c \<Longrightarrow> y \<equiv> v\<close>
+ shows \<open>(if b then x else y) \<equiv> (if c then u else v)\<close>
+ using assms if_cong[of b c x u] by auto
+
+lemma verit_if_weak_cong':
+ \<open>b \<equiv> c \<Longrightarrow> (if b then x else y) \<equiv> (if c then x else y)\<close>
+ by auto
+
+lemma verit_ite_intro_simp:
+ \<open>(if c then (a :: 'a) = (if c then P else Q') else Q) = (if c then a = P else Q)\<close>
+ \<open>(if c then R else b = (if c then R' else Q')) =
+ (if c then R else b = Q')\<close>
+ \<open>(if c then a' = a' else b' = b')\<close>
+ by (auto split: if_splits)
+
+lemma verit_or_neg:
+ \<open>(A \<Longrightarrow> B) \<Longrightarrow> B \<or> \<not>A\<close>
+ \<open>(\<not>A \<Longrightarrow> B) \<Longrightarrow> B \<or> A\<close>
+ by auto
+
+lemma verit_subst_bool: \<open>P \<Longrightarrow> f True \<Longrightarrow> f P\<close>
+ by auto
+
+lemma verit_and_pos:
+ \<open>(a \<Longrightarrow> \<not>b \<or> A) \<Longrightarrow> \<not>(a \<and> b) \<or> A\<close>
+ \<open>(a \<Longrightarrow> A) \<Longrightarrow> \<not>a \<or> A\<close>
+ \<open>(\<not>a \<Longrightarrow> A) \<Longrightarrow> a \<or> A\<close>
+ by blast+
+
+lemma verit_la_generic:
+ \<open>(a::int) \<le> x \<or> a = x \<or> a \<ge> x\<close>
+ by linarith
+
+lemma verit_tmp_bfun_elim:
+ \<open>(if b then P True else P False) = P b\<close>
+ by (cases b) auto
+
+lemma verit_eq_true_simplify:
+ \<open>(P = True) \<equiv> P\<close>
+ by auto
+
+lemma verit_and_neg:
+ \<open>B \<or> B' \<Longrightarrow> (A \<and> B) \<or> \<not>A \<or> B'\<close>
+ \<open>B \<or> B' \<Longrightarrow> (\<not>A \<and> B) \<or> A \<or> B'\<close>
+ by auto
+
+lemma verit_forall_inst:
+ \<open>A \<longleftrightarrow> B \<Longrightarrow> \<not>A \<or> B\<close>
+ \<open>\<not>A \<longleftrightarrow> B \<Longrightarrow> A \<or> B\<close>
+ \<open>A \<longleftrightarrow> B \<Longrightarrow> \<not>B \<or> A\<close>
+ \<open>A \<longleftrightarrow> \<not>B \<Longrightarrow> B \<or> A\<close>
+ \<open>A \<longrightarrow> B \<Longrightarrow> \<not>A \<or> B\<close>
+ \<open>\<not>A \<longrightarrow> B \<Longrightarrow> A \<or> B\<close>
+ by blast+
+
+lemma verit_eq_transitive:
+ \<open>A = B \<Longrightarrow> B = C \<Longrightarrow> A = C\<close>
+ \<open>A = B \<Longrightarrow> C = B \<Longrightarrow> A = C\<close>
+ \<open>B = A \<Longrightarrow> B = C \<Longrightarrow> A = C\<close>
+ \<open>B = A \<Longrightarrow> C = B \<Longrightarrow> A = C\<close>
+ by auto
+
+
subsection \<open>Setup\<close>
ML_file "Tools/SMT/smt_util.ML"
@@ -212,11 +306,14 @@
ML_file "Tools/SMT/verit_isar.ML"
ML_file "Tools/SMT/verit_proof_parse.ML"
ML_file "Tools/SMT/conj_disj_perm.ML"
+ML_file "Tools/SMT/smt_replay_methods.ML"
+ML_file "Tools/SMT/smt_replay.ML"
ML_file "Tools/SMT/z3_interface.ML"
-ML_file "Tools/SMT/z3_replay_util.ML"
ML_file "Tools/SMT/z3_replay_rules.ML"
ML_file "Tools/SMT/z3_replay_methods.ML"
ML_file "Tools/SMT/z3_replay.ML"
+ML_file "Tools/SMT/verit_replay_methods.ML"
+ML_file "Tools/SMT/verit_replay.ML"
ML_file "Tools/SMT/smt_systems.ML"
method_setup smt = \<open>
@@ -275,7 +372,7 @@
declare [[cvc3_options = ""]]
declare [[cvc4_options = "--full-saturate-quant --inst-when=full-last-call --inst-no-entail --term-db-mode=relevant --multi-trigger-linear"]]
-declare [[verit_options = "--index-sorts --index-fresh-sorts"]]
+declare [[verit_options = "--index-fresh-sorts"]]
declare [[z3_options = ""]]
text \<open>
--- a/src/HOL/Tools/SMT/conj_disj_perm.ML Tue Oct 30 22:08:36 2018 +0100
+++ b/src/HOL/Tools/SMT/conj_disj_perm.ML Tue Oct 30 22:59:06 2018 +0100
@@ -124,4 +124,4 @@
resolve_tac ctxt [prove_conj_disj_perm ct (Thm.dest_binop (Thm.dest_arg ct))] i
| _ => no_tac))
-end
+end;
--- a/src/HOL/Tools/SMT/smt_config.ML Tue Oct 30 22:08:36 2018 +0100
+++ b/src/HOL/Tools/SMT/smt_config.ML Tue Oct 30 22:59:06 2018 +0100
@@ -47,6 +47,7 @@
val trace_msg: Proof.context -> ('a -> string) -> 'a -> unit
val verbose_msg: Proof.context -> ('a -> string) -> 'a -> unit
val statistics_msg: Proof.context -> ('a -> string) -> 'a -> unit
+ val veriT_msg: Proof.context -> (unit -> 'a) -> unit
(*certificates*)
val select_certificates: string -> Context.generic -> Context.generic
@@ -179,6 +180,7 @@
val read_only_certificates = Attrib.setup_config_bool \<^binding>\<open>smt_read_only_certificates\<close> (K false)
val verbose = Attrib.setup_config_bool \<^binding>\<open>smt_verbose\<close> (K true)
val trace = Attrib.setup_config_bool \<^binding>\<open>smt_trace\<close> (K false)
+val trace_veriT = Attrib.setup_config_bool \<^binding>\<open>smt_debug_verit\<close> (K false)
val statistics = Attrib.setup_config_bool \<^binding>\<open>smt_statistics\<close> (K false)
val monomorph_limit = Attrib.setup_config_int \<^binding>\<open>smt_monomorph_limit\<close> (K 10)
val monomorph_instances = Attrib.setup_config_int \<^binding>\<open>smt_monomorph_instances\<close> (K 500)
@@ -198,6 +200,8 @@
fun trace_msg ctxt = cond_trace (Config.get ctxt trace)
fun statistics_msg ctxt = cond_trace (Config.get ctxt statistics)
+fun veriT_msg ctxt (x : unit -> 'a) = if (Config.get ctxt trace_veriT) then ignore(x ()) else ()
+
(* tools *)
--- a/src/HOL/Tools/SMT/smt_real.ML Tue Oct 30 22:08:36 2018 +0100
+++ b/src/HOL/Tools/SMT/smt_real.ML Tue Oct 30 22:59:06 2018 +0100
@@ -110,6 +110,6 @@
SMTLIB_Interface.add_logic (10, smtlib_logic) #>
setup_builtins #>
Z3_Interface.add_mk_builtins z3_mk_builtins #>
- Z3_Replay_Util.add_simproc real_linarith_proc))
+ SMT_Replay.add_simproc real_linarith_proc))
end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/SMT/smt_replay.ML Tue Oct 30 22:59:06 2018 +0100
@@ -0,0 +1,269 @@
+(* Title: HOL/Tools/SMT/smt_replay.ML
+ Author: Sascha Boehme, TU Muenchen
+ Author: Jasmin Blanchette, TU Muenchen
+ Author: Mathias Fleury, MPII
+
+Shared library for parsing and replay.
+*)
+
+signature SMT_REPLAY =
+sig
+ (*theorem nets*)
+ val thm_net_of: ('a -> thm) -> 'a list -> 'a Net.net
+ val net_instances: (int * thm) Net.net -> cterm -> (int * thm) list
+
+ (*proof combinators*)
+ val under_assumption: (thm -> thm) -> cterm -> thm
+ val discharge: thm -> thm -> thm
+
+ (*a faster COMP*)
+ type compose_data = cterm list * (cterm -> cterm list) * thm
+ val precompose: (cterm -> cterm list) -> thm -> compose_data
+ val precompose2: (cterm -> cterm * cterm) -> thm -> compose_data
+ val compose: compose_data -> thm -> thm
+
+ (*simpset*)
+ val add_simproc: Simplifier.simproc -> Context.generic -> Context.generic
+ val make_simpset: Proof.context -> thm list -> simpset
+
+ (*assertion*)
+ val add_asserted: ('a * ('b * thm) -> 'c -> 'c) ->
+ 'c -> ('d -> 'a * 'e * term * 'b) -> ('e -> bool) -> Proof.context -> thm list ->
+ (int * thm) list -> 'd list -> Proof.context ->
+ ((int * ('a * thm)) list * thm list) * (Proof.context * 'c)
+
+ (*statistics*)
+ val pretty_statistics: string -> int -> int list Symtab.table -> Pretty.T
+ val intermediate_statistics: Proof.context -> Timing.start -> int -> int -> unit
+
+ (*theorem transformation*)
+ val varify: Proof.context -> thm -> thm
+ val params_of: term -> (string * typ) list
+end;
+
+structure SMT_Replay : SMT_REPLAY =
+struct
+
+(* theorem nets *)
+
+fun thm_net_of f xthms =
+ let fun insert xthm = Net.insert_term (K false) (Thm.prop_of (f xthm), xthm)
+ in fold insert xthms Net.empty end
+
+fun maybe_instantiate ct thm =
+ try Thm.first_order_match (Thm.cprop_of thm, ct)
+ |> Option.map (fn inst => Thm.instantiate inst thm)
+
+local
+ fun instances_from_net match f net ct =
+ let
+ val lookup = if match then Net.match_term else Net.unify_term
+ val xthms = lookup net (Thm.term_of ct)
+ fun select ct = map_filter (f (maybe_instantiate ct)) xthms
+ fun select' ct =
+ let val thm = Thm.trivial ct
+ in map_filter (f (try (fn rule => rule COMP thm))) xthms end
+ in (case select ct of [] => select' ct | xthms' => xthms') end
+in
+
+fun net_instances net =
+ instances_from_net false (fn f => fn (i, thm) => Option.map (pair i) (f thm))
+ net
+
+end
+
+
+(* proof combinators *)
+
+fun under_assumption f ct =
+ let val ct' = SMT_Util.mk_cprop ct in Thm.implies_intr ct' (f (Thm.assume ct')) end
+
+fun discharge p pq = Thm.implies_elim pq p
+
+
+(* a faster COMP *)
+
+type compose_data = cterm list * (cterm -> cterm list) * thm
+
+fun list2 (x, y) = [x, y]
+
+fun precompose f rule : compose_data = (f (Thm.cprem_of rule 1), f, rule)
+fun precompose2 f rule : compose_data = precompose (list2 o f) rule
+
+fun compose (cvs, f, rule) thm =
+ discharge thm
+ (Thm.instantiate ([], map (dest_Var o Thm.term_of) cvs ~~ f (Thm.cprop_of thm)) rule)
+
+
+(* simpset *)
+
+local
+ val antisym_le1 = mk_meta_eq @{thm order_class.antisym_conv}
+ val antisym_le2 = mk_meta_eq @{thm linorder_class.antisym_conv2}
+ val antisym_less1 = mk_meta_eq @{thm linorder_class.antisym_conv1}
+ val antisym_less2 = mk_meta_eq @{thm linorder_class.antisym_conv3}
+
+ fun eq_prop t thm = HOLogic.mk_Trueprop t aconv Thm.prop_of thm
+ fun dest_binop ((c as Const _) $ t $ u) = (c, t, u)
+ | dest_binop t = raise TERM ("dest_binop", [t])
+
+ fun prove_antisym_le ctxt ct =
+ let
+ val (le, r, s) = dest_binop (Thm.term_of ct)
+ val less = Const (@{const_name less}, Term.fastype_of le)
+ val prems = Simplifier.prems_of ctxt
+ in
+ (case find_first (eq_prop (le $ s $ r)) prems of
+ NONE =>
+ find_first (eq_prop (HOLogic.mk_not (less $ r $ s))) prems
+ |> Option.map (fn thm => thm RS antisym_less1)
+ | SOME thm => SOME (thm RS antisym_le1))
+ end
+ handle THM _ => NONE
+
+ fun prove_antisym_less ctxt ct =
+ let
+ val (less, r, s) = dest_binop (HOLogic.dest_not (Thm.term_of ct))
+ val le = Const (@{const_name less_eq}, Term.fastype_of less)
+ val prems = Simplifier.prems_of ctxt
+ in
+ (case find_first (eq_prop (le $ r $ s)) prems of
+ NONE =>
+ find_first (eq_prop (HOLogic.mk_not (less $ s $ r))) prems
+ |> Option.map (fn thm => thm RS antisym_less2)
+ | SOME thm => SOME (thm RS antisym_le2))
+ end
+ handle THM _ => NONE
+
+ val basic_simpset =
+ simpset_of (put_simpset HOL_ss @{context}
+ addsimps @{thms field_simps times_divide_eq_right times_divide_eq_left arith_special
+ arith_simps rel_simps array_rules z3div_def z3mod_def NO_MATCH_def}
+ addsimprocs [@{simproc numeral_divmod},
+ Simplifier.make_simproc @{context} "fast_int_arith"
+ {lhss = [@{term "(m::int) < n"}, @{term "(m::int) \<le> n"}, @{term "(m::int) = n"}],
+ proc = K Lin_Arith.simproc},
+ Simplifier.make_simproc @{context} "antisym_le"
+ {lhss = [@{term "(x::'a::order) \<le> y"}],
+ proc = K prove_antisym_le},
+ Simplifier.make_simproc @{context} "antisym_less"
+ {lhss = [@{term "\<not> (x::'a::linorder) < y"}],
+ proc = K prove_antisym_less}])
+
+ structure Simpset = Generic_Data
+ (
+ type T = simpset
+ val empty = basic_simpset
+ val extend = I
+ val merge = Simplifier.merge_ss
+ )
+in
+
+fun add_simproc simproc context =
+ Simpset.map (simpset_map (Context.proof_of context)
+ (fn ctxt => ctxt addsimprocs [simproc])) context
+
+fun make_simpset ctxt rules =
+ simpset_of (put_simpset (Simpset.get (Context.Proof ctxt)) ctxt addsimps rules)
+
+end
+
+local
+ val remove_trigger = mk_meta_eq @{thm trigger_def}
+ val remove_fun_app = mk_meta_eq @{thm fun_app_def}
+
+ fun rewrite_conv _ [] = Conv.all_conv
+ | rewrite_conv ctxt eqs = Simplifier.full_rewrite (empty_simpset ctxt addsimps eqs)
+
+ val rewrite_true_rule = @{lemma "True \<equiv> \<not> False" by simp}
+ val prep_rules = [@{thm Let_def}, remove_trigger, remove_fun_app, rewrite_true_rule]
+
+ fun rewrite _ [] = I
+ | rewrite ctxt eqs = Conv.fconv_rule (rewrite_conv ctxt eqs)
+
+ fun lookup_assm assms_net ct =
+ net_instances assms_net ct
+ |> map (fn ithm as (_, thm) => (ithm, Thm.cprop_of thm aconvc ct))
+in
+
+fun add_asserted tab_update tab_empty p_extract cond outer_ctxt rewrite_rules assms steps ctxt =
+ let
+ val eqs = map (rewrite ctxt [rewrite_true_rule]) rewrite_rules
+ val eqs' = union Thm.eq_thm eqs prep_rules
+
+ val assms_net =
+ assms
+ |> map (apsnd (rewrite ctxt eqs'))
+ |> map (apsnd (Conv.fconv_rule Thm.eta_conversion))
+ |> thm_net_of snd
+
+ fun revert_conv ctxt = rewrite_conv ctxt eqs' then_conv Thm.eta_conversion
+
+ fun assume thm ctxt =
+ let
+ val ct = Thm.cprem_of thm 1
+ val (thm', ctxt') = yield_singleton Assumption.add_assumes ct ctxt
+ in (thm' RS thm, ctxt') end
+
+ fun add1 id fixes thm1 ((i, th), exact) ((iidths, thms), (ctxt, ptab)) =
+ let
+ val (thm, ctxt') = if exact then (Thm.implies_elim thm1 th, ctxt) else assume thm1 ctxt
+ val thms' = if exact then thms else th :: thms
+ in (((i, (id, th)) :: iidths, thms'), (ctxt', tab_update (id, (fixes, thm)) ptab)) end
+
+ fun add step
+ (cx as ((iidths, thms), (ctxt, ptab))) =
+ let val (id, rule, concl, fixes) = p_extract step in
+ if (*Z3_Proof.is_assumption rule andalso rule <> Z3_Proof.Hypothesis*) cond rule then
+ let
+ val ct = Thm.cterm_of ctxt concl
+ val thm1 = Thm.trivial ct |> Conv.fconv_rule (Conv.arg1_conv (revert_conv outer_ctxt))
+ val thm2 = singleton (Variable.export ctxt outer_ctxt) thm1
+ in
+ (case lookup_assm assms_net (Thm.cprem_of thm2 1) of
+ [] =>
+ let val (thm, ctxt') = assume thm1 ctxt
+ in ((iidths, thms), (ctxt', tab_update (id, (fixes, thm)) ptab)) end
+ | ithms => fold (add1 id fixes thm1) ithms cx)
+ end
+ else
+ cx
+ end
+ in fold add steps (([], []), (ctxt, tab_empty)) end
+
+end
+
+fun params_of t = Term.strip_qnt_vars @{const_name Pure.all} t
+
+fun varify ctxt thm =
+ let
+ val maxidx = Thm.maxidx_of thm + 1
+ val vs = params_of (Thm.prop_of thm)
+ val vars = map_index (fn (i, (n, T)) => Var ((n, i + maxidx), T)) vs
+ in Drule.forall_elim_list (map (Thm.cterm_of ctxt) vars) thm end
+
+fun intermediate_statistics ctxt start total =
+ SMT_Config.statistics_msg ctxt (fn current =>
+ "Reconstructed " ^ string_of_int current ^ " of " ^ string_of_int total ^ " steps in " ^
+ string_of_int (Time.toMilliseconds (#elapsed (Timing.result start))) ^ " ms")
+
+fun pretty_statistics solver total stats =
+ let
+ fun mean_of is =
+ let
+ val len = length is
+ val mid = len div 2
+ in if len mod 2 = 0 then (nth is (mid - 1) + nth is mid) div 2 else nth is mid end
+ fun pretty_item name p = Pretty.item (Pretty.separate ":" [Pretty.str name, p])
+ fun pretty (name, milliseconds) = pretty_item name (Pretty.block (Pretty.separate "," [
+ Pretty.str (string_of_int (length milliseconds) ^ " occurrences") ,
+ Pretty.str (string_of_int (mean_of milliseconds) ^ " ms mean time"),
+ Pretty.str (string_of_int (fold Integer.max milliseconds 0) ^ " ms maximum time"),
+ Pretty.str (string_of_int (fold Integer.add milliseconds 0) ^ " ms total time")]))
+ in
+ Pretty.big_list (solver ^ " proof reconstruction statistics:") (
+ pretty_item "total time" (Pretty.str (string_of_int total ^ " ms")) ::
+ map pretty (Symtab.dest stats))
+ end
+
+end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/SMT/smt_replay_methods.ML Tue Oct 30 22:59:06 2018 +0100
@@ -0,0 +1,337 @@
+(* Title: HOL/Tools/SMT/smt_replay_methods.ML
+ Author: Sascha Boehme, TU Muenchen
+ Author: Jasmin Blanchette, TU Muenchen
+ Author: Mathias Fleury, MPII
+
+Proof methods for replaying SMT proofs.
+*)
+
+signature SMT_REPLAY_METHODS =
+sig
+ val pretty_goal: Proof.context -> string -> string -> thm list -> term -> Pretty.T
+ val trace_goal: Proof.context -> string -> thm list -> term -> unit
+ val trace: Proof.context -> (unit -> string) -> unit
+
+ val replay_error: Proof.context -> string -> string -> thm list -> term -> 'a
+ val replay_rule_error: Proof.context -> string -> thm list -> term -> 'a
+
+ (*theory lemma methods*)
+ type th_lemma_method = Proof.context -> thm list -> term -> thm
+ val add_th_lemma_method: string * th_lemma_method -> Context.generic ->
+ Context.generic
+ val get_th_lemma_method: Proof.context -> th_lemma_method Symtab.table
+ val discharge: int -> thm list -> thm -> thm
+ val match_instantiate: Proof.context -> term -> thm -> thm
+ val prove: Proof.context -> term -> (Proof.context -> int -> tactic) -> thm
+
+ (*abstraction*)
+ type abs_context = int * term Termtab.table
+ type 'a abstracter = term -> abs_context -> 'a * abs_context
+ val add_arith_abstracter: (term abstracter -> term option abstracter) ->
+ Context.generic -> Context.generic
+
+ val abstract_lit: term -> abs_context -> term * abs_context
+ val abstract_conj: term -> abs_context -> term * abs_context
+ val abstract_disj: term -> abs_context -> term * abs_context
+ val abstract_not: (term -> abs_context -> term * abs_context) ->
+ term -> abs_context -> term * abs_context
+ val abstract_unit: term -> abs_context -> term * abs_context
+ val abstract_prop: term -> abs_context -> term * abs_context
+ val abstract_term: term -> abs_context -> term * abs_context
+ val abstract_arith: Proof.context -> term -> abs_context -> term * abs_context
+
+ val prove_abstract: Proof.context -> thm list -> term ->
+ (Proof.context -> thm list -> int -> tactic) ->
+ (abs_context -> (term list * term) * abs_context) -> thm
+ val prove_abstract': Proof.context -> term -> (Proof.context -> thm list -> int -> tactic) ->
+ (abs_context -> term * abs_context) -> thm
+ val try_provers: Proof.context -> string -> (string * (term -> 'a)) list -> thm list -> term ->
+ 'a
+
+ (*shared tactics*)
+ val cong_basic: Proof.context -> thm list -> term -> thm
+ val cong_full: Proof.context -> thm list -> term -> thm
+ val cong_unfolding_first: Proof.context -> thm list -> term -> thm
+
+ val certify_prop: Proof.context -> term -> cterm
+
+end;
+
+structure SMT_Replay_Methods: SMT_REPLAY_METHODS =
+struct
+
+(* utility functions *)
+
+fun trace ctxt f = SMT_Config.trace_msg ctxt f ()
+
+fun pretty_thm ctxt thm = Syntax.pretty_term ctxt (Thm.concl_of thm)
+
+fun pretty_goal ctxt msg rule thms t =
+ let
+ val full_msg = msg ^ ": " ^ quote rule
+ val assms =
+ if null thms then []
+ else [Pretty.big_list "assumptions:" (map (pretty_thm ctxt) thms)]
+ val concl = Pretty.big_list "proposition:" [Syntax.pretty_term ctxt t]
+ in Pretty.big_list full_msg (assms @ [concl]) end
+
+fun replay_error ctxt msg rule thms t = error (Pretty.string_of (pretty_goal ctxt msg rule thms t))
+
+fun replay_rule_error ctxt = replay_error ctxt "Failed to replay Z3 proof step"
+
+fun trace_goal ctxt rule thms t =
+ trace ctxt (fn () => Pretty.string_of (pretty_goal ctxt "Goal" rule thms t))
+
+fun as_prop (t as Const (@{const_name Trueprop}, _) $ _) = t
+ | as_prop t = HOLogic.mk_Trueprop t
+
+fun dest_prop (Const (@{const_name Trueprop}, _) $ t) = t
+ | dest_prop t = t
+
+fun dest_thm thm = dest_prop (Thm.concl_of thm)
+
+
+(* plug-ins *)
+
+type abs_context = int * term Termtab.table
+
+type 'a abstracter = term -> abs_context -> 'a * abs_context
+
+type th_lemma_method = Proof.context -> thm list -> term -> thm
+
+fun id_ord ((id1, _), (id2, _)) = int_ord (id1, id2)
+
+structure Plugins = Generic_Data
+(
+ type T =
+ (int * (term abstracter -> term option abstracter)) list *
+ th_lemma_method Symtab.table
+ val empty = ([], Symtab.empty)
+ val extend = I
+ fun merge ((abss1, ths1), (abss2, ths2)) = (
+ Ord_List.merge id_ord (abss1, abss2),
+ Symtab.merge (K true) (ths1, ths2))
+)
+
+fun add_arith_abstracter abs = Plugins.map (apfst (Ord_List.insert id_ord (serial (), abs)))
+fun get_arith_abstracters ctxt = map snd (fst (Plugins.get (Context.Proof ctxt)))
+
+fun add_th_lemma_method method = Plugins.map (apsnd (Symtab.update_new method))
+fun get_th_lemma_method ctxt = snd (Plugins.get (Context.Proof ctxt))
+
+fun match ctxt pat t =
+ (Vartab.empty, Vartab.empty)
+ |> Pattern.first_order_match (Proof_Context.theory_of ctxt) (pat, t)
+
+fun gen_certify_inst sel cert ctxt thm t =
+ let
+ val inst = match ctxt (dest_thm thm) (dest_prop t)
+ fun cert_inst (ix, (a, b)) = ((ix, a), cert b)
+ in Vartab.fold (cons o cert_inst) (sel inst) [] end
+
+fun match_instantiateT ctxt t thm =
+ if Term.exists_type (Term.exists_subtype Term.is_TVar) (dest_thm thm) then
+ Thm.instantiate (gen_certify_inst fst (Thm.ctyp_of ctxt) ctxt thm t, []) thm
+ else thm
+
+fun match_instantiate ctxt t thm =
+ let val thm' = match_instantiateT ctxt t thm in
+ Thm.instantiate ([], gen_certify_inst snd (Thm.cterm_of ctxt) ctxt thm' t) thm'
+ end
+
+fun discharge _ [] thm = thm
+ | discharge i (rule :: rules) thm = discharge (i + Thm.nprems_of rule) rules (rule RSN (i, thm))
+
+fun by_tac ctxt thms ns ts t tac =
+ Goal.prove ctxt [] (map as_prop ts) (as_prop t)
+ (fn {context, prems} => HEADGOAL (tac context prems))
+ |> Drule.generalize ([], ns)
+ |> discharge 1 thms
+
+fun prove ctxt t tac = by_tac ctxt [] [] [] t (K o tac)
+
+
+(* abstraction *)
+
+fun prove_abstract ctxt thms t tac f =
+ let
+ val ((prems, concl), (_, ts)) = f (1, Termtab.empty)
+ val ns = Termtab.fold (fn (_, v) => cons (fst (Term.dest_Free v))) ts []
+ in
+ by_tac ctxt [] ns prems concl tac
+ |> match_instantiate ctxt t
+ |> discharge 1 thms
+ end
+
+fun prove_abstract' ctxt t tac f =
+ prove_abstract ctxt [] t tac (f #>> pair [])
+
+fun lookup_term (_, terms) t = Termtab.lookup terms t
+
+fun abstract_sub t f cx =
+ (case lookup_term cx t of
+ SOME v => (v, cx)
+ | NONE => f cx)
+
+fun mk_fresh_free t (i, terms) =
+ let val v = Free ("t" ^ string_of_int i, fastype_of t)
+ in (v, (i + 1, Termtab.update (t, v) terms)) end
+
+fun apply_abstracters _ [] _ cx = (NONE, cx)
+ | apply_abstracters abs (abstracter :: abstracters) t cx =
+ (case abstracter abs t cx of
+ (NONE, _) => apply_abstracters abs abstracters t cx
+ | x as (SOME _, _) => x)
+
+fun abstract_term (t as _ $ _) = abstract_sub t (mk_fresh_free t)
+ | abstract_term (t as Abs _) = abstract_sub t (mk_fresh_free t)
+ | abstract_term t = pair t
+
+fun abstract_bin abs f t t1 t2 = abstract_sub t (abs t1 ##>> abs t2 #>> f)
+
+fun abstract_ter abs f t t1 t2 t3 =
+ abstract_sub t (abs t1 ##>> abs t2 ##>> abs t3 #>> (Scan.triple1 #> f))
+
+fun abstract_lit (@{const HOL.Not} $ t) = abstract_term t #>> HOLogic.mk_not
+ | abstract_lit t = abstract_term t
+
+fun abstract_not abs (t as @{const HOL.Not} $ t1) =
+ abstract_sub t (abs t1 #>> HOLogic.mk_not)
+ | abstract_not _ t = abstract_lit t
+
+fun abstract_conj (t as @{const HOL.conj} $ t1 $ t2) =
+ abstract_bin abstract_conj HOLogic.mk_conj t t1 t2
+ | abstract_conj t = abstract_lit t
+
+fun abstract_disj (t as @{const HOL.disj} $ t1 $ t2) =
+ abstract_bin abstract_disj HOLogic.mk_disj t t1 t2
+ | abstract_disj t = abstract_lit t
+
+fun abstract_prop (t as (c as @{const If (bool)}) $ t1 $ t2 $ t3) =
+ abstract_ter abstract_prop (fn (t1, t2, t3) => c $ t1 $ t2 $ t3) t t1 t2 t3
+ | abstract_prop (t as @{const HOL.disj} $ t1 $ t2) =
+ abstract_bin abstract_prop HOLogic.mk_disj t t1 t2
+ | abstract_prop (t as @{const HOL.conj} $ t1 $ t2) =
+ abstract_bin abstract_prop HOLogic.mk_conj t t1 t2
+ | abstract_prop (t as @{const HOL.implies} $ t1 $ t2) =
+ abstract_bin abstract_prop HOLogic.mk_imp t t1 t2
+ | abstract_prop (t as @{term "HOL.eq :: bool => _"} $ t1 $ t2) =
+ abstract_bin abstract_prop HOLogic.mk_eq t t1 t2
+ | abstract_prop t = abstract_not abstract_prop t
+
+fun abstract_arith ctxt u =
+ let
+ fun abs (t as (c as Const (\<^const_name>\<open>Hilbert_Choice.Eps\<close>, _) $ Abs (s, T, t'))) =
+ abstract_sub t (abstract_term t)
+ | abs (t as (c as Const _) $ Abs (s, T, t')) =
+ abstract_sub t (abs t' #>> (fn u' => c $ Abs (s, T, u')))
+ | abs (t as (c as Const (@{const_name If}, _)) $ t1 $ t2 $ t3) =
+ abstract_ter abs (fn (t1, t2, t3) => c $ t1 $ t2 $ t3) t t1 t2 t3
+ | abs (t as @{const HOL.Not} $ t1) = abstract_sub t (abs t1 #>> HOLogic.mk_not)
+ | abs (t as @{const HOL.disj} $ t1 $ t2) =
+ abstract_sub t (abs t1 ##>> abs t2 #>> HOLogic.mk_disj)
+ | abs (t as (c as Const (@{const_name uminus_class.uminus}, _)) $ t1) =
+ abstract_sub t (abs t1 #>> (fn u => c $ u))
+ | abs (t as (c as Const (@{const_name plus_class.plus}, _)) $ t1 $ t2) =
+ abstract_sub t (abs t1 ##>> abs t2 #>> (fn (u1, u2) => c $ u1 $ u2))
+ | abs (t as (c as Const (@{const_name minus_class.minus}, _)) $ t1 $ t2) =
+ abstract_sub t (abs t1 ##>> abs t2 #>> (fn (u1, u2) => c $ u1 $ u2))
+ | abs (t as (c as Const (@{const_name times_class.times}, _)) $ t1 $ t2) =
+ abstract_sub t (abs t1 ##>> abs t2 #>> (fn (u1, u2) => c $ u1 $ u2))
+ | abs (t as (c as Const (@{const_name z3div}, _)) $ t1 $ t2) =
+ abstract_sub t (abs t1 ##>> abs t2 #>> (fn (u1, u2) => c $ u1 $ u2))
+ | abs (t as (c as Const (@{const_name z3mod}, _)) $ t1 $ t2) =
+ abstract_sub t (abs t1 ##>> abs t2 #>> (fn (u1, u2) => c $ u1 $ u2))
+ | abs (t as (c as Const (@{const_name HOL.eq}, _)) $ t1 $ t2) =
+ abstract_sub t (abs t1 ##>> abs t2 #>> (fn (u1, u2) => c $ u1 $ u2))
+ | abs (t as (c as Const (@{const_name ord_class.less}, _)) $ t1 $ t2) =
+ abstract_sub t (abs t1 ##>> abs t2 #>> (fn (u1, u2) => c $ u1 $ u2))
+ | abs (t as (c as Const (@{const_name ord_class.less_eq}, _)) $ t1 $ t2) =
+ abstract_sub t (abs t1 ##>> abs t2 #>> (fn (u1, u2) => c $ u1 $ u2))
+ | abs t = abstract_sub t (fn cx =>
+ if can HOLogic.dest_number t then (t, cx)
+ else
+ (case apply_abstracters abs (get_arith_abstracters ctxt) t cx of
+ (SOME u, cx') => (u, cx')
+ | (NONE, _) => abstract_term t cx))
+ in abs u end
+
+fun abstract_unit (t as (@{const HOL.Not} $ (@{const HOL.disj} $ t1 $ t2))) =
+ abstract_sub t (abstract_unit t1 ##>> abstract_unit t2 #>>
+ HOLogic.mk_not o HOLogic.mk_disj)
+ | abstract_unit (t as (@{const HOL.disj} $ t1 $ t2)) =
+ abstract_sub t (abstract_unit t1 ##>> abstract_unit t2 #>>
+ HOLogic.mk_disj)
+ | abstract_unit (t as (Const(@{const_name HOL.eq}, _) $ t1 $ t2)) =
+ if fastype_of t1 = @{typ bool} then
+ abstract_sub t (abstract_unit t1 ##>> abstract_unit t2 #>>
+ HOLogic.mk_eq)
+ else abstract_lit t
+ | abstract_unit (t as (@{const HOL.Not} $ Const(@{const_name HOL.eq}, _) $ t1 $ t2)) =
+ if fastype_of t1 = @{typ bool} then
+ abstract_sub t (abstract_unit t1 ##>> abstract_unit t2 #>>
+ HOLogic.mk_eq #>> HOLogic.mk_not)
+ else abstract_lit t
+ | abstract_unit (t as (@{const HOL.Not} $ t1)) =
+ abstract_sub t (abstract_unit t1 #>> HOLogic.mk_not)
+ | abstract_unit t = abstract_lit t
+
+
+(* theory lemmas *)
+
+fun try_provers ctxt rule [] thms t = replay_rule_error ctxt rule thms t
+ | try_provers ctxt rule ((name, prover) :: named_provers) thms t =
+ (case (trace ctxt (K ("Trying prover " ^ quote name)); try prover t) of
+ SOME thm => thm
+ | NONE => try_provers ctxt rule named_provers thms t)
+
+
+(* congruence *)
+
+fun certify_prop ctxt t = Thm.cterm_of ctxt (as_prop t)
+
+fun ctac ctxt prems i st = st |> (
+ resolve_tac ctxt (@{thm refl} :: prems) i
+ ORELSE (cong_tac ctxt i THEN ctac ctxt prems (i + 1) THEN ctac ctxt prems i))
+
+fun cong_basic ctxt thms t =
+ let val st = Thm.trivial (certify_prop ctxt t)
+ in
+ (case Seq.pull (ctac ctxt thms 1 st) of
+ SOME (thm, _) => thm
+ | NONE => raise THM ("cong", 0, thms @ [st]))
+ end
+
+val cong_dest_rules = @{lemma
+ "(\<not> P \<or> Q) \<and> (P \<or> \<not> Q) \<Longrightarrow> P = Q"
+ "(P \<or> \<not> Q) \<and> (\<not> P \<or> Q) \<Longrightarrow> P = Q"
+ by fast+}
+
+fun cong_full_core_tac ctxt =
+ eresolve_tac ctxt @{thms subst}
+ THEN' resolve_tac ctxt @{thms refl}
+ ORELSE' Classical.fast_tac ctxt
+
+fun cong_full ctxt thms t = prove ctxt t (fn ctxt' =>
+ Method.insert_tac ctxt thms
+ THEN' (cong_full_core_tac ctxt'
+ ORELSE' dresolve_tac ctxt cong_dest_rules
+ THEN' cong_full_core_tac ctxt'))
+
+fun cong_unfolding_first ctxt thms t =
+ let val reorder_for_simp = try (fn thm =>
+ let val t = Thm.prop_of ( @{thm eq_reflection} OF [thm])
+ val thm = (case Logic.dest_equals t of
+ (t1, t2) => if Term.size_of_term t1 > Term.size_of_term t2 then @{thm eq_reflection} OF [thm]
+ else @{thm eq_reflection} OF [thm OF @{thms sym}])
+ handle TERM("dest_equals", _) => @{thm eq_reflection} OF [thm]
+ in thm end)
+ in
+ prove ctxt t (fn ctxt =>
+ Raw_Simplifier.rewrite_goal_tac ctxt
+ (map_filter reorder_for_simp thms)
+ THEN' Method.insert_tac ctxt thms
+ THEN' K (Clasimp.auto_tac ctxt))
+ end
+
+end;
--- a/src/HOL/Tools/SMT/smt_solver.ML Tue Oct 30 22:08:36 2018 +0100
+++ b/src/HOL/Tools/SMT/smt_solver.ML Tue Oct 30 22:59:06 2018 +0100
@@ -90,12 +90,14 @@
val _ = SMT_Config.trace_msg ctxt (pretty "Problem:" o split_lines) input
- val {redirected_output = res, output = err, return_code} =
- SMT_Config.with_timeout ctxt (run ctxt name mk_cmd) input
+ val ({elapsed, ...}, {redirected_output = res, output = err, return_code}) =
+ Timing.timing (SMT_Config.with_timeout ctxt (run ctxt name mk_cmd)) input
val _ = SMT_Config.trace_msg ctxt (pretty "Solver:") err
val output = drop_suffix (equal "") res
val _ = SMT_Config.trace_msg ctxt (pretty "Result:") output
+ val _ = SMT_Config.trace_msg ctxt (pretty "Time (ms):") [@{make_string} (Time.toMilliseconds elapsed)]
+ val _ = SMT_Config.statistics_msg ctxt (pretty "Time (ms):") [@{make_string} (Time.toMilliseconds elapsed)]
val _ = member (op =) normal_return_codes return_code orelse
raise SMT_Failure.SMT (SMT_Failure.Abnormal_Termination return_code)
--- a/src/HOL/Tools/SMT/smt_systems.ML Tue Oct 30 22:08:36 2018 +0100
+++ b/src/HOL/Tools/SMT/smt_systems.ML Tue Oct 30 22:59:06 2018 +0100
@@ -119,7 +119,7 @@
avail = make_avail "VERIT",
command = make_command "VERIT",
options = (fn ctxt => [
- "--proof-version=1",
+ "--proof-version=2",
"--proof-prune",
"--proof-merge",
"--disable-print-success",
@@ -129,7 +129,7 @@
default_max_relevant = 200 (* FUDGE *),
outcome = on_first_non_unsupported_line (outcome_of "unsat" "sat" "unknown"),
parse_proof = SOME (K VeriT_Proof_Parse.parse_proof),
- replay = NONE }
+ replay = SOME Verit_Replay.replay }
end
--- a/src/HOL/Tools/SMT/smtlib_proof.ML Tue Oct 30 22:08:36 2018 +0100
+++ b/src/HOL/Tools/SMT/smtlib_proof.ML Tue Oct 30 22:59:06 2018 +0100
@@ -265,10 +265,13 @@
fun dest_binding (SMTLIB.S [SMTLIB.Sym name, t]) = (name, Tree t)
| dest_binding b = raise SMTLIB_PARSE ("bad SMT let binding format", b)
+fun mk_choice (x, T, P) = HOLogic.choice_const T $ absfree (x, T) P
+
fun term_of t cx =
(case t of
SMTLIB.S [SMTLIB.Sym "forall", SMTLIB.S vars, body] => quant HOLogic.mk_all vars body cx
| SMTLIB.S [SMTLIB.Sym "exists", SMTLIB.S vars, body] => quant HOLogic.mk_exists vars body cx
+ | SMTLIB.S [SMTLIB.Sym "choice", SMTLIB.S vars, body] => quant mk_choice vars body cx
| SMTLIB.S [SMTLIB.Sym "let", SMTLIB.S bindings, body] =>
with_bindings (map dest_binding bindings) (term_of body) cx
| SMTLIB.S (SMTLIB.Sym "!" :: t :: _) => term_of t cx
--- a/src/HOL/Tools/SMT/verit_proof.ML Tue Oct 30 22:08:36 2018 +0100
+++ b/src/HOL/Tools/SMT/verit_proof.ML Tue Oct 30 22:59:06 2018 +0100
@@ -12,20 +12,36 @@
id: string,
rule: string,
prems: string list,
+ proof_ctxt: term list,
concl: term,
fixes: string list}
+ datatype veriT_replay_node = VeriT_Replay_Node of {
+ id: string,
+ rule: string,
+ args: term list,
+ prems: string list,
+ proof_ctxt: term list,
+ concl: term,
+ bounds: (string * typ) list,
+ subproof: (string * typ) list * term list * veriT_replay_node list}
+
(*proof parser*)
val parse: typ Symtab.table -> term Symtab.table -> string list ->
Proof.context -> veriT_step list * Proof.context
+ val parse_replay: typ Symtab.table -> term Symtab.table -> string list ->
+ Proof.context -> veriT_replay_node list * Proof.context
+ val map_replay_prems: (string list -> string list) -> veriT_replay_node -> veriT_replay_node
val veriT_step_prefix : string
val veriT_input_rule: string
+ val veriT_normalized_input_rule: string
val veriT_la_generic_rule : string
val veriT_rewrite_rule : string
val veriT_simp_arith_rule : string
- val veriT_tmp_ite_elim_rule : string
val veriT_tmp_skolemize_rule : string
+ val veriT_subproof_rule : string
+ val veriT_local_input_rule : string
end;
structure VeriT_Proof: VERIT_PROOF =
@@ -33,33 +49,66 @@
open SMTLIB_Proof
+datatype raw_veriT_node = Raw_VeriT_Node of {
+ id: string,
+ rule: string,
+ args: SMTLIB.tree,
+ prems: string list,
+ concl: SMTLIB.tree,
+ subproof: raw_veriT_node list}
+
+fun mk_raw_node id rule args prems concl subproof =
+ Raw_VeriT_Node {id = id, rule = rule, args = args, prems = prems, concl = concl,
+ subproof = subproof}
+
datatype veriT_node = VeriT_Node of {
id: string,
rule: string,
prems: string list,
+ proof_ctxt: term list,
concl: term,
bounds: string list}
-fun mk_node id rule prems concl bounds =
- VeriT_Node {id = id, rule = rule, prems = prems, concl = concl, bounds = bounds}
+fun mk_node id rule prems proof_ctxt concl bounds =
+ VeriT_Node {id = id, rule = rule, prems = prems, proof_ctxt = proof_ctxt, concl = concl,
+ bounds = bounds}
+
+datatype veriT_replay_node = VeriT_Replay_Node of {
+ id: string,
+ rule: string,
+ args: term list,
+ prems: string list,
+ proof_ctxt: term list,
+ concl: term,
+ bounds: (string * typ) list,
+ subproof: (string * typ) list * term list * veriT_replay_node list}
+
+fun mk_replay_node id rule args prems proof_ctxt concl bounds subproof =
+ VeriT_Replay_Node {id = id, rule = rule, args = args, prems = prems, proof_ctxt = proof_ctxt,
+ concl = concl, bounds = bounds, subproof = subproof}
datatype veriT_step = VeriT_Step of {
id: string,
rule: string,
prems: string list,
+ proof_ctxt: term list,
concl: term,
fixes: string list}
-fun mk_step id rule prems concl fixes =
- VeriT_Step {id = id, rule = rule, prems = prems, concl = concl, fixes = fixes}
+fun mk_step id rule prems proof_ctxt concl fixes =
+ VeriT_Step {id = id, rule = rule, prems = prems, proof_ctxt = proof_ctxt, concl = concl,
+ fixes = fixes}
val veriT_step_prefix = ".c"
val veriT_input_rule = "input"
val veriT_la_generic_rule = "la_generic"
+val veriT_normalized_input_rule = "__normalized_input" (* arbitrary *)
val veriT_rewrite_rule = "__rewrite" (* arbitrary *)
+val veriT_subproof_rule = "subproof"
+val veriT_local_input_rule = "__local_input" (* arbitrary *)
val veriT_simp_arith_rule = "simp_arith"
-val veriT_tmp_alphaconv_rule = "tmp_alphaconv"
-val veriT_tmp_ite_elim_rule = "tmp_ite_elim"
+
+(* Even the veriT developer do not know if the following rule can still appear in proofs: *)
val veriT_tmp_skolemize_rule = "tmp_skolemize"
(* proof parser *)
@@ -69,131 +118,229 @@
||>> `(with_fresh_names (term_of p))
|>> snd
-(*in order to get Z3-style quantification*)
-fun repair_quantification (SMTLIB.S (SMTLIB.Sym "forall" :: l)) =
- let val (quantified_vars, t) = split_last (map repair_quantification l)
- in
- SMTLIB.S (SMTLIB.Sym "forall" :: SMTLIB.S quantified_vars :: t :: [])
- end
- | repair_quantification (SMTLIB.S (SMTLIB.Sym "exists" :: l)) =
- let val (quantified_vars, t) = split_last (map repair_quantification l)
- in
- SMTLIB.S (SMTLIB.Sym "exists" :: SMTLIB.S quantified_vars :: t :: [])
- end
- | repair_quantification (SMTLIB.S l) = SMTLIB.S (map repair_quantification l)
- | repair_quantification x = x
-
-fun replace_bound_var_by_free_var (q $ Abs (var, ty, u)) free_var =
- (case List.find (fn v => String.isPrefix v var) free_var of
- NONE => q $ Abs (var, ty, replace_bound_var_by_free_var u free_var)
- | SOME _ => replace_bound_var_by_free_var (Term.subst_bound (Free (var, ty), u)) free_var)
- | replace_bound_var_by_free_var (u $ v) free_vars = replace_bound_var_by_free_var u free_vars $
- replace_bound_var_by_free_var v free_vars
- | replace_bound_var_by_free_var u _ = u
-
fun find_type_in_formula (Abs (v, T, u)) var_name =
if String.isPrefix var_name v then SOME T else find_type_in_formula u var_name
| find_type_in_formula (u $ v) var_name =
(case find_type_in_formula u var_name of
NONE => find_type_in_formula v var_name
| some_T => some_T)
+ | find_type_in_formula (Free(v, T)) var_name =
+ if String.isPrefix var_name v then SOME T else NONE
| find_type_in_formula _ _ = NONE
+fun find_type_of_free_in_formula (Free (v, T) $ u) var_name =
+ if String.isPrefix var_name v then SOME T else find_type_in_formula u var_name
+ | find_type_of_free_in_formula (Abs (v, T, u)) var_name =
+ if String.isPrefix var_name v then SOME T else find_type_in_formula u var_name
+ | find_type_of_free_in_formula (u $ v) var_name =
+ (case find_type_in_formula u var_name of
+ NONE => find_type_in_formula v var_name
+ | some_T => some_T)
+ | find_type_of_free_in_formula _ _ = NONE
+
fun add_bound_variables_to_ctxt concl =
fold (update_binding o
(fn s => (s, Term (Free (s, the_default dummyT (find_type_in_formula concl s))))))
-fun update_step_and_cx (node as VeriT_Node {id, rule, prems, concl, bounds}) cx =
- if rule = veriT_tmp_ite_elim_rule then
- (mk_node id rule prems concl bounds, add_bound_variables_to_ctxt concl bounds cx)
- else if rule = veriT_tmp_skolemize_rule then
- let val concl' = replace_bound_var_by_free_var concl bounds in
- (mk_node id rule prems concl' [], add_bound_variables_to_ctxt concl bounds cx)
- end
- else
- (node, cx)
+
+local
+
+ fun remove_Sym (SMTLIB.Sym y) = y
+
+ fun extract_symbols bds =
+ bds
+ |> map (fn SMTLIB.S [SMTLIB.Key _, SMTLIB.Sym x, SMTLIB.Sym y] => [x, y]
+ | SMTLIB.S syms => map remove_Sym syms)
+ |> flat
+
+ fun extract_symbols_map bds =
+ bds
+ |> map (fn SMTLIB.S [SMTLIB.Key _, SMTLIB.Sym x, _] => [x]
+ | SMTLIB.S syms => map remove_Sym syms)
+ |> flat
+in
-fun fix_subproof_steps ((((id_of_father_step, rule), prems), subproof), ((step_concl, bounds),
- cx)) =
+fun bound_vars_by_rule "bind" (SMTLIB.S bds) = extract_symbols bds
+ | bound_vars_by_rule "qnt_simplify" (SMTLIB.S bds) = extract_symbols_map bds
+ | bound_vars_by_rule "sko_forall" (SMTLIB.S bds) = extract_symbols_map bds
+ | bound_vars_by_rule "sko_ex" (SMTLIB.S bds) = extract_symbols_map bds
+ | bound_vars_by_rule _ _ = []
+
+fun global_bound_vars_by_rule _ _ = []
+
+(* VeriT adds "?" before some variable. *)
+fun remove_all_qm (SMTLIB.Sym v :: l) =
+ SMTLIB.Sym (perhaps (try (unprefix "?")) v) :: remove_all_qm l
+ | remove_all_qm (SMTLIB.S l :: l') = SMTLIB.S (remove_all_qm l) :: remove_all_qm l'
+ | remove_all_qm (SMTLIB.Key v :: l) = SMTLIB.Key v :: remove_all_qm l
+ | remove_all_qm (v :: l) = v :: remove_all_qm l
+ | remove_all_qm [] = []
+
+fun remove_all_qm2 (SMTLIB.Sym v) = SMTLIB.Sym (perhaps (try (unprefix "?")) v)
+ | remove_all_qm2 (SMTLIB.S l) = SMTLIB.S (remove_all_qm l)
+ | remove_all_qm2 (SMTLIB.Key v) = SMTLIB.Key v
+ | remove_all_qm2 v = v
+
+val parse_rule_and_args =
let
- fun mk_prop_of_term concl =
- concl |> fastype_of concl = @{typ bool} ? curry (op $) @{term Trueprop}
- fun update_prems assumption_id prems =
- map (fn prem => id_of_father_step ^ prem)
- (filter_out (curry (op =) assumption_id) prems)
- fun inline_assumption assumption assumption_id
- (VeriT_Node {id, rule, prems, concl, bounds}) =
- mk_node id rule (update_prems assumption_id prems)
- (@{const Pure.imp} $ mk_prop_of_term assumption $ mk_prop_of_term concl) bounds
- fun find_input_steps_and_inline [] last_step = ([], last_step)
- | find_input_steps_and_inline (VeriT_Node {id = id', rule, prems, concl, bounds} :: steps)
- last_step =
- if rule = veriT_input_rule then
- find_input_steps_and_inline (map (inline_assumption concl id') steps) last_step
- else
- apfst (cons (mk_node (id_of_father_step ^ id') rule prems concl bounds))
- (find_input_steps_and_inline steps (id_of_father_step ^ id'))
- val (subproof', last_step_id) = find_input_steps_and_inline subproof ""
- val prems' =
- if last_step_id = "" then
- prems
- else
- (case prems of
- NONE => SOME [last_step_id]
- | SOME l => SOME (last_step_id :: l))
+ fun parse_rule_name (SMTLIB.Sym rule :: l) = (rule, l)
+ | parse_rule_name l = (veriT_subproof_rule, l)
+ fun parse_args (SMTLIB.Key "args" :: args :: l) = (remove_all_qm2 args, l)
+ | parse_args l = (SMTLIB.S [], l)
in
- (subproof', (((((id_of_father_step, rule), prems'), step_concl), bounds), cx))
+ parse_rule_name
+ ##> parse_args
end
-(*
-(set id rule :clauses(...) :args(..) :conclusion (...)).
-or
-(set id subproof (set ...) :conclusion (...)).
-*)
+end
-fun parse_proof_step cx =
+fun parse_raw_proof_step (p : SMTLIB.tree) : raw_veriT_node =
let
fun rotate_pair (a, (b, c)) = ((a, b), c)
fun get_id (SMTLIB.S [SMTLIB.Sym "set", SMTLIB.Sym id, SMTLIB.S l]) = (id, l)
| get_id t = raise Fail ("unrecognized VeriT proof " ^ @{make_string} t)
- fun parse_rule (SMTLIB.Sym rule :: l) = (rule, l)
fun parse_source (SMTLIB.Key "clauses" :: SMTLIB.S source ::l) =
(SOME (map (fn (SMTLIB.Sym id) => id) source), l)
| parse_source l = (NONE, l)
- fun parse_subproof cx id_of_father_step ((subproof_step as SMTLIB.S (SMTLIB.Sym "set" :: _)) :: l) =
- let val (subproof_steps, cx') = parse_proof_step cx subproof_step in
- apfst (apfst (curry (op @) subproof_steps)) (parse_subproof cx' id_of_father_step l)
+ fun parse_subproof rule args id_of_father_step ((subproof_step as SMTLIB.S (SMTLIB.Sym "set" :: _)) :: l) =
+ let
+ val subproof_steps = parse_raw_proof_step subproof_step
+ in
+ apfst (curry (op ::) subproof_steps) (parse_subproof rule args id_of_father_step l)
end
- | parse_subproof cx _ l = (([], cx), l)
- fun skip_args (SMTLIB.Key "args" :: SMTLIB.S _ :: l) = l
- | skip_args l = l
- fun parse_conclusion (SMTLIB.Key "conclusion" :: SMTLIB.S concl :: []) = concl
- fun make_or_from_clausification l =
- foldl1 (fn ((concl1, bounds1), (concl2, bounds2)) =>
- (HOLogic.mk_disj (perhaps (try HOLogic.dest_Trueprop) concl1,
- perhaps (try HOLogic.dest_Trueprop) concl2), bounds1 @ bounds2)) l
- fun to_node (((((id, rule), prems), concl), bounds), cx) =
- (mk_node id rule (the_default [] prems) concl bounds, cx)
+ | parse_subproof _ _ _ l = ([], l)
+
+ fun parse_and_clausify_conclusion (SMTLIB.Key "conclusion" :: SMTLIB.S [] :: []) =
+ SMTLIB.Sym "false"
+ | parse_and_clausify_conclusion (SMTLIB.Key "conclusion" :: SMTLIB.S concl :: []) =
+ (SMTLIB.S (remove_all_qm (SMTLIB.Sym "or" :: concl)))
+
+ fun to_raw_node ((((((id, rule), args), prems), subproof), concl)) =
+ (mk_raw_node id rule args (the_default [] prems) concl subproof)
in
- get_id
- ##> parse_rule
+ (get_id
+ ##> parse_rule_and_args
+ #> rotate_pair
#> rotate_pair
##> parse_source
#> rotate_pair
- ##> skip_args
- #> (fn (((id, rule), prems), sub) => (((id, rule), prems), parse_subproof cx id sub))
+ #> (fn ((((id, rule), args), prems), sub) =>
+ ((((id, rule), args), prems), parse_subproof rule args id sub))
#> rotate_pair
- ##> parse_conclusion
- ##> map repair_quantification
- #> (fn ((((id, rule), prems), (subproof, cx)), terms) =>
- (((((id, rule), prems), subproof), fold_map (fn t => fn cx => node_of t cx) terms cx)))
- ##> apfst (fn [] => (@{const False}, []) | concls => make_or_from_clausification concls)
- #> fix_subproof_steps
- ##> to_node
- #> (fn (subproof, (step, cx)) => (subproof @ [step], cx))
- #-> fold_map update_step_and_cx
+ ##> parse_and_clausify_conclusion
+ #> to_raw_node)
+ p
+ end
+
+fun proof_ctxt_of_rule "bind" t = t
+ | proof_ctxt_of_rule "sko_forall" t = t
+ | proof_ctxt_of_rule "sko_ex" t = t
+ | proof_ctxt_of_rule "let" t = t
+ | proof_ctxt_of_rule "qnt_simplify" t = t
+ | proof_ctxt_of_rule _ _ = []
+
+fun args_of_rule "forall_inst" t = t
+ | args_of_rule _ _ = []
+
+fun map_replay_prems f (VeriT_Replay_Node {id, rule, args, prems, proof_ctxt, concl, bounds,
+ subproof = (bound, assms, subproof)}) =
+ (VeriT_Replay_Node {id = id, rule = rule, args = args, prems = f prems, proof_ctxt = proof_ctxt,
+ concl = concl, bounds = bounds, subproof = (bound, assms, map (map_replay_prems f) subproof)})
+
+fun map_replay_id f (VeriT_Replay_Node {id, rule, args, prems, proof_ctxt, concl, bounds,
+ subproof = (bound, assms, subproof)}) =
+ (VeriT_Replay_Node {id = f id, rule = rule, args = args, prems = prems, proof_ctxt = proof_ctxt,
+ concl = concl, bounds = bounds, subproof = (bound, assms, map (map_replay_id f) subproof)})
+
+fun id_of_last_step prems =
+ if null prems then []
+ else
+ let val VeriT_Replay_Node {id, ...} = List.last prems in [id] end
+
+val extract_assumptions_from_subproof =
+ let fun extract_assumptions_from_subproof (VeriT_Replay_Node {rule, concl, ...}) =
+ if rule = veriT_local_input_rule then [concl] else []
+ in
+ map extract_assumptions_from_subproof
+ #> flat
end
+fun normalized_rule_name id rule =
+ (case (rule = veriT_input_rule, can (unprefix SMTLIB_Interface.assert_prefix) id) of
+ (true, true) => veriT_normalized_input_rule
+ | (true, _) => veriT_local_input_rule
+ | _ => rule)
+
+fun is_assm_repetition id rule =
+ rule = veriT_input_rule andalso can (unprefix SMTLIB_Interface.assert_prefix) id
+
+fun postprocess_proof ctxt step =
+ let fun postprocess (Raw_VeriT_Node {id = id, rule = rule, args = args,
+ prems = prems, concl = concl, subproof = subproof}) cx =
+ let
+ val ((concl, bounds), cx') = node_of concl cx
+
+ val bound_vars = bound_vars_by_rule rule args
+
+ (* postprocess conclusion *)
+ val new_global_bounds = global_bound_vars_by_rule rule args
+ val concl = SMTLIB_Isar.unskolemize_names ctxt concl
+
+ val _ = (SMT_Config.veriT_msg ctxt) (fn () => @{print} ("id =", id, "concl =", concl))
+ val _ = (SMT_Config.veriT_msg ctxt) (fn () => @{print} ("id =", id, "cx' =", cx',
+ "bound_vars =", bound_vars))
+ val bound_vars = filter_out (member ((op =)) new_global_bounds) bound_vars
+ val bound_tvars =
+ map (fn s => (s, the (find_type_in_formula concl s))) bound_vars
+ val subproof_cx = add_bound_variables_to_ctxt concl bound_vars cx
+ val (p : veriT_replay_node list list, _) =
+ fold_map postprocess subproof subproof_cx
+
+ (* postprocess assms *)
+ val SMTLIB.S stripped_args = args
+ val sanitized_args =
+ proof_ctxt_of_rule rule stripped_args
+ |> map
+ (fn SMTLIB.S [SMTLIB.Key "=", x, y] => SMTLIB.S [SMTLIB.Sym "=", x, y]
+ | SMTLIB.S syms =>
+ SMTLIB.S (SMTLIB.Sym "and" :: map (fn x => SMTLIB.S [SMTLIB.Sym "=", x, x]) syms)
+ | x => x)
+ val (termified_args, _) = fold_map node_of sanitized_args subproof_cx |> apfst (map fst)
+ val normalized_args = map (SMTLIB_Isar.unskolemize_names ctxt) termified_args
+
+ val subproof_assms = proof_ctxt_of_rule rule normalized_args
+
+ (* postprocess arguments *)
+ val rule_args = args_of_rule rule stripped_args
+ val (termified_args, _) = fold_map term_of rule_args subproof_cx
+ val normalized_args = map (SMTLIB_Isar.unskolemize_names ctxt) termified_args
+ val rule_args = normalized_args
+
+ (* fix subproof *)
+ val p = flat p
+ val p = map (map_replay_prems (map (curry (op ^) id))) p
+ val p = map (map_replay_id (curry (op ^) id)) p
+
+ val extra_assms2 =
+ (if rule = veriT_subproof_rule then extract_assumptions_from_subproof p else [])
+
+ (* fix step *)
+ val bound_t =
+ bounds
+ |> map (fn s => (s, the_default dummyT (find_type_of_free_in_formula concl s)))
+ val fixed_prems =
+ (if null subproof then prems else map (curry (op ^) id) prems) @
+ (if is_assm_repetition id rule then [id] else []) @
+ id_of_last_step p
+ val normalized_rule = normalized_rule_name id rule
+ val step = mk_replay_node id normalized_rule rule_args fixed_prems subproof_assms concl
+ bound_t (bound_tvars, subproof_assms @ extra_assms2, p)
+ in
+ ([step], cx')
+ end
+ in postprocess step end
+
+
(*subproofs are written on multiple lines: SMTLIB can not parse then, because parentheses are
unbalanced on each line*)
fun seperate_into_steps lines =
@@ -214,111 +361,72 @@
seperate lines "" 0
end
+fun unprefix_all_syms c (SMTLIB.Sym v :: l) =
+ SMTLIB.Sym (perhaps (try (unprefix c)) v) :: unprefix_all_syms c l
+ | unprefix_all_syms c (SMTLIB.S l :: l') = SMTLIB.S (unprefix_all_syms c l) :: unprefix_all_syms c l'
+ | unprefix_all_syms c (SMTLIB.Key v :: l) = SMTLIB.Key v :: unprefix_all_syms c l
+ | unprefix_all_syms c (v :: l) = v :: unprefix_all_syms c l
+ | unprefix_all_syms _ [] = []
+
(* VeriT adds "@" before every variable. *)
-fun remove_all_at (SMTLIB.Sym v :: l) =
- SMTLIB.Sym (perhaps (try (unprefix "@")) v) :: remove_all_at l
- | remove_all_at (SMTLIB.S l :: l') = SMTLIB.S (remove_all_at l) :: remove_all_at l'
- | remove_all_at (SMTLIB.Key v :: l) = SMTLIB.Key v :: remove_all_at l
- | remove_all_at (v :: l) = v :: remove_all_at l
- | remove_all_at [] = []
+val remove_all_ats = unprefix_all_syms "@"
-fun find_in_which_step_defined var (VeriT_Node {id, bounds, ...} :: l) =
- (case List.find (fn v => String.isPrefix v var) bounds of
- NONE => find_in_which_step_defined var l
- | SOME _ => id)
- | find_in_which_step_defined var _ = raise Fail ("undefined " ^ var)
+val linearize_proof =
+ let
+ fun linearize (VeriT_Replay_Node {id = id, rule = rule, args = _, prems = prems,
+ proof_ctxt = proof_ctxt, concl = concl, bounds = bounds, subproof = (_, _, subproof)}) =
+ let
+ fun mk_prop_of_term concl =
+ concl |> fastype_of concl = @{typ bool} ? curry (op $) @{term Trueprop}
+ fun remove_assumption_id assumption_id prems =
+ filter_out (curry (op =) assumption_id) prems
+ fun inline_assumption assumption assumption_id
+ (VeriT_Node {id, rule, prems, proof_ctxt, concl, bounds}) =
+ mk_node id rule (remove_assumption_id assumption_id prems) proof_ctxt
+ (@{const Pure.imp} $ mk_prop_of_term assumption $ mk_prop_of_term concl) bounds
+ fun find_input_steps_and_inline [] = []
+ | find_input_steps_and_inline
+ (VeriT_Node {id = id', rule, prems, concl, bounds, ...} :: steps) =
+ if rule = veriT_input_rule then
+ find_input_steps_and_inline (map (inline_assumption concl id') steps)
+ else
+ mk_node (id') rule prems [] concl bounds :: find_input_steps_and_inline steps
-(*Yes every case is possible: the introduced var is not on a special size of the equality sign.*)
-fun find_ite_var_in_term (Const (@{const_name If}, _) $ _ $
- (Const (@{const_name HOL.eq}, _) $ Free (var1, _) $ Free (var2, _) ) $
- (Const (@{const_name HOL.eq}, _) $ Free (var3, _) $ Free (var4, _) )) =
+ val subproof = flat (map linearize subproof)
+ val subproof' = find_input_steps_and_inline subproof
+ in
+ subproof' @ [mk_node id rule prems proof_ctxt concl (map fst bounds)]
+ end
+ in linearize end
+
+local
+ fun import_proof_and_post_process typs funs lines ctxt =
let
- fun get_number_of_ite_transformed_var var =
- perhaps (try (unprefix "ite")) var
- |> Int.fromString
- fun is_equal_and_has_correct_substring var var' var'' =
- if var = var' andalso String.isPrefix "ite" var then SOME var'
- else if var = var'' andalso String.isPrefix "ite" var then SOME var'' else NONE
- val var1_introduced_var = is_equal_and_has_correct_substring var1 var3 var4
- val var2_introduced_var = is_equal_and_has_correct_substring var3 var1 var2
- in
- (case (var1_introduced_var, var2_introduced_var) of
- (SOME a, SOME b) =>
- (*ill-generated case, might be possible when applying the rule to max a a. Only if the
- variable have been introduced before. Probably an impossible edge case*)
- (case (get_number_of_ite_transformed_var a, get_number_of_ite_transformed_var b) of
- (SOME a, SOME b) => if a < b then var2_introduced_var else var1_introduced_var
- (*Otherwise, it is a name clase between a parameter name and the introduced variable.
- Or the name convention has been changed.*)
- | (NONE, SOME _) => var2_introduced_var
- | (SOME _, NONE) => var2_introduced_var)
- | (_, SOME _) => var2_introduced_var
- | (SOME _, _) => var1_introduced_var)
- end
- | find_ite_var_in_term (Const (@{const_name If}, _) $ _ $
- (Const (@{const_name HOL.eq}, _) $ Free (var, _) $ _ ) $
- (Const (@{const_name HOL.eq}, _) $ Free (var', _) $ _ )) =
- if var = var' then SOME var else NONE
- | find_ite_var_in_term (Const (@{const_name If}, _) $ _ $
- (Const (@{const_name HOL.eq}, _) $ _ $ Free (var, _)) $
- (Const (@{const_name HOL.eq}, _) $ _ $ Free (var', _))) =
- if var = var' then SOME var else NONE
- | find_ite_var_in_term (p $ q) =
- (case find_ite_var_in_term p of
- NONE => find_ite_var_in_term q
- | x => x)
- | find_ite_var_in_term (Abs (_, _, body)) = find_ite_var_in_term body
- | find_ite_var_in_term _ = NONE
-
-fun correct_veriT_step steps (node as VeriT_Node {id, rule, prems, concl, bounds}) =
- if rule = veriT_tmp_ite_elim_rule then
- if bounds = [] then
- (*if the introduced var has already been defined, adding the definition as a dependency*)
- let
- val new_prems = prems
- |> (case find_ite_var_in_term concl of
- NONE => I
- | SOME var => cons (find_in_which_step_defined var steps))
- in
- VeriT_Node {id = id, rule = rule, prems = new_prems, concl = concl, bounds = bounds}
- end
- else
- (*some new variables are created*)
- let val concl' = replace_bound_var_by_free_var concl bounds in
- mk_node id rule prems concl' []
- end
- else
- node
-
-fun remove_alpha_conversion _ [] = []
- | remove_alpha_conversion replace_table (VeriT_Node {id, rule, prems, concl, bounds} :: steps) =
- let
- val correct_dependency = map (perhaps (Symtab.lookup replace_table))
- val find_predecessor = perhaps (Symtab.lookup replace_table)
- in
- if rule = veriT_tmp_alphaconv_rule then
- remove_alpha_conversion (Symtab.update (id, find_predecessor (hd prems))
- replace_table) steps
- else
- VeriT_Node {id = id, rule = rule, prems = correct_dependency prems,
- concl = concl, bounds = bounds} :: remove_alpha_conversion replace_table steps
- end
-
-fun correct_veriT_steps steps =
- steps
- |> map (correct_veriT_step steps)
- |> remove_alpha_conversion Symtab.empty
+ val smtlib_lines_without_at =
+ seperate_into_steps lines
+ |> map SMTLIB.parse
+ |> remove_all_ats
+ in apfst flat (fold_map (fn l => postprocess_proof ctxt (parse_raw_proof_step l))
+ smtlib_lines_without_at (empty_context ctxt typs funs)) end
+in
fun parse typs funs lines ctxt =
let
- val smtlib_lines_without_at = remove_all_at (map SMTLIB.parse (seperate_into_steps lines))
- val (u, env) = apfst flat (fold_map (fn l => fn cx => parse_proof_step cx l)
- smtlib_lines_without_at (empty_context ctxt typs funs))
- val t = correct_veriT_steps u
+ val (u, env) = import_proof_and_post_process typs funs lines ctxt
+ val t = flat (map linearize_proof u)
fun node_to_step (VeriT_Node {id, rule, prems, concl, bounds, ...}) =
- mk_step id rule prems concl bounds
+ mk_step id rule prems [] concl bounds
in
(map node_to_step t, ctxt_of env)
end
+fun parse_replay typs funs lines ctxt =
+ let
+ val (u, env) = import_proof_and_post_process typs funs lines ctxt
+ val _ = (SMT_Config.veriT_msg ctxt) (fn () => @{print} u)
+ in
+ (u, ctxt_of env)
+ end
+end
+
end;
--- a/src/HOL/Tools/SMT/verit_proof_parse.ML Tue Oct 30 22:08:36 2018 +0100
+++ b/src/HOL/Tools/SMT/verit_proof_parse.ML Tue Oct 30 22:59:06 2018 +0100
@@ -37,7 +37,7 @@
fun step_of_assume j (_, th) =
VeriT_Proof.VeriT_Step {id = SMTLIB_Interface.assert_name_of_index (id_of_index j),
- rule = veriT_input_rule, prems = [], concl = Thm.prop_of th, fixes = []}
+ rule = veriT_input_rule, prems = [], proof_ctxt = [], concl = Thm.prop_of th, fixes = []}
val (actual_steps, _) = VeriT_Proof.parse typs terms output ctxt
val used_assert_ids = fold add_used_asserts_in_step actual_steps []
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/SMT/verit_replay.ML Tue Oct 30 22:59:06 2018 +0100
@@ -0,0 +1,207 @@
+(* Title: HOL/Tools/SMT/verit_replay.ML
+ Author: Mathias Fleury, MPII
+
+VeriT proof parsing and replay.
+*)
+
+signature VERIT_REPLAY =
+sig
+ val replay: Proof.context -> SMT_Translate.replay_data -> string list -> thm
+end;
+
+structure Verit_Replay: VERIT_REPLAY =
+struct
+
+fun under_fixes f unchanged_prems (prems, nthms) names args (concl, ctxt) =
+ let
+ val thms1 = unchanged_prems @ map (SMT_Replay.varify ctxt) prems
+ val _ = SMT_Config.veriT_msg ctxt (fn () => @{print} ("names =", names))
+ val thms2 = map snd nthms
+ val _ = SMT_Config.veriT_msg ctxt (fn () => @{print} ("prems=", prems))
+ val _ = SMT_Config.veriT_msg ctxt (fn () => @{print} ("nthms=", nthms))
+ val _ = SMT_Config.veriT_msg ctxt (fn () => @{print} ("thms1=", thms1))
+ val _ = SMT_Config.veriT_msg ctxt (fn () => @{print} ("thms2=", thms2))
+ in (f ctxt (thms1 @ thms2) args concl) end
+
+
+(** Replaying **)
+
+fun replay_thm method_for rewrite_rules ll_defs ctxt assumed unchanged_prems prems nthms
+ concl_transformation global_transformation args
+ (VeriT_Proof.VeriT_Replay_Node {id, rule, concl, bounds, ...}) =
+ let
+ val _ = SMT_Config.veriT_msg ctxt (fn () => @{print} id)
+ val rewrite = let val thy = Proof_Context.theory_of (empty_simpset ctxt) in
+ Raw_Simplifier.rewrite_term thy rewrite_rules []
+ #> not (null ll_defs) ? SMTLIB_Isar.unlift_term ll_defs
+ end
+ val post = let val thy = Proof_Context.theory_of (empty_simpset ctxt) in
+ Raw_Simplifier.rewrite_term thy rewrite_rules []
+ #> Object_Logic.atomize_term ctxt
+ #> not (null ll_defs) ? SMTLIB_Isar.unlift_term ll_defs
+ #> SMTLIB_Isar.unskolemize_names ctxt
+ #> HOLogic.mk_Trueprop
+ end
+ val concl = concl
+ |> concl_transformation
+ |> global_transformation
+ |> post
+in
+ if rule = VeriT_Proof.veriT_input_rule then
+ (case Symtab.lookup assumed id of
+ SOME (_, thm) => thm)
+ else
+ under_fixes (method_for rule) unchanged_prems
+ (prems, nthms) (map fst bounds)
+ (map rewrite args) (concl, ctxt)
+end
+
+fun add_used_asserts_in_step (VeriT_Proof.VeriT_Replay_Node {prems,
+ subproof = (_, _, subproof), ...}) =
+ union (op =) (map_filter (try SMTLIB_Interface.assert_index_of_name) prems @
+ flat (map (fn x => add_used_asserts_in_step x []) subproof))
+
+fun remove_rewrite_rules_from_rules n =
+ (fn (step as VeriT_Proof.VeriT_Replay_Node {id, ...}) =>
+ (case try SMTLIB_Interface.assert_index_of_name id of
+ NONE => SOME step
+ | SOME a => if a < n then NONE else SOME step))
+
+fun replay_step rewrite_rules ll_defs assumed proof_prems
+ (step as VeriT_Proof.VeriT_Replay_Node {id, rule, prems, bounds, args,
+ subproof = (fixes, assms, subproof), concl, ...}) state =
+ let
+ val (proofs, stats, ctxt, concl_tranformation, global_transformation) = state
+ val (_, ctxt) = Variable.variant_fixes (map fst bounds) ctxt
+ |> (fn (names, ctxt) => (names,
+ fold Variable.declare_term [SMTLIB_Isar.unskolemize_names ctxt concl] ctxt))
+
+ val (names, sub_ctxt) = Variable.variant_fixes (map fst fixes) ctxt
+ ||> fold Variable.declare_term (map Free fixes)
+ val export_vars =
+ Term.subst_free (ListPair.zip (map Free fixes, map Free (ListPair.zip (names, map snd fixes))))
+ o concl_tranformation
+
+ val post = let val thy = Proof_Context.theory_of (empty_simpset ctxt) in
+ Raw_Simplifier.rewrite_term thy rewrite_rules []
+ #> Object_Logic.atomize_term ctxt
+ #> not (null ll_defs) ? SMTLIB_Isar.unlift_term ll_defs
+ #> SMTLIB_Isar.unskolemize_names ctxt
+ #> HOLogic.mk_Trueprop
+ end
+ val assms = map (export_vars o global_transformation o post) assms
+ val (proof_prems', sub_ctxt2) = Assumption.add_assumes (map (Thm.cterm_of sub_ctxt) assms)
+ sub_ctxt
+
+ val all_proof_prems = proof_prems @ proof_prems'
+ val (proofs', stats, _, _, sub_global_rew) =
+ fold (replay_step rewrite_rules ll_defs assumed all_proof_prems) subproof
+ (assumed, stats, sub_ctxt2, export_vars, global_transformation)
+ val export_thm = singleton (Proof_Context.export sub_ctxt2 ctxt)
+ val nthms = prems
+ |> map (apsnd export_thm o the o (Symtab.lookup (if null subproof then proofs else proofs')))
+ val proof_prems =
+ if Verit_Replay_Methods.veriT_step_requires_subproof_assms rule then proof_prems else []
+ val replay = Timing.timing (replay_thm Verit_Replay_Methods.method_for rewrite_rules ll_defs
+ ctxt assumed [] (proof_prems) nthms concl_tranformation global_transformation args)
+ val ({elapsed, ...}, thm) =
+ SMT_Config.with_time_limit ctxt SMT_Config.reconstruction_step_timeout replay step
+ handle Timeout.TIMEOUT _ => raise SMT_Failure.SMT SMT_Failure.Time_Out
+ val stats' = Symtab.cons_list (rule, Time.toMilliseconds elapsed) stats
+ in (Symtab.update (id, (map fst bounds, thm)) proofs, stats', ctxt,
+ concl_tranformation, sub_global_rew) end
+
+fun replay_ll_def assms ll_defs rewrite_rules stats ctxt term =
+ let
+ val rewrite = let val thy = Proof_Context.theory_of (empty_simpset ctxt) in
+ Raw_Simplifier.rewrite_term thy rewrite_rules []
+ #> not (null ll_defs) ? SMTLIB_Isar.unlift_term ll_defs
+ end
+ val replay = Timing.timing (SMT_Replay_Methods.prove ctxt (rewrite term))
+ val ({elapsed, ...}, thm) =
+ SMT_Config.with_time_limit ctxt SMT_Config.reconstruction_step_timeout replay
+ (fn _ => Method.insert_tac ctxt (map snd assms) THEN' Classical.fast_tac ctxt)
+ handle Timeout.TIMEOUT _ => raise SMT_Failure.SMT SMT_Failure.Time_Out
+ val stats' = Symtab.cons_list ("ll_defs", Time.toMilliseconds elapsed) stats
+ in
+ (thm, stats')
+ end
+
+fun replay outer_ctxt
+ ({context = ctxt, typs, terms, rewrite_rules, assms, ll_defs, ...} : SMT_Translate.replay_data)
+ output =
+ let
+ val rewrite_rules =
+ filter_out (fn thm => Term.could_unify (Thm.prop_of @{thm verit_eq_true_simplify},
+ Thm.prop_of thm))
+ rewrite_rules
+ val num_ll_defs = length ll_defs
+ val index_of_id = Integer.add (~ num_ll_defs)
+ val id_of_index = Integer.add num_ll_defs
+
+ val (actual_steps, ctxt2) =
+ VeriT_Proof.parse_replay typs terms output ctxt
+
+ fun step_of_assume (j, (_, th)) =
+ VeriT_Proof.VeriT_Replay_Node {
+ id = SMTLIB_Interface.assert_name_of_index (id_of_index j),
+ rule = VeriT_Proof.veriT_input_rule,
+ args = [],
+ prems = [],
+ proof_ctxt = [],
+ concl = Thm.prop_of th
+ |> Raw_Simplifier.rewrite_term (Proof_Context.theory_of
+ (empty_simpset ctxt addsimps rewrite_rules)) [] [],
+ bounds = [],
+ subproof = ([], [], [])}
+ val used_assert_ids = fold add_used_asserts_in_step actual_steps []
+ fun normalize_tac ctxt = let val thy = Proof_Context.theory_of (empty_simpset ctxt) in
+ Raw_Simplifier.rewrite_term thy rewrite_rules [] end
+ val used_assm_js =
+ map_filter (fn id => let val i = index_of_id id in if i >= 0 then SOME (i, nth assms i)
+ else NONE end)
+ used_assert_ids
+
+ val assm_steps = map step_of_assume used_assm_js
+ val steps = assm_steps @ actual_steps
+
+ fun extract (VeriT_Proof.VeriT_Replay_Node {id, rule, concl, bounds, ...}) =
+ (id, rule, concl, map fst bounds)
+ fun cond rule = rule = VeriT_Proof.veriT_input_rule
+ val add_asssert = SMT_Replay.add_asserted Symtab.update Symtab.empty extract cond
+ val ((_, _), (ctxt3, assumed)) =
+ add_asssert outer_ctxt rewrite_rules assms
+ (map_filter (remove_rewrite_rules_from_rules num_ll_defs) steps) ctxt2
+
+ val used_rew_js =
+ map_filter (fn id => let val i = index_of_id id in if i < 0
+ then SOME (id, normalize_tac ctxt (nth ll_defs id)) else NONE end)
+ used_assert_ids
+ val (assumed, stats) = fold (fn ((id, thm)) => fn (assumed, stats) =>
+ let val (thm, stats) = replay_ll_def assms ll_defs rewrite_rules stats ctxt thm
+ in (Symtab.update (SMTLIB_Interface.assert_name_of_index id, ([], thm)) assumed, stats)
+ end)
+ used_rew_js (assumed, Symtab.empty)
+
+ val ctxt4 =
+ ctxt3
+ |> put_simpset (SMT_Replay.make_simpset ctxt3 [])
+ |> Config.put SAT.solver (Config.get ctxt3 SMT_Config.sat_solver)
+ val len = length steps
+ val start = Timing.start ()
+ val print_runtime_statistics = SMT_Replay.intermediate_statistics ctxt4 start len
+ fun blockwise f (i, x) y =
+ (if i > 0 andalso i mod 100 = 0 then print_runtime_statistics i else (); f x y)
+ val (proofs, stats, ctxt5, _, _) =
+ fold_index (blockwise (replay_step rewrite_rules ll_defs assumed [])) steps
+ (assumed, stats, ctxt4, fn x => x, fn x => x)
+ val _ = print_runtime_statistics len
+ val total = Time.toMilliseconds (#elapsed (Timing.result start))
+ val (_, VeriT_Proof.VeriT_Replay_Node {id, ...}) = split_last steps
+ val _ = SMT_Config.statistics_msg ctxt5
+ (Pretty.string_of o SMT_Replay.pretty_statistics "veriT" total) stats
+ in
+ Symtab.lookup proofs id |> the |> snd |> singleton (Proof_Context.export ctxt5 outer_ctxt)
+ end
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/SMT/verit_replay_methods.ML Tue Oct 30 22:59:06 2018 +0100
@@ -0,0 +1,843 @@
+(* Title: HOL/Tools/SMT/verit_replay_methods.ML
+ Author: Mathias Fleury, MPII
+
+Proof methods for replaying veriT proofs.
+*)
+
+signature VERIT_REPLAY_METHODS =
+sig
+
+ val is_skolemisation: string -> bool
+ val is_skolemisation_step: VeriT_Proof.veriT_replay_node -> bool
+
+ (* methods for veriT proof rules *)
+ val method_for: string -> Proof.context -> thm list -> term list -> term ->
+ thm
+
+ val veriT_step_requires_subproof_assms : string -> bool
+ val eq_congruent_pred: Proof.context -> 'a -> term -> thm
+end;
+
+
+structure Verit_Replay_Methods: VERIT_REPLAY_METHODS =
+struct
+
+(*Some general comments on the proof format:
+ 1. Double negations are not always removed. This means for example that the equivalence rules
+ cannot assume that the double negations have already been removed. Therefore, we match the
+ term, instantiate the theorem, then use simp (to remove double negations), and finally use
+ assumption.
+ 2. The reconstruction for rule forall_inst is buggy and tends to be very fragile, because the rule
+ is doing much more that is supposed to do. Moreover types can make trivial goals (for the
+ boolean structure) impossible to prove.
+ 3. Duplicate literals are sometimes removed, mostly by the SAT solver. We currently do not care
+ about it, since in all cases we have met, a rule like tmp_AC_simp is called to do the
+ simplification.
+
+ Rules unsupported on purpose:
+ * Distinct_Elim, XOR, let (we don't need them).
+ * tmp_skolemize (because it is not clear if veriT still generates using it).
+*)
+
+datatype verit_rule =
+ False | True |
+
+ (* input: a repeated (normalized) assumption of assumption of in a subproof *)
+ Normalized_Input | Local_Input |
+ (* Subproof: *)
+ Subproof |
+ (* Conjunction: *)
+ And | Not_And | And_Pos | And_Neg |
+ (* Disjunction"" *)
+ Or | Or_Pos | Not_Or | Or_Neg |
+ (* Disjunction: *)
+ Implies | Implies_Neg1 | Implies_Neg2 | Implies_Pos | Not_Implies1 | Not_Implies2 |
+ (* Equivalence: *)
+ Equiv_neg1 | Equiv_pos1 | Equiv_pos2 | Equiv_neg2 | Not_Equiv1 | Not_Equiv2 | Equiv1 | Equiv2 |
+ (* If-then-else: *)
+ ITE_Pos1 | ITE_Pos2 | ITE_Neg1 | ITE_Neg2 | Not_ITE1 | Not_ITE2 | ITE_Intro | ITE1 | ITE2 |
+ (* Equality: *)
+ Eq_Congruent | Eq_Reflexive | Eq_Transitive | Eq_Congruent_Pred | Trans | Refl | Cong |
+ (* Arithmetics: *)
+ LA_Disequality | LA_Generic | LA_Tautology | LIA_Generic | LA_Totality | LA_RW_Eq |
+ NLA_Generic |
+ (* Quantifiers: *)
+ Forall_Inst | Qnt_Rm_Unused | Qnt_Join | Qnt_Simplify | Bind | Skolem_Forall | Skolem_Ex |
+ (* Resolution: *)
+ Theory_Resolution | Resolution |
+ (* Various transformation: *)
+ Connective_Equiv |
+ (* Temporary rules, that the veriT developpers want to remove: *)
+ Tmp_AC_Simp |
+ Tmp_Bfun_Elim |
+ (* Unsupported rule *)
+ Unsupported
+
+val is_skolemisation = member (op =) ["sko_forall", "sko_ex"]
+fun is_skolemisation_step (VeriT_Proof.VeriT_Replay_Node {id, ...}) = is_skolemisation id
+
+fun verit_rule_of "bind" = Bind
+ | verit_rule_of "cong" = Cong
+ | verit_rule_of "refl" = Refl
+ | verit_rule_of "equiv1" = Equiv1
+ | verit_rule_of "equiv2" = Equiv2
+ | verit_rule_of "equiv_pos1" = Equiv_pos1
+ | verit_rule_of "equiv_pos2" = Equiv_pos2
+ | verit_rule_of "equiv_neg1" = Equiv_neg1
+ | verit_rule_of "equiv_neg2" = Equiv_neg2
+ | verit_rule_of "sko_forall" = Skolem_Forall
+ | verit_rule_of "sko_ex" = Skolem_Ex
+ | verit_rule_of "eq_reflexive" = Eq_Reflexive
+ | verit_rule_of "th_resolution" = Theory_Resolution
+ | verit_rule_of "forall_inst" = Forall_Inst
+ | verit_rule_of "implies_pos" = Implies_Pos
+ | verit_rule_of "or" = Or
+ | verit_rule_of "not_or" = Not_Or
+ | verit_rule_of "resolution" = Resolution
+ | verit_rule_of "eq_congruent" = Eq_Congruent
+ | verit_rule_of "connective_equiv" = Connective_Equiv
+ | verit_rule_of "trans" = Trans
+ | verit_rule_of "false" = False
+ | verit_rule_of "tmp_AC_simp" = Tmp_AC_Simp
+ | verit_rule_of "and" = And
+ | verit_rule_of "not_and" = Not_And
+ | verit_rule_of "and_pos" = And_Pos
+ | verit_rule_of "and_neg" = And_Neg
+ | verit_rule_of "or_pos" = Or_Pos
+ | verit_rule_of "or_neg" = Or_Neg
+ | verit_rule_of "not_equiv1" = Not_Equiv1
+ | verit_rule_of "not_equiv2" = Not_Equiv2
+ | verit_rule_of "not_implies1" = Not_Implies1
+ | verit_rule_of "not_implies2" = Not_Implies2
+ | verit_rule_of "implies_neg1" = Implies_Neg1
+ | verit_rule_of "implies_neg2" = Implies_Neg2
+ | verit_rule_of "implies" = Implies
+ | verit_rule_of "tmp_bfun_elim" = Tmp_Bfun_Elim
+ | verit_rule_of "ite1" = ITE1
+ | verit_rule_of "ite2" = ITE2
+ | verit_rule_of "not_ite1" = Not_ITE1
+ | verit_rule_of "not_ite2" = Not_ITE2
+ | verit_rule_of "ite_pos1" = ITE_Pos1
+ | verit_rule_of "ite_pos2" = ITE_Pos2
+ | verit_rule_of "ite_neg1" = ITE_Neg1
+ | verit_rule_of "ite_neg2" = ITE_Neg2
+ | verit_rule_of "ite_intro" = ITE_Intro
+ | verit_rule_of "la_disequality" = LA_Disequality
+ | verit_rule_of "lia_generic" = LIA_Generic
+ | verit_rule_of "la_generic" = LA_Generic
+ | verit_rule_of "la_tautology" = LA_Tautology
+ | verit_rule_of "la_totality" = LA_Totality
+ | verit_rule_of "la_rw_eq"= LA_RW_Eq
+ | verit_rule_of "nla_generic"= NLA_Generic
+ | verit_rule_of "eq_transitive" = Eq_Transitive
+ | verit_rule_of "qnt_rm_unused" = Qnt_Rm_Unused
+ | verit_rule_of "qnt_simplify" = Qnt_Simplify
+ | verit_rule_of "qnt_join" = Qnt_Join
+ | verit_rule_of "eq_congruent_pred" = Eq_Congruent_Pred
+ | verit_rule_of "subproof" = Subproof
+ | verit_rule_of r =
+ if r = VeriT_Proof.veriT_normalized_input_rule then Normalized_Input
+ else if r = VeriT_Proof.veriT_local_input_rule then Local_Input
+ else Unsupported
+
+fun string_of_verit_rule Bind = "Bind"
+ | string_of_verit_rule Cong = "Cong"
+ | string_of_verit_rule Refl = "Refl"
+ | string_of_verit_rule Equiv1 = "Equiv1"
+ | string_of_verit_rule Equiv2 = "Equiv2"
+ | string_of_verit_rule Equiv_pos1 = "Equiv_pos1"
+ | string_of_verit_rule Equiv_pos2 = "Equiv_pos2"
+ | string_of_verit_rule Equiv_neg1 = "Equiv_neg1"
+ | string_of_verit_rule Equiv_neg2 = "Equiv_neg2"
+ | string_of_verit_rule Skolem_Forall = "Skolem_Forall"
+ | string_of_verit_rule Skolem_Ex = "Skolem_Ex"
+ | string_of_verit_rule Eq_Reflexive = "Eq_Reflexive"
+ | string_of_verit_rule Theory_Resolution = "Theory_Resolution"
+ | string_of_verit_rule Forall_Inst = "forall_inst"
+ | string_of_verit_rule Or = "Or"
+ | string_of_verit_rule Not_Or = "Not_Or"
+ | string_of_verit_rule Resolution = "Resolution"
+ | string_of_verit_rule Eq_Congruent = "eq_congruent"
+ | string_of_verit_rule Connective_Equiv = "connective_equiv"
+ | string_of_verit_rule Trans = "trans"
+ | string_of_verit_rule False = "false"
+ | string_of_verit_rule And = "and"
+ | string_of_verit_rule And_Pos = "and_pos"
+ | string_of_verit_rule Not_And = "not_and"
+ | string_of_verit_rule And_Neg = "and_neg"
+ | string_of_verit_rule Or_Pos = "or_pos"
+ | string_of_verit_rule Or_Neg = "or_neg"
+ | string_of_verit_rule Tmp_AC_Simp = "tmp_AC_simp"
+ | string_of_verit_rule Not_Equiv1 = "not_equiv1"
+ | string_of_verit_rule Not_Equiv2 = "not_equiv2"
+ | string_of_verit_rule Not_Implies1 = "not_implies1"
+ | string_of_verit_rule Not_Implies2 = "not_implies2"
+ | string_of_verit_rule Implies_Neg1 = "implies_neg1"
+ | string_of_verit_rule Implies_Neg2 = "implies_neg2"
+ | string_of_verit_rule Implies = "implies"
+ | string_of_verit_rule Tmp_Bfun_Elim = "tmp_bfun_elim"
+ | string_of_verit_rule ITE1 = "ite1"
+ | string_of_verit_rule ITE2 = "ite2"
+ | string_of_verit_rule Not_ITE1 = "not_ite1"
+ | string_of_verit_rule Not_ITE2 = "not_ite2"
+ | string_of_verit_rule ITE_Pos1 = "ite_pos1"
+ | string_of_verit_rule ITE_Pos2 = "ite_pos2"
+ | string_of_verit_rule ITE_Neg1 = "ite_neg1"
+ | string_of_verit_rule ITE_Neg2 = "ite_neg2"
+ | string_of_verit_rule ITE_Intro = "ite_intro"
+ | string_of_verit_rule LA_Disequality = "la_disequality"
+ | string_of_verit_rule LA_Generic = "la_generic"
+ | string_of_verit_rule LIA_Generic = "lia_generic"
+ | string_of_verit_rule LA_Tautology = "la_tautology"
+ | string_of_verit_rule LA_RW_Eq = "la_rw_eq"
+ | string_of_verit_rule LA_Totality = "LA_Totality"
+ | string_of_verit_rule NLA_Generic = "nla_generic"
+ | string_of_verit_rule Eq_Transitive = "eq_transitive"
+ | string_of_verit_rule Qnt_Rm_Unused = "qnt_remove_unused"
+ | string_of_verit_rule Qnt_Simplify = "qnt_simplify"
+ | string_of_verit_rule Qnt_Join = "qnt_join"
+ | string_of_verit_rule Eq_Congruent_Pred = "eq_congruent_pred"
+ | string_of_verit_rule Normalized_Input = VeriT_Proof.veriT_normalized_input_rule
+ | string_of_verit_rule Local_Input = VeriT_Proof.veriT_normalized_input_rule
+ | string_of_verit_rule Subproof = "subproof"
+ | string_of_verit_rule r = "Unsupported rule: " ^ @{make_string} r
+
+(*** Methods to Replay Normal steps ***)
+(* sko_forall requires the assumptions to be able to SMT_Replay_Methods.prove the equivalence in case of double
+skolemization. See comment below. *)
+fun veriT_step_requires_subproof_assms t =
+ member (op =) ["refl", "cong", VeriT_Proof.veriT_local_input_rule, "sko_forall",
+ "sko_ex"] t
+
+fun simplify_tac ctxt thms =
+ ctxt
+ |> empty_simpset
+ |> put_simpset HOL_basic_ss
+ |> (fn ctxt => ctxt addsimps @{thms not_not eq_commute} addsimps thms)
+ |> Simplifier.full_simp_tac
+
+val bind_thms =
+ [@{lemma "(\<And>x x'. P x = Q x) \<Longrightarrow> (\<forall>x. P x) = (\<forall>y. Q y)"
+ by blast},
+ @{lemma "(\<And>x x'. P x = Q x) \<Longrightarrow> (\<exists>x. P x) = (\<exists>y. Q y)"
+ by blast},
+ @{lemma "(\<And>x x'. P x = Q x) \<Longrightarrow> (\<exists>x. P x = Q x)"
+ by blast},
+ @{lemma "(\<And>x x'. P x = Q x) \<Longrightarrow> (\<forall>x. P x = Q x)"
+ by blast}]
+
+fun TRY' tac = fn i => TRY (tac i)
+fun REPEAT' tac = fn i => REPEAT (tac i)
+fun REPEAT_CHANGED tac = fn i => REPEAT (CHANGED (tac i))
+
+fun bind ctxt [prems] t = SMT_Replay_Methods.prove ctxt t (fn _ =>
+ REPEAT' (resolve_tac ctxt bind_thms)
+ THEN' match_tac ctxt [prems]
+ THEN' simplify_tac ctxt []
+ THEN' REPEAT' (match_tac ctxt [@{thm refl}]))
+
+
+fun refl ctxt thm t =
+ (case find_first (fn thm => t = Thm.full_prop_of thm) thm of
+ SOME thm => thm
+ | NONE =>
+ (case try (Z3_Replay_Methods.refl ctxt thm) t of
+ NONE =>
+ ( Z3_Replay_Methods.cong ctxt thm t)
+ | SOME thm => thm))
+
+local
+ fun equiv_pos_neg_term ctxt thm (@{term Trueprop} $
+ (@{term HOL.disj} $ (_) $
+ ((@{term HOL.disj} $ a $ b)))) =
+ Drule.infer_instantiate' ctxt (map (SOME o Thm.cterm_of ctxt) [a, b]) thm
+
+ fun prove_equiv_pos_neg thm ctxt _ t =
+ let val thm = equiv_pos_neg_term ctxt thm t
+ in
+ SMT_Replay_Methods.prove ctxt t (fn _ =>
+ Method.insert_tac ctxt [thm]
+ THEN' simplify_tac ctxt [])
+ end
+in
+
+val equiv_pos1_thm =
+ @{lemma "\<not>(a \<longleftrightarrow> ~b) \<or> a \<or> b"
+ by blast+}
+
+val equiv_pos1 = prove_equiv_pos_neg equiv_pos1_thm
+
+val equiv_pos2_thm =
+ @{lemma "\<And>a b. ((\<not>a) \<noteq> b) \<or> a \<or> b"
+ by blast+}
+
+val equiv_pos2 = prove_equiv_pos_neg equiv_pos2_thm
+
+val equiv_neg1_thm =
+ @{lemma "(~a \<longleftrightarrow> ~b) \<or> a \<or> b"
+ by blast}
+
+val equiv_neg1 = prove_equiv_pos_neg equiv_neg1_thm
+
+val equiv_neg2_thm =
+ @{lemma "(a \<longleftrightarrow> b) \<or> a \<or> b"
+ by blast}
+
+val equiv_neg2 = prove_equiv_pos_neg equiv_neg2_thm
+
+end
+
+(* Most of the code below is due to the proof output of veriT: The description of the rule is wrong
+(and according to Pascal Fontaine, it is a bug). Anyway, currently, forall_inst does:
+ 1. swapping out the forall quantifiers
+ 2. instantiation
+ 3. boolean.
+
+However, types can mess-up things:
+ lemma \<open>(0 < degree a) = (0 \<noteq> degree a) \<Longrightarrow> 0 = degree a \<or> 0 < degree a\<close>
+ by fast
+works unlike
+ lemma \<open>((0::nat) < degree a) = (0 \<noteq> degree a) \<Longrightarrow> 0 = degree a \<or> 0 < degree a\<close>
+ by fast.
+Therefore, we use fast and auto as fall-back.
+*)
+fun forall_inst ctxt _ args t =
+ let
+ val instantiate =
+ fold (fn inst => fn tac =>
+ let val thm = Drule.infer_instantiate' ctxt [NONE, SOME (Thm.cterm_of ctxt inst)] @{thm spec}
+ in tac THEN' dmatch_tac ctxt [thm]end)
+ args
+ (K all_tac)
+ in
+ SMT_Replay_Methods.prove ctxt t (fn _ =>
+ resolve_tac ctxt [@{thm disj_not1} RSN (1, @{thm iffD2}) OF [@{thm impI}]]
+ THEN' TRY' (Raw_Simplifier.rewrite_goal_tac ctxt @{thms all_simps[symmetric] not_all})
+ THEN' TRY' instantiate
+ THEN' TRY' (simplify_tac ctxt [])
+ THEN' TRY' (SOLVED' (fn _ => HEADGOAL ( (assume_tac ctxt)
+ ORELSE'
+ TRY' (dresolve_tac ctxt @{thms conjE}
+ THEN_ALL_NEW assume_tac ctxt)
+ ORELSE'
+ TRY' (dresolve_tac ctxt @{thms verit_forall_inst}
+ THEN_ALL_NEW assume_tac ctxt))))
+ THEN' (TRY' (Classical.fast_tac ctxt))
+ THEN' (TRY' (K (Clasimp.auto_tac ctxt))))
+ end
+
+fun or _ [thm] _ = thm
+
+val implies_pos_thm =
+ [@{lemma "\<not>(A \<longrightarrow> B) \<or> \<not>A \<or> B"
+ by blast},
+ @{lemma "\<not>(\<not>A \<longrightarrow> B) \<or> A \<or> B"
+ by blast}]
+
+fun implies_pos ctxt _ t = SMT_Replay_Methods.prove ctxt t (fn _ =>
+ resolve_tac ctxt implies_pos_thm)
+
+fun extract_rewrite_rule_assumption thms =
+ let
+ fun is_rewrite_rule thm =
+ (case Thm.prop_of thm of
+ @{term Trueprop} $ (Const(@{const_name HOL.eq}, _) $ Free(_, _) $ _) => true
+ | _ => false)
+ in
+ thms
+ |> filter is_rewrite_rule
+ |> map (fn thm => thm COMP @{thm eq_reflection})
+ end
+
+(* We need to unfold the assumptions if we are in a subproof: For multiple skolemization, the context
+contains a mapping "verit_vrX \<leadsto> Eps f". The variable "verit_vrX" must be unfolded to "Eps f".
+Otherwise, the proof cannot be done. *)
+fun skolem_forall ctxt (thms) t =
+ let
+ val ts = extract_rewrite_rule_assumption thms
+ in
+ SMT_Replay_Methods.prove ctxt t (fn _ =>
+ REPEAT_CHANGED (resolve_tac ctxt @{thms verit_sko_forall'})
+ THEN' TRY' (simplify_tac ctxt ts)
+ THEN' TRY'(resolve_tac ctxt thms THEN_ALL_NEW resolve_tac ctxt @{thms refl})
+ THEN' TRY' (resolve_tac ctxt @{thms refl}))
+ end
+
+fun skolem_ex ctxt (thms) t =
+ let
+ val ts = extract_rewrite_rule_assumption thms
+ in
+ SMT_Replay_Methods.prove ctxt t (fn _ =>
+ Raw_Simplifier.rewrite_goal_tac ctxt ts
+ THEN' REPEAT_CHANGED (resolve_tac ctxt @{thms verit_sko_ex'})
+ THEN' REPEAT_CHANGED (resolve_tac ctxt thms THEN_ALL_NEW resolve_tac ctxt @{thms refl})
+ THEN' TRY' (resolve_tac ctxt @{thms refl}))
+ end
+
+fun eq_reflexive ctxt _ t = SMT_Replay_Methods.prove ctxt t (fn _ =>
+ resolve_tac ctxt [@{thm refl}])
+
+fun connective_equiv ctxt thms t = SMT_Replay_Methods.prove ctxt t (fn _ =>
+ Method.insert_tac ctxt thms
+ THEN' K (Clasimp.auto_tac ctxt))
+
+
+fun normalized_input ctxt prems t = SMT_Replay_Methods.prove ctxt t (fn _ =>
+ Method.insert_tac ctxt prems
+ THEN' TRY' (simplify_tac ctxt [])
+ THEN' TRY' (K (Clasimp.auto_tac ctxt)))
+
+val false_rule_thm = @{lemma "\<not>False" by blast}
+
+fun false_rule ctxt _ t = SMT_Replay_Methods.prove ctxt t (fn _ =>
+ resolve_tac ctxt [false_rule_thm])
+
+
+(* transitivity *)
+
+val trans_bool_thm =
+ @{lemma "P = Q \<Longrightarrow> Q \<Longrightarrow> P" by blast}
+fun trans _ [thm1, thm2] _ =
+ (case (Thm.full_prop_of thm1, Thm.full_prop_of thm2) of
+ (@{term Trueprop} $ (Const(@{const_name HOL.eq}, _) $ _ $ t2),
+ @{term Trueprop} $ (Const(@{const_name HOL.eq}, _) $ t3 $ _)) =>
+ if t2 = t3 then thm1 RSN (1, thm2 RSN (2, @{thm trans}))
+ else thm1 RSN (1, (thm2 RS sym) RSN (2, @{thm trans}))
+ | _ => trans_bool_thm OF [thm1, thm2])
+ | trans ctxt (thm1 :: thm2 :: thms) t =
+ trans ctxt (trans ctxt [thm1, thm2] t :: thms) t
+
+fun tmp_AC_rule ctxt _ t =
+ let
+ val simplify =
+ ctxt
+ |> empty_simpset
+ |> put_simpset HOL_basic_ss
+ |> (fn ctxt => ctxt addsimps @{thms ac_simps conj_ac})
+ |> Simplifier.full_simp_tac
+ in SMT_Replay_Methods.prove ctxt t (fn _ =>
+ REPEAT_ALL_NEW (simplify_tac ctxt []
+ THEN' TRY' simplify
+ THEN' TRY' (Classical.fast_tac ctxt))) end
+
+fun and_rule ctxt prems t = SMT_Replay_Methods.prove ctxt t (fn _ =>
+ Method.insert_tac ctxt prems
+ THEN' (fn i => REPEAT (dresolve_tac ctxt @{thms conjE} i THEN assume_tac ctxt (i+1)))
+ THEN' TRY' (assume_tac ctxt)
+ THEN' TRY' (simplify_tac ctxt []))
+
+fun not_and_rule ctxt prems t = SMT_Replay_Methods.prove ctxt t (fn _ =>
+ Method.insert_tac ctxt prems THEN'
+ Classical.fast_tac ctxt ORELSE' Clasimp.force_tac ctxt)
+
+fun not_or_rule ctxt prems t = SMT_Replay_Methods.prove ctxt t (fn _ =>
+ Method.insert_tac ctxt prems THEN'
+ Classical.fast_tac ctxt ORELSE' Clasimp.force_tac ctxt)
+
+local
+ fun simplify_and_pos ctxt =
+ ctxt
+ |> empty_simpset
+ |> put_simpset HOL_basic_ss
+ |> (fn ctxt => ctxt addsimps @{thms eq_commute verit_ite_intro_simp if_cancel}
+ addsimps @{thms simp_thms de_Morgan_conj})
+ |> Simplifier.full_simp_tac
+in
+
+fun and_pos ctxt _ t =
+ SMT_Replay_Methods.prove ctxt t (fn _ =>
+ REPEAT_CHANGED (resolve_tac ctxt @{thms verit_and_pos})
+ THEN' TRY' (simplify_and_pos ctxt)
+ THEN' TRY' (assume_tac ctxt)
+ THEN' TRY' (Classical.fast_tac ctxt))
+
+end
+
+fun and_neg_rule ctxt _ t = SMT_Replay_Methods.prove ctxt t (fn _ =>
+ REPEAT_CHANGED (resolve_tac ctxt @{thms verit_and_neg})
+ THEN' simplify_tac ctxt @{thms de_Morgan_conj[symmetric] excluded_middle
+ excluded_middle[of \<open>\<not>_\<close>, unfolded not_not]})
+
+fun or_pos_rule ctxt _ t = SMT_Replay_Methods.prove ctxt t (fn _ =>
+ simplify_tac ctxt @{thms simp_thms})
+
+fun or_neg_rule ctxt _ t = SMT_Replay_Methods.prove ctxt t (fn _ =>
+ resolve_tac ctxt @{thms verit_or_neg}
+ THEN' (fn i => dresolve_tac ctxt @{thms verit_subst_bool} i
+ THEN assume_tac ctxt (i+1))
+ THEN' simplify_tac ctxt @{thms simp_thms})
+
+val not_equiv1_thm =
+ @{lemma "\<not>(A \<longleftrightarrow> B) \<Longrightarrow> A \<or> B"
+ by blast}
+
+fun not_equiv1 ctxt [thm] t = SMT_Replay_Methods.prove ctxt t (fn _ =>
+ Method.insert_tac ctxt [not_equiv1_thm OF [thm]]
+ THEN' simplify_tac ctxt [])
+
+val not_equiv2_thm =
+ @{lemma "\<not>(A \<longleftrightarrow> B) \<Longrightarrow> \<not>A \<or> \<not>B"
+ by blast}
+
+fun not_equiv2 ctxt [thm] t = SMT_Replay_Methods.prove ctxt t (fn _ =>
+ Method.insert_tac ctxt [not_equiv2_thm OF [thm]]
+ THEN' simplify_tac ctxt [])
+
+val equiv1_thm =
+ @{lemma "(A \<longleftrightarrow> B) \<Longrightarrow> \<not>A \<or> B"
+ by blast}
+
+fun equiv1 ctxt [thm] t = SMT_Replay_Methods.prove ctxt t (fn _ =>
+ Method.insert_tac ctxt [equiv1_thm OF [thm]]
+ THEN' simplify_tac ctxt [])
+
+val equiv2_thm =
+ @{lemma "(A \<longleftrightarrow> B) \<Longrightarrow> A \<or> \<not>B"
+ by blast}
+
+fun equiv2 ctxt [thm] t = SMT_Replay_Methods.prove ctxt t (fn _ =>
+ Method.insert_tac ctxt [equiv2_thm OF [thm]]
+ THEN' simplify_tac ctxt [])
+
+
+val not_implies1_thm =
+ @{lemma "\<not>(A \<longrightarrow> B) \<Longrightarrow> A"
+ by blast}
+
+fun not_implies1 ctxt [thm] t = SMT_Replay_Methods.prove ctxt t (fn _ =>
+ Method.insert_tac ctxt [not_implies1_thm OF [thm]]
+ THEN' simplify_tac ctxt [])
+
+val not_implies2_thm =
+ @{lemma "\<not>(A \<longrightarrow>B) \<Longrightarrow> \<not>B"
+ by blast}
+
+fun not_implies2 ctxt [thm] t = SMT_Replay_Methods.prove ctxt t (fn _ =>
+ Method.insert_tac ctxt [not_implies2_thm OF [thm]]
+ THEN' simplify_tac ctxt [])
+
+
+local
+ fun implies_pos_neg_term ctxt thm (@{term Trueprop} $
+ (@{term HOL.disj} $ (@{term HOL.implies} $ a $ b) $ _)) =
+ Drule.infer_instantiate' ctxt (map (SOME o Thm.cterm_of ctxt) [a, b]) thm
+
+ fun prove_implies_pos_neg thm ctxt _ t =
+ let val thm = implies_pos_neg_term ctxt thm t
+ in
+ SMT_Replay_Methods.prove ctxt t (fn _ =>
+ Method.insert_tac ctxt [thm]
+ THEN' simplify_tac ctxt [])
+ end
+in
+
+val implies_neg1_thm =
+ @{lemma "(a \<longrightarrow> b) \<or> a"
+ by blast}
+
+val implies_neg1 = prove_implies_pos_neg implies_neg1_thm
+
+val implies_neg2_thm =
+ @{lemma "(a \<longrightarrow> b) \<or> \<not>b" by blast}
+
+val implies_neg2 = prove_implies_pos_neg implies_neg2_thm
+
+end
+
+val implies_thm =
+ @{lemma "(~a \<longrightarrow> b) \<Longrightarrow> a \<or> b"
+ "(a \<longrightarrow> b) \<Longrightarrow> \<not>a \<or> b"
+ by blast+}
+
+fun implies_rules ctxt prems t = SMT_Replay_Methods.prove ctxt t (fn _ =>
+ Method.insert_tac ctxt prems
+ THEN' resolve_tac ctxt implies_thm
+ THEN' assume_tac ctxt)
+
+
+(*
+Here is a case where force_tac fails, but auto_tac succeeds:
+ Ex (P x) \<noteq> P x c \<Longrightarrow>
+ (\<exists>v0. if x then P True v0 else P False v0) \<noteq> (if x then P True c else P False c)
+
+(this was before we added the eqsubst_tac). Therefore, to be safe, we add the fast, auto, and force.
+*)
+fun tmp_bfun_elim ctxt prems t = SMT_Replay_Methods.prove ctxt t (fn _ =>
+ Method.insert_tac ctxt prems
+ THEN' REPEAT_CHANGED (EqSubst.eqsubst_tac ctxt [0] @{thms verit_tmp_bfun_elim})
+ THEN' TRY' (simplify_tac ctxt [])
+ THEN' (Classical.fast_tac ctxt
+ ORELSE' K (Clasimp.auto_tac ctxt)
+ ORELSE' Clasimp.force_tac ctxt))
+
+val ite_pos1_thm =
+ @{lemma "\<not>(if x then P else Q) \<or> x \<or> Q"
+ by auto}
+
+fun ite_pos1 ctxt _ t = SMT_Replay_Methods.prove ctxt t (fn _ =>
+ resolve_tac ctxt [ite_pos1_thm])
+
+val ite_pos2_thms =
+ @{lemma "\<not>(if x then P else Q) \<or> \<not>x \<or> P" "\<not>(if \<not>x then P else Q) \<or> x \<or> P"
+ by auto}
+
+fun ite_pos2 ctxt _ t = SMT_Replay_Methods.prove ctxt t (fn _ =>
+ resolve_tac ctxt ite_pos2_thms)
+
+val ite_neg1_thms =
+ @{lemma "(if x then P else Q) \<or> x \<or> \<not>Q" "(if x then P else \<not>Q) \<or> x \<or> Q"
+ by auto}
+
+fun ite_neg1 ctxt _ t = SMT_Replay_Methods.prove ctxt t (fn _ =>
+ resolve_tac ctxt ite_neg1_thms)
+
+val ite_neg2_thms =
+ @{lemma "(if x then P else Q) \<or> \<not>x \<or> \<not>P" "(if \<not>x then P else Q) \<or> x \<or> \<not>P"
+ "(if x then \<not>P else Q) \<or> \<not>x \<or> P" "(if \<not>x then \<not>P else Q) \<or> x \<or> P"
+ by auto}
+
+fun ite_neg2 ctxt _ t = SMT_Replay_Methods.prove ctxt t (fn _ =>
+ resolve_tac ctxt ite_neg2_thms)
+
+val ite1_thm =
+ @{lemma "(if x then P else Q) \<Longrightarrow> x \<or> Q"
+ by (auto split: if_splits) }
+
+fun ite1 ctxt [thm] t = SMT_Replay_Methods.prove ctxt t (fn _ =>
+ resolve_tac ctxt [ite1_thm OF [thm]])
+
+val ite2_thm =
+ @{lemma "(if x then P else Q) \<Longrightarrow> \<not>x \<or> P"
+ by (auto split: if_splits) }
+
+fun ite2 ctxt [thm] t = SMT_Replay_Methods.prove ctxt t (fn _ =>
+ resolve_tac ctxt [ite2_thm OF [thm]])
+
+
+val not_ite1_thm =
+ @{lemma "\<not>(if x then P else Q) \<Longrightarrow> x \<or> \<not>Q"
+ by (auto split: if_splits) }
+
+fun not_ite1 ctxt [thm] t = SMT_Replay_Methods.prove ctxt t (fn _ =>
+ resolve_tac ctxt [not_ite1_thm OF [thm]])
+
+val not_ite2_thm =
+ @{lemma "\<not>(if x then P else Q) \<Longrightarrow> \<not>x \<or> \<not>P"
+ by (auto split: if_splits) }
+
+fun not_ite2 ctxt [thm] t = SMT_Replay_Methods.prove ctxt t (fn _ =>
+ resolve_tac ctxt [not_ite2_thm OF [thm]])
+
+
+fun unit_res ctxt thms t =
+ let
+ val thms = map (Conv.fconv_rule Thm.eta_long_conversion) thms
+ val t' = Thm.eta_long_conversion (Object_Logic.dest_judgment ctxt (Thm.cterm_of ctxt t))
+ val (_, t2) = Logic.dest_equals (Thm.prop_of t')
+ val thm = Z3_Replay_Methods.unit_res ctxt thms t2
+ in
+ @{thm verit_Pure_trans} OF [t', thm]
+ end
+
+fun ite_intro ctxt _ t =
+ let
+ fun simplify_ite ctxt =
+ ctxt
+ |> empty_simpset
+ |> put_simpset HOL_basic_ss
+ |> (fn ctxt => ctxt addsimps @{thms eq_commute verit_ite_intro_simp if_cancel}
+ addsimps @{thms simp_thms})
+ |> Simplifier.full_simp_tac
+ in
+ SMT_Replay_Methods.prove ctxt t (fn _ =>
+ (simplify_ite ctxt
+ THEN' TRY' (Blast.blast_tac ctxt
+ ORELSE' K (Clasimp.auto_tac ctxt)
+ ORELSE' Clasimp.force_tac ctxt)))
+ end
+
+
+(* Quantifiers *)
+
+fun qnt_rm_unused ctxt _ t = SMT_Replay_Methods.prove ctxt t (fn _ =>
+ Classical.fast_tac ctxt)
+
+fun qnt_simplify ctxt _ t = SMT_Replay_Methods.prove ctxt t (fn _ =>
+ Classical.fast_tac ctxt)
+
+fun qnt_join ctxt _ t = SMT_Replay_Methods.prove ctxt t (fn _ =>
+ Classical.fast_tac ctxt)
+
+
+(* Equality *)
+
+fun eq_transitive ctxt _ t = SMT_Replay_Methods.prove ctxt t (fn _ =>
+ REPEAT_CHANGED (resolve_tac ctxt [@{thm disj_not1} RSN (1, @{thm iffD2}) OF @{thms impI}])
+ THEN' REPEAT' (resolve_tac ctxt @{thms impI})
+ THEN' REPEAT' (eresolve_tac ctxt @{thms conjI})
+ THEN' REPEAT' (fn i => dresolve_tac ctxt @{thms verit_eq_transitive} i THEN assume_tac ctxt (i+1))
+ THEN' resolve_tac ctxt @{thms refl})
+
+local
+
+ (* Rewrite might apply below choice. As we do not want to change them (it can break other
+ rewriting steps), we cannot use Term.lambda *)
+ fun abstract_over_no_choice (v, body) =
+ let
+ fun abs lev tm =
+ if v aconv tm then Bound lev
+ else
+ (case tm of
+ Abs (a, T, t) => Abs (a, T, abs (lev + 1) t)
+ | t as (Const (\<^const_name>\<open>Hilbert_Choice.Eps\<close>, _) $ _) => t
+ | t $ u =>
+ (abs lev t $ (abs lev u handle Same.SAME => u)
+ handle Same.SAME => t $ abs lev u)
+ | _ => raise Same.SAME);
+ in abs 0 body handle Same.SAME => body end;
+
+ fun lambda_name (x, v) t =
+ Abs (if x = "" then Term.term_name v else x, fastype_of v, abstract_over_no_choice (v, t));
+
+ fun lambda v t = lambda_name ("", v) t;
+
+ fun extract_equal_terms (Const(\<^const_name>\<open>Trueprop\<close>, _) $ t) =
+ let fun ext (Const(\<^const_name>\<open>HOL.disj\<close>, _) $ (Const(\<^const_name>\<open>HOL.Not\<close>, _) $
+ (Const(\<^const_name>\<open>HOL.eq\<close>, _) $ t1 $ t2)) $ t) =
+ apfst (curry (op ::) (t1, t2)) (ext t)
+ | ext t = ([], t)
+ in ext t end
+ fun eq_congruent_tac ctxt t =
+ let
+ val (eqs, g) = extract_equal_terms t
+ fun replace1 (t1, t2) (g, tac) =
+ let
+ val abs_t1 = lambda t2 g
+ val subst = Drule.infer_instantiate' ctxt (map (SOME o Thm.cterm_of ctxt) [t1, t2, abs_t1])
+ @{thm subst}
+ in (Term.betapply (abs_t1, t1),
+ tac THEN' resolve_tac ctxt [subst]
+ THEN' TRY' (assume_tac ctxt)) end
+ val (_, tac) = fold replace1 eqs (g, K all_tac)
+ in
+ tac
+ end
+in
+
+fun eq_congruent_pred ctxt _ t =
+ SMT_Replay_Methods.prove ctxt t (fn _ =>
+ REPEAT' (resolve_tac ctxt [@{thm disj_not1[of \<open>_ = _\<close>]} RSN (1, @{thm iffD2}) OF @{thms impI}])
+ THEN' REPEAT' (eresolve_tac ctxt @{thms conjI})
+ THEN' eq_congruent_tac ctxt t
+ THEN' resolve_tac ctxt @{thms refl excluded_middle
+ excluded_middle[of \<open>\<not>_\<close>, unfolded not_not]})
+
+end
+
+
+(* subproof *)
+
+fun subproof ctxt [prem] t =
+ SMT_Replay_Methods.prove ctxt t (fn _ =>
+ (resolve_tac ctxt [@{thm disj_not1} RSN (1, @{thm iffD2}) OF [@{thm impI}],
+ @{thm disj_not1[of \<open>\<not>_\<close>, unfolded not_not]} RSN (1, @{thm iffD2}) OF [@{thm impI}]]
+ THEN' resolve_tac ctxt [prem]
+ THEN_ALL_NEW assume_tac ctxt
+ THEN' TRY' (assume_tac ctxt))
+ ORELSE' TRY' (Method.insert_tac ctxt [prem] THEN' Blast.blast_tac ctxt))
+
+
+(* la_rw_eq *)
+
+val la_rw_eq_thm = @{lemma \<open>(a :: nat) = b \<or> (a \<le> b) \<or> (a \<ge> b)\<close>
+ by auto}
+
+fun la_rw_eq ctxt _ t = SMT_Replay_Methods.prove ctxt t (fn _ =>
+ resolve_tac ctxt [la_rw_eq_thm])
+
+(* congruence *)
+fun cong ctxt thms = SMT_Replay_Methods.try_provers ctxt
+ (string_of_verit_rule Cong) [
+ ("basic", SMT_Replay_Methods.cong_basic ctxt thms),
+ ("full", SMT_Replay_Methods.cong_full ctxt thms),
+ ("unfolding then auto", SMT_Replay_Methods.cong_unfolding_first ctxt thms)] thms
+
+
+fun unsupported rule ctxt thms _ t = SMT_Replay_Methods.replay_error ctxt "Unsupported verit rule"
+ rule thms t
+
+fun ignore_args f ctxt thm _ t = f ctxt thm t
+
+fun choose Bind = ignore_args bind
+ | choose Refl = ignore_args refl
+ | choose And_Pos = ignore_args and_pos
+ | choose And_Neg = ignore_args and_neg_rule
+ | choose Cong = ignore_args cong
+ | choose Equiv_pos1 = ignore_args equiv_pos1
+ | choose Equiv_pos2 = ignore_args equiv_pos2
+ | choose Equiv_neg1 = ignore_args equiv_neg1
+ | choose Equiv_neg2 = ignore_args equiv_neg2
+ | choose Equiv1 = ignore_args equiv1
+ | choose Equiv2 = ignore_args equiv2
+ | choose Not_Equiv1 = ignore_args not_equiv1
+ | choose Not_Equiv2 = ignore_args not_equiv2
+ | choose Not_Implies1 = ignore_args not_implies1
+ | choose Not_Implies2 = ignore_args not_implies2
+ | choose Implies_Neg1 = ignore_args implies_neg1
+ | choose Implies_Neg2 = ignore_args implies_neg2
+ | choose Implies_Pos = ignore_args implies_pos
+ | choose Implies = ignore_args implies_rules
+ | choose Forall_Inst = forall_inst
+ | choose Skolem_Forall = ignore_args skolem_forall
+ | choose Skolem_Ex = ignore_args skolem_ex
+ | choose Or = ignore_args or
+ | choose Theory_Resolution = ignore_args unit_res
+ | choose Resolution = ignore_args unit_res
+ | choose Eq_Reflexive = ignore_args eq_reflexive
+ | choose Connective_Equiv = ignore_args connective_equiv
+ | choose Trans = ignore_args trans
+ | choose False = ignore_args false_rule
+ | choose Tmp_AC_Simp = ignore_args tmp_AC_rule
+ | choose And = ignore_args and_rule
+ | choose Not_And = ignore_args not_and_rule
+ | choose Not_Or = ignore_args not_or_rule
+ | choose Or_Pos = ignore_args or_pos_rule
+ | choose Or_Neg = ignore_args or_neg_rule
+ | choose Tmp_Bfun_Elim = ignore_args tmp_bfun_elim
+ | choose ITE1 = ignore_args ite1
+ | choose ITE2 = ignore_args ite2
+ | choose Not_ITE1 = ignore_args not_ite1
+ | choose Not_ITE2 = ignore_args not_ite2
+ | choose ITE_Pos1 = ignore_args ite_pos1
+ | choose ITE_Pos2 = ignore_args ite_pos2
+ | choose ITE_Neg1 = ignore_args ite_neg1
+ | choose ITE_Neg2 = ignore_args ite_neg2
+ | choose ITE_Intro = ignore_args ite_intro
+ | choose LA_Disequality = ignore_args Z3_Replay_Methods.arith_th_lemma
+ | choose LIA_Generic = ignore_args Z3_Replay_Methods.arith_th_lemma
+ | choose LA_Generic = ignore_args Z3_Replay_Methods.arith_th_lemma
+ | choose LA_Totality = ignore_args Z3_Replay_Methods.arith_th_lemma
+ | choose LA_Tautology = ignore_args Z3_Replay_Methods.arith_th_lemma
+ | choose LA_RW_Eq = ignore_args la_rw_eq
+ | choose NLA_Generic = ignore_args Z3_Replay_Methods.arith_th_lemma
+ | choose Normalized_Input = ignore_args normalized_input
+ | choose Qnt_Rm_Unused = ignore_args qnt_rm_unused
+ | choose Qnt_Simplify = ignore_args qnt_simplify
+ | choose Qnt_Join = ignore_args qnt_join
+ | choose Eq_Congruent_Pred = ignore_args eq_congruent_pred
+ | choose Eq_Congruent = ignore_args eq_congruent_pred
+ | choose Eq_Transitive = ignore_args eq_transitive
+ | choose Local_Input = ignore_args refl
+ | choose Subproof = ignore_args subproof
+ | choose r = unsupported (string_of_verit_rule r)
+
+type Verit_method = Proof.context -> thm list -> term -> thm
+type abs_context = int * term Termtab.table
+
+fun with_tracing rule method ctxt thms args t =
+ let val _ = SMT_Replay_Methods.trace_goal ctxt rule thms t
+ in method ctxt thms args t end
+
+fun method_for rule = with_tracing rule (choose (verit_rule_of rule))
+
+end;
--- a/src/HOL/Tools/SMT/z3_real.ML Tue Oct 30 22:08:36 2018 +0100
+++ b/src/HOL/Tools/SMT/z3_real.ML Tue Oct 30 22:59:06 2018 +0100
@@ -27,6 +27,6 @@
val _ = Theory.setup (Context.theory_map (
SMTLIB_Proof.add_type_parser real_type_parser #>
SMTLIB_Proof.add_term_parser real_term_parser #>
- Z3_Replay_Methods.add_arith_abstracter abstract))
+ SMT_Replay_Methods.add_arith_abstracter abstract))
end;
--- a/src/HOL/Tools/SMT/z3_replay.ML Tue Oct 30 22:08:36 2018 +0100
+++ b/src/HOL/Tools/SMT/z3_replay.ML Tue Oct 30 22:59:06 2018 +0100
@@ -16,17 +16,17 @@
structure Z3_Replay: Z3_REPLAY =
struct
-fun params_of t = Term.strip_qnt_vars @{const_name Pure.all} t
+local
+ fun extract (Z3_Proof.Z3_Step {id, rule, concl, fixes, ...}) = (id, rule, concl, fixes)
+ fun cond rule = Z3_Proof.is_assumption rule andalso rule <> Z3_Proof.Hypothesis
+in
-fun varify ctxt thm =
- let
- val maxidx = Thm.maxidx_of thm + 1
- val vs = params_of (Thm.prop_of thm)
- val vars = map_index (fn (i, (n, T)) => Var ((n, i + maxidx), T)) vs
- in Drule.forall_elim_list (map (Thm.cterm_of ctxt) vars) thm end
+val add_asserted = SMT_Replay.add_asserted Inttab.update Inttab.empty extract cond
+
+end
fun add_paramTs names t =
- fold2 (fn n => fn (_, T) => AList.update (op =) (n, T)) names (params_of t)
+ fold2 (fn n => fn (_, T) => AList.update (op =) (n, T)) names (SMT_Replay.params_of t)
fun new_fixes ctxt nTs =
let
@@ -47,7 +47,7 @@
fun under_fixes f ctxt (prems, nthms) names concl =
let
- val thms1 = map (varify ctxt) prems
+ val thms1 = map (SMT_Replay.varify ctxt) prems
val (ctxt', env) =
add_paramTs names concl []
|> fold (uncurry add_paramTs o apsnd Thm.prop_of) nthms
@@ -76,69 +76,6 @@
val stats' = Symtab.cons_list (Z3_Proof.string_of_rule rule, Time.toMilliseconds elapsed) stats
in (Inttab.update (id, (fixes, thm)) proofs, stats') end
-local
- val remove_trigger = mk_meta_eq @{thm trigger_def}
- val remove_fun_app = mk_meta_eq @{thm fun_app_def}
-
- fun rewrite_conv _ [] = Conv.all_conv
- | rewrite_conv ctxt eqs = Simplifier.full_rewrite (empty_simpset ctxt addsimps eqs)
-
- val rewrite_true_rule = @{lemma "True \<equiv> \<not> False" by simp}
- val prep_rules = [@{thm Let_def}, remove_trigger, remove_fun_app, rewrite_true_rule]
-
- fun rewrite _ [] = I
- | rewrite ctxt eqs = Conv.fconv_rule (rewrite_conv ctxt eqs)
-
- fun lookup_assm assms_net ct =
- Z3_Replay_Util.net_instances assms_net ct
- |> map (fn ithm as (_, thm) => (ithm, Thm.cprop_of thm aconvc ct))
-in
-
-fun add_asserted outer_ctxt rewrite_rules assms steps ctxt =
- let
- val eqs = map (rewrite ctxt [rewrite_true_rule]) rewrite_rules
- val eqs' = union Thm.eq_thm eqs prep_rules
-
- val assms_net =
- assms
- |> map (apsnd (rewrite ctxt eqs'))
- |> map (apsnd (Conv.fconv_rule Thm.eta_conversion))
- |> Z3_Replay_Util.thm_net_of snd
-
- fun revert_conv ctxt = rewrite_conv ctxt eqs' then_conv Thm.eta_conversion
-
- fun assume thm ctxt =
- let
- val ct = Thm.cprem_of thm 1
- val (thm', ctxt') = yield_singleton Assumption.add_assumes ct ctxt
- in (thm' RS thm, ctxt') end
-
- fun add1 id fixes thm1 ((i, th), exact) ((iidths, thms), (ctxt, ptab)) =
- let
- val (thm, ctxt') = if exact then (Thm.implies_elim thm1 th, ctxt) else assume thm1 ctxt
- val thms' = if exact then thms else th :: thms
- in (((i, (id, th)) :: iidths, thms'), (ctxt', Inttab.update (id, (fixes, thm)) ptab)) end
-
- fun add (Z3_Proof.Z3_Step {id, rule, concl, fixes, ...})
- (cx as ((iidths, thms), (ctxt, ptab))) =
- if Z3_Proof.is_assumption rule andalso rule <> Z3_Proof.Hypothesis then
- let
- val ct = Thm.cterm_of ctxt concl
- val thm1 = Thm.trivial ct |> Conv.fconv_rule (Conv.arg1_conv (revert_conv outer_ctxt))
- val thm2 = singleton (Variable.export ctxt outer_ctxt) thm1
- in
- (case lookup_assm assms_net (Thm.cprem_of thm2 1) of
- [] =>
- let val (thm, ctxt') = assume thm1 ctxt
- in ((iidths, thms), (ctxt', Inttab.update (id, (fixes, thm)) ptab)) end
- | ithms => fold (add1 id fixes thm1) ithms cx)
- end
- else
- cx
- in fold add steps (([], []), (ctxt, Inttab.empty)) end
-
-end
-
(* |- (EX x. P x) = P c |- ~ (ALL x. P x) = ~ P c *)
local
val sk_rules = @{lemma
@@ -211,42 +148,19 @@
fact_helper_ts prem_ids conjecture_id fact_helper_ids' steps}
end
-fun intermediate_statistics ctxt start total =
- SMT_Config.statistics_msg ctxt (fn current =>
- "Reconstructed " ^ string_of_int current ^ " of " ^ string_of_int total ^ " steps in " ^
- string_of_int (Time.toMilliseconds (#elapsed (Timing.result start))) ^ " ms")
-
-fun pretty_statistics total stats =
- let
- fun mean_of is =
- let
- val len = length is
- val mid = len div 2
- in if len mod 2 = 0 then (nth is (mid - 1) + nth is mid) div 2 else nth is mid end
- fun pretty_item name p = Pretty.item (Pretty.separate ":" [Pretty.str name, p])
- fun pretty (name, milliseconds) = pretty_item name (Pretty.block (Pretty.separate "," [
- Pretty.str (string_of_int (length milliseconds) ^ " occurrences") ,
- Pretty.str (string_of_int (mean_of milliseconds) ^ " ms mean time"),
- Pretty.str (string_of_int (fold Integer.max milliseconds 0) ^ " ms maximum time"),
- Pretty.str (string_of_int (fold Integer.add milliseconds 0) ^ " ms total time")]))
- in
- Pretty.big_list "Z3 proof reconstruction statistics:" (
- pretty_item "total time" (Pretty.str (string_of_int total ^ " ms")) ::
- map pretty (Symtab.dest stats))
- end
-
fun replay outer_ctxt
({context = ctxt, typs, terms, rewrite_rules, assms, ...} : SMT_Translate.replay_data) output =
let
val (steps, ctxt2) = Z3_Proof.parse typs terms output ctxt
- val ((_, rules), (ctxt3, assumed)) = add_asserted outer_ctxt rewrite_rules assms steps ctxt2
+ val ((_, rules), (ctxt3, assumed)) =
+ add_asserted outer_ctxt rewrite_rules assms steps ctxt2
val ctxt4 =
ctxt3
- |> put_simpset (Z3_Replay_Util.make_simpset ctxt3 [])
+ |> put_simpset (SMT_Replay.make_simpset ctxt3 [])
|> Config.put SAT.solver (Config.get ctxt3 SMT_Config.sat_solver)
val len = length steps
val start = Timing.start ()
- val print_runtime_statistics = intermediate_statistics ctxt4 start len
+ val print_runtime_statistics = SMT_Replay.intermediate_statistics ctxt4 start len
fun blockwise f (i, x) y =
(if i > 0 andalso i mod 100 = 0 then print_runtime_statistics i else (); f x y)
val (proofs, stats) =
@@ -254,7 +168,7 @@
val _ = print_runtime_statistics len
val total = Time.toMilliseconds (#elapsed (Timing.result start))
val (_, Z3_Proof.Z3_Step {id, ...}) = split_last steps
- val _ = SMT_Config.statistics_msg ctxt4 (Pretty.string_of o pretty_statistics total) stats
+ val _ = SMT_Config.statistics_msg ctxt4 (Pretty.string_of o SMT_Replay.pretty_statistics "Z3" total) stats
in
Inttab.lookup proofs id |> the |> snd |> discharge rules outer_ctxt ctxt4
end
--- a/src/HOL/Tools/SMT/z3_replay_methods.ML Tue Oct 30 22:08:36 2018 +0100
+++ b/src/HOL/Tools/SMT/z3_replay_methods.ML Tue Oct 30 22:59:06 2018 +0100
@@ -7,16 +7,6 @@
signature Z3_REPLAY_METHODS =
sig
- (*abstraction*)
- type abs_context = int * term Termtab.table
- type 'a abstracter = term -> abs_context -> 'a * abs_context
- val add_arith_abstracter: (term abstracter -> term option abstracter) ->
- Context.generic -> Context.generic
-
- (*theory lemma methods*)
- type th_lemma_method = Proof.context -> thm list -> term -> thm
- val add_th_lemma_method: string * th_lemma_method -> Context.generic ->
- Context.generic
(*methods for Z3 proof rules*)
type z3_method = Proof.context -> thm list -> term -> thm
@@ -48,6 +38,7 @@
val nnf_pos: z3_method
val nnf_neg: z3_method
val mp_oeq: z3_method
+ val arith_th_lemma: z3_method
val th_lemma: string -> z3_method
val method_for: Z3_Proof.z3_rule -> z3_method
end;
@@ -60,25 +51,14 @@
(* utility functions *)
-fun trace ctxt f = SMT_Config.trace_msg ctxt f ()
-
-fun pretty_thm ctxt thm = Syntax.pretty_term ctxt (Thm.concl_of thm)
+fun replay_error ctxt msg rule thms t =
+ SMT_Replay_Methods.replay_error ctxt msg (Z3_Proof.string_of_rule rule) thms t
-fun pretty_goal ctxt msg rule thms t =
- let
- val full_msg = msg ^ ": " ^ quote (Z3_Proof.string_of_rule rule)
- val assms =
- if null thms then []
- else [Pretty.big_list "assumptions:" (map (pretty_thm ctxt) thms)]
- val concl = Pretty.big_list "proposition:" [Syntax.pretty_term ctxt t]
- in Pretty.big_list full_msg (assms @ [concl]) end
-
-fun replay_error ctxt msg rule thms t = error (Pretty.string_of (pretty_goal ctxt msg rule thms t))
-
-fun replay_rule_error ctxt = replay_error ctxt "Failed to replay Z3 proof step"
+fun replay_rule_error ctxt rule thms t =
+ SMT_Replay_Methods.replay_rule_error ctxt (Z3_Proof.string_of_rule rule) thms t
fun trace_goal ctxt rule thms t =
- trace ctxt (fn () => Pretty.string_of (pretty_goal ctxt "Goal" rule thms t))
+ SMT_Replay_Methods.trace_goal ctxt (Z3_Proof.string_of_rule rule) thms t
fun as_prop (t as Const (@{const_name Trueprop}, _) $ _) = t
| as_prop t = HOLogic.mk_Trueprop t
@@ -88,50 +68,6 @@
fun dest_thm thm = dest_prop (Thm.concl_of thm)
-fun certify_prop ctxt t = Thm.cterm_of ctxt (as_prop t)
-
-fun try_provers ctxt rule [] thms t = replay_rule_error ctxt rule thms t
- | try_provers ctxt rule ((name, prover) :: named_provers) thms t =
- (case (trace ctxt (K ("Trying prover " ^ quote name)); try prover t) of
- SOME thm => thm
- | NONE => try_provers ctxt rule named_provers thms t)
-
-fun match ctxt pat t =
- (Vartab.empty, Vartab.empty)
- |> Pattern.first_order_match (Proof_Context.theory_of ctxt) (pat, t)
-
-fun gen_certify_inst sel cert ctxt thm t =
- let
- val inst = match ctxt (dest_thm thm) (dest_prop t)
- fun cert_inst (ix, (a, b)) = ((ix, a), cert b)
- in Vartab.fold (cons o cert_inst) (sel inst) [] end
-
-fun match_instantiateT ctxt t thm =
- if Term.exists_type (Term.exists_subtype Term.is_TVar) (dest_thm thm) then
- Thm.instantiate (gen_certify_inst fst (Thm.ctyp_of ctxt) ctxt thm t, []) thm
- else thm
-
-fun match_instantiate ctxt t thm =
- let val thm' = match_instantiateT ctxt t thm in
- Thm.instantiate ([], gen_certify_inst snd (Thm.cterm_of ctxt) ctxt thm' t) thm'
- end
-
-fun apply_rule ctxt t =
- (case Z3_Replay_Rules.apply ctxt (certify_prop ctxt t) of
- SOME thm => thm
- | NONE => raise Fail "apply_rule")
-
-fun discharge _ [] thm = thm
- | discharge i (rule :: rules) thm = discharge (i + Thm.nprems_of rule) rules (rule RSN (i, thm))
-
-fun by_tac ctxt thms ns ts t tac =
- Goal.prove ctxt [] (map as_prop ts) (as_prop t)
- (fn {context, prems} => HEADGOAL (tac context prems))
- |> Drule.generalize ([], ns)
- |> discharge 1 thms
-
-fun prove ctxt t tac = by_tac ctxt [] [] [] t (K o tac)
-
fun prop_tac ctxt prems =
Method.insert_tac ctxt prems
THEN' SUBGOAL (fn (prop, i) =>
@@ -141,137 +77,31 @@
fun quant_tac ctxt = Blast.blast_tac ctxt
-(* plug-ins *)
-
-type abs_context = int * term Termtab.table
-
-type 'a abstracter = term -> abs_context -> 'a * abs_context
-
-type th_lemma_method = Proof.context -> thm list -> term -> thm
-
-fun id_ord ((id1, _), (id2, _)) = int_ord (id1, id2)
-
-structure Plugins = Generic_Data
-(
- type T =
- (int * (term abstracter -> term option abstracter)) list *
- th_lemma_method Symtab.table
- val empty = ([], Symtab.empty)
- val extend = I
- fun merge ((abss1, ths1), (abss2, ths2)) = (
- Ord_List.merge id_ord (abss1, abss2),
- Symtab.merge (K true) (ths1, ths2))
-)
-
-fun add_arith_abstracter abs = Plugins.map (apfst (Ord_List.insert id_ord (serial (), abs)))
-fun get_arith_abstracters ctxt = map snd (fst (Plugins.get (Context.Proof ctxt)))
-
-fun add_th_lemma_method method = Plugins.map (apsnd (Symtab.update_new method))
-fun get_th_lemma_method ctxt = snd (Plugins.get (Context.Proof ctxt))
+fun apply_rule ctxt t =
+ (case Z3_Replay_Rules.apply ctxt (SMT_Replay_Methods.certify_prop ctxt t) of
+ SOME thm => thm
+ | NONE => raise Fail "apply_rule")
-(* abstraction *)
-
-fun prove_abstract ctxt thms t tac f =
- let
- val ((prems, concl), (_, ts)) = f (1, Termtab.empty)
- val ns = Termtab.fold (fn (_, v) => cons (fst (Term.dest_Free v))) ts []
- in
- by_tac ctxt [] ns prems concl tac
- |> match_instantiate ctxt t
- |> discharge 1 thms
- end
-
-fun prove_abstract' ctxt t tac f =
- prove_abstract ctxt [] t tac (f #>> pair [])
-
-fun lookup_term (_, terms) t = Termtab.lookup terms t
-
-fun abstract_sub t f cx =
- (case lookup_term cx t of
- SOME v => (v, cx)
- | NONE => f cx)
+(*theory-lemma*)
-fun mk_fresh_free t (i, terms) =
- let val v = Free ("t" ^ string_of_int i, fastype_of t)
- in (v, (i + 1, Termtab.update (t, v) terms)) end
-
-fun apply_abstracters _ [] _ cx = (NONE, cx)
- | apply_abstracters abs (abstracter :: abstracters) t cx =
- (case abstracter abs t cx of
- (NONE, _) => apply_abstracters abs abstracters t cx
- | x as (SOME _, _) => x)
-
-fun abstract_term (t as _ $ _) = abstract_sub t (mk_fresh_free t)
- | abstract_term (t as Abs _) = abstract_sub t (mk_fresh_free t)
- | abstract_term t = pair t
-
-fun abstract_bin abs f t t1 t2 = abstract_sub t (abs t1 ##>> abs t2 #>> f)
-
-fun abstract_ter abs f t t1 t2 t3 =
- abstract_sub t (abs t1 ##>> abs t2 ##>> abs t3 #>> (Scan.triple1 #> f))
-
-fun abstract_lit (@{const HOL.Not} $ t) = abstract_term t #>> HOLogic.mk_not
- | abstract_lit t = abstract_term t
-
-fun abstract_not abs (t as @{const HOL.Not} $ t1) =
- abstract_sub t (abs t1 #>> HOLogic.mk_not)
- | abstract_not _ t = abstract_lit t
+fun arith_th_lemma_tac ctxt prems =
+ Method.insert_tac ctxt prems
+ THEN' SELECT_GOAL (Local_Defs.unfold0_tac ctxt @{thms z3div_def z3mod_def})
+ THEN' Arith_Data.arith_tac ctxt
-fun abstract_conj (t as @{const HOL.conj} $ t1 $ t2) =
- abstract_bin abstract_conj HOLogic.mk_conj t t1 t2
- | abstract_conj t = abstract_lit t
-
-fun abstract_disj (t as @{const HOL.disj} $ t1 $ t2) =
- abstract_bin abstract_disj HOLogic.mk_disj t t1 t2
- | abstract_disj t = abstract_lit t
-
-fun abstract_prop (t as (c as @{const If (bool)}) $ t1 $ t2 $ t3) =
- abstract_ter abstract_prop (fn (t1, t2, t3) => c $ t1 $ t2 $ t3) t t1 t2 t3
- | abstract_prop (t as @{const HOL.disj} $ t1 $ t2) =
- abstract_bin abstract_prop HOLogic.mk_disj t t1 t2
- | abstract_prop (t as @{const HOL.conj} $ t1 $ t2) =
- abstract_bin abstract_prop HOLogic.mk_conj t t1 t2
- | abstract_prop (t as @{const HOL.implies} $ t1 $ t2) =
- abstract_bin abstract_prop HOLogic.mk_imp t t1 t2
- | abstract_prop (t as @{term "HOL.eq :: bool => _"} $ t1 $ t2) =
- abstract_bin abstract_prop HOLogic.mk_eq t t1 t2
- | abstract_prop t = abstract_not abstract_prop t
+fun arith_th_lemma ctxt thms t =
+ SMT_Replay_Methods.prove_abstract ctxt thms t arith_th_lemma_tac (
+ fold_map (SMT_Replay_Methods.abstract_arith ctxt o dest_thm) thms ##>>
+ SMT_Replay_Methods.abstract_arith ctxt (dest_prop t))
-fun abstract_arith ctxt u =
- let
- fun abs (t as (c as Const _) $ Abs (s, T, t')) =
- abstract_sub t (abs t' #>> (fn u' => c $ Abs (s, T, u')))
- | abs (t as (c as Const (@{const_name If}, _)) $ t1 $ t2 $ t3) =
- abstract_ter abs (fn (t1, t2, t3) => c $ t1 $ t2 $ t3) t t1 t2 t3
- | abs (t as @{const HOL.Not} $ t1) = abstract_sub t (abs t1 #>> HOLogic.mk_not)
- | abs (t as @{const HOL.disj} $ t1 $ t2) =
- abstract_sub t (abs t1 ##>> abs t2 #>> HOLogic.mk_disj)
- | abs (t as (c as Const (@{const_name uminus_class.uminus}, _)) $ t1) =
- abstract_sub t (abs t1 #>> (fn u => c $ u))
- | abs (t as (c as Const (@{const_name plus_class.plus}, _)) $ t1 $ t2) =
- abstract_sub t (abs t1 ##>> abs t2 #>> (fn (u1, u2) => c $ u1 $ u2))
- | abs (t as (c as Const (@{const_name minus_class.minus}, _)) $ t1 $ t2) =
- abstract_sub t (abs t1 ##>> abs t2 #>> (fn (u1, u2) => c $ u1 $ u2))
- | abs (t as (c as Const (@{const_name times_class.times}, _)) $ t1 $ t2) =
- abstract_sub t (abs t1 ##>> abs t2 #>> (fn (u1, u2) => c $ u1 $ u2))
- | abs (t as (c as Const (@{const_name z3div}, _)) $ t1 $ t2) =
- abstract_sub t (abs t1 ##>> abs t2 #>> (fn (u1, u2) => c $ u1 $ u2))
- | abs (t as (c as Const (@{const_name z3mod}, _)) $ t1 $ t2) =
- abstract_sub t (abs t1 ##>> abs t2 #>> (fn (u1, u2) => c $ u1 $ u2))
- | abs (t as (c as Const (@{const_name HOL.eq}, _)) $ t1 $ t2) =
- abstract_sub t (abs t1 ##>> abs t2 #>> (fn (u1, u2) => c $ u1 $ u2))
- | abs (t as (c as Const (@{const_name ord_class.less}, _)) $ t1 $ t2) =
- abstract_sub t (abs t1 ##>> abs t2 #>> (fn (u1, u2) => c $ u1 $ u2))
- | abs (t as (c as Const (@{const_name ord_class.less_eq}, _)) $ t1 $ t2) =
- abstract_sub t (abs t1 ##>> abs t2 #>> (fn (u1, u2) => c $ u1 $ u2))
- | abs t = abstract_sub t (fn cx =>
- if can HOLogic.dest_number t then (t, cx)
- else
- (case apply_abstracters abs (get_arith_abstracters ctxt) t cx of
- (SOME u, cx') => (u, cx')
- | (NONE, _) => abstract_term t cx))
- in abs u end
+val _ = Theory.setup (Context.theory_map (
+ SMT_Replay_Methods.add_th_lemma_method ("arith", arith_th_lemma)))
+
+fun th_lemma name ctxt thms =
+ (case Symtab.lookup (SMT_Replay_Methods.get_th_lemma_method ctxt) name of
+ SOME method => method ctxt thms
+ | NONE => replay_error ctxt "Bad theory" (Z3_Proof.Th_Lemma name) thms)
(* truth axiom *)
@@ -281,7 +111,7 @@
(* modus ponens *)
-fun mp _ [p, p_eq_q] _ = discharge 1 [p_eq_q, p] iffD1
+fun mp _ [p, p_eq_q] _ = SMT_Replay_Methods.discharge 1 [p_eq_q, p] iffD1
| mp ctxt thms t = replay_rule_error ctxt Z3_Proof.Modus_Ponens thms t
val mp_oeq = mp
@@ -289,7 +119,7 @@
(* reflexivity *)
-fun refl ctxt _ t = match_instantiate ctxt t @{thm refl}
+fun refl ctxt _ t = SMT_Replay_Methods.match_instantiate ctxt t @{thm refl}
(* symmetry *)
@@ -306,37 +136,10 @@
(* congruence *)
-fun ctac ctxt prems i st = st |> (
- resolve_tac ctxt (@{thm refl} :: prems) i
- ORELSE (cong_tac ctxt i THEN ctac ctxt prems (i + 1) THEN ctac ctxt prems i))
-
-fun cong_basic ctxt thms t =
- let val st = Thm.trivial (certify_prop ctxt t)
- in
- (case Seq.pull (ctac ctxt thms 1 st) of
- SOME (thm, _) => thm
- | NONE => raise THM ("cong", 0, thms @ [st]))
- end
-
-val cong_dest_rules = @{lemma
- "(\<not> P \<or> Q) \<and> (P \<or> \<not> Q) \<Longrightarrow> P = Q"
- "(P \<or> \<not> Q) \<and> (\<not> P \<or> Q) \<Longrightarrow> P = Q"
- by fast+}
-
-fun cong_full_core_tac ctxt =
- eresolve_tac ctxt @{thms subst}
- THEN' resolve_tac ctxt @{thms refl}
- ORELSE' Classical.fast_tac ctxt
-
-fun cong_full ctxt thms t = prove ctxt t (fn ctxt' =>
- Method.insert_tac ctxt thms
- THEN' (cong_full_core_tac ctxt'
- ORELSE' dresolve_tac ctxt cong_dest_rules
- THEN' cong_full_core_tac ctxt'))
-
-fun cong ctxt thms = try_provers ctxt Z3_Proof.Monotonicity [
- ("basic", cong_basic ctxt thms),
- ("full", cong_full ctxt thms)] thms
+fun cong ctxt thms = SMT_Replay_Methods.try_provers ctxt
+ (Z3_Proof.string_of_rule Z3_Proof.Monotonicity) [
+ ("basic", SMT_Replay_Methods.cong_basic ctxt thms),
+ ("full", SMT_Replay_Methods.cong_full ctxt thms)] thms
(* quantifier introduction *)
@@ -349,7 +152,7 @@
by fast+}
fun quant_intro ctxt [thm] t =
- prove ctxt t (K (REPEAT_ALL_NEW (resolve_tac ctxt (thm :: quant_intro_rules))))
+ SMT_Replay_Methods.prove ctxt t (K (REPEAT_ALL_NEW (resolve_tac ctxt (thm :: quant_intro_rules))))
| quant_intro ctxt thms t = replay_rule_error ctxt Z3_Proof.Quant_Intro thms t
@@ -357,15 +160,16 @@
(* TODO: there are no tests with this proof rule *)
fun distrib ctxt _ t =
- prove_abstract' ctxt t prop_tac (abstract_prop (dest_prop t))
+ SMT_Replay_Methods.prove_abstract' ctxt t prop_tac
+ (SMT_Replay_Methods.abstract_prop (dest_prop t))
(* elimination of conjunctions *)
fun and_elim ctxt [thm] t =
- prove_abstract ctxt [thm] t prop_tac (
- abstract_lit (dest_prop t) ##>>
- abstract_conj (dest_thm thm) #>>
+ SMT_Replay_Methods.prove_abstract ctxt [thm] t prop_tac (
+ SMT_Replay_Methods.abstract_lit (dest_prop t) ##>>
+ SMT_Replay_Methods.abstract_conj (dest_thm thm) #>>
apfst single o swap)
| and_elim ctxt thms t = replay_rule_error ctxt Z3_Proof.And_Elim thms t
@@ -373,9 +177,9 @@
(* elimination of negated disjunctions *)
fun not_or_elim ctxt [thm] t =
- prove_abstract ctxt [thm] t prop_tac (
- abstract_lit (dest_prop t) ##>>
- abstract_not abstract_disj (dest_thm thm) #>>
+ SMT_Replay_Methods.prove_abstract ctxt [thm] t prop_tac (
+ SMT_Replay_Methods.abstract_lit (dest_prop t) ##>>
+ SMT_Replay_Methods.abstract_not SMT_Replay_Methods.abstract_disj (dest_thm thm) #>>
apfst single o swap)
| not_or_elim ctxt thms t =
replay_rule_error ctxt Z3_Proof.Not_Or_Elim thms t
@@ -419,11 +223,11 @@
fun abstract_eq f (Const (@{const_name HOL.eq}, _) $ t1 $ t2) =
f t1 ##>> f t2 #>> HOLogic.mk_eq
- | abstract_eq _ t = abstract_term t
+ | abstract_eq _ t = SMT_Replay_Methods.abstract_term t
fun prove_prop_rewrite ctxt t =
- prove_abstract' ctxt t prop_tac (
- abstract_eq abstract_prop (dest_prop t))
+ SMT_Replay_Methods.prove_abstract' ctxt t prop_tac (
+ abstract_eq SMT_Replay_Methods.abstract_prop (dest_prop t))
fun arith_rewrite_tac ctxt _ =
let val backup_tac = Arith_Data.arith_tac ctxt ORELSE' Clasimp.force_tac ctxt in
@@ -432,8 +236,8 @@
end
fun prove_arith_rewrite ctxt t =
- prove_abstract' ctxt t arith_rewrite_tac (
- abstract_eq (abstract_arith ctxt) (dest_prop t))
+ SMT_Replay_Methods.prove_abstract' ctxt t arith_rewrite_tac (
+ abstract_eq (SMT_Replay_Methods.abstract_arith ctxt) (dest_prop t))
val lift_ite_thm = @{thm HOL.if_distrib} RS @{thm eq_reflection}
@@ -448,13 +252,14 @@
| _ => Conv.sub_conv (Conv.top_sweep_conv if_context_conv) ctxt) ct
fun lift_ite_rewrite ctxt t =
- prove ctxt t (fn ctxt =>
+ SMT_Replay_Methods.prove ctxt t (fn ctxt =>
CONVERSION (HOLogic.Trueprop_conv (Conv.binop_conv (if_context_conv ctxt)))
THEN' resolve_tac ctxt @{thms refl})
-fun prove_conj_disj_perm ctxt t = prove ctxt t Conj_Disj_Perm.conj_disj_perm_tac
+fun prove_conj_disj_perm ctxt t = SMT_Replay_Methods.prove ctxt t Conj_Disj_Perm.conj_disj_perm_tac
-fun rewrite ctxt _ = try_provers ctxt Z3_Proof.Rewrite [
+fun rewrite ctxt _ = SMT_Replay_Methods.try_provers ctxt
+ (Z3_Proof.string_of_rule Z3_Proof.Rewrite) [
("rules", apply_rule ctxt),
("conj_disj_perm", prove_conj_disj_perm ctxt),
("prop_rewrite", prove_prop_rewrite ctxt),
@@ -466,7 +271,7 @@
(* pulling quantifiers *)
-fun pull_quant ctxt _ t = prove ctxt t quant_tac
+fun pull_quant ctxt _ t = SMT_Replay_Methods.prove ctxt t quant_tac
(* pushing quantifiers *)
@@ -486,7 +291,7 @@
match_tac ctxt [@{thm iff_allI}, @{thm iff_exI}]
THEN' elim_unused_tac ctxt)) i st
-fun elim_unused ctxt _ t = prove ctxt t elim_unused_tac
+fun elim_unused ctxt _ t = SMT_Replay_Methods.prove ctxt t elim_unused_tac
(* destructive equality resolution *)
@@ -498,7 +303,7 @@
val quant_inst_rule = @{lemma "\<not>P x \<or> Q ==> \<not>(\<forall>x. P x) \<or> Q" by fast}
-fun quant_inst ctxt _ t = prove ctxt t (fn _ =>
+fun quant_inst ctxt _ t = SMT_Replay_Methods.prove ctxt t (fn _ =>
REPEAT_ALL_NEW (resolve_tac ctxt [quant_inst_rule])
THEN' resolve_tac ctxt @{thms excluded_middle})
@@ -532,10 +337,10 @@
val tab = Termtab.make (map (`Thm.term_of) (Thm.chyps_of thm))
val (thm', terms) = intro_hyps tab (dest_prop t) (thm, [])
in
- prove_abstract ctxt [thm'] t prop_tac (
- fold (snd oo abstract_lit) terms #>
- abstract_disj (dest_thm thm') #>> single ##>>
- abstract_disj (dest_prop t))
+ SMT_Replay_Methods.prove_abstract ctxt [thm'] t prop_tac (
+ fold (snd oo SMT_Replay_Methods.abstract_lit) terms #>
+ SMT_Replay_Methods.abstract_disj (dest_thm thm') #>> single ##>>
+ SMT_Replay_Methods.abstract_disj (dest_prop t))
end
handle LEMMA () => replay_error ctxt "Bad proof state" Z3_Proof.Lemma thms t)
| lemma ctxt thms t = replay_rule_error ctxt Z3_Proof.Lemma thms t
@@ -543,18 +348,10 @@
(* unit resolution *)
-fun abstract_unit (t as (@{const HOL.Not} $ (@{const HOL.disj} $ t1 $ t2))) =
- abstract_sub t (abstract_unit t1 ##>> abstract_unit t2 #>>
- HOLogic.mk_not o HOLogic.mk_disj)
- | abstract_unit (t as (@{const HOL.disj} $ t1 $ t2)) =
- abstract_sub t (abstract_unit t1 ##>> abstract_unit t2 #>>
- HOLogic.mk_disj)
- | abstract_unit t = abstract_lit t
-
fun unit_res ctxt thms t =
- prove_abstract ctxt thms t prop_tac (
- fold_map (abstract_unit o dest_thm) thms ##>>
- abstract_unit (dest_prop t) #>>
+ SMT_Replay_Methods.prove_abstract ctxt thms t prop_tac (
+ fold_map (SMT_Replay_Methods.abstract_unit o dest_thm) thms ##>>
+ SMT_Replay_Methods.abstract_unit (dest_prop t) #>>
(fn (prems, concl) => (prems, concl)))
@@ -576,7 +373,7 @@
(* commutativity *)
-fun comm ctxt _ t = match_instantiate ctxt t @{thm eq_commute}
+fun comm ctxt _ t = SMT_Replay_Methods.match_instantiate ctxt t @{thm eq_commute}
(* definitional axioms *)
@@ -584,11 +381,13 @@
fun def_axiom_disj ctxt t =
(case dest_prop t of
@{const HOL.disj} $ u1 $ u2 =>
- prove_abstract' ctxt t prop_tac (
- abstract_prop u2 ##>> abstract_prop u1 #>> HOLogic.mk_disj o swap)
- | u => prove_abstract' ctxt t prop_tac (abstract_prop u))
+ SMT_Replay_Methods.prove_abstract' ctxt t prop_tac (
+ SMT_Replay_Methods.abstract_prop u2 ##>> SMT_Replay_Methods.abstract_prop u1 #>>
+ HOLogic.mk_disj o swap)
+ | u => SMT_Replay_Methods.prove_abstract' ctxt t prop_tac (SMT_Replay_Methods.abstract_prop u))
-fun def_axiom ctxt _ = try_provers ctxt Z3_Proof.Def_Axiom [
+fun def_axiom ctxt _ = SMT_Replay_Methods.try_provers ctxt
+ (Z3_Proof.string_of_rule Z3_Proof.Def_Axiom) [
("rules", apply_rule ctxt),
("disj", def_axiom_disj ctxt)] []
@@ -607,11 +406,11 @@
(* negation normal form *)
fun nnf_prop ctxt thms t =
- prove_abstract ctxt thms t prop_tac (
- fold_map (abstract_prop o dest_thm) thms ##>>
- abstract_prop (dest_prop t))
+ SMT_Replay_Methods.prove_abstract ctxt thms t prop_tac (
+ fold_map (SMT_Replay_Methods.abstract_prop o dest_thm) thms ##>>
+ SMT_Replay_Methods.abstract_prop (dest_prop t))
-fun nnf ctxt rule thms = try_provers ctxt rule [
+fun nnf ctxt rule thms = SMT_Replay_Methods.try_provers ctxt (Z3_Proof.string_of_rule rule) [
("prop", nnf_prop ctxt thms),
("quant", quant_intro ctxt [hd thms])] thms
@@ -619,26 +418,6 @@
fun nnf_neg ctxt = nnf ctxt Z3_Proof.Nnf_Neg
-(* theory lemmas *)
-
-fun arith_th_lemma_tac ctxt prems =
- Method.insert_tac ctxt prems
- THEN' SELECT_GOAL (Local_Defs.unfold0_tac ctxt @{thms z3div_def z3mod_def})
- THEN' Arith_Data.arith_tac ctxt
-
-fun arith_th_lemma ctxt thms t =
- prove_abstract ctxt thms t arith_th_lemma_tac (
- fold_map (abstract_arith ctxt o dest_thm) thms ##>>
- abstract_arith ctxt (dest_prop t))
-
-val _ = Theory.setup (Context.theory_map (add_th_lemma_method ("arith", arith_th_lemma)))
-
-fun th_lemma name ctxt thms =
- (case Symtab.lookup (get_th_lemma_method ctxt) name of
- SOME method => method ctxt thms
- | NONE => replay_error ctxt "Bad theory" (Z3_Proof.Th_Lemma name) thms)
-
-
(* mapping of rules to methods *)
fun unsupported rule ctxt = replay_error ctxt "Unsupported" rule
--- a/src/HOL/Tools/SMT/z3_replay_util.ML Tue Oct 30 22:08:36 2018 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,155 +0,0 @@
-(* Title: HOL/Tools/SMT/z3_replay_util.ML
- Author: Sascha Boehme, TU Muenchen
-
-Helper functions required for Z3 proof replay.
-*)
-
-signature Z3_REPLAY_UTIL =
-sig
- (*theorem nets*)
- val thm_net_of: ('a -> thm) -> 'a list -> 'a Net.net
- val net_instances: (int * thm) Net.net -> cterm -> (int * thm) list
-
- (*proof combinators*)
- val under_assumption: (thm -> thm) -> cterm -> thm
- val discharge: thm -> thm -> thm
-
- (*a faster COMP*)
- type compose_data = cterm list * (cterm -> cterm list) * thm
- val precompose: (cterm -> cterm list) -> thm -> compose_data
- val precompose2: (cterm -> cterm * cterm) -> thm -> compose_data
- val compose: compose_data -> thm -> thm
-
- (*simpset*)
- val add_simproc: Simplifier.simproc -> Context.generic -> Context.generic
- val make_simpset: Proof.context -> thm list -> simpset
-end;
-
-structure Z3_Replay_Util: Z3_REPLAY_UTIL =
-struct
-
-(* theorem nets *)
-
-fun thm_net_of f xthms =
- let fun insert xthm = Net.insert_term (K false) (Thm.prop_of (f xthm), xthm)
- in fold insert xthms Net.empty end
-
-fun maybe_instantiate ct thm =
- try Thm.first_order_match (Thm.cprop_of thm, ct)
- |> Option.map (fn inst => Thm.instantiate inst thm)
-
-local
- fun instances_from_net match f net ct =
- let
- val lookup = if match then Net.match_term else Net.unify_term
- val xthms = lookup net (Thm.term_of ct)
- fun select ct = map_filter (f (maybe_instantiate ct)) xthms
- fun select' ct =
- let val thm = Thm.trivial ct
- in map_filter (f (try (fn rule => rule COMP thm))) xthms end
- in (case select ct of [] => select' ct | xthms' => xthms') end
-in
-
-fun net_instances net =
- instances_from_net false (fn f => fn (i, thm) => Option.map (pair i) (f thm))
- net
-
-end
-
-
-(* proof combinators *)
-
-fun under_assumption f ct =
- let val ct' = SMT_Util.mk_cprop ct in Thm.implies_intr ct' (f (Thm.assume ct')) end
-
-fun discharge p pq = Thm.implies_elim pq p
-
-
-(* a faster COMP *)
-
-type compose_data = cterm list * (cterm -> cterm list) * thm
-
-fun list2 (x, y) = [x, y]
-
-fun precompose f rule : compose_data = (f (Thm.cprem_of rule 1), f, rule)
-fun precompose2 f rule : compose_data = precompose (list2 o f) rule
-
-fun compose (cvs, f, rule) thm =
- discharge thm
- (Thm.instantiate ([], map (dest_Var o Thm.term_of) cvs ~~ f (Thm.cprop_of thm)) rule)
-
-
-(* simpset *)
-
-local
- val antisym_le1 = mk_meta_eq @{thm order_class.antisym_conv}
- val antisym_le2 = mk_meta_eq @{thm linorder_class.antisym_conv2}
- val antisym_less1 = mk_meta_eq @{thm linorder_class.antisym_conv1}
- val antisym_less2 = mk_meta_eq @{thm linorder_class.antisym_conv3}
-
- fun eq_prop t thm = HOLogic.mk_Trueprop t aconv Thm.prop_of thm
- fun dest_binop ((c as Const _) $ t $ u) = (c, t, u)
- | dest_binop t = raise TERM ("dest_binop", [t])
-
- fun prove_antisym_le ctxt ct =
- let
- val (le, r, s) = dest_binop (Thm.term_of ct)
- val less = Const (@{const_name less}, Term.fastype_of le)
- val prems = Simplifier.prems_of ctxt
- in
- (case find_first (eq_prop (le $ s $ r)) prems of
- NONE =>
- find_first (eq_prop (HOLogic.mk_not (less $ r $ s))) prems
- |> Option.map (fn thm => thm RS antisym_less1)
- | SOME thm => SOME (thm RS antisym_le1))
- end
- handle THM _ => NONE
-
- fun prove_antisym_less ctxt ct =
- let
- val (less, r, s) = dest_binop (HOLogic.dest_not (Thm.term_of ct))
- val le = Const (@{const_name less_eq}, Term.fastype_of less)
- val prems = Simplifier.prems_of ctxt
- in
- (case find_first (eq_prop (le $ r $ s)) prems of
- NONE =>
- find_first (eq_prop (HOLogic.mk_not (less $ s $ r))) prems
- |> Option.map (fn thm => thm RS antisym_less2)
- | SOME thm => SOME (thm RS antisym_le2))
- end
- handle THM _ => NONE
-
- val basic_simpset =
- simpset_of (put_simpset HOL_ss @{context}
- addsimps @{thms field_simps times_divide_eq_right times_divide_eq_left arith_special
- arith_simps rel_simps array_rules z3div_def z3mod_def NO_MATCH_def}
- addsimprocs [@{simproc numeral_divmod},
- Simplifier.make_simproc @{context} "fast_int_arith"
- {lhss = [@{term "(m::int) < n"}, @{term "(m::int) \<le> n"}, @{term "(m::int) = n"}],
- proc = K Lin_Arith.simproc},
- Simplifier.make_simproc @{context} "antisym_le"
- {lhss = [@{term "(x::'a::order) \<le> y"}],
- proc = K prove_antisym_le},
- Simplifier.make_simproc @{context} "antisym_less"
- {lhss = [@{term "\<not> (x::'a::linorder) < y"}],
- proc = K prove_antisym_less}])
-
- structure Simpset = Generic_Data
- (
- type T = simpset
- val empty = basic_simpset
- val extend = I
- val merge = Simplifier.merge_ss
- )
-in
-
-fun add_simproc simproc context =
- Simpset.map (simpset_map (Context.proof_of context)
- (fn ctxt => ctxt addsimprocs [simproc])) context
-
-fun make_simpset ctxt rules =
- simpset_of (put_simpset (Simpset.get (Context.Proof ctxt)) ctxt addsimps rules)
-
-end
-
-end;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Tue Oct 30 22:08:36 2018 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Tue Oct 30 22:59:06 2018 +0100
@@ -55,7 +55,6 @@
val vampire_skolemisation_rule = "skolemisation"
val veriT_la_generic_rule = "la_generic"
val veriT_simp_arith_rule = "simp_arith"
-val veriT_tmp_ite_elim_rule = "tmp_ite_elim"
val veriT_tmp_skolemize_rule = "tmp_skolemize"
val z3_skolemize_rule = Z3_Proof.string_of_rule Z3_Proof.Skolemize
val z3_th_lemma_rule_prefix = Z3_Proof.string_of_rule (Z3_Proof.Th_Lemma "")
@@ -63,7 +62,7 @@
val skolemize_rules =
[e_definition_rule, e_skolemize_rule, leo2_extcnf_forall_neg_rule, satallax_skolemize_rule,
- spass_skolemize_rule, vampire_skolemisation_rule, veriT_tmp_ite_elim_rule,
+ spass_skolemize_rule, vampire_skolemisation_rule,
veriT_tmp_skolemize_rule, waldmeister_skolemize_rule, z3_skolemize_rule, zipperposition_cnf_rule]
fun is_ext_rule rule = (rule = leo2_extcnf_equal_neg_rule)