1.1 --- a/src/HOL/Tools/SMT2/smt2_normalize.ML	Thu Mar 13 14:48:20 2014 +0100
     1.2 +++ b/src/HOL/Tools/SMT2/smt2_normalize.ML	Thu Mar 13 14:48:20 2014 +0100
     1.3 @@ -10,8 +10,7 @@
     1.4    val atomize_conv: Proof.context -> conv
     1.5    type extra_norm = Proof.context -> thm list * thm list -> thm list * thm list
     1.6    val add_extra_norm: SMT2_Util.class * extra_norm -> Context.generic -> Context.generic
     1.7 -  val normalize: (int * (int option * thm)) list -> Proof.context ->
     1.8 -    (int * thm) list * Proof.context
     1.9 +  val normalize: Proof.context -> (int option * thm) list -> (int * thm) list
    1.10  end
    1.11  
    1.12  structure SMT2_Normalize: SMT2_NORMALIZE =
    1.13 @@ -497,7 +496,7 @@
    1.14    let
    1.15      val (is, thms) = split_list ithms
    1.16      val (thms', extra_thms) = f thms
    1.17 -  in (is ~~ thms') @ tag_list (fold Integer.max is 0 + 1) extra_thms end
    1.18 +  in (is ~~ thms') @ map (pair ~1) extra_thms end
    1.19  
    1.20  fun unfold2 ctxt ithms =
    1.21    ithms
    1.22 @@ -558,14 +557,14 @@
    1.23  
    1.24  end
    1.25  
    1.26 -fun normalize iwthms ctxt =
    1.27 -  iwthms
    1.28 +fun normalize ctxt wthms =
    1.29 +  wthms
    1.30 +  |> map_index I
    1.31    |> gen_normalize ctxt
    1.32    |> unfold1 ctxt
    1.33    |> monomorph ctxt
    1.34    |> unfold2 ctxt
    1.35    |> apply_extra_norms ctxt
    1.36 -  |> rpair ctxt
    1.37  
    1.38  val _ = Theory.setup (Context.theory_map (
    1.39    setup_atomize #>

     2.1 --- a/src/HOL/Tools/SMT2/smt2_solver.ML	Thu Mar 13 14:48:20 2014 +0100
     2.2 +++ b/src/HOL/Tools/SMT2/smt2_solver.ML	Thu Mar 13 14:48:20 2014 +0100
     2.3 @@ -26,7 +26,7 @@
     2.4    val add_solver: solver_config -> theory -> theory
     2.5    val solver_name_of: Proof.context -> string
     2.6    val available_solvers_of: Proof.context -> string list
     2.7 -  val apply_solver: Proof.context -> (int * (int option * thm)) list ->
     2.8 +  val apply_solver: Proof.context -> (int option * thm) list ->
     2.9      ((int * (int * thm)) list * Z3_New_Proof.z3_step list) * thm
    2.10    val default_max_relevant: Proof.context -> string -> int
    2.11  
    2.12 @@ -155,6 +155,18 @@
    2.13      ((int * (int * thm)) list * Z3_New_Proof.z3_step list) * thm) option }
    2.14  
    2.15  
    2.16 +(* check well-sortedness *)
    2.17 +
    2.18 +val has_topsort = Term.exists_type (Term.exists_subtype (fn
    2.19 +    TFree (_, []) => true
    2.20 +  | TVar (_, []) => true
    2.21 +  | _ => false))
    2.22 +
    2.23 +(* top sorts cause problems with atomization *)
    2.24 +fun check_topsort ctxt thm =
    2.25 +  if has_topsort (Thm.prop_of thm) then (SMT2_Normalize.drop_fact_warning ctxt thm; TrueI) else thm
    2.26 +
    2.27 +
    2.28  (* registry *)
    2.29  
    2.30  type solver_info = {
    2.31 @@ -227,36 +239,19 @@
    2.32    let val name = solver_name_of ctxt
    2.33    in (name, get_info ctxt name) end
    2.34  
    2.35 -fun apply_solver ctxt0 iwthms =
    2.36 +fun apply_solver ctxt wthms0 =
    2.37    let
    2.38 -    val (ithms, ctxt) = SMT2_Normalize.normalize iwthms ctxt0
    2.39 +    val wthms = map (apsnd (check_topsort ctxt)) wthms0
    2.40      val (name, {command, replay, ...}) = name_and_info_of ctxt
    2.41 -  in replay ctxt (invoke name command ithms ctxt) end
    2.42 +  in replay ctxt (invoke name command (SMT2_Normalize.normalize ctxt wthms) ctxt) end
    2.43  
    2.44  val default_max_relevant = #default_max_relevant oo get_info
    2.45  val supports_filter = #supports_filter o snd o name_and_info_of 
    2.46  
    2.47  
    2.48 -(* check well-sortedness *)
    2.49 -
    2.50 -val has_topsort = Term.exists_type (Term.exists_subtype (fn
    2.51 -    TFree (_, []) => true
    2.52 -  | TVar (_, []) => true
    2.53 -  | _ => false))
    2.54 -
    2.55 -(* without this test, we would run into problems when atomizing the rules: *)
    2.56 -fun check_topsort ctxt thm =
    2.57 -  if has_topsort (Thm.prop_of thm) then
    2.58 -    (SMT2_Normalize.drop_fact_warning ctxt thm; TrueI)
    2.59 -  else
    2.60 -    thm
    2.61 -
    2.62 -fun check_topsorts ctxt iwthms = map (apsnd (apsnd (check_topsort ctxt))) iwthms
    2.63 -
    2.64 -
    2.65  (* filter *)
    2.66  
    2.67 -val cnot = Thm.cterm_of @{theory} @{const Not}
    2.68 +val no_id = ~1
    2.69  
    2.70  fun smt2_filter ctxt goal xwfacts i time_limit =
    2.71    let
    2.72 @@ -267,67 +262,63 @@
    2.73        |> Config.put SMT2_Config.timeout (Time.toReal time_limit)
    2.74  
    2.75      val ({context=ctxt, prems, concl, ...}, _) = Subgoal.focus ctxt i goal
    2.76 -    fun negate ct = Thm.dest_comb ct ||> Thm.apply cnot |-> Thm.apply
    2.77 +    fun negate ct = Thm.dest_comb ct ||> Thm.apply @{cterm Not} |-> Thm.apply
    2.78      val cprop =
    2.79        (case try negate (Thm.rhs_of (SMT2_Normalize.atomize_conv ctxt concl)) of
    2.80          SOME ct => ct
    2.81        | NONE => raise SMT2_Failure.SMT (SMT2_Failure.Other_Failure "goal is not a HOL term"))
    2.82  
    2.83 -    val iwconjecture = (~1, (NONE, Thm.assume cprop))
    2.84 -    val iwprems = map (pair ~2 o pair NONE) prems
    2.85 -    val iwfacts = map_index I (map snd xwfacts)
    2.86 +    val wconjecture = (NONE, Thm.assume cprop)
    2.87 +    val wprems = map (pair NONE) prems
    2.88 +    val wfacts = map snd xwfacts
    2.89 +    val wthms = wconjecture :: wprems @ wfacts
    2.90 +    val iwthms = map_index I wthms
    2.91  
    2.92 -    val n = length iwfacts
    2.93 -    val xfacts = map (apsnd snd) xwfacts
    2.94 +    val conjecture_i = 0
    2.95 +    val facts_i = 1 + length wprems
    2.96    in
    2.97 -    iwconjecture :: iwprems @ iwfacts
    2.98 -    |> check_topsorts ctxt
    2.99 +    wthms
   2.100      |> apply_solver ctxt
   2.101      |> fst
   2.102      |> (fn (iidths0, z3_proof) =>
   2.103 -      let val iidths = if supports_filter ctxt then iidths0 else map (apsnd (apfst (K ~1))) iwfacts
   2.104 +      let
   2.105 +        val iidths = if supports_filter ctxt then iidths0 else map (apsnd (apfst (K no_id))) iwthms
   2.106        in
   2.107          {outcome = NONE, 
   2.108           conjecture_id =
   2.109 -           the_default ~1 (Option.map fst (AList.lookup (op =) iidths (fst iwconjecture))),
   2.110 -         helper_ids = map_filter (fn (i, (id, th)) => if i >= n then SOME (id, th) else NONE) iidths,
   2.111 -         fact_ids = map_filter (fn (i, (id, _)) => try (apsnd (nth xfacts)) (id, i)) iidths,
   2.112 +           the_default no_id (Option.map fst (AList.lookup (op =) iidths conjecture_i)),
   2.113 +         helper_ids = map_filter (try (fn (~1, idth) => idth)) iidths,
   2.114 +         fact_ids = map_filter (fn (i, (id, _)) =>
   2.115 +           try (apsnd (apsnd snd o nth xwfacts)) (id, i - facts_i)) iidths,
   2.116           z3_proof = z3_proof}
   2.117        end)
   2.118    end
   2.119 -  handle SMT2_Failure.SMT fail => {outcome = SOME fail, conjecture_id = ~1, helper_ids = [],
   2.120 +  handle SMT2_Failure.SMT fail => {outcome = SOME fail, conjecture_id = no_id, helper_ids = [],
   2.121      fact_ids = [], z3_proof = []}
   2.122  
   2.123  
   2.124  (* SMT tactic *)
   2.125  
   2.126  local
   2.127 -  fun trace_assumptions ctxt iwfacts iidths =
   2.128 -    let
   2.129 -      val wfacts =
   2.130 -        iidths
   2.131 -        |> map fst
   2.132 -        |> filter (fn i => i >= 0)
   2.133 -        |> map_filter (AList.lookup (op =) iwfacts)
   2.134 -    in
   2.135 +  fun trace_assumptions ctxt wfacts iidths =
   2.136 +    let val used = map_filter (try (snd o nth wfacts) o fst) iidths in
   2.137        if Config.get ctxt SMT2_Config.trace_used_facts andalso length wfacts > 0 then
   2.138          tracing (Pretty.string_of (Pretty.big_list "SMT used facts:"
   2.139 -          (map (Display.pretty_thm ctxt o snd) wfacts)))
   2.140 +          (map (Display.pretty_thm ctxt) used)))
   2.141        else ()
   2.142      end
   2.143  
   2.144 -  fun solve ctxt iwfacts =
   2.145 -    iwfacts
   2.146 -    |> check_topsorts ctxt
   2.147 +  fun solve ctxt wfacts =
   2.148 +    wfacts
   2.149      |> apply_solver ctxt
   2.150 -    |>> apfst (trace_assumptions ctxt iwfacts)
   2.151 +    |>> apfst (trace_assumptions ctxt wfacts)
   2.152      |> snd
   2.153  
   2.154    fun str_of ctxt fail =
   2.155      SMT2_Failure.string_of_failure ctxt fail
   2.156      |> prefix ("Solver " ^ SMT2_Config.solver_of ctxt ^ ": ")
   2.157  
   2.158 -  fun safe_solve ctxt iwfacts = SOME (solve ctxt iwfacts)
   2.159 +  fun safe_solve ctxt wfacts = SOME (solve ctxt wfacts)
   2.160      handle
   2.161        SMT2_Failure.SMT (fail as SMT2_Failure.Counterexample _) =>
   2.162          (SMT2_Config.verbose_msg ctxt (str_of ctxt) fail; NONE)
   2.163 @@ -337,17 +328,14 @@
   2.164            "configuration option " ^ quote (Config.name_of SMT2_Config.timeout) ^ " might help)")
   2.165      | SMT2_Failure.SMT fail => error (str_of ctxt fail)
   2.166  
   2.167 -  fun tag_rules thms = map_index (apsnd (pair NONE)) thms
   2.168 -  fun tag_prems thms = map (pair ~1 o pair NONE) thms
   2.169 -
   2.170    fun resolve (SOME thm) = rtac thm 1
   2.171      | resolve NONE = no_tac
   2.172  
   2.173    fun tac prove ctxt rules =
   2.174      CONVERSION (SMT2_Normalize.atomize_conv ctxt)
   2.175      THEN' rtac @{thm ccontr}
   2.176 -    THEN' SUBPROOF (fn {context, prems, ...} =>
   2.177 -      resolve (prove context (tag_rules rules @ tag_prems prems))) ctxt
   2.178 +    THEN' SUBPROOF (fn {context = ctxt, prems, ...} =>
   2.179 +      resolve (prove ctxt (map (pair NONE) (rules @ prems)))) ctxt
   2.180  in
   2.181  
   2.182  val smt2_tac = tac safe_solve