# HG changeset patch # User blanchet # Date 1492698088 -7200 # Node ID f595b7532dc98b377e89098211e7761767d329f8 # Parent d10f0bbc7ea152fb2fa1ab4fb06404080dbc7d16 removed Old_SMT legacy module diff -r d10f0bbc7ea1 -r f595b7532dc9 NEWS --- a/NEWS Thu Apr 20 10:45:52 2017 +0200 +++ b/NEWS Thu Apr 20 16:21:28 2017 +0200 @@ -154,6 +154,8 @@ * Session HOL-Algebra extended by additional lattice theory: the Knaster-Tarski fixed point theorem and Galois Connections. +* SMT module: The legacy module 'src/HOL/Library/Old_SMT.thy' has been removed. + * Session HOL-Analysis: more material involving arcs, paths, covering spaces, innessential maps, retracts. Major results include the Jordan Curve Theorem and the Great Picard Theorem. diff -r d10f0bbc7ea1 -r f595b7532dc9 src/HOL/Library/Old_SMT.thy --- a/src/HOL/Library/Old_SMT.thy Thu Apr 20 10:45:52 2017 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,431 +0,0 @@ -(* Title: HOL/Library/Old_SMT.thy - Author: Sascha Boehme, TU Muenchen -*) - -section \Old Version of Bindings to Satisfiability Modulo Theories (SMT) solvers\ - -theory Old_SMT -imports "../Real" "../Word/Word" -keywords "old_smt_status" :: diag -begin - -ML_file "Old_SMT/old_smt_utils.ML" -ML_file "Old_SMT/old_smt_failure.ML" -ML_file "Old_SMT/old_smt_config.ML" - - -subsection \Triggers for quantifier instantiation\ - -text \ -Some SMT solvers support patterns as a quantifier instantiation -heuristics. Patterns may either be positive terms (tagged by "pat") -triggering quantifier instantiations -- when the solver finds a -term matching a positive pattern, it instantiates the corresponding -quantifier accordingly -- or negative terms (tagged by "nopat") -inhibiting quantifier instantiations. A list of patterns -of the same kind is called a multipattern, and all patterns in a -multipattern are considered conjunctively for quantifier instantiation. -A list of multipatterns is called a trigger, and their multipatterns -act disjunctively during quantifier instantiation. Each multipattern -should mention at least all quantified variables of the preceding -quantifier block. -\ - -typedecl pattern - -consts - pat :: "'a \ pattern" - nopat :: "'a \ pattern" - -definition trigger :: "pattern list list \ bool \ bool" where "trigger _ P = P" - - -subsection \Quantifier weights\ - -text \ -Weight annotations to quantifiers influence the priority of quantifier -instantiations. They should be handled with care for solvers, which support -them, because incorrect choices of weights might render a problem unsolvable. -\ - -definition weight :: "int \ bool \ bool" where "weight _ P = P" - -text \ -Weights must be non-negative. The value \0\ is equivalent to providing -no weight at all. - -Weights should only be used at quantifiers and only inside triggers (if the -quantifier has triggers). Valid usages of weights are as follows: - -\begin{itemize} -\item -@{term "\x. trigger [[pat (P x)]] (weight 2 (P x))"} -\item -@{term "\x. weight 3 (P x)"} -\end{itemize} -\ - - -subsection \Higher-order encoding\ - -text \ -Application is made explicit for constants occurring with varying -numbers of arguments. This is achieved by the introduction of the -following constant. -\ - -definition fun_app where "fun_app f = f" - -text \ -Some solvers support a theory of arrays which can be used to encode -higher-order functions. The following set of lemmas specifies the -properties of such (extensional) arrays. -\ - -lemmas array_rules = ext fun_upd_apply fun_upd_same fun_upd_other - fun_upd_upd fun_app_def - - -subsection \First-order logic\ - -text \ -Some SMT solvers only accept problems in first-order logic, i.e., -where formulas and terms are syntactically separated. When -translating higher-order into first-order problems, all -uninterpreted constants (those not built-in in the target solver) -are treated as function symbols in the first-order sense. Their -occurrences as head symbols in atoms (i.e., as predicate symbols) are -turned into terms by logically equating such atoms with @{term True}. -For technical reasons, @{term True} and @{term False} occurring inside -terms are replaced by the following constants. -\ - -definition term_true where "term_true = True" -definition term_false where "term_false = False" - - -subsection \Integer division and modulo for Z3\ - -definition z3div :: "int \ int \ int" where - "z3div k l = (if 0 \ l then k div l else -(k div (-l)))" - -definition z3mod :: "int \ int \ int" where - "z3mod k l = (if 0 \ l then k mod l else k mod (-l))" - - -subsection \Setup\ - -ML_file "Old_SMT/old_smt_builtin.ML" -ML_file "Old_SMT/old_smt_datatypes.ML" -ML_file "Old_SMT/old_smt_normalize.ML" -ML_file "Old_SMT/old_smt_translate.ML" -ML_file "Old_SMT/old_smt_solver.ML" -ML_file "Old_SMT/old_smtlib_interface.ML" -ML_file "Old_SMT/old_z3_interface.ML" -ML_file "Old_SMT/old_z3_proof_parser.ML" -ML_file "Old_SMT/old_z3_proof_tools.ML" -ML_file "Old_SMT/old_z3_proof_literals.ML" -ML_file "Old_SMT/old_z3_proof_methods.ML" -named_theorems old_z3_simp "simplification rules for Z3 proof reconstruction" -ML_file "Old_SMT/old_z3_proof_reconstruction.ML" -ML_file "Old_SMT/old_z3_model.ML" -ML_file "Old_SMT/old_smt_setup_solvers.ML" - -setup \ - Old_SMT_Config.setup #> - Old_SMT_Normalize.setup #> - Old_SMTLIB_Interface.setup #> - Old_Z3_Interface.setup #> - Old_SMT_Setup_Solvers.setup -\ - -method_setup old_smt = \ - Scan.optional Attrib.thms [] >> - (fn thms => fn ctxt => - (legacy_feature "Proof method \"old_smt\" will be discontinued soon -- use \"smt\" instead"; - METHOD (fn facts => HEADGOAL (Old_SMT_Solver.smt_tac ctxt (thms @ facts))))) -\ "apply an SMT solver to the current goal" - - -subsection \Configuration\ - -text \ -The current configuration can be printed by the command -\old_smt_status\, which shows the values of most options. -\ - - - -subsection \General configuration options\ - -text \ -The option \old_smt_solver\ can be used to change the target SMT -solver. The possible values can be obtained from the \old_smt_status\ -command. - -Due to licensing restrictions, Yices and Z3 are not installed/enabled -by default. Z3 is free for non-commercial applications and can be enabled -by setting the \OLD_Z3_NON_COMMERCIAL\ environment variable to -\yes\. -\ - -declare [[ old_smt_solver = z3 ]] - -text \ -Since SMT solvers are potentially non-terminating, there is a timeout -(given in seconds) to restrict their runtime. A value greater than -120 (seconds) is in most cases not advisable. -\ - -declare [[ old_smt_timeout = 20 ]] - -text \ -SMT solvers apply randomized heuristics. In case a problem is not -solvable by an SMT solver, changing the following option might help. -\ - -declare [[ old_smt_random_seed = 1 ]] - -text \ -In general, the binding to SMT solvers runs as an oracle, i.e, the SMT -solvers are fully trusted without additional checks. The following -option can cause the SMT solver to run in proof-producing mode, giving -a checkable certificate. This is currently only implemented for Z3. -\ - -declare [[ old_smt_oracle = false ]] - -text \ -Each SMT solver provides several commandline options to tweak its -behaviour. They can be passed to the solver by setting the following -options. -\ - -declare [[ old_cvc3_options = "" ]] -declare [[ old_yices_options = "" ]] -declare [[ old_z3_options = "" ]] - -text \ -Enable the following option to use built-in support for datatypes and -records. Currently, this is only implemented for Z3 running in oracle -mode. -\ - -declare [[ old_smt_datatypes = false ]] - -text \ -The SMT method provides an inference mechanism to detect simple triggers -in quantified formulas, which might increase the number of problems -solvable by SMT solvers (note: triggers guide quantifier instantiations -in the SMT solver). To turn it on, set the following option. -\ - -declare [[ old_smt_infer_triggers = false ]] - -text \ -The SMT method monomorphizes the given facts, that is, it tries to -instantiate all schematic type variables with fixed types occurring -in the problem. This is a (possibly nonterminating) fixed-point -construction whose cycles are limited by the following option. -\ - -declare [[ monomorph_max_rounds = 5 ]] - -text \ -In addition, the number of generated monomorphic instances is limited -by the following option. -\ - -declare [[ monomorph_max_new_instances = 500 ]] - - - -subsection \Certificates\ - -text \ -By setting the option \old_smt_certificates\ to the name of a file, -all following applications of an SMT solver a cached in that file. -Any further application of the same SMT solver (using the very same -configuration) re-uses the cached certificate instead of invoking the -solver. An empty string disables caching certificates. - -The filename should be given as an explicit path. It is good -practice to use the name of the current theory (with ending -\.certs\ instead of \.thy\) as the certificates file. -Certificate files should be used at most once in a certain theory context, -to avoid race conditions with other concurrent accesses. -\ - -declare [[ old_smt_certificates = "" ]] - -text \ -The option \old_smt_read_only_certificates\ controls whether only -stored certificates are should be used or invocation of an SMT solver -is allowed. When set to \true\, no SMT solver will ever be -invoked and only the existing certificates found in the configured -cache are used; when set to \false\ and there is no cached -certificate for some proposition, then the configured SMT solver is -invoked. -\ - -declare [[ old_smt_read_only_certificates = false ]] - - - -subsection \Tracing\ - -text \ -The SMT method, when applied, traces important information. To -make it entirely silent, set the following option to \false\. -\ - -declare [[ old_smt_verbose = true ]] - -text \ -For tracing the generated problem file given to the SMT solver as -well as the returned result of the solver, the option -\old_smt_trace\ should be set to \true\. -\ - -declare [[ old_smt_trace = false ]] - -text \ -From the set of assumptions given to the SMT solver, those assumptions -used in the proof are traced when the following option is set to -@{term true}. This only works for Z3 when it runs in non-oracle mode -(see options \old_smt_solver\ and \old_smt_oracle\ above). -\ - -declare [[ old_smt_trace_used_facts = false ]] - - - -subsection \Schematic rules for Z3 proof reconstruction\ - -text \ -Several prof rules of Z3 are not very well documented. There are two -lemma groups which can turn failing Z3 proof reconstruction attempts -into succeeding ones: the facts in \z3_rule\ are tried prior to -any implemented reconstruction procedure for all uncertain Z3 proof -rules; the facts in \z3_simp\ are only fed to invocations of -the simplifier when reconstructing theory-specific proof steps. -\ - -lemmas [old_z3_rule] = - refl eq_commute conj_commute disj_commute simp_thms nnf_simps - ring_distribs field_simps times_divide_eq_right times_divide_eq_left - if_True if_False not_not - -lemma [old_z3_rule]: - "(P \ Q) = (\(\P \ \Q))" - "(P \ Q) = (\(\Q \ \P))" - "(\P \ Q) = (\(P \ \Q))" - "(\P \ Q) = (\(\Q \ P))" - "(P \ \Q) = (\(\P \ Q))" - "(P \ \Q) = (\(Q \ \P))" - "(\P \ \Q) = (\(P \ Q))" - "(\P \ \Q) = (\(Q \ P))" - by auto - -lemma [old_z3_rule]: - "(P \ Q) = (Q \ \P)" - "(\P \ Q) = (P \ Q)" - "(\P \ Q) = (Q \ P)" - "(True \ P) = P" - "(P \ True) = True" - "(False \ P) = True" - "(P \ P) = True" - by auto - -lemma [old_z3_rule]: - "((P = Q) \ R) = (R | (Q = (\P)))" - by auto - -lemma [old_z3_rule]: - "(\True) = False" - "(\False) = True" - "(x = x) = True" - "(P = True) = P" - "(True = P) = P" - "(P = False) = (\P)" - "(False = P) = (\P)" - "((\P) = P) = False" - "(P = (\P)) = False" - "((\P) = (\Q)) = (P = Q)" - "\(P = (\Q)) = (P = Q)" - "\((\P) = Q) = (P = Q)" - "(P \ Q) = (Q = (\P))" - "(P = Q) = ((\P \ Q) \ (P \ \Q))" - "(P \ Q) = ((\P \ \Q) \ (P \ Q))" - by auto - -lemma [old_z3_rule]: - "(if P then P else \P) = True" - "(if \P then \P else P) = True" - "(if P then True else False) = P" - "(if P then False else True) = (\P)" - "(if P then Q else True) = ((\P) \ Q)" - "(if P then Q else True) = (Q \ (\P))" - "(if P then Q else \Q) = (P = Q)" - "(if P then Q else \Q) = (Q = P)" - "(if P then \Q else Q) = (P = (\Q))" - "(if P then \Q else Q) = ((\Q) = P)" - "(if \P then x else y) = (if P then y else x)" - "(if P then (if Q then x else y) else x) = (if P \ (\Q) then y else x)" - "(if P then (if Q then x else y) else x) = (if (\Q) \ P then y else x)" - "(if P then (if Q then x else y) else y) = (if P \ Q then x else y)" - "(if P then (if Q then x else y) else y) = (if Q \ P then x else y)" - "(if P then x else if P then y else z) = (if P then x else z)" - "(if P then x else if Q then x else y) = (if P \ Q then x else y)" - "(if P then x else if Q then x else y) = (if Q \ P then x else y)" - "(if P then x = y else x = z) = (x = (if P then y else z))" - "(if P then x = y else y = z) = (y = (if P then x else z))" - "(if P then x = y else z = y) = (y = (if P then x else z))" - by auto - -lemma [old_z3_rule]: - "0 + (x::int) = x" - "x + 0 = x" - "x + x = 2 * x" - "0 * x = 0" - "1 * x = x" - "x + y = y + x" - by auto - -lemma [old_z3_rule]: (* for def-axiom *) - "P = Q \ P \ Q" - "P = Q \ \P \ \Q" - "(\P) = Q \ \P \ Q" - "(\P) = Q \ P \ \Q" - "P = (\Q) \ \P \ Q" - "P = (\Q) \ P \ \Q" - "P \ Q \ P \ \Q" - "P \ Q \ \P \ Q" - "P \ (\Q) \ P \ Q" - "(\P) \ Q \ P \ Q" - "P \ Q \ P \ (\Q)" - "P \ Q \ (\P) \ Q" - "P \ \Q \ P \ Q" - "\P \ Q \ P \ Q" - "P \ y = (if P then x else y)" - "P \ (if P then x else y) = y" - "\P \ x = (if P then x else y)" - "\P \ (if P then x else y) = x" - "P \ R \ \(if P then Q else R)" - "\P \ Q \ \(if P then Q else R)" - "\(if P then Q else R) \ \P \ Q" - "\(if P then Q else R) \ P \ R" - "(if P then Q else R) \ \P \ \Q" - "(if P then Q else R) \ P \ \R" - "(if P then \Q else R) \ \P \ Q" - "(if P then Q else \R) \ P \ R" - by auto - -ML_file "Old_SMT/old_smt_real.ML" -ML_file "Old_SMT/old_smt_word.ML" - -hide_type (open) pattern -hide_const fun_app term_true term_false z3div z3mod -hide_const (open) trigger pat nopat weight - -end diff -r d10f0bbc7ea1 -r f595b7532dc9 src/HOL/Library/Old_SMT/old_smt_builtin.ML --- a/src/HOL/Library/Old_SMT/old_smt_builtin.ML Thu Apr 20 10:45:52 2017 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,231 +0,0 @@ -(* Title: HOL/Library/Old_SMT/old_smt_builtin.ML - Author: Sascha Boehme, TU Muenchen - -Tables of types and terms directly supported by SMT solvers. -*) - -signature OLD_SMT_BUILTIN = -sig - (*for experiments*) - val filter_builtins: (typ -> bool) -> Proof.context -> Proof.context - - (*built-in types*) - val add_builtin_typ: Old_SMT_Utils.class -> - typ * (typ -> string option) * (typ -> int -> string option) -> - Context.generic -> Context.generic - val add_builtin_typ_ext: typ * (typ -> bool) -> Context.generic -> - Context.generic - val dest_builtin_typ: Proof.context -> typ -> string option - val is_builtin_typ_ext: Proof.context -> typ -> bool - - (*built-in numbers*) - val dest_builtin_num: Proof.context -> term -> (string * typ) option - val is_builtin_num: Proof.context -> term -> bool - val is_builtin_num_ext: Proof.context -> term -> bool - - (*built-in functions*) - type 'a bfun = Proof.context -> typ -> term list -> 'a - type bfunr = string * int * term list * (term list -> term) - val add_builtin_fun: Old_SMT_Utils.class -> - (string * typ) * bfunr option bfun -> Context.generic -> Context.generic - val add_builtin_fun': Old_SMT_Utils.class -> term * string -> Context.generic -> - Context.generic - val add_builtin_fun_ext: (string * typ) * term list bfun -> - Context.generic -> Context.generic - val add_builtin_fun_ext': string * typ -> Context.generic -> Context.generic - val add_builtin_fun_ext'': string -> Context.generic -> Context.generic - val dest_builtin_fun: Proof.context -> string * typ -> term list -> - bfunr option - val dest_builtin_eq: Proof.context -> term -> term -> bfunr option - val dest_builtin_pred: Proof.context -> string * typ -> term list -> - bfunr option - val dest_builtin_conn: Proof.context -> string * typ -> term list -> - bfunr option - val dest_builtin: Proof.context -> string * typ -> term list -> bfunr option - val dest_builtin_ext: Proof.context -> string * typ -> term list -> - term list option - val is_builtin_fun: Proof.context -> string * typ -> term list -> bool - val is_builtin_fun_ext: Proof.context -> string * typ -> term list -> bool -end - -structure Old_SMT_Builtin: OLD_SMT_BUILTIN = -struct - - -(* built-in tables *) - -datatype ('a, 'b) kind = Ext of 'a | Int of 'b - -type ('a, 'b) ttab = ((typ * ('a, 'b) kind) Ord_List.T) Old_SMT_Utils.dict - -fun typ_ord ((T, _), (U, _)) = - let - fun tord (TVar _, Type _) = GREATER - | tord (Type _, TVar _) = LESS - | tord (Type (n, Ts), Type (m, Us)) = - if n = m then list_ord tord (Ts, Us) - else Term_Ord.typ_ord (T, U) - | tord TU = Term_Ord.typ_ord TU - in tord (T, U) end - -fun insert_ttab cs T f = - Old_SMT_Utils.dict_map_default (cs, []) - (Ord_List.insert typ_ord (perhaps (try Logic.varifyT_global) T, f)) - -fun merge_ttab ttabp = - Old_SMT_Utils.dict_merge (Ord_List.merge typ_ord) ttabp - -fun lookup_ttab ctxt ttab T = - let fun match (U, _) = Sign.typ_instance (Proof_Context.theory_of ctxt) (T, U) - in - get_first (find_first match) - (Old_SMT_Utils.dict_lookup ttab (Old_SMT_Config.solver_class_of ctxt)) - end - -type ('a, 'b) btab = ('a, 'b) ttab Symtab.table - -fun insert_btab cs n T f = - Symtab.map_default (n, []) (insert_ttab cs T f) - -fun merge_btab btabp = Symtab.join (K merge_ttab) btabp - -fun lookup_btab ctxt btab (n, T) = - (case Symtab.lookup btab n of - NONE => NONE - | SOME ttab => lookup_ttab ctxt ttab T) - -type 'a bfun = Proof.context -> typ -> term list -> 'a - -type bfunr = string * int * term list * (term list -> term) - -structure Builtins = Generic_Data -( - type T = - (typ -> bool, (typ -> string option) * (typ -> int -> string option)) ttab * - (term list bfun, bfunr option bfun) btab - val empty = ([], Symtab.empty) - val extend = I - fun merge ((t1, b1), (t2, b2)) = (merge_ttab (t1, t2), merge_btab (b1, b2)) -) - -fun filter_ttab keep_T = map (apsnd (filter (keep_T o fst))) - -fun filter_builtins keep_T = - Context.proof_map (Builtins.map (fn (ttab, btab) => - (filter_ttab keep_T ttab, Symtab.map (K (filter_ttab keep_T)) btab))) - - -(* built-in types *) - -fun add_builtin_typ cs (T, f, g) = - Builtins.map (apfst (insert_ttab cs T (Int (f, g)))) - -fun add_builtin_typ_ext (T, f) = - Builtins.map (apfst (insert_ttab Old_SMT_Utils.basicC T (Ext f))) - -fun lookup_builtin_typ ctxt = - lookup_ttab ctxt (fst (Builtins.get (Context.Proof ctxt))) - -fun dest_builtin_typ ctxt T = - (case lookup_builtin_typ ctxt T of - SOME (_, Int (f, _)) => f T - | _ => NONE) - -fun is_builtin_typ_ext ctxt T = - (case lookup_builtin_typ ctxt T of - SOME (_, Int (f, _)) => is_some (f T) - | SOME (_, Ext f) => f T - | NONE => false) - - -(* built-in numbers *) - -fun dest_builtin_num ctxt t = - (case try HOLogic.dest_number t of - NONE => NONE - | SOME (T, i) => - if i < 0 then NONE else - (case lookup_builtin_typ ctxt T of - SOME (_, Int (_, g)) => g T i |> Option.map (rpair T) - | _ => NONE)) - -val is_builtin_num = is_some oo dest_builtin_num - -fun is_builtin_num_ext ctxt t = - (case try HOLogic.dest_number t of - NONE => false - | SOME (T, _) => is_builtin_typ_ext ctxt T) - - -(* built-in functions *) - -fun add_builtin_fun cs ((n, T), f) = - Builtins.map (apsnd (insert_btab cs n T (Int f))) - -fun add_builtin_fun' cs (t, n) = - let - val c as (m, T) = Term.dest_Const t - fun app U ts = Term.list_comb (Const (m, U), ts) - fun bfun _ U ts = SOME (n, length (Term.binder_types T), ts, app U) - in add_builtin_fun cs (c, bfun) end - -fun add_builtin_fun_ext ((n, T), f) = - Builtins.map (apsnd (insert_btab Old_SMT_Utils.basicC n T (Ext f))) - -fun add_builtin_fun_ext' c = add_builtin_fun_ext (c, fn _ => fn _ => I) - -fun add_builtin_fun_ext'' n context = - let val thy = Context.theory_of context - in add_builtin_fun_ext' (n, Sign.the_const_type thy n) context end - -fun lookup_builtin_fun ctxt = - lookup_btab ctxt (snd (Builtins.get (Context.Proof ctxt))) - -fun dest_builtin_fun ctxt (c as (_, T)) ts = - (case lookup_builtin_fun ctxt c of - SOME (_, Int f) => f ctxt T ts - | _ => NONE) - -fun dest_builtin_eq ctxt t u = - let - val aT = TFree (Name.aT, @{sort type}) - val c = (@{const_name HOL.eq}, aT --> aT --> @{typ bool}) - fun mk ts = Term.list_comb (HOLogic.eq_const (Term.fastype_of (hd ts)), ts) - in - dest_builtin_fun ctxt c [] - |> Option.map (fn (n, i, _, _) => (n, i, [t, u], mk)) - end - -fun special_builtin_fun pred ctxt (c as (_, T)) ts = - if pred (Term.body_type T, Term.binder_types T) then - dest_builtin_fun ctxt c ts - else NONE - -fun dest_builtin_pred ctxt = special_builtin_fun (equal @{typ bool} o fst) ctxt - -fun dest_builtin_conn ctxt = - special_builtin_fun (forall (equal @{typ bool}) o (op ::)) ctxt - -fun dest_builtin ctxt c ts = - let val t = Term.list_comb (Const c, ts) - in - (case dest_builtin_num ctxt t of - SOME (n, _) => SOME (n, 0, [], K t) - | NONE => dest_builtin_fun ctxt c ts) - end - -fun dest_builtin_fun_ext ctxt (c as (_, T)) ts = - (case lookup_builtin_fun ctxt c of - SOME (_, Int f) => f ctxt T ts |> Option.map (fn (_, _, us, _) => us) - | SOME (_, Ext f) => SOME (f ctxt T ts) - | NONE => NONE) - -fun dest_builtin_ext ctxt c ts = - if is_builtin_num_ext ctxt (Term.list_comb (Const c, ts)) then SOME [] - else dest_builtin_fun_ext ctxt c ts - -fun is_builtin_fun ctxt c ts = is_some (dest_builtin_fun ctxt c ts) - -fun is_builtin_fun_ext ctxt c ts = is_some (dest_builtin_fun_ext ctxt c ts) - -end diff -r d10f0bbc7ea1 -r f595b7532dc9 src/HOL/Library/Old_SMT/old_smt_config.ML --- a/src/HOL/Library/Old_SMT/old_smt_config.ML Thu Apr 20 10:45:52 2017 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,254 +0,0 @@ -(* Title: HOL/Library/Old_SMT/old_smt_config.ML - Author: Sascha Boehme, TU Muenchen - -Configuration options and diagnostic tools for SMT. -*) - -signature OLD_SMT_CONFIG = -sig - (*solver*) - type solver_info = { - name: string, - class: Proof.context -> Old_SMT_Utils.class, - avail: unit -> bool, - options: Proof.context -> string list } - val add_solver: solver_info -> Context.generic -> Context.generic - val set_solver_options: string * string -> Context.generic -> Context.generic - val is_available: Proof.context -> string -> bool - val available_solvers_of: Proof.context -> string list - val select_solver: string -> Context.generic -> Context.generic - val solver_of: Proof.context -> string - val solver_class_of: Proof.context -> Old_SMT_Utils.class - val solver_options_of: Proof.context -> string list - - (*options*) - val oracle: bool Config.T - val datatypes: bool Config.T - val timeout: real Config.T - val random_seed: int Config.T - val read_only_certificates: bool Config.T - val verbose: bool Config.T - val trace: bool Config.T - val trace_used_facts: bool Config.T - val monomorph_limit: int Config.T - val monomorph_instances: int Config.T - val infer_triggers: bool Config.T - val filter_only_facts: bool Config.T - val debug_files: string Config.T - - (*tools*) - val with_timeout: Proof.context -> ('a -> 'b) -> 'a -> 'b - - (*diagnostics*) - val trace_msg: Proof.context -> ('a -> string) -> 'a -> unit - val verbose_msg: Proof.context -> ('a -> string) -> 'a -> unit - - (*certificates*) - val select_certificates: string -> Context.generic -> Context.generic - val certificates_of: Proof.context -> Cache_IO.cache option - - (*setup*) - val setup: theory -> theory - val print_setup: Proof.context -> unit -end - -structure Old_SMT_Config: OLD_SMT_CONFIG = -struct - -(* solver *) - -type solver_info = { - name: string, - class: Proof.context -> Old_SMT_Utils.class, - avail: unit -> bool, - options: Proof.context -> string list } - -(* FIXME just one data slot (record) per program unit *) -structure Solvers = Generic_Data -( - type T = (solver_info * string list) Symtab.table * string option - val empty = (Symtab.empty, NONE) - val extend = I - fun merge ((ss1, s1), (ss2, s2)) = - (Symtab.merge (K true) (ss1, ss2), merge_options (s1, s2)) -) - -fun set_solver_options (name, options) = - let val opts = String.tokens (Symbol.is_ascii_blank o str) options - in Solvers.map (apfst (Symtab.map_entry name (apsnd (K opts)))) end - -fun add_solver (info as {name, ...} : solver_info) context = - if Symtab.defined (fst (Solvers.get context)) name then - error ("Solver already registered: " ^ quote name) - else - context - |> Solvers.map (apfst (Symtab.update (name, (info, [])))) - |> Context.map_theory (Attrib.setup (Binding.name ("old_" ^ name ^ "_options")) - (Scan.lift (@{keyword "="} |-- Args.name) >> - (Thm.declaration_attribute o K o set_solver_options o pair name)) - ("additional command line options for SMT solver " ^ quote name)) - -fun all_solvers_of ctxt = Symtab.keys (fst (Solvers.get (Context.Proof ctxt))) - -fun solver_name_of ctxt = snd (Solvers.get (Context.Proof ctxt)) - -fun is_available ctxt name = - (case Symtab.lookup (fst (Solvers.get (Context.Proof ctxt))) name of - SOME ({avail, ...}, _) => avail () - | NONE => false) - -fun available_solvers_of ctxt = - filter (is_available ctxt) (all_solvers_of ctxt) - -fun warn_solver (Context.Proof ctxt) name = - if Context_Position.is_visible ctxt then - warning ("The SMT solver " ^ quote name ^ " is not installed.") - else () - | warn_solver _ _ = (); - -fun select_solver name context = - let - val ctxt = Context.proof_of context - val upd = Solvers.map (apsnd (K (SOME name))) - in - if not (member (op =) (all_solvers_of ctxt) name) then - error ("Trying to select unknown solver: " ^ quote name) - else if not (is_available ctxt name) then - (warn_solver context name; upd context) - else upd context - end - -fun no_solver_err () = error "No SMT solver selected" - -fun solver_of ctxt = - (case solver_name_of ctxt of - SOME name => name - | NONE => no_solver_err ()) - -fun solver_info_of default select ctxt = - (case Solvers.get (Context.Proof ctxt) of - (solvers, SOME name) => select (Symtab.lookup solvers name) - | (_, NONE) => default ()) - -fun solver_class_of ctxt = - let fun class_of ({class, ...}: solver_info, _) = class ctxt - in solver_info_of no_solver_err (class_of o the) ctxt end - -fun solver_options_of ctxt = - let - fun all_options NONE = [] - | all_options (SOME ({options, ...} : solver_info, opts)) = - opts @ options ctxt - in solver_info_of (K []) all_options ctxt end - -val setup_solver = - Attrib.setup @{binding old_smt_solver} - (Scan.lift (@{keyword "="} |-- Args.name) >> - (Thm.declaration_attribute o K o select_solver)) - "SMT solver configuration" - - -(* options *) - -val oracle = Attrib.setup_config_bool @{binding old_smt_oracle} (K true) -val datatypes = Attrib.setup_config_bool @{binding old_smt_datatypes} (K false) -val timeout = Attrib.setup_config_real @{binding old_smt_timeout} (K 30.0) -val random_seed = Attrib.setup_config_int @{binding old_smt_random_seed} (K 1) -val read_only_certificates = Attrib.setup_config_bool @{binding old_smt_read_only_certificates} (K false) -val verbose = Attrib.setup_config_bool @{binding old_smt_verbose} (K true) -val trace = Attrib.setup_config_bool @{binding old_smt_trace} (K false) -val trace_used_facts = Attrib.setup_config_bool @{binding old_smt_trace_used_facts} (K false) -val monomorph_limit = Attrib.setup_config_int @{binding old_smt_monomorph_limit} (K 10) -val monomorph_instances = Attrib.setup_config_int @{binding old_smt_monomorph_instances} (K 500) -val infer_triggers = Attrib.setup_config_bool @{binding old_smt_infer_triggers} (K false) -val filter_only_facts = Attrib.setup_config_bool @{binding old_smt_filter_only_facts} (K false) -val debug_files = Attrib.setup_config_string @{binding old_smt_debug_files} (K "") - - -(* diagnostics *) - -fun cond_trace flag f x = if flag then tracing ("SMT: " ^ f x) else () - -fun verbose_msg ctxt = cond_trace (Config.get ctxt verbose) - -fun trace_msg ctxt = cond_trace (Config.get ctxt trace) - - -(* tools *) - -fun with_timeout ctxt f x = - Timeout.apply (seconds (Config.get ctxt timeout)) f x - handle Timeout.TIMEOUT _ => raise Old_SMT_Failure.SMT Old_SMT_Failure.Time_Out - - -(* certificates *) - -(* FIXME just one data slot (record) per program unit *) -structure Certificates = Generic_Data -( - type T = Cache_IO.cache option - val empty = NONE - val extend = I - fun merge (s, _) = s (* FIXME merge options!? *) -) - -val get_certificates_path = - Option.map (Cache_IO.cache_path_of) o Certificates.get o Context.Proof - -fun select_certificates name context = context |> Certificates.put ( - if name = "" then NONE - else - Path.explode name - |> Path.append (Resources.master_directory (Context.theory_of context)) - |> SOME o Cache_IO.unsynchronized_init) - -val certificates_of = Certificates.get o Context.Proof - -val setup_certificates = - Attrib.setup @{binding old_smt_certificates} - (Scan.lift (@{keyword "="} |-- Args.name) >> - (Thm.declaration_attribute o K o select_certificates)) - "SMT certificates configuration" - - -(* setup *) - -val setup = - setup_solver #> - setup_certificates - -fun print_setup ctxt = - let - fun string_of_bool b = if b then "true" else "false" - - val names = available_solvers_of ctxt - val ns = if null names then ["(none)"] else sort_strings names - val n = the_default "(none)" (solver_name_of ctxt) - val opts = solver_options_of ctxt - - val t = string_of_real (Config.get ctxt timeout) - - val certs_filename = - (case get_certificates_path ctxt of - SOME path => Path.print path - | NONE => "(disabled)") - in - Pretty.writeln (Pretty.big_list "SMT setup:" [ - Pretty.str ("Current SMT solver: " ^ n), - Pretty.str ("Current SMT solver options: " ^ space_implode " " opts), - Pretty.str_list "Available SMT solvers: " "" ns, - Pretty.str ("Current timeout: " ^ t ^ " seconds"), - Pretty.str ("With proofs: " ^ - string_of_bool (not (Config.get ctxt oracle))), - Pretty.str ("Certificates cache: " ^ certs_filename), - Pretty.str ("Fixed certificates: " ^ - string_of_bool (Config.get ctxt read_only_certificates))]) - end - -val _ = - Outer_Syntax.command @{command_keyword old_smt_status} - "show the available SMT solvers, the currently selected SMT solver, \ - \and the values of SMT configuration options" - (Scan.succeed (Toplevel.keep (print_setup o Toplevel.context_of))) - -end diff -r d10f0bbc7ea1 -r f595b7532dc9 src/HOL/Library/Old_SMT/old_smt_datatypes.ML --- a/src/HOL/Library/Old_SMT/old_smt_datatypes.ML Thu Apr 20 10:45:52 2017 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,94 +0,0 @@ -(* Title: HOL/Library/Old_SMT/old_smt_datatypes.ML - Author: Sascha Boehme, TU Muenchen - -Collector functions for common type declarations and their representation -as algebraic datatypes. -*) - -signature OLD_SMT_DATATYPES = -sig - val add_decls: typ -> - (typ * (term * term list) list) list list * Proof.context -> - (typ * (term * term list) list) list list * Proof.context -end - -structure Old_SMT_Datatypes: OLD_SMT_DATATYPES = -struct - -fun mk_selectors T Ts = - Variable.variant_fixes (replicate (length Ts) "select") - #>> map2 (fn U => fn n => Free (n, T --> U)) Ts - - -(* free constructor type declarations *) - -fun get_ctr_sugar_decl ({ctrs, ...} : Ctr_Sugar.ctr_sugar) T Ts ctxt = - let - fun mk_constr ctr0 = - let val ctr = Ctr_Sugar.mk_ctr Ts ctr0 in - mk_selectors T (binder_types (fastype_of ctr)) #>> pair ctr - end - in - fold_map mk_constr ctrs ctxt - |>> (pair T #> single) - end - - -(* typedef declarations *) - -fun get_typedef_decl (({Abs_name, Rep_name, abs_type, rep_type, ...}, {Abs_inverse, ...}) - : Typedef.info) T Ts = - if can (curry (op RS) @{thm UNIV_I}) Abs_inverse then - let - val env = snd (Term.dest_Type abs_type) ~~ Ts - val instT = Term.map_atyps (perhaps (AList.lookup (op =) env)) - - val constr = Const (Abs_name, instT (rep_type --> abs_type)) - val select = Const (Rep_name, instT (abs_type --> rep_type)) - in [(T, [(constr, [select])])] end - else - [] - - -(* collection of declarations *) - -fun declared declss T = exists (exists (equal T o fst)) declss -fun declared' dss T = exists (exists (equal T o fst) o snd) dss - -fun get_decls T n Ts ctxt = - (case Ctr_Sugar.ctr_sugar_of ctxt n of - SOME ctr_sugar => get_ctr_sugar_decl ctr_sugar T Ts ctxt - | NONE => - (case Typedef.get_info ctxt n of - [] => ([], ctxt) - | info :: _ => (get_typedef_decl info T Ts, ctxt))) - -fun add_decls T (declss, ctxt) = - let - fun depends Ts ds = exists (member (op =) (map fst ds)) Ts - - fun add (TFree _) = I - | add (TVar _) = I - | add (T as Type (@{type_name fun}, _)) = - fold add (Term.body_type T :: Term.binder_types T) - | add @{typ bool} = I - | add (T as Type (n, Ts)) = (fn (dss, ctxt1) => - if declared declss T orelse declared' dss T then (dss, ctxt1) - else if Old_SMT_Builtin.is_builtin_typ_ext ctxt1 T then (dss, ctxt1) - else - (case get_decls T n Ts ctxt1 of - ([], _) => (dss, ctxt1) - | (ds, ctxt2) => - let - val constrTs = - maps (map (snd o Term.dest_Const o fst) o snd) ds - val Us = fold (union (op =) o Term.binder_types) constrTs [] - - fun ins [] = [(Us, ds)] - | ins ((Uds as (Us', _)) :: Udss) = - if depends Us' ds then (Us, ds) :: Uds :: Udss - else Uds :: ins Udss - in fold add Us (ins dss, ctxt2) end)) - in add T ([], ctxt) |>> append declss o map snd end - -end diff -r d10f0bbc7ea1 -r f595b7532dc9 src/HOL/Library/Old_SMT/old_smt_failure.ML --- a/src/HOL/Library/Old_SMT/old_smt_failure.ML Thu Apr 20 10:45:52 2017 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,61 +0,0 @@ -(* Title: HOL/Library/Old_SMT/old_smt_failure.ML - Author: Sascha Boehme, TU Muenchen - -Failures and exception of SMT. -*) - -signature OLD_SMT_FAILURE = -sig - type counterexample = { - is_real_cex: bool, - free_constraints: term list, - const_defs: term list} - datatype failure = - Counterexample of counterexample | - Time_Out | - Out_Of_Memory | - Abnormal_Termination of int | - Other_Failure of string - val pretty_counterexample: Proof.context -> counterexample -> Pretty.T - val string_of_failure: Proof.context -> failure -> string - exception SMT of failure -end - -structure Old_SMT_Failure: OLD_SMT_FAILURE = -struct - -type counterexample = { - is_real_cex: bool, - free_constraints: term list, - const_defs: term list} - -datatype failure = - Counterexample of counterexample | - Time_Out | - Out_Of_Memory | - Abnormal_Termination of int | - Other_Failure of string - -fun pretty_counterexample ctxt {is_real_cex, free_constraints, const_defs} = - let - val msg = - if is_real_cex then "Counterexample found (possibly spurious)" - else "Potential counterexample found" - in - if null free_constraints andalso null const_defs then Pretty.str msg - else - Pretty.big_list (msg ^ ":") - (map (Syntax.pretty_term ctxt) (free_constraints @ const_defs)) - end - -fun string_of_failure ctxt (Counterexample cex) = - Pretty.string_of (pretty_counterexample ctxt cex) - | string_of_failure _ Time_Out = "Timed out" - | string_of_failure _ Out_Of_Memory = "Ran out of memory" - | string_of_failure _ (Abnormal_Termination err) = - "Solver terminated abnormally with error code " ^ string_of_int err - | string_of_failure _ (Other_Failure msg) = msg - -exception SMT of failure - -end diff -r d10f0bbc7ea1 -r f595b7532dc9 src/HOL/Library/Old_SMT/old_smt_normalize.ML --- a/src/HOL/Library/Old_SMT/old_smt_normalize.ML Thu Apr 20 10:45:52 2017 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,652 +0,0 @@ -(* Title: HOL/Library/Old_SMT/old_smt_normalize.ML - Author: Sascha Boehme, TU Muenchen - -Normalization steps on theorems required by SMT solvers. -*) - -signature OLD_SMT_NORMALIZE = -sig - val drop_fact_warning: Proof.context -> thm -> unit - val atomize_conv: Proof.context -> conv - type extra_norm = Proof.context -> thm list * thm list -> thm list * thm list - val add_extra_norm: Old_SMT_Utils.class * extra_norm -> Context.generic -> - Context.generic - val normalize: (int * (int option * thm)) list -> Proof.context -> - (int * thm) list * Proof.context - val setup: theory -> theory -end - -structure Old_SMT_Normalize: OLD_SMT_NORMALIZE = -struct - -fun drop_fact_warning ctxt = - Old_SMT_Config.verbose_msg ctxt (prefix "Warning: dropping assumption: " o - Thm.string_of_thm ctxt) - - -(* general theorem normalizations *) - -(** instantiate elimination rules **) - -local - val (cpfalse, cfalse) = - `Old_SMT_Utils.mk_cprop (Thm.cterm_of @{context} @{const False}) - - fun inst f ct thm = - let val cv = f (Drule.strip_imp_concl (Thm.cprop_of thm)) - in Thm.instantiate ([], [(dest_Var (Thm.term_of cv), ct)]) thm end -in - -fun instantiate_elim thm = - (case Thm.concl_of thm of - @{const Trueprop} $ Var (_, @{typ bool}) => inst Thm.dest_arg cfalse thm - | Var _ => inst I cpfalse thm - | _ => thm) - -end - - -(** normalize definitions **) - -fun norm_def thm = - (case Thm.prop_of thm of - @{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ _ $ Abs _) => - norm_def (thm RS @{thm fun_cong}) - | Const (@{const_name Pure.eq}, _) $ _ $ Abs _ => - norm_def (thm RS @{thm meta_eq_to_obj_eq}) - | _ => thm) - - -(** atomization **) - -fun atomize_conv ctxt ct = - (case Thm.term_of ct of - @{const Pure.imp} $ _ $ _ => - Conv.binop_conv (atomize_conv ctxt) then_conv - Conv.rewr_conv @{thm atomize_imp} - | Const (@{const_name Pure.eq}, _) $ _ $ _ => - Conv.binop_conv (atomize_conv ctxt) then_conv - Conv.rewr_conv @{thm atomize_eq} - | Const (@{const_name Pure.all}, _) $ Abs _ => - Conv.binder_conv (atomize_conv o snd) ctxt then_conv - Conv.rewr_conv @{thm atomize_all} - | _ => Conv.all_conv) ct - -val setup_atomize = - fold Old_SMT_Builtin.add_builtin_fun_ext'' [@{const_name Pure.imp}, - @{const_name Pure.eq}, @{const_name Pure.all}, @{const_name Trueprop}] - - -(** unfold special quantifiers **) - -local - val ex1_def = mk_meta_eq @{lemma - "Ex1 = (%P. EX x. P x & (ALL y. P y --> y = x))" - by (rule ext) (simp only: Ex1_def)} - - val ball_def = mk_meta_eq @{lemma "Ball = (%A P. ALL x. x : A --> P x)" - by (rule ext)+ (rule Ball_def)} - - val bex_def = mk_meta_eq @{lemma "Bex = (%A P. EX x. x : A & P x)" - by (rule ext)+ (rule Bex_def)} - - val special_quants = [(@{const_name Ex1}, ex1_def), - (@{const_name Ball}, ball_def), (@{const_name Bex}, bex_def)] - - fun special_quant (Const (n, _)) = AList.lookup (op =) special_quants n - | special_quant _ = NONE - - fun special_quant_conv _ ct = - (case special_quant (Thm.term_of ct) of - SOME thm => Conv.rewr_conv thm - | NONE => Conv.all_conv) ct -in - -fun unfold_special_quants_conv ctxt = - Old_SMT_Utils.if_exists_conv (is_some o special_quant) - (Conv.top_conv special_quant_conv ctxt) - -val setup_unfolded_quants = - fold (Old_SMT_Builtin.add_builtin_fun_ext'' o fst) special_quants - -end - - -(** trigger inference **) - -local - (*** check trigger syntax ***) - - fun dest_trigger (Const (@{const_name pat}, _) $ _) = SOME true - | dest_trigger (Const (@{const_name nopat}, _) $ _) = SOME false - | dest_trigger _ = NONE - - fun eq_list [] = false - | eq_list (b :: bs) = forall (equal b) bs - - fun proper_trigger t = - t - |> these o try HOLogic.dest_list - |> map (map_filter dest_trigger o these o try HOLogic.dest_list) - |> (fn [] => false | bss => forall eq_list bss) - - fun proper_quant inside f t = - (case t of - Const (@{const_name All}, _) $ Abs (_, _, u) => proper_quant true f u - | Const (@{const_name Ex}, _) $ Abs (_, _, u) => proper_quant true f u - | @{const trigger} $ p $ u => - (if inside then f p else false) andalso proper_quant false f u - | Abs (_, _, u) => proper_quant false f u - | u1 $ u2 => proper_quant false f u1 andalso proper_quant false f u2 - | _ => true) - - fun check_trigger_error ctxt t = - error ("SMT triggers must only occur under quantifier and multipatterns " ^ - "must have the same kind: " ^ Syntax.string_of_term ctxt t) - - fun check_trigger_conv ctxt ct = - if proper_quant false proper_trigger (Old_SMT_Utils.term_of ct) then - Conv.all_conv ct - else check_trigger_error ctxt (Thm.term_of ct) - - - (*** infer simple triggers ***) - - fun dest_cond_eq ct = - (case Thm.term_of ct of - Const (@{const_name HOL.eq}, _) $ _ $ _ => Thm.dest_binop ct - | @{const HOL.implies} $ _ $ _ => dest_cond_eq (Thm.dest_arg ct) - | _ => raise CTERM ("no equation", [ct])) - - fun get_constrs thy (Type (n, _)) = these (Old_Datatype_Data.get_constrs thy n) - | get_constrs _ _ = [] - - fun is_constr thy (n, T) = - let fun match (m, U) = m = n andalso Sign.typ_instance thy (T, U) - in can (the o find_first match o get_constrs thy o Term.body_type) T end - - fun is_constr_pat thy t = - (case Term.strip_comb t of - (Free _, []) => true - | (Const c, ts) => is_constr thy c andalso forall (is_constr_pat thy) ts - | _ => false) - - fun is_simp_lhs ctxt t = - (case Term.strip_comb t of - (Const c, ts as _ :: _) => - not (Old_SMT_Builtin.is_builtin_fun_ext ctxt c ts) andalso - forall (is_constr_pat (Proof_Context.theory_of ctxt)) ts - | _ => false) - - fun has_all_vars vs t = - subset (op aconv) (vs, map Free (Term.add_frees t [])) - - fun minimal_pats vs ct = - if has_all_vars vs (Thm.term_of ct) then - (case Thm.term_of ct of - _ $ _ => - (case apply2 (minimal_pats vs) (Thm.dest_comb ct) of - ([], []) => [[ct]] - | (ctss, ctss') => union (eq_set (op aconvc)) ctss ctss') - | _ => []) - else [] - - fun proper_mpat _ _ _ [] = false - | proper_mpat thy gen u cts = - let - val tps = (op ~~) (`gen (map Thm.term_of cts)) - fun some_match u = tps |> exists (fn (t', t) => - Pattern.matches thy (t', u) andalso not (t aconv u)) - in not (Term.exists_subterm some_match u) end - - val pat = - Old_SMT_Utils.mk_const_pat @{theory} @{const_name pat} Old_SMT_Utils.destT1 - fun mk_pat ct = Thm.apply (Old_SMT_Utils.instT' ct pat) ct - - fun mk_clist T = apply2 (Thm.cterm_of @{context}) (HOLogic.cons_const T, HOLogic.nil_const T) - fun mk_list (ccons, cnil) f cts = fold_rev (Thm.mk_binop ccons o f) cts cnil - val mk_pat_list = mk_list (mk_clist @{typ pattern}) - val mk_mpat_list = mk_list (mk_clist @{typ "pattern list"}) - fun mk_trigger ctss = mk_mpat_list (mk_pat_list mk_pat) ctss - - val trigger_eq = - mk_meta_eq @{lemma "p = trigger t p" by (simp add: trigger_def)} - - fun insert_trigger_conv [] ct = Conv.all_conv ct - | insert_trigger_conv ctss ct = - let val (ctr, cp) = Thm.dest_binop (Thm.rhs_of trigger_eq) ||> rpair ct - in Thm.instantiate ([], map (apfst (dest_Var o Thm.term_of)) [cp, (ctr, mk_trigger ctss)]) trigger_eq end - - fun infer_trigger_eq_conv outer_ctxt (ctxt, cvs) ct = - let - val (lhs, rhs) = dest_cond_eq ct - - val vs = map Thm.term_of cvs - val thy = Proof_Context.theory_of ctxt - - fun get_mpats ct = - if is_simp_lhs ctxt (Thm.term_of ct) then minimal_pats vs ct - else [] - val gen = Variable.export_terms ctxt outer_ctxt - val filter_mpats = filter (proper_mpat thy gen (Thm.term_of rhs)) - - in insert_trigger_conv (filter_mpats (get_mpats lhs)) ct end - - fun has_trigger (@{const trigger} $ _ $ _) = true - | has_trigger _ = false - - fun try_trigger_conv cv ct = - if Old_SMT_Utils.under_quant has_trigger (Old_SMT_Utils.term_of ct) then - Conv.all_conv ct - else Conv.try_conv cv ct - - fun infer_trigger_conv ctxt = - if Config.get ctxt Old_SMT_Config.infer_triggers then - try_trigger_conv - (Old_SMT_Utils.under_quant_conv (infer_trigger_eq_conv ctxt) ctxt) - else Conv.all_conv -in - -fun trigger_conv ctxt = - Old_SMT_Utils.prop_conv - (check_trigger_conv ctxt then_conv infer_trigger_conv ctxt) - -val setup_trigger = - fold Old_SMT_Builtin.add_builtin_fun_ext'' - [@{const_name pat}, @{const_name nopat}, @{const_name trigger}] - -end - - -(** adding quantifier weights **) - -local - (*** check weight syntax ***) - - val has_no_weight = - not o Term.exists_subterm (fn @{const weight} => true | _ => false) - - fun is_weight (@{const weight} $ w $ t) = - (case try HOLogic.dest_number w of - SOME (_, i) => i >= 0 andalso has_no_weight t - | _ => false) - | is_weight t = has_no_weight t - - fun proper_trigger (@{const trigger} $ _ $ t) = is_weight t - | proper_trigger t = is_weight t - - fun check_weight_error ctxt t = - error ("SMT weight must be a non-negative number and must only occur " ^ - "under the top-most quantifier and an optional trigger: " ^ - Syntax.string_of_term ctxt t) - - fun check_weight_conv ctxt ct = - if Old_SMT_Utils.under_quant proper_trigger (Old_SMT_Utils.term_of ct) then - Conv.all_conv ct - else check_weight_error ctxt (Thm.term_of ct) - - - (*** insertion of weights ***) - - fun under_trigger_conv cv ct = - (case Thm.term_of ct of - @{const trigger} $ _ $ _ => Conv.arg_conv cv - | _ => cv) ct - - val weight_eq = - mk_meta_eq @{lemma "p = weight i p" by (simp add: weight_def)} - fun mk_weight_eq w = - let val cv = Thm.dest_arg1 (Thm.rhs_of weight_eq) - in - Thm.instantiate ([], [(dest_Var (Thm.term_of cv), Numeral.mk_cnumber @{ctyp int} w)]) - weight_eq - end - - fun add_weight_conv NONE _ = Conv.all_conv - | add_weight_conv (SOME weight) ctxt = - let val cv = Conv.rewr_conv (mk_weight_eq weight) - in Old_SMT_Utils.under_quant_conv (K (under_trigger_conv cv)) ctxt end -in - -fun weight_conv weight ctxt = - Old_SMT_Utils.prop_conv - (check_weight_conv ctxt then_conv add_weight_conv weight ctxt) - -val setup_weight = Old_SMT_Builtin.add_builtin_fun_ext'' @{const_name weight} - -end - - -(** combined general normalizations **) - -fun gen_normalize1_conv ctxt weight = - atomize_conv ctxt then_conv - unfold_special_quants_conv ctxt then_conv - Thm.beta_conversion true then_conv - trigger_conv ctxt then_conv - weight_conv weight ctxt - -fun gen_normalize1 ctxt weight thm = - thm - |> instantiate_elim - |> norm_def - |> Conv.fconv_rule (Thm.beta_conversion true then_conv Thm.eta_conversion) - |> Drule.forall_intr_vars - |> Conv.fconv_rule (gen_normalize1_conv ctxt weight) - -fun gen_norm1_safe ctxt (i, (weight, thm)) = - (case try (gen_normalize1 ctxt weight) thm of - SOME thm' => SOME (i, thm') - | NONE => (drop_fact_warning ctxt thm; NONE)) - -fun gen_normalize ctxt iwthms = map_filter (gen_norm1_safe ctxt) iwthms - - - -(* unfolding of definitions and theory-specific rewritings *) - -fun expand_head_conv cv ct = - (case Thm.term_of ct of - _ $ _ => - Conv.fun_conv (expand_head_conv cv) then_conv - Conv.try_conv (Thm.beta_conversion false) - | _ => cv) ct - - -(** rewrite bool case expressions as if expressions **) - -local - fun is_case_bool (Const (@{const_name "bool.case_bool"}, _)) = true - | is_case_bool _ = false - - val thm = mk_meta_eq @{lemma - "case_bool = (%x y P. if P then x else y)" by (rule ext)+ simp} - - fun unfold_conv _ = - Old_SMT_Utils.if_true_conv (is_case_bool o Term.head_of) - (expand_head_conv (Conv.rewr_conv thm)) -in - -fun rewrite_case_bool_conv ctxt = - Old_SMT_Utils.if_exists_conv is_case_bool (Conv.top_conv unfold_conv ctxt) - -val setup_case_bool = - Old_SMT_Builtin.add_builtin_fun_ext'' @{const_name "bool.case_bool"} - -end - - -(** unfold abs, min and max **) - -local - val abs_def = mk_meta_eq @{lemma - "abs = (%a::'a::abs_if. if a < 0 then - a else a)" - by (rule ext) (rule abs_if)} - - val min_def = mk_meta_eq @{lemma "min = (%a b. if a <= b then a else b)" - by (rule ext)+ (rule min_def)} - - val max_def = mk_meta_eq @{lemma "max = (%a b. if a <= b then b else a)" - by (rule ext)+ (rule max_def)} - - val defs = [(@{const_name min}, min_def), (@{const_name max}, max_def), - (@{const_name abs}, abs_def)] - - fun is_builtinT ctxt T = - Old_SMT_Builtin.is_builtin_typ_ext ctxt (Term.domain_type T) - - fun abs_min_max ctxt (Const (n, T)) = - (case AList.lookup (op =) defs n of - NONE => NONE - | SOME thm => if is_builtinT ctxt T then SOME thm else NONE) - | abs_min_max _ _ = NONE - - fun unfold_amm_conv ctxt ct = - (case abs_min_max ctxt (Term.head_of (Thm.term_of ct)) of - SOME thm => expand_head_conv (Conv.rewr_conv thm) - | NONE => Conv.all_conv) ct -in - -fun unfold_abs_min_max_conv ctxt = - Old_SMT_Utils.if_exists_conv (is_some o abs_min_max ctxt) - (Conv.top_conv unfold_amm_conv ctxt) - -val setup_abs_min_max = fold (Old_SMT_Builtin.add_builtin_fun_ext'' o fst) defs - -end - - -(** embedding of standard natural number operations into integer operations **) - -local - val nat_embedding = @{lemma - "ALL n. nat (int n) = n" - "ALL i. i >= 0 --> int (nat i) = i" - "ALL i. i < 0 --> int (nat i) = 0" - by simp_all} - - val simple_nat_ops = [ - @{const less (nat)}, @{const less_eq (nat)}, - @{const Suc}, @{const plus (nat)}, @{const minus (nat)}] - - val mult_nat_ops = - [@{const times (nat)}, @{const divide (nat)}, @{const modulo (nat)}] - - val nat_ops = simple_nat_ops @ mult_nat_ops - - val nat_consts = nat_ops @ [@{const numeral (nat)}, - @{const zero_class.zero (nat)}, @{const one_class.one (nat)}] - - val nat_int_coercions = [@{const of_nat (int)}, @{const nat}] - - val builtin_nat_ops = nat_int_coercions @ simple_nat_ops - - val is_nat_const = member (op aconv) nat_consts - - fun is_nat_const' @{const of_nat (int)} = true - | is_nat_const' t = is_nat_const t - - val expands = map mk_meta_eq @{lemma - "0 = nat 0" - "1 = nat 1" - "(numeral :: num => nat) = (%i. nat (numeral i))" - "op < = (%a b. int a < int b)" - "op <= = (%a b. int a <= int b)" - "Suc = (%a. nat (int a + 1))" - "op + = (%a b. nat (int a + int b))" - "op - = (%a b. nat (int a - int b))" - "op * = (%a b. nat (int a * int b))" - "op div = (%a b. nat (int a div int b))" - "op mod = (%a b. nat (int a mod int b))" - by (fastforce simp add: nat_mult_distrib nat_div_distrib nat_mod_distrib)+} - - val ints = map mk_meta_eq @{lemma - "int 0 = 0" - "int 1 = 1" - "int (Suc n) = int n + 1" - "int (n + m) = int n + int m" - "int (n - m) = int (nat (int n - int m))" - "int (n * m) = int n * int m" - "int (n div m) = int n div int m" - "int (n mod m) = int n mod int m" - by (auto simp add: of_nat_mult zdiv_int zmod_int)} - - val int_if = mk_meta_eq @{lemma - "int (if P then n else m) = (if P then int n else int m)" - by simp} - - fun mk_number_eq ctxt i lhs = - let - val eq = Old_SMT_Utils.mk_cequals lhs (Numeral.mk_cnumber @{ctyp int} i) - val tac = - Simplifier.simp_tac (put_simpset HOL_ss ctxt addsimps [@{thm of_nat_numeral}]) 1 - in Goal.norm_result ctxt (Goal.prove_internal ctxt [] eq (K tac)) end - - fun ite_conv cv1 cv2 = - Conv.combination_conv (Conv.combination_conv (Conv.arg_conv cv1) cv2) cv2 - - fun int_conv ctxt ct = - (case Thm.term_of ct of - @{const of_nat (int)} $ (n as (@{const numeral (nat)} $ _)) => - Conv.rewr_conv (mk_number_eq ctxt (snd (HOLogic.dest_number n)) ct) - | @{const of_nat (int)} $ _ => - (Conv.rewrs_conv ints then_conv Conv.sub_conv ints_conv ctxt) else_conv - (Conv.rewr_conv int_if then_conv - ite_conv (nat_conv ctxt) (int_conv ctxt)) else_conv - Conv.sub_conv (Conv.top_sweep_conv nat_conv) ctxt - | _ => Conv.no_conv) ct - - and ints_conv ctxt = Conv.top_sweep_conv int_conv ctxt - - and expand_conv ctxt = - Old_SMT_Utils.if_conv (is_nat_const o Term.head_of) - (expand_head_conv (Conv.rewrs_conv expands) then_conv ints_conv ctxt) - (int_conv ctxt) - - and nat_conv ctxt = Old_SMT_Utils.if_exists_conv is_nat_const' - (Conv.top_sweep_conv expand_conv ctxt) - - val uses_nat_int = Term.exists_subterm (member (op aconv) nat_int_coercions) -in - -val nat_as_int_conv = nat_conv - -fun add_nat_embedding thms = - if exists (uses_nat_int o Thm.prop_of) thms then (thms, nat_embedding) - else (thms, []) - -val setup_nat_as_int = - Old_SMT_Builtin.add_builtin_typ_ext (@{typ nat}, K true) #> - fold (Old_SMT_Builtin.add_builtin_fun_ext' o Term.dest_Const) builtin_nat_ops - -end - - -(** normalize numerals **) - -local - (* - rewrite Numeral1 into 1 - rewrite - 0 into 0 - *) - - fun is_irregular_number (Const (@{const_name numeral}, _) $ Const (@{const_name num.One}, _)) = - true - | is_irregular_number (Const (@{const_name uminus}, _) $ Const (@{const_name Groups.zero}, _)) = - true - | is_irregular_number _ = - false; - - fun is_strange_number ctxt t = is_irregular_number t andalso Old_SMT_Builtin.is_builtin_num ctxt t; - - val proper_num_ss = - simpset_of (put_simpset HOL_ss @{context} - addsimps @{thms Num.numeral_One minus_zero}) - - fun norm_num_conv ctxt = - Old_SMT_Utils.if_conv (is_strange_number ctxt) - (Simplifier.rewrite (put_simpset proper_num_ss ctxt)) Conv.no_conv -in - -fun normalize_numerals_conv ctxt = - Old_SMT_Utils.if_exists_conv (is_strange_number ctxt) - (Conv.top_sweep_conv norm_num_conv ctxt) - -end - - -(** combined unfoldings and rewritings **) - -fun unfold_conv ctxt = - rewrite_case_bool_conv ctxt then_conv - unfold_abs_min_max_conv ctxt then_conv - nat_as_int_conv ctxt then_conv - Thm.beta_conversion true - -fun unfold1 ctxt = map (apsnd (Conv.fconv_rule (unfold_conv ctxt))) - -fun burrow_ids f ithms = - let - val (is, thms) = split_list ithms - val (thms', extra_thms) = f thms - in (is ~~ thms') @ map (pair ~1) extra_thms end - -fun unfold2 ctxt ithms = - ithms - |> map (apsnd (Conv.fconv_rule (normalize_numerals_conv ctxt))) - |> burrow_ids add_nat_embedding - - - -(* overall normalization *) - -type extra_norm = Proof.context -> thm list * thm list -> thm list * thm list - -structure Extra_Norms = Generic_Data -( - type T = extra_norm Old_SMT_Utils.dict - val empty = [] - val extend = I - fun merge data = Old_SMT_Utils.dict_merge fst data -) - -fun add_extra_norm (cs, norm) = - Extra_Norms.map (Old_SMT_Utils.dict_update (cs, norm)) - -fun apply_extra_norms ctxt ithms = - let - val cs = Old_SMT_Config.solver_class_of ctxt - val es = Old_SMT_Utils.dict_lookup (Extra_Norms.get (Context.Proof ctxt)) cs - in burrow_ids (fold (fn e => e ctxt) es o rpair []) ithms end - -local - val ignored = member (op =) [@{const_name All}, @{const_name Ex}, - @{const_name Let}, @{const_name If}, @{const_name HOL.eq}] - - val schematic_consts_of = - let - fun collect (@{const trigger} $ p $ t) = - collect_trigger p #> collect t - | collect (t $ u) = collect t #> collect u - | collect (Abs (_, _, t)) = collect t - | collect (t as Const (n, _)) = - if not (ignored n) then Monomorph.add_schematic_consts_of t else I - | collect _ = I - and collect_trigger t = - let val dest = these o try HOLogic.dest_list - in fold (fold collect_pat o dest) (dest t) end - and collect_pat (Const (@{const_name pat}, _) $ t) = collect t - | collect_pat (Const (@{const_name nopat}, _) $ t) = collect t - | collect_pat _ = I - in (fn t => collect t Symtab.empty) end -in - -fun monomorph ctxt xthms = - let val (xs, thms) = split_list xthms - in - map (pair 1) thms - |> Monomorph.monomorph schematic_consts_of ctxt - |> maps (uncurry (map o pair)) o map2 pair xs o map (map snd) - end - -end - -fun normalize iwthms ctxt = - iwthms - |> gen_normalize ctxt - |> unfold1 ctxt - |> monomorph ctxt - |> unfold2 ctxt - |> apply_extra_norms ctxt - |> rpair ctxt - -val setup = Context.theory_map ( - setup_atomize #> - setup_unfolded_quants #> - setup_trigger #> - setup_weight #> - setup_case_bool #> - setup_abs_min_max #> - setup_nat_as_int) - -end diff -r d10f0bbc7ea1 -r f595b7532dc9 src/HOL/Library/Old_SMT/old_smt_real.ML --- a/src/HOL/Library/Old_SMT/old_smt_real.ML Thu Apr 20 10:45:52 2017 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,134 +0,0 @@ -(* Title: HOL/Library/Old_SMT/old_smt_real.ML - Author: Sascha Boehme, TU Muenchen - -SMT setup for reals. -*) - -structure Old_SMT_Real: sig end = -struct - - -(* SMT-LIB logic *) - -fun smtlib_logic ts = - if exists (Term.exists_type (Term.exists_subtype (equal @{typ real}))) ts - then SOME "AUFLIRA" - else NONE - - -(* SMT-LIB and Z3 built-ins *) - -local - fun real_num _ i = SOME (string_of_int i ^ ".0") - - fun is_linear [t] = Old_SMT_Utils.is_number t - | is_linear [t, u] = Old_SMT_Utils.is_number t orelse Old_SMT_Utils.is_number u - | is_linear _ = false - - fun mk_times ts = Term.list_comb (@{const times (real)}, ts) - - fun times _ _ ts = if is_linear ts then SOME ("*", 2, ts, mk_times) else NONE -in - -val setup_builtins = - Old_SMT_Builtin.add_builtin_typ Old_SMTLIB_Interface.smtlibC - (@{typ real}, K (SOME "Real"), real_num) #> - fold (Old_SMT_Builtin.add_builtin_fun' Old_SMTLIB_Interface.smtlibC) [ - (@{const less (real)}, "<"), - (@{const less_eq (real)}, "<="), - (@{const uminus (real)}, "~"), - (@{const plus (real)}, "+"), - (@{const minus (real)}, "-") ] #> - Old_SMT_Builtin.add_builtin_fun Old_SMTLIB_Interface.smtlibC - (Term.dest_Const @{const times (real)}, times) #> - Old_SMT_Builtin.add_builtin_fun' Old_Z3_Interface.smtlib_z3C - (@{const times (real)}, "*") #> - Old_SMT_Builtin.add_builtin_fun' Old_Z3_Interface.smtlib_z3C - (@{const divide (real)}, "/") - -end - - -(* Z3 constructors *) - -local - fun z3_mk_builtin_typ (Old_Z3_Interface.Sym ("Real", _)) = SOME @{typ real} - | z3_mk_builtin_typ (Old_Z3_Interface.Sym ("real", _)) = SOME @{typ real} - (*FIXME: delete*) - | z3_mk_builtin_typ _ = NONE - - fun z3_mk_builtin_num _ i T = - if T = @{typ real} then SOME (Numeral.mk_cnumber @{ctyp real} i) - else NONE - - fun mk_nary _ cu [] = cu - | mk_nary ct _ cts = uncurry (fold_rev (Thm.mk_binop ct)) (split_last cts) - - val mk_uminus = Thm.apply (Thm.cterm_of @{context} @{const uminus (real)}) - val add = Thm.cterm_of @{context} @{const plus (real)} - val real0 = Numeral.mk_cnumber @{ctyp real} 0 - val mk_sub = Thm.mk_binop (Thm.cterm_of @{context} @{const minus (real)}) - val mk_mul = Thm.mk_binop (Thm.cterm_of @{context} @{const times (real)}) - val mk_div = Thm.mk_binop (Thm.cterm_of @{context} @{const divide (real)}) - val mk_lt = Thm.mk_binop (Thm.cterm_of @{context} @{const less (real)}) - val mk_le = Thm.mk_binop (Thm.cterm_of @{context} @{const less_eq (real)}) - - fun z3_mk_builtin_fun (Old_Z3_Interface.Sym ("-", _)) [ct] = SOME (mk_uminus ct) - | z3_mk_builtin_fun (Old_Z3_Interface.Sym ("+", _)) cts = - SOME (mk_nary add real0 cts) - | z3_mk_builtin_fun (Old_Z3_Interface.Sym ("-", _)) [ct, cu] = - SOME (mk_sub ct cu) - | z3_mk_builtin_fun (Old_Z3_Interface.Sym ("*", _)) [ct, cu] = - SOME (mk_mul ct cu) - | z3_mk_builtin_fun (Old_Z3_Interface.Sym ("/", _)) [ct, cu] = - SOME (mk_div ct cu) - | z3_mk_builtin_fun (Old_Z3_Interface.Sym ("<", _)) [ct, cu] = - SOME (mk_lt ct cu) - | z3_mk_builtin_fun (Old_Z3_Interface.Sym ("<=", _)) [ct, cu] = - SOME (mk_le ct cu) - | z3_mk_builtin_fun (Old_Z3_Interface.Sym (">", _)) [ct, cu] = - SOME (mk_lt cu ct) - | z3_mk_builtin_fun (Old_Z3_Interface.Sym (">=", _)) [ct, cu] = - SOME (mk_le cu ct) - | z3_mk_builtin_fun _ _ = NONE -in - -val z3_mk_builtins = { - mk_builtin_typ = z3_mk_builtin_typ, - mk_builtin_num = z3_mk_builtin_num, - mk_builtin_fun = (fn _ => fn sym => fn cts => - (case try (Thm.typ_of_cterm o hd) cts of - SOME @{typ real} => z3_mk_builtin_fun sym cts - | _ => NONE)) } - -end - - -(* Z3 proof reconstruction *) - -val real_rules = @{lemma - "0 + (x::real) = x" - "x + 0 = x" - "0 * x = 0" - "1 * x = x" - "x + y = y + x" - by auto} - -val real_linarith_proc = - Simplifier.make_simproc @{context} "fast_real_arith" - {lhss = [@{term "(m::real) < n"}, @{term "(m::real) \ n"}, @{term "(m::real) = n"}], - proc = K Lin_Arith.simproc} - - -(* setup *) - -val _ = - Theory.setup - (Context.theory_map ( - Old_SMTLIB_Interface.add_logic (10, smtlib_logic) #> - setup_builtins #> - Old_Z3_Interface.add_mk_builtins z3_mk_builtins #> - fold Old_Z3_Proof_Reconstruction.add_z3_rule real_rules #> - Old_Z3_Proof_Tools.add_simproc real_linarith_proc)) - -end diff -r d10f0bbc7ea1 -r f595b7532dc9 src/HOL/Library/Old_SMT/old_smt_setup_solvers.ML --- a/src/HOL/Library/Old_SMT/old_smt_setup_solvers.ML Thu Apr 20 10:45:52 2017 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,189 +0,0 @@ -(* Title: HOL/Library/Old_SMT/old_smt_setup_solvers.ML - Author: Sascha Boehme, TU Muenchen - -Setup SMT solvers. -*) - -signature OLD_SMT_SETUP_SOLVERS = -sig - datatype z3_non_commercial = - Z3_Non_Commercial_Unknown | - Z3_Non_Commercial_Accepted | - Z3_Non_Commercial_Declined - val z3_non_commercial: unit -> z3_non_commercial - val z3_with_extensions: bool Config.T - val setup: theory -> theory -end - -structure Old_SMT_Setup_Solvers: OLD_SMT_SETUP_SOLVERS = -struct - -(* helper functions *) - -fun make_avail name () = getenv ("OLD_" ^ name ^ "_SOLVER") <> "" -fun make_command name () = [getenv ("OLD_" ^ name ^ "_SOLVER")] - -fun outcome_of unsat sat unknown solver_name line = - if String.isPrefix unsat line then Old_SMT_Solver.Unsat - else if String.isPrefix sat line then Old_SMT_Solver.Sat - else if String.isPrefix unknown line then Old_SMT_Solver.Unknown - else raise Old_SMT_Failure.SMT (Old_SMT_Failure.Other_Failure ("Solver " ^ - quote solver_name ^ " failed. Enable SMT tracing by setting the " ^ - "configuration option " ^ quote (Config.name_of Old_SMT_Config.trace) ^ " and " ^ - "see the trace for details.")) - -fun on_first_line test_outcome solver_name lines = - let - val empty_line = (fn "" => true | _ => false) - val split_first = (fn [] => ("", []) | l :: ls => (l, ls)) - val (l, ls) = split_first (snd (take_prefix empty_line lines)) - in (test_outcome solver_name l, ls) end - - -(* CVC3 *) - -local - fun cvc3_options ctxt = [ - "-seed", string_of_int (Config.get ctxt Old_SMT_Config.random_seed), - "-lang", "smtlib", "-output-lang", "presentation", - "-timeout", string_of_int (Real.ceil (Config.get ctxt Old_SMT_Config.timeout))] -in - -val cvc3: Old_SMT_Solver.solver_config = { - name = "cvc3", - class = K Old_SMTLIB_Interface.smtlibC, - avail = make_avail "CVC3", - command = make_command "CVC3", - options = cvc3_options, - default_max_relevant = 400 (* FUDGE *), - supports_filter = false, - outcome = - on_first_line (outcome_of "Unsatisfiable." "Satisfiable." "Unknown."), - cex_parser = NONE, - reconstruct = NONE } - -end - - -(* Yices *) - -val yices: Old_SMT_Solver.solver_config = { - name = "yices", - class = K Old_SMTLIB_Interface.smtlibC, - avail = make_avail "YICES", - command = make_command "YICES", - options = (fn ctxt => [ - "--rand-seed=" ^ string_of_int (Config.get ctxt Old_SMT_Config.random_seed), - "--timeout=" ^ - string_of_int (Real.ceil (Config.get ctxt Old_SMT_Config.timeout)), - "--smtlib"]), - default_max_relevant = 350 (* FUDGE *), - supports_filter = false, - outcome = on_first_line (outcome_of "unsat" "sat" "unknown"), - cex_parser = NONE, - reconstruct = NONE } - - -(* Z3 *) - -datatype z3_non_commercial = - Z3_Non_Commercial_Unknown | - Z3_Non_Commercial_Accepted | - Z3_Non_Commercial_Declined - - -local - val accepted = member (op =) ["yes", "Yes", "YES"] - val declined = member (op =) ["no", "No", "NO"] -in - -fun z3_non_commercial () = - let - val flag2 = getenv "OLD_Z3_NON_COMMERCIAL" - in - if accepted flag2 then Z3_Non_Commercial_Accepted - else if declined flag2 then Z3_Non_Commercial_Declined - else Z3_Non_Commercial_Unknown - end - -fun if_z3_non_commercial f = - (case z3_non_commercial () of - Z3_Non_Commercial_Accepted => f () - | Z3_Non_Commercial_Declined => - error (Pretty.string_of (Pretty.para - "The SMT solver Z3 may only be used for non-commercial applications.")) - | Z3_Non_Commercial_Unknown => - error - (Pretty.string_of - (Pretty.para - ("The SMT solver Z3 is not activated. To activate it, set the Isabelle \ - \system option \"z3_non_commercial\" to \"yes\" (e.g. via \ - \the Isabelle/jEdit menu Plugin Options / Isabelle / General).")) ^ - "\n\nSee also " ^ Url.print (Url.explode "http://z3.codeplex.com/license"))) - -end - - -val z3_with_extensions = - Attrib.setup_config_bool @{binding old_z3_with_extensions} (K false) - -local - fun z3_make_command name () = if_z3_non_commercial (make_command name) - - fun z3_options ctxt = - ["-rs:" ^ string_of_int (Config.get ctxt Old_SMT_Config.random_seed), - "MODEL=true", - "SOFT_TIMEOUT=" ^ - string_of_int (Real.ceil (1000.0 * Config.get ctxt Old_SMT_Config.timeout)), - "-smt"] - |> not (Config.get ctxt Old_SMT_Config.oracle) ? - append ["DISPLAY_PROOF=true", "PROOF_MODE=2"] - - fun z3_on_first_or_last_line solver_name lines = - let - fun junk l = - if String.isPrefix "WARNING: Out of allocated virtual memory" l - then raise Old_SMT_Failure.SMT Old_SMT_Failure.Out_Of_Memory - else - String.isPrefix "WARNING" l orelse - String.isPrefix "ERROR" l orelse - forall Symbol.is_ascii_blank (Symbol.explode l) - val lines = filter_out junk lines - fun outcome split = - the_default ("", []) (try split lines) - |>> outcome_of "unsat" "sat" "unknown" solver_name - in - (* Starting with version 4.0, Z3 puts the outcome on the first line of the - output rather than on the last line. *) - outcome (fn lines => (hd lines, tl lines)) - handle Old_SMT_Failure.SMT _ => outcome (swap o split_last) - end - - fun select_class ctxt = - if Config.get ctxt z3_with_extensions then Old_Z3_Interface.smtlib_z3C - else Old_SMTLIB_Interface.smtlibC -in - -val z3: Old_SMT_Solver.solver_config = { - name = "z3", - class = select_class, - avail = make_avail "Z3", - command = z3_make_command "Z3", - options = z3_options, - default_max_relevant = 350 (* FUDGE *), - supports_filter = true, - outcome = z3_on_first_or_last_line, - cex_parser = SOME Old_Z3_Model.parse_counterex, - reconstruct = SOME Old_Z3_Proof_Reconstruction.reconstruct } - -end - - -(* overall setup *) - -val setup = - Old_SMT_Solver.add_solver cvc3 #> - Old_SMT_Solver.add_solver yices #> - Old_SMT_Solver.add_solver z3 - -end diff -r d10f0bbc7ea1 -r f595b7532dc9 src/HOL/Library/Old_SMT/old_smt_solver.ML --- a/src/HOL/Library/Old_SMT/old_smt_solver.ML Thu Apr 20 10:45:52 2017 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,374 +0,0 @@ -(* Title: HOL/Library/Old_SMT/old_smt_solver.ML - Author: Sascha Boehme, TU Muenchen - -SMT solvers registry and SMT tactic. -*) - -signature OLD_SMT_SOLVER = -sig - (*configuration*) - datatype outcome = Unsat | Sat | Unknown - type solver_config = { - name: string, - class: Proof.context -> Old_SMT_Utils.class, - avail: unit -> bool, - command: unit -> string list, - options: Proof.context -> string list, - default_max_relevant: int, - supports_filter: bool, - outcome: string -> string list -> outcome * string list, - cex_parser: (Proof.context -> Old_SMT_Translate.recon -> string list -> - term list * term list) option, - reconstruct: (Proof.context -> Old_SMT_Translate.recon -> string list -> - int list * thm) option } - - (*registry*) - val add_solver: solver_config -> theory -> theory - val solver_name_of: Proof.context -> string - val available_solvers_of: Proof.context -> string list - val apply_solver: Proof.context -> (int * (int option * thm)) list -> - int list * thm - val default_max_relevant: Proof.context -> string -> int - - (*filter*) - type 'a smt_filter_data = - ('a * thm) list * ((int * thm) list * Proof.context) - val smt_filter_preprocess: Proof.context -> thm list -> thm -> - ('a * (int option * thm)) list -> int -> 'a smt_filter_data - val smt_filter_apply: Time.time -> 'a smt_filter_data -> - {outcome: Old_SMT_Failure.failure option, used_facts: ('a * thm) list} - - (*tactic*) - val smt_tac: Proof.context -> thm list -> int -> tactic - val smt_tac': Proof.context -> thm list -> int -> tactic -end - -structure Old_SMT_Solver: OLD_SMT_SOLVER = -struct - - -(* interface to external solvers *) - -local - -fun make_cmd command options problem_path proof_path = - space_implode " " - ("(exec 2>&1;" :: map Bash.string (command () @ options) @ - [File.bash_path problem_path, ")", ">", File.bash_path proof_path]) - -fun trace_and ctxt msg f x = - let val _ = Old_SMT_Config.trace_msg ctxt (fn () => msg) () - in f x end - -fun run ctxt name mk_cmd input = - (case Old_SMT_Config.certificates_of ctxt of - NONE => - if not (Old_SMT_Config.is_available ctxt name) then - error ("The SMT solver " ^ quote name ^ " is not installed.") - else if Config.get ctxt Old_SMT_Config.debug_files = "" then - trace_and ctxt ("Invoking SMT solver " ^ quote name ^ " ...") - (Cache_IO.run mk_cmd) input - else - let - val base_path = Path.explode (Config.get ctxt Old_SMT_Config.debug_files) - val in_path = Path.ext "smt_in" base_path - val out_path = Path.ext "smt_out" base_path - in Cache_IO.raw_run mk_cmd input in_path out_path end - | SOME certs => - (case Cache_IO.lookup certs input of - (NONE, key) => - if Config.get ctxt Old_SMT_Config.read_only_certificates then - error ("Bad certificate cache: missing certificate") - else - Cache_IO.run_and_cache certs key mk_cmd input - | (SOME output, _) => - trace_and ctxt ("Using cached certificate from " ^ - Path.print (Cache_IO.cache_path_of certs) ^ " ...") - I output)) - -fun run_solver ctxt name mk_cmd input = - let - fun pretty tag ls = Pretty.string_of (Pretty.big_list tag - (map Pretty.str ls)) - - val _ = Old_SMT_Config.trace_msg ctxt (pretty "Problem:" o split_lines) input - - val {redirected_output=res, output=err, return_code} = - Old_SMT_Config.with_timeout ctxt (run ctxt name mk_cmd) input - val _ = Old_SMT_Config.trace_msg ctxt (pretty "Solver:") err - - val ls = fst (take_suffix (equal "") res) - val _ = Old_SMT_Config.trace_msg ctxt (pretty "Result:") ls - - val _ = return_code <> 0 andalso - raise Old_SMT_Failure.SMT (Old_SMT_Failure.Abnormal_Termination return_code) - in ls end - -fun trace_assms ctxt = - Old_SMT_Config.trace_msg ctxt (Pretty.string_of o - Pretty.big_list "Assertions:" o map (Thm.pretty_thm ctxt o snd)) - -fun trace_recon_data ({context=ctxt, typs, terms, ...} : Old_SMT_Translate.recon) = - let - fun pretty_eq n p = Pretty.block [Pretty.str n, Pretty.str " = ", p] - fun p_typ (n, T) = pretty_eq n (Syntax.pretty_typ ctxt T) - fun p_term (n, t) = pretty_eq n (Syntax.pretty_term ctxt t) - in - Old_SMT_Config.trace_msg ctxt (fn () => - Pretty.string_of (Pretty.big_list "Names:" [ - Pretty.big_list "sorts:" (map p_typ (Symtab.dest typs)), - Pretty.big_list "functions:" (map p_term (Symtab.dest terms))])) () - end - -in - -fun invoke name command ithms ctxt = - let - val options = Old_SMT_Config.solver_options_of ctxt - val comments = ("solver: " ^ name) :: - ("timeout: " ^ string_of_real (Config.get ctxt Old_SMT_Config.timeout)) :: - ("random seed: " ^ - string_of_int (Config.get ctxt Old_SMT_Config.random_seed)) :: - "arguments:" :: options - - val (str, recon as {context=ctxt', ...}) = - ithms - |> tap (trace_assms ctxt) - |> Old_SMT_Translate.translate ctxt comments - ||> tap trace_recon_data - in (run_solver ctxt' name (make_cmd command options) str, recon) end - -end - - -(* configuration *) - -datatype outcome = Unsat | Sat | Unknown - -type solver_config = { - name: string, - class: Proof.context -> Old_SMT_Utils.class, - avail: unit -> bool, - command: unit -> string list, - options: Proof.context -> string list, - default_max_relevant: int, - supports_filter: bool, - outcome: string -> string list -> outcome * string list, - cex_parser: (Proof.context -> Old_SMT_Translate.recon -> string list -> - term list * term list) option, - reconstruct: (Proof.context -> Old_SMT_Translate.recon -> string list -> - int list * thm) option } - - -(* registry *) - -type solver_info = { - command: unit -> string list, - default_max_relevant: int, - supports_filter: bool, - reconstruct: Proof.context -> string list * Old_SMT_Translate.recon -> - int list * thm } - -structure Solvers = Generic_Data -( - type T = solver_info Symtab.table - val empty = Symtab.empty - val extend = I - fun merge data = Symtab.merge (K true) data -) - -local - fun finish outcome cex_parser reconstruct ocl outer_ctxt - (output, (recon as {context=ctxt, ...} : Old_SMT_Translate.recon)) = - (case outcome output of - (Unsat, ls) => - if not (Config.get ctxt Old_SMT_Config.oracle) andalso is_some reconstruct - then the reconstruct outer_ctxt recon ls - else ([], ocl ()) - | (result, ls) => - let - val (ts, us) = - (case cex_parser of SOME f => f ctxt recon ls | _ => ([], [])) - in - raise Old_SMT_Failure.SMT (Old_SMT_Failure.Counterexample { - is_real_cex = (result = Sat), - free_constraints = ts, - const_defs = us}) - end) - - val cfalse = Thm.cterm_of @{context} (@{const Trueprop} $ @{const False}) -in - -fun add_solver cfg = - let - val {name, class, avail, command, options, default_max_relevant, - supports_filter, outcome, cex_parser, reconstruct} = cfg - - fun core_oracle () = cfalse - - fun solver ocl = { - command = command, - default_max_relevant = default_max_relevant, - supports_filter = supports_filter, - reconstruct = finish (outcome name) cex_parser reconstruct ocl } - - val info = {name=name, class=class, avail=avail, options=options} - in - Thm.add_oracle (Binding.name name, core_oracle) #-> (fn (_, ocl) => - Context.theory_map (Solvers.map (Symtab.update_new (name, solver ocl)))) #> - Context.theory_map (Old_SMT_Config.add_solver info) - end - -end - -fun get_info ctxt name = - the (Symtab.lookup (Solvers.get (Context.Proof ctxt)) name) - -val solver_name_of = Old_SMT_Config.solver_of - -val available_solvers_of = Old_SMT_Config.available_solvers_of - -fun name_and_info_of ctxt = - let val name = solver_name_of ctxt - in (name, get_info ctxt name) end - -fun gen_preprocess ctxt iwthms = Old_SMT_Normalize.normalize iwthms ctxt - -fun gen_apply (ithms, ctxt) = - let val (name, {command, reconstruct, ...}) = name_and_info_of ctxt - in - (ithms, ctxt) - |-> invoke name command - |> reconstruct ctxt - |>> distinct (op =) - end - -fun apply_solver ctxt = gen_apply o gen_preprocess ctxt - -val default_max_relevant = #default_max_relevant oo get_info - -val supports_filter = #supports_filter o snd o name_and_info_of - - -(* check well-sortedness *) - -val has_topsort = Term.exists_type (Term.exists_subtype (fn - TFree (_, []) => true - | TVar (_, []) => true - | _ => false)) - -(* without this test, we would run into problems when atomizing the rules: *) -fun check_topsort ctxt thm = - if has_topsort (Thm.prop_of thm) then - (Old_SMT_Normalize.drop_fact_warning ctxt thm; TrueI) - else - thm - -fun check_topsorts ctxt iwthms = map (apsnd (apsnd (check_topsort ctxt))) iwthms - - -(* filter *) - -val cnot = Thm.cterm_of @{context} @{const Not} - -fun mk_result outcome xrules = { outcome = outcome, used_facts = xrules } - -type 'a smt_filter_data = ('a * thm) list * ((int * thm) list * Proof.context) - -fun smt_filter_preprocess ctxt facts goal xwthms i = - let - val ctxt = - ctxt - |> Config.put Old_SMT_Config.oracle false - |> Config.put Old_SMT_Config.filter_only_facts true - - val ({context=ctxt', prems, concl, ...}, _) = Subgoal.focus ctxt i NONE goal - fun negate ct = Thm.dest_comb ct ||> Thm.apply cnot |-> Thm.apply - val cprop = - (case try negate (Thm.rhs_of (Old_SMT_Normalize.atomize_conv ctxt' concl)) of - SOME ct => ct - | NONE => raise Old_SMT_Failure.SMT (Old_SMT_Failure.Other_Failure ( - "goal is not a HOL term"))) - in - map snd xwthms - |> map_index I - |> append (map (pair ~1 o pair NONE) (Thm.assume cprop :: prems @ facts)) - |> check_topsorts ctxt' - |> gen_preprocess ctxt' - |> pair (map (apsnd snd) xwthms) - end - -fun smt_filter_apply time_limit (xthms, (ithms, ctxt)) = - let - val ctxt' = - ctxt - |> Config.put Old_SMT_Config.timeout (Time.toReal time_limit) - - fun filter_thms false = K xthms - | filter_thms true = map_filter (try (nth xthms)) o fst - in - (ithms, ctxt') - |> gen_apply - |> filter_thms (supports_filter ctxt') - |> mk_result NONE - end - handle Old_SMT_Failure.SMT fail => mk_result (SOME fail) [] - - -(* SMT tactic *) - -local - fun trace_assumptions ctxt iwthms idxs = - let - val wthms = - idxs - |> filter (fn i => i >= 0) - |> map_filter (AList.lookup (op =) iwthms) - in - if Config.get ctxt Old_SMT_Config.trace_used_facts andalso length wthms > 0 - then - tracing (Pretty.string_of (Pretty.big_list "SMT used facts:" - (map (Thm.pretty_thm ctxt o snd) wthms))) - else () - end - - fun solve ctxt iwthms = - iwthms - |> check_topsorts ctxt - |> apply_solver ctxt - |>> trace_assumptions ctxt iwthms - |> snd - - fun str_of ctxt fail = - Old_SMT_Failure.string_of_failure ctxt fail - |> prefix ("Solver " ^ Old_SMT_Config.solver_of ctxt ^ ": ") - - fun safe_solve ctxt iwthms = SOME (solve ctxt iwthms) - handle - Old_SMT_Failure.SMT (fail as Old_SMT_Failure.Counterexample _) => - (Old_SMT_Config.verbose_msg ctxt (str_of ctxt) fail; NONE) - | Old_SMT_Failure.SMT (fail as Old_SMT_Failure.Time_Out) => - error ("SMT: Solver " ^ quote (Old_SMT_Config.solver_of ctxt) ^ ": " ^ - Old_SMT_Failure.string_of_failure ctxt fail ^ " (setting the " ^ - "configuration option " ^ quote (Config.name_of Old_SMT_Config.timeout) ^ " might help)") - | Old_SMT_Failure.SMT fail => error (str_of ctxt fail) - - fun tag_rules thms = map_index (apsnd (pair NONE)) thms - fun tag_prems thms = map (pair ~1 o pair NONE) thms - - fun resolve ctxt (SOME thm) = resolve_tac ctxt [thm] 1 - | resolve _ NONE = no_tac - - fun tac prove ctxt rules = - CONVERSION (Old_SMT_Normalize.atomize_conv ctxt) - THEN' resolve_tac ctxt @{thms ccontr} - THEN' SUBPROOF (fn {context = ctxt', prems, ...} => - resolve ctxt' (prove ctxt' (tag_rules rules @ tag_prems prems))) ctxt -in - -val smt_tac = tac safe_solve -val smt_tac' = tac (SOME oo solve) - -end - -end diff -r d10f0bbc7ea1 -r f595b7532dc9 src/HOL/Library/Old_SMT/old_smt_translate.ML --- a/src/HOL/Library/Old_SMT/old_smt_translate.ML Thu Apr 20 10:45:52 2017 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,589 +0,0 @@ -(* Title: HOL/Library/Old_SMT/old_smt_translate.ML - Author: Sascha Boehme, TU Muenchen - -Translate theorems into an SMT intermediate format and serialize them. -*) - -signature OLD_SMT_TRANSLATE = -sig - (*intermediate term structure*) - datatype squant = SForall | SExists - datatype 'a spattern = SPat of 'a list | SNoPat of 'a list - datatype sterm = - SVar of int | - SApp of string * sterm list | - SLet of string * sterm * sterm | - SQua of squant * string list * sterm spattern list * int option * sterm - - (*translation configuration*) - type prefixes = {sort_prefix: string, func_prefix: string} - type sign = { - header: string list, - sorts: string list, - dtyps: (string * (string * (string * string) list) list) list list, - funcs: (string * (string list * string)) list } - type config = { - prefixes: prefixes, - header: term list -> string list, - is_fol: bool, - has_datatypes: bool, - serialize: string list -> sign -> sterm list -> string } - type recon = { - context: Proof.context, - typs: typ Symtab.table, - terms: term Symtab.table, - rewrite_rules: thm list, - assms: (int * thm) list } - - (*translation*) - val add_config: Old_SMT_Utils.class * (Proof.context -> config) -> - Context.generic -> Context.generic - val translate: Proof.context -> string list -> (int * thm) list -> - string * recon -end - -structure Old_SMT_Translate: OLD_SMT_TRANSLATE = -struct - - -(* intermediate term structure *) - -datatype squant = SForall | SExists - -datatype 'a spattern = SPat of 'a list | SNoPat of 'a list - -datatype sterm = - SVar of int | - SApp of string * sterm list | - SLet of string * sterm * sterm | - SQua of squant * string list * sterm spattern list * int option * sterm - - - -(* translation configuration *) - -type prefixes = {sort_prefix: string, func_prefix: string} - -type sign = { - header: string list, - sorts: string list, - dtyps: (string * (string * (string * string) list) list) list list, - funcs: (string * (string list * string)) list } - -type config = { - prefixes: prefixes, - header: term list -> string list, - is_fol: bool, - has_datatypes: bool, - serialize: string list -> sign -> sterm list -> string } - -type recon = { - context: Proof.context, - typs: typ Symtab.table, - terms: term Symtab.table, - rewrite_rules: thm list, - assms: (int * thm) list } - - - -(* translation context *) - -fun make_tr_context {sort_prefix, func_prefix} = - (sort_prefix, 1, Typtab.empty, func_prefix, 1, Termtab.empty) - -fun string_of_index pre i = pre ^ string_of_int i - -fun add_typ T proper (cx as (sp, Tidx, typs, fp, idx, terms)) = - (case Typtab.lookup typs T of - SOME (n, _) => (n, cx) - | NONE => - let - val n = string_of_index sp Tidx - val typs' = Typtab.update (T, (n, proper)) typs - in (n, (sp, Tidx+1, typs', fp, idx, terms)) end) - -fun add_fun t sort (cx as (sp, Tidx, typs, fp, idx, terms)) = - (case Termtab.lookup terms t of - SOME (n, _) => (n, cx) - | NONE => - let - val n = string_of_index fp idx - val terms' = Termtab.update (t, (n, sort)) terms - in (n, (sp, Tidx, typs, fp, idx+1, terms')) end) - -fun sign_of header dtyps (_, _, typs, _, _, terms) = { - header = header, - sorts = Typtab.fold (fn (_, (n, true)) => cons n | _ => I) typs [], - dtyps = dtyps, - funcs = Termtab.fold (fn (_, (n, SOME ss)) => cons (n,ss) | _ => I) terms []} - -fun recon_of ctxt rules thms ithms (_, _, typs, _, _, terms) = - let - fun add_typ (T, (n, _)) = Symtab.update (n, T) - val typs' = Typtab.fold add_typ typs Symtab.empty - - fun add_fun (t, (n, _)) = Symtab.update (n, t) - val terms' = Termtab.fold add_fun terms Symtab.empty - - val assms = map (pair ~1) thms @ ithms - in - {context=ctxt, typs=typs', terms=terms', rewrite_rules=rules, assms=assms} - end - - - -(* preprocessing *) - -(** datatype declarations **) - -fun collect_datatypes_and_records (tr_context, ctxt) ts = - let - val (declss, ctxt') = - fold (Term.fold_types Old_SMT_Datatypes.add_decls) ts ([], ctxt) - - fun is_decl_typ T = exists (exists (equal T o fst)) declss - - fun add_typ' T proper = - (case Old_SMT_Builtin.dest_builtin_typ ctxt' T of - SOME n => pair n - | NONE => add_typ T proper) - - fun tr_select sel = - let val T = Term.range_type (Term.fastype_of sel) - in add_fun sel NONE ##>> add_typ' T (not (is_decl_typ T)) end - fun tr_constr (constr, selects) = - add_fun constr NONE ##>> fold_map tr_select selects - fun tr_typ (T, cases) = add_typ' T false ##>> fold_map tr_constr cases - val (declss', tr_context') = fold_map (fold_map tr_typ) declss tr_context - - fun add (constr, selects) = - Termtab.update (constr, length selects) #> - fold (Termtab.update o rpair 1) selects - val funcs = fold (fold (fold add o snd)) declss Termtab.empty - in ((funcs, declss', tr_context', ctxt'), ts) end - (* FIXME: also return necessary datatype and record theorems *) - - -(** eta-expand quantifiers, let expressions and built-ins *) - -local - fun eta f T t = Abs (Name.uu, T, f (Term.incr_boundvars 1 t $ Bound 0)) - - fun exp f T = eta f (Term.domain_type (Term.domain_type T)) - - fun exp2 T q = - let val U = Term.domain_type T - in Abs (Name.uu, U, q $ eta I (Term.domain_type U) (Bound 0)) end - - fun exp2' T l = - let val (U1, U2) = Term.dest_funT T ||> Term.domain_type - in Abs (Name.uu, U1, eta I U2 (l $ Bound 0)) end - - fun expf k i T t = - let val Ts = drop i (fst (Old_SMT_Utils.dest_funT k T)) - in - Term.incr_boundvars (length Ts) t - |> fold_rev (fn i => fn u => u $ Bound i) (0 upto length Ts - 1) - |> fold_rev (fn T => fn u => Abs (Name.uu, T, u)) Ts - end -in - -fun eta_expand ctxt is_fol funcs = - let - fun exp_func t T ts = - (case Termtab.lookup funcs t of - SOME k => - Term.list_comb (t, ts) - |> k <> length ts ? expf k (length ts) T - | NONE => Term.list_comb (t, ts)) - - fun expand ((q as Const (@{const_name All}, _)) $ Abs a) = q $ abs_expand a - | expand ((q as Const (@{const_name All}, T)) $ t) = q $ exp expand T t - | expand (q as Const (@{const_name All}, T)) = exp2 T q - | expand ((q as Const (@{const_name Ex}, _)) $ Abs a) = q $ abs_expand a - | expand ((q as Const (@{const_name Ex}, T)) $ t) = q $ exp expand T t - | expand (q as Const (@{const_name Ex}, T)) = exp2 T q - | expand ((l as Const (@{const_name Let}, _)) $ t $ Abs a) = - if is_fol then expand (Term.betapply (Abs a, t)) - else l $ expand t $ abs_expand a - | expand ((l as Const (@{const_name Let}, T)) $ t $ u) = - if is_fol then expand (u $ t) - else l $ expand t $ exp expand (Term.range_type T) u - | expand ((l as Const (@{const_name Let}, T)) $ t) = - if is_fol then - let val U = Term.domain_type (Term.range_type T) - in Abs (Name.uu, U, Bound 0 $ Term.incr_boundvars 1 t) end - else exp2 T (l $ expand t) - | expand (l as Const (@{const_name Let}, T)) = - if is_fol then - let val U = Term.domain_type (Term.range_type T) - in - Abs (Name.uu, Term.domain_type T, Abs (Name.uu, U, - Bound 0 $ Bound 1)) - end - else exp2' T l - | expand t = - (case Term.strip_comb t of - (u as Const (c as (_, T)), ts) => - (case Old_SMT_Builtin.dest_builtin ctxt c ts of - SOME (_, k, us, mk) => - if k = length us then mk (map expand us) - else if k < length us then - chop k (map expand us) |>> mk |> Term.list_comb - else expf k (length ts) T (mk (map expand us)) - | NONE => exp_func u T (map expand ts)) - | (u as Free (_, T), ts) => exp_func u T (map expand ts) - | (Abs a, ts) => Term.list_comb (abs_expand a, map expand ts) - | (u, ts) => Term.list_comb (u, map expand ts)) - - and abs_expand (n, T, t) = Abs (n, T, expand t) - - in map expand end - -end - - -(** introduce explicit applications **) - -local - (* - Make application explicit for functions with varying number of arguments. - *) - - fun add t i = apfst (Termtab.map_default (t, i) (Integer.min i)) - fun add_type T = apsnd (Typtab.update (T, ())) - - fun min_arities t = - (case Term.strip_comb t of - (u as Const _, ts) => add u (length ts) #> fold min_arities ts - | (u as Free _, ts) => add u (length ts) #> fold min_arities ts - | (Abs (_, T, u), ts) => add_type T #> min_arities u #> fold min_arities ts - | (_, ts) => fold min_arities ts) - - fun minimize types t i = - let - fun find_min j [] _ = j - | find_min j (U :: Us) T = - if Typtab.defined types T then j - else find_min (j + 1) Us (U --> T) - - val (Ts, T) = Term.strip_type (Term.type_of t) - in find_min 0 (take i (rev Ts)) T end - - fun app u (t, T) = - (Const (@{const_name fun_app}, T --> T) $ t $ u, Term.range_type T) - - fun apply i t T ts = - let - val (ts1, ts2) = chop i ts - val (_, U) = Old_SMT_Utils.dest_funT i T - in fst (fold app ts2 (Term.list_comb (t, ts1), U)) end -in - -fun intro_explicit_application ctxt funcs ts = - let - val (arities, types) = fold min_arities ts (Termtab.empty, Typtab.empty) - val arities' = Termtab.map (minimize types) arities - - fun app_func t T ts = - if is_some (Termtab.lookup funcs t) then Term.list_comb (t, ts) - else apply (the (Termtab.lookup arities' t)) t T ts - - fun in_list T f t = HOLogic.mk_list T (map f (HOLogic.dest_list t)) - - fun traverse Ts t = - (case Term.strip_comb t of - (q as Const (@{const_name All}, _), [Abs (x, T, u)]) => - q $ Abs (x, T, in_trigger (T :: Ts) u) - | (q as Const (@{const_name Ex}, _), [Abs (x, T, u)]) => - q $ Abs (x, T, in_trigger (T :: Ts) u) - | (q as Const (@{const_name Let}, _), [u1, u2 as Abs _]) => - q $ traverse Ts u1 $ traverse Ts u2 - | (u as Const (c as (_, T)), ts) => - (case Old_SMT_Builtin.dest_builtin ctxt c ts of - SOME (_, k, us, mk) => - let - val (ts1, ts2) = chop k (map (traverse Ts) us) - val U = Term.strip_type T |>> snd o chop k |> (op --->) - in apply 0 (mk ts1) U ts2 end - | NONE => app_func u T (map (traverse Ts) ts)) - | (u as Free (_, T), ts) => app_func u T (map (traverse Ts) ts) - | (u as Bound i, ts) => apply 0 u (nth Ts i) (map (traverse Ts) ts) - | (Abs (n, T, u), ts) => traverses Ts (Abs (n, T, traverse (T::Ts) u)) ts - | (u, ts) => traverses Ts u ts) - and in_trigger Ts ((c as @{const trigger}) $ p $ t) = - c $ in_pats Ts p $ in_weight Ts t - | in_trigger Ts t = in_weight Ts t - and in_pats Ts ps = - in_list @{typ "pattern list"} - (in_list @{typ pattern} (in_pat Ts)) ps - and in_pat Ts ((p as Const (@{const_name pat}, _)) $ t) = - p $ traverse Ts t - | in_pat Ts ((p as Const (@{const_name nopat}, _)) $ t) = - p $ traverse Ts t - | in_pat _ t = raise TERM ("bad pattern", [t]) - and in_weight Ts ((c as @{const weight}) $ w $ t) = - c $ w $ traverse Ts t - | in_weight Ts t = traverse Ts t - and traverses Ts t ts = Term.list_comb (t, map (traverse Ts) ts) - in map (traverse []) ts end - -val fun_app_eq = mk_meta_eq @{thm fun_app_def} - -end - - -(** map HOL formulas to FOL formulas (i.e., separate formulas froms terms) **) - -local - val term_bool = @{lemma "term_true ~= term_false" - by (simp add: term_true_def term_false_def)} - - val is_quant = member (op =) [@{const_name All}, @{const_name Ex}] - - val fol_rules = [ - Let_def, - mk_meta_eq @{thm term_true_def}, - mk_meta_eq @{thm term_false_def}, - @{lemma "P = True == P" by (rule eq_reflection) simp}, - @{lemma "if P then True else False == P" by (rule eq_reflection) simp}] - - fun as_term t = @{const HOL.eq (bool)} $ t $ @{const term_true} - - exception BAD_PATTERN of unit - - fun wrap_in_if pat t = - if pat then - raise BAD_PATTERN () - else - @{const If (bool)} $ t $ @{const term_true} $ @{const term_false} - - fun is_builtin_conn_or_pred ctxt c ts = - is_some (Old_SMT_Builtin.dest_builtin_conn ctxt c ts) orelse - is_some (Old_SMT_Builtin.dest_builtin_pred ctxt c ts) - - fun builtin b ctxt c ts = - (case (Const c, ts) of - (@{const HOL.eq (bool)}, [t, u]) => - if t = @{const term_true} orelse u = @{const term_true} then - Old_SMT_Builtin.dest_builtin_eq ctxt t u - else b ctxt c ts - | _ => b ctxt c ts) -in - -fun folify ctxt = - let - fun in_list T f t = HOLogic.mk_list T (map_filter f (HOLogic.dest_list t)) - - fun in_term pat t = - (case Term.strip_comb t of - (@{const True}, []) => @{const term_true} - | (@{const False}, []) => @{const term_false} - | (u as Const (@{const_name If}, _), [t1, t2, t3]) => - if pat then raise BAD_PATTERN () - else u $ in_form t1 $ in_term pat t2 $ in_term pat t3 - | (Const (c as (n, _)), ts) => - if is_builtin_conn_or_pred ctxt c ts then wrap_in_if pat (in_form t) - else if is_quant n then wrap_in_if pat (in_form t) - else Term.list_comb (Const c, map (in_term pat) ts) - | (Free c, ts) => Term.list_comb (Free c, map (in_term pat) ts) - | _ => t) - - and in_weight ((c as @{const weight}) $ w $ t) = c $ w $ in_form t - | in_weight t = in_form t - - and in_pat ((p as Const (@{const_name pat}, _)) $ t) = - p $ in_term true t - | in_pat ((p as Const (@{const_name nopat}, _)) $ t) = - p $ in_term true t - | in_pat t = raise TERM ("bad pattern", [t]) - - and in_pats ps = - in_list @{typ "pattern list"} - (SOME o in_list @{typ pattern} (try in_pat)) ps - - and in_trigger ((c as @{const trigger}) $ p $ t) = - c $ in_pats p $ in_weight t - | in_trigger t = in_weight t - - and in_form t = - (case Term.strip_comb t of - (q as Const (qn, _), [Abs (n, T, u)]) => - if is_quant qn then q $ Abs (n, T, in_trigger u) - else as_term (in_term false t) - | (Const c, ts) => - (case Old_SMT_Builtin.dest_builtin_conn ctxt c ts of - SOME (_, _, us, mk) => mk (map in_form us) - | NONE => - (case Old_SMT_Builtin.dest_builtin_pred ctxt c ts of - SOME (_, _, us, mk) => mk (map (in_term false) us) - | NONE => as_term (in_term false t))) - | _ => as_term (in_term false t)) - in - map in_form #> - cons (Old_SMT_Utils.prop_of term_bool) #> - pair (fol_rules, [term_bool], builtin) - end - -end - - -(* translation into intermediate format *) - -(** utility functions **) - -val quantifier = (fn - @{const_name All} => SOME SForall - | @{const_name Ex} => SOME SExists - | _ => NONE) - -fun group_quant qname Ts (t as Const (q, _) $ Abs (_, T, u)) = - if q = qname then group_quant qname (T :: Ts) u else (Ts, t) - | group_quant _ Ts t = (Ts, t) - -fun dest_weight (@{const weight} $ w $ t) = - (SOME (snd (HOLogic.dest_number w)), t) - | dest_weight t = (NONE, t) - -fun dest_pat (Const (@{const_name pat}, _) $ t) = (t, true) - | dest_pat (Const (@{const_name nopat}, _) $ t) = (t, false) - | dest_pat t = raise TERM ("bad pattern", [t]) - -fun dest_pats [] = I - | dest_pats ts = - (case map dest_pat ts |> split_list ||> distinct (op =) of - (ps, [true]) => cons (SPat ps) - | (ps, [false]) => cons (SNoPat ps) - | _ => raise TERM ("bad multi-pattern", ts)) - -fun dest_trigger (@{const trigger} $ tl $ t) = - (rev (fold (dest_pats o HOLogic.dest_list) (HOLogic.dest_list tl) []), t) - | dest_trigger t = ([], t) - -fun dest_quant qn T t = quantifier qn |> Option.map (fn q => - let - val (Ts, u) = group_quant qn [T] t - val (ps, p) = dest_trigger u - val (w, b) = dest_weight p - in (q, rev Ts, ps, w, b) end) - -fun fold_map_pat f (SPat ts) = fold_map f ts #>> SPat - | fold_map_pat f (SNoPat ts) = fold_map f ts #>> SNoPat - - -(** translation from Isabelle terms into SMT intermediate terms **) - -fun intermediate header dtyps builtin ctxt ts trx = - let - fun transT (T as TFree _) = add_typ T true - | transT (T as TVar _) = (fn _ => raise TYPE ("bad SMT type", [T], [])) - | transT (T as Type _) = - (case Old_SMT_Builtin.dest_builtin_typ ctxt T of - SOME n => pair n - | NONE => add_typ T true) - - fun app n ts = SApp (n, ts) - - fun trans t = - (case Term.strip_comb t of - (Const (qn, _), [Abs (_, T, t1)]) => - (case dest_quant qn T t1 of - SOME (q, Ts, ps, w, b) => - fold_map transT Ts ##>> fold_map (fold_map_pat trans) ps ##>> - trans b #>> (fn ((Ts', ps'), b') => SQua (q, Ts', ps', w, b')) - | NONE => raise TERM ("unsupported quantifier", [t])) - | (Const (@{const_name Let}, _), [t1, Abs (_, T, t2)]) => - transT T ##>> trans t1 ##>> trans t2 #>> - (fn ((U, u1), u2) => SLet (U, u1, u2)) - | (u as Const (c as (_, T)), ts) => - (case builtin ctxt c ts of - SOME (n, _, us, _) => fold_map trans us #>> app n - | NONE => transs u T ts) - | (u as Free (_, T), ts) => transs u T ts - | (Bound i, []) => pair (SVar i) - | _ => raise TERM ("bad SMT term", [t])) - - and transs t T ts = - let val (Us, U) = Old_SMT_Utils.dest_funT (length ts) T - in - fold_map transT Us ##>> transT U #-> (fn Up => - add_fun t (SOME Up) ##>> fold_map trans ts #>> SApp) - end - - val (us, trx') = fold_map trans ts trx - in ((sign_of (header ts) dtyps trx', us), trx') end - - - -(* translation *) - -structure Configs = Generic_Data -( - type T = (Proof.context -> config) Old_SMT_Utils.dict - val empty = [] - val extend = I - fun merge data = Old_SMT_Utils.dict_merge fst data -) - -fun add_config (cs, cfg) = Configs.map (Old_SMT_Utils.dict_update (cs, cfg)) - -fun get_config ctxt = - let val cs = Old_SMT_Config.solver_class_of ctxt - in - (case Old_SMT_Utils.dict_get (Configs.get (Context.Proof ctxt)) cs of - SOME cfg => cfg ctxt - | NONE => error ("SMT: no translation configuration found " ^ - "for solver class " ^ quote (Old_SMT_Utils.string_of_class cs))) - end - -fun translate ctxt comments ithms = - let - val {prefixes, is_fol, header, has_datatypes, serialize} = get_config ctxt - - val with_datatypes = - has_datatypes andalso Config.get ctxt Old_SMT_Config.datatypes - - fun no_dtyps (tr_context, ctxt) ts = - ((Termtab.empty, [], tr_context, ctxt), ts) - - val ts1 = map (Envir.beta_eta_contract o Old_SMT_Utils.prop_of o snd) ithms - - val ((funcs, dtyps, tr_context, ctxt1), ts2) = - ((make_tr_context prefixes, ctxt), ts1) - |-> (if with_datatypes then collect_datatypes_and_records else no_dtyps) - - fun is_binder (Const (@{const_name Let}, _) $ _) = true - | is_binder t = Lambda_Lifting.is_quantifier t - - fun mk_trigger ((q as Const (@{const_name All}, _)) $ Abs (n, T, t)) = - q $ Abs (n, T, mk_trigger t) - | mk_trigger (eq as (Const (@{const_name HOL.eq}, T) $ lhs $ _)) = - Term.domain_type T --> @{typ pattern} - |> (fn T => Const (@{const_name pat}, T) $ lhs) - |> HOLogic.mk_list @{typ pattern} o single - |> HOLogic.mk_list @{typ "pattern list"} o single - |> (fn t => @{const trigger} $ t $ eq) - | mk_trigger t = t - - val (ctxt2, ts3) = - ts2 - |> eta_expand ctxt1 is_fol funcs - |> rpair ctxt1 - |-> Lambda_Lifting.lift_lambdas NONE is_binder - |-> (fn (ts', defs) => fn ctxt' => - map mk_trigger defs @ ts' - |> intro_explicit_application ctxt' funcs - |> pair ctxt') - - val ((rewrite_rules, extra_thms, builtin), ts4) = - (if is_fol then folify ctxt2 else pair ([], [], I)) ts3 - - val rewrite_rules' = fun_app_eq :: rewrite_rules - in - (ts4, tr_context) - |-> intermediate header dtyps (builtin Old_SMT_Builtin.dest_builtin) ctxt2 - |>> uncurry (serialize comments) - ||> recon_of ctxt2 rewrite_rules' extra_thms ithms - end - -end diff -r d10f0bbc7ea1 -r f595b7532dc9 src/HOL/Library/Old_SMT/old_smt_utils.ML --- a/src/HOL/Library/Old_SMT/old_smt_utils.ML Thu Apr 20 10:45:52 2017 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,221 +0,0 @@ -(* Title: HOL/Library/Old_SMT/old_smt_utils.ML - Author: Sascha Boehme, TU Muenchen - -General utility functions. -*) - -signature OLD_SMT_UTILS = -sig - (*basic combinators*) - val repeat: ('a -> 'a option) -> 'a -> 'a - val repeat_yield: ('a -> 'b -> ('a * 'b) option) -> 'a -> 'b -> 'a * 'b - - (*class dictionaries*) - type class = string list - val basicC: class - val string_of_class: class -> string - type 'a dict = (class * 'a) Ord_List.T - val dict_map_default: class * 'a -> ('a -> 'a) -> 'a dict -> 'a dict - val dict_update: class * 'a -> 'a dict -> 'a dict - val dict_merge: ('a * 'a -> 'a) -> 'a dict * 'a dict -> 'a dict - val dict_lookup: 'a dict -> class -> 'a list - val dict_get: 'a dict -> class -> 'a option - - (*types*) - val dest_funT: int -> typ -> typ list * typ - - (*terms*) - val dest_conj: term -> term * term - val dest_disj: term -> term * term - val under_quant: (term -> 'a) -> term -> 'a - val is_number: term -> bool - - (*patterns and instantiations*) - val mk_const_pat: theory -> string -> (ctyp -> 'a) -> 'a * cterm - val destT1: ctyp -> ctyp - val destT2: ctyp -> ctyp - val instTs: ctyp list -> ctyp list * cterm -> cterm - val instT: ctyp -> ctyp * cterm -> cterm - val instT': cterm -> ctyp * cterm -> cterm - - (*certified terms*) - val dest_cabs: cterm -> Proof.context -> cterm * Proof.context - val dest_all_cabs: cterm -> Proof.context -> cterm * Proof.context - val dest_cbinder: cterm -> Proof.context -> cterm * Proof.context - val dest_all_cbinders: cterm -> Proof.context -> cterm * Proof.context - val mk_cprop: cterm -> cterm - val dest_cprop: cterm -> cterm - val mk_cequals: cterm -> cterm -> cterm - val term_of: cterm -> term - val prop_of: thm -> term - - (*conversions*) - val if_conv: (term -> bool) -> conv -> conv -> conv - val if_true_conv: (term -> bool) -> conv -> conv - val if_exists_conv: (term -> bool) -> conv -> conv - val binders_conv: (Proof.context -> conv) -> Proof.context -> conv - val under_quant_conv: (Proof.context * cterm list -> conv) -> - Proof.context -> conv - val prop_conv: conv -> conv -end - -structure Old_SMT_Utils: OLD_SMT_UTILS = -struct - -(* basic combinators *) - -fun repeat f = - let fun rep x = (case f x of SOME y => rep y | NONE => x) - in rep end - -fun repeat_yield f = - let fun rep x y = (case f x y of SOME (x', y') => rep x' y' | NONE => (x, y)) - in rep end - - -(* class dictionaries *) - -type class = string list - -val basicC = [] - -fun string_of_class [] = "basic" - | string_of_class cs = "basic." ^ space_implode "." cs - -type 'a dict = (class * 'a) Ord_List.T - -fun class_ord ((cs1, _), (cs2, _)) = - rev_order (list_ord fast_string_ord (cs1, cs2)) - -fun dict_insert (cs, x) d = - if AList.defined (op =) d cs then d - else Ord_List.insert class_ord (cs, x) d - -fun dict_map_default (cs, x) f = - dict_insert (cs, x) #> AList.map_entry (op =) cs f - -fun dict_update (e as (_, x)) = dict_map_default e (K x) - -fun dict_merge val_merge = sort class_ord o AList.join (op =) (K val_merge) - -fun dict_lookup d cs = - let fun match (cs', x) = if is_prefix (op =) cs' cs then SOME x else NONE - in map_filter match d end - -fun dict_get d cs = - (case AList.lookup (op =) d cs of - NONE => (case cs of [] => NONE | _ => dict_get d (take (length cs - 1) cs)) - | SOME x => SOME x) - - -(* types *) - -val dest_funT = - let - fun dest Ts 0 T = (rev Ts, T) - | dest Ts i (Type ("fun", [T, U])) = dest (T::Ts) (i-1) U - | dest _ _ T = raise TYPE ("not a function type", [T], []) - in dest [] end - - -(* terms *) - -fun dest_conj (@{const HOL.conj} $ t $ u) = (t, u) - | dest_conj t = raise TERM ("not a conjunction", [t]) - -fun dest_disj (@{const HOL.disj} $ t $ u) = (t, u) - | dest_disj t = raise TERM ("not a disjunction", [t]) - -fun under_quant f t = - (case t of - Const (@{const_name All}, _) $ Abs (_, _, u) => under_quant f u - | Const (@{const_name Ex}, _) $ Abs (_, _, u) => under_quant f u - | _ => f t) - -val is_number = - let - fun is_num env (Const (@{const_name If}, _) $ _ $ t $ u) = - is_num env t andalso is_num env u - | is_num env (Const (@{const_name Let}, _) $ t $ Abs (_, _, u)) = - is_num (t :: env) u - | is_num env (Bound i) = i < length env andalso is_num env (nth env i) - | is_num _ t = can HOLogic.dest_number t - in is_num [] end - - -(* patterns and instantiations *) - -fun mk_const_pat thy name destT = - let val cpat = Thm.global_cterm_of thy (Const (name, Sign.the_const_type thy name)) - in (destT (Thm.ctyp_of_cterm cpat), cpat) end - -val destT1 = hd o Thm.dest_ctyp -val destT2 = hd o tl o Thm.dest_ctyp - -fun instTs cUs (cTs, ct) = Thm.instantiate_cterm (map (dest_TVar o Thm.typ_of) cTs ~~ cUs, []) ct -fun instT cU (cT, ct) = instTs [cU] ([cT], ct) -fun instT' ct = instT (Thm.ctyp_of_cterm ct) - - -(* certified terms *) - -fun dest_cabs ct ctxt = - (case Thm.term_of ct of - Abs _ => - let val (n, ctxt') = yield_singleton Variable.variant_fixes Name.uu ctxt - in (snd (Thm.dest_abs (SOME n) ct), ctxt') end - | _ => raise CTERM ("no abstraction", [ct])) - -val dest_all_cabs = repeat_yield (try o dest_cabs) - -fun dest_cbinder ct ctxt = - (case Thm.term_of ct of - Const _ $ Abs _ => dest_cabs (Thm.dest_arg ct) ctxt - | _ => raise CTERM ("not a binder", [ct])) - -val dest_all_cbinders = repeat_yield (try o dest_cbinder) - -val mk_cprop = Thm.apply (Thm.cterm_of @{context} @{const Trueprop}) - -fun dest_cprop ct = - (case Thm.term_of ct of - @{const Trueprop} $ _ => Thm.dest_arg ct - | _ => raise CTERM ("not a property", [ct])) - -val equals = mk_const_pat @{theory} @{const_name Pure.eq} destT1 -fun mk_cequals ct cu = Thm.mk_binop (instT' ct equals) ct cu - -val dest_prop = (fn @{const Trueprop} $ t => t | t => t) -fun term_of ct = dest_prop (Thm.term_of ct) -fun prop_of thm = dest_prop (Thm.prop_of thm) - - -(* conversions *) - -fun if_conv pred cv1 cv2 ct = if pred (Thm.term_of ct) then cv1 ct else cv2 ct - -fun if_true_conv pred cv = if_conv pred cv Conv.all_conv - -fun if_exists_conv pred = if_true_conv (Term.exists_subterm pred) - -fun binders_conv cv ctxt = - Conv.binder_conv (binders_conv cv o snd) ctxt else_conv cv ctxt - -fun under_quant_conv cv ctxt = - let - fun quant_conv inside ctxt cvs ct = - (case Thm.term_of ct of - Const (@{const_name All}, _) $ Abs _ => - Conv.binder_conv (under_conv cvs) ctxt - | Const (@{const_name Ex}, _) $ Abs _ => - Conv.binder_conv (under_conv cvs) ctxt - | _ => if inside then cv (ctxt, cvs) else Conv.all_conv) ct - and under_conv cvs (cv, ctxt) = quant_conv true ctxt (cv :: cvs) - in quant_conv false ctxt [] end - -fun prop_conv cv ct = - (case Thm.term_of ct of - @{const Trueprop} $ _ => Conv.arg_conv cv ct - | _ => raise CTERM ("not a property", [ct])) - -end diff -r d10f0bbc7ea1 -r f595b7532dc9 src/HOL/Library/Old_SMT/old_smt_word.ML --- a/src/HOL/Library/Old_SMT/old_smt_word.ML Thu Apr 20 10:45:52 2017 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,146 +0,0 @@ -(* Title: HOL/Library/Old_SMT/old_smt_word.ML - Author: Sascha Boehme, TU Muenchen - -SMT setup for words. -*) - -structure Old_SMT_Word: sig end = -struct - -open Word_Lib - -(* SMT-LIB logic *) - -fun smtlib_logic ts = - if exists (Term.exists_type (Term.exists_subtype is_wordT)) ts - then SOME "QF_AUFBV" - else NONE - - -(* SMT-LIB builtins *) - -local - val smtlibC = Old_SMTLIB_Interface.smtlibC - - val wordT = @{typ "'a::len word"} - - fun index1 n i = n ^ "[" ^ string_of_int i ^ "]" - fun index2 n i j = n ^ "[" ^ string_of_int i ^ ":" ^ string_of_int j ^ "]" - - fun word_typ (Type (@{type_name word}, [T])) = - Option.map (index1 "BitVec") (try dest_binT T) - | word_typ _ = NONE - - fun word_num (Type (@{type_name word}, [T])) i = - Option.map (index1 ("bv" ^ string_of_int i)) (try dest_binT T) - | word_num _ _ = NONE - - fun if_fixed pred m n T ts = - let val (Us, U) = Term.strip_type T - in - if pred (U, Us) then - SOME (n, length Us, ts, Term.list_comb o pair (Const (m, T))) - else NONE - end - - fun if_fixed_all m = if_fixed (forall (can dest_wordT) o (op ::)) m - fun if_fixed_args m = if_fixed (forall (can dest_wordT) o snd) m - - fun add_word_fun f (t, n) = - let val (m, _) = Term.dest_Const t - in Old_SMT_Builtin.add_builtin_fun smtlibC (Term.dest_Const t, K (f m n)) end - - fun hd2 xs = hd (tl xs) - - fun mk_nat i = @{const nat} $ HOLogic.mk_number @{typ nat} i - - fun dest_nat (@{const nat} $ n) = snd (HOLogic.dest_number n) - | dest_nat t = raise TERM ("not a natural number", [t]) - - fun mk_shift c [t, u] = Const c $ t $ mk_nat (snd (HOLogic.dest_number u)) - | mk_shift c ts = raise TERM ("bad arguments", Const c :: ts) - - fun shift m n T ts = - let val U = Term.domain_type T - in - (case (can dest_wordT U, try (dest_nat o hd2) ts) of - (true, SOME i) => - SOME (n, 2, [hd ts, HOLogic.mk_number U i], mk_shift (m, T)) - | _ => NONE) (* FIXME: also support non-numerical shifts *) - end - - fun mk_extract c i ts = Term.list_comb (Const c, mk_nat i :: ts) - - fun extract m n T ts = - let val U = Term.range_type (Term.range_type T) - in - (case (try (dest_nat o hd) ts, try dest_wordT U) of - (SOME lb, SOME i) => - SOME (index2 n (i + lb - 1) lb, 1, tl ts, mk_extract (m, T) lb) - | _ => NONE) - end - - fun mk_extend c ts = Term.list_comb (Const c, ts) - - fun extend m n T ts = - let val (U1, U2) = Term.dest_funT T - in - (case (try dest_wordT U1, try dest_wordT U2) of - (SOME i, SOME j) => - if j-i >= 0 then SOME (index1 n (j-i), 1, ts, mk_extend (m, T)) - else NONE - | _ => NONE) - end - - fun mk_rotate c i ts = Term.list_comb (Const c, mk_nat i :: ts) - - fun rotate m n T ts = - let val U = Term.domain_type (Term.range_type T) - in - (case (can dest_wordT U, try (dest_nat o hd) ts) of - (true, SOME i) => SOME (index1 n i, 1, tl ts, mk_rotate (m, T) i) - | _ => NONE) - end -in - -val setup_builtins = - Old_SMT_Builtin.add_builtin_typ smtlibC (wordT, word_typ, word_num) #> - fold (add_word_fun if_fixed_all) [ - (@{term "uminus :: 'a::len word => _"}, "bvneg"), - (@{term "plus :: 'a::len word => _"}, "bvadd"), - (@{term "minus :: 'a::len word => _"}, "bvsub"), - (@{term "times :: 'a::len word => _"}, "bvmul"), - (@{term "bitNOT :: 'a::len word => _"}, "bvnot"), - (@{term "bitAND :: 'a::len word => _"}, "bvand"), - (@{term "bitOR :: 'a::len word => _"}, "bvor"), - (@{term "bitXOR :: 'a::len word => _"}, "bvxor"), - (@{term "word_cat :: 'a::len word => _"}, "concat") ] #> - fold (add_word_fun shift) [ - (@{term "shiftl :: 'a::len word => _ "}, "bvshl"), - (@{term "shiftr :: 'a::len word => _"}, "bvlshr"), - (@{term "sshiftr :: 'a::len word => _"}, "bvashr") ] #> - add_word_fun extract - (@{term "slice :: _ => 'a::len word => _"}, "extract") #> - fold (add_word_fun extend) [ - (@{term "ucast :: 'a::len word => _"}, "zero_extend"), - (@{term "scast :: 'a::len word => _"}, "sign_extend") ] #> - fold (add_word_fun rotate) [ - (@{term word_rotl}, "rotate_left"), - (@{term word_rotr}, "rotate_right") ] #> - fold (add_word_fun if_fixed_args) [ - (@{term "less :: 'a::len word => _"}, "bvult"), - (@{term "less_eq :: 'a::len word => _"}, "bvule"), - (@{term word_sless}, "bvslt"), - (@{term word_sle}, "bvsle") ] - -end - - -(* setup *) - -val _ = - Theory.setup - (Context.theory_map - (Old_SMTLIB_Interface.add_logic (20, smtlib_logic) #> setup_builtins)) - -end diff -r d10f0bbc7ea1 -r f595b7532dc9 src/HOL/Library/Old_SMT/old_smtlib_interface.ML --- a/src/HOL/Library/Old_SMT/old_smtlib_interface.ML Thu Apr 20 10:45:52 2017 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,161 +0,0 @@ -(* Title: HOL/Library/Old_SMT/old_smtlib_interface.ML - Author: Sascha Boehme, TU Muenchen - -Interface to SMT solvers based on the SMT-LIB format. -*) - -signature OLD_SMTLIB_INTERFACE = -sig - val smtlibC: Old_SMT_Utils.class - val add_logic: int * (term list -> string option) -> Context.generic -> - Context.generic - val translate_config: Proof.context -> Old_SMT_Translate.config - val setup: theory -> theory -end - -structure Old_SMTLIB_Interface: OLD_SMTLIB_INTERFACE = -struct - - -val smtlibC = ["smtlib"] - - -(* builtins *) - -local - fun int_num _ i = SOME (string_of_int i) - - fun is_linear [t] = Old_SMT_Utils.is_number t - | is_linear [t, u] = Old_SMT_Utils.is_number t orelse Old_SMT_Utils.is_number u - | is_linear _ = false - - fun times _ _ ts = - let val mk = Term.list_comb o pair @{const times (int)} - in if is_linear ts then SOME ("*", 2, ts, mk) else NONE end -in - -val setup_builtins = - Old_SMT_Builtin.add_builtin_typ smtlibC (@{typ int}, K (SOME "Int"), int_num) #> - fold (Old_SMT_Builtin.add_builtin_fun' smtlibC) [ - (@{const True}, "true"), - (@{const False}, "false"), - (@{const Not}, "not"), - (@{const HOL.conj}, "and"), - (@{const HOL.disj}, "or"), - (@{const HOL.implies}, "implies"), - (@{const HOL.eq (bool)}, "iff"), - (@{const HOL.eq ('a)}, "="), - (@{const If (bool)}, "if_then_else"), - (@{const If ('a)}, "ite"), - (@{const less (int)}, "<"), - (@{const less_eq (int)}, "<="), - (@{const uminus (int)}, "~"), - (@{const plus (int)}, "+"), - (@{const minus (int)}, "-") ] #> - Old_SMT_Builtin.add_builtin_fun smtlibC - (Term.dest_Const @{const times (int)}, times) - -end - - -(* serialization *) - -(** header **) - -fun fst_int_ord ((i1, _), (i2, _)) = int_ord (i1, i2) - -structure Logics = Generic_Data -( - type T = (int * (term list -> string option)) list - val empty = [] - val extend = I - fun merge data = Ord_List.merge fst_int_ord data -) - -fun add_logic pf = Logics.map (Ord_List.insert fst_int_ord pf) - -fun choose_logic ctxt ts = - let - fun choose [] = "AUFLIA" - | choose ((_, f) :: fs) = (case f ts of SOME s => s | NONE => choose fs) - in [":logic " ^ choose (Logics.get (Context.Proof ctxt))] end - - -(** serialization **) - -val add = Buffer.add -fun sep f = add " " #> f -fun enclose l r f = sep (add l #> f #> add r) -val par = enclose "(" ")" -fun app n f = (fn [] => sep (add n) | xs => par (add n #> fold f xs)) -fun line f = f #> add "\n" - -fun var i = add "?v" #> add (string_of_int i) - -fun sterm l (Old_SMT_Translate.SVar i) = sep (var (l - i - 1)) - | sterm l (Old_SMT_Translate.SApp (n, ts)) = app n (sterm l) ts - | sterm _ (Old_SMT_Translate.SLet _) = - raise Fail "SMT-LIB: unsupported let expression" - | sterm l (Old_SMT_Translate.SQua (q, ss, ps, w, t)) = - let - fun quant Old_SMT_Translate.SForall = add "forall" - | quant Old_SMT_Translate.SExists = add "exists" - val vs = map_index (apfst (Integer.add l)) ss - fun var_decl (i, s) = par (var i #> sep (add s)) - val sub = sterm (l + length ss) - fun pat kind ts = sep (add kind #> enclose "{" " }" (fold sub ts)) - fun pats (Old_SMT_Translate.SPat ts) = pat ":pat" ts - | pats (Old_SMT_Translate.SNoPat ts) = pat ":nopat" ts - fun weight NONE = I - | weight (SOME i) = - sep (add ":weight { " #> add (string_of_int i) #> add " }") - in - par (quant q #> fold var_decl vs #> sub t #> fold pats ps #> weight w) - end - -fun ssort sorts = sort fast_string_ord sorts -fun fsort funcs = sort (prod_ord fast_string_ord (K EQUAL)) funcs - -fun sdatatypes decls = - let - fun con (n, []) = sep (add n) - | con (n, sels) = par (add n #> - fold (fn (n, s) => par (add n #> sep (add s))) sels) - fun dtyp (n, decl) = add n #> fold con decl - in line (add ":datatypes " #> par (fold (par o dtyp) decls)) end - -fun serialize comments {header, sorts, dtyps, funcs} ts = - Buffer.empty - |> line (add "(benchmark Isabelle") - |> line (add ":status unknown") - |> fold (line o add) header - |> length sorts > 0 ? - line (add ":extrasorts" #> par (fold (sep o add) (ssort sorts))) - |> fold sdatatypes dtyps - |> length funcs > 0 ? ( - line (add ":extrafuns" #> add " (") #> - fold (fn (f, (ss, s)) => - line (sep (app f (sep o add) (ss @ [s])))) (fsort funcs) #> - line (add ")")) - |> fold (fn t => line (add ":assumption" #> sterm 0 t)) ts - |> line (add ":formula true)") - |> fold (fn str => line (add "; " #> add str)) comments - |> Buffer.content - - -(* interface *) - -fun translate_config ctxt = { - prefixes = { - sort_prefix = "S", - func_prefix = "f"}, - header = choose_logic ctxt, - is_fol = true, - has_datatypes = false, - serialize = serialize} - -val setup = Context.theory_map ( - setup_builtins #> - Old_SMT_Translate.add_config (smtlibC, translate_config)) - -end diff -r d10f0bbc7ea1 -r f595b7532dc9 src/HOL/Library/Old_SMT/old_z3_interface.ML --- a/src/HOL/Library/Old_SMT/old_z3_interface.ML Thu Apr 20 10:45:52 2017 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,239 +0,0 @@ -(* Title: HOL/Library/Old_SMT/old_z3_interface.ML - Author: Sascha Boehme, TU Muenchen - -Interface to Z3 based on a relaxed version of SMT-LIB. -*) - -signature OLD_Z3_INTERFACE = -sig - val smtlib_z3C: Old_SMT_Utils.class - val setup: theory -> theory - - datatype sym = Sym of string * sym list - type mk_builtins = { - mk_builtin_typ: sym -> typ option, - mk_builtin_num: theory -> int -> typ -> cterm option, - mk_builtin_fun: theory -> sym -> cterm list -> cterm option } - val add_mk_builtins: mk_builtins -> Context.generic -> Context.generic - val mk_builtin_typ: Proof.context -> sym -> typ option - val mk_builtin_num: Proof.context -> int -> typ -> cterm option - val mk_builtin_fun: Proof.context -> sym -> cterm list -> cterm option - - val is_builtin_theory_term: Proof.context -> term -> bool -end - -structure Old_Z3_Interface: OLD_Z3_INTERFACE = -struct - -val smtlib_z3C = Old_SMTLIB_Interface.smtlibC @ ["z3"] - - - -(* interface *) - -local - fun translate_config ctxt = - let - val {prefixes, header, is_fol, serialize, ...} = - Old_SMTLIB_Interface.translate_config ctxt - in - {prefixes=prefixes, header=header, is_fol=is_fol, serialize=serialize, - has_datatypes=true} - end - - fun is_div_mod @{const divide (int)} = true - | is_div_mod @{const modulo (int)} = true - | is_div_mod _ = false - - val div_by_z3div = @{lemma - "ALL k l. k div l = ( - if k = 0 | l = 0 then 0 - else if (0 < k & 0 < l) | (k < 0 & 0 < l) then z3div k l - else z3div (-k) (-l))" - by (simp add: z3div_def)} - - val mod_by_z3mod = @{lemma - "ALL k l. k mod l = ( - if l = 0 then k - else if k = 0 then 0 - else if (0 < k & 0 < l) | (k < 0 & 0 < l) then z3mod k l - else - z3mod (-k) (-l))" - by (simp add: z3mod_def)} - - val have_int_div_mod = - exists (Term.exists_subterm is_div_mod o Thm.prop_of) - - fun add_div_mod _ (thms, extra_thms) = - if have_int_div_mod thms orelse have_int_div_mod extra_thms then - (thms, div_by_z3div :: mod_by_z3mod :: extra_thms) - else (thms, extra_thms) - - val setup_builtins = - Old_SMT_Builtin.add_builtin_fun' smtlib_z3C (@{const times (int)}, "*") #> - Old_SMT_Builtin.add_builtin_fun' smtlib_z3C (@{const z3div}, "div") #> - Old_SMT_Builtin.add_builtin_fun' smtlib_z3C (@{const z3mod}, "mod") -in - -val setup = Context.theory_map ( - setup_builtins #> - Old_SMT_Normalize.add_extra_norm (smtlib_z3C, add_div_mod) #> - Old_SMT_Translate.add_config (smtlib_z3C, translate_config)) - -end - - - -(* constructors *) - -datatype sym = Sym of string * sym list - - -(** additional constructors **) - -type mk_builtins = { - mk_builtin_typ: sym -> typ option, - mk_builtin_num: theory -> int -> typ -> cterm option, - mk_builtin_fun: theory -> sym -> cterm list -> cterm option } - -fun chained _ [] = NONE - | chained f (b :: bs) = (case f b of SOME y => SOME y | NONE => chained f bs) - -fun chained_mk_builtin_typ bs sym = - chained (fn {mk_builtin_typ=mk, ...} : mk_builtins => mk sym) bs - -fun chained_mk_builtin_num ctxt bs i T = - let val thy = Proof_Context.theory_of ctxt - in chained (fn {mk_builtin_num=mk, ...} : mk_builtins => mk thy i T) bs end - -fun chained_mk_builtin_fun ctxt bs s cts = - let val thy = Proof_Context.theory_of ctxt - in chained (fn {mk_builtin_fun=mk, ...} : mk_builtins => mk thy s cts) bs end - -fun fst_int_ord ((i1, _), (i2, _)) = int_ord (i1, i2) - -structure Mk_Builtins = Generic_Data -( - type T = (int * mk_builtins) list - val empty = [] - val extend = I - fun merge data = Ord_List.merge fst_int_ord data -) - -fun add_mk_builtins mk = - Mk_Builtins.map (Ord_List.insert fst_int_ord (serial (), mk)) - -fun get_mk_builtins ctxt = map snd (Mk_Builtins.get (Context.Proof ctxt)) - - -(** basic and additional constructors **) - -fun mk_builtin_typ _ (Sym ("Bool", _)) = SOME @{typ bool} - | mk_builtin_typ _ (Sym ("Int", _)) = SOME @{typ int} - | mk_builtin_typ _ (Sym ("bool", _)) = SOME @{typ bool} (*FIXME: legacy*) - | mk_builtin_typ _ (Sym ("int", _)) = SOME @{typ int} (*FIXME: legacy*) - | mk_builtin_typ ctxt sym = chained_mk_builtin_typ (get_mk_builtins ctxt) sym - -fun mk_builtin_num _ i @{typ int} = SOME (Numeral.mk_cnumber @{ctyp int} i) - | mk_builtin_num ctxt i T = - chained_mk_builtin_num ctxt (get_mk_builtins ctxt) i T - -val mk_true = Thm.cterm_of @{context} (@{const Not} $ @{const False}) -val mk_false = Thm.cterm_of @{context} @{const False} -val mk_not = Thm.apply (Thm.cterm_of @{context} @{const Not}) -val mk_implies = Thm.mk_binop (Thm.cterm_of @{context} @{const HOL.implies}) -val mk_iff = Thm.mk_binop (Thm.cterm_of @{context} @{const HOL.eq (bool)}) -val conj = Thm.cterm_of @{context} @{const HOL.conj} -val disj = Thm.cterm_of @{context} @{const HOL.disj} - -fun mk_nary _ cu [] = cu - | mk_nary ct _ cts = uncurry (fold_rev (Thm.mk_binop ct)) (split_last cts) - -val eq = Old_SMT_Utils.mk_const_pat @{theory} @{const_name HOL.eq} Old_SMT_Utils.destT1 -fun mk_eq ct cu = Thm.mk_binop (Old_SMT_Utils.instT' ct eq) ct cu - -val if_term = - Old_SMT_Utils.mk_const_pat @{theory} @{const_name If} - (Old_SMT_Utils.destT1 o Old_SMT_Utils.destT2) -fun mk_if cc ct cu = - Thm.mk_binop (Thm.apply (Old_SMT_Utils.instT' ct if_term) cc) ct cu - -val nil_term = - Old_SMT_Utils.mk_const_pat @{theory} @{const_name Nil} Old_SMT_Utils.destT1 -val cons_term = - Old_SMT_Utils.mk_const_pat @{theory} @{const_name Cons} Old_SMT_Utils.destT1 -fun mk_list cT cts = - fold_rev (Thm.mk_binop (Old_SMT_Utils.instT cT cons_term)) cts - (Old_SMT_Utils.instT cT nil_term) - -val distinct = Old_SMT_Utils.mk_const_pat @{theory} @{const_name distinct} - (Old_SMT_Utils.destT1 o Old_SMT_Utils.destT1) -fun mk_distinct [] = mk_true - | mk_distinct (cts as (ct :: _)) = - Thm.apply (Old_SMT_Utils.instT' ct distinct) - (mk_list (Thm.ctyp_of_cterm ct) cts) - -val access = - Old_SMT_Utils.mk_const_pat @{theory} @{const_name fun_app} Old_SMT_Utils.destT1 -fun mk_access array = Thm.apply (Old_SMT_Utils.instT' array access) array - -val update = Old_SMT_Utils.mk_const_pat @{theory} @{const_name fun_upd} - (Thm.dest_ctyp o Old_SMT_Utils.destT1) -fun mk_update array index value = - let val cTs = Thm.dest_ctyp (Thm.ctyp_of_cterm array) - in - Thm.apply (Thm.mk_binop (Old_SMT_Utils.instTs cTs update) array index) value - end - -val mk_uminus = Thm.apply (Thm.cterm_of @{context} @{const uminus (int)}) -val add = Thm.cterm_of @{context} @{const plus (int)} -val int0 = Numeral.mk_cnumber @{ctyp int} 0 -val mk_sub = Thm.mk_binop (Thm.cterm_of @{context} @{const minus (int)}) -val mk_mul = Thm.mk_binop (Thm.cterm_of @{context} @{const times (int)}) -val mk_div = Thm.mk_binop (Thm.cterm_of @{context} @{const z3div}) -val mk_mod = Thm.mk_binop (Thm.cterm_of @{context} @{const z3mod}) -val mk_lt = Thm.mk_binop (Thm.cterm_of @{context} @{const less (int)}) -val mk_le = Thm.mk_binop (Thm.cterm_of @{context} @{const less_eq (int)}) - -fun mk_builtin_fun ctxt sym cts = - (case (sym, cts) of - (Sym ("true", _), []) => SOME mk_true - | (Sym ("false", _), []) => SOME mk_false - | (Sym ("not", _), [ct]) => SOME (mk_not ct) - | (Sym ("and", _), _) => SOME (mk_nary conj mk_true cts) - | (Sym ("or", _), _) => SOME (mk_nary disj mk_false cts) - | (Sym ("implies", _), [ct, cu]) => SOME (mk_implies ct cu) - | (Sym ("iff", _), [ct, cu]) => SOME (mk_iff ct cu) - | (Sym ("~", _), [ct, cu]) => SOME (mk_iff ct cu) - | (Sym ("xor", _), [ct, cu]) => SOME (mk_not (mk_iff ct cu)) - | (Sym ("if", _), [ct1, ct2, ct3]) => SOME (mk_if ct1 ct2 ct3) - | (Sym ("ite", _), [ct1, ct2, ct3]) => SOME (mk_if ct1 ct2 ct3) (* FIXME: remove *) - | (Sym ("=", _), [ct, cu]) => SOME (mk_eq ct cu) - | (Sym ("distinct", _), _) => SOME (mk_distinct cts) - | (Sym ("select", _), [ca, ck]) => SOME (Thm.apply (mk_access ca) ck) - | (Sym ("store", _), [ca, ck, cv]) => SOME (mk_update ca ck cv) - | _ => - (case (sym, try (Thm.typ_of_cterm o hd) cts, cts) of - (Sym ("+", _), SOME @{typ int}, _) => SOME (mk_nary add int0 cts) - | (Sym ("-", _), SOME @{typ int}, [ct]) => SOME (mk_uminus ct) - | (Sym ("-", _), SOME @{typ int}, [ct, cu]) => SOME (mk_sub ct cu) - | (Sym ("*", _), SOME @{typ int}, [ct, cu]) => SOME (mk_mul ct cu) - | (Sym ("div", _), SOME @{typ int}, [ct, cu]) => SOME (mk_div ct cu) - | (Sym ("mod", _), SOME @{typ int}, [ct, cu]) => SOME (mk_mod ct cu) - | (Sym ("<", _), SOME @{typ int}, [ct, cu]) => SOME (mk_lt ct cu) - | (Sym ("<=", _), SOME @{typ int}, [ct, cu]) => SOME (mk_le ct cu) - | (Sym (">", _), SOME @{typ int}, [ct, cu]) => SOME (mk_lt cu ct) - | (Sym (">=", _), SOME @{typ int}, [ct, cu]) => SOME (mk_le cu ct) - | _ => chained_mk_builtin_fun ctxt (get_mk_builtins ctxt) sym cts)) - - - -(* abstraction *) - -fun is_builtin_theory_term ctxt t = - if Old_SMT_Builtin.is_builtin_num ctxt t then true - else - (case Term.strip_comb t of - (Const c, ts) => Old_SMT_Builtin.is_builtin_fun ctxt c ts - | _ => false) - -end diff -r d10f0bbc7ea1 -r f595b7532dc9 src/HOL/Library/Old_SMT/old_z3_model.ML --- a/src/HOL/Library/Old_SMT/old_z3_model.ML Thu Apr 20 10:45:52 2017 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,337 +0,0 @@ -(* Title: HOL/Library/Old_SMT/old_z3_model.ML - Author: Sascha Boehme and Philipp Meyer, TU Muenchen - -Parser for counterexamples generated by Z3. -*) - -signature OLD_Z3_MODEL = -sig - val parse_counterex: Proof.context -> Old_SMT_Translate.recon -> string list -> - term list * term list -end - -structure Old_Z3_Model: OLD_Z3_MODEL = -struct - - -(* counterexample expressions *) - -datatype expr = True | False | Number of int * int option | Value of int | - Array of array | App of string * expr list -and array = Fresh of expr | Store of (array * expr) * expr - - -(* parsing *) - -val space = Scan.many Symbol.is_ascii_blank -fun spaced p = p --| space -fun in_parens p = spaced (Scan.$$ "(") |-- p --| spaced (Scan.$$ ")") -fun in_braces p = spaced (Scan.$$ "{") |-- p --| spaced (Scan.$$ "}") - -val digit = (fn - "0" => SOME 0 | "1" => SOME 1 | "2" => SOME 2 | "3" => SOME 3 | - "4" => SOME 4 | "5" => SOME 5 | "6" => SOME 6 | "7" => SOME 7 | - "8" => SOME 8 | "9" => SOME 9 | _ => NONE) - -val nat_num = spaced (Scan.repeat1 (Scan.some digit) >> - (fn ds => fold (fn d => fn i => i * 10 + d) ds 0)) -val int_num = spaced (Scan.optional ($$ "-" >> K (fn i => ~i)) I :|-- - (fn sign => nat_num >> sign)) - -val is_char = Symbol.is_ascii_letter orf Symbol.is_ascii_digit orf - member (op =) (raw_explode "_+*-/%~=<>$&|?!.@^#") -val name = spaced (Scan.many1 is_char >> implode) - -fun $$$ s = spaced (Scan.this_string s) - -fun array_expr st = st |> in_parens ( - $$$ "const" |-- expr >> Fresh || - $$$ "store" |-- array_expr -- expr -- expr >> Store) - -and expr st = st |> ( - $$$ "true" >> K True || - $$$ "false" >> K False || - int_num -- Scan.option ($$$ "/" |-- int_num) >> Number || - $$$ "val!" |-- nat_num >> Value || - name >> (App o rpair []) || - array_expr >> Array || - in_parens (name -- Scan.repeat1 expr) >> App) - -fun args st = ($$$ "->" >> K [] || expr ::: args) st -val args_case = args -- expr -val else_case = $$$ "else" -- $$$ "->" |-- expr >> pair ([] : expr list) - -val func = - let fun cases st = (else_case >> single || args_case ::: cases) st - in in_braces cases end - -val cex = space |-- - Scan.repeat (name --| $$$ "->" -- (func || expr >> (single o pair []))) - -fun resolve terms ((n, k), cases) = - (case Symtab.lookup terms n of - NONE => NONE - | SOME t => SOME ((t, k), cases)) - -fun annotate _ (_, []) = NONE - | annotate terms (n, [([], c)]) = resolve terms ((n, 0), (c, [])) - | annotate _ (_, [_]) = NONE - | annotate terms (n, cases as (args, _) :: _) = - let val (cases', (_, else_case)) = split_last cases - in resolve terms ((n, length args), (else_case, cases')) end - -fun read_cex terms ls = - maps (cons "\n" o raw_explode) ls - |> try (fst o Scan.finite Symbol.stopper cex) - |> the_default [] - |> map_filter (annotate terms) - - -(* translation into terms *) - -fun max_value vs = - let - fun max_val_expr (Value i) = Integer.max i - | max_val_expr (App (_, es)) = fold max_val_expr es - | max_val_expr (Array a) = max_val_array a - | max_val_expr _ = I - - and max_val_array (Fresh e) = max_val_expr e - | max_val_array (Store ((a, e1), e2)) = - max_val_array a #> max_val_expr e1 #> max_val_expr e2 - - fun max_val (_, (ec, cs)) = - max_val_expr ec #> fold (fn (es, e) => fold max_val_expr (e :: es)) cs - - in fold max_val vs ~1 end - -fun with_context terms f vs = fst (fold_map f vs (terms, max_value vs + 1)) - -fun get_term n T es (cx as (terms, next_val)) = - (case Symtab.lookup terms n of - SOME t => ((t, es), cx) - | NONE => - let val t = Var (("skolem", next_val), T) - in ((t, []), (Symtab.update (n, t) terms, next_val + 1)) end) - -fun trans_expr _ True = pair @{const True} - | trans_expr _ False = pair @{const False} - | trans_expr T (Number (i, NONE)) = pair (HOLogic.mk_number T i) - | trans_expr T (Number (i, SOME j)) = - pair (Const (@{const_name divide}, [T, T] ---> T) $ - HOLogic.mk_number T i $ HOLogic.mk_number T j) - | trans_expr T (Value i) = pair (Var (("value", i), T)) - | trans_expr T (Array a) = trans_array T a - | trans_expr T (App (n, es)) = get_term n T es #-> (fn (t, es') => - let val Ts = fst (Old_SMT_Utils.dest_funT (length es') (Term.fastype_of t)) - in - fold_map (uncurry trans_expr) (Ts ~~ es') #>> Term.list_comb o pair t - end) - -and trans_array T a = - let val (dT, rT) = Term.dest_funT T - in - (case a of - Fresh e => trans_expr rT e #>> (fn t => Abs ("x", dT, t)) - | Store ((a', e1), e2) => - trans_array T a' ##>> trans_expr dT e1 ##>> trans_expr rT e2 #>> - (fn ((m, k), v) => - Const (@{const_name fun_upd}, [T, dT, rT] ---> T) $ m $ k $ v)) - end - -fun trans_pattern T ([], e) = trans_expr T e #>> pair [] - | trans_pattern T (arg :: args, e) = - trans_expr (Term.domain_type T) arg ##>> - trans_pattern (Term.range_type T) (args, e) #>> - (fn (arg', (args', e')) => (arg' :: args', e')) - -fun mk_fun_upd T U = Const (@{const_name fun_upd}, [T --> U, T, U, T] ---> U) - -fun mk_update ([], u) _ = u - | mk_update ([t], u) f = - uncurry mk_fun_upd (Term.dest_funT (Term.fastype_of f)) $ f $ t $ u - | mk_update (t :: ts, u) f = - let - val (dT, rT) = Term.dest_funT (Term.fastype_of f) - val (dT', rT') = Term.dest_funT rT - in - mk_fun_upd dT rT $ f $ t $ - mk_update (ts, u) (absdummy dT' (Const ("_", rT'))) - end - -fun mk_lambda Ts (t, pats) = - fold_rev absdummy Ts t |> fold mk_update pats - -fun translate ((t, k), (e, cs)) = - let - val T = Term.fastype_of t - val (Us, U) = Old_SMT_Utils.dest_funT k (Term.fastype_of t) - - fun mk_full_def u' pats = - pats - |> filter_out (fn (_, u) => u aconv u') - |> HOLogic.mk_eq o pair t o mk_lambda Us o pair u' - - fun mk_eq (us, u) = HOLogic.mk_eq (Term.list_comb (t, us), u) - fun mk_eqs u' [] = [HOLogic.mk_eq (t, u')] - | mk_eqs _ pats = map mk_eq pats - in - trans_expr U e ##>> - (if k = 0 then pair [] else fold_map (trans_pattern T) cs) #>> - (fn (u', pats) => (mk_eqs u' pats, mk_full_def u' pats)) - end - - -(* normalization *) - -fun partition_eqs f = - let - fun part t (xs, ts) = - (case try HOLogic.dest_eq t of - SOME (l, r) => (case f l r of SOME x => (x::xs, ts) | _ => (xs, t::ts)) - | NONE => (xs, t :: ts)) - in (fn ts => fold part ts ([], [])) end - -fun first_eq pred = - let - fun part _ [] = NONE - | part us (t :: ts) = - (case try (pred o HOLogic.dest_eq) t of - SOME (SOME lr) => SOME (lr, fold cons us ts) - | _ => part (t :: us) ts) - in (fn ts => part [] ts) end - -fun replace_vars tab = - let - fun repl v = the_default v (AList.lookup (op aconv) tab v) - fun replace (v as Var _) = repl v - | replace (v as Free _) = repl v - | replace t = t - in map (Term.map_aterms replace) end - -fun remove_int_nat_coercions (eqs, defs) = - let - fun mk_nat_num t i = - (case try HOLogic.dest_number i of - SOME (_, n) => SOME (t, HOLogic.mk_number @{typ nat} n) - | NONE => NONE) - fun nat_of (@{const of_nat (int)} $ (t as Var _)) i = mk_nat_num t i - | nat_of (@{const nat} $ i) (t as Var _) = mk_nat_num t i - | nat_of _ _ = NONE - val (nats, eqs') = partition_eqs nat_of eqs - - fun is_coercion t = - (case try HOLogic.dest_eq t of - SOME (@{const of_nat (int)}, _) => true - | SOME (@{const nat}, _) => true - | _ => false) - in apply2 (replace_vars nats) (eqs', filter_out is_coercion defs) end - -fun unfold_funapp (eqs, defs) = - let - fun unfold_app (Const (@{const_name fun_app}, _) $ f $ t) = f $ t - | unfold_app t = t - fun unfold_eq ((eq as Const (@{const_name HOL.eq}, _)) $ t $ u) = - eq $ unfold_app t $ u - | unfold_eq t = t - - fun is_fun_app t = - (case try HOLogic.dest_eq t of - SOME (Const (@{const_name fun_app}, _), _) => true - | _ => false) - - in (map unfold_eq eqs, filter_out is_fun_app defs) end - -val unfold_eqs = - let - val is_ground = not o Term.exists_subterm Term.is_Var - fun is_non_rec (v, t) = not (Term.exists_subterm (equal v) t) - - fun rewr_var (l as Var _, r) = if is_ground r then SOME (l, r) else NONE - | rewr_var (r, l as Var _) = if is_ground r then SOME (l, r) else NONE - | rewr_var _ = NONE - - fun rewr_free' e = if is_non_rec e then SOME e else NONE - fun rewr_free (e as (Free _, _)) = rewr_free' e - | rewr_free (e as (_, Free _)) = rewr_free' (swap e) - | rewr_free _ = NONE - - fun is_trivial (Const (@{const_name HOL.eq}, _) $ t $ u) = t aconv u - | is_trivial _ = false - - fun replace r = replace_vars [r] #> filter_out is_trivial - - fun unfold_vars (es, ds) = - (case first_eq rewr_var es of - SOME (lr, es') => unfold_vars (apply2 (replace lr) (es', ds)) - | NONE => (es, ds)) - - fun unfold_frees ues (es, ds) = - (case first_eq rewr_free es of - SOME (lr, es') => - apply2 (replace lr) (es', ds) - |> unfold_frees (HOLogic.mk_eq lr :: replace lr ues) - | NONE => (ues @ es, ds)) - - in unfold_vars #> unfold_frees [] end - -fun swap_free ((eq as Const (@{const_name HOL.eq}, _)) $ t $ (u as Free _)) = - eq $ u $ t - | swap_free t = t - -fun frees_for_vars ctxt (eqs, defs) = - let - fun fresh_free i T (cx as (frees, ctxt)) = - (case Inttab.lookup frees i of - SOME t => (t, cx) - | NONE => - let - val (n, ctxt') = yield_singleton Variable.variant_fixes "" ctxt - val t = Free (n, T) - in (t, (Inttab.update (i, t) frees, ctxt')) end) - - fun repl_var (Var ((_, i), T)) = fresh_free i T - | repl_var (t $ u) = repl_var t ##>> repl_var u #>> op $ - | repl_var (Abs (n, T, t)) = repl_var t #>> (fn t' => Abs (n, T, t')) - | repl_var t = pair t - in - (Inttab.empty, ctxt) - |> fold_map repl_var eqs - ||>> fold_map repl_var defs - |> fst - end - - -(* overall procedure *) - -val is_free_constraint = Term.exists_subterm (fn Free _ => true | _ => false) - -fun is_free_def (Const (@{const_name HOL.eq}, _) $ Free _ $ _) = true - | is_free_def _ = false - -fun defined tp = - try (apply2 (fst o HOLogic.dest_eq)) tp - |> the_default false o Option.map (op aconv) - -fun add_free_defs free_cs defs = - let val (free_defs, defs') = List.partition is_free_def defs - in (free_cs @ filter_out (member defined free_cs) free_defs, defs') end - -fun is_const_def (Const (@{const_name HOL.eq}, _) $ Const _ $ _) = true - | is_const_def _ = false - -fun parse_counterex ctxt ({terms, ...} : Old_SMT_Translate.recon) ls = - read_cex terms ls - |> with_context terms translate - |> apfst flat o split_list - |> remove_int_nat_coercions - |> unfold_funapp - |> unfold_eqs - |>> map swap_free - |>> filter is_free_constraint - |-> add_free_defs - |> frees_for_vars ctxt - ||> filter is_const_def - -end - diff -r d10f0bbc7ea1 -r f595b7532dc9 src/HOL/Library/Old_SMT/old_z3_proof_literals.ML --- a/src/HOL/Library/Old_SMT/old_z3_proof_literals.ML Thu Apr 20 10:45:52 2017 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,363 +0,0 @@ -(* Title: HOL/Library/Old_SMT/old_z3_proof_literals.ML - Author: Sascha Boehme, TU Muenchen - -Proof tools related to conjunctions and disjunctions. -*) - -signature OLD_Z3_PROOF_LITERALS = -sig - (*literal table*) - type littab = thm Termtab.table - val make_littab: thm list -> littab - val insert_lit: thm -> littab -> littab - val delete_lit: thm -> littab -> littab - val lookup_lit: littab -> term -> thm option - val get_first_lit: (term -> bool) -> littab -> thm option - - (*rules*) - val true_thm: thm - val rewrite_true: thm - - (*properties*) - val is_conj: term -> bool - val is_disj: term -> bool - val exists_lit: bool -> (term -> bool) -> term -> bool - val negate: cterm -> cterm - - (*proof tools*) - val explode: bool -> bool -> bool -> term list -> thm -> thm list - val join: bool -> littab -> term -> thm - val prove_conj_disj_eq: cterm -> thm -end - -structure Old_Z3_Proof_Literals: OLD_Z3_PROOF_LITERALS = -struct - - - -(* literal table *) - -type littab = thm Termtab.table - -fun make_littab thms = - fold (Termtab.update o `Old_SMT_Utils.prop_of) thms Termtab.empty - -fun insert_lit thm = Termtab.update (`Old_SMT_Utils.prop_of thm) -fun delete_lit thm = Termtab.delete (Old_SMT_Utils.prop_of thm) -fun lookup_lit lits = Termtab.lookup lits -fun get_first_lit f = - Termtab.get_first (fn (t, thm) => if f t then SOME thm else NONE) - - - -(* rules *) - -val true_thm = @{lemma "~False" by simp} -val rewrite_true = @{lemma "True == ~ False" by simp} - - - -(* properties and term operations *) - -val is_neg = (fn @{const Not} $ _ => true | _ => false) -fun is_neg' f = (fn @{const Not} $ t => f t | _ => false) -val is_dneg = is_neg' is_neg -val is_conj = (fn @{const HOL.conj} $ _ $ _ => true | _ => false) -val is_disj = (fn @{const HOL.disj} $ _ $ _ => true | _ => false) - -fun dest_disj_term' f = (fn - @{const Not} $ (@{const HOL.disj} $ t $ u) => SOME (f t, f u) - | _ => NONE) - -val dest_conj_term = (fn @{const HOL.conj} $ t $ u => SOME (t, u) | _ => NONE) -val dest_disj_term = - dest_disj_term' (fn @{const Not} $ t => t | t => @{const Not} $ t) - -fun exists_lit is_conj P = - let - val dest = if is_conj then dest_conj_term else dest_disj_term - fun exists t = P t orelse - (case dest t of - SOME (t1, t2) => exists t1 orelse exists t2 - | NONE => false) - in exists end - -val negate = Thm.apply (Thm.cterm_of @{context} @{const Not}) - - - -(* proof tools *) - -(** explosion of conjunctions and disjunctions **) - -local - val precomp = Old_Z3_Proof_Tools.precompose2 - - fun destc ct = Thm.dest_binop (Thm.dest_arg ct) - val dest_conj1 = precomp destc @{thm conjunct1} - val dest_conj2 = precomp destc @{thm conjunct2} - fun dest_conj_rules t = - dest_conj_term t |> Option.map (K (dest_conj1, dest_conj2)) - - fun destd f ct = f (Thm.dest_binop (Thm.dest_arg (Thm.dest_arg ct))) - val dn1 = apfst Thm.dest_arg and dn2 = apsnd Thm.dest_arg - val dest_disj1 = precomp (destd I) @{lemma "~(P | Q) ==> ~P" by fast} - val dest_disj2 = precomp (destd dn1) @{lemma "~(~P | Q) ==> P" by fast} - val dest_disj3 = precomp (destd I) @{lemma "~(P | Q) ==> ~Q" by fast} - val dest_disj4 = precomp (destd dn2) @{lemma "~(P | ~Q) ==> Q" by fast} - - fun dest_disj_rules t = - (case dest_disj_term' is_neg t of - SOME (true, true) => SOME (dest_disj2, dest_disj4) - | SOME (true, false) => SOME (dest_disj2, dest_disj3) - | SOME (false, true) => SOME (dest_disj1, dest_disj4) - | SOME (false, false) => SOME (dest_disj1, dest_disj3) - | NONE => NONE) - - fun destn ct = [Thm.dest_arg (Thm.dest_arg (Thm.dest_arg ct))] - val dneg_rule = Old_Z3_Proof_Tools.precompose destn @{thm notnotD} -in - -(* - explode a term into literals and collect all rules to be able to deduce - particular literals afterwards -*) -fun explode_term is_conj = - let - val dest = if is_conj then dest_conj_term else dest_disj_term - val dest_rules = if is_conj then dest_conj_rules else dest_disj_rules - - fun add (t, rs) = Termtab.map_default (t, rs) - (fn rs' => if length rs' < length rs then rs' else rs) - - fun explode1 rules t = - (case dest t of - SOME (t1, t2) => - let val (rule1, rule2) = the (dest_rules t) - in - explode1 (rule1 :: rules) t1 #> - explode1 (rule2 :: rules) t2 #> - add (t, rev rules) - end - | NONE => add (t, rev rules)) - - fun explode0 (@{const Not} $ (@{const Not} $ t)) = - Termtab.make [(t, [dneg_rule])] - | explode0 t = explode1 [] t Termtab.empty - - in explode0 end - -(* - extract a literal by applying previously collected rules -*) -fun extract_lit thm rules = fold Old_Z3_Proof_Tools.compose rules thm - - -(* - explode a theorem into its literals -*) -fun explode is_conj full keep_intermediate stop_lits = - let - val dest_rules = if is_conj then dest_conj_rules else dest_disj_rules - val tab = fold (Termtab.update o rpair ()) stop_lits Termtab.empty - - fun explode1 thm = - if Termtab.defined tab (Old_SMT_Utils.prop_of thm) then cons thm - else - (case dest_rules (Old_SMT_Utils.prop_of thm) of - SOME (rule1, rule2) => - explode2 rule1 thm #> - explode2 rule2 thm #> - keep_intermediate ? cons thm - | NONE => cons thm) - - and explode2 dest_rule thm = - if full orelse - exists_lit is_conj (Termtab.defined tab) (Old_SMT_Utils.prop_of thm) - then explode1 (Old_Z3_Proof_Tools.compose dest_rule thm) - else cons (Old_Z3_Proof_Tools.compose dest_rule thm) - - fun explode0 thm = - if not is_conj andalso is_dneg (Old_SMT_Utils.prop_of thm) - then [Old_Z3_Proof_Tools.compose dneg_rule thm] - else explode1 thm [] - - in explode0 end - -end - - - -(** joining of literals to conjunctions or disjunctions **) - -local - fun on_cprem i f thm = f (Thm.cprem_of thm i) - fun on_cprop f thm = f (Thm.cprop_of thm) - fun precomp2 f g thm = (on_cprem 1 f thm, on_cprem 2 g thm, f, g, thm) - fun comp2 (cv1, cv2, f, g, rule) thm1 thm2 = - Thm.instantiate ([], - [(dest_Var (Thm.term_of cv1), on_cprop f thm1), - (dest_Var (Thm.term_of cv2), on_cprop g thm2)]) rule - |> Old_Z3_Proof_Tools.discharge thm1 |> Old_Z3_Proof_Tools.discharge thm2 - - fun d1 ct = Thm.dest_arg ct and d2 ct = Thm.dest_arg (Thm.dest_arg ct) - - val conj_rule = precomp2 d1 d1 @{thm conjI} - fun comp_conj ((_, thm1), (_, thm2)) = comp2 conj_rule thm1 thm2 - - val disj1 = precomp2 d2 d2 @{lemma "~P ==> ~Q ==> ~(P | Q)" by fast} - val disj2 = precomp2 d2 d1 @{lemma "~P ==> Q ==> ~(P | ~Q)" by fast} - val disj3 = precomp2 d1 d2 @{lemma "P ==> ~Q ==> ~(~P | Q)" by fast} - val disj4 = precomp2 d1 d1 @{lemma "P ==> Q ==> ~(~P | ~Q)" by fast} - - fun comp_disj ((false, thm1), (false, thm2)) = comp2 disj1 thm1 thm2 - | comp_disj ((false, thm1), (true, thm2)) = comp2 disj2 thm1 thm2 - | comp_disj ((true, thm1), (false, thm2)) = comp2 disj3 thm1 thm2 - | comp_disj ((true, thm1), (true, thm2)) = comp2 disj4 thm1 thm2 - - fun dest_conj (@{const HOL.conj} $ t $ u) = ((false, t), (false, u)) - | dest_conj t = raise TERM ("dest_conj", [t]) - - val neg = (fn @{const Not} $ t => (true, t) | t => (false, @{const Not} $ t)) - fun dest_disj (@{const Not} $ (@{const HOL.disj} $ t $ u)) = (neg t, neg u) - | dest_disj t = raise TERM ("dest_disj", [t]) - - val precomp = Old_Z3_Proof_Tools.precompose - val dnegE = precomp (single o d2 o d1) @{thm notnotD} - val dnegI = precomp (single o d1) @{lemma "P ==> ~~P" by fast} - fun as_dneg f t = f (@{const Not} $ (@{const Not} $ t)) - - val precomp2 = Old_Z3_Proof_Tools.precompose2 - fun dni f = apsnd f o Thm.dest_binop o f o d1 - val negIffE = precomp2 (dni d1) @{lemma "~(P = (~Q)) ==> Q = P" by fast} - val negIffI = precomp2 (dni I) @{lemma "P = Q ==> ~(Q = (~P))" by fast} - val iff_const = @{const HOL.eq (bool)} - fun as_negIff f (@{const HOL.eq (bool)} $ t $ u) = - f (@{const Not} $ (iff_const $ u $ (@{const Not} $ t))) - | as_negIff _ _ = NONE -in - -fun join is_conj littab t = - let - val comp = if is_conj then comp_conj else comp_disj - val dest = if is_conj then dest_conj else dest_disj - - val lookup = lookup_lit littab - - fun lookup_rule t = - (case t of - @{const Not} $ (@{const Not} $ t) => - (Old_Z3_Proof_Tools.compose dnegI, lookup t) - | @{const Not} $ (@{const HOL.eq (bool)} $ t $ (@{const Not} $ u)) => - (Old_Z3_Proof_Tools.compose negIffI, lookup (iff_const $ u $ t)) - | @{const Not} $ ((eq as Const (@{const_name HOL.eq}, _)) $ t $ u) => - let fun rewr lit = lit COMP @{thm not_sym} - in (rewr, lookup (@{const Not} $ (eq $ u $ t))) end - | _ => - (case as_dneg lookup t of - NONE => (Old_Z3_Proof_Tools.compose negIffE, as_negIff lookup t) - | x => (Old_Z3_Proof_Tools.compose dnegE, x))) - - fun join1 (s, t) = - (case lookup t of - SOME lit => (s, lit) - | NONE => - (case lookup_rule t of - (rewrite, SOME lit) => (s, rewrite lit) - | (_, NONE) => (s, comp (apply2 join1 (dest t))))) - - in snd (join1 (if is_conj then (false, t) else (true, t))) end - -end - - - -(** proving equality of conjunctions or disjunctions **) - -fun iff_intro thm1 thm2 = thm2 COMP (thm1 COMP @{thm iffI}) - -local - val cp1 = @{lemma "(~P) = (~Q) ==> P = Q" by simp} - val cp2 = @{lemma "(~P) = Q ==> P = (~Q)" by fastforce} - val cp3 = @{lemma "P = (~Q) ==> (~P) = Q" by simp} -in -fun contrapos1 prove (ct, cu) = prove (negate ct, negate cu) COMP cp1 -fun contrapos2 prove (ct, cu) = prove (negate ct, Thm.dest_arg cu) COMP cp2 -fun contrapos3 prove (ct, cu) = prove (Thm.dest_arg ct, negate cu) COMP cp3 -end - - -local - val contra_rule = @{lemma "P ==> ~P ==> False" by (rule notE)} - fun contra_left conj thm = - let - val rules = explode_term conj (Old_SMT_Utils.prop_of thm) - fun contra_lits (t, rs) = - (case t of - @{const Not} $ u => Termtab.lookup rules u |> Option.map (pair rs) - | _ => NONE) - in - (case Termtab.lookup rules @{const False} of - SOME rs => extract_lit thm rs - | NONE => - the (Termtab.get_first contra_lits rules) - |> apply2 (extract_lit thm) - |> (fn (nlit, plit) => nlit COMP (plit COMP contra_rule))) - end - - val falseE_v = dest_Var (Thm.term_of (Thm.dest_arg (Thm.dest_arg (Thm.cprop_of @{thm FalseE})))) - fun contra_right ct = Thm.instantiate ([], [(falseE_v, ct)]) @{thm FalseE} -in -fun contradict conj ct = - iff_intro (Old_Z3_Proof_Tools.under_assumption (contra_left conj) ct) - (contra_right ct) -end - - -local - fun prove_eq l r (cl, cr) = - let - fun explode' is_conj = explode is_conj true (l <> r) [] - fun make_tab is_conj thm = make_littab (true_thm :: explode' is_conj thm) - fun prove is_conj ct tab = join is_conj tab (Thm.term_of ct) - - val thm1 = Old_Z3_Proof_Tools.under_assumption (prove r cr o make_tab l) cl - val thm2 = Old_Z3_Proof_Tools.under_assumption (prove l cl o make_tab r) cr - in iff_intro thm1 thm2 end - - datatype conj_disj = CONJ | DISJ | NCON | NDIS - fun kind_of t = - if is_conj t then SOME CONJ - else if is_disj t then SOME DISJ - else if is_neg' is_conj t then SOME NCON - else if is_neg' is_disj t then SOME NDIS - else NONE -in - -fun prove_conj_disj_eq ct = - let val cp as (cl, cr) = Thm.dest_binop (Thm.dest_arg ct) - in - (case (kind_of (Thm.term_of cl), Thm.term_of cr) of - (SOME CONJ, @{const False}) => contradict true cl - | (SOME DISJ, @{const Not} $ @{const False}) => - contrapos2 (contradict false o fst) cp - | (kl, _) => - (case (kl, kind_of (Thm.term_of cr)) of - (SOME CONJ, SOME CONJ) => prove_eq true true cp - | (SOME CONJ, SOME NDIS) => prove_eq true false cp - | (SOME CONJ, _) => prove_eq true true cp - | (SOME DISJ, SOME DISJ) => contrapos1 (prove_eq false false) cp - | (SOME DISJ, SOME NCON) => contrapos2 (prove_eq false true) cp - | (SOME DISJ, _) => contrapos1 (prove_eq false false) cp - | (SOME NCON, SOME NCON) => contrapos1 (prove_eq true true) cp - | (SOME NCON, SOME DISJ) => contrapos3 (prove_eq true false) cp - | (SOME NCON, NONE) => contrapos3 (prove_eq true false) cp - | (SOME NDIS, SOME NDIS) => prove_eq false false cp - | (SOME NDIS, SOME CONJ) => prove_eq false true cp - | (SOME NDIS, NONE) => prove_eq false true cp - | _ => raise CTERM ("prove_conj_disj_eq", [ct]))) - end - -end - -end diff -r d10f0bbc7ea1 -r f595b7532dc9 src/HOL/Library/Old_SMT/old_z3_proof_methods.ML --- a/src/HOL/Library/Old_SMT/old_z3_proof_methods.ML Thu Apr 20 10:45:52 2017 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,149 +0,0 @@ -(* Title: HOL/Library/Old_SMT/old_z3_proof_methods.ML - Author: Sascha Boehme, TU Muenchen - -Proof methods for Z3 proof reconstruction. -*) - -signature OLD_Z3_PROOF_METHODS = -sig - val prove_injectivity: Proof.context -> cterm -> thm - val prove_ite: Proof.context -> cterm -> thm -end - -structure Old_Z3_Proof_Methods: OLD_Z3_PROOF_METHODS = -struct - - -fun apply tac st = - (case Seq.pull (tac 1 st) of - NONE => raise THM ("tactic failed", 1, [st]) - | SOME (st', _) => st') - - - -(* if-then-else *) - -val pull_ite = mk_meta_eq - @{lemma "f (if P then x else y) = (if P then f x else f y)" by simp} - -fun pull_ites_conv ct = - (Conv.rewr_conv pull_ite then_conv - Conv.binop_conv (Conv.try_conv pull_ites_conv)) ct - -fun prove_ite ctxt = - Old_Z3_Proof_Tools.by_tac ctxt ( - CONVERSION (Conv.arg_conv (Conv.arg1_conv pull_ites_conv)) - THEN' resolve_tac ctxt @{thms refl}) - - - -(* injectivity *) - -local - -val B = @{typ bool} -fun mk_univ T = Const (@{const_name top}, HOLogic.mk_setT T) -fun mk_inj_on T U = - Const (@{const_name inj_on}, (T --> U) --> HOLogic.mk_setT T --> B) -fun mk_inv_into T U = - Const (@{const_name inv_into}, [HOLogic.mk_setT T, T --> U, U] ---> T) - -fun mk_inv_of ctxt ct = - let - val (dT, rT) = Term.dest_funT (Thm.typ_of_cterm ct) - val inv = Thm.cterm_of ctxt (mk_inv_into dT rT) - val univ = Thm.cterm_of ctxt (mk_univ dT) - in Thm.mk_binop inv univ ct end - -fun mk_inj_prop ctxt ct = - let - val (dT, rT) = Term.dest_funT (Thm.typ_of_cterm ct) - val inj = Thm.cterm_of ctxt (mk_inj_on dT rT) - val univ = Thm.cterm_of ctxt (mk_univ dT) - in Old_SMT_Utils.mk_cprop (Thm.mk_binop inj ct univ) end - - -val disjE = @{lemma "~P | Q ==> P ==> Q" by fast} - -fun prove_inj_prop ctxt def lhs = - let - val (ct, ctxt') = Old_SMT_Utils.dest_all_cabs (Thm.rhs_of def) ctxt - val rule = disjE OF [Object_Logic.rulify ctxt' (Thm.assume lhs)] - in - Goal.init (mk_inj_prop ctxt' (Thm.dest_arg ct)) - |> apply (resolve_tac ctxt' @{thms injI}) - |> apply (Tactic.solve_tac ctxt' [rule, rule RS @{thm sym}]) - |> Goal.norm_result ctxt' o Goal.finish ctxt' - |> singleton (Variable.export ctxt' ctxt) - end - -fun prove_rhs ctxt def lhs = - Old_Z3_Proof_Tools.by_tac ctxt ( - CONVERSION (Conv.top_sweep_conv (K (Conv.rewr_conv def)) ctxt) - THEN' REPEAT_ALL_NEW (match_tac ctxt @{thms allI}) - THEN' resolve_tac ctxt [@{thm inv_f_f} OF [prove_inj_prop ctxt def lhs]]) - - -fun expand thm ct = - let - val cpat = Thm.dest_arg (Thm.rhs_of thm) - val (cl, cr) = Thm.dest_binop (Thm.dest_arg (Thm.dest_arg1 ct)) - val thm1 = Thm.instantiate (Thm.match (cpat, cl)) thm - val thm2 = Thm.instantiate (Thm.match (cpat, cr)) thm - in Conv.arg_conv (Conv.binop_conv (Conv.rewrs_conv [thm1, thm2])) ct end - -fun prove_lhs ctxt rhs = - let - val eq = Thm.symmetric (mk_meta_eq (Object_Logic.rulify ctxt (Thm.assume rhs))) - val conv = Old_SMT_Utils.binders_conv (K (expand eq)) ctxt - in - Old_Z3_Proof_Tools.by_tac ctxt ( - CONVERSION (Old_SMT_Utils.prop_conv conv) - THEN' Simplifier.simp_tac (put_simpset HOL_ss ctxt)) - end - - -fun mk_inv_def ctxt rhs = - let - val (ct, ctxt') = - Old_SMT_Utils.dest_all_cbinders (Old_SMT_Utils.dest_cprop rhs) ctxt - val (cl, cv) = Thm.dest_binop ct - val (cg, (cargs, cf)) = Drule.strip_comb cl ||> split_last - val cu = fold_rev Thm.lambda cargs (mk_inv_of ctxt' (Thm.lambda cv cf)) - in Thm.assume (Old_SMT_Utils.mk_cequals cg cu) end - -fun prove_inj_eq ctxt ct = - let - val (lhs, rhs) = - apply2 Old_SMT_Utils.mk_cprop (Thm.dest_binop (Old_SMT_Utils.dest_cprop ct)) - val lhs_thm = Thm.implies_intr rhs (prove_lhs ctxt rhs lhs) - val rhs_thm = - Thm.implies_intr lhs (prove_rhs ctxt (mk_inv_def ctxt rhs) lhs rhs) - in lhs_thm COMP (rhs_thm COMP @{thm iffI}) end - - -val swap_eq_thm = mk_meta_eq @{thm eq_commute} -val swap_disj_thm = mk_meta_eq @{thm disj_commute} - -fun swap_conv dest eq = - Old_SMT_Utils.if_true_conv ((op <) o apply2 Term.size_of_term o dest) - (Conv.rewr_conv eq) - -val swap_eq_conv = swap_conv HOLogic.dest_eq swap_eq_thm -val swap_disj_conv = swap_conv Old_SMT_Utils.dest_disj swap_disj_thm - -fun norm_conv ctxt = - swap_eq_conv then_conv - Conv.arg1_conv (Old_SMT_Utils.binders_conv (K swap_disj_conv) ctxt) then_conv - Conv.arg_conv (Old_SMT_Utils.binders_conv (K swap_eq_conv) ctxt) - -in - -fun prove_injectivity ctxt = - Old_Z3_Proof_Tools.by_tac ctxt ( - CONVERSION (Old_SMT_Utils.prop_conv (norm_conv ctxt)) - THEN' CSUBGOAL (uncurry (resolve_tac ctxt o single o prove_inj_eq ctxt))) - -end - -end diff -r d10f0bbc7ea1 -r f595b7532dc9 src/HOL/Library/Old_SMT/old_z3_proof_parser.ML --- a/src/HOL/Library/Old_SMT/old_z3_proof_parser.ML Thu Apr 20 10:45:52 2017 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,446 +0,0 @@ -(* Title: HOL/Library/Old_SMT/old_z3_proof_parser.ML - Author: Sascha Boehme, TU Muenchen - -Parser for Z3 proofs. -*) - -signature OLD_Z3_PROOF_PARSER = -sig - (*proof rules*) - datatype rule = True_Axiom | Asserted | Goal | Modus_Ponens | Reflexivity | - Symmetry | Transitivity | Transitivity_Star | Monotonicity | Quant_Intro | - Distributivity | And_Elim | Not_Or_Elim | Rewrite | Rewrite_Star | - Pull_Quant | Pull_Quant_Star | Push_Quant | Elim_Unused_Vars | - Dest_Eq_Res | Quant_Inst | Hypothesis | Lemma | Unit_Resolution | - Iff_True | Iff_False | Commutativity | Def_Axiom | Intro_Def | Apply_Def | - Iff_Oeq | Nnf_Pos | Nnf_Neg | Nnf_Star | Cnf_Star | Skolemize | - Modus_Ponens_Oeq | Th_Lemma of string list - val string_of_rule: rule -> string - - (*proof parser*) - datatype proof_step = Proof_Step of { - rule: rule, - args: cterm list, - prems: int list, - prop: cterm } - val parse: Proof.context -> typ Symtab.table -> term Symtab.table -> - string list -> - (int * cterm) list * (int * proof_step) list * string list * Proof.context -end - -structure Old_Z3_Proof_Parser: OLD_Z3_PROOF_PARSER = -struct - - -(* proof rules *) - -datatype rule = True_Axiom | Asserted | Goal | Modus_Ponens | Reflexivity | - Symmetry | Transitivity | Transitivity_Star | Monotonicity | Quant_Intro | - Distributivity | And_Elim | Not_Or_Elim | Rewrite | Rewrite_Star | - Pull_Quant | Pull_Quant_Star | Push_Quant | Elim_Unused_Vars | Dest_Eq_Res | - Quant_Inst | Hypothesis | Lemma | Unit_Resolution | Iff_True | Iff_False | - Commutativity | Def_Axiom | Intro_Def | Apply_Def | Iff_Oeq | Nnf_Pos | - Nnf_Neg | Nnf_Star | Cnf_Star | Skolemize | Modus_Ponens_Oeq | - Th_Lemma of string list - -val rule_names = Symtab.make [ - ("true-axiom", True_Axiom), - ("asserted", Asserted), - ("goal", Goal), - ("mp", Modus_Ponens), - ("refl", Reflexivity), - ("symm", Symmetry), - ("trans", Transitivity), - ("trans*", Transitivity_Star), - ("monotonicity", Monotonicity), - ("quant-intro", Quant_Intro), - ("distributivity", Distributivity), - ("and-elim", And_Elim), - ("not-or-elim", Not_Or_Elim), - ("rewrite", Rewrite), - ("rewrite*", Rewrite_Star), - ("pull-quant", Pull_Quant), - ("pull-quant*", Pull_Quant_Star), - ("push-quant", Push_Quant), - ("elim-unused", Elim_Unused_Vars), - ("der", Dest_Eq_Res), - ("quant-inst", Quant_Inst), - ("hypothesis", Hypothesis), - ("lemma", Lemma), - ("unit-resolution", Unit_Resolution), - ("iff-true", Iff_True), - ("iff-false", Iff_False), - ("commutativity", Commutativity), - ("def-axiom", Def_Axiom), - ("intro-def", Intro_Def), - ("apply-def", Apply_Def), - ("iff~", Iff_Oeq), - ("nnf-pos", Nnf_Pos), - ("nnf-neg", Nnf_Neg), - ("nnf*", Nnf_Star), - ("cnf*", Cnf_Star), - ("sk", Skolemize), - ("mp~", Modus_Ponens_Oeq), - ("th-lemma", Th_Lemma [])] - -fun string_of_rule (Th_Lemma args) = space_implode " " ("th-lemma" :: args) - | string_of_rule r = - let fun eq_rule (s, r') = if r = r' then SOME s else NONE - in the (Symtab.get_first eq_rule rule_names) end - - - -(* certified terms and variables *) - -val (var_prefix, decl_prefix) = ("v", "sk") -(* - "decl_prefix" is for skolem constants (represented by free variables), - "var_prefix" is for pseudo-schematic variables (schematic with respect - to the Z3 proof, but represented by free variables). - - Both prefixes must be distinct to avoid name interferences. - More precisely, the naming of pseudo-schematic variables must be - context-independent modulo the current proof context to be able to - use fast inference kernel rules during proof reconstruction. -*) - -fun mk_inst ctxt vars = - let - val max = fold (Integer.max o fst) vars 0 - val ns = fst (Variable.variant_fixes (replicate (max + 1) var_prefix) ctxt) - fun mk (i, v) = - (dest_Var (Thm.term_of v), Thm.cterm_of ctxt (Free (nth ns i, Thm.typ_of_cterm v))) - in map mk vars end - -fun close ctxt (ct, vars) = - let - val inst = mk_inst ctxt vars - val names = fold (Term.add_free_names o Thm.term_of o snd) inst [] - in (Thm.instantiate_cterm ([], inst) ct, names) end - - -fun mk_bound ctxt (i, T) = - let val ct = Thm.cterm_of ctxt (Var ((Name.uu, 0), T)) - in (ct, [(i, ct)]) end - -local - fun mk_quant1 ctxt q T (ct, vars) = - let - val cv = - (case AList.lookup (op =) vars 0 of - SOME cv => cv - | _ => Thm.cterm_of ctxt (Var ((Name.uu, Thm.maxidx_of_cterm ct + 1), T))) - fun dec (i, v) = if i = 0 then NONE else SOME (i-1, v) - val vars' = map_filter dec vars - in (Thm.apply (Old_SMT_Utils.instT' cv q) (Thm.lambda cv ct), vars') end - - fun quant name = - Old_SMT_Utils.mk_const_pat @{theory} name (Old_SMT_Utils.destT1 o Old_SMT_Utils.destT1) - val forall = quant @{const_name All} - val exists = quant @{const_name Ex} -in - -fun mk_quant is_forall ctxt = - fold_rev (mk_quant1 ctxt (if is_forall then forall else exists)) - -end - -local - fun prep (ct, vars) (maxidx, all_vars) = - let - val maxidx' = maxidx + Thm.maxidx_of_cterm ct + 1 - - fun part (i, cv) = - (case AList.lookup (op =) all_vars i of - SOME cu => apfst (if cu aconvc cv then I else cons (cv, cu)) - | NONE => - let val cv' = Thm.incr_indexes_cterm maxidx cv - in apfst (cons (cv, cv')) #> apsnd (cons (i, cv')) end) - - val (inst, vars') = - if null vars then ([], vars) - else fold part vars ([], []) - - in - (Thm.instantiate_cterm ([], map (apfst (dest_Var o Thm.term_of)) inst) ct, - (maxidx', vars' @ all_vars)) - end -in -fun mk_fun f ts = - let val (cts, (_, vars)) = fold_map prep ts (0, []) - in f cts |> Option.map (rpair vars) end -end - - - -(* proof parser *) - -datatype proof_step = Proof_Step of { - rule: rule, - args: cterm list, - prems: int list, - prop: cterm } - - -(** parser context **) - -val not_false = Thm.cterm_of @{context} (@{const Not} $ @{const False}) - -fun make_context ctxt typs terms = - let - val ctxt' = - ctxt - |> Symtab.fold (Variable.declare_typ o snd) typs - |> Symtab.fold (Variable.declare_term o snd) terms - - fun cert @{const True} = not_false - | cert t = Thm.cterm_of ctxt' t - - in (typs, Symtab.map (K cert) terms, Inttab.empty, [], [], ctxt') end - -fun fresh_name n (typs, terms, exprs, steps, vars, ctxt) = - let val (n', ctxt') = yield_singleton Variable.variant_fixes n ctxt - in (n', (typs, terms, exprs, steps, vars, ctxt')) end - -fun context_of (_, _, _, _, _, ctxt) = ctxt - -fun add_decl (n, T) (cx as (_, terms, _, _, _, _)) = - (case Symtab.lookup terms n of - SOME _ => cx - | NONE => cx |> fresh_name (decl_prefix ^ n) - |> (fn (m, (typs, terms, exprs, steps, vars, ctxt)) => - let - val upd = Symtab.update (n, Thm.cterm_of ctxt (Free (m, T))) - in (typs, upd terms, exprs, steps, vars, ctxt) end)) - -fun mk_typ (typs, _, _, _, _, ctxt) (s as Old_Z3_Interface.Sym (n, _)) = - (case Old_Z3_Interface.mk_builtin_typ ctxt s of - SOME T => SOME T - | NONE => Symtab.lookup typs n) - -fun mk_num (_, _, _, _, _, ctxt) (i, T) = - mk_fun (K (Old_Z3_Interface.mk_builtin_num ctxt i T)) [] - -fun mk_app (_, terms, _, _, _, ctxt) (s as Old_Z3_Interface.Sym (n, _), es) = - mk_fun (fn cts => - (case Old_Z3_Interface.mk_builtin_fun ctxt s cts of - SOME ct => SOME ct - | NONE => - Symtab.lookup terms n |> Option.map (Drule.list_comb o rpair cts))) es - -fun add_expr k t (typs, terms, exprs, steps, vars, ctxt) = - (typs, terms, Inttab.update (k, t) exprs, steps, vars, ctxt) - -fun lookup_expr (_, _, exprs, _, _, _) = Inttab.lookup exprs - -fun add_proof_step k ((r, args), prop) cx = - let - val (typs, terms, exprs, steps, vars, ctxt) = cx - val (ct, vs) = close ctxt prop - fun part (SOME e, _) (cts, ps) = (close ctxt e :: cts, ps) - | part (NONE, i) (cts, ps) = (cts, i :: ps) - val (args', prems) = fold (part o `(lookup_expr cx)) args ([], []) - val (cts, vss) = split_list args' - val step = Proof_Step {rule=r, args=rev cts, prems=rev prems, - prop = Old_SMT_Utils.mk_cprop ct} - val vars' = fold (union (op =)) (vs :: vss) vars - in (typs, terms, exprs, (k, step) :: steps, vars', ctxt) end - -fun finish (_, _, _, steps, vars, ctxt) = - let - fun coll (p as (k, Proof_Step {prems, rule, prop, ...})) (ars, ps, ids) = - (case rule of - Asserted => ((k, prop) :: ars, ps, ids) - | Goal => ((k, prop) :: ars, ps, ids) - | _ => - if Inttab.defined ids k then - (ars, p :: ps, fold (Inttab.update o rpair ()) prems ids) - else (ars, ps, ids)) - - val (ars, steps', _) = fold coll steps ([], [], Inttab.make [(~1, ())]) - in (ars, steps', vars, ctxt) end - - -(** core parser **) - -fun parse_exn line_no msg = raise Old_SMT_Failure.SMT (Old_SMT_Failure.Other_Failure - ("Z3 proof parser (line " ^ string_of_int line_no ^ "): " ^ msg)) - -fun scan_exn msg ((line_no, _), _) = parse_exn line_no msg - -fun with_info f cx = - (case f ((NONE, 1), cx) of - ((SOME _, _), cx') => cx' - | ((_, line_no), _) => parse_exn line_no "bad proof") - -fun parse_line _ _ (st as ((SOME _, _), _)) = st - | parse_line scan line ((_, line_no), cx) = - let val st = ((line_no, cx), raw_explode line) - in - (case Scan.catch (Scan.finite' Symbol.stopper (Scan.option scan)) st of - (SOME r, ((_, cx'), _)) => ((r, line_no+1), cx') - | (NONE, _) => parse_exn line_no ("bad proof line: " ^ quote line)) - end - -fun with_context f x ((line_no, cx), st) = - let val (y, cx') = f x cx - in (y, ((line_no, cx'), st)) end - - -fun lookup_context f x (st as ((_, cx), _)) = (f cx x, st) - - -(** parser combinators and parsers for basic entities **) - -fun $$ s = Scan.lift (Scan.$$ s) -fun this s = Scan.lift (Scan.this_string s) -val is_blank = Symbol.is_ascii_blank -fun blank st = Scan.lift (Scan.many1 is_blank) st -fun sep scan = blank |-- scan -fun seps scan = Scan.repeat (sep scan) -fun seps1 scan = Scan.repeat1 (sep scan) -fun seps_by scan_sep scan = scan ::: Scan.repeat (scan_sep |-- scan) - -val lpar = "(" and rpar = ")" -val lbra = "[" and rbra = "]" -fun par scan = $$ lpar |-- scan --| $$ rpar -fun bra scan = $$ lbra |-- scan --| $$ rbra - -val digit = (fn - "0" => SOME 0 | "1" => SOME 1 | "2" => SOME 2 | "3" => SOME 3 | - "4" => SOME 4 | "5" => SOME 5 | "6" => SOME 6 | "7" => SOME 7 | - "8" => SOME 8 | "9" => SOME 9 | _ => NONE) - -fun digits st = (Scan.lift (Scan.many1 Symbol.is_ascii_digit) >> implode) st - -fun nat_num st = (Scan.lift (Scan.repeat1 (Scan.some digit)) >> (fn ds => - fold (fn d => fn i => i * 10 + d) ds 0)) st - -fun int_num st = (Scan.optional ($$ "-" >> K (fn i => ~i)) I :|-- - (fn sign => nat_num >> sign)) st - -val is_char = Symbol.is_ascii_letter orf Symbol.is_ascii_digit orf - member (op =) (raw_explode "_+*-/%~=<>$&|?!.@^#") - -fun name st = (Scan.lift (Scan.many1 is_char) >> implode) st - -fun sym st = (name -- - Scan.optional (bra (seps_by ($$ ":") sym)) [] >> Old_Z3_Interface.Sym) st - -fun id st = ($$ "#" |-- nat_num) st - - -(** parsers for various parts of Z3 proofs **) - -fun sort st = Scan.first [ - this "array" |-- bra (sort --| $$ ":" -- sort) >> (op -->), - par (this "->" |-- seps1 sort) >> ((op --->) o split_last), - sym :|-- (fn s as Old_Z3_Interface.Sym (n, _) => lookup_context mk_typ s :|-- (fn - SOME T => Scan.succeed T - | NONE => scan_exn ("unknown sort: " ^ quote n)))] st - -fun bound st = (par (this ":var" |-- sep nat_num -- sep sort) :|-- - lookup_context (mk_bound o context_of)) st - -fun numb (n as (i, _)) = lookup_context mk_num n :|-- (fn - SOME n' => Scan.succeed n' - | NONE => scan_exn ("unknown number: " ^ quote (string_of_int i))) - -fun appl (app as (Old_Z3_Interface.Sym (n, _), _)) = - lookup_context mk_app app :|-- (fn - SOME app' => Scan.succeed app' - | NONE => scan_exn ("unknown function symbol: " ^ quote n)) - -fun bv_size st = (digits >> (fn sz => - Old_Z3_Interface.Sym ("bv", [Old_Z3_Interface.Sym (sz, [])]))) st - -fun bv_number_sort st = (bv_size :|-- lookup_context mk_typ :|-- (fn - SOME cT => Scan.succeed cT - | NONE => scan_exn ("unknown sort: " ^ quote "bv"))) st - -fun bv_number st = - (this "bv" |-- bra (nat_num --| $$ ":" -- bv_number_sort) :|-- numb) st - -fun frac_number st = ( - int_num --| $$ "/" -- int_num --| this "::" -- sort :|-- (fn ((i, j), T) => - numb (i, T) -- numb (j, T) :|-- (fn (n, m) => - appl (Old_Z3_Interface.Sym ("/", []), [n, m])))) st - -fun plain_number st = (int_num --| this "::" -- sort :|-- numb) st - -fun number st = Scan.first [bv_number, frac_number, plain_number] st - -fun constant st = ((sym >> rpair []) :|-- appl) st - -fun expr_id st = (id :|-- (fn i => lookup_context lookup_expr i :|-- (fn - SOME e => Scan.succeed e - | NONE => scan_exn ("unknown term id: " ^ quote (string_of_int i))))) st - -fun arg st = Scan.first [expr_id, number, constant] st - -fun application st = par ((sym -- Scan.repeat1 (sep arg)) :|-- appl) st - -fun variables st = par (this "vars" |-- seps1 (par (name |-- sep sort))) st - -fun pats st = seps (par ((this ":pat" || this ":nopat") |-- seps1 id)) st - -val ctrue = Thm.cterm_of @{context} @{const True} - -fun pattern st = par (this "pattern" |-- Scan.repeat1 (sep arg) >> - (the o mk_fun (K (SOME ctrue)))) st - -fun quant_kind st = st |> ( - this "forall" >> K (mk_quant true o context_of) || - this "exists" >> K (mk_quant false o context_of)) - -fun quantifier st = - (par (quant_kind -- sep variables --| pats -- sep arg) :|-- - lookup_context (fn cx => fn ((mk_q, Ts), body) => mk_q cx Ts body)) st - -fun expr k = - Scan.first [bound, quantifier, pattern, application, number, constant] :|-- - with_context (pair NONE oo add_expr k) - -val rule_arg = id - (* if this is modified, then 'th_lemma_arg' needs reviewing *) - -fun th_lemma_arg st = Scan.unless (sep rule_arg >> K "" || $$ rbra) (sep name) st - -fun rule_name st = ((name >> `(Symtab.lookup rule_names)) :|-- (fn - (SOME (Th_Lemma _), _) => Scan.repeat th_lemma_arg >> Th_Lemma - | (SOME r, _) => Scan.succeed r - | (NONE, n) => scan_exn ("unknown proof rule: " ^ quote n))) st - -fun rule f k = - bra (rule_name -- seps id) --| $$ ":" -- sep arg #-> - with_context (pair (f k) oo add_proof_step k) - -fun decl st = (this "decl" |-- sep name --| sep (this "::") -- sep sort :|-- - with_context (pair NONE oo add_decl)) st - -fun def st = (id --| sep (this ":=")) st - -fun node st = st |> ( - decl || - def :|-- (fn k => sep (expr k) || sep (rule (K NONE) k)) || - rule SOME ~1) - - -(** overall parser **) - -(* - Currently, terms are parsed bottom-up (i.e., along with parsing the proof - text line by line), but proofs are reconstructed top-down (i.e. by an - in-order top-down traversal of the proof tree/graph). The latter approach - was taken because some proof texts comprise irrelevant proof steps which - will thus not be reconstructed. This approach might also be beneficial - for constructing terms, but it would also increase the complexity of the - (otherwise rather modular) code. -*) - -fun parse ctxt typs terms proof_text = - make_context ctxt typs terms - |> with_info (fold (parse_line node) proof_text) - |> finish - -end diff -r d10f0bbc7ea1 -r f595b7532dc9 src/HOL/Library/Old_SMT/old_z3_proof_reconstruction.ML --- a/src/HOL/Library/Old_SMT/old_z3_proof_reconstruction.ML Thu Apr 20 10:45:52 2017 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,893 +0,0 @@ -(* Title: HOL/Library/Old_SMT/old_z3_proof_reconstruction.ML - Author: Sascha Boehme, TU Muenchen - -Proof reconstruction for proofs found by Z3. -*) - -signature OLD_Z3_PROOF_RECONSTRUCTION = -sig - val add_z3_rule: thm -> Context.generic -> Context.generic - val reconstruct: Proof.context -> Old_SMT_Translate.recon -> string list -> int list * thm -end - -structure Old_Z3_Proof_Reconstruction: OLD_Z3_PROOF_RECONSTRUCTION = -struct - - -fun z3_exn msg = raise Old_SMT_Failure.SMT (Old_SMT_Failure.Other_Failure - ("Z3 proof reconstruction: " ^ msg)) - - - -(* net of schematic rules *) - -local - val description = "declaration of Z3 proof rules" - - val eq = Thm.eq_thm - - structure Old_Z3_Rules = Generic_Data - ( - type T = thm Net.net - val empty = Net.empty - val extend = I - val merge = Net.merge eq - ) - - fun prep context = - `Thm.prop_of o rewrite_rule (Context.proof_of context) [Old_Z3_Proof_Literals.rewrite_true] - - fun ins thm context = - context |> Old_Z3_Rules.map (fn net => Net.insert_term eq (prep context thm) net handle Net.INSERT => net) - fun rem thm context = - context |> Old_Z3_Rules.map (fn net => Net.delete_term eq (prep context thm) net handle Net.DELETE => net) - - val add = Thm.declaration_attribute ins - val del = Thm.declaration_attribute rem -in - -val add_z3_rule = ins - -fun by_schematic_rule ctxt ct = - the (Old_Z3_Proof_Tools.net_instance (Old_Z3_Rules.get (Context.Proof ctxt)) ct) - -val _ = Theory.setup - (Attrib.setup @{binding old_z3_rule} (Attrib.add_del add del) description #> - Global_Theory.add_thms_dynamic (@{binding old_z3_rule}, Net.content o Old_Z3_Rules.get)) - -end - - - -(* proof tools *) - -fun named ctxt name prover ct = - let val _ = Old_SMT_Config.trace_msg ctxt I ("Z3: trying " ^ name ^ " ...") - in prover ct end - -fun NAMED ctxt name tac i st = - let val _ = Old_SMT_Config.trace_msg ctxt I ("Z3: trying " ^ name ^ " ...") - in tac i st end - -fun pretty_goal ctxt thms t = - [Pretty.block [Pretty.str "proposition: ", Syntax.pretty_term ctxt t]] - |> not (null thms) ? cons (Pretty.big_list "assumptions:" - (map (Thm.pretty_thm ctxt) thms)) - -fun try_apply ctxt thms = - let - fun try_apply_err ct = Pretty.string_of (Pretty.chunks [ - Pretty.big_list ("Z3 found a proof," ^ - " but proof reconstruction failed at the following subgoal:") - (pretty_goal ctxt thms (Thm.term_of ct)), - Pretty.str ("Declaring a rule as [old_z3_rule] might solve this problem.")]) - - fun apply [] ct = error (try_apply_err ct) - | apply (prover :: provers) ct = - (case try prover ct of - SOME thm => (Old_SMT_Config.trace_msg ctxt I "Z3: succeeded"; thm) - | NONE => apply provers ct) - - fun schematic_label full = "schematic rules" |> full ? suffix " (full)" - fun schematic ctxt full ct = - ct - |> full ? fold_rev (curry Drule.mk_implies o Thm.cprop_of) thms - |> named ctxt (schematic_label full) (by_schematic_rule ctxt) - |> fold Thm.elim_implies thms - - in apply o cons (schematic ctxt false) o cons (schematic ctxt true) end - -local - val rewr_if = - @{lemma "(if P then Q1 else Q2) = ((P --> Q1) & (~P --> Q2))" by simp} -in - -fun HOL_fast_tac ctxt = - Classical.fast_tac (put_claset HOL_cs ctxt) - -fun simp_fast_tac ctxt = - Simplifier.simp_tac (put_simpset HOL_ss ctxt addsimps [rewr_if]) - THEN_ALL_NEW HOL_fast_tac ctxt - -end - - - -(* theorems and proofs *) - -(** theorem incarnations **) - -datatype theorem = - Thm of thm | (* theorem without special features *) - MetaEq of thm | (* meta equality "t == s" *) - Literals of thm * Old_Z3_Proof_Literals.littab - (* "P1 & ... & Pn" and table of all literals P1, ..., Pn *) - -fun thm_of (Thm thm) = thm - | thm_of (MetaEq thm) = thm COMP @{thm meta_eq_to_obj_eq} - | thm_of (Literals (thm, _)) = thm - -fun meta_eq_of (MetaEq thm) = thm - | meta_eq_of p = mk_meta_eq (thm_of p) - -fun literals_of (Literals (_, lits)) = lits - | literals_of p = Old_Z3_Proof_Literals.make_littab [thm_of p] - - - -(** core proof rules **) - -(* assumption *) - -local - val remove_trigger = mk_meta_eq @{thm trigger_def} - val remove_weight = mk_meta_eq @{thm weight_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 prep_rules = [@{thm Let_def}, remove_trigger, remove_weight, - remove_fun_app, Old_Z3_Proof_Literals.rewrite_true] - - fun rewrite _ [] = I - | rewrite ctxt eqs = Conv.fconv_rule (rewrite_conv ctxt eqs) - - fun lookup_assm assms_net ct = - Old_Z3_Proof_Tools.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 asserted ctxt = - let - val eqs = map (rewrite ctxt [Old_Z3_Proof_Literals.rewrite_true]) 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)) - |> Old_Z3_Proof_Tools.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.implies_elim thm thm', ctxt') end - - fun add1 idx thm1 ((i, th), exact) ((is, 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 - ((insert (op =) i is, thms'), - (ctxt', Inttab.update (idx, Thm thm) ptab)) - end - - fun add (idx, ct) (cx as ((is, thms), (ctxt, ptab))) = - let - 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 ((is, thms), (ctxt', Inttab.update (idx, Thm thm) ptab)) end - | ithms => fold (add1 idx thm1) ithms cx) - end - in fold add asserted (([], []), (ctxt, Inttab.empty)) end - -end - - -(* P = Q ==> P ==> Q or P --> Q ==> P ==> Q *) -local - val precomp = Old_Z3_Proof_Tools.precompose2 - val comp = Old_Z3_Proof_Tools.compose - - val meta_iffD1 = @{lemma "P == Q ==> P ==> (Q::bool)" by simp} - val meta_iffD1_c = precomp Thm.dest_binop meta_iffD1 - - val iffD1_c = precomp (Thm.dest_binop o Thm.dest_arg) @{thm iffD1} - val mp_c = precomp (Thm.dest_binop o Thm.dest_arg) @{thm mp} -in -fun mp (MetaEq thm) p = Thm (Thm.implies_elim (comp meta_iffD1_c thm) p) - | mp p_q p = - let - val pq = thm_of p_q - val thm = comp iffD1_c pq handle THM _ => comp mp_c pq - in Thm (Thm.implies_elim thm p) end -end - - -(* and_elim: P1 & ... & Pn ==> Pi *) -(* not_or_elim: ~(P1 | ... | Pn) ==> ~Pi *) -local - fun is_sublit conj t = Old_Z3_Proof_Literals.exists_lit conj (fn u => u aconv t) - - fun derive conj t lits idx ptab = - let - val lit = the (Old_Z3_Proof_Literals.get_first_lit (is_sublit conj t) lits) - val ls = Old_Z3_Proof_Literals.explode conj false false [t] lit - val lits' = fold Old_Z3_Proof_Literals.insert_lit ls - (Old_Z3_Proof_Literals.delete_lit lit lits) - - fun upd thm = Literals (thm_of thm, lits') - val ptab' = Inttab.map_entry idx upd ptab - in (the (Old_Z3_Proof_Literals.lookup_lit lits' t), ptab') end - - fun lit_elim conj (p, idx) ct ptab = - let val lits = literals_of p - in - (case Old_Z3_Proof_Literals.lookup_lit lits (Old_SMT_Utils.term_of ct) of - SOME lit => (Thm lit, ptab) - | NONE => apfst Thm (derive conj (Old_SMT_Utils.term_of ct) lits idx ptab)) - end -in -val and_elim = lit_elim true -val not_or_elim = lit_elim false -end - - -(* P1, ..., Pn |- False ==> |- ~P1 | ... | ~Pn *) -local - fun step lit thm = - Thm.implies_elim (Thm.implies_intr (Thm.cprop_of lit) thm) lit - val explode_disj = Old_Z3_Proof_Literals.explode false false false - fun intro hyps thm th = fold step (explode_disj hyps th) thm - - fun dest_ccontr ct = [Thm.dest_arg (Thm.dest_arg (Thm.dest_arg1 ct))] - val ccontr = Old_Z3_Proof_Tools.precompose dest_ccontr @{thm ccontr} -in -fun lemma thm ct = - let - val cu = Old_Z3_Proof_Literals.negate (Thm.dest_arg ct) - val hyps = map_filter (try HOLogic.dest_Trueprop) (Thm.hyps_of thm) - val th = Old_Z3_Proof_Tools.under_assumption (intro hyps thm) cu - in Thm (Old_Z3_Proof_Tools.compose ccontr th) end -end - - -(* \/{P1, ..., Pn, Q1, ..., Qn}, ~P1, ..., ~Pn ==> \/{Q1, ..., Qn} *) -local - val explode_disj = Old_Z3_Proof_Literals.explode false true false - val join_disj = Old_Z3_Proof_Literals.join false - fun unit thm thms th = - let - val t = @{const Not} $ Old_SMT_Utils.prop_of thm - val ts = map Old_SMT_Utils.prop_of thms - in - join_disj (Old_Z3_Proof_Literals.make_littab (thms @ explode_disj ts th)) t - end - - fun dest_arg2 ct = Thm.dest_arg (Thm.dest_arg ct) - fun dest ct = apply2 dest_arg2 (Thm.dest_binop ct) - val contrapos = - Old_Z3_Proof_Tools.precompose2 dest @{lemma "(~P ==> ~Q) ==> Q ==> P" by fast} -in -fun unit_resolution thm thms ct = - Old_Z3_Proof_Literals.negate (Thm.dest_arg ct) - |> Old_Z3_Proof_Tools.under_assumption (unit thm thms) - |> Thm o Old_Z3_Proof_Tools.discharge thm o Old_Z3_Proof_Tools.compose contrapos -end - - -(* P ==> P == True or P ==> P == False *) -local - val iff1 = @{lemma "P ==> P == (~ False)" by simp} - val iff2 = @{lemma "~P ==> P == False" by simp} -in -fun iff_true thm = MetaEq (thm COMP iff1) -fun iff_false thm = MetaEq (thm COMP iff2) -end - - -(* distributivity of | over & *) -fun distributivity ctxt = Thm o try_apply ctxt [] [ - named ctxt "fast" (Old_Z3_Proof_Tools.by_tac ctxt (HOL_fast_tac ctxt))] - (* FIXME: not very well tested *) - - -(* Tseitin-like axioms *) -local - val disjI1 = @{lemma "(P ==> Q) ==> ~P | Q" by fast} - val disjI2 = @{lemma "(~P ==> Q) ==> P | Q" by fast} - val disjI3 = @{lemma "(~Q ==> P) ==> P | Q" by fast} - val disjI4 = @{lemma "(Q ==> P) ==> P | ~Q" by fast} - - fun prove' conj1 conj2 ct2 thm = - let - val littab = - Old_Z3_Proof_Literals.explode conj1 true (conj1 <> conj2) [] thm - |> cons Old_Z3_Proof_Literals.true_thm - |> Old_Z3_Proof_Literals.make_littab - in Old_Z3_Proof_Literals.join conj2 littab (Thm.term_of ct2) end - - fun prove rule (ct1, conj1) (ct2, conj2) = - Old_Z3_Proof_Tools.under_assumption (prove' conj1 conj2 ct2) ct1 COMP rule - - fun prove_def_axiom ct = - let val (ct1, ct2) = Thm.dest_binop (Thm.dest_arg ct) - in - (case Thm.term_of ct1 of - @{const Not} $ (@{const HOL.conj} $ _ $ _) => - prove disjI1 (Thm.dest_arg ct1, true) (ct2, true) - | @{const HOL.conj} $ _ $ _ => - prove disjI3 (Old_Z3_Proof_Literals.negate ct2, false) (ct1, true) - | @{const Not} $ (@{const HOL.disj} $ _ $ _) => - prove disjI3 (Old_Z3_Proof_Literals.negate ct2, false) (ct1, false) - | @{const HOL.disj} $ _ $ _ => - prove disjI2 (Old_Z3_Proof_Literals.negate ct1, false) (ct2, true) - | Const (@{const_name distinct}, _) $ _ => - let - fun dis_conv cv = Conv.arg_conv (Conv.arg1_conv cv) - val unfold_dis_conv = dis_conv Old_Z3_Proof_Tools.unfold_distinct_conv - fun prv cu = - let val (cu1, cu2) = Thm.dest_binop (Thm.dest_arg cu) - in prove disjI4 (Thm.dest_arg cu2, true) (cu1, true) end - in Old_Z3_Proof_Tools.with_conv unfold_dis_conv prv ct end - | @{const Not} $ (Const (@{const_name distinct}, _) $ _) => - let - fun dis_conv cv = Conv.arg_conv (Conv.arg1_conv (Conv.arg_conv cv)) - val unfold_dis_conv = dis_conv Old_Z3_Proof_Tools.unfold_distinct_conv - fun prv cu = - let val (cu1, cu2) = Thm.dest_binop (Thm.dest_arg cu) - in prove disjI1 (Thm.dest_arg cu1, true) (cu2, true) end - in Old_Z3_Proof_Tools.with_conv unfold_dis_conv prv ct end - | _ => raise CTERM ("prove_def_axiom", [ct])) - end -in -fun def_axiom ctxt = Thm o try_apply ctxt [] [ - named ctxt "conj/disj/distinct" prove_def_axiom, - Old_Z3_Proof_Tools.by_abstraction 0 (true, false) ctxt [] (fn ctxt' => - named ctxt' "simp+fast" (Old_Z3_Proof_Tools.by_tac ctxt (simp_fast_tac ctxt')))] -end - - -(* local definitions *) -local - val intro_rules = [ - @{lemma "n == P ==> (~n | P) & (n | ~P)" by simp}, - @{lemma "n == (if P then s else t) ==> (~P | n = s) & (P | n = t)" - by simp}, - @{lemma "n == P ==> n = P" by (rule meta_eq_to_obj_eq)} ] - - val apply_rules = [ - @{lemma "(~n | P) & (n | ~P) ==> P == n" by (atomize(full)) fast}, - @{lemma "(~P | n = s) & (P | n = t) ==> (if P then s else t) == n" - by (atomize(full)) fastforce} ] - - val inst_rule = Old_Z3_Proof_Tools.match_instantiate Thm.dest_arg - - fun apply_rule ct = - (case get_first (try (inst_rule ct)) intro_rules of - SOME thm => thm - | NONE => raise CTERM ("intro_def", [ct])) -in -fun intro_def ct = Old_Z3_Proof_Tools.make_hyp_def (apply_rule ct) #>> Thm - -fun apply_def thm = - get_first (try (fn rule => MetaEq (thm COMP rule))) apply_rules - |> the_default (Thm thm) -end - - -(* negation normal form *) -local - val quant_rules1 = ([ - @{lemma "(!!x. P x == Q) ==> ALL x. P x == Q" by simp}, - @{lemma "(!!x. P x == Q) ==> EX x. P x == Q" by simp}], [ - @{lemma "(!!x. P x == Q x) ==> ALL x. P x == ALL x. Q x" by simp}, - @{lemma "(!!x. P x == Q x) ==> EX x. P x == EX x. Q x" by simp}]) - - val quant_rules2 = ([ - @{lemma "(!!x. ~P x == Q) ==> ~(ALL x. P x) == Q" by simp}, - @{lemma "(!!x. ~P x == Q) ==> ~(EX x. P x) == Q" by simp}], [ - @{lemma "(!!x. ~P x == Q x) ==> ~(ALL x. P x) == EX x. Q x" by simp}, - @{lemma "(!!x. ~P x == Q x) ==> ~(EX x. P x) == ALL x. Q x" by simp}]) - - fun nnf_quant_tac ctxt thm (qs as (qs1, qs2)) i st = ( - resolve_tac ctxt [thm] ORELSE' - (match_tac ctxt qs1 THEN' nnf_quant_tac ctxt thm qs) ORELSE' - (match_tac ctxt qs2 THEN' nnf_quant_tac ctxt thm qs)) i st - - fun nnf_quant_tac_varified ctxt vars eq = - nnf_quant_tac ctxt (Old_Z3_Proof_Tools.varify vars eq) - - fun nnf_quant ctxt vars qs p ct = - Old_Z3_Proof_Tools.as_meta_eq ct - |> Old_Z3_Proof_Tools.by_tac ctxt (nnf_quant_tac_varified ctxt vars (meta_eq_of p) qs) - - fun prove_nnf ctxt = try_apply ctxt [] [ - named ctxt "conj/disj" Old_Z3_Proof_Literals.prove_conj_disj_eq, - Old_Z3_Proof_Tools.by_abstraction 0 (true, false) ctxt [] (fn ctxt' => - named ctxt' "simp+fast" (Old_Z3_Proof_Tools.by_tac ctxt' (simp_fast_tac ctxt')))] -in -fun nnf ctxt vars ps ct = - (case Old_SMT_Utils.term_of ct of - _ $ (l as Const _ $ Abs _) $ (r as Const _ $ Abs _) => - if l aconv r - then MetaEq (Thm.reflexive (Thm.dest_arg (Thm.dest_arg ct))) - else MetaEq (nnf_quant ctxt vars quant_rules1 (hd ps) ct) - | _ $ (@{const Not} $ (Const _ $ Abs _)) $ (Const _ $ Abs _) => - MetaEq (nnf_quant ctxt vars quant_rules2 (hd ps) ct) - | _ => - let - val nnf_rewr_conv = Conv.arg_conv (Conv.arg_conv - (Old_Z3_Proof_Tools.unfold_eqs ctxt - (map (Thm.symmetric o meta_eq_of) ps))) - in Thm (Old_Z3_Proof_Tools.with_conv nnf_rewr_conv (prove_nnf ctxt) ct) end) -end - - - -(** equality proof rules **) - -(* |- t = t *) -fun refl ct = MetaEq (Thm.reflexive (Thm.dest_arg (Thm.dest_arg ct))) - - -(* s = t ==> t = s *) -local - val symm_rule = @{lemma "s = t ==> t == s" by simp} -in -fun symm (MetaEq thm) = MetaEq (Thm.symmetric thm) - | symm p = MetaEq (thm_of p COMP symm_rule) -end - - -(* s = t ==> t = u ==> s = u *) -local - val trans1 = @{lemma "s == t ==> t = u ==> s == u" by simp} - val trans2 = @{lemma "s = t ==> t == u ==> s == u" by simp} - val trans3 = @{lemma "s = t ==> t = u ==> s == u" by simp} -in -fun trans (MetaEq thm1) (MetaEq thm2) = MetaEq (Thm.transitive thm1 thm2) - | trans (MetaEq thm) q = MetaEq (thm_of q COMP (thm COMP trans1)) - | trans p (MetaEq thm) = MetaEq (thm COMP (thm_of p COMP trans2)) - | trans p q = MetaEq (thm_of q COMP (thm_of p COMP trans3)) -end - - -(* t1 = s1 ==> ... ==> tn = sn ==> f t1 ... tn = f s1 .. sn - (reflexive antecendents are droppped) *) -local - exception MONO - - fun prove_refl (ct, _) = Thm.reflexive ct - fun prove_comb f g cp = - let val ((ct1, ct2), (cu1, cu2)) = apply2 Thm.dest_comb cp - in Thm.combination (f (ct1, cu1)) (g (ct2, cu2)) end - fun prove_arg f = prove_comb prove_refl f - - fun prove f cp = prove_comb (prove f) f cp handle CTERM _ => prove_refl cp - - fun prove_nary is_comb f = - let - fun prove (cp as (ct, _)) = f cp handle MONO => - if is_comb (Thm.term_of ct) - then prove_comb (prove_arg prove) prove cp - else prove_refl cp - in prove end - - fun prove_list f n cp = - if n = 0 then prove_refl cp - else prove_comb (prove_arg f) (prove_list f (n-1)) cp - - fun with_length f (cp as (cl, _)) = - f (length (HOLogic.dest_list (Thm.term_of cl))) cp - - fun prove_distinct f = prove_arg (with_length (prove_list f)) - - fun prove_eq exn lookup cp = - (case lookup (Logic.mk_equals (apply2 Thm.term_of cp)) of - SOME eq => eq - | NONE => if exn then raise MONO else prove_refl cp) - - val prove_exn = prove_eq true - and prove_safe = prove_eq false - - fun mono f (cp as (cl, _)) = - (case Term.head_of (Thm.term_of cl) of - @{const HOL.conj} => prove_nary Old_Z3_Proof_Literals.is_conj (prove_exn f) - | @{const HOL.disj} => prove_nary Old_Z3_Proof_Literals.is_disj (prove_exn f) - | Const (@{const_name distinct}, _) => prove_distinct (prove_safe f) - | _ => prove (prove_safe f)) cp -in -fun monotonicity eqs ct = - let - fun and_symmetric (t, thm) = [(t, thm), (t, Thm.symmetric thm)] - val teqs = maps (and_symmetric o `Thm.prop_of o meta_eq_of) eqs - val lookup = AList.lookup (op aconv) teqs - val cp = Thm.dest_binop (Thm.dest_arg ct) - in MetaEq (prove_exn lookup cp handle MONO => mono lookup cp) end -end - - -(* |- f a b = f b a (where f is equality) *) -local - val rule = @{lemma "a = b == b = a" by (atomize(full)) (rule eq_commute)} -in -fun commutativity ct = - MetaEq (Old_Z3_Proof_Tools.match_instantiate I - (Old_Z3_Proof_Tools.as_meta_eq ct) rule) -end - - - -(** quantifier proof rules **) - -(* P ?x = Q ?x ==> (ALL x. P x) = (ALL x. Q x) - P ?x = Q ?x ==> (EX x. P x) = (EX x. Q x) *) -local - val rules = [ - @{lemma "(!!x. P x == Q x) ==> (ALL x. P x) == (ALL x. Q x)" by simp}, - @{lemma "(!!x. P x == Q x) ==> (EX x. P x) == (EX x. Q x)" by simp}] -in -fun quant_intro ctxt vars p ct = - let - val thm = meta_eq_of p - val rules' = Old_Z3_Proof_Tools.varify vars thm :: rules - val cu = Old_Z3_Proof_Tools.as_meta_eq ct - val tac = REPEAT_ALL_NEW (match_tac ctxt rules') - in MetaEq (Old_Z3_Proof_Tools.by_tac ctxt tac cu) end -end - - -(* |- ((ALL x. P x) | Q) = (ALL x. P x | Q) *) -fun pull_quant ctxt = Thm o try_apply ctxt [] [ - named ctxt "fast" (Old_Z3_Proof_Tools.by_tac ctxt (HOL_fast_tac ctxt))] - (* FIXME: not very well tested *) - - -(* |- (ALL x. P x & Q x) = ((ALL x. P x) & (ALL x. Q x)) *) -fun push_quant ctxt = Thm o try_apply ctxt [] [ - named ctxt "fast" (Old_Z3_Proof_Tools.by_tac ctxt (HOL_fast_tac ctxt))] - (* FIXME: not very well tested *) - - -(* |- (ALL x1 ... xn y1 ... yn. P x1 ... xn) = (ALL x1 ... xn. P x1 ... xn) *) -local - val elim_all = @{lemma "P = Q ==> (ALL x. P) = Q" by fast} - val elim_ex = @{lemma "P = Q ==> (EX x. P) = Q" by fast} - - fun elim_unused_tac ctxt i st = ( - match_tac ctxt [@{thm refl}] - ORELSE' (match_tac ctxt [elim_all, elim_ex] THEN' elim_unused_tac ctxt) - ORELSE' ( - match_tac ctxt [@{thm iff_allI}, @{thm iff_exI}] - THEN' elim_unused_tac ctxt)) i st -in - -fun elim_unused_vars ctxt = Thm o Old_Z3_Proof_Tools.by_tac ctxt (elim_unused_tac ctxt) - -end - - -(* |- (ALL x1 ... xn. ~(x1 = t1 & ... xn = tn) | P x1 ... xn) = P t1 ... tn *) -fun dest_eq_res ctxt = Thm o try_apply ctxt [] [ - named ctxt "fast" (Old_Z3_Proof_Tools.by_tac ctxt (HOL_fast_tac ctxt))] - (* FIXME: not very well tested *) - - -(* |- ~(ALL x1...xn. P x1...xn) | P a1...an *) -local - val rule = @{lemma "~ P x | Q ==> ~(ALL x. P x) | Q" by fast} -in -fun quant_inst ctxt = Thm o Old_Z3_Proof_Tools.by_tac ctxt ( - REPEAT_ALL_NEW (match_tac ctxt [rule]) - THEN' resolve_tac ctxt @{thms excluded_middle}) -end - - -(* |- (EX x. P x) = P c |- ~(ALL x. P x) = ~ P c *) -local - val forall = - Old_SMT_Utils.mk_const_pat @{theory} @{const_name Pure.all} - (Old_SMT_Utils.destT1 o Old_SMT_Utils.destT1) - fun mk_forall cv ct = - Thm.apply (Old_SMT_Utils.instT' cv forall) (Thm.lambda cv ct) - - fun get_vars f mk pred ctxt t = - Term.fold_aterms f t [] - |> map_filter (fn v => - if pred v then SOME (Thm.cterm_of ctxt (mk v)) else NONE) - - fun close vars f ct ctxt = - let - val frees_of = get_vars Term.add_frees Free (member (op =) vars o fst) - val vs = frees_of ctxt (Thm.term_of ct) - val (thm, ctxt') = f (fold_rev mk_forall vs ct) ctxt - val vars_of = get_vars Term.add_vars Var (K true) ctxt' - in - (Thm.instantiate ([], map (dest_Var o Thm.term_of) (vars_of (Thm.prop_of thm)) ~~ vs) thm, - ctxt') - end - - val sk_rules = @{lemma - "c = (SOME x. P x) ==> (EX x. P x) = P c" - "c = (SOME x. ~P x) ==> (~(ALL x. P x)) = (~P c)" - by (metis someI_ex)+} -in - -fun skolemize vars = - apfst Thm oo close vars (yield_singleton Assumption.add_assumes) - -fun discharge_sk_tac ctxt i st = ( - resolve_tac ctxt @{thms trans} i - THEN resolve_tac ctxt sk_rules i - THEN (resolve_tac ctxt @{thms refl} ORELSE' discharge_sk_tac ctxt) (i+1) - THEN resolve_tac ctxt @{thms refl} i) st - -end - - - -(** theory proof rules **) - -(* theory lemmas: linear arithmetic, arrays *) -fun th_lemma ctxt simpset thms = Thm o try_apply ctxt thms [ - Old_Z3_Proof_Tools.by_abstraction 0 (false, true) ctxt thms (fn ctxt' => - Old_Z3_Proof_Tools.by_tac ctxt' ( - NAMED ctxt' "arith" (Arith_Data.arith_tac ctxt') - ORELSE' NAMED ctxt' "simp+arith" ( - Simplifier.asm_full_simp_tac (put_simpset simpset ctxt') - THEN_ALL_NEW Arith_Data.arith_tac ctxt')))] - - -(* rewriting: prove equalities: - * ACI of conjunction/disjunction - * contradiction, excluded middle - * logical rewriting rules (for negation, implication, equivalence, - distinct) - * normal forms for polynoms (integer/real arithmetic) - * quantifier elimination over linear arithmetic - * ... ? **) -local - fun spec_meta_eq_of thm = - (case try (fn th => th RS @{thm spec}) thm of - SOME thm' => spec_meta_eq_of thm' - | NONE => mk_meta_eq thm) - - fun prep (Thm thm) = spec_meta_eq_of thm - | prep (MetaEq thm) = thm - | prep (Literals (thm, _)) = spec_meta_eq_of thm - - fun unfold_conv ctxt ths = - Conv.arg_conv (Conv.binop_conv (Old_Z3_Proof_Tools.unfold_eqs ctxt - (map prep ths))) - - fun with_conv _ [] prv = prv - | with_conv ctxt ths prv = - Old_Z3_Proof_Tools.with_conv (unfold_conv ctxt ths) prv - - val unfold_conv = - Conv.arg_conv (Conv.binop_conv - (Conv.try_conv Old_Z3_Proof_Tools.unfold_distinct_conv)) - val prove_conj_disj_eq = - Old_Z3_Proof_Tools.with_conv unfold_conv Old_Z3_Proof_Literals.prove_conj_disj_eq - - fun declare_hyps ctxt thm = - (thm, snd (Assumption.add_assumes (Thm.chyps_of thm) ctxt)) -in - -val abstraction_depth = 3 - (* - This value was chosen large enough to potentially catch exceptions, - yet small enough to not cause too much harm. The value might be - increased in the future, if reconstructing 'rewrite' fails on problems - that get too much abstracted to be reconstructable. - *) - -fun rewrite simpset ths ct ctxt = - apfst Thm (declare_hyps ctxt (with_conv ctxt ths (try_apply ctxt [] [ - named ctxt "conj/disj/distinct" prove_conj_disj_eq, - named ctxt "pull-ite" Old_Z3_Proof_Methods.prove_ite ctxt, - Old_Z3_Proof_Tools.by_abstraction 0 (true, false) ctxt [] (fn ctxt' => - Old_Z3_Proof_Tools.by_tac ctxt' ( - NAMED ctxt' "simp (logic)" (Simplifier.simp_tac (put_simpset simpset ctxt')) - THEN_ALL_NEW NAMED ctxt' "fast (logic)" (fast_tac ctxt'))), - Old_Z3_Proof_Tools.by_abstraction 0 (false, true) ctxt [] (fn ctxt' => - Old_Z3_Proof_Tools.by_tac ctxt' ( - (resolve_tac ctxt' @{thms iff_allI} ORELSE' K all_tac) - THEN' NAMED ctxt' "simp (theory)" (Simplifier.simp_tac (put_simpset simpset ctxt')) - THEN_ALL_NEW ( - NAMED ctxt' "fast (theory)" (HOL_fast_tac ctxt') - ORELSE' NAMED ctxt' "arith (theory)" (Arith_Data.arith_tac ctxt')))), - Old_Z3_Proof_Tools.by_abstraction 0 (true, true) ctxt [] (fn ctxt' => - Old_Z3_Proof_Tools.by_tac ctxt' ( - (resolve_tac ctxt' @{thms iff_allI} ORELSE' K all_tac) - THEN' NAMED ctxt' "simp (full)" (Simplifier.simp_tac (put_simpset simpset ctxt')) - THEN_ALL_NEW ( - NAMED ctxt' "fast (full)" (HOL_fast_tac ctxt') - ORELSE' NAMED ctxt' "arith (full)" (Arith_Data.arith_tac ctxt')))), - named ctxt "injectivity" (Old_Z3_Proof_Methods.prove_injectivity ctxt), - Old_Z3_Proof_Tools.by_abstraction abstraction_depth (true, true) ctxt [] - (fn ctxt' => - Old_Z3_Proof_Tools.by_tac ctxt' ( - (resolve_tac ctxt' @{thms iff_allI} ORELSE' K all_tac) - THEN' NAMED ctxt' "simp (deepen)" (Simplifier.simp_tac (put_simpset simpset ctxt')) - THEN_ALL_NEW ( - NAMED ctxt' "fast (deepen)" (HOL_fast_tac ctxt') - ORELSE' NAMED ctxt' "arith (deepen)" (Arith_Data.arith_tac - ctxt'))))]) ct)) - -end - - - -(* proof reconstruction *) - -(** tracing and checking **) - -fun trace_before ctxt idx = Old_SMT_Config.trace_msg ctxt (fn r => - "Z3: #" ^ string_of_int idx ^ ": " ^ Old_Z3_Proof_Parser.string_of_rule r) - -fun check_after idx r ps ct (p, (ctxt, _)) = - if not (Config.get ctxt Old_SMT_Config.trace) then () - else - let - val thm = thm_of p - val _ = Thm.consolidate thm - in - if (Thm.cprop_of thm) aconvc ct then () - else - z3_exn (Pretty.string_of (Pretty.big_list - ("proof step failed: " ^ quote (Old_Z3_Proof_Parser.string_of_rule r) ^ - " (#" ^ string_of_int idx ^ ")") - (pretty_goal ctxt (map (thm_of o fst) ps) (Thm.prop_of thm) @ - [Pretty.block [Pretty.str "expected: ", - Syntax.pretty_term ctxt (Thm.term_of ct)]]))) - end - - -(** overall reconstruction procedure **) - -local - fun not_supported r = raise Fail ("Z3: proof rule not implemented: " ^ - quote (Old_Z3_Proof_Parser.string_of_rule r)) - - fun prove_step simpset vars r ps ct (cxp as (cx, ptab)) = - (case (r, ps) of - (* core rules *) - (Old_Z3_Proof_Parser.True_Axiom, _) => (Thm Old_Z3_Proof_Literals.true_thm, cxp) - | (Old_Z3_Proof_Parser.Asserted, _) => raise Fail "bad assertion" - | (Old_Z3_Proof_Parser.Goal, _) => raise Fail "bad assertion" - | (Old_Z3_Proof_Parser.Modus_Ponens, [(p, _), (q, _)]) => - (mp q (thm_of p), cxp) - | (Old_Z3_Proof_Parser.Modus_Ponens_Oeq, [(p, _), (q, _)]) => - (mp q (thm_of p), cxp) - | (Old_Z3_Proof_Parser.And_Elim, [(p, i)]) => - and_elim (p, i) ct ptab ||> pair cx - | (Old_Z3_Proof_Parser.Not_Or_Elim, [(p, i)]) => - not_or_elim (p, i) ct ptab ||> pair cx - | (Old_Z3_Proof_Parser.Hypothesis, _) => (Thm (Thm.assume ct), cxp) - | (Old_Z3_Proof_Parser.Lemma, [(p, _)]) => (lemma (thm_of p) ct, cxp) - | (Old_Z3_Proof_Parser.Unit_Resolution, (p, _) :: ps) => - (unit_resolution (thm_of p) (map (thm_of o fst) ps) ct, cxp) - | (Old_Z3_Proof_Parser.Iff_True, [(p, _)]) => (iff_true (thm_of p), cxp) - | (Old_Z3_Proof_Parser.Iff_False, [(p, _)]) => (iff_false (thm_of p), cxp) - | (Old_Z3_Proof_Parser.Distributivity, _) => (distributivity cx ct, cxp) - | (Old_Z3_Proof_Parser.Def_Axiom, _) => (def_axiom cx ct, cxp) - | (Old_Z3_Proof_Parser.Intro_Def, _) => intro_def ct cx ||> rpair ptab - | (Old_Z3_Proof_Parser.Apply_Def, [(p, _)]) => (apply_def (thm_of p), cxp) - | (Old_Z3_Proof_Parser.Iff_Oeq, [(p, _)]) => (p, cxp) - | (Old_Z3_Proof_Parser.Nnf_Pos, _) => (nnf cx vars (map fst ps) ct, cxp) - | (Old_Z3_Proof_Parser.Nnf_Neg, _) => (nnf cx vars (map fst ps) ct, cxp) - - (* equality rules *) - | (Old_Z3_Proof_Parser.Reflexivity, _) => (refl ct, cxp) - | (Old_Z3_Proof_Parser.Symmetry, [(p, _)]) => (symm p, cxp) - | (Old_Z3_Proof_Parser.Transitivity, [(p, _), (q, _)]) => (trans p q, cxp) - | (Old_Z3_Proof_Parser.Monotonicity, _) => (monotonicity (map fst ps) ct, cxp) - | (Old_Z3_Proof_Parser.Commutativity, _) => (commutativity ct, cxp) - - (* quantifier rules *) - | (Old_Z3_Proof_Parser.Quant_Intro, [(p, _)]) => (quant_intro cx vars p ct, cxp) - | (Old_Z3_Proof_Parser.Pull_Quant, _) => (pull_quant cx ct, cxp) - | (Old_Z3_Proof_Parser.Push_Quant, _) => (push_quant cx ct, cxp) - | (Old_Z3_Proof_Parser.Elim_Unused_Vars, _) => (elim_unused_vars cx ct, cxp) - | (Old_Z3_Proof_Parser.Dest_Eq_Res, _) => (dest_eq_res cx ct, cxp) - | (Old_Z3_Proof_Parser.Quant_Inst, _) => (quant_inst cx ct, cxp) - | (Old_Z3_Proof_Parser.Skolemize, _) => skolemize vars ct cx ||> rpair ptab - - (* theory rules *) - | (Old_Z3_Proof_Parser.Th_Lemma _, _) => (* FIXME: use arguments *) - (th_lemma cx simpset (map (thm_of o fst) ps) ct, cxp) - | (Old_Z3_Proof_Parser.Rewrite, _) => rewrite simpset [] ct cx ||> rpair ptab - | (Old_Z3_Proof_Parser.Rewrite_Star, ps) => - rewrite simpset (map fst ps) ct cx ||> rpair ptab - - | (Old_Z3_Proof_Parser.Nnf_Star, _) => not_supported r - | (Old_Z3_Proof_Parser.Cnf_Star, _) => not_supported r - | (Old_Z3_Proof_Parser.Transitivity_Star, _) => not_supported r - | (Old_Z3_Proof_Parser.Pull_Quant_Star, _) => not_supported r - - | _ => raise Fail ("Z3: proof rule " ^ - quote (Old_Z3_Proof_Parser.string_of_rule r) ^ - " has an unexpected number of arguments.")) - - fun lookup_proof ptab idx = - (case Inttab.lookup ptab idx of - SOME p => (p, idx) - | NONE => z3_exn ("unknown proof id: " ^ quote (string_of_int idx))) - - fun prove simpset vars (idx, step) (_, cxp as (ctxt, ptab)) = - let - val Old_Z3_Proof_Parser.Proof_Step {rule=r, prems, prop, ...} = step - val ps = map (lookup_proof ptab) prems - val _ = trace_before ctxt idx r - val (thm, (ctxt', ptab')) = - cxp - |> prove_step simpset vars r ps prop - |> tap (check_after idx r ps prop) - in (thm, (ctxt', Inttab.update (idx, thm) ptab')) end - - fun make_discharge_rules rules = rules @ [@{thm allI}, @{thm refl}, - @{thm reflexive}, Old_Z3_Proof_Literals.true_thm] - - fun discharge_assms_tac ctxt rules = - REPEAT (HEADGOAL (resolve_tac ctxt rules ORELSE' SOLVED' (discharge_sk_tac ctxt))) - - fun discharge_assms ctxt rules thm = - if Thm.nprems_of thm = 0 then Goal.norm_result ctxt thm - else - (case Seq.pull (discharge_assms_tac ctxt rules thm) of - SOME (thm', _) => Goal.norm_result ctxt thm' - | NONE => raise THM ("failed to discharge premise", 1, [thm])) - - fun discharge rules outer_ctxt (p, (inner_ctxt, _)) = - thm_of p - |> singleton (Proof_Context.export inner_ctxt outer_ctxt) - |> discharge_assms outer_ctxt (make_discharge_rules rules) -in - -fun reconstruct outer_ctxt recon output = - let - val {context=ctxt, typs, terms, rewrite_rules, assms} = recon - val (asserted, steps, vars, ctxt1) = - Old_Z3_Proof_Parser.parse ctxt typs terms output - - val simpset = - Old_Z3_Proof_Tools.make_simpset ctxt1 (Named_Theorems.get ctxt1 @{named_theorems old_z3_simp}) - - val ((is, rules), cxp as (ctxt2, _)) = - add_asserted outer_ctxt rewrite_rules assms asserted ctxt1 - in - if Config.get ctxt2 Old_SMT_Config.filter_only_facts then (is, @{thm TrueI}) - else - (Thm @{thm TrueI}, cxp) - |> fold (prove simpset vars) steps - |> discharge rules outer_ctxt - |> pair [] - end - -end - -end diff -r d10f0bbc7ea1 -r f595b7532dc9 src/HOL/Library/Old_SMT/old_z3_proof_tools.ML --- a/src/HOL/Library/Old_SMT/old_z3_proof_tools.ML Thu Apr 20 10:45:52 2017 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,374 +0,0 @@ -(* Title: HOL/Library/Old_SMT/old_z3_proof_tools.ML - Author: Sascha Boehme, TU Muenchen - -Helper functions required for Z3 proof reconstruction. -*) - -signature OLD_Z3_PROOF_TOOLS = -sig - (*modifying terms*) - val as_meta_eq: cterm -> cterm - - (*theorem nets*) - val thm_net_of: ('a -> thm) -> 'a list -> 'a Net.net - val net_instances: (int * thm) Net.net -> cterm -> (int * thm) list - val net_instance: thm Net.net -> cterm -> thm option - - (*proof combinators*) - val under_assumption: (thm -> thm) -> cterm -> thm - val with_conv: conv -> (cterm -> thm) -> cterm -> thm - val discharge: thm -> thm -> thm - val varify: string list -> thm -> thm - val unfold_eqs: Proof.context -> thm list -> conv - val match_instantiate: (cterm -> cterm) -> cterm -> thm -> thm - val by_tac: Proof.context -> (int -> tactic) -> cterm -> thm - val make_hyp_def: thm -> Proof.context -> thm * Proof.context - val by_abstraction: int -> bool * bool -> Proof.context -> thm list -> - (Proof.context -> cterm -> thm) -> cterm -> 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 - - (*unfolding of 'distinct'*) - val unfold_distinct_conv: conv - - (*simpset*) - val add_simproc: Simplifier.simproc -> Context.generic -> Context.generic - val make_simpset: Proof.context -> thm list -> simpset -end - -structure Old_Z3_Proof_Tools: OLD_Z3_PROOF_TOOLS = -struct - - - -(* modifying terms *) - -fun as_meta_eq ct = - uncurry Old_SMT_Utils.mk_cequals (Thm.dest_binop (Old_SMT_Utils.dest_cprop ct)) - - - -(* 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 - -fun net_instance net = try hd o instances_from_net true I net - -end - - - -(* proof combinators *) - -fun under_assumption f ct = - let val ct' = Old_SMT_Utils.mk_cprop ct - in Thm.implies_intr ct' (f (Thm.assume ct')) end - -fun with_conv conv prove ct = - let val eq = Thm.symmetric (conv ct) - in Thm.equal_elim eq (prove (Thm.lhs_of eq)) end - -fun discharge p pq = Thm.implies_elim pq p - -fun varify vars = Drule.generalize ([], vars) - -fun unfold_eqs _ [] = Conv.all_conv - | unfold_eqs ctxt eqs = - Conv.top_sweep_conv (K (Conv.rewrs_conv eqs)) ctxt - -fun match_instantiate f ct thm = - Thm.instantiate (Thm.match (f (Thm.cprop_of thm), ct)) thm - -fun by_tac ctxt tac ct = Goal.norm_result ctxt (Goal.prove_internal ctxt [] ct (K (tac 1))) - -(* - |- c x == t x ==> P (c x) - --------------------------- - c == t |- P (c x) -*) -fun make_hyp_def thm ctxt = - let - val (lhs, rhs) = Thm.dest_binop (Thm.cprem_of thm 1) - val (cf, cvs) = Drule.strip_comb lhs - val eq = Old_SMT_Utils.mk_cequals cf (fold_rev Thm.lambda cvs rhs) - fun apply cv th = - Thm.combination th (Thm.reflexive cv) - |> Conv.fconv_rule (Conv.arg_conv (Thm.beta_conversion false)) - in - yield_singleton Assumption.add_assumes eq ctxt - |>> Thm.implies_elim thm o fold apply cvs - end - - - -(* abstraction *) - -local - -fun abs_context ctxt = (ctxt, Termtab.empty, 1, false) - -fun context_of (ctxt, _, _, _) = ctxt - -fun replace (_, (cv, ct)) = Thm.forall_elim ct o Thm.forall_intr cv - -fun abs_instantiate (_, tab, _, beta_norm) = - fold replace (Termtab.dest tab) #> - beta_norm ? Conv.fconv_rule (Thm.beta_conversion true) - -fun lambda_abstract cvs t = - let - val frees = map Free (Term.add_frees t []) - val cvs' = filter (fn cv => member (op aconv) frees (Thm.term_of cv)) cvs - val vs = map (Term.dest_Free o Thm.term_of) cvs' - in (fold_rev absfree vs t, cvs') end - -fun fresh_abstraction (_, cvs) ct (cx as (ctxt, tab, idx, beta_norm)) = - let val (t, cvs') = lambda_abstract cvs (Thm.term_of ct) - in - (case Termtab.lookup tab t of - SOME (cv, _) => (Drule.list_comb (cv, cvs'), cx) - | NONE => - let - val (n, ctxt') = yield_singleton Variable.variant_fixes "x" ctxt - val cv = Thm.cterm_of ctxt' - (Free (n, map Thm.typ_of_cterm cvs' ---> Thm.typ_of_cterm ct)) - val cu = Drule.list_comb (cv, cvs') - val e = (t, (cv, fold_rev Thm.lambda cvs' ct)) - val beta_norm' = beta_norm orelse not (null cvs') - in (cu, (ctxt', Termtab.update e tab, idx + 1, beta_norm')) end) - end - -fun abs_comb f g dcvs ct = - let val (cf, cu) = Thm.dest_comb ct - in f dcvs cf ##>> g dcvs cu #>> uncurry Thm.apply end - -fun abs_arg f = abs_comb (K pair) f - -fun abs_args f dcvs ct = - (case Thm.term_of ct of - _ $ _ => abs_comb (abs_args f) f dcvs ct - | _ => pair ct) - -fun abs_list f g dcvs ct = - (case Thm.term_of ct of - Const (@{const_name Nil}, _) => pair ct - | Const (@{const_name Cons}, _) $ _ $ _ => - abs_comb (abs_arg f) (abs_list f g) dcvs ct - | _ => g dcvs ct) - -fun abs_abs f (depth, cvs) ct = - let val (cv, cu) = Thm.dest_abs NONE ct - in f (depth, cv :: cvs) cu #>> Thm.lambda cv end - -val is_atomic = - (fn Free _ => true | Var _ => true | Bound _ => true | _ => false) - -fun abstract depth (ext_logic, with_theories) = - let - fun abstr1 cvs ct = abs_arg abstr cvs ct - and abstr2 cvs ct = abs_comb abstr1 abstr cvs ct - and abstr3 cvs ct = abs_comb abstr2 abstr cvs ct - and abstr_abs cvs ct = abs_arg (abs_abs abstr) cvs ct - - and abstr (dcvs as (d, cvs)) ct = - (case Thm.term_of ct of - @{const Trueprop} $ _ => abstr1 dcvs ct - | @{const Pure.imp} $ _ $ _ => abstr2 dcvs ct - | @{const True} => pair ct - | @{const False} => pair ct - | @{const Not} $ _ => abstr1 dcvs ct - | @{const HOL.conj} $ _ $ _ => abstr2 dcvs ct - | @{const HOL.disj} $ _ $ _ => abstr2 dcvs ct - | @{const HOL.implies} $ _ $ _ => abstr2 dcvs ct - | Const (@{const_name HOL.eq}, _) $ _ $ _ => abstr2 dcvs ct - | Const (@{const_name distinct}, _) $ _ => - if ext_logic then abs_arg (abs_list abstr fresh_abstraction) dcvs ct - else fresh_abstraction dcvs ct - | Const (@{const_name If}, _) $ _ $ _ $ _ => - if ext_logic then abstr3 dcvs ct else fresh_abstraction dcvs ct - | Const (@{const_name All}, _) $ _ => - if ext_logic then abstr_abs dcvs ct else fresh_abstraction dcvs ct - | Const (@{const_name Ex}, _) $ _ => - if ext_logic then abstr_abs dcvs ct else fresh_abstraction dcvs ct - | t => (fn cx => - if is_atomic t orelse can HOLogic.dest_number t then (ct, cx) - else if with_theories andalso - Old_Z3_Interface.is_builtin_theory_term (context_of cx) t - then abs_args abstr dcvs ct cx - else if d = 0 then fresh_abstraction dcvs ct cx - else - (case Term.strip_comb t of - (Const _, _) => abs_args abstr (d-1, cvs) ct cx - | (Free _, _) => abs_args abstr (d-1, cvs) ct cx - | _ => fresh_abstraction dcvs ct cx))) - in abstr (depth, []) end - -val cimp = Thm.cterm_of @{context} @{const Pure.imp} - -fun deepen depth f x = - if depth = 0 then f depth x - else (case try (f depth) x of SOME y => y | NONE => deepen (depth - 1) f x) - -fun with_prems depth thms f ct = - fold_rev (Thm.mk_binop cimp o Thm.cprop_of) thms ct - |> deepen depth f - |> fold (fn prem => fn th => Thm.implies_elim th prem) thms - -in - -fun by_abstraction depth mode ctxt thms prove = - with_prems depth thms (fn d => fn ct => - let val (cu, cx) = abstract d mode ct (abs_context ctxt) - in abs_instantiate cx (prove (context_of cx) cu) end) - -end - - - -(* 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) - - - -(* unfolding of 'distinct' *) - -local - val set1 = @{lemma "x ~: set [] == ~False" by simp} - val set2 = @{lemma "x ~: set [x] == False" by simp} - val set3 = @{lemma "x ~: set [y] == x ~= y" by simp} - val set4 = @{lemma "x ~: set (x # ys) == False" by simp} - val set5 = @{lemma "x ~: set (y # ys) == x ~= y & x ~: set ys" by simp} - - fun set_conv ct = - (Conv.rewrs_conv [set1, set2, set3, set4] else_conv - (Conv.rewr_conv set5 then_conv Conv.arg_conv set_conv)) ct - - val dist1 = @{lemma "distinct [] == ~False" by (simp add: distinct_def)} - val dist2 = @{lemma "distinct [x] == ~False" by (simp add: distinct_def)} - val dist3 = @{lemma "distinct (x # xs) == x ~: set xs & distinct xs" - by (simp add: distinct_def)} - - fun binop_conv cv1 cv2 = Conv.combination_conv (Conv.arg_conv cv1) cv2 -in -fun unfold_distinct_conv ct = - (Conv.rewrs_conv [dist1, dist2] else_conv - (Conv.rewr_conv dist3 then_conv binop_conv set_conv unfold_distinct_conv)) ct -end - - - -(* 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} - addsimps [@{thm times_divide_eq_right}, @{thm times_divide_eq_left}] - addsimps @{thms arith_special} addsimps @{thms arith_simps} - addsimps @{thms rel_simps} - addsimps @{thms array_rules} - addsimps @{thms term_true_def} addsimps @{thms term_false_def} - addsimps @{thms z3div_def} addsimps @{thms z3mod_def} - addsimprocs [@{simproc numeral_divmod}] - addsimprocs [ - 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 d10f0bbc7ea1 -r f595b7532dc9 src/HOL/ROOT --- a/src/HOL/ROOT Thu Apr 20 10:45:52 2017 +0200 +++ b/src/HOL/ROOT Thu Apr 20 16:21:28 2017 +0200 @@ -55,7 +55,6 @@ (*legacy tools*) Old_Datatype Old_Recdef - Old_SMT Refute document_files "root.bib" "root.tex"