equal
deleted
inserted
replaced
7 * rewrite bool case expressions as if expressions, |
7 * rewrite bool case expressions as if expressions, |
8 * normalize numerals (e.g. replace negative numerals by negated positive |
8 * normalize numerals (e.g. replace negative numerals by negated positive |
9 numerals), |
9 numerals), |
10 * embed natural numbers into integers, |
10 * embed natural numbers into integers, |
11 * add extra rules specifying types and constants which occur frequently, |
11 * add extra rules specifying types and constants which occur frequently, |
|
12 * fully translate into object logic, add universal closure, |
12 * lift lambda terms, |
13 * lift lambda terms, |
13 * make applications explicit for functions with varying number of arguments, |
14 * make applications explicit for functions with varying number of arguments. |
14 * fully translate into object logic, add universal closure. |
|
15 *) |
15 *) |
16 |
16 |
17 signature SMT_NORMALIZE = |
17 signature SMT_NORMALIZE = |
18 sig |
18 sig |
19 val instantiate_free: cterm * cterm -> thm -> thm |
19 val instantiate_free: cterm * cterm -> thm -> thm |
40 in |
40 in |
41 Thm.implies_intr ct thm |
41 Thm.implies_intr ct thm |
42 |> instantiate_free (cv, cu) |
42 |> instantiate_free (cv, cu) |
43 |> (fn thm => Thm.implies_elim thm (Thm.reflexive cu)) |
43 |> (fn thm => Thm.implies_elim thm (Thm.reflexive cu)) |
44 end |
44 end |
45 |
|
46 |
|
47 |
|
48 (* simplification of trivial let expressions (whose bound variables occur at |
|
49 most once) *) |
|
50 |
|
51 local |
|
52 fun count i (Bound j) = if j = i then 1 else 0 |
|
53 | count i (t $ u) = count i t + count i u |
|
54 | count i (Abs (_, _, t)) = count (i + 1) t |
|
55 | count _ _ = 0 |
|
56 |
|
57 fun is_trivial_let (Const (@{const_name Let}, _) $ _ $ Abs (_, _, t)) = |
|
58 (count 0 t <= 1) |
|
59 | is_trivial_let _ = false |
|
60 |
|
61 fun let_conv _ = if_true_conv is_trivial_let (Conv.rewr_conv @{thm Let_def}) |
|
62 in |
|
63 fun trivial_let ctxt = |
|
64 map ((Term.exists_subterm is_trivial_let o Thm.prop_of) ?? |
|
65 Conv.fconv_rule (More_Conv.top_conv let_conv ctxt)) |
|
66 end |
|
67 |
45 |
68 |
46 |
69 |
47 |
70 (* simplification of trivial distincts (distinct should have at least |
48 (* simplification of trivial distincts (distinct should have at least |
71 three elements in the argument list) *) |
49 three elements in the argument list) *) |
505 |
483 |
506 (* combined normalization *) |
484 (* combined normalization *) |
507 |
485 |
508 fun normalize ctxt thms = |
486 fun normalize ctxt thms = |
509 thms |
487 thms |
510 |> trivial_let ctxt |
|
511 |> trivial_distinct ctxt |
488 |> trivial_distinct ctxt |
512 |> rewrite_bool_cases ctxt |
489 |> rewrite_bool_cases ctxt |
513 |> normalize_numerals ctxt |
490 |> normalize_numerals ctxt |
514 |> nat_as_int ctxt |
491 |> nat_as_int ctxt |
515 |> map (unfold_defs ctxt #> normalize_rule ctxt) |
492 |> map (unfold_defs ctxt #> normalize_rule ctxt) |