# HG changeset patch # User boehmes # Date 1256809925 -3600 # Node ID 73af7831ba1e9a572af0d0923a2ea4c01c8f32ac # Parent dfda7461950926ff3e0155c15df7fafabd65688a simplified method syntax of "smt", full normalization of binders, corrected translation of patterns into intermediate format, ignore empty lines in Z3 output diff -r dfda74619509 -r 73af7831ba1e src/HOL/SMT/Examples/SMT_Examples.thy --- 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 \ 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 \ (\m. m dvd p --> m = 1 \ m = p))" lemma "prime_nat (4*m + 1) \ m \ (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 \ id True = True" using [[smt_cert="$ISABELLE_SMT/Examples/cert/z3_hol_03"]] - by (smt add: id_def) + by (smt id_def) lemma "i \ i1 \ i \ i2 \ ((f (i1 := v1)) (i2 := v2)) i = f i" using [[smt_cert="$ISABELLE_SMT/Examples/cert/z3_hol_04"]] @@ -694,7 +694,7 @@ lemma "map (\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 \ nat list \ int" @@ -721,7 +721,7 @@ eval_dioph ks (map (\x. x div 2) xs) = (l - eval_dioph ks (map (\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 \ (P [x] \ \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 \ 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 diff -r dfda74619509 -r 73af7831ba1e src/HOL/SMT/Tools/smt_normalize.ML --- 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 = diff -r dfda74619509 -r 73af7831ba1e src/HOL/SMT/Tools/smt_solver.ML --- 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)))) diff -r dfda74619509 -r 73af7831ba1e src/HOL/SMT/Tools/smt_translate.ML --- 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 = diff -r dfda74619509 -r 73af7831ba1e src/HOL/SMT/Tools/z3_solver.ML --- 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