68 fun proc ctxt ct = |
68 fun proc ctxt ct = |
69 let |
69 let |
70 val prems = Simplifier.prems_of ctxt |
70 val prems = Simplifier.prems_of ctxt |
71 val t = Thm.term_of ct |
71 val t = Thm.term_of ct |
72 val ([t'], ctxt') = Variable.import_terms true [t] ctxt |
72 val ([t'], ctxt') = Variable.import_terms true [t] ctxt |
73 val export = singleton (Variable.export ctxt' ctxt) |
|
74 (* FIXME ctxt vs. ctxt' (!?) *) |
|
75 |
73 |
76 val (t1,t2) = Data.dest_bal t' |
74 val (t1,t2) = Data.dest_bal t' |
77 val terms1 = Data.dest_sum t1 |
75 val terms1 = Data.dest_sum t1 |
78 and terms2 = Data.dest_sum t2 |
76 and terms2 = Data.dest_sum t2 |
79 |
77 |
85 fun newshape (i,terms) = Data.mk_sum T (Data.mk_coeff(i,u)::terms) |
83 fun newshape (i,terms) = Data.mk_sum T (Data.mk_coeff(i,u)::terms) |
86 val reshape = (*Move i*u to the front and put j*u into standard form |
84 val reshape = (*Move i*u to the front and put j*u into standard form |
87 i + #m + j + k == #m + i + (j + k) *) |
85 i + #m + j + k == #m + i + (j + k) *) |
88 if n1=0 orelse n2=0 then (*trivial, so do nothing*) |
86 if n1=0 orelse n2=0 then (*trivial, so do nothing*) |
89 raise TERM("cancel_numerals", []) |
87 raise TERM("cancel_numerals", []) |
90 else Data.prove_conv [Data.norm_tac ctxt] ctxt prems |
88 else Data.prove_conv [Data.norm_tac ctxt'] ctxt' prems |
91 (t', Data.mk_bal (newshape(n1,terms1'), newshape(n2,terms2'))) |
89 (t', Data.mk_bal (newshape(n1,terms1'), newshape(n2,terms2'))) |
92 in |
90 in |
93 Option.map (export o Data.simplify_meta_eq ctxt) |
91 Option.map (singleton (Variable.export ctxt' ctxt) o Data.simplify_meta_eq ctxt') |
94 (if n2 <= n1 then |
92 (if n2 <= n1 then |
95 Data.prove_conv |
93 Data.prove_conv |
96 [Data.trans_tac ctxt reshape, resolve_tac ctxt [Data.bal_add1] 1, |
94 [Data.trans_tac ctxt' reshape, resolve_tac ctxt' [Data.bal_add1] 1, |
97 Data.numeral_simp_tac ctxt] ctxt prems |
95 Data.numeral_simp_tac ctxt'] ctxt' prems |
98 (t', Data.mk_bal (newshape(n1-n2,terms1'), Data.mk_sum T terms2')) |
96 (t', Data.mk_bal (newshape(n1-n2,terms1'), Data.mk_sum T terms2')) |
99 else |
97 else |
100 Data.prove_conv |
98 Data.prove_conv |
101 [Data.trans_tac ctxt reshape, resolve_tac ctxt [Data.bal_add2] 1, |
99 [Data.trans_tac ctxt' reshape, resolve_tac ctxt' [Data.bal_add2] 1, |
102 Data.numeral_simp_tac ctxt] ctxt prems |
100 Data.numeral_simp_tac ctxt'] ctxt' prems |
103 (t', Data.mk_bal (Data.mk_sum T terms1', newshape(n2-n1,terms2')))) |
101 (t', Data.mk_bal (Data.mk_sum T terms1', newshape(n2-n1,terms2')))) |
104 end |
102 end |
105 (* FIXME avoid handling of generic exceptions *) |
103 (* FIXME avoid handling of generic exceptions *) |
106 handle TERM _ => NONE |
104 handle TERM _ => NONE |
107 | TYPE _ => NONE; (*Typically (if thy doesn't include Numeral) |
105 | TYPE _ => NONE; (*Typically (if thy doesn't include Numeral) |