src/HOL/Tools/SMT2/smt2_normalize.ML
changeset 56090 34bd10a9a2ad
parent 56078 624faeda77b5
child 56100 0dc5f68a7802
     1.1 --- a/src/HOL/Tools/SMT2/smt2_normalize.ML	Thu Mar 13 13:18:13 2014 +0100
     1.2 +++ b/src/HOL/Tools/SMT2/smt2_normalize.ML	Thu Mar 13 13:18:14 2014 +0100
     1.3 @@ -9,8 +9,7 @@
     1.4    val drop_fact_warning: Proof.context -> thm -> unit
     1.5    val atomize_conv: Proof.context -> conv
     1.6    type extra_norm = Proof.context -> thm list * thm list -> thm list * thm list
     1.7 -  val add_extra_norm: SMT2_Utils.class * extra_norm -> Context.generic ->
     1.8 -    Context.generic
     1.9 +  val add_extra_norm: SMT2_Util.class * extra_norm -> Context.generic -> Context.generic
    1.10    val normalize: (int * (int option * thm)) list -> Proof.context ->
    1.11      (int * thm) list * Proof.context
    1.12  end
    1.13 @@ -28,8 +27,7 @@
    1.14  (** instantiate elimination rules **)
    1.15   
    1.16  local
    1.17 -  val (cpfalse, cfalse) =
    1.18 -    `SMT2_Utils.mk_cprop (Thm.cterm_of @{theory} @{const False})
    1.19 +  val (cpfalse, cfalse) = `SMT2_Util.mk_cprop (Thm.cterm_of @{theory} @{const False})
    1.20  
    1.21    fun inst f ct thm =
    1.22      let val cv = f (Drule.strip_imp_concl (Thm.cprop_of thm))
    1.23 @@ -102,8 +100,7 @@
    1.24  in
    1.25  
    1.26  fun unfold_special_quants_conv ctxt =
    1.27 -  SMT2_Utils.if_exists_conv (is_some o special_quant)
    1.28 -    (Conv.top_conv special_quant_conv ctxt)
    1.29 +  SMT2_Util.if_exists_conv (is_some o special_quant) (Conv.top_conv special_quant_conv ctxt)
    1.30  
    1.31  val setup_unfolded_quants =
    1.32    fold (SMT2_Builtin.add_builtin_fun_ext'' o fst) special_quants
    1.33 @@ -144,8 +141,7 @@
    1.34        "must have the same kind: " ^ Syntax.string_of_term ctxt t)
    1.35  
    1.36    fun check_trigger_conv ctxt ct =
    1.37 -    if proper_quant false proper_trigger (SMT2_Utils.term_of ct) then
    1.38 -      Conv.all_conv ct
    1.39 +    if proper_quant false proper_trigger (SMT2_Util.term_of ct) then Conv.all_conv ct
    1.40      else check_trigger_error ctxt (Thm.term_of ct)
    1.41  
    1.42  
    1.43 @@ -198,12 +194,10 @@
    1.44              Pattern.matches thy (t', u) andalso not (t aconv u))
    1.45          in not (Term.exists_subterm some_match u) end
    1.46  
    1.47 -  val pat =
    1.48 -    SMT2_Utils.mk_const_pat @{theory} @{const_name SMT2.pat} SMT2_Utils.destT1
    1.49 -  fun mk_pat ct = Thm.apply (SMT2_Utils.instT' ct pat) ct
    1.50 +  val pat = SMT2_Util.mk_const_pat @{theory} @{const_name SMT2.pat} SMT2_Util.destT1
    1.51 +  fun mk_pat ct = Thm.apply (SMT2_Util.instT' ct pat) ct
    1.52  
    1.53 -  fun mk_clist T = pairself (Thm.cterm_of @{theory})
    1.54 -    (HOLogic.cons_const T, HOLogic.nil_const T)
    1.55 +  fun mk_clist T = pairself (Thm.cterm_of @{theory}) (HOLogic.cons_const T, HOLogic.nil_const T)
    1.56    fun mk_list (ccons, cnil) f cts = fold_rev (Thm.mk_binop ccons o f) cts cnil
    1.57    val mk_pat_list = mk_list (mk_clist @{typ SMT2.pattern})
    1.58    val mk_mpat_list = mk_list (mk_clist @{typ "SMT2.pattern list"})  
    1.59 @@ -236,20 +230,17 @@
    1.60      | has_trigger _ = false
    1.61  
    1.62    fun try_trigger_conv cv ct =
    1.63 -    if SMT2_Utils.under_quant has_trigger (SMT2_Utils.term_of ct) then
    1.64 -      Conv.all_conv ct
    1.65 +    if SMT2_Util.under_quant has_trigger (SMT2_Util.term_of ct) then Conv.all_conv ct
    1.66      else Conv.try_conv cv ct
    1.67  
    1.68    fun infer_trigger_conv ctxt =
    1.69      if Config.get ctxt SMT2_Config.infer_triggers then
    1.70 -      try_trigger_conv
    1.71 -        (SMT2_Utils.under_quant_conv (infer_trigger_eq_conv ctxt) ctxt)
    1.72 +      try_trigger_conv (SMT2_Util.under_quant_conv (infer_trigger_eq_conv ctxt) ctxt)
    1.73      else Conv.all_conv
    1.74  in
    1.75  
    1.76  fun trigger_conv ctxt =
    1.77 -  SMT2_Utils.prop_conv
    1.78 -    (check_trigger_conv ctxt then_conv infer_trigger_conv ctxt)
    1.79 +  SMT2_Util.prop_conv (check_trigger_conv ctxt then_conv infer_trigger_conv ctxt)
    1.80  
    1.81  val setup_trigger =
    1.82    fold SMT2_Builtin.add_builtin_fun_ext''
    1.83 @@ -281,8 +272,7 @@
    1.84        Syntax.string_of_term ctxt t)
    1.85  
    1.86    fun check_weight_conv ctxt ct =
    1.87 -    if SMT2_Utils.under_quant proper_trigger (SMT2_Utils.term_of ct) then
    1.88 -      Conv.all_conv ct
    1.89 +    if SMT2_Util.under_quant proper_trigger (SMT2_Util.term_of ct) then Conv.all_conv ct
    1.90      else check_weight_error ctxt (Thm.term_of ct)
    1.91  
    1.92  
    1.93 @@ -304,12 +294,11 @@
    1.94    fun add_weight_conv NONE _ = Conv.all_conv
    1.95      | add_weight_conv (SOME weight) ctxt =
    1.96          let val cv = Conv.rewr_conv (mk_weight_eq weight)
    1.97 -        in SMT2_Utils.under_quant_conv (K (under_trigger_conv cv)) ctxt end
    1.98 +        in SMT2_Util.under_quant_conv (K (under_trigger_conv cv)) ctxt end
    1.99  in
   1.100  
   1.101  fun weight_conv weight ctxt = 
   1.102 -  SMT2_Utils.prop_conv
   1.103 -    (check_weight_conv ctxt then_conv add_weight_conv weight ctxt)
   1.104 +  SMT2_Util.prop_conv (check_weight_conv ctxt then_conv add_weight_conv weight ctxt)
   1.105  
   1.106  val setup_weight = SMT2_Builtin.add_builtin_fun_ext'' @{const_name SMT2.weight}
   1.107  
   1.108 @@ -364,12 +353,11 @@
   1.109      "case_bool = (%x y P. if P then x else y)" by (rule ext)+ simp}
   1.110  
   1.111    fun unfold_conv _ =
   1.112 -    SMT2_Utils.if_true_conv (is_case_bool o Term.head_of)
   1.113 -      (expand_head_conv (Conv.rewr_conv thm))
   1.114 +    SMT2_Util.if_true_conv (is_case_bool o Term.head_of) (expand_head_conv (Conv.rewr_conv thm))
   1.115  in
   1.116  
   1.117  fun rewrite_case_bool_conv ctxt =
   1.118 -  SMT2_Utils.if_exists_conv is_case_bool (Conv.top_conv unfold_conv ctxt)
   1.119 +  SMT2_Util.if_exists_conv is_case_bool (Conv.top_conv unfold_conv ctxt)
   1.120  
   1.121  val setup_case_bool =
   1.122    SMT2_Builtin.add_builtin_fun_ext'' @{const_name "bool.case_bool"}
   1.123 @@ -409,8 +397,7 @@
   1.124  in
   1.125  
   1.126  fun unfold_abs_min_max_conv ctxt =
   1.127 -  SMT2_Utils.if_exists_conv (is_some o abs_min_max ctxt)
   1.128 -    (Conv.top_conv unfold_amm_conv ctxt)
   1.129 +  SMT2_Util.if_exists_conv (is_some o abs_min_max ctxt) (Conv.top_conv unfold_amm_conv ctxt)
   1.130    
   1.131  val setup_abs_min_max = fold (SMT2_Builtin.add_builtin_fun_ext'' o fst) defs
   1.132  
   1.133 @@ -478,7 +465,7 @@
   1.134  
   1.135    fun mk_number_eq ctxt i lhs =
   1.136      let
   1.137 -      val eq = SMT2_Utils.mk_cequals lhs (Numeral.mk_cnumber @{ctyp int} i)
   1.138 +      val eq = SMT2_Util.mk_cequals lhs (Numeral.mk_cnumber @{ctyp int} i)
   1.139        val ctxt' = put_simpset HOL_ss ctxt addsimps @{thms Int.int_numeral}
   1.140        val tac = HEADGOAL (Simplifier.simp_tac ctxt')
   1.141      in Goal.norm_result ctxt (Goal.prove_internal ctxt [] eq (K tac)) end
   1.142 @@ -500,11 +487,10 @@
   1.143    and ints_conv ctxt = Conv.top_sweep_conv int_conv ctxt
   1.144  
   1.145    and expand_conv ctxt =
   1.146 -    SMT2_Utils.if_conv (is_nat_const o Term.head_of)
   1.147 -      (expand_head_conv (Conv.rewrs_conv expands) then_conv ints_conv ctxt)
   1.148 -      (int_conv ctxt)
   1.149 +    SMT2_Util.if_conv (is_nat_const o Term.head_of)
   1.150 +      (expand_head_conv (Conv.rewrs_conv expands) then_conv ints_conv ctxt) (int_conv ctxt)
   1.151  
   1.152 -  and nat_conv ctxt = SMT2_Utils.if_exists_conv is_nat_const' (Conv.top_sweep_conv expand_conv ctxt)
   1.153 +  and nat_conv ctxt = SMT2_Util.if_exists_conv is_nat_const' (Conv.top_sweep_conv expand_conv ctxt)
   1.154  
   1.155    val uses_nat_int = Term.exists_subterm (member (op aconv) nat_int_coercions)
   1.156  in
   1.157 @@ -544,13 +530,12 @@
   1.158        addsimps @{thms Num.numeral_One minus_zero})
   1.159  
   1.160    fun norm_num_conv ctxt =
   1.161 -    SMT2_Utils.if_conv (is_strange_number ctxt)
   1.162 -      (Simplifier.rewrite (put_simpset proper_num_ss ctxt)) Conv.no_conv
   1.163 +    SMT2_Util.if_conv (is_strange_number ctxt) (Simplifier.rewrite (put_simpset proper_num_ss ctxt))
   1.164 +      Conv.no_conv
   1.165  in
   1.166  
   1.167  fun normalize_numerals_conv ctxt =
   1.168 -  SMT2_Utils.if_exists_conv (is_strange_number ctxt)
   1.169 -    (Conv.top_sweep_conv norm_num_conv ctxt)
   1.170 +  SMT2_Util.if_exists_conv (is_strange_number ctxt) (Conv.top_sweep_conv norm_num_conv ctxt)
   1.171  
   1.172  end
   1.173  
   1.174 @@ -584,19 +569,18 @@
   1.175  
   1.176  structure Extra_Norms = Generic_Data
   1.177  (
   1.178 -  type T = extra_norm SMT2_Utils.dict
   1.179 +  type T = extra_norm SMT2_Util.dict
   1.180    val empty = []
   1.181    val extend = I
   1.182 -  fun merge data = SMT2_Utils.dict_merge fst data
   1.183 +  fun merge data = SMT2_Util.dict_merge fst data
   1.184  )
   1.185  
   1.186 -fun add_extra_norm (cs, norm) =
   1.187 -  Extra_Norms.map (SMT2_Utils.dict_update (cs, norm))
   1.188 +fun add_extra_norm (cs, norm) = Extra_Norms.map (SMT2_Util.dict_update (cs, norm))
   1.189  
   1.190  fun apply_extra_norms ctxt ithms =
   1.191    let
   1.192      val cs = SMT2_Config.solver_class_of ctxt
   1.193 -    val es = SMT2_Utils.dict_lookup (Extra_Norms.get (Context.Proof ctxt)) cs
   1.194 +    val es = SMT2_Util.dict_lookup (Extra_Norms.get (Context.Proof ctxt)) cs
   1.195    in burrow_ids (fold (fn e => e ctxt) es o rpair []) ithms end
   1.196  
   1.197  local