src/HOL/Tools/SMT/smt_normalize.ML
changeset 37786 4eb98849c5c0
parent 37153 8feed34275ce
child 38864 4abe644fcea5
     1.1 --- a/src/HOL/Tools/SMT/smt_normalize.ML	Mon Jul 12 22:35:41 2010 +0200
     1.2 +++ b/src/HOL/Tools/SMT/smt_normalize.ML	Tue Jul 13 02:29:05 2010 +0200
     1.3 @@ -41,10 +41,10 @@
     1.4          length (HOLogic.dest_list t) <= 2
     1.5      | is_trivial_distinct _ = false
     1.6  
     1.7 -  val thms = @{lemma
     1.8 -    "distinct [] == True"
     1.9 -    "distinct [x] == True"
    1.10 -    "distinct [x, y] == (x ~= y)"
    1.11 +  val thms = map mk_meta_eq @{lemma
    1.12 +    "distinct [] = True"
    1.13 +    "distinct [x] = True"
    1.14 +    "distinct [x, y] = (x ~= y)"
    1.15      by simp_all}
    1.16    fun distinct_conv _ =
    1.17      if_true_conv is_trivial_distinct (Conv.rewrs_conv thms)
    1.18 @@ -63,10 +63,10 @@
    1.19        Const (@{const_name "bool.bool_case"}, _) $ _ $ _ $ _ => true
    1.20      | _ => false)
    1.21  
    1.22 -  val thms = @{lemma
    1.23 -    "(case P of True => x | False => y) == (if P then x else y)"
    1.24 -    "(case P of False => y | True => x) == (if P then x else y)"
    1.25 -    by (rule eq_reflection, simp)+}
    1.26 +  val thms = map mk_meta_eq @{lemma
    1.27 +    "(case P of True => x | False => y) = (if P then x else y)"
    1.28 +    "(case P of False => y | True => x) = (if P then x else y)"
    1.29 +    by simp_all}
    1.30    val unfold_conv = if_true_conv is_bool_case (Conv.rewrs_conv thms)
    1.31  in
    1.32  fun rewrite_bool_cases ctxt =
    1.33 @@ -201,8 +201,8 @@
    1.34      (Conv.arg_conv (norm_conv ctxt)) (eta_conv norm_conv ctxt)
    1.35    and unfold_conv thm ctxt = Conv.rewr_conv thm then_conv keep_conv ctxt
    1.36    and unfold_ex1_conv ctxt = unfold_conv @{thm Ex1_def} ctxt
    1.37 -  and unfold_ball_conv ctxt = unfold_conv @{thm Ball_def} ctxt
    1.38 -  and unfold_bex_conv ctxt = unfold_conv @{thm Bex_def} ctxt
    1.39 +  and unfold_ball_conv ctxt = unfold_conv (mk_meta_eq @{thm Ball_def}) ctxt
    1.40 +  and unfold_bex_conv ctxt = unfold_conv (mk_meta_eq @{thm Bex_def}) ctxt
    1.41    and norm_conv ctxt ct =
    1.42      (case Thm.term_of ct of
    1.43        Const (@{const_name All}, _) $ Abs _ => keep_conv