# HG changeset patch # User fleury # Date 1540913041 -3600 # Node ID d5ab1636660bfbf976d2cd69f8149bf1572e800c # Parent a5c0d61ce5dbfad0324005a2de22db9e67e8560d split SMT reconstruction into library diff -r a5c0d61ce5db -r d5ab1636660b src/HOL/SMT.thy --- a/src/HOL/SMT.thy Sun Oct 28 16:31:13 2018 +0100 +++ b/src/HOL/SMT.thy Tue Oct 30 16:24:01 2018 +0100 @@ -212,8 +212,9 @@ 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" diff -r a5c0d61ce5db -r d5ab1636660b 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 16:24:01 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 a5c0d61ce5db -r d5ab1636660b 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 16:24:01 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 a5c0d61ce5db -r d5ab1636660b src/HOL/Tools/SMT/z3_real.ML --- a/src/HOL/Tools/SMT/z3_real.ML Sun Oct 28 16:31:13 2018 +0100 +++ b/src/HOL/Tools/SMT/z3_real.ML Tue Oct 30 16:24:01 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 a5c0d61ce5db -r d5ab1636660b src/HOL/Tools/SMT/z3_replay.ML --- a/src/HOL/Tools/SMT/z3_replay.ML Sun Oct 28 16:31:13 2018 +0100 +++ b/src/HOL/Tools/SMT/z3_replay.ML Tue Oct 30 16:24:01 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 a5c0d61ce5db -r d5ab1636660b src/HOL/Tools/SMT/z3_replay_methods.ML --- a/src/HOL/Tools/SMT/z3_replay_methods.ML Sun Oct 28 16:31:13 2018 +0100 +++ b/src/HOL/Tools/SMT/z3_replay_methods.ML Tue Oct 30 16:24:01 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 a5c0d61ce5db -r d5ab1636660b src/HOL/Tools/SMT/z3_replay_util.ML --- a/src/HOL/Tools/SMT/z3_replay_util.ML Sun Oct 28 16:31:13 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;