# HG changeset patch # User blanchet # Date 1394713093 -3600 # Node ID 99c82a837f8ad56abef403eddc74750b7e816df0 # Parent db61a0a62b2cd1cafe067249ec0b792b5959fe21 renamed ML files diff -r db61a0a62b2c -r 99c82a837f8a src/HOL/Tools/SMT2/smt2_setup_solvers.ML --- 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 diff -r db61a0a62b2c -r 99c82a837f8a src/HOL/Tools/SMT2/smt2_systems.ML --- /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 diff -r db61a0a62b2c -r 99c82a837f8a src/HOL/Tools/SMT2/smt2_util.ML --- /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 diff -r db61a0a62b2c -r 99c82a837f8a src/HOL/Tools/SMT2/smt2_utils.ML --- 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 diff -r db61a0a62b2c -r 99c82a837f8a src/HOL/Tools/SMT2/z3_new_proof_literals.ML --- 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 diff -r db61a0a62b2c -r 99c82a837f8a src/HOL/Tools/SMT2/z3_new_proof_methods.ML --- 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 diff -r db61a0a62b2c -r 99c82a837f8a src/HOL/Tools/SMT2/z3_new_proof_replay.ML --- 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 diff -r db61a0a62b2c -r 99c82a837f8a src/HOL/Tools/SMT2/z3_new_proof_rules.ML --- 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 diff -r db61a0a62b2c -r 99c82a837f8a src/HOL/Tools/SMT2/z3_new_proof_tools.ML --- 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 diff -r db61a0a62b2c -r 99c82a837f8a src/HOL/Tools/SMT2/z3_new_replay.ML --- /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 diff -r db61a0a62b2c -r 99c82a837f8a src/HOL/Tools/SMT2/z3_new_replay_literals.ML --- /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 diff -r db61a0a62b2c -r 99c82a837f8a src/HOL/Tools/SMT2/z3_new_replay_methods.ML --- /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 diff -r db61a0a62b2c -r 99c82a837f8a src/HOL/Tools/SMT2/z3_new_replay_rules.ML --- /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 diff -r db61a0a62b2c -r 99c82a837f8a src/HOL/Tools/SMT2/z3_new_replay_util.ML --- /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