8 sig |
8 sig |
9 val atomize_conv: Proof.context -> conv |
9 val atomize_conv: Proof.context -> conv |
10 type extra_norm = Proof.context -> thm list * thm list -> thm list * thm list |
10 type extra_norm = Proof.context -> thm list * thm list -> thm list * thm list |
11 val add_extra_norm: SMT_Utils.class * extra_norm -> Context.generic -> |
11 val add_extra_norm: SMT_Utils.class * extra_norm -> Context.generic -> |
12 Context.generic |
12 Context.generic |
13 val normalize: Proof.context -> (int * (int option * thm)) list -> |
13 val normalize: (int * (int option * thm)) list -> Proof.context -> |
14 (int * thm) list |
14 (int * thm) list * Proof.context |
15 val setup: theory -> theory |
15 val setup: theory -> theory |
16 end |
16 end |
17 |
17 |
18 structure SMT_Normalize: SMT_NORMALIZE = |
18 structure SMT_Normalize: SMT_NORMALIZE = |
19 struct |
19 struct |
572 fun unfold_conv ctxt = |
572 fun unfold_conv ctxt = |
573 trivial_distinct_conv ctxt then_conv |
573 trivial_distinct_conv ctxt then_conv |
574 rewrite_bool_case_conv ctxt then_conv |
574 rewrite_bool_case_conv ctxt then_conv |
575 unfold_abs_min_max_conv ctxt then_conv |
575 unfold_abs_min_max_conv ctxt then_conv |
576 nat_as_int_conv ctxt then_conv |
576 nat_as_int_conv ctxt then_conv |
577 normalize_numerals_conv ctxt then_conv |
|
578 Thm.beta_conversion true |
577 Thm.beta_conversion true |
|
578 |
|
579 fun unfold1 ctxt = map (apsnd (Conv.fconv_rule (unfold_conv ctxt))) |
579 |
580 |
580 fun burrow_ids f ithms = |
581 fun burrow_ids f ithms = |
581 let |
582 let |
582 val (is, thms) = split_list ithms |
583 val (is, thms) = split_list ithms |
583 val (thms', extra_thms) = f thms |
584 val (thms', extra_thms) = f thms |
584 in (is ~~ thms') @ map (pair ~1) extra_thms end |
585 in (is ~~ thms') @ map (pair ~1) extra_thms end |
585 |
586 |
586 fun unfold ctxt = |
587 fun unfold2 ithms ctxt = |
587 burrow_ids (map (Conv.fconv_rule (unfold_conv ctxt)) #> add_nat_embedding) |
588 ithms |
|
589 |> map (apsnd (Conv.fconv_rule (normalize_numerals_conv ctxt))) |
|
590 |> burrow_ids add_nat_embedding |
|
591 |> rpair ctxt |
588 |
592 |
589 |
593 |
590 |
594 |
591 (* overall normalization *) |
595 (* overall normalization *) |
592 |
596 |
600 fun merge data = U.dict_merge fst data |
604 fun merge data = U.dict_merge fst data |
601 ) |
605 ) |
602 |
606 |
603 fun add_extra_norm (cs, norm) = Extra_Norms.map (U.dict_update (cs, norm)) |
607 fun add_extra_norm (cs, norm) = Extra_Norms.map (U.dict_update (cs, norm)) |
604 |
608 |
605 fun apply_extra_norms ctxt = |
609 fun apply_extra_norms ithms ctxt = |
606 let |
610 let |
607 val cs = SMT_Config.solver_class_of ctxt |
611 val cs = SMT_Config.solver_class_of ctxt |
608 val es = U.dict_lookup (Extra_Norms.get (Context.Proof ctxt)) cs |
612 val es = U.dict_lookup (Extra_Norms.get (Context.Proof ctxt)) cs |
609 in burrow_ids (fold (fn e => e ctxt) es o rpair []) end |
613 in (burrow_ids (fold (fn e => e ctxt) es o rpair []) ithms, ctxt) end |
610 |
614 |
611 fun normalize ctxt iwthms = |
615 fun normalize iwthms ctxt = |
612 iwthms |
616 iwthms |
613 |> gen_normalize ctxt |
617 |> gen_normalize ctxt |
614 |> unfold ctxt |
618 |> unfold1 ctxt |
615 |> apply_extra_norms ctxt |
619 |> rpair ctxt |
|
620 |-> SMT_Monomorph.monomorph |
|
621 |-> unfold2 |
|
622 |-> apply_extra_norms |
616 |
623 |
617 val setup = Context.theory_map ( |
624 val setup = Context.theory_map ( |
618 setup_atomize #> |
625 setup_atomize #> |
619 setup_unfolded_quants #> |
626 setup_unfolded_quants #> |
620 setup_trigger #> |
627 setup_trigger #> |