62 t::past, terms) |
62 t::past, terms) |
63 end; |
63 end; |
64 |
64 |
65 (*the simplification procedure*) |
65 (*the simplification procedure*) |
66 fun proc sg _ t = |
66 fun proc sg _ t = |
67 let val (u,m,n,terms) = find_repeated (Termtab.empty, [], Data.dest_sum t) |
67 let (*first freeze any Vars in the term to prevent flex-flex problems*) |
|
68 val rand_s = gensym"_" |
|
69 fun mk_inst (var as Var((a,i),T)) = |
|
70 (var, Free((a ^ rand_s ^ string_of_int i), T)) |
|
71 val t' = subst_atomic (map mk_inst (term_vars t)) t |
|
72 val (u,m,n,terms) = find_repeated (Termtab.empty, [], Data.dest_sum t') |
68 val reshape = (*Move i*u to the front and put j*u into standard form |
73 val reshape = (*Move i*u to the front and put j*u into standard form |
69 i + #m + j + k == #m + i + (j + k) *) |
74 i + #m + j + k == #m + i + (j + k) *) |
70 if m=0 orelse n=0 then (*trivial, so do nothing*) |
75 if m=0 orelse n=0 then (*trivial, so do nothing*) |
71 raise TERM("combine_numerals", []) |
76 raise TERM("combine_numerals", []) |
72 else Data.prove_conv [Data.norm_tac] sg |
77 else Data.prove_conv [Data.norm_tac] sg |
73 (t, |
78 (t', |
74 Data.mk_sum ([Data.mk_coeff(m,u), |
79 Data.mk_sum ([Data.mk_coeff(m,u), |
75 Data.mk_coeff(n,u)] @ terms)) |
80 Data.mk_coeff(n,u)] @ terms)) |
76 in |
81 in |
77 apsome Data.simplify_meta_eq |
82 apsome Data.simplify_meta_eq |
78 (Data.prove_conv |
83 (Data.prove_conv |
79 [Data.trans_tac reshape, rtac Data.left_distrib 1, |
84 [Data.trans_tac reshape, rtac Data.left_distrib 1, |
80 Data.numeral_simp_tac] sg |
85 Data.numeral_simp_tac] sg |
81 (t, Data.mk_sum (Data.mk_coeff(m+n,u) :: terms))) |
86 (t', Data.mk_sum (Data.mk_coeff(m+n,u) :: terms))) |
82 end |
87 end |
83 handle TERM _ => None |
88 handle TERM _ => None |
84 | TYPE _ => None; (*Typically (if thy doesn't include Numeral) |
89 | TYPE _ => None; (*Typically (if thy doesn't include Numeral) |
85 Undeclared type constructor "Numeral.bin"*) |
90 Undeclared type constructor "Numeral.bin"*) |
86 |
91 |