--- a/src/HOL/Tools/SMT2/smt2_setup_solvers.ML Thu Mar 13 13:18:13 2014 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,183 +0,0 @@
-(* Title: HOL/Tools/SMT2/smt2_setup_solvers.ML
- Author: Sascha Boehme, TU Muenchen
-
-Setup SMT solvers.
-*)
-
-signature SMT2_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_extensions: bool Config.T
-end
-
-structure SMT2_Setup_Solvers: SMT2_SETUP_SOLVERS =
-struct
-
-(* helper functions *)
-
-fun make_avail name () = getenv (name ^ "_SOLVER") <> ""
-
-fun make_command name () = [getenv (name ^ "_SOLVER")]
-
-fun outcome_of unsat sat unknown solver_name line =
- if String.isPrefix unsat line then SMT2_Solver.Unsat
- else if String.isPrefix sat line then SMT2_Solver.Sat
- else if String.isPrefix unknown line then SMT2_Solver.Unknown
- else raise SMT2_Failure.SMT (SMT2_Failure.Other_Failure ("Solver " ^
- quote solver_name ^ " failed. Enable SMT tracing by setting the " ^
- "configuration option " ^ quote (Config.name_of SMT2_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 SMT2_Config.random_seed),
- "-lang", "smtlib", "-output-lang", "presentation",
- "-timeout", string_of_int (Real.ceil (Config.get ctxt SMT2_Config.timeout))]
-in
-
-val cvc3: SMT2_Solver.solver_config = {
- name = "cvc3_new",
- class = K SMTLIB2_Interface.smtlib2C,
- avail = make_avail "CVC3_NEW",
- command = make_command "CVC3_NEW",
- options = cvc3_options,
- default_max_relevant = 400 (* FUDGE *),
- supports_filter = false,
- outcome =
- on_first_line (outcome_of "Unsatisfiable." "Satisfiable." "Unknown."),
- cex_parser = NONE,
- replay = NONE }
-
-end
-
-
-(* Yices *)
-
-val yices: SMT2_Solver.solver_config = {
- name = "yices_new",
- class = K SMTLIB2_Interface.smtlib2C,
- avail = make_avail "YICES_NEW",
- command = make_command "YICES_NEW",
- options = (fn ctxt => [
- "--rand-seed=" ^ string_of_int (Config.get ctxt SMT2_Config.random_seed),
- "--timeout=" ^
- string_of_int (Real.ceil (Config.get ctxt SMT2_Config.timeout)),
- "--smtlib"]),
- default_max_relevant = 350 (* FUDGE *),
- supports_filter = false,
- outcome = on_first_line (outcome_of "unsat" "sat" "unknown"),
- cex_parser = NONE,
- replay = 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 flag1 = Options.default_string @{option z3_non_commercial}
- val flag2 = getenv "Z3_NON_COMMERCIAL"
- in
- if accepted flag1 then Z3_Non_Commercial_Accepted
- else if declined flag1 then Z3_Non_Commercial_Declined
- else 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)."))))
-
-end
-
-val z3_extensions = Attrib.setup_config_bool @{binding z3_new_extensions} (K false)
-
-local
- fun z3_make_command name () = if_z3_non_commercial (make_command name)
-
- fun z3_options ctxt =
- ["REFINE_INJ_AXIOM=false" (* not supported by replay *),
- "-rs:" ^ string_of_int (Config.get ctxt SMT2_Config.random_seed),
- "-T:" ^ string_of_int (Real.ceil (Config.get ctxt SMT2_Config.timeout)),
- "-smt2"]
-
- 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 SMT2_Failure.SMT SMT2_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 SMT2_Failure.SMT _ => outcome (swap o split_last)
- end
-
- fun select_class ctxt =
- if Config.get ctxt z3_extensions then Z3_New_Interface.smtlib2_z3C
- else SMTLIB2_Interface.smtlib2C
-in
-
-val z3: SMT2_Solver.solver_config = {
- name = "z3_new",
- class = select_class,
- avail = make_avail "Z3_NEW",
- command = z3_make_command "Z3_NEW",
- options = z3_options,
- default_max_relevant = 350 (* FUDGE *),
- supports_filter = true,
- outcome = z3_on_first_or_last_line,
- cex_parser = SOME Z3_New_Model.parse_counterex,
- replay = SOME Z3_New_Proof_Replay.replay }
-
-end
-
-
-(* overall setup *)
-
-val _ = Theory.setup (
- SMT2_Solver.add_solver cvc3 #>
- SMT2_Solver.add_solver yices #>
- SMT2_Solver.add_solver z3)
-
-end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/SMT2/smt2_systems.ML Thu Mar 13 13:18:13 2014 +0100
@@ -0,0 +1,183 @@
+(* Title: HOL/Tools/SMT2/smt2_setup_solvers.ML
+ Author: Sascha Boehme, TU Muenchen
+
+Setup SMT solvers.
+*)
+
+signature SMT2_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_extensions: bool Config.T
+end
+
+structure SMT2_Setup_Solvers: SMT2_SETUP_SOLVERS =
+struct
+
+(* helper functions *)
+
+fun make_avail name () = getenv (name ^ "_SOLVER") <> ""
+
+fun make_command name () = [getenv (name ^ "_SOLVER")]
+
+fun outcome_of unsat sat unknown solver_name line =
+ if String.isPrefix unsat line then SMT2_Solver.Unsat
+ else if String.isPrefix sat line then SMT2_Solver.Sat
+ else if String.isPrefix unknown line then SMT2_Solver.Unknown
+ else raise SMT2_Failure.SMT (SMT2_Failure.Other_Failure ("Solver " ^
+ quote solver_name ^ " failed. Enable SMT tracing by setting the " ^
+ "configuration option " ^ quote (Config.name_of SMT2_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 SMT2_Config.random_seed),
+ "-lang", "smtlib", "-output-lang", "presentation",
+ "-timeout", string_of_int (Real.ceil (Config.get ctxt SMT2_Config.timeout))]
+in
+
+val cvc3: SMT2_Solver.solver_config = {
+ name = "cvc3_new",
+ class = K SMTLIB2_Interface.smtlib2C,
+ avail = make_avail "CVC3_NEW",
+ command = make_command "CVC3_NEW",
+ options = cvc3_options,
+ default_max_relevant = 400 (* FUDGE *),
+ supports_filter = false,
+ outcome =
+ on_first_line (outcome_of "Unsatisfiable." "Satisfiable." "Unknown."),
+ cex_parser = NONE,
+ replay = NONE }
+
+end
+
+
+(* Yices *)
+
+val yices: SMT2_Solver.solver_config = {
+ name = "yices_new",
+ class = K SMTLIB2_Interface.smtlib2C,
+ avail = make_avail "YICES_NEW",
+ command = make_command "YICES_NEW",
+ options = (fn ctxt => [
+ "--rand-seed=" ^ string_of_int (Config.get ctxt SMT2_Config.random_seed),
+ "--timeout=" ^
+ string_of_int (Real.ceil (Config.get ctxt SMT2_Config.timeout)),
+ "--smtlib"]),
+ default_max_relevant = 350 (* FUDGE *),
+ supports_filter = false,
+ outcome = on_first_line (outcome_of "unsat" "sat" "unknown"),
+ cex_parser = NONE,
+ replay = 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 flag1 = Options.default_string @{option z3_non_commercial}
+ val flag2 = getenv "Z3_NON_COMMERCIAL"
+ in
+ if accepted flag1 then Z3_Non_Commercial_Accepted
+ else if declined flag1 then Z3_Non_Commercial_Declined
+ else 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)."))))
+
+end
+
+val z3_extensions = Attrib.setup_config_bool @{binding z3_new_extensions} (K false)
+
+local
+ fun z3_make_command name () = if_z3_non_commercial (make_command name)
+
+ fun z3_options ctxt =
+ ["REFINE_INJ_AXIOM=false" (* not supported by replay *),
+ "-rs:" ^ string_of_int (Config.get ctxt SMT2_Config.random_seed),
+ "-T:" ^ string_of_int (Real.ceil (Config.get ctxt SMT2_Config.timeout)),
+ "-smt2"]
+
+ 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 SMT2_Failure.SMT SMT2_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 SMT2_Failure.SMT _ => outcome (swap o split_last)
+ end
+
+ fun select_class ctxt =
+ if Config.get ctxt z3_extensions then Z3_New_Interface.smtlib2_z3C
+ else SMTLIB2_Interface.smtlib2C
+in
+
+val z3: SMT2_Solver.solver_config = {
+ name = "z3_new",
+ class = select_class,
+ avail = make_avail "Z3_NEW",
+ command = z3_make_command "Z3_NEW",
+ options = z3_options,
+ default_max_relevant = 350 (* FUDGE *),
+ supports_filter = true,
+ outcome = z3_on_first_or_last_line,
+ cex_parser = SOME Z3_New_Model.parse_counterex,
+ replay = SOME Z3_New_Proof_Replay.replay }
+
+end
+
+
+(* overall setup *)
+
+val _ = Theory.setup (
+ SMT2_Solver.add_solver cvc3 #>
+ SMT2_Solver.add_solver yices #>
+ SMT2_Solver.add_solver z3)
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/SMT2/smt2_util.ML Thu Mar 13 13:18:13 2014 +0100
@@ -0,0 +1,224 @@
+(* Title: HOL/Tools/SMT2/smt2_utils.ML
+ Author: Sascha Boehme, TU Muenchen
+
+General utility functions.
+*)
+
+signature SMT2_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 certify: Proof.context -> term -> cterm
+ val typ_of: cterm -> typ
+ 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 SMT2_Utils: SMT2_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 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.cterm_of thy (Const (name, Sign.the_const_type thy name))
+ in (destT (Thm.ctyp_of_term 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 (cTs ~~ cUs, []) ct
+fun instT cU (cT, ct) = instTs [cU] ([cT], ct)
+fun instT' ct = instT (Thm.ctyp_of_term ct)
+
+
+(* certified terms *)
+
+fun certify ctxt = Thm.cterm_of (Proof_Context.theory_of ctxt)
+
+fun typ_of ct = #T (Thm.rep_cterm ct)
+
+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 @{theory} @{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 "=="} 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/Tools/SMT2/smt2_utils.ML Thu Mar 13 13:18:13 2014 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,224 +0,0 @@
-(* Title: HOL/Tools/SMT2/smt2_utils.ML
- Author: Sascha Boehme, TU Muenchen
-
-General utility functions.
-*)
-
-signature SMT2_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 certify: Proof.context -> term -> cterm
- val typ_of: cterm -> typ
- 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 SMT2_Utils: SMT2_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 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.cterm_of thy (Const (name, Sign.the_const_type thy name))
- in (destT (Thm.ctyp_of_term 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 (cTs ~~ cUs, []) ct
-fun instT cU (cT, ct) = instTs [cU] ([cT], ct)
-fun instT' ct = instT (Thm.ctyp_of_term ct)
-
-
-(* certified terms *)
-
-fun certify ctxt = Thm.cterm_of (Proof_Context.theory_of ctxt)
-
-fun typ_of ct = #T (Thm.rep_cterm ct)
-
-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 @{theory} @{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 "=="} 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/Tools/SMT2/z3_new_proof_literals.ML Thu Mar 13 13:18:13 2014 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,357 +0,0 @@
-(* Title: HOL/Tools/SMT2/z3_new_proof_literals.ML
- Author: Sascha Boehme, TU Muenchen
-
-Proof tools related to conjunctions and disjunctions.
-*)
-
-signature Z3_NEW_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 Z3_New_Proof_Literals: Z3_NEW_PROOF_LITERALS =
-struct
-
-
-
-(* literal table *)
-
-type littab = thm Termtab.table
-
-fun make_littab thms =
- fold (Termtab.update o `SMT2_Utils.prop_of) thms Termtab.empty
-
-fun insert_lit thm = Termtab.update (`SMT2_Utils.prop_of thm)
-fun delete_lit thm = Termtab.delete (SMT2_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 @{theory} @{const Not})
-
-
-
-(* proof tools *)
-
-(** explosion of conjunctions and disjunctions **)
-
-local
- val precomp = Z3_New_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 = Z3_New_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 Z3_New_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 (SMT2_Utils.prop_of thm) then cons thm
- else
- (case dest_rules (SMT2_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) (SMT2_Utils.prop_of thm)
- then explode1 (Z3_New_Proof_Tools.compose dest_rule thm)
- else cons (Z3_New_Proof_Tools.compose dest_rule thm)
-
- fun explode0 thm =
- if not is_conj andalso is_dneg (SMT2_Utils.prop_of thm)
- then [Z3_New_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 ([], [(cv1, on_cprop f thm1), (cv2, on_cprop g thm2)]) rule
- |> Z3_New_Proof_Tools.discharge thm1 |> Z3_New_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 = Z3_New_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 = Z3_New_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) =>
- (Z3_New_Proof_Tools.compose dnegI, lookup t)
- | @{const Not} $ (@{const HOL.eq (bool)} $ t $ (@{const Not} $ u)) =>
- (Z3_New_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 => (Z3_New_Proof_Tools.compose negIffE, as_negIff lookup t)
- | x => (Z3_New_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 (pairself 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 (SMT2_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)
- |> pairself (extract_lit thm)
- |> (fn (nlit, plit) => nlit COMP (plit COMP contra_rule)))
- end
-
- val falseE_v = 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 (Z3_New_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 = Z3_New_Proof_Tools.under_assumption (prove r cr o make_tab l) cl
- val thm2 = Z3_New_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/Tools/SMT2/z3_new_proof_methods.ML Thu Mar 13 13:18:13 2014 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,667 +0,0 @@
-(* Title: HOL/Tools/SMT2/z3_new_proof.ML
- Author: Sascha Boehme, TU Muenchen
- Author: Jasmin Blanchette, TU Muenchen
-
-Proof methods for replaying Z3 proofs.
-*)
-
-signature Z3_NEW_PROOF_METHODS =
-sig
- (*abstraction*)
- type abs_context = int * term Termtab.table
- type 'a abstracter = term -> abs_context -> 'a * abs_context
- val add_arith_abstracter: (term abstracter -> term option abstracter) ->
- Context.generic -> Context.generic
-
- (*theory lemma methods*)
- type th_lemma_method = Proof.context -> thm list -> term -> thm
- val add_th_lemma_method: string * th_lemma_method -> Context.generic ->
- Context.generic
-
- (*methods for Z3 proof rules*)
- type z3_method = Proof.context -> thm list -> term -> thm
- val true_axiom: z3_method
- val mp: z3_method
- val refl: z3_method
- val symm: z3_method
- val trans: z3_method
- val cong: z3_method
- val quant_intro: z3_method
- val distrib: z3_method
- val and_elim: z3_method
- val not_or_elim: z3_method
- val rewrite: z3_method
- val rewrite_star: z3_method
- val pull_quant: z3_method
- val push_quant: z3_method
- val elim_unused: z3_method
- val dest_eq_res: z3_method
- val quant_inst: z3_method
- val lemma: z3_method
- val unit_res: z3_method
- val iff_true: z3_method
- val iff_false: z3_method
- val comm: z3_method
- val def_axiom: z3_method
- val apply_def: z3_method
- val iff_oeq: z3_method
- val nnf_pos: z3_method
- val nnf_neg: z3_method
- val mp_oeq: z3_method
- val th_lemma: string -> z3_method
- val is_assumption: Z3_New_Proof.z3_rule -> bool
- val method_for: Z3_New_Proof.z3_rule -> z3_method
-end
-
-structure Z3_New_Proof_Methods: Z3_NEW_PROOF_METHODS =
-struct
-
-type z3_method = Proof.context -> thm list -> term -> thm
-
-
-
-(* utility functions *)
-
-val trace = SMT2_Config.trace_msg
-
-fun pretty_thm ctxt thm = Syntax.pretty_term ctxt (Thm.concl_of thm)
-
-fun pretty_goal ctxt msg rule thms t =
- let
- val full_msg = msg ^ ": " ^ quote (Z3_New_Proof.string_of_rule rule)
- val assms =
- if null thms then []
- else [Pretty.big_list "assumptions:" (map (pretty_thm ctxt) thms)]
- val concl = Pretty.big_list "proposition:" [Syntax.pretty_term ctxt t]
- in Pretty.big_list full_msg (assms @ [concl]) end
-
-fun replay_error ctxt msg rule thms t = error (Pretty.string_of (pretty_goal ctxt msg rule thms t))
-
-fun replay_rule_error ctxt = replay_error ctxt "Failed to replay Z3 proof step"
-
-fun trace_goal ctxt rule thms t =
- trace ctxt (fn () => Pretty.string_of (pretty_goal ctxt "Goal" rule thms t))
-
-fun as_prop (t as Const (@{const_name Trueprop}, _) $ _) = t
- | as_prop t = HOLogic.mk_Trueprop t
-
-fun dest_prop (Const (@{const_name Trueprop}, _) $ t) = t
- | dest_prop t = t
-
-fun dest_thm thm = dest_prop (Thm.concl_of thm)
-
-fun certify_prop ctxt t = SMT2_Utils.certify ctxt (as_prop t)
-
-fun try_provers ctxt rule [] thms t = replay_rule_error ctxt rule thms t
- | try_provers ctxt rule ((name, prover) :: named_provers) thms t =
- (case (trace ctxt (K ("Trying prover " ^ quote name)); try prover t) of
- SOME thm => thm
- | NONE => try_provers ctxt rule named_provers thms t)
-
-fun match ctxt pat t =
- (Vartab.empty, Vartab.empty)
- |> Pattern.first_order_match (Proof_Context.theory_of ctxt) (pat, t)
-
-fun gen_certify_inst sel mk cert ctxt thm t =
- let
- val inst = match ctxt (dest_thm thm) (dest_prop t)
- fun cert_inst (ix, (a, b)) = (cert (mk (ix, a)), cert b)
- in Vartab.fold (cons o cert_inst) (sel inst) [] end
-
-fun match_instantiateT ctxt t thm =
- if Term.exists_type (Term.exists_subtype Term.is_TVar) (dest_thm thm) then
- let val certT = Thm.ctyp_of (Proof_Context.theory_of ctxt)
- in Thm.instantiate (gen_certify_inst fst TVar certT ctxt thm t, []) thm end
- else thm
-
-fun match_instantiate ctxt t thm =
- let
- val cert = SMT2_Utils.certify ctxt
- val thm' = match_instantiateT ctxt t thm
- in Thm.instantiate ([], gen_certify_inst snd Var cert ctxt thm' t) thm' end
-
-fun apply_rule ctxt t =
- (case Z3_New_Proof_Rules.apply ctxt (certify_prop ctxt t) of
- SOME thm => thm
- | NONE => raise Fail "apply_rule")
-
-fun discharge _ [] thm = thm
- | discharge i (rule :: rules) thm = discharge (i + Thm.nprems_of rule) rules (rule RSN (i, thm))
-
-fun by_tac ctxt thms ns ts t tac =
- Goal.prove ctxt [] (map as_prop ts) (as_prop t)
- (fn {context, prems} => HEADGOAL (tac context prems))
- |> Drule.generalize ([], ns)
- |> discharge 1 thms
-
-fun prove ctxt t tac = by_tac ctxt [] [] [] t (K o tac)
-
-fun prop_tac ctxt prems =
- Method.insert_tac prems THEN' (Classical.fast_tac ctxt ORELSE' Clasimp.force_tac ctxt)
-
-fun quant_tac ctxt = Blast.blast_tac ctxt
-
-
-
-(* plug-ins *)
-
-type abs_context = int * term Termtab.table
-
-type 'a abstracter = term -> abs_context -> 'a * abs_context
-
-type th_lemma_method = Proof.context -> thm list -> term -> thm
-
-fun id_ord ((id1, _), (id2, _)) = int_ord (id1, id2)
-
-structure Plugins = Generic_Data
-(
- type T =
- (int * (term abstracter -> term option abstracter)) list *
- th_lemma_method Symtab.table
- val empty = ([], Symtab.empty)
- val extend = I
- fun merge ((abss1, ths1), (abss2, ths2)) = (
- Ord_List.merge id_ord (abss1, abss2),
- Symtab.merge (K true) (ths1, ths2))
-)
-
-fun add_arith_abstracter abs = Plugins.map (apfst (Ord_List.insert id_ord (serial (), abs)))
-fun get_arith_abstracters ctxt = map snd (fst (Plugins.get (Context.Proof ctxt)))
-
-fun add_th_lemma_method method = Plugins.map (apsnd (Symtab.update_new method))
-fun get_th_lemma_method ctxt = snd (Plugins.get (Context.Proof ctxt))
-
-
-
-(* abstraction *)
-
-fun prove_abstract ctxt thms t tac f =
- let
- val ((prems, concl), (_, ts)) = f (1, Termtab.empty)
- val ns = Termtab.fold (fn (_, v) => cons (fst (Term.dest_Free v))) ts []
- in
- by_tac ctxt [] ns prems concl tac
- |> match_instantiate ctxt t
- |> discharge 1 thms
- end
-
-fun prove_abstract' ctxt t tac f =
- prove_abstract ctxt [] t tac (f #>> pair [])
-
-fun lookup_term (_, terms) t = Termtab.lookup terms t
-
-fun abstract_sub t f cx =
- (case lookup_term cx t of
- SOME v => (v, cx)
- | NONE => f cx)
-
-fun mk_fresh_free t (i, terms) =
- let val v = Free ("t" ^ string_of_int i, fastype_of t)
- in (v, (i + 1, Termtab.update (t, v) terms)) end
-
-fun apply_abstracters _ [] _ cx = (NONE, cx)
- | apply_abstracters abs (abstracter :: abstracters) t cx =
- (case abstracter abs t cx of
- (NONE, _) => apply_abstracters abs abstracters t cx
- | x as (SOME _, _) => x)
-
-fun abstract_term (t as _ $ _) = abstract_sub t (mk_fresh_free t)
- | abstract_term (t as Abs _) = abstract_sub t (mk_fresh_free t)
- | abstract_term t = pair t
-
-fun abstract_bin abs f t t1 t2 = abstract_sub t (abs t1 ##>> abs t2 #>> f)
-
-fun abstract_ter abs f t t1 t2 t3 =
- abstract_sub t (abs t1 ##>> abs t2 ##>> abs t3 #>> (Parse.triple1 #> f))
-
-fun abstract_lit (@{const HOL.Not} $ t) = abstract_term t #>> HOLogic.mk_not
- | abstract_lit t = abstract_term t
-
-fun abstract_not abs (t as @{const HOL.Not} $ t1) =
- abstract_sub t (abs t1 #>> HOLogic.mk_not)
- | abstract_not _ t = abstract_lit t
-
-fun abstract_conj (t as @{const HOL.conj} $ t1 $ t2) =
- abstract_bin abstract_conj HOLogic.mk_conj t t1 t2
- | abstract_conj t = abstract_lit t
-
-fun abstract_disj (t as @{const HOL.disj} $ t1 $ t2) =
- abstract_bin abstract_disj HOLogic.mk_disj t t1 t2
- | abstract_disj t = abstract_lit t
-
-fun abstract_prop (t as (c as @{const If (bool)}) $ t1 $ t2 $ t3) =
- abstract_ter abstract_prop (fn (t1, t2, t3) => c $ t1 $ t2 $ t3) t t1 t2 t3
- | abstract_prop (t as @{const HOL.disj} $ t1 $ t2) =
- abstract_bin abstract_prop HOLogic.mk_disj t t1 t2
- | abstract_prop (t as @{const HOL.conj} $ t1 $ t2) =
- abstract_bin abstract_prop HOLogic.mk_conj t t1 t2
- | abstract_prop (t as @{const HOL.implies} $ t1 $ t2) =
- abstract_bin abstract_prop HOLogic.mk_imp t t1 t2
- | abstract_prop (t as @{term "HOL.eq :: bool => _"} $ t1 $ t2) =
- abstract_bin abstract_prop HOLogic.mk_eq t t1 t2
- | abstract_prop t = abstract_not abstract_prop t
-
-fun abstract_arith ctxt u =
- let
- fun abs (t as (c as Const _) $ Abs (s, T, t')) =
- abstract_sub t (abs t' #>> (fn u' => c $ Abs (s, T, u')))
- | abs (t as (c as Const (@{const_name If}, _)) $ t1 $ t2 $ t3) =
- abstract_ter abs (fn (t1, t2, t3) => c $ t1 $ t2 $ t3) t t1 t2 t3
- | abs (t as @{const HOL.Not} $ t1) = abstract_sub t (abs t1 #>> HOLogic.mk_not)
- | abs (t as @{const HOL.disj} $ t1 $ t2) =
- abstract_sub t (abs t1 ##>> abs t2 #>> HOLogic.mk_disj)
- | abs (t as (c as Const (@{const_name uminus_class.uminus}, _)) $ t1) =
- abstract_sub t (abs t1 #>> (fn u => c $ u))
- | abs (t as (c as Const (@{const_name plus_class.plus}, _)) $ t1 $ t2) =
- abstract_sub t (abs t1 ##>> abs t2 #>> (fn (u1, u2) => c $ u1 $ u2))
- | abs (t as (c as Const (@{const_name minus_class.minus}, _)) $ t1 $ t2) =
- abstract_sub t (abs t1 ##>> abs t2 #>> (fn (u1, u2) => c $ u1 $ u2))
- | abs (t as (c as Const (@{const_name times_class.times}, _)) $ t1 $ t2) =
- abstract_sub t (abs t1 ##>> abs t2 #>> (fn (u1, u2) => c $ u1 $ u2))
- | abs (t as (c as Const (@{const_name z3div}, _)) $ t1 $ t2) =
- abstract_sub t (abs t1 ##>> abs t2 #>> (fn (u1, u2) => c $ u1 $ u2))
- | abs (t as (c as Const (@{const_name z3mod}, _)) $ t1 $ t2) =
- abstract_sub t (abs t1 ##>> abs t2 #>> (fn (u1, u2) => c $ u1 $ u2))
- | abs (t as (c as Const (@{const_name HOL.eq}, _)) $ t1 $ t2) =
- abstract_sub t (abs t1 ##>> abs t2 #>> (fn (u1, u2) => c $ u1 $ u2))
- | abs (t as (c as Const (@{const_name ord_class.less}, _)) $ t1 $ t2) =
- abstract_sub t (abs t1 ##>> abs t2 #>> (fn (u1, u2) => c $ u1 $ u2))
- | abs (t as (c as Const (@{const_name ord_class.less_eq}, _)) $ t1 $ t2) =
- abstract_sub t (abs t1 ##>> abs t2 #>> (fn (u1, u2) => c $ u1 $ u2))
- | abs t = abstract_sub t (fn cx =>
- if can HOLogic.dest_number t then (t, cx)
- else
- (case apply_abstracters abs (get_arith_abstracters ctxt) t cx of
- (SOME u, cx') => (u, cx')
- | (NONE, _) => abstract_term t cx))
- in abs u end
-
-
-
-(* truth axiom *)
-
-fun true_axiom _ _ _ = @{thm TrueI}
-
-
-
-(* modus ponens *)
-
-fun mp _ [p, p_eq_q] _ = discharge 1 [p_eq_q, p] iffD1
- | mp ctxt thms t = replay_rule_error ctxt Z3_New_Proof.Modus_Ponens thms t
-
-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 |> (
- resolve_tac (@{thm refl} :: prems) i
- ORELSE (cong_tac i THEN ctac prems (i + 1) THEN ctac prems i))
-
-fun cong_basic ctxt thms t =
- let val st = Thm.trivial (certify_prop ctxt t)
- in
- (case Seq.pull (ctac thms 1 st) of
- SOME (thm, _) => thm
- | NONE => raise THM ("cong", 0, thms @ [st]))
- end
-
-val cong_dest_rules = @{lemma
- "(~ P | Q) & (P | ~ Q) ==> P = Q"
- "(P | ~ Q) & (~ P | Q) ==> P = Q"
- by fast+}
-
-fun cong_full ctxt thms t = prove ctxt t (fn ctxt' =>
- Method.insert_tac thms
- THEN' (Classical.fast_tac ctxt'
- ORELSE' dresolve_tac cong_dest_rules
- THEN' Classical.fast_tac ctxt'))
-
-fun cong ctxt thms = try_provers ctxt Z3_New_Proof.Monotonicity [
- ("basic", cong_basic ctxt thms),
- ("full", cong_full ctxt thms)] thms
-
-
-
-(* quantifier introduction *)
-
-val quant_intro_rules = @{lemma
- "(!!x. P x = Q x) ==> (ALL x. P x) = (ALL x. Q x)"
- "(!!x. P x = Q x) ==> (EX x. P x) = (EX x. Q x)"
- "(!!x. (~ P x) = Q x) ==> (~ (EX x. P x)) = (ALL x. Q x)"
- "(!!x. (~ P x) = Q x) ==> (~ (ALL x. P x)) = (EX x. Q x)"
- by fast+}
-
-fun quant_intro ctxt [thm] t =
- prove ctxt t (K (REPEAT_ALL_NEW (resolve_tac (thm :: quant_intro_rules))))
- | 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 *)
-fun distrib ctxt _ t =
- prove_abstract' ctxt t prop_tac (abstract_prop (dest_prop t))
-
-
-
-(* elimination of conjunctions *)
-
-fun and_elim ctxt [thm] t =
- prove_abstract ctxt [thm] t prop_tac (
- abstract_lit (dest_prop t) ##>>
- abstract_conj (dest_thm thm) #>>
- apfst single o swap)
- | 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 =
- prove_abstract ctxt [thm] t prop_tac (
- abstract_lit (dest_prop t) ##>>
- abstract_not abstract_disj (dest_thm thm) #>>
- apfst single o swap)
- | not_or_elim ctxt thms t =
- replay_rule_error ctxt Z3_New_Proof.Not_Or_Elim thms t
-
-
-
-(* rewriting *)
-
-fun abstract_eq f1 f2 (Const (@{const_name HOL.eq}, _) $ t1 $ t2) =
- f1 t1 ##>> f2 t2 #>> HOLogic.mk_eq
- | abstract_eq _ _ t = abstract_term t
-
-fun prove_prop_rewrite ctxt t =
- prove_abstract' ctxt t prop_tac (
- abstract_eq abstract_prop abstract_prop (dest_prop t))
-
-fun arith_rewrite_tac ctxt _ =
- TRY o Simplifier.simp_tac ctxt
- THEN_ALL_NEW (Arith_Data.arith_tac ctxt ORELSE' Clasimp.force_tac ctxt)
-
-fun prove_arith_rewrite ctxt t =
- prove_abstract' ctxt t arith_rewrite_tac (
- abstract_eq (abstract_arith ctxt) (abstract_arith ctxt) (dest_prop t))
-
-fun rewrite ctxt _ = try_provers ctxt Z3_New_Proof.Rewrite [
- ("rules", apply_rule ctxt),
- ("prop_rewrite", prove_prop_rewrite ctxt),
- ("arith_rewrite", prove_arith_rewrite ctxt)] []
-
-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}
-val elim_ex = @{lemma "P = Q ==> (EX x. P) = Q" by fast}
-
-fun elim_unused_tac i st = (
- match_tac [@{thm refl}]
- ORELSE' (match_tac [elim_all, elim_ex] THEN' elim_unused_tac)
- ORELSE' (
- match_tac [@{thm iff_allI}, @{thm iff_exI}]
- THEN' elim_unused_tac)) i st
-
-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}
-
-fun quant_inst ctxt _ t = prove ctxt t (fn _ =>
- REPEAT_ALL_NEW (rtac quant_inst_rule)
- THEN' rtac @{thm excluded_middle})
-
-
-
-(* propositional lemma *)
-
-exception LEMMA of unit
-
-val intro_hyp_rule1 = @{lemma "(~P ==> Q) ==> P | Q" by fast}
-val intro_hyp_rule2 = @{lemma "(P ==> Q) ==> ~P | Q" by fast}
-
-fun norm_lemma thm =
- (thm COMP_INCR intro_hyp_rule1)
- handle THM _ => thm COMP_INCR intro_hyp_rule2
-
-fun negated_prop (@{const HOL.Not} $ t) = HOLogic.mk_Trueprop t
- | negated_prop t = HOLogic.mk_Trueprop (HOLogic.mk_not t)
-
-fun intro_hyps tab (t as @{const HOL.disj} $ t1 $ t2) cx =
- lookup_intro_hyps tab t (fold (intro_hyps tab) [t1, t2]) cx
- | intro_hyps tab t cx =
- lookup_intro_hyps tab t (fn _ => raise LEMMA ()) cx
-
-and lookup_intro_hyps tab t f (cx as (thm, terms)) =
- (case Termtab.lookup tab (negated_prop t) of
- NONE => f cx
- | SOME hyp => (norm_lemma (Thm.implies_intr hyp thm), t :: terms))
-
-fun lemma ctxt (thms as [thm]) t =
- (let
- val tab = Termtab.make (map (`Thm.term_of) (#hyps (Thm.crep_thm thm)))
- val (thm', terms) = intro_hyps tab (dest_prop t) (thm, [])
- in
- prove_abstract ctxt [thm'] t prop_tac (
- fold (snd oo abstract_lit) terms #>
- abstract_disj (dest_thm thm') #>> single ##>>
- abstract_disj (dest_prop t))
- end
- handle LEMMA () => replay_error ctxt "Bad proof state" Z3_New_Proof.Lemma thms t)
- | 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))) =
- abstract_sub t (abstract_unit t1 ##>> abstract_unit t2 #>>
- HOLogic.mk_not o HOLogic.mk_disj)
- | abstract_unit (t as (@{const HOL.disj} $ t1 $ t2)) =
- abstract_sub t (abstract_unit t1 ##>> abstract_unit t2 #>>
- HOLogic.mk_disj)
- | abstract_unit t = abstract_lit t
-
-fun unit_res ctxt thms t =
- prove_abstract ctxt thms t prop_tac (
- fold_map (abstract_unit o dest_thm) thms ##>>
- abstract_unit (dest_prop t) #>>
- (fn (prems, concl) => (prems, concl)))
-
-
-
-(* iff-true *)
-
-val iff_true_rule = @{lemma "P ==> P = True" by fast}
-
-fun iff_true _ [thm] _ = thm RS iff_true_rule
- | 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}
-
-fun iff_false _ [thm] _ = thm RS iff_false_rule
- | 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 =
- (case dest_prop t of
- @{const HOL.disj} $ u1 $ u2 =>
- prove_abstract' ctxt t prop_tac (
- abstract_prop u2 ##>> abstract_prop u1 #>> HOLogic.mk_disj o swap)
- | u => prove_abstract' ctxt t prop_tac (abstract_prop u))
-
-fun def_axiom ctxt _ = try_provers ctxt Z3_New_Proof.Def_Axiom [
- ("rules", apply_rule ctxt),
- ("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 =
- prove_abstract ctxt thms t prop_tac (
- fold_map (abstract_prop o dest_thm) thms ##>>
- abstract_prop (dest_prop t))
-
-fun nnf ctxt rule thms = try_provers ctxt rule [
- ("prop", nnf_prop ctxt thms),
- ("quant", quant_intro ctxt [hd thms])] thms
-
-fun nnf_pos ctxt = nnf ctxt Z3_New_Proof.Nnf_Pos
-fun nnf_neg ctxt = nnf ctxt Z3_New_Proof.Nnf_Neg
-
-
-
-(* theory lemmas *)
-
-fun arith_th_lemma_tac ctxt prems =
- Method.insert_tac prems
- THEN' SELECT_GOAL (Local_Defs.unfold_tac ctxt @{thms z3div_def z3mod_def})
- THEN' Arith_Data.arith_tac ctxt
-
-fun arith_th_lemma ctxt thms t =
- prove_abstract ctxt thms t arith_th_lemma_tac (
- fold_map (abstract_arith ctxt o dest_thm) thms ##>>
- abstract_arith ctxt (dest_prop t))
-
-val _ = Theory.setup (Context.theory_map (add_th_lemma_method ("arith", arith_th_lemma)))
-
-fun th_lemma name ctxt thms =
- (case Symtab.lookup (get_th_lemma_method ctxt) name of
- SOME method => method ctxt thms
- | NONE => replay_error ctxt "Bad theory" (Z3_New_Proof.Th_Lemma name) thms)
-
-
-
-(* mapping of rules to methods *)
-
-fun is_assumption Z3_New_Proof.Asserted = true
- | is_assumption Z3_New_Proof.Goal = true
- | is_assumption Z3_New_Proof.Hypothesis = true
- | is_assumption Z3_New_Proof.Intro_Def = true
- | is_assumption Z3_New_Proof.Skolemize = true
- | is_assumption _ = false
-
-fun unsupported rule ctxt = replay_error ctxt "Unsupported" rule
-fun assumed rule ctxt = replay_error ctxt "Assumed" rule
-
-fun choose Z3_New_Proof.True_Axiom = true_axiom
- | choose (r as Z3_New_Proof.Asserted) = assumed r
- | choose (r as Z3_New_Proof.Goal) = assumed r
- | choose Z3_New_Proof.Modus_Ponens = mp
- | choose Z3_New_Proof.Reflexivity = refl
- | choose Z3_New_Proof.Symmetry = symm
- | choose Z3_New_Proof.Transitivity = trans
- | choose (r as Z3_New_Proof.Transitivity_Star) = unsupported r
- | choose Z3_New_Proof.Monotonicity = cong
- | choose Z3_New_Proof.Quant_Intro = quant_intro
- | choose Z3_New_Proof.Distributivity = distrib
- | choose Z3_New_Proof.And_Elim = and_elim
- | choose Z3_New_Proof.Not_Or_Elim = not_or_elim
- | choose Z3_New_Proof.Rewrite = rewrite
- | choose Z3_New_Proof.Rewrite_Star = rewrite_star
- | choose Z3_New_Proof.Pull_Quant = pull_quant
- | choose (r as Z3_New_Proof.Pull_Quant_Star) = unsupported r
- | choose Z3_New_Proof.Push_Quant = push_quant
- | choose Z3_New_Proof.Elim_Unused_Vars = elim_unused
- | choose Z3_New_Proof.Dest_Eq_Res = dest_eq_res
- | choose Z3_New_Proof.Quant_Inst = quant_inst
- | choose (r as Z3_New_Proof.Hypothesis) = assumed r
- | choose Z3_New_Proof.Lemma = lemma
- | choose Z3_New_Proof.Unit_Resolution = unit_res
- | choose Z3_New_Proof.Iff_True = iff_true
- | choose Z3_New_Proof.Iff_False = iff_false
- | choose Z3_New_Proof.Commutativity = comm
- | choose Z3_New_Proof.Def_Axiom = def_axiom
- | choose (r as Z3_New_Proof.Intro_Def) = assumed r
- | choose Z3_New_Proof.Apply_Def = apply_def
- | choose Z3_New_Proof.Iff_Oeq = iff_oeq
- | choose Z3_New_Proof.Nnf_Pos = nnf_pos
- | choose Z3_New_Proof.Nnf_Neg = nnf_neg
- | choose (r as Z3_New_Proof.Nnf_Star) = unsupported r
- | choose (r as Z3_New_Proof.Cnf_Star) = unsupported r
- | choose (r as Z3_New_Proof.Skolemize) = assumed r
- | choose Z3_New_Proof.Modus_Ponens_Oeq = mp_oeq
- | choose (Z3_New_Proof.Th_Lemma name) = th_lemma name
-
-fun with_tracing rule method ctxt thms t =
- let val _ = trace_goal ctxt rule thms t
- in method ctxt thms t end
-
-fun method_for rule = with_tracing rule (choose rule)
-
-end
--- a/src/HOL/Tools/SMT2/z3_new_proof_replay.ML Thu Mar 13 13:18:13 2014 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,193 +0,0 @@
-(* Title: HOL/Tools/SMT2/z3_new_proof_replay.ML
- Author: Sascha Boehme, TU Muenchen
- Author: Jasmin Blanchette, TU Muenchen
-
-Z3 proof replay.
-*)
-
-signature Z3_NEW_PROOF_REPLAY =
-sig
- val replay: Proof.context -> SMT2_Translate.replay_data -> string list ->
- (int list * Z3_New_Proof.z3_step list) * thm
-end
-
-structure Z3_New_Proof_Replay: Z3_NEW_PROOF_REPLAY =
-struct
-
-fun params_of t = Term.strip_qnt_vars @{const_name all} t
-
-fun varify ctxt thm =
- let
- val maxidx = Thm.maxidx_of thm + 1
- val vs = params_of (Thm.prop_of thm)
- val vars = map_index (fn (i, (n, T)) => Var ((n, i + maxidx), T)) vs
- in Drule.forall_elim_list (map (SMT2_Utils.certify ctxt) vars) thm end
-
-fun add_paramTs names t =
- fold2 (fn n => fn (_, T) => AList.update (op =) (n, T)) names (params_of t)
-
-fun new_fixes ctxt nTs =
- let
- val (ns, ctxt') = Variable.variant_fixes (replicate (length nTs) "") ctxt
- fun mk (n, T) n' = (n, SMT2_Utils.certify ctxt' (Free (n', T)))
- in (ctxt', Symtab.make (map2 mk nTs ns)) end
-
-fun forall_elim_term ct (Const (@{const_name all}, _) $ (a as Abs _)) =
- Term.betapply (a, Thm.term_of ct)
- | forall_elim_term _ qt = raise TERM ("forall_elim'", [qt])
-
-fun apply_fixes elim env = fold (elim o the o Symtab.lookup env)
-
-val apply_fixes_prem = uncurry o apply_fixes Thm.forall_elim
-val apply_fixes_concl = apply_fixes forall_elim_term
-
-fun export_fixes env names = Drule.forall_intr_list (map (the o Symtab.lookup env) names)
-
-fun under_fixes f ctxt (prems, nthms) names concl =
- let
- val thms1 = map (varify ctxt) prems
- val (ctxt', env) =
- add_paramTs names concl []
- |> fold (uncurry add_paramTs o apsnd Thm.prop_of) nthms
- |> new_fixes ctxt
- val thms2 = map (apply_fixes_prem env) nthms
- val t = apply_fixes_concl env names concl
- in export_fixes env names (f ctxt' (thms1 @ thms2) t) end
-
-fun replay_thm ctxt assumed nthms
- (Z3_New_Proof.Z3_Step {id, rule, concl, fixes, is_fix_step, ...}) =
- if Z3_New_Proof_Methods.is_assumption rule then
- (case Inttab.lookup assumed id of
- SOME (_, thm) => thm
- | NONE => Thm.assume (SMT2_Utils.certify ctxt concl))
- else
- under_fixes (Z3_New_Proof_Methods.method_for rule) ctxt
- (if is_fix_step then (map snd nthms, []) else ([], nthms)) fixes concl
-
-fun replay_step ctxt assumed (step as Z3_New_Proof.Z3_Step {id, prems, fixes, ...}) proofs =
- let val nthms = map (the o Inttab.lookup proofs) prems
- in Inttab.update (id, (fixes, replay_thm ctxt assumed nthms step)) proofs end
-
-local
- val remove_trigger = mk_meta_eq @{thm SMT2.trigger_def}
- val remove_weight = mk_meta_eq @{thm SMT2.weight_def}
- val remove_fun_app = mk_meta_eq @{thm SMT2.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, Z3_New_Proof_Literals.rewrite_true]
-
- fun rewrite _ [] = I
- | rewrite ctxt eqs = Conv.fconv_rule (rewrite_conv ctxt eqs)
-
- fun lookup_assm assms_net ct =
- Z3_New_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 steps ctxt =
- let
- val eqs = map (rewrite ctxt [Z3_New_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))
- |> Z3_New_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' RS thm, ctxt') end
-
- fun add1 id fixes 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 (id, (fixes, thm)) ptab))
- end
-
- fun add (Z3_New_Proof.Z3_Step {id, rule, concl, fixes, ...})
- (cx as ((is, thms), (ctxt, ptab))) =
- if Z3_New_Proof_Methods.is_assumption rule andalso rule <> Z3_New_Proof.Hypothesis then
- let
- val ct = SMT2_Utils.certify ctxt concl
- val thm1 =
- Thm.trivial ct
- |> Conv.fconv_rule (Conv.arg1_conv (revert_conv outer_ctxt))
- val thm2 = singleton (Variable.export ctxt outer_ctxt) thm1
- in
- (case lookup_assm assms_net (Thm.cprem_of thm2 1) of
- [] =>
- let val (thm, ctxt') = assume thm1 ctxt
- in ((is, thms), (ctxt', Inttab.update (id, (fixes, thm)) ptab)) end
- | ithms => fold (add1 id fixes thm1) ithms cx)
- end
- else
- cx
- in fold add steps (([], []), (ctxt, Inttab.empty)) end
-
-end
-
-(* |- (EX x. P x) = P c |- ~ (ALL x. P x) = ~ P c *)
-local
- val sk_rules = @{lemma
- "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 discharge_sk_tac i st =
- (rtac @{thm trans} i
- THEN resolve_tac sk_rules i
- THEN (rtac @{thm refl} ORELSE' discharge_sk_tac) (i+1)
- THEN rtac @{thm refl} i) st
-
-end
-
-fun make_discharge_rules rules = rules @ [@{thm allI}, @{thm refl},
- @{thm reflexive}, Z3_New_Proof_Literals.true_thm]
-
-val intro_def_rules = @{lemma
- "(~ P | P) & (P | ~ P)"
- "(P | ~ P) & (~ P | P)"
- by fast+}
-
-fun discharge_assms_tac rules =
- REPEAT (HEADGOAL (resolve_tac (intro_def_rules @ rules) ORELSE' SOLVED' discharge_sk_tac))
-
-fun discharge_assms ctxt rules thm =
- (if Thm.nprems_of thm = 0 then
- thm
- else
- (case Seq.pull (discharge_assms_tac rules thm) of
- SOME (thm', _) => thm'
- | NONE => raise THM ("failed to discharge premise", 1, [thm])))
- |> Goal.norm_result ctxt
-
-fun discharge rules outer_ctxt inner_ctxt =
- singleton (Proof_Context.export inner_ctxt outer_ctxt)
- #> discharge_assms outer_ctxt (make_discharge_rules rules)
-
-fun replay outer_ctxt
- ({context=ctxt, typs, terms, rewrite_rules, assms} : SMT2_Translate.replay_data) output =
- let
- val (steps, ctxt1) = Z3_New_Proof.parse typs terms output ctxt
- val ctxt2 = put_simpset (Z3_New_Proof_Tools.make_simpset ctxt1 []) ctxt1
- val ((is, rules), (ctxt3, assumed)) = add_asserted outer_ctxt rewrite_rules assms steps ctxt2
- val proofs = fold (replay_step ctxt3 assumed) steps assumed
- val (_, Z3_New_Proof.Z3_Step {id, ...}) = split_last steps
- in
- if Config.get ctxt3 SMT2_Config.filter_only_facts then ((is, steps), TrueI)
- else (([], steps), Inttab.lookup proofs id |> the |> snd |> discharge rules outer_ctxt ctxt3)
- end
-
-end
--- a/src/HOL/Tools/SMT2/z3_new_proof_rules.ML Thu Mar 13 13:18:13 2014 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,56 +0,0 @@
-(* Title: HOL/Tools/SMT2/z3_new_proof_rules.ML
- Author: Sascha Boehme, TU Muenchen
-
-Custom rules for Z3 proof replay.
-*)
-
-signature Z3_NEW_PROOF_RULES =
-sig
- val apply: Proof.context -> cterm -> thm option
-end
-
-structure Z3_New_Proof_Rules: Z3_NEW_PROOF_RULES =
-struct
-
-val eq = Thm.eq_thm
-
-structure Data = Generic_Data
-(
- type T = thm Net.net
- val empty = Net.empty
- val extend = I
- val merge = Net.merge eq
-)
-
-fun maybe_instantiate ct thm =
- try Thm.first_order_match (Thm.cprop_of thm, ct)
- |> Option.map (fn inst => Thm.instantiate inst thm)
-
-fun apply ctxt ct =
- let
- val net = Data.get (Context.Proof ctxt)
- val xthms = Net.match_term net (Thm.term_of ct)
-
- fun select ct = map_filter (maybe_instantiate ct) xthms
- fun select' ct =
- let val thm = Thm.trivial ct
- in map_filter (try (fn rule => rule COMP thm)) xthms end
-
- in try hd (case select ct of [] => select' ct | xthms' => xthms') end
-
-val prep = `Thm.prop_of
-
-fun ins thm net = Net.insert_term eq (prep thm) net handle Net.INSERT => net
-fun del thm net = Net.delete_term eq (prep thm) net handle Net.DELETE => net
-
-val add = Thm.declaration_attribute (Data.map o ins)
-val del = Thm.declaration_attribute (Data.map o del)
-
-val name = Binding.name "z3_new_rule"
-
-val description = "declaration of Z3 proof rules"
-
-val _ = Theory.setup (Attrib.setup name (Attrib.add_del add del) description #>
- Global_Theory.add_thms_dynamic (name, Net.content o Data.get))
-
-end
--- a/src/HOL/Tools/SMT2/z3_new_proof_tools.ML Thu Mar 13 13:18:13 2014 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,156 +0,0 @@
-(* Title: HOL/Tools/SMT2/z3_new_proof_tools.ML
- Author: Sascha Boehme, TU Muenchen
-
-Helper functions required for Z3 proof replay.
-*)
-
-signature Z3_NEW_PROOF_TOOLS =
-sig
- (*theorem nets*)
- val thm_net_of: ('a -> thm) -> 'a list -> 'a Net.net
- val net_instances: (int * thm) Net.net -> cterm -> (int * thm) list
-
- (*proof combinators*)
- val under_assumption: (thm -> thm) -> cterm -> thm
- val discharge: thm -> thm -> thm
-
- (*a faster COMP*)
- type compose_data
- val precompose: (cterm -> cterm list) -> thm -> compose_data
- val precompose2: (cterm -> cterm * cterm) -> thm -> compose_data
- val compose: compose_data -> thm -> thm
-
- (*simpset*)
- val add_simproc: Simplifier.simproc -> Context.generic -> Context.generic
- val make_simpset: Proof.context -> thm list -> simpset
-end
-
-structure Z3_New_Proof_Tools: Z3_NEW_PROOF_TOOLS =
-struct
-
-
-
-(* theorem nets *)
-
-fun thm_net_of f xthms =
- let fun insert xthm = Net.insert_term (K false) (Thm.prop_of (f xthm), xthm)
- in fold insert xthms Net.empty end
-
-fun maybe_instantiate ct thm =
- try Thm.first_order_match (Thm.cprop_of thm, ct)
- |> Option.map (fn inst => Thm.instantiate inst thm)
-
-local
- fun instances_from_net match f net ct =
- let
- val lookup = if match then Net.match_term else Net.unify_term
- val xthms = lookup net (Thm.term_of ct)
- fun select ct = map_filter (f (maybe_instantiate ct)) xthms
- fun select' ct =
- let val thm = Thm.trivial ct
- in map_filter (f (try (fn rule => rule COMP thm))) xthms end
- in (case select ct of [] => select' ct | xthms' => xthms') end
-in
-
-fun net_instances net =
- instances_from_net false (fn f => fn (i, thm) => Option.map (pair i) (f thm))
- net
-
-end
-
-
-
-(* proof combinators *)
-
-fun under_assumption f ct =
- let val ct' = SMT2_Utils.mk_cprop ct
- in Thm.implies_intr ct' (f (Thm.assume ct')) end
-
-fun discharge p pq = Thm.implies_elim pq p
-
-
-
-(* a faster COMP *)
-
-type compose_data = cterm list * (cterm -> cterm list) * thm
-
-fun list2 (x, y) = [x, y]
-
-fun precompose f rule = (f (Thm.cprem_of rule 1), f, rule)
-fun precompose2 f rule = precompose (list2 o f) rule
-
-fun compose (cvs, f, rule) thm =
- discharge thm (Thm.instantiate ([], cvs ~~ f (Thm.cprop_of thm)) rule)
-
-
-
-(* simpset *)
-
-local
- val antisym_le1 = mk_meta_eq @{thm order_class.antisym_conv}
- val antisym_le2 = mk_meta_eq @{thm linorder_class.antisym_conv2}
- val antisym_less1 = mk_meta_eq @{thm linorder_class.antisym_conv1}
- val antisym_less2 = mk_meta_eq @{thm linorder_class.antisym_conv3}
-
- fun eq_prop t thm = HOLogic.mk_Trueprop t aconv Thm.prop_of thm
- fun dest_binop ((c as Const _) $ t $ u) = (c, t, u)
- | dest_binop t = raise TERM ("dest_binop", [t])
-
- fun prove_antisym_le ctxt t =
- let
- val (le, r, s) = dest_binop t
- 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 t =
- let
- val (less, r, s) = dest_binop (HOLogic.dest_not t)
- val le = Const (@{const_name less_eq}, Term.fastype_of less)
- val prems = Simplifier.prems_of ctxt
- in
- (case find_first (eq_prop (le $ r $ s)) prems of
- NONE =>
- find_first (eq_prop (HOLogic.mk_not (less $ s $ r))) prems
- |> Option.map (fn thm => thm RS antisym_less2)
- | SOME thm => SOME (thm RS antisym_le2))
- end
- handle THM _ => NONE
-
- val basic_simpset =
- simpset_of (put_simpset HOL_ss @{context}
- addsimps @{thms field_simps times_divide_eq_right times_divide_eq_left arith_special
- arith_simps rel_simps array_rules z3div_def z3mod_def}
- addsimprocs [@{simproc binary_int_div}, @{simproc binary_int_mod},
- Simplifier.simproc_global @{theory} "fast_int_arith" [
- "(m::int) < n", "(m::int) <= n", "(m::int) = n"] Lin_Arith.simproc,
- Simplifier.simproc_global @{theory} "antisym_le" ["(x::'a::order) <= y"] prove_antisym_le,
- Simplifier.simproc_global @{theory} "antisym_less" ["~ (x::'a::linorder) < y"]
- 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
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/SMT2/z3_new_replay.ML Thu Mar 13 13:18:13 2014 +0100
@@ -0,0 +1,193 @@
+(* Title: HOL/Tools/SMT2/z3_new_proof_replay.ML
+ Author: Sascha Boehme, TU Muenchen
+ Author: Jasmin Blanchette, TU Muenchen
+
+Z3 proof replay.
+*)
+
+signature Z3_NEW_PROOF_REPLAY =
+sig
+ val replay: Proof.context -> SMT2_Translate.replay_data -> string list ->
+ (int list * Z3_New_Proof.z3_step list) * thm
+end
+
+structure Z3_New_Proof_Replay: Z3_NEW_PROOF_REPLAY =
+struct
+
+fun params_of t = Term.strip_qnt_vars @{const_name all} t
+
+fun varify ctxt thm =
+ let
+ val maxidx = Thm.maxidx_of thm + 1
+ val vs = params_of (Thm.prop_of thm)
+ val vars = map_index (fn (i, (n, T)) => Var ((n, i + maxidx), T)) vs
+ in Drule.forall_elim_list (map (SMT2_Utils.certify ctxt) vars) thm end
+
+fun add_paramTs names t =
+ fold2 (fn n => fn (_, T) => AList.update (op =) (n, T)) names (params_of t)
+
+fun new_fixes ctxt nTs =
+ let
+ val (ns, ctxt') = Variable.variant_fixes (replicate (length nTs) "") ctxt
+ fun mk (n, T) n' = (n, SMT2_Utils.certify ctxt' (Free (n', T)))
+ in (ctxt', Symtab.make (map2 mk nTs ns)) end
+
+fun forall_elim_term ct (Const (@{const_name all}, _) $ (a as Abs _)) =
+ Term.betapply (a, Thm.term_of ct)
+ | forall_elim_term _ qt = raise TERM ("forall_elim'", [qt])
+
+fun apply_fixes elim env = fold (elim o the o Symtab.lookup env)
+
+val apply_fixes_prem = uncurry o apply_fixes Thm.forall_elim
+val apply_fixes_concl = apply_fixes forall_elim_term
+
+fun export_fixes env names = Drule.forall_intr_list (map (the o Symtab.lookup env) names)
+
+fun under_fixes f ctxt (prems, nthms) names concl =
+ let
+ val thms1 = map (varify ctxt) prems
+ val (ctxt', env) =
+ add_paramTs names concl []
+ |> fold (uncurry add_paramTs o apsnd Thm.prop_of) nthms
+ |> new_fixes ctxt
+ val thms2 = map (apply_fixes_prem env) nthms
+ val t = apply_fixes_concl env names concl
+ in export_fixes env names (f ctxt' (thms1 @ thms2) t) end
+
+fun replay_thm ctxt assumed nthms
+ (Z3_New_Proof.Z3_Step {id, rule, concl, fixes, is_fix_step, ...}) =
+ if Z3_New_Proof_Methods.is_assumption rule then
+ (case Inttab.lookup assumed id of
+ SOME (_, thm) => thm
+ | NONE => Thm.assume (SMT2_Utils.certify ctxt concl))
+ else
+ under_fixes (Z3_New_Proof_Methods.method_for rule) ctxt
+ (if is_fix_step then (map snd nthms, []) else ([], nthms)) fixes concl
+
+fun replay_step ctxt assumed (step as Z3_New_Proof.Z3_Step {id, prems, fixes, ...}) proofs =
+ let val nthms = map (the o Inttab.lookup proofs) prems
+ in Inttab.update (id, (fixes, replay_thm ctxt assumed nthms step)) proofs end
+
+local
+ val remove_trigger = mk_meta_eq @{thm SMT2.trigger_def}
+ val remove_weight = mk_meta_eq @{thm SMT2.weight_def}
+ val remove_fun_app = mk_meta_eq @{thm SMT2.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, Z3_New_Proof_Literals.rewrite_true]
+
+ fun rewrite _ [] = I
+ | rewrite ctxt eqs = Conv.fconv_rule (rewrite_conv ctxt eqs)
+
+ fun lookup_assm assms_net ct =
+ Z3_New_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 steps ctxt =
+ let
+ val eqs = map (rewrite ctxt [Z3_New_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))
+ |> Z3_New_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' RS thm, ctxt') end
+
+ fun add1 id fixes 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 (id, (fixes, thm)) ptab))
+ end
+
+ fun add (Z3_New_Proof.Z3_Step {id, rule, concl, fixes, ...})
+ (cx as ((is, thms), (ctxt, ptab))) =
+ if Z3_New_Proof_Methods.is_assumption rule andalso rule <> Z3_New_Proof.Hypothesis then
+ let
+ val ct = SMT2_Utils.certify ctxt concl
+ val thm1 =
+ Thm.trivial ct
+ |> Conv.fconv_rule (Conv.arg1_conv (revert_conv outer_ctxt))
+ val thm2 = singleton (Variable.export ctxt outer_ctxt) thm1
+ in
+ (case lookup_assm assms_net (Thm.cprem_of thm2 1) of
+ [] =>
+ let val (thm, ctxt') = assume thm1 ctxt
+ in ((is, thms), (ctxt', Inttab.update (id, (fixes, thm)) ptab)) end
+ | ithms => fold (add1 id fixes thm1) ithms cx)
+ end
+ else
+ cx
+ in fold add steps (([], []), (ctxt, Inttab.empty)) end
+
+end
+
+(* |- (EX x. P x) = P c |- ~ (ALL x. P x) = ~ P c *)
+local
+ val sk_rules = @{lemma
+ "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 discharge_sk_tac i st =
+ (rtac @{thm trans} i
+ THEN resolve_tac sk_rules i
+ THEN (rtac @{thm refl} ORELSE' discharge_sk_tac) (i+1)
+ THEN rtac @{thm refl} i) st
+
+end
+
+fun make_discharge_rules rules = rules @ [@{thm allI}, @{thm refl},
+ @{thm reflexive}, Z3_New_Proof_Literals.true_thm]
+
+val intro_def_rules = @{lemma
+ "(~ P | P) & (P | ~ P)"
+ "(P | ~ P) & (~ P | P)"
+ by fast+}
+
+fun discharge_assms_tac rules =
+ REPEAT (HEADGOAL (resolve_tac (intro_def_rules @ rules) ORELSE' SOLVED' discharge_sk_tac))
+
+fun discharge_assms ctxt rules thm =
+ (if Thm.nprems_of thm = 0 then
+ thm
+ else
+ (case Seq.pull (discharge_assms_tac rules thm) of
+ SOME (thm', _) => thm'
+ | NONE => raise THM ("failed to discharge premise", 1, [thm])))
+ |> Goal.norm_result ctxt
+
+fun discharge rules outer_ctxt inner_ctxt =
+ singleton (Proof_Context.export inner_ctxt outer_ctxt)
+ #> discharge_assms outer_ctxt (make_discharge_rules rules)
+
+fun replay outer_ctxt
+ ({context=ctxt, typs, terms, rewrite_rules, assms} : SMT2_Translate.replay_data) output =
+ let
+ val (steps, ctxt1) = Z3_New_Proof.parse typs terms output ctxt
+ val ctxt2 = put_simpset (Z3_New_Proof_Tools.make_simpset ctxt1 []) ctxt1
+ val ((is, rules), (ctxt3, assumed)) = add_asserted outer_ctxt rewrite_rules assms steps ctxt2
+ val proofs = fold (replay_step ctxt3 assumed) steps assumed
+ val (_, Z3_New_Proof.Z3_Step {id, ...}) = split_last steps
+ in
+ if Config.get ctxt3 SMT2_Config.filter_only_facts then ((is, steps), TrueI)
+ else (([], steps), Inttab.lookup proofs id |> the |> snd |> discharge rules outer_ctxt ctxt3)
+ end
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/SMT2/z3_new_replay_literals.ML Thu Mar 13 13:18:13 2014 +0100
@@ -0,0 +1,357 @@
+(* Title: HOL/Tools/SMT2/z3_new_proof_literals.ML
+ Author: Sascha Boehme, TU Muenchen
+
+Proof tools related to conjunctions and disjunctions.
+*)
+
+signature Z3_NEW_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 Z3_New_Proof_Literals: Z3_NEW_PROOF_LITERALS =
+struct
+
+
+
+(* literal table *)
+
+type littab = thm Termtab.table
+
+fun make_littab thms =
+ fold (Termtab.update o `SMT2_Utils.prop_of) thms Termtab.empty
+
+fun insert_lit thm = Termtab.update (`SMT2_Utils.prop_of thm)
+fun delete_lit thm = Termtab.delete (SMT2_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 @{theory} @{const Not})
+
+
+
+(* proof tools *)
+
+(** explosion of conjunctions and disjunctions **)
+
+local
+ val precomp = Z3_New_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 = Z3_New_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 Z3_New_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 (SMT2_Utils.prop_of thm) then cons thm
+ else
+ (case dest_rules (SMT2_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) (SMT2_Utils.prop_of thm)
+ then explode1 (Z3_New_Proof_Tools.compose dest_rule thm)
+ else cons (Z3_New_Proof_Tools.compose dest_rule thm)
+
+ fun explode0 thm =
+ if not is_conj andalso is_dneg (SMT2_Utils.prop_of thm)
+ then [Z3_New_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 ([], [(cv1, on_cprop f thm1), (cv2, on_cprop g thm2)]) rule
+ |> Z3_New_Proof_Tools.discharge thm1 |> Z3_New_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 = Z3_New_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 = Z3_New_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) =>
+ (Z3_New_Proof_Tools.compose dnegI, lookup t)
+ | @{const Not} $ (@{const HOL.eq (bool)} $ t $ (@{const Not} $ u)) =>
+ (Z3_New_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 => (Z3_New_Proof_Tools.compose negIffE, as_negIff lookup t)
+ | x => (Z3_New_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 (pairself 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 (SMT2_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)
+ |> pairself (extract_lit thm)
+ |> (fn (nlit, plit) => nlit COMP (plit COMP contra_rule)))
+ end
+
+ val falseE_v = 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 (Z3_New_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 = Z3_New_Proof_Tools.under_assumption (prove r cr o make_tab l) cl
+ val thm2 = Z3_New_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
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/SMT2/z3_new_replay_methods.ML Thu Mar 13 13:18:13 2014 +0100
@@ -0,0 +1,667 @@
+(* Title: HOL/Tools/SMT2/z3_new_proof.ML
+ Author: Sascha Boehme, TU Muenchen
+ Author: Jasmin Blanchette, TU Muenchen
+
+Proof methods for replaying Z3 proofs.
+*)
+
+signature Z3_NEW_PROOF_METHODS =
+sig
+ (*abstraction*)
+ type abs_context = int * term Termtab.table
+ type 'a abstracter = term -> abs_context -> 'a * abs_context
+ val add_arith_abstracter: (term abstracter -> term option abstracter) ->
+ Context.generic -> Context.generic
+
+ (*theory lemma methods*)
+ type th_lemma_method = Proof.context -> thm list -> term -> thm
+ val add_th_lemma_method: string * th_lemma_method -> Context.generic ->
+ Context.generic
+
+ (*methods for Z3 proof rules*)
+ type z3_method = Proof.context -> thm list -> term -> thm
+ val true_axiom: z3_method
+ val mp: z3_method
+ val refl: z3_method
+ val symm: z3_method
+ val trans: z3_method
+ val cong: z3_method
+ val quant_intro: z3_method
+ val distrib: z3_method
+ val and_elim: z3_method
+ val not_or_elim: z3_method
+ val rewrite: z3_method
+ val rewrite_star: z3_method
+ val pull_quant: z3_method
+ val push_quant: z3_method
+ val elim_unused: z3_method
+ val dest_eq_res: z3_method
+ val quant_inst: z3_method
+ val lemma: z3_method
+ val unit_res: z3_method
+ val iff_true: z3_method
+ val iff_false: z3_method
+ val comm: z3_method
+ val def_axiom: z3_method
+ val apply_def: z3_method
+ val iff_oeq: z3_method
+ val nnf_pos: z3_method
+ val nnf_neg: z3_method
+ val mp_oeq: z3_method
+ val th_lemma: string -> z3_method
+ val is_assumption: Z3_New_Proof.z3_rule -> bool
+ val method_for: Z3_New_Proof.z3_rule -> z3_method
+end
+
+structure Z3_New_Proof_Methods: Z3_NEW_PROOF_METHODS =
+struct
+
+type z3_method = Proof.context -> thm list -> term -> thm
+
+
+
+(* utility functions *)
+
+val trace = SMT2_Config.trace_msg
+
+fun pretty_thm ctxt thm = Syntax.pretty_term ctxt (Thm.concl_of thm)
+
+fun pretty_goal ctxt msg rule thms t =
+ let
+ val full_msg = msg ^ ": " ^ quote (Z3_New_Proof.string_of_rule rule)
+ val assms =
+ if null thms then []
+ else [Pretty.big_list "assumptions:" (map (pretty_thm ctxt) thms)]
+ val concl = Pretty.big_list "proposition:" [Syntax.pretty_term ctxt t]
+ in Pretty.big_list full_msg (assms @ [concl]) end
+
+fun replay_error ctxt msg rule thms t = error (Pretty.string_of (pretty_goal ctxt msg rule thms t))
+
+fun replay_rule_error ctxt = replay_error ctxt "Failed to replay Z3 proof step"
+
+fun trace_goal ctxt rule thms t =
+ trace ctxt (fn () => Pretty.string_of (pretty_goal ctxt "Goal" rule thms t))
+
+fun as_prop (t as Const (@{const_name Trueprop}, _) $ _) = t
+ | as_prop t = HOLogic.mk_Trueprop t
+
+fun dest_prop (Const (@{const_name Trueprop}, _) $ t) = t
+ | dest_prop t = t
+
+fun dest_thm thm = dest_prop (Thm.concl_of thm)
+
+fun certify_prop ctxt t = SMT2_Utils.certify ctxt (as_prop t)
+
+fun try_provers ctxt rule [] thms t = replay_rule_error ctxt rule thms t
+ | try_provers ctxt rule ((name, prover) :: named_provers) thms t =
+ (case (trace ctxt (K ("Trying prover " ^ quote name)); try prover t) of
+ SOME thm => thm
+ | NONE => try_provers ctxt rule named_provers thms t)
+
+fun match ctxt pat t =
+ (Vartab.empty, Vartab.empty)
+ |> Pattern.first_order_match (Proof_Context.theory_of ctxt) (pat, t)
+
+fun gen_certify_inst sel mk cert ctxt thm t =
+ let
+ val inst = match ctxt (dest_thm thm) (dest_prop t)
+ fun cert_inst (ix, (a, b)) = (cert (mk (ix, a)), cert b)
+ in Vartab.fold (cons o cert_inst) (sel inst) [] end
+
+fun match_instantiateT ctxt t thm =
+ if Term.exists_type (Term.exists_subtype Term.is_TVar) (dest_thm thm) then
+ let val certT = Thm.ctyp_of (Proof_Context.theory_of ctxt)
+ in Thm.instantiate (gen_certify_inst fst TVar certT ctxt thm t, []) thm end
+ else thm
+
+fun match_instantiate ctxt t thm =
+ let
+ val cert = SMT2_Utils.certify ctxt
+ val thm' = match_instantiateT ctxt t thm
+ in Thm.instantiate ([], gen_certify_inst snd Var cert ctxt thm' t) thm' end
+
+fun apply_rule ctxt t =
+ (case Z3_New_Proof_Rules.apply ctxt (certify_prop ctxt t) of
+ SOME thm => thm
+ | NONE => raise Fail "apply_rule")
+
+fun discharge _ [] thm = thm
+ | discharge i (rule :: rules) thm = discharge (i + Thm.nprems_of rule) rules (rule RSN (i, thm))
+
+fun by_tac ctxt thms ns ts t tac =
+ Goal.prove ctxt [] (map as_prop ts) (as_prop t)
+ (fn {context, prems} => HEADGOAL (tac context prems))
+ |> Drule.generalize ([], ns)
+ |> discharge 1 thms
+
+fun prove ctxt t tac = by_tac ctxt [] [] [] t (K o tac)
+
+fun prop_tac ctxt prems =
+ Method.insert_tac prems THEN' (Classical.fast_tac ctxt ORELSE' Clasimp.force_tac ctxt)
+
+fun quant_tac ctxt = Blast.blast_tac ctxt
+
+
+
+(* plug-ins *)
+
+type abs_context = int * term Termtab.table
+
+type 'a abstracter = term -> abs_context -> 'a * abs_context
+
+type th_lemma_method = Proof.context -> thm list -> term -> thm
+
+fun id_ord ((id1, _), (id2, _)) = int_ord (id1, id2)
+
+structure Plugins = Generic_Data
+(
+ type T =
+ (int * (term abstracter -> term option abstracter)) list *
+ th_lemma_method Symtab.table
+ val empty = ([], Symtab.empty)
+ val extend = I
+ fun merge ((abss1, ths1), (abss2, ths2)) = (
+ Ord_List.merge id_ord (abss1, abss2),
+ Symtab.merge (K true) (ths1, ths2))
+)
+
+fun add_arith_abstracter abs = Plugins.map (apfst (Ord_List.insert id_ord (serial (), abs)))
+fun get_arith_abstracters ctxt = map snd (fst (Plugins.get (Context.Proof ctxt)))
+
+fun add_th_lemma_method method = Plugins.map (apsnd (Symtab.update_new method))
+fun get_th_lemma_method ctxt = snd (Plugins.get (Context.Proof ctxt))
+
+
+
+(* abstraction *)
+
+fun prove_abstract ctxt thms t tac f =
+ let
+ val ((prems, concl), (_, ts)) = f (1, Termtab.empty)
+ val ns = Termtab.fold (fn (_, v) => cons (fst (Term.dest_Free v))) ts []
+ in
+ by_tac ctxt [] ns prems concl tac
+ |> match_instantiate ctxt t
+ |> discharge 1 thms
+ end
+
+fun prove_abstract' ctxt t tac f =
+ prove_abstract ctxt [] t tac (f #>> pair [])
+
+fun lookup_term (_, terms) t = Termtab.lookup terms t
+
+fun abstract_sub t f cx =
+ (case lookup_term cx t of
+ SOME v => (v, cx)
+ | NONE => f cx)
+
+fun mk_fresh_free t (i, terms) =
+ let val v = Free ("t" ^ string_of_int i, fastype_of t)
+ in (v, (i + 1, Termtab.update (t, v) terms)) end
+
+fun apply_abstracters _ [] _ cx = (NONE, cx)
+ | apply_abstracters abs (abstracter :: abstracters) t cx =
+ (case abstracter abs t cx of
+ (NONE, _) => apply_abstracters abs abstracters t cx
+ | x as (SOME _, _) => x)
+
+fun abstract_term (t as _ $ _) = abstract_sub t (mk_fresh_free t)
+ | abstract_term (t as Abs _) = abstract_sub t (mk_fresh_free t)
+ | abstract_term t = pair t
+
+fun abstract_bin abs f t t1 t2 = abstract_sub t (abs t1 ##>> abs t2 #>> f)
+
+fun abstract_ter abs f t t1 t2 t3 =
+ abstract_sub t (abs t1 ##>> abs t2 ##>> abs t3 #>> (Parse.triple1 #> f))
+
+fun abstract_lit (@{const HOL.Not} $ t) = abstract_term t #>> HOLogic.mk_not
+ | abstract_lit t = abstract_term t
+
+fun abstract_not abs (t as @{const HOL.Not} $ t1) =
+ abstract_sub t (abs t1 #>> HOLogic.mk_not)
+ | abstract_not _ t = abstract_lit t
+
+fun abstract_conj (t as @{const HOL.conj} $ t1 $ t2) =
+ abstract_bin abstract_conj HOLogic.mk_conj t t1 t2
+ | abstract_conj t = abstract_lit t
+
+fun abstract_disj (t as @{const HOL.disj} $ t1 $ t2) =
+ abstract_bin abstract_disj HOLogic.mk_disj t t1 t2
+ | abstract_disj t = abstract_lit t
+
+fun abstract_prop (t as (c as @{const If (bool)}) $ t1 $ t2 $ t3) =
+ abstract_ter abstract_prop (fn (t1, t2, t3) => c $ t1 $ t2 $ t3) t t1 t2 t3
+ | abstract_prop (t as @{const HOL.disj} $ t1 $ t2) =
+ abstract_bin abstract_prop HOLogic.mk_disj t t1 t2
+ | abstract_prop (t as @{const HOL.conj} $ t1 $ t2) =
+ abstract_bin abstract_prop HOLogic.mk_conj t t1 t2
+ | abstract_prop (t as @{const HOL.implies} $ t1 $ t2) =
+ abstract_bin abstract_prop HOLogic.mk_imp t t1 t2
+ | abstract_prop (t as @{term "HOL.eq :: bool => _"} $ t1 $ t2) =
+ abstract_bin abstract_prop HOLogic.mk_eq t t1 t2
+ | abstract_prop t = abstract_not abstract_prop t
+
+fun abstract_arith ctxt u =
+ let
+ fun abs (t as (c as Const _) $ Abs (s, T, t')) =
+ abstract_sub t (abs t' #>> (fn u' => c $ Abs (s, T, u')))
+ | abs (t as (c as Const (@{const_name If}, _)) $ t1 $ t2 $ t3) =
+ abstract_ter abs (fn (t1, t2, t3) => c $ t1 $ t2 $ t3) t t1 t2 t3
+ | abs (t as @{const HOL.Not} $ t1) = abstract_sub t (abs t1 #>> HOLogic.mk_not)
+ | abs (t as @{const HOL.disj} $ t1 $ t2) =
+ abstract_sub t (abs t1 ##>> abs t2 #>> HOLogic.mk_disj)
+ | abs (t as (c as Const (@{const_name uminus_class.uminus}, _)) $ t1) =
+ abstract_sub t (abs t1 #>> (fn u => c $ u))
+ | abs (t as (c as Const (@{const_name plus_class.plus}, _)) $ t1 $ t2) =
+ abstract_sub t (abs t1 ##>> abs t2 #>> (fn (u1, u2) => c $ u1 $ u2))
+ | abs (t as (c as Const (@{const_name minus_class.minus}, _)) $ t1 $ t2) =
+ abstract_sub t (abs t1 ##>> abs t2 #>> (fn (u1, u2) => c $ u1 $ u2))
+ | abs (t as (c as Const (@{const_name times_class.times}, _)) $ t1 $ t2) =
+ abstract_sub t (abs t1 ##>> abs t2 #>> (fn (u1, u2) => c $ u1 $ u2))
+ | abs (t as (c as Const (@{const_name z3div}, _)) $ t1 $ t2) =
+ abstract_sub t (abs t1 ##>> abs t2 #>> (fn (u1, u2) => c $ u1 $ u2))
+ | abs (t as (c as Const (@{const_name z3mod}, _)) $ t1 $ t2) =
+ abstract_sub t (abs t1 ##>> abs t2 #>> (fn (u1, u2) => c $ u1 $ u2))
+ | abs (t as (c as Const (@{const_name HOL.eq}, _)) $ t1 $ t2) =
+ abstract_sub t (abs t1 ##>> abs t2 #>> (fn (u1, u2) => c $ u1 $ u2))
+ | abs (t as (c as Const (@{const_name ord_class.less}, _)) $ t1 $ t2) =
+ abstract_sub t (abs t1 ##>> abs t2 #>> (fn (u1, u2) => c $ u1 $ u2))
+ | abs (t as (c as Const (@{const_name ord_class.less_eq}, _)) $ t1 $ t2) =
+ abstract_sub t (abs t1 ##>> abs t2 #>> (fn (u1, u2) => c $ u1 $ u2))
+ | abs t = abstract_sub t (fn cx =>
+ if can HOLogic.dest_number t then (t, cx)
+ else
+ (case apply_abstracters abs (get_arith_abstracters ctxt) t cx of
+ (SOME u, cx') => (u, cx')
+ | (NONE, _) => abstract_term t cx))
+ in abs u end
+
+
+
+(* truth axiom *)
+
+fun true_axiom _ _ _ = @{thm TrueI}
+
+
+
+(* modus ponens *)
+
+fun mp _ [p, p_eq_q] _ = discharge 1 [p_eq_q, p] iffD1
+ | mp ctxt thms t = replay_rule_error ctxt Z3_New_Proof.Modus_Ponens thms t
+
+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 |> (
+ resolve_tac (@{thm refl} :: prems) i
+ ORELSE (cong_tac i THEN ctac prems (i + 1) THEN ctac prems i))
+
+fun cong_basic ctxt thms t =
+ let val st = Thm.trivial (certify_prop ctxt t)
+ in
+ (case Seq.pull (ctac thms 1 st) of
+ SOME (thm, _) => thm
+ | NONE => raise THM ("cong", 0, thms @ [st]))
+ end
+
+val cong_dest_rules = @{lemma
+ "(~ P | Q) & (P | ~ Q) ==> P = Q"
+ "(P | ~ Q) & (~ P | Q) ==> P = Q"
+ by fast+}
+
+fun cong_full ctxt thms t = prove ctxt t (fn ctxt' =>
+ Method.insert_tac thms
+ THEN' (Classical.fast_tac ctxt'
+ ORELSE' dresolve_tac cong_dest_rules
+ THEN' Classical.fast_tac ctxt'))
+
+fun cong ctxt thms = try_provers ctxt Z3_New_Proof.Monotonicity [
+ ("basic", cong_basic ctxt thms),
+ ("full", cong_full ctxt thms)] thms
+
+
+
+(* quantifier introduction *)
+
+val quant_intro_rules = @{lemma
+ "(!!x. P x = Q x) ==> (ALL x. P x) = (ALL x. Q x)"
+ "(!!x. P x = Q x) ==> (EX x. P x) = (EX x. Q x)"
+ "(!!x. (~ P x) = Q x) ==> (~ (EX x. P x)) = (ALL x. Q x)"
+ "(!!x. (~ P x) = Q x) ==> (~ (ALL x. P x)) = (EX x. Q x)"
+ by fast+}
+
+fun quant_intro ctxt [thm] t =
+ prove ctxt t (K (REPEAT_ALL_NEW (resolve_tac (thm :: quant_intro_rules))))
+ | 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 *)
+fun distrib ctxt _ t =
+ prove_abstract' ctxt t prop_tac (abstract_prop (dest_prop t))
+
+
+
+(* elimination of conjunctions *)
+
+fun and_elim ctxt [thm] t =
+ prove_abstract ctxt [thm] t prop_tac (
+ abstract_lit (dest_prop t) ##>>
+ abstract_conj (dest_thm thm) #>>
+ apfst single o swap)
+ | 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 =
+ prove_abstract ctxt [thm] t prop_tac (
+ abstract_lit (dest_prop t) ##>>
+ abstract_not abstract_disj (dest_thm thm) #>>
+ apfst single o swap)
+ | not_or_elim ctxt thms t =
+ replay_rule_error ctxt Z3_New_Proof.Not_Or_Elim thms t
+
+
+
+(* rewriting *)
+
+fun abstract_eq f1 f2 (Const (@{const_name HOL.eq}, _) $ t1 $ t2) =
+ f1 t1 ##>> f2 t2 #>> HOLogic.mk_eq
+ | abstract_eq _ _ t = abstract_term t
+
+fun prove_prop_rewrite ctxt t =
+ prove_abstract' ctxt t prop_tac (
+ abstract_eq abstract_prop abstract_prop (dest_prop t))
+
+fun arith_rewrite_tac ctxt _ =
+ TRY o Simplifier.simp_tac ctxt
+ THEN_ALL_NEW (Arith_Data.arith_tac ctxt ORELSE' Clasimp.force_tac ctxt)
+
+fun prove_arith_rewrite ctxt t =
+ prove_abstract' ctxt t arith_rewrite_tac (
+ abstract_eq (abstract_arith ctxt) (abstract_arith ctxt) (dest_prop t))
+
+fun rewrite ctxt _ = try_provers ctxt Z3_New_Proof.Rewrite [
+ ("rules", apply_rule ctxt),
+ ("prop_rewrite", prove_prop_rewrite ctxt),
+ ("arith_rewrite", prove_arith_rewrite ctxt)] []
+
+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}
+val elim_ex = @{lemma "P = Q ==> (EX x. P) = Q" by fast}
+
+fun elim_unused_tac i st = (
+ match_tac [@{thm refl}]
+ ORELSE' (match_tac [elim_all, elim_ex] THEN' elim_unused_tac)
+ ORELSE' (
+ match_tac [@{thm iff_allI}, @{thm iff_exI}]
+ THEN' elim_unused_tac)) i st
+
+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}
+
+fun quant_inst ctxt _ t = prove ctxt t (fn _ =>
+ REPEAT_ALL_NEW (rtac quant_inst_rule)
+ THEN' rtac @{thm excluded_middle})
+
+
+
+(* propositional lemma *)
+
+exception LEMMA of unit
+
+val intro_hyp_rule1 = @{lemma "(~P ==> Q) ==> P | Q" by fast}
+val intro_hyp_rule2 = @{lemma "(P ==> Q) ==> ~P | Q" by fast}
+
+fun norm_lemma thm =
+ (thm COMP_INCR intro_hyp_rule1)
+ handle THM _ => thm COMP_INCR intro_hyp_rule2
+
+fun negated_prop (@{const HOL.Not} $ t) = HOLogic.mk_Trueprop t
+ | negated_prop t = HOLogic.mk_Trueprop (HOLogic.mk_not t)
+
+fun intro_hyps tab (t as @{const HOL.disj} $ t1 $ t2) cx =
+ lookup_intro_hyps tab t (fold (intro_hyps tab) [t1, t2]) cx
+ | intro_hyps tab t cx =
+ lookup_intro_hyps tab t (fn _ => raise LEMMA ()) cx
+
+and lookup_intro_hyps tab t f (cx as (thm, terms)) =
+ (case Termtab.lookup tab (negated_prop t) of
+ NONE => f cx
+ | SOME hyp => (norm_lemma (Thm.implies_intr hyp thm), t :: terms))
+
+fun lemma ctxt (thms as [thm]) t =
+ (let
+ val tab = Termtab.make (map (`Thm.term_of) (#hyps (Thm.crep_thm thm)))
+ val (thm', terms) = intro_hyps tab (dest_prop t) (thm, [])
+ in
+ prove_abstract ctxt [thm'] t prop_tac (
+ fold (snd oo abstract_lit) terms #>
+ abstract_disj (dest_thm thm') #>> single ##>>
+ abstract_disj (dest_prop t))
+ end
+ handle LEMMA () => replay_error ctxt "Bad proof state" Z3_New_Proof.Lemma thms t)
+ | 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))) =
+ abstract_sub t (abstract_unit t1 ##>> abstract_unit t2 #>>
+ HOLogic.mk_not o HOLogic.mk_disj)
+ | abstract_unit (t as (@{const HOL.disj} $ t1 $ t2)) =
+ abstract_sub t (abstract_unit t1 ##>> abstract_unit t2 #>>
+ HOLogic.mk_disj)
+ | abstract_unit t = abstract_lit t
+
+fun unit_res ctxt thms t =
+ prove_abstract ctxt thms t prop_tac (
+ fold_map (abstract_unit o dest_thm) thms ##>>
+ abstract_unit (dest_prop t) #>>
+ (fn (prems, concl) => (prems, concl)))
+
+
+
+(* iff-true *)
+
+val iff_true_rule = @{lemma "P ==> P = True" by fast}
+
+fun iff_true _ [thm] _ = thm RS iff_true_rule
+ | 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}
+
+fun iff_false _ [thm] _ = thm RS iff_false_rule
+ | 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 =
+ (case dest_prop t of
+ @{const HOL.disj} $ u1 $ u2 =>
+ prove_abstract' ctxt t prop_tac (
+ abstract_prop u2 ##>> abstract_prop u1 #>> HOLogic.mk_disj o swap)
+ | u => prove_abstract' ctxt t prop_tac (abstract_prop u))
+
+fun def_axiom ctxt _ = try_provers ctxt Z3_New_Proof.Def_Axiom [
+ ("rules", apply_rule ctxt),
+ ("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 =
+ prove_abstract ctxt thms t prop_tac (
+ fold_map (abstract_prop o dest_thm) thms ##>>
+ abstract_prop (dest_prop t))
+
+fun nnf ctxt rule thms = try_provers ctxt rule [
+ ("prop", nnf_prop ctxt thms),
+ ("quant", quant_intro ctxt [hd thms])] thms
+
+fun nnf_pos ctxt = nnf ctxt Z3_New_Proof.Nnf_Pos
+fun nnf_neg ctxt = nnf ctxt Z3_New_Proof.Nnf_Neg
+
+
+
+(* theory lemmas *)
+
+fun arith_th_lemma_tac ctxt prems =
+ Method.insert_tac prems
+ THEN' SELECT_GOAL (Local_Defs.unfold_tac ctxt @{thms z3div_def z3mod_def})
+ THEN' Arith_Data.arith_tac ctxt
+
+fun arith_th_lemma ctxt thms t =
+ prove_abstract ctxt thms t arith_th_lemma_tac (
+ fold_map (abstract_arith ctxt o dest_thm) thms ##>>
+ abstract_arith ctxt (dest_prop t))
+
+val _ = Theory.setup (Context.theory_map (add_th_lemma_method ("arith", arith_th_lemma)))
+
+fun th_lemma name ctxt thms =
+ (case Symtab.lookup (get_th_lemma_method ctxt) name of
+ SOME method => method ctxt thms
+ | NONE => replay_error ctxt "Bad theory" (Z3_New_Proof.Th_Lemma name) thms)
+
+
+
+(* mapping of rules to methods *)
+
+fun is_assumption Z3_New_Proof.Asserted = true
+ | is_assumption Z3_New_Proof.Goal = true
+ | is_assumption Z3_New_Proof.Hypothesis = true
+ | is_assumption Z3_New_Proof.Intro_Def = true
+ | is_assumption Z3_New_Proof.Skolemize = true
+ | is_assumption _ = false
+
+fun unsupported rule ctxt = replay_error ctxt "Unsupported" rule
+fun assumed rule ctxt = replay_error ctxt "Assumed" rule
+
+fun choose Z3_New_Proof.True_Axiom = true_axiom
+ | choose (r as Z3_New_Proof.Asserted) = assumed r
+ | choose (r as Z3_New_Proof.Goal) = assumed r
+ | choose Z3_New_Proof.Modus_Ponens = mp
+ | choose Z3_New_Proof.Reflexivity = refl
+ | choose Z3_New_Proof.Symmetry = symm
+ | choose Z3_New_Proof.Transitivity = trans
+ | choose (r as Z3_New_Proof.Transitivity_Star) = unsupported r
+ | choose Z3_New_Proof.Monotonicity = cong
+ | choose Z3_New_Proof.Quant_Intro = quant_intro
+ | choose Z3_New_Proof.Distributivity = distrib
+ | choose Z3_New_Proof.And_Elim = and_elim
+ | choose Z3_New_Proof.Not_Or_Elim = not_or_elim
+ | choose Z3_New_Proof.Rewrite = rewrite
+ | choose Z3_New_Proof.Rewrite_Star = rewrite_star
+ | choose Z3_New_Proof.Pull_Quant = pull_quant
+ | choose (r as Z3_New_Proof.Pull_Quant_Star) = unsupported r
+ | choose Z3_New_Proof.Push_Quant = push_quant
+ | choose Z3_New_Proof.Elim_Unused_Vars = elim_unused
+ | choose Z3_New_Proof.Dest_Eq_Res = dest_eq_res
+ | choose Z3_New_Proof.Quant_Inst = quant_inst
+ | choose (r as Z3_New_Proof.Hypothesis) = assumed r
+ | choose Z3_New_Proof.Lemma = lemma
+ | choose Z3_New_Proof.Unit_Resolution = unit_res
+ | choose Z3_New_Proof.Iff_True = iff_true
+ | choose Z3_New_Proof.Iff_False = iff_false
+ | choose Z3_New_Proof.Commutativity = comm
+ | choose Z3_New_Proof.Def_Axiom = def_axiom
+ | choose (r as Z3_New_Proof.Intro_Def) = assumed r
+ | choose Z3_New_Proof.Apply_Def = apply_def
+ | choose Z3_New_Proof.Iff_Oeq = iff_oeq
+ | choose Z3_New_Proof.Nnf_Pos = nnf_pos
+ | choose Z3_New_Proof.Nnf_Neg = nnf_neg
+ | choose (r as Z3_New_Proof.Nnf_Star) = unsupported r
+ | choose (r as Z3_New_Proof.Cnf_Star) = unsupported r
+ | choose (r as Z3_New_Proof.Skolemize) = assumed r
+ | choose Z3_New_Proof.Modus_Ponens_Oeq = mp_oeq
+ | choose (Z3_New_Proof.Th_Lemma name) = th_lemma name
+
+fun with_tracing rule method ctxt thms t =
+ let val _ = trace_goal ctxt rule thms t
+ in method ctxt thms t end
+
+fun method_for rule = with_tracing rule (choose rule)
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/SMT2/z3_new_replay_rules.ML Thu Mar 13 13:18:13 2014 +0100
@@ -0,0 +1,56 @@
+(* Title: HOL/Tools/SMT2/z3_new_proof_rules.ML
+ Author: Sascha Boehme, TU Muenchen
+
+Custom rules for Z3 proof replay.
+*)
+
+signature Z3_NEW_PROOF_RULES =
+sig
+ val apply: Proof.context -> cterm -> thm option
+end
+
+structure Z3_New_Proof_Rules: Z3_NEW_PROOF_RULES =
+struct
+
+val eq = Thm.eq_thm
+
+structure Data = Generic_Data
+(
+ type T = thm Net.net
+ val empty = Net.empty
+ val extend = I
+ val merge = Net.merge eq
+)
+
+fun maybe_instantiate ct thm =
+ try Thm.first_order_match (Thm.cprop_of thm, ct)
+ |> Option.map (fn inst => Thm.instantiate inst thm)
+
+fun apply ctxt ct =
+ let
+ val net = Data.get (Context.Proof ctxt)
+ val xthms = Net.match_term net (Thm.term_of ct)
+
+ fun select ct = map_filter (maybe_instantiate ct) xthms
+ fun select' ct =
+ let val thm = Thm.trivial ct
+ in map_filter (try (fn rule => rule COMP thm)) xthms end
+
+ in try hd (case select ct of [] => select' ct | xthms' => xthms') end
+
+val prep = `Thm.prop_of
+
+fun ins thm net = Net.insert_term eq (prep thm) net handle Net.INSERT => net
+fun del thm net = Net.delete_term eq (prep thm) net handle Net.DELETE => net
+
+val add = Thm.declaration_attribute (Data.map o ins)
+val del = Thm.declaration_attribute (Data.map o del)
+
+val name = Binding.name "z3_new_rule"
+
+val description = "declaration of Z3 proof rules"
+
+val _ = Theory.setup (Attrib.setup name (Attrib.add_del add del) description #>
+ Global_Theory.add_thms_dynamic (name, Net.content o Data.get))
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/SMT2/z3_new_replay_util.ML Thu Mar 13 13:18:13 2014 +0100
@@ -0,0 +1,156 @@
+(* Title: HOL/Tools/SMT2/z3_new_proof_tools.ML
+ Author: Sascha Boehme, TU Muenchen
+
+Helper functions required for Z3 proof replay.
+*)
+
+signature Z3_NEW_PROOF_TOOLS =
+sig
+ (*theorem nets*)
+ val thm_net_of: ('a -> thm) -> 'a list -> 'a Net.net
+ val net_instances: (int * thm) Net.net -> cterm -> (int * thm) list
+
+ (*proof combinators*)
+ val under_assumption: (thm -> thm) -> cterm -> thm
+ val discharge: thm -> thm -> thm
+
+ (*a faster COMP*)
+ type compose_data
+ val precompose: (cterm -> cterm list) -> thm -> compose_data
+ val precompose2: (cterm -> cterm * cterm) -> thm -> compose_data
+ val compose: compose_data -> thm -> thm
+
+ (*simpset*)
+ val add_simproc: Simplifier.simproc -> Context.generic -> Context.generic
+ val make_simpset: Proof.context -> thm list -> simpset
+end
+
+structure Z3_New_Proof_Tools: Z3_NEW_PROOF_TOOLS =
+struct
+
+
+
+(* theorem nets *)
+
+fun thm_net_of f xthms =
+ let fun insert xthm = Net.insert_term (K false) (Thm.prop_of (f xthm), xthm)
+ in fold insert xthms Net.empty end
+
+fun maybe_instantiate ct thm =
+ try Thm.first_order_match (Thm.cprop_of thm, ct)
+ |> Option.map (fn inst => Thm.instantiate inst thm)
+
+local
+ fun instances_from_net match f net ct =
+ let
+ val lookup = if match then Net.match_term else Net.unify_term
+ val xthms = lookup net (Thm.term_of ct)
+ fun select ct = map_filter (f (maybe_instantiate ct)) xthms
+ fun select' ct =
+ let val thm = Thm.trivial ct
+ in map_filter (f (try (fn rule => rule COMP thm))) xthms end
+ in (case select ct of [] => select' ct | xthms' => xthms') end
+in
+
+fun net_instances net =
+ instances_from_net false (fn f => fn (i, thm) => Option.map (pair i) (f thm))
+ net
+
+end
+
+
+
+(* proof combinators *)
+
+fun under_assumption f ct =
+ let val ct' = SMT2_Utils.mk_cprop ct
+ in Thm.implies_intr ct' (f (Thm.assume ct')) end
+
+fun discharge p pq = Thm.implies_elim pq p
+
+
+
+(* a faster COMP *)
+
+type compose_data = cterm list * (cterm -> cterm list) * thm
+
+fun list2 (x, y) = [x, y]
+
+fun precompose f rule = (f (Thm.cprem_of rule 1), f, rule)
+fun precompose2 f rule = precompose (list2 o f) rule
+
+fun compose (cvs, f, rule) thm =
+ discharge thm (Thm.instantiate ([], cvs ~~ f (Thm.cprop_of thm)) rule)
+
+
+
+(* simpset *)
+
+local
+ val antisym_le1 = mk_meta_eq @{thm order_class.antisym_conv}
+ val antisym_le2 = mk_meta_eq @{thm linorder_class.antisym_conv2}
+ val antisym_less1 = mk_meta_eq @{thm linorder_class.antisym_conv1}
+ val antisym_less2 = mk_meta_eq @{thm linorder_class.antisym_conv3}
+
+ fun eq_prop t thm = HOLogic.mk_Trueprop t aconv Thm.prop_of thm
+ fun dest_binop ((c as Const _) $ t $ u) = (c, t, u)
+ | dest_binop t = raise TERM ("dest_binop", [t])
+
+ fun prove_antisym_le ctxt t =
+ let
+ val (le, r, s) = dest_binop t
+ 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 t =
+ let
+ val (less, r, s) = dest_binop (HOLogic.dest_not t)
+ val le = Const (@{const_name less_eq}, Term.fastype_of less)
+ val prems = Simplifier.prems_of ctxt
+ in
+ (case find_first (eq_prop (le $ r $ s)) prems of
+ NONE =>
+ find_first (eq_prop (HOLogic.mk_not (less $ s $ r))) prems
+ |> Option.map (fn thm => thm RS antisym_less2)
+ | SOME thm => SOME (thm RS antisym_le2))
+ end
+ handle THM _ => NONE
+
+ val basic_simpset =
+ simpset_of (put_simpset HOL_ss @{context}
+ addsimps @{thms field_simps times_divide_eq_right times_divide_eq_left arith_special
+ arith_simps rel_simps array_rules z3div_def z3mod_def}
+ addsimprocs [@{simproc binary_int_div}, @{simproc binary_int_mod},
+ Simplifier.simproc_global @{theory} "fast_int_arith" [
+ "(m::int) < n", "(m::int) <= n", "(m::int) = n"] Lin_Arith.simproc,
+ Simplifier.simproc_global @{theory} "antisym_le" ["(x::'a::order) <= y"] prove_antisym_le,
+ Simplifier.simproc_global @{theory} "antisym_less" ["~ (x::'a::linorder) < y"]
+ 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