# HG changeset patch # User boehmes # Date 1292426996 -3600 # Node ID a17c2d669c4059f16fdc5a16ac63c6e33690b953 # Parent ceb81a08534e1f1afd256870c15ec3ae42d2fe7c the functions term_of and prop_of are also needed in earlier stages, not only for Z3 proof reconstruction, so they really belong in SMT_Utils diff -r ceb81a08534e -r a17c2d669c40 src/HOL/Tools/SMT/smt_translate.ML --- a/src/HOL/Tools/SMT/smt_translate.ML Wed Dec 15 14:29:04 2010 +0100 +++ b/src/HOL/Tools/SMT/smt_translate.ML Wed Dec 15 16:29:56 2010 +0100 @@ -378,9 +378,7 @@ | replace @{const True} = term_true | replace @{const False} = term_false | replace t = t - in - Term.map_aterms replace (HOLogic.dest_Trueprop (Thm.prop_of term_bool)) - end + in Term.map_aterms replace (U.prop_of term_bool) end val fol_rules = [ Let_def, @@ -609,8 +607,7 @@ val (builtins, ts1) = ithms - |> map (HOLogic.dest_Trueprop o Thm.prop_of o snd) - |> map (Envir.eta_contract o Envir.beta_norm) + |> map (Envir.beta_eta_contract o U.prop_of o snd) |> mark_builtins ctxt val ((dtyps, tr_context, ctxt1), ts2) = diff -r ceb81a08534e -r a17c2d669c40 src/HOL/Tools/SMT/smt_utils.ML --- a/src/HOL/Tools/SMT/smt_utils.ML Wed Dec 15 14:29:04 2010 +0100 +++ b/src/HOL/Tools/SMT/smt_utils.ML Wed Dec 15 16:29:56 2010 +0100 @@ -47,6 +47,8 @@ val mk_cprop: cterm -> cterm val dest_cprop: cterm -> cterm val mk_cequals: cterm -> cterm -> cterm + val term_of: cterm -> term + val prop_of: thm -> term (*conversions*) val if_conv: (term -> bool) -> conv -> conv -> conv @@ -177,6 +179,10 @@ val equals = mk_const_pat @{theory} @{const_name "=="} destT1 fun mk_cequals ct cu = Thm.mk_binop (instT' ct equals) ct cu +val dest_prop = (fn @{const Trueprop} $ t => t | t => t) +fun term_of ct = dest_prop (Thm.term_of ct) +fun prop_of thm = dest_prop (Thm.prop_of thm) + (* conversions *) diff -r ceb81a08534e -r a17c2d669c40 src/HOL/Tools/SMT/z3_proof_literals.ML --- a/src/HOL/Tools/SMT/z3_proof_literals.ML Wed Dec 15 14:29:04 2010 +0100 +++ b/src/HOL/Tools/SMT/z3_proof_literals.ML Wed Dec 15 16:29:56 2010 +0100 @@ -33,6 +33,7 @@ structure Z3_Proof_Literals: Z3_PROOF_LITERALS = struct +structure U = SMT_Utils structure T = Z3_Proof_Tools @@ -41,10 +42,10 @@ type littab = thm Termtab.table -fun make_littab thms = fold (Termtab.update o `T.prop_of) thms Termtab.empty +fun make_littab thms = fold (Termtab.update o `U.prop_of) thms Termtab.empty -fun insert_lit thm = Termtab.update (`T.prop_of thm) -fun delete_lit thm = Termtab.delete (T.prop_of thm) +fun insert_lit thm = Termtab.update (`U.prop_of thm) +fun delete_lit thm = Termtab.delete (U.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) @@ -161,9 +162,9 @@ val tab = fold (Termtab.update o rpair ()) stop_lits Termtab.empty fun explode1 thm = - if Termtab.defined tab (T.prop_of thm) then cons thm + if Termtab.defined tab (U.prop_of thm) then cons thm else - (case dest_rules (T.prop_of thm) of + (case dest_rules (U.prop_of thm) of SOME (rule1, rule2) => explode2 rule1 thm #> explode2 rule2 thm #> @@ -171,12 +172,12 @@ | NONE => cons thm) and explode2 dest_rule thm = - if full orelse exists_lit is_conj (Termtab.defined tab) (T.prop_of 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) fun explode0 thm = - if not is_conj andalso is_dneg (T.prop_of thm) + if not is_conj andalso is_dneg (U.prop_of thm) then [T.compose dneg_rule thm] else explode1 thm [] @@ -284,7 +285,7 @@ val contra_rule = @{lemma "P ==> ~P ==> False" by (rule notE)} fun contra_left conj thm = let - val rules = explode_term conj (T.prop_of thm) + val rules = explode_term conj (U.prop_of thm) fun contra_lits (t, rs) = (case t of @{const Not} $ u => Termtab.lookup rules u |> Option.map (pair rs) diff -r ceb81a08534e -r a17c2d669c40 src/HOL/Tools/SMT/z3_proof_reconstruction.ML --- a/src/HOL/Tools/SMT/z3_proof_reconstruction.ML Wed Dec 15 14:29:04 2010 +0100 +++ b/src/HOL/Tools/SMT/z3_proof_reconstruction.ML Wed Dec 15 16:29:56 2010 +0100 @@ -15,6 +15,7 @@ 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 @@ -233,9 +234,9 @@ fun lit_elim conj (p, idx) ct ptab = let val lits = literals_of p in - (case L.lookup_lit lits (T.term_of ct) of + (case L.lookup_lit lits (U.term_of ct) of SOME lit => (Thm lit, ptab) - | NONE => apfst Thm (derive conj (T.term_of ct) lits idx ptab)) + | NONE => apfst Thm (derive conj (U.term_of ct) lits idx ptab)) end in val and_elim = lit_elim true @@ -266,7 +267,7 @@ val explode_disj = L.explode false true false val join_disj = L.join false fun unit thm thms th = - let val t = @{const Not} $ T.prop_of thm and ts = map T.prop_of thms + 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 fun dest_arg2 ct = Thm.dest_arg (Thm.dest_arg ct) @@ -403,7 +404,7 @@ named ctxt' "simp+fast" (T.by_tac simp_fast_tac))] in fun nnf ctxt vars ps ct = - (case T.term_of ct of + (case U.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))) diff -r ceb81a08534e -r a17c2d669c40 src/HOL/Tools/SMT/z3_proof_tools.ML --- a/src/HOL/Tools/SMT/z3_proof_tools.ML Wed Dec 15 14:29:04 2010 +0100 +++ b/src/HOL/Tools/SMT/z3_proof_tools.ML Wed Dec 15 16:29:56 2010 +0100 @@ -6,9 +6,7 @@ signature Z3_PROOF_TOOLS = sig - (*accessing and modifying terms*) - val term_of: cterm -> term - val prop_of: thm -> term + (*modifying terms*) val as_meta_eq: cterm -> cterm (*theorem nets*) @@ -51,12 +49,7 @@ -(* accessing terms *) - -val dest_prop = (fn @{const Trueprop} $ t => t | t => t) - -fun term_of ct = dest_prop (Thm.term_of ct) -fun prop_of thm = dest_prop (Thm.prop_of thm) +(* modifying terms *) fun as_meta_eq ct = uncurry U.mk_cequals (Thm.dest_binop (U.dest_cprop ct))