28 (*rules*) |
28 (*rules*) |
29 val left_distrib: thm |
29 val left_distrib: thm |
30 (*proof tools*) |
30 (*proof tools*) |
31 val prove_conv: tactic list -> Proof.context -> term * term -> thm option |
31 val prove_conv: tactic list -> Proof.context -> term * term -> thm option |
32 val trans_tac: thm option -> tactic (*applies the initial lemma*) |
32 val trans_tac: thm option -> tactic (*applies the initial lemma*) |
33 val norm_tac: simpset -> tactic (*proves the initial lemma*) |
33 val norm_tac: Proof.context -> tactic (*proves the initial lemma*) |
34 val numeral_simp_tac: simpset -> tactic (*proves the final theorem*) |
34 val numeral_simp_tac: Proof.context -> tactic (*proves the final theorem*) |
35 val simplify_meta_eq: simpset -> thm -> thm (*simplifies the final theorem*) |
35 val simplify_meta_eq: Proof.context -> thm -> thm (*simplifies the final theorem*) |
36 end; |
36 end; |
37 |
37 |
38 |
38 |
39 functor CombineNumeralsFun(Data: COMBINE_NUMERALS_DATA): |
39 functor CombineNumeralsFun(Data: COMBINE_NUMERALS_DATA): |
40 sig |
40 sig |
41 val proc: simpset -> term -> thm option |
41 val proc: Proof.context -> term -> thm option |
42 end |
42 end |
43 = |
43 = |
44 struct |
44 struct |
45 |
45 |
46 (*Remove the first occurrence of #m*u from the term list*) |
46 (*Remove the first occurrence of #m*u from the term list*) |
63 | NONE => find_repeated (Termtab.update (u, n) tab, |
63 | NONE => find_repeated (Termtab.update (u, n) tab, |
64 t::past, terms)) |
64 t::past, terms)) |
65 | NONE => find_repeated (tab, t::past, terms); |
65 | NONE => find_repeated (tab, t::past, terms); |
66 |
66 |
67 (*the simplification procedure*) |
67 (*the simplification procedure*) |
68 fun proc ss t = |
68 fun proc ctxt t = |
69 let |
69 let |
70 val ctxt = Simplifier.the_context ss; |
|
71 val ([t'], ctxt') = Variable.import_terms true [t] ctxt |
70 val ([t'], ctxt') = Variable.import_terms true [t] ctxt |
72 val export = singleton (Variable.export ctxt' ctxt) |
71 val export = singleton (Variable.export ctxt' ctxt) |
|
72 (* FIXME ctxt vs. ctxt' (!?) *) |
73 |
73 |
74 val (u,m,n,terms) = find_repeated (Termtab.empty, [], Data.dest_sum t') |
74 val (u,m,n,terms) = find_repeated (Termtab.empty, [], Data.dest_sum t') |
75 val T = Term.fastype_of u |
75 val T = Term.fastype_of u |
76 |
76 |
77 val reshape = (*Move i*u to the front and put j*u into standard form |
77 val reshape = (*Move i*u to the front and put j*u into standard form |
78 i + #m + j + k == #m + i + (j + k) *) |
78 i + #m + j + k == #m + i + (j + k) *) |
79 if Data.iszero m orelse Data.iszero n then (*trivial, so do nothing*) |
79 if Data.iszero m orelse Data.iszero n then (*trivial, so do nothing*) |
80 raise TERM("combine_numerals", []) |
80 raise TERM("combine_numerals", []) |
81 else Data.prove_conv [Data.norm_tac ss] ctxt |
81 else Data.prove_conv [Data.norm_tac ctxt] ctxt |
82 (t', Data.mk_sum T ([Data.mk_coeff (m, u), Data.mk_coeff (n, u)] @ terms)) |
82 (t', Data.mk_sum T ([Data.mk_coeff (m, u), Data.mk_coeff (n, u)] @ terms)) |
83 in |
83 in |
84 Option.map (export o Data.simplify_meta_eq ss) |
84 Option.map (export o Data.simplify_meta_eq ctxt) |
85 (Data.prove_conv |
85 (Data.prove_conv |
86 [Data.trans_tac reshape, rtac Data.left_distrib 1, |
86 [Data.trans_tac reshape, rtac Data.left_distrib 1, |
87 Data.numeral_simp_tac ss] ctxt |
87 Data.numeral_simp_tac ctxt] ctxt |
88 (t', Data.mk_sum T (Data.mk_coeff(Data.add(m,n), u) :: terms))) |
88 (t', Data.mk_sum T (Data.mk_coeff(Data.add(m,n), u) :: terms))) |
89 end |
89 end |
90 (* FIXME avoid handling of generic exceptions *) |
90 (* FIXME avoid handling of generic exceptions *) |
91 handle TERM _ => NONE |
91 handle TERM _ => NONE |
92 | TYPE _ => NONE; (*Typically (if thy doesn't include Numeral) |
92 | TYPE _ => NONE; (*Typically (if thy doesn't include Numeral) |