simplified method syntax of "smt",
full normalization of binders,
corrected translation of patterns into intermediate format,
ignore empty lines in Z3 output

--- a/src/HOL/SMT/Examples/SMT_Examples.thy	Thu Oct 29 08:14:39 2009 +0100
+++ b/src/HOL/SMT/Examples/SMT_Examples.thy	Thu Oct 29 10:52:05 2009 +0100
@@ -62,7 +62,7 @@
   symm_f: "symm_f x y = symm_f y x"
 lemma "a = a \<and> symm_f a b = symm_f b a"
   using [[smt_cert="$ISABELLE_SMT/Examples/cert/z3_prop_09"]]
-  by (smt add: symm_f)
+  by (smt symm_f)
 
 (* 
 Taken from ~~/src/HOL/ex/SAT_Examples.thy.
@@ -524,7 +524,7 @@
   "prime_nat p = (1 < p \<and> (\<forall>m. m dvd p --> m = 1 \<or> m = p))"
 lemma "prime_nat (4*m + 1) \<Longrightarrow> m \<ge> (1::nat)"
   using [[smt_cert="$ISABELLE_SMT/Examples/cert/z3_nat_arith_07"]]
-  by (smt add: prime_nat_def)
+  by (smt prime_nat_def)
 
 
 section {* Bitvectors *}
@@ -686,7 +686,7 @@
 
 lemma "id 3 = 3 \<and> id True = True"
   using [[smt_cert="$ISABELLE_SMT/Examples/cert/z3_hol_03"]]
-  by (smt add: id_def)
+  by (smt id_def)
 
 lemma "i \<noteq> i1 \<and> i \<noteq> i2 \<Longrightarrow> ((f (i1 := v1)) (i2 := v2)) i = f i"
   using [[smt_cert="$ISABELLE_SMT/Examples/cert/z3_hol_04"]]
@@ -694,7 +694,7 @@
 
 lemma "map (\<lambda>i::nat. i + 1) [0, 1] = [1, 2]"
   using [[smt_cert="$ISABELLE_SMT/Examples/cert/z3_hol_05"]]
-  by (smt add: map.simps)
+  by (smt map.simps)
 
 lemma "(ALL x. P x) | ~ All P"
   using [[smt_cert="$ISABELLE_SMT/Examples/cert/z3_hol_06"]]
@@ -704,7 +704,7 @@
   "dec_10 n = (if n < 10 then n else dec_10 (n - 10))"
 lemma "dec_10 (4 * dec_10 4) = 6"
   using [[smt_cert="$ISABELLE_SMT/Examples/cert/z3_hol_07"]]
-  by (smt add: dec_10.simps)
+  by (smt dec_10.simps)
 
 axiomatization
   eval_dioph :: "int list \<Rightarrow> nat list \<Rightarrow> int"
@@ -721,7 +721,7 @@
     eval_dioph ks (map (\<lambda>x. x div 2) xs) =
       (l - eval_dioph ks (map (\<lambda>x. x mod 2) xs)) div 2)"
   using [[smt_cert="$ISABELLE_SMT/Examples/cert/z3_hol_08"]]
-  by (smt add: eval_dioph_mod[where n=2] eval_dioph_div_mult[where n=2])
+  by (smt eval_dioph_mod[where n=2] eval_dioph_div_mult[where n=2])
 
 
 section {* Monomorphization examples *}
@@ -730,7 +730,7 @@
 lemma poly_P: "P x \<and> (P [x] \<or> \<not>P[x])" by (simp add: P_def)
 lemma "P (1::int)"
   using [[smt_cert="$ISABELLE_SMT/Examples/cert/z3_mono_01"]]
-  by (smt add: poly_P)
+  by (smt poly_P)
 
 consts g :: "'a \<Rightarrow> nat"
 axioms
@@ -739,6 +739,6 @@
   g3: "g xs = length xs"
 lemma "g (Some (3::int)) = g (Some True)"
   using [[smt_cert="$ISABELLE_SMT/Examples/cert/z3_mono_02"]]
