src/HOL/Tools/SMT/smt_normalize.ML
changeset 66298 5ff9fe3fee66
parent 61268 abe08fb15a12
child 67149 e61557884799
     1.1 --- a/src/HOL/Tools/SMT/smt_normalize.ML	Thu Jul 27 15:22:35 2017 +0100
     1.2 +++ b/src/HOL/Tools/SMT/smt_normalize.ML	Fri Jul 28 15:36:32 2017 +0100
     1.3 @@ -327,6 +327,85 @@
     1.4  end
     1.5  
     1.6  
     1.7 +(** embedding of standard natural number operations into integer operations **)
     1.8 +
     1.9 +local
    1.10 +  val nat_embedding = @{thms nat_int' int_nat_nneg int_nat_neg}
    1.11 +
    1.12 +  val simple_nat_ops = [
    1.13 +    @{const less (nat)}, @{const less_eq (nat)},
    1.14 +    @{const Suc}, @{const plus (nat)}, @{const minus (nat)}]
    1.15 +
    1.16 +  val mult_nat_ops =
    1.17 +    [@{const times (nat)}, @{const divide (nat)}, @{const modulo (nat)}]
    1.18 +
    1.19 +  val nat_ops = simple_nat_ops @ mult_nat_ops
    1.20 +
    1.21 +  val nat_consts = nat_ops @ [@{const numeral (nat)},
    1.22 +    @{const zero_class.zero (nat)}, @{const one_class.one (nat)}]
    1.23 +
    1.24 +  val nat_int_coercions = [@{const of_nat (int)}, @{const nat}]
    1.25 +
    1.26 +  val builtin_nat_ops = nat_int_coercions @ simple_nat_ops
    1.27 +
    1.28 +  val is_nat_const = member (op aconv) nat_consts
    1.29 +
    1.30 +  fun is_nat_const' @{const of_nat (int)} = true
    1.31 +    | is_nat_const' t = is_nat_const t
    1.32 +
    1.33 +  val expands = map mk_meta_eq @{thms nat_zero_as_int nat_one_as_int nat_numeral_as_int
    1.34 +    nat_less_as_int nat_leq_as_int Suc_as_int nat_plus_as_int nat_minus_as_int nat_times_as_int
    1.35 +    nat_div_as_int nat_mod_as_int}
    1.36 +
    1.37 +  val ints = map mk_meta_eq @{thms of_nat_0 of_nat_1 int_Suc int_plus int_minus of_nat_mult zdiv_int
    1.38 +    zmod_int}
    1.39 +  val int_if = mk_meta_eq @{lemma "int (if P then n else m) = (if P then int n else int m)" by simp}
    1.40 +
    1.41 +  fun mk_number_eq ctxt i lhs =
    1.42 +    let
    1.43 +      val eq = SMT_Util.mk_cequals lhs (Numeral.mk_cnumber @{ctyp int} i)
    1.44 +      val ctxt' = put_simpset HOL_ss ctxt addsimps @{thms of_nat_numeral}
    1.45 +      val tac = HEADGOAL (Simplifier.simp_tac ctxt')
    1.46 +    in Goal.norm_result ctxt (Goal.prove_internal ctxt [] eq (K tac)) end
    1.47 +
    1.48 +  fun ite_conv cv1 cv2 =
    1.49 +    Conv.combination_conv (Conv.combination_conv (Conv.arg_conv cv1) cv2) cv2
    1.50 +
    1.51 +  fun int_conv ctxt ct =
    1.52 +    (case Thm.term_of ct of
    1.53 +      @{const of_nat (int)} $ (n as (@{const numeral (nat)} $ _)) =>
    1.54 +        Conv.rewr_conv (mk_number_eq ctxt (snd (HOLogic.dest_number n)) ct)
    1.55 +    | @{const of_nat (int)} $ _ =>
    1.56 +        (Conv.rewrs_conv ints then_conv Conv.sub_conv ints_conv ctxt) else_conv
    1.57 +        (Conv.rewr_conv int_if then_conv
    1.58 +          ite_conv (nat_conv ctxt) (int_conv ctxt)) else_conv
    1.59 +        Conv.sub_conv (Conv.top_sweep_conv nat_conv) ctxt
    1.60 +    | _ => Conv.no_conv) ct
    1.61 +
    1.62 +  and ints_conv ctxt = Conv.top_sweep_conv int_conv ctxt
    1.63 +
    1.64 +  and expand_conv ctxt =
    1.65 +    SMT_Util.if_conv (is_nat_const o Term.head_of)
    1.66 +      (expand_head_conv (Conv.rewrs_conv expands) then_conv ints_conv ctxt) (int_conv ctxt)
    1.67 +
    1.68 +  and nat_conv ctxt = SMT_Util.if_exists_conv is_nat_const' (Conv.top_sweep_conv expand_conv ctxt)
    1.69 +
    1.70 +  val uses_nat_int = Term.exists_subterm (member (op aconv) nat_int_coercions)
    1.71 +in
    1.72 +
    1.73 +val nat_as_int_conv = nat_conv
    1.74 +
    1.75 +fun add_nat_embedding thms =
    1.76 +  if exists (uses_nat_int o Thm.prop_of) thms then (thms, nat_embedding) else (thms, [])
    1.77 +
    1.78 +val setup_nat_as_int =
    1.79 +  SMT_Builtin.add_builtin_typ_ext (@{typ nat},
    1.80 +    fn ctxt => K (Config.get ctxt SMT_Config.nat_as_int)) #>
    1.81 +  fold (SMT_Builtin.add_builtin_fun_ext' o Term.dest_Const) builtin_nat_ops
    1.82 +
    1.83 +end
    1.84 +
    1.85 +
    1.86  (** normalize numerals **)
    1.87  
    1.88  local
    1.89 @@ -359,23 +438,27 @@
    1.90  
    1.91  (** combined unfoldings and rewritings **)
    1.92  
    1.93 -fun unfold_conv ctxt =
    1.94 -  rewrite_case_bool_conv ctxt then_conv
    1.95 -  unfold_abs_min_max_conv ctxt then_conv
    1.96 -  Thm.beta_conversion true
    1.97 -
    1.98 -fun unfold_polymorph ctxt = map (apsnd (Conv.fconv_rule (unfold_conv ctxt)))
    1.99 -fun unfold_monomorph ctxt = map (apsnd (Conv.fconv_rule (normalize_numerals_conv ctxt)))
   1.100 -
   1.101 -
   1.102 -(* overall normalization *)
   1.103 -
   1.104  fun burrow_ids f ithms =
   1.105    let
   1.106      val (is, thms) = split_list ithms
   1.107      val (thms', extra_thms) = f thms
   1.108    in (is ~~ thms') @ map (pair ~1) extra_thms end
   1.109  
   1.110 +fun unfold_conv ctxt =
   1.111 +  rewrite_case_bool_conv ctxt then_conv
   1.112 +  unfold_abs_min_max_conv ctxt then_conv
   1.113 +  (if Config.get ctxt SMT_Config.nat_as_int then nat_as_int_conv ctxt
   1.114 +   else Conv.all_conv) then_conv
   1.115 +  Thm.beta_conversion true
   1.116 +
   1.117 +fun unfold_polymorph ctxt = map (apsnd (Conv.fconv_rule (unfold_conv ctxt)))
   1.118 +fun unfold_monomorph ctxt =
   1.119 +  map (apsnd (Conv.fconv_rule (normalize_numerals_conv ctxt)))
   1.120 +  #> Config.get ctxt SMT_Config.nat_as_int ? burrow_ids add_nat_embedding
   1.121 +
   1.122 +
   1.123 +(* overall normalization *)
   1.124 +
   1.125  type extra_norm = Proof.context -> thm list * thm list -> thm list * thm list
   1.126  
   1.127  structure Extra_Norms = Generic_Data
   1.128 @@ -439,6 +522,7 @@
   1.129    setup_unfolded_quants #>
   1.130    setup_trigger #>
   1.131    setup_case_bool #>
   1.132 -  setup_abs_min_max))
   1.133 +  setup_abs_min_max #>
   1.134 +  setup_nat_as_int))
   1.135  
   1.136  end;