src/HOL/Tools/SMT2/smt2_normalize.ML
changeset 56981 3ef45ce002b5
parent 56245 84fc7dfa3cd4
child 57165 7b1bf424ec5f
     1.1 --- a/src/HOL/Tools/SMT2/smt2_normalize.ML	Fri May 16 17:11:56 2014 +0200
     1.2 +++ b/src/HOL/Tools/SMT2/smt2_normalize.ML	Fri May 16 19:13:50 2014 +0200
     1.3 @@ -8,6 +8,11 @@
     1.4  sig
     1.5    val drop_fact_warning: Proof.context -> thm -> unit
     1.6    val atomize_conv: Proof.context -> conv
     1.7 +
     1.8 +  val special_quant_table: (string * thm) list
     1.9 +  val case_bool_entry: string * thm
    1.10 +  val abs_min_max_table: (string * thm) list
    1.11 +
    1.12    type extra_norm = Proof.context -> thm list * thm list -> thm list * thm list
    1.13    val add_extra_norm: SMT2_Util.class * extra_norm -> Context.generic -> Context.generic
    1.14    val normalize: Proof.context -> (int option * thm) list -> (int * thm) list
    1.15 @@ -71,13 +76,13 @@
    1.16  
    1.17  (** unfold special quantifiers **)
    1.18  
    1.19 +val special_quant_table = [
    1.20 +  (@{const_name Ex1}, @{thm Ex1_def_raw}),
    1.21 +  (@{const_name Ball}, @{thm Ball_def_raw}),
    1.22 +  (@{const_name Bex}, @{thm Bex_def_raw})]
    1.23 +
    1.24  local
    1.25 -  val special_quants = [
    1.26 -    (@{const_name Ex1}, @{thm Ex1_def_raw}),
    1.27 -    (@{const_name Ball}, @{thm Ball_def_raw}),
    1.28 -    (@{const_name Bex}, @{thm Bex_def_raw})]
    1.29 -  
    1.30 -  fun special_quant (Const (n, _)) = AList.lookup (op =) special_quants n
    1.31 +  fun special_quant (Const (n, _)) = AList.lookup (op =) special_quant_table n
    1.32      | special_quant _ = NONE
    1.33  
    1.34    fun special_quant_conv _ ct =
    1.35 @@ -89,7 +94,7 @@
    1.36  fun unfold_special_quants_conv ctxt =
    1.37    SMT2_Util.if_exists_conv (is_some o special_quant) (Conv.top_conv special_quant_conv ctxt)
    1.38  
    1.39 -val setup_unfolded_quants = fold (SMT2_Builtin.add_builtin_fun_ext'' o fst) special_quants
    1.40 +val setup_unfolded_quants = fold (SMT2_Builtin.add_builtin_fun_ext'' o fst) special_quant_table
    1.41  
    1.42  end
    1.43  
    1.44 @@ -326,6 +331,8 @@
    1.45  
    1.46  (** rewrite bool case expressions as if expressions **)
    1.47  
    1.48 +val case_bool_entry = (@{const_name "bool.case_bool"}, @{thm case_bool_if})
    1.49 +
    1.50  local
    1.51    fun is_case_bool (Const (@{const_name "bool.case_bool"}, _)) = true
    1.52      | is_case_bool _ = false
    1.53 @@ -345,14 +352,14 @@
    1.54  
    1.55  (** unfold abs, min and max **)
    1.56  
    1.57 +val abs_min_max_table = [
    1.58 +  (@{const_name min}, @{thm min_def_raw}),
    1.59 +  (@{const_name max}, @{thm max_def_raw}),
    1.60 +  (@{const_name abs}, @{thm abs_if_raw})]
    1.61 +
    1.62  local
    1.63 -  val defs = [
    1.64 -    (@{const_name min}, @{thm min_def_raw}),
    1.65 -    (@{const_name max}, @{thm max_def_raw}),
    1.66 -    (@{const_name abs}, @{thm abs_if_raw})]
    1.67 -
    1.68    fun abs_min_max ctxt (Const (n, Type (@{type_name fun}, [T, _]))) =
    1.69 -        (case AList.lookup (op =) defs n of
    1.70 +        (case AList.lookup (op =) abs_min_max_table n of
    1.71            NONE => NONE
    1.72          | SOME thm => if SMT2_Builtin.is_builtin_typ_ext ctxt T then SOME thm else NONE)
    1.73      | abs_min_max _ _ = NONE
    1.74 @@ -366,7 +373,7 @@
    1.75  fun unfold_abs_min_max_conv ctxt =
    1.76    SMT2_Util.if_exists_conv (is_some o abs_min_max ctxt) (Conv.top_conv unfold_amm_conv ctxt)
    1.77    
    1.78 -val setup_abs_min_max = fold (SMT2_Builtin.add_builtin_fun_ext'' o fst) defs
    1.79 +val setup_abs_min_max = fold (SMT2_Builtin.add_builtin_fun_ext'' o fst) abs_min_max_table
    1.80  
    1.81  end
    1.82