--- a/src/HOL/SMT.thy Thu Jun 12 01:00:49 2014 +0200
+++ b/src/HOL/SMT.thy Thu Jun 12 01:00:49 2014 +0200
@@ -5,7 +5,7 @@
header {* Bindings to Satisfiability Modulo Theories (SMT) solvers *}
theory SMT
-imports List
+imports ATP
keywords "smt_status" :: diag
begin
--- a/src/HOL/Tools/SMT2/smt2_builtin.ML Thu Jun 12 01:00:49 2014 +0200
+++ b/src/HOL/Tools/SMT2/smt2_builtin.ML Thu Jun 12 01:00:49 2014 +0200
@@ -40,7 +40,7 @@
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
+end;
structure SMT2_Builtin: SMT2_BUILTIN =
struct
@@ -219,4 +219,4 @@
fun is_builtin_fun_ext ctxt c ts = is_some (dest_builtin_fun_ext ctxt c ts)
-end
+end;
--- a/src/HOL/Tools/SMT2/smt2_config.ML Thu Jun 12 01:00:49 2014 +0200
+++ b/src/HOL/Tools/SMT2/smt2_config.ML Thu Jun 12 01:00:49 2014 +0200
@@ -47,7 +47,7 @@
(*setup*)
val print_setup: Proof.context -> unit
-end
+end;
structure SMT2_Config: SMT2_CONFIG =
struct
@@ -246,4 +246,4 @@
\and the values of SMT configuration options"
(Scan.succeed (Toplevel.keep (print_setup o Toplevel.context_of)))
-end
+end;
--- a/src/HOL/Tools/SMT2/smt2_datatypes.ML Thu Jun 12 01:00:49 2014 +0200
+++ b/src/HOL/Tools/SMT2/smt2_datatypes.ML Thu Jun 12 01:00:49 2014 +0200
@@ -10,7 +10,7 @@
val add_decls: typ ->
(typ * (term * term list) list) list list * Proof.context ->
(typ * (term * term list) list) list list * Proof.context
-end
+end;
structure SMT2_Datatypes: SMT2_DATATYPES =
struct
@@ -90,4 +90,4 @@
in fold add Us (ins dss, ctxt2) end))
in add T ([], ctxt) |>> append declss o map snd end
-end
+end;
--- a/src/HOL/Tools/SMT2/smt2_failure.ML Thu Jun 12 01:00:49 2014 +0200
+++ b/src/HOL/Tools/SMT2/smt2_failure.ML Thu Jun 12 01:00:49 2014 +0200
@@ -14,7 +14,7 @@
Other_Failure of string
val string_of_failure: failure -> string
exception SMT of failure
-end
+end;
structure SMT2_Failure: SMT2_FAILURE =
struct
@@ -37,4 +37,4 @@
exception SMT of failure
-end
+end;
--- a/src/HOL/Tools/SMT2/smt2_normalize.ML Thu Jun 12 01:00:49 2014 +0200
+++ b/src/HOL/Tools/SMT2/smt2_normalize.ML Thu Jun 12 01:00:49 2014 +0200
@@ -16,7 +16,7 @@
type extra_norm = Proof.context -> thm list * thm list -> thm list * thm list
val add_extra_norm: SMT2_Util.class * extra_norm -> Context.generic -> Context.generic
val normalize: Proof.context -> thm list -> (int * thm) list
-end
+end;
structure SMT2_Normalize: SMT2_NORMALIZE =
struct
@@ -264,7 +264,6 @@
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 =
@@ -456,7 +455,6 @@
|> burrow_ids add_nat_embedding
-
(* overall normalization *)
type extra_norm = Proof.context -> thm list * thm list -> thm list * thm list
@@ -526,4 +524,4 @@
setup_abs_min_max #>
setup_nat_as_int))
-end
+end;
--- a/src/HOL/Tools/SMT2/smt2_real.ML Thu Jun 12 01:00:49 2014 +0200
+++ b/src/HOL/Tools/SMT2/smt2_real.ML Thu Jun 12 01:00:49 2014 +0200
@@ -118,4 +118,4 @@
Z3_New_Interface.add_mk_builtins z3_mk_builtins #>
Z3_New_Replay_Util.add_simproc real_linarith_proc))
-end
+end;
--- a/src/HOL/Tools/SMT2/smt2_solver.ML Thu Jun 12 01:00:49 2014 +0200
+++ b/src/HOL/Tools/SMT2/smt2_solver.ML Thu Jun 12 01:00:49 2014 +0200
@@ -38,12 +38,11 @@
(*tactic*)
val smt2_tac: Proof.context -> thm list -> int -> tactic
val smt2_tac': Proof.context -> thm list -> int -> tactic
-end
+end;
structure SMT2_Solver: SMT2_SOLVER =
struct
-
(* interface to external solvers *)
local
@@ -298,4 +297,4 @@
end
-end
+end;
--- a/src/HOL/Tools/SMT2/smt2_systems.ML Thu Jun 12 01:00:49 2014 +0200
+++ b/src/HOL/Tools/SMT2/smt2_systems.ML Thu Jun 12 01:00:49 2014 +0200
@@ -12,7 +12,7 @@
Z3_Non_Commercial_Declined
val z3_non_commercial: unit -> z3_non_commercial
val z3_extensions: bool Config.T
-end
+end;
structure SMT2_Systems: SMT2_SYSTEMS =
struct
@@ -155,4 +155,4 @@
SMT2_Solver.add_solver yices #>
SMT2_Solver.add_solver z3)
-end
+end;
--- a/src/HOL/Tools/SMT2/smt2_translate.ML Thu Jun 12 01:00:49 2014 +0200
+++ b/src/HOL/Tools/SMT2/smt2_translate.ML Thu Jun 12 01:00:49 2014 +0200
@@ -35,7 +35,7 @@
(*translation*)
val add_config: SMT2_Util.class * (Proof.context -> config) -> Context.generic -> Context.generic
val translate: Proof.context -> string list -> (int * thm) list -> string * replay_data
-end
+end;
structure SMT2_Translate: SMT2_TRANSLATE =
struct
@@ -54,7 +54,6 @@
SQua of squant * string list * sterm spattern list * sterm
-
(* translation configuration *)
type sign = {
@@ -76,7 +75,6 @@
assms: (int * thm) list }
-
(* translation context *)
fun add_components_of_typ (Type (s, Ts)) =
@@ -131,7 +129,6 @@
end
-
(* preprocessing *)
(** datatype declarations **)
@@ -454,7 +451,6 @@
in ((sign_of (header ts) dtyps trx', us), trx') end
-
(* translation *)
structure Configs = Generic_Data
@@ -521,4 +517,4 @@
||> replay_data_of ctxt2 rewrite_rules ithms
end
-end
+end;
--- a/src/HOL/Tools/SMT2/smt2_util.ML Thu Jun 12 01:00:49 2014 +0200
+++ b/src/HOL/Tools/SMT2/smt2_util.ML Thu Jun 12 01:00:49 2014 +0200
@@ -59,7 +59,7 @@
val under_quant_conv: (Proof.context * cterm list -> conv) ->
Proof.context -> conv
val prop_conv: conv -> conv
-end
+end;
structure SMT2_Util: SMT2_UTIL =
struct
@@ -221,4 +221,4 @@
@{const Trueprop} $ _ => Conv.arg_conv cv ct
| _ => raise CTERM ("not a property", [ct]))
-end
+end;
--- a/src/HOL/Tools/SMT2/smtlib2.ML Thu Jun 12 01:00:49 2014 +0200
+++ b/src/HOL/Tools/SMT2/smtlib2.ML Thu Jun 12 01:00:49 2014 +0200
@@ -17,7 +17,7 @@
val parse: string list -> tree
val pretty_tree: tree -> Pretty.T
val str_of: tree -> string
-end
+end;
structure SMTLIB2: SMTLIB2 =
struct
@@ -37,7 +37,6 @@
datatype unfinished = None | String of string | Symbol of string
-
(* utilities *)
fun read_raw pred l cs =
@@ -47,7 +46,6 @@
| x => x)
-
(* numerals and decimals *)
fun int_of cs = fst (read_int cs)
@@ -60,7 +58,6 @@
| (cs1, cs2) => (Num (int_of cs1), cs2))
-
(* binary numbers *)
fun is_bin c = (c = "0" orelse c = "1")
@@ -68,7 +65,6 @@
fun read_bin l cs = read_raw is_bin l cs |>> Num o fst o read_radix_int 2
-
(* hex numbers *)
val is_hex = member (op =) (raw_explode "0123456789abcdefABCDEF")
@@ -85,7 +81,6 @@
fun read_hex l cs = read_raw is_hex l cs |>> Num o unhex 0
-
(* symbols *)
val symbol_chars = raw_explode "~!@$%^&*_+=<>.?/-"
@@ -98,7 +93,6 @@
fun read_sym f l cs = read_raw is_sym l cs |>> f o implode
-
(* quoted tokens *)
fun read_quoted stop (escape, replacement) cs =
@@ -116,7 +110,6 @@
fun read_symbol cs = read_quoted ["|"] ([], "") cs
-
(* core parser *)
fun read _ [] rest tss = (rest, tss)
@@ -172,7 +165,6 @@
fun parse lines = finish (fold add_line lines (1, (None, [[]])))
-
(* pretty printer *)
fun pretty_tree (Num i) = Pretty.str (string_of_int i)
@@ -196,4 +188,4 @@
val str_of = Pretty.str_of o pretty_tree
-end
+end;
--- a/src/HOL/Tools/SMT2/smtlib2_interface.ML Thu Jun 12 01:00:49 2014 +0200
+++ b/src/HOL/Tools/SMT2/smtlib2_interface.ML Thu Jun 12 01:00:49 2014 +0200
@@ -11,7 +11,7 @@
val add_logic: int * (term list -> string option) -> Context.generic -> Context.generic
val translate_config: Proof.context -> SMT2_Translate.config
val assert_index_of_name: string -> int
-end
+end;
structure SMTLIB2_Interface: SMTLIB2_INTERFACE =
struct
@@ -156,4 +156,4 @@
(setup_builtins #>
SMT2_Translate.add_config (smtlib2C, translate_config)))
-end
+end;
--- a/src/HOL/Tools/SMT2/z3_new_interface.ML Thu Jun 12 01:00:49 2014 +0200
+++ b/src/HOL/Tools/SMT2/z3_new_interface.ML Thu Jun 12 01:00:49 2014 +0200
@@ -19,7 +19,7 @@
val mk_builtin_fun: Proof.context -> sym -> cterm list -> cterm option
val is_builtin_theory_term: Proof.context -> term -> bool
-end
+end;
structure Z3_New_Interface: Z3_NEW_INTERFACE =
struct
@@ -27,7 +27,6 @@
val smtlib2_z3C = SMTLIB2_Interface.smtlib2C @ ["z3"]
-
(* interface *)
local
@@ -63,7 +62,6 @@
end
-
(* constructors *)
datatype sym = Sym of string * sym list
@@ -185,7 +183,6 @@
| _ => chained_mk_builtin_fun ctxt (get_mk_builtins ctxt) sym cts))
-
(* abstraction *)
fun is_builtin_theory_term ctxt t =
@@ -195,4 +192,4 @@
(Const c, ts) => SMT2_Builtin.is_builtin_fun ctxt c ts
| _ => false)
-end
+end;
--- a/src/HOL/Tools/SMT2/z3_new_proof.ML Thu Jun 12 01:00:49 2014 +0200
+++ b/src/HOL/Tools/SMT2/z3_new_proof.ML Thu Jun 12 01:00:49 2014 +0200
@@ -194,7 +194,6 @@
error (msg ^ ": " ^ SMTLIB2.str_of t)
-
(* handling of bound variables *)
fun subst_of tyenv =
@@ -269,7 +268,6 @@
end
-
(* linearizing proofs and resolving types of bound variables *)
fun has_step (tab, _) = Inttab.defined tab
@@ -300,7 +298,6 @@
rev (snd (snd (lin_proof ctxt Symtab.empty node (Inttab.empty, []))))
-
(* overall proof parser *)
fun parse typs funs lines ctxt =
--- a/src/HOL/Tools/SMT2/z3_new_real.ML Thu Jun 12 01:00:49 2014 +0200
+++ b/src/HOL/Tools/SMT2/z3_new_real.ML Thu Jun 12 01:00:49 2014 +0200
@@ -29,4 +29,4 @@
SMTLIB2_Proof.add_term_parser real_term_parser #>
Z3_New_Replay_Methods.add_arith_abstracter abstract))
-end
+end;
--- a/src/HOL/Tools/SMT2/z3_new_replay.ML Thu Jun 12 01:00:49 2014 +0200
+++ b/src/HOL/Tools/SMT2/z3_new_replay.ML Thu Jun 12 01:00:49 2014 +0200
@@ -11,7 +11,7 @@
((string * ATP_Problem_Generate.stature) * thm) list -> term list -> term -> string list ->
SMT2_Solver.parsed_proof
val replay: Proof.context -> SMT2_Translate.replay_data -> string list -> thm
-end
+end;
structure Z3_New_Replay: Z3_NEW_REPLAY =
struct
@@ -216,4 +216,4 @@
Inttab.lookup proofs id |> the |> snd |> discharge rules outer_ctxt ctxt4
end
-end
+end;
--- a/src/HOL/Tools/SMT2/z3_new_replay_literals.ML Thu Jun 12 01:00:49 2014 +0200
+++ b/src/HOL/Tools/SMT2/z3_new_replay_literals.ML Thu Jun 12 01:00:49 2014 +0200
@@ -28,13 +28,11 @@
val explode: bool -> bool -> bool -> term list -> thm -> thm list
val join: bool -> littab -> term -> thm
val prove_conj_disj_eq: cterm -> thm
-end
+end;
structure Z3_New_Replay_Literals: Z3_NEW_REPLAY_LITERALS =
struct
-
-
(* literal table *)
type littab = thm Termtab.table
@@ -48,14 +46,12 @@
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)
@@ -84,7 +80,6 @@
val negate = Thm.apply (Thm.cterm_of @{theory} @{const Not})
-
(* proof tools *)
(** explosion of conjunctions and disjunctions **)
@@ -353,4 +348,4 @@
end
-end
+end;
--- a/src/HOL/Tools/SMT2/z3_new_replay_methods.ML Thu Jun 12 01:00:49 2014 +0200
+++ b/src/HOL/Tools/SMT2/z3_new_replay_methods.ML Thu Jun 12 01:00:49 2014 +0200
@@ -50,7 +50,7 @@
val mp_oeq: z3_method
val th_lemma: string -> z3_method
val method_for: Z3_New_Proof.z3_rule -> z3_method
-end
+end;
structure Z3_New_Replay_Methods: Z3_NEW_REPLAY_METHODS =
struct
@@ -58,7 +58,6 @@
type z3_method = Proof.context -> thm list -> term -> thm
-
(* utility functions *)
fun trace ctxt f = SMT2_Config.trace_msg ctxt f ()
@@ -144,7 +143,6 @@
fun quant_tac ctxt = Blast.blast_tac ctxt
-
(* plug-ins *)
type abs_context = int * term Termtab.table
@@ -174,7 +172,6 @@
fun get_th_lemma_method ctxt = snd (Plugins.get (Context.Proof ctxt))
-
(* abstraction *)
fun prove_abstract ctxt thms t tac f =
@@ -279,13 +276,11 @@
in abs u end
-
(* truth axiom *)
fun true_axiom _ _ _ = @{thm TrueI}
-
(* modus ponens *)
fun mp _ [p, p_eq_q] _ = discharge 1 [p_eq_q, p] iffD1
@@ -294,27 +289,23 @@
val mp_oeq = mp
-
(* reflexivity *)
fun refl ctxt _ t = match_instantiate ctxt t @{thm refl}
-
(* symmetry *)
fun symm _ [thm] _ = thm RS @{thm sym}
| symm ctxt thms t = replay_rule_error ctxt Z3_New_Proof.Reflexivity thms t
-
(* transitivity *)
fun trans _ [thm1, thm2] _ = thm1 RSN (1, thm2 RSN (2, @{thm trans}))
| trans ctxt thms t = replay_rule_error ctxt Z3_New_Proof.Transitivity thms t
-
(* congruence *)
fun ctac prems i st = st |> (
@@ -345,7 +336,6 @@
("full", cong_full ctxt thms)] thms
-
(* quantifier introduction *)
val quant_intro_rules = @{lemma
@@ -360,7 +350,6 @@
| quant_intro ctxt thms t = replay_rule_error ctxt Z3_New_Proof.Quant_Intro thms t
-
(* distributivity of conjunctions and disjunctions *)
(* TODO: there are no tests with this proof rule *)
@@ -368,7 +357,6 @@
prove_abstract' ctxt t prop_tac (abstract_prop (dest_prop t))
-
(* elimination of conjunctions *)
fun and_elim ctxt [thm] t =
@@ -379,7 +367,6 @@
| and_elim ctxt thms t = replay_rule_error ctxt Z3_New_Proof.And_Elim thms t
-
(* elimination of negated disjunctions *)
fun not_or_elim ctxt [thm] t =
@@ -391,7 +378,6 @@
replay_rule_error ctxt Z3_New_Proof.Not_Or_Elim thms t
-
(* rewriting *)
local
@@ -452,19 +438,16 @@
fun rewrite_star ctxt = rewrite ctxt
-
(* pulling quantifiers *)
fun pull_quant ctxt _ t = prove ctxt t quant_tac
-
(* pushing quantifiers *)
fun push_quant _ _ _ = raise Fail "unsupported" (* FIXME *)
-
(* elimination of unused bound variables *)
val elim_all = @{lemma "P = Q ==> (ALL x. P) = Q" by fast}
@@ -480,13 +463,11 @@
fun elim_unused ctxt _ t = prove ctxt t (fn _ => elim_unused_tac)
-
(* destructive equality resolution *)
fun dest_eq_res _ _ _ = raise Fail "dest_eq_res" (* FIXME *)
-
(* quantifier instantiation *)
val quant_inst_rule = @{lemma "~P x | Q ==> ~(ALL x. P x) | Q" by fast}
@@ -496,7 +477,6 @@
THEN' rtac @{thm excluded_middle})
-
(* propositional lemma *)
exception LEMMA of unit
@@ -535,7 +515,6 @@
| lemma ctxt thms t = replay_rule_error ctxt Z3_New_Proof.Lemma thms t
-
(* unit resolution *)
fun abstract_unit (t as (@{const HOL.Not} $ (@{const HOL.disj} $ t1 $ t2))) =
@@ -553,7 +532,6 @@
(fn (prems, concl) => (prems, concl)))
-
(* iff-true *)
val iff_true_rule = @{lemma "P ==> P = True" by fast}
@@ -562,7 +540,6 @@
| iff_true ctxt thms t = replay_rule_error ctxt Z3_New_Proof.Iff_True thms t
-
(* iff-false *)
val iff_false_rule = @{lemma "~P ==> P = False" by fast}
@@ -571,13 +548,11 @@
| iff_false ctxt thms t = replay_rule_error ctxt Z3_New_Proof.Iff_False thms t
-
(* commutativity *)
fun comm ctxt _ t = match_instantiate ctxt t @{thm eq_commute}
-
(* definitional axioms *)
fun def_axiom_disj ctxt t =
@@ -592,20 +567,17 @@
("disj", def_axiom_disj ctxt)] []
-
(* application of definitions *)
fun apply_def _ [thm] _ = thm (* TODO: cover also the missing cases *)
| apply_def ctxt thms t = replay_rule_error ctxt Z3_New_Proof.Apply_Def thms t
-
(* iff-oeq *)
fun iff_oeq _ _ _ = raise Fail "iff_oeq" (* FIXME *)
-
(* negation normal form *)
fun nnf_prop ctxt thms t =
@@ -621,7 +593,6 @@
fun nnf_neg ctxt = nnf ctxt Z3_New_Proof.Nnf_Neg
-
(* theory lemmas *)
fun arith_th_lemma_tac ctxt prems =
@@ -642,7 +613,6 @@
| NONE => replay_error ctxt "Bad theory" (Z3_New_Proof.Th_Lemma name) thms)
-
(* mapping of rules to methods *)
fun unsupported rule ctxt = replay_error ctxt "Unsupported" rule
@@ -693,4 +663,4 @@
fun method_for rule = with_tracing rule (choose rule)
-end
+end;
--- a/src/HOL/Tools/SMT2/z3_new_replay_rules.ML Thu Jun 12 01:00:49 2014 +0200
+++ b/src/HOL/Tools/SMT2/z3_new_replay_rules.ML Thu Jun 12 01:00:49 2014 +0200
@@ -7,7 +7,7 @@
signature Z3_NEW_REPLAY_RULES =
sig
val apply: Proof.context -> cterm -> thm option
-end
+end;
structure Z3_New_Replay_Rules: Z3_NEW_REPLAY_RULES =
struct
@@ -51,4 +51,4 @@
val _ = Theory.setup (Attrib.setup name (Attrib.add_del add del) description #>
Global_Theory.add_thms_dynamic (name, Net.content o Data.get))
-end
+end;
--- a/src/HOL/Tools/SMT2/z3_new_replay_util.ML Thu Jun 12 01:00:49 2014 +0200
+++ b/src/HOL/Tools/SMT2/z3_new_replay_util.ML Thu Jun 12 01:00:49 2014 +0200
@@ -23,13 +23,11 @@
(*simpset*)
val add_simproc: Simplifier.simproc -> Context.generic -> Context.generic
val make_simpset: Proof.context -> thm list -> simpset
-end
+end;
structure Z3_New_Replay_Util: Z3_NEW_REPLAY_UTIL =
struct
-
-
(* theorem nets *)
fun thm_net_of f xthms =
@@ -59,7 +57,6 @@
end
-
(* proof combinators *)
fun under_assumption f ct =
@@ -68,7 +65,6 @@
fun discharge p pq = Thm.implies_elim pq p
-
(* a faster COMP *)
type compose_data = cterm list * (cterm -> cterm list) * thm
@@ -82,7 +78,6 @@
discharge thm (Thm.instantiate ([], cvs ~~ f (Thm.cprop_of thm)) rule)
-
(* simpset *)
local
@@ -152,4 +147,4 @@
end
-end
+end;
--- a/src/HOL/Word/Tools/smt2_word.ML Thu Jun 12 01:00:49 2014 +0200
+++ b/src/HOL/Word/Tools/smt2_word.ML Thu Jun 12 01:00:49 2014 +0200
@@ -9,12 +9,11 @@
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
+ if exists (Term.exists_type (Term.exists_subtype is_wordT)) ts then SOME "QF_AUFBV" else NONE
(* SMT-LIB builtins *)
@@ -141,4 +140,4 @@
SMTLIB2_Interface.add_logic (20, smtlib_logic) #>
setup_builtins))
-end
+end;