src/HOL/Tools/SMT/smt_normalize.ML
changeset 41328 6792a5c92a58
parent 41327 49feace87649
child 42183 173b0f488428
     1.1 --- a/src/HOL/Tools/SMT/smt_normalize.ML	Mon Dec 20 21:04:45 2010 +0100
     1.2 +++ b/src/HOL/Tools/SMT/smt_normalize.ML	Mon Dec 20 22:02:57 2010 +0100
     1.3 @@ -18,16 +18,14 @@
     1.4  structure SMT_Normalize: SMT_NORMALIZE =
     1.5  struct
     1.6  
     1.7 -structure U = SMT_Utils
     1.8 -structure B = SMT_Builtin
     1.9 -
    1.10  
    1.11  (* general theorem normalizations *)
    1.12  
    1.13  (** instantiate elimination rules **)
    1.14   
    1.15  local
    1.16 -  val (cpfalse, cfalse) = `U.mk_cprop (Thm.cterm_of @{theory} @{const False})
    1.17 +  val (cpfalse, cfalse) =
    1.18 +    `SMT_Utils.mk_cprop (Thm.cterm_of @{theory} @{const False})
    1.19  
    1.20    fun inst f ct thm =
    1.21      let val cv = f (Drule.strip_imp_concl (Thm.cprop_of thm))
    1.22 @@ -70,8 +68,8 @@
    1.23    | _ => Conv.all_conv) ct
    1.24  
    1.25  val setup_atomize =
    1.26 -  fold B.add_builtin_fun_ext'' [@{const_name "==>"}, @{const_name "=="},
    1.27 -    @{const_name all}, @{const_name Trueprop}]
    1.28 +  fold SMT_Builtin.add_builtin_fun_ext'' [@{const_name "==>"},
    1.29 +    @{const_name "=="}, @{const_name all}, @{const_name Trueprop}]
    1.30  
    1.31  
    1.32  (** unfold special quantifiers **)
    1.33 @@ -100,10 +98,11 @@
    1.34  in
    1.35  
    1.36  fun unfold_special_quants_conv ctxt =
    1.37 -  U.if_exists_conv (is_some o special_quant)
    1.38 +  SMT_Utils.if_exists_conv (is_some o special_quant)
    1.39      (Conv.top_conv special_quant_conv ctxt)
    1.40  
    1.41 -val setup_unfolded_quants = fold (B.add_builtin_fun_ext'' o fst) special_quants
    1.42 +val setup_unfolded_quants =
    1.43 +  fold (SMT_Builtin.add_builtin_fun_ext'' o fst) special_quants
    1.44  
    1.45  end
    1.46  
    1.47 @@ -141,7 +140,8 @@
    1.48        "must have the same kind: " ^ Syntax.string_of_term ctxt t)
    1.49  
    1.50    fun check_trigger_conv ctxt ct =
    1.51 -    if proper_quant false proper_trigger (U.term_of ct) then Conv.all_conv ct
    1.52 +    if proper_quant false proper_trigger (SMT_Utils.term_of ct) then
    1.53 +      Conv.all_conv ct
    1.54      else check_trigger_error ctxt (Thm.term_of ct)
    1.55  
    1.56  
    1.57 @@ -169,7 +169,7 @@
    1.58    fun is_simp_lhs ctxt t =
    1.59      (case Term.strip_comb t of
    1.60        (Const c, ts as _ :: _) =>
    1.61 -        not (B.is_builtin_fun_ext ctxt c ts) andalso
    1.62 +        not (SMT_Builtin.is_builtin_fun_ext ctxt c ts) andalso
    1.63          forall (is_constr_pat (ProofContext.theory_of ctxt)) ts
    1.64      | _ => false)
    1.65  
    1.66 @@ -194,8 +194,9 @@
    1.67              Pattern.matches thy (t', u) andalso not (t aconv u))
    1.68          in not (Term.exists_subterm some_match u) end
    1.69  
    1.70 -  val pat = U.mk_const_pat @{theory} @{const_name SMT.pat} U.destT1
    1.71 -  fun mk_pat ct = Thm.capply (U.instT' ct pat) ct
    1.72 +  val pat =
    1.73 +    SMT_Utils.mk_const_pat @{theory} @{const_name SMT.pat} SMT_Utils.destT1
    1.74 +  fun mk_pat ct = Thm.capply (SMT_Utils.instT' ct pat) ct
    1.75  
    1.76    fun mk_clist T = pairself (Thm.cterm_of @{theory})
    1.77      (HOLogic.cons_const T, HOLogic.nil_const T)
    1.78 @@ -231,20 +232,24 @@
    1.79      | has_trigger _ = false
    1.80  
    1.81    fun try_trigger_conv cv ct =
    1.82 -    if U.under_quant has_trigger (U.term_of ct) then Conv.all_conv ct
    1.83 +    if SMT_Utils.under_quant has_trigger (SMT_Utils.term_of ct) then
    1.84 +      Conv.all_conv ct
    1.85      else Conv.try_conv cv ct
    1.86  
    1.87    fun infer_trigger_conv ctxt =
    1.88      if Config.get ctxt SMT_Config.infer_triggers then
    1.89 -      try_trigger_conv (U.under_quant_conv (infer_trigger_eq_conv ctxt) ctxt)
    1.90 +      try_trigger_conv
    1.91 +        (SMT_Utils.under_quant_conv (infer_trigger_eq_conv ctxt) ctxt)
    1.92      else Conv.all_conv
    1.93  in
    1.94  
    1.95  fun trigger_conv ctxt =
    1.96 -  U.prop_conv (check_trigger_conv ctxt then_conv infer_trigger_conv ctxt)
    1.97 +  SMT_Utils.prop_conv
    1.98 +    (check_trigger_conv ctxt then_conv infer_trigger_conv ctxt)
    1.99  
   1.100 -val setup_trigger = fold B.add_builtin_fun_ext''
   1.101 -  [@{const_name SMT.pat}, @{const_name SMT.nopat}, @{const_name SMT.trigger}]
   1.102 +val setup_trigger =
   1.103 +  fold SMT_Builtin.add_builtin_fun_ext''
   1.104 +    [@{const_name SMT.pat}, @{const_name SMT.nopat}, @{const_name SMT.trigger}]
   1.105  
   1.106  end
   1.107  
   1.108 @@ -272,7 +277,8 @@
   1.109        Syntax.string_of_term ctxt t)
   1.110  
   1.111    fun check_weight_conv ctxt ct =
   1.112 -    if U.under_quant proper_trigger (U.term_of ct) then Conv.all_conv ct
   1.113 +    if SMT_Utils.under_quant proper_trigger (SMT_Utils.term_of ct) then
   1.114 +      Conv.all_conv ct
   1.115      else check_weight_error ctxt (Thm.term_of ct)
   1.116  
   1.117  
   1.118 @@ -294,13 +300,14 @@
   1.119    fun add_weight_conv NONE _ = Conv.all_conv
   1.120      | add_weight_conv (SOME weight) ctxt =
   1.121          let val cv = Conv.rewr_conv (mk_weight_eq weight)
   1.122 -        in U.under_quant_conv (K (under_trigger_conv cv)) ctxt end
   1.123 +        in SMT_Utils.under_quant_conv (K (under_trigger_conv cv)) ctxt end
   1.124  in
   1.125  
   1.126  fun weight_conv weight ctxt = 
   1.127 -  U.prop_conv (check_weight_conv ctxt then_conv add_weight_conv weight ctxt)
   1.128 +  SMT_Utils.prop_conv
   1.129 +    (check_weight_conv ctxt then_conv add_weight_conv weight ctxt)
   1.130  
   1.131 -val setup_weight = B.add_builtin_fun_ext'' @{const_name SMT.weight}
   1.132 +val setup_weight = SMT_Builtin.add_builtin_fun_ext'' @{const_name SMT.weight}
   1.133  
   1.134  end
   1.135  
   1.136 @@ -355,11 +362,12 @@
   1.137      "distinct [x, y] = (x ~= y)"
   1.138      by simp_all}
   1.139    fun distinct_conv _ =
   1.140 -    U.if_true_conv is_trivial_distinct (Conv.rewrs_conv thms)
   1.141 +    SMT_Utils.if_true_conv is_trivial_distinct (Conv.rewrs_conv thms)
   1.142  in
   1.143  
   1.144 -fun trivial_distinct_conv ctxt = U.if_exists_conv is_trivial_distinct
   1.145 -  (Conv.top_conv distinct_conv ctxt)
   1.146 +fun trivial_distinct_conv ctxt =
   1.147 +  SMT_Utils.if_exists_conv is_trivial_distinct
   1.148 +    (Conv.top_conv distinct_conv ctxt)
   1.149  
   1.150  end
   1.151  
   1.152 @@ -373,13 +381,14 @@
   1.153    val thm = mk_meta_eq @{lemma
   1.154      "bool_case = (%x y P. if P then x else y)" by (rule ext)+ simp}
   1.155  
   1.156 -  fun unfold_conv _ = U.if_true_conv is_bool_case (Conv.rewr_conv thm)
   1.157 +  fun unfold_conv _ = SMT_Utils.if_true_conv is_bool_case (Conv.rewr_conv thm)
   1.158  in
   1.159  
   1.160 -fun rewrite_bool_case_conv ctxt = U.if_exists_conv is_bool_case
   1.161 -  (Conv.top_conv unfold_conv ctxt)
   1.162 +fun rewrite_bool_case_conv ctxt =
   1.163 +  SMT_Utils.if_exists_conv is_bool_case (Conv.top_conv unfold_conv ctxt)
   1.164  
   1.165 -val setup_bool_case = B.add_builtin_fun_ext'' @{const_name "bool.bool_case"}
   1.166 +val setup_bool_case =
   1.167 +  SMT_Builtin.add_builtin_fun_ext'' @{const_name "bool.bool_case"}
   1.168  
   1.169  end
   1.170  
   1.171 @@ -400,7 +409,8 @@
   1.172    val defs = [(@{const_name min}, min_def), (@{const_name max}, max_def),
   1.173      (@{const_name abs}, abs_def)]
   1.174  
   1.175 -  fun is_builtinT ctxt T = B.is_builtin_typ_ext ctxt (Term.domain_type T)
   1.176 +  fun is_builtinT ctxt T =
   1.177 +    SMT_Builtin.is_builtin_typ_ext ctxt (Term.domain_type T)
   1.178  
   1.179    fun abs_min_max ctxt (Const (n, T)) =
   1.180          (case AList.lookup (op =) defs n of
   1.181 @@ -415,10 +425,10 @@
   1.182  in
   1.183  
   1.184  fun unfold_abs_min_max_conv ctxt =
   1.185 -  U.if_exists_conv (is_some o abs_min_max ctxt)
   1.186 +  SMT_Utils.if_exists_conv (is_some o abs_min_max ctxt)
   1.187      (Conv.top_conv unfold_amm_conv ctxt)
   1.188    
   1.189 -val setup_abs_min_max = fold (B.add_builtin_fun_ext'' o fst) defs
   1.190 +val setup_abs_min_max = fold (SMT_Builtin.add_builtin_fun_ext'' o fst) defs
   1.191  
   1.192  end
   1.193  
   1.194 @@ -482,7 +492,7 @@
   1.195  
   1.196    fun mk_number_eq ctxt i lhs =
   1.197      let
   1.198 -      val eq = U.mk_cequals lhs (Numeral.mk_cnumber @{ctyp int} i)
   1.199 +      val eq = SMT_Utils.mk_cequals lhs (Numeral.mk_cnumber @{ctyp int} i)
   1.200        val ss = HOL_ss
   1.201          addsimps [@{thm Nat_Numeral.int_nat_number_of}]
   1.202          addsimps @{thms neg_simps}
   1.203 @@ -508,11 +518,11 @@
   1.204    and ints_conv ctxt = Conv.top_sweep_conv int_conv ctxt
   1.205  
   1.206    and expand_conv ctxt =
   1.207 -    U.if_conv (is_nat_const o Term.head_of)
   1.208 +    SMT_Utils.if_conv (is_nat_const o Term.head_of)
   1.209        (expand_head_conv (Conv.rewrs_conv expands) then_conv ints_conv ctxt)
   1.210        (int_conv ctxt)
   1.211  
   1.212 -  and nat_conv ctxt = U.if_exists_conv is_nat_const'
   1.213 +  and nat_conv ctxt = SMT_Utils.if_exists_conv is_nat_const'
   1.214      (Conv.top_sweep_conv expand_conv ctxt)
   1.215  
   1.216    val uses_nat_int = Term.exists_subterm (member (op aconv) nat_int_coercions)
   1.217 @@ -525,8 +535,8 @@
   1.218    else (thms, [])
   1.219  
   1.220  val setup_nat_as_int =
   1.221 -  B.add_builtin_typ_ext (@{typ nat}, K true) #>
   1.222 -  fold (B.add_builtin_fun_ext' o Term.dest_Const) builtin_nat_ops
   1.223 +  SMT_Builtin.add_builtin_typ_ext (@{typ nat}, K true) #>
   1.224 +  fold (SMT_Builtin.add_builtin_fun_ext' o Term.dest_Const) builtin_nat_ops
   1.225  
   1.226  end
   1.227  
   1.228 @@ -542,7 +552,7 @@
   1.229  
   1.230    fun is_strange_number ctxt (t as Const (@{const_name number_of}, _) $ _) =
   1.231          (case try HOLogic.dest_number t of
   1.232 -          SOME (_, i) => B.is_builtin_num ctxt t andalso i < 2
   1.233 +          SOME (_, i) => SMT_Builtin.is_builtin_num ctxt t andalso i < 2
   1.234          | NONE => false)
   1.235      | is_strange_number _ _ = false
   1.236  
   1.237 @@ -558,12 +568,14 @@
   1.238        "Int.Bit1 (- k) = - Int.Bit1 (Int.pred k)"
   1.239        by simp_all (simp add: pred_def)}
   1.240  
   1.241 -  fun norm_num_conv ctxt = U.if_conv (is_strange_number ctxt)
   1.242 -    (Simplifier.rewrite (Simplifier.context ctxt pos_num_ss)) Conv.no_conv
   1.243 +  fun norm_num_conv ctxt =
   1.244 +    SMT_Utils.if_conv (is_strange_number ctxt)
   1.245 +      (Simplifier.rewrite (Simplifier.context ctxt pos_num_ss)) Conv.no_conv
   1.246  in
   1.247  
   1.248 -fun normalize_numerals_conv ctxt = U.if_exists_conv (is_strange_number ctxt)
   1.249 -  (Conv.top_sweep_conv norm_num_conv ctxt)
   1.250 +fun normalize_numerals_conv ctxt =
   1.251 +  SMT_Utils.if_exists_conv (is_strange_number ctxt)
   1.252 +    (Conv.top_sweep_conv norm_num_conv ctxt)
   1.253  
   1.254  end
   1.255  
   1.256 @@ -599,18 +611,19 @@
   1.257  
   1.258  structure Extra_Norms = Generic_Data
   1.259  (
   1.260 -  type T = extra_norm U.dict
   1.261 +  type T = extra_norm SMT_Utils.dict
   1.262    val empty = []
   1.263    val extend = I
   1.264 -  fun merge data = U.dict_merge fst data
   1.265 +  fun merge data = SMT_Utils.dict_merge fst data
   1.266  )
   1.267  
   1.268 -fun add_extra_norm (cs, norm) = Extra_Norms.map (U.dict_update (cs, norm))
   1.269 +fun add_extra_norm (cs, norm) =
   1.270 +  Extra_Norms.map (SMT_Utils.dict_update (cs, norm))
   1.271  
   1.272  fun apply_extra_norms ithms ctxt =
   1.273    let
   1.274      val cs = SMT_Config.solver_class_of ctxt
   1.275 -    val es = U.dict_lookup (Extra_Norms.get (Context.Proof ctxt)) cs
   1.276 +    val es = SMT_Utils.dict_lookup (Extra_Norms.get (Context.Proof ctxt)) cs
   1.277    in (burrow_ids (fold (fn e => e ctxt) es o rpair []) ithms, ctxt) end
   1.278  
   1.279  fun normalize iwthms ctxt =