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
authorboehmes
Wed Dec 15 16:29:56 2010 +0100 (2010-12-15)
changeset 41172a17c2d669c40
parent 41165 ceb81a08534e
child 41173 7c6178d45cc8
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
src/HOL/Tools/SMT/smt_translate.ML
src/HOL/Tools/SMT/smt_utils.ML
src/HOL/Tools/SMT/z3_proof_literals.ML
src/HOL/Tools/SMT/z3_proof_reconstruction.ML
src/HOL/Tools/SMT/z3_proof_tools.ML
     1.1 --- a/src/HOL/Tools/SMT/smt_translate.ML	Wed Dec 15 14:29:04 2010 +0100
     1.2 +++ b/src/HOL/Tools/SMT/smt_translate.ML	Wed Dec 15 16:29:56 2010 +0100
     1.3 @@ -378,9 +378,7 @@
     1.4        | replace @{const True} = term_true
     1.5        | replace @{const False} = term_false
     1.6        | replace t = t
     1.7 -  in
     1.8 -    Term.map_aterms replace (HOLogic.dest_Trueprop (Thm.prop_of term_bool))
     1.9 -  end
    1.10 +  in Term.map_aterms replace (U.prop_of term_bool) end
    1.11  
    1.12  val fol_rules = [
    1.13    Let_def,
    1.14 @@ -609,8 +607,7 @@
    1.15  
    1.16      val (builtins, ts1) =
    1.17        ithms
    1.18 -      |> map (HOLogic.dest_Trueprop o Thm.prop_of o snd)
    1.19 -      |> map (Envir.eta_contract o Envir.beta_norm)
    1.20 +      |> map (Envir.beta_eta_contract o U.prop_of o snd)
    1.21        |> mark_builtins ctxt
    1.22  
    1.23      val ((dtyps, tr_context, ctxt1), ts2) =
     2.1 --- a/src/HOL/Tools/SMT/smt_utils.ML	Wed Dec 15 14:29:04 2010 +0100
     2.2 +++ b/src/HOL/Tools/SMT/smt_utils.ML	Wed Dec 15 16:29:56 2010 +0100
     2.3 @@ -47,6 +47,8 @@
     2.4    val mk_cprop: cterm -> cterm
     2.5    val dest_cprop: cterm -> cterm
     2.6    val mk_cequals: cterm -> cterm -> cterm
     2.7 +  val term_of: cterm -> term
     2.8 +  val prop_of: thm -> term
     2.9  
    2.10    (*conversions*)
    2.11    val if_conv: (term -> bool) -> conv -> conv -> conv
    2.12 @@ -177,6 +179,10 @@
    2.13  val equals = mk_const_pat @{theory} @{const_name "=="} destT1
    2.14  fun mk_cequals ct cu = Thm.mk_binop (instT' ct equals) ct cu
    2.15  
    2.16 +val dest_prop = (fn @{const Trueprop} $ t => t | t => t)
    2.17 +fun term_of ct = dest_prop (Thm.term_of ct)
    2.18 +fun prop_of thm = dest_prop (Thm.prop_of thm)
    2.19 +
    2.20  
    2.21  (* conversions *)
    2.22  
     3.1 --- a/src/HOL/Tools/SMT/z3_proof_literals.ML	Wed Dec 15 14:29:04 2010 +0100
     3.2 +++ b/src/HOL/Tools/SMT/z3_proof_literals.ML	Wed Dec 15 16:29:56 2010 +0100
     3.3 @@ -33,6 +33,7 @@
     3.4  structure Z3_Proof_Literals: Z3_PROOF_LITERALS =
     3.5  struct
     3.6  
     3.7 +structure U = SMT_Utils
     3.8  structure T = Z3_Proof_Tools
     3.9  
    3.10  
    3.11 @@ -41,10 +42,10 @@
    3.12  
    3.13  type littab = thm Termtab.table
    3.14  
    3.15 -fun make_littab thms = fold (Termtab.update o `T.prop_of) thms Termtab.empty
    3.16 +fun make_littab thms = fold (Termtab.update o `U.prop_of) thms Termtab.empty
    3.17  
    3.18 -fun insert_lit thm = Termtab.update (`T.prop_of thm)
    3.19 -fun delete_lit thm = Termtab.delete (T.prop_of thm)
    3.20 +fun insert_lit thm = Termtab.update (`U.prop_of thm)
    3.21 +fun delete_lit thm = Termtab.delete (U.prop_of thm)
    3.22  fun lookup_lit lits = Termtab.lookup lits
    3.23  fun get_first_lit f =
    3.24    Termtab.get_first (fn (t, thm) => if f t then SOME thm else NONE)
    3.25 @@ -161,9 +162,9 @@
    3.26      val tab = fold (Termtab.update o rpair ()) stop_lits Termtab.empty
    3.27  
    3.28      fun explode1 thm =
    3.29 -      if Termtab.defined tab (T.prop_of thm) then cons thm
    3.30 +      if Termtab.defined tab (U.prop_of thm) then cons thm
    3.31        else
    3.32 -        (case dest_rules (T.prop_of thm) of
    3.33 +        (case dest_rules (U.prop_of thm) of
    3.34            SOME (rule1, rule2) =>
    3.35              explode2 rule1 thm #>
    3.36              explode2 rule2 thm #>
    3.37 @@ -171,12 +172,12 @@
    3.38          | NONE => cons thm)
    3.39  
    3.40      and explode2 dest_rule thm =
    3.41 -      if full orelse exists_lit is_conj (Termtab.defined tab) (T.prop_of thm)
    3.42 +      if full orelse exists_lit is_conj (Termtab.defined tab) (U.prop_of thm)
    3.43        then explode1 (T.compose dest_rule thm)
    3.44        else cons (T.compose dest_rule thm)
    3.45  
    3.46      fun explode0 thm =
    3.47 -      if not is_conj andalso is_dneg (T.prop_of thm)
    3.48 +      if not is_conj andalso is_dneg (U.prop_of thm)
    3.49        then [T.compose dneg_rule thm]
    3.50        else explode1 thm []
    3.51  
    3.52 @@ -284,7 +285,7 @@
    3.53    val contra_rule = @{lemma "P ==> ~P ==> False" by (rule notE)}
    3.54    fun contra_left conj thm =
    3.55      let
    3.56 -      val rules = explode_term conj (T.prop_of thm)
    3.57 +      val rules = explode_term conj (U.prop_of thm)
    3.58        fun contra_lits (t, rs) =
    3.59          (case t of
    3.60            @{const Not} $ u => Termtab.lookup rules u |> Option.map (pair rs)
     4.1 --- a/src/HOL/Tools/SMT/z3_proof_reconstruction.ML	Wed Dec 15 14:29:04 2010 +0100
     4.2 +++ b/src/HOL/Tools/SMT/z3_proof_reconstruction.ML	Wed Dec 15 16:29:56 2010 +0100
     4.3 @@ -15,6 +15,7 @@
     4.4  structure Z3_Proof_Reconstruction: Z3_PROOF_RECONSTRUCTION =
     4.5  struct
     4.6  
     4.7 +structure U = SMT_Utils
     4.8  structure P = Z3_Proof_Parser
     4.9  structure T = Z3_Proof_Tools
    4.10  structure L = Z3_Proof_Literals
    4.11 @@ -233,9 +234,9 @@
    4.12    fun lit_elim conj (p, idx) ct ptab =
    4.13      let val lits = literals_of p
    4.14      in
    4.15 -      (case L.lookup_lit lits (T.term_of ct) of
    4.16 +      (case L.lookup_lit lits (U.term_of ct) of
    4.17          SOME lit => (Thm lit, ptab)
    4.18 -      | NONE => apfst Thm (derive conj (T.term_of ct) lits idx ptab))
    4.19 +      | NONE => apfst Thm (derive conj (U.term_of ct) lits idx ptab))
    4.20      end
    4.21  in
    4.22  val and_elim = lit_elim true
    4.23 @@ -266,7 +267,7 @@
    4.24    val explode_disj = L.explode false true false
    4.25    val join_disj = L.join false
    4.26    fun unit thm thms th =
    4.27 -    let val t = @{const Not} $ T.prop_of thm and ts = map T.prop_of thms
    4.28 +    let val t = @{const Not} $ U.prop_of thm and ts = map U.prop_of thms
    4.29      in join_disj (L.make_littab (thms @ explode_disj ts th)) t end
    4.30  
    4.31    fun dest_arg2 ct = Thm.dest_arg (Thm.dest_arg ct)
    4.32 @@ -403,7 +404,7 @@
    4.33        named ctxt' "simp+fast" (T.by_tac simp_fast_tac))]
    4.34  in
    4.35  fun nnf ctxt vars ps ct =
    4.36 -  (case T.term_of ct of
    4.37 +  (case U.term_of ct of
    4.38      _ $ (l as Const _ $ Abs _) $ (r as Const _ $ Abs _) =>
    4.39        if l aconv r
    4.40        then MetaEq (Thm.reflexive (Thm.dest_arg (Thm.dest_arg ct)))
     5.1 --- a/src/HOL/Tools/SMT/z3_proof_tools.ML	Wed Dec 15 14:29:04 2010 +0100
     5.2 +++ b/src/HOL/Tools/SMT/z3_proof_tools.ML	Wed Dec 15 16:29:56 2010 +0100
     5.3 @@ -6,9 +6,7 @@
     5.4  
     5.5  signature Z3_PROOF_TOOLS =
     5.6  sig
     5.7 -  (*accessing and modifying terms*)
     5.8 -  val term_of: cterm -> term
     5.9 -  val prop_of: thm -> term
    5.10 +  (*modifying terms*)
    5.11    val as_meta_eq: cterm -> cterm
    5.12  
    5.13    (*theorem nets*)
    5.14 @@ -51,12 +49,7 @@
    5.15  
    5.16  
    5.17  
    5.18 -(* accessing terms *)
    5.19 -
    5.20 -val dest_prop = (fn @{const Trueprop} $ t => t | t => t)
    5.21 -
    5.22 -fun term_of ct = dest_prop (Thm.term_of ct)
    5.23 -fun prop_of thm = dest_prop (Thm.prop_of thm)
    5.24 +(* modifying terms *)
    5.25  
    5.26  fun as_meta_eq ct = uncurry U.mk_cequals (Thm.dest_binop (U.dest_cprop ct))
    5.27