src/HOL/Tools/SMT/smt_normalize.ML
changeset 41059 d2b1fc1b8e19
parent 40686 4725ed462387
child 41072 9f9bc1bdacef
     1.1 --- a/src/HOL/Tools/SMT/smt_normalize.ML	Mon Dec 06 16:54:22 2010 +0100
     1.2 +++ b/src/HOL/Tools/SMT/smt_normalize.ML	Tue Dec 07 14:53:12 2010 +0100
     1.3 @@ -23,12 +23,14 @@
     1.4      (int * thm) list * Proof.context
     1.5    val atomize_conv: Proof.context -> conv
     1.6    val eta_expand_conv: (Proof.context -> conv) -> Proof.context -> conv
     1.7 +  val setup: theory -> theory
     1.8  end
     1.9  
    1.10  structure SMT_Normalize: SMT_NORMALIZE =
    1.11  struct
    1.12  
    1.13  structure U = SMT_Utils
    1.14 +structure B = SMT_Builtin
    1.15  
    1.16  infix 2 ??
    1.17  fun (test ?? f) x = if test x then f x else x
    1.18 @@ -95,6 +97,9 @@
    1.19  fun rewrite_bool_cases ctxt =
    1.20    map (apsnd ((Term.exists_subterm is_bool_case o Thm.prop_of) ??
    1.21      Conv.fconv_rule (Conv.top_conv (K unfold_conv) ctxt)))
    1.22 +
    1.23 +val setup_bool_case = B.add_builtin_fun_ext'' @{const_name "bool.bool_case"}
    1.24 +
    1.25  end
    1.26  
    1.27  
    1.28 @@ -203,10 +208,20 @@
    1.29    val uses_nat_type = Term.exists_type (Term.exists_subtype (equal @{typ nat}))
    1.30    val uses_nat_int = Term.exists_subterm (member (op aconv)
    1.31      [@{const of_nat (int)}, @{const nat}])
    1.32 +
    1.33 +  val nat_ops = [
    1.34 +    @{const less (nat)}, @{const less_eq (nat)},
    1.35 +    @{const Suc}, @{const plus (nat)}, @{const minus (nat)},
    1.36 +    @{const times (nat)}, @{const div (nat)}, @{const mod (nat)}]
    1.37 +  val nat_ops' = @{const of_nat (int)} :: @{const nat} :: nat_ops
    1.38  in
    1.39  fun nat_as_int ctxt =
    1.40    map (apsnd ((uses_nat_type o Thm.prop_of) ?? Conv.fconv_rule (conv ctxt))) #>
    1.41    exists (uses_nat_int o Thm.prop_of o snd) ?? append nat_embedding
    1.42 +
    1.43 +val setup_nat_as_int =
    1.44 +  B.add_builtin_typ_ext (@{typ nat}, K true) #>
    1.45 +  fold (B.add_builtin_fun_ext' o Term.dest_Const) nat_ops'
    1.46  end
    1.47  
    1.48  
    1.49 @@ -263,7 +278,7 @@
    1.50      | _ =>
    1.51          (case Term.strip_comb (Thm.term_of ct) of
    1.52            (Const (c as (_, T)), ts) =>
    1.53 -            if SMT_Builtin.is_partially_builtin ctxt c
    1.54 +            if SMT_Builtin.is_builtin_fun ctxt c ts
    1.55              then eta_args_conv norm_conv
    1.56                (length (Term.binder_types T) - length ts)
    1.57              else args_conv o norm_conv
    1.58 @@ -294,7 +309,7 @@
    1.59      | _ =>
    1.60          (case Term.strip_comb t of
    1.61            (Const (c as (_, T)), ts) =>
    1.62 -            if SMT_Builtin.is_builtin ctxt c
    1.63 +            if SMT_Builtin.is_builtin_fun ctxt c ts
    1.64              then length (Term.binder_types T) = length ts andalso
    1.65                forall (is_normed ctxt) ts
    1.66              else forall (is_normed ctxt) ts
    1.67 @@ -302,6 +317,11 @@
    1.68  in
    1.69  fun norm_binder_conv ctxt =
    1.70    U.if_conv (is_normed ctxt) Conv.all_conv (norm_conv ctxt)
    1.71 +
    1.72 +val setup_unfolded_quants =
    1.73 +  fold B.add_builtin_fun_ext'' [@{const_name Ball}, @{const_name Bex},
    1.74 +    @{const_name Ex1}]
    1.75 +
    1.76  end
    1.77  
    1.78  fun norm_def ctxt thm =
    1.79 @@ -325,6 +345,10 @@
    1.80        Conv.rewr_conv @{thm atomize_all}
    1.81    | _ => Conv.all_conv) ct
    1.82  
    1.83 +val setup_atomize =
    1.84 +  fold B.add_builtin_fun_ext'' [@{const_name "==>"}, @{const_name "=="},
    1.85 +    @{const_name all}, @{const_name Trueprop}]
    1.86 +
    1.87  fun normalize_rule ctxt =
    1.88    Conv.fconv_rule (
    1.89      (* reduce lambda abstractions, except at known binders: *)
    1.90 @@ -554,4 +578,14 @@
    1.91      |-> (if with_datatypes then datatype_selectors else pair)
    1.92    end
    1.93  
    1.94 +
    1.95 +
    1.96 +(* setup *)
    1.97 +
    1.98 +val setup =
    1.99 +  setup_bool_case #>
   1.100 +  setup_nat_as_int #>
   1.101 +  setup_unfolded_quants #>
   1.102 +  setup_atomize
   1.103 +
   1.104  end