src/HOL/Tools/SMT/smt_normalize.ML
changeset 40663 e080c9e68752
parent 40579 98ebd2300823
child 40681 872b08416fb4
     1.1 --- a/src/HOL/Tools/SMT/smt_normalize.ML	Mon Nov 22 15:45:42 2010 +0100
     1.2 +++ b/src/HOL/Tools/SMT/smt_normalize.ML	Mon Nov 22 15:45:43 2010 +0100
     1.3 @@ -28,12 +28,11 @@
     1.4  structure SMT_Normalize: SMT_NORMALIZE =
     1.5  struct
     1.6  
     1.7 +structure U = SMT_Utils
     1.8 +
     1.9  infix 2 ??
    1.10  fun (test ?? f) x = if test x then f x else x
    1.11  
    1.12 -fun if_conv c cv1 cv2 ct = (if c (Thm.term_of ct) then cv1 else cv2) ct
    1.13 -fun if_true_conv c cv = if_conv c cv Conv.all_conv
    1.14 -
    1.15  
    1.16  
    1.17  (* simplification of trivial distincts (distinct should have at least
    1.18 @@ -53,7 +52,7 @@
    1.19      "SMT.distinct [x, y] = (x ~= y)"
    1.20      by (simp_all add: distinct_def)}
    1.21    fun distinct_conv _ =
    1.22 -    if_true_conv is_trivial_distinct (Conv.rewrs_conv thms)
    1.23 +    U.if_true_conv is_trivial_distinct (Conv.rewrs_conv thms)
    1.24  in
    1.25  fun trivial_distinct ctxt =
    1.26    map (apsnd ((Term.exists_subterm is_trivial_distinct o Thm.prop_of) ??
    1.27 @@ -71,7 +70,7 @@
    1.28  
    1.29    val thm = mk_meta_eq @{lemma
    1.30      "(case P of True => x | False => y) = (if P then x else y)" by simp}
    1.31 -  val unfold_conv = if_true_conv is_bool_case (Conv.rewr_conv thm)
    1.32 +  val unfold_conv = U.if_true_conv is_bool_case (Conv.rewr_conv thm)
    1.33  in
    1.34  fun rewrite_bool_cases ctxt =
    1.35    map (apsnd ((Term.exists_subterm is_bool_case o Thm.prop_of) ??
    1.36 @@ -105,7 +104,7 @@
    1.37        "Int.Bit1 (- k) = - Int.Bit1 (Int.pred k)"
    1.38        by simp_all (simp add: pred_def)}
    1.39  
    1.40 -  fun pos_conv ctxt = if_conv (is_strange_number ctxt)
    1.41 +  fun pos_conv ctxt = U.if_conv (is_strange_number ctxt)
    1.42      (Simplifier.rewrite (Simplifier.context ctxt pos_numeral_ss))
    1.43      Conv.no_conv
    1.44  in
    1.45 @@ -282,7 +281,7 @@
    1.46          | (_, ts) => forall (is_normed ctxt) ts))
    1.47  in
    1.48  fun norm_binder_conv ctxt =
    1.49 -  if_conv (is_normed ctxt) Conv.all_conv (norm_conv ctxt)
    1.50 +  U.if_conv (is_normed ctxt) Conv.all_conv (norm_conv ctxt)
    1.51  end
    1.52  
    1.53  fun norm_def ctxt thm =
    1.54 @@ -321,13 +320,6 @@
    1.55  (* lift lambda terms into additional rules *)
    1.56  
    1.57  local
    1.58 -  val meta_eq = @{cpat "op =="}
    1.59 -  val meta_eqT = hd (Thm.dest_ctyp (Thm.ctyp_of_term meta_eq))
    1.60 -  fun inst_meta cT = Thm.instantiate_cterm ([(meta_eqT, cT)], []) meta_eq
    1.61 -  fun mk_meta_eq ct cu = Thm.mk_binop (inst_meta (Thm.ctyp_of_term ct)) ct cu
    1.62 -
    1.63 -  fun cert ctxt = Thm.cterm_of (ProofContext.theory_of ctxt)
    1.64 -
    1.65    fun used_vars cvs ct =
    1.66      let
    1.67        val lookup = AList.lookup (op aconv) (map (` Thm.term_of) cvs)
    1.68 @@ -350,7 +342,7 @@
    1.69            let
    1.70              val {T, ...} = Thm.rep_cterm ct' and n = Name.uu
    1.71              val (n', ctxt') = yield_singleton Variable.variant_fixes n ctxt
    1.72 -            val cu = mk_meta_eq (cert ctxt (Free (n', T))) ct'
    1.73 +            val cu = U.mk_cequals (U.certify ctxt (Free (n', T))) ct'
    1.74              val (eq, ctxt'') = yield_singleton Assumption.add_assumes cu ctxt'
    1.75              val defs' = Termtab.update (Thm.term_of ct', eq) defs
    1.76            in (apply_def cvs' eq, (ctxt'', defs')) end)