-  by (smt add: g1 g2 g3 list.size)
+  by (smt g1 g2 g3 list.size)
 
 end

--- a/src/HOL/SMT/Tools/smt_normalize.ML	Thu Oct 29 08:14:39 2009 +0100
+++ b/src/HOL/SMT/Tools/smt_normalize.ML	Thu Oct 29 10:52:05 2009 +0100
@@ -33,7 +33,8 @@
     AddFunUpdRules |
     AddAbsMinMaxRules
 
-  val normalize: config list -> Proof.context -> thm list -> cterm list * thm list
+  val normalize: config list -> Proof.context -> thm list ->
+    cterm list * thm list
 
   val setup: theory -> theory
 end
@@ -41,10 +42,42 @@
 structure SMT_Normalize: SMT_NORMALIZE =
 struct
 
-val norm_binder_conv = Conv.try_conv (More_Conv.rewrs_conv [
-  @{lemma "All P == ALL x. P x" by (rule reflexive)},
-  @{lemma "Ex P == EX x. P x" by (rule reflexive)},
-  @{lemma "Let c P == let x = c in P x" by (rule reflexive)}])
+local
+  val all1 = @{lemma "All P == ALL x. P x" by (rule reflexive)}
+  val all2 = @{lemma "All == (%P. ALL x. P x)" by (rule reflexive)}
+  val ex1 = @{lemma "Ex P == EX x. P x" by (rule reflexive)}
+  val ex2 = @{lemma "Ex == (%P. EX x. P x)" by (rule reflexive)}
+  val let1 = @{lemma "Let c P == let x = c in P x" by (rule reflexive)}
+  val let2 = @{lemma "Let c == (%P. let x = c in P x)" by (rule reflexive)}
+  val let3 = @{lemma "Let == (%c P. let x = c in P x)" by (rule reflexive)}
+
+  fun all_abs_conv cv ctxt =
+    Conv.abs_conv (all_abs_conv cv o snd) ctxt else_conv cv ctxt
+  fun keep_conv ctxt = More_Conv.binder_conv norm_conv ctxt
+  and unfold_conv rule ctxt =
+    Conv.rewr_conv rule then_conv all_abs_conv keep_conv ctxt
+  and unfold_let_conv rule ctxt =
+    Conv.rewr_conv rule then_conv
+    all_abs_conv (fn cx => Conv.combination_conv
+      (Conv.arg_conv (norm_conv cx)) (Conv.abs_conv (norm_conv o snd) cx)) ctxt
+  and norm_conv ctxt ct =
+    (case Thm.term_of ct of
+      Const (@{const_name All}, _) $ Abs _ => keep_conv
+    | Const (@{const_name All}, _) $ _ => unfold_conv all1
+    | Const (@{const_name All}, _) => unfold_conv all2
+    | Const (@{const_name Ex}, _) $ Abs _ => keep_conv
+    | Const (@{const_name Ex}, _) $ _ => unfold_conv ex1
+    | Const (@{const_name Ex}, _) => unfold_conv ex2
+    | Const (@{const_name Let}, _) $ _ $ Abs _ => keep_conv
+    | Const (@{const_name Let}, _) $ _ $ _ => unfold_let_conv let1
+    | Const (@{const_name Let}, _) $ _ => unfold_let_conv let2
+    | Const (@{const_name Let}, _) => unfold_let_conv let3
+    | Abs _ => Conv.abs_conv (norm_conv o snd)
+    | _ $ _ => Conv.comb_conv o norm_conv
+    | _ => K Conv.all_conv) ctxt ct
+in
+val norm_binder_conv = norm_conv
+end
 
 fun cert ctxt = Thm.cterm_of (ProofContext.theory_of ctxt)
 
@@ -65,10 +98,10 @@
   Conv.fconv_rule (
     Thm.beta_conversion true then_conv
     Thm.eta_conversion then_conv
-    More_Conv.bottom_conv (K norm_binder_conv) ctxt) #>
+    norm_binder_conv ctxt) #>
   norm_def ctxt #>
   Drule.forall_intr_vars #>
