equal
deleted
inserted
replaced
11 * fully translate into object logic, add universal closure. |
11 * fully translate into object logic, add universal closure. |
12 *) |
12 *) |
13 |
13 |
14 signature SMT_NORMALIZE = |
14 signature SMT_NORMALIZE = |
15 sig |
15 sig |
16 val normalize_rule: Proof.context -> thm -> thm |
|
17 val instantiate_free: cterm * cterm -> thm -> thm |
16 val instantiate_free: cterm * cterm -> thm -> thm |
18 val discharge_definition: cterm -> thm -> thm |
17 val discharge_definition: cterm -> thm -> thm |
19 |
18 |
20 val trivial_let: Proof.context -> thm list -> thm list |
19 val normalize: Proof.context -> thm list -> cterm list * thm list |
21 val positive_numerals: Proof.context -> thm list -> thm list |
|
22 val nat_as_int: Proof.context -> thm list -> thm list |
|
23 val add_pair_rules: Proof.context -> thm list -> thm list |
|
24 val add_fun_upd_rules: Proof.context -> thm list -> thm list |
|
25 |
|
26 datatype config = |
|
27 RewriteTrivialLets | |
|
28 RewriteNegativeNumerals | |
|
29 RewriteNaturalNumbers | |
|
30 AddPairRules | |
|
31 AddFunUpdRules |
|
32 |
|
33 val normalize: config list -> Proof.context -> thm list -> |
|
34 cterm list * thm list |
|
35 end |
20 end |
36 |
21 |
37 structure SMT_Normalize: SMT_NORMALIZE = |
22 structure SMT_Normalize: SMT_NORMALIZE = |
38 struct |
23 struct |
39 |
24 |
483 end |
468 end |
484 |
469 |
485 |
470 |
486 (* combined normalization *) |
471 (* combined normalization *) |
487 |
472 |
488 datatype config = |
473 fun normalize ctxt thms = |
489 RewriteTrivialLets | |
474 thms |
490 RewriteNegativeNumerals | |
475 |> trivial_let ctxt |
491 RewriteNaturalNumbers | |
476 |> positive_numerals ctxt |
492 AddPairRules | |
477 |> nat_as_int ctxt |
493 AddFunUpdRules |
478 |> add_pair_rules ctxt |
494 |
479 |> add_fun_upd_rules ctxt |
495 fun normalize config ctxt thms = |
480 |> map (unfold_defs ctxt #> normalize_rule ctxt) |
496 let fun if_enabled c f = member (op =) config c ? f ctxt |
481 |> lift_lambdas ctxt |
497 in |
482 |> apsnd (explicit_application ctxt) |
498 thms |
483 |
499 |> if_enabled RewriteTrivialLets trivial_let |
484 end |
500 |> if_enabled RewriteNegativeNumerals positive_numerals |
|
501 |> if_enabled RewriteNaturalNumbers nat_as_int |
|
502 |> if_enabled AddPairRules add_pair_rules |
|
503 |> if_enabled AddFunUpdRules add_fun_upd_rules |
|
504 |> map (unfold_defs ctxt #> normalize_rule ctxt) |
|
505 |> lift_lambdas ctxt |
|
506 |> apsnd (explicit_application ctxt) |
|
507 end |
|
508 |
|
509 end |
|