--- a/etc/symbols Thu Oct 29 11:41:39 2009 +0100
+++ b/etc/symbols Thu Oct 29 13:37:55 2009 +0100
@@ -244,10 +244,10 @@
\<Inter> code: 0x0022c2 font: Isabelle abbrev: Inter
\<union> code: 0x00222a font: Isabelle abbrev: Un
\<Union> code: 0x0022c3 font: Isabelle abbrev: Union
-\<squnion> code: 0x002294 font: Isabelle abbrev: |_|
-\<Squnion> code: 0x002a06 font: Isabelle abbrev: |||
-\<sqinter> code: 0x002293 font: Isabelle abbrev: &&
-\<Sqinter> code: 0x002a05 font: Isabelle abbrev: &&&
+\<squnion> code: 0x002294 font: Isabelle
+\<Squnion> code: 0x002a06 font: Isabelle
+\<sqinter> code: 0x002293 font: Isabelle
+\<Sqinter> code: 0x002a05 font: Isabelle
\<setminus> code: 0x002216 font: Isabelle
\<propto> code: 0x00221d font: Isabelle
\<uplus> code: 0x00228e font: Isabelle
--- a/src/HOL/SMT/Examples/SMT_Examples.thy Thu Oct 29 11:41:39 2009 +0100
+++ b/src/HOL/SMT/Examples/SMT_Examples.thy Thu Oct 29 13:37:55 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 11:41:39 2009 +0100
+++ b/src/HOL/SMT/Tools/smt_normalize.ML Thu Oct 29 13:37:55 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 11:41:39 2009 +0100
+++ b/src/HOL/SMT/Tools/smt_solver.ML Thu Oct 29 13:37:55 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 11:41:39 2009 +0100
+++ b/src/HOL/SMT/Tools/smt_translate.ML Thu Oct 29 13:37:55 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 11:41:39 2009 +0100
+++ b/src/HOL/SMT/Tools/z3_solver.ML Thu Oct 29 13:37:55 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