-  Conv.fconv_rule ObjectLogic.atomize
+  Conv.fconv_rule (ObjectLogic.atomize then_conv norm_binder_conv ctxt)
 
 fun instantiate_free (cv, ct) thm =
   if Term.exists_subterm (equal (Thm.term_of cv)) (Thm.prop_of thm)
@@ -321,11 +354,9 @@
         | Abs _ => at_lambda cvs
         | _ $ _ => in_comb (repl cvs) (repl cvs)
         | _ => none) ct
-      and at_lambda cvs ct cx =
-        let
-          val (thm1, cx') = in_abs repl cvs ct cx
-          val (thm2, cx'') = replace ctxt cvs (Thm.rhs_of thm1) cx'
-        in (Thm.transitive thm1 thm2, cx'') end
+      and at_lambda cvs ct =
+        in_abs repl cvs ct #-> (fn thm =>
+        replace ctxt cvs (Thm.rhs_of thm) #>> Thm.transitive thm)
     in repl [] end
 in
 fun lift_lambdas ctxt thms =

--- a/src/HOL/SMT/Tools/smt_solver.ML	Thu Oct 29 08:14:39 2009 +0100
+++ b/src/HOL/SMT/Tools/smt_solver.ML	Thu Oct 29 10:52:05 2009 +0100
@@ -230,7 +230,7 @@
 val smt_tac = smt_tac' false
 
 val smt_method =
-  Scan.optional (Scan.lift (Args.add -- Args.colon) |-- Attrib.thms) [] >>
+  Scan.optional Attrib.thms [] >>
   (fn thms => fn ctxt => METHOD (fn facts =>
     HEADGOAL (smt_tac ctxt (thms @ facts))))
 

--- a/src/HOL/SMT/Tools/smt_translate.ML	Thu Oct 29 08:14:39 2009 +0100
+++ b/src/HOL/SMT/Tools/smt_translate.ML	Thu Oct 29 10:52:05 2009 +0100
@@ -201,9 +201,9 @@
   fun dest_trigger (@{term trigger} $ tl $ t) = (HOLogic.dest_list tl, t)
     | dest_trigger t = ([], t)
 
-  fun pat f ps (Const (@{const_name pat}, _) $ p) = SPat (rev (f p :: ps))
-    | pat f ps (Const (@{const_name nopat}, _) $ p) = SNoPat (rev (f p :: ps))
-    | pat f ps (Const (@{const_name andpat}, _) $ p $ t) = pat f (f p :: ps) t
+  fun pat f ts (Const (@{const_name pat}, _) $ t) = SPat (rev (f t :: ts))
+    | pat f ts (Const (@{const_name nopat}, _) $ t) = SNoPat (rev (f t :: ts))
+    | pat f ts (Const (@{const_name andpat}, _) $ p $ t) = pat f (f t :: ts) p
     | pat _ _ t = raise TERM ("pat", [t])
 
   fun trans Ts t =

--- a/src/HOL/SMT/Tools/z3_solver.ML	Thu Oct 29 08:14:39 2009 +0100
+++ b/src/HOL/SMT/Tools/z3_solver.ML	Thu Oct 29 10:52:05 2009 +0100
@@ -43,8 +43,11 @@
 
 fun check_unsat recon output =
   let
-    val raw = not o String.isPrefix "WARNING" orf String.isPrefix "ERROR"
-    val (ls, l) = the_default ([], "") (try split_last (filter raw output))
+    fun jnk l =
+      String.isPrefix "WARNING" l orelse
+      String.isPrefix "ERROR" l orelse
+      forall Symbol.is_ascii_blank (Symbol.explode l)
+    val (ls, l) = the_default ([], "") (try split_last (filter_out jnk output))
   in
     if String.isPrefix "unsat" l then ls
     else if String.isPrefix "sat" l then raise_cex true recon ls