src/HOL/Tools/SMT2/smt2_normalize.ML
changeset 57165 7b1bf424ec5f
parent 56981 3ef45ce002b5
child 57229 489083abce44
     1.1 --- a/src/HOL/Tools/SMT2/smt2_normalize.ML	Tue Jun 03 10:35:51 2014 +0200
     1.2 +++ b/src/HOL/Tools/SMT2/smt2_normalize.ML	Tue Jun 03 11:43:07 2014 +0200
     1.3 @@ -15,7 +15,7 @@
     1.4  
     1.5    type extra_norm = Proof.context -> thm list * thm list -> thm list * thm list
     1.6    val add_extra_norm: SMT2_Util.class * extra_norm -> Context.generic -> Context.generic
     1.7 -  val normalize: Proof.context -> (int option * thm) list -> (int * thm) list
     1.8 +  val normalize: Proof.context -> thm list -> (int * thm) list
     1.9  end
    1.10  
    1.11  structure SMT2_Normalize: SMT2_NORMALIZE =
    1.12 @@ -239,79 +239,25 @@
    1.13  end
    1.14  
    1.15  
    1.16 -(** adding quantifier weights **)
    1.17 -
    1.18 -local
    1.19 -  (*** check weight syntax ***)
    1.20 -
    1.21 -  val has_no_weight =
    1.22 -    not o Term.exists_subterm (fn @{const SMT2.weight} => true | _ => false)
    1.23 -
    1.24 -  fun is_weight (@{const SMT2.weight} $ w $ t) =
    1.25 -        (case try HOLogic.dest_number w of
    1.26 -          SOME (_, i) => i >= 0 andalso has_no_weight t
    1.27 -        | _ => false)
    1.28 -    | is_weight t = has_no_weight t
    1.29 -
    1.30 -  fun proper_trigger (@{const SMT2.trigger} $ _ $ t) = is_weight t
    1.31 -    | proper_trigger t = is_weight t 
    1.32 -
    1.33 -  fun check_weight_error ctxt t =
    1.34 -    error ("SMT weight must be a non-negative number and must only occur " ^
    1.35 -      "under the top-most quantifier and an optional trigger: " ^
    1.36 -      Syntax.string_of_term ctxt t)
    1.37 -
    1.38 -  fun check_weight_conv ctxt ct =
    1.39 -    if SMT2_Util.under_quant proper_trigger (SMT2_Util.term_of ct) then Conv.all_conv ct
    1.40 -    else check_weight_error ctxt (Thm.term_of ct)
    1.41 -
    1.42 -
    1.43 -  (*** insertion of weights ***)
    1.44 -
    1.45 -  fun under_trigger_conv cv ct =
    1.46 -    (case Thm.term_of ct of
    1.47 -      @{const SMT2.trigger} $ _ $ _ => Conv.arg_conv cv
    1.48 -    | _ => cv) ct
    1.49 -
    1.50 -  val weight_eq = mk_meta_eq @{lemma "p = SMT2.weight i p" by (simp add: weight_def)}
    1.51 -  fun mk_weight_eq w =
    1.52 -    let val cv = Thm.dest_arg1 (Thm.rhs_of weight_eq)
    1.53 -    in Thm.instantiate ([], [(cv, Numeral.mk_cnumber @{ctyp int} w)]) weight_eq end
    1.54 -
    1.55 -  fun add_weight_conv NONE _ = Conv.all_conv
    1.56 -    | add_weight_conv (SOME weight) ctxt =
    1.57 -        let val cv = Conv.rewr_conv (mk_weight_eq weight)
    1.58 -        in SMT2_Util.under_quant_conv (K (under_trigger_conv cv)) ctxt end
    1.59 -in
    1.60 -
    1.61 -fun weight_conv weight ctxt = 
    1.62 -  SMT2_Util.prop_conv (check_weight_conv ctxt then_conv add_weight_conv weight ctxt)
    1.63 -
    1.64 -val setup_weight = SMT2_Builtin.add_builtin_fun_ext'' @{const_name SMT2.weight}
    1.65 -
    1.66 -end
    1.67 -
    1.68 -
    1.69  (** combined general normalizations **)
    1.70  
    1.71 -fun gen_normalize1_conv ctxt weight =
    1.72 +fun gen_normalize1_conv ctxt =
    1.73    atomize_conv ctxt then_conv
    1.74    unfold_special_quants_conv ctxt then_conv
    1.75    Thm.beta_conversion true then_conv
    1.76 -  trigger_conv ctxt then_conv
    1.77 -  weight_conv weight ctxt
    1.78 +  trigger_conv ctxt
    1.79  
    1.80 -fun gen_normalize1 ctxt weight =
    1.81 +fun gen_normalize1 ctxt =
    1.82    instantiate_elim #>
    1.83    norm_def #>
    1.84    Conv.fconv_rule (Thm.beta_conversion true then_conv Thm.eta_conversion) #>
    1.85    Drule.forall_intr_vars #>
    1.86 -  Conv.fconv_rule (gen_normalize1_conv ctxt weight) #>
    1.87 +  Conv.fconv_rule (gen_normalize1_conv ctxt) #>
    1.88    (* Z3 4.3.1 silently normalizes "P --> Q --> R" to "P & Q --> R" *)
    1.89    Raw_Simplifier.rewrite_rule ctxt @{thms HOL.imp_conjL[symmetric, THEN eq_reflection]}
    1.90  
    1.91 -fun gen_norm1_safe ctxt (i, (weight, thm)) =
    1.92 -  (case try (gen_normalize1 ctxt weight) thm of
    1.93 +fun gen_norm1_safe ctxt (i, thm) =
    1.94 +  (case try (gen_normalize1 ctxt) thm of
    1.95      SOME thm' => SOME (i, thm')
    1.96    | NONE => (drop_fact_warning ctxt thm; NONE))
    1.97  
    1.98 @@ -576,7 +522,6 @@
    1.99    setup_atomize #>
   1.100    setup_unfolded_quants #>
   1.101    setup_trigger #>
   1.102 -  setup_weight #>
   1.103    setup_case_bool #>
   1.104    setup_abs_min_max #>
   1.105    setup_nat_as_int))