# HG changeset patch # User wenzelm # Date 1540936746 -3600 # Node ID ab98f058f9dcc0af3abdf6bbcc9094b2607672f4 # Parent 9660bbf5ce7e85ee0cf9e185242d259d2504fdf0# Parent be8c70794375eee3a2b93bb2579fe0859295c8c4 merged diff -r be8c70794375 -r ab98f058f9dc CONTRIBUTORS --- 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 ----------------------------- diff -r be8c70794375 -r ab98f058f9dc NEWS --- 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: diff -r be8c70794375 -r ab98f058f9dc src/HOL/Data_Structures/Array_Braun.thy --- 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 \ nat \ 'a tree" where -"braun_of_rec x n = (if n=0 then Leaf +fun braun_of_naive :: "'a \ nat \ '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 \ nat \ 'a tree * 'a tree" where "braun2_of x n = (if n = 0 then (Leaf, Node Leaf x Leaf) diff -r be8c70794375 -r ab98f058f9dc src/HOL/SMT.thy --- 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 \Extra theorems for veriT reconstruction\ + +lemma verit_sko_forall: \(\x. P x) \ P (SOME x. \P x)\ + using someI[of \\x. \P x\] + by auto + +lemma verit_sko_forall': \P (SOME x. \P x) = A \ (\x. P x) = A\ + by (subst verit_sko_forall) + +lemma verit_sko_forall_indirect: \x = (SOME x. \P x) \ (\x. P x) \ P x\ + using someI[of \\x. \P x\] + by auto + +lemma verit_sko_ex: \(\x. P x) \ P (SOME x. P x)\ + using someI[of \\x. P x\] + by auto + +lemma verit_sko_ex': \P (SOME x. P x) = A \ (\x. P x) = A\ + by (subst verit_sko_ex) + +lemma verit_sko_ex_indirect: \x = (SOME x. P x) \ (\x. P x) \ P x\ + using someI[of \\x. P x\] + by auto + +lemma verit_Pure_trans: + \P \ Q \ Q \ P\ + by auto + +lemma verit_if_cong: + assumes \b \ c\ + and \c \ x \ u\ + and \\ c \ y \ v\ + shows \(if b then x else y) \ (if c then u else v)\ + using assms if_cong[of b c x u] by auto + +lemma verit_if_weak_cong': + \b \ c \ (if b then x else y) \ (if c then x else y)\ + by auto + +lemma verit_ite_intro_simp: + \(if c then (a :: 'a) = (if c then P else Q') else Q) = (if c then a = P else Q)\ + \(if c then R else b = (if c then R' else Q')) = + (if c then R else b = Q')\ + \(if c then a' = a' else b' = b')\ + by (auto split: if_splits) + +lemma verit_or_neg: + \(A \ B) \ B \ \A\ + \(\A \ B) \ B \ A\ + by auto + +lemma verit_subst_bool: \P \ f True \ f P\ + by auto + +lemma verit_and_pos: + \(a \ \b \ A) \ \(a \ b) \ A\ + \(a \ A) \ \a \ A\ + \(\a \ A) \ a \ A\ + by blast+ + +lemma verit_la_generic: + \(a::int) \ x \ a = x \ a \ x\ + by linarith + +lemma verit_tmp_bfun_elim: + \(if b then P True else P False) = P b\ + by (cases b) auto + +lemma verit_eq_true_simplify: + \(P = True) \ P\ + by auto + +lemma verit_and_neg: + \B \ B' \ (A \ B) \ \A \ B'\ + \B \ B' \ (\A \ B) \ A \ B'\ + by auto + +lemma verit_forall_inst: + \A \ B \ \A \ B\ + \\A \ B \ A \ B\ + \A \ B \ \B \ A\ + \A \ \B \ B \ A\ + \A \ B \ \A \ B\ + \\A \ B \ A \ B\ + by blast+ + +lemma verit_eq_transitive: + \A = B \ B = C \ A = C\ + \A = B \ C = B \ A = C\ + \B = A \ B = C \ A = C\ + \B = A \ C = B \ A = C\ + by auto + + subsection \Setup\ 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 = \ @@ -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 \ diff -r be8c70794375 -r ab98f058f9dc src/HOL/Tools/SMT/conj_disj_perm.ML --- 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; diff -r be8c70794375 -r ab98f058f9dc src/HOL/Tools/SMT/smt_config.ML --- 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>\smt_read_only_certificates\ (K false) val verbose = Attrib.setup_config_bool \<^binding>\smt_verbose\ (K true) val trace = Attrib.setup_config_bool \<^binding>\smt_trace\ (K false) +val trace_veriT = Attrib.setup_config_bool \<^binding>\smt_debug_verit\ (K false) val statistics = Attrib.setup_config_bool \<^binding>\smt_statistics\ (K false) val monomorph_limit = Attrib.setup_config_int \<^binding>\smt_monomorph_limit\ (K 10) val monomorph_instances = Attrib.setup_config_int \<^binding>\smt_monomorph_instances\ (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 *) diff -r be8c70794375 -r ab98f058f9dc src/HOL/Tools/SMT/smt_real.ML --- 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; diff -r be8c70794375 -r ab98f058f9dc src/HOL/Tools/SMT/smt_replay.ML --- /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) \ n"}, @{term "(m::int) = n"}], + proc = K Lin_Arith.simproc}, + Simplifier.make_simproc @{context} "antisym_le" + {lhss = [@{term "(x::'a::order) \ y"}], + proc = K prove_antisym_le}, + Simplifier.make_simproc @{context} "antisym_less" + {lhss = [@{term "\ (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 \ \ 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; diff -r be8c70794375 -r ab98f058f9dc src/HOL/Tools/SMT/smt_replay_methods.ML --- /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>\Hilbert_Choice.Eps\, _) $ 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 + "(\ P \ Q) \ (P \ \ Q) \ P = Q" + "(P \ \ Q) \ (\ P \ Q) \ 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; diff -r be8c70794375 -r ab98f058f9dc src/HOL/Tools/SMT/smt_solver.ML --- 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) diff -r be8c70794375 -r ab98f058f9dc src/HOL/Tools/SMT/smt_systems.ML --- 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 diff -r be8c70794375 -r ab98f058f9dc src/HOL/Tools/SMT/smtlib_proof.ML --- 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 diff -r be8c70794375 -r ab98f058f9dc src/HOL/Tools/SMT/verit_proof.ML --- 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; diff -r be8c70794375 -r ab98f058f9dc src/HOL/Tools/SMT/verit_proof_parse.ML --- 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 [] diff -r be8c70794375 -r ab98f058f9dc src/HOL/Tools/SMT/verit_replay.ML --- /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 diff -r be8c70794375 -r ab98f058f9dc src/HOL/Tools/SMT/verit_replay_methods.ML --- /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 "(\x x'. P x = Q x) \ (\x. P x) = (\y. Q y)" + by blast}, + @{lemma "(\x x'. P x = Q x) \ (\x. P x) = (\y. Q y)" + by blast}, + @{lemma "(\x x'. P x = Q x) \ (\x. P x = Q x)" + by blast}, + @{lemma "(\x x'. P x = Q x) \ (\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 "\(a \ ~b) \ a \ b" + by blast+} + +val equiv_pos1 = prove_equiv_pos_neg equiv_pos1_thm + +val equiv_pos2_thm = + @{lemma "\a b. ((\a) \ b) \ a \ b" + by blast+} + +val equiv_pos2 = prove_equiv_pos_neg equiv_pos2_thm + +val equiv_neg1_thm = + @{lemma "(~a \ ~b) \ a \ b" + by blast} + +val equiv_neg1 = prove_equiv_pos_neg equiv_neg1_thm + +val equiv_neg2_thm = + @{lemma "(a \ b) \ a \ 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 \(0 < degree a) = (0 \ degree a) \ 0 = degree a \ 0 < degree a\ + by fast +works unlike + lemma \((0::nat) < degree a) = (0 \ degree a) \ 0 = degree a \ 0 < degree a\ + 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 "\(A \ B) \ \A \ B" + by blast}, + @{lemma "\(\A \ B) \ A \ 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 \ 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 "\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 \ Q \ 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 \\_\, 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 "\(A \ B) \ A \ 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 "\(A \ B) \ \A \ \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 \ B) \ \A \ 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 \ B) \ A \ \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 "\(A \ B) \ 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 "\(A \B) \ \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 \ b) \ a" + by blast} + +val implies_neg1 = prove_implies_pos_neg implies_neg1_thm + +val implies_neg2_thm = + @{lemma "(a \ b) \ \b" by blast} + +val implies_neg2 = prove_implies_pos_neg implies_neg2_thm + +end + +val implies_thm = + @{lemma "(~a \ b) \ a \ b" + "(a \ b) \ \a \ 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) \ P x c \ + (\v0. if x then P True v0 else P False v0) \ (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 "\(if x then P else Q) \ x \ 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 "\(if x then P else Q) \ \x \ P" "\(if \x then P else Q) \ x \ 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) \ x \ \Q" "(if x then P else \Q) \ x \ 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) \ \x \ \P" "(if \x then P else Q) \ x \ \P" + "(if x then \P else Q) \ \x \ P" "(if \x then \P else Q) \ x \ 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) \ x \ 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) \ \x \ 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 "\(if x then P else Q) \ x \ \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 "\(if x then P else Q) \ \x \ \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>\Hilbert_Choice.Eps\, _) $ _) => 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>\Trueprop\, _) $ t) = + let fun ext (Const(\<^const_name>\HOL.disj\, _) $ (Const(\<^const_name>\HOL.Not\, _) $ + (Const(\<^const_name>\HOL.eq\, _) $ 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 \_ = _\]} 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 \\_\, 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 \\_\, 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 \(a :: nat) = b \ (a \ b) \ (a \ b)\ + 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; diff -r be8c70794375 -r ab98f058f9dc src/HOL/Tools/SMT/z3_real.ML --- 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; diff -r be8c70794375 -r ab98f058f9dc src/HOL/Tools/SMT/z3_replay.ML --- 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 \ \ 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 diff -r be8c70794375 -r ab98f058f9dc src/HOL/Tools/SMT/z3_replay_methods.ML --- 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 - "(\ P \ Q) \ (P \ \ Q) \ P = Q" - "(P \ \ Q) \ (\ P \ Q) \ 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 "\P x \ Q ==> \(\x. P x) \ 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 diff -r be8c70794375 -r ab98f058f9dc src/HOL/Tools/SMT/z3_replay_util.ML --- 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) \ n"}, @{term "(m::int) = n"}], - proc = K Lin_Arith.simproc}, - Simplifier.make_simproc @{context} "antisym_le" - {lhss = [@{term "(x::'a::order) \ y"}], - proc = K prove_antisym_le}, - Simplifier.make_simproc @{context} "antisym_less" - {lhss = [@{term "\ (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; diff -r be8c70794375 -r ab98f058f9dc src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- 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)