equal
deleted
inserted
replaced
3 Author: Amine Chaieb, TU Muenchen |
3 Author: Amine Chaieb, TU Muenchen |
4 *) |
4 *) |
5 |
5 |
6 signature NORMALIZER = |
6 signature NORMALIZER = |
7 sig |
7 sig |
8 val mk_cnumber : ctyp -> int -> cterm |
8 val mk_cnumber : ctyp -> integer -> cterm |
9 val mk_cnumeral : int -> cterm |
9 val mk_cnumeral : integer -> cterm |
10 val semiring_normalize_conv : Proof.context -> Conv.conv |
10 val semiring_normalize_conv : Proof.context -> Conv.conv |
11 val semiring_normalize_tac : Proof.context -> int -> tactic |
11 val semiring_normalize_tac : Proof.context -> int -> tactic |
12 val semiring_normalize_wrapper : NormalizerData.entry -> Conv.conv |
12 val semiring_normalize_wrapper : NormalizerData.entry -> Conv.conv |
13 val semiring_normalizers_conv : |
13 val semiring_normalizers_conv : |
14 cterm list -> cterm list * thm list -> cterm list * thm list -> |
14 cterm list -> cterm list * thm list -> cterm list * thm list -> |
34 in |
34 in |
35 |
35 |
36 fun mk_cnumeral 0 = pls_const |
36 fun mk_cnumeral 0 = pls_const |
37 | mk_cnumeral ~1 = min_const |
37 | mk_cnumeral ~1 = min_const |
38 | mk_cnumeral i = |
38 | mk_cnumeral i = |
39 let val (q, r) = IntInf.divMod (i, 2) |
39 let val (q, r) = Integer.divmod i 2 |
40 in Thm.capply (Thm.capply bit_const (mk_cnumeral q)) (mk_cbit (IntInf.toInt r)) |
40 in Thm.capply (Thm.capply bit_const (mk_cnumeral q)) (mk_cbit (Integer.machine_int r)) end; |
41 end; |
|
42 |
41 |
43 fun mk_cnumber cT = |
42 fun mk_cnumber cT = |
44 let |
43 let |
45 val [nb_of, z, on] = |
44 val [nb_of, z, on] = |
46 map (Drule.cterm_rule (instantiate' [SOME cT] [])) [@{cpat "number_of"}, zero, one] |
45 map (Drule.cterm_rule (instantiate' [SOME cT] [])) [@{cpat "number_of"}, zero, one] |