67 (*the simplification procedure*) |
67 (*the simplification procedure*) |
68 fun proc ctxt ct = |
68 fun proc ctxt ct = |
69 let |
69 let |
70 val t = Thm.term_of ct |
70 val t = Thm.term_of ct |
71 val ([t'], ctxt') = Variable.import_terms true [t] ctxt |
71 val ([t'], ctxt') = Variable.import_terms true [t] ctxt |
72 val export = singleton (Variable.export ctxt' ctxt) |
|
73 (* FIXME ctxt vs. ctxt' (!?) *) |
|
74 |
72 |
75 val (u,m,n,terms) = find_repeated (Termtab.empty, [], Data.dest_sum t') |
73 val (u,m,n,terms) = find_repeated (Termtab.empty, [], Data.dest_sum t') |
76 val T = Term.fastype_of u |
74 val T = Term.fastype_of u |
77 |
75 |
78 val reshape = (*Move i*u to the front and put j*u into standard form |
76 val reshape = (*Move i*u to the front and put j*u into standard form |
79 i + #m + j + k == #m + i + (j + k) *) |
77 i + #m + j + k == #m + i + (j + k) *) |
80 if Data.iszero m orelse Data.iszero n then (*trivial, so do nothing*) |
78 if Data.iszero m orelse Data.iszero n then (*trivial, so do nothing*) |
81 raise TERM("combine_numerals", []) |
79 raise TERM("combine_numerals", []) |
82 else Data.prove_conv [Data.norm_tac ctxt] ctxt |
80 else Data.prove_conv [Data.norm_tac ctxt'] ctxt' |
83 (t', Data.mk_sum T ([Data.mk_coeff (m, u), Data.mk_coeff (n, u)] @ terms)) |
81 (t', Data.mk_sum T ([Data.mk_coeff (m, u), Data.mk_coeff (n, u)] @ terms)) |
84 in |
82 in |
85 Option.map (export o Data.simplify_meta_eq ctxt) |
83 Option.map (singleton (Variable.export ctxt' ctxt) o Data.simplify_meta_eq ctxt') |
86 (Data.prove_conv |
84 (Data.prove_conv |
87 [Data.trans_tac ctxt reshape, resolve_tac ctxt [Data.left_distrib] 1, |
85 [Data.trans_tac ctxt' reshape, resolve_tac ctxt' [Data.left_distrib] 1, |
88 Data.numeral_simp_tac ctxt] ctxt |
86 Data.numeral_simp_tac ctxt'] ctxt' |
89 (t', Data.mk_sum T (Data.mk_coeff(Data.add(m,n), u) :: terms))) |
87 (t', Data.mk_sum T (Data.mk_coeff(Data.add(m,n), u) :: terms))) |
90 end |
88 end |
91 (* FIXME avoid handling of generic exceptions *) |
89 (* FIXME avoid handling of generic exceptions *) |
92 handle TERM _ => NONE |
90 handle TERM _ => NONE |
93 | TYPE _ => NONE; (*Typically (if thy doesn't include Numeral) |
91 | TYPE _ => NONE; (*Typically (if thy doesn't include Numeral) |