# HG changeset patch # User boehmes # Date 1292878977 -3600 # Node ID 6792a5c92a580e14344c4144f4fb398d96eafd24 # Parent 49feace8764921c381f80f1c45def26577cc3f7c avoid ML structure aliases (especially single-letter abbreviations) diff -r 49feace87649 -r 6792a5c92a58 src/HOL/SMT.thy --- a/src/HOL/SMT.thy Mon Dec 20 21:04:45 2010 +0100 +++ b/src/HOL/SMT.thy Mon Dec 20 22:02:57 2010 +0100 @@ -17,13 +17,13 @@ ("Tools/SMT/smt_translate.ML") ("Tools/SMT/smt_solver.ML") ("Tools/SMT/smtlib_interface.ML") + ("Tools/SMT/z3_interface.ML") ("Tools/SMT/z3_proof_parser.ML") ("Tools/SMT/z3_proof_tools.ML") ("Tools/SMT/z3_proof_literals.ML") ("Tools/SMT/z3_proof_methods.ML") ("Tools/SMT/z3_proof_reconstruction.ML") ("Tools/SMT/z3_model.ML") - ("Tools/SMT/z3_interface.ML") ("Tools/SMT/smt_setup_solvers.ML") begin diff -r 49feace87649 -r 6792a5c92a58 src/HOL/Tools/SMT/smt_builtin.ML --- a/src/HOL/Tools/SMT/smt_builtin.ML Mon Dec 20 21:04:45 2010 +0100 +++ b/src/HOL/Tools/SMT/smt_builtin.ML Mon Dec 20 22:02:57 2010 +0100 @@ -47,15 +47,12 @@ structure SMT_Builtin: SMT_BUILTIN = struct -structure U = SMT_Utils -structure C = SMT_Config - (* built-in tables *) datatype ('a, 'b) kind = Ext of 'a | Int of 'b -type ('a, 'b) ttab = ((typ * ('a, 'b) kind) Ord_List.T) U.dict +type ('a, 'b) ttab = ((typ * ('a, 'b) kind) Ord_List.T) SMT_Utils.dict fun typ_ord ((T, _), (U, _)) = let @@ -68,16 +65,17 @@ in tord (T, U) end fun insert_ttab cs T f = - U.dict_map_default (cs, []) + SMT_Utils.dict_map_default (cs, []) (Ord_List.insert typ_ord (perhaps (try Logic.varifyT_global) T, f)) fun merge_ttab ttabp = - U.dict_merge (uncurry (Ord_List.union typ_ord) o swap) ttabp + SMT_Utils.dict_merge (uncurry (Ord_List.union typ_ord) o swap) ttabp fun lookup_ttab ctxt ttab T = let fun match (U, _) = Sign.typ_instance (ProofContext.theory_of ctxt) (T, U) in - get_first (find_first match) (U.dict_lookup ttab (C.solver_class_of ctxt)) + get_first (find_first match) + (SMT_Utils.dict_lookup ttab (SMT_Config.solver_class_of ctxt)) end type ('a, 'b) btab = ('a, 'b) ttab Symtab.table @@ -108,7 +106,7 @@ Builtin_Types.map (insert_ttab cs T (Int (f, g))) fun add_builtin_typ_ext (T, f) = - Builtin_Types.map (insert_ttab U.basicC T (Ext f)) + Builtin_Types.map (insert_ttab SMT_Utils.basicC T (Ext f)) fun lookup_builtin_typ ctxt = lookup_ttab ctxt (Builtin_Types.get (Context.Proof ctxt)) @@ -168,7 +166,7 @@ in add_builtin_fun cs (c, bfun) end fun add_builtin_fun_ext ((n, T), f) = - Builtin_Funcs.map (insert_btab U.basicC n T (Ext f)) + Builtin_Funcs.map (insert_btab SMT_Utils.basicC n T (Ext f)) fun add_builtin_fun_ext' c = add_builtin_fun_ext (c, fn _ => fn _ => fn _ => true) diff -r 49feace87649 -r 6792a5c92a58 src/HOL/Tools/SMT/smt_normalize.ML --- a/src/HOL/Tools/SMT/smt_normalize.ML Mon Dec 20 21:04:45 2010 +0100 +++ b/src/HOL/Tools/SMT/smt_normalize.ML Mon Dec 20 22:02:57 2010 +0100 @@ -18,16 +18,14 @@ structure SMT_Normalize: SMT_NORMALIZE = struct -structure U = SMT_Utils -structure B = SMT_Builtin - (* general theorem normalizations *) (** instantiate elimination rules **) local - val (cpfalse, cfalse) = `U.mk_cprop (Thm.cterm_of @{theory} @{const False}) + val (cpfalse, cfalse) = + `SMT_Utils.mk_cprop (Thm.cterm_of @{theory} @{const False}) fun inst f ct thm = let val cv = f (Drule.strip_imp_concl (Thm.cprop_of thm)) @@ -70,8 +68,8 @@ | _ => Conv.all_conv) ct val setup_atomize = - fold B.add_builtin_fun_ext'' [@{const_name "==>"}, @{const_name "=="}, - @{const_name all}, @{const_name Trueprop}] + fold SMT_Builtin.add_builtin_fun_ext'' [@{const_name "==>"}, + @{const_name "=="}, @{const_name all}, @{const_name Trueprop}] (** unfold special quantifiers **) @@ -100,10 +98,11 @@ in fun unfold_special_quants_conv ctxt = - U.if_exists_conv (is_some o special_quant) + SMT_Utils.if_exists_conv (is_some o special_quant) (Conv.top_conv special_quant_conv ctxt) -val setup_unfolded_quants = fold (B.add_builtin_fun_ext'' o fst) special_quants +val setup_unfolded_quants = + fold (SMT_Builtin.add_builtin_fun_ext'' o fst) special_quants end @@ -141,7 +140,8 @@ "must have the same kind: " ^ Syntax.string_of_term ctxt t) fun check_trigger_conv ctxt ct = - if proper_quant false proper_trigger (U.term_of ct) then Conv.all_conv ct + if proper_quant false proper_trigger (SMT_Utils.term_of ct) then + Conv.all_conv ct else check_trigger_error ctxt (Thm.term_of ct) @@ -169,7 +169,7 @@ fun is_simp_lhs ctxt t = (case Term.strip_comb t of (Const c, ts as _ :: _) => - not (B.is_builtin_fun_ext ctxt c ts) andalso + not (SMT_Builtin.is_builtin_fun_ext ctxt c ts) andalso forall (is_constr_pat (ProofContext.theory_of ctxt)) ts | _ => false) @@ -194,8 +194,9 @@ Pattern.matches thy (t', u) andalso not (t aconv u)) in not (Term.exists_subterm some_match u) end - val pat = U.mk_const_pat @{theory} @{const_name SMT.pat} U.destT1 - fun mk_pat ct = Thm.capply (U.instT' ct pat) ct + val pat = + SMT_Utils.mk_const_pat @{theory} @{const_name SMT.pat} SMT_Utils.destT1 + fun mk_pat ct = Thm.capply (SMT_Utils.instT' ct pat) ct fun mk_clist T = pairself (Thm.cterm_of @{theory}) (HOLogic.cons_const T, HOLogic.nil_const T) @@ -231,20 +232,24 @@ | has_trigger _ = false fun try_trigger_conv cv ct = - if U.under_quant has_trigger (U.term_of ct) then Conv.all_conv ct + if SMT_Utils.under_quant has_trigger (SMT_Utils.term_of ct) then + Conv.all_conv ct else Conv.try_conv cv ct fun infer_trigger_conv ctxt = if Config.get ctxt SMT_Config.infer_triggers then - try_trigger_conv (U.under_quant_conv (infer_trigger_eq_conv ctxt) ctxt) + try_trigger_conv + (SMT_Utils.under_quant_conv (infer_trigger_eq_conv ctxt) ctxt) else Conv.all_conv in fun trigger_conv ctxt = - U.prop_conv (check_trigger_conv ctxt then_conv infer_trigger_conv ctxt) + SMT_Utils.prop_conv + (check_trigger_conv ctxt then_conv infer_trigger_conv ctxt) -val setup_trigger = fold B.add_builtin_fun_ext'' - [@{const_name SMT.pat}, @{const_name SMT.nopat}, @{const_name SMT.trigger}] +val setup_trigger = + fold SMT_Builtin.add_builtin_fun_ext'' + [@{const_name SMT.pat}, @{const_name SMT.nopat}, @{const_name SMT.trigger}] end @@ -272,7 +277,8 @@ Syntax.string_of_term ctxt t) fun check_weight_conv ctxt ct = - if U.under_quant proper_trigger (U.term_of ct) then Conv.all_conv ct + if SMT_Utils.under_quant proper_trigger (SMT_Utils.term_of ct) then + Conv.all_conv ct else check_weight_error ctxt (Thm.term_of ct) @@ -294,13 +300,14 @@ fun add_weight_conv NONE _ = Conv.all_conv | add_weight_conv (SOME weight) ctxt = let val cv = Conv.rewr_conv (mk_weight_eq weight) - in U.under_quant_conv (K (under_trigger_conv cv)) ctxt end + in SMT_Utils.under_quant_conv (K (under_trigger_conv cv)) ctxt end in fun weight_conv weight ctxt = - U.prop_conv (check_weight_conv ctxt then_conv add_weight_conv weight ctxt) + SMT_Utils.prop_conv + (check_weight_conv ctxt then_conv add_weight_conv weight ctxt) -val setup_weight = B.add_builtin_fun_ext'' @{const_name SMT.weight} +val setup_weight = SMT_Builtin.add_builtin_fun_ext'' @{const_name SMT.weight} end @@ -355,11 +362,12 @@ "distinct [x, y] = (x ~= y)" by simp_all} fun distinct_conv _ = - U.if_true_conv is_trivial_distinct (Conv.rewrs_conv thms) + SMT_Utils.if_true_conv is_trivial_distinct (Conv.rewrs_conv thms) in -fun trivial_distinct_conv ctxt = U.if_exists_conv is_trivial_distinct - (Conv.top_conv distinct_conv ctxt) +fun trivial_distinct_conv ctxt = + SMT_Utils.if_exists_conv is_trivial_distinct + (Conv.top_conv distinct_conv ctxt) end @@ -373,13 +381,14 @@ val thm = mk_meta_eq @{lemma "bool_case = (%x y P. if P then x else y)" by (rule ext)+ simp} - fun unfold_conv _ = U.if_true_conv is_bool_case (Conv.rewr_conv thm) + fun unfold_conv _ = SMT_Utils.if_true_conv is_bool_case (Conv.rewr_conv thm) in -fun rewrite_bool_case_conv ctxt = U.if_exists_conv is_bool_case - (Conv.top_conv unfold_conv ctxt) +fun rewrite_bool_case_conv ctxt = + SMT_Utils.if_exists_conv is_bool_case (Conv.top_conv unfold_conv ctxt) -val setup_bool_case = B.add_builtin_fun_ext'' @{const_name "bool.bool_case"} +val setup_bool_case = + SMT_Builtin.add_builtin_fun_ext'' @{const_name "bool.bool_case"} end @@ -400,7 +409,8 @@ val defs = [(@{const_name min}, min_def), (@{const_name max}, max_def), (@{const_name abs}, abs_def)] - fun is_builtinT ctxt T = B.is_builtin_typ_ext ctxt (Term.domain_type T) + fun is_builtinT ctxt T = + SMT_Builtin.is_builtin_typ_ext ctxt (Term.domain_type T) fun abs_min_max ctxt (Const (n, T)) = (case AList.lookup (op =) defs n of @@ -415,10 +425,10 @@ in fun unfold_abs_min_max_conv ctxt = - U.if_exists_conv (is_some o abs_min_max ctxt) + SMT_Utils.if_exists_conv (is_some o abs_min_max ctxt) (Conv.top_conv unfold_amm_conv ctxt) -val setup_abs_min_max = fold (B.add_builtin_fun_ext'' o fst) defs +val setup_abs_min_max = fold (SMT_Builtin.add_builtin_fun_ext'' o fst) defs end @@ -482,7 +492,7 @@ fun mk_number_eq ctxt i lhs = let - val eq = U.mk_cequals lhs (Numeral.mk_cnumber @{ctyp int} i) + val eq = SMT_Utils.mk_cequals lhs (Numeral.mk_cnumber @{ctyp int} i) val ss = HOL_ss addsimps [@{thm Nat_Numeral.int_nat_number_of}] addsimps @{thms neg_simps} @@ -508,11 +518,11 @@ and ints_conv ctxt = Conv.top_sweep_conv int_conv ctxt and expand_conv ctxt = - U.if_conv (is_nat_const o Term.head_of) + SMT_Utils.if_conv (is_nat_const o Term.head_of) (expand_head_conv (Conv.rewrs_conv expands) then_conv ints_conv ctxt) (int_conv ctxt) - and nat_conv ctxt = U.if_exists_conv is_nat_const' + and nat_conv ctxt = SMT_Utils.if_exists_conv is_nat_const' (Conv.top_sweep_conv expand_conv ctxt) val uses_nat_int = Term.exists_subterm (member (op aconv) nat_int_coercions) @@ -525,8 +535,8 @@ else (thms, []) val setup_nat_as_int = - B.add_builtin_typ_ext (@{typ nat}, K true) #> - fold (B.add_builtin_fun_ext' o Term.dest_Const) builtin_nat_ops + SMT_Builtin.add_builtin_typ_ext (@{typ nat}, K true) #> + fold (SMT_Builtin.add_builtin_fun_ext' o Term.dest_Const) builtin_nat_ops end @@ -542,7 +552,7 @@ fun is_strange_number ctxt (t as Const (@{const_name number_of}, _) $ _) = (case try HOLogic.dest_number t of - SOME (_, i) => B.is_builtin_num ctxt t andalso i < 2 + SOME (_, i) => SMT_Builtin.is_builtin_num ctxt t andalso i < 2 | NONE => false) | is_strange_number _ _ = false @@ -558,12 +568,14 @@ "Int.Bit1 (- k) = - Int.Bit1 (Int.pred k)" by simp_all (simp add: pred_def)} - fun norm_num_conv ctxt = U.if_conv (is_strange_number ctxt) - (Simplifier.rewrite (Simplifier.context ctxt pos_num_ss)) Conv.no_conv + fun norm_num_conv ctxt = + SMT_Utils.if_conv (is_strange_number ctxt) + (Simplifier.rewrite (Simplifier.context ctxt pos_num_ss)) Conv.no_conv in -fun normalize_numerals_conv ctxt = U.if_exists_conv (is_strange_number ctxt) - (Conv.top_sweep_conv norm_num_conv ctxt) +fun normalize_numerals_conv ctxt = + SMT_Utils.if_exists_conv (is_strange_number ctxt) + (Conv.top_sweep_conv norm_num_conv ctxt) end @@ -599,18 +611,19 @@ structure Extra_Norms = Generic_Data ( - type T = extra_norm U.dict + type T = extra_norm SMT_Utils.dict val empty = [] val extend = I - fun merge data = U.dict_merge fst data + fun merge data = SMT_Utils.dict_merge fst data ) -fun add_extra_norm (cs, norm) = Extra_Norms.map (U.dict_update (cs, norm)) +fun add_extra_norm (cs, norm) = + Extra_Norms.map (SMT_Utils.dict_update (cs, norm)) fun apply_extra_norms ithms ctxt = let val cs = SMT_Config.solver_class_of ctxt - val es = U.dict_lookup (Extra_Norms.get (Context.Proof ctxt)) cs + val es = SMT_Utils.dict_lookup (Extra_Norms.get (Context.Proof ctxt)) cs in (burrow_ids (fold (fn e => e ctxt) es o rpair []) ithms, ctxt) end fun normalize iwthms ctxt = diff -r 49feace87649 -r 6792a5c92a58 src/HOL/Tools/SMT/smt_solver.ML --- a/src/HOL/Tools/SMT/smt_solver.ML Mon Dec 20 21:04:45 2010 +0100 +++ b/src/HOL/Tools/SMT/smt_solver.ML Mon Dec 20 22:02:57 2010 +0100 @@ -51,8 +51,6 @@ structure SMT_Solver: SMT_SOLVER = struct -structure C = SMT_Config - (* configuration *) @@ -109,13 +107,13 @@ [File.shell_path problem_path, "2>&1", ">", File.shell_path proof_path]) fun run ctxt cmd args input = - (case C.certificates_of ctxt of + (case SMT_Config.certificates_of ctxt of NONE => - if Config.get ctxt C.debug_files = "" then + if Config.get ctxt SMT_Config.debug_files = "" then Cache_IO.run (make_cmd (choose cmd) args) input else let - val base_path = Path.explode (Config.get ctxt C.debug_files) + val base_path = Path.explode (Config.get ctxt SMT_Config.debug_files) val in_path = Path.ext "smt_in" base_path val out_path = Path.ext "smt_out" base_path in @@ -124,7 +122,7 @@ | SOME certs => (case Cache_IO.lookup certs input of (NONE, key) => - if Config.get ctxt C.fixed then + if Config.get ctxt SMT_Config.fixed then error ("Bad certificates cache: missing certificate") else Cache_IO.run_and_cache certs key (make_cmd (choose cmd) args) input @@ -140,14 +138,14 @@ fun pretty tag ls = Pretty.string_of (Pretty.big_list tag (map Pretty.str ls)) - val _ = C.trace_msg ctxt (pretty "Problem:" o split_lines) input + val _ = SMT_Config.trace_msg ctxt (pretty "Problem:" o split_lines) input val {redirected_output=res, output=err, return_code} = - C.with_timeout ctxt (run ctxt cmd args) input - val _ = C.trace_msg ctxt (pretty "Solver:") err + SMT_Config.with_timeout ctxt (run ctxt cmd args) input + val _ = SMT_Config.trace_msg ctxt (pretty "Solver:") err val ls = rev (snd (chop_while (equal "") (rev res))) - val _ = C.trace_msg ctxt (pretty "Result:") ls + val _ = SMT_Config.trace_msg ctxt (pretty "Result:") ls val _ = null ls andalso return_code <> 0 andalso raise SMT_Failure.SMT (SMT_Failure.Abnormal_Termination return_code) @@ -155,8 +153,9 @@ end -fun trace_assms ctxt = C.trace_msg ctxt (Pretty.string_of o - Pretty.big_list "Assertions:" o map (Display.pretty_thm ctxt o snd)) +fun trace_assms ctxt = + SMT_Config.trace_msg ctxt (Pretty.string_of o + Pretty.big_list "Assertions:" o map (Display.pretty_thm ctxt o snd)) fun trace_recon_data ({context=ctxt, typs, terms, ...} : SMT_Translate.recon) = let @@ -164,7 +163,7 @@ fun p_typ (n, T) = pretty_eq n (Syntax.pretty_typ ctxt T) fun p_term (n, t) = pretty_eq n (Syntax.pretty_term ctxt t) in - C.trace_msg ctxt (fn () => + SMT_Config.trace_msg ctxt (fn () => Pretty.string_of (Pretty.big_list "Names:" [ Pretty.big_list "sorts:" (map p_typ (Symtab.dest typs)), Pretty.big_list "functions:" (map p_term (Symtab.dest terms))])) () @@ -172,10 +171,11 @@ fun invoke name cmd options ithms ctxt = let - val args = C.solver_options_of ctxt @ options ctxt + val args = SMT_Config.solver_options_of ctxt @ options ctxt val comments = ("solver: " ^ name) :: - ("timeout: " ^ string_of_real (Config.get ctxt C.timeout)) :: - ("random seed: " ^ string_of_int (Config.get ctxt C.random_seed)) :: + ("timeout: " ^ string_of_real (Config.get ctxt SMT_Config.timeout)) :: + ("random seed: " ^ + string_of_int (Config.get ctxt SMT_Config.random_seed)) :: "arguments:" :: args val (str, recon as {context=ctxt', ...}) = @@ -192,7 +192,7 @@ |> filter (fn i => i >= 0) |> map_filter (AList.lookup (op =) iwthms) in - if Config.get ctxt C.trace_used_facts andalso length wthms > 0 + if Config.get ctxt SMT_Config.trace_used_facts andalso length wthms > 0 then tracing (Pretty.string_of (Pretty.big_list "SMT used facts:" (map (Display.pretty_thm ctxt o snd) wthms))) @@ -243,7 +243,7 @@ (output, (recon as {context=ctxt, ...} : SMT_Translate.recon)) = (case outcome output of (Unsat, ls) => - if not (Config.get ctxt C.oracle) andalso is_some reconstruct + if not (Config.get ctxt SMT_Config.oracle) andalso is_some reconstruct then the reconstruct outer_ctxt recon ls else ([], ocl ()) | (result, ls) => @@ -273,7 +273,7 @@ in Thm.add_oracle (Binding.name name, core_oracle) #-> (fn (_, ocl) => Context.theory_map (Solvers.map (Symtab.update_new (name, solver ocl)))) #> - Context.theory_map (C.add_solver (name, class)) + Context.theory_map (SMT_Config.add_solver (name, class)) end end @@ -282,7 +282,7 @@ the (Symtab.lookup (Solvers.get (Context.Proof ctxt)) name) fun name_and_solver_of ctxt = - let val name = C.solver_of ctxt + let val name = SMT_Config.solver_of ctxt in (name, get_info ctxt name) end val solver_name_of = fst o name_and_solver_of @@ -326,9 +326,9 @@ let val ctxt = Proof.context_of st - |> Config.put C.oracle false - |> Config.put C.drop_bad_facts true - |> Config.put C.filter_only_facts true + |> Config.put SMT_Config.oracle false + |> Config.put SMT_Config.drop_bad_facts true + |> Config.put SMT_Config.filter_only_facts true val {facts, goal, ...} = Proof.goal st val ({context=ctxt', prems, concl, ...}, _) = Subgoal.focus ctxt i goal @@ -348,7 +348,7 @@ fun smt_filter_tail time_limit run_remote ((xs, wthms), ((iwthms', ctxt), iwthms)) = let - val ctxt = ctxt |> Config.put C.timeout (Time.toReal time_limit) + val ctxt = ctxt |> Config.put SMT_Config.timeout (Time.toReal time_limit) val xrules = xs ~~ map snd wthms in ((iwthms', ctxt), iwthms) @@ -369,15 +369,16 @@ THEN' SUBPROOF (fn {context=ctxt', prems, ...} => let val solve = snd o solver_of ctxt' NONE ctxt' o tap check_topsort - val tag = "Solver " ^ C.solver_of ctxt' ^ ": " + val tag = "Solver " ^ SMT_Config.solver_of ctxt' ^ ": " val str_of = prefix tag o SMT_Failure.string_of_failure ctxt' fun safe_solve iwthms = if pass_exns then SOME (solve iwthms) else (SOME (solve iwthms) handle SMT_Failure.SMT (fail as SMT_Failure.Counterexample _) => - (C.verbose_msg ctxt' str_of fail; NONE) - | SMT_Failure.SMT fail => (C.trace_msg ctxt' str_of fail; NONE)) + (SMT_Config.verbose_msg ctxt' str_of fail; NONE) + | SMT_Failure.SMT fail => + (SMT_Config.trace_msg ctxt' str_of fail; NONE)) in safe_solve (map (pair ~1 o pair NONE) (rules @ prems)) |> (fn SOME thm => Tactic.rtac thm 1 | _ => Tactical.no_tac) diff -r 49feace87649 -r 6792a5c92a58 src/HOL/Tools/SMT/smt_translate.ML --- a/src/HOL/Tools/SMT/smt_translate.ML Mon Dec 20 21:04:45 2010 +0100 +++ b/src/HOL/Tools/SMT/smt_translate.ML Mon Dec 20 22:02:57 2010 +0100 @@ -45,9 +45,6 @@ structure SMT_Translate: SMT_TRANSLATE = struct -structure U = SMT_Utils -structure B = SMT_Builtin - (* intermediate term structure *) @@ -169,7 +166,7 @@ in Abs (Name.uu, U1, eta U2 (l $ Bound 0)) end fun expf k i T t = - let val Ts = drop i (fst (U.dest_funT k T)) + let val Ts = drop i (fst (SMT_Utils.dest_funT k T)) in Term.incr_boundvars (length Ts) t |> fold_index (fn (i, _) => fn u => u $ Bound i) Ts @@ -195,7 +192,7 @@ | expand t = (case Term.strip_comb t of (u as Const (c as (_, T)), ts) => - (case B.dest_builtin ctxt c ts of + (case SMT_Builtin.dest_builtin ctxt c ts of SOME (_, k, us, mk) => if k = length us then mk (map expand us) else expf k (length ts) T (mk (map expand us)) @@ -302,8 +299,10 @@ (Const (@{const_name SMT.fun_app}, T --> T) $ t $ u, Term.range_type T) fun apply i t T ts = - let val (ts1, ts2) = chop i ts - in fst (fold app ts2 (Term.list_comb (t, ts1), snd (U.dest_funT i T))) end + let + val (ts1, ts2) = chop i ts + val (_, U) = SMT_Utils.dest_funT i T + in fst (fold app ts2 (Term.list_comb (t, ts1), U)) end in fun intro_explicit_application ts = @@ -351,14 +350,14 @@ @{const If (bool)} $ t $ @{const SMT.term_true} $ @{const SMT.term_false} fun is_builtin_conn_or_pred ctxt c ts = - is_some (B.dest_builtin_conn ctxt c ts) orelse - is_some (B.dest_builtin_pred ctxt c ts) + is_some (SMT_Builtin.dest_builtin_conn ctxt c ts) orelse + is_some (SMT_Builtin.dest_builtin_pred ctxt c ts) fun builtin b ctxt c ts = (case (Const c, ts) of (@{const HOL.eq (bool)}, [t, u]) => if t = @{const SMT.term_true} orelse u = @{const SMT.term_true} then - B.dest_builtin_eq ctxt t u + SMT_Builtin.dest_builtin_eq ctxt t u else b ctxt c ts | _ => b ctxt c ts) in @@ -400,16 +399,16 @@ q $ Abs (n, T, in_trigger u) else as_term (in_term t) | (Const c, ts) => - (case B.dest_builtin_conn ctxt c ts of + (case SMT_Builtin.dest_builtin_conn ctxt c ts of SOME (_, _, us, mk) => mk (map in_form us) | NONE => - (case B.dest_builtin_pred ctxt c ts of + (case SMT_Builtin.dest_builtin_pred ctxt c ts of SOME (_, _, us, mk) => mk (map in_term us) | NONE => as_term (in_term t))) | _ => as_term (in_term t)) in map (reduce_let #> in_form) #> - cons (U.prop_of term_bool) #> + cons (SMT_Utils.prop_of term_bool) #> pair (fol_rules, [term_bool], builtin) end @@ -466,7 +465,7 @@ fun transT (T as TFree _) = add_typ T true | transT (T as TVar _) = (fn _ => raise TYPE ("bad SMT type", [T], [])) | transT (T as Type _) = - (case B.dest_builtin_typ ctxt T of + (case SMT_Builtin.dest_builtin_typ ctxt T of SOME n => pair n | NONE => add_typ T true) @@ -492,7 +491,7 @@ | _ => raise TERM ("bad SMT term", [t])) and transs t T ts = - let val (Us, U) = U.dest_funT (length ts) T + let val (Us, U) = SMT_Utils.dest_funT (length ts) T in fold_map transT Us ##>> transT U #-> (fn Up => add_fun t (SOME Up) ##>> fold_map trans ts #>> SApp) @@ -507,21 +506,21 @@ structure Configs = Generic_Data ( - type T = (Proof.context -> config) U.dict + type T = (Proof.context -> config) SMT_Utils.dict val empty = [] val extend = I - fun merge data = U.dict_merge fst data + fun merge data = SMT_Utils.dict_merge fst data ) -fun add_config (cs, cfg) = Configs.map (U.dict_update (cs, cfg)) +fun add_config (cs, cfg) = Configs.map (SMT_Utils.dict_update (cs, cfg)) fun get_config ctxt = let val cs = SMT_Config.solver_class_of ctxt in - (case U.dict_get (Configs.get (Context.Proof ctxt)) cs of + (case SMT_Utils.dict_get (Configs.get (Context.Proof ctxt)) cs of SOME cfg => cfg ctxt | NONE => error ("SMT: no translation configuration found " ^ - "for solver class " ^ quote (U.string_of_class cs))) + "for solver class " ^ quote (SMT_Utils.string_of_class cs))) end fun translate ctxt comments ithms = @@ -533,7 +532,7 @@ fun no_dtyps (tr_context, ctxt) ts = (([], tr_context, ctxt), ts) - val ts1 = map (Envir.beta_eta_contract o U.prop_of o snd) ithms + val ts1 = map (Envir.beta_eta_contract o SMT_Utils.prop_of o snd) ithms val ((dtyps, tr_context, ctxt1), ts2) = ((make_tr_context prefixes, ctxt), ts1) @@ -551,7 +550,7 @@ val rewrite_rules' = fun_app_eq :: rewrite_rules in (ts4, tr_context) - |-> intermediate header dtyps (builtin B.dest_builtin) ctxt2 + |-> intermediate header dtyps (builtin SMT_Builtin.dest_builtin) ctxt2 |>> uncurry (serialize comments) ||> recon_of ctxt2 rewrite_rules' extra_thms ithms end diff -r 49feace87649 -r 6792a5c92a58 src/HOL/Tools/SMT/smtlib_interface.ML --- a/src/HOL/Tools/SMT/smtlib_interface.ML Mon Dec 20 21:04:45 2010 +0100 +++ b/src/HOL/Tools/SMT/smtlib_interface.ML Mon Dec 20 22:02:57 2010 +0100 @@ -16,10 +16,6 @@ structure SMTLIB_Interface: SMTLIB_INTERFACE = struct -structure U = SMT_Utils -structure B = SMT_Builtin -structure N = SMT_Normalize -structure T = SMT_Translate val smtlibC = ["smtlib"] @@ -29,8 +25,8 @@ local fun int_num _ i = SOME (string_of_int i) - fun is_linear [t] = U.is_number t - | is_linear [t, u] = U.is_number t orelse U.is_number u + fun is_linear [t] = SMT_Utils.is_number t + | is_linear [t, u] = SMT_Utils.is_number t orelse SMT_Utils.is_number u | is_linear _ = false fun times _ _ ts = @@ -49,8 +45,8 @@ in val setup_builtins = - B.add_builtin_typ smtlibC (@{typ int}, K (SOME "Int"), int_num) #> - fold (B.add_builtin_fun' smtlibC) [ + SMT_Builtin.add_builtin_typ smtlibC (@{typ int}, K (SOME "Int"), int_num) #> + fold (SMT_Builtin.add_builtin_fun' smtlibC) [ (@{const True}, "true"), (@{const False}, "false"), (@{const Not}, "not"), @@ -66,8 +62,10 @@ (@{const uminus (int)}, "~"), (@{const plus (int)}, "+"), (@{const minus (int)}, "-") ] #> - B.add_builtin_fun smtlibC (Term.dest_Const @{const times (int)}, times) #> - B.add_builtin_fun smtlibC (Term.dest_Const @{const distinct ('a)}, distinct) + SMT_Builtin.add_builtin_fun smtlibC + (Term.dest_Const @{const times (int)}, times) #> + SMT_Builtin.add_builtin_fun smtlibC + (Term.dest_Const @{const distinct ('a)}, distinct) end @@ -106,18 +104,20 @@ fun var i = add "?v" #> add (string_of_int i) -fun sterm l (T.SVar i) = sep (var (l - i - 1)) - | sterm l (T.SApp (n, ts)) = app n (sterm l) ts - | sterm _ (T.SLet _) = raise Fail "SMT-LIB: unsupported let expression" - | sterm l (T.SQua (q, ss, ps, w, t)) = +fun sterm l (SMT_Translate.SVar i) = sep (var (l - i - 1)) + | sterm l (SMT_Translate.SApp (n, ts)) = app n (sterm l) ts + | sterm _ (SMT_Translate.SLet _) = + raise Fail "SMT-LIB: unsupported let expression" + | sterm l (SMT_Translate.SQua (q, ss, ps, w, t)) = let - val quant = add o (fn T.SForall => "forall" | T.SExists => "exists") + fun quant SMT_Translate.SForall = add "forall" + | quant SMT_Translate.SExists = add "exists" val vs = map_index (apfst (Integer.add l)) ss fun var_decl (i, s) = par (var i #> sep (add s)) val sub = sterm (l + length ss) fun pat kind ts = sep (add kind #> enclose "{" " }" (fold sub ts)) - fun pats (T.SPat ts) = pat ":pat" ts - | pats (T.SNoPat ts) = pat ":nopat" ts + fun pats (SMT_Translate.SPat ts) = pat ":pat" ts + | pats (SMT_Translate.SNoPat ts) = pat ":nopat" ts fun weight NONE = I | weight (SOME i) = sep (add ":weight { " #> add (string_of_int i) #> add " }") @@ -168,6 +168,6 @@ val setup = Context.theory_map ( setup_builtins #> - T.add_config (smtlibC, translate_config)) + SMT_Translate.add_config (smtlibC, translate_config)) end diff -r 49feace87649 -r 6792a5c92a58 src/HOL/Tools/SMT/z3_model.ML --- a/src/HOL/Tools/SMT/z3_model.ML Mon Dec 20 21:04:45 2010 +0100 +++ b/src/HOL/Tools/SMT/z3_model.ML Mon Dec 20 22:02:57 2010 +0100 @@ -13,8 +13,6 @@ structure Z3_Model: Z3_MODEL = struct -structure U = SMT_Utils - (* counterexample expressions *) @@ -125,7 +123,7 @@ | trans_expr T (Value i) = pair (Var (("value", i), T)) | trans_expr T (Array a) = trans_array T a | trans_expr T (App (n, es)) = get_term n T es #-> (fn (t, es') => - let val Ts = fst (U.dest_funT (length es') (Term.fastype_of t)) + let val Ts = fst (SMT_Utils.dest_funT (length es') (Term.fastype_of t)) in fold_map (uncurry trans_expr) (Ts ~~ es') #>> Term.list_comb o pair t end) @@ -167,7 +165,7 @@ fun translate ((t, k), (e, cs)) = let val T = Term.fastype_of t - val (Us, U) = U.dest_funT k (Term.fastype_of t) + val (Us, U) = SMT_Utils.dest_funT k (Term.fastype_of t) fun mk_full_def u' pats = pats diff -r 49feace87649 -r 6792a5c92a58 src/HOL/Tools/SMT/z3_proof_literals.ML --- a/src/HOL/Tools/SMT/z3_proof_literals.ML Mon Dec 20 21:04:45 2010 +0100 +++ b/src/HOL/Tools/SMT/z3_proof_literals.ML Mon Dec 20 22:02:57 2010 +0100 @@ -33,19 +33,17 @@ structure Z3_Proof_Literals: Z3_PROOF_LITERALS = struct -structure U = SMT_Utils -structure T = Z3_Proof_Tools - (* literal table *) type littab = thm Termtab.table -fun make_littab thms = fold (Termtab.update o `U.prop_of) thms Termtab.empty +fun make_littab thms = + fold (Termtab.update o `SMT_Utils.prop_of) thms Termtab.empty -fun insert_lit thm = Termtab.update (`U.prop_of thm) -fun delete_lit thm = Termtab.delete (U.prop_of thm) +fun insert_lit thm = Termtab.update (`SMT_Utils.prop_of thm) +fun delete_lit thm = Termtab.delete (SMT_Utils.prop_of thm) fun lookup_lit lits = Termtab.lookup lits fun get_first_lit f = Termtab.get_first (fn (t, thm) => if f t then SOME thm else NONE) @@ -93,18 +91,20 @@ (** explosion of conjunctions and disjunctions **) local + val precomp = Z3_Proof_Tools.precompose2 + fun destc ct = Thm.dest_binop (Thm.dest_arg ct) - val dest_conj1 = T.precompose2 destc @{thm conjunct1} - val dest_conj2 = T.precompose2 destc @{thm conjunct2} + val dest_conj1 = precomp destc @{thm conjunct1} + val dest_conj2 = precomp destc @{thm conjunct2} fun dest_conj_rules t = dest_conj_term t |> Option.map (K (dest_conj1, dest_conj2)) fun destd f ct = f (Thm.dest_binop (Thm.dest_arg (Thm.dest_arg ct))) val dn1 = apfst Thm.dest_arg and dn2 = apsnd Thm.dest_arg - val dest_disj1 = T.precompose2 (destd I) @{lemma "~(P | Q) ==> ~P" by fast} - val dest_disj2 = T.precompose2 (destd dn1) @{lemma "~(~P | Q) ==> P" by fast} - val dest_disj3 = T.precompose2 (destd I) @{lemma "~(P | Q) ==> ~Q" by fast} - val dest_disj4 = T.precompose2 (destd dn2) @{lemma "~(P | ~Q) ==> Q" by fast} + val dest_disj1 = precomp (destd I) @{lemma "~(P | Q) ==> ~P" by fast} + val dest_disj2 = precomp (destd dn1) @{lemma "~(~P | Q) ==> P" by fast} + val dest_disj3 = precomp (destd I) @{lemma "~(P | Q) ==> ~Q" by fast} + val dest_disj4 = precomp (destd dn2) @{lemma "~(P | ~Q) ==> Q" by fast} fun dest_disj_rules t = (case dest_disj_term' is_neg t of @@ -115,7 +115,7 @@ | NONE => NONE) fun destn ct = [Thm.dest_arg (Thm.dest_arg (Thm.dest_arg ct))] - val dneg_rule = T.precompose destn @{thm notnotD} + val dneg_rule = Z3_Proof_Tools.precompose destn @{thm notnotD} in (* @@ -150,7 +150,7 @@ (* extract a literal by applying previously collected rules *) -fun extract_lit thm rules = fold T.compose rules thm +fun extract_lit thm rules = fold Z3_Proof_Tools.compose rules thm (* @@ -162,9 +162,9 @@ val tab = fold (Termtab.update o rpair ()) stop_lits Termtab.empty fun explode1 thm = - if Termtab.defined tab (U.prop_of thm) then cons thm + if Termtab.defined tab (SMT_Utils.prop_of thm) then cons thm else - (case dest_rules (U.prop_of thm) of + (case dest_rules (SMT_Utils.prop_of thm) of SOME (rule1, rule2) => explode2 rule1 thm #> explode2 rule2 thm #> @@ -172,13 +172,14 @@ | NONE => cons thm) and explode2 dest_rule thm = - if full orelse exists_lit is_conj (Termtab.defined tab) (U.prop_of thm) - then explode1 (T.compose dest_rule thm) - else cons (T.compose dest_rule thm) + if full orelse + exists_lit is_conj (Termtab.defined tab) (SMT_Utils.prop_of thm) + then explode1 (Z3_Proof_Tools.compose dest_rule thm) + else cons (Z3_Proof_Tools.compose dest_rule thm) fun explode0 thm = - if not is_conj andalso is_dneg (U.prop_of thm) - then [T.compose dneg_rule thm] + if not is_conj andalso is_dneg (SMT_Utils.prop_of thm) + then [Z3_Proof_Tools.compose dneg_rule thm] else explode1 thm [] in explode0 end @@ -195,7 +196,7 @@ fun precomp2 f g thm = (on_cprem 1 f thm, on_cprem 2 g thm, f, g, thm) fun comp2 (cv1, cv2, f, g, rule) thm1 thm2 = Thm.instantiate ([], [(cv1, on_cprop f thm1), (cv2, on_cprop g thm2)]) rule - |> T.discharge thm1 |> T.discharge thm2 + |> Z3_Proof_Tools.discharge thm1 |> Z3_Proof_Tools.discharge thm2 fun d1 ct = Thm.dest_arg ct and d2 ct = Thm.dest_arg (Thm.dest_arg ct) @@ -219,13 +220,15 @@ fun dest_disj (@{const Not} $ (@{const HOL.disj} $ t $ u)) = (neg t, neg u) | dest_disj t = raise TERM ("dest_disj", [t]) - val dnegE = T.precompose (single o d2 o d1) @{thm notnotD} - val dnegI = T.precompose (single o d1) @{lemma "P ==> ~~P" by fast} + val precomp = Z3_Proof_Tools.precompose + val dnegE = precomp (single o d2 o d1) @{thm notnotD} + val dnegI = precomp (single o d1) @{lemma "P ==> ~~P" by fast} fun as_dneg f t = f (@{const Not} $ (@{const Not} $ t)) + val precomp2 = Z3_Proof_Tools.precompose2 fun dni f = apsnd f o Thm.dest_binop o f o d1 - val negIffE = T.precompose2 (dni d1) @{lemma "~(P = (~Q)) ==> Q = P" by fast} - val negIffI = T.precompose2 (dni I) @{lemma "P = Q ==> ~(Q = (~P))" by fast} + val negIffE = precomp2 (dni d1) @{lemma "~(P = (~Q)) ==> Q = P" by fast} + val negIffI = precomp2 (dni I) @{lemma "P = Q ==> ~(Q = (~P))" by fast} val iff_const = @{const HOL.eq (bool)} fun as_negIff f (@{const HOL.eq (bool)} $ t $ u) = f (@{const Not} $ (iff_const $ u $ (@{const Not} $ t))) @@ -241,16 +244,17 @@ fun lookup_rule t = (case t of - @{const Not} $ (@{const Not} $ t) => (T.compose dnegI, lookup t) + @{const Not} $ (@{const Not} $ t) => + (Z3_Proof_Tools.compose dnegI, lookup t) | @{const Not} $ (@{const HOL.eq (bool)} $ t $ (@{const Not} $ u)) => - (T.compose negIffI, lookup (iff_const $ u $ t)) + (Z3_Proof_Tools.compose negIffI, lookup (iff_const $ u $ t)) | @{const Not} $ ((eq as Const (@{const_name HOL.eq}, _)) $ t $ u) => let fun rewr lit = lit COMP @{thm not_sym} in (rewr, lookup (@{const Not} $ (eq $ u $ t))) end | _ => (case as_dneg lookup t of - NONE => (T.compose negIffE, as_negIff lookup t) - | x => (T.compose dnegE, x))) + NONE => (Z3_Proof_Tools.compose negIffE, as_negIff lookup t) + | x => (Z3_Proof_Tools.compose dnegE, x))) fun join1 (s, t) = (case lookup t of @@ -285,7 +289,7 @@ val contra_rule = @{lemma "P ==> ~P ==> False" by (rule notE)} fun contra_left conj thm = let - val rules = explode_term conj (U.prop_of thm) + val rules = explode_term conj (SMT_Utils.prop_of thm) fun contra_lits (t, rs) = (case t of @{const Not} $ u => Termtab.lookup rules u |> Option.map (pair rs) @@ -303,7 +307,8 @@ fun contra_right ct = Thm.instantiate ([], [(falseE_v, ct)]) @{thm FalseE} in fun contradict conj ct = - iff_intro (T.under_assumption (contra_left conj) ct) (contra_right ct) + iff_intro (Z3_Proof_Tools.under_assumption (contra_left conj) ct) + (contra_right ct) end @@ -314,8 +319,8 @@ fun make_tab is_conj thm = make_littab (true_thm :: explode' is_conj thm) fun prove is_conj ct tab = join is_conj tab (Thm.term_of ct) - val thm1 = T.under_assumption (prove r cr o make_tab l) cl - val thm2 = T.under_assumption (prove l cl o make_tab r) cr + val thm1 = Z3_Proof_Tools.under_assumption (prove r cr o make_tab l) cl + val thm2 = Z3_Proof_Tools.under_assumption (prove l cl o make_tab r) cr in iff_intro thm1 thm2 end datatype conj_disj = CONJ | DISJ | NCON | NDIS diff -r 49feace87649 -r 6792a5c92a58 src/HOL/Tools/SMT/z3_proof_methods.ML --- a/src/HOL/Tools/SMT/z3_proof_methods.ML Mon Dec 20 21:04:45 2010 +0100 +++ b/src/HOL/Tools/SMT/z3_proof_methods.ML Mon Dec 20 22:02:57 2010 +0100 @@ -12,9 +12,6 @@ structure Z3_Proof_Methods: Z3_PROOF_METHODS = struct -structure U = SMT_Utils -structure T = Z3_Proof_Tools - fun apply tac st = (case Seq.pull (tac 1 st) of @@ -36,24 +33,24 @@ fun mk_inv_of ctxt ct = let - val (dT, rT) = Term.dest_funT (U.typ_of ct) - val inv = U.certify ctxt (mk_inv_into dT rT) - val univ = U.certify ctxt (mk_univ dT) + val (dT, rT) = Term.dest_funT (SMT_Utils.typ_of ct) + val inv = SMT_Utils.certify ctxt (mk_inv_into dT rT) + val univ = SMT_Utils.certify ctxt (mk_univ dT) in Thm.mk_binop inv univ ct end fun mk_inj_prop ctxt ct = let - val (dT, rT) = Term.dest_funT (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 (dT, rT) = Term.dest_funT (SMT_Utils.typ_of ct) + val inj = SMT_Utils.certify ctxt (mk_inj_on dT rT) + val univ = SMT_Utils.certify ctxt (mk_univ dT) + in SMT_Utils.mk_cprop (Thm.mk_binop inj ct univ) end val disjE = @{lemma "~P | Q ==> P ==> Q" by fast} fun prove_inj_prop ctxt def lhs = let - val (ct, ctxt') = U.dest_all_cabs (Thm.rhs_of def) ctxt + val (ct, ctxt') = SMT_Utils.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,7 +61,7 @@ end fun prove_rhs ctxt def lhs = - T.by_tac ( + Z3_Proof_Tools.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])) #> @@ -82,24 +79,27 @@ fun prove_lhs ctxt rhs = let val eq = Thm.symmetric (mk_meta_eq (Object_Logic.rulify (Thm.assume rhs))) + val conv = SMT_Utils.binders_conv (K (expand eq)) ctxt in - T.by_tac ( - CONVERSION (U.prop_conv (U.binders_conv (K (expand eq)) ctxt)) + Z3_Proof_Tools.by_tac ( + CONVERSION (SMT_Utils.prop_conv conv) THEN' Simplifier.simp_tac HOL_ss) end fun mk_inv_def ctxt rhs = let - val (ct, ctxt') = U.dest_all_cbinders (U.dest_cprop rhs) ctxt + val (ct, ctxt') = + SMT_Utils.dest_all_cbinders (SMT_Utils.dest_cprop rhs) ctxt val (cl, cv) = Thm.dest_binop ct val (cg, (cargs, cf)) = Drule.strip_comb cl ||> split_last val cu = fold_rev Thm.cabs cargs (mk_inv_of ctxt' (Thm.cabs cv cf)) - in Thm.assume (U.mk_cequals cg cu) end + in Thm.assume (SMT_Utils.mk_cequals cg cu) end fun prove_inj_eq ctxt ct = let - val (lhs, rhs) = pairself U.mk_cprop (Thm.dest_binop (U.dest_cprop ct)) + val (lhs, rhs) = + pairself SMT_Utils.mk_cprop (Thm.dest_binop (SMT_Utils.dest_cprop ct)) 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 @@ -109,22 +109,22 @@ val swap_disj_thm = mk_meta_eq @{thm disj_commute} fun swap_conv dest eq = - U.if_true_conv ((op <) o pairself Term.size_of_term o dest) + SMT_Utils.if_true_conv ((op <) o pairself Term.size_of_term o dest) (Conv.rewr_conv eq) val swap_eq_conv = swap_conv HOLogic.dest_eq swap_eq_thm -val swap_disj_conv = swap_conv U.dest_disj swap_disj_thm +val swap_disj_conv = swap_conv SMT_Utils.dest_disj swap_disj_thm fun norm_conv ctxt = swap_eq_conv then_conv - Conv.arg1_conv (U.binders_conv (K swap_disj_conv) ctxt) then_conv - Conv.arg_conv (U.binders_conv (K swap_eq_conv) ctxt) + Conv.arg1_conv (SMT_Utils.binders_conv (K swap_disj_conv) ctxt) then_conv + Conv.arg_conv (SMT_Utils.binders_conv (K swap_eq_conv) ctxt) in fun prove_injectivity ctxt = - T.by_tac ( - CONVERSION (U.prop_conv (norm_conv ctxt)) + Z3_Proof_Tools.by_tac ( + CONVERSION (SMT_Utils.prop_conv (norm_conv ctxt)) THEN' CSUBGOAL (uncurry (Tactic.rtac o prove_inj_eq ctxt))) end diff -r 49feace87649 -r 6792a5c92a58 src/HOL/Tools/SMT/z3_proof_parser.ML --- a/src/HOL/Tools/SMT/z3_proof_parser.ML Mon Dec 20 21:04:45 2010 +0100 +++ b/src/HOL/Tools/SMT/z3_proof_parser.ML Mon Dec 20 22:02:57 2010 +0100 @@ -31,9 +31,6 @@ structure Z3_Proof_Parser: Z3_PROOF_PARSER = struct -structure U = SMT_Utils -structure I = Z3_Interface - (* proof rules *) @@ -113,7 +110,8 @@ 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, U.certify ctxt (Free (nth ns i, #T (Thm.rep_cterm v)))) + fun mk (i, v) = + (v, SMT_Utils.certify ctxt (Free (nth ns i, #T (Thm.rep_cterm v)))) in map mk vars end fun close ctxt (ct, vars) = @@ -124,7 +122,7 @@ fun mk_bound ctxt (i, T) = - let val ct = U.certify ctxt (Var ((Name.uu, 0), T)) + let val ct = SMT_Utils.certify ctxt (Var ((Name.uu, 0), T)) in (ct, [(i, ct)]) end local @@ -133,11 +131,13 @@ val cv = (case AList.lookup (op =) vars 0 of SOME cv => cv - | _ => U.certify ctxt (Var ((Name.uu, maxidx_of ct + 1), T))) + | _ => SMT_Utils.certify ctxt (Var ((Name.uu, maxidx_of ct + 1), T))) fun dec (i, v) = if i = 0 then NONE else SOME (i-1, v) - in (Thm.capply (U.instT' cv q) (Thm.cabs cv ct), map_filter dec vars) end + val vars' = map_filter dec vars + in (Thm.capply (SMT_Utils.instT' cv q) (Thm.cabs cv ct), vars') end - fun quant name = U.mk_const_pat @{theory} name (U.destT1 o U.destT1) + fun quant name = + SMT_Utils.mk_const_pat @{theory} name (SMT_Utils.destT1 o SMT_Utils.destT1) val forall = quant @{const_name All} val exists = quant @{const_name Ex} in @@ -197,7 +197,7 @@ |> Symtab.fold (Variable.declare_term o snd) terms fun cert @{const True} = not_false - | cert t = U.certify ctxt' t + | cert t = SMT_Utils.certify ctxt' t in (typs, Symtab.map (K cert) terms, Inttab.empty, [], [], ctxt') end @@ -212,20 +212,21 @@ SOME _ => cx | NONE => cx |> fresh_name (decl_prefix ^ n) |> (fn (m, (typs, terms, exprs, steps, vars, ctxt)) => - let val upd = Symtab.update (n, U.certify ctxt (Free (m, T))) + let + val upd = Symtab.update (n, SMT_Utils.certify ctxt (Free (m, T))) in (typs, upd terms, exprs, steps, vars, ctxt) end)) -fun mk_typ (typs, _, _, _, _, ctxt) (s as I.Sym (n, _)) = - (case I.mk_builtin_typ ctxt s of +fun mk_typ (typs, _, _, _, _, ctxt) (s as Z3_Interface.Sym (n, _)) = + (case Z3_Interface.mk_builtin_typ ctxt s of SOME T => SOME T | NONE => Symtab.lookup typs n) fun mk_num (_, _, _, _, _, ctxt) (i, T) = - mk_fun (K (I.mk_builtin_num ctxt i T)) [] + mk_fun (K (Z3_Interface.mk_builtin_num ctxt i T)) [] -fun mk_app (_, terms, _, _, _, ctxt) (s as I.Sym (n, _), es) = +fun mk_app (_, terms, _, _, _, ctxt) (s as Z3_Interface.Sym (n, _), es) = mk_fun (fn cts => - (case I.mk_builtin_fun ctxt s cts of + (case Z3_Interface.mk_builtin_fun ctxt s cts of SOME ct => SOME ct | NONE => Symtab.lookup terms n |> Option.map (Drule.list_comb o rpair cts))) es @@ -243,8 +244,8 @@ | part (NONE, i) (cts, ps) = (cts, i :: ps) val (args', prems) = fold (part o `(lookup_expr cx)) args ([], []) val (cts, vss) = split_list args' - val step = - Proof_Step {rule=r, args=rev cts, prems=rev prems, prop=U.mk_cprop ct} + val step = Proof_Step {rule=r, args=rev cts, prems=rev prems, + prop = SMT_Utils.mk_cprop ct} val vars' = fold (union (op =)) (vs :: vss) vars in (typs, terms, exprs, (k, step) :: steps, vars', ctxt) end @@ -326,8 +327,8 @@ fun name st = (Scan.lift (Scan.many1 is_char) >> implode) st -fun sym st = - (name -- Scan.optional (bra (seps_by ($$ ":") sym)) [] >> I.Sym) st +fun sym st = (name -- + Scan.optional (bra (seps_by ($$ ":") sym)) [] >> Z3_Interface.Sym) st fun id st = ($$ "#" |-- nat_num) st @@ -337,7 +338,7 @@ fun sort st = Scan.first [ this "array" |-- bra (sort --| $$ ":" -- sort) >> (op -->), par (this "->" |-- seps1 sort) >> ((op --->) o split_last), - sym :|-- (fn s as I.Sym (n, _) => lookup_context mk_typ s :|-- (fn + sym :|-- (fn s as Z3_Interface.Sym (n, _) => lookup_context mk_typ s :|-- (fn SOME T => Scan.succeed T | NONE => scan_exn ("unknown sort: " ^ quote n)))] st @@ -348,11 +349,13 @@ SOME n' => Scan.succeed n' | NONE => scan_exn ("unknown number: " ^ quote (string_of_int i))) -fun appl (app as (I.Sym (n, _), _)) = lookup_context mk_app app :|-- (fn - SOME app' => Scan.succeed app' - | NONE => scan_exn ("unknown function symbol: " ^ quote n)) +fun appl (app as (Z3_Interface.Sym (n, _), _)) = + lookup_context mk_app app :|-- (fn + SOME app' => Scan.succeed app' + | NONE => scan_exn ("unknown function symbol: " ^ quote n)) -fun bv_size st = (digits >> (fn sz => I.Sym ("bv", [I.Sym (sz, [])]))) st +fun bv_size st = (digits >> (fn sz => + Z3_Interface.Sym ("bv", [Z3_Interface.Sym (sz, [])]))) st fun bv_number_sort st = (bv_size :|-- lookup_context mk_typ :|-- (fn SOME cT => Scan.succeed cT @@ -364,7 +367,7 @@ fun frac_number st = ( int_num --| $$ "/" -- int_num --| this "::" -- sort :|-- (fn ((i, j), T) => numb (i, T) -- numb (j, T) :|-- (fn (n, m) => - appl (I.Sym ("/", []), [n, m])))) st + appl (Z3_Interface.Sym ("/", []), [n, m])))) st fun plain_number st = (int_num --| this "::" -- sort :|-- numb) st diff -r 49feace87649 -r 6792a5c92a58 src/HOL/Tools/SMT/z3_proof_reconstruction.ML --- a/src/HOL/Tools/SMT/z3_proof_reconstruction.ML Mon Dec 20 21:04:45 2010 +0100 +++ b/src/HOL/Tools/SMT/z3_proof_reconstruction.ML Mon Dec 20 22:02:57 2010 +0100 @@ -15,11 +15,6 @@ structure Z3_Proof_Reconstruction: Z3_PROOF_RECONSTRUCTION = struct -structure U = SMT_Utils -structure P = Z3_Proof_Parser -structure T = Z3_Proof_Tools -structure L = Z3_Proof_Literals -structure M = Z3_Proof_Methods fun z3_exn msg = raise SMT_Failure.SMT (SMT_Failure.Other_Failure ("Z3 proof reconstruction: " ^ msg)) @@ -43,7 +38,8 @@ val merge = Net.merge eq ) - val prep = `Thm.prop_of o Simplifier.rewrite_rule [L.rewrite_true] + val prep = + `Thm.prop_of o Simplifier.rewrite_rule [Z3_Proof_Literals.rewrite_true] fun ins thm net = Net.insert_term eq (prep thm) net handle Net.INSERT => net fun del thm net = Net.delete_term eq (prep thm) net handle Net.DELETE => net @@ -55,7 +51,7 @@ val add_z3_rule = Z3_Rules.map o ins fun by_schematic_rule ctxt ct = - the (T.net_instance (Z3_Rules.get (Context.Proof ctxt)) ct) + the (Z3_Proof_Tools.net_instance (Z3_Rules.get (Context.Proof ctxt)) ct) val z3_rules_setup = Attrib.setup (Binding.name z3_ruleN) (Attrib.add_del add del) description #> @@ -115,7 +111,7 @@ datatype theorem = Thm of thm | (* theorem without special features *) MetaEq of thm | (* meta equality "t == s" *) - Literals of thm * L.littab + Literals of thm * Z3_Proof_Literals.littab (* "P1 & ... & Pn" and table of all literals P1, ..., Pn *) fun thm_of (Thm thm) = thm @@ -126,7 +122,7 @@ | meta_eq_of p = mk_meta_eq (thm_of p) fun literals_of (Literals (_, lits)) = lits - | literals_of p = L.make_littab [thm_of p] + | literals_of p = Z3_Proof_Literals.make_littab [thm_of p] @@ -143,27 +139,27 @@ (Simplifier.context ctxt Simplifier.empty_ss addsimps eqs) val prep_rules = [@{thm Let_def}, remove_trigger, remove_weight, - remove_fun_app, L.rewrite_true] + remove_fun_app, Z3_Proof_Literals.rewrite_true] fun rewrite ctxt eqs = Conv.fconv_rule (rewrite_conv ctxt eqs) fun burrow_snd_option f (i, thm) = Option.map (pair i) (f thm) fun lookup_assm assms_net ct = - T.net_instance' burrow_snd_option assms_net ct + Z3_Proof_Tools.net_instance' burrow_snd_option assms_net ct |> Option.map (fn ithm as (_, thm) => (ithm, Thm.cprop_of thm aconvc ct)) in fun add_asserted outer_ctxt rewrite_rules assms asserted ctxt = let - val eqs = map (rewrite ctxt [L.rewrite_true]) rewrite_rules + val eqs = map (rewrite ctxt [Z3_Proof_Literals.rewrite_true]) rewrite_rules val eqs' = union Thm.eq_thm eqs prep_rules val assms_net = assms |> map (apsnd (rewrite ctxt eqs')) |> map (apsnd (Conv.fconv_rule Thm.eta_conversion)) - |> T.thm_net_of snd + |> Z3_Proof_Tools.thm_net_of snd fun revert_conv ctxt = rewrite_conv ctxt eqs' then_conv Thm.eta_conversion @@ -202,17 +198,20 @@ (* P = Q ==> P ==> Q or P --> Q ==> P ==> Q *) local - val meta_iffD1 = @{lemma "P == Q ==> P ==> (Q::bool)" by simp} - val meta_iffD1_c = T.precompose2 Thm.dest_binop meta_iffD1 + val precomp = Z3_Proof_Tools.precompose2 + val comp = Z3_Proof_Tools.compose - val iffD1_c = T.precompose2 (Thm.dest_binop o Thm.dest_arg) @{thm iffD1} - val mp_c = T.precompose2 (Thm.dest_binop o Thm.dest_arg) @{thm mp} + val meta_iffD1 = @{lemma "P == Q ==> P ==> (Q::bool)" by simp} + val meta_iffD1_c = precomp Thm.dest_binop meta_iffD1 + + val iffD1_c = precomp (Thm.dest_binop o Thm.dest_arg) @{thm iffD1} + val mp_c = precomp (Thm.dest_binop o Thm.dest_arg) @{thm mp} in -fun mp (MetaEq thm) p = Thm (Thm.implies_elim (T.compose meta_iffD1_c thm) p) +fun mp (MetaEq thm) p = Thm (Thm.implies_elim (comp meta_iffD1_c thm) p) | mp p_q p = let val pq = thm_of p_q - val thm = T.compose iffD1_c pq handle THM _ => T.compose mp_c pq + val thm = comp iffD1_c pq handle THM _ => comp mp_c pq in Thm (Thm.implies_elim thm p) end end @@ -220,23 +219,25 @@ (* and_elim: P1 & ... & Pn ==> Pi *) (* not_or_elim: ~(P1 | ... | Pn) ==> ~Pi *) local - fun is_sublit conj t = L.exists_lit conj (fn u => u aconv t) + fun is_sublit conj t = Z3_Proof_Literals.exists_lit conj (fn u => u aconv t) fun derive conj t lits idx ptab = let - val lit = the (L.get_first_lit (is_sublit conj t) lits) - val ls = L.explode conj false false [t] lit - val lits' = fold L.insert_lit ls (L.delete_lit lit lits) + val lit = the (Z3_Proof_Literals.get_first_lit (is_sublit conj t) lits) + val ls = Z3_Proof_Literals.explode conj false false [t] lit + val lits' = fold Z3_Proof_Literals.insert_lit ls + (Z3_Proof_Literals.delete_lit lit lits) fun upd thm = Literals (thm_of thm, lits') - in (the (L.lookup_lit lits' t), Inttab.map_entry idx upd ptab) end + val ptab' = Inttab.map_entry idx upd ptab + in (the (Z3_Proof_Literals.lookup_lit lits' t), ptab') end fun lit_elim conj (p, idx) ct ptab = let val lits = literals_of p in - (case L.lookup_lit lits (U.term_of ct) of + (case Z3_Proof_Literals.lookup_lit lits (SMT_Utils.term_of ct) of SOME lit => (Thm lit, ptab) - | NONE => apfst Thm (derive conj (U.term_of ct) lits idx ptab)) + | NONE => apfst Thm (derive conj (SMT_Utils.term_of ct) lits idx ptab)) end in val and_elim = lit_elim true @@ -248,36 +249,42 @@ local fun step lit thm = Thm.implies_elim (Thm.implies_intr (Thm.cprop_of lit) thm) lit - val explode_disj = L.explode false false false + val explode_disj = Z3_Proof_Literals.explode false false false fun intro hyps thm th = fold step (explode_disj hyps th) thm fun dest_ccontr ct = [Thm.dest_arg (Thm.dest_arg (Thm.dest_arg1 ct))] - val ccontr = T.precompose dest_ccontr @{thm ccontr} + val ccontr = Z3_Proof_Tools.precompose dest_ccontr @{thm ccontr} in fun lemma thm ct = let - val cu = L.negate (Thm.dest_arg ct) + val cu = Z3_Proof_Literals.negate (Thm.dest_arg ct) val hyps = map_filter (try HOLogic.dest_Trueprop) (#hyps (Thm.rep_thm thm)) - in Thm (T.compose ccontr (T.under_assumption (intro hyps thm) cu)) end + val th = Z3_Proof_Tools.under_assumption (intro hyps thm) cu + in Thm (Z3_Proof_Tools.compose ccontr th) end end (* \/{P1, ..., Pn, Q1, ..., Qn}, ~P1, ..., ~Pn ==> \/{Q1, ..., Qn} *) local - val explode_disj = L.explode false true false - val join_disj = L.join false + val explode_disj = Z3_Proof_Literals.explode false true false + val join_disj = Z3_Proof_Literals.join false fun unit thm thms th = - let val t = @{const Not} $ U.prop_of thm and ts = map U.prop_of thms - in join_disj (L.make_littab (thms @ explode_disj ts th)) t end + let + val t = @{const Not} $ SMT_Utils.prop_of thm + val ts = map SMT_Utils.prop_of thms + in + join_disj (Z3_Proof_Literals.make_littab (thms @ explode_disj ts th)) t + end fun dest_arg2 ct = Thm.dest_arg (Thm.dest_arg ct) fun dest ct = pairself dest_arg2 (Thm.dest_binop ct) - val contrapos = T.precompose2 dest @{lemma "(~P ==> ~Q) ==> Q ==> P" by fast} + val contrapos = + Z3_Proof_Tools.precompose2 dest @{lemma "(~P ==> ~Q) ==> Q ==> P" by fast} in fun unit_resolution thm thms ct = - L.negate (Thm.dest_arg ct) - |> T.under_assumption (unit thm thms) - |> Thm o T.discharge thm o T.compose contrapos + Z3_Proof_Literals.negate (Thm.dest_arg ct) + |> Z3_Proof_Tools.under_assumption (unit thm thms) + |> Thm o Z3_Proof_Tools.discharge thm o Z3_Proof_Tools.compose contrapos end @@ -293,7 +300,7 @@ (* distributivity of | over & *) fun distributivity ctxt = Thm o try_apply ctxt [] [ - named ctxt "fast" (T.by_tac (Classical.fast_tac HOL_cs))] + named ctxt "fast" (Z3_Proof_Tools.by_tac (Classical.fast_tac HOL_cs))] (* FIXME: not very well tested *) @@ -305,11 +312,15 @@ val disjI4 = @{lemma "(Q ==> P) ==> P | ~Q" by fast} fun prove' conj1 conj2 ct2 thm = - let val lits = L.true_thm :: L.explode conj1 true (conj1 <> conj2) [] thm - in L.join conj2 (L.make_littab lits) (Thm.term_of ct2) end + let + val littab = + Z3_Proof_Literals.explode conj1 true (conj1 <> conj2) [] thm + |> cons Z3_Proof_Literals.true_thm + |> Z3_Proof_Literals.make_littab + in Z3_Proof_Literals.join conj2 littab (Thm.term_of ct2) end fun prove rule (ct1, conj1) (ct2, conj2) = - T.under_assumption (prove' conj1 conj2 ct2) ct1 COMP rule + Z3_Proof_Tools.under_assumption (prove' conj1 conj2 ct2) ct1 COMP rule fun prove_def_axiom ct = let val (ct1, ct2) = Thm.dest_binop (Thm.dest_arg ct) @@ -318,32 +329,34 @@ @{const Not} $ (@{const HOL.conj} $ _ $ _) => prove disjI1 (Thm.dest_arg ct1, true) (ct2, true) | @{const HOL.conj} $ _ $ _ => - prove disjI3 (L.negate ct2, false) (ct1, true) + prove disjI3 (Z3_Proof_Literals.negate ct2, false) (ct1, true) | @{const Not} $ (@{const HOL.disj} $ _ $ _) => - prove disjI3 (L.negate ct2, false) (ct1, false) + prove disjI3 (Z3_Proof_Literals.negate ct2, false) (ct1, false) | @{const HOL.disj} $ _ $ _ => - prove disjI2 (L.negate ct1, false) (ct2, true) + prove disjI2 (Z3_Proof_Literals.negate ct1, false) (ct2, true) | Const (@{const_name distinct}, _) $ _ => let fun dis_conv cv = Conv.arg_conv (Conv.arg1_conv cv) + val unfold_dis_conv = dis_conv Z3_Proof_Tools.unfold_distinct_conv fun prv cu = let val (cu1, cu2) = Thm.dest_binop (Thm.dest_arg cu) in prove disjI4 (Thm.dest_arg cu2, true) (cu1, true) end - in T.with_conv (dis_conv T.unfold_distinct_conv) prv ct end + in Z3_Proof_Tools.with_conv unfold_dis_conv prv ct end | @{const Not} $ (Const (@{const_name distinct}, _) $ _) => let fun dis_conv cv = Conv.arg_conv (Conv.arg1_conv (Conv.arg_conv cv)) + val unfold_dis_conv = dis_conv Z3_Proof_Tools.unfold_distinct_conv fun prv cu = let val (cu1, cu2) = Thm.dest_binop (Thm.dest_arg cu) in prove disjI1 (Thm.dest_arg cu1, true) (cu2, true) end - in T.with_conv (dis_conv T.unfold_distinct_conv) prv ct end + in Z3_Proof_Tools.with_conv unfold_dis_conv prv ct end | _ => raise CTERM ("prove_def_axiom", [ct])) end in fun def_axiom ctxt = Thm o try_apply ctxt [] [ named ctxt "conj/disj/distinct" prove_def_axiom, - T.by_abstraction (true, false) ctxt [] (fn ctxt' => - named ctxt' "simp+fast" (T.by_tac simp_fast_tac))] + Z3_Proof_Tools.by_abstraction (true, false) ctxt [] (fn ctxt' => + named ctxt' "simp+fast" (Z3_Proof_Tools.by_tac simp_fast_tac))] end @@ -360,14 +373,14 @@ @{lemma "(~P | n = s) & (P | n = t) ==> (if P then s else t) == n" by (atomize(full)) fastsimp} ] - val inst_rule = T.match_instantiate Thm.dest_arg + val inst_rule = Z3_Proof_Tools.match_instantiate Thm.dest_arg fun apply_rule ct = (case get_first (try (inst_rule ct)) intro_rules of SOME thm => thm | NONE => raise CTERM ("intro_def", [ct])) in -fun intro_def ct = T.make_hyp_def (apply_rule ct) #>> Thm +fun intro_def ct = Z3_Proof_Tools.make_hyp_def (apply_rule ct) #>> Thm fun apply_def thm = get_first (try (fn rule => MetaEq (thm COMP rule))) apply_rules @@ -394,17 +407,20 @@ (Tactic.match_tac qs1 THEN' nnf_quant_tac thm qs) ORELSE' (Tactic.match_tac qs2 THEN' nnf_quant_tac thm qs)) i st + fun nnf_quant_tac_varified vars eq = + nnf_quant_tac (Z3_Proof_Tools.varify vars eq) + fun nnf_quant vars qs p ct = - T.as_meta_eq ct - |> T.by_tac (nnf_quant_tac (T.varify vars (meta_eq_of p)) qs) + Z3_Proof_Tools.as_meta_eq ct + |> Z3_Proof_Tools.by_tac (nnf_quant_tac_varified vars (meta_eq_of p) qs) fun prove_nnf ctxt = try_apply ctxt [] [ - named ctxt "conj/disj" L.prove_conj_disj_eq, - T.by_abstraction (true, false) ctxt [] (fn ctxt' => - named ctxt' "simp+fast" (T.by_tac simp_fast_tac))] + named ctxt "conj/disj" Z3_Proof_Literals.prove_conj_disj_eq, + Z3_Proof_Tools.by_abstraction (true, false) ctxt [] (fn ctxt' => + named ctxt' "simp+fast" (Z3_Proof_Tools.by_tac simp_fast_tac))] in fun nnf ctxt vars ps ct = - (case U.term_of ct of + (case SMT_Utils.term_of ct of _ $ (l as Const _ $ Abs _) $ (r as Const _ $ Abs _) => if l aconv r then MetaEq (Thm.reflexive (Thm.dest_arg (Thm.dest_arg ct))) @@ -414,8 +430,9 @@ | _ => let val nnf_rewr_conv = Conv.arg_conv (Conv.arg_conv - (T.unfold_eqs ctxt (map (Thm.symmetric o meta_eq_of) ps))) - in Thm (T.with_conv nnf_rewr_conv (prove_nnf ctxt) ct) end) + (Z3_Proof_Tools.unfold_eqs ctxt + (map (Thm.symmetric o meta_eq_of) ps))) + in Thm (Z3_Proof_Tools.with_conv nnf_rewr_conv (prove_nnf ctxt) ct) end) end @@ -483,15 +500,15 @@ SOME eq => eq | NONE => if exn then raise MONO else prove_refl cp) - val prove_eq_exn = prove_eq true - and prove_eq_safe = prove_eq false + val prove_exn = prove_eq true + and prove_safe = prove_eq false fun mono f (cp as (cl, _)) = (case Term.head_of (Thm.term_of cl) of - @{const HOL.conj} => prove_nary L.is_conj (prove_eq_exn f) - | @{const HOL.disj} => prove_nary L.is_disj (prove_eq_exn f) - | Const (@{const_name distinct}, _) => prove_distinct (prove_eq_safe f) - | _ => prove (prove_eq_safe f)) cp + @{const HOL.conj} => prove_nary Z3_Proof_Literals.is_conj (prove_exn f) + | @{const HOL.disj} => prove_nary Z3_Proof_Literals.is_disj (prove_exn f) + | Const (@{const_name distinct}, _) => prove_distinct (prove_safe f) + | _ => prove (prove_safe f)) cp in fun monotonicity eqs ct = let @@ -499,7 +516,7 @@ val teqs = maps (and_symmetric o `Thm.prop_of o meta_eq_of) eqs val lookup = AList.lookup (op aconv) teqs val cp = Thm.dest_binop (Thm.dest_arg ct) - in MetaEq (prove_eq_exn lookup cp handle MONO => mono lookup cp) end + in MetaEq (prove_exn lookup cp handle MONO => mono lookup cp) end end @@ -507,7 +524,9 @@ local val rule = @{lemma "a = b == b = a" by (atomize(full)) (rule eq_commute)} in -fun commutativity ct = MetaEq (T.match_instantiate I (T.as_meta_eq ct) rule) +fun commutativity ct = + MetaEq (Z3_Proof_Tools.match_instantiate I + (Z3_Proof_Tools.as_meta_eq ct) rule) end @@ -524,21 +543,22 @@ fun quant_intro vars p ct = let val thm = meta_eq_of p - val rules' = T.varify vars thm :: rules - val cu = T.as_meta_eq ct - in MetaEq (T.by_tac (REPEAT_ALL_NEW (Tactic.match_tac rules')) cu) end + val rules' = Z3_Proof_Tools.varify vars thm :: rules + val cu = Z3_Proof_Tools.as_meta_eq ct + val tac = REPEAT_ALL_NEW (Tactic.match_tac rules') + in MetaEq (Z3_Proof_Tools.by_tac tac cu) end end (* |- ((ALL x. P x) | Q) = (ALL x. P x | Q) *) fun pull_quant ctxt = Thm o try_apply ctxt [] [ - named ctxt "fast" (T.by_tac (Classical.fast_tac HOL_cs))] + named ctxt "fast" (Z3_Proof_Tools.by_tac (Classical.fast_tac HOL_cs))] (* FIXME: not very well tested *) (* |- (ALL x. P x & Q x) = ((ALL x. P x) & (ALL x. Q x)) *) fun push_quant ctxt = Thm o try_apply ctxt [] [ - named ctxt "fast" (T.by_tac (Classical.fast_tac HOL_cs))] + named ctxt "fast" (Z3_Proof_Tools.by_tac (Classical.fast_tac HOL_cs))] (* FIXME: not very well tested *) @@ -556,13 +576,13 @@ Tactic.match_tac [@{thm refl}, @{thm iff_allI}, @{thm iff_exI}] ORELSE' CONVERSION (elim_unused_conv ctxt)) in -fun elim_unused_vars ctxt = Thm o T.by_tac (elim_unused_tac ctxt) +fun elim_unused_vars ctxt = Thm o Z3_Proof_Tools.by_tac (elim_unused_tac ctxt) end (* |- (ALL x1 ... xn. ~(x1 = t1 & ... xn = tn) | P x1 ... xn) = P t1 ... tn *) fun dest_eq_res ctxt = Thm o try_apply ctxt [] [ - named ctxt "fast" (T.by_tac (Classical.fast_tac HOL_cs))] + named ctxt "fast" (Z3_Proof_Tools.by_tac (Classical.fast_tac HOL_cs))] (* FIXME: not very well tested *) @@ -570,7 +590,7 @@ local val rule = @{lemma "~ P x | Q ==> ~(ALL x. P x) | Q" by fast} in -val quant_inst = Thm o T.by_tac ( +val quant_inst = Thm o Z3_Proof_Tools.by_tac ( REPEAT_ALL_NEW (Tactic.match_tac [rule]) THEN' Tactic.rtac @{thm excluded_middle}) end @@ -599,7 +619,7 @@ fun kind (Const (@{const_name Ex}, _) $ _) = (sk_ex_rule, I, I) | kind (@{const Not} $ (Const (@{const_name All}, _) $ _)) = - (sk_all_rule, Thm.dest_arg, L.negate) + (sk_all_rule, Thm.dest_arg, Z3_Proof_Literals.negate) | kind t = raise TERM ("skolemize", [t]) fun dest_abs_type (Abs (_, T, _)) = T @@ -628,7 +648,8 @@ (case mct of SOME ct => ctxt - |> T.make_hyp_def (inst_sk rule (Thm.instantiate_cterm ([], is) cb) ct) + |> Z3_Proof_Tools.make_hyp_def + (inst_sk rule (Thm.instantiate_cterm ([], is) cb) ct) |>> pair ((cv, ct) :: is) o Thm.transitive thm | NONE => ((is, transitive (Conv.rewr_conv elim) thm), ctxt)) in @@ -649,10 +670,12 @@ (* theory lemmas: linear arithmetic, arrays *) fun th_lemma ctxt simpset thms = Thm o try_apply ctxt thms [ - T.by_abstraction (false, true) ctxt thms (fn ctxt' => T.by_tac ( - NAMED ctxt' "arith" (Arith_Data.arith_tac ctxt') - ORELSE' NAMED ctxt' "simp+arith" (Simplifier.simp_tac simpset THEN_ALL_NEW - Arith_Data.arith_tac ctxt')))] + Z3_Proof_Tools.by_abstraction (false, true) ctxt thms (fn ctxt' => + Z3_Proof_Tools.by_tac ( + NAMED ctxt' "arith" (Arith_Data.arith_tac ctxt') + ORELSE' NAMED ctxt' "simp+arith" ( + Simplifier.simp_tac simpset + THEN_ALL_NEW Arith_Data.arith_tac ctxt')))] (* rewriting: prove equalities: @@ -680,14 +703,18 @@ | prep (Literals (thm, _)) = spec_meta_eq_of thm fun unfold_conv ctxt ths = - Conv.arg_conv (Conv.binop_conv (T.unfold_eqs ctxt (map prep ths))) + Conv.arg_conv (Conv.binop_conv (Z3_Proof_Tools.unfold_eqs ctxt + (map prep ths))) fun with_conv _ [] prv = prv - | with_conv ctxt ths prv = T.with_conv (unfold_conv ctxt ths) prv + | with_conv ctxt ths prv = + Z3_Proof_Tools.with_conv (unfold_conv ctxt ths) prv 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 + Conv.arg_conv (Conv.binop_conv + (Conv.try_conv Z3_Proof_Tools.unfold_distinct_conv)) + val prove_conj_disj_eq = + Z3_Proof_Tools.with_conv unfold_conv Z3_Proof_Literals.prove_conj_disj_eq fun assume_prems ctxt thm = Assumption.add_assumes (Drule.cprems_of thm) ctxt @@ -697,20 +724,23 @@ 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)) + Z3_Proof_Tools.by_abstraction (true, false) ctxt [] (fn ctxt' => + Z3_Proof_Tools.by_tac ( + NAMED ctxt' "simp (logic)" (Simplifier.simp_tac simpset) + THEN_ALL_NEW NAMED ctxt' "fast (logic)" (Classical.fast_tac HOL_cs))), + Z3_Proof_Tools.by_abstraction (false, true) ctxt [] (fn ctxt' => + Z3_Proof_Tools.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')))), + Z3_Proof_Tools.by_abstraction (true, true) ctxt [] (fn ctxt' => + Z3_Proof_Tools.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" (Z3_Proof_Methods.prove_injectivity ctxt)]) ct)) end @@ -721,7 +751,7 @@ (** tracing and checking **) fun trace_before ctxt idx = SMT_Config.trace_msg ctxt (fn r => - "Z3: #" ^ string_of_int idx ^ ": " ^ P.string_of_rule r) + "Z3: #" ^ string_of_int idx ^ ": " ^ Z3_Proof_Parser.string_of_rule r) fun check_after idx r ps ct (p, (ctxt, _)) = if not (Config.get ctxt SMT_Config.trace) then () @@ -729,11 +759,13 @@ let val thm = thm_of p |> tap (Thm.join_proofs o single) in if (Thm.cprop_of thm) aconvc ct then () - else z3_exn (Pretty.string_of (Pretty.big_list ("proof step failed: " ^ - quote (P.string_of_rule r) ^ " (#" ^ string_of_int idx ^ ")") + else + z3_exn (Pretty.string_of (Pretty.big_list + ("proof step failed: " ^ quote (Z3_Proof_Parser.string_of_rule r) ^ + " (#" ^ string_of_int idx ^ ")") (pretty_goal ctxt (map (thm_of o fst) ps) (Thm.prop_of thm) @ - [Pretty.block [Pretty.str "expected: ", - Syntax.pretty_term ctxt (Thm.term_of ct)]]))) + [Pretty.block [Pretty.str "expected: ", + Syntax.pretty_term ctxt (Thm.term_of ct)]]))) end @@ -741,61 +773,67 @@ local fun not_supported r = raise Fail ("Z3: proof rule not implemented: " ^ - quote (P.string_of_rule r)) + quote (Z3_Proof_Parser.string_of_rule r)) fun prove_step simpset vars r ps ct (cxp as (cx, ptab)) = (case (r, ps) of (* core rules *) - (P.True_Axiom, _) => (Thm L.true_thm, cxp) - | (P.Asserted, _) => raise Fail "bad assertion" - | (P.Goal, _) => raise Fail "bad assertion" - | (P.Modus_Ponens, [(p, _), (q, _)]) => (mp q (thm_of p), cxp) - | (P.Modus_Ponens_Oeq, [(p, _), (q, _)]) => (mp q (thm_of p), cxp) - | (P.And_Elim, [(p, i)]) => and_elim (p, i) ct ptab ||> pair cx - | (P.Not_Or_Elim, [(p, i)]) => not_or_elim (p, i) ct ptab ||> pair cx - | (P.Hypothesis, _) => (Thm (Thm.assume ct), cxp) - | (P.Lemma, [(p, _)]) => (lemma (thm_of p) ct, cxp) - | (P.Unit_Resolution, (p, _) :: ps) => + (Z3_Proof_Parser.True_Axiom, _) => (Thm Z3_Proof_Literals.true_thm, cxp) + | (Z3_Proof_Parser.Asserted, _) => raise Fail "bad assertion" + | (Z3_Proof_Parser.Goal, _) => raise Fail "bad assertion" + | (Z3_Proof_Parser.Modus_Ponens, [(p, _), (q, _)]) => + (mp q (thm_of p), cxp) + | (Z3_Proof_Parser.Modus_Ponens_Oeq, [(p, _), (q, _)]) => + (mp q (thm_of p), cxp) + | (Z3_Proof_Parser.And_Elim, [(p, i)]) => + and_elim (p, i) ct ptab ||> pair cx + | (Z3_Proof_Parser.Not_Or_Elim, [(p, i)]) => + not_or_elim (p, i) ct ptab ||> pair cx + | (Z3_Proof_Parser.Hypothesis, _) => (Thm (Thm.assume ct), cxp) + | (Z3_Proof_Parser.Lemma, [(p, _)]) => (lemma (thm_of p) ct, cxp) + | (Z3_Proof_Parser.Unit_Resolution, (p, _) :: ps) => (unit_resolution (thm_of p) (map (thm_of o fst) ps) ct, cxp) - | (P.Iff_True, [(p, _)]) => (iff_true (thm_of p), cxp) - | (P.Iff_False, [(p, _)]) => (iff_false (thm_of p), cxp) - | (P.Distributivity, _) => (distributivity cx ct, cxp) - | (P.Def_Axiom, _) => (def_axiom cx ct, cxp) - | (P.Intro_Def, _) => intro_def ct cx ||> rpair ptab - | (P.Apply_Def, [(p, _)]) => (apply_def (thm_of p), cxp) - | (P.Iff_Oeq, [(p, _)]) => (p, cxp) - | (P.Nnf_Pos, _) => (nnf cx vars (map fst ps) ct, cxp) - | (P.Nnf_Neg, _) => (nnf cx vars (map fst ps) ct, cxp) + | (Z3_Proof_Parser.Iff_True, [(p, _)]) => (iff_true (thm_of p), cxp) + | (Z3_Proof_Parser.Iff_False, [(p, _)]) => (iff_false (thm_of p), cxp) + | (Z3_Proof_Parser.Distributivity, _) => (distributivity cx ct, cxp) + | (Z3_Proof_Parser.Def_Axiom, _) => (def_axiom cx ct, cxp) + | (Z3_Proof_Parser.Intro_Def, _) => intro_def ct cx ||> rpair ptab + | (Z3_Proof_Parser.Apply_Def, [(p, _)]) => (apply_def (thm_of p), cxp) + | (Z3_Proof_Parser.Iff_Oeq, [(p, _)]) => (p, cxp) + | (Z3_Proof_Parser.Nnf_Pos, _) => (nnf cx vars (map fst ps) ct, cxp) + | (Z3_Proof_Parser.Nnf_Neg, _) => (nnf cx vars (map fst ps) ct, cxp) (* equality rules *) - | (P.Reflexivity, _) => (refl ct, cxp) - | (P.Symmetry, [(p, _)]) => (symm p, cxp) - | (P.Transitivity, [(p, _), (q, _)]) => (trans p q, cxp) - | (P.Monotonicity, _) => (monotonicity (map fst ps) ct, cxp) - | (P.Commutativity, _) => (commutativity ct, cxp) + | (Z3_Proof_Parser.Reflexivity, _) => (refl ct, cxp) + | (Z3_Proof_Parser.Symmetry, [(p, _)]) => (symm p, cxp) + | (Z3_Proof_Parser.Transitivity, [(p, _), (q, _)]) => (trans p q, cxp) + | (Z3_Proof_Parser.Monotonicity, _) => (monotonicity (map fst ps) ct, cxp) + | (Z3_Proof_Parser.Commutativity, _) => (commutativity ct, cxp) (* quantifier rules *) - | (P.Quant_Intro, [(p, _)]) => (quant_intro vars p ct, cxp) - | (P.Pull_Quant, _) => (pull_quant cx ct, cxp) - | (P.Push_Quant, _) => (push_quant cx ct, cxp) - | (P.Elim_Unused_Vars, _) => (elim_unused_vars cx ct, cxp) - | (P.Dest_Eq_Res, _) => (dest_eq_res cx ct, cxp) - | (P.Quant_Inst, _) => (quant_inst ct, cxp) - | (P.Skolemize, _) => skolemize ct cx ||> rpair ptab + | (Z3_Proof_Parser.Quant_Intro, [(p, _)]) => (quant_intro vars p ct, cxp) + | (Z3_Proof_Parser.Pull_Quant, _) => (pull_quant cx ct, cxp) + | (Z3_Proof_Parser.Push_Quant, _) => (push_quant cx ct, cxp) + | (Z3_Proof_Parser.Elim_Unused_Vars, _) => (elim_unused_vars cx ct, cxp) + | (Z3_Proof_Parser.Dest_Eq_Res, _) => (dest_eq_res cx ct, cxp) + | (Z3_Proof_Parser.Quant_Inst, _) => (quant_inst ct, cxp) + | (Z3_Proof_Parser.Skolemize, _) => skolemize ct cx ||> rpair ptab (* theory rules *) - | (P.Th_Lemma _, _) => (* FIXME: use arguments *) + | (Z3_Proof_Parser.Th_Lemma _, _) => (* FIXME: use arguments *) (th_lemma cx simpset (map (thm_of o fst) ps) ct, cxp) - | (P.Rewrite, _) => rewrite simpset [] ct cx ||> rpair ptab - | (P.Rewrite_Star, ps) => rewrite simpset (map fst ps) ct cx ||> rpair ptab + | (Z3_Proof_Parser.Rewrite, _) => rewrite simpset [] ct cx ||> rpair ptab + | (Z3_Proof_Parser.Rewrite_Star, ps) => + rewrite simpset (map fst ps) ct cx ||> rpair ptab - | (P.Nnf_Star, _) => not_supported r - | (P.Cnf_Star, _) => not_supported r - | (P.Transitivity_Star, _) => not_supported r - | (P.Pull_Quant_Star, _) => not_supported r + | (Z3_Proof_Parser.Nnf_Star, _) => not_supported r + | (Z3_Proof_Parser.Cnf_Star, _) => not_supported r + | (Z3_Proof_Parser.Transitivity_Star, _) => not_supported r + | (Z3_Proof_Parser.Pull_Quant_Star, _) => not_supported r - | _ => raise Fail ("Z3: proof rule " ^ quote (P.string_of_rule r) ^ - " has an unexpected number of arguments.")) + | _ => raise Fail ("Z3: proof rule " ^ + quote (Z3_Proof_Parser.string_of_rule r) ^ + " has an unexpected number of arguments.")) fun lookup_proof ptab idx = (case Inttab.lookup ptab idx of @@ -804,7 +842,7 @@ fun prove simpset vars (idx, step) (_, cxp as (ctxt, ptab)) = let - val P.Proof_Step {rule=r, prems, prop, ...} = step + val Z3_Proof_Parser.Proof_Step {rule=r, prems, prop, ...} = step val ps = map (lookup_proof ptab) prems val _ = trace_before ctxt idx r val (thm, (ctxt', ptab')) = @@ -832,9 +870,10 @@ fun reconstruct outer_ctxt recon output = let val {context=ctxt, typs, terms, rewrite_rules, assms} = recon - val (asserted, steps, vars, ctxt1) = P.parse ctxt typs terms output + val (asserted, steps, vars, ctxt1) = + Z3_Proof_Parser.parse ctxt typs terms output - val simpset = T.make_simpset ctxt1 (Z3_Simps.get ctxt1) + val simpset = Z3_Proof_Tools.make_simpset ctxt1 (Z3_Simps.get ctxt1) val ((is, rules), cxp as (ctxt2, _)) = add_asserted outer_ctxt rewrite_rules assms asserted ctxt1 diff -r 49feace87649 -r 6792a5c92a58 src/HOL/Tools/SMT/z3_proof_tools.ML --- a/src/HOL/Tools/SMT/z3_proof_tools.ML Mon Dec 20 21:04:45 2010 +0100 +++ b/src/HOL/Tools/SMT/z3_proof_tools.ML Mon Dec 20 22:02:57 2010 +0100 @@ -44,14 +44,12 @@ structure Z3_Proof_Tools: Z3_PROOF_TOOLS = struct -structure U = SMT_Utils -structure I = Z3_Interface - (* modifying terms *) -fun as_meta_eq ct = uncurry U.mk_cequals (Thm.dest_binop (U.dest_cprop ct)) +fun as_meta_eq ct = + uncurry SMT_Utils.mk_cequals (Thm.dest_binop (SMT_Utils.dest_cprop ct)) @@ -80,7 +78,7 @@ (* proof combinators *) fun under_assumption f ct = - let val ct' = U.mk_cprop ct + let val ct' = SMT_Utils.mk_cprop ct in Thm.implies_intr ct' (f (Thm.assume ct')) end fun with_conv conv prove ct = @@ -109,7 +107,7 @@ let val (lhs, rhs) = Thm.dest_binop (Thm.cprem_of thm 1) val (cf, cvs) = Drule.strip_comb lhs - val eq = U.mk_cequals cf (fold_rev Thm.cabs cvs rhs) + val eq = SMT_Utils.mk_cequals cf (fold_rev Thm.cabs cvs rhs) fun apply cv th = Thm.combination th (Thm.reflexive cv) |> Conv.fconv_rule (Conv.arg_conv (Thm.beta_conversion false)) @@ -149,8 +147,8 @@ | NONE => let val (n, ctxt') = yield_singleton Variable.variant_fixes "x" ctxt - val cv = U.certify ctxt' - (Free (n, map U.typ_of cvs' ---> U.typ_of ct)) + val cv = SMT_Utils.certify ctxt' + (Free (n, map SMT_Utils.typ_of cvs' ---> SMT_Utils.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') @@ -211,7 +209,7 @@ | t => (fn cx => if is_atomic t orelse can HOLogic.dest_number t then (ct, cx) else if with_theories andalso - I.is_builtin_theory_term (context_of cx) t + Z3_Interface.is_builtin_theory_term (context_of cx) t then abs_args abstr cvs ct cx else fresh_abstraction cvs ct cx)) in abstr [] end