src/HOL/Tools/SMT/smt_normalize.ML
changeset 50601 74da81de127f
parent 47207 9368aa814518
child 51575 907efc894051
     1.1 --- a/src/HOL/Tools/SMT/smt_normalize.ML	Thu Dec 20 09:49:00 2012 +0100
     1.2 +++ b/src/HOL/Tools/SMT/smt_normalize.ML	Fri Dec 21 11:05:42 2012 +0100
     1.3 @@ -346,6 +346,14 @@
     1.4  
     1.5  (* unfolding of definitions and theory-specific rewritings *)
     1.6  
     1.7 +fun expand_head_conv cv ct =
     1.8 +  (case Thm.term_of ct of
     1.9 +    _ $ _ =>
    1.10 +      Conv.fun_conv (expand_head_conv cv) then_conv
    1.11 +      Conv.try_conv (Thm.beta_conversion false)
    1.12 +  | _ => cv) ct
    1.13 +
    1.14 +
    1.15  (** rewrite bool case expressions as if expressions **)
    1.16  
    1.17  local
    1.18 @@ -355,7 +363,9 @@
    1.19    val thm = mk_meta_eq @{lemma
    1.20      "bool_case = (%x y P. if P then x else y)" by (rule ext)+ simp}
    1.21  
    1.22 -  fun unfold_conv _ = SMT_Utils.if_true_conv is_bool_case (Conv.rewr_conv thm)
    1.23 +  fun unfold_conv _ =
    1.24 +    SMT_Utils.if_true_conv (is_bool_case o Term.head_of)
    1.25 +      (expand_head_conv (Conv.rewr_conv thm))
    1.26  in
    1.27  
    1.28  fun rewrite_bool_case_conv ctxt =
    1.29 @@ -393,8 +403,8 @@
    1.30      | abs_min_max _ _ = NONE
    1.31  
    1.32    fun unfold_amm_conv ctxt ct =
    1.33 -    (case abs_min_max ctxt (Thm.term_of ct) of
    1.34 -      SOME thm => Conv.rewr_conv thm
    1.35 +    (case abs_min_max ctxt (Term.head_of (Thm.term_of ct)) of
    1.36 +      SOME thm => expand_head_conv (Conv.rewr_conv thm)
    1.37      | NONE => Conv.all_conv) ct
    1.38  in
    1.39  
    1.40 @@ -460,8 +470,11 @@
    1.41      "int (n * m) = int n * int m"
    1.42      "int (n div m) = int n div int m"
    1.43      "int (n mod m) = int n mod int m"
    1.44 +    by (auto simp add: int_mult zdiv_int zmod_int)}
    1.45 +
    1.46 +  val int_if = mk_meta_eq @{lemma
    1.47      "int (if P then n else m) = (if P then int n else int m)"
    1.48 -    by (auto simp add: int_mult zdiv_int zmod_int)}
    1.49 +    by simp}
    1.50  
    1.51    fun mk_number_eq ctxt i lhs =
    1.52      let
    1.53 @@ -471,12 +484,8 @@
    1.54        fun tac _ = Simplifier.simp_tac (Simplifier.context ctxt ss) 1       
    1.55      in Goal.norm_result (Goal.prove_internal [] eq tac) end
    1.56  
    1.57 -  fun expand_head_conv cv ct =
    1.58 -    (case Thm.term_of ct of
    1.59 -      _ $ _ =>
    1.60 -        Conv.fun_conv (expand_head_conv cv) then_conv
    1.61 -        Thm.beta_conversion false
    1.62 -    | _ => cv) ct
    1.63 +  fun ite_conv cv1 cv2 =
    1.64 +    Conv.combination_conv (Conv.combination_conv (Conv.arg_conv cv1) cv2) cv2
    1.65  
    1.66    fun int_conv ctxt ct =
    1.67      (case Thm.term_of ct of
    1.68 @@ -484,7 +493,9 @@
    1.69          Conv.rewr_conv (mk_number_eq ctxt (snd (HOLogic.dest_number n)) ct)
    1.70      | @{const of_nat (int)} $ _ =>
    1.71          (Conv.rewrs_conv ints then_conv Conv.sub_conv ints_conv ctxt) else_conv
    1.72 -        Conv.sub_conv (Conv.top_sweep_conv nat_conv) ctxt        
    1.73 +        (Conv.rewr_conv int_if then_conv
    1.74 +          ite_conv (nat_conv ctxt) (int_conv ctxt)) else_conv
    1.75 +        Conv.sub_conv (Conv.top_sweep_conv nat_conv) ctxt
    1.76      | _ => Conv.no_conv) ct
    1.77  
    1.78    and ints_conv ctxt = Conv.top_sweep_conv int_conv ctxt