--- a/NEWS Fri Apr 21 20:07:51 2017 +0200
+++ b/NEWS Fri Apr 21 20:36:20 2017 +0200
@@ -151,6 +151,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.
--- a/src/Doc/Prog_Prove/Bool_nat_list.thy Fri Apr 21 20:07:51 2017 +0200
+++ b/src/Doc/Prog_Prove/Bool_nat_list.thy Fri Apr 21 20:36:20 2017 +0200
@@ -416,7 +416,7 @@
@{prop"tl(x#xs) = xs"}
\end{isabelle}
Note that since HOL is a logic of total functions, @{term"hd []"} is defined,
-but we do now know what the result is. That is, @{term"hd []"} is not undefined
+but we do not know what the result is. That is, @{term"hd []"} is not undefined
but underdefined.
\fi
%
--- a/src/Doc/Sledgehammer/document/root.tex Fri Apr 21 20:07:51 2017 +0200
+++ b/src/Doc/Sledgehammer/document/root.tex Fri Apr 21 20:36:20 2017 +0200
@@ -816,7 +816,7 @@
Versions strictly above 1.8 support the TPTP typed first-order format (TFF0).
\item[\labelitemi] \textbf{\textit{verit}:} veriT \cite{bouton-et-al-2009} is an
-SMT solver developed by David Déharbe, Pascal Fontaine, and their colleagues.
+SMT solver developed by David D\'eharbe, Pascal Fontaine, and their colleagues.
It is specifically designed to produce detailed proofs for reconstruction in
proof assistants. To use veriT, set the environment variable
\texttt{VERIT\_SOLVER} to the complete path of the executable, including the
--- a/src/HOL/Library/Old_SMT.thy Fri Apr 21 20:07:51 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 \<open>Old Version of Bindings to Satisfiability Modulo Theories (SMT) solvers\<close>
-
-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 \<open>Triggers for quantifier instantiation\<close>
-
-text \<open>
-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.
-\<close>
-
-typedecl pattern
-
-consts
- pat :: "'a \<Rightarrow> pattern"
- nopat :: "'a \<Rightarrow> pattern"
-
-definition trigger :: "pattern list list \<Rightarrow> bool \<Rightarrow> bool" where "trigger _ P = P"
-
-
-subsection \<open>Quantifier weights\<close>
-
-text \<open>
-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.
-\<close>
-
-definition weight :: "int \<Rightarrow> bool \<Rightarrow> bool" where "weight _ P = P"
-
-text \<open>
-Weights must be non-negative. The value \<open>0\<close> 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 "\<forall>x. trigger [[pat (P x)]] (weight 2 (P x))"}
-\item
-@{term "\<forall>x. weight 3 (P x)"}
-\end{itemize}
-\<close>
-
-
-subsection \<open>Higher-order encoding\<close>
-
-text \<open>
-Application is made explicit for constants occurring with varying
-numbers of arguments. This is achieved by the introduction of the
-following constant.
-\<close>
-
-definition fun_app where "fun_app f = f"
-
-text \<open>
-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.
-\<close>
-
-lemmas array_rules = ext fun_upd_apply fun_upd_same fun_upd_other
- fun_upd_upd fun_app_def
-
-
-subsection \<open>First-order logic\<close>
-
-text \<open>
-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.
-\<close>
-
-definition term_true where "term_true = True"
-definition term_false where "term_false = False"
-
-
-subsection \<open>Integer division and modulo for Z3\<close>
-
-definition z3div :: "int \<Rightarrow> int \<Rightarrow> int" where
- "z3div k l = (if 0 \<le> l then k div l else -(k div (-l)))"
-
-definition z3mod :: "int \<Rightarrow> int \<Rightarrow> int" where
- "z3mod k l = (if 0 \<le> l then k mod l else k mod (-l))"
-
-
-subsection \<open>Setup\<close>
-
-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 \<open>
- Old_SMT_Config.setup #>
- Old_SMT_Normalize.setup #>
- Old_SMTLIB_Interface.setup #>
- Old_Z3_Interface.setup #>
- Old_SMT_Setup_Solvers.setup
-\<close>
-
-method_setup old_smt = \<open>
- 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)))))
-\<close> "apply an SMT solver to the current goal"
-
-
-subsection \<open>Configuration\<close>
-
-text \<open>
-The current configuration can be printed by the command
-\<open>old_smt_status\<close>, which shows the values of most options.
-\<close>
-
-
-
-subsection \<open>General configuration options\<close>
-
-text \<open>
-The option \<open>old_smt_solver\<close> can be used to change the target SMT
-solver. The possible values can be obtained from the \<open>old_smt_status\<close>
-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 \<open>OLD_Z3_NON_COMMERCIAL\<close> environment variable to
-\<open>yes\<close>.
-\<close>
-
-declare [[ old_smt_solver = z3 ]]
-
-text \<open>
-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.
-\<close>
-
-declare [[ old_smt_timeout = 20 ]]
-
-text \<open>
-SMT solvers apply randomized heuristics. In case a problem is not
-solvable by an SMT solver, changing the following option might help.
-\<close>
-
-declare [[ old_smt_random_seed = 1 ]]
-
-text \<open>
-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.
-\<close>
-
-declare [[ old_smt_oracle = false ]]
-
-text \<open>
-Each SMT solver provides several commandline options to tweak its
-behaviour. They can be passed to the solver by setting the following
-options.
-\<close>
-
-declare [[ old_cvc3_options = "" ]]
-declare [[ old_yices_options = "" ]]
-declare [[ old_z3_options = "" ]]
-
-text \<open>
-Enable the following option to use built-in support for datatypes and
-records. Currently, this is only implemented for Z3 running in oracle
-mode.
-\<close>
-
-declare [[ old_smt_datatypes = false ]]
-
-text \<open>
-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.
-\<close>
-
-declare [[ old_smt_infer_triggers = false ]]
-
-text \<open>
-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.
-\<close>
-
-declare [[ monomorph_max_rounds = 5 ]]
-
-text \<open>
-In addition, the number of generated monomorphic instances is limited
-by the following option.
-\<close>
-
-declare [[ monomorph_max_new_instances = 500 ]]
-
-
-
-subsection \<open>Certificates\<close>
-
-text \<open>
-By setting the option \<open>old_smt_certificates\<close> 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
-\<open>.certs\<close> instead of \<open>.thy\<close>) 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.
-\<close>
-
-declare [[ old_smt_certificates = "" ]]
-
-text \<open>
-The option \<open>old_smt_read_only_certificates\<close> controls whether only
-stored certificates are should be used or invocation of an SMT solver
-is allowed. When set to \<open>true\<close>, no SMT solver will ever be
-invoked and only the existing certificates found in the configured
-cache are used; when set to \<open>false\<close> and there is no cached
-certificate for some proposition, then the configured SMT solver is
-invoked.
-\<close>
-
-declare [[ old_smt_read_only_certificates = false ]]
-
-
-
-subsection \<open>Tracing\<close>
-
-text \<open>
-The SMT method, when applied, traces important information. To
-make it entirely silent, set the following option to \<open>false\<close>.
-\<close>
-
-declare [[ old_smt_verbose = true ]]
-
-text \<open>
-For tracing the generated problem file given to the SMT solver as
-well as the returned result of the solver, the option
-\<open>old_smt_trace\<close> should be set to \<open>true\<close>.
-\<close>
-
-declare [[ old_smt_trace = false ]]
-
-text \<open>
-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 \<open>old_smt_solver\<close> and \<open>old_smt_oracle\<close> above).
-\<close>
-
-declare [[ old_smt_trace_used_facts = false ]]
-
-
-
-subsection \<open>Schematic rules for Z3 proof reconstruction\<close>
-
-text \<open>
-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 \<open>z3_rule\<close> are tried prior to
-any implemented reconstruction procedure for all uncertain Z3 proof
-rules; the facts in \<open>z3_simp\<close> are only fed to invocations of
-the simplifier when reconstructing theory-specific proof steps.
-\<close>
-
-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 \<and> Q) = (\<not>(\<not>P \<or> \<not>Q))"
- "(P \<and> Q) = (\<not>(\<not>Q \<or> \<not>P))"
- "(\<not>P \<and> Q) = (\<not>(P \<or> \<not>Q))"
- "(\<not>P \<and> Q) = (\<not>(\<not>Q \<or> P))"
- "(P \<and> \<not>Q) = (\<not>(\<not>P \<or> Q))"
- "(P \<and> \<not>Q) = (\<not>(Q \<or> \<not>P))"
- "(\<not>P \<and> \<not>Q) = (\<not>(P \<or> Q))"
- "(\<not>P \<and> \<not>Q) = (\<not>(Q \<or> P))"
- by auto
-
-lemma [old_z3_rule]:
- "(P \<longrightarrow> Q) = (Q \<or> \<not>P)"
- "(\<not>P \<longrightarrow> Q) = (P \<or> Q)"
- "(\<not>P \<longrightarrow> Q) = (Q \<or> P)"
- "(True \<longrightarrow> P) = P"
- "(P \<longrightarrow> True) = True"
- "(False \<longrightarrow> P) = True"
- "(P \<longrightarrow> P) = True"
- by auto
-
-lemma [old_z3_rule]:
- "((P = Q) \<longrightarrow> R) = (R | (Q = (\<not>P)))"
- by auto
-
-lemma [old_z3_rule]:
- "(\<not>True) = False"
- "(\<not>False) = True"
- "(x = x) = True"
- "(P = True) = P"
- "(True = P) = P"
- "(P = False) = (\<not>P)"
- "(False = P) = (\<not>P)"
- "((\<not>P) = P) = False"
- "(P = (\<not>P)) = False"
- "((\<not>P) = (\<not>Q)) = (P = Q)"
- "\<not>(P = (\<not>Q)) = (P = Q)"
- "\<not>((\<not>P) = Q) = (P = Q)"
- "(P \<noteq> Q) = (Q = (\<not>P))"
- "(P = Q) = ((\<not>P \<or> Q) \<and> (P \<or> \<not>Q))"
- "(P \<noteq> Q) = ((\<not>P \<or> \<not>Q) \<and> (P \<or> Q))"
- by auto
-
-lemma [old_z3_rule]:
- "(if P then P else \<not>P) = True"
- "(if \<not>P then \<not>P else P) = True"
- "(if P then True else False) = P"
- "(if P then False else True) = (\<not>P)"
- "(if P then Q else True) = ((\<not>P) \<or> Q)"
- "(if P then Q else True) = (Q \<or> (\<not>P))"
- "(if P then Q else \<not>Q) = (P = Q)"
- "(if P then Q else \<not>Q) = (Q = P)"
- "(if P then \<not>Q else Q) = (P = (\<not>Q))"
- "(if P then \<not>Q else Q) = ((\<not>Q) = P)"
- "(if \<not>P then x else y) = (if P then y else x)"
- "(if P then (if Q then x else y) else x) = (if P \<and> (\<not>Q) then y else x)"
- "(if P then (if Q then x else y) else x) = (if (\<not>Q) \<and> P then y else x)"
- "(if P then (if Q then x else y) else y) = (if P \<and> Q then x else y)"
- "(if P then (if Q then x else y) else y) = (if Q \<and> 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 \<or> Q then x else y)"
- "(if P then x else if Q then x else y) = (if Q \<or> 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 \<or> P \<or> Q"
- "P = Q \<or> \<not>P \<or> \<not>Q"
- "(\<not>P) = Q \<or> \<not>P \<or> Q"
- "(\<not>P) = Q \<or> P \<or> \<not>Q"
- "P = (\<not>Q) \<or> \<not>P \<or> Q"
- "P = (\<not>Q) \<or> P \<or> \<not>Q"
- "P \<noteq> Q \<or> P \<or> \<not>Q"
- "P \<noteq> Q \<or> \<not>P \<or> Q"
- "P \<noteq> (\<not>Q) \<or> P \<or> Q"
- "(\<not>P) \<noteq> Q \<or> P \<or> Q"
- "P \<or> Q \<or> P \<noteq> (\<not>Q)"
- "P \<or> Q \<or> (\<not>P) \<noteq> Q"
- "P \<or> \<not>Q \<or> P \<noteq> Q"
- "\<not>P \<or> Q \<or> P \<noteq> Q"
- "P \<or> y = (if P then x else y)"
- "P \<or> (if P then x else y) = y"
- "\<not>P \<or> x = (if P then x else y)"
- "\<not>P \<or> (if P then x else y) = x"
- "P \<or> R \<or> \<not>(if P then Q else R)"
- "\<not>P \<or> Q \<or> \<not>(if P then Q else R)"
- "\<not>(if P then Q else R) \<or> \<not>P \<or> Q"
- "\<not>(if P then Q else R) \<or> P \<or> R"
- "(if P then Q else R) \<or> \<not>P \<or> \<not>Q"
- "(if P then Q else R) \<or> P \<or> \<not>R"
- "(if P then \<not>Q else R) \<or> \<not>P \<or> Q"
- "(if P then Q else \<not>R) \<or> P \<or> 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
--- a/src/HOL/Library/Old_SMT/old_smt_builtin.ML Fri Apr 21 20:07:51 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
--- a/src/HOL/Library/Old_SMT/old_smt_config.ML Fri Apr 21 20:07:51 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
--- a/src/HOL/Library/Old_SMT/old_smt_datatypes.ML Fri Apr 21 20:07:51 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
--- a/src/HOL/Library/Old_SMT/old_smt_failure.ML Fri Apr 21 20:07:51 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
--- a/src/HOL/Library/Old_SMT/old_smt_normalize.ML Fri Apr 21 20:07:51 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
--- a/src/HOL/Library/Old_SMT/old_smt_real.ML Fri Apr 21 20:07:51 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) \<le> 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
--- a/src/HOL/Library/Old_SMT/old_smt_setup_solvers.ML Fri Apr 21 20:07:51 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
--- a/src/HOL/Library/Old_SMT/old_smt_solver.ML Fri Apr 21 20:07:51 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
--- a/src/HOL/Library/Old_SMT/old_smt_translate.ML Fri Apr 21 20:07:51 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
--- a/src/HOL/Library/Old_SMT/old_smt_utils.ML Fri Apr 21 20:07:51 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
--- a/src/HOL/Library/Old_SMT/old_smt_word.ML Fri Apr 21 20:07:51 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
--- a/src/HOL/Library/Old_SMT/old_smtlib_interface.ML Fri Apr 21 20:07:51 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
--- a/src/HOL/Library/Old_SMT/old_z3_interface.ML Fri Apr 21 20:07:51 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
--- a/src/HOL/Library/Old_SMT/old_z3_model.ML Fri Apr 21 20:07:51 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
-
--- a/src/HOL/Library/Old_SMT/old_z3_proof_literals.ML Fri Apr 21 20:07:51 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
--- a/src/HOL/Library/Old_SMT/old_z3_proof_methods.ML Fri Apr 21 20:07:51 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
--- a/src/HOL/Library/Old_SMT/old_z3_proof_parser.ML Fri Apr 21 20:07:51 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
--- a/src/HOL/Library/Old_SMT/old_z3_proof_reconstruction.ML Fri Apr 21 20:07:51 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
--- a/src/HOL/Library/Old_SMT/old_z3_proof_tools.ML Fri Apr 21 20:07:51 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) \<le> n"}, @{term "(m::int) = n"}],
- proc = K Lin_Arith.simproc},
- Simplifier.make_simproc @{context} "antisym_le"
- {lhss = [@{term "(x::'a::order) \<le> y"}],
- proc = K prove_antisym_le},
- Simplifier.make_simproc @{context} "antisym_less"
- {lhss = [@{term "\<not> (x::'a::linorder) < y"}],
- proc = K prove_antisym_less}])
-
- structure Simpset = Generic_Data
- (
- type T = simpset
- val empty = basic_simpset
- val extend = I
- val merge = Simplifier.merge_ss
- )
-in
-
-fun add_simproc simproc context =
- Simpset.map (simpset_map (Context.proof_of context)
- (fn ctxt => ctxt addsimprocs [simproc])) context
-
-fun make_simpset ctxt rules =
- simpset_of (put_simpset (Simpset.get (Context.Proof ctxt)) ctxt addsimps rules)
-
-end
-
-end
--- a/src/HOL/ROOT Fri Apr 21 20:07:51 2017 +0200
+++ b/src/HOL/ROOT Fri Apr 21 20:36:20 2017 +0200
@@ -59,7 +59,6 @@
(*legacy tools*)
Old_Datatype
Old_Recdef
- Old_SMT
Refute
document_files "root.bib" "root.tex"