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.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)
```