--- a/src/HOL/Tools/SMT2/smt2_normalize.ML Mon Jul 28 11:03:28 2014 +0200
+++ b/src/HOL/Tools/SMT2/smt2_normalize.ML Sun Jul 27 21:20:11 2014 +0200
@@ -324,84 +324,6 @@
end
-(** embedding of standard natural number operations into integer operations **)
-
-local
- val nat_embedding = @{thms nat_int' int_nat_nneg int_nat_neg}
-
- val simple_nat_ops = [
- @{const less (nat)}, @{const less_eq (nat)},
- @{const Suc}, @{const plus (nat)}, @{const minus (nat)}]
-
- val mult_nat_ops =
- [@{const times (nat)}, @{const div (nat)}, @{const mod (nat)}]
-
- val nat_ops = simple_nat_ops @ mult_nat_ops
-
- val nat_consts = nat_ops @ [@{const numeral (nat)},
- @{const zero_class.zero (nat)}, @{const one_class.one (nat)}]
-
- val nat_int_coercions = [@{const of_nat (int)}, @{const nat}]
-
- val builtin_nat_ops = nat_int_coercions @ simple_nat_ops
-
- val is_nat_const = member (op aconv) nat_consts
-
- fun is_nat_const' @{const of_nat (int)} = true
- | is_nat_const' t = is_nat_const t
-
- val expands = map mk_meta_eq @{thms nat_zero_as_int nat_one_as_int nat_numeral_as_int
- nat_less_as_int nat_leq_as_int Suc_as_int nat_plus_as_int nat_minus_as_int nat_times_as_int
- nat_div_as_int nat_mod_as_int}
-
- val ints = map mk_meta_eq @{thms int_0 int_1 int_Suc int_plus int_minus int_mult zdiv_int
- zmod_int}
- val int_if = mk_meta_eq @{lemma "int (if P then n else m) = (if P then int n else int m)" by simp}
-
- fun mk_number_eq ctxt i lhs =
- let
- val eq = SMT2_Util.mk_cequals lhs (Numeral.mk_cnumber @{ctyp int} i)
- val ctxt' = put_simpset HOL_ss ctxt addsimps @{thms Int.int_numeral}
- val tac = HEADGOAL (Simplifier.simp_tac ctxt')
- in Goal.norm_result ctxt (Goal.prove_internal ctxt [] eq (K tac)) end
-
- fun ite_conv cv1 cv2 =
- Conv.combination_conv (Conv.combination_conv (Conv.arg_conv cv1) cv2) cv2
-
- fun int_conv ctxt ct =
- (case Thm.term_of ct of
- @{const of_nat (int)} $ (n as (@{const numeral (nat)} $ _)) =>
- Conv.rewr_conv (mk_number_eq ctxt (snd (HOLogic.dest_number n)) ct)
- | @{const of_nat (int)} $ _ =>
- (Conv.rewrs_conv ints then_conv Conv.sub_conv ints_conv ctxt) else_conv
- (Conv.rewr_conv int_if then_conv
- ite_conv (nat_conv ctxt) (int_conv ctxt)) else_conv
- Conv.sub_conv (Conv.top_sweep_conv nat_conv) ctxt
- | _ => Conv.no_conv) ct
-
- and ints_conv ctxt = Conv.top_sweep_conv int_conv ctxt
-
- and expand_conv ctxt =
- SMT2_Util.if_conv (is_nat_const o Term.head_of)
- (expand_head_conv (Conv.rewrs_conv expands) then_conv ints_conv ctxt) (int_conv ctxt)
-
- and nat_conv ctxt = SMT2_Util.if_exists_conv is_nat_const' (Conv.top_sweep_conv expand_conv ctxt)
-
- val uses_nat_int = Term.exists_subterm (member (op aconv) nat_int_coercions)
-in
-
-val nat_as_int_conv = nat_conv
-
-fun add_nat_embedding thms =
- if exists (uses_nat_int o Thm.prop_of) thms then (thms, nat_embedding) else (thms, [])
-
-val setup_nat_as_int =
- SMT2_Builtin.add_builtin_typ_ext (@{typ nat}, K true) #>
- fold (SMT2_Builtin.add_builtin_fun_ext' o Term.dest_Const) builtin_nat_ops
-
-end
-
-
(** normalize numerals **)
local
@@ -414,14 +336,12 @@
true
| is_irregular_number (Const (@{const_name uminus}, _) $ Const (@{const_name Groups.zero}, _)) =
true
- | is_irregular_number _ =
- false;
+ | is_irregular_number _ = false
- fun is_strange_number ctxt t = is_irregular_number t andalso SMT2_Builtin.is_builtin_num ctxt t;
+ fun is_strange_number ctxt t = is_irregular_number t andalso SMT2_Builtin.is_builtin_num ctxt t
val proper_num_ss =
- simpset_of (put_simpset HOL_ss @{context}
- addsimps @{thms Num.numeral_One minus_zero})
+ simpset_of (put_simpset HOL_ss @{context} addsimps @{thms Num.numeral_One minus_zero})
fun norm_num_conv ctxt =
SMT2_Util.if_conv (is_strange_number ctxt) (Simplifier.rewrite (put_simpset proper_num_ss ctxt))
@@ -439,10 +359,13 @@
fun unfold_conv ctxt =
rewrite_case_bool_conv ctxt then_conv
unfold_abs_min_max_conv ctxt then_conv
- nat_as_int_conv ctxt then_conv
Thm.beta_conversion true
-fun unfold1 ctxt = map (apsnd (Conv.fconv_rule (unfold_conv ctxt)))
+fun unfold_polymorph ctxt = map (apsnd (Conv.fconv_rule (unfold_conv ctxt)))
+fun unfold_monomorph ctxt = map (apsnd (Conv.fconv_rule (normalize_numerals_conv ctxt)))
+
+
+(* overall normalization *)
fun burrow_ids f ithms =
let
@@ -450,14 +373,6 @@
val (thms', extra_thms) = f thms
in (is ~~ thms') @ map (pair ~1) extra_thms end
-fun unfold2 ctxt ithms =
- ithms
- |> map (apsnd (Conv.fconv_rule (normalize_numerals_conv ctxt)))
- |> burrow_ids add_nat_embedding
-
-
-(* overall normalization *)
-
type extra_norm = Proof.context -> thm list * thm list -> thm list * thm list
structure Extra_Norms = Generic_Data
@@ -511,9 +426,9 @@
wthms
|> map_index I
|> gen_normalize ctxt
- |> unfold1 ctxt
+ |> unfold_polymorph ctxt
|> monomorph ctxt
- |> unfold2 ctxt
+ |> unfold_monomorph ctxt
|> apply_extra_norms ctxt
val _ = Theory.setup (Context.theory_map (
@@ -521,7 +436,6 @@
setup_unfolded_quants #>
setup_trigger #>
setup_case_bool #>
- setup_abs_min_max #>
- setup_nat_as_int))
+ setup_abs_min_max))
end;