# HG changeset patch
# User boehmes
# Date 1256041322 -7200
# Node ID 4fb8a33f74d69d9fbd5394d2fec11e55d9e62269
# Parent  b73b74fe23c330cb09928d25abcdba92becececd
eliminated extraneous wrapping of public records,
replaced simp_tac by best_tac (simplifier failed),
less strict condition for rewrite (can also handle equations with single literal on left-hand side)

diff -r b73b74fe23c3 -r 4fb8a33f74d6 src/HOL/SMT/Tools/cvc3_solver.ML
--- a/src/HOL/SMT/Tools/cvc3_solver.ML	Tue Oct 20 12:06:17 2009 +0200
+++ b/src/HOL/SMT/Tools/cvc3_solver.ML	Tue Oct 20 14:22:02 2009 +0200
@@ -31,7 +31,7 @@
     val p = Pretty.big_list (cex_kind real ^ " found:") (map Pretty.str ls')
   in error (Pretty.string_of p) end
 
-fun core_oracle (SMT_Solver.ProofData {context, output, recon, ...}) =
+fun core_oracle ({context, output, recon, ...} : SMT_Solver.proof_data) =
   let
     val empty_line = (fn "" => true | _ => false)
     val split_first = (fn [] => ("", []) | l :: ls => (l, ls))
@@ -43,12 +43,11 @@
     else error (solver_name ^ " failed")
   end
 
-fun smtlib_solver oracle _ =
-  SMT_Solver.SolverConfig {
-    command = {env_var=env_var, remote_name=solver_name},
-    arguments = options,
-    interface = SMTLIB_Interface.interface,
-    reconstruct = oracle }
+fun smtlib_solver oracle _ = {
+  command = {env_var=env_var, remote_name=solver_name},
+  arguments = options,
+  interface = SMTLIB_Interface.interface,
+  reconstruct = oracle }
 
 val setup =
   Thm.add_oracle (Binding.name solver_name, core_oracle) #-> (fn (_, oracle) =>
diff -r b73b74fe23c3 -r 4fb8a33f74d6 src/HOL/SMT/Tools/smt_solver.ML
--- a/src/HOL/SMT/Tools/smt_solver.ML	Tue Oct 20 12:06:17 2009 +0200
+++ b/src/HOL/SMT/Tools/smt_solver.ML	Tue Oct 20 14:22:02 2009 +0200
@@ -8,17 +8,15 @@
 sig
   exception SMT_COUNTEREXAMPLE of bool * term list
 
-  datatype interface = Interface of {
+  type interface = {
     normalize: SMT_Normalize.config list,
     translate: SMT_Translate.config }
-
-  datatype proof_data = ProofData of {
+  type proof_data = {
     context: Proof.context,
     output: string list,
     recon: SMT_Translate.recon,
     assms: thm list option }
-
-  datatype solver_config = SolverConfig of {
+  type solver_config = {
     command: {env_var: string, remote_name: string},
     arguments: string list,
     interface: interface,
@@ -58,17 +56,17 @@
 exception SMT_COUNTEREXAMPLE of bool * term list
 
 
-datatype interface = Interface of {
+type interface = {
   normalize: SMT_Normalize.config list,
   translate: SMT_Translate.config }
 
-datatype proof_data = ProofData of {
+type proof_data = {
   context: Proof.context,
   output: string list,
   recon: SMT_Translate.recon,
   assms: thm list option }
 
-datatype solver_config = SolverConfig of {
+type solver_config = {
   command: {env_var: string, remote_name: string},
   arguments: string list,
   interface: interface,
@@ -144,12 +142,12 @@
 end
 
 fun make_proof_data ctxt ((recon, thms), ls) =
-  ProofData {context=ctxt, output=ls, recon=recon, assms=SOME thms}
+  {context=ctxt, output=ls, recon=recon, assms=SOME thms}
 
 fun gen_solver solver ctxt prems =
   let
-    val SolverConfig {command, arguments, interface, reconstruct} = solver ctxt
-    val Interface {normalize=nc, translate=tc} = interface
+    val {command, arguments, interface, reconstruct} = solver ctxt
+    val {normalize=nc, translate=tc} = interface
     val thy = ProofContext.theory_of ctxt
   in
     SMT_Normalize.normalize nc ctxt prems
diff -r b73b74fe23c3 -r 4fb8a33f74d6 src/HOL/SMT/Tools/smt_translate.ML
--- a/src/HOL/SMT/Tools/smt_translate.ML	Tue Oct 20 12:06:17 2009 +0200
+++ b/src/HOL/SMT/Tools/smt_translate.ML	Tue Oct 20 14:22:02 2009 +0200
@@ -34,29 +34,29 @@
   val bv_extract: (int -> int -> string) -> builtin_fun
 
   (* configuration options *)
-  datatype prefixes = Prefixes of {
+  type prefixes = {
     var_prefix: string,
     typ_prefix: string,
     fun_prefix: string,
     pred_prefix: string }
-  datatype markers = Markers of {
+  type markers = {
     term_marker: string,
     formula_marker: string }
-  datatype builtins = Builtins of {
+  type builtins = {
     builtin_typ: typ -> string option,
     builtin_num: int * typ -> string option,
     builtin_fun: bool -> builtin_table }
-  datatype sign = Sign of {
+  type sign = {
     typs: string list,
     funs: (string * (string list * string)) list,
     preds: (string * string list) list }
-  datatype config = Config of {
+  type config = {
     strict: bool,
     prefixes: prefixes,
     markers: markers,
     builtins: builtins,
     serialize: sign -> (string, string) sterm list -> TextIO.outstream -> unit}
-  datatype recon = Recon of {typs: typ Symtab.table, terms: term Symtab.table}
+  type recon = {typs: typ Symtab.table, terms: term Symtab.table}
 
   val translate: config -> theory -> thm list -> TextIO.outstream ->
     recon * thm list
@@ -159,29 +159,29 @@
 
 (* Configuration options *)
 
-datatype prefixes = Prefixes of {
+type prefixes = {
   var_prefix: string,
   typ_prefix: string,
   fun_prefix: string,
   pred_prefix: string }
-datatype markers = Markers of {
+type markers = {
   term_marker: string,
   formula_marker: string }
-datatype builtins = Builtins of {
+type builtins = {
   builtin_typ: typ -> string option,
   builtin_num: int * typ -> string option,
   builtin_fun: bool -> builtin_table }
-datatype sign = Sign of {
+type sign = {
   typs: string list,
   funs: (string * (string list * string)) list,
   preds: (string * string list) list }
-datatype config = Config of {
+type config = {
   strict: bool,
   prefixes: prefixes,
   markers: markers,
   builtins: builtins,
   serialize: sign -> (string, string) sterm list -> TextIO.outstream -> unit}
-datatype recon = Recon of {typs: typ Symtab.table, terms: term Symtab.table}
+type recon = {typs: typ Symtab.table, terms: term Symtab.table}
 
 
 (* Translate Isabelle/HOL terms into SMT intermediate terms.
@@ -409,7 +409,7 @@
   fun add_typ x (typs, funs, preds) = (Typtab.update x typs, funs, preds)
   fun add_fun true x (typs, funs, preds) = (typs, Termtab.update x funs, preds)
     | add_fun false x (typs, funs, preds) = (typs, funs, Termtab.update x preds)
-  fun make_sign (typs, funs, preds) = Sign {
+  fun make_sign (typs, funs, preds) = {
     typs = map snd (Typtab.dest typs),
     funs = map snd (Termtab.dest funs),
     preds = map (apsnd fst o snd) (Termtab.dest preds) }
@@ -418,11 +418,11 @@
       val rTs = Typtab.dest typs |> map swap |> Symtab.make
       val rts = Termtab.dest funs @ Termtab.dest preds
         |> map (apfst fst o swap) |> Symtab.make
-    in Recon {typs=rTs, terms=rts} end
+    in {typs=rTs, terms=rts} end
 
   fun either f g x = (case f x of NONE => g x | y => y)
 
-  fun rep_typ (Builtins {builtin_typ, ...}) T (st as (vars, ns, sgn)) =
+  fun rep_typ ({builtin_typ, ...} : builtins) T (st as (vars, ns, sgn)) =
     (case either builtin_typ (lookup_typ sgn) T of
       SOME n => (n, st)
     | NONE =>
@@ -444,16 +444,16 @@
           val (n, ns') = fresh_fun loc ns
         in (n, (vars, ns', add_fun loc (t, (n, uns)) sgn)) end)
 
-  fun rep_num (bs as Builtins {builtin_num, ...}) (i, T) st =
+  fun rep_num (bs as {builtin_num, ...} : builtins) (i, T) st =
     (case builtin_num (i, T) of
       SOME n => (n, st)
     | NONE => rep_fun bs true (HOLogic.mk_number T i) T 0 st)
 in
 fun signature_of prefixes markers builtins thy ts =
   let
-    val Prefixes {var_prefix, typ_prefix, fun_prefix, pred_prefix} = prefixes
-    val Markers {formula_marker, term_marker} = markers
-    val Builtins {builtin_fun, ...} = builtins
+    val {var_prefix, typ_prefix, fun_prefix, pred_prefix} = prefixes
+    val {formula_marker, term_marker} = markers
+    val {builtin_fun, ...} = builtins
 
     fun sign loc t =
       (case t of
@@ -493,7 +493,7 @@
 (* Combination of all translation functions and invocation of serialization. *)
 
 fun translate config thy thms stream =
-  let val Config {strict, prefixes, markers, builtins, serialize} = config
+  let val {strict, prefixes, markers, builtins, serialize} = config
   in
     map Thm.prop_of thms
     |> SMT_Monomorph.monomorph thy
diff -r b73b74fe23c3 -r 4fb8a33f74d6 src/HOL/SMT/Tools/smtlib_interface.ML
--- a/src/HOL/SMT/Tools/smtlib_interface.ML	Tue Oct 20 12:06:17 2009 +0200
+++ b/src/HOL/SMT/Tools/smtlib_interface.ML	Tue Oct 20 14:22:02 2009 +0200
@@ -109,7 +109,7 @@
           | wr_pat (T.SNoPat ts) = wrp "nopat" ts
       in par (wr_quant q #> fold wr_var vs #> wre b #> fold wr_pat ps) end)
 
-fun serialize attributes (T.Sign {typs, funs, preds}) ts stream =
+fun serialize attributes ({typs, funs, preds} : T.sign) ts stream =
   let
     fun wr_decl (n, Ts) = wr_line (sep (par (wr n #> fold wr1 Ts)))
   in
@@ -135,14 +135,14 @@
 
 (* SMT solver interface using the SMT-LIB input format *)
 
-val basic_builtins = T.Builtins {
+val basic_builtins = {
   builtin_typ = builtin_typ,
   builtin_num = builtin_num,
   builtin_fun = (fn true => builtin_funcs | false => builtin_preds) }
 
 val default_attributes = [":logic AUFLIRA", ":status unknown"]
 
-fun gen_interface builtins attributes = SMT_Solver.Interface {
+fun gen_interface builtins attributes = {
   normalize = [
     SMT_Normalize.RewriteTrivialLets,
     SMT_Normalize.RewriteNegativeNumerals,
@@ -150,14 +150,14 @@
     SMT_Normalize.AddAbsMinMaxRules,
     SMT_Normalize.AddPairRules,
     SMT_Normalize.AddFunUpdRules ],
-  translate = T.Config {
+  translate = {
     strict = true,
-    prefixes = T.Prefixes {
+    prefixes = {
       var_prefix = "x",
       typ_prefix = "T",
       fun_prefix = "uf_",
       pred_prefix = "up_" },
-    markers = T.Markers {
+    markers = {
       term_marker = term_marker,
       formula_marker = formula_marker },
     builtins = builtins,
diff -r b73b74fe23c3 -r 4fb8a33f74d6 src/HOL/SMT/Tools/yices_solver.ML
--- a/src/HOL/SMT/Tools/yices_solver.ML	Tue Oct 20 12:06:17 2009 +0200
+++ b/src/HOL/SMT/Tools/yices_solver.ML	Tue Oct 20 14:22:02 2009 +0200
@@ -26,7 +26,7 @@
 
 structure S = SMT_Solver
 
-fun core_oracle (SMT_Solver.ProofData {context, output, recon, ...}) =
+fun core_oracle ({context, output, recon, ...} : SMT_Solver.proof_data) =
   let
     val empty_line = (fn "" => true | _ => false)
     val split_first = (fn [] => ("", []) | l :: ls => (l, ls))
@@ -38,12 +38,11 @@
     else error (solver_name ^ " failed")
   end
 
-fun smtlib_solver oracle _ =
-  SMT_Solver.SolverConfig {
-    command = {env_var=env_var, remote_name=solver_name},
-    arguments = options,
-    interface = SMTLIB_Interface.interface,
-    reconstruct = oracle }
+fun smtlib_solver oracle _ = {
+  command = {env_var=env_var, remote_name=solver_name},
+  arguments = options,
+  interface = SMTLIB_Interface.interface,
+  reconstruct = oracle }
 
 val setup =
   Thm.add_oracle (Binding.name solver_name, core_oracle) #-> (fn (_, oracle) =>
diff -r b73b74fe23c3 -r 4fb8a33f74d6 src/HOL/SMT/Tools/z3_interface.ML
--- a/src/HOL/SMT/Tools/z3_interface.ML	Tue Oct 20 12:06:17 2009 +0200
+++ b/src/HOL/SMT/Tools/z3_interface.ML	Tue Oct 20 14:22:02 2009 +0200
@@ -88,7 +88,7 @@
   (@{term word_sless}, "bvslt"),
   (@{term word_sle}, "bvsle")]
 
-val builtins = T.Builtins {
+val builtins = {
   builtin_typ = builtin_typ,
   builtin_num = builtin_num,
   builtin_fun = (fn true => builtin_funcs | false => builtin_preds) }
diff -r b73b74fe23c3 -r 4fb8a33f74d6 src/HOL/SMT/Tools/z3_model.ML
--- a/src/HOL/SMT/Tools/z3_model.ML	Tue Oct 20 12:06:17 2009 +0200
+++ b/src/HOL/SMT/Tools/z3_model.ML	Tue Oct 20 14:22:02 2009 +0200
@@ -47,7 +47,7 @@
 fun make_context (ttab, nctxt, vtab) =
   Context {ttab=ttab, nctxt=nctxt, vtab=vtab}
 
-fun empty_context (SMT_Translate.Recon {terms, ...}) =
+fun empty_context ({terms, ...} : SMT_Translate.recon) =
   let
     val ns = Symtab.fold (Term.add_free_names o snd) terms []
     val nctxt = Name.make_context ns
diff -r b73b74fe23c3 -r 4fb8a33f74d6 src/HOL/SMT/Tools/z3_proof.ML
--- a/src/HOL/SMT/Tools/z3_proof.ML	Tue Oct 20 12:06:17 2009 +0200
+++ b/src/HOL/SMT/Tools/z3_proof.ML	Tue Oct 20 14:22:02 2009 +0200
@@ -56,7 +56,7 @@
 fun make_context (Ttab, ttab, etab, ptab, nctxt) =
   Context {Ttab=Ttab, ttab=ttab, etab=etab, ptab=ptab, nctxt=nctxt}
 
-fun empty_context thy (SMT_Translate.Recon {typs, terms=ttab}) =
+fun empty_context thy ({typs, terms=ttab} : SMT_Translate.recon) =
   let
     val ttab' = Symtab.map (fn @{term True} => @{term "~False"} | t => t) ttab
     val ns = Symtab.fold (Term.add_free_names o snd) ttab' []
diff -r b73b74fe23c3 -r 4fb8a33f74d6 src/HOL/SMT/Tools/z3_proof_rules.ML
--- a/src/HOL/SMT/Tools/z3_proof_rules.ML	Tue Oct 20 12:06:17 2009 +0200
+++ b/src/HOL/SMT/Tools/z3_proof_rules.ML	Tue Oct 20 14:22:02 2009 +0200
@@ -811,12 +811,12 @@
 
 (** |- ((ALL x. P x) | Q) = (ALL x. P x | Q) **)
 val pull_quant =
-  Thm o by_tac (Tactic.rtac @{thm refl} ORELSE' Simplifier.simp_tac HOL_ss)
+  Thm o by_tac (Tactic.rtac @{thm refl} ORELSE' Classical.best_tac HOL_cs)
 
 
 (** |- (ALL x. P x & Q x) = ((ALL x. P x) & (ALL x. Q x)) **)
 val push_quant =
-  Thm o by_tac (Tactic.rtac @{thm refl} ORELSE' Simplifier.simp_tac HOL_ss)
+  Thm o by_tac (Tactic.rtac @{thm refl} ORELSE' Classical.best_tac HOL_cs)
 
 
 (**
@@ -1131,15 +1131,12 @@
     iff_intro (under_assumption (contra_left conj) ct) (contra_right ct)
 
   fun conj_disj ct =
-    let
-      val cp as (cl, _) = Thm.dest_binop (Thm.dest_arg ct)
-      val (lhs, rhs) = pairself Thm.term_of cp
+    let val cp as (cl, cr) = Thm.dest_binop (Thm.dest_arg ct)
     in
-      if is_conj lhs andalso rhs = @{term False}
-      then contradiction true cl
-      else if is_disj lhs andalso rhs = @{term "~False"}
-      then contrapos2 (contradiction false o fst) cp
-      else prove_conj_disj_eq (Thm.dest_arg ct)
+      (case Thm.term_of cr of
+        @{term False} => contradiction true cl
+      | @{term "~False"} => contrapos2 (contradiction false o fst) cp
+      | _ => prove_conj_disj_eq (Thm.dest_arg ct))
     end
 
   val distinct =
diff -r b73b74fe23c3 -r 4fb8a33f74d6 src/HOL/SMT/Tools/z3_solver.ML
--- a/src/HOL/SMT/Tools/z3_solver.ML	Tue Oct 20 12:06:17 2009 +0200
+++ b/src/HOL/SMT/Tools/z3_solver.ML	Tue Oct 20 14:22:02 2009 +0200
@@ -52,22 +52,21 @@
     else error (solver_name ^ " failed")
   end
 
-fun core_oracle (SMT_Solver.ProofData {output, recon, ...}) =
+fun core_oracle ({output, recon, ...} : SMT_Solver.proof_data) =
   check_unsat recon output
   |> K @{cprop False}
 
-fun prover (SMT_Solver.ProofData {context, output, recon, assms}) =
+fun prover ({context, output, recon, assms} : SMT_Solver.proof_data) =
   check_unsat recon output
   |> Z3_Proof.reconstruct context assms recon
 
 fun solver oracle ctxt =
   let val with_proof = Config.get ctxt proofs
   in
-    SMT_Solver.SolverConfig {
-      command = {env_var=env_var, remote_name=solver_name},
-      arguments = cmdline_options ctxt,
-      interface = Z3_Interface.interface,
-      reconstruct = if with_proof then prover else oracle }
+    {command = {env_var=env_var, remote_name=solver_name},
+    arguments = cmdline_options ctxt,
+    interface = Z3_Interface.interface,
+    reconstruct = if with_proof then prover else oracle}
   end
 
 val setup =