# HG changeset patch # User boehmes # Date 1290437143 -3600 # Node ID e080c9e68752e4d9c7fb4e422ac2f6bb1974c9d0 # Parent 798aad2229c02fe9c298bf37b4f65a8a6626b410 share and use more utility functions; slightly reduced complexity for Z3 proof rule 'rewrite' diff -r 798aad2229c0 -r e080c9e68752 src/HOL/Tools/SMT/smt_normalize.ML --- a/src/HOL/Tools/SMT/smt_normalize.ML Mon Nov 22 15:45:42 2010 +0100 +++ b/src/HOL/Tools/SMT/smt_normalize.ML Mon Nov 22 15:45:43 2010 +0100 @@ -28,12 +28,11 @@ structure SMT_Normalize: SMT_NORMALIZE = struct +structure U = SMT_Utils + infix 2 ?? fun (test ?? f) x = if test x then f x else x -fun if_conv c cv1 cv2 ct = (if c (Thm.term_of ct) then cv1 else cv2) ct -fun if_true_conv c cv = if_conv c cv Conv.all_conv - (* simplification of trivial distincts (distinct should have at least @@ -53,7 +52,7 @@ "SMT.distinct [x, y] = (x ~= y)" by (simp_all add: distinct_def)} fun distinct_conv _ = - if_true_conv is_trivial_distinct (Conv.rewrs_conv thms) + U.if_true_conv is_trivial_distinct (Conv.rewrs_conv thms) in fun trivial_distinct ctxt = map (apsnd ((Term.exists_subterm is_trivial_distinct o Thm.prop_of) ?? @@ -71,7 +70,7 @@ val thm = mk_meta_eq @{lemma "(case P of True => x | False => y) = (if P then x else y)" by simp} - val unfold_conv = if_true_conv is_bool_case (Conv.rewr_conv thm) + val unfold_conv = U.if_true_conv is_bool_case (Conv.rewr_conv thm) in fun rewrite_bool_cases ctxt = map (apsnd ((Term.exists_subterm is_bool_case o Thm.prop_of) ?? @@ -105,7 +104,7 @@ "Int.Bit1 (- k) = - Int.Bit1 (Int.pred k)" by simp_all (simp add: pred_def)} - fun pos_conv ctxt = if_conv (is_strange_number ctxt) + fun pos_conv ctxt = U.if_conv (is_strange_number ctxt) (Simplifier.rewrite (Simplifier.context ctxt pos_numeral_ss)) Conv.no_conv in @@ -282,7 +281,7 @@ | (_, ts) => forall (is_normed ctxt) ts)) in fun norm_binder_conv ctxt = - if_conv (is_normed ctxt) Conv.all_conv (norm_conv ctxt) + U.if_conv (is_normed ctxt) Conv.all_conv (norm_conv ctxt) end fun norm_def ctxt thm = @@ -321,13 +320,6 @@ (* lift lambda terms into additional rules *) local - val meta_eq = @{cpat "op =="} - val meta_eqT = hd (Thm.dest_ctyp (Thm.ctyp_of_term meta_eq)) - fun inst_meta cT = Thm.instantiate_cterm ([(meta_eqT, cT)], []) meta_eq - fun mk_meta_eq ct cu = Thm.mk_binop (inst_meta (Thm.ctyp_of_term ct)) ct cu - - fun cert ctxt = Thm.cterm_of (ProofContext.theory_of ctxt) - fun used_vars cvs ct = let val lookup = AList.lookup (op aconv) (map (` Thm.term_of) cvs) @@ -350,7 +342,7 @@ let val {T, ...} = Thm.rep_cterm ct' and n = Name.uu val (n', ctxt') = yield_singleton Variable.variant_fixes n ctxt - val cu = mk_meta_eq (cert ctxt (Free (n', T))) ct' + val cu = U.mk_cequals (U.certify ctxt (Free (n', T))) ct' val (eq, ctxt'') = yield_singleton Assumption.add_assumes cu ctxt' val defs' = Termtab.update (Thm.term_of ct', eq) defs in (apply_def cvs' eq, (ctxt'', defs')) end) diff -r 798aad2229c0 -r e080c9e68752 src/HOL/Tools/SMT/smt_translate.ML --- a/src/HOL/Tools/SMT/smt_translate.ML Mon Nov 22 15:45:42 2010 +0100 +++ b/src/HOL/Tools/SMT/smt_translate.ML Mon Nov 22 15:45:43 2010 +0100 @@ -52,6 +52,9 @@ structure SMT_Translate: SMT_TRANSLATE = struct +structure U = SMT_Utils + + (* intermediate term structure *) datatype squant = SForall | SExists @@ -107,13 +110,6 @@ (* utility functions *) -val dest_funT = - let - fun dest Ts 0 T = (rev Ts, T) - | dest Ts i (Type ("fun", [T, U])) = dest (T::Ts) (i-1) U - | dest _ _ T = raise TYPE ("dest_funT", [T], []) - in dest [] end - val quantifier = (fn @{const_name All} => SOME SForall | @{const_name Ex} => SOME SExists @@ -348,7 +344,7 @@ and new_dtyps dts cx = let fun new_decl i t = - let val (Ts, T) = dest_funT i (Term.fastype_of t) + let val (Ts, T) = U.dest_funT i (Term.fastype_of t) in fold_map transT Ts ##>> transT T ##>> new_fun func_prefix t NONE #>> swap @@ -396,7 +392,7 @@ | _ => raise TERM ("smt_translate", [t])) and transs t T ts = - let val (Us, U) = dest_funT (length ts) T + let val (Us, U) = U.dest_funT (length ts) T in fold_map transT Us ##>> transT U #-> (fn Up => fresh_fun func_prefix t (SOME Up) ##>> fold_map trans ts #>> SApp) diff -r 798aad2229c0 -r e080c9e68752 src/HOL/Tools/SMT/smt_utils.ML --- a/src/HOL/Tools/SMT/smt_utils.ML Mon Nov 22 15:45:42 2010 +0100 +++ b/src/HOL/Tools/SMT/smt_utils.ML Mon Nov 22 15:45:43 2010 +0100 @@ -9,6 +9,10 @@ val repeat: ('a -> 'a option) -> 'a -> 'a val repeat_yield: ('a -> 'b -> ('a * 'b) option) -> 'a -> 'b -> 'a * 'b + (* types *) + val split_type: typ -> typ * typ + val dest_funT: int -> typ -> typ list * typ + (* terms *) val dest_conj: term -> term * term val dest_disj: term -> term * term @@ -23,6 +27,7 @@ (* certified terms *) val certify: Proof.context -> term -> cterm + val typ_of: cterm -> typ val dest_cabs: cterm -> Proof.context -> cterm * Proof.context val dest_all_cabs: cterm -> Proof.context -> cterm * Proof.context val dest_cbinder: cterm -> Proof.context -> cterm * Proof.context @@ -50,6 +55,18 @@ in rep end +(* types *) + +fun split_type T = (Term.domain_type T, Term.range_type T) + +val dest_funT = + let + fun dest Ts 0 T = (rev Ts, T) + | dest Ts i (Type ("fun", [T, U])) = dest (T::Ts) (i-1) U + | dest _ _ T = raise TYPE ("not a function type", [T], []) + in dest [] end + + (* terms *) fun dest_conj (@{const HOL.conj} $ t $ u) = (t, u) @@ -77,6 +94,8 @@ fun certify ctxt = Thm.cterm_of (ProofContext.theory_of ctxt) +fun typ_of ct = #T (Thm.rep_cterm ct) + fun dest_cabs ct ctxt = (case Thm.term_of ct of Abs _ => @@ -93,7 +112,7 @@ val dest_all_cbinders = repeat_yield (try o dest_cbinder) -val mk_cprop = Thm.capply @{cterm Trueprop} +val mk_cprop = Thm.capply (Thm.cterm_of @{theory} @{const Trueprop}) fun dest_cprop ct = (case Thm.term_of ct of @@ -106,9 +125,9 @@ (* conversions *) -fun if_conv f cv1 cv2 ct = if f (Thm.term_of ct) then cv1 ct else cv2 ct +fun if_conv pred cv1 cv2 ct = if pred (Thm.term_of ct) then cv1 ct else cv2 ct -fun if_true_conv f cv = if_conv f cv Conv.all_conv +fun if_true_conv pred cv = if_conv pred cv Conv.all_conv fun binders_conv cv ctxt = Conv.binder_conv (binders_conv cv o snd) ctxt else_conv cv ctxt diff -r 798aad2229c0 -r e080c9e68752 src/HOL/Tools/SMT/z3_model.ML --- a/src/HOL/Tools/SMT/z3_model.ML Mon Nov 22 15:45:42 2010 +0100 +++ b/src/HOL/Tools/SMT/z3_model.ML Mon Nov 22 15:45:43 2010 +0100 @@ -13,6 +13,9 @@ structure Z3_Model: Z3_MODEL = struct +structure U = SMT_Utils + + (* counterexample expressions *) datatype expr = True | False | Number of int * int option | Value of int | @@ -214,15 +217,13 @@ fun mk_fun_upd T U = Const (@{const_name fun_upd}, [T --> U, T, U, T] ---> U) -fun split_type T = (Term.domain_type T, Term.range_type T) - fun mk_update ([], u) _ = u | mk_update ([t], u) f = - uncurry mk_fun_upd (split_type (Term.fastype_of f)) $ f $ t $ u + uncurry mk_fun_upd (U.split_type (Term.fastype_of f)) $ f $ t $ u | mk_update (t :: ts, u) f = let - val (dT, rT) = split_type (Term.fastype_of f) - val (dT', rT') = split_type rT + val (dT, rT) = U.split_type (Term.fastype_of f) + val (dT', rT') = U.split_type rT in mk_fun_upd dT rT $ f $ t $ mk_update (ts, u) (Term.absdummy (dT', Const ("_", rT'))) diff -r 798aad2229c0 -r e080c9e68752 src/HOL/Tools/SMT/z3_proof_methods.ML --- a/src/HOL/Tools/SMT/z3_proof_methods.ML Mon Nov 22 15:45:42 2010 +0100 +++ b/src/HOL/Tools/SMT/z3_proof_methods.ML Mon Nov 22 15:45:43 2010 +0100 @@ -13,6 +13,7 @@ struct structure U = SMT_Utils +structure T = Z3_Proof_Tools fun apply tac st = @@ -35,26 +36,24 @@ fun mk_inv_of ctxt ct = let - val T = #T (Thm.rep_cterm ct) - val dT = Term.domain_type T - val inv = U.certify ctxt (mk_inv_into dT (Term.range_type T)) + val (dT, rT) = U.split_type (U.typ_of ct) + val inv = U.certify ctxt (mk_inv_into dT rT) val univ = U.certify ctxt (mk_univ dT) in Thm.mk_binop inv univ ct end fun mk_inj_prop ctxt ct = let - val T = #T (Thm.rep_cterm ct) - val dT = Term.domain_type T - val inj = U.certify ctxt (mk_inj_on dT (Term.range_type T)) + val (dT, rT) = U.split_type (U.typ_of ct) + val inj = U.certify ctxt (mk_inj_on dT rT) val univ = U.certify ctxt (mk_univ dT) in U.mk_cprop (Thm.mk_binop inj ct univ) end val disjE = @{lemma "~P | Q ==> P ==> Q" by fast} -fun prove_inj_prop ctxt hdef lhs = +fun prove_inj_prop ctxt def lhs = let - val (ct, ctxt') = U.dest_all_cabs (Thm.rhs_of hdef) ctxt + val (ct, ctxt') = U.dest_all_cabs (Thm.rhs_of def) ctxt val rule = disjE OF [Object_Logic.rulify (Thm.assume lhs)] in Goal.init (mk_inj_prop ctxt' (Thm.dest_arg ct)) @@ -64,12 +63,12 @@ |> singleton (Variable.export ctxt' ctxt) end -fun prove_rhs ctxt hdef lhs rhs = - Goal.init rhs - |> apply (CONVERSION (Conv.top_sweep_conv (K (Conv.rewr_conv hdef)) ctxt)) - |> apply (REPEAT_ALL_NEW (Tactic.match_tac @{thms allI})) - |> apply (Tactic.rtac (@{thm inv_f_f} OF [prove_inj_prop ctxt hdef lhs])) - |> Goal.norm_result o Goal.finish ctxt +fun prove_rhs ctxt def lhs = + T.by_tac ( + CONVERSION (Conv.top_sweep_conv (K (Conv.rewr_conv def)) ctxt) + THEN' REPEAT_ALL_NEW (Tactic.match_tac @{thms allI}) + THEN' Tactic.rtac (@{thm inv_f_f} OF [prove_inj_prop ctxt def lhs])) #> + Thm.elim_implies def fun expand thm ct = @@ -80,18 +79,17 @@ val thm2 = Thm.instantiate (Thm.match (cpat, cr)) thm in Conv.arg_conv (Conv.binop_conv (Conv.rewrs_conv [thm1, thm2])) ct end -fun prove_lhs ctxt rhs lhs = +fun prove_lhs ctxt rhs = let val eq = Thm.symmetric (mk_meta_eq (Object_Logic.rulify (Thm.assume rhs))) in - Goal.init lhs - |> apply (CONVERSION (U.prop_conv (U.binders_conv (K (expand eq)) ctxt))) - |> apply (Simplifier.simp_tac HOL_ss) - |> Goal.finish ctxt + T.by_tac ( + CONVERSION (U.prop_conv (U.binders_conv (K (expand eq)) ctxt)) + THEN' Simplifier.simp_tac HOL_ss) end -fun mk_hdef ctxt rhs = +fun mk_inv_def ctxt rhs = let val (ct, ctxt') = U.dest_all_cbinders (U.dest_cprop rhs) ctxt val (cl, cv) = Thm.dest_binop ct @@ -102,9 +100,8 @@ fun prove_inj_eq ctxt ct = let val (lhs, rhs) = pairself U.mk_cprop (Thm.dest_binop (U.dest_cprop ct)) - val hdef = mk_hdef ctxt rhs - val lhs_thm = Thm.implies_intr rhs (prove_lhs ctxt rhs lhs) - val rhs_thm = Thm.implies_intr lhs (prove_rhs ctxt hdef lhs rhs) + val lhs_thm = prove_lhs ctxt rhs lhs + val rhs_thm = prove_rhs ctxt (mk_inv_def ctxt rhs) lhs rhs in lhs_thm COMP (rhs_thm COMP @{thm iffI}) end @@ -125,12 +122,10 @@ in -fun prove_injectivity ctxt ct = - ct - |> Goal.init - |> apply (CONVERSION (U.prop_conv (norm_conv ctxt))) - |> apply (CSUBGOAL (uncurry (Tactic.rtac o prove_inj_eq ctxt))) - |> Goal.norm_result o Goal.finish ctxt +fun prove_injectivity ctxt = + T.by_tac ( + CONVERSION (U.prop_conv (norm_conv ctxt)) + THEN' CSUBGOAL (uncurry (Tactic.rtac o prove_inj_eq ctxt))) end diff -r 798aad2229c0 -r e080c9e68752 src/HOL/Tools/SMT/z3_proof_parser.ML --- a/src/HOL/Tools/SMT/z3_proof_parser.ML Mon Nov 22 15:45:42 2010 +0100 +++ b/src/HOL/Tools/SMT/z3_proof_parser.ML Mon Nov 22 15:45:43 2010 +0100 @@ -103,24 +103,20 @@ context-independent modulo the current proof context to be able to use fast inference kernel rules during proof reconstruction. *) -fun certify ctxt = Thm.cterm_of (ProofContext.theory_of ctxt) - val maxidx_of = #maxidx o Thm.rep_cterm fun mk_inst ctxt vars = let val max = fold (Integer.max o fst) vars 0 val ns = fst (Variable.variant_fixes (replicate (max + 1) var_prefix) ctxt) - fun mk (i, v) = (v, certify ctxt (Free (nth ns i, #T (Thm.rep_cterm v)))) + fun mk (i, v) = (v, U.certify ctxt (Free (nth ns i, #T (Thm.rep_cterm v)))) in map mk vars end -val mk_prop = Thm.capply (Thm.cterm_of @{theory} @{const Trueprop}) - fun close ctxt (ct, vars) = let val inst = mk_inst ctxt vars val names = fold (Term.add_free_names o Thm.term_of o snd) inst [] - in (mk_prop (Thm.instantiate_cterm ([], inst) ct), names) end + in (U.mk_cprop (Thm.instantiate_cterm ([], inst) ct), names) end fun mk_bound thy (i, T) = @@ -195,7 +191,7 @@ |> Symtab.fold (Variable.declare_term o snd) terms fun cert @{const True} = not_false - | cert t = certify ctxt' t + | cert t = U.certify ctxt' t in (typs, Symtab.map (K cert) terms, Inttab.empty, Inttab.empty, [], ctxt') end @@ -210,7 +206,7 @@ SOME _ => cx | NONE => cx |> fresh_name (decl_prefix ^ n) |> (fn (m, (typs, terms, exprs, steps, vars, ctxt)) => - let val upd = Symtab.update (n, certify ctxt (Free (m, T))) + let val upd = Symtab.update (n, U.certify ctxt (Free (m, T))) in (typs, upd terms, exprs, steps, vars, ctxt) end)) fun mk_typ (typs, _, _, _, _, ctxt) (s as I.Sym (n, _)) = diff -r 798aad2229c0 -r e080c9e68752 src/HOL/Tools/SMT/z3_proof_reconstruction.ML --- a/src/HOL/Tools/SMT/z3_proof_reconstruction.ML Mon Nov 22 15:45:42 2010 +0100 +++ b/src/HOL/Tools/SMT/z3_proof_reconstruction.ML Mon Nov 22 15:45:43 2010 +0100 @@ -683,33 +683,29 @@ val unfold_conv = Conv.arg_conv (Conv.binop_conv (Conv.try_conv T.unfold_distinct_conv)) val prove_conj_disj_eq = T.with_conv unfold_conv L.prove_conj_disj_eq + + fun assume_prems ctxt thm = + Assumption.add_assumes (Drule.cprems_of thm) ctxt + |>> (fn thms => fold Thm.elim_implies thms thm) in -fun rewrite' ctxt simpset ths = Thm o with_conv ctxt ths (try_apply ctxt [] [ - named ctxt "conj/disj/distinct" prove_conj_disj_eq, - T.by_abstraction (true, false) ctxt [] (fn ctxt' => T.by_tac ( - NAMED ctxt' "simp (logic)" (Simplifier.simp_tac simpset) - THEN_ALL_NEW NAMED ctxt' "fast (logic)" (Classical.fast_tac HOL_cs))), - T.by_abstraction (false, true) ctxt [] (fn ctxt' => T.by_tac ( - NAMED ctxt' "simp (theory)" (Simplifier.simp_tac simpset) - THEN_ALL_NEW ( - NAMED ctxt' "fast (theory)" (Classical.fast_tac HOL_cs) - ORELSE' NAMED ctxt' "arith (theory)" (Arith_Data.arith_tac ctxt')))), - T.by_abstraction (true, true) ctxt [] (fn ctxt' => T.by_tac ( - NAMED ctxt' "simp (full)" (Simplifier.simp_tac simpset) - THEN_ALL_NEW ( - NAMED ctxt' "fast (full)" (Classical.fast_tac HOL_cs) - ORELSE' NAMED ctxt' "arith (full)" (Arith_Data.arith_tac ctxt')))), - named ctxt "injectivity" (M.prove_injectivity ctxt)]) - -fun rewrite simpset thms ct ctxt = (* FIXME: join with rewrite' *) - let - val thm = rewrite' ctxt simpset thms ct - val ord = Term_Ord.fast_term_ord o pairself Thm.term_of - val chyps = fold (Ord_List.union ord o #hyps o Thm.crep_thm o thm_of) thms [] - val new_chyps = Ord_List.subtract ord chyps (#hyps (Thm.crep_thm (thm_of thm))) - val (_, ctxt') = Assumption.add_assumes new_chyps ctxt - in (thm, ctxt') end +fun rewrite simpset ths ct ctxt = + apfst Thm (assume_prems ctxt (with_conv ctxt ths (try_apply ctxt [] [ + named ctxt "conj/disj/distinct" prove_conj_disj_eq, + T.by_abstraction (true, false) ctxt [] (fn ctxt' => T.by_tac ( + NAMED ctxt' "simp (logic)" (Simplifier.simp_tac simpset) + THEN_ALL_NEW NAMED ctxt' "fast (logic)" (Classical.fast_tac HOL_cs))), + T.by_abstraction (false, true) ctxt [] (fn ctxt' => T.by_tac ( + NAMED ctxt' "simp (theory)" (Simplifier.simp_tac simpset) + THEN_ALL_NEW ( + NAMED ctxt' "fast (theory)" (Classical.fast_tac HOL_cs) + ORELSE' NAMED ctxt' "arith (theory)" (Arith_Data.arith_tac ctxt')))), + T.by_abstraction (true, true) ctxt [] (fn ctxt' => T.by_tac ( + NAMED ctxt' "simp (full)" (Simplifier.simp_tac simpset) + THEN_ALL_NEW ( + NAMED ctxt' "fast (full)" (Classical.fast_tac HOL_cs) + ORELSE' NAMED ctxt' "arith (full)" (Arith_Data.arith_tac ctxt')))), + named ctxt "injectivity" (M.prove_injectivity ctxt)]) ct)) end diff -r 798aad2229c0 -r e080c9e68752 src/HOL/Tools/SMT/z3_proof_tools.ML --- a/src/HOL/Tools/SMT/z3_proof_tools.ML Mon Nov 22 15:45:42 2010 +0100 +++ b/src/HOL/Tools/SMT/z3_proof_tools.ML Mon Nov 22 15:45:43 2010 +0100 @@ -9,7 +9,6 @@ (* accessing and modifying terms *) val term_of: cterm -> term val prop_of: thm -> term - val mk_prop: cterm -> cterm val as_meta_eq: cterm -> cterm (* theorem nets *) @@ -59,9 +58,7 @@ fun term_of ct = dest_prop (Thm.term_of ct) fun prop_of thm = dest_prop (Thm.prop_of thm) -val mk_prop = Thm.capply (Thm.cterm_of @{theory} @{const Trueprop}) - -fun as_meta_eq ct = uncurry U.mk_cequals (Thm.dest_binop (Thm.dest_arg ct)) +fun as_meta_eq ct = uncurry U.mk_cequals (Thm.dest_binop (U.dest_cprop ct)) @@ -85,7 +82,7 @@ (* proof combinators *) fun under_assumption f ct = - let val ct' = mk_prop ct + let val ct' = U.mk_cprop ct in Thm.implies_intr ct' (f (Thm.assume ct')) end fun with_conv conv prove ct = @@ -125,9 +122,6 @@ local -fun typ_of ct = #T (Thm.rep_cterm ct) -fun certify ctxt = Thm.cterm_of (ProofContext.theory_of ctxt) - fun abs_context ctxt = (ctxt, Termtab.empty, 1, false) fun context_of (ctxt, _, _, _) = ctxt @@ -153,7 +147,8 @@ | NONE => let val (n, ctxt') = yield_singleton Variable.variant_fixes "x" ctxt - val cv = certify ctxt' (Free (n, map typ_of cvs' ---> typ_of ct)) + val cv = U.certify ctxt' + (Free (n, map U.typ_of cvs' ---> U.typ_of ct)) val cu = Drule.list_comb (cv, cvs') val e = (t, (cv, fold_rev Thm.cabs cvs' ct)) val beta_norm' = beta_norm orelse not (null cvs')