25 val mk_coeff: IntInf.int * term -> term |
25 val mk_coeff: IntInf.int * term -> term |
26 val dest_coeff: term -> IntInf.int * term |
26 val dest_coeff: term -> IntInf.int * term |
27 (*rules*) |
27 (*rules*) |
28 val left_distrib: thm |
28 val left_distrib: thm |
29 (*proof tools*) |
29 (*proof tools*) |
30 val prove_conv: tactic list -> Sign.sg -> string list -> term * term -> thm option |
30 val prove_conv: tactic list -> theory -> string list -> term * term -> thm option |
31 val trans_tac: thm option -> tactic (*applies the initial lemma*) |
31 val trans_tac: simpset -> thm option -> tactic (*applies the initial lemma*) |
32 val norm_tac: tactic (*proves the initial lemma*) |
32 val norm_tac: simpset -> tactic (*proves the initial lemma*) |
33 val numeral_simp_tac: tactic (*proves the final theorem*) |
33 val numeral_simp_tac: simpset -> tactic (*proves the final theorem*) |
34 val simplify_meta_eq: thm -> thm (*simplifies the final theorem*) |
34 val simplify_meta_eq: simpset -> thm -> thm (*simplifies the final theorem*) |
35 end; |
35 end; |
36 |
36 |
37 |
37 |
38 functor CombineNumeralsFun(Data: COMBINE_NUMERALS_DATA): |
38 functor CombineNumeralsFun(Data: COMBINE_NUMERALS_DATA): |
39 sig |
39 sig |
40 val proc: Sign.sg -> simpset -> term -> thm option |
40 val proc: theory -> simpset -> term -> thm option |
41 end |
41 end |
42 = |
42 = |
43 struct |
43 struct |
44 |
44 |
45 (*Remove the first occurrence of #m*u from the term list*) |
45 (*Remove the first occurrence of #m*u from the term list*) |
62 | NONE => find_repeated (Termtab.update ((u,n), tab), |
62 | NONE => find_repeated (Termtab.update ((u,n), tab), |
63 t::past, terms)) |
63 t::past, terms)) |
64 | NONE => find_repeated (tab, t::past, terms); |
64 | NONE => find_repeated (tab, t::past, terms); |
65 |
65 |
66 (*the simplification procedure*) |
66 (*the simplification procedure*) |
67 fun proc sg _ t = |
67 fun proc thy ss t = |
68 let (*first freeze any Vars in the term to prevent flex-flex problems*) |
68 let (*first freeze any Vars in the term to prevent flex-flex problems*) |
69 val (t', xs) = Term.adhoc_freeze_vars t |
69 val (t', xs) = Term.adhoc_freeze_vars t |
70 val (u,m,n,terms) = find_repeated (Termtab.empty, [], Data.dest_sum t') |
70 val (u,m,n,terms) = find_repeated (Termtab.empty, [], Data.dest_sum t') |
71 val T = Term.fastype_of u |
71 val T = Term.fastype_of u |
72 val reshape = (*Move i*u to the front and put j*u into standard form |
72 val reshape = (*Move i*u to the front and put j*u into standard form |
73 i + #m + j + k == #m + i + (j + k) *) |
73 i + #m + j + k == #m + i + (j + k) *) |
74 if m=0 orelse n=0 then (*trivial, so do nothing*) |
74 if m=0 orelse n=0 then (*trivial, so do nothing*) |
75 raise TERM("combine_numerals", []) |
75 raise TERM("combine_numerals", []) |
76 else Data.prove_conv [Data.norm_tac] sg xs |
76 else Data.prove_conv [Data.norm_tac ss] thy xs |
77 (t', |
77 (t', |
78 Data.mk_sum T ([Data.mk_coeff(m,u), |
78 Data.mk_sum T ([Data.mk_coeff(m,u), |
79 Data.mk_coeff(n,u)] @ terms)) |
79 Data.mk_coeff(n,u)] @ terms)) |
80 in |
80 in |
81 Option.map Data.simplify_meta_eq |
81 Option.map (Data.simplify_meta_eq ss) |
82 (Data.prove_conv |
82 (Data.prove_conv |
83 [Data.trans_tac reshape, rtac Data.left_distrib 1, |
83 [Data.trans_tac ss reshape, rtac Data.left_distrib 1, |
84 Data.numeral_simp_tac] sg xs |
84 Data.numeral_simp_tac ss] thy xs |
85 (t', Data.mk_sum T (Data.mk_coeff(Data.add(m,n), u) :: terms))) |
85 (t', Data.mk_sum T (Data.mk_coeff(Data.add(m,n), u) :: terms))) |
86 end |
86 end |
87 handle TERM _ => NONE |
87 handle TERM _ => NONE |
88 | TYPE _ => NONE; (*Typically (if thy doesn't include Numeral) |
88 | TYPE _ => NONE; (*Typically (if thy doesn't include Numeral) |
89 Undeclared type constructor "Numeral.bin"*) |
89 Undeclared type constructor "Numeral.bin"*) |