tuning
authorblanchet
Thu Jun 12 01:00:49 2014 +0200 (2014-06-12)
changeset 57229489083abce44
parent 57228 d52012eabf0d
child 57230 ec5ff6bb2a92
tuning
src/HOL/SMT.thy
src/HOL/Tools/SMT2/smt2_builtin.ML
src/HOL/Tools/SMT2/smt2_config.ML
src/HOL/Tools/SMT2/smt2_datatypes.ML
src/HOL/Tools/SMT2/smt2_failure.ML
src/HOL/Tools/SMT2/smt2_normalize.ML
src/HOL/Tools/SMT2/smt2_real.ML
src/HOL/Tools/SMT2/smt2_solver.ML
src/HOL/Tools/SMT2/smt2_systems.ML
src/HOL/Tools/SMT2/smt2_translate.ML
src/HOL/Tools/SMT2/smt2_util.ML
src/HOL/Tools/SMT2/smtlib2.ML
src/HOL/Tools/SMT2/smtlib2_interface.ML
src/HOL/Tools/SMT2/z3_new_interface.ML
src/HOL/Tools/SMT2/z3_new_proof.ML
src/HOL/Tools/SMT2/z3_new_real.ML
src/HOL/Tools/SMT2/z3_new_replay.ML
src/HOL/Tools/SMT2/z3_new_replay_literals.ML
src/HOL/Tools/SMT2/z3_new_replay_methods.ML
src/HOL/Tools/SMT2/z3_new_replay_rules.ML
src/HOL/Tools/SMT2/z3_new_replay_util.ML
src/HOL/Word/Tools/smt2_word.ML
     1.1 --- a/src/HOL/SMT.thy	Thu Jun 12 01:00:49 2014 +0200
     1.2 +++ b/src/HOL/SMT.thy	Thu Jun 12 01:00:49 2014 +0200
     1.3 @@ -5,7 +5,7 @@
     1.4  header {* Bindings to Satisfiability Modulo Theories (SMT) solvers *}
     1.5  
     1.6  theory SMT
     1.7 -imports List
     1.8 +imports ATP
     1.9  keywords "smt_status" :: diag
    1.10  begin
    1.11  
     2.1 --- a/src/HOL/Tools/SMT2/smt2_builtin.ML	Thu Jun 12 01:00:49 2014 +0200
     2.2 +++ b/src/HOL/Tools/SMT2/smt2_builtin.ML	Thu Jun 12 01:00:49 2014 +0200
     2.3 @@ -40,7 +40,7 @@
     2.4    val dest_builtin_ext: Proof.context -> string * typ -> term list -> term list option
     2.5    val is_builtin_fun: Proof.context -> string * typ -> term list -> bool
     2.6    val is_builtin_fun_ext: Proof.context -> string * typ -> term list -> bool
     2.7 -end
     2.8 +end;
     2.9  
    2.10  structure SMT2_Builtin: SMT2_BUILTIN =
    2.11  struct
    2.12 @@ -219,4 +219,4 @@
    2.13  
    2.14  fun is_builtin_fun_ext ctxt c ts = is_some (dest_builtin_fun_ext ctxt c ts)
    2.15  
    2.16 -end
    2.17 +end;
     3.1 --- a/src/HOL/Tools/SMT2/smt2_config.ML	Thu Jun 12 01:00:49 2014 +0200
     3.2 +++ b/src/HOL/Tools/SMT2/smt2_config.ML	Thu Jun 12 01:00:49 2014 +0200
     3.3 @@ -47,7 +47,7 @@
     3.4  
     3.5    (*setup*)
     3.6    val print_setup: Proof.context -> unit
     3.7 -end
     3.8 +end;
     3.9  
    3.10  structure SMT2_Config: SMT2_CONFIG =
    3.11  struct
    3.12 @@ -246,4 +246,4 @@
    3.13      \and the values of SMT configuration options"
    3.14      (Scan.succeed (Toplevel.keep (print_setup o Toplevel.context_of)))
    3.15  
    3.16 -end
    3.17 +end;
     4.1 --- a/src/HOL/Tools/SMT2/smt2_datatypes.ML	Thu Jun 12 01:00:49 2014 +0200
     4.2 +++ b/src/HOL/Tools/SMT2/smt2_datatypes.ML	Thu Jun 12 01:00:49 2014 +0200
     4.3 @@ -10,7 +10,7 @@
     4.4    val add_decls: typ ->
     4.5      (typ * (term * term list) list) list list * Proof.context ->
     4.6      (typ * (term * term list) list) list list * Proof.context
     4.7 -end
     4.8 +end;
     4.9  
    4.10  structure SMT2_Datatypes: SMT2_DATATYPES =
    4.11  struct
    4.12 @@ -90,4 +90,4 @@
    4.13              in fold add Us (ins dss, ctxt2) end))
    4.14    in add T ([], ctxt) |>> append declss o map snd end
    4.15  
    4.16 -end
    4.17 +end;
     5.1 --- a/src/HOL/Tools/SMT2/smt2_failure.ML	Thu Jun 12 01:00:49 2014 +0200
     5.2 +++ b/src/HOL/Tools/SMT2/smt2_failure.ML	Thu Jun 12 01:00:49 2014 +0200
     5.3 @@ -14,7 +14,7 @@
     5.4      Other_Failure of string
     5.5    val string_of_failure: failure -> string
     5.6    exception SMT of failure
     5.7 -end
     5.8 +end;
     5.9  
    5.10  structure SMT2_Failure: SMT2_FAILURE =
    5.11  struct
    5.12 @@ -37,4 +37,4 @@
    5.13  
    5.14  exception SMT of failure
    5.15  
    5.16 -end
    5.17 +end;
     6.1 --- a/src/HOL/Tools/SMT2/smt2_normalize.ML	Thu Jun 12 01:00:49 2014 +0200
     6.2 +++ b/src/HOL/Tools/SMT2/smt2_normalize.ML	Thu Jun 12 01:00:49 2014 +0200
     6.3 @@ -16,7 +16,7 @@
     6.4    type extra_norm = Proof.context -> thm list * thm list -> thm list * thm list
     6.5    val add_extra_norm: SMT2_Util.class * extra_norm -> Context.generic -> Context.generic
     6.6    val normalize: Proof.context -> thm list -> (int * thm) list
     6.7 -end
     6.8 +end;
     6.9  
    6.10  structure SMT2_Normalize: SMT2_NORMALIZE =
    6.11  struct
    6.12 @@ -264,7 +264,6 @@
    6.13  fun gen_normalize ctxt iwthms = map_filter (gen_norm1_safe ctxt) iwthms
    6.14  
    6.15  
    6.16 -
    6.17  (* unfolding of definitions and theory-specific rewritings *)
    6.18  
    6.19  fun expand_head_conv cv ct =
    6.20 @@ -456,7 +455,6 @@
    6.21    |> burrow_ids add_nat_embedding
    6.22  
    6.23  
    6.24 -
    6.25  (* overall normalization *)
    6.26  
    6.27  type extra_norm = Proof.context -> thm list * thm list -> thm list * thm list
    6.28 @@ -526,4 +524,4 @@
    6.29    setup_abs_min_max #>
    6.30    setup_nat_as_int))
    6.31  
    6.32 -end
    6.33 +end;
     7.1 --- a/src/HOL/Tools/SMT2/smt2_real.ML	Thu Jun 12 01:00:49 2014 +0200
     7.2 +++ b/src/HOL/Tools/SMT2/smt2_real.ML	Thu Jun 12 01:00:49 2014 +0200
     7.3 @@ -118,4 +118,4 @@
     7.4    Z3_New_Interface.add_mk_builtins z3_mk_builtins #>
     7.5    Z3_New_Replay_Util.add_simproc real_linarith_proc))
     7.6  
     7.7 -end
     7.8 +end;
     8.1 --- a/src/HOL/Tools/SMT2/smt2_solver.ML	Thu Jun 12 01:00:49 2014 +0200
     8.2 +++ b/src/HOL/Tools/SMT2/smt2_solver.ML	Thu Jun 12 01:00:49 2014 +0200
     8.3 @@ -38,12 +38,11 @@
     8.4    (*tactic*)
     8.5    val smt2_tac: Proof.context -> thm list -> int -> tactic
     8.6    val smt2_tac': Proof.context -> thm list -> int -> tactic
     8.7 -end
     8.8 +end;
     8.9  
    8.10  structure SMT2_Solver: SMT2_SOLVER =
    8.11  struct
    8.12  
    8.13 -
    8.14  (* interface to external solvers *)
    8.15  
    8.16  local
    8.17 @@ -298,4 +297,4 @@
    8.18  
    8.19  end
    8.20  
    8.21 -end
    8.22 +end;
     9.1 --- a/src/HOL/Tools/SMT2/smt2_systems.ML	Thu Jun 12 01:00:49 2014 +0200
     9.2 +++ b/src/HOL/Tools/SMT2/smt2_systems.ML	Thu Jun 12 01:00:49 2014 +0200
     9.3 @@ -12,7 +12,7 @@
     9.4      Z3_Non_Commercial_Declined
     9.5    val z3_non_commercial: unit -> z3_non_commercial
     9.6    val z3_extensions: bool Config.T
     9.7 -end
     9.8 +end;
     9.9  
    9.10  structure SMT2_Systems: SMT2_SYSTEMS =
    9.11  struct
    9.12 @@ -155,4 +155,4 @@
    9.13    SMT2_Solver.add_solver yices #>
    9.14    SMT2_Solver.add_solver z3)
    9.15  
    9.16 -end
    9.17 +end;
    10.1 --- a/src/HOL/Tools/SMT2/smt2_translate.ML	Thu Jun 12 01:00:49 2014 +0200
    10.2 +++ b/src/HOL/Tools/SMT2/smt2_translate.ML	Thu Jun 12 01:00:49 2014 +0200
    10.3 @@ -35,7 +35,7 @@
    10.4    (*translation*)
    10.5    val add_config: SMT2_Util.class * (Proof.context -> config) -> Context.generic -> Context.generic
    10.6    val translate: Proof.context -> string list -> (int * thm) list -> string * replay_data
    10.7 -end
    10.8 +end;
    10.9  
   10.10  structure SMT2_Translate: SMT2_TRANSLATE =
   10.11  struct
   10.12 @@ -54,7 +54,6 @@
   10.13    SQua of squant * string list * sterm spattern list * sterm
   10.14  
   10.15  
   10.16 -
   10.17  (* translation configuration *)
   10.18  
   10.19  type sign = {
   10.20 @@ -76,7 +75,6 @@
   10.21    assms: (int * thm) list }
   10.22  
   10.23  
   10.24 -
   10.25  (* translation context *)
   10.26  
   10.27  fun add_components_of_typ (Type (s, Ts)) =
   10.28 @@ -131,7 +129,6 @@
   10.29    end
   10.30  
   10.31  
   10.32 -
   10.33  (* preprocessing *)
   10.34  
   10.35  (** datatype declarations **)
   10.36 @@ -454,7 +451,6 @@
   10.37    in ((sign_of (header ts) dtyps trx', us), trx') end
   10.38  
   10.39  
   10.40 -
   10.41  (* translation *)
   10.42  
   10.43  structure Configs = Generic_Data
   10.44 @@ -521,4 +517,4 @@
   10.45      ||> replay_data_of ctxt2 rewrite_rules ithms
   10.46    end
   10.47  
   10.48 -end
   10.49 +end;
    11.1 --- a/src/HOL/Tools/SMT2/smt2_util.ML	Thu Jun 12 01:00:49 2014 +0200
    11.2 +++ b/src/HOL/Tools/SMT2/smt2_util.ML	Thu Jun 12 01:00:49 2014 +0200
    11.3 @@ -59,7 +59,7 @@
    11.4    val under_quant_conv: (Proof.context * cterm list -> conv) ->
    11.5      Proof.context -> conv
    11.6    val prop_conv: conv -> conv
    11.7 -end
    11.8 +end;
    11.9  
   11.10  structure SMT2_Util: SMT2_UTIL =
   11.11  struct
   11.12 @@ -221,4 +221,4 @@
   11.13      @{const Trueprop} $ _ => Conv.arg_conv cv ct
   11.14    | _ => raise CTERM ("not a property", [ct]))
   11.15  
   11.16 -end
   11.17 +end;
    12.1 --- a/src/HOL/Tools/SMT2/smtlib2.ML	Thu Jun 12 01:00:49 2014 +0200
    12.2 +++ b/src/HOL/Tools/SMT2/smtlib2.ML	Thu Jun 12 01:00:49 2014 +0200
    12.3 @@ -17,7 +17,7 @@
    12.4    val parse: string list -> tree
    12.5    val pretty_tree: tree -> Pretty.T
    12.6    val str_of: tree -> string
    12.7 -end
    12.8 +end;
    12.9  
   12.10  structure SMTLIB2: SMTLIB2 =
   12.11  struct
   12.12 @@ -37,7 +37,6 @@
   12.13  datatype unfinished = None | String of string | Symbol of string
   12.14  
   12.15  
   12.16 -
   12.17  (* utilities *)
   12.18  
   12.19  fun read_raw pred l cs =
   12.20 @@ -47,7 +46,6 @@
   12.21    | x => x)
   12.22  
   12.23  
   12.24 -
   12.25  (* numerals and decimals *)
   12.26  
   12.27  fun int_of cs = fst (read_int cs)
   12.28 @@ -60,7 +58,6 @@
   12.29    | (cs1, cs2) => (Num (int_of cs1), cs2))
   12.30  
   12.31  
   12.32 -
   12.33  (* binary numbers *)
   12.34  
   12.35  fun is_bin c = (c = "0" orelse c = "1")
   12.36 @@ -68,7 +65,6 @@
   12.37  fun read_bin l cs = read_raw is_bin l cs |>> Num o fst o read_radix_int 2
   12.38  
   12.39  
   12.40 -
   12.41  (* hex numbers *)
   12.42  
   12.43  val is_hex = member (op =) (raw_explode "0123456789abcdefABCDEF")
   12.44 @@ -85,7 +81,6 @@
   12.45  fun read_hex l cs = read_raw is_hex l cs |>> Num o unhex 0
   12.46  
   12.47  
   12.48 -
   12.49  (* symbols *)
   12.50  
   12.51  val symbol_chars = raw_explode "~!@$%^&*_+=<>.?/-" 
   12.52 @@ -98,7 +93,6 @@
   12.53  fun read_sym f l cs = read_raw is_sym l cs |>> f o implode
   12.54  
   12.55  
   12.56 -
   12.57  (* quoted tokens *)
   12.58  
   12.59  fun read_quoted stop (escape, replacement) cs =
   12.60 @@ -116,7 +110,6 @@
   12.61  fun read_symbol cs = read_quoted ["|"] ([], "") cs
   12.62  
   12.63  
   12.64 -
   12.65  (* core parser *)
   12.66  
   12.67  fun read _ [] rest tss = (rest, tss)
   12.68 @@ -172,7 +165,6 @@
   12.69  fun parse lines = finish (fold add_line lines (1, (None, [[]])))
   12.70  
   12.71  
   12.72 -
   12.73  (* pretty printer *)
   12.74  
   12.75  fun pretty_tree (Num i) = Pretty.str (string_of_int i)
   12.76 @@ -196,4 +188,4 @@
   12.77  
   12.78  val str_of = Pretty.str_of o pretty_tree
   12.79  
   12.80 -end
   12.81 +end;
    13.1 --- a/src/HOL/Tools/SMT2/smtlib2_interface.ML	Thu Jun 12 01:00:49 2014 +0200
    13.2 +++ b/src/HOL/Tools/SMT2/smtlib2_interface.ML	Thu Jun 12 01:00:49 2014 +0200
    13.3 @@ -11,7 +11,7 @@
    13.4    val add_logic: int * (term list -> string option) -> Context.generic -> Context.generic
    13.5    val translate_config: Proof.context -> SMT2_Translate.config
    13.6    val assert_index_of_name: string -> int
    13.7 -end
    13.8 +end;
    13.9  
   13.10  structure SMTLIB2_Interface: SMTLIB2_INTERFACE =
   13.11  struct
   13.12 @@ -156,4 +156,4 @@
   13.13    (setup_builtins #>
   13.14     SMT2_Translate.add_config (smtlib2C, translate_config)))
   13.15  
   13.16 -end
   13.17 +end;
    14.1 --- a/src/HOL/Tools/SMT2/z3_new_interface.ML	Thu Jun 12 01:00:49 2014 +0200
    14.2 +++ b/src/HOL/Tools/SMT2/z3_new_interface.ML	Thu Jun 12 01:00:49 2014 +0200
    14.3 @@ -19,7 +19,7 @@
    14.4    val mk_builtin_fun: Proof.context -> sym -> cterm list -> cterm option
    14.5  
    14.6    val is_builtin_theory_term: Proof.context -> term -> bool
    14.7 -end
    14.8 +end;
    14.9  
   14.10  structure Z3_New_Interface: Z3_NEW_INTERFACE =
   14.11  struct
   14.12 @@ -27,7 +27,6 @@
   14.13  val smtlib2_z3C = SMTLIB2_Interface.smtlib2C @ ["z3"]
   14.14  
   14.15  
   14.16 -
   14.17  (* interface *)
   14.18  
   14.19  local
   14.20 @@ -63,7 +62,6 @@
   14.21  end
   14.22  
   14.23  
   14.24 -
   14.25  (* constructors *)
   14.26  
   14.27  datatype sym = Sym of string * sym list
   14.28 @@ -185,7 +183,6 @@
   14.29      | _ => chained_mk_builtin_fun ctxt (get_mk_builtins ctxt) sym cts))
   14.30  
   14.31  
   14.32 -
   14.33  (* abstraction *)
   14.34  
   14.35  fun is_builtin_theory_term ctxt t =
   14.36 @@ -195,4 +192,4 @@
   14.37        (Const c, ts) => SMT2_Builtin.is_builtin_fun ctxt c ts
   14.38      | _ => false)
   14.39  
   14.40 -end
   14.41 +end;
    15.1 --- a/src/HOL/Tools/SMT2/z3_new_proof.ML	Thu Jun 12 01:00:49 2014 +0200
    15.2 +++ b/src/HOL/Tools/SMT2/z3_new_proof.ML	Thu Jun 12 01:00:49 2014 +0200
    15.3 @@ -194,7 +194,6 @@
    15.4             error (msg ^ ": " ^ SMTLIB2.str_of t)
    15.5  
    15.6  
    15.7 -
    15.8  (* handling of bound variables *)
    15.9  
   15.10  fun subst_of tyenv =
   15.11 @@ -269,7 +268,6 @@
   15.12    end
   15.13  
   15.14  
   15.15 -
   15.16  (* linearizing proofs and resolving types of bound variables *)
   15.17  
   15.18  fun has_step (tab, _) = Inttab.defined tab
   15.19 @@ -300,7 +298,6 @@
   15.20    rev (snd (snd (lin_proof ctxt Symtab.empty node (Inttab.empty, []))))
   15.21  
   15.22  
   15.23 -
   15.24  (* overall proof parser *)
   15.25  
   15.26  fun parse typs funs lines ctxt =
    16.1 --- a/src/HOL/Tools/SMT2/z3_new_real.ML	Thu Jun 12 01:00:49 2014 +0200
    16.2 +++ b/src/HOL/Tools/SMT2/z3_new_real.ML	Thu Jun 12 01:00:49 2014 +0200
    16.3 @@ -29,4 +29,4 @@
    16.4    SMTLIB2_Proof.add_term_parser real_term_parser #>
    16.5    Z3_New_Replay_Methods.add_arith_abstracter abstract))
    16.6  
    16.7 -end
    16.8 +end;
    17.1 --- a/src/HOL/Tools/SMT2/z3_new_replay.ML	Thu Jun 12 01:00:49 2014 +0200
    17.2 +++ b/src/HOL/Tools/SMT2/z3_new_replay.ML	Thu Jun 12 01:00:49 2014 +0200
    17.3 @@ -11,7 +11,7 @@
    17.4      ((string * ATP_Problem_Generate.stature) * thm) list -> term list -> term -> string list ->
    17.5      SMT2_Solver.parsed_proof
    17.6    val replay: Proof.context -> SMT2_Translate.replay_data -> string list -> thm
    17.7 -end
    17.8 +end;
    17.9  
   17.10  structure Z3_New_Replay: Z3_NEW_REPLAY =
   17.11  struct
   17.12 @@ -216,4 +216,4 @@
   17.13      Inttab.lookup proofs id |> the |> snd |> discharge rules outer_ctxt ctxt4
   17.14    end
   17.15  
   17.16 -end
   17.17 +end;
    18.1 --- a/src/HOL/Tools/SMT2/z3_new_replay_literals.ML	Thu Jun 12 01:00:49 2014 +0200
    18.2 +++ b/src/HOL/Tools/SMT2/z3_new_replay_literals.ML	Thu Jun 12 01:00:49 2014 +0200
    18.3 @@ -28,13 +28,11 @@
    18.4    val explode: bool -> bool -> bool -> term list -> thm -> thm list
    18.5    val join: bool -> littab -> term -> thm
    18.6    val prove_conj_disj_eq: cterm -> thm
    18.7 -end
    18.8 +end;
    18.9  
   18.10  structure Z3_New_Replay_Literals: Z3_NEW_REPLAY_LITERALS =
   18.11  struct
   18.12  
   18.13 -
   18.14 -
   18.15  (* literal table *)
   18.16  
   18.17  type littab = thm Termtab.table
   18.18 @@ -48,14 +46,12 @@
   18.19    Termtab.get_first (fn (t, thm) => if f t then SOME thm else NONE)
   18.20  
   18.21  
   18.22 -
   18.23  (* rules *)
   18.24  
   18.25  val true_thm = @{lemma "~False" by simp}
   18.26  val rewrite_true = @{lemma "True == ~ False" by simp}
   18.27  
   18.28  
   18.29 -
   18.30  (* properties and term operations *)
   18.31  
   18.32  val is_neg = (fn @{const Not} $ _ => true | _ => false)
   18.33 @@ -84,7 +80,6 @@
   18.34  val negate = Thm.apply (Thm.cterm_of @{theory} @{const Not})
   18.35  
   18.36  
   18.37 -
   18.38  (* proof tools *)
   18.39  
   18.40  (** explosion of conjunctions and disjunctions **)
   18.41 @@ -353,4 +348,4 @@
   18.42  
   18.43  end
   18.44  
   18.45 -end
   18.46 +end;
    19.1 --- a/src/HOL/Tools/SMT2/z3_new_replay_methods.ML	Thu Jun 12 01:00:49 2014 +0200
    19.2 +++ b/src/HOL/Tools/SMT2/z3_new_replay_methods.ML	Thu Jun 12 01:00:49 2014 +0200
    19.3 @@ -50,7 +50,7 @@
    19.4    val mp_oeq: z3_method
    19.5    val th_lemma: string -> z3_method
    19.6    val method_for: Z3_New_Proof.z3_rule -> z3_method
    19.7 -end
    19.8 +end;
    19.9  
   19.10  structure Z3_New_Replay_Methods: Z3_NEW_REPLAY_METHODS =
   19.11  struct
   19.12 @@ -58,7 +58,6 @@
   19.13  type z3_method = Proof.context -> thm list -> term -> thm
   19.14  
   19.15  
   19.16 -
   19.17  (* utility functions *)
   19.18  
   19.19  fun trace ctxt f = SMT2_Config.trace_msg ctxt f ()
   19.20 @@ -144,7 +143,6 @@
   19.21  fun quant_tac ctxt = Blast.blast_tac ctxt
   19.22  
   19.23  
   19.24 -
   19.25  (* plug-ins *)
   19.26  
   19.27  type abs_context = int * term Termtab.table
   19.28 @@ -174,7 +172,6 @@
   19.29  fun get_th_lemma_method ctxt = snd (Plugins.get (Context.Proof ctxt))
   19.30  
   19.31  
   19.32 -
   19.33  (* abstraction *)
   19.34  
   19.35  fun prove_abstract ctxt thms t tac f =
   19.36 @@ -279,13 +276,11 @@
   19.37    in abs u end
   19.38  
   19.39  
   19.40 -
   19.41  (* truth axiom *)
   19.42  
   19.43  fun true_axiom _ _ _ = @{thm TrueI}
   19.44  
   19.45  
   19.46 -
   19.47  (* modus ponens *)
   19.48  
   19.49  fun mp _ [p, p_eq_q] _ = discharge 1 [p_eq_q, p] iffD1
   19.50 @@ -294,27 +289,23 @@
   19.51  val mp_oeq = mp
   19.52  
   19.53  
   19.54 -
   19.55  (* reflexivity *)
   19.56  
   19.57  fun refl ctxt _ t = match_instantiate ctxt t @{thm refl}
   19.58  
   19.59  
   19.60 -
   19.61  (* symmetry *)
   19.62  
   19.63  fun symm _ [thm] _ = thm RS @{thm sym}
   19.64    | symm ctxt thms t = replay_rule_error ctxt Z3_New_Proof.Reflexivity thms t
   19.65  
   19.66  
   19.67 -
   19.68  (* transitivity *)
   19.69  
   19.70  fun trans _ [thm1, thm2] _ = thm1 RSN (1, thm2 RSN (2, @{thm trans}))
   19.71    | trans ctxt thms t = replay_rule_error ctxt Z3_New_Proof.Transitivity thms t
   19.72  
   19.73  
   19.74 -
   19.75  (* congruence *)
   19.76  
   19.77  fun ctac prems i st = st |> (
   19.78 @@ -345,7 +336,6 @@
   19.79    ("full", cong_full ctxt thms)] thms
   19.80  
   19.81  
   19.82 -
   19.83  (* quantifier introduction *)
   19.84  
   19.85  val quant_intro_rules = @{lemma
   19.86 @@ -360,7 +350,6 @@
   19.87    | quant_intro ctxt thms t = replay_rule_error ctxt Z3_New_Proof.Quant_Intro thms t
   19.88  
   19.89  
   19.90 -
   19.91  (* distributivity of conjunctions and disjunctions *)
   19.92  
   19.93  (* TODO: there are no tests with this proof rule *)
   19.94 @@ -368,7 +357,6 @@
   19.95    prove_abstract' ctxt t prop_tac (abstract_prop (dest_prop t))
   19.96  
   19.97  
   19.98 -
   19.99  (* elimination of conjunctions *)
  19.100  
  19.101  fun and_elim ctxt [thm] t =
  19.102 @@ -379,7 +367,6 @@
  19.103    | and_elim ctxt thms t = replay_rule_error ctxt Z3_New_Proof.And_Elim thms t
  19.104  
  19.105  
  19.106 -
  19.107  (* elimination of negated disjunctions *)
  19.108  
  19.109  fun not_or_elim ctxt [thm] t =
  19.110 @@ -391,7 +378,6 @@
  19.111        replay_rule_error ctxt Z3_New_Proof.Not_Or_Elim thms t
  19.112  
  19.113  
  19.114 -
  19.115  (* rewriting *)
  19.116  
  19.117  local
  19.118 @@ -452,19 +438,16 @@
  19.119  fun rewrite_star ctxt = rewrite ctxt
  19.120  
  19.121  
  19.122 -
  19.123  (* pulling quantifiers *)
  19.124  
  19.125  fun pull_quant ctxt _ t = prove ctxt t quant_tac
  19.126  
  19.127  
  19.128 -
  19.129  (* pushing quantifiers *)
  19.130  
  19.131  fun push_quant _ _ _ = raise Fail "unsupported" (* FIXME *)
  19.132  
  19.133  
  19.134 -
  19.135  (* elimination of unused bound variables *)
  19.136  
  19.137  val elim_all = @{lemma "P = Q ==> (ALL x. P) = Q" by fast}
  19.138 @@ -480,13 +463,11 @@
  19.139  fun elim_unused ctxt _ t = prove ctxt t (fn _ => elim_unused_tac)
  19.140  
  19.141  
  19.142 -
  19.143  (* destructive equality resolution *)
  19.144  
  19.145  fun dest_eq_res _ _ _ = raise Fail "dest_eq_res" (* FIXME *)
  19.146  
  19.147  
  19.148 -
  19.149  (* quantifier instantiation *)
  19.150  
  19.151  val quant_inst_rule = @{lemma "~P x | Q ==> ~(ALL x. P x) | Q" by fast}
  19.152 @@ -496,7 +477,6 @@
  19.153    THEN' rtac @{thm excluded_middle})
  19.154  
  19.155  
  19.156 -
  19.157  (* propositional lemma *)
  19.158  
  19.159  exception LEMMA of unit
  19.160 @@ -535,7 +515,6 @@
  19.161    | lemma ctxt thms t = replay_rule_error ctxt Z3_New_Proof.Lemma thms t
  19.162  
  19.163  
  19.164 -
  19.165  (* unit resolution *)
  19.166  
  19.167  fun abstract_unit (t as (@{const HOL.Not} $ (@{const HOL.disj} $ t1 $ t2))) =
  19.168 @@ -553,7 +532,6 @@
  19.169      (fn (prems, concl) => (prems, concl)))
  19.170  
  19.171  
  19.172 -
  19.173  (* iff-true *)
  19.174  
  19.175  val iff_true_rule = @{lemma "P ==> P = True" by fast}
  19.176 @@ -562,7 +540,6 @@
  19.177    | iff_true ctxt thms t = replay_rule_error ctxt Z3_New_Proof.Iff_True thms t
  19.178  
  19.179  
  19.180 -
  19.181  (* iff-false *)
  19.182  
  19.183  val iff_false_rule = @{lemma "~P ==> P = False" by fast}
  19.184 @@ -571,13 +548,11 @@
  19.185    | iff_false ctxt thms t = replay_rule_error ctxt Z3_New_Proof.Iff_False thms t
  19.186  
  19.187  
  19.188 -
  19.189  (* commutativity *)
  19.190  
  19.191  fun comm ctxt _ t = match_instantiate ctxt t @{thm eq_commute}
  19.192  
  19.193  
  19.194 -
  19.195  (* definitional axioms *)
  19.196  
  19.197  fun def_axiom_disj ctxt t =
  19.198 @@ -592,20 +567,17 @@
  19.199    ("disj", def_axiom_disj ctxt)] []
  19.200  
  19.201  
  19.202 -
  19.203  (* application of definitions *)
  19.204  
  19.205  fun apply_def _ [thm] _ = thm (* TODO: cover also the missing cases *)
  19.206    | apply_def ctxt thms t = replay_rule_error ctxt Z3_New_Proof.Apply_Def thms t
  19.207  
  19.208  
  19.209 -
  19.210  (* iff-oeq *)
  19.211  
  19.212  fun iff_oeq _ _ _ = raise Fail "iff_oeq" (* FIXME *)
  19.213  
  19.214  
  19.215 -
  19.216  (* negation normal form *)
  19.217  
  19.218  fun nnf_prop ctxt thms t =
  19.219 @@ -621,7 +593,6 @@
  19.220  fun nnf_neg ctxt = nnf ctxt Z3_New_Proof.Nnf_Neg
  19.221  
  19.222  
  19.223 -
  19.224  (* theory lemmas *)
  19.225  
  19.226  fun arith_th_lemma_tac ctxt prems =
  19.227 @@ -642,7 +613,6 @@
  19.228    | NONE => replay_error ctxt "Bad theory" (Z3_New_Proof.Th_Lemma name) thms)
  19.229  
  19.230  
  19.231 -
  19.232  (* mapping of rules to methods *)
  19.233  
  19.234  fun unsupported rule ctxt = replay_error ctxt "Unsupported" rule
  19.235 @@ -693,4 +663,4 @@
  19.236  
  19.237  fun method_for rule = with_tracing rule (choose rule)
  19.238  
  19.239 -end
  19.240 +end;
    20.1 --- a/src/HOL/Tools/SMT2/z3_new_replay_rules.ML	Thu Jun 12 01:00:49 2014 +0200
    20.2 +++ b/src/HOL/Tools/SMT2/z3_new_replay_rules.ML	Thu Jun 12 01:00:49 2014 +0200
    20.3 @@ -7,7 +7,7 @@
    20.4  signature Z3_NEW_REPLAY_RULES =
    20.5  sig
    20.6    val apply: Proof.context -> cterm -> thm option
    20.7 -end
    20.8 +end;
    20.9  
   20.10  structure Z3_New_Replay_Rules: Z3_NEW_REPLAY_RULES =
   20.11  struct
   20.12 @@ -51,4 +51,4 @@
   20.13  val _ = Theory.setup (Attrib.setup name (Attrib.add_del add del) description #>
   20.14    Global_Theory.add_thms_dynamic (name, Net.content o Data.get))
   20.15  
   20.16 -end
   20.17 +end;
    21.1 --- a/src/HOL/Tools/SMT2/z3_new_replay_util.ML	Thu Jun 12 01:00:49 2014 +0200
    21.2 +++ b/src/HOL/Tools/SMT2/z3_new_replay_util.ML	Thu Jun 12 01:00:49 2014 +0200
    21.3 @@ -23,13 +23,11 @@
    21.4    (*simpset*)
    21.5    val add_simproc: Simplifier.simproc -> Context.generic -> Context.generic
    21.6    val make_simpset: Proof.context -> thm list -> simpset
    21.7 -end
    21.8 +end;
    21.9  
   21.10  structure Z3_New_Replay_Util: Z3_NEW_REPLAY_UTIL =
   21.11  struct
   21.12  
   21.13 -
   21.14 -
   21.15  (* theorem nets *)
   21.16  
   21.17  fun thm_net_of f xthms =
   21.18 @@ -59,7 +57,6 @@
   21.19  end
   21.20  
   21.21  
   21.22 -
   21.23  (* proof combinators *)
   21.24  
   21.25  fun under_assumption f ct =
   21.26 @@ -68,7 +65,6 @@
   21.27  fun discharge p pq = Thm.implies_elim pq p
   21.28  
   21.29  
   21.30 -
   21.31  (* a faster COMP *)
   21.32  
   21.33  type compose_data = cterm list * (cterm -> cterm list) * thm
   21.34 @@ -82,7 +78,6 @@
   21.35    discharge thm (Thm.instantiate ([], cvs ~~ f (Thm.cprop_of thm)) rule)
   21.36  
   21.37  
   21.38 -
   21.39  (* simpset *)
   21.40  
   21.41  local
   21.42 @@ -152,4 +147,4 @@
   21.43  
   21.44  end
   21.45  
   21.46 -end
   21.47 +end;
    22.1 --- a/src/HOL/Word/Tools/smt2_word.ML	Thu Jun 12 01:00:49 2014 +0200
    22.2 +++ b/src/HOL/Word/Tools/smt2_word.ML	Thu Jun 12 01:00:49 2014 +0200
    22.3 @@ -9,12 +9,11 @@
    22.4  
    22.5  open Word_Lib
    22.6  
    22.7 +
    22.8  (* SMT-LIB logic *)
    22.9  
   22.10  fun smtlib_logic ts =
   22.11 -  if exists (Term.exists_type (Term.exists_subtype is_wordT)) ts
   22.12 -  then SOME "QF_AUFBV"
   22.13 -  else NONE
   22.14 +  if exists (Term.exists_type (Term.exists_subtype is_wordT)) ts then SOME "QF_AUFBV" else NONE
   22.15  
   22.16  
   22.17  (* SMT-LIB builtins *)
   22.18 @@ -141,4 +140,4 @@
   22.19    SMTLIB2_Interface.add_logic (20, smtlib_logic) #>
   22.20    setup_builtins))
   22.21  
   22.22 -end
   22.23 +end;